0%

Post-Bytecode Contract Audit

Goal

Freeze the real post-bytecode integration seam before changing provenance code. This section executes only after the terminal section of plans/bytecode-vm and treats the implementation that actually shipped as authoritative over proposal-era names.

Entry Contract

The hard structural dependency is bytecode-vm#s-07271bdd. The audit begins from the completed ExecutableProgram-equivalent product, its verifier, stable function/call/event/drop/retain identities, runtime call description, and the separate VM and compiled physical-planning surfaces. Candidate names in this plan are explanatory; the seam record must bind to actual source symbols and tests.

The evaluator remains an independent canonical semantic oracle. It may observe and compare normalized logical events, but it does not consume compiled layout or become another physical realization of AIMS. AIMS remains the sole authority for logical ownership, lifetime, extent, owner-bound, cleanup, thread-reachability, and external-visibility facts.

Required Disposition

The audit produces an exhaustive table for every ownership-relevant field and carrier: producer, logical meaning, stable identity key, verifier rule, VM consumer, compiled consumer, evaluator observation, and retirement status. It also records which bytecode-vm checks are reused verbatim and which AIMS-specific checks extend them.

The transferred burden-tracking obligations are explicit here so closure loses nothing: current executable conformance and VF-7 continue in this plan; cross-block TRMC admission moves to semantic-optimization-pipeline; per-iteration allocation elision and proven-unique list mutation move to repr-opt; LLVM sanitizers, Alive2, and nightly verification remain supported and are not torn down.

Banned Approaches

Do not preselect names from the bytecode plan without verifying the landed implementation. Do not duplicate ExecutableProgram, bytecode verifier logic, stable ID allocation, runtime call schemas, or layout planners. Do not make evaluator execution depend on VM or compiled layout. Do not carry mechanism-shaped ownership decisions in shared logical IR merely to preserve a transitional API.

Completion Evidence

The section closes only when the binding seam decision and machine-readable inventory agree with the completed bytecode implementation, every transferred obligation has a successor, and the contract-audit probe reports PASS.

Work Items

  • Read the completed bytecode-vm implementation, tests, verifier contracts, and terminal decision records after bytecode-vm#s-07271bdd; record the actual shipped executable-artifact, stable-identity, call-signature, layout-plan, cleanup, and executor-projection symbols without assuming the proposal-era names survived unchanged.
  • Write content/decisions/03-post-bytecode-contract.md as the binding seam map: one closed backend-neutral logical artifact, evaluator as an independent semantic oracle, AIMS as sole logical ownership authority, and VM/LLVM/native/WASM/JIT as sibling physical projections.
  • Inventory every remaining shared or pre-projection ownership carrier, including RcStrategy, RcAtomicity, RcInc, RcDec, ValueRepr, layout-derived funding, and executor-specific cleanup facts; classify each as neutral logical fact, physical adapter input, compatibility residue, or forbidden duplicate authority.
  • Reconcile the bytecode verifier’s totality, identity, malformed-artifact, and call-boundary checks with the provenance plan so later sections extend that verifier contract instead of building a second validator or a parallel executable schema.
  • Map the residual obligations transferred from completed aims-burden-tracking: VF-7/current executable conformance, proof-to-implementation bridge, canonical roster and documentation cleanup, parity, unwind/drop correspondence, and leak freedom; point TRMC and representation optimizations to their external successor plans.
  • Run the contract-audit probe and preserve a machine-readable seam inventory that subsequent sections consume; any ambiguity about the shipped bytecode contract blocks schema implementation and is resolved in the decision record first.