1	import Base
2	import ../../lib/common.bend as C
3	
4	# GF(p) and Z/nZ for secp256k1 (SEC 2 section 2.4.1), over the natural
5	# numbers: p = 2^256 - 2^32 - 977, n the group order. Nothing of the
6	# implementation is used; this is the arithmetic of HACL*'s Spec.K256
7	# (felem / qelem: add, sub, mul, finv by Fermat, fsqrt by (p + 1) / 4).
8	#
9	# The proof checker keeps closed natural numbers in unary, so no 256-bit
10	# constant is ever written closed: 2^k is C.shift(k, one) and a constant is
11	# digits(one, ds), both with `one` a variable that every clause takes with
12	# the hypothesis {one == 1n : Nat}. For one == 1 they are the usual
13	# constants; no other value satisfies the hypothesis, so each clause says
14	# exactly what it says with the constants written out (the device of
15	# spec/math/w64.bend and spec/crypto/curve25519/field.bend).
16	
17	# a number from its little-endian radix-2^16 digits, each scaled by one:
18	# digits(1, [d0, d1, ...]) = d0 + 2^16 d1 + ...
19	def digits(+one: Nat, ds: List<&2, Nat>) -> Nat:
20	  match ds:
21	    case Nil{}:
22	      0n
23	    case d <> dt:
24	      Nat.add(Nat.mul(one, d), C.shift(16n, digits(one, dt)))
25	
26	# 2^256
27	def w256(+one: Nat) -> Nat:
28	  C.shift(256n, one)
29	
30	# 2^256 - p = 2^32 + 977, and p
31	def cp(+one: Nat) -> Nat:
32	  digits(one, [977n, 0n, 1n])
33	
34	def prime(+one: Nat) -> Nat:
35	  Nat.sub(w256(one), cp(one))
36	
37	# 2^256 - n = 432420386565659656852420866390673177327, and n
38	def cn(+one: Nat) -> Nat:
39	  digits(one, [48831n, 12233n, 41331n, 16429n, 24516n, 20663n, 8985n, 17745n, 1n])
40	
41	def order(+one: Nat) -> Nat:
42	  Nat.sub(w256(one), cn(one))
43	
44	# ---- arithmetic modulo m (m = p for the field, m = n for scalars) ----
45	
46	def madd(+m: Nat, a: Nat, b: Nat) -> Nat:
47	  Nat.mod(Nat.add(a, b), m)
48	
49	# a - b mod m
50	def msub(+m: Nat, a: Nat, b: Nat) -> Nat:
51	  Nat.mod(Nat.sub(Nat.add(a, m), Nat.mod(b, m)), m)
52	
53	def mneg(+m: Nat, a: Nat) -> Nat:
54	  msub(m, 0n, a)
55	
56	def mmul(+m: Nat, a: Nat, b: Nat) -> Nat:
57	  Nat.mod(Nat.mul(a, b), m)
58	
59	def mpow(+m: Nat, a: Nat, e: Nat) -> Nat:
60	  Nat.mod(Nat.pow(a, e), m)
61	
62	# a^(m - 2): for a prime m the inverse of a nonzero a (Fermat); 0 for 0
63	def minv(+m: Nat, a: Nat) -> Nat:
64	  mpow(m, a, Nat.sub(m, 2n))
65	
66	# a^((p + 1) / 4): a square root of a whenever a is a square mod p
67	# (p = 3 mod 4)
68	def fsqrt(+m: Nat, a: Nat) -> Nat:
69	  mpow(m, a, Nat.div(Nat.add(m, 1n), 4n))
70	
71	# ---- the representation (for the clauses) ----
72	
73	# the value of little-endian radix-2^16 limbs
74	def value(+one: Nat, xs: List<&2, Nat>) -> Nat:
75	  digits(one, xs)
76	
77	# exactly 16 limbs, each below 2^16
78	def limbs16(+one: Nat, n: Nat, xs: List<&2, Nat>) -> Bool:
79	  match n xs:
80	    case 0n Nil{}:
81	      True{}
82	    case 0n x <> t:
83	      False{}
84	    case 1n+k Nil{}:
85	      False{}
86	    case 1n+k x <> t:
87	      Bool.and(Nat.is_lt(x, C.shift(16n, one)), limbs16(one, k, t))
88	
89	# a reduced element mod m: 16 limbs below 2^16 of value below m
90	def reduced(+one: Nat, +m: Nat, +xs: List<&2, Nat>) -> Bool:
91	  Bool.and(limbs16(one, 16n, xs), Nat.is_lt(value(one, xs), m))