proofs/containers/hash_table/modn.bend
bend-collections-laws-containers@1.0.0.0 · 84 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat.bend as N
3import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
4import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/word_value.bend as WV
5import bend-collections-laws-containers@1.0.0.0/proofs/lib/u32div.bend as UD
6import bend-collections-laws-containers@1.0.0.0/proofs/containers/hash_table/cyc.bend as CY
7
8# Offsets around a ring of n buckets (n > 0):
9# pos(n, h, t) == (h + t) mod n the bucket t steps after h
10# dist(n, h, j) == (j + n - h) mod n the steps from h to j
11# and they are inverse.
12
13def pos(+n: Nat, +h: Nat, +t: Nat) -> Nat:
14 Nat.mod(Nat.add(h, t), n)
15
16def dist(+n: Nat, +h: Nat, +j: Nat) -> Nat:
17 Nat.mod(Nat.add(j, Nat.sub(n, h)), n)
18
19def dm_e2(+bp: Nat, +v: Nat, g: WV.go_equation(bp, v, bp, 0n, 0n)) -> {v == Nat.add(Nat.mul(Nat.div(v, 1n+bp), 1n+bp), Nat.mod(v, 1n+bp)) : Nat}:
20 (e, l) = g
21 e
22
23def dm_l2(+bp: Nat, +v: Nat, g: WV.go_equation(bp, v, bp, 0n, 0n)) -> {Nat.is_lt(Nat.mod(v, 1n+bp), 1n+bp) == True{} : Bool}:
24 (e, l) = g
25 N.le_lt_succ(Nat.mod(v, 1n+bp), bp, l)
26
27# v == (v / n) n + v mod n, and v mod n < n
28def dm_eq(+bp: Nat, +v: Nat) -> {v == Nat.add(Nat.mul(Nat.div(v, 1n+bp), 1n+bp), Nat.mod(v, 1n+bp)) : Nat}:
29 dm_e2(bp, v, WV.go(bp, v, bp, 0n, 0n, N.add_zero(bp)))
30
31def dm_lt(+bp: Nat, +v: Nat) -> {Nat.is_lt(Nat.mod(v, 1n+bp), 1n+bp) == True{} : Bool}:
32 dm_l2(bp, v, WV.go(bp, v, bp, 0n, 0n, N.add_zero(bp)))
33
34# (q n + r) mod n == r mod n
35def absorb(+bp: Nat, +q: Nat, +r: Nat) -> {Nat.mod(Nat.add(Nat.mul(q, 1n+bp), r), 1n+bp) == Nat.mod(r, 1n+bp) : Nat}:
36 +n = {1n+bp : Nat}
37 +qr = Nat.div(r, n)
38 +m = Nat.mod(r, n)
39 +e = Equal.trans(Nat, Nat.add(Nat.mul(q, n), r), Nat.add(Nat.mul(q, n), Nat.add(Nat.mul(qr, n), m)), Nat.add(Nat.mul(Nat.add(q, qr), n), m),
40 Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(q, n), z), r, Nat.add(Nat.mul(qr, n), m), dm_eq(bp, r)),
41 Equal.trans(Nat, Nat.add(Nat.mul(q, n), Nat.add(Nat.mul(qr, n), m)), Nat.add(Nat.add(Nat.mul(q, n), Nat.mul(qr, n)), m), Nat.add(Nat.mul(Nat.add(q, qr), n), m),
42 Equal.sym(Nat, Nat.add(Nat.add(Nat.mul(q, n), Nat.mul(qr, n)), m), Nat.add(Nat.mul(q, n), Nat.add(Nat.mul(qr, n), m)), N.add_assoc(Nat.mul(q, n), Nat.mul(qr, n), m)),
43 Equal.cong(Nat, Nat, z => Nat.add(z, m), Nat.add(Nat.mul(q, n), Nat.mul(qr, n)), Nat.mul(Nat.add(q, qr), n), Equal.sym(Nat, Nat.mul(Nat.add(q, qr), n), Nat.add(Nat.mul(q, n), Nat.mul(qr, n)), NA.mul_add_right(q, qr, n)))))
44 Equal.trans(Nat, Nat.mod(Nat.add(Nat.mul(q, n), r), n), Nat.mod(Nat.add(Nat.mul(Nat.add(q, qr), n), m), n), m, Equal.cong(Nat, Nat, z => Nat.mod(z, n), Nat.add(Nat.mul(q, n), r), Nat.add(Nat.mul(Nat.add(q, qr), n), m), e), UD.mod_identify(Nat.add(q, qr), n, m, dm_lt(bp, r)))
45
46# x + (y mod n) and x + y agree mod n
47def mod_inner(+bp: Nat, +x: Nat, +y: Nat) -> {Nat.mod(Nat.add(x, Nat.mod(y, 1n+bp)), 1n+bp) == Nat.mod(Nat.add(x, y), 1n+bp) : Nat}:
48 +n = {1n+bp : Nat}
49 +qy = Nat.div(y, n)
50 +my = Nat.mod(y, n)
51 +e = Equal.trans(Nat, Nat.add(x, y), Nat.add(x, Nat.add(Nat.mul(qy, n), my)), Nat.add(Nat.mul(qy, n), Nat.add(x, my)),
52 Equal.cong(Nat, Nat, z => Nat.add(x, z), y, Nat.add(Nat.mul(qy, n), my), dm_eq(bp, y)),
53 NA.add_swap(x, Nat.mul(qy, n), my))
54 Equal.sym(Nat, Nat.mod(Nat.add(x, y), n), Nat.mod(Nat.add(x, my), n), Equal.trans(Nat, Nat.mod(Nat.add(x, y), n), Nat.mod(Nat.add(Nat.mul(qy, n), Nat.add(x, my)), n), Nat.mod(Nat.add(x, my), n), Equal.cong(Nat, Nat, z => Nat.mod(z, n), Nat.add(x, y), Nat.add(Nat.mul(qy, n), Nat.add(x, my)), e), absorb(bp, qy, Nat.add(x, my))))
55
56def pos_lt(+bp: Nat, +h: Nat, +t: Nat) -> {Nat.is_lt(pos(1n+bp, h, t), 1n+bp) == True{} : Bool}:
57 dm_lt(bp, Nat.add(h, t))
58
59def dist_lt(+bp: Nat, +h: Nat, +j: Nat) -> {Nat.is_lt(dist(1n+bp, h, j), 1n+bp) == True{} : Bool}:
60 dm_lt(bp, Nat.add(j, Nat.sub(1n+bp, h)))
61
62# walking dist(h, j) steps from h reaches j
63def pos_dist(+bp: Nat, +h: Nat, +j: Nat, +hh: {Nat.is_lt(h, 1n+bp) == True{} : Bool}, +hj: {Nat.is_lt(j, 1n+bp) == True{} : Bool}) -> {pos(1n+bp, h, dist(1n+bp, h, j)) == j : Nat}:
64 +n = {1n+bp : Nat}
65 +s = Nat.add(j, Nat.sub(n, h))
66 +e = Equal.trans(Nat, Nat.add(h, s), Nat.add(j, Nat.add(h, Nat.sub(n, h))), Nat.add(n, j), NA.add_swap(h, j, Nat.sub(n, h)),
67 Equal.trans(Nat, Nat.add(j, Nat.add(h, Nat.sub(n, h))), Nat.add(j, n), Nat.add(n, j), Equal.cong(Nat, Nat, z => Nat.add(j, z), Nat.add(h, Nat.sub(n, h)), n, N.sub_add(n, h, N.lt_le(h, n, hh))), N.add_comm(j, n)))
68 Equal.trans(Nat, Nat.mod(Nat.add(h, Nat.mod(s, n)), n), Nat.mod(Nat.add(h, s), n), j, mod_inner(bp, h, s),
69 Equal.trans(Nat, Nat.mod(Nat.add(h, s), n), Nat.mod(Nat.add(n, j), n), j, Equal.cong(Nat, Nat, z => Nat.mod(z, n), Nat.add(h, s), Nat.add(n, j), e), CY.mod_plus(n, j, hj)))
70
71# the distance from h to the bucket t < n steps after h is t
72def dist_pos(+bp: Nat, +h: Nat, +t: Nat, +hh: {Nat.is_lt(h, 1n+bp) == True{} : Bool}, +ht: {Nat.is_lt(t, 1n+bp) == True{} : Bool}) -> {dist(1n+bp, h, pos(1n+bp, h, t)) == t : Nat}:
73 +n = {1n+bp : Nat}
74 +d = Nat.sub(n, h)
75 +x = Nat.mod(Nat.add(h, t), n)
76 +e1 = Equal.trans(Nat, Nat.mod(Nat.add(x, d), n), Nat.mod(Nat.add(d, x), n), Nat.mod(Nat.add(d, Nat.add(h, t)), n), Equal.cong(Nat, Nat, z => Nat.mod(z, n), Nat.add(x, d), Nat.add(d, x), N.add_comm(x, d)), mod_inner(bp, d, Nat.add(h, t)))
77 +e2 = Equal.trans(Nat, Nat.add(d, Nat.add(h, t)), Nat.add(Nat.add(d, h), t), Nat.add(n, t), Equal.sym(Nat, Nat.add(Nat.add(d, h), t), Nat.add(d, Nat.add(h, t)), N.add_assoc(d, h, t)),
78 Equal.cong(Nat, Nat, z => Nat.add(z, t), Nat.add(d, h), n, Equal.trans(Nat, Nat.add(d, h), Nat.add(h, d), n, N.add_comm(d, h), N.sub_add(n, h, N.lt_le(h, n, hh)))))
79 Equal.trans(Nat, Nat.mod(Nat.add(x, d), n), Nat.mod(Nat.add(d, Nat.add(h, t)), n), t, e1, Equal.trans(Nat, Nat.mod(Nat.add(d, Nat.add(h, t)), n), Nat.mod(Nat.add(n, t), n), t, Equal.cong(Nat, Nat, z => Nat.mod(z, n), Nat.add(d, Nat.add(h, t)), Nat.add(n, t), e2), CY.mod_plus(n, t, ht)))
80
81# the bucket after pos(h, t) is pos(h, t + 1)
82def pos_next(+bp: Nat, +h: Nat, +t: Nat) -> {Nat.mod(1n+pos(1n+bp, h, t), 1n+bp) == pos(1n+bp, h, 1n+t) : Nat}:
83 +n = {1n+bp : Nat}
84 Equal.trans(Nat, Nat.mod(Nat.add(1n, Nat.mod(Nat.add(h, t), n)), n), Nat.mod(Nat.add(1n, Nat.add(h, t)), n), Nat.mod(Nat.add(h, 1n+t), n), mod_inner(bp, 1n, Nat.add(h, t)), Equal.cong(Nat, Nat, z => Nat.mod(z, n), 1n+Nat.add(h, t), Nat.add(h, 1n+t), Equal.sym(Nat, Nat.add(h, 1n+t), 1n+Nat.add(h, t), N.add_succ(h, t))))