proofs/lib/lemmas/src/driver.bend
bend-collections-laws-containers@1.0.0.0 · 72 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/clock.bend as Clock
4import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/src/cache.bend as C
5import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/src/public.bend as Pub
6
7# Deterministic model of the host clock loop over an explicit provider-event
8# list. Only the neutral Clock.ClockEvent/Clock.Error datatypes are imported from the
9# clock specification; no specification function is used. The adapter runs
10# this machine through src/host.bend begin/answer (proofs/host_loop.bend).
11type Outcome<-K: Data, -V: Data> is Data:
12 Returned{cache: C.Cache<K, V>, answer: Pub.Answer<K, V>, remaining: List<&2, Clock.ClockEvent>, requests: Nat}
13 Failed{cache: C.Cache<K, V>, error: Clock.Error, remaining: List<&2, Clock.ClockEvent>, requests: Nat}
14
15def bump(-K: Data, -V: Data, outcome: Outcome<K, V>) -> Outcome<K, V>:
16 match outcome:
17 case Returned{c, answer, events, requests}: Returned{c, answer, events, 1n+requests}
18 case Failed{c, error, events, requests}: Failed{c, error, events, 1n+requests}
19
20# One step: the provider event answering a Waiting progress either resumes the
21# machine or stops it with the retained state and the error. drive is its
22# iteration (drive_advance in END_TO_END.bend); src/host.bend answer uses it.
23type Step<-K: Data, -V: Data> is Data:
24 Continue{progress: Pub.Progress<K, V>}
25 Stopped{cache: C.Cache<K, V>, error: Clock.Error}
26
27def advance(-K: Data, -V: Data, zero_value: V, pending: Pub.Pending<K, V>, event: Clock.ClockEvent) -> Step<K, V>:
28 match event:
29 case Clock.Sample{now}: Continue{Pub.resume(K, V, zero_value, pending, now)}
30 case Clock.InvalidSample{reason}: Stopped{Pub.abandon(K, V, pending), Clock.Invalid{reason}}
31 case Clock.ProviderException{reason}: Stopped{Pub.abandon(K, V, pending), Clock.Thrown{reason}}
32
33def drive(-K: Data, -V: Data, +zero_value: V, events: List<&2, Clock.ClockEvent>, progress: Pub.Progress<K, V>) -> Outcome<K, V>:
34 match events progress:
35 case remaining Pub.Finished{c, answer}: Returned{c, answer, remaining, 0n}
36 case Nil{} Pub.Waiting{pending}: Failed{Pub.abandon(K, V, pending), Clock.Exhausted{}, Nil{}, 1n}
37 case Con{Clock.InvalidSample{reason}, tail} Pub.Waiting{pending}: Failed{Pub.abandon(K, V, pending), Clock.Invalid{reason}, tail, 1n}
38 case Con{Clock.ProviderException{reason}, tail} Pub.Waiting{pending}: Failed{Pub.abandon(K, V, pending), Clock.Thrown{reason}, tail, 1n}
39 case Con{Clock.Sample{now}, tail} Pub.Waiting{pending}: bump(K, V, drive(K, V, zero_value, tail, Pub.resume(K, V, zero_value, pending, now)))
40
41def execute(~K: Data, ~encode: K -> String, -V: Data, zero_key: K, +zero_value: V, c: C.Cache<K, V>, events: List<&2, Clock.ClockEvent>, request: Pub.Request<K, V>) -> Outcome<K, V>:
42 drive(K, V, zero_value, events, Pub.start(K, V, encode, zero_key, zero_value, c, request))
43
44def cache(-K: Data, -V: Data, outcome: Outcome<K, V>) -> C.Cache<K, V>:
45 match outcome:
46 case Returned{c, answer, events, requests}: c
47 case Failed{c, error, events, requests}: c
48
49def remaining(-K: Data, -V: Data, outcome: Outcome<K, V>) -> List<&2, Clock.ClockEvent>:
50 match outcome:
51 case Returned{c, answer, events, requests}: events
52 case Failed{c, error, events, requests}: events
53
54def requests(-K: Data, -V: Data, outcome: Outcome<K, V>) -> Nat:
55 match outcome:
56 case Returned{c, answer, events, count}: count
57 case Failed{c, error, events, count}: count
58
59# A caller may catch a failed command and continue from the retained state.
60type Trace<-K: Data, -V: Data> is Data:
61 Ran{cache: C.Cache<K, V>, remaining: List<&2, Clock.ClockEvent>, outcomes: List<&2, Outcome<K, V>>, requests: Nat}
62
63def prepend(-K: Data, -V: Data, +outcome: Outcome<K, V>, rest: Trace<K, V>) -> Trace<K, V>:
64 Ran{c, events, outcomes, count} = rest
65 Ran{c, events, Con{outcome, outcomes}, Nat.add(requests(K, V, outcome), count)}
66
67def run(~K: Data, ~encode: K -> String, -V: Data, requests: List<&2, Pub.Request<K, V>>, c: C.Cache<K, V>, +zero_key: K, +zero_value: V, events: List<&2, Clock.ClockEvent>) -> Trace<K, V>:
68 match requests:
69 case Nil{}: Ran{c, events, Nil{}, 0n}
70 case Con{request, tail}:
71 +outcome = execute(~K, ~encode, V, zero_key, zero_value, c, events, request)
72 prepend(K, V, outcome, run(~K, ~encode, V, tail, cache(K, V, outcome), zero_key, zero_value, remaining(K, V, outcome)))