~/bend-docscommunity

proofs/crypto/curve25519/ladder.bend source

proofs/crypto/curve25519/ladder.bend on the hub · documented module

import Baseimport ../../../spec/lib/common.bend as Cimport ../../../spec/crypto/curve25519/field.bend as FSimport ../../../spec/crypto/curve25519/x25519.bend as Simport ../../../src/crypto/curve25519/field.bend as Fimport ../../../src/crypto/curve25519/x25519.bend as Ximport ../../lib/nat.bend as Nimport ../../lib/logic.bend as Limport ../../lib/word.bend as WDimport ./limbs.bend as LMimport ./consts.bend as Kimport ./fieldops.bend as FOimport ./canon.bend as CNimport ./cong.bend as Gimport ./rel.bend as RLimport ./mulw.bend as MWimport ./pow.bend as PWimport ./xbits.bend as XBimport ./prime.bend as PR# X25519 == RFC 7748 (spec/crypto/curve25519/x25519.bend): the ladder state# of the implementation is related to the specification's state field by# field (RL.R), the swap bit is equal; every rung keeps the relation; the# final cswap, inversion, product and encoding give the same bytes.def v(+x: U32) -> Nat:  U32.to_nat(x)def DP(-A: Data, -B: Data) -> Data:  Sigma<&2, &2, A, _ => B>def Rst(+pp: Nat, st: X.St, sst: S.LSt) -> Data:  match st sst:    case X.St{x2, z2, x3, z3, sw} S.LSt{a2, b2, a3, b3, sws}:      DP(RL.R(pp, x2, a2), DP(RL.R(pp, z2, b2), DP(RL.R(pp, x3, a3), DP(RL.R(pp, z3, b3), DP({U32.to_nat(sw) == sws : Nat}, {Nat.is_le(sws, 1n) == True{} : Bool})))))# ---- conditional swaps ----def o_sel(+one: Nat, +h1: {one == 1n : Nat}, +sw: U32, +s: Nat, +hs: {v(sw) == s : Nat}, +hb: {Nat.is_le(s, 1n) == True{} : Bool}, +a: List<&2, U32>, +b: List<&2, U32>, +oa: {LM.okb(32n, a, 255n) == True{} : Bool}, +ob: {LM.okb(32n, b, 255n) == True{} : Bool}) -> {LM.okb(32n, F.select(sw, a, b), 255n) == True{} : Bool}:  match s:    case 0n:      %Equal.sym(U32, sw, 0, XB.u0(sw, hs)) : {LM.okb(32n, F.select(_, a, b), 255n) == True{} : Bool}      %Equal.sym(List<&2, U32>, F.select(0, a, b), a, FO.select0(one, h1, 32n, a, b, oa, ob)) : {LM.okb(32n, _, 255n) == True{} : Bool}      oa    case 1n:      %Equal.sym(U32, sw, 1, XB.u1(sw, hs)) : {LM.okb(32n, F.select(_, a, b), 255n) == True{} : Bool}      %Equal.sym(List<&2, U32>, F.select(1, a, b), b, FO.select1(one, h1, 32n, a, b, oa, ob)) : {LM.okb(32n, _, 255n) == True{} : Bool}      ob    case 2n+q:      Empty.absurd({LM.okb(32n, F.select(sw, a, b), 255n) == True{} : Bool}, L.false_true(hb))def c_fst(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +sw: U32, +s: Nat, +hs: {v(sw) == s : Nat}, +hb: {Nat.is_le(s, 1n) == True{} : Bool}, +a: List<&2, U32>, +b: List<&2, U32>, +A: Nat, +B: Nat, +oa: {LM.okb(32n, a, 255n) == True{} : Bool}, +ca: G.ceq(pp, FS.value(a), A), +ob: {LM.okb(32n, b, 255n) == True{} : Bool}, +cb: G.ceq(pp, FS.value(b), B)) -> G.ceq(pp, FS.value(F.select(sw, a, b)), S.cs_fst(s, A, B)):  match s:    case 0n:      %Equal.sym(U32, sw, 0, XB.u0(sw, hs)) : G.ceq(pp, FS.value(F.select(_, a, b)), A)      %Equal.sym(List<&2, U32>, F.select(0, a, b), a, FO.select0(one, h1, 32n, a, b, oa, ob)) : G.ceq(pp, FS.value(_), A)      ca    case 1n:      %Equal.sym(U32, sw, 1, XB.u1(sw, hs)) : G.ceq(pp, FS.value(F.select(_, a, b)), B)      %Equal.sym(List<&2, U32>, F.select(1, a, b), b, FO.select1(one, h1, 32n, a, b, oa, ob)) : G.ceq(pp, FS.value(_), B)      cb    case 2n+q:      Empty.absurd(G.ceq(pp, FS.value(F.select(sw, a, b)), B), L.false_true(hb))def c_snd(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +sw: U32, +s: Nat, +hs: {v(sw) == s : Nat}, +hb: {Nat.is_le(s, 1n) == True{} : Bool}, +a: List<&2, U32>, +b: List<&2, U32>, +A: Nat, +B: Nat, +oa: {LM.okb(32n, a, 255n) == True{} : Bool}, +ca: G.ceq(pp, FS.value(a), A), +ob: {LM.okb(32n, b, 255n) == True{} : Bool}, +cb: G.ceq(pp, FS.value(b), B)) -> G.ceq(pp, FS.value(F.select(sw, b, a)), S.cs_snd(s, A, B)):  match s:    case 0n:      %Equal.sym(U32, sw, 0, XB.u0(sw, hs)) : G.ceq(pp, FS.value(F.select(_, b, a)), B)      %Equal.sym(List<&2, U32>, F.select(0, b, a), b, FO.select0(one, h1, 32n, b, a, ob, oa)) : G.ceq(pp, FS.value(_), B)      cb    case 1n:      %Equal.sym(U32, sw, 1, XB.u1(sw, hs)) : G.ceq(pp, FS.value(F.select(_, b, a)), A)      %Equal.sym(List<&2, U32>, F.select(1, b, a), a, FO.select1(one, h1, 32n, b, a, ob, oa)) : G.ceq(pp, FS.value(_), A)      ca    case 2n+q:      Empty.absurd(G.ceq(pp, FS.value(F.select(sw, b, a)), A), L.false_true(hb))# ---- one step ----def a24_c(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +c24: List<&2, U32>, +hv: {K.valo(one, c24) == S.a24(one) : Nat}) -> G.ceq(pp, FS.value(c24), S.a24(one)):  G.c_eq(pp, FS.value(c24), S.a24(one), Equal.trans(Nat, FS.value(c24), K.valo(one, c24), S.a24(one), Equal.sym(Nat, K.valo(one, c24), FS.value(c24), K.valo_value(one, h1, c24)), hv))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)))))# ---- one rung: swap ^= k_t, cswap, step ----def rung_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), +st: X.St, +sst: S.LSt, +h: Rst(pp, st, sst), +kt: U32, +KT: Nat, +hk: {v(kt) == KT : Nat}, +hkb: {Nat.is_le(KT, 1n) == True{} : Bool}) -> Rst(pp, X.rung(c24, x1, st, kt), S.rung(one, 1n+pp, X1, sst, KT)):  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)      +w = U32.xor(sw, kt)      +W = S.bxor(sws, KT)      +hw = XB.xor_bits(sw, kt, sws, KT, hs, hk, hsb, hkb)      +hwb = XB.bxor_le(sws, KT, hkb)      step_rel(one, h1, pp, hP, c24, oc, hv, x1, X1, o1, c1, F.select(w, x2, x3), S.cs_fst(W, a2, a3), o_sel(one, h1, w, W, hw, hwb, x2, x3, o2, o3), c_fst(one, h1, pp, w, W, hw, hwb, x2, x3, a2, a3, o2, c2, o3, c3), F.select(w, z2, z3), S.cs_fst(W, b2, b3), o_sel(one, h1, w, W, hw, hwb, z2, z3, oz2, oz3), c_fst(one, h1, pp, w, W, hw, hwb, z2, z3, b2, b3, oz2, cz2, oz3, cz3), F.select(w, x3, x2), S.cs_snd(W, a2, a3), o_sel(one, h1, w, W, hw, hwb, x3, x2, o3, o2), c_snd(one, h1, pp, w, W, hw, hwb, x2, x3, a2, a3, o2, c2, o3, c3), F.select(w, z3, z2), S.cs_snd(W, b2, b3), o_sel(one, h1, w, W, hw, hwb, z3, z2, oz3, oz2), c_snd(one, h1, pp, w, W, hw, hwb, z2, z3, b2, b3, oz2, cz2, oz3, cz3), kt, KT, hk, hkb)# ---- the ladder ----def ladder_rel(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}, +n: Nat, +c24: List<&2, U32>, +oc: {LM.okb(32n, c24, 255n) == True{} : Bool}, +hv: {K.valo(one, c24) == S.a24(one) : Nat}, +kc: List<&2, U32>, +hkc: {LM.lea(kc, 255n) == True{} : Bool}, +x1: List<&2, U32>, +X1: Nat, +o1: {LM.okb(32n, x1, 255n) == True{} : Bool}, +c1: G.ceq(pp, FS.value(x1), X1), +st: X.St, +sst: S.LSt, +h: Rst(pp, st, sst)) -> Rst(pp, X.ladder(n, c24, kc, x1, st), S.ladder(one, 1n+pp, n, FS.value(kc), X1, sst)):  match n:    case 0n:      h    case 1n+ +t:      +kt = X.kbit(kc, t)      +KT = S.kbit(FS.value(kc), t)      ladder_rel(one, h1, pp, hP, t, c24, oc, hv, kc, hkc, x1, X1, o1, c1, X.rung(c24, x1, st, kt), S.rung(one, 1n+pp, X1, sst, KT), rung_rel(one, h1, pp, hP, c24, oc, hv, x1, X1, o1, c1, st, sst, h, kt, KT, XB.kbit_val(kc, t, hkc), XB.kbit_le(kc, t, hkc)))# ---- the end: cswap, x2 / z2, encode ----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))# ---- X25519 ----def a24_shape() -> {X.a24() == Con{65, Con{219, Con{1, K.rep(29n, 0, Nil{})}}} : List<&2, U32>}:  {==}def a24_valo(+one: Nat) -> {K.valo(one, X.a24()) == S.a24(one) : Nat}:  %Equal.sym(List<&2, U32>, X.a24(), Con{65, Con{219, Con{1, K.rep(29n, 0, Nil{})}}}, a24_shape()) : {K.valo(one, _) == S.a24(one) : Nat}  %Equal.sym(Nat, K.valo(one, K.rep(29n, 0, Nil{})), 0n, K.run0(one, 29n, Nil{})) : {Nat.add(Nat.mul(one, v(65)), C.shift(8n, Nat.add(Nat.mul(one, v(219)), C.shift(8n, Nat.add(Nat.mul(one, v(1)), C.shift(8n, _)))))) == S.a24(one) : Nat}  {==}def x25519_rel(+one: Nat, +h1: {one == 1n : Nat}, +pp: Nat, +hP: {Nat.add(1n+pp, 19n) == WD.sc(255n, one) : Nat}, +k: List<&2, U32>, +u: List<&2, U32>, +hk: {LM.okb(32n, k, 255n) == True{} : Bool}, +hu: {LM.okb(32n, u, 255n) == True{} : Bool}) -> {X.x25519_raw(k, u) == S.finish(1n+pp, S.ladder(one, 1n+pp, X.nbits(k), FS.value(X.clamp(k)), Nat.mod(S.decode_u(u), 1n+pp), S.LSt{1n, 0n, Nat.mod(S.decode_u(u), 1n+pp), 1n, 0n})) : List<&2, U32>}:  +P = {1n+pp : Nat}  +x1 = F.of_bytes(u)  +X1 = Nat.mod(S.decode_u(u), P)  +o1 = XB.mask_okb(31n, u, hu)  +c1 = G.c_trans(pp, FS.value(F.mask_top(u)), FS.value(S.mask_last(u)), X1, G.c_eq(pp, FS.value(F.mask_top(u)), FS.value(S.mask_last(u)), Equal.cong(List<&2, U32>, Nat, z => FS.value(z), F.mask_top(u), S.mask_last(u), XB.mask_eq(u))), G.c_sym(pp, X1, FS.value(S.mask_last(u)), G.c_mod(pp, FS.value(S.mask_last(u)))))  +kc = X.clamp(k)  +hkc = LM.okb_lea(32n, kc, 255n, XB.clamp_okb(k, hk))  +hl = ladder_rel(one, h1, pp, hP, X.nbits(k), X.a24(), {==}, a24_valo(one), kc, hkc, x1, X1, o1, c1, X.St{F.one(), F.zero(), x1, F.one(), 0}, S.LSt{1n, 0n, X1, 1n, 0n}, (({==}, G.c_eq(pp, FS.value(F.one()), 1n, {==})), (({==}, G.c_eq(pp, FS.value(F.zero()), 0n, {==})), ((o1, c1), (({==}, G.c_eq(pp, FS.value(F.one()), 1n, {==})), ({==}, {==}))))))  finish_rel(one, h1, pp, hP, X.ladder(X.nbits(k), X.a24(), kc, x1, X.St{F.one(), F.zero(), x1, F.one(), 0}), S.ladder(one, P, X.nbits(k), FS.value(kc), X1, S.LSt{1n, 0n, X1, 1n, 0n}), hl)def x25519_value(+one: Nat, +h1: {one == 1n : Nat}, +k: List<&2, U32>, +u: List<&2, U32>, +hk: {FS.tight(k) == True{} : Bool}, +hu: {FS.tight(u) == True{} : Bool}) -> S.X25519.value(one, h1, k, u, hk, hu):  +pp = PR.pp_of(one)  +P = {1n+pp : Nat}  +X1 = Nat.mod(S.decode_u(u), P)  +st0 = {S.LSt{1n, 0n, X1, 1n, 0n} : S.LSt}  %Equal.sym(Nat, FS.prime(one), P, PR.prime_eq(one, h1)) : {X.x25519_raw(k, u) == S.x25519_p(one, _, k, u) : List<&2, U32>}  %XB.nbits_eq(k) : {X.x25519_raw(k, u) == S.finish(P, S.ladder(one, P, _, S.decode_scalar(k), X1, st0)) : List<&2, U32>}  %Equal.cong(List<&2, U32>, Nat, z => FS.value(z), X.clamp(k), S.clamp(k), XB.clamp_eq(k)) : {X.x25519_raw(k, u) == S.finish(P, S.ladder(one, P, X.nbits(k), _, X1, st0)) : List<&2, U32>}  x25519_rel(one, h1, pp, PR.hP(one, h1), k, u, LM.bytes_okb(32n, k, hk), LM.bytes_okb(32n, u, hu))