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. Mission criterion 4 (every residual RC op traceable to a burden-registry proof failure) closes THROUGH this section’s contract plus aims-burden-tracking’s registry convergence — the traceability evidence is part of the contract doc.

Blocked-by

  • plans/aims-burden-tracking/ sections 05 (phase-6 lattice rewrite), 06 (phase-7 mechanical lowering), 07B (broad-shape self-sufficiency), 09 (predicate-stack retirement) — the burden architecture must converge before the contract freezes.
  • 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 = first projection — its existing sections 02/03/04 become projection work; BIR fact tables = second projection). The amendment is executed against THAT plan via its own 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 (6 flags), ReturnContract (uniqueness/preserves_freshness/locality/shape), ParamContract essentials (borrowed_read_only, iter_consumes, may_share), reuse/alloc events (LocalAllocCandidate/ReuseCandidate), burden provenance (burden_emitted distinction) — as a typed side structure keyed by function/instruction, NOT new ArcFunction policy fields that downstream could mutate (read-only side table per CH-4 shape; 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 (which fields, which invariants, what the optimizing tier MAY and MUST NOT do — RC placement is AIMS-owned, full stop); reviewed against canon.md §7.1 invariant 5 + the Coexistence theorems; /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 first projection).
  • 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 incl. the RC-placement ban) + /tpr-review clean.
  • Fact-fidelity matrix green (oracle comparison) with freshness/effect pins.