def reduce_okb

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/curve25519/reduce.bend:139

import Base
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/proofs/lib/word.bend as WD
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32.bend as U
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/curve25519/fold.bend as FD

139# reduce gives 32 limbs below 2^8
140def reduce_okb(+one: Nat, +h1: {one == 1n : Nat}, +xs: List<&2, U32>, +hx: {LM.okb(32n, xs, WD.sc(28n, one)) == True{} : Bool}) -> {LM.okb(32n, F.reduce(xs), 255n) == True{} : Bool}:
141  +y2 = F.pass(F.pass(xs))
142  +hy2 = FD.pass_okb(one, h1, F.pass(xs), FD.pass_okb(one, h1, xs, hx))
143  +r3 = F.carry(y2, 0)
144  +c3 = v(LM.cc(r3))
145  +z = last_zero(one, h1, FS.value(LM.cl(r3)), c3, FS.value(y2), FD.cr_val(one, h1, y2, hy2), two_lt(one, h1, xs, hx), Nat.is_lt(c3, one), {==})
146  +cz = U.injective(LM.cc(r3), 0, z)
147  %Equal.sym(List<&2, U32>, F.pass_fin(r3), LM.cl(r3), pass_exact(r3, cz)) : {LM.okb(32n, _, 255n) == True{} : Bool}
148  FD.cr_okb(one, h1, y2, hy2)