def cs_one

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/curve25519/freeze.bend:143

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/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
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/consts.bend as K
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/fieldops.bend as FO

143def cs_one(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}, +x: List<&2, U32>, +cp: List<&2, U32>, +hx: {LM.okb(32n, x, 255n) == True{} : Bool}, +hk: {LM.okb(32n, cp, 128n) == True{} : Bool}, +hv: {K.valo(one, cp) == Nat.add(1n+pp, 38n) : Nat}, +hc: {Nat.is_lt(v(LM.cc(F.carry(F.addl(x, cp), 0))), one) == False{} : Bool}) -> {csg(x, cp) == LM.cl(F.carry(F.addl(x, cp), 0)) : List<&2, U32>}:
144  +r = F.carry(F.addl(x, cp), 0)
145  +c1 = Equal.trans(Nat, v(LM.cc(r)), one, 1n, o_c(one, h1, pp, hP, x, cp, hx, hk, hv, hc), h1)
146  +co = U.injective(LM.cc(r), 1, c1)
147  %Equal.sym(List<&2, U32>, F.csub_fin(r, x), F.select(LM.cc(r), x, LM.cl(r)), cs_eta(r, x)) : {_ == LM.cl(r) : List<&2, U32>}
148  %Equal.cong(U32, List<&2, U32>, z => F.select(z, x, LM.cl(r)), 1, LM.cc(r), Equal.sym(U32, LM.cc(r), 1, co)) : {_ == LM.cl(r) : List<&2, U32>}
149  FO.select1(one, h1, 32n, x, LM.cl(r), hx, FD.cr_okb(one, h1, F.addl(x, cp), ad_okb(one, h1, x, cp, hx, hk)))