def dec_y_rel_core

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

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/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/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/math/natural/arith.bend as NR
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/cong.bend as G
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/ed25519/prel.bend as PR
import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/pcodec.bend as PC

106def dec_y_rel_core(+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)), +y: List<&2, U32>, +Y: Nat, +hyv: {FS.value(y) == Y : Nat}, +hy: {LM.okb(32n, y, 255n) == True{} : Bool}, +x0: U32, +b0: Nat, +hx0: {v(x0) == b0 : Nat}, +hb0: {Nat.is_le(b0, 1n) == True{} : Bool}, +bad: Bool, +hbad: {PT.ge_p(y) == bad : Bool}, +hlt: {Bool.not(Nat.is_lt(Y, 1n+pp)) == bad : Bool}) -> PC.MR(pp, PT.dec_y(cs, y, x0, bad), SE.dec_y(1n+pp, D, Y, b0, bad)):
107  match bad:
108    case True{}:
109      {==}
110    case False{}:
111      +P = {1n+pp : Nat}
112      +lt = nf(Nat.is_lt(Y, P), hlt)
113      +ry = RL.mkR(pp, y, Y, hy, G.c_eq(pp, FS.value(y), Y, hyv))
114      +hYr = NR.mod_of(0n, pp, Y, lt)
115      +yy = F.sq(y)
116      +YY = FS.fmul(P, Y, Y)
117      +ryy = PR.rsq(one, h1, pp, hP, y, Y, ry)
118      +u = F.sub(yy, F.one())
119      +UU = FS.fsub(P, YY, 1n)
120      +ru = PR.rsub(one, h1, pp, hP, yy, F.one(), YY, 1n, ryy, PC.r_one(pp))
121      +vv = F.add(F.mul(PT.cs_d(cs), yy), F.one())
122      +VV = FS.fadd(P, FS.fmul(P, D, YY), 1n)
123      +rv = PR.radd(one, h1, pp, hP, F.mul(PT.cs_d(cs), yy), F.one(), FS.fmul(P, D, YY), 1n, PR.rmul(one, h1, pp, hP, PT.cs_d(cs), yy, D, YY, rd, ryy), PC.r_one(pp))
124      +v3 = F.mul(F.sq(vv), vv)
125      +V3 = FS.fmul(P, FS.fmul(P, VV, VV), VV)
126      +rv3 = PR.rmul(one, h1, pp, hP, F.sq(vv), vv, FS.fmul(P, VV, VV), VV, PR.rsq(one, h1, pp, hP, vv, VV, rv), rv)
127      +v7 = F.mul(F.sq(v3), vv)
128      +V7 = FS.fmul(P, FS.fmul(P, V3, V3), VV)
129      +rv7 = PR.rmul(one, h1, pp, hP, F.sq(v3), vv, FS.fmul(P, V3, V3), VV, PR.rsq(one, h1, pp, hP, v3, V3, rv3), rv)
130      +uv7 = F.mul(u, v7)
131      +UV7 = FS.fmul(P, UU, V7)
132      +ruv7 = PR.rmul(one, h1, pp, hP, u, v7, UU, V7, ru, rv7)
133      +pw = F.pow_p58(uv7)
134      +PWV = FS.fpow(P, UV7, Nat.div(Nat.sub(P, 5n), 8n))
135      +rpw = RL.r_p58(one, h1, pp, hP, uv7, UV7, RL.r_o(pp, uv7, UV7, ruv7), RL.r_c(pp, uv7, UV7, ruv7))
136      +x = F.mul(F.mul(u, v3), pw)
137      +XX = FS.fmul(P, FS.fmul(P, UU, V3), PWV)
138      +rx = PR.rmul(one, h1, pp, hP, F.mul(u, v3), pw, FS.fmul(P, UU, V3), PWV, PR.rmul(one, h1, pp, hP, u, v3, UU, V3, ru, rv3), rpw)
139      +vxx = F.mul(vv, F.sq(x))
140      +VXX = FS.fmul(P, VV, FS.fmul(P, XX, XX))
141      +rvxx = PR.rmul(one, h1, pp, hP, vv, F.sq(x), VV, FS.fmul(P, XX, XX), rv, PR.rsq(one, h1, pp, hP, x, XX, rx))
142      +NU = FS.fsub(P, 0n, UU)
143      +rnu = PR.rsub(one, h1, pp, hP, F.zero(), u, 0n, UU, PC.r_zero(pp), ru)
144      +eu = PC.eq_rel(one, h1, pp, hP, vxx, u, VXX, UU, rvxx, ru, PC.red(pp, Nat.mul(VV, FS.fmul(P, XX, XX))), PC.red(pp, Nat.sub(Nat.add(YY, P), Nat.mod(1n, P))))
145      +enu = PC.eq_rel(one, h1, pp, hP, vxx, F.neg(u), VXX, NU, rvxx, rnu, PC.red(pp, Nat.mul(VV, FS.fmul(P, XX, XX))), PC.red(pp, Nat.sub(Nat.add(0n, P), Nat.mod(UU, P))))
146      dec_root_rel(one, h1, pp, hP, cs, rs, x, XX, rx, PC.red(pp, Nat.mul(FS.fmul(P, UU, V3), PWV)), y, Y, ry, x0, b0, hx0, hb0, u, vxx, F.eq(vxx, u), F.eq(vxx, F.neg(u)), Nat.is_eq(VXX, UU), Nat.is_eq(VXX, NU), eu, enu)