Native/JIT Shared-Input Contract

Goal

Specify — and do not yet freeze — the pure semantic data seam shared by VM tier-0 and the future ori_backend compiled/JIT tier, without requiring bytecode, BIR/MIR, frames, or encodings to be identical.

The seam is asymmetric today and one endpoint does not exist. ori_vm::compile::compile(&ExecutableProgram) takes the closed post-AIMS artifact as its sole input; the compiled tier’s declared seam ori_codegen::CodegenInput carries frontend inputs (CanonResult, TypeCheckResult, Pool) and its own module doc gates widening on types absent from the workspace. ori_backend and ori_engine are unbuilt. A neutrality contract authored against one live consumer is shaped by that consumer, so this section produces a specification with a deferred freeze; the freeze happens when a second consumer exists.

Sequencing — this section executes third, not first

• s-ba8f2041 (executable-program-contract) owns the artifact, the purity contract, the anti-fork test over ori_llvm and ori_vm alike, and the backend-neutral naming freeze. Cite it; never re-specify it.
• s-429b48fe (production-eval-architecture-contract) owns the name-freeze and states VmLayoutPlan / CompiledLayoutPlan(TargetSpec) have zero definitions in tree. Its “name-freeze precedes every other item” applies transitively here.
• repr-opt#13 owns ReprEvidence / VmLayoutPlan / CompiledLayoutPlan coinage. The adoption-vs-coinage decision across these three plans is a prerequisite of this section, not a detail inside it.
• s-c22d62a9 creates the VM production entry point every parity claim here presupposes. s-4b00387e owns the parity harness, the leak gate, and the regression baseline.

Implementation Sketch

• Adopt the frozen naming; author no contract text against types absent from the workspace. Seven of the twelve contract names this section once wrote as extant resolve to zero definitions.
• Subtraction precedes addition: remove the repr_plan: ReprPlan neutrality leak from the shared artifact before adding any compiled-tier field to it. LLVM reads it in production; the VM reads it zero times in production and fabricates a dummy in test fixtures only. A shared-carrier field one consumer must fabricate is the live LEAK:backend-ownership-calculus-fork instance.
• Map onto s-ba8f2041’s shipped ExecutableProgram families — identity/provenance, callable inventory, ownership/drop, runtime-call descriptors — rather than re-specifying the artifact it owns.
• Do not route the seam through realize_closed_program: it returns ArcPipelineBatchOutcome and is not the artifact producer. The sole ExecutableProgram::validate edge is oric::realization::program::realize_arc_program.
• Keep VM VmCallSig and compiled FunctionAbi distinct, and adopt the VM’s already-coined vocabulary rather than duplicating it: PhysicalVmPlan is the live VM layout plan; VmRetainPlan / VmCalleeOwnerDemand are the live VM ownership projection. Coining a second name for either is a naming fork, not a contract.
• Each backend may lower differently; neither may add semantic discovery or reclassify AIMS ownership policy. The graph finds no convergence between the VM lowerer and the LLVM emitter, so the shared abstraction must be authored, not extracted.
• Name the oracle for disagreement: the evaluator is the representation-abstract behavioral oracle. A third executor entering a harness that already carries open two-way parity breaks will surface them as VM-vs-X mismatches; a three-way disagreement resolves to the evaluator.
• Coordinate with native-backend architecture/BIR work (s-4fa1f7d2, s-4148408d) and native-backend#s-3caa36e9 (where ori_backend first becomes real) before freezing either side.
• Any change altering ExecutableProgram’s shape budgets the ori_llvm::codegen::arc_emitter module family and ori_arc::ir into its change-set; that family is the historical co-change blast radius of the freeze/VM-compile surface.

Evidence caveats carried into this section’s claims

• The co-change blast radius above is directional, not a current count: those edges predate the current code import.
• “No convergence between the VM lowerer and the LLVM emitter” is a WEAK negative — the sibling-divergence nominations are pre-import. Read both endpoint sources before relying on it to justify authoring rather than extracting the shared abstraction.
• Module-boundary evidence for this seam is dark this run: the derived community bundle has not consumed the current import and returns no assignment for these symbols.
• Cross-repo semantic search cannot reach the ingested VM prior-art corpus (those repos are symbol-indexed but not embedded), so the prior-art path into them is symbol-name search only.
• Absence of a bug cluster for this terrain is absence of evidence — the code is new — never evidence of absence.

Ownership boundary — ori_engine

• Put the production coordinator in a narrow ori_engine layer above both executors; treat the name as a placeholder and preserve the boundary.
• Give it tiering policy, immutable profile snapshots, code-memory lifetime, safepoint transitions, and tier counters — and split those responsibilities rather than landing one type that owns policy AND lifetime AND transitions AND counters.
• Enforce safepoint and tier-entry ordering in the type system, not by convention; convention-enforced ordering is temporal coupling.
• Make ori_vm expose typed hot-region/state snapshots and checked resume points. Make ori_backend compile explicit artifacts purely into an owned JitArtifact.
• Forbid either backend depending on the other or on ori_engine; pin the dependency direction that already holds, first and independently.
• Let oric select interpreter-only versus tiered execution and construct the engine; keep hot-loop semantics outside the driver.

Observability substrate — absent, and a prerequisite

• ori_vm carries zero ORI_* seams: no tracing target, no dump flag, no ablation toggle. Tier-transition counters, deopt counts, and state-map rejections have nowhere to surface until one is created.
• diagnostics/bytecode-verify.sh does not exist; dual-exec-verify.sh is two-way (interpreter vs LLVM) with no VM leg.
• Any tracing target this seam introduces is declared in the central tracing registry (COMPILER:trace-target-central-registry); any ORI_DISABLE_* / ORI_FORCE_* tier toggle carries a test asserting its documented bisection effect (COMPILER:ablation-toggle-untested).

Prototype Tiering Matrix

• Compare static typed specialization/quickening, generated handlers, method JIT, region/loop JIT, trace JIT, and ori_backend reuse as competing measured variants.
• Run every variant against the same interpreter-only parent. Measure combinations independently; never presume additive gains.
• Record warmup, compilation latency, steady-state time, code size, memory, tier entries, bailouts/deopts, and parity.
• Tier input is explicit immutable data: ExecutableProgram, VerifiedProgram/region identity, proved type/repr/ownership facts, profile snapshot, and the adopted target-spec / compiled-layout carriers.
• Tier output is an owned artifact plus checked VM/compiled state maps.
• Forbid compiler databases, ambient runtime state, fallback callbacks, and process-global mutable profiles at the seam.
• Disable the seam in interpreter-only benchmarks; label every transition in tiered benchmarks.
• Materialize and validate a bijective OSR/deoptimization map for every live register, local aggregate/iterator/heap handle, ownership obligation, panic continuation, source location, and return continuation at each entry/exit.
• Reject tier entry on a missing or ambiguous mapping; never reconstruct semantics ad hoc. The accepted map is a refined type carrying its proof, not a bool/Result<()> verdict handing the raw frame downstream, and no incomplete-mapping case falls through silently.
• Allow LLVM JIT as a prototype comparator; keep retained production tier compilation in ori_backend.
• Forbid ori_vm dependencies on compiled backends and hidden compiled fallback for unsupported VM execution.

Ori-Original Hypothesis: Verified Tracelets

• Treat verified tracelets as a prototype hypothesis, not an adopted design. Preserve ordinary verified bytecode as the complete semantic expansion and the deopt target; a failed optimization degrades to a no-op, never a crash.
• Let a pure optimizer describe RegionPlan over post-AIMS logical identities — entry PC, covered expansion PCs/hash, live-ins/outs, normal/exceptional exits, source/effect order, runtime calls, ownership/RC delta, resource accounting, and exact state maps.
• Accept the plan only when every fact mechanically corresponds to the baseline expansion.
• State the map over logical AIMS event identities rather than physical slots, so one map validates against the VM’s physical projection and the compiled layout plan independently. The ownership-restoration term is what makes this stronger than the external prior art, which restores interpreter stack slots and explicitly excludes ownership/GC integration from its theorems.

Three constraints the prototype carries as falsifiable kill-criteria:

1. A region may not span an unresolved sharing observation. Restoring an in-flight COW mutation requires knowing which branch the physical projection took — an outcome a logical-only map cannot express. This narrows tracelet coverage, and the perf case must survive the narrowing.
2. Map preservation is a mechanically checked post-condition of every region rewrite, not an authoring convention. Snapshot maintenance under optimizer passes is where deopt bugs live in every surveyed system.
3. The contract is specified now and frozen only when a second consumer exists; neutrality is unfalsifiable while ori_backend is absent.

Measure three interchangeable implementations behind the same accepted plan:

1. a portable Rust tracelet that removes per-op dispatch while retaining checked semantic operations;
2. an AIMS-guided quickened tracelet that consumes frozen quickening-eligibility and ownership facts, guards only their declared runtime preconditions at entry, and removes redundant COW/RC checks within the region; guard failure dequickens to baseline and never reclassifies AIMS policy;
3. a native region body produced by a JIT candidate and entered/exited through the identical state maps.

• Hypothesize one proof-carrying region contract can unify superinstructions, quickening, OSR/deoptimization, and JIT without separate semantic engines.
• Exploit Ori facts dynamic VMs reconstruct: closed call targets, static types/reprs, post-AIMS ownership, and effects. Do not import the compensation machinery other systems built for static facts they lack.
• Prove any ownership-restoration claim in the compiled Lean before implementing it; the ownership-on-deopt obligation is the one thing the external literature does not cover.
• Reject the hypothesis when proof/metadata cost, optimizer fragility, parity surface, portability, or macro performance loses to separate mechanisms.
• Include numeric loops, list transform/update, reductions, calls, panic edges, and RC/COW aliasing. Execute each retained expansion as the optimized cell’s oracle.
• Benchmark combined tracelet/quickening/JIT variants against every individual parent. Require multi-program wins with absolute parity before changing production architecture.
• Land no RegionPlan / state-map / adapter machinery in production before a measured variant earns it; this work is prototype-gated and must never bind production.

Layer Coverage

Backend-layer dispositions are stated against the terrain rather than assumed. ori_vm is a [dev-dependencies] entry of oric and CodegenBackendChoice has one variant, so the VM has no production entry point; an LLVM-only parity run never covers a VM-affecting change.

Unpinned surfaces the conformance work must close

• bind_executable_program — the compiled tier’s entire consumption of the shared artifact — has zero direct test callers, and it is the consumer that reads the leaked repr_plan. The first pin here is negative: an artifact whose compiled-layout carrier is absent or neutral must still bind on the LLVM side.
• The VM’s physical-plan validator family has zero direct test callers.
• The hottest symbol in the terrain (program_freeze::validate) has zero direct test callers while its public wrapper carries the pins; the pins sit on the facade and the churn sits on the implementation.

Work Items

• Adopt (never invent) the TargetSpec / CompiledLayoutPlan / VmLayoutPlan / ReprEvidence naming frozen by s-429b48fe’s architecture decision record and repr-opt#13’s coinage; do not author these names independently. Before adding any compiled-tier field to the shared ExecutableProgram, remove the existing repr_plan: ReprPlan neutrality leak (source-verified: LLVM-only consumer, 19 production reads in ori_llvm/src, zero in ori_vm production code) by scoping it to the compiled-layout carrier those owners define — subtraction precedes addition. Then document canonical executable-program identity/provenance, operation correspondence, ownership trace, representation facts, callable inventory, and runtime-call contracts as a mapping onto s-ba8f2041’s already-shipped ExecutableProgram families (identity/provenance, callable inventory, ownership/drop, runtime-call descriptors), never re-specifying the artifact s-ba8f2041 owns. Sequence this work after s-ba8f2041 closes the artifact and s-429b48fe / repr-opt#13 land the naming freeze; do not author contract text against types absent from the workspace.
• Cite (never re-declare) s-ba8f2041’s anti-fork test and s-4b00387e’s absolute-parity / leak-freedom criteria rather than re-authoring them. Add pure-seam conformance tests proving ori_vm consumes the shared ExecutableProgram faithfully today; extend the same conformance-test class to the compiled ori_backend lowerer only once native-backend#s-3caa36e9 lands that crate — sequence the ori_backend leg on that landing rather than asserting it against a nonexistent consumer now. Freeze the ori_engine production-coordinator ownership boundary (tiering policy, immutable profile snapshots, code-memory lifetime, safepoint transitions, tier counters) as a narrow layer above both executors, with an explicit dependency-direction test forbidding either backend from depending on the other or on ori_engine. Coordinate the boundary’s shape with native-backend architecture/BIR sections (s-4fa1f7d2, s-4148408d) before freezing it.
• Prototype the Verified-Tracelets hypothesis as its own tracked deliverable (currently described only in section prose with no owning work item): define a proof-carrying RegionPlan over post-AIMS ArcVarId identities (entry PC, covered PCs, live-ins/outs, normal/exceptional exits, ownership/RC delta, exact state maps), owned by neither the VM nor the compiled tier; measure three interchangeable implementations (portable-Rust tracelet, AIMS-guided quickened tracelet, native JIT region) against the same interpreter-only parent and against each other. Carry the three constraints external prior-art triangulation (OSR-Distilled PLDI’18, sourir/POPL’21, the deopt-maintenance critique) established as load-bearing and that the section’s current prose omits: (i) a region may not span an unresolved sharing observation, (ii) map-preservation is a mechanically checked post-condition of every region rewrite, not an authoring convention, (iii) bijective OSR/deoptimization state maps reject tier entry on any missing or ambiguous mapping rather than reconstructing semantics ad hoc. Promote no mechanism without multi-program wins and absolute evaluator/VM/LLVM/AOT parity; this work is prototype-gated per the plan’s own north-star gate 7 and must never bind production.

Intel dossier — pointer and tier disposition

Dossier: jit-handoff-contract--s-1fd9d2db.intel.md (this section’s content/intel/ sidecar)

Read that dossier from line 1 through EOF before acting on this section. This block is a pointer and an audit record, never a substitute: not the BLUF, not a summary, not selected tiers.