proofs/lib/lemmas/spec/public_commands.bend source
proofs/lib/lemmas/spec/public_commands.bend on the hub · documented module
import Baseimport ../types/model.bend as Timport ./cache.bend as Simport ./operations.bend as Oimport ./clock.bend as Clockimport ./effectful_operations.bend as Eimport ./effectful_aggregate.bend as A# Public callback-free observations. Metrics' storage-dependent Collisions field# is always the documented zero/not-applicable adaptation. Diagnostics describe# the abstract bound-entry count; refinement establishes the native leaf count.type Reply<-K: Data, -V: Data> is Data: NoReply{} Boolean{value: Bool} Value{value: V, found: Bool} Oldest{key: K, value: V, found: Bool} KeyList{keys: List<&2, K>} ValueList{values: List<&2, V>} Length{length: Nat} Counters{metrics: T.Metrics} Storage{leaves: Nat, recency: Nat, capacity: Nat, metrics: T.Metrics}type CmdResult<-K: Data, -V: Data> is Data: Returned{state: S.Model<K, V>, reply: Reply<K, V>, remaining: List<&2, Clock.ClockEvent>, requests: Nat} Failed{state: S.Model<K, V>, error: Clock.Error, remaining: List<&2, Clock.ClockEvent>, requests: Nat}type Projection<-K: Data> is Data: Flag{} ValueOnly{} RemovedOldest{} CapturedOldest{key: K} Nothing{} Keys{} Values{}def value(-K: Data, -V: Data, zero: V, item: Maybe<&2, T.Entry<K, V>>, present: Bool) -> V: match item present: case Some{T.Item{k, v, d}} True{}: v case x y: zerodef key(-K: Data, -V: Data, zero: K, item: Maybe<&2, T.Entry<K, V>>, present: Bool) -> K: match item present: case Some{T.Item{k, v, d}} True{}: k case x y: zerodef 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>: match kind: case Flag{}: Boolean{present} case ValueOnly{}: Value{value(K, V, zero_value, item, present), present} case RemovedOldest{}: Oldest{key(K, V, zero_key, item, present), value(K, V, zero_value, item, present), present} case CapturedOldest{captured}: Oldest{captured, value(K, V, zero_value, item, present), present} case Nothing{}: NoReply{} case Keys{}: KeyList{O.entry_keys(K, V, O.all_entries(~K, ~same, V, s))} case Values{}: ValueList{O.entry_values(K, V, O.all_entries(~K, ~same, V, s))}def 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>: S.Observed{+s, item, present, ignored} = observed Returned{s, project(~K, ~same, V, s, zero_key, zero_value, item, present, kind), events, requests}def 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>: match outcome: case E.Failed{s, error, events, requests}: Failed{s, error, events, requests} case E.Returned{observed, events, requests}: observation(~K, ~same, V, zero_key, zero_value, kind, observed, events, requests)def 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>: match found: case None{}: Returned{s, Oldest{zero_key, zero_value, False{}}, events, 0n} 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))def 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>: match order: case Nil{}: Returned{s, Oldest{zero_key, zero_value, False{}}, events, 0n} case Con{first, tail}: oldest_binding(~K, ~same, V, s, zero_key, zero_value, events, S.find(~K, ~same, V, bindings, first))def 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>: S.Abstract{cap, bindings, order, life, counts, cb} = s oldest_order(~K, ~same, V, s, bindings, order, zero_key, zero_value, events)def metrics(-K: Data, -V: Data, +s: S.Model<K, V>, events: List<&2, Clock.ClockEvent>) -> CmdResult<K, V>: S.Abstract{cap, bindings, order, life, counts, cb} = s Returned{s, Counters{counts}, events, 0n}def reset(-K: Data, -V: Data, s: S.Model<K, V>, events: List<&2, Clock.ClockEvent>) -> CmdResult<K, V>: S.Abstract{cap, bindings, order, life, counts, cb} = s Returned{S.Abstract{cap, bindings, order, life, T.zero_metrics(), cb}, Counters{counts}, events, 0n}# Leaves counts the bound keys of the abstract finite map (the entries reachable# through the recency list); it is independent of binding-list storage order.def diagnostics(~K: Data, ~same: K -> K -> Bool, -V: Data, +s: S.Model<K, V>, events: List<&2, Clock.ClockEvent>) -> CmdResult<K, V>: S.Abstract{cap, bindings, order, life, counts, cb} = s 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}# All typed commands have explicit independent semantics. Invalid transport and# rejected host arguments need a separate marshalling relation; they are not# silently coerced into one of these legal typed commands.def 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>: match command: case S.Add{k, v}: effect(~K, ~same, V, zero_key, zero_value, Flag{}, E.add(~K, ~same, V, s, k, v, events)) 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)) case S.Get{k}: effect(~K, ~same, V, zero_key, zero_value, ValueOnly{}, E.read(~K, ~same, V, s, k, True{}, events)) case S.GetAndRefresh{k, ns}: effect(~K, ~same, V, zero_key, zero_value, ValueOnly{}, E.refresh(~K, ~same, V, s, k, ns, events)) case S.Peek{k}: effect(~K, ~same, V, zero_key, zero_value, ValueOnly{}, E.read(~K, ~same, V, s, k, False{}, events)) case S.Contains{k}: effect(~K, ~same, V, zero_key, zero_value, Flag{}, E.read(~K, ~same, V, s, k, False{}, events)) case S.Remove{k}: observation(~K, ~same, V, zero_key, zero_value, Flag{}, S.remove(~K, ~same, V, s, k), events, 0n) case S.RemoveOldest{}: observation(~K, ~same, V, zero_key, zero_value, RemovedOldest{}, O.remove_oldest(~K, ~same, V, s), events, 0n) case S.GetOldest{}: oldest(~K, ~same, V, s, zero_key, zero_value, events) case S.Keys{}: effect(~K, ~same, V, zero_key, zero_value, Keys{}, A.purge_expired(~K, ~same, V, s, events)) case S.Values{}: effect(~K, ~same, V, zero_key, zero_value, Values{}, A.purge_expired(~K, ~same, V, s, events)) case S.PurgeExpired{}: effect(~K, ~same, V, zero_key, zero_value, Nothing{}, A.purge_expired(~K, ~same, V, s, events)) case S.Purge{}: Returned{S.purged(K, V, s), NoReply{}, events, 0n} case S.Len{}: Returned{s, Length{S.length(K, V, s)}, events, 0n} case S.SetLifetime{ns}: Returned{S.set_lifetime(K, V, s, ns), NoReply{}, events, 0n} case S.Metrics{}: metrics(K, V, s, events) case S.ResetMetrics{}: reset(K, V, s, events) case S.Diagnostics{}: diagnostics(~K, ~same, V, s, events)