proofs/containers/hash_table/delw.bend
bend-collections-laws-containers@1.0.0.0 · 48 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/lib/logic.bend as L
3import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat.bend as N
4import bend-collections-laws-containers@1.0.0.0/proofs/lib/array.bend as AR
5import bend-collections-laws-containers@1.0.0.0/spec/lib/common.bend as SC
6import bend-collections-laws-containers@1.0.0.0/proofs/lib/u32div.bend as UD
7import bend-collections-laws-containers@1.0.0.0/src/containers/hash_table.bend as H
8import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/table.bend as TB
9import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/buckets.bend as B
10import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/cyc.bend as CY
11import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/inv.bend as IV
12import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/insm.bend as IM
13import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/grow.bend as GR
14import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/shift.bend as SH
15
16# del_at, stated over the table's 2^k buckets.
17
18
19def dfin2(+kl: List<&2, String>, +k: Nat, +V0: List<&2, B.Bk>, +Tf: AR.Tree<U32>) -> 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
22def DelAt2(+kl: List<&2, String>, +k: Nat, +OT: AR.Tree<U32>, +i: Nat) -> Type:
23 Sigma<&1, &1, AR.Tree<U32>, Tf => {H.del_at(AR.thaw(U32, OT), CY.msk(k), U32.from_nat(i)) == AR.thaw(U32, Tf) : Array<U32>} & {dfin2(kl, k, IM.bupd(TB.buckets(AR.slots(U32, OT), kl, SC.pow2(k)), i, B.BE{}), Tf) == True{} : Bool}>
24
25def 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
29def d2_fin(+kl: List<&2, String>, +k: Nat, +hk31: {Nat.is_lt(k, 31n) == True{} : Bool}, +OT: AR.Tree<U32>, +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.pow2(k))))), g3, L.and_intro(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)))), g4, L.and_intro(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))), g5, g6)))))))
39
40
41# THEOREM: deleting a full bucket of a good table (2^k buckets, a free one)
42def del_ok2(+k: Nat, +hk31: {Nat.is_lt(k, 31n) == True{} : Bool}, +kl: List<&2, String>, +OT: AR.Tree<U32>, +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))