0%

Section 03: Backend-Neutral AIMS Facts and LLVM Projection

Status: Not Started Goal: Freeze AIMS interprocedural results (MemoryContract, ParamContract, ReturnContract, EffectSummary) once in the shared executable artifact, then let LLVM project them into optimization metadata. The current FunctionCompiler.aims_contracts map is a transitional orchestration detail, not the production ownership or transport seam.

Success Criteria:

  • Shared realization publishes an immutable typed fact plan keyed by stable function identity
  • ArcIrEmitter has read-only access to the current function’s projected AIMS facts
  • Every admitted executor consumes the same plan without a backend-local contract/effect/alias scan
  • Only a frozen returns_fresh_self_alloc fact may produce LLVM return noalias
  • Frozen MemoryAccessClass::ReadOnly may produce LLVM memory(read); no path emits memory(none) yet
  • ORI_DUMP_AFTER_LLVM=1 shows new attributes on appropriate call sites

Context: The closed-program realize_closed_program() entry runs the AIMS SCC fixpoint and freezes rich per-function contracts into one validated executable artifact. Each contract contains parameter access/consumption/cardinality/locality/uniqueness, return freshness, and a function effect summary; the internal fixpoint is not a backend-callable API.

The current contracts are consumed during ARC realization but do not survive as a closed backend-neutral fact surface. The cure is to publish them through shared realization and let LLVM consume a typed projection; passing a private raw map deeper into ori_llvm alone would preserve the architectural bug.

AIMS is not an LLVM analysis. Its compiled calculus and Rust realization produce neutral ownership, fresh-self-allocation, memory-access, disjointness, and unwind facts for VM, LLVM, native, compiled-WebAssembly, and JIT consumers. LLVM attributes are one adapter spelling. The evaluator remains the canonical-IR behavior oracle and does not define a competing ownership plan.

Current migration evidence:

  • oric now realizes one closed ExecutableProgram, binds it through bind_executable_program, and compiles bodies from artifact identities; FunctionCompiler::new cannot accept an arbitrary contract map.
  • The remaining production gate is exhaustive validation that every body and projection is artifact-backed and that no VM, LLVM, native, compiled-WebAssembly, or JIT adapter can invoke or reconstruct the internal AIMS pipeline.
  • LLVM-local nounwind analysis is a migration gap, not a pattern to copy for new facts.

Depends on: Section 02 (metadata infrastructure for alias.scope).

03.1 Publish the Shared Fact Plan and Project It to LLVM

File(s): shared realization/ExecutableProgram carrier, compiler/ori_llvm/src/codegen/arc_emitter/mod.rs

  • Define an immutable typed AIMS fact plan keyed by the same stable function IDs as ExecutableProgram

  • Construct and validate the plan once during shared realization; reject missing, duplicate, or stale function facts before backend selection

  • Store the plan in the validated executable artifact so VM, LLVM, native, compiled-WebAssembly, and JIT projections receive one identity

  • Give ArcIrEmitter a read-only LLVM view with only the facts needed to emit attributes and metadata

  • Prove the adapter cannot mutate contracts, run AIMS, or infer a missing fact from LLVM types, names, or layout

  • Verify: timeout 150 cargo t -p ori_llvm passes (no behavioral change yet)

  • /tpr-review passed — independent review found no critical or major issues (or all findings triaged)

  • /impl-hygiene-review passed — hygiene review clean. MUST run AFTER /tpr-review is clean.

  • Subsection close-out (03.1) — MANDATORY before starting the next subsection. Run /improve-tooling retrospectively on THIS subsection’s debugging journey (per .claude/skills/improve-tooling/SKILL.md “Per-Subsection Workflow”): which diagnostics/ scripts you ran, where you added dbg!/tracing calls, where output was hard to interpret, where test failures gave unhelpful messages, where you ran the same command sequence repeatedly. Forward-look: what tool/log/diagnostic would shorten the next regression in this code path by 10 minutes? Implement improvements NOW (zero deferral) and commit each via SEPARATE /commit-push using a valid conventional-commit type (build(diagnostics): ... — surfaced by section-03.1 retrospective — build/test/chore/ci/docs are valid; tools(...) is rejected by the lefthook commit-msg hook). Mandatory even when nothing felt painful. If genuinely no gaps, document briefly: “Retrospective 03.1: no tooling gaps”. Update this subsection’s status in section frontmatter to complete.

  • /sync-claude section-close doc sync — verify Claude artifacts across all section commits. Map changed crates to rules files, check CLAUDE.md, canon.md. Fix drift NOW.

  • Repo hygiene check — run diagnostics/repo-hygiene.sh --check and clean any detected temp files.

03.2 Emit noalias on Fresh Allocations

File(s): compiler/ori_llvm/src/codegen/arc_emitter/apply.rs or equivalent call-site emission

Uniqueness::Unique is insufficient for LLVM noalias: a unique result may pass through a caller-visible input or take over a consumed COW operand’s storage. Only the stronger neutral ReturnContract.returns_fresh_self_alloc fact proves that every return path produces storage allocated inside the callee and inaccessible through an upstream alias. Freeze that fact by stable function identity, then project it to the LLVM declaration and matching call-site return.

  • At call-site emission, look up the callee’s stable function ID in the shared AIMS fact plan
  • Write failing AOT test FIRST (TDD): function that returns a freshly allocated list → before the fix, IR dump does NOT show noalias on the return. This test will verify the attribute after the fix.
  • If and only if the frozen returns_fresh_self_alloc fact is true, add the LLVM return noalias projection
  • Use IrBuilder::add_call_site_return_attribute() (may need to add this method if it doesn’t exist — attributes.rs already has parameter-level call-site attributes)
  • Verify AOT test now passes: noalias appears in IR dump on fresh allocation returns
  • Verify: ORI_DUMP_AFTER_LLVM=1 shows noalias on return of allocation functions
  • Add negative pins for unique parameter passthrough, field/view return, and typed COW storage takeover; none may receive return noalias
  • For frozen RL-31-disjoint parameters, emit !alias.scope + !noalias metadata pairs on the corresponding accesses. Borrowed parameters alone are not disjointness proof.
  • Verify: no test regressions (noalias/alias.scope are hints, not behavioral)

Matrix dimensions:

  • Types: [int] (list allocation), str (string allocation), {str: int} (map allocation), user struct

  • Patterns: direct self-allocation, borrowed/field/view return, consumed-operand takeover, and two proven-disjoint borrowed params

  • Semantic pin: IR dump test showing noalias on fresh allocation return

  • Semantic pin: IR dump test showing !alias.scope and !noalias on disjoint parameter loads

  • /tpr-review passed — independent review found no critical or major issues (or all findings triaged)

  • /impl-hygiene-review passed — hygiene review clean. MUST run AFTER /tpr-review is clean.

  • Subsection close-out (03.2) — MANDATORY before starting the next subsection. Run /improve-tooling retrospectively on THIS subsection’s debugging journey (per .claude/skills/improve-tooling/SKILL.md “Per-Subsection Workflow”): which diagnostics/ scripts you ran, where you added dbg!/tracing calls, where output was hard to interpret, where test failures gave unhelpful messages, where you ran the same command sequence repeatedly. Forward-look: what tool/log/diagnostic would shorten the next regression in this code path by 10 minutes? Implement improvements NOW (zero deferral) and commit each via SEPARATE /commit-push using a valid conventional-commit type (build(diagnostics): ... — surfaced by section-03.2 retrospective — build/test/chore/ci/docs are valid; tools(...) is rejected by the lefthook commit-msg hook). Mandatory even when nothing felt painful. If genuinely no gaps, document briefly: “Retrospective 03.2: no tooling gaps”. Update this subsection’s status in section frontmatter to complete.

  • /sync-claude section-close doc sync — verify Claude artifacts across all section commits. Map changed crates to rules files, check CLAUDE.md, canon.md. Fix drift NOW.

  • Repo hygiene check — run diagnostics/repo-hygiene.sh --check and clean any detected temp files.

03.3 Emit Effect-Based Call Site Annotations

File(s): compiler/ori_llvm/src/codegen/arc_emitter/apply.rs

Freeze a backend-neutral whole-function memory-access fact from IC-3/IC-5 plus typed runtime-operation effects. Ownership/FIP effects alone do not describe I/O, panic TLS, allocator state, or other inaccessible memory. Unknown calls and missing descriptors fail closed as ReadWrite. LLVM may then project a proven ReadOnly fact as memory(read) when its ABI does not add an sret write. memory(none) remains forbidden until the calculus models both inaccessible reads and inaccessible writes and proves their absence.

  • At call-site emission, look up the callee’s stable function ID in the shared AIMS fact plan
  • Require a typed memory-effect descriptor for every call/runtime operation; missing or unknown descriptors produce ReadWrite
  • Record may_read_inaccessible and may_write_inaccessible separately; panic/throw control flow is orthogonal only after its TLS, stderr, and runtime writes are represented
  • Project only frozen MemoryAccessClass::ReadOnly as LLVM memory(read) and suppress it for sret functions
  • Do not call add_memory_none_attribute() in this section; add a negative IR pin proving it is absent
  • Use the existing IrBuilder::add_memory_read_attribute() adapter without an LLVM-local ARC-IR scan
  • Write failing AOT test FIRST (TDD): call a pure function inside a loop → before the fix, the call is NOT hoisted. This test will verify LICM after the fix.
  • Verify AOT test now passes: IR shows the pure function call hoisted above the loop header
  • Verify: no test regressions

Matrix dimensions:

  • Types: scalar read-only function, allocator, collection mutation, I/O, panic, and unknown runtime call

  • Patterns: direct and transitive calls, sret return, call inside loop, and descriptor-missing rejection

  • Semantic pin: loop containing pure function call → IR shows the call hoisted above the loop header

  • Negative pins: print/panic/unknown/allocating functions receive neither memory(read) nor memory(none)

  • /tpr-review passed — independent review found no critical or major issues (or all findings triaged)

  • /impl-hygiene-review passed — hygiene review clean. MUST run AFTER /tpr-review is clean.

  • Subsection close-out (03.3) — MANDATORY before starting the next subsection. Run /improve-tooling retrospectively on THIS subsection’s debugging journey (per .claude/skills/improve-tooling/SKILL.md “Per-Subsection Workflow”): which diagnostics/ scripts you ran, where you added dbg!/tracing calls, where output was hard to interpret, where test failures gave unhelpful messages, where you ran the same command sequence repeatedly. Forward-look: what tool/log/diagnostic would shorten the next regression in this code path by 10 minutes? Implement improvements NOW (zero deferral) and commit each via SEPARATE /commit-push using a valid conventional-commit type (build(diagnostics): ... — surfaced by section-03.3 retrospective — build/test/chore/ci/docs are valid; tools(...) is rejected by the lefthook commit-msg hook). Mandatory even when nothing felt painful. If genuinely no gaps, document briefly: “Retrospective 03.3: no tooling gaps”. Update this subsection’s status in section frontmatter to complete.

  • /sync-claude section-close doc sync — verify Claude artifacts across all section commits. Map changed crates to rules files, check CLAUDE.md, canon.md. Fix drift NOW.

  • Repo hygiene check — run diagnostics/repo-hygiene.sh --check and clean any detected temp files.

03.R Third Party Review Findings

  • None.

03.N Completion Checklist

  • Shared realization validates and freezes one typed AIMS fact plan before backend selection
  • VM, LLVM, native, compiled-WebAssembly, and JIT entry points consume the same fact identity without re-analysis
  • ArcIrEmitter queries the read-only LLVM projection by stable function identity
  • Only fresh-self-allocation returns get LLVM return noalias; passthrough/takeover negative pins stay unannotated
  • Proven read-only functions get memory(read) where ABI-safe; memory(none) is absent
  • ORI_DUMP_AFTER_LLVM=1 demonstrates new attributes
  • timeout 150 ./test-all.sh green (debug AND release — cargo b --release && timeout 150 ./test-all.sh)
  • Cross-executor parity: evaluator, VM, LLVM debug/release, and AOT agree; dual-exec-verify.sh supplies only the current evaluator/LLVM leg
  • ORI_CHECK_LEAKS=1 clean on test programs exercising new attributes (noalias/memory() are optimization hints but verify RC ops remain balanced)
  • No spurious warnings
  • Plan annotation cleanup
  • Plan sync — update plan metadata
    • This section status → complete
    • 00-overview.md updated
    • index.md updated
  • /tpr-review passed
  • /impl-hygiene-review passed
  • /improve-tooling retrospective completed — MANDATORY at section close, after both reviews are clean. Reflect on the section’s debugging journey (which diagnostics/ scripts you ran, which command sequences you repeated, where you added ad-hoc dbg!/tracing calls, where output was hard to interpret) and identify any tool/log/diagnostic improvement that would have made this section materially easier OR that would help the next section touching this area. Implement every accepted improvement NOW (zero deferral) and commit each via SEPARATE /commit-push. The retrospective is mandatory even when nothing felt painful — that is exactly when blind spots accumulate. See .claude/skills/improve-tooling/SKILL.md “Retrospective Mode” for the full protocol.

Exit Criteria: One validated typed AIMS fact plan survives shared realization and every physical executor consumes its stable identity without re-analysis. LLVM faithfully projects only proved fresh-self-allocation, read-only, and disjointness facts; all negative witnesses remain unstrengthened. Every affected executor preserves behavior/cleanup parity.