def dec_fin_rel_core

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

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/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/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/curve25519/ladder.bend as LD
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

47def dec_fin_rel_core(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}, +x: List<&2, U32>, +a: Nat, +rx: RL.R(pp, x, a), +ha: {Nat.mod(a, 1n+pp) == a : Nat}, +y: List<&2, U32>, +b: Nat, +ry: RL.R(pp, y, b), +x0: U32, +b0: Nat, +hx0: {v(x0) == b0 : Nat}, +hb0: {Nat.is_le(b0, 1n) == True{} : Bool}, +fs: Bool, +hf: {Bool.and(F.is_zero(x), U32.is_eq(x0, 1)) == fs : Bool}) -> PC.MR(pp, PT.dec_fin(x, y, x0, fs), SE.dec_fin(1n+pp, a, b, b0, fs)):
48  match fs:
49    case True{}:
50      {==}
51    case False{}:
52      +P = {1n+pp : Nat}
53      +s = U32.xor(F.parity(x), x0)
54      +S = SX.bxor(Nat.mod(a, 2n), b0)
55      +hs = XB.xor_bits(F.parity(x), x0, Nat.mod(a, 2n), b0, PC.par_rel(one, h1, pp, hP, x, a, rx, ha), hx0, PC.mod2_le(a), hb0)
56      +hsb = XB.bxor_le(Nat.mod(a, 2n), b0, hb0)
57      +nx = F.neg(x)
58      +NX = FS.fsub(P, 0n, a)
59      +rn = PR.rsub(one, h1, pp, hP, F.zero(), x, 0n, a, PC.r_zero(pp), rx)
60      +ox = RL.r_o(pp, x, a, rx)
61      +on = RL.r_o(pp, nx, NX, rn)
62      +x2 = F.select(s, x, nx)
63      +X2 = SX.cs_fst(S, a, NX)
64      +r2 = RL.mkR(pp, x2, X2, LD.o_sel(one, h1, s, S, hs, hsb, x, nx, ox, on), LD.c_fst(one, h1, pp, s, S, hs, hsb, x, nx, a, NX, ox, RL.r_c(pp, x, a, rx), on, RL.r_c(pp, nx, NX, rn)))
65      PR.mk(pp, x2, y, F.one(), F.mul(x2, y), X2, b, 1n, FS.fmul(P, X2, b), r2, ry, PC.r_one(pp), PR.rmul(one, h1, pp, hP, x2, y, X2, b, r2, ry))