Foreign Function Interface

Table of contents

Resilient programs call into C libraries through extern blocks.

Quick start

extern "libm.so.6" {
    fn sqrt(x: Float) -> Float requires _0 >= 0.0 ensures result >= 0.0;
}

fn main() {
    println(sqrt(16.0));   // prints: 4
    println(sqrt(2.0));    // prints: 1.4142135623730951
}
main();

Run with: cargo run --features ffi -- examples/ffi_libm.rs

Extern block syntax

extern "LIBRARY_PATH" {
    fn NAME(PARAM: TYPE, ...) -> RETURN_TYPE [contracts];
}

LIBRARY_PATH is passed verbatim to the OS dynamic linker:

Platform libm path
Linux libm.so.6
macOS libm.dylib

Supported types (v1)

Only primitive types are supported in FFI Phase 1:

Resilient C ABI
Int int64_t
Float double
Bool bool
String not yet supported
Void void
OpaquePtr void* (opaque)
Callback C function pointer (Phase 1 stub — see below)

At most 8 parameters per extern function.

OpaquePtr — opaque C handles

An OpaquePtr is a void* the language can receive, store, and pass back but never dereference. Use it to model C “handle” types like FILE*, sqlite3*, or an allocator-owned struct pointer:

extern "libfoo.so" {
    fn alloc_point() -> OpaquePtr;
    fn free_point(p: OpaquePtr) -> Void;
    fn get_x(p: OpaquePtr) -> Int;
}

let p = alloc_point();
let x = get_x(p);
free_point(p);

Semantics:

  • Resilient code cannot dereference, compare, or inspect the pointer — only pass it along to another FFI call.
  • Lifetime is the C library’s responsibility. If you leak a handle or use it after the C side freed it, that is a use after free on the C side; the language provides no safety net.
  • Pass-through is zero-copy: the trampoline ferries the raw address across the ABI unchanged.

Trampoline coverage today:

Signature Supported
() -> OpaquePtr yes
(OpaquePtr) -> OpaquePtr yes
(OpaquePtr) -> Int yes
(OpaquePtr) -> Float yes
(OpaquePtr) -> Bool yes
(OpaquePtr) -> Void yes

Higher arities extend mechanically by adding an arm to dispatch_explicit in ffi_trampolines.rs.

Callback — Phase 1 stub

Callback types are recognised in FFI declarations:

extern "libfoo.so" {
    fn register_handler(cb: Callback) -> Void;
}

Passing a Resilient function as Callback is stubbed in Phase 1 and returns a clean error:

FFI: extern fn `register_handler` uses a Callback parameter; callbacks
require the trampoline feature (planned for Phase 2)

Real trampoline support is planned for Phase 2 (bytecode VM).

Contracts

Pre- and post-conditions work the same as on Resilient functions:

fn sqrt(x: Float) -> Float
    requires _0 >= 0.0
    ensures  result >= 0.0;

Arguments are bound positionally as _0, _1, … in requires clauses. The return value is bound as result in ensures clauses.

Violations are caught at runtime before (or after) the C call, producing a contract violation error.

@trusted functions

@trusted
fn fast_log(x: Float) -> Float requires _0 > 0.0 ensures result >= 0.0;

@trusted propagates the ensures clause as an SMT axiom to the Z3 verifier. The ensures clause is still evaluated at runtime; a failure does not abort the program. Instead, the clause is passed through and asserted as an axiom for the Z3 verifier, which can reason about the foreign function’s postcondition without you needing to prove it inline.

C symbol aliases

When the Resilient name differs from the C symbol, use = "c_name":

extern "libc.so.6" {
    fn c_abs(x: Int) -> Int = "abs";
}

no_std / embedded use

For no_std targets, the dynamic linker is unavailable. Use the resilient-runtime crate’s StaticRegistry instead:

[dependencies]
resilient-runtime = { features = ["ffi-static"] }

See the no_std guide for the full registration API.

Design spec

See the FFI design spec for the full type model, contract semantics, and the roadmap for Phase 2 (bytecode VM) and Phase 3 (Cranelift JIT).