input-output-hkSolver

SMT-based reasoning core for Lean4

Blaster - An SMT Backend for Lean4

Lean Version Z3 Version License Contributions Welcome

Blaster provides an SMT backend for Z3 proofs. Blaster works by first aggressively optimizing the Lean expression of a theorem, sometimes up to a True goal, before sending the remaining goal and context to an SMT solver.

Table of Contents

Installation

Prerequisites

Blaster is built with the philosophy that fewer dependencies mean better maintainability and more optimization opportunities. That said, Blaster requires:

  • Lean4 v4.24.0 (or compatible version)
  • Z3 v4.15.2 (or compatible version)

Installing Lean4

We strive to stay in sync with the latest stable release of Lean4.

Currently supported version: Lean4 v4.24.0

Please follow the official installation guidelines from the Lean4 GitHub repository.

Installing Z3

We do our best to stay updated with the latest release of Z3. However, regressions can occur and often require extensive research and resolution, so Blaster might be slightly behind the latest version.

Currently tested version: Z3 v4.15.2

Note: Blaster should work with later releases, though no guarantees are made.

Please follow the official installation guidelines from the Z3 GitHub repository.

How to use?

In order to use Blaster, your project needs to depend on lean-blaster.

Using lakefile.toml

If you use lakefile.toml then, simply add a dependency to this repository:

[[require]]
name = "Solver"
git = "https://github.com/input-output-hk/Lean-blaster"
rev = "main"

Using lakefile.lean

If you use lakefile.lean then, simply add a dependency to this repository:

require «Solver» from git
  "https://github.com/input-output-hk/Lean-blaster" @ "main"

Solver options

  • timeout: specifying the timeout (in second) to be used for the backend smt solver (defaut: ∞)
  • verbose: activating debug info (default: 0)
  • only-smt-lib: only translating unsolved goals to smt-lib without invoking the backend solver (default: 0)
  • only-optimize: only perform optimization on lean specification and do not translate to smt-lib (default: 0)
  • dump-smt-lib: display the smt lib query to stdout (default: 0)
  • random-seed: seed for the random number generator (default: none)
  • gen-cex: generate counterexample for falsified theorems (default: 1)
  • solve-result: specify the expected result from the #solve command, i.e., 0 for 'Valid', 1 for 'Falsified' and 2 for 'Undetermined'. (default: 0)

Call to the solver

Command

You can call the solver by invoking the #solve command on a theorem name or on a propositional expression. The syntax is as follows:

  • #solve (option1: n) (option2: n) [theoremName]; or
  • #solve (option1: n) (option2: n) [theoremBody]

For example,

theorem addCommute : ∀ (a b : Nat), a + b = b + a := by sorry
#solve (only-optimize: 1) (solve-result: 0) [addCommute]
-- or
#solve (only-optimize: 1) (solve-result: 0) [∀ (a b : Nat), a + b = b + a]
-- or
#solve [∀ (a b : Nat), a + b = b + a]
Tactic

The solver can also be invoked via the blaster tactic. This tactic can be combined with other Lean4 tactics when trying to prove a theorem. The syntax is as follows: by blaster (option1: n) (option2: n).

For example,

theorem addCommute : ∀ (a b : Nat), a + b = b + a := by
  blaster (only-optimize: 1)
-- or
theorem length_set {as : List α} {i : Nat} {a : α} : (as.set i a).length = as.length := by
  induction as generalizing i <;> unfold List.set <;> blaster

[!NOTE] The tool does not perform proof reconstruction right now.

  • When the solver declares a goal as Valid, the tactic currently concludes the proof with an admit.
  • When the solver declares a goal as Falsified, the tactic fails and a counterexample is provided as witness. No counterexample is provided when a goal is reduced to False at the optimization phase.
  • When the solver returns Undetermined (i.e., the back-end solver was not able to prove/refute the goal), the tactic returns the current goal to be solved.

Features

Supported

Parametric Inductive Data Types
inductive Either (α : Type u) (β : Type v) where
 | Left : α -> Either α β
 | Right : β -> Either α β

def isLeft : Either a b -> Bool
 | Either.Left _  => true
 | Either.Right _ => false

def isRight : Either a b -> Bool
 | Either.Left _  => false
 | Either.Right _ => true

theorem isLeft_not_isRight_iff : ∀ (x : Either α β), ¬ (isRight x) = isLeft x := by blaster
Mutually Inductive Data Types
mutual
inductive A
  | self : A → A
  | other : B → A
  | empty
inductive B
  | self : B → B
  | other : A → B
  | empty
end

mutual
def A.sizeA : A → Nat
  | .self a => a.sizeA + 1
  | .other b => b.sizeB + 1
  | .empty => 0

def B.sizeB : B → Nat
  | .self b => b.sizeB + 1
  | .other a => a.sizeA + 1
  | .empty => 0
end

theorem A_self_size (a : A) : (A.self a).sizeA = a.sizeA + 1 := by blaster
Recursive Functions
#solve [ ∀ (x : Nat) (xs : List Nat), List.length xs + 1 = List.length (x :: xs) ]
Mutually Recursive Functions
mutual
  def isEven : Nat → Bool
    | 0 => true
    | n+1 => isOdd n

  def isOdd : Nat → Bool
    | 0 => false
    | n+1 => isEven n
end

#solve [ ∀ (n : Nat), isEven (n+1) = isOdd n ]

#solve [ ∀ (n : Nat), isEven (n+2) → isEven n ]
Polymorphism
inductive Either (α : Type u) (β : Type v) where
 | Left : α -> Either α β
 | Right : β -> Either α β

instance [BEq a] [BEq b] : BEq (Either a b) where
  beq | Either.Left a1, Either.Left a2 => a1 == a2
      | Either.Right b1, Either.Right b2 => b1 == b2
      | _, _ => false

#solve
  [ (∀ (α : Type) (a b : α), [BEq α] → a == b → a = b) →
      (∀ (α : Type) (β : Type) (x y : Either α β), [BEq α] → [BEq β] → x == y → x = y)
  ]
Higher-Order Logic
Quantification over Functions
#solve [ (∀ (β : Type) (x : Term (List β)) (f : Term (List β) → Nat), f x > 10) →
         (∀ (α : Type) (x y : Term (List α)) (f : Term (List α) → Nat), f x + f y > 20)
       ]
Higher-Order Functions
#solve [ ∀ (x : Nat) (xs : List Nat), !(List.isEmpty xs) →
         List.head! (List.map (Nat.add x) xs) ≥ x
       ]
Counterexample Generation for Recursive Data Types/Functions
def sizeOfTerm (t : Term α) : Nat :=
  match t with
  | .Ident _ => 1
  | .Seq xs => List.length xs
  | .App _ args => List.length args
  | .Annotated t' _ => 1 + sizeOfTerm t'

#solve [ ∀ (α : Type) (x : Term α), sizeOfTerm x < 10 ]

❌ Falsified
Counterexample:
 - x: (let ((a!1 (Test.SmtPredQualifier.Term.Annotated
             (Test.SmtPredQualifier.Term.Annotated
               (Test.SmtPredQualifier.Term.Annotated
                 (Test.SmtPredQualifier.Term.Ident "!a!")
                 (as List.nil (@List (@Test.SmtPredQualifier.Attribute @@Type))))
               (as List.nil (@List (@Test.SmtPredQualifier.Attribute @@Type))))
             (as List.nil (@List (@Test.SmtPredQualifier.Attribute @@Type))))))
(let ((a!2 (Test.SmtPredQualifier.Term.Annotated
             (Test.SmtPredQualifier.Term.Annotated
               (Test.SmtPredQualifier.Term.Annotated
                 (Test.SmtPredQualifier.Term.Annotated
                   a!1
                   (as List.nil
                       (@List (@Test.SmtPredQualifier.Attribute @@Type))))
                 (as List.nil (@List (@Test.SmtPredQualifier.Attribute @@Type))))
               (as List.nil (@List (@Test.SmtPredQualifier.Attribute @@Type))))
             (as List.nil (@List (@Test.SmtPredQualifier.Attribute @@Type))))))
  (Test.SmtPredQualifier.Term.Annotated
    (Test.SmtPredQualifier.Term.Annotated
      a!2
      (as List.nil (@List (@Test.SmtPredQualifier.Attribute @@Type))))
    (as List.nil (@List (@Test.SmtPredQualifier.Attribute @@Type))))))
State-Machine Formalization
instance counterStateMachine : StateMachine Request CounterState where
  init _ := { state := .Ready, timer := 0}
  next i s :=
    match s.state with
    | .Ready =>
         match i with
         | .Tr => { state := .Delay, timer := 0}
         | _ => s
    | .Delay =>
         if s.timer < 3
         then {s with timer := s.timer + 1}
         else {s with state := .Busy }
    | .Busy =>
         match i with
         | .Fa => {s with state := .Ready}
         | _ => s

  assumptions _ _ := True -- no assumptions

  invariants _ s :=
    (s.timer > 0 → s.timer < 3 → s.state = .Delay) ∧
    s.timer ≥ 0 ∧
    s.timer ≤ 3
Bounded Model Checking (BMC)

Command #bmc is provided to search for counterexamples up to a specified depth k on a given state machine instance. When no provided, depth k defaults to 10. For example, a counterexample is detected at Depth 4, when invariant s.timer ≤ 3 is changed to s.timer < 3

#bmc (max-depth: 8) (verbose: 1) [counterStateMachine]

❌ Falsified
Counterexample detected at Depth 4:
 - «Test.Counter02.counterStateMachine.input@1»: Test.Counter02.Request.Tr
 - «Test.Counter02.counterStateMachine.input@2»: Test.Counter02.Request.Fa
 - «Test.Counter02.counterStateMachine.input@3»: Test.Counter02.Request.Fa
 - «Test.Counter02.counterStateMachine.input@4»: Test.Counter02.Request.Tr
BMC at Depth 0
BMC at Depth 1
BMC at Depth 2
BMC at Depth 3
BMC at Depth 4
K-Induction

Command #kind is provided to prove that a state machine's invariants are always satisfied. It basically conducts an inductive proof in which the base case is handled via BMC, and the step case verifies that whenever the invariants hold for an arbitrary state, they must also hold for all states reachable from it.

#kind (max-depth: 1) (verbose: 2) [counterStateMachine]
✅ Valid
KInd at Depth 0
KInd at Depth 1

Currently Unsupported

Indexed Inductive Data Types

Indexed inductive data types are not yet supported because they lack a native representation at SMT-LIB level. We expect to add support soon via a suitable encoding that faithfully preserves the Lean4 semantics. For example,

inductive Finn : Nat → Type where
  | fzero : {n : Nat} → Finn n
  | fsucc : {n : Nat} → Finn n → Finn (n+1)
Inductive Predicates

Inductive predicates are not yet supported, but our plan is to enable them by translating each predicate into an equivalent boolean function at SMT-LIB level.

Implicit Induction Proof

The #solve command and the #blaster tactic do not currently attempt induction on their own. Users can work around this by pairing #blaster with the induction tactic in Lean4. We plan to enhance this by introducing heuristics that enable automatic inductive reasoning. For example,

inductive Path where
 | Here : Path
 | There : Path -> Path

def check_valid_path {α : Type}[BEq α](v : α)(p : Path)(ls : List α)
 : Bool
 := match p , ls with
    | .Here , .cons l _ls     => v == l
    | .There rs , .cons _ ls  => check_valid_path v rs ls
    | _ , _ => false

theorem validProof {α : Type}[BEq α](v : α)(p : Path)(ls : List α)
 : check_valid_path v p ls == true -> List.elem v ls := by
   induction ls generalizing p <;> blaster
Implicit Case Analysis

Currently, neither #solve nor #blaster performs case analysis to split a goal into subgoals. Users can address this by using #blaster alongside Lean4’s by_cases tactic. Our plan is to support automatic goal decomposition so that smaller SMT queries are generated instead of one monolithic query. This will highlight the harder subgoals and make them simpler for users to examine manually.

Examples

Examples are provided in the Tests folder.

Issues

The Tests/Issues folder contains examples that were, at some point, not properly handled by our tool.

Optimize

The Tests/Optimize folder contains examples of just the optimization step of the tool.

Validator examples

The Tests/Smt/Benchmarks/ValidatorsExamples contains simplified examples of Cardano validators. It contains two examples HelloWorld and Vesting.

State Machine

The Tests/StateMachine folder contains example on how to use the state machine formalization.

Benchmarks

Blaster has been benchmarked against a variety of well-known benchmarks to evaluate its performance and correctness. The evaluation can be found on this public repository: Blaster-benchmarking

Lean Natural Number Game
  • Repository: NNG4
  • Results: 103/117
  • Notes:
    • Failed on the examples that are not considered theorems by Lean
    • Failed on most of the Power examples
    • It includes Fermat's Last Theorem so 100% is unlikely to happen
Lean Set Theory Game
  • Repository: STG4
  • Results: 51/52
  • Notes:
    • Failed on the singleton theorem from FamCombo
Verina.io
  • Repository: [Add link here]
  • Results: [Add results here]
"Lean-Book"
  • Repository: [Add link here]
  • Results: [Add results here]

General description of Blaster

Blaster uses a three-step process to automatically reason about Lean theorems.

First step: optimization and normalization

Before translation to SMT-LIB, blaster optimizes the Lean expression (see Solver/Optimize/Basic.lean). This step simplifies the expression and prepares it for SMT translation by applying various transformations and rewriting rules, which can significantly improve the SMT solver's performance. These rules are applied recursively to the expression tree and are designed to reduce the complexity of the SMT query.

The core optimization logic is orchestrated in Solver/Optimize/Basic.lean, which applies a variety of strategies, including:

  • Beta Reduction: Lambda applications are simplified by substituting arguments into the lambda body.
  • Function Unfolding: Non-recursive and non-opaque functions are unfolded to their definitions.
  • Let-Expression Inlining: Let-bindings are inlined to simplify the expression.

In addition to these general strategies, Lean-blaster applies a set of specific rewriting rules for different types of expressions, primarily located in the Solver/Optimize/Rewriting/ directory. We give a few examples in this section to illustrate the goal of those rules.

Boolean Operations

Boolean expressions are simplified using a set of rules. These rules include:

  • Identity: true && e simplifies to e, and false || e simplifies to e.
  • Annihilation: false && e simplifies to false, and true || e simplifies to true.
  • Constants: e && not e simplifies to false, and e || not e simplifies to true.
  • Hypothesis-based simplification: If an expression is known to be true or false from the current context, it is simplified accordingly.
Natural Number Arithmetic

Arithmetic operations on natural numbers are optimized using a variety of algebraic simplifications and constant folding rules, which can be found in Solver/Optimize/Rewriting/OptimizeNat.lean. These include:

  • Constant Folding: Expressions with constant values are evaluated (e.g., 2 + 3 is replaced with 5).
  • Identity and Annihilation:
    • 0 + n simplifies to n.
    • n - 0 simplifies to n.
    • 1 * n simplifies to n.
    • 0 * n simplifies to 0.
    • And many more.
  • Algebraic Simplifications: More complex rules are applied, such as:
    • (m * n) / m, where n and m are expressions, simplifies to n if m is known to be non-zero in the current context.
  • Normalization: Arguments to commutative operators like Nat.add and Nat.mul are reordered to a canonical form, which helps in identifying further optimization opportunities.

These are just a few examples of the many optimization rules that Blaster applies to simplify expressions before they are sent to the SMT solver. This pre-processing step is crucial for the tool's performance and allows it to handle more complex verification tasks.

Control Flow and Pattern Matching

Blaster also includes a set of rules for simplifying control flow expressions like if-then-else (ITE), dependent if-then-else (DITE) and match expressions. These rules, found in Solver/Optimize/Rewriting/OptimizeITE.lean and Solver/Optimize/Rewriting/OptimizeMatch.lean, are designed to reduce the complexity of the expression by eliminating redundant branches and propagating constants.

  • ITE/DITE Simplification: if-then-else expressions are simplified in several ways:

    • If the condition is a constant (true or false), the expression is replaced with the corresponding branch.
    • If the then and else branches are equivalent expressions, the whole if-then-else is replaced with that branch.
    • And many more.

  • Match Expression Optimization: match expressions are optimized by:

    • Constant Propagation: If a discriminator (the value being matched on) is a known constant, the match expression is replaced with the corresponding branch.
    • Unreachable Branch Elimination: If a branch is determined to be unreachable based on the current context, it is eliminated.
    • Normalization: In some cases, match expressions are normalized into a series of if-then-else expressions to enable further simplification.
Function propagation

Function propagation is another key optimization strategy, detailed in Solver/Optimize/Rewriting/FunPropagation.lean. This technique simplifies expressions by "pushing" function calls into their arguments. For example, a function applied to an if-then-else expression can be transformed into an if-then-else expression where the function is applied to both the then and else branches. This can be particularly effective when one of the branches can be further simplified after the function is applied using other optimization rules.

Second-step: SMT Translation

Using the whole set of optimization rules, it may happen that a theorem can be reduced to True. This concludes the proof and the theorem is considered as Valid. For some other cases, a theorem may also be reduced to False and will therefore be declared as Falsified. Most of the time, a proof might not be concluded at the optimization phase. In this case, the optimized Lean expression is translated into an SMT-LIB format and submitted to the backend solver. The translation step is handled in Solver/Smt/Translate.lean. This process involves several key steps:

  1. Expression Traversal: The tool recursively traverses the Lean expression tree.
  2. Type and Function Translation: Lean types and functions are mapped to their SMT-LIB equivalents.
  3. Quantifier Handling: Universal and existential quantifiers are translated into SMT-LIB quantifiers.
  4. Application Translation: Function applications are translated into SMT-LIB function calls.

Final step: SMT Solver Interaction

Once an expression has been translated, Blaster interacts with an external SMT solver (i.e., Z3) to verify the SMT-LIB formula. This is done by asserting the negation of the formula to determine its satisfiability. The results are interpreted as follows:

  • unsat: The original expression is valid.
  • sat: The original expression is falsified, and a counterexample may be generated.
  • unknown: The solver could not determine the validity of the expression.

Contributing

We welcome all contributions! Whether it's bug reports, feature requests, documentation improvements, or code contributions, your help is appreciated.

Please see our Contributing Guidelines for more information on how to get started.

Ways to Contribute

  • Report bugs and issues
  • Suggest new features or improvements
  • Improve documentation
  • Submit pull requests

Maintained by:

Questions? Feel free to open an issue or reach out to the maintainers.