1 import Base 2 import ../../lib/logic.bend as L 3 import ../../lib/nat.bend as N 4 import ../../lib/u32.bend as U 5 import ../../lib/array.bend as AR 6 import ../../../spec/lib/common.bend as SC 7 import ../../lib/word.bend as WD 8 import ../../lib/u32div.bend as UD 9 import ../../math/hash/hash.bend as PH 10 import ../../../src/math/hash.bend as HS 11 import ../../../src/containers/hash_table.bend as H 12 import ./strings.bend as STR 13 import ./keys.bend as K 14 import ./table.bend as TB 15 import ./buckets.bend as B 16 import ./cyc.bend as CY 17 import ./probe_impl.bend as PI 18 import ./qprobe.bend as QP 19 import ../../lib/words32.bend as W32 20 21 # The whole probe (H.probe): every key, long or one-character, starting at 22 # its home bucket with fuel n. 23 24 def zero_mask(+p: Nat) -> {WD.uw(p, WD.mask(p, 0n)) == 0n : Nat}: 25 match p: 26 case 0n: 27 {==} 28 case 1n+q: 29 Equal.cong(Nat, Nat, Nat.double, WD.uw(q, WD.mask(q, 0n)), 0n, zero_mask(q)) 30 31 def dbl_step(+u: Nat) -> {Nat.add(1n+Nat.double(u), 1n) == Nat.double(Nat.add(u, 1n)) : Nat}: 32 match u: 33 case 0n: 34 {==} 35 case 1n+v: 36 Equal.cong(Nat, Nat, z => 2n+z, Nat.add(1n+Nat.double(v), 1n), Nat.double(Nat.add(v, 1n)), dbl_step(v)) 37 38 # 2^k - 1 + 1 == 2^k for the mask word 39 def mask_val(+n: Nat, +k: Nat, +hk: {Nat.is_le(k, n) == True{} : Bool}) -> {Nat.add(WD.uw(n, WD.mask(n, k)), 1n) == SC.pow2(k) : Nat}: 40 match n k: 41 case 0n 0n: 42 {==} 43 case 0n 1n+j: 44 Empty.absurd({Nat.add(WD.uw(0n, WD.mask(0n, 1n+j)), 1n) == SC.pow2(1n+j) : Nat}, L.false_true(hk)) 45 case 1n+p 0n: 46 Equal.cong(Nat, Nat, z => Nat.add(Nat.double(z), 1n), WD.uw(p, WD.mask(p, 0n)), 0n, zero_mask(p)) 47 case 1n+p 1n+j: 48 +u = WD.uw(p, WD.mask(p, j)) 49 # 1 + 2u + 1 == 2 (u + 1) 50 Equal.trans(Nat, Nat.add(1n+Nat.double(u), 1n), Nat.double(Nat.add(u, 1n)), SC.pow2(1n+j), dbl_step(u), Equal.cong(Nat, Nat, Nat.double, Nat.add(u, 1n), SC.pow2(j), mask_val(p, j, hk))) 51 52 # the probe's fuel, mask + 1, is the number of buckets 53 def fuel_eq(+one: Nat, +h1: {one == 1n : Nat}, +k: Nat, +hk31: {Nat.is_lt(k, 31n) == True{} : Bool}) -> {U32.to_nat(U32.inc(CY.msk(k))) == SC.pow2(k) : Nat}: 54 +hk = N.lt_le(k, 32n, N.lt_trans(k, 31n, 32n, hk31, {==})) 55 +v = UD.v(CY.msk(k)) 56 +ea = Equal.trans(Nat, Nat.add(v, 1n), Nat.add(WD.uw(32n, WD.mask(32n, k)), 1n), SC.pow2(k), Equal.cong(Nat, Nat, z => Nat.add(z, 1n), v, WD.uw(32n, WD.mask(32n, k)), UD.vw(WD.mask(32n, k))), mask_val(32n, k, hk)) 57 +e1 = Equal.trans(Nat, 1n+v, Nat.add(v, 1n), SC.pow2(k), Equal.sym(Nat, Nat.add(v, 1n), 1n+v, N.add_comm(v, 1n)), ea) 58 +hb = L.subst(Nat, z => {Nat.is_lt(z, WD.sc(32n, one)) == True{} : Bool}, SC.pow2(k), 1n+v, Equal.sym(Nat, 1n+v, SC.pow2(k), e1), N.lt_le_trans(SC.pow2(k), SC.pow2(1n+k), WD.sc(32n, one), N.pow2_lt_succ(k), W32.pow_le32(one, h1, 1n+k, hk31))) 59 Equal.trans(Nat, UD.v(U32.inc(CY.msk(k))), 1n+v, SC.pow2(k), W32.inc_val(one, h1, CY.msk(k), hb), e1) 60 61 # a home bucket is a bucket 62 def home_lt(+w: U32, +k: Nat) -> {Nat.is_lt(UD.v(HS.bucket(w, CY.msk(k))), SC.pow2(k)) == True{} : Bool}: 63 L.subst(Nat, z => {Nat.is_lt(UD.v(HS.bucket(w, CY.msk(k))), z) == True{} : Bool}, WD.sc(k, 1n), SC.pow2(k), Equal.sym(Nat, SC.pow2(k), WD.sc(k, 1n), U.pow2_scale(k)), PH.bucket_lt(w, k, CY.msk(k), {==})) 64 65 # ---- the probe's result ---- 66 67 # the key as the probe hands it back: "" for a short key 68 def st_c(+c: U32, +t: String, sh: Bool) -> String: 69 match sh: 70 case True{}: 71 SNil{} 72 case False{}: 73 SCon{Chr{c}, t} 74 75 def stored(key: String) -> String: 76 match key: 77 case SNil{}: 78 SNil{} 79 case SCon{Chr{+c}, +t}: 80 st_c(c, t, K.short_c(c, t)) 81 82 def ProbeOK(+tabT: AR.Tree, +sd: Nat, +kl0: List<&2, String>, +skey: String, +w: U32, r: B.Res, v: H.Found & U32) -> Type: 83 Sigma<&1, &1, AR.Tree, K2 => {v == (PI.fd_of(r, AR.thaw(U32, tabT), AR.thaw(String, K2), skey), w) : H.Found & U32} & ({AR.slots(String, K2) == kl0 : List<&2, String>} & {AR.perfect(String, sd, K2) == True{} : Bool})> 84 85 def po_of_fo(+tabT: AR.Tree, +sd: Nat, +kl0: List<&2, String>, +key: String, +w: U32, -r: B.Res, -fd: H.Found, fo: PI.FindOK(tabT, sd, kl0, key, r, fd)) -> ProbeOK(tabT, sd, kl0, key, w, r, (fd, w)): 86 match fo: 87 case Tuple{K2, Tuple{e, rest}}: 88 (K2, (Equal.cong(H.Found, H.Found & U32, z => (z, w), fd, PI.fd_of(r, AR.thaw(U32, tabT), AR.thaw(String, K2), key), e), rest)) 89 90 def probe_long_ok(+one: Nat, +h1: {one == 1n : Nat}, +k: Nat, +hk31: {Nat.is_lt(k, 31n) == True{} : Bool}, +tabT: AR.Tree, +pt: {AR.perfect(U32, 1n+k, tabT) == True{} : Bool}, +sd: Nat, +hsd: {Nat.is_lt(sd, 32n) == True{} : Bool}, +kl0: List<&2, String>, +K: AR.Tree, +hsl: {AR.slots(String, K) == kl0 : List<&2, String>}, +pk: {AR.perfect(String, sd, K) == True{} : Bool}, +hwell: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, tabT), kl0, SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +key: String, +hkey: {K.shortk(key) == False{} : Bool}) -> ProbeOK(tabT, sd, kl0, key, STR.lword(key), B.pf(key, TB.buckets(AR.slots(U32, tabT), kl0, SC.pow2(k)), SC.pow2(k), SC.pow2(k), B.mstep(key, B.at(TB.buckets(AR.slots(U32, tabT), kl0, SC.pow2(k)), UD.v(HS.bucket(STR.lword(key), CY.msk(k))))), UD.v(HS.bucket(STR.lword(key), CY.msk(k)))), H.probe_long(AR.thaw(U32, tabT), AR.thaw(String, K), CY.msk(k), key)): 91 +bs = TB.buckets(AR.slots(U32, tabT), kl0, SC.pow2(k)) 92 +n = SC.pow2(k) 93 +w = STR.lword(key) 94 +i = HS.bucket(w, CY.msk(k)) 95 +r = B.pf(key, bs, n, n, B.mstep(key, B.at(bs, UD.v(i))), UD.v(i)) 96 fo = po_of_fo(tabT, sd, kl0, key, w, r, H.find(n, H.step(AR.thaw(U32, tabT), AR.thaw(String, K), i, key, w), CY.msk(k), w, i), PI.find_ok(one, h1, k, hk31, tabT, pt, sd, hsd, kl0, key, hkey, hwell, n, i, home_lt(w, k), K, hsl, pk)) 97 f1 = L.subst(Nat, f => ProbeOK(tabT, sd, kl0, key, w, r, (H.find(f, H.step(AR.thaw(U32, tabT), AR.thaw(String, K), i, key, w), CY.msk(k), w, i), w)), n, U32.to_nat(U32.inc(CY.msk(k))), Equal.sym(Nat, U32.to_nat(U32.inc(CY.msk(k))), n, fuel_eq(one, h1, k, hk31)), fo) 98 L.subst(String & U32, v => ProbeOK(tabT, sd, kl0, key, w, r, H.probe_lw(AR.thaw(U32, tabT), AR.thaw(String, K), CY.msk(k), v)), (key, w), H.key_long(key), Equal.sym(String & U32, H.key_long(key), (key, w), STR.key_long(key)), f1) 99 100 def qfin_of(r: B.Res, tab: Array, ks: Array, +w: U32) -> {H.q_fin(ks, w, QP.qf_of(r, tab)) == (PI.fd_of(r, tab, ks, SNil{}), w) : H.Found & U32}: 101 match r: 102 case B.RHit{a, l}: 103 {==} 104 case B.REnd{a}: 105 {==} 106 107 def probe_short_ok(+one: Nat, +h1: {one == 1n : Nat}, +k: Nat, +hk31: {Nat.is_lt(k, 31n) == True{} : Bool}, +tabT: AR.Tree, +pt: {AR.perfect(U32, 1n+k, tabT) == True{} : Bool}, +sd: Nat, +hsd: {Nat.is_lt(sd, 32n) == True{} : Bool}, +kl0: List<&2, String>, +K: AR.Tree, +hsl: {AR.slots(String, K) == kl0 : List<&2, String>}, +pk: {AR.perfect(String, sd, K) == True{} : Bool}, +hwell: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, tabT), kl0, SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +c: U32, +hc: {U32.is_lt(c, H.tag()) == True{} : Bool}) -> ProbeOK(tabT, sd, kl0, SNil{}, H.short_word(c), B.pf(SCon{Chr{c}, SNil{}}, TB.buckets(AR.slots(U32, tabT), kl0, SC.pow2(k)), SC.pow2(k), SC.pow2(k), B.mstep(SCon{Chr{c}, SNil{}}, B.at(TB.buckets(AR.slots(U32, tabT), kl0, SC.pow2(k)), UD.v(HS.bucket(H.short_word(c), CY.msk(k))))), UD.v(HS.bucket(H.short_word(c), CY.msk(k)))), H.probe_short(AR.thaw(U32, tabT), AR.thaw(String, K), CY.msk(k), c, True{})): 108 +w = H.short_word(c) 109 +i = HS.bucket(w, CY.msk(k)) 110 +n = SC.pow2(k) 111 +r = B.pf(SCon{Chr{c}, SNil{}}, TB.buckets(AR.slots(U32, tabT), kl0, SC.pow2(k)), SC.pow2(k), SC.pow2(k), B.mstep(SCon{Chr{c}, SNil{}}, B.at(TB.buckets(AR.slots(U32, tabT), kl0, SC.pow2(k)), UD.v(HS.bucket(H.short_word(c), CY.msk(k))))), UD.v(HS.bucket(H.short_word(c), CY.msk(k)))) 112 +q = QP.qfind_ok(one, h1, k, hk31, tabT, pt, sd, kl0, c, hc, hwell, n, i, home_lt(w, k)) 113 +e1 = Equal.trans(H.Found & U32, H.q_fin(AR.thaw(String, K), w, H.qfind(n, H.qstep(AR.thaw(U32, tabT), i, w), CY.msk(k), w, i)), H.q_fin(AR.thaw(String, K), w, QP.qf_of(r, AR.thaw(U32, tabT))), (PI.fd_of(r, AR.thaw(U32, tabT), AR.thaw(String, K), SNil{}), w), Equal.cong(H.QFound, H.Found & U32, z => H.q_fin(AR.thaw(String, K), w, z), H.qfind(n, H.qstep(AR.thaw(U32, tabT), i, w), CY.msk(k), w, i), QP.qf_of(r, AR.thaw(U32, tabT)), q), qfin_of(r, AR.thaw(U32, tabT), AR.thaw(String, K), w)) 114 +e2 = L.subst(Nat, f => {H.q_fin(AR.thaw(String, K), w, H.qfind(f, H.qstep(AR.thaw(U32, tabT), i, w), CY.msk(k), w, i)) == (PI.fd_of(r, AR.thaw(U32, tabT), AR.thaw(String, K), SNil{}), w) : H.Found & U32}, n, U32.to_nat(U32.inc(CY.msk(k))), Equal.sym(Nat, U32.to_nat(U32.inc(CY.msk(k))), n, fuel_eq(one, h1, k, hk31)), e1) 115 (K, (e2, (hsl, pk))) 116 117 def pc_short(+one: Nat, +h1: {one == 1n : Nat}, +k: Nat, +hk31: {Nat.is_lt(k, 31n) == True{} : Bool}, +tabT: AR.Tree, +pt: {AR.perfect(U32, 1n+k, tabT) == True{} : Bool}, +sd: Nat, +hsd: {Nat.is_lt(sd, 32n) == True{} : Bool}, +kl0: List<&2, String>, +K: AR.Tree, +hsl: {AR.slots(String, K) == kl0 : List<&2, String>}, +pk: {AR.perfect(String, sd, K) == True{} : Bool}, +hwell: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, tabT), kl0, SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +c: U32, +b: Bool, +hb: {U32.is_lt(c, H.tag()) == b : Bool}) -> ProbeOK(tabT, sd, kl0, st_c(c, SNil{}, b), K.kw_c(c, SNil{}, b), B.pf(SCon{Chr{c}, SNil{}}, TB.buckets(AR.slots(U32, tabT), kl0, SC.pow2(k)), SC.pow2(k), SC.pow2(k), B.mstep(SCon{Chr{c}, SNil{}}, B.at(TB.buckets(AR.slots(U32, tabT), kl0, SC.pow2(k)), UD.v(HS.bucket(K.kw_c(c, SNil{}, b), CY.msk(k))))), UD.v(HS.bucket(K.kw_c(c, SNil{}, b), CY.msk(k)))), H.probe_short(AR.thaw(U32, tabT), AR.thaw(String, K), CY.msk(k), c, b)): 118 match b: 119 case True{}: 120 probe_short_ok(one, h1, k, hk31, tabT, pt, sd, hsd, kl0, K, hsl, pk, hwell, c, hb) 121 case False{}: 122 probe_long_ok(one, h1, k, hk31, tabT, pt, sd, hsd, kl0, K, hsl, pk, hwell, SCon{Chr{c}, SNil{}}, hb) 123 124 def pc(+one: Nat, +h1: {one == 1n : Nat}, +k: Nat, +hk31: {Nat.is_lt(k, 31n) == True{} : Bool}, +tabT: AR.Tree, +pt: {AR.perfect(U32, 1n+k, tabT) == True{} : Bool}, +sd: Nat, +hsd: {Nat.is_lt(sd, 32n) == True{} : Bool}, +kl0: List<&2, String>, +K: AR.Tree, +hsl: {AR.slots(String, K) == kl0 : List<&2, String>}, +pk: {AR.perfect(String, sd, K) == True{} : Bool}, +hwell: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, tabT), kl0, SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +c: U32, +t: String) -> ProbeOK(tabT, sd, kl0, st_c(c, t, K.short_c(c, t)), K.kw_c(c, t, K.short_c(c, t)), B.pf(SCon{Chr{c}, t}, TB.buckets(AR.slots(U32, tabT), kl0, SC.pow2(k)), SC.pow2(k), SC.pow2(k), B.mstep(SCon{Chr{c}, t}, B.at(TB.buckets(AR.slots(U32, tabT), kl0, SC.pow2(k)), UD.v(HS.bucket(K.kw_c(c, t, K.short_c(c, t)), CY.msk(k))))), UD.v(HS.bucket(K.kw_c(c, t, K.short_c(c, t)), CY.msk(k)))), H.probe_c(AR.thaw(U32, tabT), AR.thaw(String, K), CY.msk(k), c, t)): 125 match t: 126 case SNil{}: 127 pc_short(one, h1, k, hk31, tabT, pt, sd, hsd, kl0, K, hsl, pk, hwell, c, U32.is_lt(c, H.tag()), {==}) 128 case SCon{+d, +t2}: 129 probe_long_ok(one, h1, k, hk31, tabT, pt, sd, hsd, kl0, K, hsl, pk, hwell, SCon{Chr{c}, SCon{d, t2}}, {==}) 130 131 # THEOREM: the probe of any key is the model probe from the key's home 132 # bucket with fuel n; it hands back the key's stored form and its word. 133 def probe_ok(+one: Nat, +h1: {one == 1n : Nat}, +k: Nat, +hk31: {Nat.is_lt(k, 31n) == True{} : Bool}, +tabT: AR.Tree, +pt: {AR.perfect(U32, 1n+k, tabT) == True{} : Bool}, +sd: Nat, +hsd: {Nat.is_lt(sd, 32n) == True{} : Bool}, +kl0: List<&2, String>, +K: AR.Tree, +hsl: {AR.slots(String, K) == kl0 : List<&2, String>}, +pk: {AR.perfect(String, sd, K) == True{} : Bool}, +hwell: {B.all_lt(B.PWell{TB.buckets(AR.slots(U32, tabT), kl0, SC.pow2(k)), sd}, SC.pow2(k)) == True{} : Bool}, +key: String) -> ProbeOK(tabT, sd, kl0, stored(key), K.kword(key), B.pf(key, TB.buckets(AR.slots(U32, tabT), kl0, SC.pow2(k)), SC.pow2(k), SC.pow2(k), B.mstep(key, B.at(TB.buckets(AR.slots(U32, tabT), kl0, SC.pow2(k)), UD.v(HS.bucket(K.kword(key), CY.msk(k))))), UD.v(HS.bucket(K.kword(key), CY.msk(k)))), H.probe(AR.thaw(U32, tabT), AR.thaw(String, K), CY.msk(k), key)): 134 match key: 135 case SNil{}: 136 probe_long_ok(one, h1, k, hk31, tabT, pt, sd, hsd, kl0, K, hsl, pk, hwell, SNil{}, {==}) 137 case SCon{Chr{+c}, +t}: 138 pc(one, h1, k, hk31, tabT, pt, sd, hsd, kl0, K, hsl, pk, hwell, c, t)