proofs/crypto/poly1305/poly.bend

bend-collections-laws-crypto@1.0.0.0 · 128 lines · 8 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/lemmas/proofs/nat_algebra.bend as NA
5import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend as NR
6import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/poly1305/modp.bend as MP
7import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/poly1305/mac.bend as M
8
9# The accumulator of spec/crypto/poly1305.bend (reduced mod p after every
10# block) is the polynomial of the blocks evaluated at r, reduced once:
11#   absorb(bs, r, 0) == poly(bs, r) mod (2^130 - 5)
12# (Horner's rule, then "reduction commutes with + and *", Mathlib's
13# Nat.add_mod / Nat.mul_mod; the modulus is written 1 + bp throughout, with
14# 1 + bp == 2^130 - 5 from modp.bend).
15
16# Horner's rule without reduction.
17def horner(bs: List<&2, List<&2, U32>>, +r: Nat, a: Nat) -> Nat:
18  match bs:
19    case Nil{}: a
20    case b <> rest: horner(rest, r, Nat.mul(r, Nat.add(a, R.coeff(b))))
21
22def len(+bs: List<&2, List<&2, U32>>) -> Nat:
23  List.length(&2, List<&2, U32>, bs)
24
25# (r (a + n)) X == a (r X) + n (r X)
26law step_alg:
27  for +r: Nat
28  for +a: Nat
29  for +n: Nat
30  for +x: Nat
31  for +p: Nat
32  {Nat.add(Nat.mul(Nat.mul(r, Nat.add(a, n)), x), p) == Nat.add(Nat.mul(a, Nat.mul(r, x)), Nat.add(Nat.mul(n, Nat.mul(r, x)), p)) : Nat}
33
34def step_alg(r, a, n, x, p):
35  +RX = Nat.mul(r, x)
36  +e1 = Equal.trans(Nat, Nat.mul(Nat.mul(r, Nat.add(a, n)), x), Nat.mul(Nat.mul(Nat.add(a, n), r), x), Nat.mul(Nat.add(a, n), RX),
37    Equal.cong(Nat, Nat, z => Nat.mul(z, x), Nat.mul(r, Nat.add(a, n)), Nat.mul(Nat.add(a, n), r), NA.mul_comm(r, Nat.add(a, n))),
38    NA.mul_assoc(Nat.add(a, n), r, x))
39  +e2 = Equal.trans(Nat, Nat.mul(Nat.mul(r, Nat.add(a, n)), x), Nat.mul(Nat.add(a, n), RX), Nat.add(Nat.mul(a, RX), Nat.mul(n, RX)), e1, NA.mul_add_right(a, n, RX))
40  Equal.trans(Nat, Nat.add(Nat.mul(Nat.mul(r, Nat.add(a, n)), x), p), Nat.add(Nat.add(Nat.mul(a, RX), Nat.mul(n, RX)), p), Nat.add(Nat.mul(a, RX), Nat.add(Nat.mul(n, RX), p)),
41    Equal.cong(Nat, Nat, z => Nat.add(z, p), Nat.mul(Nat.mul(r, Nat.add(a, n)), x), Nat.add(Nat.mul(a, RX), Nat.mul(n, RX)), e2),
42    NA.add_assoc(Nat.mul(a, RX), Nat.mul(n, RX), p))
43
44# horner(bs, r, a) == a r^q + poly(bs, r)
45law horner_poly:
46  for +bs: List<&2, List<&2, U32>>
47  for +r: Nat
48  for +a: Nat
49  {horner(bs, r, a) == Nat.add(Nat.mul(a, Nat.pow(r, len(bs))), R.poly(bs, r)) : Nat}
50
51def horner_poly(bs, r, a):
52  match bs:
53    case Nil{}:
54      Equal.sym(Nat, Nat.add(Nat.mul(a, 1n), 0n), a, Equal.trans(Nat, Nat.add(Nat.mul(a, 1n), 0n), Nat.mul(a, 1n), a, NA.add_zero(Nat.mul(a, 1n)), NA.mul_one(a)))
55    case b <> rest:
56      +x = Nat.mul(r, Nat.add(a, R.coeff(b)))
57      Equal.trans(Nat, horner(rest, r, x), Nat.add(Nat.mul(x, Nat.pow(r, len(rest))), R.poly(rest, r)), Nat.add(Nat.mul(a, Nat.mul(r, Nat.pow(r, len(rest)))), Nat.add(Nat.mul(R.coeff(b), Nat.mul(r, Nat.pow(r, len(rest)))), R.poly(rest, r))),
58        horner_poly(rest, r, x),
59        step_alg(r, a, R.coeff(b), Nat.pow(r, len(rest)), R.poly(rest, r)))
60
61# horner only depends on its start value mod n.
62law horner_mod:
63  for +bp: Nat
64  for +bs: List<&2, List<&2, U32>>
65  for +r: Nat
66  for +x: Nat
67  {Nat.mod(horner(bs, r, Nat.mod(x, 1n+bp)), 1n+bp) == Nat.mod(horner(bs, r, x), 1n+bp) : Nat}
68
69def next_mod(+bp: Nat, +r: Nat, +x: Nat, +n: Nat) -> {Nat.mod(Nat.mul(r, Nat.add(Nat.mod(x, 1n+bp), n)), 1n+bp) == Nat.mod(Nat.mul(r, Nat.add(x, n)), 1n+bp) : Nat}:
70  +m = {1n+bp : Nat}
71  Equal.trans(Nat, Nat.mod(Nat.mul(r, Nat.add(Nat.mod(x, m), n)), m), Nat.mod(Nat.mul(r, Nat.mod(Nat.add(Nat.mod(x, m), n), m)), m), Nat.mod(Nat.mul(r, Nat.add(x, n)), m),
72    Equal.sym(Nat, Nat.mod(Nat.mul(r, Nat.mod(Nat.add(Nat.mod(x, m), n), m)), m), Nat.mod(Nat.mul(r, Nat.add(Nat.mod(x, m), n)), m), NR.mod_mul_r(bp, r, Nat.add(Nat.mod(x, m), n))),
73    Equal.trans(Nat, Nat.mod(Nat.mul(r, Nat.mod(Nat.add(Nat.mod(x, m), n), m)), m), Nat.mod(Nat.mul(r, Nat.mod(Nat.add(x, n), m)), m), Nat.mod(Nat.mul(r, Nat.add(x, n)), m),
74      Equal.cong(Nat, Nat, z => Nat.mod(Nat.mul(r, z), m), Nat.mod(Nat.add(Nat.mod(x, m), n), m), Nat.mod(Nat.add(x, n), m), NR.mod_add_l(bp, x, n)),
75      NR.mod_mul_r(bp, r, Nat.add(x, n))))
76
77def horner_mod(bp, bs, r, x):
78  match bs:
79    case Nil{}: NR.mod_mod(bp, x)
80    case b <> rest:
81      +m = {1n+bp : Nat}
82      +y1 = Nat.mul(r, Nat.add(Nat.mod(x, m), R.coeff(b)))
83      +y2 = Nat.mul(r, Nat.add(x, R.coeff(b)))
84      Equal.trans(Nat, Nat.mod(horner(rest, r, y1), m), Nat.mod(horner(rest, r, Nat.mod(y1, m)), m), Nat.mod(horner(rest, r, y2), m),
85        Equal.sym(Nat, Nat.mod(horner(rest, r, Nat.mod(y1, m)), m), Nat.mod(horner(rest, r, y1), m), horner_mod(bp, rest, r, y1)),
86        Equal.trans(Nat, Nat.mod(horner(rest, r, Nat.mod(y1, m)), m), Nat.mod(horner(rest, r, Nat.mod(y2, m)), m), Nat.mod(horner(rest, r, y2), m),
87          Equal.cong(Nat, Nat, z => Nat.mod(horner(rest, r, z), m), Nat.mod(y1, m), Nat.mod(y2, m), next_mod(bp, r, x, R.coeff(b))),
88          horner_mod(bp, rest, r, y2)))
89
90# absorb(bs, r, a) == horner(bs, r, a) mod p, for a < p.
91law absorb_horner:
92  for +one: Nat
93  for +h1: {one == 1n : Nat}
94  for +bs: List<&2, List<&2, U32>>
95  for +r: Nat
96  for +a: Nat
97  for +ha: {Nat.is_lt(a, 1n+M.bpv(one)) == True{} : Bool}
98  {R.absorb(bs, r, a) == Nat.mod(horner(bs, r, a), 1n+M.bpv(one)) : Nat}
99
100def absorb_horner(one, h1, bs, r, a, ha):
101  match bs:
102    case Nil{}: Equal.sym(Nat, Nat.mod(a, 1n+M.bpv(one)), a, NR.mod_of(0n, M.bpv(one), a, ha))
103    case b <> rest:
104      +bp = M.bpv(one)
105      +m = {1n+bp : Nat}
106      +y = Nat.mul(r, Nat.add(a, R.coeff(b)))
107      +em = MP.modp_mod(one, h1, bp, M.bp5(one, h1), y)
108      Equal.trans(Nat, R.absorb(rest, r, R.modp(y)), R.absorb(rest, r, Nat.mod(y, m)), Nat.mod(horner(rest, r, y), m),
109        Equal.cong(Nat, Nat, z => R.absorb(rest, r, z), R.modp(y), Nat.mod(y, m), em),
110        Equal.trans(Nat, R.absorb(rest, r, Nat.mod(y, m)), Nat.mod(horner(rest, r, Nat.mod(y, m)), m), Nat.mod(horner(rest, r, y), m),
111          absorb_horner(one, h1, rest, r, Nat.mod(y, m), NR.dm_lt(bp, y)),
112          horner_mod(bp, rest, r, y)))
113
114# The accumulator is the polynomial at r, reduced mod 2^130 - 5.
115law absorb_poly:
116  for +one: Nat
117  for +h1: {one == 1n : Nat}
118  for +bs: List<&2, List<&2, U32>>
119  for +r: Nat
120  {R.absorb(bs, r, 0n) == Nat.mod(R.poly(bs, r), Nat.sub(C.shift(130n, one), 5n)) : Nat}
121
122def absorb_poly(one, h1, bs, r):
123  +m = {1n+M.bpv(one) : Nat}
124  Equal.trans(Nat, R.absorb(bs, r, 0n), Nat.mod(horner(bs, r, 0n), m), Nat.mod(R.poly(bs, r), Nat.sub(C.shift(130n, one), 5n)),
125    absorb_horner(one, h1, bs, r, 0n, {==}),
126    Equal.trans(Nat, Nat.mod(horner(bs, r, 0n), m), Nat.mod(R.poly(bs, r), m), Nat.mod(R.poly(bs, r), Nat.sub(C.shift(130n, one), 5n)),
127      Equal.cong(Nat, Nat, z => Nat.mod(z, m), horner(bs, r, 0n), R.poly(bs, r), horner_poly(bs, r, 0n)),
128      Equal.cong(Nat, Nat, z => Nat.mod(R.poly(bs, r), z), m, Nat.sub(C.shift(130n, one), 5n), Equal.sym(Nat, Nat.sub(C.shift(130n, one), 5n), m, M.pp_eq(one, h1, M.bpv(one), M.bp5(one, h1))))))