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

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.

A matching layout, including a BAREWire StructDescriptor or a measured record or buffer layout, SHALL NOT authorize dereferencing a CHandle<'T> or converting it to a Ptr<'T, 'Region, 'Access> or any interior pointer or reference. Such a layout supplies schema and byte-offset facts only; sharing memory with C or C++ code without copying requires the separate admission obligations of §5.6.

2.2 Nullable Handles (FFI Only)

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.ofExtern

Admits a declared external function as a typed native entry under its current boundary contract.

Implementation status, October 14, 2026 (informative): Local immutable declared-extern entry formation and invocation are accepted for Linux AMD64 libc under an explicitly selected process-link contract. Module-level entry storage, other ABI/target forms and library loading remain outside that accepted scope. Unsupported forms must issue the located refusal rather than substitute symbol-only lookup.

Signature:

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

Semantics:

• The operand MUST resolve to the actual compiler-recognized extern binding. A symbol string, descriptor quotation, ordinary function, lambda or captured closure is not an extern declaration.
• CCS/Baker SHALL establish the complete function signature, native ABI, passing modes, calling convention, required conversions and code lifetime from that declaration, its exact current descriptor and the selected target. Equal C names or equal physical signatures do not establish declaration or contract identity.
• Forming the entry does not execute the extern’s source placeholder, evaluate its descriptor, or prove the external function’s behavior. Any supplied behavioral contract remains a separately recorded external execution hypothesis.
• Symbol resolution and code residence SHALL follow the actual link/loading contract. Missing, ambiguous, stale or unsupported contracts SHALL be diagnosed before witnessing. Entry formation grants no ownership, retention, unloading or exported-library loading authority.
• The entry is nonnull only under the admitted declaration/loading contract. FnPtr.fromSymbol is retired and SHALL be refused with a located diagnostic naming FnPtr.ofExtern.

Example:

// NativeLabs.Libc.labs is an existing generated extern with its ABI descriptor.
let private labsEntry = FnPtr.ofExtern NativeLabs.Libc.labs
let result = FnPtr.invoke labsEntry 5

Code Generation: The middle end retains the admitted external func.func declaration and a func.constant referring to that declaration. Neither symbol spelling nor a source placeholder supplies authority. Target pathways realize the admitted function value through their standard lowerings; the LLVM pathway uses the corresponding native declaration and llvm.mlir.addressof. No middle-end pointer/integer cast or raw code-address carrier is introduced.

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 or callback table requires a separately declared and admitted projection (REC-TABLE-PROJECTION, CCS8418), including measured target layout (REC-TABLE-LAYOUT, CCS8419), per-field entry contracts and absence evidence (REC-TABLE-CONTRACT, CCS8420), initialization-only writes and immutable snapshot reads (REC-TABLE-WRITE, CCS8421), table storage and environment residence and retirement obligations (REC-TABLE-RESIDENCE, CCS8422), and any declared discriminant selecting between alternative callback fields (REC-TABLE-DISCRIMINANT, CCS8423) (§5.3, §5.5, §5.6). Without that projection, or through a pointer hop or reinterpretation, 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 and native callback table violations 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 interior callable components (CCS8410–CCS8415) and native callback tables (REC-TABLE, CCS8418–CCS8423) 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>>:

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

The supported explicit-promise callback profile records foreign acceptance of absence separately from callback activation, through a CallbackAbsenceContract. Without that premise, a None conversion remains Pending. The promise alone does not discharge the source-to-target conversion obligation. Some retains its existing entry, activation and lifetime requirements independently.

4.2 Return Value Marshalling (C → Clef)

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

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:

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, and MAY expose a typed entry through FnPtr.ofExtern/FnPtr.invoke only after that same declared contract is admitted. Entry formation supplies no alternative symbol-only authority and does not weaken representation, lifetime or preservation obligations.

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.

For an operation sharing memory with a C or C++ library without copying, the binding SHALL identify the actual shared region and allocation, the accessed fields or elements, and the foreign retention class and retirement event. A matching BAREWire StructDescriptor or measured record or buffer layout supplies schema and byte-offset facts only. It SHALL NOT by itself discharge any of the four Shared-memory obligations in §5.6 or authorize a handle dereference or conversion prohibited by §2.1.

A binding whose operation invokes a supplied callback only within its own activation and retires every use of it before returning MAY declare that scope (Platform Bindings, Quotation Structure Requirements, ScopedCallbackDescriptor). The declaration is a library obligation with identified provenance, read for activation, demand and initialization order alike; it is never compiler-established evidence that the binding honours it.

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. Admit a captured closure as a native callback only through an admitted callback adapter under the Callback environments obligations of §5.6 (associating the void* userdata slot with one declared environment type and its actual producer, callback entry and release/retirement operation; retaining the flat environment across registration and every possible invocation; releasing that retained environment exactly once via a native destroy hook after the last possible invocation, undoing retention on registration failure, or establishing explicit retirement and release when no destroy hook exists), while preserving the restriction that FnPtr.ofFunction (§3.4) applies only to closed module-level functions without captures and that a native callback slot without an associated userdata context argument admits closed entries only

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, a nullable incoming value, or a captured callback environment, it MUST reject that contract; a bare FnPtr, CHandle, or closed-only entry is not a substitute for the missing adapter or obligation.

When a C API accepts or retains a struct of callback function pointers as a native callback or listener table, Farscape and the compiler MUST enforce the table projection and contract obligations of §3.6 (items 2, 3, 5 and 6), §5.3 and §5.6 and refuse any violation with its REC-TABLE diagnostic code (Error Handling): a crossing without a separately declared and admitted table projection or via a pointer hop (REC-TABLE-PROJECTION, CCS8418), a projection whose layout disagrees with the target’s measured StructDescriptor (REC-TABLE-LAYOUT, CCS8419), a field lacking its declared CallbackDescriptor or receiving contract identity, mismatching a parameter or result representation or calling convention, or supplying None or narrowing nullability without established absence evidence (REC-TABLE-CONTRACT, CCS8420), a post-initialization entry write, zero-filled entry or non-snapshot read (REC-TABLE-WRITE, CCS8421), table storage or a captured environment that is borrowed beyond the call, fails to outlive every foreign read or invocation interval, or lacks required environment retirement or release (REC-TABLE-RESIDENCE, CCS8422), or a projection that selects between alternative callback fields without a declared discriminant (REC-TABLE-DISCRIMINANT, CCS8423).

5.6 Boundary Proof Obligations

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

The buffer-return example in Decidable by Construction, §6.4, develops this boundary’s evidence chain: the actual call, success branch, out-parameter, destination and consumer remain associated. A bound on a different counter cannot establish that this call initialized the prefix being consumed. The paper’s tiered account is informative; the requirements below govern admitted bindings.

For their application to a callback completing a stateful-service request, see Coexponential Exploration in the Clef Programming Language, §§4.3, 10.4 and 10.6. The research account binds completion to its invocation and captured environment, and distinguishes retiring an actor identity from reclaiming storage still reachable by outstanding foreign or device work.

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.

Shared-memory obligations. Sharing memory across the FFI boundary with a C or C++ library without copying SHALL require all four obligations below to be established on the PSG before emission. A matching layout, including a BAREWire StructDescriptor or measured record or buffer layout, supplies schema and byte-offset facts only and SHALL NOT suffice for admission.

1. Bounded extent. The byte bound SHALL derive from the actual allocation or region capacity, or an admitted boundary extent proof tied to that storage. The element count and stride, including field offsets and access sizes, SHALL be related to that byte bound so that every accessed byte lies within the admitted extent under the actual arithmetic and conversion semantics. A count, stride or layout size alone SHALL NOT constitute an extent proof.
2. Alignment and byte order. The shared region and every accessed field or element SHALL have alignment and byte order compatible with the selected target’s measured or declared ABI and the applicable BAREWire descriptor requirements. Matching offsets alone SHALL NOT establish either property.
3. Lifetime and retention. An established lifetime SHALL cover the foreign retention class. Call-bounded sharing SHALL retire every foreign access before the call returns. If the library retains memory after a call returns, the backing region and allocation SHALL outlive every interval in which the library or asynchronous or device work may read or write the storage, until an admitted release, unregister or completion event retires foreign access. Return from the registering call alone SHALL NOT retire retained access or authorize reclamation or reuse of the storage.
4. Access discipline. The shared interval SHALL enforce the admitted ReadOnly or ReadWrite access kind for each participant, together with volatility and ordering requirements where applicable. ReadOnly SHALL exclude writes through that access; ReadWrite SHALL NOT by itself establish exclusive access. The discipline SHALL exclude conflicting use, including concurrent or aliased mutation between Clef and foreign code during the shared interval. Any transfer or synchronization permitting a change of access SHALL be established before the affected use.

These obligations SHALL remain tied to the actual storage, accesses and retirement participants under PSG settlement and preservation and Identity and dependent code below. A missing obligation SHALL remain unresolved and prevent emission of the sharing operation. Even a matching layout SHALL NOT authorize dereferencing a CHandle<'T> or converting it to a Ptr<'T, 'Region, 'Access> or any interior pointer or reference; an admitted boundary projection establishes a separate memory view under the obligations above, never a generic reinterpretation of the opaque handle.

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.

Inferred coverage. For each required boundary claim C, the implementation SHALL derive a sound overapproximation R of reachable states at the actual use from the program and admitted contracts. If a discharge proves H ⇒ C under obligation premises H, it SHALL separately establish R ⊆ H and the applicable non-vacuity conditions below. It SHALL NOT insert H or C as an assumption merely to derive R or establish their own coverage. Applicable obligations SHALL be inferred without application predicates or refinement-type annotations; a binding contract supplies identified premises, not a discharge. Missing required premises SHALL remain Pending.

Path and transfer soundness. A guard may narrow R only for the actual value and path it controls, while that evidence remains valid. Joins SHALL cover every predecessor not established unreachable; loop invariants SHALL cover entry and every iteration not established unreachable. Transfers SHALL respect the actual arithmetic, signedness, conversion and wrapping semantics of the source and target representations. A mathematical-integer result alone does not justify a native conversion, truncation or machine operation. Control-flow facts SHALL be established by their owning transfer rules, without introducing a new external hypothesis or erasing inherited dependencies.

Foreign semantic premises. ABI width, signedness and layout concern representation, not behavioral bounds on a foreign result. Such bounds SHALL come from established evidence, an admitted contract with identified provenance and applicable preconditions, or a checked conversion of the actual value. Unchecked foreign behavior SHALL remain an explicit external execution hypothesis (§5.1) in the claim’s trusted base, with its header, GIR or pilot (binding-author declaration) provenance and contract identity and version retained in validity dependencies. Derived claims and code consuming them SHALL inherit those dependencies. Neither a descriptor’s presence nor the desired safety property supplies that hypothesis implicitly. A relational contract, such as -1 ≤ result ≤ count, SHALL be instantiated with the actual argument at each application and its admitted preconditions; substituting a fixed capacity or only an upper bound on that argument does not establish the exact argument-result relation. Preconditions on program participants, including buffer extent, count and initialization, SHALL be established at that application or remain Pending; declaring the foreign contract does not establish those caller obligations. A missing required semantic result contract SHALL leave dependent safety claims Pending at the call site; ABI representability SHALL remain separate.

Premise origins and source participants. A boundary claim SHALL distinguish the selected target platform’s declared ABI widths as trusted-base assumptions, an extent established from the actual allocation node as a graph-proved fact, and a descriptor’s result relation as an external execution hypothesis with identified provenance. A target measurement establishes a representation fact relative to the platform declaration; both evidence origins SHALL remain explicit. For a platform-library operation whose claims depend on a native result, that result and the applicable guards, actual arguments and allocation participants SHALL be present in the owning platform source before obligation elaboration. A read-and-copy operation returning a string may keep its numeric count internal; its public string result does not substitute for that participant. Lowering SHALL NOT invent witness facts to replace the missing source operation, guard or allocation, or promote one premise category into another.

Native-to-Clef narrowing. Initial elaboration SHALL retain a distinct node-level obligation for each native-to-Clef narrowing. It SHALL remain Pending until the selected target’s source and destination widths and signedness are settled, then be checked at those actual representations. Narrowing includes a same-width signedness change that cannot represent every source value. The obligation SHALL cover the actual converted value, including admitted error results; checking only the value after truncation does not establish safe admission.

Coverage and non-vacuity outcomes. A discharged conditional formula does not establish that its premises cover the actual use. The implementation SHALL distinguish established coverage, an uncovered abstract state, formula refutation, established concrete failure, inconsistent premises, established unreachability, and missing or undecided evidence. An uncovered model in R outside H SHALL NOT be reported as a concrete program failure without establishing its realizability and violation of the required claim. A model of H ∧ ¬C refutes the conditional formula under H; the claim is not established. It SHALL be reported as a concrete program failure only when its realizability under the actual program and admitted contracts is established. Inconsistent premises SHALL NOT be reported as successful verification of a reachable use. Establishing premise consistency alone does not establish coverage or transfer soundness.

For discharge by refutation at a use not established unreachable, the implementation SHALL establish SAT(H) separately from UNSAT(H ∧ ¬C), projecting both queries from the same typed obligation record and checking context. An unknown result or checking error SHALL leave the obligation Pending; an unsatisfiable H SHALL be reported as inconsistent premises rather than a discharged reachable claim. Established unreachability SHALL be derived for R by sound transfer without assuming the obligation’s own premises; UNSAT(H) alone does not establish it.

Obligation completeness. The owning elaboration SHALL account for every applicable boundary rule and its actual participants independently of whether a ready proposition can be constructed. A missing participant or premise SHALL retain an unresolved obligation or a located admission failure, never silently remove the rule. Agreement between two projections of the same obligations does not establish this census, the truth of their common premises, or their correspondence to source behavior.

Identity and dependent code. These judgments SHALL extend the existing typed PSG obligations and their owning inference and settlement passes. Projections SHALL retain the same claim identity, proposition, premises and checking context. Changed supporting facts SHALL invalidate the affected discharge even when the claim’s declaration and semantic role remain unchanged. Code that consumes a discharge for representation selection or check removal SHALL depend on its identity and current validity; invalidation SHALL revoke that code’s eligibility even when its source region is unchanged. Preservation or rechecking at lowering remains required by Conformance §6.

Informative. If a copy uses length r - 1 and a destination extent of 1023, an upper bound alone is insufficient: its length rule includes 0 ≤ r - 1 ≤ 1023, together with initialized source and destination extents and the actual conversion semantics. Admitting r = 0 or r = -1 violates that lower bound, although both satisfy (r - 1) ≤ 1023. Assuming r ≥ 1 in a query does not establish that the source excludes those outcomes.

6. Examples

6.1 GTK Bindings

This example spells the native transport signatures. GtkExtern denotes an imported module of compiler-recognized extern declarations with their complete descriptors; it is a schematic module name, not a symbol lookup or a claim that a regenerated GTK library has passed acceptance. 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

// Entries from declared extern bindings; native contracts remain attached.
let private gtk_init_ptr : FnPtr<Option<CHandle<int>> -> Option<CHandle<CHandle<byte>>> -> unit> =
    FnPtr.ofExtern GtkExtern.gtk_init

let private gtk_window_new_ptr : FnPtr<int -> CHandle<GtkWindow>> =
    FnPtr.ofExtern GtkExtern.gtk_window_new

let private gtk_widget_show_all_ptr : FnPtr<CHandle<GtkWidget> -> unit> =
    FnPtr.ofExtern GtkExtern.gtk_widget_show_all

let private gtk_main_ptr : FnPtr<unit -> unit> =
    FnPtr.ofExtern GtkExtern.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. LibcExtern below is a schematic imported module containing compiler-recognized extern declarations and their descriptors. The private entries illustrate native carriers; they do not create those declarations, 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<CHandle<byte> -> int> =
    FnPtr.ofExtern LibcExtern.strlen

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

// free: accepts NULL (no-op)
let private free_ptr : FnPtr<Option<CHandle<unit>> -> unit> =
    FnPtr.ofExtern LibcExtern.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.ofExtern admits an existing extern declaration under its complete current ABI and code-lifetime contract; symbol-only FnPtr.fromSymbol is refused
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
10. Sharing memory with C or C++ code without copying SHALL establish all four §5.6 shared-memory obligations on the PSG before emission: bounded extent, compatible alignment and byte order, lifetime covering the foreign retention class, and access excluding conflicting use. Retained sharing SHALL keep the backing region and allocation live through all foreign, asynchronous and device access until admitted retirement
11. A matching layout supplies schema and byte-offset facts only and SHALL NOT suffice for zero-copy sharing, authorize dereferencing a CHandle<'T>, or authorize converting it to a Ptr<'T, 'Region, 'Access> or any interior pointer or reference