~/jendhub

proofs/math/u64/u64.bend

bend-collections-laws-crypto@1.0.0.0 · 258 lines · 31 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/spec/math/u64.bend as SU
3import bend-collections-laws-crypto@1.0.0.0/src/math/u64.bend as U
4import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/src/wide.bend as W
5import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S
6import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
7import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
8import bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32.bend as U3
9import bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32alg.bend as A
10import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/numeric.bend as NUM
11import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/addition.bend as AD
12import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/modular_addition.bend as MA
13import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/word_addition.bend as WA
14import bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend as WD
15import bend-collections-laws-crypto@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))