proofs/crypto/poly1305/modp.bend

bend-collections-laws-crypto@1.0.0.0 · 189 lines · 9 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
3import bend-collections-laws-crypto@1.0.0.0/spec/crypto/poly1305.bend as R
4import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
5import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
6import bend-collections-laws-crypto@1.0.0.0/proofs/lib/arith.bend as AR
7import bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32alg.bend as UA
8import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
9import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/width.bend as WW
10import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64mul.bend as WM
11import bend-collections-laws-crypto@1.0.0.0/proofs/math/typed/w64sh.bend as SH
12import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend as NR
13import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/poly1305/arith.bend as A
14
15# spec/crypto/poly1305.bend's modp(x) is x mod p. The modulus is written
16# 1 + bp with 1 + bp + 5 == 2^130 == C.shift(130n, one), one == 1 (the checker
17# expands a closed 2^130 in unary, so neither is ever closed).
18
19law bigp:
20  for +one: Nat
21  for +h1: {one == 1n : Nat}
22  for +bp: Nat
23  for +h5: {Nat.add(1n+bp, 5n) == C.shift(130n, one) : Nat}
24  for +x: Nat
25  {C.shift(130n, x) == Nat.add(Nat.mul(x, 1n+bp), Nat.mul(x, 5n)) : Nat}
26
27def bigp(one, h1, bp, h5, x):
28  A.tr(C.shift(130n, x), Nat.mul(x, C.shift(130n, one)), Nat.add(Nat.mul(x, 1n+bp), Nat.mul(x, 5n)), WW.shift_mul_one(130n, one, h1, x),
29    A.tr(Nat.mul(x, C.shift(130n, one)), Nat.mul(x, Nat.add(1n+bp, 5n)), Nat.add(Nat.mul(x, 1n+bp), Nat.mul(x, 5n)),
30      Equal.cong(Nat, Nat, t => Nat.mul(x, t), C.shift(130n, one), Nat.add(1n+bp, 5n), A.sy(Nat.add(1n+bp, 5n), C.shift(130n, one), h5)),
31      NA.mul_add_left(x, 1n+bp, 5n)))
32
33# x == hi p + fold(x)
34law fold_eq:
35  for +one: Nat
36  for +h1: {one == 1n : Nat}
37  for +bp: Nat
38  for +h5: {Nat.add(1n+bp, 5n) == C.shift(130n, one) : Nat}
39  for +x: Nat
40  {x == Nat.add(Nat.mul(C.high(130n, x), 1n+bp), R.fold(x)) : Nat}
41
42def fold_eq(one, h1, bp, h5, x):
43  +lo = C.low(130n, x)
44  +hi = C.high(130n, x)
45  A.tr(x, Nat.add(lo, C.shift(130n, hi)), Nat.add(Nat.mul(hi, 1n+bp), Nat.add(lo, Nat.mul(hi, 5n))), WW.low_high(130n, x),
46    A.tr(Nat.add(lo, C.shift(130n, hi)), Nat.add(lo, Nat.add(Nat.mul(hi, 1n+bp), Nat.mul(hi, 5n))), Nat.add(Nat.mul(hi, 1n+bp), Nat.add(lo, Nat.mul(hi, 5n))),
47      WM.cong_r(lo, C.shift(130n, hi), Nat.add(Nat.mul(hi, 1n+bp), Nat.mul(hi, 5n)), bigp(one, h1, bp, h5, hi)),
48      NA.add_swap(lo, Nat.mul(hi, 1n+bp), Nat.mul(hi, 5n))))
49
50law fold_mod:
51  for +one: Nat
52  for +h1: {one == 1n : Nat}
53  for +bp: Nat
54  for +h5: {Nat.add(1n+bp, 5n) == C.shift(130n, one) : Nat}
55  for +x: Nat
56  {Nat.mod(R.fold(x), 1n+bp) == Nat.mod(x, 1n+bp) : Nat}
57
58def fold_mod(one, h1, bp, h5, x):
59  +hi = C.high(130n, x)
60  A.sy(Nat.mod(x, 1n+bp), Nat.mod(R.fold(x), 1n+bp),
61    A.tr(Nat.mod(x, 1n+bp), Nat.mod(Nat.add(Nat.mul(hi, 1n+bp), R.fold(x)), 1n+bp), Nat.mod(R.fold(x), 1n+bp),
62      Equal.cong(Nat, Nat, t => Nat.mod(t, 1n+bp), x, Nat.add(Nat.mul(hi, 1n+bp), R.fold(x)), fold_eq(one, h1, bp, h5, x)),
63      NR.absorb(bp, hi, R.fold(x))))
64
65law folds_mod:
66  for +one: Nat
67  for +h1: {one == 1n : Nat}
68  for +bp: Nat
69  for +h5: {Nat.add(1n+bp, 5n) == C.shift(130n, one) : Nat}
70  for +n: Nat
71  for +x: Nat
72  {Nat.mod(R.folds(n, x), 1n+bp) == Nat.mod(x, 1n+bp) : Nat}
73
74def folds_mod(one, h1, bp, h5, n, x):
75  match n:
76    case 0n: {==}
77    case 1n+k: A.tr(Nat.mod(R.folds(k, R.fold(x)), 1n+bp), Nat.mod(R.fold(x), 1n+bp), Nat.mod(x, 1n+bp), folds_mod(one, h1, bp, h5, k, R.fold(x)), fold_mod(one, h1, bp, h5, x))
78
79# a fold on x < k + 1 + 2^130 gives a value below k + 2^130
80def fold_lt_c(+one: Nat, +h1: {one == 1n : Nat}, +bp: Nat, +h5: {Nat.add(1n+bp, 5n) == C.shift(130n, one) : Nat}, +k: Nat, +x: Nat, +h: {Nat.is_lt(x, Nat.add(1n+k, C.shift(130n, one))) == True{} : Bool}, +c: Bool, +hc: {Nat.is_eq(C.high(130n, x), 0n) == c : Bool}) -> {Nat.is_lt(R.fold(x), Nat.add(k, C.shift(130n, one))) == True{} : Bool}:
81  match c:
82    case True{}:
83      +s = C.shift(130n, one)
84      +hi = C.high(130n, x)
85      +lo = C.low(130n, x)
86      +h0 = N.eq_from_is_eq(hi, 0n, hc)
87      +ef = A.tr(R.fold(x), Nat.add(lo, Nat.mul(0n, 5n)), x, WM.cong_r(lo, Nat.mul(hi, 5n), Nat.mul(0n, 5n), Equal.cong(Nat, Nat, t => Nat.mul(t, 5n), hi, 0n, h0)),
88        A.tr(Nat.add(lo, 0n), lo, x, N.add_zero(lo), WW.low_fit(130n, x, hc)))
89      A.lt_substl(x, R.fold(x), Nat.add(k, s), A.sy(R.fold(x), x, ef), N.lt_le_trans(x, s, Nat.add(k, s), WW.lt_one(130n, one, h1, x, hc), A.le_add_l(k, s)))
90    case False{}:
91      +s = C.shift(130n, one)
92      +hi = C.high(130n, x)
93      +lo = C.low(130n, x)
94      +f = R.fold(x)
95      +hp = Nat.mul(hi, 1n+bp)
96      +h1h = N.lt_succ_le_succ(0n, hi, N.lt_or_eq(0n, hi, N.zero_le(hi), N.is_eq_sym_false(hi, 0n, hc)))
97      +hp1b = A.le_substl(Nat.mul(1n, 1n+bp), 1n+bp, hp, AR.one_mul(1n+bp), AR.mul_le(1n, hi, 1n+bp, h1h))
98      +lx = A.le_subst(1n+f, Nat.add(hp, f), x, A.sy(x, Nat.add(hp, f), fold_eq(one, h1, bp, h5, x)), WW.le_add_r(1n, hp, f, N.le_trans(1n, 1n+bp, hp, N.zero_le(bp), hp1b)))
99      N.lt_le_trans(f, x, Nat.add(k, s), N.succ_le_lt(f, x, lx), N.lt_succ_le(x, Nat.add(k, s), h))
100
101law folds_fit:
102  for +one: Nat
103  for +h1: {one == 1n : Nat}
104  for +bp: Nat
105  for +h5: {Nat.add(1n+bp, 5n) == C.shift(130n, one) : Nat}
106  for +n: Nat
107  for +x: Nat
108  for +h: {Nat.is_lt(x, Nat.add(n, C.shift(130n, one))) == True{} : Bool}
109  {C.fits(130n, R.folds(n, x)) == True{} : Bool}
110
111def folds_fit(one, h1, bp, h5, n, x, h):
112  match n:
113    case 0n: WW.fits_one(130n, one, h1, x, h)
114    case 1n+k: folds_fit(one, h1, bp, h5, k, R.fold(x), fold_lt_c(one, h1, bp, h5, k, x, h, Nat.is_eq(C.high(130n, x), 0n), {==}))
115
116# y < 2^130: canon(y) == y mod p
117def canon_c(+one: Nat, +h1: {one == 1n : Nat}, +bp: Nat, +h5: {Nat.add(1n+bp, 5n) == C.shift(130n, one) : Nat}, +y: Nat, +hy: {C.fits(130n, y) == True{} : Bool}, +b: Bool, +hb: {C.fits(130n, Nat.add(y, 5n)) == b : Bool}) -> {R.pick(b, y, C.low(130n, Nat.add(y, 5n))) == Nat.mod(y, 1n+bp) : Nat}:
118  match b:
119    case True{}:
120      +s = C.shift(130n, one)
121      +pp = {1n+bp : Nat}
122      +l1 = A.lt_subst(Nat.add(y, 5n), s, Nat.add(pp, 5n), A.sy(Nat.add(pp, 5n), s, h5), WW.lt_one(130n, one, h1, Nat.add(y, 5n), hb))
123      +l2 = A.btrue(Nat.is_lt(y, pp), Nat.is_lt(Nat.add(y, 5n), Nat.add(pp, 5n)), Equal.sym(Bool, Nat.is_lt(Nat.add(y, 5n), Nat.add(pp, 5n)), Nat.is_lt(y, pp), WW.lt_cancel_r(y, pp, 5n)), l1)
124      A.sy(Nat.mod(y, pp), y, NR.mod_of(0n, bp, y, l2))
125    case False{}:
126      +s = C.shift(130n, one)
127      +pp = {1n+bp : Nat}
128      +x = Nat.add(y, 5n)
129      +lo = C.low(130n, x)
130      +hi = C.high(130n, x)
131      # 5 <= 2^130 and 16 <= 2^130
132      +h16 = N.le_trans(16n, C.shift(4n, one), s, L.subst(Nat, z => {Nat.is_le(16n, C.shift(4n, z)) == True{} : Bool}, 1n, one, A.sy(one, 1n, h1), {==}), WW.shift_ge(126n, C.shift(4n, one)))
133      +ly = WW.lt_one(130n, one, h1, y, hy)
134      +lx = A.lt_add2(y, 5n, s, s, ly, N.lt_le_trans(5n, 16n, s, {==}, h16))
135      +f131 = WW.fits_one(131n, one, h1, x, A.lt_subst(x, Nat.add(s, s), Nat.double(s), A.sy(Nat.double(s), Nat.add(s, s), NA.double_self(s)), lx))
136      +h2 = WW.lt_of_fits(1n, hi, SH.fits_high(130n, 1n, x, f131))
137      +hne = N.is_eq_sym_false(hi, 0n, hb)
138      +h1h = N.lt_succ_le_succ(0n, hi, N.lt_or_eq(0n, hi, N.zero_le(hi), hne))
139      +ehi = N.le_antisym(hi, 1n, N.lt_succ_le(hi, 1n, h2), h1h)
140      # x == lo + 2^130 hi == lo + s
141      +ex = A.tr(x, Nat.add(lo, C.shift(130n, hi)), Nat.add(lo, s), WW.low_high(130n, x),
142        WM.cong_r(lo, C.shift(130n, hi), s, A.tr(C.shift(130n, hi), Nat.mul(hi, s), s, WW.shift_mul_one(130n, one, h1, hi),
143          A.tr(Nat.mul(hi, s), Nat.mul(1n, s), s, Equal.cong(Nat, Nat, t => Nat.mul(t, s), hi, 1n, ehi), AR.one_mul(s)))))
144      # y == lo + p
145      +e2 = A.tr(Nat.add(y, 5n), Nat.add(lo, Nat.add(pp, 5n)), Nat.add(Nat.add(lo, pp), 5n),
146        A.tr(Nat.add(y, 5n), Nat.add(lo, s), Nat.add(lo, Nat.add(pp, 5n)), ex, WM.cong_r(lo, s, Nat.add(pp, 5n), A.sy(Nat.add(pp, 5n), s, h5))),
147        A.sy(Nat.add(Nat.add(lo, pp), 5n), Nat.add(lo, Nat.add(pp, 5n)), N.add_assoc(lo, pp, 5n)))
148      +ey = UA.add_cancel_r(y, Nat.add(lo, pp), 5n, e2)
149      # lo < 5 <= p
150      +l5a = A.lt_subst(Nat.add(lo, s), Nat.add(s, 5n), Nat.add(5n, s), N.add_comm(s, 5n), A.lt_substl(Nat.add(y, 5n), Nat.add(lo, s), Nat.add(s, 5n), ex, N.lt_add_r2(y, s, 5n, ly)))
151      +l5b = A.btrue(Nat.is_lt(lo, 5n), Nat.is_lt(Nat.add(lo, s), Nat.add(5n, s)), Equal.sym(Bool, Nat.is_lt(Nat.add(lo, s), Nat.add(5n, s)), Nat.is_lt(lo, 5n), WW.lt_cancel_r(lo, 5n, s)), l5a)
152      +h10 = A.le_subst(10n, s, Nat.add(pp, 5n), A.sy(Nat.add(pp, 5n), s, h5), N.le_trans(10n, 16n, s, {==}, h16))
153      +h9 = N.succ_le_lt(9n, Nat.add(pp, 5n), h10)
154      +h4 = A.btrue(Nat.is_lt(4n, pp), Nat.is_lt(Nat.add(4n, 5n), Nat.add(pp, 5n)), Equal.sym(Bool, Nat.is_lt(Nat.add(4n, 5n), Nat.add(pp, 5n)), Nat.is_lt(4n, pp), WW.lt_cancel_r(4n, pp, 5n)), h9)
155      +hp5 = N.lt_succ_le_succ(4n, pp, h4)
156      +llo = N.lt_le_trans(lo, 5n, pp, l5b, hp5)
157      A.sy(Nat.mod(y, pp), lo, A.tr(Nat.mod(y, pp), Nat.mod(Nat.add(Nat.mul(1n, pp), lo), pp), lo,
158        Equal.cong(Nat, Nat, t => Nat.mod(t, pp), y, Nat.add(Nat.mul(1n, pp), lo), A.tr(y, Nat.add(lo, pp), Nat.add(Nat.mul(1n, pp), lo), ey, A.tr(Nat.add(lo, pp), Nat.add(pp, lo), Nat.add(Nat.mul(1n, pp), lo), N.add_comm(lo, pp), WM.cong_l(pp, Nat.mul(1n, pp), lo, A.sy(Nat.mul(1n, pp), pp, AR.one_mul(pp)))))),
159        NR.mod_of(1n, bp, lo, llo)))
160
161law canon_mod:
162  for +one: Nat
163  for +h1: {one == 1n : Nat}
164  for +bp: Nat
165  for +h5: {Nat.add(1n+bp, 5n) == C.shift(130n, one) : Nat}
166  for +y: Nat
167  for +hy: {C.fits(130n, y) == True{} : Bool}
168  {R.canon(y) == Nat.mod(y, 1n+bp) : Nat}
169
170def canon_mod(one, h1, bp, h5, y, hy):
171  match y:
172    case 0n: {==}
173    case 1n+z: canon_c(one, h1, bp, h5, 1n+z, hy, C.fits(130n, Nat.add(1n+z, 5n)), {==})
174
175# modp(x) is x mod p, for every x
176law modp_mod:
177  for +one: Nat
178  for +h1: {one == 1n : Nat}
179  for +bp: Nat
180  for +h5: {Nat.add(1n+bp, 5n) == C.shift(130n, one) : Nat}
181  for +x: Nat
182  {R.modp(x) == Nat.mod(x, 1n+bp) : Nat}
183
184def modp_mod(one, h1, bp, h5, x):
185  +s = C.shift(130n, one)
186  +hs = N.succ_le_lt(0n, s, A.one_le_shift(130n, one, h1))
187  +hx = A.lt_substl(Nat.add(x, 0n), x, Nat.add(x, s), N.add_zero(x), N.lt_add_left(0n, s, x, hs))
188  +y = R.folds(x, x)
189  A.tr(R.canon(y), Nat.mod(y, 1n+bp), Nat.mod(x, 1n+bp), canon_mod(one, h1, bp, h5, y, folds_fit(one, h1, bp, h5, x, x, hx)), folds_mod(one, h1, bp, h5, x, x))