~/bend-docscommunity

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

raw source on the hub · import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/spec/equivalence.bend as Equivalence

3 imports
import Base
import ./cache.bend as S
import ../types/model.bend as T

Types

type Canonical source · line 17 · raw

@-K:Data -> @-V:Data -> Data

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.

Definitions

def keep_stray source · line 30 · raw

@-K:Data -> @-V:Data -> @entry:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V> -> @rest:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>> -> @bound:Bool -> List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>>

Templates

template lookups source · line 20 · raw

@-K:Data -> @-same:(@_:K -> @_:K -> Bool) -> @-V:Data -> @order:List<&2, K> -> @+bindings:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>> -> List<&2, Maybe<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>>>

template member source · line 25 · raw

@-K:Data -> @-same:(@_:K -> @_:K -> Bool) -> @order:List<&2, K> -> @+key:K -> Bool

template stray source · line 35 · raw

@-K:Data -> @-same:(@_:K -> @_:K -> Bool) -> @-V:Data -> @+order:List<&2, K> -> @bindings:List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>> -> List<&2, 0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/types/model.Entry<K, V>>

template canonical source · line 40 · raw

@-K:Data -> @-same:(@_:K -> @_:K -> Bool) -> @-V:Data -> @s:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Model<K, V> -> Canonical<K, V>

template states source · line 44 · raw

@-K:Data -> @-same:(@_:K -> @_:K -> Bool) -> @-V:Data -> @a:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Model<K, V> -> @b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Model<K, V> -> Data

template observations source · line 47 · raw

@-K:Data -> @-same:(@_:K -> @_:K -> Bool) -> @-V:Data -> @a:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Observation<K, V> -> @b:0x5c489f5d9646d7cc9aa3dd8137e9dc07/proofs/lib/lemmas/spec/cache.Observation<K, V> -> Type