def sub_core

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/curve25519/fieldops.bend:127

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend as NA
import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend as NR
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/num.bend as M
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/poly.bend as PL

127# S + B == A + 8 P gives S == (A + P - (B mod P)) mod P, mod P
128def sub_core(+pp: Nat, +A: Nat, +B: Nat, +S: Nat, +hS: {Nat.add(S, B) == Nat.add(A, Nat.mul(8n, 1n+pp)) : Nat}) -> {Nat.mod(S, 1n+pp) == Nat.mod(Nat.sub(Nat.add(A, 1n+pp), Nat.mod(B, 1n+pp)), 1n+pp) : Nat}:
129  +P = {1n+pp : Nat}
130  +q = Nat.div(B, P)
131  +r = Nat.mod(B, P)
132  +W = Nat.sub(Nat.add(A, P), r)
133  +hB = NR.dm_eq(pp, B)
134  +rle = N.le_trans(r, P, Nat.add(A, P), N.lt_le(r, P, NR.dm_lt(pp, B)), PL.le_add_l(A, P))
135  +hW = Equal.trans(Nat, Nat.add(W, r), Nat.add(r, W), Nat.add(A, P), NA.add_comm(W, r), N.sub_add(Nat.add(A, P), r, rle))
136  +x1 = Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(q, P), S), r), Nat.add(S, Nat.add(Nat.mul(q, P), r)), Nat.add(A, Nat.mul(8n, P)),
137    Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(q, P), S), r), Nat.add(Nat.add(S, Nat.mul(q, P)), r), Nat.add(S, Nat.add(Nat.mul(q, P), r)), M.cong_l(Nat.add(Nat.mul(q, P), S), Nat.add(S, Nat.mul(q, P)), r, NA.add_comm(Nat.mul(q, P), S)), NA.add_assoc(S, Nat.mul(q, P), r)),
138    Equal.trans(Nat, Nat.add(S, Nat.add(Nat.mul(q, P), r)), Nat.add(S, B), Nat.add(A, Nat.mul(8n, P)), M.cong_r(S, Nat.add(Nat.mul(q, P), r), B, Equal.sym(Nat, B, Nat.add(Nat.mul(q, P), r), hB)), hS))
139  +x2 = Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(7n, P), W), r), Nat.add(Nat.mul(7n, P), Nat.add(W, r)), Nat.add(A, Nat.mul(8n, P)), NA.add_assoc(Nat.mul(7n, P), W, r),
140    Equal.trans(Nat, Nat.add(Nat.mul(7n, P), Nat.add(W, r)), Nat.add(Nat.mul(7n, P), Nat.add(A, P)), Nat.add(A, Nat.mul(8n, P)), M.cong_r(Nat.mul(7n, P), Nat.add(W, r), Nat.add(A, P), hW),
141      Equal.trans(Nat, Nat.add(Nat.mul(7n, P), Nat.add(A, P)), Nat.add(A, Nat.add(Nat.mul(7n, P), P)), Nat.add(A, Nat.mul(8n, P)), NA.add_swap(Nat.mul(7n, P), A, P), M.cong_r(A, Nat.add(Nat.mul(7n, P), P), Nat.mul(8n, P), NA.add_comm(Nat.mul(7n, P), P)))))
142  +x3 = Equal.trans(Nat, Nat.add(r, Nat.add(Nat.mul(q, P), S)), Nat.add(Nat.add(Nat.mul(q, P), S), r), Nat.add(r, Nat.add(Nat.mul(7n, P), W)), NA.add_comm(r, Nat.add(Nat.mul(q, P), S)),
143    Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(q, P), S), r), Nat.add(Nat.add(Nat.mul(7n, P), W), r), Nat.add(r, Nat.add(Nat.mul(7n, P), W)), Equal.trans(Nat, Nat.add(Nat.add(Nat.mul(q, P), S), r), Nat.add(A, Nat.mul(8n, P)), Nat.add(Nat.add(Nat.mul(7n, P), W), r), x1, Equal.sym(Nat, Nat.add(Nat.add(Nat.mul(7n, P), W), r), Nat.add(A, Nat.mul(8n, P)), x2)), NA.add_comm(Nat.add(Nat.mul(7n, P), W), r)))
144  +x4 = NR.add_cancel(r, Nat.add(Nat.mul(q, P), S), Nat.add(Nat.mul(7n, P), W), x3)
145  +m1 = Equal.sym(Nat, Nat.mod(Nat.add(Nat.mul(q, P), S), P), Nat.mod(S, P), NR.absorb(pp, q, S))
146  +m2 = M.cong_mod(P, Nat.add(Nat.mul(q, P), S), Nat.add(Nat.mul(7n, P), W), x4)
147  +m3 = NR.absorb(pp, 7n, W)
148  Equal.trans(Nat, Nat.mod(S, P), Nat.mod(Nat.add(Nat.mul(q, P), S), P), Nat.mod(W, P), m1, Equal.trans(Nat, Nat.mod(Nat.add(Nat.mul(q, P), S), P), Nat.mod(Nat.add(Nat.mul(7n, P), W), P), Nat.mod(W, P), m2, m3))