1 import Base 2 import ../../../spec/lib/common.bend as C 3 import ../../../spec/crypto/curve25519/field.bend as FS 4 import ../../../spec/crypto/curve25519/x25519.bend as S 5 import ../../../src/crypto/curve25519/field.bend as F 6 import ../../../src/crypto/curve25519/x25519.bend as X 7 import ../../lib/nat.bend as N 8 import ../../lib/logic.bend as L 9 import ../../lib/word.bend as WD 10 import ./limbs.bend as LM 11 import ./consts.bend as K 12 import ./fieldops.bend as FO 13 import ./canon.bend as CN 14 import ./cong.bend as G 15 import ./rel.bend as RL 16 import ./mulw.bend as MW 17 import ./pow.bend as PW 18 import ./xbits.bend as XB 19 import ./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 26 def v(+x: U32) -> Nat: 27 U32.to_nat(x) 28 29 def DP(-A: Data, -B: Data) -> Data: 30 Sigma<&2, &2, A, _ => B> 31 32 def 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 39 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}: 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 52 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)): 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 65 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)): 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 80 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)): 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 83 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)): 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 153 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)): 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 177 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)): 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 188 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>}: 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 227 def a24_shape() -> {X.a24() == Con{65, Con{219, Con{1, K.rep(29n, 0, Nil{})}}} : List<&2, U32>}: 228 {==} 229 230 def 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 235 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>}: 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 246 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): 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))