0%

s21 — Verification Suite Completion: The Three Layers

Goal

The Alive2-replacing verification architecture is COMPLETE and CI-resident: (1) evaluator/VM/LLVM/ori_backend differential as the permanent behavioral gate, (2) per-component symbolic checkers hardened, (3) BIR-vs-canonical translation validation sampling in CI, and (4) cache/invalidation/parallel/budget sensitivity checks that make the compile-cost architecture executable, plus a fuzzing wave.

Implementation Sketch

  • Layer 1 — multi-executor parity fold: the s16 sweep becomes a permanent test-all.sh + CI member across host targets, direct compiled WASM, and the qemu matrix (s09 CI); mismatch triage runbook documents evaluator-vs-VM-vs-LLVM-vs-native bisection.
  • 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); logical ownership-event verifier on BIR mirroring VF-1 (exact event identity/edge/order/normal-and-unwind discharge per path), plus a separate CompiledLayoutPlan checker for whatever counter, region, stack, or other physical actions the target selects.
  • 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.
  • Compile-architecture layer: exercise the s17B exact invalidation matrix, jobs/cache-state byte determinism, fragment corruption/version misses, and s19 adversarial budget-exhaustion corpus in permanent CI. Every configured optimizing pass must report deterministic fuel/growth accounting; the registry test rejects an unbudgeted pass.
  • Fuzzing wave 1: program generator (or corpus-mutation over tests/spec) feeds the multi-executor 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, stale-cache key, over-broad invalidation, global-lock scaling loss, unbudgeted/unbounded rewrite) — every layer carries its negative pin before this section closes.

Work Items

  • Evaluator/VM/LLVM/native 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 plus optimizer fuel/growth/bounded-termination registry checks in CI (per-commit budget + full nightly-equivalent) consuming s19 per-pass hooks.
  • Fuzzing wave 1 (generator/mutation -> multi-executor parity -> auto-filed findings) + negative-pin sensitivity proofs for behavioral, symbolic, translation, and compile-architecture layers.