Production Eval Architecture Contract

Goal

• Freeze the clean production destination before prototype code can become architecture by inertia.
• Use pure typed transformations, one owner per transform, explicit state/effect boundaries, and one closed program.
• Keep the tree-walker independent and require absolute evaluator/VM/LLVM/AOT/ori_backend parity.

Deliver a decision record plus enforcement tests, never a feature implementation. The vertical artifact spine already exists and is hot; the horizontal physical-plan split is prose. Name-freeze precedes every other item here.

• Land the dependency/impurity architectural tests before the ADR; they are unblocked today and depend on no naming decision.
• Treat every remaining item as blocked on the name freeze.

Destination Dataflow

source/module graph
    |
    v
oric frontend queries: parse -> typecheck -> canonicalize
    |
    +-------------------- CanonProgram ---------------------> ori_eval
    |                                                          |
    v                                                          v
oric::realization (one owner; no backend callbacks)        EvalOutcome
    |
    v
ori_repr::ExecutableProgram::validate()
  closed callable inventory + post-AIMS ARC + ReprEvidence + AIMS carriers
    |
    +--------------------------+--------------------------------------+
    |                                                                 |
    v                                                                 v
ori_vm::plan_layout                                          ori_target::TargetSpec
    |                                                                 |
    v                                                                 v
BytecodeProgram -> verify -> VerifiedProgram       ori_repr::CompiledLayoutPlan
    |                                                       /                  \
    v                                                      v                    v
VmSession::execute                                  ori_llvm adapter       ori_backend
    |                                                LLVM artifact       BIR/MIR/emit
    v                                                      |                    |
VmOutcome                                                  v                    v
                                                     LlvmOutcome       BackendOutcome
                                                                    machine artifact or
                                                                  complete WebAssembly module
    |                                                        |                    |
    +--------------------------+-----------------------------+--------------------+
                               |
                     normalized ExecutionOutcome
                               |
                    oric presentation/diagnostic boundary

Names are illustrative until the architecture decision record is locked; ownership and dependency direction are normative.

• Keep the tree-walker as an independent semantic oracle over canonical IR.
• Never force the tree-walker to consume post-AIMS ARC.
• Derive CanonProgram and ExecutableProgram from one immutable frontend snapshot with shared provenance.
• Feed the exact validated ExecutableProgram identity and callable inventory to VM, LLVM, and ori_backend.
• Emit WebAssembly directly through ori_backend; exclude ori_eval and ori_vm from its code generation.

Crate and Module Ownership

This table states the destination, not the build graph. Ground every row before the ADR cites it:

• Allow oric -> {ori_eval, ori_vm, ori_codegen, ori_llvm, ori_backend} and ori_vm -> ori_repr.

• Allow {ori_llvm, ori_backend} -> {ori_codegen, ori_repr, ori_target} and ori_codegen -> {ori_repr, ori_target}.

• Allow ori_repr -> {ori_target, ori_arc, ori_types, ori_ir} and executor/runtime adapters -> ori_rt.

• Forbid dependencies among ori_vm, ori_llvm, and ori_backend; reject reverse/lateral edges in tests.

• Compute shared semantic facts, legality, proofs, identities, runtime contracts, and eligibility once upstream.

• AIMS is not an LLVM-specific phase and LLVM is not its terminal consumer. VM, LLVM/native, compiled-WebAssembly, and JIT are sibling physical projections of the same exact logical fact identities.

• Maintain exactly one kernel-checked AIMS calculus and one post-AIMS semantic ownership plan for VM, LLVM, ori_backend, and later JIT tiers. Backend validation proves encoding fidelity; it never re-derives ownership policy.

• Keep the evaluator outside the physical AIMS branch as the representation-abstract behavioral oracle. Observable parity with the evaluator never means duplicating or simulating the ownership calculus inside ori_eval.

• Enforce proof-first chronology at the seam: compiled Lean theorem -> conforming Rust realization -> validated typed carrier -> backend-private encoding. A prototype cannot self-fund, weaken, or reinterpret ownership evidence.

• Compute compiled layout, enum encoding, calling ABI, header shape, and runtime declarations in CompiledLayoutPlan.

• Keep VM storage in the VM; keep IR mapping, selection, allocation, relocation, and emission in compiled backends.

• Treat VM frame/arena recycling and compiled target layout as physical lifetime mechanisms below the shared ownership seam. Neither may add, suppress, or reclassify a calculus-owned transfer, retain, release, COW, drop, or unwind event.

• Treat a repeated backend match/analysis as a seam defect and move it upstream before promotion.

• Close ordinary functions, impl methods, derives, intrinsics, and registry-owned bodyless runtime calls in the same executable inventory. Direct LLVM derive synthesis or method-spelling dispatch blocks VM production promotion.

Pure Seam Contracts

Each seam accepts immutable explicit inputs and returns owned/borrowed data or a typed error. Hidden reads, callbacks, logging, environment access, global mutation, and backend-specific handles are forbidden inside the transformation.

Pure means referentially transparent at the boundary: profiling counters may observe a stage from outside it, but a stage cannot alter semantics, inspect a comparator, or choose a different result because profiling is enabled.

Grounded seam facts the ADR pins rather than assumes:

• ori_arc::pipeline::realize_closed_program has exactly two admitted production callers, both in oric (realization/program/aims.rs, commands/emit_aims_state/mod.rs). Pin caller-crate = oric on that exact function.
• The one-owner realization invariant is protected by convention today; only an architectural test makes it load-bearing.
• Verification’s fail-closed totality is the seam most exposed to malformed input; pin positive and negative cases on it before the ADR closes.
• ExecutableProgram::validate and program_freeze::validate are the repo’s #1 and #3 hotspots. Any re-shaping of the admissibility gate re-shapes both at once; sequence it behind the architectural pins.

AIMS Calculus and Physical-Projection Boundary

AIMS must answer semantic obligations and admissibility questions, never select a backend mechanism. AIMS is not an LLVM calculus; the shipped implementation’s LLVM-shaped carriers and backend-local call sites are migration debt, not its architectural scope.

Replace the transitional physical-strategy fields embedded in the current RL-14..RL-21 carrier implementation with a neutral fact product whose stable identity is bound into ExecutableProgram; compose representation-owned neutral extent evidence beside it:

Each physical planner returns both a plan and a validation witness against the exact fact identity:

• plan_vm(program, vm_options) -> ValidatedVmLayoutPlan may select registers, generation-checked handles, typed arenas, regions, packed fields, or VM-owned counters.
• plan_compiled(program, target) -> ValidatedCompiledLayoutPlan may select stack, caller storage, regions, heap, exact header width, offsets, ABI classes, and compiled runtime adapters.
• A plan may conservatively choose a longer-lived or wider-capacity representation. It may not choose shorter lifetime, insufficient sharing capacity, weaker cleanup, weaker synchronization, or externally incompatible layout.
• Validation proves satisfies(plan, facts) and exact program/fact identity; it does not rerun AIMS. Missing, stale, mismatched, or malformed facts fail closed.
• LLVM, native, direct WebAssembly, VM, and JIT lowering consume only validated plans. Any local test of source type, name, RC value, LLVM type, VM tag, or target layout that changes an AIMS-owned event is an architecture violation.
• Physical event elision is legal only when the bound AIMS artifact already carries the corresponding discharge/eligibility fact. A backend cannot create a new proof from layout or runtime state.

This split keeps one calculus while permitting different physical winners. For example, the VM may satisfy a function-lifetime fact with a traced session arena while compiled code uses an alloca or region; both preserve the same transfer/drop/unwind contract without sharing representation.

Physical vocabulary already sits inside the neutral crate. Name the disposition of each site in the ADR:

• RcStrategy is defined twice: ori_arc/src/ir/repr.rs:128 (the ARC IR carrier scheduled for retirement) and ori_repr/src/plan/query.rs:60 (inside the crate this contract designates backend-neutral).
• RcAtomicity is defined at ori_arc/src/ir/repr.rs:181.
• Decide which definition dies and which becomes a CompiledLayoutPlan-private field; a physical count-strategy enum living in ori_repr is the exact fork this boundary forbids.
• Make the no-physical-vocabulary gate an architectural test, not a review convention. It is the single most load-bearing clause in this contract: every remaining anti-pattern collapses the neutral facts and the physical plans into one another.

Enforce the one-declaration principle by exhaustive closed matching, never by code generation:

• Author each operation’s contract once as declarative data and require every consumer to match it exhaustively, so a new declaration fails to compile until every executor handles it.
• Reject whole-tier code generation from one instruction DSL. The tiers deliberately do not share a value representation, so generation either leaks physical vocabulary into the neutral declaration or emits only dispatch shells while the hand-written bodies drift.
• Reject promoting the tree-walker to the specification. The written spec is SSOT over every implementation including the evaluator; the evaluator is a consumer of the definition, never the definition.

Closed Executable Program

The validated artifact must contain or reference, with stable identities and deterministic ordering:

• the source/module/frontend provenance needed to correlate all executors;

• every reachable ordinary function, lambda, monomorphization, import, impl method, derive/intrinsic, and built-in target;

• post-AIMS ArcFunction CFGs and exact logical ownership-event kind, bound fact/drop-plan identity, operand, multiplicity, order, transfer edge, cleanup, and provenance identity;

• typed primitive-operation semantic descriptors, including result ownership, provenance, operand use, and logical allocation effects, plus optimization eligibility facts consumed identically by VM, LLVM, and ori_backend;

• entry points and a closed direct/indirect call-target census;

• neutral ReprEvidence, typed AIMS carriers, type/constant metadata, and backend-neutral runtime-call descriptors from which VM and compiled call contracts are projected;

• backend-neutral AIMS freshness, effect/access, disjointness, transfer, thread-reachability, unwind, and logical drop-plan facts. Atomic instructions, LLVM attributes, and metadata are projections of these facts, never artifact vocabulary or an AIMS-specific destination;

• an artifact/schema version and all inputs needed for a deterministic cache fingerprint.

• Fail construction on a missing callable, runtime descriptor, representation fact, ownership provenance, or version.

• Forbid VM, LLVM, and ori_backend from lazily discovering or synthesizing missing semantic items.

• Represent derives as realized bodies or closed typed intrinsic descriptors; forbid backend-only semantic callbacks.

Validity carried by the type requires one gate and one fingerprint. Ship them together:

• Name ori_repr::executable::ExecutableProgram::validate (executable/mod.rs:217) the sole fail-closed admissibility gate; demote program_freeze::validate, validation.rs checks, and external::validate_external_callables (external.rs:369) to its private internal stages.
• Forbid any consumer from re-checking what the validated type already proves.
• Treat the deterministic artifact fingerprint as part of the validated-type deliverable, not a follow-on. Validity scoped to an ambient type pool, interner, and registry is a validated artifact plus an unwritten precondition; the prototype’s pool-address-identity guard is migration evidence, not the contract.
• Bind every fact identity to function and site so a fact cannot be replayed across functions or forged by a caller.

Add the remaining fact families through one indexed fact table, never an N+1 accessor pair:

• ExecutableProgram exposes parallel per-FunctionId accessors that differ only in the fact type they index: function_effects (mod.rs:313), fresh_return_facts (:319), param_disjointness (:331), callable_facts (:337). Confirmed at source, not a stale nomination.
• Index newtypes re-derive the same index/from_index boilerplate at mod.rs:50/:54, mod.rs:82, and external.rs:53/:57. Collapse them behind one shared index definition; this is the lowest-risk cleanup in scope.
• Keep the external_function / external_functions pair; a lookup plus an iterator is legitimate.
• Confirm function_family_lambdas (mod.rs:256) adds behavior beyond forwarding to FunctionFamilyTopology::lambdas before retaining it.

VM Artifact and Runtime Boundaries

• Lower and prepare through explicit readiness types: ExecutableProgram -> BytecodeProgram -> VerifiedProgram -> PhysicalVmPlan. Only a plan bound to one immutable verified-program identity is executable; the identity plan preserves the unfused generic reference lane.
• Use the selected safe verified VM slot model and logical VmCallSig; compiled FunctionAbi is shared by LLVM and ori_backend but does not define VM frames. No transmute, native-frame aliasing, or raw native-layout slot is assumed.
• Bytecode contains stable function/constant/type/runtime-call indices, explicit control-flow targets, and references to exact logical ValueSemanticsId/ExecutableDropPlanId facts. Physical count strategy, header, synchronization, or helper operands belong to the validated VmLayoutPlan adapter, not the shared ISA contract. Encoding version and verifier limits are mandatory.
• Verification checks opcode shape, operand/register/constant/function/type indices, branch targets, call signatures, entry points, ownership operands, resource ceilings, and reachable fallthrough before dispatch.
• PhysicalVmPlan is an overlay, not another semantic instruction language. It carries canonical-PC maps, logical-to-physical bindings, plan-owned metadata/footprint metrics, and verifier-derived proofs; generic, fused, and later JIT execution reuse the same primitive semantic contracts and exact AIMS order.
• Treat canonical-plus-physical retention as measured memory, never as free preparation state. A production physical plan retains the verified identity and only cold expansion/source/state data that execution or diagnostics require; duplicated operand/proof tables must earn their bytes, and the optimized run may release reconstructible canonical storage once its selected plan is self-sufficient. Differential testing constructs separate reference and candidate plans rather than forcing every production session to retain both executor images.
• Physical preparation cannot mutate or specialize VerifiedProgram in place, consult benchmark/profile identity implicitly, or introduce a mid-run fallback. Interpreter-only runs disable tier creation; a separately labeled tier service consumes explicit region/state maps without making ori_vm depend on LLVM or compiled ABI frames.
• Each physical entry owns an ordered, nonempty canonical-PC span. A canonical-PC-indexed reverse map records the owning physical entry, offset, ordered read/write bindings, state roots, and normal/exceptional continuation facts. Construction rejects gaps, overlap, out-of-order spans, out-of-bounds bindings, and failed round trips.
• Every canonical operation remains one logical step. With probes enabled or insufficient remaining fuel for a span, the same physical plan enters per-PC progress mode and stops at the exact canonical prefix. An infallible, effect-free span may batch its count only when fuel covers the complete span and probes are disabled.
• Synchronize canonical PC and committed step count before every fallible arithmetic site, allocation, runtime call, RC operation, effect, call, return, panic, unwind, or cleanup boundary. A failing optimized site reports the same error, PC, logical-step count, roots, output prefix, and ownership state as its retained canonical expansion.
• Select profiled versus unprofiled execution once at entry. Profiled physical spans emit one event per canonical PC in source order; opcode, pair, region, and quota-prefix records must equal the canonical reference path exactly.
• VmSession owns registers/frames, heap/handle tables, runtime services, limits/fuel, panic state, output capture, counters, and leak accounting for exactly one execution. A test gets a fresh session; parallelism is enabled only after isolation and race stress pass.
• Runtime services are a narrow injected capability surface. Production printing, panic construction, time/random/environment access, and other effects cannot be reached through ambient globals.
• Logical ownership and alias-isolation obligations execute in exact post-AIMS order. A physical planner may realize them with counters, tracing, copying, recycling, regions, or a proved no-op only when its validated satisfaction witness permits that choice; prototype no-op event tracing is evidence tooling only and is forbidden in production.

Backend Selection and Fallback Policy

• Keep codegen choice and execution choice as separate axes.

• Use CodegenBackendChoice { Llvm, Native } only at the compiled boundary used by ori build.

• Use ExecutionBackend { Vm, Compiled(CodegenBackendChoice) } for ori run and ori test.

• Flatten execution choices to the user-facing --backend=vm|llvm|native values.

• Treat EvalMode::Const as a compiler mode and TargetSpec::Wasm32* as a compiled target.

• Keep the enums closed and exhaustively matched; Ori has no out-of-tree backend requirement.

• ori run --backend=vm and ori test --backend=vm either execute wholly in the VM or return a typed unsupported/compile/verify/runtime diagnostic. They never silently call ori_eval or LLVM.

• Const evaluation explicitly uses ori_eval. Direct WASM build/run uses CodegenBackendChoice::Native plus a WASM TargetSpec, emits a complete module, and uses an explicit WASM runtime/host adapter when execution is requested. No tree-walker or bytecode path is involved.

• --dual is an explicit diagnostic request that independently runs selected executors from the same frontend provenance and compares outcomes. It is never invoked implicitly in production.

• Prototype harnesses must report entered_vm, fell_back, unsupported, and failed separately. Fallback results do not count toward VM coverage or performance.

Absolute Parity Contract

For every applicable accepted program, evaluator, VM, LLVM debug/release/AOT, and admitted ori_backend targets must agree on:

• result value and type, stdout bytes/order, exit status, and test outcome;

• panic versus success, panic/stack-overflow class, and source attribution;

• evaluation/effect order and externally visible runtime calls;

• deterministic diagnostic identity/class for equivalent failures;

• ownership/cleanup outcome, leak counters, and required RC trace correspondence.

• Allow only a frozen, reviewed normalizer for inherently nondeterministic presentation fields.

• Forbid value rewrites, output reordering, diagnostic merging, panic suppression, and leak/ownership concealment.

• Treat a mismatch as a correctness failure at the owning phase.

• Invalidate the corresponding performance sample and block production adoption.

The evaluator oracle is necessary and provably insufficient. Ownership divergence is below observable behavior:

• An arena versus an alloca is unobservable, so an output diff against the evaluator cannot detect an ownership-trace divergence until it leaks or double-frees.
• Treat the ownership-event-trace equality obligation as a second, separate check: every tier erases to the identical logical event trace while its mechanism differs.
• That check has no instrument today. The two-build RC diff compares two compiled builds, not a VM against a compiled build. Build the cross-tier ownership-event-trace comparison before any parity claim here counts as evidence.
• Make the oracle relation a gate over the frozen denominator, not a report.

RC and ownership evidence is admissible only from the burden-sole path:

• Cite only readings taken under ORI_DISABLE_PREDICATE_STACK_RC=1 ORI_VERIFY_ARC=1 ORI_VERIFY_EACH=1.
• Treat a default-path RC count as false-green and inadmissible as an ADR fact.
• Rank surviving counter actions by their named non-discharge cause; each survivor names the AIMS dimension whose proof was insufficient, and a survivor concentrated in a top hotspot is where a backend-local shortcut is most tempting.

Errors, Limits, and Cache Lifetime

• Use typed RealizationError, bytecode compile/verify errors, and VmError/resource-limit outcomes internally; convert to user diagnostics once in oric. Do not propagate String as the architectural error contract.
• User-controlled recursion, frames, registers, bytecode, constants, aggregate sizes, iterator steps, and verifier work carry checked limits/overflow handling. Malformed input never panics or reaches a runtime call.
• Start with an explicit session-local cache keyed by executable-program fingerprint, VM encoding version, target-independent options, and all representation inputs. Cache values are immutable verified programs.
• Salsa/persistent caching is deferred until deterministic equality/hash/serialization and invalidation tests exist for every transitive input. No cache holds CompilerDb, LLVM contexts, runtime services, or per-run state.

Prototype-to-Production Decision Rule

• Judge prototype components individually.
• Retain production-shaped code in its final owner only after every API, seam, test, parity, safety, and hygiene gate.
• Treat example code, duplicates, fallback, semantic shortcuts, no-op RC, and comparator-specific paths as disposable.

1. record measured decisions and rejected alternatives in the architecture decision record;
2. classify each component as retain, harden in owner, replace, or delete, with a named invariant/test for every retain decision;
3. keep production-owned APIs in place when they already implement the destination seam, and port only behavior justified by parity, safety, and profiling evidence from disposable harnesses;
4. delete the prototype harness and every duplicate opcode/value/dispatch definition before the production section can close;
5. reject any retained backend implementation that re-derives a semantic fact available to another backend instead of consuming one shared fact.

Evidence admissibility for the architecture decision record:

• Verify every graph-sourced claim against source before recording it; the code-intelligence embedding, insights, sibling-divergence, co-change, test-topology, rc-remarks, and aims-state facets are stale.
• Never read a zero-caller result on an impl method as dead code; method-call resolution is systematically under-resolved, and the artifact validate/freeze pair reports zero callers while ranking as a top hotspot.
• Treat a zero-row hygiene or co-change result as unknown, never as clean.
• Treat the reference-VM corpus as name-navigable only. Cross-repo semantic search is unavailable for the six ingested VM repositories, and the north-star interpreter’s bytecode handlers are assembly the extractor does not index.
• Read the peer projects’ interpreter-relocation and interpreter-dispatch defect history before writing the ADR’s evaluator-boundary clause. A peer relocating its interpreter onto a lower shared IR is currently fixing dispatch and closure-capture defects while doing so; a peer with a shipped ownership model carries an order of magnitude more ownership-verifier issues than any other repository in the corpus. Both raise this contract’s bar.
• Derive Ori’s design independently from typed ARC/AIMS contracts; peer source study informs design pressure only.

Live Prototype Evidence Ledger

The 2026-07-14 worktree prototype is intentionally landing candidate production seams directly in their proposed owners while retaining a thin example only for measurement.

• Treat the earlier fused example’s 88.4 ms versus Python’s 777.2 ms reading as strategy evidence only.
• Reject it as a production result because the operations were example-owned and production gates were not met.
• Measure the production-shaped baseline and every explicit bytecode optimization pass separately.

Cross-Plan Contract

• Extends backend-boundary#s-30e3c9a6; that plan owns extracting shared pre-codegen orchestration.
• Coordinates artifact identity and translation with native-backend#s-4fa1f7d2 and native-backend#s-4148408d without importing BIR, compiled ABI, or target layout into the VM; repr-opt#13 owns the shared TargetSpec/CompiledLayoutPlan correction used by both compiled backends.
• Treats direct compiled WASM as a plans/native-backend deliverable and explicitly excludes evaluator-hosted or VM-hosted WASM execution from this plan.
• This section is the architectural prerequisite for value ABI, walking skeleton, ISA, compiler, dispatch, integration, parity, and performance work.

Coordinate with the owning plans; do not absorb their deliverables. This section owns the decision and the enforcement:

• Coordinate any ExecutableProgram rename with backend-boundary and native-backend in one change set; the name is referenced by 12 plans. PhysicalVmPlan is VM-private and renameable unilaterally.
• Express the ori_backend parity requirement as a contract clause plus a blocking pointer to native-backend#s-4fa1f7d2, or narrow it to evaluator/VM/LLVM with the deferred half carrying a concrete anchor. It is not completable inside this section.

Layer Coverage

• Treat the L9, L10, and L12 rows as close-blocking until their stated gates hold; do not restore a bare Covered.
• Re-verify each row against the two-dimension executor requirement: cross-executor parity and resource/ownership leak-freedom are separate legs, and neither alone satisfies the backend dimension.

Work Items

• Prove forbidden dependency and impurity constraints with architectural tests, including no oric, ori_llvm, or ori_backend dependency from ori_vm; no backend callback during realization; one shared compiled layout/ABI classification; and no mutable process-global execution state.
• Freeze the production eval dataflow, module ownership, dependency direction, pure seam APIs, typed error boundaries, state lifetime, and no-fallback invariants in an architecture decision record informed by prototype evidence. The ADR MUST explicitly decide and record: (1) the name-freeze order for VmLayoutPlan, CompiledLayoutPlan(TargetSpec), TargetSpec, and RuntimeCallSpec — none of which exist in the tree today — coordinated in the same change set with repr-opt#13 and native-backend#s-4fa1f7d2/#s-4148408d so a name is not picked in isolation and then contradicted by a sibling plan; (2) ori_codegen’s disposition — either commit ori_llvm to depend on it and implement CodegenBackend (coordinated with backend-boundary#s-90024726, which owns that wiring) or explicitly record ori_codegen as target-only/not-yet-wired — rather than let the crate-ownership table describe an intention as if it were the current build graph; (3) which single validator (ori_repr::executable::ExecutableProgram::validate, program_freeze::validate, or one of the validation.rs functions) is the sole fail-closed admissibility gate, demoting the remaining near-duplicate validators to its private internal stages.
• Implement the shared immutable executable-program realization and fixed execution/codegen routing so tree-walker, VM, LLVM debug/release/AOT, and admitted ori_backend targets preserve absolute observable parity — including the ownership/cleanup event trace and RC-trace correspondence required by the Absolute Parity Contract, not merely output/value behavior — without duplicated semantic discovery. Re-root every differential/parity fixture onto realize_closed_program() -> ExecutableProgram::validate() production output rather than hand-constructed ori_repr::plan::ReprPlan::new() inputs (the current pattern in ori_vm/ori_llvm test fixtures), and build or wire the cross-tier ownership-event-trace comparison instrument this requires, before any parity claim in this section’s Layer Coverage table counts.

Intel dossier — pointer and tier disposition

Dossier: production-eval-architecture-contract--s-429b48fe.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.