1 import Base 2 import ../../lib/logic.bend as L 3 import ../../lib/nat.bend as N 4 import ../../../spec/lib/common.bend as SC 5 import ../../../spec/containers/hash_table.bend as S 6 import ../../../spec/containers/lru.bend as SP 7 import ../../../src/math/u64.bend as W 8 import ../hash_table/keys.bend as K 9 import ../hash_table/words.bend as WR 10 import ../hash_table/state.bend as HT 11 import ./state.bend as ST 12 import ../../lib/nat_list.bend as NL 13 14 # The model's entries along the recency list: find, membership of keys. 15 16 17 # slot s's entry as find returns it (m is its value cell) 18 def fnd(~V: Data, +ll: List<&2, U32>, +kl: List<&2, String>, +s: Nat, m: Maybe<&2, V>) -> Maybe<&2, SP.Ent>: 19 match m: 20 case None{}: 21 None{} 22 case Some{v}: 23 Some{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)}}} 24 25 def or_r(+a: Bool, +b: Bool, +h: {b == True{} : Bool}) -> {Bool.or(a, b) == True{} : Bool}: 26 L.subst(Bool, z => {Bool.or(a, z) == True{} : Bool}, True{}, b, Equal.sym(Bool, b, True{}, h), WR.or_true(a)) 27 28 # ---- membership of keys ---- 29 30 def mk_here(~V: Data, +ll: List<&2, U32>, +kl: List<&2, String>, +s: Nat, +m: Maybe<&2, V>, +hm: {HT.some_b(~V, m) == True{} : Bool}, +r: List<&2, SP.Ent>) -> {S.mem(ST.skey(ll, kl, s), SP.keys_of(~V, SC.append(SP.Ent, ST.sent_m(~V, ll, kl, s, m), r))) == True{} : Bool}: 31 match m: 32 case None{}: 33 Empty.absurd({S.mem(ST.skey(ll, kl, s), SP.keys_of(~V, SC.append(SP.Ent, ST.sent_m(~V, ll, kl, s, None{}), r))) == True{} : Bool}, L.false_true(hm)) 34 case Some{v}: 35 L.subst(Bool, z => {Bool.or(z, S.mem(ST.skey(ll, kl, s), SP.keys_of(~V, r))) == True{} : Bool}, True{}, S.str_eq(ST.skey(ll, kl, s), ST.skey(ll, kl, s)), Equal.sym(Bool, S.str_eq(ST.skey(ll, kl, s), ST.skey(ll, kl, s)), True{}, K.str_refl(ST.skey(ll, kl, s))), {==}) 36 37 def mk_there(~V: Data, +ll: List<&2, U32>, +kl: List<&2, String>, +x: String, +s0: Nat, +m: Maybe<&2, V>, +r: List<&2, SP.Ent>, +h: {S.mem(x, SP.keys_of(~V, r)) == True{} : Bool}) -> {S.mem(x, SP.keys_of(~V, SC.append(SP.Ent, ST.sent_m(~V, ll, kl, s0, m), r))) == True{} : Bool}: 38 match m: 39 case None{}: 40 h 41 case Some{v}: 42 L.subst(Bool, z => {Bool.or(S.str_eq(ST.skey(ll, kl, s0), x), z) == True{} : Bool}, True{}, S.mem(x, SP.keys_of(~V, r)), Equal.sym(Bool, S.mem(x, SP.keys_of(~V, r)), True{}, h), WR.or_true(S.str_eq(ST.skey(ll, kl, s0), x))) 43 44 def mk_c(~V: Data, +ll: List<&2, U32>, +kl: List<&2, String>, +el: List<&2, Maybe<&2, V>>, +s: Nat, +s0: Nat, +t: List<&2, Nat>, +hl: {ST.live(~V, el, s) == True{} : Bool}, +c: Bool, +hc: {Nat.is_eq(s0, s) == c : Bool}, +hm: {Bool.or(c, NL.memn(s, t)) == True{} : Bool}, rec: @h: {NL.memn(s, t) == True{} : Bool} -> {S.mem(ST.skey(ll, kl, s), SP.keys_of(~V, ST.es(~V, ll, kl, el, t))) == True{} : Bool}) -> {S.mem(ST.skey(ll, kl, s), SP.keys_of(~V, ST.es(~V, ll, kl, el, Con{s0, t}))) == True{} : Bool}: 45 match c: 46 case True{}: 47 +e = N.eq_from_is_eq(s0, s, hc) 48 L.subst(Nat, z => {S.mem(ST.skey(ll, kl, s), SP.keys_of(~V, SC.append(SP.Ent, ST.sent_m(~V, ll, kl, z, HT.nthm(~V, el, z)), ST.es(~V, ll, kl, el, t)))) == True{} : Bool}, s, s0, Equal.sym(Nat, s0, s, e), mk_here(~V, ll, kl, s, HT.nthm(~V, el, s), hl, ST.es(~V, ll, kl, el, t))) 49 case False{}: 50 mk_there(~V, ll, kl, ST.skey(ll, kl, s), s0, HT.nthm(~V, el, s0), ST.es(~V, ll, kl, el, t), rec(hm)) 51 52 # a live slot on the list has its key among the model's keys 53 def mem_keys(~V: Data, +ll: List<&2, U32>, +kl: List<&2, String>, +el: List<&2, Maybe<&2, V>>, +s: Nat, +hl: {ST.live(~V, el, s) == True{} : Bool}, +sl: List<&2, Nat>, +hm: {NL.memn(s, sl) == True{} : Bool}) -> {S.mem(ST.skey(ll, kl, s), SP.keys_of(~V, ST.es(~V, ll, kl, el, sl))) == True{} : Bool}: 54 match sl: 55 case Nil{}: 56 Empty.absurd({S.mem(ST.skey(ll, kl, s), SP.keys_of(~V, ST.es(~V, ll, kl, el, Nil{}))) == True{} : Bool}, L.false_true(hm)) 57 case Con{+s0, +t}: 58 mk_c(~V, ll, kl, el, s, s0, t, hl, Nat.is_eq(s0, s), {==}, hm, h => mem_keys(~V, ll, kl, el, s, hl, t, h)) 59 60 # ---- find ---- 61 62 def not_true_f(+b: Bool, +h: {Bool.not(b) == True{} : Bool}) -> {b == False{} : Bool}: 63 K.not_true_eq(b, h) 64 65 # an entry whose key is not key is skipped 66 def find_skip(~V: Data, +ll: List<&2, U32>, +kl: List<&2, String>, +s0: Nat, +m: Maybe<&2, V>, +r: List<&2, SP.Ent>, +key: String, +hk: {Bool.or(Bool.not(HT.some_b(~V, m)), Bool.not(S.str_eq(ST.skey(ll, kl, s0), key))) == True{} : Bool}) -> {SP.find(~V, SC.append(SP.Ent, ST.sent_m(~V, ll, kl, s0, m), r), key) == SP.find(~V, r, key) : Maybe<&2, SP.Ent>}: 67 match m: 68 case None{}: 69 {==} 70 case Some{v}: 71 +ef = not_true_f(S.str_eq(ST.skey(ll, kl, s0), key), hk) 72 L.subst(Bool, z => {Bool.pick(Maybe<&2, SP.Ent>, z, Some{SP.LE{ST.skey(ll, kl, s0), v, ST.lw(ll, s0, 3n), W.U64{ST.lw(ll, s0, 4n), ST.lw(ll, s0, 5n)}}}, SP.find(~V, r, key)) == SP.find(~V, r, key) : Maybe<&2, SP.Ent>}, False{}, S.str_eq(ST.skey(ll, kl, s0), key), Equal.sym(Bool, S.str_eq(ST.skey(ll, kl, s0), key), False{}, ef), {==}) 73 74 # the entry holding key is found 75 def find_here(~V: Data, +ll: List<&2, U32>, +kl: List<&2, String>, +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.find(~V, SC.append(SP.Ent, ST.sent_m(~V, ll, kl, s, m), r), key) == fnd(~V, ll, kl, s, m) : Maybe<&2, SP.Ent>}: 76 match m: 77 case None{}: 78 Empty.absurd({SP.find(~V, SC.append(SP.Ent, ST.sent_m(~V, ll, kl, s, None{}), r), key) == fnd(~V, ll, kl, s, None{}) : Maybe<&2, SP.Ent>}, L.false_true(hm)) 79 case Some{v}: 80 L.subst(Bool, z => {Bool.pick(Maybe<&2, SP.Ent>, z, Some{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.find(~V, r, key)) == Some{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)}}} : Maybe<&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), {==}) 81 82 # the key of an earlier slot differs (keys are unique), and the rest of the 83 # keys are unique 84 def split_d(~V: Data, +ll: List<&2, U32>, +kl: List<&2, String>, +el: List<&2, Maybe<&2, V>>, +s: Nat, +hl: {ST.live(~V, el, s) == True{} : Bool}, +t: List<&2, Nat>, +hmt: {NL.memn(s, t) == True{} : Bool}, +key: String, +hk: {S.str_eq(ST.skey(ll, kl, s), key) == True{} : Bool}, +s0: Nat, +d: Bool, +hd: {S.str_eq(ST.skey(ll, kl, s0), key) == d : Bool}, +hn: {Bool.not(S.mem(ST.skey(ll, kl, s0), SP.keys_of(~V, ST.es(~V, ll, kl, el, t)))) == True{} : Bool}) -> {Bool.not(d) == True{} : Bool}: 85 match d: 86 case False{}: 87 {==} 88 case True{}: 89 +e0 = K.str_eq_of(ST.skey(ll, kl, s0), key, hd) 90 +e1 = K.str_eq_of(ST.skey(ll, kl, s), key, hk) 91 +e = Equal.trans(String, ST.skey(ll, kl, s), key, ST.skey(ll, kl, s0), e1, Equal.sym(String, ST.skey(ll, kl, s0), key, e0)) 92 +hin = L.subst(String, z => {S.mem(z, SP.keys_of(~V, ST.es(~V, ll, kl, el, t))) == True{} : Bool}, ST.skey(ll, kl, s), ST.skey(ll, kl, s0), e, mem_keys(~V, ll, kl, el, s, hl, t, hmt)) 93 Empty.absurd({Bool.not(True{}) == True{} : Bool}, L.false_true(L.subst(Bool, z => {Bool.not(z) == True{} : Bool}, S.mem(ST.skey(ll, kl, s0), SP.keys_of(~V, ST.es(~V, ll, kl, el, t))), True{}, hin, hn))) 94 95 def split_m1(~V: Data, +ll: List<&2, U32>, +kl: List<&2, String>, +el: List<&2, Maybe<&2, V>>, +s: Nat, +hl: {ST.live(~V, el, s) == True{} : Bool}, +t: List<&2, Nat>, +hmt: {NL.memn(s, t) == True{} : Bool}, +key: String, +hk: {S.str_eq(ST.skey(ll, kl, s), key) == True{} : Bool}, +s0: Nat, +m: Maybe<&2, V>, +hnd: {S.nodup(SP.keys_of(~V, SC.append(SP.Ent, ST.sent_m(~V, ll, kl, s0, m), ST.es(~V, ll, kl, el, t)))) == True{} : Bool}) -> {Bool.or(Bool.not(HT.some_b(~V, m)), Bool.not(S.str_eq(ST.skey(ll, kl, s0), key))) == True{} : Bool}: 96 match m: 97 case None{}: 98 {==} 99 case Some{v}: 100 +hn = L.and_left(Bool.not(S.mem(ST.skey(ll, kl, s0), SP.keys_of(~V, ST.es(~V, ll, kl, el, t)))), S.nodup(SP.keys_of(~V, ST.es(~V, ll, kl, el, t))), hnd) 101 split_d(~V, ll, kl, el, s, hl, t, hmt, key, hk, s0, S.str_eq(ST.skey(ll, kl, s0), key), {==}, hn) 102 103 # the keys after an entry are unique 104 def nd_tail(~V: Data, +ll: List<&2, U32>, +kl: List<&2, String>, +el: List<&2, Maybe<&2, V>>, +t: List<&2, Nat>, +s0: Nat, +m: Maybe<&2, V>, +hnd: {S.nodup(SP.keys_of(~V, SC.append(SP.Ent, ST.sent_m(~V, ll, kl, s0, m), ST.es(~V, ll, kl, el, t)))) == True{} : Bool}) -> {S.nodup(SP.keys_of(~V, ST.es(~V, ll, kl, el, t))) == True{} : Bool}: 105 match m: 106 case None{}: 107 hnd 108 case Some{v}: 109 L.and_right(Bool.not(S.mem(ST.skey(ll, kl, s0), SP.keys_of(~V, ST.es(~V, ll, kl, el, t)))), S.nodup(SP.keys_of(~V, ST.es(~V, ll, kl, el, t))), hnd) 110 111 def fh_c(~V: Data, +ll: List<&2, U32>, +kl: List<&2, String>, +el: List<&2, Maybe<&2, V>>, +s: Nat, +hl: {ST.live(~V, el, s) == True{} : Bool}, +key: String, +hk: {S.str_eq(ST.skey(ll, kl, s), key) == True{} : Bool}, +s0: Nat, +t: List<&2, Nat>, +hnd: {S.nodup(SP.keys_of(~V, ST.es(~V, ll, kl, el, Con{s0, t}))) == True{} : Bool}, +c: Bool, +hc: {Nat.is_eq(s0, s) == c : Bool}, +hm: {Bool.or(c, NL.memn(s, t)) == True{} : Bool}, rec: @h: {NL.memn(s, t) == True{} : Bool} -> @hn: {S.nodup(SP.keys_of(~V, ST.es(~V, ll, kl, el, t))) == True{} : Bool} -> {SP.find(~V, ST.es(~V, ll, kl, el, t), key) == fnd(~V, ll, kl, s, HT.nthm(~V, el, s)) : Maybe<&2, SP.Ent>}) -> {SP.find(~V, ST.es(~V, ll, kl, el, Con{s0, t}), key) == fnd(~V, ll, kl, s, HT.nthm(~V, el, s)) : Maybe<&2, SP.Ent>}: 112 match c: 113 case True{}: 114 +e = N.eq_from_is_eq(s0, s, hc) 115 L.subst(Nat, z => {SP.find(~V, SC.append(SP.Ent, ST.sent_m(~V, ll, kl, z, HT.nthm(~V, el, z)), ST.es(~V, ll, kl, el, t)), key) == fnd(~V, ll, kl, s, HT.nthm(~V, el, s)) : Maybe<&2, SP.Ent>}, s, s0, Equal.sym(Nat, s0, s, e), find_here(~V, ll, kl, s, HT.nthm(~V, el, s), hl, ST.es(~V, ll, kl, el, t), key, hk)) 116 case False{}: 117 Equal.trans(Maybe<&2, SP.Ent>, SP.find(~V, ST.es(~V, ll, kl, el, Con{s0, t}), key), SP.find(~V, ST.es(~V, ll, kl, el, t), key), fnd(~V, ll, kl, s, HT.nthm(~V, el, s)), find_skip(~V, ll, kl, s0, HT.nthm(~V, el, s0), ST.es(~V, ll, kl, el, t), key, split_m1(~V, ll, kl, el, s, hl, t, hm, key, hk, s0, HT.nthm(~V, el, s0), hnd)), rec(hm, nd_tail(~V, ll, kl, el, t, s0, HT.nthm(~V, el, s0), hnd))) 118 119 # THEOREM (model side): a live listed slot holding key is what find returns 120 def find_hit(~V: Data, +ll: List<&2, U32>, +kl: List<&2, String>, +el: List<&2, Maybe<&2, V>>, +s: Nat, +hl: {ST.live(~V, el, s) == True{} : Bool}, +key: String, +hk: {S.str_eq(ST.skey(ll, kl, s), key) == True{} : Bool}, +sl: List<&2, Nat>, +hm: {NL.memn(s, sl) == True{} : Bool}, +hnd: {S.nodup(SP.keys_of(~V, ST.es(~V, ll, kl, el, sl))) == True{} : Bool}) -> {SP.find(~V, ST.es(~V, ll, kl, el, sl), key) == fnd(~V, ll, kl, s, HT.nthm(~V, el, s)) : Maybe<&2, SP.Ent>}: 121 match sl: 122 case Nil{}: 123 Empty.absurd({SP.find(~V, ST.es(~V, ll, kl, el, Nil{}), key) == fnd(~V, ll, kl, s, HT.nthm(~V, el, s)) : Maybe<&2, SP.Ent>}, L.false_true(hm)) 124 case Con{+s0, +t}: 125 fh_c(~V, ll, kl, el, s, hl, key, hk, s0, t, hnd, Nat.is_eq(s0, s), {==}, hm, h => hn => find_hit(~V, ll, kl, el, s, hl, key, hk, t, h, hn)) 126 127 # no listed slot holds key: find returns nothing 128 def find_miss(~V: Data, +ll: List<&2, U32>, +kl: List<&2, String>, +el: List<&2, Maybe<&2, V>>, +key: String, +sl: List<&2, Nat>, +h: {ST.nokey(~V, ll, kl, sl, key) == True{} : Bool}) -> {SP.find(~V, ST.es(~V, ll, kl, el, sl), key) == None{} : Maybe<&2, SP.Ent>}: 129 match sl: 130 case Nil{}: 131 {==} 132 case Con{+s0, +t}: 133 +h0 = L.and_left(Bool.not(S.str_eq(ST.skey(ll, kl, s0), key)), ST.nokey(~V, ll, kl, t, key), h) 134 Equal.trans(Maybe<&2, SP.Ent>, SP.find(~V, ST.es(~V, ll, kl, el, Con{s0, t}), key), SP.find(~V, ST.es(~V, ll, kl, el, t), key), None{}, find_skip(~V, ll, kl, s0, HT.nthm(~V, el, s0), ST.es(~V, ll, kl, el, t), key, or_r(Bool.not(HT.some_b(~V, HT.nthm(~V, el, s0))), Bool.not(S.str_eq(ST.skey(ll, kl, s0), key)), h0)), find_miss(~V, ll, kl, el, key, t, L.and_right(Bool.not(S.str_eq(ST.skey(ll, kl, s0), key)), ST.nokey(~V, ll, kl, t, key), h)))