spec/crypto/aes/poly.bend checks

raw source on the hub · import bend-collections-laws-crypto@1.0.0.0/spec/crypto/aes/poly.bend as Poly

1 import

import Base

Definitions

def add source · line 9 · raw

@a:List<&2, Bool> -> @b:List<&2, Bool> -> List<&2, Bool>

Coefficient-wise sum (XOR); the longer tail is kept.

def scale source · line 19 · raw

@+c:Bool -> @a:List<&2, Bool> -> List<&2, Bool>

c * a for a constant c in GF(2).

def mul source · line 27 · raw

@a:List<&2, Bool> -> @+b:List<&2, Bool> -> List<&2, Bool>

The schoolbook product: (c + x*q(x)) * b(x) = c*b(x) + x*(q(x)*b(x)).

def top source · line 35 · raw

@n:Nat -> @w:Word(n) -> Bool

The coefficient of x^(n-1) of a residue.

def wscale source · line 44 · raw

@n:Nat -> @c:Bool -> @w:Word(n) -> Word(n)

def constant source · line 52 · raw

@n:Nat -> @c:Bool -> Word(n)

The constant polynomial c as a residue.

def times_x source · line 62 · raw

@+n:Nat -> @+low:Word(n) -> @+r:Word(n) -> Word(n)

Multiplication by x modulo m(x) = x^n + low(x) (deg low < n): shift every coefficient up one degree; the coefficient that reaches x^n is replaced by low(x), since x^n = low(x) modulo m(x).

def reduce source · line 67 · raw

@+n:Nat -> @+low:Word(n) -> @p:List<&2, Bool> -> Word(n)

p(x) modulo m(x) = x^n + low(x), by Horner's rule: p(x) = c + x*q(x), so p mod m = c + x*(q mod m) mod m.

def coefficients source · line 75 · raw

@n:Nat -> @w:Word(n) -> List<&2, Bool>

The coefficients of a residue, as a polynomial.