1 import Base 2 import ../../lib/logic.bend as L 3 import ../../lib/list.bend as LL 4 import ../../lib/array.bend as AR 5 import ../../../spec/lib/common.bend as SC 6 import ../../../spec/containers/hash_table.bend as S 7 import ../../lib/u32div.bend as UD 8 import ../../../src/containers/hash_table.bend as H 9 import ./strings.bend as STR 10 import ./table.bend as TB 11 import ./arr.bend as AX 12 import ./buckets.bend as B 13 import ../../lib/words32.bend as W32 14 15 # The implementation's probe step for a long key, on arrays built from mirror 16 # trees: it reads bucket i's word x and link l; on a word match it swaps the 17 # stored key out, compares and puts it back (the stored keys are unchanged). 18 19 def step_of(ms: B.MS, tab: Array, ks: Array, key: String) -> H.Step: 20 match ms: 21 case B.MEnd{}: 22 H.SEnd{tab, ks, key} 23 case B.MHit{l}: 24 H.SHit{tab, ks, key, l} 25 case B.MNext{}: 26 H.SNext{tab, ks, key} 27 28 def pick_step(tab: Array, +l: U32, ks: Array, key: String, +e: Bool) -> {H.sk_pick(tab, l, ks, key, e) == step_of(Bool.pick(B.MS, e, B.MHit{l}, B.MNext{}), tab, ks, key) : H.Step}: 29 match e: 30 case True{}: 31 {==} 32 case False{}: 33 {==} 34 35 # the stored keys after a compare at link l: taken out, put back 36 def kcmp(+sd: Nat, +ksT: AR.Tree, +l: U32) -> AR.Tree: 37 AR.upd(String, sd, AR.upd(String, sd, ksT, UD.v(H.slot(l)), SNil{}), UD.v(H.slot(l)), TB.nths(AR.slots(String, ksT), UD.v(H.slot(l)))) 38 39 def kcmp_slots(+sd: Nat, +ksT: AR.Tree, +l: U32, +hs: {Nat.is_lt(UD.v(H.slot(l)), SC.pow2(sd)) == True{} : Bool}, +pk: {AR.perfect(String, sd, ksT) == True{} : Bool}) -> {AR.slots(String, kcmp(sd, ksT, l)) == AR.slots(String, ksT) : List<&2, String>}: 40 +j = UD.v(H.slot(l)) 41 +kl = AR.slots(String, ksT) 42 +k1 = AR.upd(String, sd, ksT, j, SNil{}) 43 +p1 = AR.upd_perfect(String, sd, ksT, j, SNil{}, pk) 44 +e1 = AR.upd_slots(String, sd, k1, j, TB.nths(kl, j), hs, p1) 45 +e2 = Equal.cong(List<&2, String>, List<&2, String>, z => SC.update(String, z, j, TB.nths(kl, j)), AR.slots(String, k1), SC.update(String, kl, j, SNil{}), AR.upd_slots(String, sd, ksT, j, SNil{}, hs, pk)) 46 Equal.trans(List<&2, String>, AR.slots(String, kcmp(sd, ksT, l)), SC.update(String, AR.slots(String, k1), j, TB.nths(kl, j)), kl, e1, 47 Equal.trans(List<&2, String>, SC.update(String, AR.slots(String, k1), j, TB.nths(kl, j)), SC.update(String, SC.update(String, kl, j, SNil{}), j, TB.nths(kl, j)), kl, e2, 48 Equal.trans(List<&2, String>, SC.update(String, SC.update(String, kl, j, SNil{}), j, TB.nths(kl, j)), SC.update(String, kl, j, TB.nths(kl, j)), kl, TB.upd_upd(kl, j, SNil{}, TB.nths(kl, j)), TB.upd_self(kl, j)))) 49 50 def kcmp_perfect(+sd: Nat, +ksT: AR.Tree, +l: U32, +pk: {AR.perfect(String, sd, ksT) == True{} : Bool}) -> {AR.perfect(String, sd, kcmp(sd, ksT, l)) == True{} : Bool}: 51 AR.upd_perfect(String, sd, AR.upd(String, sd, ksT, UD.v(H.slot(l)), SNil{}), UD.v(H.slot(l)), TB.nths(AR.slots(String, ksT), UD.v(H.slot(l))), AR.upd_perfect(String, sd, ksT, UD.v(H.slot(l)), SNil{}, pk)) 52 53 # comparing the probed key with the key stored at link l 54 def cmp_path(tab: Array, +sd: Nat, +ksT: AR.Tree, +l: U32, +key: String, +hsd: {Nat.is_lt(sd, 32n) == True{} : Bool}, +hs: {Nat.is_lt(UD.v(H.slot(l)), SC.pow2(sd)) == True{} : Bool}, +pk: {AR.perfect(String, sd, ksT) == True{} : Bool}) -> {H.sk_same(tab, AR.thaw(String, ksT), l, key, True{}) == step_of(Bool.pick(B.MS, S.str_eq(key, TB.nths(AR.slots(String, ksT), UD.v(H.slot(l)))), B.MHit{l}, B.MNext{}), tab, AR.thaw(String, kcmp(sd, ksT, l)), key) : H.Step}: 55 +j = UD.v(H.slot(l)) 56 +kl = AR.slots(String, ksT) 57 +k = TB.nths(kl, j) 58 +k1 = AR.upd(String, sd, ksT, j, SNil{}) 59 +e = S.str_eq(key, k) 60 +hsw = AR.swap(String, sd, ksT, H.slot(l), SNil{}, k, hsd, hs, AX.nths_of(sd, ksT, j, hs, pk), pk) 61 +hk1 = L.subst(List<&2, String>, ys => {SC.nth(String, ys, j) == Some{SNil{}} : Maybe<&2, String>}, SC.update(String, kl, j, SNil{}), AR.slots(String, k1), Equal.sym(List<&2, String>, AR.slots(String, k1), SC.update(String, kl, j, SNil{}), AR.upd_slots(String, sd, ksT, j, SNil{}, hs, pk)), LL.nth_update_same(String, kl, j, SNil{}, LL.nth_lt_length(String, kl, j, k, AX.nths_of(sd, ksT, j, hs, pk)))) 62 +hset = AR.set(String, sd, k1, H.slot(l), k, SNil{}, hsd, hs, hk1, AR.upd_perfect(String, sd, ksT, j, SNil{}, pk)) 63 +s1 = Equal.cong(Array & String, H.Step, r => H.sk_cmp(tab, l, key, r), Array.swap(String, AR.thaw(String, ksT), H.slot(l), SNil{}), (AR.thaw(String, k1), k), hsw) 64 +s2 = Equal.cong((String & String) & Bool, H.Step, r => H.sk_fin(tab, l, AR.thaw(String, k1), r), H.eq(key, k), ((key, k), e), STR.eq(key, k)) 65 +s3 = Equal.cong(Array, H.Step, a => H.sk_pick(tab, l, a, key, e), Array.set(String, AR.thaw(String, k1), H.slot(l), k), AR.thaw(String, kcmp(sd, ksT, l)), hset) 66 Equal.trans(H.Step, H.sk_cmp(tab, l, key, Array.swap(String, AR.thaw(String, ksT), H.slot(l), SNil{})), H.sk_fin(tab, l, AR.thaw(String, k1), H.eq(key, k)), step_of(Bool.pick(B.MS, e, B.MHit{l}, B.MNext{}), tab, AR.thaw(String, kcmp(sd, ksT, l)), key), s1, 67 Equal.trans(H.Step, H.sk_fin(tab, l, AR.thaw(String, k1), H.eq(key, k)), H.sk_pick(tab, l, Array.set(String, AR.thaw(String, k1), H.slot(l), k), key, e), step_of(Bool.pick(B.MS, e, B.MHit{l}, B.MNext{}), tab, AR.thaw(String, kcmp(sd, ksT, l)), key), s2, 68 Equal.trans(H.Step, H.sk_pick(tab, l, Array.set(String, AR.thaw(String, k1), H.slot(l), k), key, e), H.sk_pick(tab, l, AR.thaw(String, kcmp(sd, ksT, l)), key, e), step_of(Bool.pick(B.MS, e, B.MHit{l}, B.MNext{}), tab, AR.thaw(String, kcmp(sd, ksT, l)), key), s3, pick_step(tab, l, AR.thaw(String, kcmp(sd, ksT, l)), key, e)))) 69 70 # the decision of a long-key step on word x, link l, stored key k 71 def ld_w(+key: String, +l: U32, +k: String, same: Bool) -> B.MS: 72 match same: 73 case False{}: 74 B.MNext{} 75 case True{}: 76 Bool.pick(B.MS, S.str_eq(key, k), B.MHit{l}, B.MNext{}) 77 78 def ld_e(+key: String, +w: U32, +x: U32, +l: U32, +k: String, empty: Bool) -> B.MS: 79 match empty: 80 case True{}: 81 B.MEnd{} 82 case False{}: 83 ld_w(key, l, k, U32.is_eq(x, w)) 84 85 def ldec(+key: String, +w: U32, +x: U32, +l: U32, +k: String) -> B.MS: 86 ld_e(key, w, x, l, k, U32.is_eq(x, 0)) 87 88 def ka_w(+sd: Nat, +ksT: AR.Tree, +l: U32, same: Bool) -> AR.Tree: 89 match same: 90 case False{}: 91 ksT 92 case True{}: 93 kcmp(sd, ksT, l) 94 95 def ka_e(+sd: Nat, +ksT: AR.Tree, +w: U32, +x: U32, +l: U32, empty: Bool) -> AR.Tree: 96 match empty: 97 case True{}: 98 ksT 99 case False{}: 100 ka_w(sd, ksT, l, U32.is_eq(x, w)) 101 102 # the stored keys after a long-key step 103 def kafter(+sd: Nat, +ksT: AR.Tree, +w: U32, +x: U32, +l: U32) -> AR.Tree: 104 ka_e(sd, ksT, w, x, l, U32.is_eq(x, 0)) 105 106 def st_same(tab: Array, +sd: Nat, +ksT: AR.Tree, +l: U32, +key: String, +hsd: {Nat.is_lt(sd, 32n) == True{} : Bool}, +hs: {Nat.is_lt(UD.v(H.slot(l)), SC.pow2(sd)) == True{} : Bool}, +pk: {AR.perfect(String, sd, ksT) == True{} : Bool}, +same: Bool) -> {H.sk_same(tab, AR.thaw(String, ksT), l, key, same) == step_of(ld_w(key, l, TB.nths(AR.slots(String, ksT), UD.v(H.slot(l))), same), tab, AR.thaw(String, ka_w(sd, ksT, l, same)), key) : H.Step}: 107 match same: 108 case False{}: 109 {==} 110 case True{}: 111 cmp_path(tab, sd, ksT, l, key, hsd, hs, pk) 112 113 def st_empty(+td: Nat, +tabT: AR.Tree, +sd: Nat, +ksT: AR.Tree, +i: U32, +key: String, +w: U32, +hd: {Nat.is_lt(td, 32n) == True{} : Bool}, +hsd: {Nat.is_lt(sd, 32n) == True{} : Bool}, +pt: {AR.perfect(U32, td, tabT) == True{} : Bool}, +pk: {AR.perfect(String, sd, ksT) == True{} : Bool}, +hl: {Nat.is_lt(UD.v(U32.inc(U32.shl(i))), SC.pow2(td)) == True{} : Bool}, +x: U32, +hs: {B.implies(Bool.not(U32.is_eq(x, 0)), Nat.is_lt(UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), UD.v(U32.inc(U32.shl(i)))))), SC.pow2(sd))) == True{} : Bool}, +e: Bool, +he: {U32.is_eq(x, 0) == e : Bool}) -> {H.sk_empty(AR.thaw(U32, tabT), AR.thaw(String, ksT), i, key, w, x, e) == step_of(ld_e(key, w, x, W32.nth0(AR.slots(U32, tabT), UD.v(U32.inc(U32.shl(i)))), TB.nths(AR.slots(String, ksT), UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), UD.v(U32.inc(U32.shl(i))))))), e), AR.thaw(U32, tabT), AR.thaw(String, ka_e(sd, ksT, w, x, W32.nth0(AR.slots(U32, tabT), UD.v(U32.inc(U32.shl(i)))), e)), key) : H.Step}: 114 match e: 115 case True{}: 116 {==} 117 case False{}: 118 +l = W32.nth0(AR.slots(U32, tabT), UD.v(U32.inc(U32.shl(i)))) 119 +hs2 = B.imp_elim(Bool.not(U32.is_eq(x, 0)), Nat.is_lt(UD.v(H.slot(l)), SC.pow2(sd)), hs, L.subst(Bool, b => {Bool.not(b) == True{} : Bool}, False{}, U32.is_eq(x, 0), Equal.sym(Bool, U32.is_eq(x, 0), False{}, he), {==})) 120 +g = AX.getw(td, tabT, U32.inc(U32.shl(i)), hd, hl, pt) 121 Equal.trans(H.Step, H.sk_l(AR.thaw(String, ksT), key, x, w, Array.get(U32, AR.thaw(U32, tabT), U32.inc(U32.shl(i)))), H.sk_l(AR.thaw(String, ksT), key, x, w, (AR.thaw(U32, tabT), l)), step_of(ld_w(key, l, TB.nths(AR.slots(String, ksT), UD.v(H.slot(l))), U32.is_eq(x, w)), AR.thaw(U32, tabT), AR.thaw(String, ka_w(sd, ksT, l, U32.is_eq(x, w))), key), 122 Equal.cong(Array & U32, H.Step, r => H.sk_l(AR.thaw(String, ksT), key, x, w, r), Array.get(U32, AR.thaw(U32, tabT), U32.inc(U32.shl(i))), (AR.thaw(U32, tabT), l), g), 123 st_same(AR.thaw(U32, tabT), sd, ksT, l, key, hsd, hs2, pk, U32.is_eq(x, w))) 124 125 # THEOREM: a long-key probe step reads bucket i and decides as ldec. 126 def step_long(+td: Nat, +tabT: AR.Tree, +sd: Nat, +ksT: AR.Tree, +i: U32, +key: String, +w: U32, +hd: {Nat.is_lt(td, 32n) == True{} : Bool}, +hsd: {Nat.is_lt(sd, 32n) == True{} : Bool}, +pt: {AR.perfect(U32, td, tabT) == True{} : Bool}, +pk: {AR.perfect(String, sd, ksT) == True{} : Bool}, +hw: {Nat.is_lt(UD.v(U32.shl(i)), SC.pow2(td)) == True{} : Bool}, +hl: {Nat.is_lt(UD.v(U32.inc(U32.shl(i))), SC.pow2(td)) == True{} : Bool}, +hs: {B.implies(Bool.not(U32.is_eq(W32.nth0(AR.slots(U32, tabT), UD.v(U32.shl(i))), 0)), Nat.is_lt(UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), UD.v(U32.inc(U32.shl(i)))))), SC.pow2(sd))) == True{} : Bool}) -> {H.step(AR.thaw(U32, tabT), AR.thaw(String, ksT), i, key, w) == step_of(ldec(key, w, W32.nth0(AR.slots(U32, tabT), UD.v(U32.shl(i))), W32.nth0(AR.slots(U32, tabT), UD.v(U32.inc(U32.shl(i)))), TB.nths(AR.slots(String, ksT), UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), UD.v(U32.inc(U32.shl(i)))))))), AR.thaw(U32, tabT), AR.thaw(String, kafter(sd, ksT, w, W32.nth0(AR.slots(U32, tabT), UD.v(U32.shl(i))), W32.nth0(AR.slots(U32, tabT), UD.v(U32.inc(U32.shl(i)))))), key) : H.Step}: 127 +x = W32.nth0(AR.slots(U32, tabT), UD.v(U32.shl(i))) 128 +g = AX.getw(td, tabT, U32.shl(i), hd, hw, pt) 129 Equal.trans(H.Step, H.sk_w(AR.thaw(String, ksT), i, key, w, Array.get(U32, AR.thaw(U32, tabT), U32.shl(i))), H.sk_w(AR.thaw(String, ksT), i, key, w, (AR.thaw(U32, tabT), x)), step_of(ldec(key, w, x, W32.nth0(AR.slots(U32, tabT), UD.v(U32.inc(U32.shl(i)))), TB.nths(AR.slots(String, ksT), UD.v(H.slot(W32.nth0(AR.slots(U32, tabT), UD.v(U32.inc(U32.shl(i)))))))), AR.thaw(U32, tabT), AR.thaw(String, kafter(sd, ksT, w, x, W32.nth0(AR.slots(U32, tabT), UD.v(U32.inc(U32.shl(i)))))), key), 130 Equal.cong(Array & U32, H.Step, r => H.sk_w(AR.thaw(String, ksT), i, key, w, r), Array.get(U32, AR.thaw(U32, tabT), U32.shl(i)), (AR.thaw(U32, tabT), x), g), 131 st_empty(td, tabT, sd, ksT, i, key, w, hd, hsd, pt, pk, hl, x, hs, U32.is_eq(x, 0), {==}))