proofs/lib/lemmas/proofs/store_lookup_refinement.bend
bend-collections-laws-containers@1.0.0.0 · 33 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/spec/operations.bend as O
6import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/types/model.bend as T
7import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/refinement.bend as F
8import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/invariants.bend as Inv
9import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/lookup_refinement.bend as L
10import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/spec_lookup.bend as Lookup
11import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/spec_write_lookup.bend as Write
12import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/abstraction_bindings.bend as B
13import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/removal_lookup.bend as Storage
14import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/recency_unique.bend as Unique
15
16def target(-V: Data, s: S.Model<String, V>, key: String, value: V, deadline: T.Int64, flag: Bool, events: List<&2, T.LruEvent<String, V>>, query: String) -> Maybe<&2, T.Entry<String, V>>:
17 S.find(~String, ~Lookup.string_same, V, B.model_bindings(String, V, O.observed_state(String, V, O.write(~String, ~Lookup.string_same, V, s, key, value, deadline, flag, events))), query)
18
19def same(-V: Data, +c: C.Cache<String, V>, +key: String, +value: V, +deadline: T.Int64, +flag: Bool, +events: List<&2, T.LruEvent<String, V>>) -> {C.lookup(String, V, C.step_cache(String, V, C.store(String, V, c, key, key, value, deadline, flag, events)), key) == target(V, F.abstract(String, V, c), key, value, deadline, flag, events, key) : Maybe<&2, T.Entry<String, V>>}:
20 Equal.trans(Maybe<&2, T.Entry<String, V>>, C.lookup(String, V, C.step_cache(String, V, C.store(String, V, c, key, key, value, deadline, flag, events)), key), Some{T.Item{key, value, deadline}}, target(V, F.abstract(String, V, c), key, value, deadline, flag, events, key), F.store_lookup(String, V, c, key, key, value, deadline, flag, events), Equal.sym(Maybe<&2, T.Entry<String, V>>, target(V, F.abstract(String, V, c), key, value, deadline, flag, events, key), Some{T.Item{key, value, deadline}}, Write.same(V, F.abstract(String, V, c), key, value, deadline, flag, events)))
21
22def other(-V: Data, +c: C.Cache<String, V>, +key: String, +value: V, +deadline: T.Int64, +flag: Bool, +events: List<&2, T.LruEvent<String, V>>, +query: String, +valid: {Inv.representation(~String, ~Codec.string_encode, V, c) == True{} : Bool}, +different: {String.eq(key, query) == False{} : Bool}) -> {C.lookup(String, V, C.step_cache(String, V, C.store(String, V, c, key, key, value, deadline, flag, events)), query) == target(V, F.abstract(String, V, c), key, value, deadline, flag, events, query) : Maybe<&2, T.Entry<String, V>>}:
23 Equal.trans(Maybe<&2, T.Entry<String, V>>, C.lookup(String, V, C.step_cache(String, V, C.store(String, V, c, key, key, value, deadline, flag, events)), query), C.lookup(String, V, c, query), target(V, F.abstract(String, V, c), key, value, deadline, flag, events, query), F.store_other_lookup(String, V, c, key, key, value, deadline, flag, events, query, Write.reverse_false(key, query, different), Storage.valid_storage(V, c, valid)), Equal.trans(Maybe<&2, T.Entry<String, V>>, C.lookup(String, V, c, query), S.find(~String, ~Lookup.string_same, V, B.model_bindings(String, V, F.abstract(String, V, c)), query), target(V, F.abstract(String, V, c), key, value, deadline, flag, events, query), L.string_lookup(V, c, query, valid), Equal.sym(Maybe<&2, T.Entry<String, V>>, target(V, F.abstract(String, V, c), key, value, deadline, flag, events, query), S.find(~String, ~Lookup.string_same, V, B.model_bindings(String, V, F.abstract(String, V, c)), query), Write.other(V, F.abstract(String, V, c), key, value, deadline, flag, events, query, different))))
24
25def decide(-V: Data, +c: C.Cache<String, V>, +key: String, +value: V, +deadline: T.Int64, +flag: Bool, +events: List<&2, T.LruEvent<String, V>>, +query: String, valid: {Inv.representation(~String, ~Codec.string_encode, V, c) == True{} : Bool}, equal: Bool, decision: {String.eq(key, query) == equal : Bool}) -> {C.lookup(String, V, C.step_cache(String, V, C.store(String, V, c, key, key, value, deadline, flag, events)), query) == target(V, F.abstract(String, V, c), key, value, deadline, flag, events, query) : Maybe<&2, T.Entry<String, V>>}:
26 match equal:
27 case False{}: other(V, c, key, value, deadline, flag, events, query, valid, decision)
28 case True{}:
29 %Unique.equal_boolean(key, query, decision) : {C.lookup(String, V, C.step_cache(String, V, C.store(String, V, c, key, key, value, deadline, flag, events)), _) == target(V, F.abstract(String, V, c), key, value, deadline, flag, events, _) : Maybe<&2, T.Entry<String, V>>}
30 same(V, c, key, value, deadline, flag, events)
31
32def correspondence(-V: Data, c: C.Cache<String, V>, +key: String, value: V, deadline: T.Int64, flag: Bool, events: List<&2, T.LruEvent<String, V>>, +query: String, valid: {Inv.representation(~String, ~Codec.string_encode, V, c) == True{} : Bool}) -> {C.lookup(String, V, C.step_cache(String, V, C.store(String, V, c, key, key, value, deadline, flag, events)), query) == target(V, F.abstract(String, V, c), key, value, deadline, flag, events, query) : Maybe<&2, T.Entry<String, V>>}:
33 decide(V, c, key, value, deadline, flag, events, query, valid, String.eq(key, query), {==})