1 import Base 2 import ../../lib/logic.bend as L 3 import ../../lib/nat.bend as N 4 import ../../lib/array.bend as AR 5 import ../../../spec/lib/common.bend as SC 6 import ../../lib/u32div.bend as UD 7 import ../../../src/containers/hash_table.bend as H 8 import ./table.bend as TB 9 import ./buckets.bend as B 10 import ./cyc.bend as CY 11 import ./inv.bend as IV 12 import ./insm.bend as IM 13 import ./grow.bend as GR 14 import ./shift.bend as SH 15 16 # del_at, stated over the table's 2^k buckets. 17 18 19 def dfin2(+kl: List<&2, String>, +k: Nat, +V0: List<&2, B.Bk>, +Tf: AR.Tree) -> Bool: 20 Bool.and(AR.perfect(U32, 1n+k, Tf), Bool.and(B.cluster(TB.buckets(AR.slots(U32, Tf), kl, SC.pow2(k)), SC.pow2(k), CY.msk(k)), Bool.and(B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, Tf), kl, SC.pow2(k))}, SC.pow2(k)), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, Tf), kl, SC.pow2(k)), V0, SC.pow2(k)}, SC.pow2(k)), Bool.and(B.all_lt(B.PTo{V0, TB.buckets(AR.slots(U32, Tf), kl, SC.pow2(k)), SC.pow2(k)}, SC.pow2(k)), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, Tf), kl, SC.pow2(k)), SC.pow2(k)), IV.occn(V0, SC.pow2(k)))))))) 21 22 def DelAt2(+kl: List<&2, String>, +k: Nat, +OT: AR.Tree, +i: Nat) -> Type: 23 Sigma<&1, &1, AR.Tree, Tf => {H.del_at(AR.thaw(U32, OT), CY.msk(k), U32.from_nat(i)) == AR.thaw(U32, Tf) : Array} & {dfin2(kl, k, IM.bupd(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), i, B.BE{}), Tf) == True{} : Bool}> 24 25 def hN(+k: Nat, +hk: {Nat.is_lt(k, 31n) == True{} : Bool}) -> {1n+UD.v(CY.msk(k)) == SC.pow2(k) : Nat}: 26 Equal.trans(Nat, 1n+UD.v(CY.msk(k)), Nat.add(UD.v(CY.msk(k)), 1n), SC.pow2(k), N.add_comm(1n, UD.v(CY.msk(k))), GR.mskv(k, N.lt_le(k, 32n, N.lt_trans(k, 31n, 32n, hk, {==})))) 27 28 29 def d2_fin(+kl: List<&2, String>, +k: Nat, +hk31: {Nat.is_lt(k, 31n) == True{} : Bool}, +OT: AR.Tree, +i: Nat, d: SH.DelAt(kl, k, UD.v(CY.msk(k)), OT, i)) -> DelAt2(kl, k, OT, i): 30 match d: 31 case Tuple{+Tf, Tuple{+e1, +hd}}: 32 +g1 = SH.f1(kl, k, UD.v(CY.msk(k)), IM.bupd(TB.buckets(AR.slots(U32, OT), kl, 1n+UD.v(CY.msk(k))), i, B.BE{}), Tf, hd) 33 +g2 = L.subst(Nat, z => {B.cluster(TB.buckets(AR.slots(U32, Tf), kl, z), z, CY.msk(k)) == True{} : Bool} , 1n+UD.v(CY.msk(k)), SC.pow2(k), hN(k, hk31), SH.f2(kl, k, UD.v(CY.msk(k)), IM.bupd(TB.buckets(AR.slots(U32, OT), kl, 1n+UD.v(CY.msk(k))), i, B.BE{}), Tf, hd)) 34 +g3 = L.subst(Nat, z => {B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, Tf), kl, z)}, z) == True{} : Bool} , 1n+UD.v(CY.msk(k)), SC.pow2(k), hN(k, hk31), SH.f3(kl, k, UD.v(CY.msk(k)), IM.bupd(TB.buckets(AR.slots(U32, OT), kl, 1n+UD.v(CY.msk(k))), i, B.BE{}), Tf, hd)) 35 +g4 = L.subst(Nat, z => {B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, Tf), kl, z), IM.bupd(TB.buckets(AR.slots(U32, OT), kl, z), i, B.BE{}), z}, z) == True{} : Bool} , 1n+UD.v(CY.msk(k)), SC.pow2(k), hN(k, hk31), SH.f4(kl, k, UD.v(CY.msk(k)), IM.bupd(TB.buckets(AR.slots(U32, OT), kl, 1n+UD.v(CY.msk(k))), i, B.BE{}), Tf, hd)) 36 +g5 = L.subst(Nat, z => {B.all_lt(B.PTo{IM.bupd(TB.buckets(AR.slots(U32, OT), kl, z), i, B.BE{}), TB.buckets(AR.slots(U32, Tf), kl, z), z}, z) == True{} : Bool} , 1n+UD.v(CY.msk(k)), SC.pow2(k), hN(k, hk31), SH.f5(kl, k, UD.v(CY.msk(k)), IM.bupd(TB.buckets(AR.slots(U32, OT), kl, 1n+UD.v(CY.msk(k))), i, B.BE{}), Tf, hd)) 37 +g6 = L.subst(Nat, z => {Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, Tf), kl, z), z), IV.occn(IM.bupd(TB.buckets(AR.slots(U32, OT), kl, z), i, B.BE{}), z)) == True{} : Bool} , 1n+UD.v(CY.msk(k)), SC.pow2(k), hN(k, hk31), SH.f6(kl, k, UD.v(CY.msk(k)), IM.bupd(TB.buckets(AR.slots(U32, OT), kl, 1n+UD.v(CY.msk(k))), i, B.BE{}), Tf, hd)) 38 (Tf, (e1, L.and_intro(AR.perfect(U32, 1n+k, Tf), Bool.and(B.cluster(TB.buckets(AR.slots(U32, Tf), kl, SC.pow2(k)), SC.pow2(k), CY.msk(k)), Bool.and(B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, Tf), kl, SC.pow2(k))}, SC.pow2(k)), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, Tf), kl, SC.pow2(k)), IM.bupd(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), i, B.BE{}), SC.pow2(k)}, SC.pow2(k)), Bool.and(B.all_lt(B.PTo{IM.bupd(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), i, B.BE{}), TB.buckets(AR.slots(U32, Tf), kl, SC.pow2(k)), SC.pow2(k)}, SC.pow2(k)), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, Tf), kl, SC.pow2(k)), SC.pow2(k)), IV.occn(IM.bupd(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), i, B.BE{}), SC.pow2(k))))))), g1, L.and_intro(B.cluster(TB.buckets(AR.slots(U32, Tf), kl, SC.pow2(k)), SC.pow2(k), CY.msk(k)), Bool.and(B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, Tf), kl, SC.pow2(k))}, SC.pow2(k)), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, Tf), kl, SC.pow2(k)), IM.bupd(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), i, B.BE{}), SC.pow2(k)}, SC.pow2(k)), Bool.and(B.all_lt(B.PTo{IM.bupd(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), i, B.BE{}), TB.buckets(AR.slots(U32, Tf), kl, SC.pow2(k)), SC.pow2(k)}, SC.pow2(k)), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, Tf), kl, SC.pow2(k)), SC.pow2(k)), IV.occn(IM.bupd(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), i, B.BE{}), SC.pow2(k)))))), g2, L.and_intro(B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, Tf), kl, SC.pow2(k))}, SC.pow2(k)), Bool.and(B.all_lt(B.PFrom{TB.buckets(AR.slots(U32, Tf), kl, SC.pow2(k)), IM.bupd(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), i, B.BE{}), SC.pow2(k)}, SC.pow2(k)), Bool.and(B.all_lt(B.PTo{IM.bupd(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), i, B.BE{}), TB.buckets(AR.slots(U32, Tf), kl, SC.pow2(k)), SC.pow2(k)}, SC.pow2(k)), Nat.is_eq(IV.occn(TB.buckets(AR.slots(U32, Tf), kl, SC.pow2(k)), SC.pow2(k)), IV.occn(IM.bupd(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), i, B.BE{}), SC.pow 39 40 41 # THEOREM: deleting a full bucket of a good table (2^k buckets, a free one) 42 def del_ok2(+k: Nat, +hk31: {Nat.is_lt(k, 31n) == True{} : Bool}, +kl: List<&2, String>, +OT: AR.Tree, +pot: {AR.perfect(U32, 1n+k, OT) == True{} : Bool}, +i: Nat, +hi: {Nat.is_lt(i, SC.pow2(k)) == True{} : Bool}, +cl: {B.cluster(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), SC.pow2(k), CY.msk(k)) == True{} : Bool}, +huo: {B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k))}, SC.pow2(k)) == True{} : Bool}, +hoi: {B.occ(B.at(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), i)) == True{} : Bool}, +hem: {Nat.is_lt(IV.occn(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), SC.pow2(k)), SC.pow2(k)) == True{} : Bool}) -> DelAt2(kl, k, OT, i): 43 +hi2 = L.subst(Nat, z => {Nat.is_lt(i, z) == True{} : Bool} , SC.pow2(k), 1n+UD.v(CY.msk(k)), Equal.sym(Nat, 1n+UD.v(CY.msk(k)), SC.pow2(k), hN(k, hk31)), hi) 44 +cl2 = L.subst(Nat, z => {B.cluster(TB.buckets(AR.slots(U32, OT), kl, z), z, CY.msk(k)) == True{} : Bool} , SC.pow2(k), 1n+UD.v(CY.msk(k)), Equal.sym(Nat, 1n+UD.v(CY.msk(k)), SC.pow2(k), hN(k, hk31)), cl) 45 +hu2 = L.subst(Nat, z => {B.all_lt(B.PUniq{TB.buckets(AR.slots(U32, OT), kl, z)}, z) == True{} : Bool} , SC.pow2(k), 1n+UD.v(CY.msk(k)), Equal.sym(Nat, 1n+UD.v(CY.msk(k)), SC.pow2(k), hN(k, hk31)), huo) 46 +ho2 = L.subst(Nat, z => {B.occ(B.at(TB.buckets(AR.slots(U32, OT), kl, z), i)) == True{} : Bool} , SC.pow2(k), 1n+UD.v(CY.msk(k)), Equal.sym(Nat, 1n+UD.v(CY.msk(k)), SC.pow2(k), hN(k, hk31)), hoi) 47 +he2 = L.subst(Nat, z => {Nat.is_lt(IV.occn(TB.buckets(AR.slots(U32, OT), kl, z), z), z) == True{} : Bool} , SC.pow2(k), 1n+UD.v(CY.msk(k)), Equal.sym(Nat, 1n+UD.v(CY.msk(k)), SC.pow2(k), hN(k, hk31)), hem) 48 d2_fin(kl, k, hk31, OT, i, SH.del_ok(1n, {==}, k, hk31, UD.v(CY.msk(k)), hN(k, hk31), kl, OT, pot, i, hi2, cl2, hu2, ho2, he2))