0%

s04 — Verification Pre-work: Multi-Executor Parity Harness

Goal

The verification rails exist BEFORE any backend code: Native is a first-class compiled execution mode in the test runner (AOT-shaped), the differential harness models evaluator, VM, LLVM, and native independently, and test-all.sh carries a gated native suite slot. A temporarily unavailable executor is reported as unavailable; final promotion requires every applicable executor, never a reduced comparator set disguised as parity.

Implementation Sketch

  • Backend enum gains Native at compiler_repo/compiler/oric/src/test/runner/mod.rs:31-37; dispatch at runner/mod.rs:421-498 gets dual cfg arms per the LLVM precedent (#[cfg(feature = "native_backend")] real arm + degraded error arm). Until s05 lands the feature, the real arm is a stub returning a clear “native backend not built” error.
  • AOT-shaped test execution design (per Step 6B verdict): compile module to object -> link with libori_rt.a -> run test exports as a process; NO in-memory/JIT path for native. New oric/src/test/runner/native_backend.rs skeleton documents the contract; native tests parallelize (no LLVM Context lock — do NOT inherit the sequential restriction at runner/mod.rs:123).
  • Evolve compiler_repo/diagnostics/dual-exec-verify.sh into a generic multi-executor harness (retain a compatibility wrapper if callers require it): columns for evaluator, VM, LLVM profile/AOT, and ori_backend target; mismatch classes identify the failing pair and preserve existing LLVM-vs-evaluator behavior when native or VM is not yet built.
  • compiler_repo/test-all.sh: run_ori_native() suite function registered but auto-skipping until the s09 milestone flips it on; JSON output schema extended for the suite.
  • Per aims-burden-tracking section-14 (will DELETE alive2 + sanitizer-smoke infra): the native verification stack builds ONLY on the retained layer (AIMS snapshots, lattice props, oracle, builtins, ORI_VERIFY_ARC, dual-exec, valgrind, benchmarks) — zero new dependencies on doomed infra.

Test Strategy

  • Harness changes are infrastructure (carve-out from compiler rigor) but get regression coverage: runner dispatch unit tests for the new enum arm; multi-executor self-tests with one synthetic mismatch and one unavailable executor; test-all.sh JSON schema check.

Work Items

  • Backend::Native enum variant + dual-cfg dispatch arms + CLI —backend=native parsing (stub-error until s05).
  • native_backend.rs AOT-shaped test-execution contract: compile->link->run-exports design + skeleton; parallel execution (no Context lock inheritance).
  • Differential harness -> explicit evaluator/VM/LLVM/native executor matrix with pair-specific mismatch classes, unavailable accounting, and sensitivity self-tests.
  • test-all.sh run_ori_native suite slot (auto-skip until s09 milestone) + JSON schema extension.
  • Verification-inventory doc: retained backend-agnostic layer enumerated; explicit zero-dependency statement on section-14-doomed infra.