Ladder.finish_rel: def of bend-collections-laws-crypto@1.0.0.0 Import: import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/ladder.bend as Ladder Lines 188-223 of bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/ladder.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/ladder.bend&start_line=188&end_line=223 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 S 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/proofs/lib/word.bend as WD import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/canon.bend as CN 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/mulw.bend as MW import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/pow.bend as PW import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/xbits.bend as XB def finish_rel(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}, +st: X.St, +sst: S.LSt, +h: Rst(pp, st, sst)) -> {X.finish(st) == S.finish(1n+pp, sst) : List<&2, U32>}: match st sst: case X.St{+x2, +z2, +x3, +z3, +sw} S.LSt{+a2, +b2, +a3, +b3, +sws}: (+r2, +h2) = h (+rz2, +h3) = h2 (+r3, +h4) = h3 (+rz3, +h5) = h4 (+hs, +hsb) = h5 +o2 = RL.r_o(pp, x2, a2, r2) +c2 = RL.r_c(pp, x2, a2, r2) +oz2 = RL.r_o(pp, z2, b2, rz2) +cz2 = RL.r_c(pp, z2, b2, rz2) +o3 = RL.r_o(pp, x3, a3, r3) +c3 = RL.r_c(pp, x3, a3, r3) +oz3 = RL.r_o(pp, z3, b3, rz3) +cz3 = RL.r_c(pp, z3, b3, rz3) +P = {1n+pp : Nat} +xs = F.select(sw, x2, x3) +XS = S.cs_fst(sws, a2, a3) +zs = F.select(sw, z2, z3) +ZS = S.cs_fst(sws, b2, b3) +ox = o_sel(one, h1, sw, sws, hs, hsb, x2, x3, o2, o3) +cx = c_fst(one, h1, pp, sw, sws, hs, hsb, x2, x3, a2, a3, o2, c2, o3, c3) +oz = o_sel(one, h1, sw, sws, hs, hsb, z2, z3, oz2, oz3) +cz = c_fst(one, h1, pp, sw, sws, hs, hsb, z2, z3, b2, b3, oz2, cz2, oz3, cz3) +oi = PW.inv_okb(one, h1, zs, oz) +ci = RL.rc_inv(one, h1, pp, hP, zs, ZS, oz, cz) +m = F.mul(xs, F.inv(zs)) +MM = FS.fmul(P, XS, FS.finv(P, ZS)) +om = MW.mul_okb(one, h1, xs, F.inv(zs), ox, oi) +cm = RL.rc_mul(one, h1, pp, hP, xs, F.inv(zs), XS, FS.finv(P, ZS), ox, cx, oi, ci) +y = F.freeze(m) +oy = CN.freeze_okb(one, h1, pp, hP, m, om) +ey = Equal.trans(Nat, FS.value(y), Nat.mod(FS.value(m), P), Nat.mod(MM, P), CN.freeze_val(one, h1, pp, hP, m, om), cm) +e1 = Equal.sym(List<&2, U32>, S.le_bytes(32n, FS.value(y)), y, XB.bytes_le(32n, y, oy)) Equal.trans(List<&2, U32>, y, S.le_bytes(32n, FS.value(y)), S.le_bytes(32n, Nat.mod(MM, P)), e1, Equal.cong(Nat, List<&2, U32>, z => S.le_bytes(32n, z), FS.value(y), Nat.mod(MM, P), ey)) Uses (35): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans 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.mod https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/canon.bend&name=freeze_okb https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/canon.bend&name=freeze_val https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/ladder.bend&name=Rst 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/mulw.bend&name=mul_okb https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/pow.bend&name=inv_okb 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/rel.bend&name=rc_inv https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/rel.bend&name=rc_mul https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/xbits.bend&name=bytes_le 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=finv 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=value https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/curve25519/x25519.bend&name=LSt 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/curve25519/x25519.bend&name=finish https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/curve25519/x25519.bend&name=le_bytes https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/field.bend&name=freeze https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/field.bend&name=inv 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=select https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/x25519.bend&name=St https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/x25519.bend&name=finish