23 KiB
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:
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
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 * qtynested 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:
- For each pipeline in the core's pipeline list:
- Walk stages left to right.
- If the stage is a leaf: execute its actions (forward messages, read windows, emit outputs).
- If the stage is an actor: pop messages from its queue and execute matching handlers.
- 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:
- Runs the L1 reference interpreter (Tool 1) on the program.
- Runs the L0 codegen + x86-64 execution on the same program.
- Compares final actor states field by field: L1 interpreter values vs. L0 region memory.
- 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 = 3at 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
storeinentryfor a field) - A wrong queue region kind (using
Stateinstead ofQueue) - A mismatched argument count (handler expects 2 args but only 1
queue_pop) - A missing control block (no
loop_checkmeans 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:
- Run the L1 interpreter through all steps, collecting every unique actor state observed.
- Verify all L0 blocks are reachable (no dead blocks).
- Verify all L0 regions are accessed (no dead regions).
- Verify the L0 loop limit matches the L1 core step count.
- Verify the exit block contains
Terminate. - 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: Ndeclaration 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
# 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