1	import Base
2	import ../../../spec/lib/common.bend as C
3	import ../../../spec/crypto/poly1305.bend as R
4	import ../../lib/nat.bend as N
5	import ../../lib/logic.bend as L
6	import ../../lib/arith.bend as AR
7	import ../../lib/u32alg.bend as UA
8	import ../../lib/lemmas/proofs/nat_algebra.bend as NA
9	import ../../math/typed/width.bend as WW
10	import ../../math/typed/w64mul.bend as WM
11	import ../../math/typed/w64sh.bend as SH
12	import ../../math/natural/arith.bend as NR
13	import ./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	
19	law 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	
27	def 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)
34	law 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	
42	def 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	
50	law 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	
58	def 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	
65	law 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	
74	def 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
80	def 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	
101	law 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	
111	def 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
117	def 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	
161	law 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	
170	def 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
176	law 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	
184	def 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))