914 lines
37 KiB
HTML
914 lines
37 KiB
HTML
<!DOCTYPE html>
|
||
<html lang="en">
|
||
<head>
|
||
<meta charset="utf-8">
|
||
<meta name="viewport" content="width=device-width, initial-scale=1.0, maximum-scale=5.0">
|
||
<title>Pipeline Walkthrough: L1 Source to x86-64</title>
|
||
<link rel="stylesheet" href="https://cdn.jsdelivr.net/npm/prismjs@1.29.0/themes/prism-tomorrow.min.css">
|
||
<style>
|
||
:root {
|
||
--bg: #1a1a2e;
|
||
--bg-code: #16213e;
|
||
--bg-inline: #0f3460;
|
||
--fg: #e0e0e0;
|
||
--fg-dim: #a0a0b0;
|
||
--accent: #e94560;
|
||
--accent2: #53a8b6;
|
||
--border: #2a2a4a;
|
||
--table-stripe: #1e1e3a;
|
||
}
|
||
|
||
* { box-sizing: border-box; margin: 0; padding: 0; }
|
||
|
||
html {
|
||
font-size: 16px;
|
||
-webkit-text-size-adjust: 100%;
|
||
scroll-behavior: smooth;
|
||
}
|
||
|
||
body {
|
||
font-family: -apple-system, BlinkMacSystemFont, 'Segoe UI', Roboto,
|
||
'Helvetica Neue', Arial, sans-serif;
|
||
background: var(--bg);
|
||
color: var(--fg);
|
||
line-height: 1.7;
|
||
padding: 1rem;
|
||
max-width: 100%;
|
||
overflow-x: hidden;
|
||
overflow-wrap: break-word;
|
||
}
|
||
|
||
article {
|
||
max-width: 720px;
|
||
margin: 0 auto;
|
||
}
|
||
|
||
h1 {
|
||
font-size: clamp(1.3rem, 4vw, 1.6rem);
|
||
margin: 1.5rem 0 0.8rem;
|
||
color: var(--accent);
|
||
line-height: 1.3;
|
||
border-bottom: 2px solid var(--accent);
|
||
padding-bottom: 0.4rem;
|
||
}
|
||
|
||
h2 {
|
||
font-size: clamp(1.1rem, 3vw, 1.3rem);
|
||
margin: 2rem 0 0.6rem;
|
||
color: var(--accent2);
|
||
border-bottom: 1px solid var(--border);
|
||
padding-bottom: 0.3rem;
|
||
}
|
||
|
||
h3 {
|
||
font-size: clamp(1rem, 2.5vw, 1.1rem);
|
||
margin: 1.5rem 0 0.5rem;
|
||
color: var(--fg);
|
||
}
|
||
|
||
p {
|
||
margin: 0.6rem 0;
|
||
}
|
||
|
||
strong {
|
||
color: var(--accent2);
|
||
}
|
||
|
||
a {
|
||
color: var(--accent2);
|
||
text-decoration: none;
|
||
}
|
||
|
||
/* Code blocks */
|
||
pre {
|
||
background: var(--bg-code);
|
||
border: 1px solid var(--border);
|
||
border-radius: 6px;
|
||
padding: 0.8rem;
|
||
margin: 0.8rem 0;
|
||
overflow-x: auto;
|
||
-webkit-overflow-scrolling: touch;
|
||
font-size: clamp(0.7rem, 1.8vw, 0.82rem);
|
||
line-height: 1.5;
|
||
white-space: pre;
|
||
word-wrap: normal;
|
||
}
|
||
|
||
/* Override Prism theme to match page palette */
|
||
pre[class*="language-"],
|
||
code[class*="language-"] {
|
||
background: var(--bg-code) !important;
|
||
text-shadow: none !important;
|
||
}
|
||
|
||
pre code {
|
||
background: none !important;
|
||
padding: 0;
|
||
border: none;
|
||
font-size: inherit;
|
||
color: var(--fg);
|
||
}
|
||
|
||
code {
|
||
font-family: 'SF Mono', 'Fira Code', 'Cascadia Code', 'Menlo',
|
||
'Consolas', monospace;
|
||
background: var(--bg-inline);
|
||
padding: 0.15rem 0.35rem;
|
||
border-radius: 3px;
|
||
font-size: 0.88em;
|
||
}
|
||
|
||
/* Pipeline flow diagram */
|
||
.pipeline {
|
||
margin: 1.2rem 0;
|
||
padding: 1rem;
|
||
border: 1px solid var(--border);
|
||
border-radius: 8px;
|
||
background: var(--bg-code);
|
||
}
|
||
|
||
.pipeline-title {
|
||
text-align: center;
|
||
font-weight: 600;
|
||
color: var(--accent2);
|
||
margin-bottom: 1rem;
|
||
font-size: 0.95rem;
|
||
}
|
||
|
||
.pipeline-flow {
|
||
display: flex;
|
||
flex-direction: column;
|
||
align-items: center;
|
||
}
|
||
|
||
.pf-node {
|
||
background: var(--bg);
|
||
border: 1px solid var(--border);
|
||
border-radius: 6px;
|
||
padding: 0.45rem 1.2rem;
|
||
text-align: center;
|
||
font-size: 0.88rem;
|
||
font-weight: 500;
|
||
width: 100%;
|
||
max-width: 14rem;
|
||
}
|
||
|
||
.pf-node small {
|
||
font-size: 0.78rem;
|
||
color: var(--fg-dim);
|
||
font-weight: 400;
|
||
}
|
||
|
||
.pf-node.pf-final {
|
||
border-color: var(--accent);
|
||
color: var(--accent);
|
||
}
|
||
|
||
.pf-edge {
|
||
display: flex;
|
||
flex-direction: column;
|
||
align-items: center;
|
||
padding: 0.15rem 0;
|
||
font-size: 0.75rem;
|
||
color: var(--fg-dim);
|
||
font-style: italic;
|
||
line-height: 1.2;
|
||
}
|
||
|
||
.pf-edge::after {
|
||
content: '\25BC';
|
||
color: var(--accent2);
|
||
font-size: 0.7rem;
|
||
font-style: normal;
|
||
}
|
||
|
||
.pf-gate {
|
||
color: var(--accent);
|
||
font-weight: 600;
|
||
font-style: normal;
|
||
}
|
||
|
||
/* Tables */
|
||
.table-wrapper {
|
||
overflow-x: auto;
|
||
-webkit-overflow-scrolling: touch;
|
||
margin: 0.8rem 0;
|
||
border-radius: 6px;
|
||
}
|
||
|
||
table {
|
||
width: 100%;
|
||
border-collapse: collapse;
|
||
font-size: 0.88rem;
|
||
}
|
||
|
||
th, td {
|
||
border: 1px solid var(--border);
|
||
padding: 0.5rem 0.6rem;
|
||
text-align: left;
|
||
}
|
||
|
||
th {
|
||
background: var(--bg-code);
|
||
font-weight: 600;
|
||
color: var(--accent2);
|
||
white-space: nowrap;
|
||
}
|
||
|
||
td {
|
||
white-space: normal;
|
||
}
|
||
|
||
tr:nth-child(even) {
|
||
background: var(--table-stripe);
|
||
}
|
||
|
||
/* Responsive card tables on mobile */
|
||
@media (max-width: 600px) {
|
||
table.responsive-cards,
|
||
table.responsive-cards thead,
|
||
table.responsive-cards tbody,
|
||
table.responsive-cards tr,
|
||
table.responsive-cards th,
|
||
table.responsive-cards td {
|
||
display: block;
|
||
}
|
||
|
||
table.responsive-cards thead {
|
||
position: absolute;
|
||
width: 1px;
|
||
height: 1px;
|
||
overflow: hidden;
|
||
clip: rect(0, 0, 0, 0);
|
||
}
|
||
|
||
table.responsive-cards tr {
|
||
margin-bottom: 0.8rem;
|
||
border: 1px solid var(--border);
|
||
border-radius: 6px;
|
||
background: var(--bg-code);
|
||
overflow: hidden;
|
||
}
|
||
|
||
table.responsive-cards tr:nth-child(even) {
|
||
background: var(--bg-code);
|
||
}
|
||
|
||
table.responsive-cards td {
|
||
border: none;
|
||
border-bottom: 1px solid var(--border);
|
||
padding: 0.5rem 0.7rem;
|
||
}
|
||
|
||
table.responsive-cards td:last-child {
|
||
border-bottom: none;
|
||
}
|
||
|
||
table.responsive-cards td::before {
|
||
content: attr(data-label);
|
||
display: block;
|
||
font-weight: 600;
|
||
color: var(--accent2);
|
||
font-size: 0.75rem;
|
||
text-transform: uppercase;
|
||
letter-spacing: 0.03em;
|
||
margin-bottom: 0.15rem;
|
||
}
|
||
}
|
||
|
||
/* Simple 2-col tables */
|
||
table.simple-table th,
|
||
table.simple-table td {
|
||
white-space: nowrap;
|
||
}
|
||
|
||
/* Lists */
|
||
ul, ol {
|
||
margin: 0.5rem 0 0.5rem 1.2rem;
|
||
}
|
||
|
||
li {
|
||
margin: 0.3rem 0;
|
||
}
|
||
|
||
li > ul, li > ol {
|
||
margin: 0.2rem 0 0.2rem 1rem;
|
||
}
|
||
|
||
/* Horizontal rules */
|
||
hr {
|
||
border: none;
|
||
border-top: 1px solid var(--border);
|
||
margin: 2rem 0;
|
||
}
|
||
|
||
/* Blockquotes */
|
||
blockquote {
|
||
border-left: 3px solid var(--accent);
|
||
padding: 0.4rem 0.8rem;
|
||
margin: 0.8rem 0;
|
||
color: var(--fg-dim);
|
||
background: var(--bg-code);
|
||
border-radius: 0 4px 4px 0;
|
||
}
|
||
|
||
/* Mobile adjustments */
|
||
@media (max-width: 600px) {
|
||
body {
|
||
padding: 0.6rem;
|
||
}
|
||
|
||
pre {
|
||
padding: 0.6rem;
|
||
border-radius: 4px;
|
||
}
|
||
|
||
table { font-size: 0.82rem; }
|
||
th, td { padding: 0.4rem 0.5rem; }
|
||
}
|
||
|
||
/* Scroll hint for wide content on mobile */
|
||
.scroll-hint {
|
||
text-align: center;
|
||
font-size: 0.72rem;
|
||
color: var(--fg-dim);
|
||
margin-top: -0.4rem;
|
||
margin-bottom: 0.6rem;
|
||
}
|
||
|
||
@media (min-width: 768px) {
|
||
.scroll-hint {
|
||
display: none;
|
||
}
|
||
}
|
||
|
||
/* Print-friendly */
|
||
@media print {
|
||
body { background: white; color: black; }
|
||
pre { border-color: #ccc; background: #f8f8f8; }
|
||
h1 { color: #333; border-color: #333; }
|
||
h2 { color: #555; }
|
||
}
|
||
</style>
|
||
</head>
|
||
<body>
|
||
<article>
|
||
<h1>Pipeline Walkthrough: From L1 Source to x86-64 Execution</h1>
|
||
<p>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.</p>
|
||
<p>The program used is <code>examples/product.l1</code> — a product tracker that accumulates purchase quantities and costs, with an observer that emits the running total after each step.</p>
|
||
<p><strong>Reproducibility.</strong> Every output shown in this document can be regenerated:</p>
|
||
<pre><code class="language-bash">cargo run -- examples/product.l1 --dump-ir # all IRs + hex dump
|
||
cargo run -- examples/product.l1 # execution output
|
||
</code></pre>
|
||
<h2>Pipeline Overview</h2>
|
||
<div class="pipeline">
|
||
<div class="pipeline-title">Compiler Pipeline</div>
|
||
<div class="pipeline-flow">
|
||
<div class="pf-node">DSL Source <small>(.l1)</small></div>
|
||
<div class="pf-edge">Parse</div>
|
||
<div class="pf-node">L1 IR</div>
|
||
<div class="pf-edge pf-gate">Verify (L1)</div>
|
||
<div class="pf-node">L1 IR <small>(verified)</small></div>
|
||
<div class="pf-edge">Emit</div>
|
||
<div class="pf-node">L0 IR</div>
|
||
<div class="pf-edge pf-gate">Verify (L0)</div>
|
||
<div class="pf-node">L0 IR <small>(verified)</small></div>
|
||
<div class="pf-edge">Codegen</div>
|
||
<div class="pf-node">x86-64 Machine Code</div>
|
||
<div class="pf-edge"></div>
|
||
<div class="pf-node pf-final">Execute</div>
|
||
</div>
|
||
</div>
|
||
<p>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.</p>
|
||
<h2>The Source Program</h2>
|
||
<p>The program models a product ledger. Each step, a purchase arrives: 3 units at price 7. The <code>ledger</code> 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.</p>
|
||
<p>After 4 steps, the expected state is:</p>
|
||
<ul>
|
||
<li><code>count</code> = 12 (4 purchases × 3 units each)</li>
|
||
<li><code>total</code> = 84 (4 × (7 × 3) = 4 × 21)</li>
|
||
<li>Emitted values: [21, 42, 63, 84] — the running total after each step</li>
|
||
</ul>
|
||
<pre><code class="language-clike">// 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
|
||
}
|
||
</code></pre>
|
||
<p>The key DSL concepts at work:</p>
|
||
<ul>
|
||
<li><strong>Actor</strong> (<code>ledger</code>): Owns mutable state. Processes messages one at a time, serialized. State fields <code>count</code> and <code>total</code> are typed (<code>u64</code>) and initialized to zero.</li>
|
||
<li><strong>Window</strong> (<code>summary</code>): Grants read-only access to a subset of actor state. The <code>report</code> leaf can read <code>count</code> and <code>total</code> through this window, but cannot write to them. Safety requires that readers and the actor's message handler never execute concurrently.</li>
|
||
<li><strong>Leaves</strong> (<code>buy</code>, <code>report</code>): Stateless processors. <code>buy</code> forwards a <code>Purchase</code> message to the actor. <code>report</code> reads state through the window and emits the total as observable output.</li>
|
||
<li><strong>Pipeline</strong> (<code>main</code>): An ordered execution chain — <code>buy → ledger → report</code>. Each step, the pipeline executes left to right: the leaf sends a message, the actor processes it, the observer reads the result.</li>
|
||
<li><strong>Core</strong> (<code>main</code>): The execution schedule. Declares which actors, leaves, and pipelines participate, and bounds execution to exactly 4 steps.</li>
|
||
</ul>
|
||
<h2>L1 IR</h2>
|
||
<p>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.</p>
|
||
<pre><code class="language-clike">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
|
||
}
|
||
</code></pre>
|
||
<p>What parsing resolved:</p>
|
||
<ul>
|
||
<li><strong>Structural normalization.</strong> The actor's state block, window declarations, and message handlers are parsed into distinct typed structures. The handler body <code>count = count + qty</code> / <code>total = total + (price * qty)</code> becomes an explicit block of assignment expressions with nested arithmetic nodes.</li>
|
||
<li><strong>Name binding.</strong> Every reference — the leaf's <code>forward(ledger, ...)</code>, the window's <code>readers(report)</code>, the pipeline's <code>buy -> ledger -> report</code>, 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.</li>
|
||
<li><strong>Syntactic sugar dissolved.</strong> The <code>process { ... }</code> 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.</li>
|
||
</ul>
|
||
<p>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.</p>
|
||
<h2>L1 Verification</h2>
|
||
<p>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.</p>
|
||
<p>The checks, mapped to the spec's four property categories:</p>
|
||
<div class="table-wrapper">
|
||
<table class="responsive-cards">
|
||
<thead>
|
||
<tr>
|
||
<th>Property</th>
|
||
<th>Check</th>
|
||
<th>What it catches</th>
|
||
</tr>
|
||
</thead>
|
||
<tbody><tr>
|
||
<td data-label="Property"><strong>Safety</strong></td>
|
||
<td data-label="Check">Ref resolution</td>
|
||
<td data-label="What it catches">Every name in cores, pipelines, windows, and leaf actions resolves to a declared actor, leaf, or pipeline. Catches dangling references — a <code>forward</code> to a non-existent actor, a window naming a non-existent reader, a pipeline referencing an undeclared entity.</td>
|
||
</tr>
|
||
<tr>
|
||
<td data-label="Property"><strong>Safety</strong></td>
|
||
<td data-label="Check">Exclusive ownership</td>
|
||
<td data-label="What it catches">Each actor and leaf belongs to exactly one core. Prevents the same entity from being claimed by two different execution contexts.</td>
|
||
</tr>
|
||
<tr>
|
||
<td data-label="Property"><strong>Safety</strong></td>
|
||
<td data-label="Check">Window separation</td>
|
||
<td data-label="What it catches">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.</td>
|
||
</tr>
|
||
<tr>
|
||
<td data-label="Property"><strong>Consistency</strong></td>
|
||
<td data-label="Check">Pipeline well-formedness</td>
|
||
<td data-label="What it catches">Every pipeline has at least 2 stages. No stage appears twice within a pipeline (which would indicate a cycle).</td>
|
||
</tr>
|
||
<tr>
|
||
<td data-label="Property"><strong>Liveness</strong></td>
|
||
<td data-label="Check">Buffer conservation</td>
|
||
<td data-label="What it catches">Every leaf has at least one action (forward, read, or emit). A leaf with no actions would mean its input is never consumed.</td>
|
||
</tr>
|
||
<tr>
|
||
<td data-label="Property"><strong>Resource bound</strong></td>
|
||
<td data-label="Check">Finiteness</td>
|
||
<td data-label="What it catches">Every core has <code>steps > 0</code>. 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.</td>
|
||
</tr>
|
||
</tbody></table>
|
||
</div>
|
||
<p>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.</p>
|
||
<h2>L0 IR</h2>
|
||
<p>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.</p>
|
||
<pre><code>=== 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
|
||
</code></pre>
|
||
<p class="scroll-hint">Swipe to scroll wide content</p>
|
||
<p>Here is what happened to each L1 concept:</p>
|
||
<p><strong>Actors became regions.</strong> The actor <code>ledger</code> with state fields <code>count: u64 = 0</code> and <code>total: u64 = 0</code> became <code>region ledger_state : 16 bytes, rw, state</code> — 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: <code>store.64 ledger_state[0]</code> writes the count field, <code>store.64 ledger_state[8]</code> writes the total field.</p>
|
||
<p><strong>Messages became queues.</strong> The <code>forward(ledger, Purchase(7, 3))</code> in the <code>buy</code> leaf became two <code>queue_push</code> operations — one for each argument (price=7, qty=3) — into <code>region ledger_purchase_queue : 272 bytes, rw, queue</code>. The actor's <code>on Purchase(price, qty)</code> handler became two <code>queue_pop</code> 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.</p>
|
||
<p><strong>The pipeline became a loop.</strong> The <code>steps: 4</code> in the core schedule became <code>region step_counter : 8 bytes, rw, control</code>, a <code>loop_check</code> block with <code>cmp.lt</code> 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 <code>loop_check</code>.</p>
|
||
<p><strong>Window reads became loads.</strong> The <code>report</code> leaf's <code>read(ledger.summary.total)</code> became <code>r13 = load.64 ledger_state[8]</code> — 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.</p>
|
||
<p><strong>Emit became a queue push.</strong> The <code>emit(total)</code> became <code>queue_push output, r14</code> — pushing the loaded total value into <code>region output : 48 bytes, rw, output</code>. The output region is sized for exactly 4 steps: 16 bytes header + 4 × 8 bytes data = 48 bytes.</p>
|
||
<p><strong>Everything became explicit.</strong> 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.</p>
|
||
<p>Walking through the blocks:</p>
|
||
<ul>
|
||
<li><strong><code>entry</code></strong>: Loads immediate 0, stores it to both state fields (<code>ledger_state[0]</code> and <code>[8]</code>), the step counter, and the output head. Jumps to <code>loop_check</code>.</li>
|
||
<li><strong><code>loop_check</code></strong>: Loads the step counter, loads the bound (4), compares. Branches to <code>step</code> if counter < 4, otherwise to <code>exit</code>.</li>
|
||
<li><strong><code>step</code></strong>: 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 <code>loop_check</code>.</li>
|
||
<li><strong><code>exit</code></strong>: Terminates execution.</li>
|
||
</ul>
|
||
<h2>L0 Verification</h2>
|
||
<p>L0 verification checks the concrete IR after emission, before codegen. It collects all errors (unlike L1 verification which stops at the first). The checks:</p>
|
||
<div class="table-wrapper">
|
||
<table class="responsive-cards">
|
||
<thead>
|
||
<tr>
|
||
<th>Property</th>
|
||
<th>Check</th>
|
||
<th>What it catches</th>
|
||
</tr>
|
||
</thead>
|
||
<tbody><tr>
|
||
<td data-label="Property"><strong>Safety</strong></td>
|
||
<td data-label="Check">Control flow targets</td>
|
||
<td data-label="What it catches">Every <code>branch</code> and <code>jump</code> names a block that exists. A dangling target would mean the program jumps into the void.</td>
|
||
</tr>
|
||
<tr>
|
||
<td data-label="Property"><strong>Safety</strong></td>
|
||
<td data-label="Check">Block reachability</td>
|
||
<td data-label="What it catches">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.</td>
|
||
</tr>
|
||
<tr>
|
||
<td data-label="Property"><strong>Safety</strong></td>
|
||
<td data-label="Check">Region declarations</td>
|
||
<td data-label="What it catches">Every <code>load</code> and <code>store</code> names a region that is declared in the regions list. An undeclared region reference would mean accessing memory that doesn't exist.</td>
|
||
</tr>
|
||
<tr>
|
||
<td data-label="Property"><strong>Safety</strong></td>
|
||
<td data-label="Check">Region bounds</td>
|
||
<td data-label="What it catches">Every memory access satisfies <code>offset + access_size ≤ region_size</code>. Out-of-bounds access would read or write past the region boundary.</td>
|
||
</tr>
|
||
<tr>
|
||
<td data-label="Property"><strong>Safety</strong></td>
|
||
<td data-label="Check">Access mode</td>
|
||
<td data-label="What it catches">Stores to read-only regions are rejected. The access mode is a compile-time invariant that codegen can rely on.</td>
|
||
</tr>
|
||
<tr>
|
||
<td data-label="Property"><strong>Resource bound</strong></td>
|
||
<td data-label="Check">Queue safety</td>
|
||
<td data-label="What it catches"><code>queue_push</code> and <code>queue_pop</code> only operate on regions with queue or output kind. Using queue operations on a state or control region would corrupt its layout.</td>
|
||
</tr>
|
||
<tr>
|
||
<td data-label="Property"><strong>Resource bound</strong></td>
|
||
<td data-label="Check">Memory capacity</td>
|
||
<td data-label="What it catches">Total memory is bounded — every region has a fixed size, and all sizes are known at compile time. The <code>total_memory()</code> utility sums all region sizes (in this program: 16 + 272 + 8 + 48 = 344 bytes).</td>
|
||
</tr>
|
||
</tbody></table>
|
||
</div>
|
||
<p>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.</p>
|
||
<h2>x86-64 Machine Code</h2>
|
||
<p>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.</p>
|
||
<h3>Raw hex dump</h3>
|
||
<pre><code>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
|
||
</code></pre>
|
||
<p>491 bytes of x86-64 machine code.</p>
|
||
<h3>Annotated disassembly</h3>
|
||
<p>The generated function follows the System V AMD64 calling convention. It receives a single argument in <code>rdi</code>: a pointer to an array of region base addresses. Region bases are loaded into dedicated registers at entry:</p>
|
||
<div class="table-wrapper">
|
||
<table class="simple-table">
|
||
<thead>
|
||
<tr>
|
||
<th>Register</th>
|
||
<th>Region</th>
|
||
</tr>
|
||
</thead>
|
||
<tbody><tr>
|
||
<td>R12</td>
|
||
<td><code>ledger_state</code> (16 bytes, state)</td>
|
||
</tr>
|
||
<tr>
|
||
<td>R13</td>
|
||
<td><code>ledger_purchase_queue</code> (272 bytes, queue)</td>
|
||
</tr>
|
||
<tr>
|
||
<td>R14</td>
|
||
<td><code>step_counter</code> (8 bytes, control)</td>
|
||
</tr>
|
||
<tr>
|
||
<td>R15</td>
|
||
<td><code>output</code> (48 bytes, output)</td>
|
||
</tr>
|
||
</tbody></table>
|
||
</div>
|
||
<p>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.</p>
|
||
<pre><code class="language-nasm">; === 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
|
||
</code></pre>
|
||
<p class="scroll-hint">Swipe to scroll wide content</p>
|
||
<p><strong>Codegen strategy:</strong></p>
|
||
<ul>
|
||
<li><p><strong>Regions become register-indirect memory.</strong> 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: <code>mov [r12+0x08], rax</code> writes to <code>ledger_state</code> at offset 8 (the <code>total</code> field). Named regions preserve aliasing knowledge all the way to machine code — the codegen knows that <code>[r12+0x00]</code> and <code>[r14+0x00]</code> can never alias because they point to different regions.</p>
|
||
</li>
|
||
<li><p><strong>Block structure maps to jump targets.</strong> The L0 blocks (<code>entry</code>, <code>loop_check</code>, <code>step</code>, <code>exit</code>) become contiguous instruction sequences with <code>jmp</code>/<code>jne</code> 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.</p>
|
||
</li>
|
||
<li><p><strong>Queue operations translate to ring buffer indexing.</strong> Each <code>queue_push</code> becomes: load head from <code>[base+0]</code>, compute slot address as <code>base + 16 + head*8</code>, store the value, increment head, store head back. <code>queue_pop</code> does the same with tail at <code>[base+8]</code>. The pattern is identical every time — five instructions for each queue operation.</p>
|
||
</li>
|
||
<li><p><strong>Arithmetic is direct.</strong> <code>add</code> → <code>add</code>, <code>mul</code> → <code>imul</code>. The move-then-operate pattern (<code>mov rax, r11; add rax, r10</code>) 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.</p>
|
||
</li>
|
||
<li><p><strong>Comparisons use <code>setcc</code> + <code>movzx</code>.</strong> The <code>cmp.lt</code> operation becomes <code>cmp rcx, rdx; setl bl; movzx rbx, bl</code> — compare, set a byte flag, zero-extend to 64 bits. The result feeds into <code>test rbx, rbx; jne</code> for the conditional branch.</p>
|
||
</li>
|
||
</ul>
|
||
<h2>Execution</h2>
|
||
<p>Running the program produces:</p>
|
||
<pre><code>Execution complete.
|
||
step_counter[0] = 4
|
||
output[0] = 4
|
||
ledger_state[0] = 12
|
||
ledger_purchase_queue[0] = 8
|
||
output values: [21, 42, 63, 84]
|
||
</code></pre>
|
||
<p>Interpreting the results:</p>
|
||
<ul>
|
||
<li><strong><code>ledger_state[0] = 12</code></strong>: The <code>count</code> field. 4 steps × 3 units per step = 12. Correct.</li>
|
||
<li><strong><code>step_counter[0] = 4</code></strong>: The loop ran exactly 4 iterations. Correct.</li>
|
||
<li><strong><code>ledger_purchase_queue[0] = 8</code></strong>: The queue head advanced 8 positions (2 pushes per step × 4 steps). Correct.</li>
|
||
<li><strong><code>output[0] = 4</code></strong>: The output head — 4 values were emitted. Correct.</li>
|
||
<li><strong><code>output values: [21, 42, 63, 84]</code></strong>: The running total after each step:<ul>
|
||
<li>Step 1: 0 + (7 × 3) = 21</li>
|
||
<li>Step 2: 21 + 21 = 42</li>
|
||
<li>Step 3: 42 + 21 = 63</li>
|
||
<li>Step 4: 63 + 21 = 84</li>
|
||
</ul>
|
||
</li>
|
||
</ul>
|
||
<p>Every value matches the program's intent. The total field (at <code>ledger_state[8]</code>, not shown in the summary line but readable from the region) holds 84. The loop from source intent to machine execution is closed.</p>
|
||
<h2>Closing</h2>
|
||
<p>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.</p>
|
||
<p>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.</p>
|
||
<p>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.</p>
|
||
|
||
</article>
|
||
<script src="https://cdn.jsdelivr.net/npm/prismjs@1.29.0/prism.min.js"></script>
|
||
<script src="https://cdn.jsdelivr.net/npm/prismjs@1.29.0/components/prism-nasm.min.js"></script>
|
||
<script src="https://cdn.jsdelivr.net/npm/prismjs@1.29.0/components/prism-bash.min.js"></script>
|
||
</body>
|
||
</html>
|