proofs/lib/lemmas/spec/equivalence.bend
bend-collections-laws-containers@1.0.0.0 · 50 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/spec/cache.bend as S
3import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/types/model.bend as T
4
5# Extensional finite-map equality deliberately ignores binding-list storage
6# order. It preserves every queried entry (original key, value and deadline),
7# exact observable recency, capacity, configuration, metrics and inert metadata.
8# This is independent of the implementation and its abstraction function.
9#
10# Two models are related when their canonical forms are equal. The canonical
11# form keeps every non-binding field exactly and replaces the binding list by
12# (1) the lookup result at each recency key, in recency order, and (2) the
13# bindings whose key is not in the recency list ("stray", normally empty), in
14# list order. With a key equality that reflects equality, related models agree
15# on S.find for EVERY key (proofs/canonical.bend, lookup_agreement). Unlike a
16# pointwise function premise, this is one reusable equality proof.
17type Canonical<-K: Data, -V: Data> is Data:
18 Canon{capacity: Nat, recency: List<&2, K>, lifetime: T.Int64, counts: T.Metrics, callback: Bool, lookups: List<&2, Maybe<&2, T.Entry<K, V>>>, stray: List<&2, T.Entry<K, V>>}
19
20def lookups(~K: Data, ~same: K -> K -> Bool, -V: Data, order: List<&2, K>, +bindings: List<&2, T.Entry<K, V>>) -> List<&2, Maybe<&2, T.Entry<K, V>>>:
21 match order:
22 case Nil{}: Nil{}
23 case Con{+k, tail}: Con{S.find(~K, ~same, V, bindings, k), lookups(~K, ~same, V, tail, bindings)}
24
25def member(~K: Data, ~same: K -> K -> Bool, order: List<&2, K>, +key: K) -> Bool:
26 match order:
27 case Nil{}: False{}
28 case Con{k, tail}: Bool.or(same(k)(key), member(~K, ~same, tail, key))
29
30def keep_stray(-K: Data, -V: Data, entry: T.Entry<K, V>, rest: List<&2, T.Entry<K, V>>, bound: Bool) -> List<&2, T.Entry<K, V>>:
31 match bound:
32 case True{}: rest
33 case False{}: Con{entry, rest}
34
35def stray(~K: Data, ~same: K -> K -> Bool, -V: Data, +order: List<&2, K>, bindings: List<&2, T.Entry<K, V>>) -> List<&2, T.Entry<K, V>>:
36 match bindings:
37 case Nil{}: Nil{}
38 case Con{T.Item{+k, v, d}, tail}: keep_stray(K, V, T.Item{k, v, d}, stray(~K, ~same, V, order, tail), member(~K, ~same, order, k))
39
40def canonical(~K: Data, ~same: K -> K -> Bool, -V: Data, s: S.Model<K, V>) -> Canonical<K, V>:
41 S.Abstract{cap, +bindings, +order, life, counts, cb} = s
42 Canon{cap, order, life, counts, cb, lookups(~K, ~same, V, order, bindings), stray(~K, ~same, V, order, bindings)}
43
44def states(~K: Data, ~same: K -> K -> Bool, -V: Data, a: S.Model<K, V>, b: S.Model<K, V>) -> Data:
45 {canonical(~K, ~same, V, a) == canonical(~K, ~same, V, b) : Canonical<K, V>}
46
47def observations(~K: Data, ~same: K -> K -> Bool, -V: Data, a: S.Observation<K, V>, b: S.Observation<K, V>) -> Type:
48 match a b:
49 case S.Observed{as, ai, af, ae} S.Observed{bs, bi, bf, be}:
50 states(~K, ~same, V, as, bs) & {ai == bi : Maybe<&2, T.Entry<K, V>>} & {af == bf : Bool} & {ae == be : List<&2, T.LruEvent<K, V>>}