proofs/lib/lemmas/spec/effectful_aggregate.bend
bend-collections-laws-containers@1.0.0.0 · 48 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/spec/cache.bend as S
5import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as N
6import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/spec/operations.bend as O
7import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/spec/effectful_operations.bend as E
8
9# Ordered abstract bindings, not implementation fuel or native Map traversal.
10# Every successful removal is retained even when the next provider event fails.
11type Prefix<-K: Data, -V: Data> is Data:
12 Finished{removed: List<&2, T.Entry<K, V>>, retained: List<&2, T.Entry<K, V>>, remaining: List<&2, Clock.ClockEvent>, requests: Nat}
13 Failed{error: Clock.Error, removed: List<&2, T.Entry<K, V>>, retained: List<&2, T.Entry<K, V>>, remaining: List<&2, Clock.ClockEvent>, requests: Nat}
14
15def prepend(-K: Data, -V: Data, entry: T.Entry<K, V>, result: Prefix<K, V>) -> Prefix<K, V>:
16 match result:
17 case Finished{removed, retained, events, requests}: Finished{Con{entry, removed}, retained, events, 1n+requests}
18 case Failed{error, removed, retained, events, requests}: Failed{error, Con{entry, removed}, retained, events, 1n+requests}
19
20def decide(-K: Data, -V: Data, entry: T.Entry<K, V>, tail: List<&2, T.Entry<K, V>>, events: List<&2, Clock.ClockEvent>, rest: Prefix<K, V>, expired: Bool) -> Prefix<K, V>:
21 match expired:
22 case False{}: Finished{Nil{}, Con{entry, tail}, events, 1n}
23 case True{}: prepend(K, V, entry, rest)
24
25def sentinel(-K: Data, -V: Data, entry: T.Entry<K, V>, tail: List<&2, T.Entry<K, V>>, events: List<&2, Clock.ClockEvent>, result: Prefix<K, V>, immortal: Bool) -> Prefix<K, V>:
26 match immortal:
27 case True{}: Finished{Nil{}, Con{entry, tail}, events, 0n}
28 case False{}: result
29
30def prefix(-K: Data, -V: Data, ordered: List<&2, T.Entry<K, V>>, events: List<&2, Clock.ClockEvent>) -> Prefix<K, V>:
31 match ordered events:
32 case Nil{} remaining: Finished{Nil{}, Nil{}, remaining, 0n}
33 case Con{T.Item{+key, +value, T.I64{+bits}}, +tail} Nil{}:
34 sentinel(K, V, T.Item{key, value, T.I64{bits}}, tail, Nil{}, Failed{Clock.Exhausted{}, Nil{}, Con{T.Item{key, value, T.I64{bits}}, tail}, Nil{}, 1n}, N.zero(bits))
35 case Con{T.Item{+key, +value, T.I64{+bits}}, +tail} Con{Clock.InvalidSample{+reason}, +remaining}:
36 sentinel(K, V, T.Item{key, value, T.I64{bits}}, tail, Con{Clock.InvalidSample{reason}, remaining}, Failed{Clock.Invalid{reason}, Nil{}, Con{T.Item{key, value, T.I64{bits}}, tail}, remaining, 1n}, N.zero(bits))
37 case Con{T.Item{+key, +value, T.I64{+bits}}, +tail} Con{Clock.ProviderException{+reason}, +remaining}:
38 sentinel(K, V, T.Item{key, value, T.I64{bits}}, tail, Con{Clock.ProviderException{reason}, remaining}, Failed{Clock.Thrown{reason}, Nil{}, Con{T.Item{key, value, T.I64{bits}}, tail}, remaining, 1n}, N.zero(bits))
39 case Con{T.Item{+key, +value, T.I64{+bits}}, +tail} Con{Clock.Sample{+now}, +remaining}:
40 sentinel(K, V, T.Item{key, value, T.I64{bits}}, tail, Con{Clock.Sample{now}, remaining}, decide(K, V, T.Item{key, value, T.I64{bits}}, tail, remaining, prefix(K, V, tail, remaining), N.expired(T.I64{bits}, now)), N.zero(bits))
41
42def apply_prefix(~K: Data, ~same: K -> K -> Bool, -V: Data, s: S.Model<K, V>, result: Prefix<K, V>) -> E.Outcome<K, V>:
43 match result:
44 case Finished{removed, retained, events, requests}: E.Returned{S.Observed{O.remove_entries(~K, ~same, V, removed, s), None{}, False{}, Nil{}}, events, requests}
45 case Failed{error, removed, retained, events, requests}: E.Failed{O.remove_entries(~K, ~same, V, removed, s), error, events, requests}
46
47def purge_expired(~K: Data, ~same: K -> K -> Bool, -V: Data, +s: S.Model<K, V>, events: List<&2, Clock.ClockEvent>) -> E.Outcome<K, V>:
48 apply_prefix(~K, ~same, V, s, prefix(K, V, O.all_entries(~K, ~same, V, s), events))