Module word_ring 

Kernel ring proofs for the word ring ℤ/2ⁿ (Word8/Word16/Word32/Word64).

The crate::ring procedure proves a polynomial identity by reducing both sides to a canonical multivariate polynomial over ℤ and comparing. An identity that canonicalizes equal holds in every commutative ring — so it holds in the word ring ℤ/2ⁿ, whose +/* are wrapping_add/wrapping_mul (the quotient of ℤ by 2ⁿℤ; the ring axioms survive the quotient).

This is the soundness certificate behind every reassociation and product reshaping the optimizer performs on wrapping arithmetic: associativity, commutativity, distributivity, and the Karatsuba/gauss product form are all kernel-certified here, at FULL word width with no bound on the operands. The bit-logic side of the crypto (xor, rotl) is not polynomial and is certified separately by bitblast→CDCL.

Each lemma returns true iff the kernel certifies it; the tests pin both the positive proofs and their non-vacuity (a WRONG identity must NOT canonicalize equal).

Functions

add_associative

(a + b) + c = a + (b + c) — additive associativity in ℤ/2ⁿ.

add_commutative

a + b = b + a — additive commutativity in ℤ/2ⁿ.

additive_identity

a + 0 = a — additive identity in ℤ/2ⁿ.

all_word_ring_laws_certified

Every word-ring law the optimizer leans on, kernel-certified — a single gate.

karatsuba_expand

(a + b)(c + d) = ac + ad + bc + bd — the Karatsuba/gauss product expansion, the identity the 3-multiply NTT butterfly and complex-multiply reshaping rely on, certified at full word width.

left_distributive

a · (b + c) = a · b + a · c — left distributivity in ℤ/2ⁿ.

mul_associative

(a · b) · c = a · (b · c) — multiplicative associativity in ℤ/2ⁿ.

mul_commutative

a · b = b · a — multiplicative commutativity in ℤ/2ⁿ.

multiplicative_identity

a · 1 = a — multiplicative identity in ℤ/2ⁿ.