Parity, Safety, and Verification
Goal
Prove absolute observable behavior parity among the current evaluator oracle, VM, LLVM debug/release, and AOT, plus memory safety/leak freedom and robust malformed-chunk rejection, before the VM can become the default.
Implementation Sketch
- Finish
diagnostics/bytecode-verify.shas the single production-path harness with fixture selection and JSON output. Compare result/type, stdout bytes and order, stderr/diagnostic identity and class, exit status, test results, effects, panic/stack-overflow behavior, ownership traces, and leak counters. - Cover the full callable/program surface: ordinary and recursive functions, generics/monomorphizations, closures/captures, imports, impl/trait methods, derives/intrinsics, built-ins, pattern CFGs, collections/COW, strings, panics, and cleanup paths.
- Run evaluator versus VM and both against LLVM debug/release and AOT over every applicable case. A mismatch is localized with the shared frontend/executable-program/function/chunk provenance, invalidates affected performance samples, and blocks adoption.
- Run
ORI_CHECK_LEAKS=1, exact logical AIMS traces, and projection-specific ownership diagnostics on memory-heavy and exceptional paths. Each executor must satisfy the same post-AIMS event identities, but literal RC traces are evidence only for a counter-selecting projection. A mismatch is repaired at the shared fact producer or the faulty physical mapping, never by inventing VM-local ownership policy. - Add verifier property/fuzz tests for malformed opcodes, types, constants, jumps, call signatures, resource limits, and encoding versions. No malformed chunk may panic, read out of bounds, or reach a runtime call.
- Freeze and review the normalizer before results. It may remove only inherently nondeterministic presentation fields such as temporary paths; it cannot change values, reorder output, merge diagnostic classes, suppress panic/exit differences, or hide ownership/leak mismatches.
- Flip the default only after correctness, safety, CLI, and isolation criteria are green. Absolute parity is invariant: there are no tolerances, waivers, backend-specific expected semantics, or fallback-based passes, and performance never trades against it.
Live Regression Gate
The last user-confirmed aims-burden-revision-2 LLVM-spec baseline before the VM/shared-artifact prototype is 5,022 passed, 147 failed, 92 skipped, 92 LCFail, 0 leaks in 70.6 seconds.
The original catastrophic anchor remains canonical run 1784112741022385646-a8df69a2 at be79b45406e62843fd1b7b361d8d3c25e73d9455: 344 LLVM-spec passes, 4,901 failures, 29 skips, and 4,900 LCFail. It is retained as regression history, not the live recovery state.
The newest source-stable canonical generation is 1784152040048560798-895db0ce: 23,063 passed, 676 failed, 213 skipped, 463 LCFail, and 9 AOT process leaks overall. LLVM spec is 4,646 passed, 548 failed, 83 skipped, 463 LCFail, and 0 RC leaks; evaluator is 5,189/28/65; AOT is 2,924/73 with nine process leaks; Rust workspace is 9,291/19; Rust LLVM is 632/8; runtime is 366/0; doctests are 15 passed plus 65 skipped.
Recovery is substantial but the exact gate is still missed by 376 LLVM passes, 401 LLVM failures, 371 LCFail cases, and nine process leaks.
- The immediate gate is the producer-owned callable census: close derived/core/imported/transitive bodies, mint stable identities for tests and concrete method receivers, deduplicate convergent source routes before ARC lowering, and bind operator/runtime/registry/capability targets by exact semantic identity. Keep
LoweredArcBatchduplicate-parent andExecutableProgramclosure validation strict. - Suspend performance promotion and further semantic-surface expansion until a fresh canonical
test-allrun restores at least>= 5,022LLVM-spec passes,<= 147failures,<= 92LCFail, and zero leaks. Differences in corpus size do not excuse any baseline-green case that now fails; exact case-identity comparison remains mandatory. - A focused reproducer passing is diagnostic evidence only. Restoration is proved only by the canonical runtime’s terminal structured summary and case-level comparison with the baseline.
- If the restored run remains outside the baseline envelope, isolate and remove the responsible prototype change before resuming VM optimization. Do not normalize, waive, relabel, or accept the regression as the cost of the shared seam.
Layer Coverage
| Layer | Disposition |
|---|---|
| L1 | Covered by production spec fixtures that include accepted/rejected parse cases. |
| L2 | Covered by production compile-pass/fail fixtures before backend execution. |
| L3 | Covered by pattern/desugar fixtures executed through all applicable backends. |
| L4 | Covered by exact AIMS ownership-event/cleanup traces, stable provenance, and per-projection satisfaction checks. |
| L5 | Covered by the full tree-walker/VM observable-parity criterion. |
| L6 | Covered by the LLVM-debug parity criterion. |
| L7 | Covered by the LLVM-release parity criterion. |
| L8 | Covered by the AOT parity criterion. |
| L9 | Covered by the section cross-executor criterion. |
| L10 | Covered by the section leak-freedom criterion. |
| L11 | Covered by the full applicable spec-corpus criterion. |
| L12 | Covered by the real CLI differential criterion. |
Work Items
- Complete the production differential harness, frozen presentation-only normalizer, and full callable/spec/malformed-chunk corpus; require zero evaluator/VM/LLVM-debug/LLVM-release/AOT observable mismatches.
- Wire debug/release/AOT, cross-executor, leak, panic, isolation, and real-CLI gates into CI; flip the default only when every correctness and safety criterion is satisfied.