proofs/containers/lru/touch.bend
bend-collections-laws-containers@1.0.0.0 · 84 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/lib/logic.bend as L
3import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
4import bend-collections-laws-containers@1.0.0.0/spec/containers/hash_table.bend as S
5import bend-collections-laws-containers@1.0.0.0/spec/containers/lru.bend as SP
6import bend-collections-laws-containers@1.0.0.0/src/math/u64.bend as W
7import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/keys.bend as K
8import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/state.bend as HT
9import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/state.bend as ST
10import bend-collections-laws-containers@1.0.0.0/proofs/containers/lru/lists.bend as LS
11import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat_list.bend as NL
12
13# The recency list and the model when a slot moves to the newest end.
14
15
16# ---- splitting a list at a member ----
17
18
19
20
21
22# ---- the model ----
23
24# the entry of a live slot
25def ent(~V: Data, +ll: List<&2, U32>, +kl: List<&2, String>, +el: List<&2, Maybe<&2, V>>, +s: Nat, m: Maybe<&2, V>) -> List<&2, SP.Ent<V>>:
26 ST.sent_m(~V, ll, kl, s, m)
27
28def enk_of(~V: Data, +x: String, +key: String, +hx: {S.str_eq(x, key) == True{} : Bool}, +xs: List<&2, SP.Ent<V>>, +h: {S.mem(x, SP.keys_of(~V, xs)) == False{} : Bool}) -> {LS.enk(~V, xs, key) == True{} : Bool}:
29 match xs:
30 case Nil{}:
31 {==}
32 case Con{SP.LE{+k, +v, +t, +d}, +r}:
33 +h1 = NL.or_ff_l(S.str_eq(k, x), S.mem(x, SP.keys_of(~V, r)), h)
34 +ex = K.str_eq_of(x, key, hx)
35 +h2 = L.subst(String, z => {S.str_eq(k, z) == False{} : Bool}, x, key, ex, h1)
36 L.and_intro(Bool.not(S.str_eq(k, key)), LS.enk(~V, r, key), NL.not_f(S.str_eq(k, key), h2), enk_of(~V, x, key, hx, r, NL.or_ff_r(S.str_eq(k, x), S.mem(x, SP.keys_of(~V, r)), h)))
37
38def drop_here(~V: Data, +ll: List<&2, U32>, +kl: List<&2, String>, +el: List<&2, Maybe<&2, V>>, +s: Nat, +m: Maybe<&2, V>, +hm: {HT.some_b(~V, m) == True{} : Bool}, +r: List<&2, SP.Ent<V>>, +key: String, +hk: {S.str_eq(ST.skey(ll, kl, s), key) == True{} : Bool}) -> {SP.drop(~V, SC.append(SP.Ent<V>, ST.sent_m(~V, ll, kl, s, m), r), key) == r : List<&2, SP.Ent<V>>}:
39 match m:
40 case None{}:
41 Empty.absurd({SP.drop(~V, SC.append(SP.Ent<V>, ST.sent_m(~V, ll, kl, s, None{}), r), key) == r : List<&2, SP.Ent<V>>}, L.false_true(hm))
42 case Some{v}:
43 L.subst(Bool, z => {Bool.pick(List<&2, SP.Ent<V>>, z, r, Con{SP.LE{ST.skey(ll, kl, s), v, ST.lw(ll, s, 3n), W.U64{ST.lw(ll, s, 4n), ST.lw(ll, s, 5n)}}, SP.drop(~V, r, key)}) == r : List<&2, SP.Ent<V>>}, True{}, S.str_eq(ST.skey(ll, kl, s), key), Equal.sym(Bool, S.str_eq(ST.skey(ll, kl, s), key), True{}, hk), {==})
44
45def keys_here(~V: Data, +ll: List<&2, U32>, +kl: List<&2, String>, +el: List<&2, Maybe<&2, V>>, +s: Nat, +m: Maybe<&2, V>, +hm: {HT.some_b(~V, m) == True{} : Bool}, +r: List<&2, SP.Ent<V>>) -> {SP.keys_of(~V, SC.append(SP.Ent<V>, ST.sent_m(~V, ll, kl, s, m), r)) == Con{ST.skey(ll, kl, s), SP.keys_of(~V, r)} : List<&2, String>}:
46 match m:
47 case None{}:
48 Empty.absurd({SP.keys_of(~V, SC.append(SP.Ent<V>, ST.sent_m(~V, ll, kl, s, None{}), r)) == Con{ST.skey(ll, kl, s), SP.keys_of(~V, r)} : List<&2, String>}, L.false_true(hm))
49 case Some{v}:
50 {==}
51
52# keys unique and s holding key: no slot of a holds it
53def enk_a(~V: Data, +ll: List<&2, U32>, +kl: List<&2, String>, +el: List<&2, Maybe<&2, V>>, +a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +hl: {ST.live(~V, el, s) == True{} : Bool}, +key: String, +hk: {S.str_eq(ST.skey(ll, kl, s), key) == True{} : Bool}, +hnd: {S.nodup(SP.keys_of(~V, ST.es(~V, ll, kl, el, SC.append(Nat, a, Con{s, b})))) == True{} : Bool}) -> {LS.enk(~V, ST.es(~V, ll, kl, el, a), key) == True{} : Bool}:
54 +ka = SP.keys_of(~V, ST.es(~V, ll, kl, el, a))
55 +kb = SP.keys_of(~V, ST.es(~V, ll, kl, el, b))
56 +e1 = Equal.trans(List<&2, String>, SP.keys_of(~V, ST.es(~V, ll, kl, el, SC.append(Nat, a, Con{s, b}))), SP.keys_of(~V, SC.append(SP.Ent<V>, ST.es(~V, ll, kl, el, a), ST.es(~V, ll, kl, el, Con{s, b}))), SC.append(String, ka, Con{ST.skey(ll, kl, s), kb}), Equal.cong(List<&2, SP.Ent<V>>, List<&2, String>, z => SP.keys_of(~V, z), ST.es(~V, ll, kl, el, SC.append(Nat, a, Con{s, b})), SC.append(SP.Ent<V>, ST.es(~V, ll, kl, el, a), ST.es(~V, ll, kl, el, Con{s, b})), LS.es_app(~V, ll, kl, el, a, Con{s, b})), Equal.trans(List<&2, String>, SP.keys_of(~V, SC.append(SP.Ent<V>, ST.es(~V, ll, kl, el, a), ST.es(~V, ll, kl, el, Con{s, b}))), SC.append(String, ka, SP.keys_of(~V, ST.es(~V, ll, kl, el, Con{s, b}))), SC.append(String, ka, Con{ST.skey(ll, kl, s), kb}), LS.keys_app(~V, ST.es(~V, ll, kl, el, a), ST.es(~V, ll, kl, el, Con{s, b})), Equal.cong(List<&2, String>, List<&2, String>, z => SC.append(String, ka, z), SP.keys_of(~V, ST.es(~V, ll, kl, el, Con{s, b})), Con{ST.skey(ll, kl, s), kb}, keys_here(~V, ll, kl, el, s, HT.nthm(~V, el, s), hl, ST.es(~V, ll, kl, el, b)))))
57 +h2 = L.subst(List<&2, String>, z => {S.nodup(z) == True{} : Bool}, SP.keys_of(~V, ST.es(~V, ll, kl, el, SC.append(Nat, a, Con{s, b}))), SC.append(String, ka, Con{ST.skey(ll, kl, s), kb}), e1, hnd)
58 +h3 = L.and_right(S.nodup(SC.append(String, ka, kb)), Bool.not(S.mem(ST.skey(ll, kl, s), SC.append(String, ka, kb))), L.subst(Bool, z => {z == True{} : Bool}, S.nodup(SC.append(String, ka, Con{ST.skey(ll, kl, s), kb})), Bool.and(S.nodup(SC.append(String, ka, kb)), Bool.not(S.mem(ST.skey(ll, kl, s), SC.append(String, ka, kb)))), LS.nd_mid_s(ka, ST.skey(ll, kl, s), kb), h2))
59 +h4 = NL.or_f_l(S.mem(ST.skey(ll, kl, s), ka), S.mem(ST.skey(ll, kl, s), kb), L.subst(Bool, z => {z == False{} : Bool}, S.mem(ST.skey(ll, kl, s), SC.append(String, ka, kb)), Bool.or(S.mem(ST.skey(ll, kl, s), ka), S.mem(ST.skey(ll, kl, s), kb)), LS.mem_app_s(ST.skey(ll, kl, s), ka, kb), L.not_true(S.mem(ST.skey(ll, kl, s), SC.append(String, ka, kb)), h3)))
60 enk_of(~V, ST.skey(ll, kl, s), key, hk, ST.es(~V, ll, kl, el, a), h4)
61
62
63# the model entry of slot s holding value v
64def ev(~V: Data, +ll: List<&2, U32>, +kl: List<&2, String>, +s: Nat, +v: V) -> SP.Ent<V>:
65 SP.LE{ST.skey(ll, kl, s), v, ST.lw(ll, s, 3n), W.U64{ST.lw(ll, s, 4n), ST.lw(ll, s, 5n)}}
66
67def es_cons(~V: Data, +ll: List<&2, U32>, +kl: List<&2, String>, +el: List<&2, Maybe<&2, V>>, +s: Nat, +v: V, +hm: {HT.nthm(~V, el, s) == Some{v} : Maybe<&2, V>}, +b: List<&2, Nat>) -> {ST.es(~V, ll, kl, el, Con{s, b}) == Con{SP.LE{ST.skey(ll, kl, s), v, ST.lw(ll, s, 3n), W.U64{ST.lw(ll, s, 4n), ST.lw(ll, s, 5n)}}, ST.es(~V, ll, kl, el, b)} : List<&2, SP.Ent<V>>}:
68 Equal.cong(Maybe<&2, V>, List<&2, SP.Ent<V>>, z => SC.append(SP.Ent<V>, ST.sent_m(~V, ll, kl, s, z), ST.es(~V, ll, kl, el, b)), HT.nthm(~V, el, s), Some{v}, hm)
69
70# THEOREM (model side of a touch): dropping the key's entry and appending it
71# is the model of the list a ++ b ++ [s]
72def spec_touch(~V: Data, +ll: List<&2, U32>, +kl: List<&2, String>, +el: List<&2, Maybe<&2, V>>, +a: List<&2, Nat>, +s: Nat, +b: List<&2, Nat>, +v: V, +hm: {HT.nthm(~V, el, s) == Some{v} : Maybe<&2, V>}, +key: String, +hk: {S.str_eq(ST.skey(ll, kl, s), key) == True{} : Bool}, +hnd: {S.nodup(SP.keys_of(~V, ST.es(~V, ll, kl, el, SC.append(Nat, a, Con{s, b})))) == True{} : Bool}) -> {SP.snoc(~V, SP.drop(~V, ST.es(~V, ll, kl, el, SC.append(Nat, a, Con{s, b})), key), SP.LE{ST.skey(ll, kl, s), v, ST.lw(ll, s, 3n), W.U64{ST.lw(ll, s, 4n), ST.lw(ll, s, 5n)}}) == ST.es(~V, ll, kl, el, SC.append(Nat, SC.append(Nat, a, b), Con{s, Nil{}})) : List<&2, SP.Ent<V>>}:
73 +hl = L.subst(Maybe<&2, V>, z => {HT.some_b(~V, z) == True{} : Bool}, Some{v}, HT.nthm(~V, el, s), Equal.sym(Maybe<&2, V>, HT.nthm(~V, el, s), Some{v}, hm), {==})
74 +ea = LS.es_app(~V, ll, kl, el, a, Con{s, b})
75 +ec = es_cons(~V, ll, kl, el, s, v, hm, b)
76 +e1 = Equal.trans(List<&2, SP.Ent<V>>, ST.es(~V, ll, kl, el, SC.append(Nat, a, Con{s, b})), SC.append(SP.Ent<V>, ST.es(~V, ll, kl, el, a), ST.es(~V, ll, kl, el, Con{s, b})), SC.append(SP.Ent<V>, ST.es(~V, ll, kl, el, a), Con{SP.LE{ST.skey(ll, kl, s), v, ST.lw(ll, s, 3n), W.U64{ST.lw(ll, s, 4n), ST.lw(ll, s, 5n)}}, ST.es(~V, ll, kl, el, b)}), ea, Equal.cong(List<&2, SP.Ent<V>>, List<&2, SP.Ent<V>>, z => SC.append(SP.Ent<V>, ST.es(~V, ll, kl, el, a), z), ST.es(~V, ll, kl, el, Con{s, b}), Con{SP.LE{ST.skey(ll, kl, s), v, ST.lw(ll, s, 3n), W.U64{ST.lw(ll, s, 4n), ST.lw(ll, s, 5n)}}, ST.es(~V, ll, kl, el, b)}, ec))
77 +hen = enk_a(~V, ll, kl, el, a, s, b, hl, key, hk, hnd)
78 +d1 = LS.drop_app(~V, ST.es(~V, ll, kl, el, a), Con{SP.LE{ST.skey(ll, kl, s), v, ST.lw(ll, s, 3n), W.U64{ST.lw(ll, s, 4n), ST.lw(ll, s, 5n)}}, ST.es(~V, ll, kl, el, b)}, key, hen)
79 +d2 = L.subst(Bool, z => {Bool.pick(List<&2, SP.Ent<V>>, z, ST.es(~V, ll, kl, el, b), Con{SP.LE{ST.skey(ll, kl, s), v, ST.lw(ll, s, 3n), W.U64{ST.lw(ll, s, 4n), ST.lw(ll, s, 5n)}}, SP.drop(~V, ST.es(~V, ll, kl, el, b), key)}) == ST.es(~V, ll, kl, el, b) : List<&2, SP.Ent<V>>}, True{}, S.str_eq(ST.skey(ll, kl, s), key), Equal.sym(Bool, S.str_eq(ST.skey(ll, kl, s), key), True{}, hk), {==})
80 +dr = Equal.trans(List<&2, SP.Ent<V>>, SP.drop(~V, SC.append(SP.Ent<V>, ST.es(~V, ll, kl, el, a), Con{SP.LE{ST.skey(ll, kl, s), v, ST.lw(ll, s, 3n), W.U64{ST.lw(ll, s, 4n), ST.lw(ll, s, 5n)}}, ST.es(~V, ll, kl, el, b)}), key), SC.append(SP.Ent<V>, ST.es(~V, ll, kl, el, a), SP.drop(~V, Con{SP.LE{ST.skey(ll, kl, s), v, ST.lw(ll, s, 3n), W.U64{ST.lw(ll, s, 4n), ST.lw(ll, s, 5n)}}, ST.es(~V, ll, kl, el, b)}, key)), SC.append(SP.Ent<V>, ST.es(~V, ll, kl, el, a), ST.es(~V, ll, kl, el, b)), d1, Equal.cong(List<&2, SP.Ent<V>>, List<&2, SP.Ent<V>>, z => SC.append(SP.Ent<V>, ST.es(~V, ll, kl, el, a), z), SP.drop(~V, Con{SP.LE{ST.skey(ll, kl, s), v, ST.lw(ll, s, 3n), W.U64{ST.lw(ll, s, 4n), ST.lw(ll, s, 5n)}}, ST.es(~V, ll, kl, el, b)}, key), ST.es(~V, ll, kl, el, b), d2))
81 +d3 = Equal.trans(List<&2, SP.Ent<V>>, SP.drop(~V, ST.es(~V, ll, kl, el, SC.append(Nat, a, Con{s, b})), key), SP.drop(~V, SC.append(SP.Ent<V>, ST.es(~V, ll, kl, el, a), Con{SP.LE{ST.skey(ll, kl, s), v, ST.lw(ll, s, 3n), W.U64{ST.lw(ll, s, 4n), ST.lw(ll, s, 5n)}}, ST.es(~V, ll, kl, el, b)}), key), SC.append(SP.Ent<V>, ST.es(~V, ll, kl, el, a), ST.es(~V, ll, kl, el, b)), Equal.cong(List<&2, SP.Ent<V>>, List<&2, SP.Ent<V>>, z => SP.drop(~V, z, key), ST.es(~V, ll, kl, el, SC.append(Nat, a, Con{s, b})), SC.append(SP.Ent<V>, ST.es(~V, ll, kl, el, a), Con{SP.LE{ST.skey(ll, kl, s), v, ST.lw(ll, s, 3n), W.U64{ST.lw(ll, s, 4n), ST.lw(ll, s, 5n)}}, ST.es(~V, ll, kl, el, b)}), e1), dr)
82 +sn = Equal.trans(List<&2, SP.Ent<V>>, SP.snoc(~V, SP.drop(~V, ST.es(~V, ll, kl, el, SC.append(Nat, a, Con{s, b})), key), SP.LE{ST.skey(ll, kl, s), v, ST.lw(ll, s, 3n), W.U64{ST.lw(ll, s, 4n), ST.lw(ll, s, 5n)}}), SP.snoc(~V, SC.append(SP.Ent<V>, ST.es(~V, ll, kl, el, a), ST.es(~V, ll, kl, el, b)), SP.LE{ST.skey(ll, kl, s), v, ST.lw(ll, s, 3n), W.U64{ST.lw(ll, s, 4n), ST.lw(ll, s, 5n)}}), SC.append(SP.Ent<V>, SC.append(SP.Ent<V>, ST.es(~V, ll, kl, el, a), ST.es(~V, ll, kl, el, b)), Con{SP.LE{ST.skey(ll, kl, s), v, ST.lw(ll, s, 3n), W.U64{ST.lw(ll, s, 4n), ST.lw(ll, s, 5n)}}, Nil{}}), Equal.cong(List<&2, SP.Ent<V>>, List<&2, SP.Ent<V>>, z => SP.snoc(~V, z, SP.LE{ST.skey(ll, kl, s), v, ST.lw(ll, s, 3n), W.U64{ST.lw(ll, s, 4n), ST.lw(ll, s, 5n)}}), SP.drop(~V, ST.es(~V, ll, kl, el, SC.append(Nat, a, Con{s, b})), key), SC.append(SP.Ent<V>, ST.es(~V, ll, kl, el, a), ST.es(~V, ll, kl, el, b)), d3), LS.snoc_app(~V, SC.append(SP.Ent<V>, ST.es(~V, ll, kl, el, a), ST.es(~V, ll, kl, el, b)), SP.LE{ST.skey(ll, kl, s), v, ST.lw(ll, s, 3n), W.U64{ST.lw(ll, s, 4n), ST.lw(ll, s, 5n)}}))
83 +r1 = Equal.trans(List<&2, SP.Ent<V>>, ST.es(~V, ll, kl, el, SC.append(Nat, SC.append(Nat, a, b), Con{s, Nil{}})), SC.append(SP.Ent<V>, ST.es(~V, ll, kl, el, SC.append(Nat, a, b)), ST.es(~V, ll, kl, el, Con{s, Nil{}})), SC.append(SP.Ent<V>, SC.append(SP.Ent<V>, ST.es(~V, ll, kl, el, a), ST.es(~V, ll, kl, el, b)), Con{SP.LE{ST.skey(ll, kl, s), v, ST.lw(ll, s, 3n), W.U64{ST.lw(ll, s, 4n), ST.lw(ll, s, 5n)}}, Nil{}}), LS.es_app(~V, ll, kl, el, SC.append(Nat, a, b), Con{s, Nil{}}), Equal.trans(List<&2, SP.Ent<V>>, SC.append(SP.Ent<V>, ST.es(~V, ll, kl, el, SC.append(Nat, a, b)), ST.es(~V, ll, kl, el, Con{s, Nil{}})), SC.append(SP.Ent<V>, SC.append(SP.Ent<V>, ST.es(~V, ll, kl, el, a), ST.es(~V, ll, kl, el, b)), ST.es(~V, ll, kl, el, Con{s, Nil{}})), SC.append(SP.Ent<V>, SC.append(SP.Ent<V>, ST.es(~V, ll, kl, el, a), ST.es(~V, ll, kl, el, b)), Con{SP.LE{ST.skey(ll, kl, s), v, ST.lw(ll, s, 3n), W.U64{ST.lw(ll, s, 4n), ST.lw(ll, s, 5n)}}, Nil{}}), Equal.cong(List<&2, SP.Ent<V>>, List<&2, SP.Ent<V>>, z => SC.append(SP.Ent<V>, z, ST.es(~V, ll, kl, el, Con{s, Nil{}})), ST.es(~V, ll, kl, el, SC.append(Nat, a, b)), SC.append(SP.Ent<V>, ST.es(~V, ll, kl, el, a), ST.es(~V, ll, kl, el, b)), LS.es_app(~V, ll, kl, el, a, b)), Equal.cong(List<&2, SP.Ent<V>>, List<&2, SP.Ent<V>>, z => SC.append(SP.Ent<V>, SC.append(SP.Ent<V>, ST.es(~V, ll, kl, el, a), ST.es(~V, ll, kl, el, b)), z), ST.es(~V, ll, kl, el, Con{s, Nil{}}), Con{SP.LE{ST.skey(ll, kl, s), v, ST.lw(ll, s, 3n), W.U64{ST.lw(ll, s, 4n), ST.lw(ll, s, 5n)}}, Nil{}}, es_cons(~V, ll, kl, el, s, v, hm, Nil{}))))
84 Equal.trans(List<&2, SP.Ent<V>>, SP.snoc(~V, SP.drop(~V, ST.es(~V, ll, kl, el, SC.append(Nat, a, Con{s, b})), key), SP.LE{ST.skey(ll, kl, s), v, ST.lw(ll, s, 3n), W.U64{ST.lw(ll, s, 4n), ST.lw(ll, s, 5n)}}), SC.append(SP.Ent<V>, SC.append(SP.Ent<V>, ST.es(~V, ll, kl, el, a), ST.es(~V, ll, kl, el, b)), Con{SP.LE{ST.skey(ll, kl, s), v, ST.lw(ll, s, 3n), W.U64{ST.lw(ll, s, 4n), ST.lw(ll, s, 5n)}}, Nil{}}), ST.es(~V, ll, kl, el, SC.append(Nat, SC.append(Nat, a, b), Con{s, Nil{}})), sn, Equal.sym(List<&2, SP.Ent<V>>, ST.es(~V, ll, kl, el, SC.append(Nat, SC.append(Nat, a, b), Con{s, Nil{}})), SC.append(SP.Ent<V>, SC.append(SP.Ent<V>, ST.es(~V, ll, kl, el, a), ST.es(~V, ll, kl, el, b)), Con{SP.LE{ST.skey(ll, kl, s), v, ST.lw(ll, s, 3n), W.U64{ST.lw(ll, s, 4n), ST.lw(ll, s, 5n)}}, Nil{}}), r1))