proofs/lib/lemmas/spec/public_commands.bend
bend-collections-laws-containers@1.0.0.0 · 115 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/operations.bend as O
5import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/spec/clock.bend as Clock
6import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/spec/effectful_operations.bend as E
7import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/spec/effectful_aggregate.bend as A
8
9# Public callback-free observations. Metrics' storage-dependent Collisions field
10# is always the documented zero/not-applicable adaptation. Diagnostics describe
11# the abstract bound-entry count; refinement establishes the native leaf count.
12type Reply<-K: Data, -V: Data> is Data:
13 NoReply{}
14 Boolean{value: Bool}
15 Value{value: V, found: Bool}
16 Oldest{key: K, value: V, found: Bool}
17 KeyList{keys: List<&2, K>}
18 ValueList{values: List<&2, V>}
19 Length{length: Nat}
20 Counters{metrics: T.Metrics}
21 Storage{leaves: Nat, recency: Nat, capacity: Nat, metrics: T.Metrics}
22
23type CmdResult<-K: Data, -V: Data> is Data:
24 Returned{state: S.Model<K, V>, reply: Reply<K, V>, remaining: List<&2, Clock.ClockEvent>, requests: Nat}
25 Failed{state: S.Model<K, V>, error: Clock.Error, remaining: List<&2, Clock.ClockEvent>, requests: Nat}
26
27type Projection<-K: Data> is Data:
28 Flag{}
29 ValueOnly{}
30 RemovedOldest{}
31 CapturedOldest{key: K}
32 Nothing{}
33 Keys{}
34 Values{}
35
36def value(-K: Data, -V: Data, zero: V, item: Maybe<&2, T.Entry<K, V>>, present: Bool) -> V:
37 match item present:
38 case Some{T.Item{k, v, d}} True{}: v
39 case x y: zero
40
41def key(-K: Data, -V: Data, zero: K, item: Maybe<&2, T.Entry<K, V>>, present: Bool) -> K:
42 match item present:
43 case Some{T.Item{k, v, d}} True{}: k
44 case x y: zero
45
46def project(~K: Data, ~same: K -> K -> Bool, -V: Data, s: S.Model<K, V>, zero_key: K, zero_value: V, +item: Maybe<&2, T.Entry<K, V>>, +present: Bool, kind: Projection<K>) -> Reply<K, V>:
47 match kind:
48 case Flag{}: Boolean{present}
49 case ValueOnly{}: Value{value(K, V, zero_value, item, present), present}
50 case RemovedOldest{}: Oldest{key(K, V, zero_key, item, present), value(K, V, zero_value, item, present), present}
51 case CapturedOldest{captured}: Oldest{captured, value(K, V, zero_value, item, present), present}
52 case Nothing{}: NoReply{}
53 case Keys{}: KeyList{O.entry_keys(K, V, O.all_entries(~K, ~same, V, s))}
54 case Values{}: ValueList{O.entry_values(K, V, O.all_entries(~K, ~same, V, s))}
55
56def observation(~K: Data, ~same: K -> K -> Bool, -V: Data, zero_key: K, zero_value: V, kind: Projection<K>, observed: S.Observation<K, V>, events: List<&2, Clock.ClockEvent>, requests: Nat) -> CmdResult<K, V>:
57 S.Observed{+s, item, present, ignored} = observed
58 Returned{s, project(~K, ~same, V, s, zero_key, zero_value, item, present, kind), events, requests}
59
60def effect(~K: Data, ~same: K -> K -> Bool, -V: Data, zero_key: K, zero_value: V, kind: Projection<K>, outcome: E.Outcome<K, V>) -> CmdResult<K, V>:
61 match outcome:
62 case E.Failed{s, error, events, requests}: Failed{s, error, events, requests}
63 case E.Returned{observed, events, requests}: observation(~K, ~same, V, zero_key, zero_value, kind, observed, events, requests)
64
65def oldest_binding(~K: Data, ~same: K -> K -> Bool, -V: Data, s: S.Model<K, V>, zero_key: K, zero_value: V, events: List<&2, Clock.ClockEvent>, found: Maybe<&2, T.Entry<K, V>>) -> CmdResult<K, V>:
66 match found:
67 case None{}: Returned{s, Oldest{zero_key, zero_value, False{}}, events, 0n}
68 case Some{T.Item{+original, v, d}}: effect(~K, ~same, V, zero_key, zero_value, CapturedOldest{original}, E.read(~K, ~same, V, s, original, False{}, events))
69
70def oldest_order(~K: Data, ~same: K -> K -> Bool, -V: Data, s: S.Model<K, V>, bindings: List<&2, T.Entry<K, V>>, order: List<&2, K>, zero_key: K, zero_value: V, events: List<&2, Clock.ClockEvent>) -> CmdResult<K, V>:
71 match order:
72 case Nil{}: Returned{s, Oldest{zero_key, zero_value, False{}}, events, 0n}
73 case Con{first, tail}: oldest_binding(~K, ~same, V, s, zero_key, zero_value, events, S.find(~K, ~same, V, bindings, first))
74
75def oldest(~K: Data, ~same: K -> K -> Bool, -V: Data, +s: S.Model<K, V>, zero_key: K, zero_value: V, events: List<&2, Clock.ClockEvent>) -> CmdResult<K, V>:
76 S.Abstract{cap, bindings, order, life, counts, cb} = s
77 oldest_order(~K, ~same, V, s, bindings, order, zero_key, zero_value, events)
78
79def metrics(-K: Data, -V: Data, +s: S.Model<K, V>, events: List<&2, Clock.ClockEvent>) -> CmdResult<K, V>:
80 S.Abstract{cap, bindings, order, life, counts, cb} = s
81 Returned{s, Counters{counts}, events, 0n}
82
83def reset(-K: Data, -V: Data, s: S.Model<K, V>, events: List<&2, Clock.ClockEvent>) -> CmdResult<K, V>:
84 S.Abstract{cap, bindings, order, life, counts, cb} = s
85 Returned{S.Abstract{cap, bindings, order, life, T.zero_metrics(), cb}, Counters{counts}, events, 0n}
86
87# Leaves counts the bound keys of the abstract finite map (the entries reachable
88# through the recency list); it is independent of binding-list storage order.
89def diagnostics(~K: Data, ~same: K -> K -> Bool, -V: Data, +s: S.Model<K, V>, events: List<&2, Clock.ClockEvent>) -> CmdResult<K, V>:
90 S.Abstract{cap, bindings, order, life, counts, cb} = s
91 Returned{s, Storage{List.length(&2, T.Entry<K, V>, O.all_entries(~K, ~same, V, s)), List.length(&2, K, order), cap, counts}, events, 0n}
92
93# All typed commands have explicit independent semantics. Invalid transport and
94# rejected host arguments need a separate marshalling relation; they are not
95# silently coerced into one of these legal typed commands.
96def execute(~K: Data, ~same: K -> K -> Bool, -V: Data, +s: S.Model<K, V>, zero_key: K, zero_value: V, events: List<&2, Clock.ClockEvent>, command: S.Command<K, V>) -> CmdResult<K, V>:
97 match command:
98 case S.Add{k, v}: effect(~K, ~same, V, zero_key, zero_value, Flag{}, E.add(~K, ~same, V, s, k, v, events))
99 case S.AddWithLifetime{k, v, ns}: effect(~K, ~same, V, zero_key, zero_value, Flag{}, E.add_with_lifetime(~K, ~same, V, s, k, v, ns, events))
100 case S.Get{k}: effect(~K, ~same, V, zero_key, zero_value, ValueOnly{}, E.read(~K, ~same, V, s, k, True{}, events))
101 case S.GetAndRefresh{k, ns}: effect(~K, ~same, V, zero_key, zero_value, ValueOnly{}, E.refresh(~K, ~same, V, s, k, ns, events))
102 case S.Peek{k}: effect(~K, ~same, V, zero_key, zero_value, ValueOnly{}, E.read(~K, ~same, V, s, k, False{}, events))
103 case S.Contains{k}: effect(~K, ~same, V, zero_key, zero_value, Flag{}, E.read(~K, ~same, V, s, k, False{}, events))
104 case S.Remove{k}: observation(~K, ~same, V, zero_key, zero_value, Flag{}, S.remove(~K, ~same, V, s, k), events, 0n)
105 case S.RemoveOldest{}: observation(~K, ~same, V, zero_key, zero_value, RemovedOldest{}, O.remove_oldest(~K, ~same, V, s), events, 0n)
106 case S.GetOldest{}: oldest(~K, ~same, V, s, zero_key, zero_value, events)
107 case S.Keys{}: effect(~K, ~same, V, zero_key, zero_value, Keys{}, A.purge_expired(~K, ~same, V, s, events))
108 case S.Values{}: effect(~K, ~same, V, zero_key, zero_value, Values{}, A.purge_expired(~K, ~same, V, s, events))
109 case S.PurgeExpired{}: effect(~K, ~same, V, zero_key, zero_value, Nothing{}, A.purge_expired(~K, ~same, V, s, events))
110 case S.Purge{}: Returned{S.purged(K, V, s), NoReply{}, events, 0n}
111 case S.Len{}: Returned{s, Length{S.length(K, V, s)}, events, 0n}
112 case S.SetLifetime{ns}: Returned{S.set_lifetime(K, V, s, ns), NoReply{}, events, 0n}
113 case S.Metrics{}: metrics(K, V, s, events)
114 case S.ResetMetrics{}: reset(K, V, s, events)
115 case S.Diagnostics{}: diagnostics(~K, ~same, V, s, events)