spec/crypto/aes/poly.bend

bend-collections-laws-crypto@1.0.0.0 · 80 lines · 9 definitions

1import Base
2
3# Polynomials over GF(2), as FIPS 197 section 4 and SP 800-38D section 6.3 use
4# them. A polynomial is the list of its coefficients, the coefficient of x^0
5# first; a residue modulo a polynomial m(x) of degree n is a Word(n) of n
6# coefficients (Base's Word: a Bool vector, index 0 first).
7
8# Coefficient-wise sum (XOR); the longer tail is kept.
9def add(a: List<&2, Bool>, b: List<&2, Bool>) -> List<&2, Bool>:
10  match a b:
11    case Nil{} _:
12      b
13    case x <> xs Nil{}:
14      x <> xs
15    case x <> xs y <> ys:
16      Bool.xor(x, y) <> add(xs, ys)
17
18# c * a for a constant c in GF(2).
19def scale(+c: Bool, a: List<&2, Bool>) -> List<&2, Bool>:
20  match a:
21    case Nil{}:
22      Nil{}
23    case x <> xs:
24      Bool.and(c, x) <> scale(c, xs)
25
26# The schoolbook product: (c + x*q(x)) * b(x) = c*b(x) + x*(q(x)*b(x)).
27def mul(a: List<&2, Bool>, +b: List<&2, Bool>) -> List<&2, Bool>:
28  match a:
29    case Nil{}:
30      Nil{}
31    case c <> q:
32      add(scale(c, b), False{} <> mul(q, b))
33
34# The coefficient of x^(n-1) of a residue.
35def top(n: Nat, w: Word(n)) -> Bool:
36  match n w:
37    case 0n WNil{}:
38      False{}
39    case 1n WCon{b, t}:
40      b
41    case 2n+p WCon{b, t}:
42      top(1n+p, t)
43
44def wscale(n: Nat, c: Bool, w: Word(n)) -> Word(n):
45  match c:
46    case True{}:
47      w
48    case False{}:
49      Word.zero(n)
50
51# The constant polynomial c as a residue.
52def constant(n: Nat, c: Bool) -> Word(n):
53  match n:
54    case 0n:
55      WNil{}
56    case 1n+p:
57      WCon{c, Word.zero(p)}
58
59# Multiplication by x modulo m(x) = x^n + low(x) (deg low < n): shift every
60# coefficient up one degree; the coefficient that reaches x^n is replaced by
61# low(x), since x^n = low(x) modulo m(x).
62def times_x(+n: Nat, +low: Word(n), +r: Word(n)) -> Word(n):
63  Word.xor(n, wscale(n, top(n, r), low), Word.shl(n, r))
64
65# p(x) modulo m(x) = x^n + low(x), by Horner's rule:
66# p(x) = c + x*q(x), so p mod m = c + x*(q mod m) mod m.
67def reduce(+n: Nat, +low: Word(n), p: List<&2, Bool>) -> Word(n):
68  match p:
69    case Nil{}:
70      Word.zero(n)
71    case c <> q:
72      Word.xor(n, constant(n, c), times_x(n, low, reduce(n, low, q)))
73
74# The coefficients of a residue, as a polynomial.
75def coefficients(n: Nat, w: Word(n)) -> List<&2, Bool>:
76  match n w:
77    case 0n WNil{}:
78      Nil{}
79    case 1n+p WCon{b, t}:
80      b <> coefficients(p, t)