def pass_exact

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

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/crypto/curve25519/limbs.bend as LM
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/fold.bend as FD

134def pass_exact(+r: F.Cr, +hc: {LM.cc(r) == 0 : U32}) -> {F.pass_fin(r) == LM.cl(r) : List<&2, U32>}:
135  %Equal.sym(List<&2, U32>, F.pass_fin(r), F.add0(LM.cl(r), U32.mul(38, LM.cc(r))), FD.pass_fin_eta(r)) : {_ == LM.cl(r) : List<&2, U32>}
136  %Equal.cong(U32, List<&2, U32>, z => F.add0(LM.cl(r), U32.mul(38, z)), 0, LM.cc(r), Equal.sym(U32, LM.cc(r), 0, hc)) : {_ == LM.cl(r) : List<&2, U32>}
137  FD.add0_zero(LM.cl(r))