def step_rel

bend-collections-laws-crypto@1.0.0.0 · proofs/crypto/curve25519/ladder.bend:83

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

83def 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)):
84  +P = {1n+pp : Nat}
85  +A24 = S.a24(one)
86  +cc = a24_c(one, h1, pp, c24, hv)
87  +a = F.add(x2, z2)
88  +A = FS.fadd(P, X2, Z2)
89  +oa = FO.add_okb(one, h1, x2, z2, o2, oz2)
90  +ca = RL.rc_add(one, h1, pp, hP, x2, z2, X2, Z2, o2, c2, oz2, cz2)
91  +aa = F.sq(a)
92  +AA = FS.fmul(P, A, A)
93  +oaa = MW.sq_okb(one, h1, a, oa)
94  +caa = RL.rc_sq(one, h1, pp, hP, a, A, oa, ca)
95  +b = F.sub(x2, z2)
96  +B = FS.fsub(P, X2, Z2)
97  +ob = FO.sub_okb(one, h1, x2, z2, o2, oz2)
98  +cb = RL.rc_sub(one, h1, pp, hP, x2, z2, X2, Z2, o2, c2, oz2, cz2)
99  +bb = F.sq(b)
100  +BB = FS.fmul(P, B, B)
101  +obb = MW.sq_okb(one, h1, b, ob)
102  +cbb = RL.rc_sq(one, h1, pp, hP, b, B, ob, cb)
103  +e = F.sub(aa, bb)
104  +E = FS.fsub(P, AA, BB)
105  +oe = FO.sub_okb(one, h1, aa, bb, oaa, obb)
106  +ce = RL.rc_sub(one, h1, pp, hP, aa, bb, AA, BB, oaa, caa, obb, cbb)
107  +c = F.add(x3, z3)
108  +CC = FS.fadd(P, X3, Z3)
109  +occ = FO.add_okb(one, h1, x3, z3, o3, oz3)
110  +ccc = RL.rc_add(one, h1, pp, hP, x3, z3, X3, Z3, o3, c3, oz3, cz3)
111  +d = F.sub(x3, z3)
112  +D = FS.fsub(P, X3, Z3)
113  +od = FO.sub_okb(one, h1, x3, z3, o3, oz3)
114  +cd = RL.rc_sub(one, h1, pp, hP, x3, z3, X3, Z3, o3, c3, oz3, cz3)
115  +da = F.mul(d, a)
116  +DA = FS.fmul(P, D, A)
117  +oda = MW.mul_okb(one, h1, d, a, od, oa)
118  +cda = RL.rc_mul(one, h1, pp, hP, d, a, D, A, od, cd, oa, ca)
119  +cb2 = F.mul(c, b)
120  +CB = FS.fmul(P, CC, B)
121  +ocb = MW.mul_okb(one, h1, c, b, occ, ob)
122  +ccb = RL.rc_mul(one, h1, pp, hP, c, b, CC, B, occ, ccc, ob, cb)
123  +oo1 = MW.mul_okb(one, h1, aa, bb, oaa, obb)
124  +co1 = RL.rc_mul(one, h1, pp, hP, aa, bb, AA, BB, oaa, caa, obb, cbb)
125  +ec = F.mul(e, c24)
126  +EC = FS.fmul(P, E, A24)
127  +oec = MW.mul_okb(one, h1, e, c24, oe, oc)
128  +cec = RL.rc_mul(one, h1, pp, hP, e, c24, E, A24, oe, ce, oc, cc)
129  +sm = F.add(aa, ec)
130  +SM = FS.fadd(P, AA, EC)
131  +osm = FO.add_okb(one, h1, aa, ec, oaa, oec)
132  +csm = RL.rc_add(one, h1, pp, hP, aa, ec, AA, EC, oaa, caa, oec, cec)
133  +oo2 = MW.mul_okb(one, h1, e, sm, oe, osm)
134  +co2 = RL.rc_mul(one, h1, pp, hP, e, sm, E, SM, oe, ce, osm, csm)
135  +sg = F.add(da, cb2)
136  +SG = FS.fadd(P, DA, CB)
137  +osg = FO.add_okb(one, h1, da, cb2, oda, ocb)
138  +csg = RL.rc_add(one, h1, pp, hP, da, cb2, DA, CB, oda, cda, ocb, ccb)
139  +oo3 = MW.sq_okb(one, h1, sg, osg)
140  +co3 = RL.rc_sq(one, h1, pp, hP, sg, SG, osg, csg)
141  +t = F.sub(da, cb2)
142  +T = FS.fsub(P, DA, CB)
143  +ot = FO.sub_okb(one, h1, da, cb2, oda, ocb)
144  +ct = RL.rc_sub(one, h1, pp, hP, da, cb2, DA, CB, oda, cda, ocb, ccb)
145  +ott = MW.sq_okb(one, h1, t, ot)
146  +ctt = RL.rc_sq(one, h1, pp, hP, t, T, ot, ct)
147  +oo4 = MW.mul_okb(one, h1, x1, F.sq(t), o1, ott)
148  +co4 = RL.rc_mul(one, h1, pp, hP, x1, F.sq(t), X1, FS.fmul(P, T, T), o1, c1, ott, ctt)
149  ((oo1, co1), ((oo2, co2), ((oo3, co3), ((oo4, co4), (hk, hkb)))))