proofs/containers/hash_table/cyc.bend
bend-collections-laws-containers@1.0.0.0 · 115 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/proofs/lib/u32alg.bend as A
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/arith.bend as AR
8import bend-collections-laws-containers@1.0.0.0/proofs/lib/u32div.bend as UD
9import bend-collections-laws-containers@1.0.0.0/proofs/math/u64/u64div.bend as UV
10import bend-collections-laws-containers@1.0.0.0/src/containers/hash_table.bend as H
11import bend-collections-laws-containers@1.0.0.0/proofs/lib/words32.bend as W32
12
13# Bucket indices of a table of N = 2^k buckets (mask = 2^k - 1, k <= 30):
14# and_mod x & mask == x mod N
15# next bnext(i) == (i + 1) mod N
16# dist (b - a) & mask == (b + N - a) mod N (the cyclic distance a -> b)
17# Bounds are over the symbolic `one` (see proofs/math/word.bend).
18
19def msk(+k: Nat) -> U32:
20 U32{WD.mask(32n, k)}
21
22# x & (2^k - 1) is x mod 2^k
23def and_mod(+one: Nat, +h1: {one == 1n : Nat}, +k: Nat, +x: U32) -> {UD.v(U32.and(x, msk(k))) == Nat.mod(UD.v(x), WD.sc(k, one)) : Nat}:
24 +a = UD.v(U32.and(x, msk(k)))
25 +hp = UV.hp32(k, x)
26 +split = UV.and32(k, x, msk(k), {==})
27 +lt = UV.and32_lt(k, one, h1, x, msk(k), {==})
28 +e = Equal.trans(Nat, UD.v(x), Nat.add(a, WD.sc(k, hp)), Nat.add(Nat.mul(hp, WD.sc(k, one)), a), split,
29 Equal.trans(Nat, Nat.add(a, WD.sc(k, hp)), Nat.add(WD.sc(k, hp), a), Nat.add(Nat.mul(hp, WD.sc(k, one)), a), N.add_comm(a, WD.sc(k, hp)), Equal.cong(Nat, Nat, z => Nat.add(z, a), WD.sc(k, hp), Nat.mul(hp, WD.sc(k, one)), Equal.sym(Nat, Nat.mul(hp, WD.sc(k, one)), WD.sc(k, hp), AR.mul_sc1(k, one, h1, hp)))))
30 Equal.sym(Nat, Nat.mod(UD.v(x), WD.sc(k, one)), a, Equal.trans(Nat, Nat.mod(UD.v(x), WD.sc(k, one)), Nat.mod(Nat.add(Nat.mul(hp, WD.sc(k, one)), a), WD.sc(k, one)), a, Equal.cong(Nat, Nat, z => Nat.mod(z, WD.sc(k, one)), UD.v(x), Nat.add(Nat.mul(hp, WD.sc(k, one)), a), e), UD.mod_identify(hp, WD.sc(k, one), a, lt)))
31
32
33# the next bucket, cyclically
34def next_val(+one: Nat, +h1: {one == 1n : Nat}, +k: Nat, +i: U32, +hk: {Nat.is_lt(WD.sc(k, one), WD.sc(32n, one)) == True{} : Bool}, +hi: {Nat.is_lt(UD.v(i), WD.sc(k, one)) == True{} : Bool}) -> {UD.v(H.bnext(i, msk(k))) == Nat.mod(1n+UD.v(i), WD.sc(k, one)) : Nat}:
35 +hin = W32.inc_val(one, h1, i, N.le_lt_trans(1n+UD.v(i), WD.sc(k, one), WD.sc(32n, one), N.lt_succ_le_succ(UD.v(i), WD.sc(k, one), hi), hk))
36 Equal.trans(Nat, UD.v(U32.and(U32.inc(i), msk(k))), Nat.mod(UD.v(U32.inc(i)), WD.sc(k, one)), Nat.mod(1n+UD.v(i), WD.sc(k, one)), and_mod(one, h1, k, U32.inc(i)), Equal.cong(Nat, Nat, z => Nat.mod(z, WD.sc(k, one)), UD.v(U32.inc(i)), 1n+UD.v(i), hin))
37
38# ---- cyclic distance ----
39
40def sub_split(+a: Nat, +n: Nat, +m: Nat, +ha: {Nat.is_le(a, n) == True{} : Bool}, +hn: {Nat.is_le(n, m) == True{} : Bool}) -> {Nat.sub(m, a) == Nat.add(Nat.sub(n, a), Nat.sub(m, n)) : Nat}:
41 +e1 = N.sub_add(n, a, ha)
42 +e2 = N.sub_add(m, n, hn)
43 # m == a + ((n - a) + (m - n))
44 +e3 = Equal.trans(Nat, m, Nat.add(n, Nat.sub(m, n)), Nat.add(a, Nat.add(Nat.sub(n, a), Nat.sub(m, n))), Equal.sym(Nat, Nat.add(n, Nat.sub(m, n)), m, e2),
45 Equal.trans(Nat, Nat.add(n, Nat.sub(m, n)), Nat.add(Nat.add(a, Nat.sub(n, a)), Nat.sub(m, n)), Nat.add(a, Nat.add(Nat.sub(n, a), Nat.sub(m, n))), Equal.cong(Nat, Nat, z => Nat.add(z, Nat.sub(m, n)), n, Nat.add(a, Nat.sub(n, a)), Equal.sym(Nat, Nat.add(a, Nat.sub(n, a)), n, e1)), N.add_assoc(a, Nat.sub(n, a), Nat.sub(m, n))))
46 %Equal.sym(Nat, m, Nat.add(a, Nat.add(Nat.sub(n, a), Nat.sub(m, n))), e3) : {Nat.sub(_, a) == Nat.add(Nat.sub(n, a), Nat.sub(m, n)) : Nat}
47 N.add_sub_cancel(a, Nat.add(Nat.sub(n, a), Nat.sub(m, n)))
48
49# (N + r) mod N == r for r < N
50def mod_plus(+n: Nat, +r: Nat, +h: {Nat.is_lt(r, n) == True{} : Bool}) -> {Nat.mod(Nat.add(n, r), n) == r : Nat}:
51 +e = Equal.cong(Nat, Nat, z => Nat.add(z, r), n, Nat.mul(1n, n), Equal.sym(Nat, Nat.mul(1n, n), n, N.add_zero(n)))
52 Equal.trans(Nat, Nat.mod(Nat.add(n, r), n), Nat.mod(Nat.add(Nat.mul(1n, n), r), n), r, Equal.cong(Nat, Nat, z => Nat.mod(z, n), Nat.add(n, r), Nat.add(Nat.mul(1n, n), r), e), UD.mod_identify(1n, n, r, h))
53
54def mod_small(+n: Nat, +r: Nat, +h: {Nat.is_lt(r, n) == True{} : Bool}) -> {Nat.mod(r, n) == r : Nat}:
55 UD.mod_identify(0n, n, r, h)
56
57def lt_add_r(+a: Nat, +b: Nat, +x: Nat, +h: {Nat.is_lt(a, b) == True{} : Bool}) -> {Nat.is_lt(Nat.add(a, x), Nat.add(b, x)) == True{} : Bool}:
58 L.subst(Nat, z => {Nat.is_lt(z, Nat.add(b, x)) == True{} : Bool}, Nat.add(x, a), Nat.add(a, x), N.add_comm(x, a), L.subst(Nat, z => {Nat.is_lt(Nat.add(x, a), z) == True{} : Bool}, Nat.add(x, b), Nat.add(b, x), N.add_comm(x, b), N.lt_add_left(a, b, x, h)))
59
60# b + (n - a) == n + (b - a) when a <= b and a <= n
61def wrap_free(+a: Nat, +b: Nat, +n: Nat, +hab: {Nat.is_le(a, b) == True{} : Bool}, +han: {Nat.is_le(a, n) == True{} : Bool}) -> {Nat.add(b, Nat.sub(n, a)) == Nat.add(n, Nat.sub(b, a)) : Nat}:
62 +x = Nat.sub(b, a)
63 +y = Nat.sub(n, a)
64 +e1 = Equal.cong(Nat, Nat, z => Nat.add(z, y), b, Nat.add(a, x), Equal.sym(Nat, Nat.add(a, x), b, N.sub_add(b, a, hab)))
65 +e2 = Equal.trans(Nat, Nat.add(Nat.add(a, x), y), Nat.add(Nat.add(a, y), x), Nat.add(n, x), A.add_rot(a, x, y), Equal.cong(Nat, Nat, z => Nat.add(z, x), Nat.add(a, y), n, N.sub_add(n, a, han)))
66 Equal.trans(Nat, Nat.add(b, y), Nat.add(Nat.add(a, x), y), Nat.add(n, x), e1, e2)
67
68def dist_le(+one: Nat, +h1: {one == 1n : Nat}, +k: Nat, +a: U32, +b: U32, +hb: {Nat.is_lt(UD.v(b), WD.sc(k, one)) == True{} : Bool}, +han: {Nat.is_le(UD.v(a), WD.sc(k, one)) == True{} : Bool}, +hab: {Nat.is_le(UD.v(a), UD.v(b)) == True{} : Bool}) -> {Nat.mod(UD.v(U32.sub(b, a)), WD.sc(k, one)) == Nat.mod(Nat.add(UD.v(b), Nat.sub(WD.sc(k, one), UD.v(a))), WD.sc(k, one)) : Nat}:
69 +n = WD.sc(k, one)
70 +d = Nat.sub(UD.v(b), UD.v(a))
71 +hd = N.le_lt_trans(d, UD.v(b), n, AR.sub_le2(UD.v(b), UD.v(a)), hb)
72 +l = Equal.trans(Nat, Nat.mod(UD.v(U32.sub(b, a)), n), Nat.mod(d, n), d, Equal.cong(Nat, Nat, z => Nat.mod(z, n), UD.v(U32.sub(b, a)), d, U.sub_nat(b, a, hab)), mod_small(n, d, hd))
73 +r = Equal.trans(Nat, Nat.mod(Nat.add(UD.v(b), Nat.sub(n, UD.v(a))), n), Nat.mod(Nat.add(n, d), n), d, Equal.cong(Nat, Nat, z => Nat.mod(z, n), Nat.add(UD.v(b), Nat.sub(n, UD.v(a))), Nat.add(n, d), wrap_free(UD.v(a), UD.v(b), n, hab, han)), mod_plus(n, d, hd))
74 Equal.trans(Nat, Nat.mod(UD.v(U32.sub(b, a)), n), d, Nat.mod(Nat.add(UD.v(b), Nat.sub(n, UD.v(a))), n), l, Equal.sym(Nat, Nat.mod(Nat.add(UD.v(b), Nat.sub(n, UD.v(a))), n), d, r))
75
76def dist_gt(+one: Nat, +h1: {one == 1n : Nat}, +k: Nat, +j: Nat, +hkj: {Nat.add(k, j) == 32n : Nat}, +a: U32, +b: U32, +ha: {Nat.is_lt(UD.v(a), WD.sc(k, one)) == True{} : Bool}, +hba: {Nat.is_lt(UD.v(b), UD.v(a)) == True{} : Bool}) -> {Nat.mod(UD.v(U32.sub(b, a)), WD.sc(k, one)) == Nat.mod(Nat.add(UD.v(b), Nat.sub(WD.sc(k, one), UD.v(a))), WD.sc(k, one)) : Nat}:
77 +n = WD.sc(k, one)
78 +kk = WD.sc(32n, one)
79 +av = UD.v(a)
80 +bv = UD.v(b)
81 +m = Nat.sub(WD.sc(j, one), one)
82 +hk = Equal.trans(Nat, kk, WD.sc(Nat.add(k, j), one), WD.sc(k, WD.sc(j, one)), Equal.cong(Nat, Nat, z => WD.sc(z, one), 32n, Nat.add(k, j), Equal.sym(Nat, Nat.add(k, j), 32n, hkj)), AR.sc_idx(k, j, one))
83 +hnk = L.subst(Nat, z => {Nat.is_le(n, z) == True{} : Bool}, WD.sc(k, WD.sc(j, one)), kk, Equal.sym(Nat, kk, WD.sc(k, WD.sc(j, one)), hk), AR.sc_le(k, one, WD.sc(j, one), AR.le_sc(j, one)))
84 +han = N.lt_le(av, n, ha)
85 +hak = N.le_trans(av, n, kk, han, hnk)
86 +d = Nat.add(bv, Nat.sub(kk, av))
87 +r = Nat.add(bv, Nat.sub(n, av))
88 # the machine difference is b + (2^32 - a)
89 +e = Equal.trans(Nat, Nat.add(bv, kk), Nat.add(bv, Nat.add(Nat.sub(kk, av), av)), Nat.add(d, av),
90 Equal.cong(Nat, Nat, z => Nat.add(bv, z), kk, Nat.add(Nat.sub(kk, av), av), Equal.sym(Nat, Nat.add(Nat.sub(kk, av), av), kk, Equal.trans(Nat, Nat.add(Nat.sub(kk, av), av), Nat.add(av, Nat.sub(kk, av)), kk, N.add_comm(Nat.sub(kk, av), av), N.sub_add(kk, av, hak)))),
91 Equal.sym(Nat, Nat.add(d, av), Nat.add(bv, Nat.add(Nat.sub(kk, av), av)), N.add_assoc(bv, Nat.sub(kk, av), av)))
92 +hd = L.subst(Nat, z => {Nat.is_lt(d, z) == True{} : Bool}, Nat.add(av, Nat.sub(kk, av)), kk, N.sub_add(kk, av, hak), lt_add_r(bv, av, Nat.sub(kk, av), hba))
93 +hsub = UD.sub32(one, h1, b, a, d, e, hd)
94 +hr = L.subst(Nat, z => {Nat.is_lt(r, z) == True{} : Bool}, Nat.add(av, Nat.sub(n, av)), n, N.sub_add(n, av, han), lt_add_r(bv, av, Nat.sub(n, av), hba))
95 # d == mul(m, n) + r
96 +ekn = Equal.trans(Nat, Nat.sub(kk, n), Nat.sub(WD.sc(k, WD.sc(j, one)), n), Nat.mul(m, n), Equal.cong(Nat, Nat, z => Nat.sub(z, n), kk, WD.sc(k, WD.sc(j, one)), hk),
97 Equal.trans(Nat, Nat.sub(WD.sc(k, WD.sc(j, one)), n), WD.sc(k, m), Nat.mul(m, n), Equal.sym(Nat, WD.sc(k, m), Nat.sub(WD.sc(k, WD.sc(j, one)), n), AR.sc_sub(k, WD.sc(j, one), one)), Equal.sym(Nat, Nat.mul(m, n), WD.sc(k, m), AR.mul_sc1(k, one, h1, m))))
98 +ed = Equal.trans(Nat, d, Nat.add(bv, Nat.add(Nat.sub(n, av), Nat.sub(kk, n))), Nat.add(Nat.mul(m, n), r),
99 Equal.cong(Nat, Nat, z => Nat.add(bv, z), Nat.sub(kk, av), Nat.add(Nat.sub(n, av), Nat.sub(kk, n)), sub_split(av, n, kk, han, hnk)),
100 Equal.trans(Nat, Nat.add(bv, Nat.add(Nat.sub(n, av), Nat.sub(kk, n))), Nat.add(r, Nat.sub(kk, n)), Nat.add(Nat.mul(m, n), r),
101 Equal.sym(Nat, Nat.add(r, Nat.sub(kk, n)), Nat.add(bv, Nat.add(Nat.sub(n, av), Nat.sub(kk, n))), N.add_assoc(bv, Nat.sub(n, av), Nat.sub(kk, n))),
102 Equal.trans(Nat, Nat.add(r, Nat.sub(kk, n)), Nat.add(r, Nat.mul(m, n)), Nat.add(Nat.mul(m, n), r), Equal.cong(Nat, Nat, z => Nat.add(r, z), Nat.sub(kk, n), Nat.mul(m, n), ekn), N.add_comm(r, Nat.mul(m, n)))))
103 +l = Equal.trans(Nat, Nat.mod(UD.v(U32.sub(b, a)), n), Nat.mod(Nat.add(Nat.mul(m, n), r), n), r, Equal.cong(Nat, Nat, z => Nat.mod(z, n), UD.v(U32.sub(b, a)), Nat.add(Nat.mul(m, n), r), Equal.trans(Nat, UD.v(U32.sub(b, a)), d, Nat.add(Nat.mul(m, n), r), hsub, ed)), UD.mod_identify(m, n, r, hr))
104 Equal.trans(Nat, Nat.mod(UD.v(U32.sub(b, a)), n), r, Nat.mod(r, n), l, Equal.sym(Nat, Nat.mod(r, n), r, mod_small(n, r, hr)))
105
106def dist_g(+one: Nat, +h1: {one == 1n : Nat}, +k: Nat, +j: Nat, +hkj: {Nat.add(k, j) == 32n : Nat}, +a: U32, +b: U32, +ha: {Nat.is_lt(UD.v(a), WD.sc(k, one)) == True{} : Bool}, +hb: {Nat.is_lt(UD.v(b), WD.sc(k, one)) == True{} : Bool}, +c: Bool, +hc: {Nat.is_le(UD.v(a), UD.v(b)) == c : Bool}) -> {Nat.mod(UD.v(U32.sub(b, a)), WD.sc(k, one)) == Nat.mod(Nat.add(UD.v(b), Nat.sub(WD.sc(k, one), UD.v(a))), WD.sc(k, one)) : Nat}:
107 match c:
108 case True{}:
109 dist_le(one, h1, k, a, b, hb, N.lt_le(UD.v(a), WD.sc(k, one), ha), hc)
110 case False{}:
111 dist_gt(one, h1, k, j, hkj, a, b, ha, N.not_le_lt(UD.v(a), UD.v(b), hc))
112
113# THEOREM: (b - a) & mask is the cyclic distance from a to b.
114def dist(+one: Nat, +h1: {one == 1n : Nat}, +k: Nat, +j: Nat, +hkj: {Nat.add(k, j) == 32n : Nat}, +a: U32, +b: U32, +ha: {Nat.is_lt(UD.v(a), WD.sc(k, one)) == True{} : Bool}, +hb: {Nat.is_lt(UD.v(b), WD.sc(k, one)) == True{} : Bool}) -> {UD.v(U32.and(U32.sub(b, a), msk(k))) == Nat.mod(Nat.add(UD.v(b), Nat.sub(WD.sc(k, one), UD.v(a))), WD.sc(k, one)) : Nat}:
115 Equal.trans(Nat, UD.v(U32.and(U32.sub(b, a), msk(k))), Nat.mod(UD.v(U32.sub(b, a)), WD.sc(k, one)), Nat.mod(Nat.add(UD.v(b), Nat.sub(WD.sc(k, one), UD.v(a))), WD.sc(k, one)), and_mod(one, h1, k, U32.sub(b, a)), dist_g(one, h1, k, j, hkj, a, b, ha, hb, Nat.is_le(UD.v(a), UD.v(b)), {==}))