proofs/lib/lemmas/spec/equivalence.bend source

proofs/lib/lemmas/spec/equivalence.bend on the hub · documented module

import Baseimport ./cache.bend as Simport ../types/model.bend as T# Extensional finite-map equality deliberately ignores binding-list storage# order. It preserves every queried entry (original key, value and deadline),# exact observable recency, capacity, configuration, metrics and inert metadata.# This is independent of the implementation and its abstraction function.## Two models are related when their canonical forms are equal. The canonical# form keeps every non-binding field exactly and replaces the binding list by# (1) the lookup result at each recency key, in recency order, and (2) the# bindings whose key is not in the recency list ("stray", normally empty), in# list order. With a key equality that reflects equality, related models agree# on S.find for EVERY key (proofs/canonical.bend, lookup_agreement). Unlike a# pointwise function premise, this is one reusable equality proof.type Canonical<-K: Data, -V: Data> is Data:  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>>}def 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>>>:  match order:    case Nil{}: Nil{}    case Con{+k, tail}: Con{S.find(~K, ~same, V, bindings, k), lookups(~K, ~same, V, tail, bindings)}def member(~K: Data, ~same: K -> K -> Bool, order: List<&2, K>, +key: K) -> Bool:  match order:    case Nil{}: False{}    case Con{k, tail}: Bool.or(same(k)(key), member(~K, ~same, tail, key))def 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>>:  match bound:    case True{}: rest    case False{}: Con{entry, rest}def 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>>:  match bindings:    case Nil{}: Nil{}    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))def canonical(~K: Data, ~same: K -> K -> Bool, -V: Data, s: S.Model<K, V>) -> Canonical<K, V>:  S.Abstract{cap, +bindings, +order, life, counts, cb} = s  Canon{cap, order, life, counts, cb, lookups(~K, ~same, V, order, bindings), stray(~K, ~same, V, order, bindings)}def states(~K: Data, ~same: K -> K -> Bool, -V: Data, a: S.Model<K, V>, b: S.Model<K, V>) -> Data:  {canonical(~K, ~same, V, a) == canonical(~K, ~same, V, b) : Canonical<K, V>}def observations(~K: Data, ~same: K -> K -> Bool, -V: Data, a: S.Observation<K, V>, b: S.Observation<K, V>) -> Type:  match a b:    case S.Observed{as, ai, af, ae} S.Observed{bs, bi, bf, be}:      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>>}