~/jendhub

proofs/crypto/curve25519/ladder.bend

bend-collections-laws-crypto@1.0.0.0 · 254 lines · 15 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/spec/lib/common.bend as C
3import bend-collections-laws-crypto@1.0.0.0/spec/crypto/curve25519/field.bend as FS
4import bend-collections-laws-crypto@1.0.0.0/spec/crypto/curve25519/x25519.bend as S
5import bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/field.bend as F
6import bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/x25519.bend as X
7import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
8import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
9import bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend as WD
10import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend as LM
11import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/consts.bend as K
12import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/fieldops.bend as FO
13import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/canon.bend as CN
14import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/cong.bend as G
15import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/rel.bend as RL
16import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/mulw.bend as MW
17import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/pow.bend as PW
18import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/xbits.bend as XB
19import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/prime.bend as PR
20
21# X25519 == RFC 7748 (spec/crypto/curve25519/x25519.bend): the ladder state
22# of the implementation is related to the specification's state field by
23# field (RL.R), the swap bit is equal; every rung keeps the relation; the
24# final cswap, inversion, product and encoding give the same bytes.
25
26def v(+x: U32) -> Nat:
27  U32.to_nat(x)
28
29def DP(-A: Data, -B: Data) -> Data:
30  Sigma<&2, &2, A, _ => B>
31
32def Rst(+pp: Nat, st: X.St, sst: S.LSt) -> Data:
33  match st sst:
34    case X.St{x2, z2, x3, z3, sw} S.LSt{a2, b2, a3, b3, sws}:
35      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})))))
36
37# ---- conditional swaps ----
38
39def 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}:
40  match s:
41    case 0n:
42      %Equal.sym(U32, sw, 0, XB.u0(sw, hs)) : {LM.okb(32n, F.select(_, a, b), 255n) == True{} : Bool}
43      %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}
44      oa
45    case 1n:
46      %Equal.sym(U32, sw, 1, XB.u1(sw, hs)) : {LM.okb(32n, F.select(_, a, b), 255n) == True{} : Bool}
47      %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}
48      ob
49    case 2n+q:
50      Empty.absurd({LM.okb(32n, F.select(sw, a, b), 255n) == True{} : Bool}, L.false_true(hb))
51
52def 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)):
53  match s:
54    case 0n:
55      %Equal.sym(U32, sw, 0, XB.u0(sw, hs)) : G.ceq(pp, FS.value(F.select(_, a, b)), A)
56      %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)
57      ca
58    case 1n:
59      %Equal.sym(U32, sw, 1, XB.u1(sw, hs)) : G.ceq(pp, FS.value(F.select(_, a, b)), B)
60      %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)
61      cb
62    case 2n+q:
63      Empty.absurd(G.ceq(pp, FS.value(F.select(sw, a, b)), B), L.false_true(hb))
64
65def 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)):
66  match s:
67    case 0n:
68      %Equal.sym(U32, sw, 0, XB.u0(sw, hs)) : G.ceq(pp, FS.value(F.select(_, b, a)), B)
69      %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)
70      cb
71    case 1n:
72      %Equal.sym(U32, sw, 1, XB.u1(sw, hs)) : G.ceq(pp, FS.value(F.select(_, b, a)), A)
73      %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)
74      ca
75    case 2n+q:
76      Empty.absurd(G.ceq(pp, FS.value(F.select(sw, b, a)), A), L.false_true(hb))
77
78# ---- one step ----
79
80def 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)):
81  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))
82
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)))))
150
151# ---- one rung: swap ^= k_t, cswap, step ----
152
153def 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)):
154  match st sst:
155    case X.St{+x2, +z2, +x3, +z3, +sw} S.LSt{+a2, +b2, +a3, +b3, +sws}:
156      (+r2, +h2) = h
157      (+rz2, +h3) = h2
158      (+r3, +h4) = h3
159      (+rz3, +h5) = h4
160      (+hs, +hsb) = h5
161      +o2 = RL.r_o(pp, x2, a2, r2)
162      +c2 = RL.r_c(pp, x2, a2, r2)
163      +oz2 = RL.r_o(pp, z2, b2, rz2)
164      +cz2 = RL.r_c(pp, z2, b2, rz2)
165      +o3 = RL.r_o(pp, x3, a3, r3)
166      +c3 = RL.r_c(pp, x3, a3, r3)
167      +oz3 = RL.r_o(pp, z3, b3, rz3)
168      +cz3 = RL.r_c(pp, z3, b3, rz3)
169      +w = U32.xor(sw, kt)
170      +W = S.bxor(sws, KT)
171      +hw = XB.xor_bits(sw, kt, sws, KT, hs, hk, hsb, hkb)
172      +hwb = XB.bxor_le(sws, KT, hkb)
173      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)
174
175# ---- the ladder ----
176
177def 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)):
178  match n:
179    case 0n:
180      h
181    case 1n+ +t:
182      +kt = X.kbit(kc, t)
183      +KT = S.kbit(FS.value(kc), t)
184      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)))
185
186# ---- the end: cswap, x2 / z2, encode ----
187
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))
224
225# ---- X25519 ----
226
227def a24_shape() -> {X.a24() == Con{65, Con{219, Con{1, K.rep(29n, 0, Nil{})}}} : List<&2, U32>}:
228  {==}
229
230def a24_valo(+one: Nat) -> {K.valo(one, X.a24()) == S.a24(one) : Nat}:
231  %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}
232  %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}
233  {==}
234
235def 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>}:
236  +P = {1n+pp : Nat}
237  +x1 = F.of_bytes(u)
238  +X1 = Nat.mod(S.decode_u(u), P)
239  +o1 = XB.mask_okb(31n, u, hu)
240  +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)))))
241  +kc = X.clamp(k)
242  +hkc = LM.okb_lea(32n, kc, 255n, XB.clamp_okb(k, hk))
243  +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, {==})), ({==}, {==}))))))
244  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)
245
246def 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):
247  +pp = PR.pp_of(one)
248  +P = {1n+pp : Nat}
249  +X1 = Nat.mod(S.decode_u(u), P)
250  +st0 = {S.LSt{1n, 0n, X1, 1n, 0n} : S.LSt}
251  %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>}
252  %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>}
253  %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>}
254  x25519_rel(one, h1, pp, PR.hP(one, h1), k, u, LM.bytes_okb(32n, k, hk), LM.bytes_okb(32n, u, hu))