Fieldops.sub_core: def of bend-collections-laws-crypto@1.0.0.0 Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/fieldops.bend as Fieldops Lines 127-148 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/fieldops.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/fieldops.bend&start_line=127&end_line=148 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 # S + B == A + 8 P gives S == (A + P - (B mod P)) mod P, mod P def 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}: +P = {1n+pp : Nat} +q = Nat.div(B, P) +r = Nat.mod(B, P) +W = Nat.sub(Nat.add(A, P), r) +hB = NR.dm_eq(pp, B) +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)) +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)) +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)), 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)), 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)) +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), 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), 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))))) +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)), 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))) +x4 = NR.add_cancel(r, Nat.add(Nat.mul(q, P), S), Nat.add(Nat.mul(7n, P), W), x3) +m1 = Equal.sym(Nat, Nat.mod(Nat.add(Nat.mul(q, P), S), P), Nat.mod(S, P), NR.absorb(pp, q, S)) +m2 = M.cong_mod(P, Nat.add(Nat.mul(q, P), S), Nat.add(Nat.mul(7n, P), W), x4) +m3 = NR.absorb(pp, 7n, W) 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)) Uses (22): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.div https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mod https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.sub https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/num.bend&name=cong_l https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/num.bend&name=cong_mod https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/num.bend&name=cong_r https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/poly.bend&name=le_add_l https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=add_assoc https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=add_comm https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/proofs/nat_algebra.bend&name=add_swap https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=le_trans https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=lt_le https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend&name=sub_add https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend&name=absorb https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend&name=add_cancel https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend&name=dm_eq https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend&name=dm_lt