JAR: Join-Accumulate Refine

18.1. Galois Field GF(2^16)🔗

🔗def
Jar.Erasure.GF16 : Type
Jar.Erasure.GF16 : Type

Element of GF(2^16). Represented as a 16-bit integer. Field polynomial: x^16 + x^5 + x^3 + x^2 + 1.

🔗def
Jar.Erasure.GF_POLYNOMIAL : UInt32
Jar.Erasure.GF_POLYNOMIAL : UInt32

The irreducible polynomial for GF(2^16): x^16 + x^5 + x^3 + x^2 + 1. In binary: 0x1002D (bit 16 + bit 5 + bit 3 + bit 2 + bit 0).

🔗def
Jar.Erasure.GF_ORDER : Nat
Jar.Erasure.GF_ORDER : Nat

GF(2^16) order = 2^16 = 65536.

🔗def
Jar.Erasure.GF_MODULUS : UInt16
Jar.Erasure.GF_MODULUS : UInt16

GF(2^16) modulus = 65535. Used as the "infinity" log value (log of 0).

🔗def
Jar.Erasure.GF_BITS : Nat
Jar.Erasure.GF_BITS : Nat

Number of bits in GF elements.

🔗def
Jar.Erasure.CANTOR_BASIS : Array UInt16
Jar.Erasure.CANTOR_BASIS : Array UInt16

Cantor basis vectors for GF(2^16). These define the basis change between standard and Cantor representations. Values from the reed-solomon-simd crate.

GF(2^16) arithmetic uses log/exp tables built from the Cantor basis. Multiplication operates via log/exp table lookups; inversion uses Fermat's little theorem.

🔗def
Jar.Erasure.addMod (x y : UInt16) : UInt16
Jar.Erasure.addMod (x y : UInt16) : UInt16

Modular addition for log values: (x + y) mod 65535, mapping 65535 to 0.

🔗def
Jar.Erasure.buildExpLog : Array UInt16 × Array UInt16
Jar.Erasure.buildExpLog : Array UInt16 × Array UInt16

Build the exp and log tables for GF(2^16) with Cantor basis. Returns (exp, log) where:

  • exp maps discrete logarithm → Cantor basis element

  • log maps Cantor basis element → discrete logarithm

  • Multiplication: a * b = exp[addMod(log[a], log[b])] (for a,b ≠ 0)

🔗def
Jar.Erasure.expTable : Array UInt16
Jar.Erasure.expTable : Array UInt16

Cached exp table.

🔗def
Jar.Erasure.logTable : Array UInt16
Jar.Erasure.logTable : Array UInt16

Cached log table.

🔗def
Jar.Erasure.tableMul (x logM : UInt16) : UInt16
Jar.Erasure.tableMul (x logM : UInt16) : UInt16

Multiply GF element x by element whose log is logM, using exp/log tables. Returns 0 if x = 0.

🔗def
Jar.Erasure.gfMul (x y : UInt16) : UInt16
Jar.Erasure.gfMul (x y : UInt16) : UInt16

Multiply two GF(2^16) elements.

🔗def
Jar.Erasure.gfInv (x : UInt16) : UInt16
Jar.Erasure.gfInv (x : UInt16) : UInt16

Multiplicative inverse in GF(2^16). Returns 0 for input 0.

🔗def
Jar.Erasure.buildSkew : Array UInt16
Jar.Erasure.buildSkew : Array UInt16

Build the skew factor table used in FFT/IFFT butterflies. The skew table has 65535 entries (indexed 0..65534).

🔗def
Jar.Erasure.skewTable : Array UInt16
Jar.Erasure.skewTable : Array UInt16

Cached skew table.