proofs/lib/lemmas/proofs/lookup_refinement.bend
bend-collections-laws-containers@1.0.0.0 · 59 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/src/cache.bend as C
3import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/src/codec.bend as Codec
4import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/spec/cache.bend as S
5import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/types/model.bend as T
6import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/refinement.bend as F
7import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/invariants.bend as Inv
8import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/spec_lookup.bend as Lookup
9import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/abstraction_lookup.bend as Abstract
10import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/abstraction_bindings.bend as B
11import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/abstraction_identity.bend as Identity
12import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/cache_key_identity.bend as Key
13import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/representation_access.bend as Access
14import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_routing.bend as Logic
15import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/recency_unique.bend as Unique
16import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/map_key_membership.bend as Keys
17
18def reflects(~K: Data, ~same: K -> K -> Bool) -> Type:
19 @+a: K -> @+b: K -> {same(a)(b) == True{} : Bool} -> {a == b : K}
20
21def reflexive(~K: Data, ~same: K -> K -> Bool) -> Type:
22 @+a: K -> {same(a)(a) == True{} : Bool}
23
24def matching(~K: Data, ~encode: K -> String, ~same: K -> K -> Bool, -V: Data, +c: C.Cache<K, V>, +query: K, entry: T.Entry<K, V>, valid: {Inv.representation(~K, ~encode, V, c) == True{} : Bool}, reflection: reflects(~K, ~same), proof: B.contains(T.Entry<K, V>, B.model_bindings(K, V, F.abstract(K, V, c)), entry) & {same(Lookup.key(K, V, entry))(query) == True{} : Bool}) -> {C.lookup(K, V, c, encode(query)) == Some{entry} : Maybe<&2, T.Entry<K, V>>}:
25 T.Item{+original, +value, +deadline} = entry
26 (member, matched) = proof
27 eq = reflection(original, query, matched)
28 Equal.trans(Maybe<&2, T.Entry<K, V>>, C.lookup(K, V, c, encode(query)), C.lookup(K, V, c, encode(original)), Some{T.Item{original, value, deadline}}, Equal.cong(K, Maybe<&2, T.Entry<K, V>>, k => C.lookup(K, V, c, encode(k)), query, original, Equal.sym(K, original, query, eq)), Abstract.binding(~K, ~encode, V, c, T.Item{original, value, deadline}, valid, member))
29
30def model_found(~K: Data, ~encode: K -> String, ~same: K -> K -> Bool, -V: Data, +c: C.Cache<K, V>, +query: K, +entry: T.Entry<K, V>, valid: {Inv.representation(~K, ~encode, V, c) == True{} : Bool}, reflection: reflects(~K, ~same), found: {S.find(~K, ~same, V, B.model_bindings(K, V, F.abstract(K, V, c)), query) == Some{entry} : Maybe<&2, T.Entry<K, V>>}) -> {C.lookup(K, V, c, encode(query)) == Some{entry} : Maybe<&2, T.Entry<K, V>>}:
31 matching(~K, ~encode, ~same, V, c, query, entry, valid, reflection, Lookup.returned(~K, ~same, V, B.model_bindings(K, V, F.abstract(K, V, c)), query, entry, found))
32
33def native_present(~K: Data, ~encode: K -> String, ~same: K -> K -> Bool, -V: Data, +c: C.Cache<K, V>, +query: K, entry: T.Entry<K, V>, valid: {Inv.representation(~K, ~encode, V, c) == True{} : Bool}, injective: Key.injective(~K, ~encode), reflexivity: reflexive(~K, ~same), +found: {C.lookup(K, V, c, encode(query)) == Some{entry} : Maybe<&2, T.Entry<K, V>>}) -> {Maybe.is_some(&2, T.Entry<K, V>, S.find(~K, ~same, V, B.model_bindings(K, V, F.abstract(K, V, c)), query)) == True{} : Bool}:
34 T.Item{+original, +value, +deadline} = entry
35 eq = Key.lookup_original_key(~K, ~encode, V, c, query, original, value, deadline, injective, Access.get_identities(~K, ~encode, V, c, valid), found)
36 matched = Equal.trans(Bool, same(original)(query), same(query)(query), True{}, Equal.cong(K, Bool, k => same(k)(query), original, query, Equal.sym(K, query, original, eq)), reflexivity(query))
37 Lookup.member_present(~K, ~same, V, B.model_bindings(K, V, F.abstract(K, V, c)), query, T.Item{original, value, deadline}, matched, B.lookup_retained_by_abstraction(K, V, c, encode(query), T.Item{original, value, deadline}, found))
38
39def native_missing(~K: Data, ~encode: K -> String, ~same: K -> K -> Bool, -V: Data, +c: C.Cache<K, V>, +query: K, valid: {Inv.representation(~K, ~encode, V, c) == True{} : Bool}, injective: Key.injective(~K, ~encode), reflexivity: reflexive(~K, ~same), missing: {S.find(~K, ~same, V, B.model_bindings(K, V, F.abstract(K, V, c)), query) == None{} : Maybe<&2, T.Entry<K, V>>}, native: Maybe<&2, T.Entry<K, V>>, checked: {C.lookup(K, V, c, encode(query)) == native : Maybe<&2, T.Entry<K, V>>}) -> {C.lookup(K, V, c, encode(query)) == None{} : Maybe<&2, T.Entry<K, V>>}:
40 match native:
41 case None{}: checked
42 case Some{entry}:
43 Empty.absurd({C.lookup(K, V, c, encode(query)) == None{} : Maybe<&2, T.Entry<K, V>>}, Logic.false_true(Equal.trans(Bool, False{}, Maybe.is_some(&2, T.Entry<K, V>, S.find(~K, ~same, V, B.model_bindings(K, V, F.abstract(K, V, c)), query)), True{}, Equal.sym(Bool, Maybe.is_some(&2, T.Entry<K, V>, S.find(~K, ~same, V, B.model_bindings(K, V, F.abstract(K, V, c)), query)), False{}, Equal.cong(Maybe<&2, T.Entry<K, V>>, Bool, m => Maybe.is_some(&2, T.Entry<K, V>, m), S.find(~K, ~same, V, B.model_bindings(K, V, F.abstract(K, V, c)), query), None{}, missing)), native_present(~K, ~encode, ~same, V, c, query, entry, valid, injective, reflexivity, checked))))
44
45def decision(~K: Data, ~encode: K -> String, ~same: K -> K -> Bool, -V: Data, +c: C.Cache<K, V>, +query: K, valid: {Inv.representation(~K, ~encode, V, c) == True{} : Bool}, injective: Key.injective(~K, ~encode), reflection: reflects(~K, ~same), reflexivity: reflexive(~K, ~same), model: Maybe<&2, T.Entry<K, V>>, checked: {S.find(~K, ~same, V, B.model_bindings(K, V, F.abstract(K, V, c)), query) == model : Maybe<&2, T.Entry<K, V>>}) -> {C.lookup(K, V, c, encode(query)) == model : Maybe<&2, T.Entry<K, V>>}:
46 match model:
47 case None{}: native_missing(~K, ~encode, ~same, V, c, query, valid, injective, reflexivity, checked, C.lookup(K, V, c, encode(query)), {==})
48 case Some{entry}: model_found(~K, ~encode, ~same, V, c, query, entry, valid, reflection, checked)
49
50# Exact finite-map lookup, including absence, with independently specified key
51# equality. Representation and custom-codec/equality contracts are explicit.
52def correspondence(~K: Data, ~encode: K -> String, ~same: K -> K -> Bool, -V: Data, +c: C.Cache<K, V>, +query: K, valid: {Inv.representation(~K, ~encode, V, c) == True{} : Bool}, injective: Key.injective(~K, ~encode), reflection: reflects(~K, ~same), reflexivity: reflexive(~K, ~same)) -> {C.lookup(K, V, c, encode(query)) == S.find(~K, ~same, V, B.model_bindings(K, V, F.abstract(K, V, c)), query) : Maybe<&2, T.Entry<K, V>>}:
53 decision(~K, ~encode, ~same, V, c, query, valid, injective, reflection, reflexivity, S.find(~K, ~same, V, B.model_bindings(K, V, F.abstract(K, V, c)), query), {==})
54
55def string_reflexive(+key: String) -> {String.eq(key, key) == True{} : Bool}:
56 Keys.eq_true(key, key, {==})
57
58def string_lookup(-V: Data, c: C.Cache<String, V>, query: String, valid: {Inv.representation(~String, ~Codec.string_encode, V, c) == True{} : Bool}) -> {C.lookup(String, V, c, Codec.string_encode(query)) == S.find(~String, ~Lookup.string_same, V, B.model_bindings(String, V, F.abstract(String, V, c)), query) : Maybe<&2, T.Entry<String, V>>}:
59 correspondence(~String, ~Codec.string_encode, ~Lookup.string_same, V, c, query, valid, Codec.string_injective, Unique.equal_boolean, string_reflexive)