proofs/containers/hash_table/insu.bend
bend-collections-laws-containers@1.0.0.0 · 87 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/u32.bend as U
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/word.bend as WD
7import bend-collections-laws-containers@1.0.0.0/proofs/lib/u32div.bend as UD
8import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/cyc.bend as CY
9import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/probe_all.bend as PA
10import bend-collections-laws-containers@1.0.0.0/proofs/lib/words32.bend as W32
11
12# U32 facts for insertion: links and slots, the load test, counters.
13
14
15# x < 2^d with d + 1 < 32 leaves room for one more
16
17
18# THEOREM: the slot of the link of s is s
19
20
21# THEOREM: a link is never 0
22
23# ---- comparisons ----
24
25def is_gt_nat(+a: U32, +b: U32) -> {U32.is_gt(a, b) == Nat.is_gt(UD.v(a), UD.v(b)) : Bool}:
26 Equal.cong(Cmp, Bool, c => Cmp.is_gt(c), U32.cmp(a, b), Nat.cmp(UD.v(a), UD.v(b)), U.u32_cmp(a, b))
27
28def gt_le_c(+a: Nat, +b: Nat, +c: Cmp, +hc: {Nat.cmp(a, b) == c : Cmp}, +h: {Cmp.is_gt(c) == False{} : Bool}) -> {Cmp.is_le(c) == True{} : Bool}:
29 match c:
30 case LT{}:
31 {==}
32 case EQ{}:
33 {==}
34 case GT{}:
35 Empty.absurd({Cmp.is_le(GT{}) == True{} : Bool}, L.true_false(h))
36
37def gt_false_le(+a: Nat, +b: Nat, +h: {Nat.is_gt(a, b) == False{} : Bool}) -> {Nat.is_le(a, b) == True{} : Bool}:
38 gt_le_c(a, b, Nat.cmp(a, b), {==}, h)
39
40def gt_le_t(+a: Nat, +b: Nat, +c: Cmp, +h: {Cmp.is_gt(c) == True{} : Bool}) -> {Cmp.is_le(c) == False{} : Bool}:
41 match c:
42 case LT{}:
43 Empty.absurd({Cmp.is_le(LT{}) == False{} : Bool}, L.false_true(h))
44 case EQ{}:
45 Empty.absurd({Cmp.is_le(EQ{}) == False{} : Bool}, L.false_true(h))
46 case GT{}:
47 {==}
48
49# a > b: not a <= b
50def gt_true_nle(+a: Nat, +b: Nat, +h: {Nat.is_gt(a, b) == True{} : Bool}) -> {Nat.is_le(a, b) == False{} : Bool}:
51 gt_le_t(a, b, Nat.cmp(a, b), h)
52
53# ---- the load test ----
54
55def dle_c(+x: Nat, +y: Nat, +h: {Nat.is_le(Nat.double(x), Nat.double(y)) == True{} : Bool}, +c: Bool, +hc: {Nat.is_le(x, y) == c : Bool}) -> {c == True{} : Bool}:
56 match c:
57 case True{}:
58 {==}
59 case False{}:
60 Empty.absurd({False{} == True{} : Bool}, L.true_false(Equal.trans(Bool, True{}, Nat.is_le(Nat.double(x), Nat.double(y)), False{}, Equal.sym(Bool, Nat.is_le(Nat.double(x), Nat.double(y)), True{}, h), N.lt_not_le(Nat.double(y), Nat.double(x), N.double_lt(y, x, N.not_le_lt(x, y, hc))))))
61
62def dbl_le_inv(+x: Nat, +y: Nat, +h: {Nat.is_le(Nat.double(x), Nat.double(y)) == True{} : Bool}) -> {Nat.is_le(x, y) == True{} : Bool}:
63 dle_c(x, y, h, Nat.is_le(x, y), {==})
64
65# 2x <= 2^(p+1): x + 1 <= 2^(p+1)
66def succ_le_pow(+x: Nat, +p: Nat, +h: {Nat.is_le(Nat.double(x), SC.pow2(1n+p)) == True{} : Bool}) -> {Nat.is_le(1n+x, SC.pow2(1n+p)) == True{} : Bool}:
67 N.le_trans(1n+x, 1n+SC.pow2(p), SC.pow2(1n+p), dbl_le_inv(x, SC.pow2(p), h), N.double_succ_le(SC.pow2(p), N.pow2_pos(p)))
68
69def over_c(+one: Nat, +h1: {one == 1n : Nat}, +k: Nat, +hk31: {Nat.is_lt(k, 31n) == True{} : Bool}, +hk0: {Nat.is_lt(0n, k) == True{} : Bool}, +x: Nat, +h: {Nat.is_le(Nat.double(x), SC.pow2(k)) == True{} : Bool}) -> {Nat.is_le(1n+x, SC.pow2(k)) == True{} : Bool}:
70 match k:
71 case 0n:
72 Empty.absurd({Nat.is_le(1n+x, SC.pow2(0n)) == True{} : Bool}, L.false_true(hk0))
73 case 1n+p:
74 succ_le_pow(x, p, h)
75
76# THEOREM: with at most half the buckets full, one more entry is n + 1 and
77# the load test compares 2(n + 1) with the bucket count
78def inc_n(+one: Nat, +h1: {one == 1n : Nat}, +k: Nat, +hk31: {Nat.is_lt(k, 31n) == True{} : Bool}, +hk0: {Nat.is_lt(0n, k) == True{} : Bool}, +n: U32, +hl: {Nat.is_le(Nat.double(UD.v(n)), SC.pow2(k)) == True{} : Bool}) -> {UD.v(U32.inc(n)) == 1n+UD.v(n) : Nat}:
79 W32.inc_val(one, h1, n, N.le_lt_trans(1n+UD.v(n), SC.pow2(k), WD.sc(32n, one), over_c(one, h1, k, hk31, hk0, UD.v(n), hl), 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))))
80
81def over_val(+one: Nat, +h1: {one == 1n : Nat}, +k: Nat, +hk31: {Nat.is_lt(k, 31n) == True{} : Bool}, +hk0: {Nat.is_lt(0n, k) == True{} : Bool}, +n: U32, +hl: {Nat.is_le(Nat.double(UD.v(n)), SC.pow2(k)) == True{} : Bool}) -> {U32.is_gt(U32.shl(U32.inc(n)), U32.inc(CY.msk(k))) == Nat.is_gt(Nat.double(1n+UD.v(n)), SC.pow2(k)) : Bool}:
82 +ei = inc_n(one, h1, k, hk31, hk0, n, hl)
83 +d1 = N.double_le(1n+UD.v(n), SC.pow2(k), over_c(one, h1, k, hk31, hk0, UD.v(n), hl))
84 +d2 = L.subst(Nat, z => {Nat.is_lt(Nat.double(z), SC.pow2(2n+k)) == True{} : Bool}, 1n+UD.v(n), UD.v(U32.inc(n)), Equal.sym(Nat, UD.v(U32.inc(n)), 1n+UD.v(n), ei), N.le_lt_trans(Nat.double(1n+UD.v(n)), SC.pow2(1n+k), SC.pow2(2n+k), d1, N.pow2_lt_succ(1n+k)))
85 +es = Equal.trans(Nat, UD.v(U32.shl(U32.inc(n))), Nat.double(UD.v(U32.inc(n))), Nat.double(1n+UD.v(n)), U.shl_value(U32.inc(n), 2n+k, N.lt_succ_le(k, 30n, hk31), d2), Equal.cong(Nat, Nat, z => Nat.double(z), UD.v(U32.inc(n)), 1n+UD.v(n), ei))
86 Equal.trans(Bool, U32.is_gt(U32.shl(U32.inc(n)), U32.inc(CY.msk(k))), Nat.is_gt(UD.v(U32.shl(U32.inc(n))), UD.v(U32.inc(CY.msk(k)))), Nat.is_gt(Nat.double(1n+UD.v(n)), SC.pow2(k)), is_gt_nat(U32.shl(U32.inc(n)), U32.inc(CY.msk(k))),
87 Equal.trans(Bool, Nat.is_gt(UD.v(U32.shl(U32.inc(n))), UD.v(U32.inc(CY.msk(k)))), Nat.is_gt(Nat.double(1n+UD.v(n)), UD.v(U32.inc(CY.msk(k)))), Nat.is_gt(Nat.double(1n+UD.v(n)), SC.pow2(k)), Equal.cong(Nat, Bool, z => Nat.is_gt(z, UD.v(U32.inc(CY.msk(k)))), UD.v(U32.shl(U32.inc(n))), Nat.double(1n+UD.v(n)), es), Equal.cong(Nat, Bool, z => Nat.is_gt(Nat.double(1n+UD.v(n)), z), UD.v(U32.inc(CY.msk(k))), SC.pow2(k), PA.fuel_eq(one, h1, k, hk31))))