def reduce_m

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

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/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/scalar2.bend as S2

94def reduce_m(+one: Nat, +h1: {one == 1n : Nat}, +bs: List<&2, U32>, +hb: {LM.lea(bs, 255n) == True{} : Bool}) -> {FS.value(ESC.reduce(bs)) == Nat.mod(FS.value(bs), 1n+mmL(one)) : Nat}:
95  +mm = mmL(one)
96  +n = X.bitlen(bs)
97  +V = FS.value(bs)
98  %Equal.sym(List<&2, U32>, ESC.mac(n, bs, F.one(), F.zero()), S2.macg(n, bs, F.one(), F.zero(), ESC.comp_l()), S2.mac_eq(n, bs, F.one(), F.zero())) : {FS.value(_) == Nat.mod(V, 1n+mm) : Nat}
99  +e = S2.mac_val(one, h1, mm, h2L(one, h1), ESC.comp_l(), cp_okb(), hvL(one, h1), n, bs, F.one(), F.zero(), hb, {==}, one_lt(one, h1), {==}, {==})
100  +e2 = Equal.trans(Nat, Nat.add(WD.sc(n, 0n), Nat.mul(C.low(n, V), 1n)), Nat.add(0n, Nat.mul(C.low(n, V), 1n)), V, M.cong_l(WD.sc(n, 0n), 0n, Nat.mul(C.low(n, V), 1n), A.sc_zero(n)), Equal.trans(Nat, Nat.mul(C.low(n, V), 1n), C.low(n, V), V, NA.mul_one(C.low(n, V)), S2.low_all(bs, hb)))
101  Equal.trans(Nat, FS.value(S2.macg(n, bs, F.one(), F.zero(), ESC.comp_l())), Nat.mod(Nat.add(WD.sc(n, 0n), Nat.mul(C.low(n, V), 1n)), 1n+mm), Nat.mod(V, 1n+mm), e, M.cong_mod(1n+mm, Nat.add(WD.sc(n, 0n), Nat.mul(C.low(n, V), 1n)), V, e2))