0%

Physical Satisfaction Projections

Goal

Make VM and compiled execution sibling physical projections of one logical product, with explicit and verifiable satisfaction maps instead of implicit reanalysis.

Projection Boundary

A satisfaction map is keyed by the logical product’s stable identities and records how a physical plan discharges each logical obligation. VM planning may use VM call signatures, slot/storage choices, and the VM layout plan. Compiled planning may use the compiled ABI/layout plan and may choose representation, atomicity, fused retain/release sequences, and target-specific cleanup. Those decisions remain downstream and cannot rewrite shared logical facts.

A single physical action may satisfy multiple logical obligations only through an explicit fused-expansion record whose covered identities are unique and complete. One logical obligation cannot disappear because a backend inferred it was unnecessary unless a proved neutral fact authorizes that discharge and the map records it.

Verification

Reuse and extend the executable artifact verifier. Validate totality, identity membership, artifact fingerprint agreement, allowed multiplicity, fused coverage, cleanup ordering constraints, call-boundary compatibility, and normal/unwind coverage. Missing or foreign map entries fail closed before execution.

Mechanism Retirement

Mechanism-shaped carriers in shared IR are either deleted or quarantined inside projection adapters with no upstream reads. This section owns the implementation cutover; the final section owns removal of compatibility shims, toggles, and stale documentation after all matrices are green.

Completion Evidence

The projection-totality probe must cover both VM and compiled paths, must-fire and must-not-fire cases, malformed maps, and an extensibility fixture showing that a synthetic sibling adapter consumes the stable contract without extending AIMS semantics.

Work Items

  • Define exhaustive satisfaction maps from every logical lifetime, extent, owner-bound, cleanup, observation, and retain/drop obligation into the shipped VM and compiled physical-planning structures, keyed by the same stable identities.
  • Implement the VM projection as a consumer of neutral AIMS facts plus the bytecode-owned VM call signatures and layout plan; prove it neither reclassifies ownership nor exports VM slot/layout decisions back into shared IR.
  • Implement the compiled projection as a consumer of the same facts plus the bytecode-owned compiled ABI/layout plan; select retain/release expansion, fused sequences, atomicity, representation, and cleanup schedule only inside the physical adapter.
  • Extend the shared verifier so satisfaction maps are total, single-valued where required, explicitly fused where permitted, identity-preserving, and rejected when missing, duplicated, stale, cross-artifact, or semantically incompatible.
  • Add must-fire and must-not-fire projection tests for normal/unwind cleanup, user drops, closures, protocols, aliases, aggregates, loops, external visibility, thread reachability, and malformed/tampered maps across VM and compiled executors.
  • Delete or isolate duplicate physical authority in shared logical IR and demonstrate that adding another sibling executor requires only a new physical satisfaction adapter, not changes to AIMS logical semantics.