synplexum/spec.md

# Compiler Spec: L3 → L0

*A four-layer compiler for ML training pipelines, from intent to bare metal.*

Each layer is a closed DSL with finite forms. Each has its own IR suited to the decisions made at that level. Optimization happens *between* layers during lowering and *within* layers as IR→IR rewrites. Never at the DSL surface.

Lowering between layers is **search**: enumerate valid candidates at the target layer, score them, pick the best. If search is slow, the representation is wrong.

```
┌─────────────────────────────────────────────┐
│  L3 Spec          what you want             │
├───────────────── search ────────────────────┤
│  L2 Method        how, algorithmically      │
├───────────────── search ────────────────────┤
│  L1 Placement     where, on what            │
├───────────────── emit ──────────────────────┤
│  L0 Machine       explicit execution        │
├─────────────────────────────────────────────┤
│  Codegen          PTX / LLVM IR / x86 / ... │
└─────────────────────────────────────────────┘
        ↕ rewrites within each layer
```

---

## Zen

- Read little; write little
- Correctness via DSL model, not assertions
- Every stage as simple as possible; all mutations checkable
- Unbounded execution = specification error
- Optimize between stages, closer to machine; not at DSL level
- Never sacrifice performance for correctness; change the representation
- Specify via properties: liveness, safety, consistency, resource bounds

The last point is structural. Every verification table in this document classifies its checks under exactly these four property kinds. If a check doesn't fit one of them, it doesn't belong.

### Property Definitions

**Safety** — references resolve, types match, nothing dangling. *"You will not read garbage."*

**Consistency** — declared constraints agree with each other and with structure. *"Your spec doesn't contradict itself."*

**Liveness** — every resource produced is consumed; every buffer freed; no dead allocations. *"Nothing is wasted."*

**Resource bound** — memory, compute, time, space are all finite and known. *"You will not run forever or exhaust the machine."*

### Verification Without Solvers

The restricted DSL makes each check a specific algorithm. Conservation is a graph walk. Separation is set disjointness. Boundedness is constant arithmetic. If the DSL allowed recursion, unbounded loops, or dynamic allocation, we'd need SAT solvers. Because it doesn't, we don't.

---

## L3: Spec

### Purpose

Declare *what* you want. No algorithms, no hardware, no shapes beyond the data itself. This is a contract that all lower layers must satisfy.

### DSL Forms

```
data <n> {
    <field> : <domain>
    ...
}

model <n> {
    in:         <data_ref>
    out:        <domain>
    properties: [<constraint>, ...]
}

loss <n> {
    <term_name> : <loss_kind>(<args>), weight: <float>
    ...
    combine: <combinator>
}

goal: minimize(<loss_ref>) | maximize(<ref>) | pareto([<refs>])
```

### Domain Types

```
tensor(dtype, shape)        fixed shape
sequence(domain, max_len)   variable-length, bounded
table(col: domain, ...)     tabular
dist(n)                     probability distribution over n classes
scalar(dtype)               single value
```

### Model Constraints

These are not implementations. They bound what L2 may produce.

```
depth(n)                    max composed stages
width(n)                    max hidden dimension
causal                      output_t depends only on input_≤t
autoregressive              output is fed back as input
equivariant(group)          symmetry constraint
param_budget(n)             max parameter count
latency_budget(ms)          max forward pass time (needs L1 info)
```

### Loss Kinds

```
divergence(predicted, target)           ce, kl, etc. (choice is L2)
norm(target, p)                         Lp on params or activations
constraint(predicate)                   hard constraint → penalty
reconstruction(input, decoded)          autoencoders
contrastive(anchor, positive, negative) representation learning
custom(name, reads: [refs])             escape hatch, user-defined
```

### IR

```
L3_IR = {
    data:   Map<Name, DataDecl>
    models: Map<Name, ModelDecl>
    losses: Map<Name, LossDecl>
    goal:   Goal
    hints:  Map<Path, EscapeHatch>
}
```

All refs resolved. All domains concrete. No optionals. A total description.

### Verification

| Property       | Check                  | Catches                                                   |
|----------------|------------------------|-----------------------------------------------------------|
| Safety         | Ref resolution         | Dangling references to data fields, model outputs         |
| Consistency    | Domain compatibility   | Model input domain ≠ data field domain                    |
| Safety         | Loss signature         | Loss term reads something that doesn't exist              |
| Consistency    | Constraint agreement   | `depth(2)` + `autoregressive` on feedforward output       |
| Resource bound | Finiteness             | Everything bounded, no recursion at this level            |

All checks decidable. All linear in program size.

### Optimization

**None.** L3 is a spec. You don't optimize a spec. You may *simplify* it — merge redundant loss terms, canonicalize domains — but no semantic changes.

### Trace — MNIST at L3

```
data mnist {
    images : tensor(f32, [28, 28])
    labels : tensor(u8, [1])
}

model classify {
    in:  mnist.images
    out: dist(10)
    properties: [depth(3), width(512), param_budget(500K)]
}

loss objective {
    ce:     divergence(classify.out, mnist.labels), weight: 1.0
    sparse: norm(classify.params, p=1),             weight: 1e-4
    combine: weighted_sum
}

goal: minimize(objective)
```

This is the entire program. Everything below exists to make it run.

---

## L3 → L2 Lowering

Given an L3 spec, enumerate valid L2 programs and pick the best.

The search space is combinatorial over (sample) × (architecture) × (backward) × (update). Architecture is the big one — it's a DAG construction problem. The search is structured, not brute force:

From `depth(3)` + `sequential`: 3-layer chain. Width search over powers-of-2 up to `width(n)`. If `causal`, only causal attention. If `autoregressive`, add feedback edges. Backward filtered by architecture compatibility. Update mostly independent. Sample constrained by data domain.

Cost model scores without lowering to L1: param count, FLOPs per step, memory high-water mark, known convergence priors.

If search produces >10K candidates: **representation too loose.** Add constraints at L3 or tighten the enumeration grammar.

---

## L2: Method

### Purpose

Choose *how* to achieve the spec. Algorithms, architecture, training strategy. Still no hardware, no memory, no scheduling.

### DSL Forms

```
methods for <model_ref> {
    sample:   <sample_method>
    infer:    <infer_method>
    backward: <backward_method>
    update:   <update_method>
}
```

#### Sample Methods

```
epoch_shuffle(batch: n, drop_last: bool)
stream_window(window: n, stride: n)
curriculum([{ filter: <pred>, duration: n_steps }, ...])
replay(buffer: n, priority: <kind>)
distributed_shard(shards: n, method: <inner>)
```

#### Infer Methods (Architecture)

```
sequential([<layer>, ...])
residual([<block>, ...])
diffusion_chain(steps: n, noise: <schedule>, denoiser: <infer>)
recurrent(cell: <infer>, steps: n | until(<pred>))
graph(nodes: <infer>, edges: <adjacency>)
mixture(experts: [<infer>], gate: <infer>)
```

#### Layer Primitives

```
linear(in, out)
conv(in_ch, out_ch, kernel, stride, padding)
attn(heads, dim, causal: bool)
norm(kind: layer | group(n) | rms)
act(fn: relu | gelu | silu | swish)
embed(vocab, dim)
pool(kind: avg | max, kernel)
dropout(p)                                training only
```

#### Backward Methods

```
autodiff(mode: reverse | forward, checkpoint: [<layer_ref>])
evolution(pop: n, sigma: f, selection: <kind>)
dfa(feedback_dim: n)
reinforce(baseline: <kind>)
straight_through(estimator: <kind>)
zeroth_order(samples: n, sigma: f)
hybrid(primary: <backward>, aux: <backward>, blend: <schedule>)
```

`autodiff` is an L2 declaration. L2→L1 lowering expands it into an explicit backward DAG in the tensor graph. At L1 and below, forward and backward are both explicit — no compiler magic.

#### Update Methods

```
sgd(lr)
adam(lr, beta1, beta2, eps)
muon(lr, ns_steps)
lion(lr, beta1, beta2)
schedule(warmup: n, decay: <kind>, inner: <update>)
gradient_clip(max_norm: f, inner: <update>)
ema(decay: f, inner: <update>)
```

### IR

```
L2_IR = {
    sample:   SampleNode
    infer:    InferGraph              DAG of layer nodes
    backward: BackwardDecl
    update:   UpdateChain
    shapes:   Map<NodeId, Shape>     propagated during verification
    hints:    Map<Path, EscapeHatch>
}
```

The InferGraph is a DAG, not a sequence. `sequential` and `residual` are sugar that lower into the DAG form. This makes fusion and rewrite uniform.

**Key principle:** `recurrent(... steps: n)` is finite. `recurrent(... until(pred))` is a specification error unless `pred` is proven terminating with a maximum bound. We do not allow unbounded execution.

### Verification

| Property       | Check                    | Catches                                                |
|----------------|--------------------------|--------------------------------------------------------|
| Consistency    | Shape propagation        | Mismatched shapes on infer DAG edges                   |
| Consistency    | Spec constraint check    | depth, width, param_budget violated                    |
| Consistency    | Backward compatibility   | Backward method can't handle infer graph structure     |
| Consistency    | Update shape match       | Update produces params of wrong shape                  |
| Consistency    | Sample/data match        | Batch shape inconsistent with data domains             |
| Resource bound | Finiteness               | DAG is acyclic (recurrent unrolled to fixed depth)     |
| Resource bound | Resource estimation      | Rough FLOPs, memory — feeds L1 search cost model       |

### Optimization (IR→IR rewrites)

Semantics-preserving transformations on L2 IR: layer fusion (`linear → act` becomes `fused_linear_act`), redundant norm elimination, checkpoint selection for memory/compute tradeoff, architecture search pruning of dominated candidates.

### Trace — MNIST at L2

```
methods for classify {
    sample:   epoch_shuffle(batch: 128)

    infer: sequential [
        linear(784, 256), norm(layer), gelu,
        linear(256, 256), norm(layer), gelu,
        linear(256, 10),  softmax
    ]

    backward: autodiff(mode: reverse)
    update:   schedule(warmup: 1000, decay: cosine,
                       inner: adam(lr: 3e-4))
}
```

Search chose this from L3 constraints: 3-layer sequential (from `depth(3)`), widths 256 (under `width(512)`), ~200K params (under `param_budget(500K)`). `softmax` output satisfies `dist(10)`.

---

## L2 → L1 Lowering

Given an L2 method and a hardware description, produce a valid L1 placement. Search decides: which compute goes on which node, how to partition across accelerators, pipeline depth, where to stage data, whether to fuse or split stages.

Cost model uses hardware specs: transfer time = data_size / bandwidth, compute time = FLOPs / throughput, memory pressure = peak live tensors, pipeline bubble ratio = (depth − 1) / (depth × stages).

If placement search explodes, either the hardware description is too ambiguous or the L2 method has too many equivalent decompositions.

Three things happen during this lowering that don't happen at other boundaries:

1. **Backward expansion.** If L2 declares `autodiff(mode: reverse)`, the lowering derives the backward pass and writes it as explicit tensor ops in the L1 tensor graph. At L1, no operation is implicit.

2. **Update materialization.** L2's `adam(lr, beta1, beta2, eps)` becomes an explicit actor handler with tensor arithmetic at L1.

3. **Data binding.** L3's abstract data declarations gain physical storage locations (`@ ssd_0, path: "..."`).

---

## L1: Placement

### Purpose

Map the L2 method onto specific hardware. This is the layer where the systems-level DSL lives. It answers two questions: **where** does each computation live (topology + placement), and **when** does it execute (schedule + dataflow).

Six declaration forms: system, data, actor, stage, tensor_graph, pipeline. Plus a schedule block.

### DSL Forms — Topology

```
system <n> {
    node <id> { kind: <storage|memory|compute>, <properties> }
    ...
    edges {
        <id> -> <id>  : bandwidth <rate>      // unidirectional
        <id> <-> <id> : bandwidth <rate>      // bidirectional
    }
}
```

Node kinds:
- `storage` — persistent (SSD, disk). Source of data.
- `memory` — volatile (RAM, HBM). Has `capacity`.
- `compute` — processing (CPU, GPU). Has `isa`, and optionally `vram`, `cores`, `sm`, etc.

### DSL Forms — Data Sources

```
data <n> {
    <field> : <domain> @ <storage_node>, path: <string>
    ...
}
```

Binds L3's abstract data declarations to physical storage. The `@` annotation names the topology node where the data lives at rest.

### DSL Forms — Actors

Actors own mutable state. They process messages one at a time — serialized, no concurrent access to their state.

```
actor <n> on <node> {
    state {
        <field> : <type>, <init>
        ...
    }

    window <n> : (<fields>)
        readers(<stage_or_graph_refs>)

    on <MessageType>(<args>) {
        <update logic>
    }
}
```

**Windows** grant read-only access to actor state from stages or tensor graphs. The actor's message handler is the only writer. Safety requires that readers and writers never execute concurrently — enforced by data dependency chains within a step and actor serialization across steps.

### DSL Forms — Stages

Stages are stateless dataflow processors. They receive buffers, do work, and forward results. Every buffer received must be consumed exactly once — forwarded or freed. No exceptions.

```
stage <n> on <node> {
    reads: <refs>                          // optional window reads

    fn process(<args>) -> forward(<target>, <outputs>)
                        | Drop(<buf>) {
        <body>
    }
}
```

Buffer types carry region provenance: `buf<ram_0>`, `buf<gpu_0>`. Every forwarding site is checked: target exists, arity matches, types match, region provenance matches the target's placement.

### DSL Forms — Tensor Graphs

Lazy DAGs of primitive tensor ops. Run on accelerators. No control flow, no mutation, no side effects — pure compute.

```
tensor_graph <n> on <node> {
    reads: <window_refs>

    fn compute(<inputs>) -> (<outputs>) {
        let t0 = tensor_matmul(x, w)
        let t1 = tensor_add(t0, tensor_broadcast(b, shape))
        ...
        return (loss, gw, gb)
    }
}
```

The `reads` clause grants access to actor state via a window — same mechanism as stages. The body is a sequence of `let` bindings over primitive tensor ops. No autodiff — both forward and backward are explicit. Movement ops (reshape, permute, broadcast) are free — metadata only.

**Primitive tensor ops:**

```
tensor_matmul(a, b)              matrix multiply
tensor_add(a, b)                 elementwise add
tensor_sub(a, b)                 elementwise subtract
tensor_mul(a, b)                 elementwise multiply
tensor_scale(a, scalar)          scalar multiply
tensor_broadcast(a, shape)       expand dimensions
tensor_transpose(a)              transpose
tensor_reduce_mean(a)            reduce mean (all axes)
tensor_reduce_sum(a, axis: n)    reduce sum on axis
tensor_const(v)                  scalar constant
```

### DSL Forms — Pipelines

Ordered chains of stages and tensor graphs.

```
pipeline <n> {
    <stage_or_graph> -> <stage_or_graph> -> ...
}
```

### DSL Forms — Schedule

```
schedule {
    pipelines: [<refs>]
    actors:    [<refs>]
    pipeline_depth: <n>
}
```

No explicit phases. Execution order is inferred from `forward()` edges — the dependency DAG. `pipeline_depth` controls overlap: at depth 2, step N+1's early stages can overlap with step N's late stages. The actor is the serialization fence between steps.

### IR

```
L1_IR = {
    topology:      Graph<NodeId, Edge>           hardware graph
    data_sources:  Map<Name, DataDecl>
    placement:     Map<L2_NodeId, HW_NodeId>     where each computation lives
    actors:        Map<Name, ActorDecl>
    stages:        Map<Name, StageDecl>
    tensor_graphs: Map<Name, TensorDAG>          lazy compute DAGs
    pipelines:     [Pipeline]                    ordered stage/graph chains
    schedule:      ScheduleDecl
    hints:         Map<Path, EscapeHatch>
}
```

Every cross-reference is resolved during parsing. `demux` reading `connection_manager.routes` becomes a pointer within the tree. If a name is unresolved, the parser rejects. If a syntax rule is violated, the parser rejects. Semantic validity is the verifier's job.

### Verification — Structural (Phase 1)

Reads the IR. Does **not** transform it. If it also rewrote things, we'd need to verify the verifier's transformations. Keeping it read-only keeps it auditable.

| Property       | Check                       | Catches                                                       |
|----------------|-----------------------------|---------------------------------------------------------------|
| Safety         | Topology consistency        | Edges reference nonexistent nodes; no path for transfers      |
| Safety         | Ref resolution              | Dangling window reads, missing forward targets                |
| Safety         | Forwarding signatures       | Arity mismatch, type mismatch, region provenance mismatch    |
| Safety         | Window separation           | Reader and writer may execute concurrently                    |
| Consistency    | Tensor shape propagation    | Mismatched shapes in tensor graph DAG                         |
| Consistency    | Region provenance           | `buf<ram_0>` forwarded to a `gpu_0` tensor graph              |
| Liveness       | Buffer conservation         | Buffer allocated but never freed or forwarded                 |
| Liveness       | Tensor reachability         | DAG node neither consumed nor named as output                 |
| Resource bound | Persistent memory bounded   | Actor state exceeds node capacity                             |
| Resource bound | DAG finiteness              | Tensor graph or pipeline contains a cycle                     |

**Conservation check per stage:** build the control flow graph, walk every path tracking live `Buffer` resources. Every path must end with an empty live set. If any path ends with a live buffer, the verifier rejects with the specific path and buffer name.

**Separation check:** within a step, the data dependency chain ensures the window reader (tensor graph) completes before the writer (actor handler) fires. At `pipeline_depth > 1`, cross-step safety requires that step N's actor update completes before step N+1's reader begins — the actor serializes this.

### Optimization (IR→IR rewrites)

Stage fusion (merge adjacent stages on same node), pipeline rebalancing, tensor graph rewriting (fuse ops, eliminate copies), communication optimization (overlap compute and transfer), parallelism mapping (data/tensor/pipeline parallel as topology + placement rewrites).

### Trace — MNIST at L1 (abbreviated)

```
system single_gpu {
    node ssd_0  { kind: storage }
    node ram_0  { kind: memory, capacity: 32GB }
    node cpu_0  { kind: compute, isa: x86_64, cores: 8 }
    node gpu_0  { kind: compute, isa: cuda, vram: 24GB, sm: 84 }

    edges {
        ssd_0 -> ram_0  : bandwidth 2GB/s
        ram_0 <-> cpu_0 : bandwidth 50GB/s
        cpu_0 <-> gpu_0 : bandwidth 32GB/s
    }
}

actor model_state on gpu_0 {
    state {
        w : tensor(f32, [784, 256]), init: kaiming
        b : tensor(f32, [256]),      init: zeros
    }

    window weights : (w, b)
        readers(forward_backward)

    on GradUpdate(gw, gb) {
        let lr = 3e-4
        w = tensor_sub(w, tensor_scale(gw, lr))
        b = tensor_sub(b, tensor_scale(gb, lr))
    }
}

stage load_data on cpu_0 { ... }
stage transfer_to_gpu on cpu_0 { ... }
tensor_graph forward_backward on gpu_0 {
    reads: model_state.weights
    fn compute(x, y) -> (loss, gw, gb) { ... }
}
stage transfer_grads on cpu_0 { ... }

pipeline train { load_data -> transfer_to_gpu -> forward_backward }
pipeline grad_return { transfer_grads }

schedule {
    pipelines: [train, grad_return]
    actors: [model_state]
    pipeline_depth: 2
}
```

---

## L1 → L0 Lowering

Not search — **emission.** The verified L1 IR is lowered into L0 through three compiler passes, then split into two code paths.

### Pass 1: Memory Planning

Compiler-derived, not user-declared. Three strategies selected by lifetime analysis:

| Strategy       | Use                      | Lifetime                         |
|----------------|--------------------------|----------------------------------|
| **Persistent** | Actor state (w, b)       | Init → program end               |
| **Arena**      | Tensor intermediates     | Graph start → graph end, bulk reset |
| **Pool**       | Transfer staging buffers | alloc → free, freelist           |

### Pass 2: Stream Inference

Each step's GPU work gets a stream. At `pipeline_depth: N`, N streams. Cross-stream dependencies become sync events.

```
stream_0: step N   → K0, K1, ..., sgd_kernel
stream_1: step N+1 → K0, K1, ..., sgd_kernel

sync: event recorded after sgd_kernel on stream_0
      waited before K0 on stream_1
```

### Pass 3: Kernel Scheduling & Fusion

Tensor graph DAG nodes are grouped into kernels. Fusion rules: elementwise ops fuse freely; reduction forces a kernel boundary; different iteration spaces cannot fuse.

### Dual Emission

The verified L1 IR splits into two code paths:

**Path A — Control.** Stages and actor handlers emit to **Control IR** (Machine IR). This is the CPU-side orchestration: data loading, transfers, message dispatch, pipeline coordination.

**Path B — Compute.** Tensor graphs emit to **Compute IR** (UOps). This is the accelerator-side math: matmuls, reductions, elementwise, fused kernels.

Both paths feed into the Phase 2 (concrete) verifier before codegen.

---

## L0: Machine

### Purpose

Fully explicit execution plan. Every buffer, every kernel, every stream, every byte. No decisions left. This is what actually runs.

### Control IR

Ten operations over named memory regions. SSA registers. No flat address space — every load and store names its region, so the backend knows all aliasing without analysis.

```
load.{sz}  rgn[off]           read from named region
store.{sz} rgn[off], val      write to region (rw only)
hash val → reg                deterministic hash for map indexing
arith {op} a, b → reg         add, sub, mul, and, or, shift
cmp {op} a, b → reg           eq, neq, lt, gt → 1-bit result
branch reg → blk, blk         conditional jump
jump → blk                    unconditional jump
queue_push rgn, val            push descriptor to queue
queue_pop rgn → reg            pop descriptor from queue
terminate                      end of execution unit
```

**Regions** are named, sized, access-controlled memory. Not a flat address space — specific bounded things. This preserves aliasing knowledge all the way to codegen. A flat address space throws this away and forces the backend to re-derive it.

Why not target C? C implies abstractions we don't use: a call stack (we don't recurse), a general pointer model (we have named regions), function boundaries (we inline everything). The C compiler then has to *re-discover* structure we already know. It may fail and generate worse code. More importantly, C is a black box: we lose visibility into what actually executes.

### Compute IR (UOps)

Atomic operations inside a kernel. Each is a typed node `(op, dtype, src[], arg)` forming a DAG rooted at STORE nodes.

| Category     | Ops                                                  |
|--------------|------------------------------------------------------|
| Memory       | `LOAD` `STORE` `INDEX`                               |
| Arithmetic   | `ADD` `MUL` `MULACC` `NEG` `RECIPROCAL` `MAX` `MOD` |
| Compare      | `CMPLT` `CMPNE` `WHERE`                              |
| Transcendent | `EXP2` `LOG2` `SIN` `SQRT`                           |
| Control      | `RANGE` `END` `IF` `ENDIF` `BARRIER`                 |
| Type         | `CONST` `CAST` `BITCAST` `VECTORIZE` `GEP`           |
| Special      | `WMMA` `REDUCE` `CUSTOM`                             |

~25 ops. Complete for any dense numeric kernel. `CUSTOM` covers sparse, scatter, and target-specific intrinsics.

### IR

```
L0_IR = {
    memory_plan:   Map<BufferId, MemorySlot>
    kernel_plan:   [KernelDecl]
    stream_plan:   Map<StreamId, [KernelId]>
    sync_plan:     [SyncPoint]
    transfer_plan: [Transfer]
    init_plan:     [InitOp]
    control_blocks: [Block]              Machine IR blocks
}

KernelDecl = {
    id:         KernelId
    inputs:     [BufferId]
    outputs:    [BufferId]
    ops:        [UOp]                    the kernel body
    grid:       (x, y, z)
    block:      (x, y, z)
    shared_mem: bytes
}

MemorySlot = {
    pool:       PoolId                   which physical memory
    offset:     bytes
    size:       bytes
    lifetime:   (first_use, last_use)
}
```

### Verification — Concrete (Phase 2)

After memory planning, stream inference, and kernel scheduling. Pure read-only checks on the concrete plan.

| Property       | Check                      | Catches                                                |
|----------------|----------------------------|--------------------------------------------------------|
| Safety         | Kernel correctness         | UOp sequences don't type-check, out-of-bounds access   |
| Safety         | Buffer lifetime safety     | Overlapping writes to same memory slot                 |
| Safety         | Stream hazard check        | Shared mutable region + different streams, no sync     |
| Liveness       | Sync completeness          | Cross-stream dependency missing a barrier              |
| Resource bound | Memory capacity            | Sum of live slots > pool capacity at any time t        |
| Resource bound | Pool exhaustion            | No headroom for transient allocations at pipeline depth |

### Optimization (IR→IR rewrites)

Closest to the metal. Most aggressive. Kernel fusion (merge adjacent kernels sharing buffers), memory packing (minimize peak by reordering lifetimes), launch config tuning (grid/block for occupancy), instruction selection (UOp → target ISA), register pressure management, prefetch insertion.

---

## Codegen

L0 IR → target code. This is the only target-dependent phase in the entire compiler.

### Control Path

Machine IR → target backend. The 10 ops translate mechanically.

| Backend    | Characteristics                                                                |
|------------|--------------------------------------------------------------------------------|
| **x86-64** | Each op → 1–3 instructions. ~5 live values, no spills. Regions → register pointers. |
| **LLVM**   | Regions become pointer arguments with `!noalias` metadata. LLVM gets perfect aliasing. |
| **eBPF**   | Machine IR's restrictions (no loops, bounded access, linear resources) already satisfy the eBPF verifier. Nearly 1:1. |
| **FPGA**   | Each block → combinational pipeline stage. Regions → BRAM ports. `queue_push` → FIFO write-enable. `terminate` → valid signal. |

### Compute Path

UOps → target ISA. Three passes:

1. **Instruction selection** — maps UOps to target ISA. `MULACC` → `fma.rn.f32` on PTX, `vfmadd` on x86.
2. **Register allocation** — handles spill/fill and manages pressure per-target. GPU has thousands of registers (occupancy-sensitive), CPU has 16 GPRs (spill-heavy).
3. **ISA emission** — produces final text or binary. Warp divergence on GPU means `IF/ENDIF` UOps have different cost profiles than on CPU. Vectorization width is target-dependent.

### Bounded Complexity

Codegen is deferred complexity, not buried complexity. The contract is clear: L0 IR is target-independent. Codegen is the *only* target-dependent phase. The UOp set is small enough that adding a new backend means writing ~25 emission rules plus register allocation for that target. This is a bounded, mechanical task — not an open research problem. The Machine IR is similarly small: 10 ops, each mapping to a handful of target instructions.

---

## Linking & Runtime

### Binary Structure

One binary. CPU object + accelerator blobs + metadata.

```
.text     schedule_loop, stage_pipeline, actor_dispatch, platform_primitives
.rodata   kernel cubins, memory_layout_table, stream_descriptors, schedule_descriptor
.data     pool_metadata, arena_metadata
.bss      gpu_context, stream_handles, event_handles
```

### Platform Primitives

Hand-written per platform. The generated code calls into these. The emitter produces control flow + kernels. The runtime provides the operations.

| Primitive           | Linux + CUDA                      |
|---------------------|-----------------------------------|
| `region_alloc`      | Pool: atomic pop. Arena: bump.    |
| `region_free`       | Pool: atomic push. Arena: no-op.  |
| `dma_ssd_to_ram`    | `io_uring` / mmap+prefault        |
| `pcie_dma_h2d`      | `cuMemcpyHtoDAsync`              |
| `pcie_dma_d2h`      | `cuMemcpyDtoHAsync`              |
| `gpu_dispatch`      | `cuLaunchKernel`                  |
| `gpu_sync`          | `cuStreamSynchronize`             |
| `gpu_event_*`       | `cuEventRecord / cuStreamWaitEvent` |
| `queue_push/pop`    | Ring buffer in shared memory      |

Machine IR and kernel descriptors are target-independent. Only backends and primitive implementations change per platform.

### Runtime Error Policy

All correctness errors caught at compile time by the two-phase verifier. The binary assumes all static proofs hold. Hardware faults crash the process — outside scope of generated code.

---

## Escape Hatches

At any layer, annotate with `#[<target_layer>::<directive>]`:

```
// At L3: force a method choice
model classify {
    ...
    #[l2::backward(evolution(pop: 50))]
}

// At L2: force a placement
infer: sequential [
    linear(784, 256),
    #[l1::on(gpu_1)]
    linear(256, 10)
]

// At L2: force a kernel
infer: sequential [
    linear(784, 256),
    #[l0::kernel("fused_gelu.ptx")]
    ...
]
```

The escape hatch **must pass verification at its target layer.** You can inline PTX, but it must have the right buffer types. The compiler checks the boundary. If it fails, the error points at the annotation — the user broke the contract.

An escape hatch is **opaque to optimization** at layers above its target. `#[l0::kernel(...)]` cannot be fused with adjacent ops at L1. It's a black box with a typed boundary. This is the price of escaping.

---

## Search Architecture

Every lowering boundary uses the same pattern:

```
lower(source_ir, target_constraints) -> Result<target_ir, SearchFailure>

    1. enumerate(source_ir, target_grammar) -> [candidate]
    2. filter(candidates, verify_target)    -> [valid]
    3. score(valid, cost_model_target)      -> [(candidate, cost)]
    4. select(scored)                       -> target_ir | SearchFailure

SearchFailure =
    NoCandidates(reason)        constraints too tight
  | TooManyCandidates(count)    representation too loose
  | Timeout(budget_exhausted)   problem is genuinely hard
```

SearchFailure is a diagnostic, not an error. It tells you what to fix: tighten constraints, loosen them, or redesign the layer boundary.

---

## Data Ingestion

Data flows from storage to device memory before any kernel touches it:

```
Storage → decode (CPU) → Host Memory → batch → Staging → DMA → Device
```

The contract boundaries are clean: L2 says *what* to sample (epoch shuffle, curriculum, etc.), L1 says *where* to stage it (which memory pool, which node), L0 says *how* bytes move (DMA ops, transfer plan). Format-specific decoders (JPEG, video, custom binary) are pluggable at the L1/L0 boundary — they're `CUSTOM` UOps or host-side init ops.

---

## Open Questions

**1. Recurrence and variable-length.** Current stance: everything finite, `until(pred)` is spec error without a proven bound. But transformers process variable-length sequences. Is `sequence(domain, max_len)` at L3 enough? Or do we need a richer notion?

**2. Multi-model composition.** GAN = generator + discriminator. Distillation = teacher + student. RL = policy + value + environment. L3 currently has one model per spec. Do we want multiple models with relationships, or a separate composition layer?

**3. Training loop structure.** L3 says `goal: minimize(loss)`. Real training has phases — pretrain, finetune, RLHF. Epochs, checkpointing, evaluation. Probably L2 as a `schedule`, but it needs design.

**4. Cost model grounding.** L2 cost model is heuristic. L1 uses hardware specs. Neither is calibrated. Do we want empirical calibration — run a few kernels, measure, update?

**5. Incremental compilation.** If you change one loss term at L3, do you re-search all of L2? Probably: hash each IR node, re-lower only the subgraph whose inputs changed.

**6. The host language.** Rust for the compiler (algebraic types = IR correctness for free). But the DSL parser, the REPL, the interactive experience — Python bindings? LSP?

---

## What Is Resolved

- Layer count and purpose (4 layers, clear separation of concerns)
- L1 is the systems-level DSL: actors, stages, pipelines, windows, tensor graphs, topology
- Dual emission from L1: stages/actors → Control IR, tensor graphs → Compute IR (UOps)
- Two-phase verification: structural (pre-scheduling, at L1) and concrete (post-scheduling, at L0)
- Verification at every layer, classified by four property kinds
- Named memory regions in Control IR — aliasing known to codegen without analysis
- Memory planning as a compiler pass (persistent, arena, pool), not user-declared
- Stream inference from pipeline_depth + placement
- Escape hatch semantics (typed, opaque, verified at target)
- Codegen contract (target-independent L0 IR, target-dependent emission only)
- Data ingestion contract (L2 what, L1 where, L0 how)
- Search architecture (uniform enumerate → filter → score → select at every boundary)
- Platform primitives as the narrow runtime interface
- No autodiff at L1 — backward is explicit; autodiff is an L2 method expanded during lowering
- Dependency-inferred scheduling — no user-specified phases