def mul_add_m

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/ed25519/scalar3.bend:103

import Base
import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/curve25519/field.bend as FS
import bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/field.bend as F
import bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/x25519.bend as X
import bend-collections-laws-crypto@1.0.0.0/src/crypto/ed25519/scalar.bend as ESC
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend as WD
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32alg.bend as A
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/limbs.bend as LM
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/scalar.bend as SC
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/scalar2.bend as S2

103def mul_add_m(+one: Nat, +h1: {one == 1n : Nat}, +k: List<&2, U32>, +s: List<&2, U32>, +r: List<&2, U32>, +hk: {LM.lea(k, 255n) == True{} : Bool}, +hs: {LM.okb(32n, s, 255n) == True{} : Bool}, +hr: {LM.okb(32n, r, 255n) == True{} : Bool}, +ls: {Nat.is_lt(FS.value(s), 1n+mmL(one)) == True{} : Bool}, +lr: {Nat.is_lt(FS.value(r), 1n+mmL(one)) == True{} : Bool}) -> {FS.value(ESC.mul_add(k, s, r)) == Nat.mod(Nat.add(FS.value(r), Nat.mul(FS.value(k), FS.value(s))), 1n+mmL(one)) : Nat}:
104  +mm = mmL(one)
105  +P = {1n+mm : Nat}
106  +n = X.bitlen(k)
107  +K2 = FS.value(k)
108  +S = FS.value(s)
109  +R = FS.value(r)
110  +cp = ESC.comp_l()
111  +hv = hvL(one, h1)
112  +h2 = h2L(one, h1)
113  +mg = S2.macg(n, k, s, F.zero(), cp)
114  +om = S2.mac_okb(one, h1, mm, cp, cp_okb(), hv, n, k, s, F.zero(), hk, hs, {==})
115  +lm = S2.mac_below(one, h1, mm, h2, cp, cp_okb(), hv, n, k, s, F.zero(), hk, hs, ls, {==}, {==})
116  +em = S2.mac_val(one, h1, mm, h2, cp, cp_okb(), hv, n, k, s, F.zero(), hk, hs, ls, {==}, {==})
117  +em2 = Equal.trans(Nat, FS.value(mg), Nat.mod(Nat.add(WD.sc(n, 0n), Nat.mul(C.low(n, K2), S)), P), Nat.mod(Nat.mul(K2, S), P), em, M.cong_mod(P, Nat.add(WD.sc(n, 0n), Nat.mul(C.low(n, K2), S)), Nat.mul(K2, S), Equal.trans(Nat, Nat.add(WD.sc(n, 0n), Nat.mul(C.low(n, K2), S)), Nat.add(0n, Nat.mul(C.low(n, K2), S)), Nat.mul(K2, S), M.cong_l(WD.sc(n, 0n), 0n, Nat.mul(C.low(n, K2), S), A.sc_zero(n)), Equal.cong(Nat, Nat, z => Nat.mul(z, S), C.low(n, K2), K2, S2.low_all(k, hk)))))
118  %Equal.sym(List<&2, U32>, ESC.mac(n, k, s, F.zero()), mg, S2.mac_eq(n, k, s, F.zero())) : {FS.value(ESC.addm(_, r)) == Nat.mod(Nat.add(R, Nat.mul(K2, S)), P) : Nat}
119  +ea = SC.addg_val(one, h1, mm, h2, cp, cp_okb(), hv, mg, r, om, hr, lm, lr)
120  +eb = Equal.trans(Nat, Nat.mod(Nat.add(FS.value(mg), R), P), Nat.mod(Nat.add(Nat.mod(Nat.mul(K2, S), P), R), P), Nat.mod(Nat.add(R, Nat.mul(K2, S)), P), M.cong_mod(P, Nat.add(FS.value(mg), R), Nat.add(Nat.mod(Nat.mul(K2, S), P), R), M.cong_l(FS.value(mg), Nat.mod(Nat.mul(K2, S), P), R, em2)), Equal.trans(Nat, Nat.mod(Nat.add(Nat.mod(Nat.mul(K2, S), P), R), P), Nat.mod(Nat.add(Nat.mul(K2, S), R), P), Nat.mod(Nat.add(R, Nat.mul(K2, S)), P), NR.mod_add_l(mm, Nat.mul(K2, S), R), M.cong_mod(P, Nat.add(Nat.mul(K2, S), R), Nat.add(R, Nat.mul(K2, S)), NA.add_comm(Nat.mul(K2, S), R))))
121  Equal.trans(Nat, FS.value(SC.addg(mg, r, cp)), Nat.mod(Nat.add(FS.value(mg), R), P), Nat.mod(Nat.add(R, Nat.mul(K2, S)), P), ea, eb)