1 import Base 2 import ../../lib/logic.bend as L 3 import ../../../spec/lib/common.bend as SC 4 import ../../../spec/containers/hash_table.bend as S 5 import ../../../spec/containers/lru.bend as SP 6 import ../../../src/math/u64.bend as W 7 import ../hash_table/keys.bend as K 8 import ../hash_table/state.bend as HT 9 import ./state.bend as ST 10 import ./lists.bend as LS 11 import ../../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 25 def 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>: 26 ST.sent_m(~V, ll, kl, s, m) 27 28 def enk_of(~V: Data, +x: String, +key: String, +hx: {S.str_eq(x, key) == True{} : Bool}, +xs: List<&2, SP.Ent>, +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 38 def 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>, +key: String, +hk: {S.str_eq(ST.skey(ll, kl, s), key) == True{} : Bool}) -> {SP.drop(~V, SC.append(SP.Ent, ST.sent_m(~V, ll, kl, s, m), r), key) == r : List<&2, SP.Ent>}: 39 match m: 40 case None{}: 41 Empty.absurd({SP.drop(~V, SC.append(SP.Ent, ST.sent_m(~V, ll, kl, s, None{}), r), key) == r : List<&2, SP.Ent>}, L.false_true(hm)) 42 case Some{v}: 43 L.subst(Bool, z => {Bool.pick(List<&2, SP.Ent>, 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>}, 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 45 def 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>) -> {SP.keys_of(~V, SC.append(SP.Ent, 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, 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 53 def 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, 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>, 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, 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, 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 64 def ev(~V: Data, +ll: List<&2, U32>, +kl: List<&2, String>, +s: Nat, +v: V) -> SP.Ent: 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 67 def 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>}: 68 Equal.cong(Maybe<&2, V>, List<&2, SP.Ent>, z => SC.append(SP.Ent, 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] 72 def 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>}: 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>, ST.es(~V, ll, kl, el, SC.append(Nat, a, Con{s, b})), SC.append(SP.Ent, ST.es(~V, ll, kl, el, a), ST.es(~V, ll, kl, el, Con{s, b})), SC.append(SP.Ent, 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>, List<&2, SP.Ent>, z => SC.append(SP.Ent, 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>, 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>}, 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>, SP.drop(~V, SC.append(SP.Ent, 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, 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, ST.es(~V, ll, kl, el, a), ST.es(~V, ll, kl, el, b)), d1, Equal.cong(List<&2, SP.Ent>, List<&2, SP.Ent>, z => SC.append(SP.Ent, 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>, SP.drop(~V, ST.es(~V, ll, kl, el, SC.append(Nat, a, Con{s, b})), key), SP.drop(~V, SC.append(SP.Ent, 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, ST.es(~V, ll, kl, el, a), ST.es(~V, ll, kl, el, b)), Equal.cong(List<&2, SP.Ent>, List<&2, SP.Ent>, z => SP.drop(~V, z, key), ST.es(~V, ll, kl, el, SC.append(Nat, a, Con{s, b})), SC.append(SP.Ent, 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>, 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, 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, SC.append(SP.Ent, 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>, List<&2, SP.Ent>, 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, ST.es(~V, ll, kl, el, a), ST.es(~V, ll, kl, el, b)), d3), LS.snoc_app(~V, SC.append(SP.Ent, 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>, ST.es(~V, ll, kl, el, SC.append(Nat, SC.append(Nat, a, b), Con{s, Nil{}})), SC.append(SP.Ent, ST.es(~V, ll, kl, el, SC.append(Nat, a, b)), ST.es(~V, ll, kl, el, Con{s, Nil{}})), SC.append(SP.Ent, SC.append(SP.Ent, 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>, SC.append(SP.Ent, ST.es(~V, ll, kl, el, SC.append(Nat, a, b)), ST.es(~V, ll, kl, el, Con{s, Nil{}})), SC.append(SP.Ent, SC.append(SP.Ent, 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, SC.append(SP.Ent, 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>, List<&2, SP.Ent>, z => SC.append(SP.Ent, 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, 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>, List<&2, SP.Ent>, z => SC.append(SP.Ent, SC.append(SP.Ent, 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>, 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, SC.append(SP.Ent, 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>, ST.es(~V, ll, kl, el, SC.append(Nat, SC.append(Nat, a, b), Con{s, Nil{}})), SC.append(SP.Ent, SC.append(SP.Ent, 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))