def decode_rel

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/ed25519/pdec.bend:152

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/spec/crypto/curve25519/x25519.bend as SX
import bend-collections-laws-crypto@1.0.0.0/spec/crypto/ed25519.bend as SE
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/point.bend as PT
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/crypto/curve25519/limbs.bend as LM
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/rel.bend as RL
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/xbits.bend as XB
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/pcodec.bend as PC

152def decode_rel(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}, +cs: PT.Cs, +D: Nat, +rd: RL.R(pp, PT.cs_d(cs), D), +rs: RL.R(pp, PT.cs_s(cs), SE.sqm1(1n+pp)), +bs: List<&2, U32>, +hb: {LM.okb(32n, bs, 255n) == True{} : Bool}) -> PC.MR(pp, PT.decode(cs, bs), SE.decode(1n+pp, D, bs)):
153  +y = F.mask_top(bs)
154  +Y = FS.value(SX.mask_last(bs))
155  +hyv = Equal.cong(List<&2, U32>, Nat, z => FS.value(z), F.mask_top(bs), SX.mask_last(bs), XB.mask_eq(bs))
156  +hy = XB.mask_okb(31n, bs, hb)
157  +hl = LM.okb_lea(32n, bs, 255n, hb)
158  +hbad = Equal.trans(Bool, PT.ge_p(y), Bool.not(Nat.is_lt(FS.value(y), 1n+pp)), Bool.not(Nat.is_lt(Y, 1n+pp)), ge_p_eq(one, h1, pp, hP, y, hy), Equal.cong(Nat, Bool, z => Bool.not(Nat.is_lt(z, 1n+pp)), FS.value(y), Y, hyv))
159  dec_y_rel(one, h1, pp, hP, cs, D, rd, rs, y, Y, hyv, hy, X.kbit(bs, 255n), SX.kbit(FS.value(bs), 255n), XB.kbit_val(bs, 255n, hl), XB.kbit_le(bs, 255n, hl), Bool.not(Nat.is_lt(Y, 1n+pp)), hbad, {==})