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

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 exercises every verification-relevant feature:

• 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 requires a reference semantics — a definition of what the source program means, independent of the compiler.

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 is the specification: if 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]

Each step follows pipeline order: buy forwards Purchase(7, 3) to ledger, the actor processes it (multiplying price × qty and accumulating), then report reads the updated total through the window and emits it. 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.

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.

Side-by-side comparison for product.l1

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 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.

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 all inputs to the program.

Check 1: Actor state → L0 region mapping

Check 2: Handler → queue_pop + arithmetic

Check 3: Leaf forward → queue_push

Check 4: Window read → state region load

Checks 5–7: Emit, control structure, step counter

What it catches vs. trace equivalence

The trace checker catches bugs that manifest on a specific input. 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)

Tool 4: Bounded State Space Explorer

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.

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.

State space enumeration for product.l1

Exploration statistics

Why bounded model checking works here

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:

• Execution is bounded by construction. The steps: N declaration means the program always terminates in exactly N iterations. No SAT solver needed.
• 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.
• The state space is tractable. For product.l1: 5 states (init + 4 steps). 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

Field mappings

The structural correspondence checker produces a mapping between L1 actor fields and their L0 region locations:

This mapping is the refinement relation — 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.

What Else Could Be Built

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.

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 — 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.

Inductive Invariant Synthesis (IC3/PDR-inspired)

What it is: 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.

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, inductive invariant synthesis would be essential.

Proof Certificate Generation (CompCert-inspired)

What it is: 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.

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 allow an external tool to independently confirm correctness.

Why it’s not needed yet: 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.

Pipeline Summary

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