StrataBoole

StrataBoole is a standalone Lean 4 package implementing the Boole dialect for Strata. Boole is a high-level imperative specification language designed for deductive program verification, offering a friendlier surface syntax that compiles down to Strata Core for analysis.

Overview

Boole extends Strata Core with:

• Global variables with var declarations and modifies clauses (translated to inout parameters)
• returns syntax for procedure outputs (vs. Core's out parameter modifiers)
• call lhs := f(args) syntax for calls with outputs
• For loops (for ... to, for ... downto, C-style for(;;))
• Unicode quantifiers (∀, ∃) alongside ASCII (forall, exists)
• Extensional equality (=~=) for map types

The analysis pipeline is: Boole program → parse via DDM → translate to Strata Core → perform analysis

Boole is the target of trusted translations from source languages. For the whole pipeline end to end, Rust with Verus specifications through Boole to cvc5 and to a proof checked by Lean's kernel, follow DALEK_BENCHMARK.md on the demo/dalek-sum-of-slice branch. It reproduces one real function step by step with the verus-boole translator; the other target programs are listed in docs/BooleBenchmarks.md. New to the repository? Start with docs/onboarding.md, a longer walk-through that ends with your first verified program.

Package Structure

StrataBoole/
├── lakefile.toml            # Lake build config (depends on Strata)
├── lean-toolchain           # Lean version selection
├── StrataBoole.lean         # Root module
├── StrataBoole/
│   ├── Grammar.lean         # DDM dialect grammar definition
│   ├── Boole.lean           # Code generation from grammar (#strata_gen)
│   ├── Verify.lean          # Translation to Core + verification pipeline
│   └── MetaVerifier.lean    # Tactic infrastructure (gen_smt_vcs_boole)
├── StrataBooleTest.lean     # Test root module
├── StrataBooleTest/
│   ├── demo.lean            # Basic loop verification example
│   ├── find_max.lean         # Array search with quantified invariants
│   ├── insertion_sort.lean   # Sorting algorithm verification
│   ├── ...                   # Additional test/example files
│   └── FeatureRequests/      # Tests for planned/experimental features
└── docs/                    # Onboarding guide, benchmarks, feature requests

Building

From the repository root:

lake build

To run all tests (builds the test library, which includes #eval and #guard_msgs checks):

lake test

Lake fetches the pinned Strata commit and lean-smt; the Lean version is pinned in lean-toolchain. Anything that runs the solver needs cvc5 on your PATH.

Writing a Boole Program

Programs can be embedded in Lean using the #strata ... #end syntax:

import StrataBoole.MetaVerifier

open Strata

def myProgram : StrataDDM.Program :=
#strata
program Boole;

procedure Add(x: int, y: int) returns (r: int)
spec {
  requires (x >= 0 && y >= 0);
  ensures (r == x + y);
}
{
  r := x + y;
};
#end

Programs can also be stored in *.boole.st source files. However, there is not currently a top-level CLI that will process these files. To load external files in the Boole dialect from a client of the StrataBoole package, use StrataDDM.readStrataFile to get a StrataDDM.Program and Strata.Boole.getProgram to translate it to a Strata.Boole.Program.

Verifying a Program

Runtime verification (via SMT solver)

#eval Strata.Boole.verify "cvc5" myProgram (options := .quiet)

Proof-mode verification (checked by Lean's kernel)

theorem myProgram_correct : Strata.smtVCsCorrectBoole myProgram := by
  gen_smt_vcs_boole
  all_goals (try grind)

The gen_smt_vcs_boole tactic unfolds the program into individual SMT verification conditions as Lean goals. Each goal can then be discharged by grind, omega, simp, or by lean-smt's smt tactic (import Smt), which calls cvc5 and replays its proof so that Lean's kernel checks it.

Key Concepts

Verification Pipeline

1. Parse: The DDM (Dialect Definition Mechanism) parses Boole syntax from #strata blocks
2. Translate: Strata.Boole.toCoreProgram converts Boole AST to Strata Core
3. VCG: Core's verifier generates verification conditions via symbolic execution
4. Encode: VCs are encoded as SMT-LIB formulas
5. Solve: Either dispatched to an external solver or proved within Lean

SMT-level and program-level routes

Both routes keep the program as data, so both are deep embeddings. They differ in the level that Lean gives a meaning to.

Everything above works at the SMT-LIB level. The verification-condition generator and the SMT encoding are trusted translations, and what gets checked is the SMT-LIB they produce: the solver route trusts cvc5 to check it, the Lean route the kernel and the lifting of SMT terms to Lean.

A program-level route is being worked out on the feat/hoare-logic branch. A Boole program's contract is proved, through its lowering to Core, against Core's Hoare logic (Strata/Languages/Core/Logic/), whose rules are theorems about Core's operational semantics. A tactic applies the rules and lifts what is left to goals over Lean values, so the generator and the encoding leave the trusted base. The plan and its status are in docs/HoareLogic.md on that branch.

Boole vs. Core Syntax

Boole	Core equivalent
var x : int; (global)	adds x as inout parameter to procedures whose modifies lists it; in parameter elsewhere
modifies x; (clause)	promotes the corresponding global to inout in this procedure's signature
returns (r: int)	out r: int parameter
call y := f(x);	call(inout globals, in x, out y)
for i := 0 to n	init i; while(i <= n) { ...; i := i + 1 }
∀ x:int . P	forall x:int :: P

Maps (Arrays)

Boole uses Map types with select/store syntax:

type Array := Map int int;
// Read: A[i]
// Write: A[i] := v;

Testing

Test files serve as both regression tests and usage examples. Each test file:

• Defines a Boole program
• Verifies it using #eval (runtime) and/or a theorem (proof-mode)
• Uses #guard_msgs to pin expected output

Good starting points:

• demo.lean - Simple loop with arithmetic invariant
• find_max.lean - Array traversal with quantified invariants
• procedure_signatures.lean - Procedure calling conventions
• function_definitions.lean - Pure function definitions with preconditions

License

Apache-2.0 OR MIT