~/jendhub

proofs/crypto/curve25519/proof.bend

bend-collections-laws-crypto@1.0.0.0 · 214 lines · 42 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/spec/crypto/kex.bend as SK
6import bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/field.bend as F
7import bend-collections-laws-crypto@1.0.0.0/src/crypto/curve25519/x25519.bend as X
8import bend-collections-laws-crypto@1.0.0.0/src/crypto/kex.bend as K
9import bend-collections-laws-crypto@1.0.0.0/proofs/lib/nat.bend as N
10import bend-collections-laws-crypto@1.0.0.0/proofs/lib/logic.bend as L
11import bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend as WD
12import bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32.bend as U
13import bend-collections-laws-crypto@1.0.0.0/proofs/math/natural/arith.bend as NR
14import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/limbs.bend as LM
15import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/fieldops.bend as FO
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/canon.bend as CN
19import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/eqf.bend as EQ
20import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/xbits.bend as XB
21import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/ladder.bend as LD
22import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/prime.bend as PR
23import bend-collections-laws-crypto@1.0.0.0/proofs/crypto/curve25519/cong.bend as G
24
25# Gate for GF(2^255 - 19), X25519 and the key-exchange facade:
26# `bend proofs/crypto/curve25519/proof.bend` checks every clause of
27# spec/crypto/curve25519/field.bend, spec/crypto/curve25519/x25519.bend and
28# spec/crypto/kex.bend, for every input.
29
30def v(+x: U32) -> Nat:
31  U32.to_nat(x)
32
33def pp1(+one: Nat) -> Nat:
34  PR.pp_of(one)
35
36def ok(+a: List<&2, U32>, +h: {FS.tight(a) == True{} : Bool}) -> {LM.okb(32n, a, 255n) == True{} : Bool}:
37  LM.bytes_okb(32n, a, h)
38
39def tight_of(+a: List<&2, U32>, +h: {LM.okb(32n, a, 255n) == True{} : Bool}) -> {FS.tight(a) == True{} : Bool}:
40  LM.okb_bytes(32n, a, h)
41
42# a statement about p = 1 + pp, restated about FS.prime(one)
43def at_p(+one: Nat, +h1: {one == 1n : Nat}, -M: Nat -> Type, pf: M(1n+pp1(one))) -> M(FS.prime(one)):
44  L.subst(Nat, M, 1n+pp1(one), FS.prime(one), Equal.sym(Nat, FS.prime(one), 1n+pp1(one), PR.prime_eq(one, h1)), pf)
45
46# ---- field clauses ----
47
48def add_value(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, U32>, +b: List<&2, U32>, +ha: {FS.tight(a) == True{} : Bool}, +hb: {FS.tight(b) == True{} : Bool}) -> FS.Add.value(one, h1, a, b, ha, hb):
49  at_p(one, h1, z => {Nat.mod(FS.value(F.add(a, b)), z) == FS.fadd(z, FS.value(a), FS.value(b)) : Nat}, FO.add_mod(one, h1, pp1(one), PR.hP(one, h1), a, b, ok(a, ha), ok(b, hb)))
50
51def add_tight(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, U32>, +b: List<&2, U32>, +ha: {FS.tight(a) == True{} : Bool}, +hb: {FS.tight(b) == True{} : Bool}) -> FS.Add.tight(one, h1, a, b, ha, hb):
52  tight_of(F.add(a, b), FO.add_okb(one, h1, a, b, ok(a, ha), ok(b, hb)))
53
54def sub_value(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, U32>, +b: List<&2, U32>, +ha: {FS.tight(a) == True{} : Bool}, +hb: {FS.tight(b) == True{} : Bool}) -> FS.Sub.value(one, h1, a, b, ha, hb):
55  at_p(one, h1, z => {Nat.mod(FS.value(F.sub(a, b)), z) == FS.fsub(z, FS.value(a), FS.value(b)) : Nat}, FO.sub_mod(one, h1, pp1(one), PR.hP(one, h1), a, b, ok(a, ha), ok(b, hb)))
56
57def sub_tight(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, U32>, +b: List<&2, U32>, +ha: {FS.tight(a) == True{} : Bool}, +hb: {FS.tight(b) == True{} : Bool}) -> FS.Sub.tight(one, h1, a, b, ha, hb):
58  tight_of(F.sub(a, b), FO.sub_okb(one, h1, a, b, ok(a, ha), ok(b, hb)))
59
60def mul_value(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, U32>, +b: List<&2, U32>, +ha: {FS.tight(a) == True{} : Bool}, +hb: {FS.tight(b) == True{} : Bool}) -> FS.Mul.value(one, h1, a, b, ha, hb):
61  at_p(one, h1, z => {Nat.mod(FS.value(F.mul(a, b)), z) == FS.fmul(z, FS.value(a), FS.value(b)) : Nat}, MW.mul_mod(one, h1, pp1(one), PR.hP(one, h1), a, b, ok(a, ha), ok(b, hb)))
62
63def mul_tight(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, U32>, +b: List<&2, U32>, +ha: {FS.tight(a) == True{} : Bool}, +hb: {FS.tight(b) == True{} : Bool}) -> FS.Mul.tight(one, h1, a, b, ha, hb):
64  tight_of(F.mul(a, b), MW.mul_okb(one, h1, a, b, ok(a, ha), ok(b, hb)))
65
66def sq_value(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, U32>, +ha: {FS.tight(a) == True{} : Bool}) -> FS.Sq.value(one, h1, a, ha):
67  at_p(one, h1, z => {Nat.mod(FS.value(F.sq(a)), z) == FS.fmul(z, FS.value(a), FS.value(a)) : Nat}, MW.sq_mod(one, h1, pp1(one), PR.hP(one, h1), a, ok(a, ha)))
68
69def sq_tight(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, U32>, +ha: {FS.tight(a) == True{} : Bool}) -> FS.Sq.tight(one, h1, a, ha):
70  tight_of(F.sq(a), MW.sq_okb(one, h1, a, ok(a, ha)))
71
72def mul_small_value(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, U32>, +k: U32, +ha: {FS.tight(a) == True{} : Bool}, +hk: {Nat.is_lt(U32.to_nat(k), C.shift(17n, one)) == True{} : Bool}) -> FS.MulSmall.value(one, h1, a, k, ha, hk):
73  at_p(one, h1, z => {Nat.mod(FS.value(F.mul_small(a, k)), z) == FS.fmul(z, FS.value(a), U32.to_nat(k)) : Nat}, MW.mul_small_mod(one, h1, pp1(one), PR.hP(one, h1), a, k, ok(a, ha), N.lt_le(v(k), WD.sc(17n, one), hk)))
74
75def mul_small_tight(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, U32>, +k: U32, +ha: {FS.tight(a) == True{} : Bool}, +hk: {Nat.is_lt(U32.to_nat(k), C.shift(17n, one)) == True{} : Bool}) -> FS.MulSmall.tight(one, h1, a, k, ha, hk):
76  tight_of(F.mul_small(a, k), MW.mul_small_okb(one, h1, a, k, ok(a, ha), N.lt_le(v(k), WD.sc(17n, one), hk)))
77
78def select_zero(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, U32>, +b: List<&2, U32>, +ha: {FS.tight(a) == True{} : Bool}, +hb: {FS.tight(b) == True{} : Bool}) -> FS.Select.zero(one, h1, a, b, ha, hb):
79  FO.select0(one, h1, 32n, a, b, ok(a, ha), ok(b, hb))
80
81def select_one(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, U32>, +b: List<&2, U32>, +ha: {FS.tight(a) == True{} : Bool}, +hb: {FS.tight(b) == True{} : Bool}) -> FS.Select.one(one, h1, a, b, ha, hb):
82  FO.select1(one, h1, 32n, a, b, ok(a, ha), ok(b, hb))
83
84def inv_value(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, U32>, +ha: {FS.tight(a) == True{} : Bool}) -> FS.Inv.value(one, h1, a, ha):
85  +pp = pp1(one)
86  +e = G.c_trans(pp, FS.value(F.inv(a)), Nat.pow(FS.value(a), Nat.sub(1n+pp, 2n)), FS.finv(1n+pp, FS.value(a)), PW.inv_val(one, h1, pp, PR.hP(one, h1), a, ok(a, ha)), G.c_sym(pp, FS.finv(1n+pp, FS.value(a)), Nat.pow(FS.value(a), Nat.sub(1n+pp, 2n)), G.c_mod(pp, Nat.pow(FS.value(a), Nat.sub(1n+pp, 2n)))))
87  at_p(one, h1, z => {Nat.mod(FS.value(F.inv(a)), z) == FS.finv(z, FS.value(a)) : Nat}, Equal.trans(Nat, Nat.mod(FS.value(F.inv(a)), 1n+pp), Nat.mod(FS.finv(1n+pp, FS.value(a)), 1n+pp), FS.finv(1n+pp, FS.value(a)), e, NR.mod_mod(pp, Nat.pow(FS.value(a), Nat.sub(1n+pp, 2n)))))
88
89def inv_tight(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, U32>, +ha: {FS.tight(a) == True{} : Bool}) -> FS.Inv.tight(one, h1, a, ha):
90  tight_of(F.inv(a), PW.inv_okb(one, h1, a, ok(a, ha)))
91
92def p58_value(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, U32>, +ha: {FS.tight(a) == True{} : Bool}) -> FS.PowP58.value(one, h1, a, ha):
93  +pp = pp1(one)
94  +k = Nat.div(Nat.sub(1n+pp, 5n), 8n)
95  +e = G.c_trans(pp, FS.value(F.pow_p58(a)), Nat.pow(FS.value(a), k), FS.fpow(1n+pp, FS.value(a), k), PW.p58_val(one, h1, pp, PR.hP(one, h1), a, ok(a, ha)), G.c_sym(pp, FS.fpow(1n+pp, FS.value(a), k), Nat.pow(FS.value(a), k), G.c_mod(pp, Nat.pow(FS.value(a), k))))
96  at_p(one, h1, z => {Nat.mod(FS.value(F.pow_p58(a)), z) == FS.fpow(z, FS.value(a), Nat.div(Nat.sub(z, 5n), 8n)) : Nat}, Equal.trans(Nat, Nat.mod(FS.value(F.pow_p58(a)), 1n+pp), Nat.mod(FS.fpow(1n+pp, FS.value(a), k), 1n+pp), FS.fpow(1n+pp, FS.value(a), k), e, NR.mod_mod(pp, Nat.pow(FS.value(a), k))))
97
98def p58_tight(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, U32>, +ha: {FS.tight(a) == True{} : Bool}) -> FS.PowP58.tight(one, h1, a, ha):
99  tight_of(F.pow_p58(a), PW.p58_okb(one, h1, a, ok(a, ha)))
100
101def freeze_value(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, U32>, +ha: {FS.tight(a) == True{} : Bool}) -> FS.Freeze.value(one, h1, a, ha):
102  at_p(one, h1, z => {FS.value(F.freeze(a)) == Nat.mod(FS.value(a), z) : Nat}, CN.freeze_val(one, h1, pp1(one), PR.hP(one, h1), a, ok(a, ha)))
103
104def freeze_tight(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, U32>, +ha: {FS.tight(a) == True{} : Bool}) -> FS.Freeze.tight(one, h1, a, ha):
105  tight_of(F.freeze(a), CN.freeze_okb(one, h1, pp1(one), PR.hP(one, h1), a, ok(a, ha)))
106
107def of_bytes_tight(+one: Nat, +h1: {one == 1n : Nat}, +bs: List<&2, U32>, +hb: {FS.tight(bs) == True{} : Bool}) -> FS.OfBytes.tight(one, h1, bs, hb):
108  tight_of(F.of_bytes(bs), XB.mask_okb(31n, bs, ok(bs, hb)))
109
110def eq_value(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, U32>, +b: List<&2, U32>, +ha: {FS.tight(a) == True{} : Bool}, +hb: {FS.tight(b) == True{} : Bool}) -> FS.Eq.value(one, h1, a, b, ha, hb):
111  at_p(one, h1, z => {F.eq(a, b) == Nat.is_eq(Nat.mod(FS.value(a), z), Nat.mod(FS.value(b), z)) : Bool}, EQ.eq_val(one, h1, pp1(one), PR.hP(one, h1), a, b, ok(a, ha), ok(b, hb)))
112
113def is_zero_value(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, U32>, +ha: {FS.tight(a) == True{} : Bool}) -> FS.IsZero.value(one, h1, a, ha):
114  at_p(one, h1, z => {F.is_zero(a) == Nat.is_eq(Nat.mod(FS.value(a), z), 0n) : Bool}, CN.is_zero_val(one, h1, pp1(one), PR.hP(one, h1), a, ok(a, ha)))
115
116def parity_value(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, U32>, +ha: {FS.tight(a) == True{} : Bool}) -> FS.Parity.value(one, h1, a, ha):
117  at_p(one, h1, z => {U32.to_nat(F.parity(a)) == Nat.mod(Nat.mod(FS.value(a), z), 2n) : Nat}, CN.parity_val(one, h1, pp1(one), PR.hP(one, h1), a, ok(a, ha)))
118
119# ---- X25519 ----
120
121def 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):
122  LD.x25519_value(one, h1, k, u, hk, hu)
123
124def valid_eq(+n: Nat, +xs: List<&2, U32>) -> {X.valid_bytes(n, xs) == FS.bytes_ok(n, xs) : Bool}:
125  match n xs:
126    case 0n Nil{}:
127      {==}
128    case 0n Con{y, yt}:
129      {==}
130    case 1n+m Nil{}:
131      {==}
132    case 1n+ +m Con{+y, +yt}:
133      +e1 = U.is_lt_nat(y, 256)
134      +e2 = valid_eq(m, yt)
135      Equal.trans(Bool, Bool.and(U32.is_lt(y, 256), X.valid_bytes(m, yt)), Bool.and(Nat.is_lt(v(y), 256n), X.valid_bytes(m, yt)), Bool.and(Nat.is_lt(v(y), 256n), FS.bytes_ok(m, yt)), Equal.cong(Bool, Bool, z => Bool.and(z, X.valid_bytes(m, yt)), U32.is_lt(y, 256), Nat.is_lt(v(y), 256n), e1), Equal.cong(Bool, Bool, z => Bool.and(Nat.is_lt(v(y), 256n), z), X.valid_bytes(m, yt), FS.bytes_ok(m, yt), e2))
136
137def checked_by(+one: Nat, +h1: {one == 1n : Nat}, +k: List<&2, U32>, +u: List<&2, U32>, +b1: Bool, +e1: {FS.tight(k) == b1 : Bool}, +b2: Bool, +e2: {FS.tight(u) == b2 : Bool}) -> {X.x25519_if(Bool.and(b1, b2), k, u) == Bool.pick(Maybe<&2, List<&2, U32>>, Bool.and(b1, b2), Some{S.x25519(one, k, u)}, None{}) : Maybe<&2, List<&2, U32>>}:
138  match b1 b2:
139    case True{} True{}:
140      Equal.cong(List<&2, U32>, Maybe<&2, List<&2, U32>>, z => Some{z}, X.x25519_raw(k, u), S.x25519(one, k, u), x25519_value(one, h1, k, u, e1, e2))
141    case True{} False{}:
142      {==}
143    case False{} _:
144      {==}
145
146def x25519_checked(+one: Nat, +h1: {one == 1n : Nat}, +k: List<&2, U32>, +u: List<&2, U32>) -> S.X25519.checked(one, h1, k, u):
147  %Equal.sym(Bool, X.valid_bytes(32n, k), FS.tight(k), valid_eq(32n, k)) : {X.x25519_if(Bool.and(_, X.valid_bytes(32n, u)), k, u) == Bool.pick(Maybe<&2, List<&2, U32>>, Bool.and(FS.tight(k), FS.tight(u)), Some{S.x25519(one, k, u)}, None{}) : Maybe<&2, List<&2, U32>>}
148  %Equal.sym(Bool, X.valid_bytes(32n, u), FS.tight(u), valid_eq(32n, u)) : {X.x25519_if(Bool.and(FS.tight(k), _), k, u) == Bool.pick(Maybe<&2, List<&2, U32>>, Bool.and(FS.tight(k), FS.tight(u)), Some{S.x25519(one, k, u)}, None{}) : Maybe<&2, List<&2, U32>>}
149  checked_by(one, h1, k, u, FS.tight(k), {==}, FS.tight(u), {==})
150
151# ---- the key-exchange facade ----
152
153def le_bytes_ok(+n: Nat, +x: Nat) -> {FS.bytes_ok(n, S.le_bytes(n, x)) == True{} : Bool}:
154  match n:
155    case 0n:
156      {==}
157    case 1n+ +m:
158      +r = Nat.mod(x, 256n)
159      +hr = NR.dm_lt(255n, x)
160      +e = U.to_nat_from_nat(r, 8n, {==}, hr)
161      +h = L.subst(Nat, z => {Nat.is_lt(z, 256n) == True{} : Bool}, r, v(U32.from_nat(r)), Equal.sym(Nat, v(U32.from_nat(r)), r, e), hr)
162      L.and_intro(Nat.is_lt(v(U32.from_nat(r)), 256n), FS.bytes_ok(m, S.le_bytes(m, Nat.div(x, 256n))), h, le_bytes_ok(m, Nat.div(x, 256n)))
163
164def finish_tight(+p: Nat, +st: S.LSt) -> {FS.tight(S.finish(p, st)) == True{} : Bool}:
165  match st:
166    case S.LSt{+x2, +z2, +x3, +z3, +sw}:
167      le_bytes_ok(32n, Nat.mod(FS.fmul(p, S.cs_fst(sw, x2, x3), FS.finv(p, S.cs_fst(sw, z2, z3))), p))
168
169def spec_tight(+one: Nat, +k: List<&2, U32>, +u: List<&2, U32>) -> {FS.tight(S.x25519(one, k, u)) == True{} : Bool}:
170  +p = FS.prime(one)
171  +x1 = Nat.mod(S.decode_u(u), p)
172  finish_tight(p, S.ladder(one, p, S.bits(k), S.decode_scalar(k), x1, S.LSt{1n, 0n, x1, 1n, 0n}))
173
174def zero_eq(+one: Nat, +h1: {one == 1n : Nat}, +ss: List<&2, U32>, +hs: {LM.okb(32n, ss, 255n) == True{} : Bool}) -> {U32.is_eq(F.sum_all(ss, 0), 0) == Nat.is_eq(FS.value(ss), 0n) : Bool}:
175  +e1 = CN.u32_iz(F.sum_all(ss, 0))
176  +e2 = Equal.cong(Nat, Bool, z => Nat.is_eq(z, 0n), v(F.sum_all(ss, 0)), CN.sumv(ss), CN.sum_v(one, h1, 32n, ss, 0, hs, CN.cb32_lt(one, h1)))
177  Equal.trans(Bool, U32.is_eq(F.sum_all(ss, 0), 0), Nat.is_eq(v(F.sum_all(ss, 0)), 0n), Nat.is_eq(FS.value(ss), 0n), e1, Equal.trans(Bool, Nat.is_eq(v(F.sum_all(ss, 0)), 0n), Nat.is_eq(CN.sumv(ss), 0n), Nat.is_eq(FS.value(ss), 0n), e2, CN.iz_sum(ss)))
178
179def base_eq() -> {X.base() == SK.base() : List<&2, U32>}:
180  {==}
181
182def base_tight() -> {FS.tight(X.base()) == True{} : Bool}:
183  {==}
184
185def kex_public(+one: Nat, +h1: {one == 1n : Nat}, +seed: List<&2, U32>, +hs: {FS.tight(seed) == True{} : Bool}) -> SK.Kex.public(one, h1, seed, hs):
186  e = x25519_checked(one, h1, seed, X.base())
187  %Equal.sym(Maybe<&2, List<&2, U32>>, X.x25519(seed, X.base()), Bool.pick(Maybe<&2, List<&2, U32>>, Bool.and(FS.tight(seed), FS.tight(X.base())), Some{S.x25519(one, seed, X.base())}, None{}), e) : {K.keypair_of(seed, _) == Some{K.Keypair{seed, S.x25519(one, seed, SK.base())}} : Maybe<&2, K.Keypair>}
188  %Equal.sym(Bool, FS.tight(seed), True{}, hs) : {K.keypair_of(seed, Bool.pick(Maybe<&2, List<&2, U32>>, Bool.and(_, FS.tight(X.base())), Some{S.x25519(one, seed, X.base())}, None{})) == Some{K.Keypair{seed, S.x25519(one, seed, SK.base())}} : Maybe<&2, K.Keypair>}
189  {==}
190
191def nz_eq(+ss: List<&2, U32>, +z: Bool) -> {K.nonzero(ss, z) == SK.unless_zero(ss, z) : Maybe<&2, List<&2, U32>>}:
192  match z:
193    case True{}:
194      {==}
195    case False{}:
196      {==}
197
198def shared_by(+one: Nat, +h1: {one == 1n : Nat}, +ss: List<&2, U32>, +hs: {FS.tight(ss) == True{} : Bool}) -> {K.shared_of(Some{ss}) == SK.unless_zero(ss, Nat.is_eq(FS.value(ss), 0n)) : Maybe<&2, List<&2, U32>>}:
199  +e1 = zero_eq(one, h1, ss, ok(ss, hs))
200  %Equal.sym(Bool, U32.is_eq(F.sum_all(ss, 0), 0), Nat.is_eq(FS.value(ss), 0n), e1) : {K.nonzero(ss, _) == SK.unless_zero(ss, Nat.is_eq(FS.value(ss), 0n)) : Maybe<&2, List<&2, U32>>}
201  nz_eq(ss, Nat.is_eq(FS.value(ss), 0n))
202
203def kex_shared(+one: Nat, +h1: {one == 1n : Nat}, +sk: List<&2, U32>, +pk: List<&2, U32>, +hs: {FS.tight(sk) == True{} : Bool}, +hp: {FS.tight(pk) == True{} : Bool}) -> SK.Kex.shared(one, h1, sk, pk, hs, hp):
204  e = x25519_checked(one, h1, sk, pk)
205  %Equal.sym(Maybe<&2, List<&2, U32>>, X.x25519(sk, pk), Bool.pick(Maybe<&2, List<&2, U32>>, Bool.and(FS.tight(sk), FS.tight(pk)), Some{S.x25519(one, sk, pk)}, None{}), e) : {K.shared_of(_) == SK.unless_zero(S.x25519(one, sk, pk), Nat.is_eq(FS.value(S.x25519(one, sk, pk)), 0n)) : Maybe<&2, List<&2, U32>>}
206  %Equal.sym(Bool, FS.tight(sk), True{}, hs) : {K.shared_of(Bool.pick(Maybe<&2, List<&2, U32>>, Bool.and(_, FS.tight(pk)), Some{S.x25519(one, sk, pk)}, None{})) == SK.unless_zero(S.x25519(one, sk, pk), Nat.is_eq(FS.value(S.x25519(one, sk, pk)), 0n)) : Maybe<&2, List<&2, U32>>}
207  %Equal.sym(Bool, FS.tight(pk), True{}, hp) : {K.shared_of(Bool.pick(Maybe<&2, List<&2, U32>>, Bool.and(True{}, _), Some{S.x25519(one, sk, pk)}, None{})) == SK.unless_zero(S.x25519(one, sk, pk), Nat.is_eq(FS.value(S.x25519(one, sk, pk)), 0n)) : Maybe<&2, List<&2, U32>>}
208  shared_by(one, h1, S.x25519(one, sk, pk), spec_tight(one, sk, pk))
209
210def kex_reject(+sk: List<&2, U32>, +pk: List<&2, U32>, +h: {Bool.and(FS.tight(sk), FS.tight(pk)) == False{} : Bool}) -> SK.Kex.reject(sk, pk, h):
211  %Equal.sym(Bool, X.valid_bytes(32n, sk), FS.tight(sk), valid_eq(32n, sk)) : {K.shared_of(X.x25519_if(Bool.and(_, X.valid_bytes(32n, pk)), sk, pk)) == None{} : Maybe<&2, List<&2, U32>>}
212  %Equal.sym(Bool, X.valid_bytes(32n, pk), FS.tight(pk), valid_eq(32n, pk)) : {K.shared_of(X.x25519_if(Bool.and(FS.tight(sk), _), sk, pk)) == None{} : Maybe<&2, List<&2, U32>>}
213  %Equal.sym(Bool, Bool.and(FS.tight(sk), FS.tight(pk)), False{}, h) : {K.shared_of(X.x25519_if(_, sk, pk)) == None{} : Maybe<&2, List<&2, U32>>}
214  {==}