1	import Base
2	import ../../lib/common.bend as C
3	import ../../../src/crypto/curve25519/field.bend as F
4	
5	# GF(p), p = 2^255 - 19, over the natural numbers, and the contract of
6	# src/crypto/curve25519/field.bend.
7	#
8	# The checker keeps every closed natural number it compares in unary, so
9	# 2^255 is never written closed: it is C.shift(255n, one), with `one` a
10	# variable that every clause takes together with the hypothesis
11	# {one == 1n : Nat}. For one == 1 these are the usual constants; no other
12	# value of `one` satisfies the hypothesis, so each clause says exactly what
13	# it says with the constants written out. (The same device as the proofs of
14	# spec/math/w64.bend, which keep 2^32 as a shift of a symbolic one.)
15	#
16	# Representation: a field element is a list of U32 limbs, little-endian in
17	# radix 2^8 (value = RFC 7748's decodeLittleEndian); "tight" is 32 limbs,
18	# each below 2^8, which is also a 32-byte string.
19	#
20	#   function          clauses
21	#   add               Add.value, Add.tight
22	#   sub               Sub.value, Sub.tight
23	#   mul, sq           Mul.value, Mul.tight, Sq.value, Sq.tight
24	#   mul_small         MulSmall.value, MulSmall.tight
25	#   select            Select.zero, Select.one
26	#   inv               Inv.value, Inv.tight
27	#   pow_p58           PowP58.value, PowP58.tight
28	#   freeze, to_bytes  Freeze.value (the canonical representative), Freeze.tight
29	#   of_bytes          OfBytes.tight (its value is covered by X25519.value)
30	#   eq, is_zero       Eq.value, IsZero.value
31	#   parity            Parity.value
32	
33	# decodeLittleEndian (RFC 7748 section 5): sum of b_i 2^(8 i)
34	def value(xs: List<&2, U32>) -> Nat:
35	  match xs:
36	    case Nil{}:
37	      0n
38	    case Con{h, t}:
39	      Nat.add(U32.to_nat(h), C.shift(8n, value(t)))
40	
41	# n values, each below 2^8
42	def bytes_ok(n: Nat, xs: List<&2, U32>) -> Bool:
43	  match n:
44	    case 0n:
45	      match xs:
46	        case Nil{}:
47	          True{}
48	        case Con{x, xt}:
49	          False{}
50	    case 1n+m:
51	      match xs:
52	        case Nil{}:
53	          False{}
54	        case Con{x, xt}:
55	          Bool.and(Nat.is_lt(U32.to_nat(x), 256n), bytes_ok(m, xt))
56	
57	def tight(xs: List<&2, U32>) -> Bool:
58	  bytes_ok(32n, xs)
59	
60	# a constant from its little-endian base-256 digits, each scaled by the
61	# symbolic one (so the checker never unfolds it): digits(one, [65n, 219n, 1n])
62	# is 121665 for one == 1
63	def digits(+one: Nat, ds: List<&2, Nat>) -> Nat:
64	  match ds:
65	    case Nil{}:
66	      0n
67	    case Con{d, dt}:
68	      Nat.add(Nat.mul(one, d), C.shift(8n, digits(one, dt)))
69	
70	# a constant from its little-endian bytes (U32 values), each scaled by the
71	# symbolic one: uvalue(one, bs) is value(bs) for one == 1
72	def uvalue(+one: Nat, xs: List<&2, U32>) -> Nat:
73	  match xs:
74	    case Nil{}:
75	      0n
76	    case Con{x, xt}:
77	      Nat.add(Nat.mul(one, U32.to_nat(x)), C.shift(8n, uvalue(one, xt)))
78	
79	# p = 2^255 - 19
80	def prime(+one: Nat) -> Nat:
81	  Nat.sub(C.shift(255n, one), 19n)
82	
83	# arithmetic mod p (every result reduced)
84	def fadd(+p: Nat, a: Nat, b: Nat) -> Nat:
85	  Nat.mod(Nat.add(a, b), p)
86	
87	def fsub(+p: Nat, a: Nat, b: Nat) -> Nat:
88	  Nat.mod(Nat.sub(Nat.add(a, p), Nat.mod(b, p)), p)
89	
90	def fmul(+p: Nat, a: Nat, b: Nat) -> Nat:
91	  Nat.mod(Nat.mul(a, b), p)
92	
93	def fpow(+p: Nat, a: Nat, e: Nat) -> Nat:
94	  Nat.mod(Nat.pow(a, e), p)
95	
96	# a^(p - 2): the inverse of a nonzero a (Fermat), 0 for 0 (RFC 7748 section 5)
97	def finv(+p: Nat, a: Nat) -> Nat:
98	  fpow(p, a, Nat.sub(p, 2n))
99	
100	# ---- clauses ----
101	
102	def Add.value(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, U32>, +b: List<&2, U32>, +ha: {tight(a) == True{} : Bool}, +hb: {tight(b) == True{} : Bool}) -> Type:
103	  {Nat.mod(value(F.add(a, b)), prime(one)) == fadd(prime(one), value(a), value(b)) : Nat}
104	
105	def Add.tight(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, U32>, +b: List<&2, U32>, +ha: {tight(a) == True{} : Bool}, +hb: {tight(b) == True{} : Bool}) -> Type:
106	  {tight(F.add(a, b)) == True{} : Bool}
107	
108	def Sub.value(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, U32>, +b: List<&2, U32>, +ha: {tight(a) == True{} : Bool}, +hb: {tight(b) == True{} : Bool}) -> Type:
109	  {Nat.mod(value(F.sub(a, b)), prime(one)) == fsub(prime(one), value(a), value(b)) : Nat}
110	
111	def Sub.tight(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, U32>, +b: List<&2, U32>, +ha: {tight(a) == True{} : Bool}, +hb: {tight(b) == True{} : Bool}) -> Type:
112	  {tight(F.sub(a, b)) == True{} : Bool}
113	
114	def Mul.value(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, U32>, +b: List<&2, U32>, +ha: {tight(a) == True{} : Bool}, +hb: {tight(b) == True{} : Bool}) -> Type:
115	  {Nat.mod(value(F.mul(a, b)), prime(one)) == fmul(prime(one), value(a), value(b)) : Nat}
116	
117	def Mul.tight(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, U32>, +b: List<&2, U32>, +ha: {tight(a) == True{} : Bool}, +hb: {tight(b) == True{} : Bool}) -> Type:
118	  {tight(F.mul(a, b)) == True{} : Bool}
119	
120	def Sq.value(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, U32>, +ha: {tight(a) == True{} : Bool}) -> Type:
121	  {Nat.mod(value(F.sq(a)), prime(one)) == fmul(prime(one), value(a), value(a)) : Nat}
122	
123	def Sq.tight(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, U32>, +ha: {tight(a) == True{} : Bool}) -> Type:
124	  {tight(F.sq(a)) == True{} : Bool}
125	
126	# k below 2^17
127	def MulSmall.value(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, U32>, +k: U32, +ha: {tight(a) == True{} : Bool}, +hk: {Nat.is_lt(U32.to_nat(k), C.shift(17n, one)) == True{} : Bool}) -> Type:
128	  {Nat.mod(value(F.mul_small(a, k)), prime(one)) == fmul(prime(one), value(a), U32.to_nat(k)) : Nat}
129	
130	def MulSmall.tight(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, U32>, +k: U32, +ha: {tight(a) == True{} : Bool}, +hk: {Nat.is_lt(U32.to_nat(k), C.shift(17n, one)) == True{} : Bool}) -> Type:
131	  {tight(F.mul_small(a, k)) == True{} : Bool}
132	
133	def Select.zero(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, U32>, +b: List<&2, U32>, +ha: {tight(a) == True{} : Bool}, +hb: {tight(b) == True{} : Bool}) -> Type:
134	  {F.select(0, a, b) == a : List<&2, U32>}
135	
136	def Select.one(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, U32>, +b: List<&2, U32>, +ha: {tight(a) == True{} : Bool}, +hb: {tight(b) == True{} : Bool}) -> Type:
137	  {F.select(1, a, b) == b : List<&2, U32>}
138	
139	def Inv.value(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, U32>, +ha: {tight(a) == True{} : Bool}) -> Type:
140	  {Nat.mod(value(F.inv(a)), prime(one)) == finv(prime(one), value(a)) : Nat}
141	
142	def Inv.tight(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, U32>, +ha: {tight(a) == True{} : Bool}) -> Type:
143	  {tight(F.inv(a)) == True{} : Bool}
144	
145	# a^((p - 5) / 8), RFC 8032 section 5.1.3
146	def PowP58.value(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, U32>, +ha: {tight(a) == True{} : Bool}) -> Type:
147	  {Nat.mod(value(F.pow_p58(a)), prime(one)) == fpow(prime(one), value(a), Nat.div(Nat.sub(prime(one), 5n), 8n)) : Nat}
148	
149	def PowP58.tight(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, U32>, +ha: {tight(a) == True{} : Bool}) -> Type:
150	  {tight(F.pow_p58(a)) == True{} : Bool}
151	
152	# the canonical representative, which is the 32-byte encoding
153	def Freeze.value(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, U32>, +ha: {tight(a) == True{} : Bool}) -> Type:
154	  {value(F.freeze(a)) == Nat.mod(value(a), prime(one)) : Nat}
155	
156	def Freeze.tight(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, U32>, +ha: {tight(a) == True{} : Bool}) -> Type:
157	  {tight(F.freeze(a)) == True{} : Bool}
158	
159	def OfBytes.tight(+one: Nat, +h1: {one == 1n : Nat}, +bs: List<&2, U32>, +hb: {tight(bs) == True{} : Bool}) -> Type:
160	  {tight(F.of_bytes(bs)) == True{} : Bool}
161	
162	def Eq.value(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, U32>, +b: List<&2, U32>, +ha: {tight(a) == True{} : Bool}, +hb: {tight(b) == True{} : Bool}) -> Type:
163	  {F.eq(a, b) == Nat.is_eq(Nat.mod(value(a), prime(one)), Nat.mod(value(b), prime(one))) : Bool}
164	
165	def IsZero.value(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, U32>, +ha: {tight(a) == True{} : Bool}) -> Type:
166	  {F.is_zero(a) == Nat.is_eq(Nat.mod(value(a), prime(one)), 0n) : Bool}
167	
168	def Parity.value(+one: Nat, +h1: {one == 1n : Nat}, +a: List<&2, U32>, +ha: {tight(a) == True{} : Bool}) -> Type:
169	  {U32.to_nat(F.parity(a)) == Nat.mod(Nat.mod(value(a), prime(one)), 2n) : Nat}