1	import Base
2	import ./limbs.bend as L
3	
4	# Integers modulo the group order
5	# n = 2^256 - 432420386565659656852420866390673177327 (SEC 2 section 2.4.1),
6	# on 16 limbs of radix 2^16 (src/crypto/secp256k1/limbs.bend), reduced
7	# (exactly 16 limbs below 2^16, value below n). The contract is
8	# spec/crypto/secp256k1/scalar.bend.
9	
10	# 2^256 - n, in radix 2^16
11	def c() -> List<&2, Nat>:
12	  [48831n, 12233n, 41331n, 16429n, 24516n, 20663n, 8985n, 17745n, 1n]
13	
14	def reduce_u(xs: List<&2, Nat>) -> List<&2, Nat>:
15	  L.reduce(c(), 4n, xs)
16	
17	def reduce(xs: List<&2, Nat>) -> List<&2, Nat>:
18	  reduce_u(xs)
19	
20	def zero() -> List<&2, Nat>:
21	  L.norm16([])
22	
23	def small(+k: Nat) -> List<&2, Nat>:
24	  L.norm16([k])
25	
26	def one() -> List<&2, Nat>:
27	  small(1n)
28	
29	def add_u(a: List<&2, Nat>, b: List<&2, Nat>) -> List<&2, Nat>:
30	  reduce_u(L.add(a, b))
31	
32	def add_b(a: List<&2, Nat>, b: List<&2, Nat>) -> List<&2, Nat>:
33	  match b:
34	    case Nil{}: add_u(a, Nil{})
35	    case y <> u: add_u(a, y <> u)
36	
37	def add(a: List<&2, Nat>, b: List<&2, Nat>) -> List<&2, Nat>:
38	  match a:
39	    case Nil{}: add_b(Nil{}, b)
40	    case x <> t: add_b(x <> t, b)
41	
42	def neg_u(a: List<&2, Nat>) -> List<&2, Nat>:
43	  reduce_u(L.neg_raw(c(), a))
44	
45	# (one argument: nothing to look at first)
46	def neg(a: List<&2, Nat>) -> List<&2, Nat>:
47	  neg_u(a)
48	
49	def mul_u(a: List<&2, Nat>, +b: List<&2, Nat>) -> List<&2, Nat>:
50	  reduce_u(L.conv(a, b))
51	
52	def mul_b(a: List<&2, Nat>, b: List<&2, Nat>) -> List<&2, Nat>:
53	  match b:
54	    case Nil{}: mul_u(a, Nil{})
55	    case y <> u: mul_u(a, y <> u)
56	
57	def mul(a: List<&2, Nat>, b: List<&2, Nat>) -> List<&2, Nat>:
58	  match a:
59	    case Nil{}: mul_b(Nil{}, b)
60	    case x <> t: mul_b(x <> t, b)
61	
62	def pow_step(b: Nat, +x: List<&2, Nat>, +s: List<&2, Nat>) -> List<&2, Nat>:
63	  match b:
64	    case 0n: s
65	    case 1n+k: mul(s, x)
66	
67	def pow_go(+x: List<&2, Nat>, bits: List<&2, Nat>, +acc: List<&2, Nat>) -> List<&2, Nat>:
68	  match bits:
69	    case Nil{}: acc
70	    case b <> t: pow_go(x, t, pow_step(b, x, mul(acc, acc)))
71	
72	# x is looked at first, so that on an unknown x nothing is unfolded
73	def pow(x: List<&2, Nat>, bits: List<&2, Nat>, +acc: List<&2, Nat>) -> List<&2, Nat>:
74	  match x:
75	    case Nil{}: pow_go(Nil{}, bits, acc)
76	    case +y <> +t: pow_go(y <> t, bits, acc)
77	
78	# the bits of n - 2, most significant first (the proofs show they are those
79	# of 2^256 - 1 - (c + 1), c + 1 = 2^256 - n + 1)
80	def inv_bits() -> List<&2, Nat>:
81	  [1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n,
82	   1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n,
83	   1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n,
84	   1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 0n,
85	   1n, 0n, 1n, 1n, 1n, 0n, 1n, 0n, 1n, 0n, 1n, 0n, 1n, 1n, 1n, 0n, 1n, 1n, 0n, 1n, 1n, 1n, 0n, 0n, 1n, 1n, 1n, 0n, 0n, 1n, 1n, 0n,
86	   1n, 0n, 1n, 0n, 1n, 1n, 1n, 1n, 0n, 1n, 0n, 0n, 1n, 0n, 0n, 0n, 1n, 0n, 1n, 0n, 0n, 0n, 0n, 0n, 0n, 0n, 1n, 1n, 1n, 0n, 1n, 1n,
87	   1n, 0n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 1n, 0n, 1n, 0n, 0n, 1n, 0n, 0n, 1n, 0n, 1n, 1n, 1n, 1n, 0n, 1n, 0n, 0n, 0n, 1n, 1n, 0n, 0n,
88	   1n, 1n, 0n, 1n, 0n, 0n, 0n, 0n, 0n, 0n, 1n, 1n, 0n, 1n, 1n, 0n, 0n, 1n, 0n, 0n, 0n, 0n, 0n, 1n, 0n, 0n, 1n, 1n, 1n, 1n, 1n, 1n]
89	
90	# a^(n - 2): the inverse of a nonzero a, 0 for 0
91	def inv(+a: List<&2, Nat>) -> List<&2, Nat>:
92	  pow(a, inv_bits(), one())
93	
94	def is_zero(a: List<&2, Nat>) -> Bool:
95	  L.is_zero(a)
96	
97	def eq_b(a: List<&2, Nat>, b: List<&2, Nat>) -> Bool:
98	  match b:
99	    case Nil{}: L.eq(a, Nil{})
100	    case y <> u: L.eq(a, y <> u)
101	
102	def eq(a: List<&2, Nat>, b: List<&2, Nat>) -> Bool:
103	  match a:
104	    case Nil{}: eq_b(Nil{}, b)
105	    case x <> t: eq_b(x <> t, b)
106	
107	# a < n, for 16 limbs below 2^16
108	def lt_n(a: List<&2, Nat>) -> Bool:
109	  L.ltm(c(), a)
110	
111	# 2^256 - n - 1
112	def cm1() -> List<&2, Nat>:
113	  [48830n, 12233n, 41331n, 16429n, 24516n, 20663n, 8985n, 17745n, 1n]
114	
115	# a > n / 2 (n is odd), i.e. 2 a >= n + 1 = 2^256 - cm1: the carry out of
116	# 2 a + cm1
117	def is_high(a: List<&2, Nat>) -> Bool:
118	  Bool.not(L.ltm(cm1(), L.scal(2n, a)))
119	
120	def select(+b: Nat, x: List<&2, Nat>, y: List<&2, Nat>) -> List<&2, Nat>:
121	  L.select(b, x, y)