0%

§01 — AIMS FFI Contract Extension

Context

Approved proposal §1 (docs/ori_lang/proposals/approved/ffi-boundary-safety-proposal.md) states that AIMS today treats extern calls as opaque — assume-the-worst conservative — because extern declarations do not produce MemoryContract fragments. This section makes extern declarations first-class contract providers, so the existing interprocedural SCC fixpoint (IC-1 / IC-2 / IC-3 / IC-4 / IC-5) consumes them alongside native Ori callees.

Invariant #5 is load-bearing here. Any implementation approach that introduces a parallel structure (shadow contract table, separate FFI lattice, independent ownership annotation pass, or backend-mechanism field) is out of scope AND will be rejected at /tpr-review. The extension MUST be additive on MemoryContract / ParamContract / ReturnContract / EffectSummary and freeze stable logical event identities in the shared ExecutableProgram.

Backend-neutral seam. AIMS owns the logical owner-credit, transfer, cleanup, effect, and unwind facts. VmLayoutPlan and CompiledLayoutPlan(TargetSpec) are sibling consumers that choose physical mechanisms and prove plan satisfaction. LLVM is one adapter over the compiled plan; LLVM IR, helper calls, counters, headers, ABI details, and VM opcodes are never AIMS facts.

§01.1 — Design Log FIRST (gate — do not implement before this)

Before any Rust changes land, write plans/ffi-boundary-safety/section-01-design-log.md answering:

  • Which ParamContract field(s) carry the FFI-declared ownership (owned vs borrowed)? — default: reuse ParamContract.access (Owned/Borrowed) since that is the existing SSOT per aims-rules.md §1.1.
  • Which ParamContract field carries may_share for FFI parameters? — default: reuse the existing may_share field on ParamContract per aims-rules.md §5 IC-3.
  • Which ReturnContract field carries the FFI-declared return ownership + preserves_freshness? — default: reuse ReturnContract.uniqueness (Unique for owned returns from fresh C allocations) and ReturnContract.preserves_freshness (true for owned + known-fresh allocator; false for borrowed returns which copy immediately per approved Deep FFI).
  • Which EffectSummary fields cover #error(errno) / #error(nonzero) / etc.? — default: may_throw = true when #error(...) != none (error paths produce Result::Err, which the caller’s control-flow graph must account for); may_allocate = true when the callee is known to allocate (e.g., sqlite3_open creates a handle); may_deallocate = true for #free(...) functions.
  • What new field (if ANY) is needed? — if none, note that explicitly. If one is needed, justify why it cannot be expressed on existing fields and verify the addition does not violate L-5 (finite height) or L-10 (monotone join).
  • Cite each field mapping against aims-rules.md rule anchor (IC-2, IC-3, IC-4, IC-5) — reviewers will check these verbatim.

Acceptance. The design log is complete when it exhaustively lists every FFI-declarable annotation (owned, borrowed, owned CPtr return, borrowed str return, borrowed [byte] return, #error(errno), #error(nonzero), #error(null), #error(negative), #error(success: N), #error(none), #free(fn), out param, #borrow_from(p) — the last deferred to §04 but the schema must accommodate it) and maps each to a concrete MemoryContract field.

Failure mode. If the design log cannot express an annotation using existing contract fields, STOP. Do not add a sibling structure. Either (a) propose a specific field addition with justification, or (b) file a bug per CLAUDE.md §Bug Handling — ZERO DEFERRAL and escalate via AskUserQuestion.

§01.2 — ExternDecl → MemoryContract fragment emitter

Once §01.1 is signed off:

  • Add fn extract_extern_contract(decl: &ExternDecl) -> MemoryContract in compiler/ori_arc/src/aims/interprocedural/extract.rs (NEW function; do NOT modify the existing extract_function_contract core logic — share helpers only).
  • Wire into the SCC fixpoint: extern decls appear as nodes in the call graph at IC-1 with their contract pre-populated (no fixpoint iteration needed — externs have no bodies to analyze). Supply those producer-authored facts to the one whole-batch realize_closed_program() entry per arc.md §Entry Points; do not expose the internal contract fixpoint as an FFI- or backend-callable API.
  • Each extern function’s contract is produced ONCE at crate-type-check time and cached in the Salsa query layer (per compiler.md §Salsa purity requirements).
  • Update ori_arc/src/aims/contract/mod.rs documentation comments to note FFI-origin contracts (reading-only — do not change field definitions unless §01.1 justified a new field).

§01.3 — Call-site refinement (TF-6 interop)

  • In the intraprocedural analysis (compiler/ori_arc/src/aims/intraprocedural/mod.rs), the existing TF-6 (aims-rules.md §3) refine(CONSERVATIVE, callee.return_contract) already handles any callee with a contract, regardless of origin. Verify with a targeted unit test that an extern callee’s contract narrows the call-site AimsState correctly.
  • Verify TF-11 argument demand refinement (aims-rules.md §3 TF-11 Apply row) fires correctly for FFI arguments: Borrowed Absent → zero demand; Owned Absent → (arg, Once, Linear) plus the exact logical cleanup obligation currently carried under the transitional RL-5 dec spelling; locality/uniqueness/may_share propagation applies identically to FFI calls.
  • NO new code path needed here — this subsection validates the existing refinement mechanics work for FFI contracts. If they don’t, that’s a bug in TF-6/TF-11, not a new “FFI refinement” code path.

§01.4 — Realization phase validation

  • Verify the current realize_rc_reuse (Step 5) and realize_annotations (Step 10) entry points freeze the correct logical owner-credit, transfer, cleanup, COW/reuse, effect, and unwind identities for FFI-touching functions. These function names are transitional implementation spellings; realization must not branch on FFI origin or choose a backend mechanism.
  • Verify verify_fip_contract (Step 5a, aims-rules.md §5 IC-6) correctly certifies FFI-only functions: a function whose body is let x = RSA_new(); sign(x, ...); RSA_free(x) with all owned/borrowed contracts provided should reach FipContract::Certified with zero unmatched logical allocation/cleanup obligations.
  • Bind the frozen facts into ExecutableProgram by stable identity and add plan-satisfaction checks for both VmLayoutPlan and CompiledLayoutPlan(TargetSpec). Neither planner may re-derive ownership from representation or feed a physical verdict back into AIMS.
  • NO realization-level code changes expected. If changes ARE needed, flag as a design-log deviation and STOP for review.

§01.5 — Matrix test coverage (MANDATORY)

Per CLAUDE.md §Fix Completeness and tests.md §Matrix Testing Rule:

  • Failing tests FIRST (TDD order):
    • AIMS snapshot/oracle test in compiler/oric/tests/aims-snapshots/ffi_contract/ showing the contract fragment and exact stable owner/transfer/cleanup identities for an annotated extern declaration.
    • VM and compiled plan-satisfaction tests that consume those same identities without re-analysis; an unsupported FFI execution lane must fail explicitly rather than silently omit an obligation.
    • Current compiled-projection AOT FileCheck test in compiler/ori_llvm/tests/aot/ffi_contract.rs that asserts zero RcInc/RcDec actions in emitted LLVM IR for the canonical owned-chain program. This check validates one counter plan only.
  • Matrix dimensions (must test ALL cells):
    • Ownership × Error protocol: owned/borrowed × #error(errno)/#error(nonzero)/#error(null)/#error(negative)/#error(none) = 10 cells.
    • Return types: c_int, owned CPtr, borrowed CPtr, borrowed str, borrowed [byte], Result<..., FfiError> (auto-wrapped by #error(...) != none) = 6 cells.
    • Argument patterns: owned CPtr arg + dead elsewhere; borrowed CPtr arg + used after call; owned CPtr chained into another FFI call (ownership transfer); borrowed str + interior mutation attempt (should stay COW-safe).
  • Semantic pins:
    • One Ori program tests/spec/ffi/aims_zero_rc.ori (legacy filename retained for continuity) whose primary assertion is an exact logical ownership chain with no redundant credit/release event. Reverting §01 must change that frozen trace.
    • For the current compiled counter projection only, retain the FileCheck assertion (CHECK-NOT: call void @ori_rc_inc / CHECK-NOT: call void @ori_rc_dec) and bind every surviving physical action to a frozen event identity.
    • One negative logical pin: a program with an owned CPtr returned and used twice must retain exactly one additional owner-credit event. If the compiled plan selects counters, its projection must emit exactly one corresponding RcInc; that physical spelling is not the AIMS rule.
  • Verification layer matrix:
    • VF-1 structural check clean on FFI-touching functions (cargo test -p ori_arc -- verify::check_function).
    • VF-2 AbsentParamHasUses does not false-positive on FFI absent params.
    • VF-3 oracle cross-check independently verifies the frozen FFI contract and logical event identities against the declared contract (cargo test -p ori_arc -- oracle).
    • VF-4 FIP certification matrix: FipContract::Certified, FipContract::Bounded(N), FipContract::Conditional, FipContract::Never each reachable via a test program with appropriate FFI call mix.
  • Multi-executor parity: Every admitted FFI executor matches the evaluator/handler oracle for value, typed error, effects, and cleanup behavior. VM and compiled lanes preserve the same frozen event identities; the current compiled counter lane additionally reports zero leaks under ORI_CHECK_LEAKS=1.
  • Projection boundary: LLVM FileCheck failures diagnose the current compiled physical plan or adapter. They may not redefine the AIMS contract, and LLVM-only success cannot close this section.
  • Debug + release: both build modes pass all tests.

§01.6 — AIMS rule additions (documentation)

  • Update .claude/rules/aims-rules.md §5 to note that ParamContract/ReturnContract/EffectSummary accept FFI-origin contracts identically to native contracts — add a one-paragraph note near IC-2/IC-3 citing this section. Co-commit with §01.2.
  • Update .claude/rules/arc.md §"What AIMS does TODAY" bullet list to mention FFI contract participation once §01 ships. Co-commit with §01.2.
  • NO changes to the formal rules themselves — they already admit FFI contracts; this is a documentation sync.

Completion Checklist

  • §01.1 design log exists, cites aims-rules.md anchors, passes independent reading.
  • §01.2 extract_extern_contract lands; Salsa-cached; unit-tested.
  • §01.3 call-site refinement validated via unit tests.
  • §01.4 logical realization validated; stable identities frozen; FipContract::Certified reachable for pure-FFI bodies; VM and compiled plan-satisfaction checks pass.
  • §01.5 matrix tests green (all cells), logical semantic pins green, sibling-projection checks green, current LLVM FileCheck green, negative pin green, both debug + release.
  • §01.6 aims-rules.md + arc.md documentation sync committed.
  • ./test-all.sh green (full suite).
  • ./clippy-all.sh green (zero warnings introduced).
  • ORI_CHECK_LEAKS=1 ./binary reports zero leaks on the FFI test programs.
  • /tpr-review run to consensus (clean).
  • /impl-hygiene-review run to consensus (clean).
  • /improve-tooling section-close sweep run.
  • /sync-claude section-close doc sync run.
  • Plan status flipped: sections[id=01].status: complete; reviewed: true; overview Quick Reference updated.

§01.R — Third Party Review Findings

  • None.