ADR-0007: FFI Trust Boundary
Status: accepted
Date: 2026-07-25
Context
Foreign calls can invalidate ownership, effect ordering, specialization reproducibility, and proof assumptions through hidden state or ABI mismatch. NAUX still needs operating-system and interoperability boundaries during its evolution.
Options considered
| Option | Benefit | Cost |
|---|---|---|
| Unrestricted C ABI | Easy integration | Destroys proof boundary |
| No FFI | Maximum isolation | Prevents practical hosted use |
| Unsafe contract + safe capability wrapper | Explicit trust | More declarations and checking |
Decision
Raw ABI declarations require unsafe and a hashed contract covering ABI,
ownership, lifetime, mutation, errors, threading, callbacks, and hidden-state
dependencies.
Safe wrappers expose checked capability types. Foreign calls carry an explicit FFI effect and are specialization barriers unless the contract proves the required property.
A pure declaration also excludes time, randomness, locale, thread-local
state, environment state, and hidden mutable state.
Rationale
The contract makes foreign behavior visible to ordering, hashing, and translation validation without pretending external code is verified.
Trade-offs
- FFI is more verbose.
- Incorrect unsafe contracts remain programmer obligations.
- Callbacks and resumptions are deferred from Core-N0.
Consequences
FFI contract hashes are part of residual provenance. No foreign library is a permitted permanent dependency of the final normal release path.
Revisit trigger
Add callbacks, async FFI, or specialization-through-FFI only after capability, unwind, and resumption semantics are accepted.