1	import Base
2	import ./limbs.bend as L
3	
4	# GF(p), p = 2^256 - 2^32 - 977 (SEC 2 section 2.4.1), on 16 limbs of
5	# radix 2^16 (src/crypto/secp256k1/limbs.bend). Every operation takes and
6	# returns reduced elements: exactly 16 limbs below 2^16, value below p.
7	# The contract is spec/crypto/secp256k1/field.bend; the proofs are in
8	# proofs/crypto/secp256k1/.
9	#
10	# Inversion and square root are exponentiations by the public exponents
11	# p - 2 (Fermat) and (p + 1) / 4 (p = 3 mod 4), square-and-multiply over
12	# the exponent's bits: the branch is on the public exponent, never on the
13	# base.
14	
15	# 2^256 - p = 2^32 + 977
16	def c() -> List<&2, Nat>:
17	  [977n, 0n, 1n]
18	
19	def reduce(xs: List<&2, Nat>) -> List<&2, Nat>:
20	  L.reduce(c(), 3n, xs)
21	
22	def small(+k: Nat) -> List<&2, Nat>:
23	  L.norm16([k])
24	
25	def zero() -> List<&2, Nat>:
26	  small(0n)
27	
28	def one() -> List<&2, Nat>:
29	  small(1n)
30	
31	# The operations look at their first argument first (and are the *_u
32	# forms then), so that on unknown arguments the proof checker keeps them
33	# folded instead of unfolding the reduction.
34	
35	def add_u(a: List<&2, Nat>, b: List<&2, Nat>) -> List<&2, Nat>:
36	  reduce(L.add(a, b))
37	
38	def add_b(a: List<&2, Nat>, b: List<&2, Nat>) -> List<&2, Nat>:
39	  match b:
40	    case Nil{}: add_u(a, Nil{})
41	    case y <> u: add_u(a, y <> u)
42	
43	def add(a: List<&2, Nat>, b: List<&2, Nat>) -> List<&2, Nat>:
44	  match a:
45	    case Nil{}: add_b(Nil{}, b)
46	    case x <> t: add_b(x <> t, b)
47	
48	# a - b = a + (p - b); the first argument is looked at first, so that a
49	# constant b is never unfolded while a is unknown
50	def sub(a: List<&2, Nat>, +b: List<&2, Nat>) -> List<&2, Nat>:
51	  match a:
52	    case Nil{}: reduce(L.neg_raw(c(), b))
53	    case x <> t: reduce(L.add(x <> t, L.neg_raw(c(), b)))
54	
55	def neg_u(a: List<&2, Nat>) -> List<&2, Nat>:
56	  reduce(L.neg_raw(c(), a))
57	
58	# (one argument: nothing to look at first)
59	def neg(a: List<&2, Nat>) -> List<&2, Nat>:
60	  neg_u(a)
61	
62	def mul_u(a: List<&2, Nat>, +b: List<&2, Nat>) -> List<&2, Nat>:
63	  reduce(L.conv(a, b))
64	
65	def mul_b(a: List<&2, Nat>, b: List<&2, Nat>) -> List<&2, Nat>:
66	  match b:
67	    case Nil{}: mul_u(a, Nil{})
68	    case y <> u: mul_u(a, y <> u)
69	
70	def mul(a: List<&2, Nat>, b: List<&2, Nat>) -> List<&2, Nat>:
71	  match a:
72	    case Nil{}: mul_b(Nil{}, b)
73	    case x <> t: mul_b(x <> t, b)
74	
75	def sq(+a: List<&2, Nat>) -> List<&2, Nat>:
76	  mul(a, a)
77	
78	# x^e for the exponent e given by its bits, most significant first
79	def pow_step(b: Nat, +x: List<&2, Nat>, +s: List<&2, Nat>) -> List<&2, Nat>:
80	  match b:
81	    case 0n: s
82	    case 1n+k: mul(s, x)
83	
84	def pow_go(+x: List<&2, Nat>, bits: List<&2, Nat>, +acc: List<&2, Nat>) -> List<&2, Nat>:
85	  match bits:
86	    case Nil{}: acc
87	    case b <> t: pow_go(x, t, pow_step(b, x, sq(acc)))
88	
89	# x is looked at first, so that on an unknown x nothing is unfolded
90	def pow(x: List<&2, Nat>, bits: List<&2, Nat>, +acc: List<&2, Nat>) -> List<&2, Nat>:
91	  match x:
92	    case Nil{}: pow_go(Nil{}, bits, acc)
93	    case +y <> +t: pow_go(y <> t, bits, acc)
94	
95	# the bits of p - 2 = 2^256 - 1 - (c + 1): those of c + 1, flipped
96	def inv_bits() -> List<&2, Nat>:
97	  L.cbits(L.bits(L.norm16([978n, 0n, 1n])))
98	
99	def init2(xs: List<&2, Nat>) -> List<&2, Nat>:
100	  List.reverse(&2, Nat, L.drop(2n, List.reverse(&2, Nat, xs)))
101	
102	# the bits of (p + 1) / 4: p + 1 = 2^256 - 1 - (c - 2), without its last two bits
103	def sqrt_bits() -> List<&2, Nat>:
104	  init2(L.cbits(L.bits(L.norm16([975n, 0n, 1n]))))
105	
106	# a^(p - 2): the inverse of a nonzero a, 0 for 0
107	def inv(+a: List<&2, Nat>) -> List<&2, Nat>:
108	  pow(a, inv_bits(), one())
109	
110	# a^((p + 1) / 4): a square root of a when a is a square (p = 3 mod 4)
111	def sqrt(+a: List<&2, Nat>) -> List<&2, Nat>:
112	  pow(a, sqrt_bits(), one())
113	
114	def is_zero(a: List<&2, Nat>) -> Bool:
115	  L.is_zero(a)
116	
117	def eq_b(a: List<&2, Nat>, b: List<&2, Nat>) -> Bool:
118	  match b:
119	    case Nil{}: L.eq(a, Nil{})
120	    case y <> u: L.eq(a, y <> u)
121	
122	def eq(a: List<&2, Nat>, b: List<&2, Nat>) -> Bool:
123	  match a:
124	    case Nil{}: eq_b(Nil{}, b)
125	    case x <> t: eq_b(x <> t, b)
126	
127	# a mod 2 (the parity of the canonical representative)
128	def parity(a: List<&2, Nat>) -> Nat:
129	  Nat.mod(L.hd0(a), 2n)
130	
131	# a < p, for 16 limbs below 2^16
132	def lt_p(a: List<&2, Nat>) -> Bool:
133	  L.ltm(c(), a)
134	
135	# b ? x : y, branch-free, for b in {0, 1}
136	def select(+b: Nat, x: List<&2, Nat>, y: List<&2, Nat>) -> List<&2, Nat>:
137	  L.select(b, x, y)