GitHub

Phase 1 Proof Contract

Updated: 2026-07-09

This contract defines how Phase 1 features move from refinement evidence to SEFO materialization. The goal is to prove each slice as it lands, not to defer all proof work until the end of the project.

Scope

Phase 1 covers this loop:

  1. The refinement checker proves a fact.
  2. The fact is carried as a ProofSlot.
  3. E-graph rewrites inspect the proof as a guard.
  4. Materialization changes executable IR only when the proof gate is satisfied.
  5. Interpreter, VM, and JIT/fallback behavior remain equivalent.

Contract

  • Proof evidence must have a named source: refinement solving, branch-local condition refinement, SCCP feedback, or e-graph feedback.
  • Proofs must attach to the current value identity, not just a variable name. Current e-graph lowering versions mutable loads as symbols like var:$x@0 and var:$x@1 so stale facts cannot cross reassignment.
  • ProofSlot merges may keep exact/range/nonzero facts only when the numeric facts remain consistent.
  • Proof-gated rewrites must produce an obligation diagnostic with one of three statuses: Discharged, Blocked, or Deferred.
  • Materialization may rewrite executable IR only after the e-graph confirms the target equivalence. For x / x -> 1, the current gate requires both: x is proven nonzero, and the div-self-nonzero obligation is discharged.
  • Strict proof validation must pass before a proof-gated change is considered ready for CI.

Current Strict Gate

Use either of these local gates:

naux dev refine --strict path/to/file.nx
NAUX_IR_PROOF_STRICT=1 cargo test -p naux --test refinement_closed_loop_tests

The strict gate currently checks:

  • Optimized IR proof slots are structurally valid.
  • x / x -> 1 materialization is backed by a discharged div-self-nonzero obligation in the same feedback round.
  • Solver strict mode reports undischarged refinement constraints as errors.

Done Criteria For A New Phase 1 Feature

  • Add a positive closed-loop test proving the intended optimization/safety win.
  • Add a negative test proving stale or missing evidence does not optimize.
  • Add interpreter/VM/JIT parity coverage when runtime behavior is affected.
  • Ensure naux dev refine shows readable proof obligation diagnostics.
  • Run the strict gate and update this contract when its observable requirements or admitted proof sources change.

Open Gaps

  • Extend strict materialization checks beyond div-self-nonzero to range-based and-mask rewrites and future collection bounds rewrites.
  • Move proof identity fully onto SSA value IDs and joins.
  • Add structured JSON diagnostics once the text report stabilizes.
  • Add Coq certificates for a small core of materialization rules after the lightweight contract stops moving.