proofs/lib/lemmas/proofs/removal_state.bend
bend-collections-laws-containers@1.0.0.0 · 52 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/spec/equivalence.bend as E
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
13import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/removal_lookup.bend as Delete
14import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/removal_representation.bend as Rep
15import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/string_order.bend as Order
16import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/disabled.bend as Disabled
17import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/canonical_native.bend as Native
18import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/canonical_string.bend as CS
19
20def normal_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, query) == S.find(~String, ~Lookup.string_same, V, B.model_bindings(String, V, Order.normal(V, c)), query) : Maybe<&2, T.Entry<String, V>>}:
21 C.State{+cap, +table, +order, +life, +counts, +cb} = c
22 L.string_lookup(V, C.State{cap, table, order, life, counts, cb}, query, valid)
23
24def binding_lookup(-V: Data, +c: C.Cache<String, V>, +removed: String, +query: String, +entry: T.Entry<String, V>, +valid: {Inv.representation(~String, ~Codec.string_encode, V, c) == True{} : Bool}) -> {S.find(~String, ~Lookup.string_same, V, B.model_bindings(String, V, Order.normal(V, C.step_cache(String, V, C.remove_present(String, V, c, removed, False{}, entry)))), query) == S.find(~String, ~Lookup.string_same, V, S.erase(~String, ~Lookup.string_same, V, B.model_bindings(String, V, Order.normal(V, c)), removed), query) : Maybe<&2, T.Entry<String, V>>}:
25 C.State{+cap, +table, +order, +life, +counts, +cb} = c
26 Equal.trans(Maybe<&2, T.Entry<String, V>>, S.find(~String, ~Lookup.string_same, V, B.model_bindings(String, V, Order.normal(V, C.step_cache(String, V, C.remove_present(String, V, C.State{cap, table, order, life, counts, cb}, removed, False{}, entry)))), query), C.lookup(String, V, C.step_cache(String, V, C.remove_present(String, V, C.State{cap, table, order, life, counts, cb}, removed, False{}, entry)), query), S.find(~String, ~Lookup.string_same, V, S.erase(~String, ~Lookup.string_same, V, B.model_bindings(String, V, Order.normal(V, C.State{cap, table, order, life, counts, cb})), removed), query), Equal.sym(Maybe<&2, T.Entry<String, V>>, C.lookup(String, V, C.step_cache(String, V, C.remove_present(String, V, C.State{cap, table, order, life, counts, cb}, removed, False{}, entry)), query), S.find(~String, ~Lookup.string_same, V, B.model_bindings(String, V, Order.normal(V, C.step_cache(String, V, C.remove_present(String, V, C.State{cap, table, order, life, counts, cb}, removed, False{}, entry)))), query), normal_lookup(V, C.step_cache(String, V, C.remove_present(String, V, C.State{cap, table, order, life, counts, cb}, removed, False{}, entry)), query, Rep.remove_present(~String, ~Codec.string_encode, V, C.State{cap, table, order, life, counts, cb}, removed, False{}, entry, valid))), Delete.correspondence(V, C.State{cap, table, order, life, counts, cb}, removed, query, entry, valid))
27
28# Lookups at any list of recency keys agree after the actual removal.
29def lookups_removed(-V: Data, +c: C.Cache<String, V>, +key: String, +entry: T.Entry<String, V>, +valid: {Inv.representation(~String, ~Codec.string_encode, V, c) == True{} : Bool}, xs: List<&2, String>) -> {E.lookups(~String, ~Lookup.string_same, V, xs, B.model_bindings(String, V, Order.normal(V, C.step_cache(String, V, C.remove_present(String, V, c, key, False{}, entry))))) == E.lookups(~String, ~Lookup.string_same, V, xs, S.erase(~String, ~Lookup.string_same, V, B.model_bindings(String, V, Order.normal(V, c)), key)) : List<&2, Maybe<&2, T.Entry<String, V>>>}:
30 match xs:
31 case Nil{}: {==}
32 case Con{+q, +rest}: CS.cons_equal(Maybe<&2, T.Entry<String, V>>, S.find(~String, ~Lookup.string_same, V, B.model_bindings(String, V, Order.normal(V, C.step_cache(String, V, C.remove_present(String, V, c, key, False{}, entry)))), q), S.find(~String, ~Lookup.string_same, V, S.erase(~String, ~Lookup.string_same, V, B.model_bindings(String, V, Order.normal(V, c)), key), q), E.lookups(~String, ~Lookup.string_same, V, rest, B.model_bindings(String, V, Order.normal(V, C.step_cache(String, V, C.remove_present(String, V, c, key, False{}, entry))))), E.lookups(~String, ~Lookup.string_same, V, rest, S.erase(~String, ~Lookup.string_same, V, B.model_bindings(String, V, Order.normal(V, c)), key)), binding_lookup(V, c, key, q, entry, valid), lookups_removed(V, c, key, entry, valid, rest))
33
34def normalized(-V: Data, +c: C.Cache<String, V>, +key: String, +entry: T.Entry<String, V>, +valid: {Inv.representation(~String, ~Codec.string_encode, V, c) == True{} : Bool}) -> E.states(~String, ~Lookup.string_same, V, Order.normal(V, C.step_cache(String, V, C.remove_present(String, V, c, key, False{}, entry))), O.observed_state(String, V, S.remove_existing(~String, ~Lookup.string_same, V, Order.normal(V, c), key, entry))):
35 C.State{+cap, +table, +order, +life, T.Counts{+i, +e, +r, +h, +m}, +cb} = c
36 Native.by_fields(V, cap, C.without(order, key), S.unlist(~String, ~Lookup.string_same, order, key), life, T.Counts{i, e, Word.inc(64n, r), h, m}, cb, F.bindings(String, V, Map.to_list(&2, Maybe<&2, T.Entry<String, V>>, Map.del(&2, Maybe<&2, T.Entry<String, V>>, table, key))), S.erase(~String, ~Lookup.string_same, V, F.bindings(String, V, Map.to_list(&2, Maybe<&2, T.Entry<String, V>>, table)), key), Order.filter(order, key), lookups_removed(V, C.State{cap, table, order, life, T.Counts{i, e, r, h, m}, cb}, key, entry, valid, S.unlist(~String, ~Lookup.string_same, order, key)), Native.stray_normal(V, cap, Map.del(&2, Maybe<&2, T.Entry<String, V>>, table, key), C.without(order, key), life, T.Counts{i, e, Word.inc(64n, r), h, m}, cb, Rep.remove_present(~String, ~Codec.string_encode, V, C.State{cap, table, order, life, T.Counts{i, e, r, h, m}, cb}, key, False{}, entry, valid)), CS.removed_stray(V, order, F.bindings(String, V, Map.to_list(&2, Maybe<&2, T.Entry<String, V>>, table)), key, Native.stray_normal(V, cap, table, order, life, T.Counts{i, e, r, h, m}, cb, valid)))
37
38# Full abstract state correspondence for the actual removal phase. Native Map
39# enumeration order is ignored only for bindings; recency and metrics are exact.
40def correspondence(-V: Data, +c: C.Cache<String, V>, +key: String, +entry: T.Entry<String, V>, +valid: {Inv.representation(~String, ~Codec.string_encode, V, c) == True{} : Bool}) -> E.states(~String, ~Lookup.string_same, V, F.abstract(String, V, C.step_cache(String, V, C.remove_present(String, V, c, key, False{}, entry))), O.observed_state(String, V, S.remove_existing(~String, ~Lookup.string_same, V, F.abstract(String, V, c), key, entry))):
41 %Equal.sym(S.Model<String, V>, F.abstract(String, V, C.step_cache(String, V, C.remove_present(String, V, c, key, False{}, entry))), Order.normal(V, C.step_cache(String, V, C.remove_present(String, V, c, key, False{}, entry))), Order.normalize(V, C.step_cache(String, V, C.remove_present(String, V, c, key, False{}, entry)), Rep.remove_present(~String, ~Codec.string_encode, V, c, key, False{}, entry, valid))) : E.states(~String, ~Lookup.string_same, V, _, O.observed_state(String, V, S.remove_existing(~String, ~Lookup.string_same, V, F.abstract(String, V, c), key, entry)))
42 %Equal.sym(S.Model<String, V>, F.abstract(String, V, c), Order.normal(V, c), Order.normalize(V, c, valid)) : E.states(~String, ~Lookup.string_same, V, Order.normal(V, C.step_cache(String, V, C.remove_present(String, V, c, key, False{}, entry))), O.observed_state(String, V, S.remove_existing(~String, ~Lookup.string_same, V, _, key, entry)))
43 normalized(V, c, key, entry, valid)
44
45def no_events(-V: Data, +entry: T.Entry<String, V>, cb: Bool, disabled: {cb == False{} : Bool}) -> {C.events(String, V, cb, entry) == S.callbacks(String, V, Con{entry, Nil{}}, cb) : List<&2, T.LruEvent<String, V>>}:
46 T.Item{+original, +value, +deadline} = entry
47 %Equal.sym(Bool, cb, False{}, disabled) : {C.events(String, V, _, T.Item{original, value, deadline}) == S.callbacks(String, V, Con{T.Item{original, value, deadline}, Nil{}}, _) : List<&2, T.LruEvent<String, V>>}
48 {==}
49
50def observation(-V: Data, +c: C.Cache<String, V>, +key: String, +entry: T.Entry<String, V>, valid: {Inv.representation(~String, ~Codec.string_encode, V, c) == True{} : Bool}, disabled: {Disabled.flag(String, V, c) == False{} : Bool}) -> E.observations(~String, ~Lookup.string_same, V, F.observe(String, V, C.remove_present(String, V, c, key, False{}, entry)), S.remove_existing(~String, ~Lookup.string_same, V, F.abstract(String, V, c), key, entry)):
51 C.State{+cap, +table, +order, +life, T.Counts{+i, +e, +r, +h, +m}, +cb} = c
52 (correspondence(V, C.State{cap, table, order, life, T.Counts{i, e, r, h, m}, cb}, key, entry, valid), {==}, {==}, no_events(V, entry, cb, disabled))