proofs/lib/lemmas/proofs/ordered_entries.bend
bend-collections-laws-containers@1.0.0.0 · 62 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/spec_lookup.bend as Lookup
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/abstraction_bindings.bend as B
13import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/string_order.bend as Order
14import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/abstraction_recency.bend as Recency
15
16def native(-V: Data, c: C.Cache<String, V>, order: List<&2, String>) -> List<&2, T.Entry<String, V>>:
17 C.State{cap, table, recency, life, counts, cb} = c
18 C.entries_go(String, V, order, table)
19
20def collect(-V: Data, found: Maybe<&2, T.Entry<String, V>>, rest: List<&2, T.Entry<String, V>>) -> {C.collect_entry(String, V, found, rest) == O.collect(String, V, found, rest) : List<&2, T.Entry<String, V>>}:
21 match found:
22 case None{}: {==}
23 case Some{entry}: {==}
24
25def ordered(-V: Data, +c: C.Cache<String, V>, 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<String, V>>}:
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<String, V>>, 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<String, V>>}
31 Equal.trans(List<&2, T.Entry<String, V>>, 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<String, V>>, List<&2, T.Entry<String, V>>, 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.
34def all_entries(-V: Data, c: C.Cache<String, V>, +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<String, V>>}:
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<String, V>>}
37 ordered(V, C.State{cap, table, order, life, counts, cb}, order, valid)
38
39def keys_projection(-K: Data, -V: Data, entries: List<&2, T.Entry<K, V>>) -> {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
45def values_projection(-K: Data, -V: Data, entries: List<&2, T.Entry<K, V>>) -> {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
51def keys(-V: Data, +c: C.Cache<String, V>, 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<String, V>>, 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
54def values(-V: Data, +c: C.Cache<String, V>, 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<String, V>>, 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.
58def complete_keys(-V: Data, +c: C.Cache<String, V>, 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<String, V>}:
59 Equal.cong(List<&2, String>, P.Aggregate<String, V>, 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
61def complete_values(-V: Data, +c: C.Cache<String, V>, 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<String, V>}:
62 Equal.cong(List<&2, V>, P.Aggregate<String, V>, 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))