proofs/math/u64/u64.bend
bend-collections-laws-containers@1.0.0.0 · 258 lines · 0 definitions
1import Base
2import bend-collections-laws-containers@1.0.0.0/spec/math/u64.bend as SU
3import bend-collections-laws-containers@1.0.0.0/src/math/u64.bend as U
4import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/src/wide.bend as W
5import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S
6import bend-collections-laws-containers@1.0.0.0/proofs/lib/logic.bend as L
7import bend-collections-laws-containers@1.0.0.0/proofs/lib/nat.bend as N
8import bend-collections-laws-containers@1.0.0.0/proofs/lib/u32.bend as U3
9import bend-collections-laws-containers@1.0.0.0/proofs/lib/u32alg.bend as A
10import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/numeric.bend as NUM
11import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/addition.bend as AD
12import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/modular_addition.bend as MA
13import bend-collections-laws-containers@1.0.0.0/proofs/lib/lemmas/proofs/word_addition.bend as WA
14import bend-collections-laws-containers@1.0.0.0/proofs/lib/word.bend as WD
15import bend-collections-laws-containers@1.0.0.0/proofs/lib/u32div.bend as UD
16
17# src/math/u64.bend against its specification spec/math/u64.bend: a U64
18# denotes the 64-bit word bits(a) (low limb first).
19
20def bits(a: U.U64) -> Word(64n):
21 SU.bits(a)
22
23# ---- comparison ----
24
25def order_eq(+c: Cmp) -> {U.order(c, EQ{}) == c : Cmp}:
26 match c:
27 case LT{}:
28 {==}
29 case EQ{}:
30 {==}
31 case GT{}:
32 {==}
33
34def fin_order(+x: Bool, +y: Bool, +c: Cmp, +d: Cmp) -> {Word.cmp.fin(x, y, U.order(c, d)) == U.order(c, Word.cmp.fin(x, y, d)) : Cmp}:
35 match c:
36 case LT{}:
37 {==}
38 case EQ{}:
39 {==}
40 case GT{}:
41 {==}
42
43# Comparing two joined words is comparing the high parts, then the low parts.
44def cmp_join(+n: Nat, +m: Nat, +a1: Word(n), +b1: Word(m), +a2: Word(n), +b2: Word(m)) -> {Word.cmp(Nat.add(n, m), W.join(n, m, a1, b1), W.join(n, m, a2, b2)) == U.order(Word.cmp(m, b1, b2), Word.cmp(n, a1, a2)) : Cmp}:
45 match n a1 a2:
46 case 0n WNil{} WNil{}:
47 Equal.sym(Cmp, U.order(Word.cmp(m, b1, b2), EQ{}), Word.cmp(m, b1, b2), order_eq(Word.cmp(m, b1, b2)))
48 case 1n+p WCon{x, t1} WCon{y, t2}:
49 %Equal.sym(Cmp, Word.cmp(Nat.add(p, m), W.join(p, m, t1, b1), W.join(p, m, t2, b2)), U.order(Word.cmp(m, b1, b2), Word.cmp(p, t1, t2)), cmp_join(p, m, t1, b1, t2, b2)) : {Word.cmp.fin(x, y, _) == U.order(Word.cmp(m, b1, b2), Word.cmp.fin(x, y, Word.cmp(p, t1, t2))) : Cmp}
50 fin_order(x, y, Word.cmp(m, b1, b2), Word.cmp(p, t1, t2))
51
52def u32_cmp(+x: Word(32n), +y: Word(32n)) -> {U32.cmp(U32{x}, U32{y}) == Word.cmp(32n, x, y) : Cmp}:
53 {==}
54
55def cmp_pack(+alo: U32, +ahi: U32, +blo: U32, +bhi: U32) -> {Word.cmp(64n, W.pack(alo, ahi), W.pack(blo, bhi)) == U.order(U32.cmp(ahi, bhi), U32.cmp(alo, blo)) : Cmp}:
56 match alo ahi blo bhi:
57 case U32{a} U32{b} U32{c} U32{d}:
58 cmp_join(32n, 32n, a, b, c, d)
59
60def ge_fin_zero(+c: Cmp, +x: Bool, +h: {Cmp.is_ge(c) == True{} : Bool}) -> {Cmp.is_ge(Word.cmp.fin(x, False{}, c)) == True{} : Bool}:
61 match c x:
62 case LT{} _:
63 Empty.absurd({Cmp.is_ge(Word.cmp.fin(x, False{}, LT{})) == True{} : Bool}, L.false_true(h))
64 case EQ{} True{}:
65 {==}
66 case EQ{} False{}:
67 {==}
68 case GT{} _:
69 {==}
70
71# Nothing compares below zero.
72def ge_zero(+n: Nat, +w: Word(n)) -> {Cmp.is_ge(Word.cmp(n, w, Word.zero(n))) == True{} : Bool}:
73 match n w:
74 case 0n WNil{}:
75 {==}
76 case 1n+p WCon{x, t}:
77 ge_fin_zero(Word.cmp(p, t, Word.zero(p)), x, ge_zero(p, t))
78
79def ge_order(+c: Cmp, +d: Cmp, +h: {Cmp.is_ge(d) == True{} : Bool}) -> {Cmp.is_ge(U.order(c, d)) == Cmp.is_ge(c) : Bool}:
80 match c:
81 case LT{}:
82 {==}
83 case EQ{}:
84 h
85 case GT{}:
86 {==}
87
88def threshold() -> {S.sign_threshold(63n) == W.join(32n, 32n, Word.zero(32n), S.sign_threshold(31n)) : Word(64n)}:
89 {==}
90
91def threshold_u32() -> {2147483648 == U32{S.sign_threshold(31n)} : U32}:
92 {==}
93
94# The sign of the 64-bit word is the top bit of the high limb.
95def negative_pack(+lo: U32, +hi: U32) -> {S.negative(W.pack(lo, hi)) == U32.is_ge(hi, 2147483648) : Bool}:
96 match lo hi:
97 case U32{a} U32{b}:
98 %Equal.sym(Word(64n), W.join(32n, 32n, Word.zero(32n), S.sign_threshold(31n)), S.sign_threshold(63n), threshold()) : {Cmp.is_ge(Word.cmp(64n, W.join(32n, 32n, a, b), _)) == U32.is_ge(U32{b}, 2147483648) : Bool}
99 %Equal.sym(Cmp, Word.cmp(64n, W.join(32n, 32n, a, b), W.join(32n, 32n, Word.zero(32n), S.sign_threshold(31n))), U.order(Word.cmp(32n, b, S.sign_threshold(31n)), Word.cmp(32n, a, Word.zero(32n))), cmp_join(32n, 32n, a, b, Word.zero(32n), S.sign_threshold(31n))) : {Cmp.is_ge(_) == U32.is_ge(U32{b}, 2147483648) : Bool}
100 %Equal.sym(U32, U32{S.sign_threshold(31n)}, 2147483648, threshold_u32()) : {Cmp.is_ge(U.order(Word.cmp(32n, b, S.sign_threshold(31n)), Word.cmp(32n, a, Word.zero(32n)))) == U32.is_ge(U32{b}, _) : Bool}
101 ge_order(Word.cmp(32n, b, S.sign_threshold(31n)), Word.cmp(32n, a, Word.zero(32n)), ge_zero(32n, a))
102
103def le_sign_spec(+alo: U32, +ahi: U32, +blo: U32, +bhi: U32, +na: Bool, +nb: Bool) -> {U.le_sign(alo, ahi, blo, bhi, na, nb) == S.order(W.pack(alo, ahi), W.pack(blo, bhi), na, nb) : Bool}:
104 match na nb:
105 case True{} False{}:
106 {==}
107 case False{} True{}:
108 {==}
109 case True{} True{}:
110 %cmp_pack(alo, ahi, blo, bhi) : {Cmp.is_le(_) == Cmp.is_le(Word.cmp(64n, W.pack(alo, ahi), W.pack(blo, bhi))) : Bool}
111 {==}
112 case False{} False{}:
113 %cmp_pack(alo, ahi, blo, bhi) : {Cmp.is_le(_) == Cmp.is_le(Word.cmp(64n, W.pack(alo, ahi), W.pack(blo, bhi))) : Bool}
114 {==}
115
116# THEOREM: le_signed is the specification's signed 64-bit order.
117def le_signed(+a: U.U64, +b: U.U64) -> {U.le_signed(a, b) == S.order(bits(a), bits(b), S.negative(bits(a)), S.negative(bits(b))) : Bool}:
118 match a b:
119 case U.U64{alo, ahi} U.U64{blo, bhi}:
120 %Equal.sym(Bool, S.negative(W.pack(alo, ahi)), U32.is_ge(ahi, 2147483648), negative_pack(alo, ahi)) : {U.le_signed(U.U64{alo, ahi}, U.U64{blo, bhi}) == S.order(W.pack(alo, ahi), W.pack(blo, bhi), _, S.negative(W.pack(blo, bhi))) : Bool}
121 %Equal.sym(Bool, S.negative(W.pack(blo, bhi)), U32.is_ge(bhi, 2147483648), negative_pack(blo, bhi)) : {U.le_signed(U.U64{alo, ahi}, U.U64{blo, bhi}) == S.order(W.pack(alo, ahi), W.pack(blo, bhi), U32.is_ge(ahi, 2147483648), _) : Bool}
122 le_sign_spec(alo, ahi, blo, bhi, U32.is_ge(ahi, 2147483648), U32.is_ge(bhi, 2147483648))
123
124# ---- zero test ----
125
126def eq_order(+c: Cmp, +d: Cmp) -> {Cmp.is_eq(U.order(c, d)) == Bool.and(Cmp.is_eq(d), Cmp.is_eq(c)) : Bool}:
127 match c d:
128 case LT{} LT{}:
129 {==}
130 case LT{} EQ{}:
131 {==}
132 case LT{} GT{}:
133 {==}
134 case EQ{} LT{}:
135 {==}
136 case EQ{} EQ{}:
137 {==}
138 case EQ{} GT{}:
139 {==}
140 case GT{} LT{}:
141 {==}
142 case GT{} EQ{}:
143 {==}
144 case GT{} GT{}:
145 {==}
146
147def zero_pack() -> {Word.zero(64n) == W.pack(0, 0) : Word(64n)}:
148 {==}
149
150# THEOREM: is_zero is the specification's zero test.
151def is_zero(+a: U.U64) -> {U.is_zero(a) == S.zero(bits(a)) : Bool}:
152 match a:
153 case U.U64{lo, hi}:
154 %Equal.sym(Word(64n), W.pack(0, 0), Word.zero(64n), zero_pack()) : {U.is_zero(U.U64{lo, hi}) == Cmp.is_eq(Word.cmp(64n, W.pack(lo, hi), _)) : Bool}
155 %Equal.sym(Cmp, Word.cmp(64n, W.pack(lo, hi), W.pack(0, 0)), U.order(U32.cmp(hi, 0), U32.cmp(lo, 0)), cmp_pack(lo, hi, 0, 0)) : {U.is_zero(U.U64{lo, hi}) == Cmp.is_eq(_) : Bool}
156 Equal.sym(Bool, Cmp.is_eq(U.order(U32.cmp(hi, 0), U32.cmp(lo, 0))), Bool.and(Cmp.is_eq(U32.cmp(lo, 0)), Cmp.is_eq(U32.cmp(hi, 0))), eq_order(U32.cmp(hi, 0), U32.cmp(lo, 0)))
157
158# ---- addition ----
159
160def val(+a: U.U64) -> Nat:
161 S.unsigned(64n, bits(a))
162
163def val_pack(+lo: U32, +hi: U32) -> {S.unsigned(64n, W.pack(lo, hi)) == Nat.add(UD.v(lo), WD.sc(32n, UD.v(hi))) : Nat}:
164 NUM.pack_interpretation(lo, hi)
165
166def carry32(+x: U32, +y: U32) -> Bool:
167 match x y:
168 case U32{a} U32{b}:
169 AD.carry_out(32n, a, b, False{})
170
171def add_cons(+x: U32, +y: U32) -> {Nat.add(UD.v(U32.add(x, y)), WD.sc(32n, S.bit_value(carry32(x, y)))) == Nat.add(UD.v(x), UD.v(y)) : Nat}:
172 match x y:
173 case U32{+a} U32{+b}:
174 %Equal.sym(Nat, UD.v(U32{Word.add(32n, a, b)}), WD.uw(32n, Word.add(32n, a, b)), UD.vw(Word.add(32n, a, b))) : {Nat.add(_, WD.sc(32n, S.bit_value(AD.carry_out(32n, a, b, False{})))) == Nat.add(UD.v(U32{a}), UD.v(U32{b})) : Nat}
175 %Equal.sym(Nat, UD.v(U32{a}), WD.uw(32n, a), UD.vw(a)) : {Nat.add(WD.uw(32n, Word.add(32n, a, b)), WD.sc(32n, S.bit_value(AD.carry_out(32n, a, b, False{})))) == Nat.add(_, UD.v(U32{b})) : Nat}
176 %Equal.sym(Nat, UD.v(U32{b}), WD.uw(32n, b), UD.vw(b)) : {Nat.add(WD.uw(32n, Word.add(32n, a, b)), WD.sc(32n, S.bit_value(AD.carry_out(32n, a, b, False{})))) == Nat.add(WD.uw(32n, a), _) : Nat}
177 A.cons(32n, a, b)
178
179def add_lt1(+one: Nat, +h1: {one == 1n : Nat}, +x: U32, +y: U32) -> {U32.is_lt(U32.add(x, y), x) == carry32(x, y) : Bool}:
180 %Equal.sym(Bool, U32.is_lt(U32.add(x, y), x), Nat.is_lt(UD.v(U32.add(x, y)), UD.v(x)), U3.is_lt_nat(U32.add(x, y), x)) : {_ == carry32(x, y) : Bool}
181 WD.carry_lt(32n, one, h1, UD.v(U32.add(x, y)), UD.v(x), UD.v(y), carry32(x, y), add_cons(x, y), UD.vb(one, h1, y))
182
183# the low-limb wrap test is the low-limb carry
184def add_lt(+x: U32, +y: U32) -> {U32.is_lt(U32.add(x, y), x) == carry32(x, y) : Bool}:
185 add_lt1(1n, {==}, x, y)
186
187def carry_v(+c: Bool) -> {UD.v(U.carry(c)) == S.bit_value(c) : Nat}:
188 match c:
189 case True{}:
190 {==}
191 case False{}:
192 {==}
193
194def add_hi(ahi: U32, bhi: U32, c: Bool) -> U32:
195 U32.add(U32.add(ahi, bhi), U.carry(c))
196
197def add_over(a: U.U64, b: U.U64) -> Nat:
198 match a b:
199 case U.U64{+alo, +ahi} U.U64{+blo, +bhi}:
200 Nat.add(S.bit_value(carry32(ahi, bhi)), S.bit_value(carry32(U32.add(ahi, bhi), U.carry(U32.is_lt(U32.add(alo, blo), alo)))))
201
202# the sum loses exactly 2^64 times the high carries
203def add_value(+a: U.U64, +b: U.U64) -> {Nat.add(val(U.add(a, b)), WD.sc(64n, add_over(a, b))) == Nat.add(val(a), val(b)) : Nat}:
204 match a b:
205 case U.U64{+alo, +ahi} U.U64{+blo, +bhi}:
206 +lo = U32.add(alo, blo)
207 +cb = U32.is_lt(lo, alo)
208 +t = U32.add(ahi, bhi)
209 +h = U32.add(t, U.carry(cb))
210 +c0 = S.bit_value(carry32(alo, blo))
211 +c1 = S.bit_value(carry32(ahi, bhi))
212 +c2 = S.bit_value(carry32(t, U.carry(cb)))
213 +f1 = add_cons(alo, blo)
214 +f2 = add_cons(ahi, bhi)
215 +f3 = Equal.trans(Nat, Nat.add(UD.v(h), WD.sc(32n, c2)), Nat.add(UD.v(t), UD.v(U.carry(cb))), Nat.add(UD.v(t), c0), add_cons(t, U.carry(cb)),
216 Equal.cong(Nat, Nat, z => Nat.add(UD.v(t), z), UD.v(U.carry(cb)), c0, Equal.trans(Nat, UD.v(U.carry(cb)), S.bit_value(cb), c0, carry_v(cb), Equal.cong(Bool, Nat, S.bit_value, cb, carry32(alo, blo), add_lt(alo, blo)))))
217 %Equal.sym(Nat, S.unsigned(64n, W.pack(lo, h)), Nat.add(UD.v(lo), WD.sc(32n, UD.v(h))), val_pack(lo, h)) : {Nat.add(_, WD.sc(64n, Nat.add(c1, c2))) == Nat.add(S.unsigned(64n, W.pack(alo, ahi)), S.unsigned(64n, W.pack(blo, bhi))) : Nat}
218 %Equal.sym(Nat, S.unsigned(64n, W.pack(alo, ahi)), Nat.add(UD.v(alo), WD.sc(32n, UD.v(ahi))), val_pack(alo, ahi)) : {Nat.add(Nat.add(UD.v(lo), WD.sc(32n, UD.v(h))), WD.sc(64n, Nat.add(c1, c2))) == Nat.add(_, S.unsigned(64n, W.pack(blo, bhi))) : Nat}
219 %Equal.sym(Nat, S.unsigned(64n, W.pack(blo, bhi)), Nat.add(UD.v(blo), WD.sc(32n, UD.v(bhi))), val_pack(blo, bhi)) : {Nat.add(Nat.add(UD.v(lo), WD.sc(32n, UD.v(h))), WD.sc(64n, Nat.add(c1, c2))) == Nat.add(Nat.add(UD.v(alo), WD.sc(32n, UD.v(ahi))), _) : Nat}
220 WD.add_alg(32n, UD.v(lo), UD.v(h), UD.v(t), c0, c1, c2, UD.v(alo), UD.v(ahi), UD.v(blo), UD.v(bhi), f1, f2, f3)
221
222# THEOREM: add is 64-bit wrapping addition.
223def add(+a: U.U64, +b: U.U64) -> {bits(U.add(a, b)) == Word.add(64n, bits(a), bits(b)) : Word(64n)}:
224 Equal.trans(Word(64n), bits(U.add(a, b)), S.from_nat(64n, Nat.add(val(a), val(b))), Word.add(64n, bits(a), bits(b)),
225 Equal.trans(Word(64n), bits(U.add(a, b)), S.from_nat(64n, Nat.add(val(U.add(a, b)), WD.sc(64n, add_over(a, b)))), S.from_nat(64n, Nat.add(val(a), val(b))),
226 Equal.sym(Word(64n), S.from_nat(64n, Nat.add(val(U.add(a, b)), WD.sc(64n, add_over(a, b)))), bits(U.add(a, b)), MA.reconstruct(64n, bits(U.add(a, b)), add_over(a, b))),
227 Equal.cong(Nat, Word(64n), z => S.from_nat(64n, z), Nat.add(val(U.add(a, b)), WD.sc(64n, add_over(a, b))), Nat.add(val(a), val(b)), add_value(a, b))),
228 Equal.sym(Word(64n), Word.add(64n, bits(a), bits(b)), S.from_nat(64n, Nat.add(val(a), val(b))), WA.refines(64n, bits(a), bits(b))))
229
230# ---- negation ----
231
232def inc_zero32(+x: Word(32n)) -> {U32.is_zero(U32{Word.inc(32n, x)}) == WD.ones(32n, x) : Bool}:
233 WD.inc_zero(32n, x)
234
235def add_carry(+xw: Word(32n), +c: Bool) -> {U32.add(U32{xw}, U.carry(c)) == U32{WD.incif(32n, c, xw)} : U32}:
236 match c:
237 case True{}:
238 Equal.cong(Word(32n), U32, w => U32{w}, Word.add(32n, xw, WD.one_word(31n)), Word.inc(32n, xw), WD.add_one(31n, xw))
239 case False{}:
240 A.add_zero(U32{xw})
241
242# THEOREM: neg is two's-complement negation.
243def neg(+a: U.U64) -> {bits(U.neg(a)) == Word.inc(64n, Word.not(64n, bits(a))) : Word(64n)}:
244 match a:
245 case U.U64{+lo, +hi}:
246 match lo hi:
247 case U32{+x} U32{+y}:
248 +nx = Word.not(32n, x)
249 +ny = Word.not(32n, y)
250 +j = W.join(32n, 32n, Word.inc(32n, nx), WD.incif(32n, WD.ones(32n, nx), ny))
251 +p1 = Equal.cong(U32, Word(64n), z => W.pack(U32{Word.inc(32n, nx)}, z), U32.add(U32{ny}, U.carry(U32.is_zero(U32{Word.inc(32n, nx)}))), U32{WD.incif(32n, WD.ones(32n, nx), ny)},
252 Equal.trans(U32, U32.add(U32{ny}, U.carry(U32.is_zero(U32{Word.inc(32n, nx)}))), U32.add(U32{ny}, U.carry(WD.ones(32n, nx))), U32{WD.incif(32n, WD.ones(32n, nx), ny)},
253 Equal.cong(Bool, U32, c => U32.add(U32{ny}, U.carry(c)), U32.is_zero(U32{Word.inc(32n, nx)}), WD.ones(32n, nx), inc_zero32(nx)),
254 add_carry(ny, WD.ones(32n, nx))))
255 +p2 = Equal.trans(Word(64n), Word.inc(64n, Word.not(64n, W.join(32n, 32n, x, y))), Word.inc(64n, W.join(32n, 32n, nx, ny)), j,
256 Equal.cong(Word(64n), Word(64n), w => Word.inc(64n, w), Word.not(64n, W.join(32n, 32n, x, y)), W.join(32n, 32n, nx, ny), WD.not_join(32n, 32n, x, y)),
257 WD.inc_join(32n, 32n, nx, ny))
258 Equal.trans(Word(64n), bits(U.neg(U.U64{U32{x}, U32{y}})), j, Word.inc(64n, Word.not(64n, W.join(32n, 32n, x, y))), p1, Equal.sym(Word(64n), Word.inc(64n, Word.not(64n, W.join(32n, 32n, x, y))), j, p2))