FFI Boundary Semantics

FFI Boundary Semantics

This chapter defines the Foreign Function Interface (FFI) boundary between Clef code and external C libraries on a target that links a host C runtime (Lane 1, hosted). It establishes the null-safety contract, the opaque-handle representation of a C binding’s pointer, and the normative requirements for binding generation tools like Farscape. It is the C instance of the foreign-boundary family; the JavaScript instance is JavaScript Boundary Semantics, and the two share the family invariant stated in §1.1. The FFI boundary exists whenever a C runtime is linked, and its presence is independent of whether the target is freestanding:

  • Hosted — libc is linked dynamically; the FFI boundary of this chapter applies as written.
  • Freestanding with static libc — libc is linked statically and its resources are accessed directly, with no dynamic linker in the image. The FFI boundary still exists and this chapter still applies; static coupling removes the dynamic-binding step (a supply-chain consideration developed in Getting to the Heart of Unikernels, out of scope here).
  • Bare (no C runtime) — no libc is linked at all, so there is no FFI boundary and nothing in this chapter applies. Interior memory follows the lifetime lattice defined in closure-representation.md §3.3.

Interior Clef has no raw pointer type. nativeptr<'T>, voidptr, and nativeint-as-pointer are not denotable in Clef source, at the FFI boundary or anywhere else. A C binding that returns a pointer marshals that pointer through an opaque handle, CHandle<'T>: the handle is non-arithmetic and non-dereferenceable in Clef source, and its only use is to be passed back across the boundary to another C binding. Interior callable values use the flat closure. Admitted memory views use the region and access carrier Ptr<'T, 'Region, 'Access> with bounds and lifetime obligations carried on the PSG (Memory Regions); a C handle cannot be cast into such a view. A register is the width-typed Mmio handle.

Implementation checkpoint, October 3, 2026 (informative): Farscape implements conservative nullable data-pointer generation and refuses unsupported adapters before writing output. CCS rejects raw source addresses, forged handles/function pointers and unavailable foreign lifetime/pointer adapters. Calque rejects the corresponding unsafe or managed-only source mechanisms before formatting writes. Native callable ABI publication through Baker/Fidelity.PSG and general foreign acquisition, retention and release adapters remain incomplete. FnPtr.fromSymbol currently produces CCS8096; the current native callback fixture is refused for missing target ABI realization. The contracts and examples below specify the required behavior; they do not establish native execution of an unimplemented conversion. Regenerated libraries require complete project checking and native validation for their actual target before adoption.

1. Null Safety Principle

1.1 Core Invariant

Null exists ONLY at the FFI boundary. Within Clef code, CHandle<'T> and FnPtr<'F> are NEVER null.

This invariant is fundamental to Clef’s memory safety guarantees. Unlike C where any pointer may be null, Clef enforces non-nullability at the type level. A C binding hands back an opaque handle rather than a raw pointer, so interior code never holds a dereferenceable address.

The statement above is the C instance of a family invariant that holds at every foreign boundary: a boundary’s absence sentinels exist only in its boundary conversions, and no foreign sentinel is representable in interior Clef. The C boundary’s sentinel is NULL, converted through Option as this chapter specifies. The JavaScript boundary’s absence alphabet has three states, converted as JavaScript Boundary Semantics §5 specifies. Each boundary chapter confines its own sentinels; interior code is identical under both.

1.2 Rationale

Null pointer dereferences are a leading cause of crashes and security vulnerabilities in native code. By eliminating null from the type system’s interior, Clef provides:

  1. Compile-time discipline: The type checker excludes null from an admitted handle; the boundary must establish admission and the resource’s separate validity and lifetime obligations
  2. Explicit optionality: Option<CHandle<'T>> makes nullability visible in the type signature
  3. Clean FFI boundary: Null handling is isolated to the interface with C code
  4. Boundary checks: Any required runtime null check occurs before admission, without adding a null state to interior handles

Non-nullness is not evidence that foreign storage remains allocated, that a handle names the expected object, or that a callable entry remains available. Those properties require the boundary obligations of §5.6. The type checker cannot establish them by inspecting a C declaration alone.

1.3 The FFI Boundary

The FFI boundary is the interface between Clef code and external C functions. At this boundary:

  • Outgoing (Clef → C): Option<CHandle<'T>> converts to nullable C pointer

    • None → NULL
    • Some handle → the pointer the handle carries
  • Incoming (C → Clef): Nullable C pointer converts to Option<CHandle<'T>>

    • NULL → None
    • Non-null → Some handle
┌─────────────────────────────────────────────────────────┐
│  Clef World                                        │
│                                                         │
│  CHandle<'T>            - NEVER null, opaque           │
│  FnPtr<'F>              - NEVER null                   │
│  Option<CHandle<'T>>    - explicit nullability         │
│  Option<FnPtr<'F>>      - explicit nullability         │
└─────────────────────────────────────────────────────────┘
                         ↕ FFI Boundary
┌─────────────────────────────────────────────────────────┐
│  C World                                                │
│                                                         │
│  T*                    - may be NULL                   │
│  void (*f)(...)        - may be NULL                   │
└─────────────────────────────────────────────────────────┘

2. Pointer Types at FFI Boundary

2.1 Non-Nullable Handles

Clef TypeC EquivalentSemantics
CHandle<'T>T* (non-null)Opaque typed handle; non-arithmetic and non-dereferenceable; resource validity is a separate obligation
CHandle<unit>void* (non-null)Opaque handle; carries no evidence for reinterpreting the foreign object’s type
FnPtr<'F>Function pointer (non-null)Declared callable entry; its complete ABI and code lifetime must be established

A CHandle<'T> carries a C pointer across the boundary but exposes no pointer operations in Clef source: no arithmetic, no dereference, no conversion to an integer. Its only role is to be handed back to another C binding. These types have no null representation, and attempting to construct a null value is a compile-time error.

2.2 Nullable Handles (FFI Only)

Clef TypeC EquivalentSemantics
Option<CHandle<'T>>T* (nullable)None or a nonnull typed handle
Option<CHandle<unit>>void* (nullable)None or a nonnull opaque handle
Option<FnPtr<'F>>Function pointer (nullable)None or a nonnull callable entry

At the FFI boundary, Option expresses absence without admitting a null handle or null callable entry inside Clef. The same ordinary Option value may be retained and matched by interior code.

2.3 Memory Layout

The native C carrier of Option<CHandle<'T>> or Option<FnPtr<'F>> is a single platform word:

  • None is represented as the bit pattern 0 (null)
  • Some handle is represented as the carried pointer value itself

This specifies the boundary carrier, not the representation of every interior Option value. The compiler SHALL convert between that carrier and the admitted logical None/Some representation. A specialization that also gives an interior optional handle this single-word layout SHALL establish the required representation equivalence. It SHALL NOT reinterpret a generic tagged option as a C pointer merely because its source type contains a handle.

3. FnPtr Intrinsics

3.1 FnPtr Type

FnPtr<'F> is a function pointer type where 'F is the full function signature:

FnPtr<unit -> unit>                              // void (*)(void)
FnPtr<int -> int>                                // int (*)(int)
FnPtr<Option<CHandle<byte>> -> int -> int>        // int (*)(char*, int)
FnPtr<Option<CHandle<int>> -> unit>               // void (*)(int*)
FnPtr<CHandle<byte> -> int>                       // int (*)(char* _Nonnull)
 

The type parameter 'F MUST be a function type ('a -> 'b). Using a non-function type is a compile-time error.

3.2 FnPtr.fromSymbol

Declares an external symbol to be resolved by the linker.

Signature:

FnPtr.fromSymbol<'F> : string -> FnPtr<'F>

Semantics:

  • The string argument MUST be a compile-time constant (string literal)
  • Returns a non-null function pointer (linker guarantees symbol exists)
  • Symbol resolution occurs at link time, not runtime

Example:

// Declare external C functions
let private strlen_ptr = FnPtr.fromSymbol<CHandle<byte> -> int> "strlen"
let private gtk_init_ptr =
    FnPtr.fromSymbol<Option<CHandle<int>> -> Option<CHandle<CHandle<byte>>> -> unit> "gtk_init"

Code Generation: The middle end emits portable dialects only: an external func.func declaration for the symbol, and the symbol as a func.constant referencing that declaration — a first-class function value in the portable dialect, with no cast. Each target pathway realizes it through its standard lowerings: the LLVM pathway (CPU/MCU) lowers the declaration to an llvm.func and the constant to an llvm.mlir.addressof, which is the address the C side receives; other pathways realize it in their own terms. The conversion of a function value to an address is therefore a pathway commitment made at the extern boundary, never a middle-end operation.

3.3 FnPtr.invoke

Calls a function through a function pointer.

Signature:

FnPtr.invoke : FnPtr<'F> -> 'F

Semantics:

  • Invokes the function with the provided arguments
  • Arguments matching Option<CHandle<'T>> are marshalled (None → NULL)
  • Return values matching Option<CHandle<'T>> are marshalled (NULL → None)

Example:

// Call external function
let len = FnPtr.invoke strlen_ptr myStringPtr

// Call with nullable arguments (None → NULL)
FnPtr.invoke gtk_init_ptr None None

3.4 FnPtr.ofFunction

Admits a module-level Clef function as a native-entry value with a settled receiving contract.

Signature:

FnPtr.ofFunction : 'F -> FnPtr<'F>

Constraints:

  • The argument MUST be a reference to a module-level let binding
  • Lambdas and closures are REJECTED at compile time
  • The function must not capture any environment
  • The complete parameter and result representations, conversions and code lifetime MUST be settled from the binding, its receiving contract and the selected target

For a compiler-owned family, CCS/Baker MAY establish a portable interior calling convention from the selected target’s declared capabilities. Every supplying origin and indirect invocation MUST agree with that contract. Baker SHALL record identity conversions explicitly where the selected representations already agree. Code-lifetime evidence SHALL retain the actual declaration and its residence in the containing program image. Aggregate transport follows §3.6 and preserves these premises.

A portable interior convention authorizes operations within Clef. Crossing a foreign boundary additionally requires the declared foreign contract, a settled native ABI and any Baker-established adaptation. An entry awaiting those facts MUST be refused at that crossing. The middle end retains a portable function value, and the target pathway realizes its address only at an admitted extern boundary. Loading and retention obligations follow the actual loading contract under §5.6.

Rationale: A C callback requires both a stable entry and its declared native ABI. An interior flat closure’s code value and environment are not automatically a C entry and void* pair. A captured callback requires an admitted adapter and retention/release proof under §5.6; FnPtr.ofFunction itself does not supply that mechanism.

Example:

// OK - top-level function
let myCallback (x: int) : int = x + 1
let callbackPtr = FnPtr.ofFunction myCallback

// ERROR - lambda (even without captures)
let ptr = FnPtr.ofFunction (fun x -> x + 1)  // Compile error

// ERROR - closure with captures
let multiplier = 2
let ptr = FnPtr.ofFunction (fun x -> x * multiplier)  // Compile error
 

3.5 Optional Function Pointers

An absent function pointer is represented by None of type Option<FnPtr<'F>>. Pattern matching distinguishes absence from a callable value.

let maybeCallback : Option<FnPtr<int -> unit>> = None
match maybeCallback with
| Some cb -> FnPtr.invoke cb 42
| None -> ()

Interior Option<FnPtr<'F>> uses the ordinary union-payload protocol of Discriminated Union Representation §9.1. Some retains the entry as a callable component with its contract; None has no callable payload. This does not store a null function value, add an absent member to the callable family, or require the C-boundary absence conversion of §4. That conversion is a separate boundary obligation.

3.6 Interior Records and Callable Components

A record holding FnPtr<'F> inside Clef is an interior logical record. Construction, copy-and-update, field selection, aliasing, branching, matching, passing and returning it do not cross the FFI boundary. Each native-entry field uses the callable-component protocol of Closure Representation §2.4, with explicit absence of an ordinary closure environment. Ordinary function fields retain their flat environments under that same protocol. Callable union payloads use it as specified in Discriminated Union Representation §9.1.

  1. Component representation. CCS/Baker settles the complete finite family of alternatives that construction, copy or assignment can supply to a slot. A single-entry family needs no code storage. A family of n > 1 alternatives stores a finite selector with logical domain exactly [0, n). Reading the slot reconstructs the selected function value through portable control flow. The selector is neither an address nor an encoding of one; no conversion between selectors and code addresses is permitted. No interior aggregate data slot holds a native entry as an integer, handle, byte pattern or address.
  2. Contract identity. Each inhabited native-entry slot has one receiving contract identity. The contract includes parameter and result representations and conversions, calling convention, code-lifetime premises and applicable resource obligations (§3.4, §5.3, §5.6). Its identity retains the governing declaration and content; equal source types, machine signatures or word sizes do not establish equal contracts. Every alternative SHALL carry that receiving contract or an explicit Baker-settled adapter to it. A field read, alias, copy, parameter, result or join SHALL preserve the contract. Missing or incompatible contracts at a commitment are rejected, never inferred from the Clef function type alone.
  3. Association and writes. A boundary declaration’s record and field names resolve to the instantiated declaration and slot identity, not later source spelling. Construction, copy-and-update and assignment retain the written alternative and its actual formation. A write with several possible entries requires source-settled dispatch; comparing function values to reconstruct that dispatch is not permitted. Reads retain their established snapshot; later reassignment does not change an earlier read’s value.
  4. Complete evidence. Every supplying origin and write must participate in the slot’s settled account. Equal implementation symbols do not merge formation occurrences or discharge code lifetime. An entry of unknown origin, including one supplied dynamically by foreign code, cannot be assumed to belong to a finite family. Storing it requires a separately admitted representation preserving its contract and lifetime. Until that representation is admitted, the store is diagnosed at commitment. This is an admission limit, not permission to represent an interior entry as data.
  5. No implicit C layout. Interior record byte placement covers its data, selectors and any ordinary closure environment views under the settled Clef layout. Foreign code SHALL NOT read or write this interior form as a C structure, buffer, byte view or region. A native listener table requires a separately declared and admitted projection, including layout, target realization, entry contracts and retention obligations (§5.6). Without that projection the crossing is rejected.
  6. Absence and freshness. An inhabited FnPtr component always denotes an admitted entry; it is never zero-filled or defaulted. Optional entries use §3.5. Every aggregate row, including formation, slot, selection, contract and tag relations, SHALL contribute to the published dependency account. Changed formation, environment or tag evidence SHALL invalidate dependent selections and proof receipts before witnessing, even when the resulting function or observable value is unchanged.

Implementations SHALL diagnose unsupported aggregate forms at the commitment boundary rather than introduce a raw code carrier or manufacture a contract. Interior optional components and C-boundary absence conversions are independent admission questions. The compiler diagnostic allocations for these obligations are given in Error Handling.

4. Option↔NULL Marshalling

This is C-boundary absence conversion: Clef None corresponds to C NULL, and C NULL corresponds to Clef None. NULL belongs to the foreign ABI; the conversion does not introduce a null value, null literal or raw pointer comparison into Clef. Its interior operands and results use Option.

4.1 Parameter Marshalling (Clef → C)

When a function parameter has type Option<CHandle<'T>> or Option<FnPtr<'F>>:

Clef ValueC Value
NoneNULL (0)
Some handlethe pointer the handle carries

Optimization: When the argument is a compile-time None literal, the compiler directly emits null without runtime checks.

4.2 Return Value Marshalling (C → Clef)

When a function return type is Option<CHandle<'T>> or Option<FnPtr<'F>>:

C ValueClef Value
NULL (0)None
Non-nullSome handle

Code Generation (portable dialects): For an optional data handle, the middle end may express an admitted native-word comparison with portable operations such as func.call, index and arith.cmpi, then construct the settled logical option. An optional native entry instead requires an admitted boundary conversion whose callable result remains a function value. It SHALL NOT convert that function value to index or compare it with integer zero to implement absence. Native address/null realization belongs to the target pathway. An unsupported conversion is diagnosed at the crossing. Neither form permits reinterpreting a generic tagged option as a native word; any single-word specialization requires representation equivalence evidence. Interior Option<FnPtr> remains governed by §3.5 and §3.6.

4.3 Non-Marshalled Types

Scalar values and admitted nonnull handles do not require an absence conversion:

  • CHandle<'T>: passed as-is (must be non-null)
  • FnPtr<'F>: passed as-is (must be non-null)
  • int, float, etc.: passed as-is (value types)

Their ABI widths, signedness, passing modes and result convention remain declared boundary facts. A logical value’s source kind does not establish its native representation.

5. Farscape Binding Generation Contract

This section defines normative requirements for Farscape and other binding generation tools.

Informative. The C++ Binding via Farscape guide describes how these requirements are applied in practice.

5.1 C Nullability Annotation Mapping

Farscape MUST interpret C nullability annotations as follows:

C AnnotationPlatformClef Output
_NonnullClang/AppleCHandle<'T>
_NullableClang/AppleOption<CHandle<'T>>
_Null_unspecifiedClang/AppleSee default policy
__attribute__((nonnull))GCCCHandle<'T>
_In_Windows SALCHandle<'T>
_In_opt_Windows SALOption<CHandle<'T>>
_Out_Windows SALCHandle<'T>
_Out_opt_Windows SALOption<CHandle<'T>>

The same policy applies to function-pointer slots using FnPtr<'F> and Option<FnPtr<'F>>. Attributes identify the annotated pointer level and parameter positions; typedefs, macro expansion and output cells SHALL NOT erase that evidence. A nonnull annotation on an outer pointer does not establish that a pointed-to value is nonnull. Contradictory native and binding annotations SHALL be diagnosed.

An annotation read from a native header is contract evidence with identified provenance. A representation fact measured against the selected target, including a record layout carried in a BAREWire descriptor under the selected platform declaration, is established evidence and SHALL be recorded as such. A checked conversion establishes admission from the actual returned value before constructing a nonnull handle. Reliance on foreign behavior that neither measurement nor a checked conversion establishes SHALL be recorded as an external execution hypothesis under Conformance §6.1.

5.2 Default Policy (Unannotated Pointers)

When C code lacks nullability annotations, Farscape MUST apply these defaults:

Function Parameters:

  • Default: Option<CHandle<'T>> for a data pointer, or Option<FnPtr<'F>> for a function-pointer slot
  • A nonnull contract may narrow the accepted argument to CHandle<'T> or FnPtr<'F>

Function Return Values:

  • Default: Option<CHandle<'T>> for a data pointer, or Option<FnPtr<'F>> for a function pointer
  • A nonnull result requires explicit native or binding contract evidence, or a checked boundary conversion that rejects absence before admission

These defaults also apply to pointer fields in an admitted native value-record projection and to every native argument and result within a callback signature. A qualifier on a callback argument does not establish that the callback slot is nonnull. A qualifier on an inner pointer does not establish that an outer pointer or output cell is nonnull.

Rationale: Absence of an annotation does not prove that C never returns or accepts NULL. An opaque pointer typedef follows the same default as an explicit T*; its spelling does not remove nullability. An implementation unable to realize a required optional function-pointer or callback-entry conversion SHALL diagnose that unsupported contract before emitting a binding, rather than silently substituting a nonnull carrier.

5.3 Generated Binding Structure

Farscape-generated bindings MUST declare the native symbol, complete C ABI, permitted absence conversions, and the resource contract before exposing a Clef operation. A binding MAY use compiler-recognized extern declarations with FunctionDescriptor metadata and declared CallbackDescriptor entries, or the FnPtr.fromSymbol/FnPtr.invoke route. Both forms are subject to the same representation, lifetime and preservation obligations; use of a particular symbol-resolution intrinsic is not mandatory.

Source signatures use Clef value kinds and opaque carriers. Native integer widths and signedness, pointer widths, calling convention and passing modes belong to the descriptor and selected target declaration. An opaque C pointer typedef supplies a nominal marker for CHandle<Marker>, not a record exposing an integer address, a null constructor, or a dereference operation.

The binding owns native marshaling, callback adaptation and resource lifecycle. Its application-facing operations SHALL establish those obligations before invoking an application handler or admitting an application value. A native entry record or a descriptor placed in a binding package does not itself discharge them.

5.4 Ambiguity Handling

When nullability is ambiguous, Farscape MUST retain the nullable default or diagnose an unsupported conversion. It SHOULD:

  1. Identify missing evidence and the nullable policy applied
  2. Support a hints file for manual override
  3. Document the default in generated binding comments

Binding hints are contract declarations with identified provenance. They SHALL NOT erase contradictory native evidence or silently discharge a lifetime, spatial or ownership obligation. The implementation SHALL state the subset of boundary conversions it admits and diagnose required obligations outside that subset.

Hints File Format (illustrative contract; concrete generator syntax is implementation-defined):

[gtk_window_new]
return = "nonnull"  # Declared native result contract, not proof of the C implementation

[g_object_get_data]
return = "nullable"  # Override: may return NULL if key not found
 

5.5 Callback Function Types

For C functions accepting callbacks, Farscape MUST:

  1. Generate FnPtr<'F> for non-null callback parameters
  2. Generate Option<FnPtr<'F>> for nullable callback parameters
  3. Document that callbacks must be top-level functions (no closures)

The complete callback signature includes the nullability of every native input and result, independently of whether the callback slot itself is optional. A narrower API may require a supplied nonnull entry where the C API also permits an absent slot; it SHALL document that restriction. Native values arriving through the entry still require their own admission evidence or adapter. Where the implementation cannot convert an optional slot or a nullable incoming value, it MUST reject that contract; a bare FnPtr or CHandle is not a substitute for the missing conversion.

5.6 Boundary Proof Obligations

The following requirements concern admitted bindings. They do not assert that any particular generator or compiler implements every case.

Resource identity and ownership. A returned foreign handle’s contract SHALL identify whether the resource is owned, borrowed from a named owner, or static, the operations permitted on it, and any release or retention obligation. An owned acquisition SHALL be paired with its release operation, including cleanup on failure. A borrowed handle’s owner SHALL outlive every use. A static classification requires an established lifetime covering all uses. Missing ownership information SHALL NOT be reported as proof that a resource is borrowed or needs no release.

Retirement and aliases. Release or ownership transfer SHALL retire the caller’s right to use every affected alias. Subsequent calls with a retired handle SHALL be excluded by an established graph lifetime/resource obligation or prevented by a binding-owned checked retirement mechanism. A reusable copy of the opaque word does not preserve validity after free, destruction, disconnect or library unload. These obligations use the lifetime/coeffect discipline of Memory Regions, without adding ownership or borrowing annotations to Clef source.

Spatial admission. A buffer crossing SHALL establish its element representation, byte extent, alignment, access mode and permitted retention. Native length arguments SHALL be related to the actual Clef bound; a count or stride alone is not an extent proof. A NUL-terminated operation also requires a terminator within the admitted extent. strlen receiving a nonnull CHandle does not establish any of these facts. A mapped native result may become a Ptr<'T, 'Region, 'Access> only through an admitted boundary projection that establishes its bounds, region lifetime and access obligations; no generic handle reinterpretation is permitted.

Callback environments. A void* userdata slot SHALL be associated with one declared environment type and its actual producer, callback entry and release/retirement operation. Matching the native word size does not establish that association. A binding SHALL NOT retype userdata as an integer or recover a captured environment through an unchecked cast. The native adapter SHALL declare and preserve the complete C arity and result convention while converting values before invoking the interior Clef handler.

For a captured callback, the retained flat environment SHALL outlive registration and every possible invocation. A native destroy hook SHALL release that same retained environment exactly once after the last possible invocation; registration failure SHALL undo any retention already performed. Without a destroy hook, the binding SHALL establish explicit retirement and release. A closed module entry has no captured environment to retain; a no-op release hook for that entry does not establish captured-callback support.

PSG settlement and preservation. CCS/Baker SHALL derive the applicable ABI, absence, resource, spatial and callback-environment obligations during elaboration, with the actual acquisition, call, callback, alias and release participants. Saturation SHALL retain unresolved premises and settle the admitted representation and lifetime coeffects before emission (Closure Representation §11, Program Semantic Graph). A declaration or recorded proposition is not its proof. Required unresolved obligations SHALL be diagnosed at the commitment boundary; lowering SHALL preserve or recheck discharged properties under Conformance §6. Reliance on foreign code or an execution environment SHALL remain distinguishable from compiler-established evidence.

6. Examples

6.1 GTK Bindings

This example spells the native transport signatures. Admission also requires the target ABI descriptors and resource contracts of §5.6, including the window’s owner and retirement operation. Returning a nonnull window handle alone does not establish its usable lifetime.

module Platform.GTK

// External declarations
let private gtk_init_ptr =
    FnPtr.fromSymbol<Option<CHandle<int>> -> Option<CHandle<CHandle<byte>>> -> unit> "gtk_init"

let private gtk_window_new_ptr =
    FnPtr.fromSymbol<int -> CHandle<GtkWindow>> "gtk_window_new"

let private gtk_widget_show_all_ptr =
    FnPtr.fromSymbol<CHandle<GtkWidget> -> unit> "gtk_widget_show_all"

let private gtk_main_ptr =
    FnPtr.fromSymbol<unit -> unit> "gtk_main"

// Native binding operations; resource obligations remain attached to every use
let gtkInit () =
    FnPtr.invoke gtk_init_ptr None None

let gtkWindowNew (windowType: GtkWindowType) : CHandle<GtkWindow> =
    FnPtr.invoke gtk_window_new_ptr (int windowType)

let gtkWidgetShowAll (widget: CHandle<GtkWidget>) : unit =
    FnPtr.invoke gtk_widget_show_all_ptr widget

let gtkMain () =
    FnPtr.invoke gtk_main_ptr ()

6.2 libc Bindings

This example is hosted-libc (Lane 1). malloc/free exist only where a C runtime with a heap is linked. On a no-heap target these particular bindings do not exist, and interior memory follows the lifetime lattice of closure-representation.md §3.3: a value that classifies as genuinely-dynamic on a no-heap target is a compile-time lifetime error rather than a call to malloc. A bare target with no C runtime at all has no FFI boundary of any kind.

The binding contract classifies a successful malloc acquisition as owned, pairs it with free, and retires every affected alias on release. A strlen argument requires an admitted byte extent with a terminator inside that extent. The following private declarations illustrate native carriers; they do not supply these proofs or expose an unchecked allocation/release API to application code.

module Platform.Libc

// strlen: accepts a live, admitted NUL-terminated byte sequence
let private strlen_ptr =
    FnPtr.fromSymbol<CHandle<byte> -> int> "strlen"

// malloc: may return NULL on failure
let private malloc_ptr =
    FnPtr.fromSymbol<int -> Option<CHandle<unit>>> "malloc"

// free: accepts NULL (no-op)
let private free_ptr =
    FnPtr.fromSymbol<Option<CHandle<unit>> -> unit> "free"

6.3 Callback Pattern

A GLib gpointer userdata argument is a foreign void*, never a Clef integer. A binding that admits a nonnull typed context uses matching callback and release signatures:

module Platform.GLib

type IdleContext = private | Opaque_IdleContext

// gboolean (*)(gpointer), under a declared nonnull context contract
type GSourceFunc = CHandle<IdleContext> -> int

// void (*)(gpointer), retiring that same context
type GDestroyNotify = CHandle<IdleContext> -> unit

type IdleEntry = { Invoke: FnPtr<GSourceFunc> }
type IdleReleaseEntry = { Release: FnPtr<GDestroyNotify> }

The binding SHALL declare a CallbackDescriptor for each entry, including gboolean’s native integer representation and the release entry’s C void result. It SHALL pass an actual admitted IdleContext resource to g_idle_add_full, keep that resource live for every invocation, and connect native source teardown to the matching release entry. A captured handler additionally requires the retained flat-environment obligation of §5.6. Supplying None as userdata requires a nullable callback-input adapter; it cannot be combined with the nonnull signatures above. An implementation lacking the necessary conversion or retention mechanism SHALL reject the registration.

The ordinary application handler receives values converted by the binding. The native context and release entries remain within the binding; their opaque carriers do not authorize a userdata cast or application-side pointer operation.

7. Normative Summary

  1. A C binding’s pointer marshals through the opaque CHandle<'T>; interior Clef has no raw pointer type, and nativeptr<'T>/voidptr/nativeint-as-pointer are not denotable anywhere. CHandle<'T> and FnPtr<'F> are NEVER null within Clef code
  2. Option<CHandle<'T>> and Option<FnPtr<'F>> represent nullable pointers at the FFI boundary
  3. FnPtr.fromSymbol declares linker-resolved external symbols
  4. FnPtr.invoke calls through function pointers with automatic Option↔NULL marshalling
  5. FnPtr.ofFunction converts top-level functions only (no closures)
  6. Farscape MUST follow the nullability annotation mapping and default policies defined herein
  7. This chapter applies wherever a host C runtime is linked, whether dynamically (hosted) or statically (freestanding with static libc); a bare target with no C runtime has no FFI boundary, and its interior memory follows the lifetime lattice of closure-representation.md §3.3
  8. Unannotated foreign pointers are nullable; nonnull admission requires explicit contract evidence or a checked conversion. Unsupported required conversions SHALL be diagnosed rather than replaced by a nonnull carrier
  9. Non-nullness does not discharge resource validity, ownership, alias retirement, spatial extent or callback-environment lifetime. CCS/Baker SHALL carry and settle the applicable obligations on the PSG, and lowering SHALL preserve or recheck them under Conformance §6