def finish_rel

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

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

188def 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>}:
189  match st sst:
190    case X.St{+x2, +z2, +x3, +z3, +sw} S.LSt{+a2, +b2, +a3, +b3, +sws}:
191      (+r2, +h2) = h
192      (+rz2, +h3) = h2
193      (+r3, +h4) = h3
194      (+rz3, +h5) = h4
195      (+hs, +hsb) = h5
196      +o2 = RL.r_o(pp, x2, a2, r2)
197      +c2 = RL.r_c(pp, x2, a2, r2)
198      +oz2 = RL.r_o(pp, z2, b2, rz2)
199      +cz2 = RL.r_c(pp, z2, b2, rz2)
200      +o3 = RL.r_o(pp, x3, a3, r3)
201      +c3 = RL.r_c(pp, x3, a3, r3)
202      +oz3 = RL.r_o(pp, z3, b3, rz3)
203      +cz3 = RL.r_c(pp, z3, b3, rz3)
204      +P = {1n+pp : Nat}
205      +xs = F.select(sw, x2, x3)
206      +XS = S.cs_fst(sws, a2, a3)
207      +zs = F.select(sw, z2, z3)
208      +ZS = S.cs_fst(sws, b2, b3)
209      +ox = o_sel(one, h1, sw, sws, hs, hsb, x2, x3, o2, o3)
210      +cx = c_fst(one, h1, pp, sw, sws, hs, hsb, x2, x3, a2, a3, o2, c2, o3, c3)
211      +oz = o_sel(one, h1, sw, sws, hs, hsb, z2, z3, oz2, oz3)
212      +cz = c_fst(one, h1, pp, sw, sws, hs, hsb, z2, z3, b2, b3, oz2, cz2, oz3, cz3)
213      +oi = PW.inv_okb(one, h1, zs, oz)
214      +ci = RL.rc_inv(one, h1, pp, hP, zs, ZS, oz, cz)
215      +m = F.mul(xs, F.inv(zs))
216      +MM = FS.fmul(P, XS, FS.finv(P, ZS))
217      +om = MW.mul_okb(one, h1, xs, F.inv(zs), ox, oi)
218      +cm = RL.rc_mul(one, h1, pp, hP, xs, F.inv(zs), XS, FS.finv(P, ZS), ox, cx, oi, ci)
219      +y = F.freeze(m)
220      +oy = CN.freeze_okb(one, h1, pp, hP, m, om)
221      +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)
222      +e1 = Equal.sym(List<&2, U32>, S.le_bytes(32n, FS.value(y)), y, XB.bytes_le(32n, y, oy))
223      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))