1 import Base 2 import ../src/cache.bend as C 3 import ../src/protocol.bend as P 4 import ../src/codec.bend as Codec 5 import ../spec/cache.bend as S 6 import ../spec/operations.bend as O 7 import ../types/model.bend as T 8 import ./refinement.bend as F 9 import ./invariants.bend as Inv 10 import ./spec_lookup.bend as Lookup 11 import ./lookup_refinement.bend as L 12 import ./abstraction_bindings.bend as B 13 import ./string_order.bend as Order 14 import ./abstraction_recency.bend as Recency 15 16 def native(-V: Data, c: C.Cache, order: List<&2, String>) -> List<&2, T.Entry>: 17 C.State{cap, table, recency, life, counts, cb} = c 18 C.entries_go(String, V, order, table) 19 20 def collect(-V: Data, found: Maybe<&2, T.Entry>, rest: List<&2, T.Entry>) -> {C.collect_entry(String, V, found, rest) == O.collect(String, V, found, rest) : List<&2, T.Entry>}: 21 match found: 22 case None{}: {==} 23 case Some{entry}: {==} 24 25 def ordered(-V: Data, +c: C.Cache, order: List<&2, String>, +valid: {Inv.representation(~String, ~Codec.string_encode, V, c) == True{} : Bool}) -> {native(V, c, order) == O.ordered(~String, ~Lookup.string_same, V, order, B.model_bindings(String, V, F.abstract(String, V, c))) : List<&2, T.Entry>}: 26 C.State{+cap, +table, +recency, +life, +counts, +cb} = c 27 match order: 28 case Nil{}: {==} 29 case Con{+key, +tail}: 30 %Equal.sym(Maybe<&2, T.Entry>, C.lookup(String, V, C.State{cap, table, recency, life, counts, cb}, key), S.find(~String, ~Lookup.string_same, V, B.model_bindings(String, V, F.abstract(String, V, C.State{cap, table, recency, life, counts, cb})), key), L.string_lookup(V, C.State{cap, table, recency, life, counts, cb}, key, valid)) : {C.collect_entry(String, V, _, C.entries_go(String, V, tail, table)) == O.collect(String, V, S.find(~String, ~Lookup.string_same, V, B.model_bindings(String, V, F.abstract(String, V, C.State{cap, table, recency, life, counts, cb})), key), O.ordered(~String, ~Lookup.string_same, V, tail, B.model_bindings(String, V, F.abstract(String, V, C.State{cap, table, recency, life, counts, cb})))) : List<&2, T.Entry>} 31 Equal.trans(List<&2, T.Entry>, C.collect_entry(String, V, S.find(~String, ~Lookup.string_same, V, B.model_bindings(String, V, F.abstract(String, V, C.State{cap, table, recency, life, counts, cb})), key), C.entries_go(String, V, tail, table)), C.collect_entry(String, V, S.find(~String, ~Lookup.string_same, V, B.model_bindings(String, V, F.abstract(String, V, C.State{cap, table, recency, life, counts, cb})), key), O.ordered(~String, ~Lookup.string_same, V, tail, B.model_bindings(String, V, F.abstract(String, V, C.State{cap, table, recency, life, counts, cb})))), O.collect(String, V, S.find(~String, ~Lookup.string_same, V, B.model_bindings(String, V, F.abstract(String, V, C.State{cap, table, recency, life, counts, cb})), key), O.ordered(~String, ~Lookup.string_same, V, tail, B.model_bindings(String, V, F.abstract(String, V, C.State{cap, table, recency, life, counts, cb})))), Equal.cong(List<&2, T.Entry>, List<&2, T.Entry>, xs => C.collect_entry(String, V, S.find(~String, ~Lookup.string_same, V, B.model_bindings(String, V, F.abstract(String, V, C.State{cap, table, recency, life, counts, cb})), key), xs), C.entries_go(String, V, tail, table), O.ordered(~String, ~Lookup.string_same, V, tail, B.model_bindings(String, V, F.abstract(String, V, C.State{cap, table, recency, life, counts, cb}))), ordered(V, C.State{cap, table, recency, life, counts, cb}, tail, valid)), collect(V, S.find(~String, ~Lookup.string_same, V, B.model_bindings(String, V, F.abstract(String, V, C.State{cap, table, recency, life, counts, cb})), key), O.ordered(~String, ~Lookup.string_same, V, tail, B.model_bindings(String, V, F.abstract(String, V, C.State{cap, table, recency, life, counts, cb}))))) 32 33 # Exact ordered entries, retaining original keys, values and deadlines. 34 def all_entries(-V: Data, c: C.Cache, +valid: {Inv.representation(~String, ~Codec.string_encode, V, c) == True{} : Bool}) -> {C.entries(String, V, c) == O.all_entries(~String, ~Lookup.string_same, V, F.abstract(String, V, c)) : List<&2, T.Entry>}: 35 C.State{+cap, +table, +order, +life, +counts, +cb} = c 36 %Equal.sym(List<&2, String>, Recency.model_order(String, V, F.abstract(String, V, C.State{cap, table, order, life, counts, cb})), order, Order.faithful(V, C.State{cap, table, order, life, counts, cb}, valid)) : {C.entries_go(String, V, order, table) == O.ordered(~String, ~Lookup.string_same, V, _, B.model_bindings(String, V, F.abstract(String, V, C.State{cap, table, order, life, counts, cb}))) : List<&2, T.Entry>} 37 ordered(V, C.State{cap, table, order, life, counts, cb}, order, valid) 38 39 def keys_projection(-K: Data, -V: Data, entries: List<&2, T.Entry>) -> {P.keys_of(K, V, entries) == O.entry_keys(K, V, entries) : List<&2, K>}: 40 match entries: 41 case Nil{}: {==} 42 case Con{T.Item{+key, value, deadline}, +tail}: 43 Equal.cong(List<&2, K>, List<&2, K>, xs => Con{key, xs}, P.keys_of(K, V, tail), O.entry_keys(K, V, tail), keys_projection(K, V, tail)) 44 45 def values_projection(-K: Data, -V: Data, entries: List<&2, T.Entry>) -> {P.values_of(K, V, entries) == O.entry_values(K, V, entries) : List<&2, V>}: 46 match entries: 47 case Nil{}: {==} 48 case Con{T.Item{key, +value, deadline}, +tail}: 49 Equal.cong(List<&2, V>, List<&2, V>, xs => Con{value, xs}, P.values_of(K, V, tail), O.entry_values(K, V, tail), values_projection(K, V, tail)) 50 51 def keys(-V: Data, +c: C.Cache, valid: {Inv.representation(~String, ~Codec.string_encode, V, c) == True{} : Bool}) -> {P.keys_of(String, V, C.entries(String, V, c)) == O.entry_keys(String, V, O.all_entries(~String, ~Lookup.string_same, V, F.abstract(String, V, c))) : List<&2, String>}: 52 Equal.trans(List<&2, String>, P.keys_of(String, V, C.entries(String, V, c)), O.entry_keys(String, V, C.entries(String, V, c)), O.entry_keys(String, V, O.all_entries(~String, ~Lookup.string_same, V, F.abstract(String, V, c))), keys_projection(String, V, C.entries(String, V, c)), Equal.cong(List<&2, T.Entry>, List<&2, String>, xs => O.entry_keys(String, V, xs), C.entries(String, V, c), O.all_entries(~String, ~Lookup.string_same, V, F.abstract(String, V, c)), all_entries(V, c, valid))) 53 54 def values(-V: Data, +c: C.Cache, valid: {Inv.representation(~String, ~Codec.string_encode, V, c) == True{} : Bool}) -> {P.values_of(String, V, C.entries(String, V, c)) == O.entry_values(String, V, O.all_entries(~String, ~Lookup.string_same, V, F.abstract(String, V, c))) : List<&2, V>}: 55 Equal.trans(List<&2, V>, P.values_of(String, V, C.entries(String, V, c)), O.entry_values(String, V, C.entries(String, V, c)), O.entry_values(String, V, O.all_entries(~String, ~Lookup.string_same, V, F.abstract(String, V, c))), values_projection(String, V, C.entries(String, V, c)), Equal.cong(List<&2, T.Entry>, List<&2, V>, xs => O.entry_values(String, V, xs), C.entries(String, V, c), O.all_entries(~String, ~Lookup.string_same, V, F.abstract(String, V, c)), all_entries(V, c, valid))) 56 57 # Actual aggregate completion constructors, not the still-open expiry loop. 58 def complete_keys(-V: Data, +c: C.Cache, valid: {Inv.representation(~String, ~Codec.string_encode, V, c) == True{} : Bool}) -> {P.complete(String, V, c, P.KeyList{}) == P.Complete{c, O.entry_keys(String, V, O.all_entries(~String, ~Lookup.string_same, V, F.abstract(String, V, c))), Nil{}} : P.Aggregate}: 59 Equal.cong(List<&2, String>, P.Aggregate, xs => P.Complete{c, xs, Nil{}}, P.keys_of(String, V, C.entries(String, V, c)), O.entry_keys(String, V, O.all_entries(~String, ~Lookup.string_same, V, F.abstract(String, V, c))), keys(V, c, valid)) 60 61 def complete_values(-V: Data, +c: C.Cache, valid: {Inv.representation(~String, ~Codec.string_encode, V, c) == True{} : Bool}) -> {P.complete(String, V, c, P.ValueList{}) == P.Complete{c, Nil{}, O.entry_values(String, V, O.all_entries(~String, ~Lookup.string_same, V, F.abstract(String, V, c))) } : P.Aggregate}: 62 Equal.cong(List<&2, V>, P.Aggregate, xs => P.Complete{c, Nil{}, xs}, P.values_of(String, V, C.entries(String, V, c)), O.entry_values(String, V, O.all_entries(~String, ~Lookup.string_same, V, F.abstract(String, V, c))), values(V, c, valid))