Skip to main content

Foreign Function Interface

Verum speaks C. Every FFI boundary uses the C ABI — not C++, not Rust's extern "Rust", not a higher-level binding that hides marshalling. This is semantic honesty applied to interop: the boundary is a system-level contract, and Verum refuses to pretend otherwise.

extern "C" blocks​

extern "C" {
    fn malloc(size: Int) -> *mut Byte;
    fn free(ptr: *mut Byte);
    fn printf(fmt: *const Byte, ...) -> Int;
}

Declares C functions available to Verum. These declarations do not generate code — they describe the foreign symbol's signature.

caution
A Text is not a C string

A variadic call works — snprintf(buf, 32, fmt, 42) returns 2 and writes 42 at both tiers — but the format argument above is a C const char *, and Text.as_ptr() does not give you one. Text is length-prefixed with no terminator, so the callee reads past the end until it finds a zero byte somewhere in the heap.

It fails by luck, which is why it is easy to miss. In one session three formats worked and one did not, and the only difference was the byte that happened to follow them:

"%ld"      worked        "%d"       worked
"%ld-x"    worked        "abcde"    worked
"%ld-%ld"  garbage

Two of those are five characters long, so length is not the axis. Build the C string yourself with an explicit 0 byte, or pass a byte slice together with its length where the callee accepts one.

Widths in the variadic tail

The tail's arguments have no declared types, so they travel at Verum's own widths: Int as 64-bit, Float as 64-bit. That matches what %ld, %lld, %f and %p read. It does not match %d, which reads 32 bits — and the truncation is silent:

%d   with 4294967338   prints 42
%ld  with 4294967338   prints 4294967338

Use the 64-bit specifier, or narrow the value yourself before the call.

Calling convention​

@extern("C", calling_convention = "stdcall")
fn win_api_call(x: Int) -> Int;

Calling conventions: C, stdcall, fastcall, aapcs, swiftcall, and naked (for assembly interop).

Exposing Verum to C​

@extern("C")
pub fn verum_add(a: Int, b: Int) -> Int {
    a + b
}

An @extern("C") pub fn is emitted with C linkage. Its name must be a valid C identifier.

Boundary contracts​

Every FFI boundary must declare a boundary contract — not just types, but guarantees:

ffi MyLib {
    @extern("C")
    fn my_lib_process(
        input: *const Byte,
        len:   Int,
        out:   *mut Byte,
    ) -> Int;

    requires      len >= 0 && len <= 1024;
    requires      out != null;
    ensures       result >= 0 => bytes_written_up_to(out, result);
    memory_effects = Reads(input);
    memory_effects = Writes(out);
    thread_safe   = true;
    errors_via    = ReturnCode(result < 0);
    @ownership(transfer_to = "caller", borrow = [input])
}

The contract components:

  • requires — preconditions the caller must guarantee.
  • ensures — postconditions the library promises.
  • memory_effects — what the call reads, writes, allocates, deallocates. Options:
    • Pure — no effects.
    • Reads(path) — reads from the given memory region.
    • Writes(path) — writes to the given memory region.
    • Allocates — allocates new heap memory (caller takes ownership).
    • Deallocates(path) — releases the memory at path.
    • Combined with +: Reads(input) + Writes(out) + Allocates.
  • thread_safe — Boolean. Whether the call is safe to invoke concurrently without external synchronisation.
  • errors_via — how errors are reported:
    • None — infallible.
    • Errno — thread-local errno.
    • ReturnCode(pattern) — sentinel return value. The pattern names what counts as error: ReturnCode(result < 0) means "negative return values are errors".
    • ReturnValue(expr) — the call returns a distinguished value; if it equals expr, the error was signalled. Optional with Errno suffix says errno carries the error code: ReturnValue(null) with Errno.
    • Exception — C++ exception (for extern "C++").
  • @ownership(...) — who owns allocations, what is borrowed, what is transferred. Modes:
    • transfer_to = "caller" — the call returns an owned resource; the caller must release it.
    • transfer_from = "caller" — the call takes ownership of an argument; the caller must no longer use it.
    • borrow — no ownership change; caller retains ownership.
    • shared — both sides keep a reference-counted view.

These contracts become SMT obligations at every call site.

Raw pointers​

*const T            // immutable raw pointer
*mut T              // mutable raw pointer
*volatile T         // volatile read
*volatile mut T     // volatile write
  • Dereferencing is unsafe.
  • null is a legal value; ptr.is_null() checks.
  • No CBGR protection — these are pure addresses.

Layout​

Types that cross the FFI boundary must have a stable layout. Use @repr(C):

@repr(C)
type CStruct is {
    id:      Int32,
    name:    *const Byte,   // null-terminated UTF-8
    padding: [UInt8; 4],
};

@repr(transparent) for newtype wrappers:

@repr(transparent)
type Handle is (*mut Byte);

String interop​

C strings are *const Byte (null-terminated). Verum has no from_c_str: a pointer is not a slice, so you supply the length and decode explicitly.

mount core.intrinsics.memory.{slice_from_raw_parts};

let c: *const Byte = ...;
let bytes          = unsafe { slice_from_raw_parts(c as &Byte, len) };
let text: Text     = Text.from_utf8(bytes)?;

Text.from_utf8 returns Result<Text, Utf8Error> — validation is a value you handle, not something that happens invisibly during a conversion. Text.from_utf8_lossy substitutes replacement characters instead. Raw non-null-terminated byte sequences use &unsafe [Byte].

Callbacks​

Passing Verum functions to C requires they be plain (no closures, no contexts, no panics that cross the boundary):

@extern("C")
fn my_callback(ctx: *mut Void, data: *const Byte) -> Int {
    // plain code, no `using`, no `async`, no `Heap` allocations that
    // escape.
}

// Elsewhere:
unsafe {
    c_lib.register(my_callback as *const Void);
}

Panics that cross the FFI boundary are undefined behaviour. Wrap the body in try { ... } recover { _ => 1 /* error sentinel */ } if you need to suppress them.

Build-system integration​

verum.toml:

[dependencies]
openssl = { ffi = "system", libraries = ["ssl", "crypto"] }

[build]
link-search = ["/usr/local/lib"]
c-flags = ["-DOPENSSL_VERSION=3"]

Or use a build script for complex setups. See Build system.

What Verum does not do​

  • No bindgen: Verum does not auto-generate FFI bindings from C headers. Binding a C library is a deliberate act of contract authoring.
  • No extern "C++": C++ with its ABI zoo is out of scope. Wrap C++ in a C shim.
  • No auto-marshalling: Text does not silently become char*. You write the conversion.

Worked example — a minimal libsodium binding​

ffi Sodium {
    @extern("C")
    fn sodium_init() -> Int;

    @extern("C")
    fn randombytes_buf(buf: *mut Byte, size: Int);

    @extern("C")
    fn crypto_secretbox_easy(
        ciphertext: *mut Byte,
        message:    *const Byte,
        message_len: Int,
        nonce:      *const Byte,
        key:        *const Byte,
    ) -> Int;

    requires      message_len >= 0;
    memory_effects = Reads(message, nonce, key);
    memory_effects = Writes(ciphertext);
    thread_safe   = true;
    errors_via    = ReturnCode(result != 0);
    @ownership(borrow = [message, nonce, key, ciphertext])
}

const KEY_BYTES:    Int = 32;
const NONCE_BYTES:  Int = 24;
const MAC_BYTES:    Int = 16;

pub fn seal(message: &[Byte], key: &[Byte; 32]) -> List<Byte> {
    assert(Sodium.sodium_init() >= 0);

    let mut nonce = [0u8; NONCE_BYTES];
    unsafe {
        Sodium.randombytes_buf(nonce.as_mut_ptr(), NONCE_BYTES);
    }

    let mut out = List.with_capacity(message.len() + MAC_BYTES);
    out.resize(message.len() + MAC_BYTES, 0);
    let rc = unsafe {
        Sodium.crypto_secretbox_easy(
            out.as_mut_ptr(), message.as_ptr(), message.len(),
            nonce.as_ptr(), key.as_ptr(),
        )
    };
    assert(rc == 0);

    let mut framed = List.from(nonce);
    framed.extend(out);
    framed
}

Every unsafe block is narrowly scoped, the boundary contract pins down what the library reads and writes, and SMT discharges the requires at each call site. See Cookbook → FFI for a full walkthrough including error translation.

See also​