proofs/lib/lemmas/spec/traces.bend

bend-collections-laws-containers@1.0.0.0 · 36 lines · 0 definitions

1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/types/model.bend as T
3import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/spec/cache.bend as S
4import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/spec/clock.bend as Clock
5import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/spec/public_commands.bend as P
6
7# A caller may catch a failure and issue the next command. Each result retains
8# the partial state and exact unused provider events. No failure becomes success.
9type Trace<-K: Data, -V: Data> is Data:
10  Finished{state: S.Model<K, V>, remaining: List<&2, Clock.ClockEvent>, observations: List<&2, P.CmdResult<K, V>>, requests: Nat}
11
12def state(-K: Data, -V: Data, result: P.CmdResult<K, V>) -> S.Model<K, V>:
13  match result:
14    case P.Returned{s, reply, events, count}: s
15    case P.Failed{s, error, events, count}: s
16
17def remaining(-K: Data, -V: Data, result: P.CmdResult<K, V>) -> List<&2, Clock.ClockEvent>:
18  match result:
19    case P.Returned{s, reply, events, count}: events
20    case P.Failed{s, error, events, count}: events
21
22def requests(-K: Data, -V: Data, result: P.CmdResult<K, V>) -> Nat:
23  match result:
24    case P.Returned{s, reply, events, count}: count
25    case P.Failed{s, error, events, count}: count
26
27def prepend(-K: Data, -V: Data, +result: P.CmdResult<K, V>, rest: Trace<K, V>) -> Trace<K, V>:
28  Finished{s, events, observations, count} = rest
29  Finished{s, events, Con{result, observations}, Nat.add(requests(K, V, result), count)}
30
31def run(~K: Data, ~same: K -> K -> Bool, -V: Data, commands: List<&2, S.Command<K, V>>, s: S.Model<K, V>, +zero_key: K, +zero_value: V, events: List<&2, Clock.ClockEvent>) -> Trace<K, V>:
32  match commands:
33    case Nil{}: Finished{s, events, Nil{}, 0n}
34    case Con{command, tail}:
35      +result = P.execute(~K, ~same, V, s, zero_key, zero_value, events, command)
36      prepend(K, V, result, run(~K, ~same, V, tail, state(K, V, result), zero_key, zero_value, remaining(K, V, result)))