FFI Boundary Safety — Deep FFI Part 2
8 sections
Overview
Make Ori's mission claim "memory safety across the entire program surface, including FFI" (missions.md §Ori, §AIMS) hold in implementation. Approved Deep FFI made the FFI surface safe (declarative marshalling, ownership annotations, #free, handler-based mocking). This plan extends that safety across the boundary: the AIMS lattice analysis sees FFI ownership contracts as typed interprocedural facts (not opaque conservative calls), header-derived signatures eliminate transcription drift, struct layouts are verified against C headers at compile time, returned-pointer lifetimes bind to named parameters via #borrow_from, callback capabilities propagate through registration, and handler-mocking formalization gains partial-mock strict mode plus record/replay.
Planned
8 sections
AIMS FFI Contract Extension
Teach the AIMS lattice analysis to consume FFI ownership contracts as typed interprocedural facts, eliminating conservative RC retention at the FFI boundary 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.