Section 04: Cross-Executor Verification

Context

The old section tested mostly LLVM helpers and proposed source-pattern audits. That cannot validate the final architecture. Verification must prove:

• semantic behavior is independent of physical representation;
• VM enum storage is verifier-safe and measured for speed and memory;
• LLVM and ori_backend consume the same compiled layout and ABI;
• direct compiled WebAssembly behaves like the native compiled paths;
• AIMS ownership and final memory state are invariant across layouts.

Every positive pin needs a paired negative pin that rejects the broken shape. Tests that invoke dead gated helpers without exercising production selection do not close a layer.

04.1 Plan, Verifier, and Emitter Tests

• Replace source-text assertions with tests that construct validated EnumReprEvidence, VmEnumLayout, and CompiledEnumLayout, then invoke the real bytecode compiler/verifier, LLVM emitter, and ori_backend BIR/module emitter.
• Add table/property tests for every encoding and enum shape: explicit, niche, tagged pointer, tagless; unit, heterogeneous payload, generic, recursive-reference, runtime ABI, #repr("c"), nested, and unsupported-target fallback.
• Add LLVM emitter-driven tests for construction, tag access, match, semantic projection, SetTag where legal, derive Eq/Comparable/Hashable/Format, RC/drop, Option/Result helpers, panic, and unwind. Assert emitted IR structure and execute the linked result.
• Add ori_backend tests over the same fixtures. Assert BIR references shared layout IDs, target lowering resolves the expected field locations/ABI, native objects link, and the WASM writer emits a complete directly executable module.
• Add VM compiler/verifier tests over the same semantic fixtures. Assert specialized opcode/operand selection, verified register or heap classes, correct trace/drop schemas, and rejection of cross-variant access, bad tags, forged handles, absent side storage, and double drop.
• Add checked-layout negative tests for overflow, impossible alignment, missing variants/fields, duplicate IDs, ABI conflict, unsupported target encoding, stale fingerprint, and mismatched ExecutableProgram identity.
• Prove tests traverse production selection gates. Each encoding fixture must assert the selected layout before testing emission; a helper forced with a fabricated encoding is supplementary, not sufficient.
• Keep fixtures backend-neutral and generated from one semantic matrix. Backend-specific tests may add assertions but may not duplicate the layout expected-value algorithm.

04.2 Seam and ABI Enforcement

• Enforce private construction and immutable access for evidence and plan entries. Only the canonical builders may select encoding or compute layout; emitters receive validated references or stable IDs.
• Add a structural seam scan with an explicit allowlist for enum aggregate index literals, local tag/payload offset arithmetic, backend target-data queries, VM-layout access from compiled code, compiled-layout access from AIMS/VM execution, and layout fallback calls.
• Add cross-backend identity fixtures that serialize TargetSpec, CompiledEnumLayout, FunctionAbi, and runtime declarations once and feed the same bytes to LLVM and ori_backend. Assert both reject a mutated fingerprint or incompatible target.
• Add target fixtures for x86-64, aarch64, riscv64, s390x, wasm32, and every admitted wasm64 variant. Cover pointer width, endianness, alignment, public/FFI layout, runtime ABI, and tagged-pointer eligibility.
• Add an architecture test proving ori_eval and AIMS compile without either physical layout type, ori_vm cannot import compiled layout, and ori_llvm/ori_backend cannot import VM layout or each other.
• Make seam, identity, and target-matrix checks required gates in the canonical compiler verification flow; a manual grep result cannot be the only enforcement.

04.3 Behavioral, Leak, Performance, and Memory Matrix

• Freeze a broad corpus before tuning: existing enum/Option/Result/iterator/derive tests plus micro, medium, allocation-heavy, string, collection, graph, nested-control, recursive, error/unwind, and combined-application programs at multiple input scales.
• Run normalized outcome parity across evaluator, VM, LLVM debug, LLVM release, linked AOT, admitted ori_backend native targets, and direct compiled WASM. Compare return values, stdout/effect order, panics, source attribution, and deterministic formatting/hash results.
• Run the AIMS logical verifier plus independent VM and compiled-plan satisfaction/leak tools across all memory-owning cells. Require identical frozen ownership/drop event identities and ordering; allow physical action traces to differ only when each validates against those facts. The burden-sole probe judges only the current compiled-counter RC/AOT adapter. Require zero final live allocations on success, panic, unwind, verifier rejection, and runtime-limit failure.
• Measure enum-heavy VM workloads with wall time, executed bytecodes, bytecode bytes, frame/register bytes, heap live/peak/allocated bytes, allocation count, final live bytes, and whole-process RSS. Record compile/startup cost separately from steady execution.
• Enforce the VM bottom bar on the frozen combined corpus: geometric-mean execution at least 2x faster than pinned Python, no hidden fallback or parity mismatch, workload-attributable peak memory at most half Python, and unadjusted RSS no worse than Python.
• Track pinned LuaJIT -joff time and memory as the strict-interpreter north star by workload family. Report regressions and gaps; do not narrow the corpus to workloads that favor one enum encoding.
• Compare canonical versus optimized enum layouts within each executor. A candidate is invalid if it changes behavior, AIMS facts, ABI where constrained, leak state, or verifier acceptance; speed and memory results from invalid cells are discarded.
• Prove the LLVM path remains intact by comparing pre-migration and post-migration structural IR, runtime ABI fixtures, debug/release behavior, AOT linkage, and leak state before accepting VM or native-backend changes.
• Run the canonical test-all runtime to a terminal structured verdict, plus required target/emitter/benchmark/leak gates. No suite error, crash, untracked disposition, or new failure may remain.

04.4 Completion Checklist

• Source-text-only tests are replaced by production-path plan, verifier, emitter, object/module, and execution tests.
• API visibility and structural seam gates prevent backend-local enum layout or ABI reconstruction.
• Every semantic shape and admitted physical encoding has positive, negative, and interaction coverage.
• Evaluator, VM, LLVM debug/release/AOT, ori_backend, and direct WASM observable parity is clean.
• AIMS facts are physical-layout invariant and all memory-owning paths end with zero live allocations.
• LLVM and ori_backend consume identical compiled-layout and ABI fixtures for every admitted target.
• VM enum representation clears the Python speed and memory bottom bars on the frozen broad combined corpus.
• LuaJIT -joff north-star gaps are measured by workload family with no hidden fallback.
• Canonical test-all, target, format, lint, seam, leak, and repository-hygiene gates are clean.
• Third-party review is clean and all validated findings are fixed.
• Implementation-hygiene review is clean after third-party review.
• Cross-plan contracts, docs, and plan findings reflect the retained production architecture with no obsolete LLVM-only or take-project instructions.

04.R Third Party Review Findings

• The prior verification scope stopped at interpreter/LLVM dual execution and therefore could not prove the VM, ori_backend, or direct-WASM seams.
• Lexical grep checks are useful discovery tools but insufficient architecture enforcement. The revised plan combines visibility, typed APIs, structural scans, negative tests, and cross-backend identity fixtures.
• The prior niche-helper approach could execute a dead helper without proving production selection. The revised matrix asserts selection and then executes the real entry point.