proofs/lib/lemmas/proofs/absent_read.bend
bend-collections-laws-containers@1.0.0.0 · 39 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/protocol.bend as P
4import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/src/codec.bend as Codec
5import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/spec/cache.bend as S
6import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/spec/operations.bend as O
7import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/types/model.bend as T
8import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/refinement.bend as F
9import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/invariants.bend as Inv
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/lookup_refinement.bend as L
12import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/spec_lookup.bend as Lookup
13
14def branch(~K: Data, ~same: K -> K -> Bool, -V: Data, c: C.Cache<K, V>, key: K, code: String, +now: T.Int64, +tracked: Bool) -> {F.observe(K, V, C.read_found(K, V, c, code, now, tracked, None{})) == O.read_found(~K, ~same, V, F.abstract(K, V, c), key, now, tracked, None{}) : S.Observation<K, V>}:
15 C.State{cap, table, order, life, T.Counts{i, e, r, h, m}, cb} = c
16 match tracked:
17 case False{}: {==}
18 case True{}: {==}
19
20def model_dispatch(~K: Data, ~same: K -> K -> Bool, -V: Data, +s: S.Model<K, V>, +key: K, +now: T.Int64, +tracked: Bool, missing: {S.find(~K, ~same, V, B.model_bindings(K, V, s), key) == None{} : Maybe<&2, T.Entry<K, V>>}) -> {O.read(~K, ~same, V, s, key, now, tracked) == O.read_found(~K, ~same, V, s, key, now, tracked, None{}) : S.Observation<K, V>}:
21 S.Abstract{cap, bindings, order, life, counts, cb} = s
22 Equal.cong(Maybe<&2, T.Entry<K, V>>, S.Observation<K, V>, found => O.read_found(~K, ~same, V, S.Abstract{cap, bindings, order, life, counts, cb}, key, now, tracked, found), S.find(~K, ~same, V, bindings, key), None{}, missing)
23
24# Arbitrary represented cache with an absent key, not merely an empty cache.
25# Tracked Get increments Misses; untracked Peek/Contains do not. Both preserve
26# all bindings, recency, lifetime and other counters, returning no entry/events.
27def string_read(-V: Data, +c: C.Cache<String, V>, +key: String, +now: T.Int64, +tracked: Bool, valid: {Inv.representation(~String, ~Codec.string_encode, V, c) == True{} : Bool}, +missing: {S.find(~String, ~Lookup.string_same, V, B.model_bindings(String, V, F.abstract(String, V, c)), key) == None{} : Maybe<&2, T.Entry<String, V>>}) -> {F.observe(String, V, C.read_encoded(String, V, c, key, now, tracked)) == O.read(~String, ~Lookup.string_same, V, F.abstract(String, V, c), key, now, tracked) : S.Observation<String, V>}:
28 native = Equal.trans(Maybe<&2, T.Entry<String, V>>, C.lookup(String, V, c, key), S.find(~String, ~Lookup.string_same, V, B.model_bindings(String, V, F.abstract(String, V, c)), key), None{}, L.string_lookup(V, c, key, valid), missing)
29 Equal.trans(S.Observation<String, V>, F.observe(String, V, C.read_encoded(String, V, c, key, now, tracked)), F.observe(String, V, C.read_found(String, V, c, key, now, tracked, None{})), O.read(~String, ~Lookup.string_same, V, F.abstract(String, V, c), key, now, tracked), Equal.cong(Maybe<&2, T.Entry<String, V>>, S.Observation<String, V>, found => F.observe(String, V, C.read_found(String, V, c, key, now, tracked, found)), C.lookup(String, V, c, key), None{}, native), Equal.trans(S.Observation<String, V>, F.observe(String, V, C.read_found(String, V, c, key, now, tracked, None{})), O.read_found(~String, ~Lookup.string_same, V, F.abstract(String, V, c), key, now, tracked, None{}), O.read(~String, ~Lookup.string_same, V, F.abstract(String, V, c), key, now, tracked), branch(~String, ~Lookup.string_same, V, c, key, key, now, tracked), Equal.sym(S.Observation<String, V>, O.read(~String, ~Lookup.string_same, V, F.abstract(String, V, c), key, now, tracked), O.read_found(~String, ~Lookup.string_same, V, F.abstract(String, V, c), key, now, tracked, None{}), model_dispatch(~String, ~Lookup.string_same, V, F.abstract(String, V, c), key, now, tracked, missing))))
30
31# The facade calls P.read rather than C.read_encoded. This equation connects
32# its absent branch, including the no-removal signal, to the proved core branch.
33def protocol_branch(-K: Data, -V: Data, c: C.Cache<K, V>, code: String, now: T.Int64, tracked: Bool) -> {P.read_found(K, V, c, code, now, tracked, None{}) == P.Reading{C.read_found(K, V, c, code, now, tracked, None{}), False{}} : P.Read<K, V>}:
34 C.State{cap, table, order, life, counts, cb} = c
35 {==}
36
37def protocol_missing(-K: Data, -V: Data, +c: C.Cache<K, V>, +code: String, +now: T.Int64, +tracked: Bool, +missing: {C.lookup(K, V, c, code) == None{} : Maybe<&2, T.Entry<K, V>>}) -> {P.read(K, V, c, code, now, tracked) == P.Reading{C.read_encoded(K, V, c, code, now, tracked), False{}} : P.Read<K, V>}:
38 %Equal.sym(Maybe<&2, T.Entry<K, V>>, C.lookup(K, V, c, code), None{}, missing) : {P.read_found(K, V, c, code, now, tracked, _) == P.Reading{C.read_found(K, V, c, code, now, tracked, _), False{}} : P.Read<K, V>}
39 protocol_branch(K, V, c, code, now, tracked)