Platform Bindings and System Intrinsics

Platform bindings define the interface between Clef code and platform-specific operations. This chapter specifies the three-layer binding architecture used by CCS (Clef Compiler Service) and Composer.

Overview

Clef uses a three-layer architecture for platform operations:

This approach:

• Avoids BCL dependencies (System.Runtime.InteropServices)
• Enables compile-time platform specialization
• Provides type-safe syscall interfaces
• Separates intrinsic operations from external library bindings

Layer 1: CCS Intrinsics

CCS recognizes certain operations as intrinsic to the native type universe. These are recognized by module pattern - no declaration in user code is needed.

The Sys Module

The Sys module provides direct system call primitives:

module Sys =
    /// Write bytes to a file descriptor
    /// fd: file descriptor (0=stdin, 1=stdout, 2=stderr)
    /// buffer: bounded stack array holding the data
    /// count: number of bytes to write
    /// Returns: number of bytes written, or negative on error
    val write : fd:int -> buffer:array<byte, 'n, Stack> -> count:int -> int

    /// Read bytes from a file descriptor
    /// fd: file descriptor
    /// buffer: bounded stack array to receive the data
    /// maxCount: maximum bytes to read
    /// Returns: number of bytes read, or negative on error
    val read : fd:int -> buffer:array<byte, 'n, Stack> -> maxCount:int -> int

    /// Exit the process with the specified code
    /// This function never returns
    val exit : code:int -> 'T

The buffer parameter carries the bounded stack array whose bound the compiler knows, not a raw pointer. There is no nativeptr<byte> surface for an intrinsic argument. The interior mechanism that carries the buffer’s address to the target pathway is not user-denotable; source code names only the array.

Buffer and Register Surfaces

Layer 1 exposes no raw-pointer module. A buffer is a bounded stack array (array<byte, 'n, Stack>), whose bound the compiler carries so an intrinsic reads and writes within it without a denotable pointer. A memory-mapped register is the width-typed Mmio handle. A pointer returned by a C binding is the opaque CHandle<'T>, which is non-arithmetic and non-dereferenceable and exists only to be handed back across the boundary. The interior pointer mechanism is the flat closure. None of nativeptr<'T>, voidptr, nativeint-as-pointer, or a NativePtr.* operation is denotable in Clef source, at the Layer 1 boundary or anywhere else.

Intrinsic Recognition

CCS recognizes intrinsics by module path pattern during type checking. When code calls Sys.write, CCS:

1. Matches the module path Sys
2. Matches the member name write
3. Returns the intrinsic’s native type signature
4. Marks the call as SemanticKind.Intrinsic in the SemanticGraph

CCS/Baker settles the intrinsic’s demand, platform, storage and ABI obligations on the PSG. Alex witnesses the admitted portable form; Composer’s backend provides its target-specific implementation.

Platform-Specific Implementation

Composer’s backend realizes Sys intrinsics for each target platform from the declaration and ABI facts settled by CCS/Baker.

Linux x86-64

Syscall convention: rax=syscall number, rdi=arg1, rsi=arg2, rdx=arg3

Linux ARM64

macOS x86-64

Note: macOS x86-64 uses BSD syscall numbers with 0x2000000 offset.

macOS ARM64

Windows x86-64

Freestanding

For bare-metal targets, intrinsics may:

• Map to hardware registers
• Generate inline assembly
• Require target-specific configuration

JavaScript (JSIR Pathway)

The Sys intrinsics have no realization on the JSIR pathway: an isolate has no file descriptors, no syscalls, and no process to exit. A program that reaches a Sys intrinsic when compiled for this pathway SHALL be diagnosed with CCS8030 (platform intrinsic not available for target). Console output and every other host service on the managed substrate are host APIs reached through generated bindings (JavaScript Boundary Semantics §7), not Layer 1 intrinsics; termination belongs to the host, not to the program.

Layer 2: Binding Libraries

External library bindings (GTK, CMSIS, OpenGL, etc.) require rich semantic metadata that CCS cannot know intrinsically:

• Memory layouts and alignment
• Ownership semantics (managed, unmanaged, refcounted)
• Volatile access requirements
• Callback calling conventions
• Register mappings (for hardware peripherals)
• FFI calling conventions

The Quotation Solution

Clef quotations (<@ ... @>) are compile-time inspectable data structures, an intrinsic form of the language (Expressions, Quoted Expressions). Unlike regular code, which compiles to instructions, a quotation is elaborated into the program graph as data the compiler reads during compilation; it has no run-time value and is never evaluated.

This makes quotations the form for carrying binding metadata:

• Generated by Farscape from C/C++ headers
• Compiled with the program, as Clef source
• Read at compile time by CCS, structurally, by type name and field name
• Never executed at runtime, and never referenced from executed code (CCS8066)

Backend Independence

Generated binding source and the middle end SHALL describe boundary semantics independently of any backend dialect. Their opaque carriers, absence conversions, ABI declarations, resource obligations and source correspondence SHALL NOT embed LLVM dialect types, operations or expansion plans. The selected backend alone realizes an admitted contract in its target vocabulary. A library using HIP, MLIR-AIE or another non-LLVM vocabulary SHALL NOT require an LLVM representation in its binding or middle-end contract.

MMIO describes access semantics, not a target or backend selection. MCU and virtio unikernel pathways MAY realize the same admitted access intent through different target vocabularies. The presence of MMIO SHALL NOT select LLVM; the selected backend must provide its own realization or refuse the intent.

Alex retains structured, source-bound intent when target realization is needed; it SHALL report portable text as explicitly unavailable rather than fabricate text, omit an operation or reinterpret a carrier. Target-produced text remains a backend artifact. An unavailable code-content commitment SHALL NOT become an empty or constant reuse key. Quoted strings, foreign symbol names and comments that merely mention a backend are data, not dialect constructs.

Owned Nullable Return Contracts

An owned nullable return MAY be declared by a sibling <name>ResourceDescriptor : Expr<ResourceDescriptor> beside the extern <name> in the same module. This resource declaration is separate from its FunctionDescriptor; CallerOwns or CalleeOwns alone establishes no resource protocol. The resource quotation has no acquisition name or C-symbol field: CCS/Baker associates it with the exact sibling declaration and its body. Declarations sharing a C symbol, ABI or handle type SHALL remain distinct.

type ResourceRelease = { Binding: string; Parameter: int }
type ResourceProtocol = OwnedNullableReturn of ResourceRelease
type ResourceDescriptor = {
    Resource: ResourceProtocol
    Hypothesis: ExternalExecutionHypothesis
}

let mallocFirstResourceDescriptor : Expr<ResourceDescriptor> = <@
    { Resource = OwnedNullableReturn
          { Binding = "Storage.freeFirst"; Parameter = 0 }
      Hypothesis =
          { Identity = "storage-first"; Version = "1"; Source = "pilot declaration" } }
@>

Binding identifies the fully qualified Clef release declaration, not its C symbol. Parameter is its zero-based native receiving ordinal. This first protocol requires a single matching nonnull handle parameter at ordinal zero and a raw Void release result, with no other arguments or integer status convention. Its only permitted foreign operation is that exact release; foreign retention and ownership transfer are excluded.

Native null SHALL convert to None, creating no owned resource and permitting no release. A nonnull result SHALL convert to Some of a nonnull opaque CHandle<'T>. These are explicit boundary conversions at the selected target’s pointer width, not a reinterpretation of a generic interior Option (FFI Boundary §2.3). After a nonnull acquisition, source code SHALL explicitly pair the resource with the declared release on every admitted exit, including later failure exits. Release SHALL retire all affected aliases. The descriptor inserts no cleanup.

The identified, versioned external hypothesis states the foreign behavior; it does not prove the compiler’s conversion, cleanup or retirement obligations. CCS/Baker SHALL establish those obligations through nanopass elaboration and saturation with their actual source participants. Publication and Alex observe the settled facts. Missing contracts or unresolved obligations SHALL retain their refusal at commitment. Descriptor, hypothesis, target ABI or release support changes SHALL invalidate dependent evidence and any code that consumed it. This protocol grants no spatial access, loading authority, borrowed/static classification or broader resource operations.

How Quotation Binding Works

Step 1: Farscape Generates Binding Library

Farscape parses C/C++ headers and generates F# binding libraries:

// Generated by Farscape from gtk.h
module Gtk.Bindings

open BAREWire.Descriptors
open Memory

/// Type descriptor - quotation carries layout and semantics
let gtkWindowDescriptor: Expr<TypeDescriptor> = <@
    { TypeName = "GtkWindow"
      CName = "GtkWindow"
      Layout = { Size = 24un; Alignment = 8un }
      Ownership = Unmanaged
      RefCounted = true
      Destructor = Some "gtk_widget_destroy" }
@>

/// Function descriptor - quotation carries calling convention
let gtkWindowNewDescriptor: Expr<FunctionDescriptor> = <@
    { CName = "gtk_window_new"
      Parameters = [
          { Name = "type"; Type = I32; PassBy = Value }
      ]
      ReturnType = Handle gtkWindowDescriptor
      CallingConvention = CDecl
      OwnershipTransfer = CallerOwns }
@>

/// The callable function: the sibling declaration the descriptor describes
let windowNew (windowType: int) : CHandle<GtkWindow> =
    failwith "Binding placeholder"

Step 2: CCS Inspects Quotations at Compile Time

When CCS encounters a call to a binding function, it:

1. Recognizes the binding pattern by module structure
2. Associates the descriptor quotation with the exact sibling declaration it describes, by graph identity, as for resource descriptors above. Farscape emits descriptor bindings with the *Descriptor suffix.
3. Inspects quotation structure to extract metadata
4. Attaches metadata to SemanticGraph nodes

User code: let window = Gtk.windowNew 0
                ↓
CCS: "This calls Gtk.Bindings.windowNew"
                ↓
CCS: "Resolve the sibling descriptor declaration"
                ↓
CCS: Inspects <@ { CName = "gtk_window_new"; ... } @>
                ↓
SemanticGraph node gets:
  - FFI.CName = "gtk_window_new"
  - FFI.CallingConvention = CDecl
  - FFI.OwnershipTransfer = CallerOwns
  - MemoryRegion = Unmanaged

Step 3: Alex Uses Metadata for Code Generation

The metadata flows from SemanticGraph to Alex:

SemanticGraph node (with FFI metadata)
                ↓
Alex reads: "FFI call to gtk_window_new, CDecl, returns owned pointer"
                ↓
Alex emits the portable call node; a target pathway emits the target-specific call
with the correct ABI and ownership tracking (LLVM being one such pathway)

Active Patterns for Recognition

Binding libraries also provide active patterns for PSG traversal:

/// Active pattern for matching GTK window creation
let (|GtkWindowCreate|_|) (node: SemanticNode) =
    match node.Kind with
    | Application(funcNode, args) when
        funcNode.Symbol = Some "Gtk.Bindings.windowNew" ->
        Some { WindowType = extractArg args 0 }
    | _ -> None

/// Active pattern for matching GTK signal connection
let (|GtkSignalConnect|_|) (node: SemanticNode) =
    match node.Kind with
    | Application(funcNode, args) when
        funcNode.Symbol = Some "Gtk.Bindings.signalConnect" ->
        let widget = extractArg args 0
        let signal = extractArg args 1
        let callback = extractArg args 2
        Some { Widget = widget; Signal = signal; Callback = callback }
    | _ -> None

CCS/Baker uses these patterns while elaborating binding declarations and calls. It publishes the resolved binding identity, operands and boundary contract; Alex consumes those settled facts without recognizing library names or reconstructing a binding contract during emission.

Quotation Structure Requirements

Binding quotations must follow specific structure for CCS inspection:

/// Type descriptor quotation
type TypeDescriptor = {
    TypeName: string          // F# type name
    CName: string             // C/C++ type name
    Layout: LayoutInfo        // Size, alignment
    Ownership: OwnershipKind  // Managed | Unmanaged | RefCounted
    RefCounted: bool          // Uses reference counting
    Destructor: string option // Cleanup function name
}

/// Function descriptor quotation
type FunctionDescriptor = {
    CName: string                 // C function name
    Parameters: ParameterInfo[]   // Parameter types and passing
    ReturnType: TypeRef           // Return type reference
    CallingConvention: CallConv   // CDecl | StdCall | FastCall
    OwnershipTransfer: Transfer   // CallerOwns | CalleeOwns | Borrowed
}

/// Hardware register descriptor (for embedded)
type RegisterDescriptor = {
    Name: string              // Register name
    Address: usize            // Memory-mapped address (platform-word integer, as the Mmio handle carries it)
    AccessKind: AccessKind    // ReadOnly | WriteOnly | ReadWrite | Volatile
    ResetValue: uint32        // Value after reset
    Fields: FieldInfo[]       // Bit field definitions
}

/// Scoped callback declaration: the named operation invokes this parameter
/// within its own call and retires every use of it before returning
type ScopedCallbackDescriptor = {
    Binding: string           // Fully qualified binding whose operation takes the callback
    Parameter: string         // Its function-valued parameter
}

A binding whose operation invokes a supplied callback only within the operation’s own activation and retires every use and capture of it before returning MAY declare that contract with a ScopedCallbackDescriptor. The declaration states the binding’s obligation; CCS/Baker reads it structurally, records reliance on it as a library premise, checks the program’s uses of the callback and of the values the callback receives against the declared scope, and does not prove that the binding honours it (Conformance §6.1; Program Structure and Execution, Execution of Static Initializers).

Optional Callback Absence Contracts

An explicit promise that an extern parameter accepts absence of a callable entry MAY be declared by a sibling quoted CallbackAbsenceContract:

type CallbackAbsenceContract = {
    Binding: string
    Parameter: int
    Hypothesis: ExternalExecutionHypothesis
}

Binding identifies the exact fully qualified Clef extern declaration; Parameter is its original zero-based native receiving ordinal. Neither the C symbol nor the generated quotation’s value name establishes that identity. This promise is separate from callback activation. Its hypothesis SHALL have nonempty identity, version and source, with an identity distinct from the activation hypothesis at that ordinal. It is an external execution hypothesis, not a proof of foreign behavior, purity, functionhood or invocation count.

The first supported profile requires exactly one current CallbackInvocationContract at that declaration and ordinal, with a ScopedCallbackDescriptor limiting activation and retirement to the receiving call. This profile restriction does not change the meaning of absence. The absence promise supplies no lifetime, calling convention or target-conversion authority of its own.

Farscape expresses the promise through the optional absence_hypothesis = { identity, version, source } table on an existing callback_invocations item with scope = "during_call". There is no Boolean or default promise. Both header nonnull evidence and pilot nonnull evidence conflict with this promise and SHALL be diagnosed. For this explicit-promise profile, a header _Nullable alone does not supply the promise. When it is missing, acceptance of None remains Pending; Some gains no additional premise from absence-only evidence.

CCS/Baker SHALL discover the quotation through the existing module-level descriptor census within its retained source graph, using the resolved BAREWire.Descriptors.CallbackAbsenceContract declaration identity. It SHALL NOT introduce a second discovery walk or use a same-named unrelated record as authority. A source module outside the captured input closure is not made available by this declaration. Within the census, malformed, stray, duplicate or mismatched recognized quotations SHALL be diagnosed; a valid fresh rename of the quotation’s value binding remains admissible.

The exact quotation identity, content and versioned hypothesis SHALL participate in each dependent None conversion’s account. Changing or withdrawing that support invalidates the dependent evidence. Absence-only support SHALL remain separate from the Some conversion account. A fresh valid quotation does not authorize replay of evidence issued for an earlier quotation. This contract establishes no durable proof-reuse mechanism.

Native absence conversion still requires its own source and selected-target obligation under FFI Boundary §4. An inhabited interior FnPtr is never null, and the interior Option remains an ordinary tagged value.

Why Quotations, Not Attributes?

Quotations can express:

• Nested structures (layouts containing fields)
• References to other types (pointer to TypeDescriptor)
• Complex expressions (computed offsets, conditional layouts)
• All without runtime overhead

Layer 3: User Code

User code uses intrinsics and binding libraries. It does NOT declare platform bindings.

Correct Usage Pattern

// Console module - uses CCS intrinsics directly
module Console

let inline write (s: string) : unit =
    // s.Bytes is the string's bounded backing array; no raw pointer is named
    Sys.write 1 s.Bytes s.Length |> ignore

let inline writeln (s: string) : unit =
    write s
    let nl : array<byte, 1, Stack> = [| 0x0Auy |]
    Sys.write 1 nl 1 |> ignore

Invalid Binding Stubs

Platform bindings SHALL NOT use BCL stubs:

// WRONG - Do not declare platform bindings with BCL stubs
module Platform.Bindings =
    let writeBytes fd buffer count : int =
        Unchecked.defaultof<int>  // BCL dependency!
 

This pattern creates BCL dependencies and does not provide a platform binding contract.

Standard File Descriptors

Standard file descriptors on Unix-like systems:

Intrinsic Constraints

CCS intrinsics have restrictions:

1. No closures: Intrinsics cannot capture environment
2. Primitive or sanctioned-handle types only: Arguments and returns must be primitive types, a bounded stack array, the Mmio register handle, or a CHandle<'T>; there is no raw-pointer argument type
3. No exceptions: Errors returned via return values
4. No dynamic allocation: Intrinsics do not allocate on a heap. A buffer they operate on is a scope-bounded stack array or program-lifetime static storage, per the lifetime lattice; an intrinsic never introduces a genuinely-dynamic allocation, so it remains usable on a no-heap freestanding target
5. No currying: Intrinsics must be called with all arguments

Diagnostics

Platform Descriptor

The Platform Descriptor is a quotation-based structure that defines platform-specific characteristics. CCS/Baker reads it from Fidelity.Platform and settles the required platform facts, widths, representations and boundary contracts on the PSG. Alex observes that publication; Composer’s backend realizes the admitted form for the selected target.

The descriptor is a quotation and stays one: the record inside it is typed, while the facts it is assembled from (vendor documents, board packs, project files) are stringly typed or not typed at all, and the quotation is what carries the type over them. The compiler never evaluates the quotation. At saturation it reads the typed record structurally, by type name and field name, into the platform context: the width dimensions by their declared names and the representations the target offers. Every width or representation a program needs is answered from that declaration and never defaulted (the project file carries no width; a word_size key is reported as CCS8205 and not read). A seal spelled by name (int32, float64) resolves to the representation of that name; a seal named through a dimension (int, nativeint) resolves to the offered representation of its family at the dimension’s declared width, whatever the descriptor names it. A site the declaration does not answer is CCS8203 (undeclared dimension) or CCS8204 (unoffered representation). A defect of the declaration itself is reported at the declaration, never at a program site: CCS8206 (an element the compiler cannot read), CCS8207 (a tag outside its vocabulary, a width of no bits, a name declared twice, a Register width disagreeing with the word size), CCS8208 (a second description of one form among the binding’s sources). See Error Handling.

Informative. The Building Bulletproof eBPF Programs design orientation applies this descriptor discipline to the Linux kernel’s programmable surface, where hooks, helpers, and verifier budgets fill the same record vocabulary.

Structure

type PlatformDescriptor = {
    Architecture: Architecture          // X86_64, ARM64, RISCV64, etc.
    OperatingSystem: OperatingSystem    // Linux, Windows, MacOS, BareMetal
    Widths: WidthDeclaration list         // { Name = "Pointer"; Bits = 64 }, { Name = "Register"; Bits = 64 }, ...
    Representations: Representation list  // every numeric representation the target offers
    Endianness: Endianness              // Little or Big
    TypeLayouts: Map<string, TypeLayout>  // Type sizes and alignments
    SyscallConvention: SyscallConvention  // Syscall ABI
    MemoryRegions: MemoryRegion list      // Per-target; e.g. Stack, Text, Data, and Heap only where the target has an allocator
    FreestandingStartup: FreestandingStartup option  // Entry point for freestanding mode
}

/// A width dimension the target declares by name; the language's `WidthDimension of name: string`
/// ([NTU Types](ntu-types.md)) names it, and the compiler's context keys the declared bits by that name.
type WidthDeclaration = { Name: string; Bits: int }

/// A numeric representation the target offers ([Numeric Selection §7, §9.6](numeric-selection.md)).
type Representation = {
    Name: string           // "int32", "float64", "posit32", ...
    Capability: Capability // native | emulated | unavailable
    Family: Family         // int | uint | ieee | posit | fixed
    Bits: int
    MinMagnitude: string   // least finite value, exact decimal text
    MaxMagnitude: string   // greatest finite value, exact decimal text
    Boundary: Boundary     // wrap | saturate | exact
}

MemoryRegions is per-target. A hosted target lists Stack, Heap, Text, Data. A freestanding target with no allocator has no Heap: it lists Stack for scope-bounded values and static storage (.bss-class Sram/Flash) for program-lifetime values. A value that would classify as genuinely dynamic on such a target is a compile-time lifetime error, not a silent heap allocation. See the four-point lifetime lattice in closure-representation.md §3.3.

Freestanding Startup

For freestanding builds (no libc), the platform descriptor includes startup information:

type FreestandingStartup =
    /// Hosted freestanding ELF (Linux, no libc): a named entry symbol the linker
    /// points at, and a numbered exit syscall. "_start"/60 is this convention, not
    /// a universal freestanding one.
    | HostedElf of EntrySymbol: string * ExitSyscall: int64
    /// Bare-metal M33: control arrives at the reset vector, there is no
    /// _start symbol, no linker entry flag, no argv, and no syscall. Exit is a halt.
    | ResetVector of ResetHandler: string

The startup shape is per-target. _start plus a numbered exit syscall is the hosted-ELF freestanding convention; a bare-metal target has neither.

When output_kind = "freestanding" is specified in the project file for a hosted-ELF target, the compiler:

1. Generates a _start wrapper function
2. _start creates an empty string array, calls the F# main, and calls Sys.exit
3. Links with -Wl,-e,_start to set the entry point

For a bare-metal M33 target the compiler instead:

1. Emits the reset handler as the reset-vector entry (no _start symbol, no linker entry flag)
2. The reset handler calls the F# main with no argv (arguments do not exist)
3. Return from main is a halt (a wfi/spin), not an exit syscall

Console Mode

For console builds (with libc), no special entry point handling is needed:

• libc provides _start which initializes the runtime and calls main
• The F# main function is emitted with C-compatible signature
• The F# type array<string> -> int maps to the platform C ABI

Linux x86-64 Example (hosted ELF)

The SyscallConvention and FreestandingStartup below are the hosted-ELF freestanding shape: SysV argument registers, a _start entry symbol, and a numbered exit syscall. These belong to this target, not to freestanding mode in general (the M33 example that follows has none of them).

let platform: Expr<PlatformDescriptor> = <@
    { Architecture = X86_64
      OperatingSystem = Linux
      Widths = [ { Name = "Pointer"; Bits = 64 }; { Name = "Register"; Bits = 64 } ]
      Representations =
        [ { Name = "int32"; Capability = Native; Family = Int; Bits = 32
            MinMagnitude = "-2147483648"; MaxMagnitude = "2147483647"; Boundary = Wrap }
          { Name = "int64"; Capability = Native; Family = Int; Bits = 64
            MinMagnitude = "-9223372036854775808"; MaxMagnitude = "9223372036854775807"; Boundary = Wrap }
          { Name = "posit32"; Capability = Emulated; Family = Posit; Bits = 32
            MinMagnitude = "-1329227995784915872903807060280344576"; MaxMagnitude = "1329227995784915872903807060280344576"; Boundary = Saturate }
          (* every other representation the target offers, each with its capability, exact range and boundary *) ]
      Endianness = Little
      TypeLayouts = (* ... *)
      SyscallConvention =
        { CallingConvention = SysV_AMD64
          ArgRegisters = [| RDI; RSI; RDX; R10; R8; R9 |]
          ReturnRegister = RAX
          SyscallNumberRegister = RAX
          SyscallInstruction = Syscall }
      MemoryRegions = (* ... *)
      FreestandingStartup = Some (HostedElf ("_start", 60L))
    }
@>

Bare-Metal M33 Example (reset-vector entry)

The bare-metal Cortex-M33 target has no syscall ABI and no _start. Pointer is the 4-byte platform word, there is no Heap region, and startup is the reset vector.

let platform: Expr<PlatformDescriptor> = <@
    { Architecture = ARM_Thumbv8m
      OperatingSystem = BareMetal
      Widths = [ { Name = "Pointer"; Bits = 32 }; { Name = "Register"; Bits = 32 } ]
      Representations =
        [ { Name = "int32"; Capability = Native; Family = Int; Bits = 32
            MinMagnitude = "-2147483648"; MaxMagnitude = "2147483647"; Boundary = Wrap }
          (* the integer representations the core offers; a float only where the FPU is declared *) ]
      Endianness = Little
      TypeLayouts = (* ... *)
      SyscallConvention = NoSyscalls
      MemoryRegions = (* Stack + static Flash/Sram; no Heap *)
      FreestandingStartup = Some (ResetVector "Reset_Handler")
    }
@>

Managed-Substrate Descriptor (JSIR Pathway)

This subsection binds implementations claiming the JavaScript Substrate profile (Conformance §7).

The record vocabulary of PlatformDescriptor presumes an instruction-set target: an architecture, a syscall convention, memory regions, a startup symbol. None of these has a value for the JavaScript isolate the JSIR pathway targets, and an implementation SHALL NOT fabricate them. The JSIR pathway’s target SHALL instead be described by a managed-substrate descriptor recording, at minimum:

1. the host environment class (a service-worker isolate, a browser, a server-side JavaScript runtime);
2. the module system and export conventions that form the entry contract (the entry-point modes of Program Structure and Execution);
3. the host API surface that bindings are generated against, and its version (JavaScript Boundary Semantics §7); and
4. the wide-integer realization (Width Inference §8).

The managed-substrate capability requirements in Platform Predicates §6 require a consumer of these descriptor facts.

Compile-Time Resolution

The platform descriptor is inspected at compile time:

1. CCS reads the platform descriptor from Fidelity.Platform
2. For freestanding mode, Intrinsic Elaboration generates the _start wrapper
3. The wrapper uses Sys.emptyStringArray and Sys.exit intrinsics
4. Alex emits portable dialects (func, scf, arith, memref, index), committing to no target; a target pathway lowers them and supplies the entry glue. On the hosted x86-64 pathway that glue is an _start symbol the linker points at via -Wl,-e,_start; the bare-metal M33 pathway has no linker entry flag and no _start (control arrives at the reset vector).

The F# code author writes idiomatic F# (main: string[] -> int); the compiler handles entry point generation based on the platform and output mode

Program-Lifetime Spaces

For each numeric representation it offers, a PlatformDescriptor SHALL declare its capability (native, emulated, or unavailable; Numeric Selection §7) and its boundary semantics (wrap, saturate, or exact; Numeric Selection §9); the compiler reads both and declares neither. Among its MemoryRegions, a PlatformDescriptor SHALL designate by name exactly one immutable program-lifetime space and at most one mutable program-lifetime space. These are the spaces the representation chapters cite when a value is placed at the program-lifetime point of the lifetime lattice (Closure Representation §3.3): the sentinel image of an empty collection, a string literal, a program-lifetime closure environment. On an ELF target they are the rodata and data sections; on an MCU the flash and SRAM regions; on a GPU constant memory (and, where the target has one, a writable global segment); on an FPGA initialised BRAM. The role is declared, not inferred: the descriptor names the region, and a Resides edge (Program Hypergraph §6) cites that name as the obligation’s authority.

An implementation SHALL NOT fabricate a space the descriptor does not declare; this is the two-sided preservation obligation of Conformance §6. A program-lifetime value whose required space the selected descriptor does not declare is a compile-time error, not a fallback placement. A managed-substrate descriptor (the JavaScript Substrate profile) declares no memory spaces; there, program-lifetime values are realised by the host value model under the carrier-realisation rule of Backend Lowering Architecture §4.5, and the Resides obligation is discharged by that profile’s declaration.