965 lines
30 KiB
HTML
965 lines
30 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>Formal Verification Pipeline: Proving L1→L0 Lowering Correctness</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;
|
|
--pass: #4ec9b0;
|
|
--fail: #e94560;
|
|
}
|
|
|
|
* { 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-node.pf-pass {
|
|
border-color: var(--pass);
|
|
color: var(--pass);
|
|
}
|
|
|
|
.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;
|
|
}
|
|
|
|
/* Verification result boxes */
|
|
.verify-box {
|
|
border: 1px solid var(--border);
|
|
border-radius: 8px;
|
|
margin: 1rem 0;
|
|
overflow: hidden;
|
|
}
|
|
|
|
.verify-header {
|
|
padding: 0.5rem 0.8rem;
|
|
font-weight: 600;
|
|
font-size: 0.9rem;
|
|
display: flex;
|
|
justify-content: space-between;
|
|
align-items: center;
|
|
}
|
|
|
|
.verify-header.pass {
|
|
background: rgba(78, 201, 176, 0.15);
|
|
border-bottom: 1px solid rgba(78, 201, 176, 0.3);
|
|
color: var(--pass);
|
|
}
|
|
|
|
.verify-body {
|
|
padding: 0.6rem 0.8rem;
|
|
background: var(--bg-code);
|
|
font-size: 0.85rem;
|
|
}
|
|
|
|
.verify-body p {
|
|
margin: 0.3rem 0;
|
|
}
|
|
|
|
.check-pass {
|
|
color: var(--pass);
|
|
}
|
|
|
|
.check-fail {
|
|
color: var(--fail);
|
|
}
|
|
|
|
.tradition {
|
|
font-style: italic;
|
|
color: var(--fg-dim);
|
|
margin: 0.3rem 0 0.6rem;
|
|
font-size: 0.88rem;
|
|
}
|
|
|
|
/* 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>Formal Verification Pipeline: Proving L1→L0 Lowering Correctness</h1>
|
|
|
|
<p>This document walks through the formal verification pipeline that proves the L1→L0 compilation preserves semantics. Three verification tools — inspired by real-world formal methods — examine the lowering from different angles. Together, they provide strong evidence that the compiler does what it claims.</p>
|
|
|
|
<p>The program used is <code>examples/product.l1</code> — a product tracker with multi-field state, compound arithmetic, and observable output. It exercises every DSL feature: actors, windows, message handlers, leaves, pipelines, and bounded execution.</p>
|
|
|
|
<p><strong>Reproducibility.</strong> Every output shown here can be regenerated:</p>
|
|
<pre><code class="language-bash">cargo run -- verify examples/product.l1 # full verification pipeline
|
|
cargo run -- examples/product.l1 # execution output
|
|
cargo run -- examples/product.l1 --dump-ir # all IRs + hex dump
|
|
</code></pre>
|
|
|
|
<h2>Pipeline Overview</h2>
|
|
|
|
<div class="pipeline">
|
|
<div class="pipeline-title">Verification 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 pf-gate">Translation Validation</div>
|
|
<div class="pf-node pf-pass">Verification Report</div>
|
|
</div>
|
|
</div>
|
|
|
|
<p>After the standard L0 verification gate passes, the translation validation phase runs three independent verification tools. All three must pass for the translation to be considered correct.</p>
|
|
|
|
<h2>The Example Program</h2>
|
|
|
|
<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 {
|
|
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>After 4 steps: <code>count</code> = 12, <code>total</code> = 84, emitted values = [21, 42, 63, 84].</p>
|
|
|
|
<p>This program exercises every verification-relevant feature:</p>
|
|
<ul>
|
|
<li><strong>Multi-field state</strong> — two fields at different offsets, both mutated per step</li>
|
|
<li><strong>Compound arithmetic</strong> — <code>price * qty</code> nested inside an addition</li>
|
|
<li><strong>Window reads</strong> — a leaf reading actor state through a read-only window</li>
|
|
<li><strong>Observable output</strong> — emitted values that both L1 and L0 must agree on</li>
|
|
</ul>
|
|
|
|
<hr>
|
|
|
|
<h2>Tool 1: L1 Reference Interpreter</h2>
|
|
|
|
<p class="tradition">Tradition: CompCert’s translation validation requires a reference semantics — a definition of what the source program means, independent of the compiler.</p>
|
|
|
|
<p>The L1 reference interpreter executes L1 IR directly, without lowering to L0. It steps through pipeline stages, dispatches messages to actor handlers, updates state, reads windows, and collects emitted outputs. The interpreter <em>is</em> the specification: if L0 execution produces the same observable trace, the lowering preserved semantics.</p>
|
|
|
|
<h3>Execution trace for product.l1</h3>
|
|
|
|
<pre><code>--- Step 0 ---
|
|
send Purchase([7, 3]) -> ledger
|
|
read ledger.summary.total = 21
|
|
emit 21
|
|
ledger { count=3, total=21 }
|
|
--- Step 1 ---
|
|
send Purchase([7, 3]) -> ledger
|
|
read ledger.summary.total = 42
|
|
emit 42
|
|
ledger { count=6, total=42 }
|
|
--- Step 2 ---
|
|
send Purchase([7, 3]) -> ledger
|
|
read ledger.summary.total = 63
|
|
emit 63
|
|
ledger { count=9, total=63 }
|
|
--- Step 3 ---
|
|
send Purchase([7, 3]) -> ledger
|
|
read ledger.summary.total = 84
|
|
emit 84
|
|
ledger { count=12, total=84 }
|
|
--- Final ---
|
|
ledger { count=12, total=84 }
|
|
outputs: [21, 42, 63, 84]
|
|
</code></pre>
|
|
|
|
<p>Each step follows pipeline order: <code>buy</code> forwards <code>Purchase(7, 3)</code> to <code>ledger</code>, the actor processes it (multiplying price × qty and accumulating), then <code>report</code> reads the updated total through the window and emits it. State evolves deterministically: count increments by 3 each step, total by 21.</p>
|
|
|
|
<h3>Operational semantics</h3>
|
|
|
|
<p>The interpreter’s step function:</p>
|
|
<ol>
|
|
<li>For each pipeline in the core’s pipeline list:</li>
|
|
<li>Walk stages left to right.</li>
|
|
<li>If the stage is a <strong>leaf</strong>: execute its actions (forward messages, read windows, emit outputs).</li>
|
|
<li>If the stage is an <strong>actor</strong>: pop messages from its queue and execute matching handlers.</li>
|
|
<li>After all pipelines complete: record the trace step (state snapshot, messages, reads, outputs).</li>
|
|
</ol>
|
|
|
|
<p>This is the <em>reference semantics</em>. Any correct lowering must produce the same final state and the same output sequence.</p>
|
|
|
|
<hr>
|
|
|
|
<h2>Tool 2: Trace Equivalence Checker</h2>
|
|
|
|
<p class="tradition">Tradition: CompCert’s verified C compiler uses translation validation — running both the source semantics and the compiled output on the same input, then comparing observable behavior.</p>
|
|
|
|
<p>The trace equivalence checker runs the L1 reference interpreter and the L0 codegen+execution on the same program, then compares final actor states field by field and emitted output sequences element by element.</p>
|
|
|
|
<h3>Side-by-side comparison for product.l1</h3>
|
|
|
|
<div class="table-wrapper">
|
|
<table class="responsive-cards">
|
|
<thead>
|
|
<tr>
|
|
<th>Observable</th>
|
|
<th>L1 Interpreter</th>
|
|
<th>L0 Execution</th>
|
|
<th>Match</th>
|
|
</tr>
|
|
</thead>
|
|
<tbody>
|
|
<tr>
|
|
<td data-label="Observable"><code>ledger.count</code> (final)</td>
|
|
<td data-label="L1 Interpreter">12</td>
|
|
<td data-label="L0 Execution"><code>ledger_state[0]</code> = 12</td>
|
|
<td data-label="Match"><span class="check-pass">✓</span></td>
|
|
</tr>
|
|
<tr>
|
|
<td data-label="Observable"><code>ledger.total</code> (final)</td>
|
|
<td data-label="L1 Interpreter">84</td>
|
|
<td data-label="L0 Execution"><code>ledger_state[8]</code> = 84</td>
|
|
<td data-label="Match"><span class="check-pass">✓</span></td>
|
|
</tr>
|
|
<tr>
|
|
<td data-label="Observable">Output[0]</td>
|
|
<td data-label="L1 Interpreter">21</td>
|
|
<td data-label="L0 Execution">21</td>
|
|
<td data-label="Match"><span class="check-pass">✓</span></td>
|
|
</tr>
|
|
<tr>
|
|
<td data-label="Observable">Output[1]</td>
|
|
<td data-label="L1 Interpreter">42</td>
|
|
<td data-label="L0 Execution">42</td>
|
|
<td data-label="Match"><span class="check-pass">✓</span></td>
|
|
</tr>
|
|
<tr>
|
|
<td data-label="Observable">Output[2]</td>
|
|
<td data-label="L1 Interpreter">63</td>
|
|
<td data-label="L0 Execution">63</td>
|
|
<td data-label="Match"><span class="check-pass">✓</span></td>
|
|
</tr>
|
|
<tr>
|
|
<td data-label="Observable">Output[3]</td>
|
|
<td data-label="L1 Interpreter">84</td>
|
|
<td data-label="L0 Execution">84</td>
|
|
<td data-label="Match"><span class="check-pass">✓</span></td>
|
|
</tr>
|
|
</tbody>
|
|
</table>
|
|
</div>
|
|
|
|
<div class="verify-box">
|
|
<div class="verify-header pass"><span>Trace Equivalence</span> <span>PASS</span></div>
|
|
<div class="verify-body">
|
|
<p>Outputs match: 4 values. Final states agree across 1 actor.</p>
|
|
</div>
|
|
</div>
|
|
|
|
<h3>What it catches</h3>
|
|
|
|
<p>If the emitter generated <code>Sub</code> instead of <code>Add</code> for the handler’s <code>count = count + qty</code>:</p>
|
|
<ul>
|
|
<li>L1 interpreter would compute <code>count = 0 + 3 = 3</code> at step 0</li>
|
|
<li>L0 execution would compute <code>count = 0 - 3 = 18446744073709551613</code> (wrapping subtraction)</li>
|
|
<li>Diagnostic: <code>"final state mismatch: ledger.count = 3 (L1) vs 18446744073709551613 (L0)"</code></li>
|
|
</ul>
|
|
|
|
<p>This is not hypothetical — the test suite includes a deliberate corruption test that verifies this exact scenario.</p>
|
|
|
|
<h3>How it differs from CompCert</h3>
|
|
|
|
<p>CompCert’s translation validation runs on each compilation pass independently, with pass-specific simulation relations. Our version is end-to-end: L1 interpreter vs. final x86-64 execution. This is coarser (it can’t pinpoint <em>which</em> pass introduced a bug) but simpler and catches any bug that affects observable behavior, regardless of which compilation stage introduced it.</p>
|
|
|
|
<hr>
|
|
|
|
<h2>Tool 3: Structural Correspondence Checker</h2>
|
|
|
|
<p class="tradition">Tradition: Refinement type systems (Liquid Haskell, F*) prove that a concrete implementation refines an abstract specification by establishing a correspondence between abstract and concrete types.</p>
|
|
|
|
<p>The structural checker walks L1 IR and L0 IR in parallel, verifying structural invariants. Unlike the trace checker (which tests specific inputs), the structural checker verifies properties that hold for <em>all</em> inputs to the program.</p>
|
|
|
|
<h3>Check 1: Actor state → L0 region mapping</h3>
|
|
|
|
<div class="table-wrapper">
|
|
<table class="responsive-cards">
|
|
<thead>
|
|
<tr>
|
|
<th>L1 Field</th>
|
|
<th>L0 Region</th>
|
|
<th>Offset</th>
|
|
<th>Init Store</th>
|
|
<th>Status</th>
|
|
</tr>
|
|
</thead>
|
|
<tbody>
|
|
<tr>
|
|
<td data-label="L1 Field"><code>ledger.count</code> : u64</td>
|
|
<td data-label="L0 Region"><code>ledger_state</code> (State, 16 bytes)</td>
|
|
<td data-label="Offset">0</td>
|
|
<td data-label="Init Store"><code>store.64 ledger_state[0], r0</code></td>
|
|
<td data-label="Status"><span class="check-pass">✓</span></td>
|
|
</tr>
|
|
<tr>
|
|
<td data-label="L1 Field"><code>ledger.total</code> : u64</td>
|
|
<td data-label="L0 Region"><code>ledger_state</code> (State, 16 bytes)</td>
|
|
<td data-label="Offset">8</td>
|
|
<td data-label="Init Store"><code>store.64 ledger_state[8], r0</code></td>
|
|
<td data-label="Status"><span class="check-pass">✓</span></td>
|
|
</tr>
|
|
</tbody>
|
|
</table>
|
|
</div>
|
|
|
|
<h3>Check 2: Handler → queue_pop + arithmetic</h3>
|
|
|
|
<div class="table-wrapper">
|
|
<table class="responsive-cards">
|
|
<thead>
|
|
<tr>
|
|
<th>L1 Handler</th>
|
|
<th>L0 Queue Region</th>
|
|
<th>Args</th>
|
|
<th>Pops</th>
|
|
<th>Arith (L1)</th>
|
|
<th>Arith (L0)</th>
|
|
</tr>
|
|
</thead>
|
|
<tbody>
|
|
<tr>
|
|
<td data-label="L1 Handler"><code>ledger.on Purchase</code></td>
|
|
<td data-label="L0 Queue Region"><code>ledger_purchase_queue</code> (Queue)</td>
|
|
<td data-label="Args">2</td>
|
|
<td data-label="Pops">2 <span class="check-pass">✓</span></td>
|
|
<td data-label="Arith (L1)">3</td>
|
|
<td data-label="Arith (L0)">≥3 <span class="check-pass">✓</span></td>
|
|
</tr>
|
|
</tbody>
|
|
</table>
|
|
</div>
|
|
|
|
<h3>Check 3: Leaf forward → queue_push</h3>
|
|
|
|
<div class="table-wrapper">
|
|
<table class="simple-table">
|
|
<thead>
|
|
<tr><th>L1 Leaf</th><th>Forward Target</th><th>L0 Queue Push</th><th>Status</th></tr>
|
|
</thead>
|
|
<tbody>
|
|
<tr><td><code>buy</code></td><td><code>ledger</code></td><td><code>queue_push ledger_purchase_queue</code></td><td><span class="check-pass">✓</span></td></tr>
|
|
</tbody>
|
|
</table>
|
|
</div>
|
|
|
|
<h3>Check 4: Window read → state region load</h3>
|
|
|
|
<div class="table-wrapper">
|
|
<table class="simple-table">
|
|
<thead>
|
|
<tr><th>L1 Leaf</th><th>Window Read</th><th>L0 Load</th><th>Status</th></tr>
|
|
</thead>
|
|
<tbody>
|
|
<tr><td><code>report</code></td><td><code>ledger.summary.total</code></td><td><code>load.64 ledger_state[8]</code></td><td><span class="check-pass">✓</span></td></tr>
|
|
</tbody>
|
|
</table>
|
|
</div>
|
|
|
|
<h3>Checks 5–7: Emit, control structure, step counter</h3>
|
|
|
|
<div class="table-wrapper">
|
|
<table class="simple-table">
|
|
<thead>
|
|
<tr><th>Check</th><th>Expected</th><th>Found</th><th>Status</th></tr>
|
|
</thead>
|
|
<tbody>
|
|
<tr><td>Emit → Output region</td><td><code>region output</code> of kind Output</td><td>Present</td><td><span class="check-pass">✓</span></td></tr>
|
|
<tr><td>Control blocks</td><td>entry, loop_check, step, exit</td><td>All present</td><td><span class="check-pass">✓</span></td></tr>
|
|
<tr><td>Step counter</td><td><code>step_counter</code> region (Control)</td><td>Present</td><td><span class="check-pass">✓</span></td></tr>
|
|
</tbody>
|
|
</table>
|
|
</div>
|
|
|
|
<div class="verify-box">
|
|
<div class="verify-header pass"><span>Structural Correspondence</span> <span>PASS</span></div>
|
|
<div class="verify-body">
|
|
<p>All structural invariants verified. Every L1 construct maps to the expected L0 structure.</p>
|
|
</div>
|
|
</div>
|
|
|
|
<h3>What it catches vs. trace equivalence</h3>
|
|
|
|
<p>The trace checker catches bugs that manifest on a specific input. The structural checker catches <em>classes</em> of bugs:</p>
|
|
<ul>
|
|
<li>A missing state field initialization (no <code>store</code> in <code>entry</code> for a field)</li>
|
|
<li>A wrong queue region kind (using <code>State</code> instead of <code>Queue</code>)</li>
|
|
<li>A mismatched argument count (handler expects 2 args but only 1 <code>queue_pop</code>)</li>
|
|
<li>A missing control block (no <code>loop_check</code> means no bounded execution)</li>
|
|
</ul>
|
|
|
|
<hr>
|
|
|
|
<h2>Tool 4: Bounded State Space Explorer</h2>
|
|
|
|
<p class="tradition">Tradition: CBMC (bounded model checking for C) exhaustively explores all reachable states within a finite bound. Our bounded explorer exploits the fact that L1 programs have inherently finite state spaces.</p>
|
|
|
|
<p>The bounded explorer runs the L1 interpreter through all steps, collecting every unique actor state. It then verifies that all L0 blocks are reachable, all L0 regions are accessed, the loop limit matches, and control flow is well-formed.</p>
|
|
|
|
<h3>State space enumeration for product.l1</h3>
|
|
|
|
<div class="table-wrapper">
|
|
<table class="responsive-cards">
|
|
<thead>
|
|
<tr>
|
|
<th>Step</th>
|
|
<th>ledger.count</th>
|
|
<th>ledger.total</th>
|
|
<th>State ID</th>
|
|
</tr>
|
|
</thead>
|
|
<tbody>
|
|
<tr>
|
|
<td data-label="Step">(init)</td>
|
|
<td data-label="ledger.count">0</td>
|
|
<td data-label="ledger.total">0</td>
|
|
<td data-label="State ID">S0</td>
|
|
</tr>
|
|
<tr>
|
|
<td data-label="Step">0</td>
|
|
<td data-label="ledger.count">3</td>
|
|
<td data-label="ledger.total">21</td>
|
|
<td data-label="State ID">S1</td>
|
|
</tr>
|
|
<tr>
|
|
<td data-label="Step">1</td>
|
|
<td data-label="ledger.count">6</td>
|
|
<td data-label="ledger.total">42</td>
|
|
<td data-label="State ID">S2</td>
|
|
</tr>
|
|
<tr>
|
|
<td data-label="Step">2</td>
|
|
<td data-label="ledger.count">9</td>
|
|
<td data-label="ledger.total">63</td>
|
|
<td data-label="State ID">S3</td>
|
|
</tr>
|
|
<tr>
|
|
<td data-label="Step">3</td>
|
|
<td data-label="ledger.count">12</td>
|
|
<td data-label="ledger.total">84</td>
|
|
<td data-label="State ID">S4</td>
|
|
</tr>
|
|
</tbody>
|
|
</table>
|
|
</div>
|
|
|
|
<h3>Exploration statistics</h3>
|
|
|
|
<div class="table-wrapper">
|
|
<table class="simple-table">
|
|
<thead>
|
|
<tr><th>Metric</th><th>Value</th></tr>
|
|
</thead>
|
|
<tbody>
|
|
<tr><td>States explored</td><td>5</td></tr>
|
|
<tr><td>L0 blocks reached</td><td>4/4 (100%)</td></tr>
|
|
<tr><td>L0 regions used</td><td>4/4 (100%)</td></tr>
|
|
<tr><td>L0 loop limit</td><td>4 (matches L1 core steps <span class="check-pass">✓</span>)</td></tr>
|
|
<tr><td>Exit block has <code>Terminate</code></td><td><span class="check-pass">✓</span></td></tr>
|
|
<tr><td>Control flow well-formed</td><td><span class="check-pass">✓</span></td></tr>
|
|
</tbody>
|
|
</table>
|
|
</div>
|
|
|
|
<div class="verify-box">
|
|
<div class="verify-header pass"><span>Bounded Model Check</span> <span>PASS</span></div>
|
|
<div class="verify-body">
|
|
<p>5 unique states explored across 4 steps. All 4 L0 blocks reachable, all 4 regions accessed. Bounded execution verified.</p>
|
|
</div>
|
|
</div>
|
|
|
|
<h3>Why bounded model checking works here</h3>
|
|
|
|
<p>Traditional bounded model checkers like CBMC handle arbitrary C programs with unbounded loops, dynamic memory, and pointer arithmetic — requiring SAT/SMT solvers. Our DSL is fundamentally different:</p>
|
|
<ul>
|
|
<li><strong>Execution is bounded by construction.</strong> The <code>steps: N</code> declaration means the program always terminates in exactly N iterations. No SAT solver needed.</li>
|
|
<li><strong>State is finite and small.</strong> Actor fields are typed (<code>u64</code>) and initialized with known values. With known constant inputs each step, the state at step N is fully determined.</li>
|
|
<li><strong>The state space is tractable.</strong> For product.l1: 5 states (init + 4 steps). The “bounded” model check is actually a <em>complete</em> check — there are no states outside the bound.</li>
|
|
</ul>
|
|
|
|
<hr>
|
|
|
|
<h2>Verification Report</h2>
|
|
|
|
<p>Running <code>cargo run -- verify examples/product.l1</code> produces:</p>
|
|
|
|
<pre><code>=== Translation Validation Report ===
|
|
[PASS] Trace Equivalence
|
|
[Trace Equivalence] INFO: outputs match: 4 values, final states agree across 1 actors
|
|
[PASS] Structural Correspondence
|
|
[Structural Correspondence] INFO: all structural invariants verified
|
|
[PASS] Bounded Model Check
|
|
[Bounded Model Check] INFO: explored 5 unique states across 4 steps
|
|
[Bounded Model Check] INFO: L0 loop limit (4) matches L1 core steps
|
|
[Bounded Model Check] INFO: all 4 L0 blocks reachable, all 4 regions accessed, bounded execution verified
|
|
--- Field Mappings ---
|
|
ledger.count -> ledger_state[0]
|
|
ledger.total -> ledger_state[8]
|
|
--- Exploration Stats ---
|
|
states explored: 5
|
|
L0 blocks reached: 4/4
|
|
L0 regions used: 4/4
|
|
Overall: PASS
|
|
</code></pre>
|
|
|
|
<h3>Field mappings</h3>
|
|
|
|
<p>The structural correspondence checker produces a mapping between L1 actor fields and their L0 region locations:</p>
|
|
|
|
<div class="table-wrapper">
|
|
<table class="simple-table">
|
|
<thead>
|
|
<tr><th>L1 Field</th><th>L0 Location</th></tr>
|
|
</thead>
|
|
<tbody>
|
|
<tr><td><code>ledger.count</code></td><td><code>ledger_state[0]</code></td></tr>
|
|
<tr><td><code>ledger.total</code></td><td><code>ledger_state[8]</code></td></tr>
|
|
</tbody>
|
|
</table>
|
|
</div>
|
|
|
|
<p>This mapping is the <em>refinement relation</em> — the bridge between L1’s abstract named fields and L0’s concrete byte offsets. Every field is accounted for, every offset is correct, every access in L0 can be traced back to a field in L1.</p>
|
|
|
|
<hr>
|
|
|
|
<h2>What Else Could Be Built</h2>
|
|
|
|
<p>The three tools verify the lowering through concrete execution, structural analysis, and bounded enumeration. More sophisticated techniques from the formal verification literature could extend the pipeline further. These are not built — the DSL’s finite, bounded nature makes them unnecessary — but they represent natural next steps for a larger system.</p>
|
|
|
|
<h3>Symbolic Execution Engine (KLEE-inspired)</h3>
|
|
|
|
<p><strong>What it is:</strong> Instead of running the program with concrete values (price=7, qty=3), symbolic execution treats inputs as symbolic variables and tracks constraints along execution paths. Each branch creates a fork with the branch condition added as a constraint.</p>
|
|
|
|
<p><strong>What it would add:</strong> The current verification proves correctness for the program’s specific constants. Symbolic execution would prove correctness for <em>parameterized</em> inputs — that for <em>any</em> price P and quantity Q, the lowering preserves <code>total = total + P * Q</code>.</p>
|
|
|
|
<p><strong>Why it’s not needed yet:</strong> L1 programs have fixed inputs (leaf actions use constant expressions). There are no symbolic parameters — every execution is fully determined by the source text.</p>
|
|
|
|
<h3>Inductive Invariant Synthesis (IC3/PDR-inspired)</h3>
|
|
|
|
<p><strong>What it is:</strong> IC3/PDR synthesizes inductive invariants — properties that hold at every reachable state and are preserved by every transition. It works backward from a safety property, finding increasingly strong invariants until it proves the property or finds a counterexample.</p>
|
|
|
|
<p><strong>What it would add:</strong> Proofs that hold across <em>arbitrary</em> step counts. Our bounded explorer verifies <code>steps: 4</code>. IC3 could prove that for <code>steps: N</code> (any N), the lowering is correct — that the correspondence between L1 and L0 is an inductive invariant of the step function.</p>
|
|
|
|
<p><strong>Why it’s not needed yet:</strong> L1 cores declare a fixed step count. We enumerate all states. If the step count were parameterized, inductive invariant synthesis would be essential.</p>
|
|
|
|
<h3>Proof Certificate Generation (CompCert-inspired)</h3>
|
|
|
|
<p><strong>What it is:</strong> CompCert generates machine-checkable proof certificates verified by an independent proof checker (Coq). The certificate proves the compiled code refines the source semantics, and the proof checker confirms validity without trusting the compiler.</p>
|
|
|
|
<p><strong>What it would add:</strong> Independent verifiability. Our verification tools are part of the same codebase as the compiler — a bug in the verifier could mask a bug in the compiler. Proof certificates allow an external tool to independently confirm correctness.</p>
|
|
|
|
<p><strong>Why it’s not needed yet:</strong> The system is small enough for direct auditing. The three tools are independent of compilation logic. Proof certificates become valuable when the compiler is too complex for direct review.</p>
|
|
|
|
<hr>
|
|
|
|
<h2>Pipeline Summary</h2>
|
|
|
|
<div class="pipeline">
|
|
<div class="pipeline-title">Full Verification Pipeline — product.l1</div>
|
|
<div class="pipeline-flow">
|
|
<div class="pf-node">Parse <small>DSL → L1 IR</small></div>
|
|
<div class="pf-edge pf-gate">Verify L1 (6 checks)</div>
|
|
<div class="pf-node">Emit <small>L1 IR → L0 IR</small></div>
|
|
<div class="pf-edge pf-gate">Verify L0 (7 checks)</div>
|
|
<div class="pf-node">Translation Validation</div>
|
|
<div class="pf-edge">Tool 1: Trace Equivalence</div>
|
|
<div class="pf-node pf-pass">PASS <small>4 outputs, 1 actor</small></div>
|
|
<div class="pf-edge">Tool 2: Structural Correspondence</div>
|
|
<div class="pf-node pf-pass">PASS <small>7 invariants verified</small></div>
|
|
<div class="pf-edge">Tool 3: Bounded Model Check</div>
|
|
<div class="pf-node pf-pass">PASS <small>5 states, 4/4 blocks, 4/4 regions</small></div>
|
|
<div class="pf-edge"></div>
|
|
<div class="pf-node pf-final">Overall: PASS</div>
|
|
</div>
|
|
</div>
|
|
|
|
<h3>Commands to reproduce</h3>
|
|
|
|
<pre><code class="language-bash"># Full verification pipeline
|
|
cargo run -- verify examples/product.l1
|
|
|
|
# Run the program (standard execution)
|
|
cargo run -- examples/product.l1
|
|
|
|
# Dump all intermediate representations
|
|
cargo run -- examples/product.l1 --dump-ir
|
|
|
|
# Run the REPL and verify interactively
|
|
cargo run -- repl
|
|
# then: :load examples/product.l1
|
|
# then: :verify
|
|
|
|
# Run all tests (includes verification tool tests)
|
|
cargo test
|
|
</code></pre>
|
|
|
|
</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-bash.min.js"></script>
|
|
<script src="https://cdn.jsdelivr.net/npm/prismjs@1.29.0/components/prism-clike.min.js"></script>
|
|
</body>
|
|
</html>
|