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 ../../../spec/crypto/kex.bend as SK
6	import ../../../src/crypto/curve25519/field.bend as F
7	import ../../../src/crypto/curve25519/x25519.bend as X
8	import ../../../src/crypto/kex.bend as K
9	import ../../lib/nat.bend as N
10	import ../../lib/logic.bend as L
11	import ../../lib/word.bend as WD
12	import ../../lib/u32.bend as U
13	import ../../math/natural/arith.bend as NR
14	import ./limbs.bend as LM
15	import ./fieldops.bend as FO
16	import ./mulw.bend as MW
17	import ./pow.bend as PW
18	import ./canon.bend as CN
19	import ./eqf.bend as EQ
20	import ./xbits.bend as XB
21	import ./ladder.bend as LD
22	import ./prime.bend as PR
23	import ./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	
30	def v(+x: U32) -> Nat:
31	  U32.to_nat(x)
32	
33	def pp1(+one: Nat) -> Nat:
34	  PR.pp_of(one)
35	
36	def 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	
39	def 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)
43	def 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	
48	def 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	
51	def 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	
54	def 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	
57	def 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	
60	def 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	
63	def 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	
66	def 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	
69	def 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	
72	def 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	
75	def 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	
78	def 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	
81	def 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	
84	def 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	
89	def 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	
92	def 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	
98	def 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	
101	def 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	
104	def 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	
107	def 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	
110	def 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	
113	def 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	
116	def 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	
121	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):
122	  LD.x25519_value(one, h1, k, u, hk, hu)
123	
124	def 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	
137	def 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	
146	def 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	
153	def 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	
164	def 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	
169	def 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	
174	def 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	
179	def base_eq() -> {X.base() == SK.base() : List<&2, U32>}:
180	  {==}
181	
182	def base_tight() -> {FS.tight(X.base()) == True{} : Bool}:
183	  {==}
184	
185	def 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	
191	def 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	
198	def 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	
203	def 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	
210	def 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	  {==}