1	import Base
2	import ../../../spec/crypto/curve25519/field.bend as FS
3	import ../../../src/crypto/curve25519/field.bend as F
4	import ../../lib/nat.bend as N
5	import ../../lib/logic.bend as L
6	import ../../lib/word.bend as WD
7	import ../../lib/lemmas/proofs/nat_algebra.bend as NA
8	import ../../math/natural/arith.bend as NR
9	import ./limbs.bend as LM
10	import ./fieldops.bend as FO
11	import ./canon.bend as CN
12	import ./cong.bend as G
13	
14	# F.eq(a, b) = is_zero(sub(a, b)) decides a == b mod p. With A, B the
15	# reduced values, w = (A + p) - B is in [1, 2p), and w mod p == 0 iff w == p
16	# iff A == B.
17	
18	def pw(+pp: Nat, +A: Nat, +B: Nat) -> Nat:
19	  Nat.sub(Nat.add(A, 1n+pp), B)
20	
21	def w_eq(+pp: Nat, +A: Nat, +B: Nat, +hB: {Nat.is_lt(B, 1n+pp) == True{} : Bool}) -> {Nat.add(pw(pp, A, B), B) == Nat.add(A, 1n+pp) : Nat}:
22	  +P = {1n+pp : Nat}
23	  +le = N.le_trans(B, P, Nat.add(A, P), N.lt_le(B, P, hB), G.le_add_l(A, P))
24	  Equal.trans(Nat, Nat.add(pw(pp, A, B), B), Nat.add(B, pw(pp, A, B)), Nat.add(A, P), NA.add_comm(pw(pp, A, B), B), N.sub_add(Nat.add(A, P), B, le))
25	
26	def w_zero(+pp: Nat, +A: Nat, +B: Nat, +hB: {Nat.is_lt(B, 1n+pp) == True{} : Bool}, +e: {A == B : Nat}) -> {Nat.mod(pw(pp, A, B), 1n+pp) == 0n : Nat}:
27	  +P = {1n+pp : Nat}
28	  +w = pw(pp, A, B)
29	  +e2 = L.subst(Nat, z => {Nat.add(w, z) == Nat.add(A, P) : Nat}, B, A, Equal.sym(Nat, A, B, e), w_eq(pp, A, B, hB))
30	  +e3 = NR.add_cancel(A, w, P, Equal.trans(Nat, Nat.add(A, w), Nat.add(w, A), Nat.add(A, P), NA.add_comm(A, w), e2))
31	  +e4 = Equal.trans(Nat, P, Nat.mul(1n, P), Nat.add(Nat.mul(1n, P), 0n), Equal.sym(Nat, Nat.mul(1n, P), P, NA.add_zero(P)), Equal.sym(Nat, Nat.add(Nat.mul(1n, P), 0n), Nat.mul(1n, P), N.add_zero(Nat.mul(1n, P))))
32	  Equal.trans(Nat, Nat.mod(w, P), Nat.mod(Nat.add(Nat.mul(1n, P), 0n), P), 0n, G.c_eq(pp, w, Nat.add(Nat.mul(1n, P), 0n), Equal.trans(Nat, w, P, Nat.add(Nat.mul(1n, P), 0n), e3, e4)), NR.mod_of(1n, pp, 0n, {==}))
33	
34	# w mod p == 0 gives A == B: the quotient q has w == q p, and q is 1
35	def q_one(+pp: Nat, +A: Nat, +B: Nat, +q: Nat, +hA: {Nat.is_lt(A, 1n+pp) == True{} : Bool}, +hB: {Nat.is_lt(B, 1n+pp) == True{} : Bool}, +hw: {Nat.add(Nat.mul(q, 1n+pp), B) == Nat.add(A, 1n+pp) : Nat}) -> {A == B : Nat}:
36	  match q:
37	    case 0n:
38	      +P = {1n+pp : Nat}
39	      +c = L.subst(Nat, z => {Nat.is_le(P, z) == True{} : Bool}, Nat.add(A, P), B, Equal.sym(Nat, B, Nat.add(A, P), hw), G.le_add_l(A, P))
40	      Empty.absurd({A == B : Nat}, L.true_not_false(Nat.is_lt(B, P), hB, N.le_not_lt(B, P, c)))
41	    case 1n:
42	      +P = {1n+pp : Nat}
43	      +h2 = Equal.trans(Nat, Nat.add(P, B), Nat.add(Nat.mul(1n, P), B), Nat.add(A, P), Equal.cong(Nat, Nat, z => Nat.add(z, B), P, Nat.mul(1n, P), Equal.sym(Nat, Nat.mul(1n, P), P, NA.add_zero(P))), hw)
44	      NR.add_cancel(P, A, B, Equal.sym(Nat, Nat.add(P, B), Nat.add(P, A), Equal.trans(Nat, Nat.add(P, B), Nat.add(A, P), Nat.add(P, A), h2, NA.add_comm(A, P))))
45	    case 2n+ +r:
46	      +P = {1n+pp : Nat}
47	      +big = Nat.add(P, Nat.add(P, Nat.add(Nat.mul(r, P), B)))
48	      +h2 = Equal.trans(Nat, big, Nat.add(Nat.mul(2n+r, P), B), Nat.add(A, P), Equal.sym(Nat, Nat.add(Nat.mul(2n+r, P), B), big, Equal.trans(Nat, Nat.add(Nat.add(P, Nat.add(P, Nat.mul(r, P))), B), Nat.add(P, Nat.add(Nat.add(P, Nat.mul(r, P)), B)), big, NA.add_assoc(P, Nat.add(P, Nat.mul(r, P)), B), Equal.cong(Nat, Nat, z => Nat.add(P, z), Nat.add(Nat.add(P, Nat.mul(r, P)), B), Nat.add(P, Nat.add(Nat.mul(r, P), B)), NA.add_assoc(P, Nat.mul(r, P), B)))), hw)
49	      +l1 = N.le_add_left(P, Nat.add(P, Nat.add(Nat.mul(r, P), B)), P, N.le_add_right(P, Nat.add(Nat.mul(r, P), B)))
50	      +l2 = L.subst(Nat, z => {Nat.is_le(Nat.add(P, P), z) == True{} : Bool}, big, Nat.add(A, P), h2, l1)
51	      +l3 = N.lt_le_trans(Nat.add(A, P), Nat.add(P, P), Nat.add(A, P), N.lt_add_r2(A, P, P, hA), l2)
52	      Empty.absurd({A == B : Nat}, L.true_not_false(Nat.is_lt(Nat.add(A, P), Nat.add(A, P)), l3, N.lt_irrefl(Nat.add(A, P))))
53	
54	def w_ne(+pp: Nat, +A: Nat, +B: Nat, +hA: {Nat.is_lt(A, 1n+pp) == True{} : Bool}, +hB: {Nat.is_lt(B, 1n+pp) == True{} : Bool}, +h: {Nat.mod(pw(pp, A, B), 1n+pp) == 0n : Nat}) -> {A == B : Nat}:
55	  +P = {1n+pp : Nat}
56	  +w = pw(pp, A, B)
57	  +q = Nat.div(w, P)
58	  +e1 = NR.dm_eq(pp, w)
59	  +e2 = Equal.trans(Nat, w, Nat.add(Nat.mul(q, P), Nat.mod(w, P)), Nat.add(Nat.mul(q, P), 0n), e1, Equal.cong(Nat, Nat, z => Nat.add(Nat.mul(q, P), z), Nat.mod(w, P), 0n, h))
60	  +e3 = Equal.trans(Nat, w, Nat.add(Nat.mul(q, P), 0n), Nat.mul(q, P), e2, N.add_zero(Nat.mul(q, P)))
61	  +e4 = Equal.trans(Nat, Nat.add(Nat.mul(q, P), B), Nat.add(w, B), Nat.add(A, P), Equal.cong(Nat, Nat, z => Nat.add(z, B), Nat.mul(q, P), w, Equal.sym(Nat, w, Nat.mul(q, P), e3)), w_eq(pp, A, B, hB))
62	  q_one(pp, A, B, q, hA, hB, e4)
63	
64	def eq_false(+pp: Nat, +A: Nat, +B: Nat, +hA: {Nat.is_lt(A, 1n+pp) == True{} : Bool}, +hB: {Nat.is_lt(B, 1n+pp) == True{} : Bool}, +hb: {Nat.is_eq(A, B) == False{} : Bool}, +c: Bool, +hc: {Nat.is_eq(Nat.mod(pw(pp, A, B), 1n+pp), 0n) == c : Bool}) -> {Nat.is_eq(Nat.mod(pw(pp, A, B), 1n+pp), 0n) == Nat.is_eq(A, B) : Bool}:
65	  match c:
66	    case True{}:
67	      +m = Nat.mod(pw(pp, A, B), 1n+pp)
68	      +e = w_ne(pp, A, B, hA, hB, N.eq_from_is_eq(m, 0n, hc))
69	      Empty.absurd({Nat.is_eq(m, 0n) == Nat.is_eq(A, B) : Bool}, L.true_not_false(Nat.is_eq(A, B), L.subst(Nat, z => {Nat.is_eq(A, z) == True{} : Bool}, A, B, e, N.is_eq_refl(A)), hb))
70	    case False{}:
71	      +m = Nat.mod(pw(pp, A, B), 1n+pp)
72	      Equal.trans(Bool, Nat.is_eq(m, 0n), False{}, Nat.is_eq(A, B), hc, Equal.sym(Bool, Nat.is_eq(A, B), False{}, hb))
73	
74	def eq_bool(+pp: Nat, +A: Nat, +B: Nat, +hA: {Nat.is_lt(A, 1n+pp) == True{} : Bool}, +hB: {Nat.is_lt(B, 1n+pp) == True{} : Bool}, +b: Bool, +hb: {Nat.is_eq(A, B) == b : Bool}) -> {Nat.is_eq(Nat.mod(pw(pp, A, B), 1n+pp), 0n) == Nat.is_eq(A, B) : Bool}:
75	  match b:
76	    case True{}:
77	      +e = N.eq_from_is_eq(A, B, hb)
78	      Equal.trans(Bool, Nat.is_eq(Nat.mod(pw(pp, A, B), 1n+pp), 0n), True{}, Nat.is_eq(A, B), Equal.cong(Nat, Bool, z => Nat.is_eq(z, 0n), Nat.mod(pw(pp, A, B), 1n+pp), 0n, w_zero(pp, A, B, hB, e)), Equal.sym(Bool, Nat.is_eq(A, B), True{}, hb))
79	    case False{}:
80	      eq_false(pp, A, B, hA, hB, hb, Nat.is_eq(Nat.mod(pw(pp, A, B), 1n+pp), 0n), {==})
81	
82	def eq_val(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}, +a: List<&2, U32>, +b: List<&2, U32>, +ha: {LM.okb(32n, a, 255n) == True{} : Bool}, +hb: {LM.okb(32n, b, 255n) == True{} : Bool}) -> {F.eq(a, b) == Nat.is_eq(Nat.mod(FS.value(a), 1n+pp), Nat.mod(FS.value(b), 1n+pp)) : Bool}:
83	  +P = {1n+pp : Nat}
84	  +A = Nat.mod(FS.value(a), P)
85	  +B = Nat.mod(FS.value(b), P)
86	  +d = F.sub(a, b)
87	  +e1 = CN.is_zero_val(one, h1, pp, hP, d, FO.sub_okb(one, h1, a, b, ha, hb))
88	  +e2 = FO.sub_mod(one, h1, pp, hP, a, b, ha, hb)
89	  +e3 = G.c_subm(pp, FS.value(a), A, B, G.c_sym(pp, A, FS.value(a), G.c_mod(pp, FS.value(a))), N.lt_le(B, P, NR.dm_lt(pp, FS.value(b))))
90	  +e4 = Equal.trans(Nat, Nat.mod(FS.value(d), P), Nat.mod(Nat.sub(Nat.add(FS.value(a), P), B), P), Nat.mod(pw(pp, A, B), P), e2, e3)
91	  +e5 = Equal.cong(Nat, Bool, z => Nat.is_eq(z, 0n), Nat.mod(FS.value(d), P), Nat.mod(pw(pp, A, B), P), e4)
92	  Equal.trans(Bool, F.eq(a, b), Nat.is_eq(Nat.mod(FS.value(d), P), 0n), Nat.is_eq(A, B), e1, Equal.trans(Bool, Nat.is_eq(Nat.mod(FS.value(d), P), 0n), Nat.is_eq(Nat.mod(pw(pp, A, B), P), 0n), Nat.is_eq(A, B), e5, eq_bool(pp, A, B, NR.dm_lt(pp, FS.value(a)), NR.dm_lt(pp, FS.value(b)), Nat.is_eq(A, B), {==})))