1	import Base
2	import ../../lib/common.bend as C
3	import ./field.bend as FS
4	import ../../../src/crypto/curve25519/x25519.bend as X
5	
6	# X25519, RFC 7748 section 5, over the natural numbers: a transcription of
7	# the RFC's decodeScalar25519, decodeUCoordinate, encodeUCoordinate and the
8	# Montgomery ladder pseudo-code, every operation mod p (FS.fadd, FS.fsub,
9	# FS.fmul, FS.finv). HACL*'s Spec.Curve25519 is the same transcription.
10	# `one` is the symbolic 1 of field.bend.
11	#
12	#   clause          statement
13	#   X25519.value    the implementation equals this specification on every
14	#                   pair of 32-byte strings (bytes below 256)
15	#   X25519.checked  the checked entry point: Some of it on valid input,
16	#                   None otherwise
17	
18	# decodeScalar25519's clamping: k[0] &= 248; k[31] &= 127; k[31] |= 64
19	def clamp_last(xs: List<&2, U32>) -> List<&2, U32>:
20	  match xs:
21	    case Nil{}:
22	      Nil{}
23	    case Con{x, xt}:
24	      match xt:
25	        case Nil{}:
26	          Con{U32.or(U32.and(x, 127), 64), Nil{}}
27	        case Con{y, yt}:
28	          Con{x, clamp_last(Con{y, yt})}
29	
30	def clamp(bs: List<&2, U32>) -> List<&2, U32>:
31	  match bs:
32	    case Nil{}:
33	      Nil{}
34	    case Con{b, bt}:
35	      clamp_last(Con{U32.and(b, 248), bt})
36	
37	def decode_scalar(bs: List<&2, U32>) -> Nat:
38	  FS.value(clamp(bs))
39	
40	# decodeUCoordinate: the last byte's top bit masked (bits = 255)
41	def mask_last(xs: List<&2, U32>) -> List<&2, U32>:
42	  match xs:
43	    case Nil{}:
44	      Nil{}
45	    case Con{x, xt}:
46	      match xt:
47	        case Nil{}:
48	          Con{U32.and(x, 127), Nil{}}
49	        case Con{y, yt}:
50	          Con{x, mask_last(Con{y, yt})}
51	
52	def decode_u(bs: List<&2, U32>) -> Nat:
53	  FS.value(mask_last(bs))
54	
55	# encodeUCoordinate: u mod p as 32 little-endian bytes
56	def le_bytes(n: Nat, +x: Nat) -> List<&2, U32>:
57	  match n:
58	    case 0n:
59	      Nil{}
60	    case 1n+m:
61	      Con{U32.from_nat(Nat.mod(x, 256n)), le_bytes(m, Nat.div(x, 256n))}
62	
63	def encode_u(+p: Nat, u: Nat) -> List<&2, U32>:
64	  le_bytes(32n, Nat.mod(u, p))
65	
66	# k_t = (k >> t) & 1
67	def kbit(+k: Nat, t: Nat) -> Nat:
68	  C.bit(C.high(t, k))
69	
70	# swap ^= k_t, on bits
71	def bxor(a: Nat, b: Nat) -> Nat:
72	  match a:
73	    case 0n:
74	      b
75	    case 1n+q:
76	      Nat.sub(1n, b)
77	
78	# cswap(swap, a, b), RFC 7748: (a, b) when swap is 0, (b, a) when it is 1;
79	# cs_fst and cs_snd are its two components
80	def cs_fst(swap: Nat, a: Nat, b: Nat) -> Nat:
81	  match swap:
82	    case 0n:
83	      a
84	    case 1n+q:
85	      b
86	
87	def cs_snd(swap: Nat, a: Nat, b: Nat) -> Nat:
88	  match swap:
89	    case 0n:
90	      b
91	    case 1n+q:
92	      a
93	
94	type LSt is Data:
95	  LSt{x2: Nat, z2: Nat, x3: Nat, z3: Nat, swap: Nat}
96	
97	# a24 = 121665
98	def a24(+one: Nat) -> Nat:
99	  FS.digits(one, [65n, 219n, 1n])
100	
101	def step(+one: Nat, +p: Nat, +x1: Nat, +x2: Nat, +z2: Nat, +x3: Nat, +z3: Nat, kt: Nat) -> LSt:
102	  +a = FS.fadd(p, x2, z2)
103	  +aa = FS.fmul(p, a, a)
104	  +b = FS.fsub(p, x2, z2)
105	  +bb = FS.fmul(p, b, b)
106	  +e = FS.fsub(p, aa, bb)
107	  +c = FS.fadd(p, x3, z3)
108	  +d = FS.fsub(p, x3, z3)
109	  +da = FS.fmul(p, d, a)
110	  +cb = FS.fmul(p, c, b)
111	  +s = FS.fadd(p, da, cb)
112	  +t = FS.fsub(p, da, cb)
113	  LSt{FS.fmul(p, aa, bb), FS.fmul(p, e, FS.fadd(p, aa, FS.fmul(p, e, a24(one)))), FS.fmul(p, s, s), FS.fmul(p, x1, FS.fmul(p, t, t)), kt}
114	
115	def rung(+one: Nat, +p: Nat, +x1: Nat, st: LSt, +kt: Nat) -> LSt:
116	  match st:
117	    case LSt{+x2, +z2, +x3, +z3, swap}:
118	      +sw = bxor(swap, kt)
119	      step(one, p, x1, cs_fst(sw, x2, x3), cs_fst(sw, z2, z3), cs_snd(sw, x2, x3), cs_snd(sw, z2, z3), kt)
120	
121	# for t = n - 1 down to 0
122	def ladder(+one: Nat, +p: Nat, n: Nat, +k: Nat, +x1: Nat, st: LSt) -> LSt:
123	  match n:
124	    case 0n:
125	      st
126	    case 1n+ +t:
127	      ladder(one, p, t, k, x1, rung(one, p, x1, st, kbit(k, t)))
128	
129	def finish(+p: Nat, st: LSt) -> List<&2, U32>:
130	  match st:
131	    case LSt{x2, z2, x3, z3, +swap}:
132	      encode_u(p, FS.fmul(p, cs_fst(swap, x2, x3), FS.finv(p, cs_fst(swap, z2, z3))))
133	
134	# RFC 7748's `bits` (255 for X25519) as 8 * len(k) - 1 of the 32-byte scalar
135	def bits(k: List<&2, U32>) -> Nat:
136	  Nat.sub(Nat.mul(8n, C.length(U32, k)), 1n)
137	
138	def x25519_p(+one: Nat, +p: Nat, +k: List<&2, U32>, u: List<&2, U32>) -> List<&2, U32>:
139	  +x1 = Nat.mod(decode_u(u), p)
140	  finish(p, ladder(one, p, bits(k), decode_scalar(k), x1, LSt{1n, 0n, x1, 1n, 0n}))
141	
142	def x25519(+one: Nat, k: List<&2, U32>, u: List<&2, U32>) -> List<&2, U32>:
143	  x25519_p(one, FS.prime(one), k, u)
144	
145	# ---- clauses ----
146	
147	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}) -> Type:
148	  {X.x25519_raw(k, u) == x25519(one, k, u) : List<&2, U32>}
149	
150	def X25519.checked(+one: Nat, +h1: {one == 1n : Nat}, +k: List<&2, U32>, +u: List<&2, U32>) -> Type:
151	  {X.x25519(k, u) == Bool.pick(Maybe<&2, List<&2, U32>>, Bool.and(FS.tight(k), FS.tight(u)), Some{x25519(one, k, u)}, None{}) : Maybe<&2, List<&2, U32>>}