Closed Executable-Program Contract

Goal

Define and prove the closed backend-neutral program artifact consumed through one pure data seam by the VM, LLVM, native, compiled-WebAssembly, and JIT projections. No executor may rediscover a callable body, ownership decision, representation fact, runtime descriptor, or language dispatch rule.

Current Gap

• This section closes an existing artifact; it does not introduce a second one. ExecutableProgram (ori_repr/src/executable/mod.rs) already exists behind a validate() gate (ori_repr/src/executable/program_freeze.rs) fed by the single production producer oric::realization::program::realize_arc_program (oric/src/realization/program.rs:244, validating at :287) — the sole ExecutableProgram::validate edge. ori_arc::realize_closed_program (ori_arc/src/pipeline/mod.rs:94) is NOT that producer: it returns ArcPipelineBatchOutcome and has two non-test callers. It already carries the ownership, effect, callable, closure-adapter, retain-plan, user-drop-plan, and representation fact families. The missing work is exhaustive callable coverage, the fail-closed missing-entry diagnostic, the purity contract on the seam, and the backend-neutral naming freeze.
• The realized ARC set behind that producer is not yet a complete program: backend-local emission survives downstream of the single producer. Source-verified instances:
  • ori_llvm::codegen::derive_codegen::compile_derives consumes ori_ir::Module plus ori_types bodies directly and re-runs its own concrete-instantiation, nested-derive, and field/variant substitution discovery. Derived methods therefore never pass through the artifact. This open-world derive path is not a hypothetical hygiene concern: it anchors a live open derive-bug cluster (BUG-04-209/210/216/290, BUG-04-279, BUG-04-195, BUG-04-212, BUG-03-013), each an instance of one backend re-deriving instantiation/dispatch off the artifact. Routing derives through the artifact closes that class, not one instance.
  • FunctionCompiler::bind_executable_program is optional (executable_program: Option<_>) and documents omission as conservative. An optional binding is a fail-open the census must convert to fail-closed. It is bound through two production LLVM entry paths — the evaluator/JIT compile_all_functions path and the AOT emit_realized_program codegen path — so the fail-open exists on both; the census’s mandatory-binding rule must fail-close at each, never only one.
  • FunctionCompiler::bind_executable_method_targets documents a surviving open-world derived-method path beside the frozen method census.
• Two consumers already read the artifact, not one: the LLVM function compiler, and ori_vm::compile::compile(&ExecutableProgram), which already accepts the validated artifact as its sole input. The census and the anti-fork test cover both consumers, never LLVM alone.
• A VM over an incomplete artifact can pass arithmetic demonstrations while failing real programs.

Implementation Sketch

• Extend the backend-boundary realization seam rather than adding run_evaluation_vm()-specific orchestration. realize_arc_program is the only edge that produces the validated artifact; extending its output bundle is the whole-surface move, so no work here creates a second realization path.
• Make realization a deterministic transformation over explicit immutable frontend/import inputs. It returns a validated artifact or typed error; it cannot invoke a backend, perform I/O, inspect profiling/comparator state, or carry CompilerDb, LLVM, VM, or runtime-session handles across the seam. The purity boundary is enforced at oric::realization::program, the driver site that holds the only production call; the boundary must name explicitly what may not cross it, not rely on convention (impl-hygiene.md PHASE-06, PHASE-24, SPEC-34; DESIGN:leaky-abstraction).
• Define the closed ExecutableProgram with stable function identities, entry points, post-AIMS ArcFunctions, representation/type facts, canonical primitive-operation classifications, import and monomorphization provenance, impl-method targets, derive/built-in target descriptors, and backend-neutral runtime-call identities. RealizedProgram no longer exists anywhere in the tree; never reintroduce it as a parallel artifact, a compatibility alias, or a transitional type name. The artifact is a frozen DATA bundle consumed only through accessor queries, never a shared builder-method trait — data carries no backend API to over-fit, avoiding the failure mode of a shared-builder abstraction that mirrors one backend’s model. validate() is the closed artifact’s fail-closed semantic checker; the artifact stays closed, never open-extensible, so a consumer re-deriving meaning and a callable kind falling through are both unrepresentable rather than merely discouraged.
• Give every runtime-call identity one logical signature: value/result types, logical type or storage-site parameters, operand ownership/use, result aliasing/freshness, effects, unwind behavior, and allocation eligibility. Helper symbol, sret expansion, byte size/alignment, C ABI arity, VM handle shape, and JIT/native calling sequence belong only to the selected physical adapter. Reject an artifact whose logical arity or fact identity is incomplete; never preserve a compiled-helper operand merely because one backend currently needs it.
• Freeze AIMS results under backend-neutral domain names: logical ownership/drop events and plans, freshness, effect/access, parameter disjointness, thread reachability, COW/reuse, transfer, and unwind obligations. Atomic/non-atomic instructions and memory orderings are physical satisfactions of thread reachability, not AIMS facts. LLVM noalias/memory(...)/alias scopes, VM opcodes, native instructions, and JIT guards are downstream projections and never fields of the calculus model. A shared-carrier field whose name asserts placement, header shape, atomicity, opcode, or ABI is a presumptive fork unless it is scoped to VmLayoutPlan or CompiledLayoutPlan (impl-hygiene.md PHASE-62 LEAK:backend-ownership-calculus-fork, SSOT-19 LEAK:aims-ad-hoc-emission). FunctionAbi leaking into VM frames is the concrete instance to reject.
• Apply one anti-fork test to every current consumer, ori_llvm and ori_vm alike: they may translate shared facts into different encodings or target instructions, but neither may repeat semantic discovery, type/operator classification, ownership reasoning, callable resolution, or optimization eligibility analysis (impl-hygiene.md PHASE-54 LEAK:frontend-reimplementation; DESIGN-26 proactive-at-add for each new consumer).
• Decide explicitly whether derives become realized ARC bodies or remain typed intrinsic descriptors implemented by every backend. Either choice must be exhaustive and testable; LLVM-only callbacks are forbidden. Whichever is chosen, derive_codegen’s concrete-instantiation, nested-derive, and substitution discovery moves behind the artifact: a backend re-deriving which instantiations exist is the same fork whether the body is realized or descriptor-driven. The derive path is the single highest-risk anti-pattern on this surface (impl-hygiene.md PHASE-54 LEAK:frontend-reimplementation) and the census’s hardest, highest-value leg; read the open derive-bug cluster’s failure shapes — BUG-04-209 and BUG-04-290 first (unregistered-mono then wrong-fallback) — before fixing the disposition, so the choice closes that class rather than one instance.
• Add a compiler-surface census against every consumer of the single producer, not against LLVM alone. Realization fails with an actionable diagnostic if any reachable callable lacks a backend-neutral representation. The census obeys these rules:
  • Name every callable kind explicitly — ordinary, imported, monomorphized, impl-method, derive, built-in, closure — with a match the compiler forces to stay exhaustive as kinds are added. A boolean or subset condition that lets an unnamed kind fall through is rejected (impl-hygiene.md COVER-14, COVER-16, COVER-28 GAP:conditional-fallthrough-not-exhaustive).
  • Collapse the surviving backend-local emission paths into one canonical closed artifact plus N pure projections; the paths themselves are the duplication with no canonical home (impl-hygiene.md SSOT-18 LEAK:algorithmic-duplication).
  • Return the refined validated artifact carrying its own proof, never a boolean verdict beside an unvalidated bundle, so an unvalidated artifact is unrepresentable downstream (DESIGN:validate-not-parse, FLOW-27). Keep missing-entry distinguishable from valid-but-deferred; do not collapse them into one error (FLOW-75).
  • Make artifact binding mandatory at each consumer. Remove the optional-binding fail-open rather than documenting it as conservative. On LLVM the binding is reached through both production entry paths (evaluator/JIT compile_all_functions and AOT emit_realized_program); the fail-close covers both, never only one.
  • Extend the existing census substrate in ori_repr/src/executable/program_freeze/metadata.rs (validate_function_symbols, build_function_ids, freeze_function_metadata, freeze_roots) rather than adding a parallel coverage pass. freeze_function_metadata is the hottest, highest-betweenness symbol on the surface — the funnel every callable kind routes through; extend it with dense pins, never fork it. Its validate_function_symbols/validate_version/build_function_ids/freeze_roots/freeze_method_targets family is a near-duplicate cluster; factor it into one exhaustive per-callable-kind funnel ONLY where that funnel genuinely subsumes each — kinds needing genuinely divergent validation stay separate and share only the exhaustive dispatch skeleton, so the collapse never becomes a DESIGN:wrong-abstraction.
  • Build the census as a new leg of the existing realization diagnostic surface — oric::commands::emit_aims_state, ORI_DUMP_AFTER_ARC=1, ORI_VERIFY_ARC=1 ORI_VERIFY_EACH=1, compiler_repo/diagnostics/bisect-passes.sh — so a missing-entry failure is attributable to a realization phase and observable by diffing the realized function inventory against each consumer’s emission set. compiler_repo/diagnostics/class-ledger-census.sh --run is the structural precedent — a per-function replaced-vs-fallback census with a ranked fallback-reason table; model the callable-coverage census on that shape. A one-off script is not acceptable.
• Scope the closure to the reachable-callable set, never a monolithic whole-program freeze. Whole-program closure buys completeness at an unbounded compile cost that would defeat this plan’s own edit-run-test mission, so the artifact must be a per-callable-composable frozen bundle: close and verify only the callable set reachable from the entry roots, and cache per-function frozen facts under deterministic keys. This is why a Salsa chunk cache stays deferred — the deterministic-key precondition is unmet today, so the cache remains session-local.
• Prototype the smallest consumer against impl methods, derives, closures, imports, and monomorphizations before freezing the artifact API. ori_vm::compile::compile(&ExecutableProgram) is the existing smallest consumer; drive the fixture through the real realize_arc_program path rather than a seam-injected stub (impl-hygiene.md TEST-14 INVERTED-TDD:seam-injected-only-coverage). The section’s L12 disposition stays N/A only until an executor is wired; once the walking skeleton lands, the fixture must exercise the real entry point.

Cross-Plan Contract

• Hard prerequisite: backend-boundary#s-30e3c9a6 shared pre-codegen orchestration. It owns and freezes the seam; re-verified against source at 2026-07-24 it now reads completed+reviewed (not in-progress), so the seam owner has LANDED — co-design against the landed seam, and the 2026-07-21 defer’s stated clearing condition is satisfied (see HISTORY).
• Seam-name correction handed back from backend-boundary#s-30e3c9a6 (verified against source at head 0f3a686fc): the seam that section owns and freezes is oric::realization::program::realize_arc_program + ArcProgramRealizationInput, NOT ori_arc::realize_closed_program. realize_closed_program (ori_arc/src/pipeline/mod.rs:94) returns ArcPipelineBatchOutcome, not ExecutableProgram, and carries two non-test callers (oric/src/realization/program/aims.rs:22, oric/src/commands/emit_aims_state/mod.rs:234). Every claim in this section that names realize_closed_program as the producer of the validated artifact is corrected above; do not re-introduce that name as the seam.
• The bytecode plan extends that owner; it does not fork it.
• production-eval-architecture-contract#s-429b48fe freezes the downstream crate/dependency, purity, state, error, no-fallback, and absolute-parity contracts before this artifact becomes production API.
• Coordinate the representation triple, never invent it. ReprEvidence, VmLayoutPlan, CompiledLayoutPlan, and FunctionAbi have zero declarations in the tree today — they appear only in doc comments naming them as targets. repr-opt#13 (Shared Representation Evidence and Backend Layout Plans) owns their shape. Fixing those shapes here without that owner makes this section not independently workable. FunctionAbi therefore is a fork to prevent, not an existing type to consume — its appearance in a shared carrier is a presumptive violation.
• Coordinate the shared artifact with native-backend#s-4148408d (BIR translation) and #s-4633748c (typed-fact surface): the native backend consumes the same closed artifact, so the neutral-naming freeze is binding on it too. semantic-optimization-pipeline#03 owns the AIMS-fact / LLVM-projection boundary this section codifies; aims-provenance-ledger#s-5a317426 audits the contract after it lands.
• Downstream consumers of this artifact inside the plan: walking-skeleton#s-0279c4d5 (first thin end-to-end seam), bytecode-compiler#s-bf63aada, register-vm-dispatch#s-d34c4229, jit-handoff-contract#s-1fd9d2db, parity-verification#s-4b00387e, plus aims-interprocedural-evidence-boundary#s-f03dffb9, tagged-built-in-callable-identity#s-374b9321, uniform-evaluator-scalar-dispatch-altitude#s-dab8add2, and value-abi-runtime-alignment#s-f9b40534 for the fact families the artifact freezes.
• ExecutableProgram is a shared artifact under active co-ownership: 33 plan references, with enum-layout-ssot (its repr_plan field), repr-opt#11/#12, and bug-04-293 in progress. ArcFunction — the functions field’s element type — is under four in-progress bug plans. Any change to the struct shape reconciles with those owners first (state-discipline.md §5: plan boundaries are implementation boundaries); prefer additive fact families over reshaping functions.

Layer Coverage

Work Items

• Extend the backend-boundary realization seam into one closed backend-neutral executable-program bundle covering ordinary functions, lambdas, monomorphizations, imports, impl methods, derives, and built-in dispatch; add a coverage census and fail-closed missing-entry diagnostics.
• Prototype typed VM slots and a logical VM call convention against neutral ReprEvidence plus AIMS facts, coordinating the ReprEvidence/VmLayoutPlan/CompiledLayoutPlan shape with repr-opt#13 (Shared Representation Evidence and Backend Layout Plans, their owning section) rather than inventing it unilaterally; document the native-boundary adapter, and choose the safe Rust representation from measured correctness and dispatch evidence; defer raw native-layout frames and OSR unless the prototype proves them necessary.

Verification Obligations

• The intel graph carries per-run-variable freshness; distrust its insights, sibling-divergence, co-change, test-topology, aims-state, and rc-remarks facets regardless of any single run’s readings, and note ExecutableProgram is a data type the CALLS graph under-represents. Read the consumer surface from source — program_freeze/metadata.rs, ori_llvm/src/codegen/function_compiler/, ori_llvm/src/codegen/derive_codegen/, ori_vm/src/compile/ — never from a call-graph query, a parallel-drift nomination, or a graph-cached number.
• Re-verify the backend-local-path inventory in this section’s Current Gap against live source before scoping the census; it was source-verified at authoring time, not detector-confirmed.
• The artifact freeze and its validate() gate are unit-pinned, but the census completeness, the anti-fork property on BOTH consumers, and the missing-entry-vs-valid-but-deferred distinction are the untested surface. Write the negative pins FIRST: a callable kind with no backend-neutral representation must FAIL the census pre-fix, and the optional binding left unbound must FAIL — otherwise the census-as-validator work risks INVERTED-TDD.
• Do NOT cite a graph-cached AIMS-state or RC number; run the census-diagnostic surface live. Any RC/AOT verdict read during this work is valid ONLY on the burden-sole path (ORI_DISABLE_PREDICATE_STACK_RC=1); a default-path count is false-green (arc.md §STOP).
• Re-read backend-boundary#s-30e3c9a6 from source before treating w-8627274b’s defer as live; at 2026-07-24 it reads completed+reviewed (see HISTORY), so the graph/body state divergence resolves in favor of the completed state.
• BUG-04-266 (open — emit_unified.rs at 23x the line cap) neighbors the realization surface this work extends; do not enlarge it.

HISTORY

• 2026-07-21 — cross-plan deferral: w-8627274b is deferred on backend-boundary s-30e3c9a6 (not-started), an INV-21 merge-layer hard-defer. The plan is not done and was not closed; the block clears only through backend-boundary’s own progress.
• 2026-07-24 — prerequisite re-verified, defer basis cleared: backend-boundary#s-30e3c9a6 (the seam owner) reads completed+reviewed in source, verified via the plan read API. The 2026-07-21 defer stated it clears only through backend-boundary’s own progress; that condition is now satisfied, so the INV-21 merge-layer block basis has cleared. The orchestrator re-evaluates the block on next serve; this section did not self-flip route state.

Intel dossier — pointer and tier disposition

Dossier: executable-program-contract--s-ba8f2041.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.