Ladder.step_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 83-149 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=83&end_line=149 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/limbs.bend as LM import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/consts.bend as K import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/fieldops.bend as FO 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/curve25519/mulw.bend as MW def step_rel(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}, +c24: List<&2, U32>, +oc: {LM.okb(32n, c24, 255n) == True{} : Bool}, +hv: {K.valo(one, c24) == S.a24(one) : Nat}, +x1: List<&2, U32>, +X1: Nat, +o1: {LM.okb(32n, x1, 255n) == True{} : Bool}, +c1: G.ceq(pp, FS.value(x1), X1), +x2: List<&2, U32>, +X2: Nat, +o2: {LM.okb(32n, x2, 255n) == True{} : Bool}, +c2: G.ceq(pp, FS.value(x2), X2), +z2: List<&2, U32>, +Z2: Nat, +oz2: {LM.okb(32n, z2, 255n) == True{} : Bool}, +cz2: G.ceq(pp, FS.value(z2), Z2), +x3: List<&2, U32>, +X3: Nat, +o3: {LM.okb(32n, x3, 255n) == True{} : Bool}, +c3: G.ceq(pp, FS.value(x3), X3), +z3: List<&2, U32>, +Z3: Nat, +oz3: {LM.okb(32n, z3, 255n) == True{} : Bool}, +cz3: G.ceq(pp, FS.value(z3), Z3), +kt: U32, +KT: Nat, +hk: {v(kt) == KT : Nat}, +hkb: {Nat.is_le(KT, 1n) == True{} : Bool}) -> Rst(pp, X.step(c24, x1, x2, z2, x3, z3, kt), S.step(one, 1n+pp, X1, X2, Z2, X3, Z3, KT)): +P = {1n+pp : Nat} +A24 = S.a24(one) +cc = a24_c(one, h1, pp, c24, hv) +a = F.add(x2, z2) +A = FS.fadd(P, X2, Z2) +oa = FO.add_okb(one, h1, x2, z2, o2, oz2) +ca = RL.rc_add(one, h1, pp, hP, x2, z2, X2, Z2, o2, c2, oz2, cz2) +aa = F.sq(a) +AA = FS.fmul(P, A, A) +oaa = MW.sq_okb(one, h1, a, oa) +caa = RL.rc_sq(one, h1, pp, hP, a, A, oa, ca) +b = F.sub(x2, z2) +B = FS.fsub(P, X2, Z2) +ob = FO.sub_okb(one, h1, x2, z2, o2, oz2) +cb = RL.rc_sub(one, h1, pp, hP, x2, z2, X2, Z2, o2, c2, oz2, cz2) +bb = F.sq(b) +BB = FS.fmul(P, B, B) +obb = MW.sq_okb(one, h1, b, ob) +cbb = RL.rc_sq(one, h1, pp, hP, b, B, ob, cb) +e = F.sub(aa, bb) +E = FS.fsub(P, AA, BB) +oe = FO.sub_okb(one, h1, aa, bb, oaa, obb) +ce = RL.rc_sub(one, h1, pp, hP, aa, bb, AA, BB, oaa, caa, obb, cbb) +c = F.add(x3, z3) +CC = FS.fadd(P, X3, Z3) +occ = FO.add_okb(one, h1, x3, z3, o3, oz3) +ccc = RL.rc_add(one, h1, pp, hP, x3, z3, X3, Z3, o3, c3, oz3, cz3) +d = F.sub(x3, z3) +D = FS.fsub(P, X3, Z3) +od = FO.sub_okb(one, h1, x3, z3, o3, oz3) +cd = RL.rc_sub(one, h1, pp, hP, x3, z3, X3, Z3, o3, c3, oz3, cz3) +da = F.mul(d, a) +DA = FS.fmul(P, D, A) +oda = MW.mul_okb(one, h1, d, a, od, oa) +cda = RL.rc_mul(one, h1, pp, hP, d, a, D, A, od, cd, oa, ca) +cb2 = F.mul(c, b) +CB = FS.fmul(P, CC, B) +ocb = MW.mul_okb(one, h1, c, b, occ, ob) +ccb = RL.rc_mul(one, h1, pp, hP, c, b, CC, B, occ, ccc, ob, cb) +oo1 = MW.mul_okb(one, h1, aa, bb, oaa, obb) +co1 = RL.rc_mul(one, h1, pp, hP, aa, bb, AA, BB, oaa, caa, obb, cbb) +ec = F.mul(e, c24) +EC = FS.fmul(P, E, A24) +oec = MW.mul_okb(one, h1, e, c24, oe, oc) +cec = RL.rc_mul(one, h1, pp, hP, e, c24, E, A24, oe, ce, oc, cc) +sm = F.add(aa, ec) +SM = FS.fadd(P, AA, EC) +osm = FO.add_okb(one, h1, aa, ec, oaa, oec) +csm = RL.rc_add(one, h1, pp, hP, aa, ec, AA, EC, oaa, caa, oec, cec) +oo2 = MW.mul_okb(one, h1, e, sm, oe, osm) +co2 = RL.rc_mul(one, h1, pp, hP, e, sm, E, SM, oe, ce, osm, csm) +sg = F.add(da, cb2) +SG = FS.fadd(P, DA, CB) +osg = FO.add_okb(one, h1, da, cb2, oda, ocb) +csg = RL.rc_add(one, h1, pp, hP, da, cb2, DA, CB, oda, cda, ocb, ccb) +oo3 = MW.sq_okb(one, h1, sg, osg) +co3 = RL.rc_sq(one, h1, pp, hP, sg, SG, osg, csg) +t = F.sub(da, cb2) +T = FS.fsub(P, DA, CB) +ot = FO.sub_okb(one, h1, da, cb2, oda, ocb) +ct = RL.rc_sub(one, h1, pp, hP, da, cb2, DA, CB, oda, cda, ocb, ccb) +ott = MW.sq_okb(one, h1, t, ot) +ctt = RL.rc_sq(one, h1, pp, hP, t, T, ot, ct) +oo4 = MW.mul_okb(one, h1, x1, F.sq(t), o1, ott) +co4 = RL.rc_mul(one, h1, pp, hP, x1, F.sq(t), X1, FS.fmul(P, T, T), o1, c1, ott, ctt) ((oo1, co1), ((oo2, co2), ((oo3, co3), ((oo4, co4), (hk, hkb))))) Uses (33): https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool 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=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/cong.bend&name=ceq https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/consts.bend&name=valo https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/fieldops.bend&name=add_okb https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/fieldops.bend&name=sub_okb 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=a24_c https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/ladder.bend&name=v https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend&name=okb 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/mulw.bend&name=sq_okb https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/rel.bend&name=rc_add 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/rel.bend&name=rc_sq https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/rel.bend&name=rc_sub 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=fadd 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/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=a24 https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/spec/crypto/curve25519/x25519.bend&name=step https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/field.bend&name=add 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=sq https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/field.bend&name=sub https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/x25519.bend&name=step