spec/crypto/secp256k1/field.bend

bend-collections-laws-crypto@1.0.0.0 · 91 lines · 16 definitions

1import Base
2import bend-collections-laws-crypto@1.0.0.0/spec/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 + ...
19def 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
27def w256(+one: Nat) -> Nat:
28  C.shift(256n, one)
29
30# 2^256 - p = 2^32 + 977, and p
31def cp(+one: Nat) -> Nat:
32  digits(one, [977n, 0n, 1n])
33
34def prime(+one: Nat) -> Nat:
35  Nat.sub(w256(one), cp(one))
36
37# 2^256 - n = 432420386565659656852420866390673177327, and n
38def cn(+one: Nat) -> Nat:
39  digits(one, [48831n, 12233n, 41331n, 16429n, 24516n, 20663n, 8985n, 17745n, 1n])
40
41def 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
46def madd(+m: Nat, a: Nat, b: Nat) -> Nat:
47  Nat.mod(Nat.add(a, b), m)
48
49# a - b mod m
50def msub(+m: Nat, a: Nat, b: Nat) -> Nat:
51  Nat.mod(Nat.sub(Nat.add(a, m), Nat.mod(b, m)), m)
52
53def mneg(+m: Nat, a: Nat) -> Nat:
54  msub(m, 0n, a)
55
56def mmul(+m: Nat, a: Nat, b: Nat) -> Nat:
57  Nat.mod(Nat.mul(a, b), m)
58
59def 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
63def 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)
68def 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
74def value(+one: Nat, xs: List<&2, Nat>) -> Nat:
75  digits(one, xs)
76
77# exactly 16 limbs, each below 2^16
78def 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
90def reduced(+one: Nat, +m: Nat, +xs: List<&2, Nat>) -> Bool:
91  Bool.and(limbs16(one, 16n, xs), Nat.is_lt(value(one, xs), m))