1	import Base
2	import ../../../spec/lib/common.bend as C
3	import ../../../spec/crypto/poly1305.bend as R
4	import ../../lib/lemmas/proofs/nat_algebra.bend as NA
5	import ../../math/natural/arith.bend as NR
6	import ./modp.bend as MP
7	import ./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.
17	def 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	
22	def 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)
26	law 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	
34	def 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)
45	law 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	
51	def 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.
62	law 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	
69	def 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	
77	def 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.
91	law 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	
100	def 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.
115	law 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	
122	def 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))))))