FFI Boundary Safety — Deep FFI Part 2
8 sections
Overview
Make memory safety hold across the entire program surface, including FFI (missions.md §Ori, §AIMS):
Planned
8 sections
AIMS FFI Contract Extension
Teach AIMS to consume FFI ownership contracts as typed interprocedural facts and freeze one exact backend-neutral owner/transfer/cleanup trace while preserving Invariant #5 (unified model).
Header-Assisted Extern Blocks — #header(...)
Read C headers via libclang at build time; auto-derive extern signatures for functions listed in the block body; preserve boundary visibility (explicit function list + explicit annotations) while eliminating signature-transcription boilerplate.
Compile-Time Struct Layout Verification
Verify every `#repr(\"c\")` Ori struct against its matching C header struct layout at compile time; emit E4015 with field-by-field diff on mismatch. Prevent silent memory corruption from library-upgrade-driven layout drift.
#borrow_from(param) — Lifetime Annotations at the Boundary
Let extern declarations express 'this returned pointer borrows from THIS named parameter'; enforce at compile time that the return does not outlive the parameter's scope. Integrate with AIMS via Locality::Borrowed(p) — NO new lattice dimension.
Callback Capability Propagation
Let callback parameter types declare the capabilities the C runtime will provide; verify at compile time that the registered Ori closure uses ONLY those capabilities. Convert runtime capability-missing failures into compile-time E4019 errors at the registration site.
FFI-Aware Diagnostics
Every E40xx FFI-family diagnostic produced by §01–§05 carries a secondary span pointing at the relevant C declaration when `#header(...)` is in use. Users never have to manually cross-reference Ori errors against C headers.
Handler-Mocking Formalization + Record/Replay
Formalize three practical details of handler-based FFI mocking: (7a) #strict partial-mock mode rejecting unmocked calls at compile time; (7b) stateful-mock + FFI state integration (documentation only — mechanism already approved); (7c) record/replay via `std.ffi.trace` with deterministic-by-construction replay.
Spec, Grammar, and ori-syntax.md Sync
Propagate every attribute, grammar production, and type/method addition from §01–§07 to the authoritative surface: spec clause 26 (FFI), grammar.ebnf Annex A, and .claude/rules/ori-syntax.md. Cross-cutting — ships incrementally with each implementation section; §08 is the final aggregate check.