1 import Base 2 import ../src/cache.bend as C 3 import ../src/codec.bend as Codec 4 import ../spec/cache.bend as S 5 import ../spec/operations.bend as O 6 import ../spec/equivalence.bend as E 7 import ../types/model.bend as T 8 import ./refinement.bend as F 9 import ./invariants.bend as Inv 10 import ./abstraction_bindings.bend as B 11 import ./lookup_refinement.bend as L 12 import ./spec_lookup.bend as Lookup 13 import ./removal_lookup.bend as Delete 14 import ./removal_representation.bend as Rep 15 import ./string_order.bend as Order 16 import ./disabled.bend as Disabled 17 import ./canonical_native.bend as Native 18 import ./canonical_string.bend as CS 19 20 def normal_lookup(-V: Data, c: C.Cache, 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>}: 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 24 def binding_lookup(-V: Data, +c: C.Cache, +removed: String, +query: String, +entry: T.Entry, +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>}: 25 C.State{+cap, +table, +order, +life, +counts, +cb} = c 26 Equal.trans(Maybe<&2, T.Entry>, 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>, 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. 29 def lookups_removed(-V: Data, +c: C.Cache, +key: String, +entry: T.Entry, +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>>}: 30 match xs: 31 case Nil{}: {==} 32 case Con{+q, +rest}: CS.cons_equal(Maybe<&2, T.Entry>, 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 34 def normalized(-V: Data, +c: C.Cache, +key: String, +entry: T.Entry, +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>, Map.del(&2, Maybe<&2, T.Entry>, table, key))), S.erase(~String, ~Lookup.string_same, V, F.bindings(String, V, Map.to_list(&2, Maybe<&2, T.Entry>, 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>, 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>, 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. 40 def correspondence(-V: Data, +c: C.Cache, +key: String, +entry: T.Entry, +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, 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, 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 45 def no_events(-V: Data, +entry: T.Entry, cb: Bool, disabled: {cb == False{} : Bool}) -> {C.events(String, V, cb, entry) == S.callbacks(String, V, Con{entry, Nil{}}, cb) : List<&2, T.LruEvent>}: 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>} 48 {==} 49 50 def observation(-V: Data, +c: C.Cache, +key: String, +entry: T.Entry, 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))