src/crypto/secp256k1/scalar.bend

bend-collections-laws-crypto@1.0.0.0 · 121 lines · 26 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/src/crypto/secp256k1/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
11def c() -> List<&2, Nat>:
12  [48831n, 12233n, 41331n, 16429n, 24516n, 20663n, 8985n, 17745n, 1n]
13
14def reduce_u(xs: List<&2, Nat>) -> List<&2, Nat>:
15  L.reduce(c(), 4n, xs)
16
17def reduce(xs: List<&2, Nat>) -> List<&2, Nat>:
18  reduce_u(xs)
19
20def zero() -> List<&2, Nat>:
21  L.norm16([])
22
23def small(+k: Nat) -> List<&2, Nat>:
24  L.norm16([k])
25
26def one() -> List<&2, Nat>:
27  small(1n)
28
29def add_u(a: List<&2, Nat>, b: List<&2, Nat>) -> List<&2, Nat>:
30  reduce_u(L.add(a, b))
31
32def 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
37def 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
42def 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)
46def neg(a: List<&2, Nat>) -> List<&2, Nat>:
47  neg_u(a)
48
49def mul_u(a: List<&2, Nat>, +b: List<&2, Nat>) -> List<&2, Nat>:
50  reduce_u(L.conv(a, b))
51
52def 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
57def 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
62def 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
67def 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
73def 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)
80def 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
91def inv(+a: List<&2, Nat>) -> List<&2, Nat>:
92  pow(a, inv_bits(), one())
93
94def is_zero(a: List<&2, Nat>) -> Bool:
95  L.is_zero(a)
96
97def 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
102def 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
108def lt_n(a: List<&2, Nat>) -> Bool:
109  L.ltm(c(), a)
110
111# 2^256 - n - 1
112def 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
117def is_high(a: List<&2, Nat>) -> Bool:
118  Bool.not(L.ltm(cm1(), L.scal(2n, a)))
119
120def select(+b: Nat, x: List<&2, Nat>, y: List<&2, Nat>) -> List<&2, Nat>:
121  L.select(b, x, y)