Bytecode Compiler — ExecutableProgram to Verified Chunks

Goal

Compile the entire closed executable-program artifact to verified chunks while preserving post-AIMS control flow, calls, representation facts, and ownership operations structurally.

This is closure and inversion work on a live surface, not construction. ori_vm::compile and ori_vm::verify already exist and already consume &ExecutableProgram (compile/mod.rs, compile/instruction.rs, compile/terminator.rs, verify.rs; Verifier carries 40 methods). Every deliverable below extends that surface; none of it starts from an empty module.

Implementation Sketch

Callable and instruction coverage

• Compile stable function identities and every reachable callable category: ordinary functions, lambdas, monomorphizations, imports, impl methods, derives/intrinsics, and built-ins. Missing targets are compile errors with source context.
• Close the concrete coverage residue: the 11 ArcInstr variants compile_instruction currently rejects (instruction.rs:490-534) — RcDecPartial/RcDecField/RcDecVariant, all five Burden* carriers, and Reset/Reuse/CollectionReuse. Consume the frozen class-ledger event set, PV-6’s authority-union field decomposition, and RL-11/RL-11a/RL-12 reuse facts; never invent a VM-local skip-set or reuse rule.
• Keep unsupported_kind/unsupported_operation an exhaustive match. Replacing it with a _ fallthrough as variants land breaks the compiler-forced missing-target contract.
• Scope callable-category coverage against what the artifact actually carries today: the input is not fully closed while s-ba8f2041’s w-8627274b remains deferred on backend-boundary#s-30e3c9a6 and backend-local emission paths survive.

CFG translation and block/edge provenance

• Translate the existing ARC CFG directly. Pattern decision trees and self-tail-call rewriting have already happened; bytecode compilation must not perform either transformation again, must not consume DecisionTreePool, and must not reconstruct pattern meaning, call resolution, or tail-call structure from the op stream.
• Produce the block/edge table exactly once. compile::block_starts (mod.rs:392) already computes the ArcBlockId -> Pc map and compile_function discards it; physical::flow::discover_blocks (flow.rs:14) then re-derives block boundaries from the flat op stream. Retain that map as a first-class provenance field on BytecodeFunction and make discover_blocks a reader of it. A third independent CFG derivation inside the verifier is banned.
• Carry provenance at (block, edge) grain, not per-PC — the sparse block-boundary representation already validated as exact-analysis-preserving.
• The provenance table is a producer-emitted correspondence certificate, not an inference target: the compiler emits what it did, and the verifier never guesses the transformation.

Registers, constants, and metadata

• Allocate typed registers/slots from liveness, shared evidence, and VmLayoutPlan. Resolve enum construction/projection/drop through VmEnumLayout; keep compiled byte offsets, LLVM aggregate indices, and platform ABI thresholds out of bytecode lowering.
• Register::from_arc (bytecode/ids.rs:39) is today a raw identity map off ArcVarId, so register_count == var_types.len(). Any change to destination-register identity ships with the evaluator/LLVM parity fixture in the same change — a prior attempt broke parity at exactly this seam (static destination-register identity returned 99 where evaluator and LLVM required 37 and 73).
• Build constants, closures/captures, call descriptors, source maps, and exception/panic metadata deterministically. There is no source map on the surface today; it is new construction inside an existing struct.
• Attach ownership-event provenance once, in rc_semantics (instruction.rs:430-488), which both compile_rc_inc and compile_rc_dec already delegate to — never twice at the two call sites. If per-argument provenance is added, add it once across compile_direct_call and compile_closure_call.
• Compile output remains session-cached until deterministic key/version requirements are proven.

The provenance verifier

• Replace the global ownership-event multiset check with a two-stage, source-driven, CFG-aware verifier extending verify() -> VerifiedProgram.
• Stage A — event agreement. Each source ARC block/edge has provenance to emitted bytecode ranges; exact logical event kind, ValueSemanticsId, ExecutableDropPlanId, operand, multiplicity, order, edge, and provenance identities must agree on every reachable path.
• Stage B — plan satisfaction. Separately prove the referenced VmLayoutPlan satisfies those facts by extending physical::validation::validate_plan, not forking it. No shared physical RcStrategy equality is required, and no RcStrategy name may be encoded into a shared provenance field.
• Neither stage may consume the other’s conclusion. A verifier that checks bytecode against bytecode is the self-referential design already rejected for accepting truncated coverage, wrong operands, and unjustified copy no-ops.
• Coverage is driven by the source. Stage A iterates ArcFunction blocks and CFG edges as the driving set and demands a provenance claim for every source event and every emitted range. Unclaimed entries on either side fail closed. Iterating the certificate and checking it maps somewhere is the vacuity attack, not the check. Under source-driven coverage an unsupported ArcInstr variant is an unclaimed source event, so the coverage-residue work above and the verifier are one requirement seen from two ends.
• Join conservatively at merges. Unknown is top and rejects; an optimistic default at an unknown or unreachable edge is an unsound summary.
• Validate once at branding, never per execution entry. The check runs inside verify() before branding and adds zero per-execution cost. Do not add per-execution validation at physical::prepare_candidate.
• The verifier checks agreement with the frozen events, never whether the events are correct. Event correctness is PV-1..PV-6 and RL-2/RL-4/RL-5, proved upstream; a VM-side ownership decision is ad-hoc AIMS emission.
• Fused instructions prove an equivalent logical expansion of the frozen event set.
• Keep the provenance check its own pass over the block/edge table. Verifier::operation (span 74, fanout 16, betweenness 145) and compile_terminator (span 108) are the two largest structural risks in the surface; per-edge ownership logic must not become another arm of the opcode match.
• Verify every chunk before execution; compiler and verifier failures are diagnostics, not panics. verify() failing is the product working — no gate, early return, or #[cfg] may make the verifier skip a class of function.

Sequencing

• Land the BytecodeFunction provenance-field shape change as its own commit, before verifier logic. Its blast radius lands on the crate’s highest-churn cluster (physical::prepare_candidate, physical::analysis::prepare_function, physical::prepare, physical::solver::analyze), so behavior and restructure stay in separate commits.
• Write the negative pins first and confirm them red. The established shape in compile/tests.rs is forge-and-reject (verifier_rejects_forged_non_atomic_rc_semantics, verifier_rejects_parameter_ownership_metadata_drift, verifier_rejects_closure_capture_arity_drift, verifier_rejects_stale_closure_adapter_retain_plan); the CFG-aware matrix forges a dropped, duplicated, or reordered ownership event on one edge and asserts rejection.
• Scope the TDD matrix by reading compiler/ori_vm/src/compile/tests.rs and compiler/ori_vm/src/physical/tests/ directly, and L11 scope from tests/spec/ directly. The graph’s test-topology and spec-diagnostics tiers are substrate-dark for this surface and their zeros are not evidence of missing coverage.

Ground truth and observability

• Compare emitted chunk events against ORI_DUMP_AFTER_ARC=1 (the post-AIMS ArcFunction CFG) and ORI_DUMP_AFTER_BURDEN=1 (the class-ledger event identities placed at Step 4b). Those two dumps are the reproducible ground truth for “exact logical event kind, multiplicity, order, edge”.
• Any RC/ownership comparison against the compiled projection must be read under ORI_DISABLE_PREDICATE_STACK_RC=1 ORI_VERIFY_ARC=1 ORI_VERIFY_EACH=1. A default-path RC reading is false-green and is not admissible evidence.
• There is no VM diagnostic script and no ORI_VM_* env seam. That gap routes to /improve-tooling, never into this section’s code. Any verification toggle added here ships with a test asserting its documented effect.

Design Constraints

• One block/edge table, produced once at compile time, consumed by verify and physical — no second or third derivation.
• The verifier consumes ArcFunction facts; it never re-derives frontend meaning from the op stream.
• The verifier checks agreement against frozen AIMS facts; it never decides an ownership question, and VmLayoutPlan satisfaction stays a separable proof.
• Field-grain decs and reuse come from PV-6 and RL-11/RL-11a/RL-12; no VM-local skip-set or reuse rule.
• Missing-target and unsupported-variant handling stays an exhaustive compiler-forced match.
• verify() keeps returning the proof-carrying refined type; the unverified state stays unrepresentable downstream. No boolean verdict beside an unvalidated chunk.
• Unknown facts at merges are conservative-top and reject.
• Constrained symbols — pre-existing external hazards, none of them this section’s deliverable:
  • physical::flow::discover_blocks — make it a consumer of emitted provenance; extending it as a third derivation entrenches the duplication.
  • Register::from_arc — do not change destination-register identity without the evaluator/LLVM parity fixture in the same change.
  • physical::validation::validate_plan — fold Stage B into or beside it; replacing it re-opens the rejected self-referential design.
  • physical::prepare_candidate — the pre-branding entry the validate-once contract hangs off; add no per-execution validation here.

Ownership Boundaries

• s-ba8f2041 executable-program-contract owns the sole input and names ori_vm::compile::compile(&ExecutableProgram) as its existing smallest consumer. Any change to compile()’s signature or BytecodeFunction’s shape reconciles with that section’s anti-fork test before landing.
• s-55a7979e isa-design owns opcode semantics, versioned deterministic chunks, and the encoding verifier (bounds, register types, CFG targets, call signatures, constants, RC opcode operands, version compatibility). This section owns the provenance verifier.
• s-d34c4229 register-vm-dispatch consumes the chunks; s-4b00387e parity-verification owns the L9 cross-executor corpus and the L10 leak corpus.
• s-c22d62a9 ori-run-test-integration owns the production entry point.
• The Compiler seam is already pure — source: &ExecutableProgram plus five append-only side tables, no I/O, no session handle, no LLVM type. Keep it that way for s-429b48fe.

Layer Coverage

Coverage Gaps Carried Into Execution

• The input artifact is not yet closed (s-ba8f2041 w-8627274b deferred on backend-boundary#s-30e3c9a6; surviving backend-local emission via ori_llvm::codegen::derive_codegen and optional bind_executable_program). “Compile the entire closed artifact” is bounded by what the artifact carries at execution time.
• The intel graph carries no in-house or reference-repo prior art for verifying that a bytecode lowering preserves ownership events per path; the reference interpreters in the graph emit bytecode without a separate verification pass. Design from the section’s own contract, not from a graph nomination.
• History-coupling and community/divergence facets are stale for this surface. Budget the change-set structurally from the call adjacency and the ISA/physical boundary, not from co-change history.
• A callers <symbol> zero result is not evidence of an unused symbol anywhere in ori_vm; use the exact-file catalog query.
• This validator proves preservation, never correctness. If AIMS placed events incorrectly, nothing here catches it — that remains the L9/L10 criteria owned by s-4b00387e.

Work Items

• Compile the closed executable-program artifact to deterministic verified chunks, including all callable categories, typed register allocation, constants, closures, source maps, and actionable missing-target failures.
• Compile the closed executable-program artifact to deterministic verified chunks, covering every reachable callable category (ordinary functions, lambdas, monomorphizations, imports, impl methods, derives/intrinsics, built-ins) with actionable missing-target compile errors. Close the 11 currently-rejected ArcInstr variants (RcDecPartial/Field/Variant, the five Burden* carriers, Reset/Reuse/CollectionReuse) by consuming the frozen class-ledger event set, PV-6’s authority-union field-decomposition, and RL-11/RL-11a/RL-12 reuse facts directly — never inventing a VM-local skip-set or reuse rule. Retain the ArcBlockId -> Pc block/edge map already computed by block_starts as a first-class provenance field on BytecodeFunction instead of discarding it, so physical::flow::discover_blocks becomes a consumer of that field rather than an independent re-derivation. Allocate typed registers/slots from liveness, shared evidence, and VmLayoutPlan; ship any change to destination-register identity together with the evaluator/LLVM parity fixture in the same change (per the register-allocation parity break recorded in ledger attempt #7). Build constants, closures/captures, call descriptors, source maps, and exception/panic metadata deterministically.
• Translate the already-lowered ARC CFG directly (no DecisionTreePool re-consumption, no tail-call rediscovery) and implement a two-stage, source-driven block/edge/path-sensitive ownership-operation provenance verifier extending verify() -> VerifiedProgram, validated once at branding and never per execution entry (per ledger attempts #16/#18). Stage A checks exact logical event kind, ValueSemanticsId, ExecutableDropPlanId, operand, multiplicity, order, and edge agreement between each source ArcFunction block/edge and its emitted bytecode range, iterating the SOURCE ArcFunction blocks and CFG edges as the driving set and demanding a provenance claim for every source event and every emitted range so an unclaimed entry on either side fails closed — this is the fix for the self-referential-verifier dead end ledger attempt #13 rejected. Stage B separately proves the referenced VmLayoutPlan satisfies those frozen facts (extending physical::validation::validate_plan); neither stage may consume the other’s conclusion. Join facts conservatively at CFG merges (unknown is top and rejects). Fused instructions must prove an equivalent logical expansion of the frozen event set, never re-derive or locally decide ownership.

Intel dossier — pointer and tier disposition

Dossier: bytecode-compiler--s-bf63aada.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.