1 import Base 2 import ../../lib/logic.bend as L 3 import ../../lib/nat.bend as N 4 import ../../lib/u32alg.bend as A 5 import ../../lib/u32.bend as U 6 import ../../../spec/lib/common.bend as SC 7 import ../../lib/u32div.bend as UD 8 import ../../../src/containers/hash_table.bend as H 9 import ./keys.bend as K 10 import ./buckets.bend as B 11 import ./state.bend as ST 12 13 # Tools for the updates: finding the bucket that holds a key, distinct full 14 # buckets have distinct links, and reading a slot list after an update. 15 16 def Holder(+bs: List<&2, B.Bk>, +key: String, +m: Nat) -> Type: 17 Sigma<&1, &1, Nat, j => {Nat.is_lt(j, m) == True{} : Bool} & {B.hold(key, B.at(bs, j)) == True{} : Bool}> 18 19 def hold_up(+bs: List<&2, B.Bk>, +key: String, +q: Nat, e: Holder(bs, key, q)) -> Holder(bs, key, 1n+q): 20 match e: 21 case Tuple{+j, Tuple{hj, hk}}: 22 (j, (N.lt_trans(j, q, 1n+q, hj, N.lt_succ(q)), hk)) 23 24 def fh_c(+bs: List<&2, B.Bk>, +key: String, +q: Nat, +c: Bool, +hc: {Bool.not(B.hold(key, B.at(bs, q))) == c : Bool}, +h: {Bool.and(c, B.all_lt(B.PNo{bs, key}, q)) == False{} : Bool}, rec: @hq: {B.all_lt(B.PNo{bs, key}, q) == False{} : Bool} -> Holder(bs, key, q)) -> Holder(bs, key, 1n+q): 25 match c: 26 case False{}: 27 (q, (N.lt_succ(q), K.not_true_eq2(B.hold(key, B.at(bs, q)), hc))) 28 case True{}: 29 hold_up(bs, key, q, rec(h)) 30 31 # not every bucket is free of key: one holds it 32 def find_hold(+bs: List<&2, B.Bk>, +key: String, +m: Nat, +h: {B.all_lt(B.PNo{bs, key}, m) == False{} : Bool}) -> Holder(bs, key, m): 33 match m: 34 case 0n: 35 Empty.absurd(Holder(bs, key, 0n), L.true_false(h)) 36 case 1n+q: 37 fh_c(bs, key, q, Bool.not(B.hold(key, B.at(bs, q))), {==}, h, hq => find_hold(bs, key, q, hq)) 38 39 # ---- links ---- 40 41 # slot(l) = l - 1 is injective 42 def slot_inj(+a: U32, +b: U32, +h: {UD.v(H.slot(a)) == UD.v(H.slot(b)) : Nat}) -> {a == b : U32}: 43 +e = U.injective(H.slot(a), H.slot(b), h) 44 Equal.trans(U32, a, U32.add(U32.sub(a, 1), 1), b, Equal.sym(U32, U32.add(U32.sub(a, 1), 1), a, A.sub_add(a, 1)), Equal.trans(U32, U32.add(U32.sub(a, 1), 1), U32.add(U32.sub(b, 1), 1), b, Equal.cong(U32, U32, z => U32.add(z, 1), U32.sub(a, 1), U32.sub(b, 1), e), A.sub_add(b, 1))) 45 46 def nolb_c(+bs: List<&2, B.Bk>, +l: U32, +q: Nat, +h: {Bool.and(Bool.not(Bool.and(B.occ(B.at(bs, q)), U32.is_eq(B.lnk(B.at(bs, q)), l))), B.nolb(bs, l, q)) == True{} : Bool}, +j: Nat, +hj: {Nat.is_lt(j, 1n+q) == True{} : Bool}, +c: Bool, +hc: {Nat.is_eq(j, q) == c : Bool}, rec: @hlt: {Nat.is_lt(j, q) == True{} : Bool} -> {Bool.not(Bool.and(B.occ(B.at(bs, j)), U32.is_eq(B.lnk(B.at(bs, j)), l))) == True{} : Bool}) -> {Bool.not(Bool.and(B.occ(B.at(bs, j)), U32.is_eq(B.lnk(B.at(bs, j)), l))) == True{} : Bool}: 47 match c: 48 case True{}: 49 L.subst(Nat, z => {Bool.not(Bool.and(B.occ(B.at(bs, z)), U32.is_eq(B.lnk(B.at(bs, z)), l))) == True{} : Bool}, q, j, Equal.sym(Nat, j, q, N.eq_from_is_eq(j, q, hc)), L.and_left(Bool.not(Bool.and(B.occ(B.at(bs, q)), U32.is_eq(B.lnk(B.at(bs, q)), l))), B.nolb(bs, l, q), h)) 50 case False{}: 51 rec(N.lt_or_eq(j, q, N.lt_succ_le(j, q, hj), hc)) 52 53 def nolb_inst(+bs: List<&2, B.Bk>, +l: U32, +m: Nat, +h: {B.nolb(bs, l, m) == True{} : Bool}, +j: Nat, +hj: {Nat.is_lt(j, m) == True{} : Bool}) -> {Bool.not(Bool.and(B.occ(B.at(bs, j)), U32.is_eq(B.lnk(B.at(bs, j)), l))) == True{} : Bool}: 54 match m: 55 case 0n: 56 Empty.absurd({Bool.not(Bool.and(B.occ(B.at(bs, j)), U32.is_eq(B.lnk(B.at(bs, j)), l))) == True{} : Bool}, N.lt_zero_absurd(j, hj)) 57 case 1n+q: 58 nolb_c(bs, l, q, h, j, hj, Nat.is_eq(j, q), {==}, hlt => nolb_inst(bs, l, q, L.and_right(Bool.not(Bool.and(B.occ(B.at(bs, q)), U32.is_eq(B.lnk(B.at(bs, q)), l))), B.nolb(bs, l, q), h), j, hlt)) 59 60 # the full bucket b at index i and the full bucket at j < i have different links 61 def link_ne_b(+bs: List<&2, B.Bk>, +i: Nat, +j: Nat, +hji: {Nat.is_lt(j, i) == True{} : Bool}, +b: B.Bk, +hu: {B.uq_b(bs, i, b) == True{} : Bool}, +hob: {B.occ(b) == True{} : Bool}, +hoj: {B.occ(B.at(bs, j)) == True{} : Bool}) -> {U32.is_eq(B.lnk(B.at(bs, j)), B.lnk(b)) == False{} : Bool}: 62 match b: 63 case B.BE{}: 64 Empty.absurd({U32.is_eq(B.lnk(B.at(bs, j)), B.lnk(B.BE{})) == False{} : Bool}, L.false_true(hob)) 65 case B.BF{w, +l, +k}: 66 +nl = nolb_inst(bs, l, i, L.and_right(B.nohb(bs, k, i), B.nolb(bs, l, i), hu), j, hji) 67 K.not_true_eq(U32.is_eq(B.lnk(B.at(bs, j)), l), L.subst(Bool, z => {Bool.not(Bool.and(z, U32.is_eq(B.lnk(B.at(bs, j)), l))) == True{} : Bool}, B.occ(B.at(bs, j)), True{}, hoj, nl)) 68 69 def slots_ne_of(+a: U32, +b: U32, +h: {U32.is_eq(a, b) == False{} : Bool}, +c: Bool, +hc: {Nat.is_eq(UD.v(H.slot(a)), UD.v(H.slot(b))) == c : Bool}) -> {c == False{} : Bool}: 70 match c: 71 case False{}: 72 {==} 73 case True{}: 74 +eab = slot_inj(a, b, N.eq_from_is_eq(UD.v(H.slot(a)), UD.v(H.slot(b)), hc)) 75 Empty.absurd({True{} == False{} : Bool}, L.true_false(Equal.trans(Bool, True{}, U32.is_eq(a, b), False{}, L.subst(U32, z => {True{} == U32.is_eq(a, z) : Bool}, a, b, eab, Equal.sym(Bool, U32.is_eq(a, a), True{}, U.u32_eq_refl(a))), h))) 76 77 def slot_ne_lt(+bs: List<&2, B.Bk>, +n: Nat, +huq: {B.all_lt(B.PUniq{bs}, n) == True{} : Bool}, +i: Nat, +j: Nat, +hi: {Nat.is_lt(i, n) == True{} : Bool}, +hji: {Nat.is_lt(j, i) == True{} : Bool}, +oi: {B.occ(B.at(bs, i)) == True{} : Bool}, +oj: {B.occ(B.at(bs, j)) == True{} : Bool}) -> {Nat.is_eq(UD.v(H.slot(B.lnk(B.at(bs, j)))), UD.v(H.slot(B.lnk(B.at(bs, i))))) == False{} : Bool}: 78 slots_ne_of(B.lnk(B.at(bs, j)), B.lnk(B.at(bs, i)), link_ne_b(bs, i, j, hji, B.at(bs, i), B.all_inst(B.PUniq{bs}, n, huq, i, hi), oi, oj), Nat.is_eq(UD.v(H.slot(B.lnk(B.at(bs, j)))), UD.v(H.slot(B.lnk(B.at(bs, i))))), {==}) 79 80 def slot_ne_c(+bs: List<&2, B.Bk>, +n: Nat, +huq: {B.all_lt(B.PUniq{bs}, n) == True{} : Bool}, +i: Nat, +j: Nat, +hi: {Nat.is_lt(i, n) == True{} : Bool}, +hj: {Nat.is_lt(j, n) == True{} : Bool}, +hne: {Nat.is_eq(j, i) == False{} : Bool}, +oi: {B.occ(B.at(bs, i)) == True{} : Bool}, +oj: {B.occ(B.at(bs, j)) == True{} : Bool}, +c: Bool, +hc: {Nat.is_lt(j, i) == c : Bool}) -> {Nat.is_eq(UD.v(H.slot(B.lnk(B.at(bs, j)))), UD.v(H.slot(B.lnk(B.at(bs, i))))) == False{} : Bool}: 81 match c: 82 case True{}: 83 slot_ne_lt(bs, n, huq, i, j, hi, hc, oi, oj) 84 case False{}: 85 N.is_eq_sym_false(UD.v(H.slot(B.lnk(B.at(bs, i)))), UD.v(H.slot(B.lnk(B.at(bs, j)))), slot_ne_lt(bs, n, huq, j, i, hj, N.lt_or_eq(i, j, N.not_lt_le(j, i, hc), N.is_eq_sym_false(j, i, hne)), oj, oi)) 86 87 # THEOREM: distinct full buckets use distinct slots 88 def slot_ne(+bs: List<&2, B.Bk>, +n: Nat, +huq: {B.all_lt(B.PUniq{bs}, n) == True{} : Bool}, +i: Nat, +j: Nat, +hi: {Nat.is_lt(i, n) == True{} : Bool}, +hj: {Nat.is_lt(j, n) == True{} : Bool}, +hne: {Nat.is_eq(j, i) == False{} : Bool}, +oi: {B.occ(B.at(bs, i)) == True{} : Bool}, +oj: {B.occ(B.at(bs, j)) == True{} : Bool}) -> {Nat.is_eq(UD.v(H.slot(B.lnk(B.at(bs, j)))), UD.v(H.slot(B.lnk(B.at(bs, i))))) == False{} : Bool}: 89 slot_ne_c(bs, n, huq, i, j, hi, hj, hne, oi, oj, Nat.is_lt(j, i), {==}) 90 91 # ---- slot lists after an update ---- 92 93 def nthm_upd_same(~V: Data, +vsl: List<&2, Maybe<&2, V>>, +s: Nat, +m: Maybe<&2, V>, +h: {Nat.is_lt(s, SC.length(Maybe<&2, V>, vsl)) == True{} : Bool}) -> {ST.nthm(~V, SC.update(Maybe<&2, V>, vsl, s, m), s) == m : Maybe<&2, V>}: 94 match vsl s: 95 case Nil{} _: 96 Empty.absurd({ST.nthm(~V, SC.update(Maybe<&2, V>, Nil{}, s, m), s) == m : Maybe<&2, V>}, N.lt_zero_absurd(s, h)) 97 case Con{x, t} 0n: 98 {==} 99 case Con{x, t} 1n+p: 100 nthm_upd_same(~V, t, p, m, h) 101 102 def nthm_upd_other(~V: Data, +vsl: List<&2, Maybe<&2, V>>, +s: Nat, +t: Nat, +m: Maybe<&2, V>, +h: {Nat.is_eq(s, t) == False{} : Bool}) -> {ST.nthm(~V, SC.update(Maybe<&2, V>, vsl, s, m), t) == ST.nthm(~V, vsl, t) : Maybe<&2, V>}: 103 match vsl s t: 104 case Nil{} _ _: 105 {==} 106 case Con{x, r} 0n 0n: 107 Empty.absurd({ST.nthm(~V, SC.update(Maybe<&2, V>, Con{x, r}, 0n, m), 0n) == ST.nthm(~V, Con{x, r}, 0n) : Maybe<&2, V>}, L.true_false(h)) 108 case Con{x, r} 0n 1n+q: 109 {==} 110 case Con{x, r} 1n+p 0n: 111 {==} 112 case Con{x, r} 1n+p 1n+q: 113 nthm_upd_other(~V, r, p, q, m, h)