Module rules 

Rewrite rules (EXODIA Groups 1–3) with KERNEL-CHECKED soundness certificates (D11b): the compiler’s e-graph is a sibling of the proof engine, not a stranger.

Soundness discipline

Three obligations gate every rule, and all three fail closed:

1. Type: a rule fires only when the operand kinds are PROVEN (literal nodes or Oracle facts). Float operands never rewrite — -0.0 + 0.0 == +0.0 already breaks x + 0 → x bit-for-bit.
2. Error/effect preservation: a rule that DELETES a subterm (stops it being evaluated) requires CompilerEGraph::provably_total — (a / b) * 0 → 0 would erase the divide-by-zero. Short-circuit forms (false ∧ x → false) are exempt for the RIGHT operand only, because the runtime never evaluates it either.
3. Value: the identity itself carries a certificate checked through logicaffeine_kernel:
   • Certificate::Ring — polynomial identity via the kernel ring tactic. Ring identities with integer coefficients hold in EVERY commutative ring, in particular ℤ/2⁶⁴ = wrapping i64.
   • Certificate::BoolCases — exhaustive Bool case analysis: both sides are built as CIC terms over Match-defined and/or/not and normalized BY THE KERNEL for every valuation.
   • Certificate::Bitvector — wrapping/shift identities outside the ring fragment, exhaustively checked on the adversarial i64 boundary grid. The full Z3 bitvector theorem lands with the Forge SMT layer (M15); this grid is the standing mechanical check.

Structs

Rewrite

Enums

BoolExpr

A tiny boolean expression language evaluated through kernel normalization (Match-defined connectives over the prelude’s Bool).

Certificate

RingExpr

A tiny polynomial expression language reified into the kernel’s ring tactic syntax.

Functions

all

verify_all_with_kernel

Check every rule’s certificate through the kernel. Returns the number of verified rules; the first failure aborts with the rule’s name.