0%

s21 — Verification Suite Completion: The Three Layers

Goal

The Alive2-replacing verification architecture is COMPLETE and CI-resident: (1) triple-parity differential as the permanent behavioral gate, (2) per-component symbolic checkers hardened, (3) BIR-vs-canonical translation validation sampling in CI, plus a fuzzing wave.

Implementation Sketch

  • Layer 1 — triple-parity fold: the tri-exec sweep (s16) becomes a permanent test-all.sh + CI member across host targets and the qemu matrix (s09 CI); mismatch triage runbook documented (diagnostics/ extension: native-vs-llvm-vs-interp bisect helper per tooling-first).
  • Layer 2 — symbolic checkers hardened: regalloc checker (s11) extended to full coverage incl. unwind edges and parallel-move cycles; isel rule-verification harness — per-instruction-family random-input equivalence testing of BIR semantics vs emitted MIR semantics (interpreter-as-oracle on the BIR side, execution on the MIR side); RC-balance verifier on BIR mirroring VF-1 (net-zero per path over RC multiset — extends the s06/s19 guardrail into a path-sensitive check).
  • Layer 3 — translation validation: BIR-after-mid-end vs the evaluator-consumed canonical IR — sampled functions execute under both (evaluator on CanExpr; native on BIR-lowered code) over generated inputs; per-pass (before,after) pairs from s19 hooks validated the same way; CI runs a sampling budget per commit and the full sweep nightly-equivalent.
  • Fuzzing wave 1: program generator (or corpus-mutation over tests/spec) feeding the tri-parity harness; crashes/mismatches auto-file via the bug tracker discipline; coverage-guided where cheap.
  • The retained AIMS verification layer (snapshots, lattice props, oracle, builtins) is asserted UNTOUCHED — this suite adds, never weakens (INVERTED-TDD watch on any gate edit).

Test Strategy

  • Self-tests per layer: injected-mismatch fixtures prove each layer DETECTS (parity sensitivity, checker rejection, validation divergence) — every layer carries its negative pin before this section closes.

Work Items

  • Tri-parity permanent CI fold + mismatch-bisect diagnostic helper + triage runbook.
  • Regalloc checker full-coverage hardening (unwind edges, move cycles) + isel rule-verification harness (oracle-vs-execution per instruction family).
  • Path-sensitive RC-balance verifier on BIR (VF-1 mirror) wired into ORI_VERIFY_ARC runs.
  • Translation-validation sampling in CI (per-commit budget + full nightly-equivalent) consuming s19 per-pass hooks.
  • Fuzzing wave 1 (generator/mutation -> tri-parity -> auto-filed findings) + negative-pin sensitivity proofs for all three layers.