Memory Regions

Memory region types define where memory lives and how it behaves. They are intrinsic to Clef and guide code generation throughout the compilation pipeline.

Overview

Clef extends the type system with memory region information. Every pointer type carries region semantics that determine:

• Allocation strategy
• Access patterns (volatile, cached)
• Lifetime constraints
• Code generation decisions

Region Types

The following memory regions are defined:

Sram and Flash are also the static storage of the lifetime lattice: a value whose lifetime is the whole program (constructed once, held to program end, never freed) is placed in Sram when mutable or Flash when immutable, as a program-lifetime global rather than a heap allocation. A fixed-address Peripheral register is already a program-lifetime global of this kind; a program-lifetime closure, list, or record is the same, and lives in the same static storage. This is what lets a target without a heap still hold a value that outlives its constructing scope.

The lattice extends one rung past the process on targets that claim the Freestanding Substrate profile: Modular Blob Storage persists values that outlive a program run, and Namespace Storage layers names and history above it. Both are placed through the regions of this chapter — sealed records in non-volatile storage, working sets in bounded RAM — and both carry their durability as a coeffect committed at target binding.

Stack

Stack-allocated values have automatic lifetime bounded by their lexical scope.

let example () =
    // Fixed-size stack array; storage is allocated in the Stack region
    let buffer : array<byte, 1024, Stack> = [| 0uy; ... |]
    // A region-typed handle to the buffer's storage, valid until the function returns
    let handle : Ptr<byte, Stack, ReadWrite> = Ptr.ofArray buffer
    use handle

Properties:

• Thread-local storage
• Automatic cleanup at scope exit
• Size limits enforced by platform

Arena

Arena-allocated values are bulk-allocated and freed together.

Status (January 2026): Arena is implemented as a CCS (Clef Compiler Service) intrinsic type with compiler-provided operations.

Type Definition:

// Arena<[<Measure>] 'lifetime> - CCS intrinsic type
// Layout: NTUCompound(3) = { Base: index, Capacity: index, Position: index }
//   Base and Capacity are the arena's buffer as a memref<?xi8> view (base index into the declared
//   space, extent); Position is the bump cursor. No field is an address.
 

Current Implementation (Level 3 - Explicit):

// Create arena from a bounded stack array as backing memory
let arenaMem : array<byte, 4096, Stack> = [| 0uy; ... |]
let mutable arena = Arena.fromArray arenaMem  // capacity taken from the array bound

// Allocate from arena (note: byref parameter for mutation)
let buffer = Arena.alloc &arena 256  // Returns a Ptr<byte, Arena, ReadWrite> handle
let aligned = Arena.allocAligned &arena 64 16  // 64 bytes, 16-byte aligned

// Query and reset
let remaining = Arena.remaining arena
Arena.reset &arena  // Position back to the arena's floor (0, or the sentinel slot; see Floor below)
 

Arena Operations (CCS Intrinsics):

Lifetime Parameter: The 'lifetime measure parameter enables future lifetime tracking. Currently documentation-level; compiler enforcement planned.

Three Levels of Control (Lifetime Inference Principle):

1. Level 3 (Explicit): Full control via Arena.fromArray, Arena.alloc &arena (implemented)
2. Level 2 (Hints): arena { } computation expression (future)
3. Level 1 (Inferred): Escape analysis via inline expansion - see Inline Functions and Escape Analysis (implemented)

Properties:

• No individual deallocation
• O(1) bump allocation
• Cache-friendly locality
• Scope-bounded lifetime
• Backing memory comes from the stack, from static storage (Sram/Flash), or, where the target has one, from the heap. A target without a heap backs arenas with stack or static storage only.

The { Base, Capacity, Position } layout states the allocation discipline as checkable facts: every allocation advances Position by the requested (aligned) size, and Position never exceeds Capacity. An implementation’s allocation emission is subject to the preservation and diagnostic obligations over exactly these facts.

Floor. An arena that hosts nodes of a collection type (List Operations §5.2, Map Representation §2.2, Set Representation §2.2) carries the sentinel of that type at offset 0, copied from the type’s program-lifetime sentinel image when the arena is created. The arena’s floor is the size of that slot, taken as the largest sentinel slot among the node types the arena hosts; every sentinel image is all-zero (tag Empty is case 0, height is 0, links are 0, payload slots are zero), so one slot at offset 0 serves every hosted type. Position begins at the floor, alloc never returns an index below it, and reset returns Position to the floor, never to 0. These are literal facts of the arena’s saturated layout, and they are what the collection chapters’ VC-RO obligations rest on: every store into a node lies at or above the floor by construction, and no runtime index value need be reasoned about. An arena that hosts no such type has floor 0.

Peripheral

Peripheral regions represent memory-mapped I/O with volatile semantics.

let gpioReg : Ptr<uint32, Peripheral, ReadWrite> = Ptr.ofAddress 0x48000000UL

Properties:

• Volatile loads and stores
• No reordering by compiler or CPU
• Memory barriers as required
• Not cacheable

Sram

General-purpose RAM with standard memory semantics.

Properties:

• Cacheable
• Standard load/store semantics
• May be reordered by optimizer

Flash

Read-only program memory, typically for embedded systems.

let lookupTable : Ptr<int, Flash, ReadOnly> = ...

Properties:

• Read-only access enforced
• Link-time placement
• Cacheable

Region-Typed Pointers

Pointers carry region and access information in their type:

type Ptr<'T, 'Region, 'Access>

Examples:

Ptr<uint32, Peripheral, ReadWrite>  // GPIO register
Ptr<byte, Flash, ReadOnly>          // Constant data
Ptr<int, Stack, ReadWrite>          // Stack buffer
Ptr<float, Arena, ReadWrite>        // Arena-allocated array
 

Compile-Time Enforcement

Region mismatches are type errors:

// ERROR: Cannot assign Peripheral pointer to Stack pointer
let wrong : Ptr<int, Stack, ReadWrite> = peripheralPtr

Code Generation Effects

Lifetime Constraints

Lifetime verification in Clef is coeffect discipline carried on the Program Semantic Graph, with no ownership or borrowing annotations in the source language. The normative floor is in place: every value is classified against the four-point lifetime lattice by escape analysis (Closure Representation §3.3), placement follows the classification, a classification with no home on the selected target is diagnosed at compile time, and the classification is subject to the preservation and introduction obligations of Conformance §6.

The rules that remain to be specified are the lifetime orderings: that a region outlives every value placed in it, and that every use of a value falls within its region’s extent. These are orderings over the lattice, decidable facts stated and discharged as proof obligations that ride the PSG with the escape coeffect (Program Semantic Graph §14.3). A future revision of this chapter SHALL state the ordering rules and their obligation forms; the mechanism is fixed as coeffect-and-obligation discipline, and no ownership or borrowing vocabulary is planned.

Target Reachability

The region types of this chapter name storage a target provides, and the platform descriptor lists the regions each target has (Platform Bindings). A construct whose region the selected target does not provide SHALL be diagnosed at compile time when compiled for that target; reachability is carried as a lattice-family coeffect alongside escape classification (Grade Discipline §4.1).

On the JSIR pathway, no region of this chapter exists: the host garbage collector owns placement, every lifetime class of the lifetime lattice has a home, and Ptr, Arena, Mmio, and every region-typed construct SHALL be diagnosed as unavailable for the target (the CCS8030 pattern of Platform Bindings). The lifetime lattice itself still classifies every value at design time on that pathway; only the storage classes of this chapter are absent.

Grammar

region-type :=
    Stack
    Arena
    Peripheral
    Sram
    Flash

region-typed-ptr := Ptr < type , region-type , access-kind >