Pipeline Walkthrough: From L1 Source to x86-64 Execution

This document traces a single L1 program through every stage of the compiler pipeline, from DSL source text to x86-64 machine code and execution. Every intermediate representation is shown in full. Nothing is excerpted, summarized, or hidden. The purpose is to demonstrate that each transformation preserves meaning while lowering abstraction, and that verification gates between stages ensure each representation is structurally sound before the next stage consumes it.

The program used is examples/product.l1 — a product tracker that accumulates purchase quantities and costs, with an observer that emits the running total after each step.

Reproducibility. Every output shown in this document can be regenerated:

cargo run -- examples/product.l1 --dump-ir    # all IRs + hex dump
cargo run -- examples/product.l1              # execution output

Pipeline Overview

Compiler Pipeline

DSL Source (.l1)

Parse

L1 IR

Verify (L1)

L1 IR (verified)

Emit

L0 IR

Verify (L0)

L0 IR (verified)

Codegen

x86-64 Machine Code

Execute

Two verification gates sit between the representations. The first (L1 verification) checks structural properties of the high-level IR before lowering. The second (L0 verification) checks concrete properties of the machine-level IR before codegen. Each gate is a pass/fail decision. If verification fails, the pipeline stops — no invalid IR reaches the next stage.

The Source Program

The program models a product ledger. Each step, a purchase arrives: 3 units at price 7. The ledger actor multiplies price by quantity to compute the line cost, accumulates both a running unit count and a running cost total. An observer reads the total through a window and emits it as output.

After 4 steps, the expected state is:

count = 12 (4 purchases × 3 units each)
total = 84 (4 × (7 × 3) = 4 × 21)
Emitted values: [21, 42, 63, 84] — the running total after each step

// Product tracker: accumulates quantity and total cost from purchase events.
//
// Each step, a purchase of 3 units at price 7 arrives.
// The actor multiplies price * quantity to get the line cost,
// then adds it to the running total.
//
// After 4 steps:
//   count = 4 * 3 = 12
//   total = 4 * (7 * 3) = 84
//   emitted values: [21, 42, 63, 84]

actor ledger {
    state {
        count: u64 = 0
        total: u64 = 0
    }

    window summary : (count, total)
        readers(report)

    on Purchase(price: u64, qty: u64) {
        count = count + qty
        total = total + (price * qty)
    }
}

leaf buy {
    process {
        forward(ledger, Purchase(7, 3))
    }
}

leaf report {
    reads ledger.summary
    process {
        read(ledger.summary.total)
        emit(total)
    }
}

pipeline main {
    buy -> ledger -> report
}

core main {
    actors: [ledger]
    leaves: [buy, report]
    pipelines: [main]
    steps: 4
}

The key DSL concepts at work:

Actor (ledger): Owns mutable state. Processes messages one at a time, serialized. State fields count and total are typed (u64) and initialized to zero.
Window (summary): Grants read-only access to a subset of actor state. The report leaf can read count and total through this window, but cannot write to them. Safety requires that readers and the actor's message handler never execute concurrently.
Leaves (buy, report): Stateless processors. buy forwards a Purchase message to the actor. report reads state through the window and emits the total as observable output.
Pipeline (main): An ordered execution chain — buy → ledger → report. Each step, the pipeline executes left to right: the leaf sends a message, the actor processes it, the observer reads the result.
Core (main): The execution schedule. Declares which actors, leaves, and pipelines participate, and bounds execution to exactly 4 steps.

L1 IR

Parsing transforms the source text into a structured, normalized intermediate representation. The parser resolves all names, validates syntax, and produces the L1 IR shown below.

actor ledger {
  state {
    count: u64 = 0
    total: u64 = 0
  }
  window summary : (count, total) readers(report)
  on Purchase(price: u64, qty: u64) { count = (count + qty); total = (total + (price * qty)) }
}
leaf buy { forward(ledger, Purchase(7, 3)); }
leaf report { reads ledger.summary; read(ledger.summary.total); emit(total); }
pipeline main { buy -> ledger -> report }
core main {
  actors: [ledger]
  leaves: [buy, report]
  pipelines: [main]
  steps: 4
}

What parsing resolved:

Structural normalization. The actor's state block, window declarations, and message handlers are parsed into distinct typed structures. The handler body count = count + qty / total = total + (price * qty) becomes an explicit block of assignment expressions with nested arithmetic nodes.
Name binding. Every reference — the leaf's forward(ledger, ...), the window's readers(report), the pipeline's buy -> ledger -> report, the core's entity lists — resolves to a declared entity. If any name were misspelled or missing, the parser would reject the program before the IR is constructed.
Syntactic sugar dissolved. The process { ... } wrapper in leaf declarations is dissolved — the IR stores the action list directly. The semicolons and braces of the display format are the IR's canonical serialization, not the source syntax.

What is preserved: the complete program semantics. Every actor, state field, initialization value, handler, window, leaf action, pipeline ordering, and schedule parameter appears in the IR exactly as declared. Nothing is lost, nothing is added. The IR is a total, unambiguous description of the program.

L1 Verification

L1 verification is a pass/fail gate — it produces no new IR. It reads the L1 IR and checks six structural properties. If any check fails, the pipeline stops and reports the specific violation.

The checks, mapped to the spec's four property categories:

Property	Check	What it catches
Safety	Ref resolution	Every name in cores, pipelines, windows, and leaf actions resolves to a declared actor, leaf, or pipeline. Catches dangling references — a `forward` to a non-existent actor, a window naming a non-existent reader, a pipeline referencing an undeclared entity.
Safety	Exclusive ownership	Each actor and leaf belongs to exactly one core. Prevents the same entity from being claimed by two different execution contexts.
Safety	Window separation	Window readers must be leaves (not actors). Readers must be in the same core as the actor. A leaf that both reads a window on an actor AND forwards messages to that same actor is rejected — this would create a read-write hazard.
Consistency	Pipeline well-formedness	Every pipeline has at least 2 stages. No stage appears twice within a pipeline (which would indicate a cycle).
Liveness	Buffer conservation	Every leaf has at least one action (forward, read, or emit). A leaf with no actions would mean its input is never consumed.
Resource bound	Finiteness	Every core has `steps > 0`. Cross-pipeline cycles are detected via topological sort — if the entity ordering across all pipelines contains a cycle, the program cannot make progress and is rejected.

By the time verification passes, the L1 IR has been proven structurally sound: all references resolve, ownership is exclusive, windows are safe, pipelines are well-formed, buffers are consumed, and execution is bounded. The emit stage can trust its input completely.

L0 IR

Emission transforms the verified L1 IR into L0 IR — the machine-level representation. This is the most important transformation in the pipeline. High-level concepts dissolve into explicit, low-level operations over named memory regions.

=== Regions ===
  region ledger_state : 16 bytes, rw, state
  region ledger_purchase_queue : 272 bytes, rw, queue
  region step_counter : 8 bytes, rw, control
  region output : 48 bytes, rw, output
=== Blocks ===
entry:
  r0 = imm #0
  store.64 ledger_state[0], r0
  store.64 ledger_state[8], r0
  store.64 step_counter[0], r0
  store.64 output[0], r0
  jump -> loop_check
loop_check:
  r1 = load.64 step_counter[0]
  r2 = imm #4
  r3 = cmp.lt r1, r2
  branch r3 -> step, exit
step:
  r4 = imm #7
  queue_push ledger_purchase_queue, r4
  r5 = imm #3
  queue_push ledger_purchase_queue, r5
  r6 = queue_pop ledger_purchase_queue
  r7 = queue_pop ledger_purchase_queue
  r8 = load.64 ledger_state[0]
  r9 = add r8, r7
  store.64 ledger_state[0], r9
  r10 = load.64 ledger_state[8]
  r11 = mul r6, r7
  r12 = add r10, r11
  store.64 ledger_state[8], r12
  r13 = load.64 ledger_state[8]
  r14 = load.64 ledger_state[8]
  queue_push output, r14
  r15 = load.64 step_counter[0]
  r16 = add r15, #1
  store.64 step_counter[0], r16
  jump -> loop_check
exit:
  terminate

Swipe to scroll wide content

Here is what happened to each L1 concept:

Actors became regions. The actor ledger with state fields count: u64 = 0 and total: u64 = 0 became region ledger_state : 16 bytes, rw, state — two 8-byte fields at offsets 0 and 8. The actor's identity dissolved. What remains is a named, sized, access-controlled memory region. Loads and stores name this region explicitly: store.64 ledger_state[0] writes the count field, store.64 ledger_state[8] writes the total field.

Messages became queues. The forward(ledger, Purchase(7, 3)) in the buy leaf became two queue_push operations — one for each argument (price=7, qty=3) — into region ledger_purchase_queue : 272 bytes, rw, queue. The actor's on Purchase(price, qty) handler became two queue_pop operations that retrieve those values, followed by arithmetic on the state region. The queue region is a ring buffer: 16 bytes for head and tail pointers, plus capacity for 16 messages × 2 arguments × 8 bytes = 256 bytes of data.

The pipeline became a loop. The steps: 4 in the core schedule became region step_counter : 8 bytes, rw, control, a loop_check block with cmp.lt against immediate #4, and a conditional branch. Each iteration walks the pipeline stages in order (buy's forward → ledger's handler → report's read and emit), then increments the step counter and jumps back to loop_check.

Window reads became loads. The report leaf's read(ledger.summary.total) became r13 = load.64 ledger_state[8] — a direct load from the state region at the total field's offset. The window abstraction is gone; what remains is a memory access that the verifier already proved safe.

Emit became a queue push. The emit(total) became queue_push output, r14 — pushing the loaded total value into region output : 48 bytes, rw, output. The output region is sized for exactly 4 steps: 16 bytes header + 4 × 8 bytes data = 48 bytes.

Everything became explicit. Every load, every store, every register assignment, every comparison, every branch is visible. There is no implicit state, no hidden control flow, no magic. The L0 IR is a total description of what the machine will do.

Walking through the blocks:

entry: Loads immediate 0, stores it to both state fields (ledger_state[0] and [8]), the step counter, and the output head. Jumps to loop_check.
loop_check: Loads the step counter, loads the bound (4), compares. Branches to step if counter < 4, otherwise to exit.
step: Executes one complete pipeline iteration. Pushes price (7) and qty (3) to the queue, pops them back (simulating message delivery), loads count, adds qty, stores count. Loads total, multiplies price × qty, adds to total, stores total. Reads total through the window, pushes it to output. Increments step counter. Jumps back to loop_check.
exit: Terminates execution.

L0 Verification

L0 verification checks the concrete IR after emission, before codegen. It collects all errors (unlike L1 verification which stops at the first). The checks:

Property	Check	What it catches
Safety	Control flow targets	Every `branch` and `jump` names a block that exists. A dangling target would mean the program jumps into the void.
Safety	Block reachability	Every block is reachable from the entry block (the first block) via BFS over control flow edges. Unreachable blocks are dead code that may contain invalid operations.
Safety	Region declarations	Every `load` and `store` names a region that is declared in the regions list. An undeclared region reference would mean accessing memory that doesn't exist.
Safety	Region bounds	Every memory access satisfies `offset + access_size ≤ region_size`. Out-of-bounds access would read or write past the region boundary.
Safety	Access mode	Stores to read-only regions are rejected. The access mode is a compile-time invariant that codegen can rely on.
Resource bound	Queue safety	`queue_push` and `queue_pop` only operate on regions with queue or output kind. Using queue operations on a state or control region would corrupt its layout.
Resource bound	Memory capacity	Total memory is bounded — every region has a fixed size, and all sizes are known at compile time. The `total_memory()` utility sums all region sizes (in this program: 16 + 272 + 8 + 48 = 344 bytes).

After L0 verification passes, the IR is proven safe for codegen: all control flow is valid, all memory accesses are in-bounds, all access modes are respected, and all queue operations target the correct region kinds.

x86-64 Machine Code

Codegen translates the verified L0 IR into x86-64 machine code. The translation is mechanical: each L0 operation maps to a small, predictable cluster of x86 instructions.

Raw hex dump

53 55 41 54 41 55 41 56 41 57 4c 8b a7 00 00 00
00 4c 8b af 08 00 00 00 4c 8b b7 10 00 00 00 4c
8b bf 18 00 00 00 48 b8 00 00 00 00 00 00 00 00
49 89 84 24 00 00 00 00 49 89 84 24 08 00 00 00
49 89 86 00 00 00 00 49 89 87 00 00 00 00 e9 00
00 00 00 49 8b 8e 00 00 00 00 48 ba 04 00 00 00
00 00 00 00 48 39 d1 0f 9c c3 48 0f b6 db 48 85
db 0f 85 05 00 00 00 e9 64 01 00 00 48 be 07 00
00 00 00 00 00 00 49 8b bd 00 00 00 00 48 89 fd
48 b9 03 00 00 00 00 00 00 00 48 c1 e5 03 48 81
c5 10 00 00 00 4c 01 ed 48 89 75 00 48 81 c7 01
00 00 00 49 89 bd 00 00 00 00 49 b8 03 00 00 00
00 00 00 00 49 8b bd 00 00 00 00 48 89 fd 48 b9
03 00 00 00 00 00 00 00 48 c1 e5 03 48 81 c5 10
00 00 00 4c 01 ed 4c 89 45 00 48 81 c7 01 00 00
00 49 89 bd 00 00 00 00 49 8b bd 08 00 00 00 48
89 fd 48 c1 e5 03 48 81 c5 10 00 00 00 4c 01 ed
4c 8b 4d 00 48 81 c7 01 00 00 00 49 89 bd 08 00
00 00 49 8b bd 08 00 00 00 48 89 fd 48 c1 e5 03
48 81 c5 10 00 00 00 4c 01 ed 4c 8b 55 00 48 81
c7 01 00 00 00 49 89 bd 08 00 00 00 4d 8b 9c 24
00 00 00 00 4c 89 d8 4c 01 d0 49 89 84 24 00 00
00 00 49 8b 8c 24 08 00 00 00 4c 89 ca 49 0f af
d2 48 89 cb 48 01 d3 49 89 9c 24 08 00 00 00 49
8b b4 24 08 00 00 00 4d 8b 84 24 08 00 00 00 49
8b bf 00 00 00 00 48 89 fd 48 b9 03 00 00 00 00
00 00 00 48 c1 e5 03 48 81 c5 10 00 00 00 4c 01
fd 4c 89 45 00 48 81 c7 01 00 00 00 49 89 bf 00
00 00 00 4d 8b 8e 00 00 00 00 4d 89 ca 49 81 c2
01 00 00 00 4d 89 96 00 00 00 00 e9 73 fe ff ff
41 5f 41 5e 41 5d 41 5c 5d 5b c3

491 bytes of x86-64 machine code.

Annotated disassembly

The generated function follows the System V AMD64 calling convention. It receives a single argument in rdi: a pointer to an array of region base addresses. Region bases are loaded into dedicated registers at entry:

Register	Region
R12	`ledger_state` (16 bytes, state)
R13	`ledger_purchase_queue` (272 bytes, queue)
R14	`step_counter` (8 bytes, control)
R15	`output` (48 bytes, output)

SSA registers are allocated from the remaining pool: RAX, RCX, RDX, RBX, RSI, R8–R11. RBP and RDI are used as scratch temporaries for queue address computation.

; === prologue: save callee-saved registers ===
0x00: push   rbx                     ; save callee-saved
0x01: push   rbp
0x02: push   r12
0x04: push   r13
0x06: push   r14
0x08: push   r15

; === load region base pointers from rdi array ===
0x0a: mov    r12, [rdi+0x00]         ; r12 = &ledger_state
0x11: mov    r13, [rdi+0x08]         ; r13 = &ledger_purchase_queue
0x18: mov    r14, [rdi+0x10]         ; r14 = &step_counter
0x1f: mov    r15, [rdi+0x18]         ; r15 = &output

; === entry block: initialize regions ===
;     r0 = imm #0
0x26: movabs rax, 0x0                ; rax = 0 (r0)

;     store.64 ledger_state[0], r0   — count = 0
0x30: mov    [r12+0x00], rax

;     store.64 ledger_state[8], r0   — total = 0
0x38: mov    [r12+0x08], rax

;     store.64 step_counter[0], r0   — step = 0
0x40: mov    [r14+0x00], rax

;     store.64 output[0], r0         — output head = 0
0x47: mov    [r15+0x00], rax

;     jump -> loop_check
0x4e: jmp    0x53                    ; fall through to loop_check

; === loop_check block: compare step counter to bound ===
;     r1 = load.64 step_counter[0]
0x53: mov    rcx, [r14+0x00]         ; rcx = step counter (r1)

;     r2 = imm #4
0x5a: movabs rdx, 0x4                ; rdx = 4 (r2)

;     r3 = cmp.lt r1, r2
0x64: cmp    rcx, rdx                ; compare step < 4
0x67: setl   bl                      ; bl = 1 if less
0x6a: movzx  rbx, bl                 ; rbx = zero-extended result (r3)

;     branch r3 -> step, exit
0x6e: test   rbx, rbx                ; test condition
0x71: jne    0x7c                    ; if true → step block
0x77: jmp    0x1e0                   ; if false → exit block

; === step block: pipeline execution ===

; --- leaf buy: forward(ledger, Purchase(7, 3)) ---
;     r4 = imm #7
0x7c: movabs rsi, 0x7                ; rsi = 7, the price (r4)

;     queue_push ledger_purchase_queue, r4
;       load head, compute slot address, store value, increment head
0x86: mov    rdi, [r13+0x00]         ; rdi = queue head
0x8d: mov    rbp, rdi                ; rbp = head (working copy)
0x90: movabs rcx, 0x3                ; rcx = 3 (modulo constant, unused here)
0x9a: shl    rbp, 0x3                ; rbp = head * 8
0x9e: add    rbp, 0x10               ; rbp += 16 (skip header)
0xa5: add    rbp, r13                ; rbp = &queue[head] absolute
0xa8: mov    [rbp+0x00], rsi         ; queue[head] = 7 (price)
0xac: add    rdi, 0x1                ; head++
0xb3: mov    [r13+0x00], rdi         ; store updated head

;     r5 = imm #3
0xba: movabs r8, 0x3                 ; r8 = 3, the quantity (r5)

;     queue_push ledger_purchase_queue, r5
0xc4: mov    rdi, [r13+0x00]         ; rdi = queue head
0xcb: mov    rbp, rdi
0xce: movabs rcx, 0x3
0xd8: shl    rbp, 0x3
0xdc: add    rbp, 0x10
0xe3: add    rbp, r13
0xe6: mov    [rbp+0x00], r8          ; queue[head] = 3 (qty)
0xea: add    rdi, 0x1
0xf1: mov    [r13+0x00], rdi         ; store updated head

; --- actor ledger: queue_pop × 2, then handler body ---
;     r6 = queue_pop ledger_purchase_queue  (price)
0xf8: mov    rdi, [r13+0x08]         ; rdi = queue tail
0xff: mov    rbp, rdi
0x102: shl   rbp, 0x3
0x106: add   rbp, 0x10
0x10d: add   rbp, r13
0x110: mov   r9, [rbp+0x00]          ; r9 = popped price value (r6)
0x114: add   rdi, 0x1                ; tail++
0x11b: mov   [r13+0x08], rdi         ; store updated tail

;     r7 = queue_pop ledger_purchase_queue  (qty)
0x122: mov   rdi, [r13+0x08]         ; rdi = queue tail
0x129: mov   rbp, rdi
0x12c: shl   rbp, 0x3
0x130: add   rbp, 0x10
0x137: add   rbp, r13
0x13a: mov   r10, [rbp+0x00]         ; r10 = popped qty value (r7)
0x13e: add   rdi, 0x1
0x145: mov   [r13+0x08], rdi

; --- handler: count = count + qty ---
;     r8 = load.64 ledger_state[0]   — load count
0x14c: mov   r11, [r12+0x00]         ; r11 = count (r8)

;     r9 = add r8, r7                — count + qty
0x154: mov   rax, r11                ; rax = count
0x157: add   rax, r10                ; rax = count + qty (r9)

;     store.64 ledger_state[0], r9   — store updated count
0x15a: mov   [r12+0x00], rax

; --- handler: total = total + (price * qty) ---
;     r10 = load.64 ledger_state[8]  — load total
0x162: mov   rcx, [r12+0x08]         ; rcx = total (r10)

;     r11 = mul r6, r7               — price * qty
0x16a: mov   rdx, r9                 ; rdx = price
0x16d: imul  rdx, r10                ; rdx = price * qty (r11)

;     r12 = add r10, r11             — total + (price * qty)
0x171: mov   rbx, rcx                ; rbx = total
0x174: add   rbx, rdx                ; rbx = total + price*qty (r12)

;     store.64 ledger_state[8], r12  — store updated total
0x177: mov   [r12+0x08], rbx

; --- leaf report: read + emit ---
;     r13 = load.64 ledger_state[8]  — read total through window
0x17f: mov   rsi, [r12+0x08]         ; rsi = total (r13)

;     r14 = load.64 ledger_state[8]  — emit expression: load total
0x187: mov   r8, [r12+0x08]          ; r8 = total (r14)

;     queue_push output, r14         — emit(total)
0x18f: mov   rdi, [r15+0x00]         ; rdi = output head
0x196: mov   rbp, rdi
0x199: movabs rcx, 0x3
0x1a3: shl   rbp, 0x3
0x1a7: add   rbp, 0x10
0x1ae: add   rbp, r15                ; rbp = &output[head]
0x1b1: mov   [rbp+0x00], r8          ; output[head] = total
0x1b5: add   rdi, 0x1
0x1bc: mov   [r15+0x00], rdi         ; head++

; --- step counter increment ---
;     r15 = load.64 step_counter[0]
0x1c3: mov   r9, [r14+0x00]          ; r9 = step counter (r15)

;     r16 = add r15, #1
0x1ca: mov   r10, r9
0x1cd: add   r10, 0x1                ; r10 = step + 1 (r16)

;     store.64 step_counter[0], r16
0x1d4: mov   [r14+0x00], r10         ; store updated step counter

;     jump -> loop_check
0x1db: jmp   0x53                    ; back to loop_check

; === exit block: terminate ===
;     restore callee-saved registers and return
0x1e0: pop   r15
0x1e2: pop   r14
0x1e4: pop   r13
0x1e6: pop   r12
0x1e8: pop   rbp
0x1e9: pop   rbx
0x1ea: ret

Swipe to scroll wide content

Codegen strategy:

Regions become register-indirect memory. Each region's base address is loaded into a dedicated callee-saved register (R12–R15) at function entry. All loads and stores use these base registers with constant displacements: mov [r12+0x08], rax writes to ledger_state at offset 8 (the total field). Named regions preserve aliasing knowledge all the way to machine code — the codegen knows that [r12+0x00] and [r14+0x00] can never alias because they point to different regions.
Block structure maps to jump targets. The L0 blocks (entry, loop_check, step, exit) become contiguous instruction sequences with jmp/jne instructions connecting them. Jump targets are resolved in a two-pass fixup: the first pass emits placeholder offsets, the second patches them once all block positions are known.
Queue operations translate to ring buffer indexing. Each queue_push becomes: load head from [base+0], compute slot address as base + 16 + head*8, store the value, increment head, store head back. queue_pop does the same with tail at [base+8]. The pattern is identical every time — five instructions for each queue operation.
Arithmetic is direct. add → add, mul → imul. The move-then-operate pattern (mov rax, r11; add rax, r10) is the codegen's way of preserving SSA semantics in a register machine: the destination register is first loaded with the left operand, then the operation is applied with the right operand.
Comparisons use setcc + movzx. The cmp.lt operation becomes cmp rcx, rdx; setl bl; movzx rbx, bl — compare, set a byte flag, zero-extend to 64 bits. The result feeds into test rbx, rbx; jne for the conditional branch.

Execution

Running the program produces:

Execution complete.
  step_counter[0] = 4
  output[0] = 4
  ledger_state[0] = 12
  ledger_purchase_queue[0] = 8
  output values: [21, 42, 63, 84]

Interpreting the results:

ledger_state[0] = 12: The count field. 4 steps × 3 units per step = 12. Correct.
step_counter[0] = 4: The loop ran exactly 4 iterations. Correct.
ledger_purchase_queue[0] = 8: The queue head advanced 8 positions (2 pushes per step × 4 steps). Correct.
output[0] = 4: The output head — 4 values were emitted. Correct.
output values: [21, 42, 63, 84]: The running total after each step:
- Step 1: 0 + (7 × 3) = 21
- Step 2: 21 + 21 = 42
- Step 3: 42 + 21 = 63
- Step 4: 63 + 21 = 84

Every value matches the program's intent. The total field (at ledger_state[8], not shown in the summary line but readable from the region) holds 84. The loop from source intent to machine execution is closed.

Closing

This walkthrough traced a single program through six transformations: parse, L1 verify, emit, L0 verify, codegen, execute. At each stage, the representation was shown in full — no excerpts, no elisions.

Three properties of the pipeline emerge from this trace. First, every representation is total and inspectable. The L1 IR is a complete, unambiguous description of the program. The L0 IR is a complete, explicit description of the execution. The machine code is a complete, executable binary. Nothing is hidden at any layer. Second, verification gates between representations mean each stage can trust its input. The emitter knows all references resolve because L1 verification proved it. The codegen knows all memory accesses are in-bounds because L0 verification proved it. Trust is replaced by proof.

Third, the transformations are mechanical and traceable. Every L0 instruction maps back to an L1 concept. Every x86 instruction maps back to an L0 operation. No stage introduces decisions the previous stage didn't authorize. The machine code is a direct consequence of the source program, with every intermediate step visible and verifiable.