437 lines
23 KiB
Markdown
437 lines
23 KiB
Markdown
# Formal Verification Pipeline: Proving L1→L0 Lowering Correctness
|
||
|
||
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.
|
||
|
||
The program used is `examples/product.l1` — 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.
|
||
|
||
**Reproducibility.** Every output shown here can be regenerated:
|
||
|
||
```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
|
||
```
|
||
|
||
## Pipeline Overview
|
||
|
||
The verification pipeline extends the standard compilation pipeline with a translation validation phase:
|
||
|
||
```
|
||
┌──────────┐ ┌───────┐ ┌───────────┐ ┌───────┐ ┌───────────┐
|
||
│ DSL │ │ L1 │ │ L1 IR │ │ L0 │ │ L0 IR │
|
||
│ Source │─────▶│ IR │─────▶│ (verified) │─────▶│ IR │─────▶│ (verified) │
|
||
│ (.l1) │ │ │ │ │ │ │ │ │
|
||
└──────────┘ └───────┘ └───────────┘ └───────┘ └───────────┘
|
||
Parse Verify(L1) Emit Verify(L0)
|
||
│
|
||
▼
|
||
┌─────────────────────────┐
|
||
│ Translation Validation │
|
||
│ ┌───────────────────┐ │
|
||
│ │ Trace Equivalence │ │
|
||
│ │ (CompCert-style) │ │
|
||
│ └───────────────────┘ │
|
||
│ ┌───────────────────┐ │
|
||
│ │ Structural │ │
|
||
│ │ Correspondence │ │
|
||
│ │ (Refinement-type) │ │
|
||
│ └───────────────────┘ │
|
||
│ ┌───────────────────┐ │
|
||
│ │ Bounded Model │ │
|
||
│ │ Checking (CBMC) │ │
|
||
│ └───────────────────┘ │
|
||
└─────────────────────────┘
|
||
│
|
||
▼
|
||
┌─────────────────┐
|
||
│ Verification │
|
||
│ Report │
|
||
│ (PASS / FAIL) │
|
||
└─────────────────┘
|
||
```
|
||
|
||
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.
|
||
|
||
## The Example Program
|
||
|
||
```l1
|
||
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
|
||
}
|
||
```
|
||
|
||
After 4 steps: `count` = 12, `total` = 84, emitted values = [21, 42, 63, 84].
|
||
|
||
This program is ideal for verification because it exercises:
|
||
- **Multi-field state** — two fields at different offsets, both mutated per step
|
||
- **Compound arithmetic** — `price * qty` nested inside an addition
|
||
- **Window reads** — a leaf reading actor state through a read-only window
|
||
- **Observable output** — emitted values that both L1 and L0 must agree on
|
||
|
||
---
|
||
|
||
## Tool 1: L1 Reference Interpreter
|
||
|
||
**Tradition:** CompCert's translation validation approach requires a *reference semantics* — a definition of what the source program means, independent of the compiler.
|
||
|
||
**What it is:** An abstract interpreter that executes L1 IR directly, without lowering to L0. It steps through the program's pipeline stages, dispatches messages to actor handlers, updates state, reads windows, and collects emitted outputs.
|
||
|
||
**Why it exists:** To prove the L0 lowering is correct, we need something to compare against. The L1 interpreter *is* the specification. If the L0 execution produces the same observable trace, the lowering preserved semantics.
|
||
|
||
### Execution trace for product.l1
|
||
|
||
```
|
||
--- 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]
|
||
```
|
||
|
||
**What the trace shows:** Each step follows the pipeline order: `buy` forwards a `Purchase(7, 3)` message to `ledger`, the actor processes it (multiplying price × qty and accumulating), then `report` reads the updated total through the window and emits it. The state evolves deterministically: count increments by 3 each step, total by 21.
|
||
|
||
### Operational semantics
|
||
|
||
The interpreter's step function:
|
||
|
||
1. For each pipeline in the core's pipeline list:
|
||
2. Walk stages left to right.
|
||
3. If the stage is a **leaf**: execute its actions (forward messages, read windows, emit outputs).
|
||
4. If the stage is an **actor**: pop messages from its queue and execute matching handlers.
|
||
5. After all pipelines complete: record the trace step (state snapshot, messages, reads, outputs).
|
||
|
||
This is the *reference semantics*. Any correct lowering must produce the same final state and the same output sequence.
|
||
|
||
---
|
||
|
||
## Tool 2: Trace Equivalence Checker
|
||
|
||
**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. Our trace equivalence checker follows this pattern exactly.
|
||
|
||
**What it does:**
|
||
1. Runs the L1 reference interpreter (Tool 1) on the program.
|
||
2. Runs the L0 codegen + x86-64 execution on the same program.
|
||
3. Compares final actor states field by field: L1 interpreter values vs. L0 region memory.
|
||
4. Compares emitted output sequences element by element.
|
||
|
||
### Side-by-side comparison for product.l1
|
||
|
||
| Observable | L1 Interpreter | L0 Execution | Match |
|
||
|---|---|---|---|
|
||
| `ledger.count` (final) | 12 | `ledger_state[0]` = 12 | ✓ |
|
||
| `ledger.total` (final) | 84 | `ledger_state[8]` = 84 | ✓ |
|
||
| Output[0] | 21 | 21 | ✓ |
|
||
| Output[1] | 42 | 42 | ✓ |
|
||
| Output[2] | 63 | 63 | ✓ |
|
||
| Output[3] | 84 | 84 | ✓ |
|
||
|
||
**Result: PASS** — outputs match (4 values), final states agree across 1 actor.
|
||
|
||
### What it catches
|
||
|
||
If the emitter generated `Sub` instead of `Add` for the handler's `count = count + qty`:
|
||
- L1 interpreter would compute `count = 0 + 3 = 3` at step 0
|
||
- L0 execution would compute `count = 0 - 3 = 18446744073709551613` (wrapping subtraction)
|
||
- Diagnostic: `"final state mismatch: ledger.count = 3 (L1) vs 18446744073709551613 (L0)"`
|
||
|
||
This is not a hypothetical — the test suite includes a deliberate corruption test that verifies this exact scenario.
|
||
|
||
### How it differs from CompCert
|
||
|
||
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 *which* pass introduced a bug) but simpler and catches any bug that affects observable behavior, regardless of which compilation stage introduced it.
|
||
|
||
---
|
||
|
||
## Tool 3: Structural Correspondence Checker
|
||
|
||
**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. Our structural checker does the same at the IR level: it verifies that L1 IR structures map to the expected L0 IR structures.
|
||
|
||
**What it does:** Walk the 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 *all* inputs to the program.
|
||
|
||
### Structural checks for product.l1
|
||
|
||
**Check 1: Actor state → L0 region mapping**
|
||
|
||
| L1 Field | L0 Region | Offset | Size | Init Store in `entry` |
|
||
|---|---|---|---|---|
|
||
| `ledger.count` : u64 | `ledger_state` (State, 16 bytes) | 0 | 8 | `store.64 ledger_state[0], r0` ✓ |
|
||
| `ledger.total` : u64 | `ledger_state` (State, 16 bytes) | 8 | 8 | `store.64 ledger_state[8], r0` ✓ |
|
||
|
||
Every L1 actor state field maps to a correctly typed, correctly sized L0 region slot at the right offset.
|
||
|
||
**Check 2: Handler → queue_pop + arithmetic**
|
||
|
||
| L1 Handler | L0 Queue Region | Args | Pops | Arithmetic Ops (L1) | Arithmetic Ops (L0) |
|
||
|---|---|---|---|---|---|
|
||
| `ledger.on Purchase(price, qty)` | `ledger_purchase_queue` (Queue) | 2 | 2 ✓ | 3 (add, mul, add) | ≥3 ✓ |
|
||
|
||
The handler has 2 arguments, so L0 must have 2 `queue_pop` operations from the purchase queue. The handler body has 3 arithmetic operations (`count + qty`, `price * qty`, `total + ...`), and L0's step block has at least 3 `Arith` operations.
|
||
|
||
**Check 3: Leaf forward → queue_push**
|
||
|
||
| L1 Leaf | Forward Target | L0 Queue Push |
|
||
|---|---|---|
|
||
| `buy` | `ledger` | `queue_push ledger_purchase_queue` ✓ |
|
||
|
||
**Check 4: Window read → state region load**
|
||
|
||
| L1 Leaf | Window Read | L0 Load |
|
||
|---|---|---|
|
||
| `report` | `ledger.summary.total` | `load.64 ledger_state[8]` ✓ |
|
||
|
||
The window field `total` is at offset 8 in the actor's state. The L0 step block contains a load from `ledger_state[8]`.
|
||
|
||
**Check 5: Emit → output region**
|
||
|
||
L1 has `emit(total)` in leaf `report` → L0 has `region output` of kind `Output` ✓
|
||
|
||
**Check 6: Control structure**
|
||
|
||
Required L0 blocks present: `entry` ✓, `loop_check` ✓, `step` ✓, `exit` ✓
|
||
|
||
**Check 7: Step counter**
|
||
|
||
`step_counter` region of kind `Control` exists ✓
|
||
|
||
**Result: PASS** — all structural invariants verified.
|
||
|
||
### What it catches vs. trace equivalence
|
||
|
||
The trace checker catches bugs that manifest on a specific input (the program's constants). The structural checker catches *classes* of bugs:
|
||
|
||
- A missing state field initialization (no `store` in `entry` for a field)
|
||
- A wrong queue region kind (using `State` instead of `Queue`)
|
||
- A mismatched argument count (handler expects 2 args but only 1 `queue_pop`)
|
||
- A missing control block (no `loop_check` means no bounded execution)
|
||
|
||
These are structural properties of the lowering that hold regardless of what values flow through the program.
|
||
|
||
---
|
||
|
||
## Tool 4: Bounded State Space Explorer
|
||
|
||
**Tradition:** CBMC (bounded model checking for C) and similar tools exhaustively explore all reachable states within a finite bound. Our bounded explorer exploits the fact that L1 programs have inherently finite state spaces: the core's step count bounds execution, and all state fields are initialized with known values with known arithmetic applied each step.
|
||
|
||
**What it does:**
|
||
1. Run the L1 interpreter through all steps, collecting every unique actor state observed.
|
||
2. Verify all L0 blocks are reachable (no dead blocks).
|
||
3. Verify all L0 regions are accessed (no dead regions).
|
||
4. Verify the L0 loop limit matches the L1 core step count.
|
||
5. Verify the exit block contains `Terminate`.
|
||
6. Verify control flow: entry → loop_check, loop_check → step/exit, step → loop_check.
|
||
|
||
### State space enumeration for product.l1
|
||
|
||
| Step | ledger.count | ledger.total | State ID |
|
||
|---|---|---|---|
|
||
| (init) | 0 | 0 | S0 |
|
||
| 0 | 3 | 21 | S1 |
|
||
| 1 | 6 | 42 | S2 |
|
||
| 2 | 9 | 63 | S3 |
|
||
| 3 | 12 | 84 | S4 |
|
||
|
||
**5 unique states** explored across 4 steps.
|
||
|
||
### Exploration statistics
|
||
|
||
| Metric | Value |
|
||
|---|---|
|
||
| States explored | 5 |
|
||
| L0 blocks reached | 4/4 (100%) |
|
||
| L0 regions used | 4/4 (100%) |
|
||
| L0 loop limit | 4 (matches L1 core steps ✓) |
|
||
| Exit block has `Terminate` | ✓ |
|
||
| Control flow well-formed | ✓ |
|
||
|
||
**Result: PASS** — all 4 L0 blocks reachable, all 4 regions accessed, bounded execution verified.
|
||
|
||
### Why bounded model checking works here
|
||
|
||
Traditional bounded model checkers like CBMC must handle arbitrary C programs with unbounded loops, dynamic memory, and pointer arithmetic — requiring SAT/SMT solvers to reason about feasibility. Our DSL is fundamentally different:
|
||
|
||
- **Execution is bounded by construction.** The `steps: N` declaration in the core means the program always terminates in exactly N iterations. No SAT solver needed — we simply enumerate.
|
||
- **State is finite and small.** Actor fields are typed (`u64`) and initialized with known values. With known constant inputs each step, the state at step N is fully determined by N.
|
||
- **The state space is tractable.** For product.l1: 5 states (init + 4 steps). Even programs with many actors and fields have state counts bounded by `steps + 1`.
|
||
|
||
This makes exhaustive enumeration not just feasible but trivial. The "bounded" model check is actually a *complete* check — there are no states outside the bound.
|
||
|
||
---
|
||
|
||
## Verification Report
|
||
|
||
Running `cargo run -- verify examples/product.l1` produces:
|
||
|
||
```
|
||
=== 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
|
||
```
|
||
|
||
All three tools pass. The lowering is verified correct.
|
||
|
||
---
|
||
|
||
## What Else Could Be Built
|
||
|
||
The three tools implemented here 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.
|
||
|
||
### Symbolic Execution Engine (KLEE-inspired)
|
||
|
||
**What it is:** 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.
|
||
|
||
**What it would add:** The current verification proves correctness for the program's specific constants. Symbolic execution would prove correctness for *parameterized* inputs — e.g., that for *any* price P and quantity Q, the lowering preserves `total = total + P * Q`.
|
||
|
||
**Why it's not needed yet:** L1 programs have fixed inputs (leaf actions use constant expressions). There are no symbolic parameters — every execution is fully determined by the source text. Symbolic execution would become relevant if L1 gained runtime input channels.
|
||
|
||
### Inductive Invariant Synthesis (IC3/PDR-inspired)
|
||
|
||
**What it is:** IC3 (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 either proves the property or finds a counterexample.
|
||
|
||
**What it would add:** Proofs that hold across *arbitrary* step counts. Our bounded explorer verifies `steps: 4`. IC3 could prove that for `steps: N` (any N), the lowering is correct — that the correspondence between L1 and L0 is an inductive invariant of the step function.
|
||
|
||
**Why it's not needed yet:** L1 cores declare a fixed step count. We enumerate all states. If the step count were parameterized (e.g., `steps: N` where N is a runtime input), inductive invariant synthesis would be essential.
|
||
|
||
### Proof Certificate Generation (CompCert-inspired)
|
||
|
||
**What it is:** CompCert generates machine-checkable proof certificates that can be verified by an independent proof checker (Coq). The certificate proves that the compiled code refines the source semantics, and the proof checker confirms the certificate is valid without trusting the compiler.
|
||
|
||
**What it would add:** 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 would allow an external tool (a small, trusted proof checker) to independently confirm correctness.
|
||
|
||
**Why it's not needed yet:** The system is small enough that the verification code can be audited directly. The three tools are independent of the compilation code (they don't share transformation logic). Proof certificates become valuable when the compiler is too complex for direct auditing.
|
||
|
||
---
|
||
|
||
## Pipeline Summary
|
||
|
||
The full verification pipeline for `examples/product.l1`:
|
||
|
||
```
|
||
┌─────────────────────────────────────────────────────────────────────┐
|
||
│ Full Verification Pipeline │
|
||
├─────────────────────────────────────────────────────────────────────┤
|
||
│ │
|
||
│ 1. Parse cargo run -- examples/product.l1 │
|
||
│ DSL source (.l1) → L1 IR │
|
||
│ │
|
||
│ 2. Verify L1 6 structural checks │
|
||
│ Reference resolution, ownership, window safety, │
|
||
│ pipeline well-formedness, buffer conservation, finiteness │
|
||
│ │
|
||
│ 3. Emit L1 IR → L0 IR │
|
||
│ Actors→regions, messages→queues, pipelines→loops, │
|
||
│ windows→loads, emit→output queue_push │
|
||
│ │
|
||
│ 4. Verify L0 7 concrete checks │
|
||
│ Control flow targets, reachability, region declarations, │
|
||
│ region bounds, access mode, queue safety, memory capacity │
|
||
│ │
|
||
│ 5. Translation Validation 3 verification tools │
|
||
│ ┌─────────────────────────────────────────────┐ │
|
||
│ │ a. Trace Equivalence (CompCert-style) │ │
|
||
│ │ L1 interpreter vs L0 execution │ │
|
||
│ │ Compare: final states + output values │ │
|
||
│ │ Result: PASS (4 outputs, 1 actor) │ │
|
||
│ ├─────────────────────────────────────────────┤ │
|
||
│ │ b. Structural Correspondence (refinement) │ │
|
||
│ │ L1 IR ↔ L0 IR parallel walk │ │
|
||
│ │ 7 structural invariant checks │ │
|
||
│ │ Result: PASS (all invariants hold) │ │
|
||
│ ├─────────────────────────────────────────────┤ │
|
||
│ │ c. Bounded Model Check (CBMC-style) │ │
|
||
│ │ 5 states explored, 4/4 blocks, 4/4 regions│ │
|
||
│ │ Result: PASS (bounded execution verified) │ │
|
||
│ └─────────────────────────────────────────────┘ │
|
||
│ │
|
||
│ Overall: PASS │
|
||
│ │
|
||
└─────────────────────────────────────────────────────────────────────┘
|
||
```
|
||
|
||
### Commands to reproduce
|
||
|
||
```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
|
||
```
|