Pdec.dec_fin_rel_core: def of bend-collections-laws-crypto@1.0.0.0 Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/pdec.bend as Pdec Lines 47-65 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/pdec.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/pdec.bend&start_line=47&end_line=65 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 def 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)): match fs: case True{}: {==} case False{}: +P = {1n+pp : Nat} +s = U32.xor(F.parity(x), x0) +S = SX.bxor(Nat.mod(a, 2n), b0) +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) +hsb = XB.bxor_le(Nat.mod(a, 2n), b0, hb0) +nx = F.neg(x) +NX = FS.fsub(P, 0n, a) +rn = PR.rsub(one, h1, pp, hP, F.zero(), x, 0n, a, PC.r_zero(pp), rx) +ox = RL.r_o(pp, x, a, rx) +on = RL.r_o(pp, nx, NX, rn) +x2 = F.select(s, x, nx) +X2 = SX.cs_fst(S, a, NX) +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))) 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)) Uses (41): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.and https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=List https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.is_le https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mod https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32 https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.is_eq https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.xor https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/ladder.bend&name=c_fst https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/ladder.bend&name=o_sel https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/rel.bend&name=R https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/rel.bend&name=mkR https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/rel.bend&name=r_c https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/rel.bend&name=r_o https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/xbits.bend&name=bxor_le https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/xbits.bend&name=xor_bits https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/pcodec.bend&name=MR https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/pcodec.bend&name=mod2_le https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/pcodec.bend&name=par_rel https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/pcodec.bend&name=r_one https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/pcodec.bend&name=r_zero https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/pdec.bend&name=v https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/prel.bend&name=mk https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/prel.bend&name=rmul https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/ed25519/prel.bend&name=rsub https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend&name=sc https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/curve25519/field.bend&name=fmul https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/curve25519/field.bend&name=fsub https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/curve25519/x25519.bend&name=bxor https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/curve25519/x25519.bend&name=cs_fst https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/ed25519.bend&name=dec_fin https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/field.bend&name=is_zero https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/field.bend&name=mul https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/field.bend&name=neg https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/field.bend&name=one https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/field.bend&name=parity https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/field.bend&name=select https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/field.bend&name=zero https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/ed25519/point.bend&name=dec_fin