def reduce_okb

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

import Base
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/crypto/curve25519/limbs.bend as LM
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/scalar2.bend as S2

131def reduce_okb(+one: Nat, +h1: {one == 1n : Nat}, +bs: List<&2, U32>, +hb: {LM.lea(bs, 255n) == True{} : Bool}) -> {LM.okb(32n, ESC.reduce(bs), 255n) == True{} : Bool}:
132  %Equal.sym(List<&2, U32>, ESC.mac(X.bitlen(bs), bs, F.one(), F.zero()), S2.macg(X.bitlen(bs), bs, F.one(), F.zero(), ESC.comp_l()), S2.mac_eq(X.bitlen(bs), bs, F.one(), F.zero())) : {LM.okb(32n, _, 255n) == True{} : Bool}
133  S2.mac_okb(one, h1, mmL(one), ESC.comp_l(), cp_okb(), hvL(one, h1), X.bitlen(bs), bs, F.one(), F.zero(), hb, {==}, {==})