0%

s18 — Typed Fact Surface + Optimizing-Tier Input Contract Freeze

Goal

The AIMS facts that today die at realization survive into a backend-neutral typed fact surface, BIR’s reserved side-table slots populate from it, and the optimizing-tier input contract freezes — read-only consumption, AIMS invariant 5 intact. The mission’s traceability criterion closes through this section’s contract plus the logical-event identities supplied by AIMS: every physical memory-management operation names both its frozen obligation and the CompiledLayoutPlan choice that realizes it.

Counter-survivor remarks remain diagnostics for the current RC projection, not the definition of AIMS.

Blocked-by

  • plans/aims-provenance-ledger/ S09 (compiled-counter floor closure) and S10 (observability/documentation consolidation). The consumed calculus, class-ledger authority, and physical-projection boundary already come from S01/S03/S08 plus content/decisions/00-cross-plan-rasi-rc-placement.md IC-PV-1/P1; this section must not revive the superseded plan’s raw AimsStateMap or transitional Burden/Rc carriers as an input contract.
  • plans/semantic-optimization-pipeline/ reshape amendment (below) — coordinated, not duplicated.

Implementation Sketch

  • Cross-plan reshape (user-approved predecessor-gate): amend semantic-optimization-pipeline so its primary deliverable is the backend-neutral typed fact surface. Facts leave AIMS/typeck as typed data; LLVM metadata and BIR fact tables are independent sibling projections with no precedence or policy authority. Execute the amendment through that plan’s lifecycle; this section consumes the surface.
  • Fact retention: extend realization output so the pass-time facts verified as lost at plan time become retained surface fields — EffectSummary (six flags), ReturnContract (uniqueness/preserves_freshness/locality/shape), ParamContract essentials (borrowed_read_only, iter_consumes, may_share), logical allocation-site and lifetime/placement-eligibility facts (LifetimeBound / PlacementEligibilityCandidate) plus logical ReuseCandidate, and burden provenance (burden_emitted distinction) — as a typed side structure keyed by function/instruction, not new ArcFunction policy fields that downstream could mutate. These facts authorize possible projections; they never imply local or stack allocation. Keep the side table read-only per the CH-4 shape with serde-skip derived-data discipline.
  • BIR population: s06’s reserved side-table slots fill from the surface during translation; BIR verifier extends (facts reference valid instruction indices; fact-table immutability after translation).
  • Contract freeze: the consumption contract document names which fields and invariants the optimizing tier MAY consume and MUST preserve. Exact logical ownership-event identity, multiplicity, ordering, transfer edge, and cleanup obligation are AIMS-owned, full stop. Physical storage, header, counter, synchronization, ABI, helper, and instruction selection are owned by the validated compiled plan and backend adapter. Review against canon.md §7.1 invariant 5 plus the Coexistence theorems; run /tpr-review on the contract.
  • AIMS change protocol: any ori_arc-side retention change follows arc.md §CP-1..CP-4 (calculus-first where a rule’s semantics are touched; retention of already-computed facts is data plumbing, not a calculus change — the boundary is argued explicitly in the contract doc).

Test Strategy

  • Matrix: fact field x program shape (call-heavy, reuse-heavy, borrow-heavy, effect-diverse) — surface values equal the pass-time values (oracle-style re-derivation comparison per the VF-3 precedent).
  • Semantic pin: a known-fresh-return program pins preserves_freshness=true surviving to BIR; a known-effectful callee pins may_allocate.
  • Negative pin: mutation of a fact table post-translation is rejected (immutability check).

Work Items

  • semantic-optimization-pipeline reshape amendment landed via that plan’s lifecycle (typed surface primary; LLVM metadata and BIR tables are sibling projections).
  • Realization fact retention (effects/return-provenance/param-essentials/reuse-events/burden-provenance) as a read-only typed side structure with serde-skip discipline; CP-protocol boundary argued + reviewed.
  • BIR fact-slot population + verifier extension (index validity, post-translation immutability with negative pin).
  • Optimizing-tier input contract doc frozen (MAY/MUST-NOT, including the logical-event-replacement ban and physical-projection boundary)
    • /tpr-review clean.
  • Fact-fidelity matrix green (oracle comparison) with freshness/effect pins.