Verification for Dummies: SMT and Induction

Adrien Champion

adrien.champion@ocamlpro.com
This work is licensed under a Creative Commons Attribution-ShareAlike 4.0 International License.

This book broadly discusses induction as a formal verification technique, which here really means formal program verification. I will use concrete, runnable examples whenever possible. Some of them can run directly in a browser, while others require to run small easy-to-retrieve tools locally. Such is the case for pretty much all examples dealing directly with induction.

The next chapters discuss the following notions:

formal logics and formal frameworks;
SMT-solving: modern, low-level verification building blocks;
declarative transition systems;
transition system unrolling;
BMC and induction proofs over transition systems;
candidate strengthening.

The approach presented here is far from being the only one when it comes to program verification. It happens to be relatively simple to understand, and I believe that familiarity with the notions discussed here makes understanding other approaches significantly easier.

This book thus hopes to serve both as a relatively deep dive into the specific technique of SMT-based induction, as well as an example of the technical challenges inherent to both developing and using automated proof engines.

Some chapters contain a few pieces of Rust code. Usually to provide a runnable version of a system under discussion, or to serve as example of actual code that we want to encode and verify. Some notions of Rust could definitely help in places, but this is not mandatory (probably).

Preface

High-level presentation of (formal) verification as a formal method.
SMT Solvers

SMT solvers are the basic building blocks for many modern verification tools.
Transition Systems

Transition systems are one way to encode a wide variety of programs in a framework suited for formal verification. Following sections will discuss all notions in the context of transition systems as they are fairly easy to understand. They definitely have downsides, but one can get a surprising mileage out of them if careful.
SMT and Transition Systems

Transition systems are represented by formulas that SMT solver can work on. This chapter lays out the foundation for more complex SMT-based analyses.
Unrolling and BMC

Bounded Model-Checking is, in general, not a verification technique. Still, it is quite useful for finding concrete counterexample, i.e. a concrete behavior of the system that illustrates a problem. It is also a good context to showcase what one can do with a transition system using an SMT solver.
BMC: Mikino

Mikino is a small proof engine that can perform BMC. While it requires getting familiar with its simple input format, it abstracts SMT solvers for us so that we can focus on higher-level concepts.
Induction

Induction is a natural step from BMC: it requires a simple BMC-like base check but also a step check which is simple to encode with SMT solvers. Since induction is a verification technique contrary to BMC, this is where we finally start proving things.
Induction: Mikino and Step Cex-s

In addition to BMC, mikino can also perform induction. It can thus prove inductive properties of a system. Once again, mikino abstracts the SMT solver for us. Mikino is designed with user experience in mind, so by the end of this chapter you will probably be able to experiment by modifying systems introduced so far, or write your own.
Candidate Strengthening

This chapter is quite technical and a bit theoretical. Make sure you are comfortable with all the notions discussed so far before diving in.

An invariant for a system is not necessarily inductive. This last part of the series focuses on candidate strengthening, which is really about discovering useful, powerful facts about the system's behavior. Such facts can make non-inductive invariants inductive, which is why most modern induction-based verification engines focus heavily on candidate strengthening.

This chapter, unlike previous ones, aims at proving an actual piece of code by encoding it as a transition system. It also touches on the complexity of verification and the notion of undecidability.

Preface

This preface is a high-level introduction to formal verification. It then goes into the details of what a formal verification tool looks like, and which aspects of such tools we will discuss in later posts.

Formal logics deal with reasoning in the context of a formal framework. For example, a type system is a formal framework. Strongly-typed programming languages rely on type systems to (dis)prove that programs are well-typed. For example, consider the following Rust function.

#![allow(unused)]
fn main() {
fn demo(n: usize) -> usize {
    let mut res = n;
    if n % 2 == 0 {
        res = 2*n;
    } else {
        res = 2*n + 1;
    }
    return res;
}
println!("demo(7): {}", demo(7))
}

When the Rust compiler type-checks this function, it goes through its body and aggregates some constraints. These constraints are an abstraction of the definition that the type system can reason about to (dis)prove that the program respects some type-related properties. For instance, let mut res = n; is abstracted as "res has the same type as n". The fact that, at this point, res is equal to n is not relevant for type-checking.

Rust's most peculiar feature is the notion of ownership and the associated borrow-checker. Similar to type-checking, borrow-checking abstracts the actual code to encode it in a framework so that it can reason about the program. Type-checking's core notion is that of types, and the equivalent for borrow-checking is lifetimes, i.e. the length of time for which some data exists and can be used.

Understanding lifetimes and the borrow-checker is not required for the next chapters. It is presented here as an example of encoding a problem in a framework where constraints can be constructed. Looking at these constraints, a tool (the borrow-checker here) can draw conclusion regarding the (un)safety of the program.

Consider the following Rust function, where 'a is a lifetime parameter.

#![allow(unused)]
fn main() {
// DOES NOT COMPILE
fn demo<'a>(n: &'a mut usize) -> &'a mut usize {
    let mut res = *n;
    res += 1;
    // error[E0515]: cannot return reference to local variable `res`
    return &mut res;
    //     ^^^^^^^^ returns a reference to data owned by the current function
}
}

Now, this code does not compile because of the notion of ownership. Here, the function's body owns res since it created (allocated) it and, since it does not transfer res itself to the caller (only &mut res), res is freed when we exit the body of the function (res's owner):

i) res only lives for the lifetime 'demo (lifetime of the body of demo)
ii) demo returns a mutable reference to res
iii) the output of demo is a mutable reference of the same lifetime 'a as its input

The compiler can then infer that demo's output has lifetime 'demo from i) and ii), and thus 'a must be equal to 'demo from iii). However, it follows from iii) that 'a must, in general, live strictly longer (be valid for longer) than 'demo. So, we have 'a > 'demo and since 'a = 'demo, we reach a contradiction: 'demo > 'demo. This means that there is no solution to the constraints, and the compiler proceeds to reject the program by telling us that res does not live long enough.

Type-checking and borrow-checking are examples of verification processes. In both cases, the semantics of the program is encoded in a proof system. The encoding of the program and the rules of the proof system let the compiler build a set of constraints.

It is interesting to note that formal verification, at its core, really consists in searching for a proof of correctness. As we saw, the borrow-checker aggregates constraints and then looks for a solution. In the paragraph above, we were looking for an interpretation of the different lifetimes of the program that verifies, or "satisfies" all the constraint.

Searching for a proof, which consists in trying to solve some constraints is done by a solver. From our point of view, the solver is our main building block. It is the block responsible for producing an actual answer from the encoding of the verification problem.

Now, the real question is "what does it mean for the constraints to have a solution, or to have none?". In the case of type-checking, the type constraints have a solution if and only if the program is well-typed. It says very little about memory-safety and thread-safety on its own, which is why type-checking is followed by borrow-checking in the Rust compiler.

The borrow-checker on the other hand builds constraints such that the existence of a solution implies the absence of Undefined Behavior (UB) in the program. At least as long as there are no unsafe blocks in it.

Properties and Specification

The main point of the discussion above is to highlight a well-known fact in formal verification. There is no such thing as verifying a program: all we can do is verify that some properties hold for a program. This might seem like a trivial distinction, but it has consequences that verification novices tend to overlook.

Type-checking and borrow-checking verify built-in properties: the program is well-typed and cannot exhibit UB. We do not need to write a specification to tell them to verify these properties. (Arguably, the type/ownership information we write throughout the program acts as a partial/local specification.)

As a consequence, if we want to verify something the compiler is not able to do, we need two things. First, we need some kind of specification, i.e. the properties we want to prove. We might want to prove relatively general properties, for instance that no division by zero can occur. Similar to type-checking and borrow-checking, this kind of property is built-in: whatever the program to verify is, the property stays the same.

But our properties might depend on the exact program that goes through the verification process. For example, we might want to prove input/output contracts on the functions of the programs we analyze: the output of fun_1 is positive, the output of fun_2 is strictly greater than its second input... In this case, programs will need some kind of annotation to specify these contracts. Contrary to built-in properties, these program-specific properties are an input of the verification tool.

Solvers and Encoding

The second thing we need is a solver in which we can reason about the properties we are interested in, on the programs we are interested in. In general, the solver will not accept the programs we want to solve directly: we need to perform some encoding to generate the constraints for the solver.

The endgame is to build a verification tool that looks something like this:


                              ┌───────────────────────┐
                              │   Verification Tool   │
                              ├───────────────────────┤
 ┌─────────────────────┐      │                       │
 │   Program to check  │      │     ┌──────────┐      │
 │and properties if not├──────┼─────► Encoding │      │
 │      built-in       │      │     └────┬─────┘      │
 └─────────────────────┘      │          │constraints │
                              │          │            │
                              │      ┌───▼─────┐      │
                              │      │ Solving │      │
                              │      └───┬─────┘      │
                              │          │success     │
                              │          │or failure  │
 ┌──────────────────────┐     │  ┌───────▼─────────┐  │
 │ User-friendly output ◄─────┼──┤ Post-processing │  │
 └──────────────────────┘     │  └─────────────────┘  │
                              │                       │
                              └───────────────────────┘

Expressiveness

An important thing we have to consider is the expressiveness of the solver: it must be able to represent and reason about our programs well enough that it is able to check our properties.

Spoiler alert: verification is expensive. Usable, practical formal verification requires quite a lot of clever engineering at every level. Also, generally speaking, the more expressive a solver is the more expensive using it will be. Roughly speaking, ideally, a good/efficient solver for a verification process is a solver that can handle exactly what we need and nothing else.

This is in fact how verification projects start, usually. Verification experts will take a very long look at the kind of programs and properties targeted by the project and establish a list of suitable solvers. Crucial aspects to look for in this process include

types of the values manipulated: booleans, integers, floats, hash sets, lists, user-defined types...
operations over these values: linear multiplication, non-linear multiplication, modulo...
control flow: recursion, iterators, loops, pattern-matching, switch-case...

Delimiting some kind of expressiveness perimeter to describe what we want the solver to support is crucial and quite technical. The immediate danger is to get this perimeter wrong, and later realize that aspects we missed make the solver we selected useless. This is why it tends to be difficult to extend the expressiveness of a verification framework in directions not identified in early stages.

If, when we chose the solver, all we had were booleans and integers with the usual operations over them, it is for example very unlikely that we will be able to handle hash sets without huge changes in the verification framework such as changing the solver.

Soundness (of the Encoding)

Solvers have a notion of soundness. Roughly, a solver is sound if it can only prove valid results (meaning it cannot prove things that are "wrong"). Since we are interested in using (not designing) solvers, let's not go into more details on the notion of solver soundness and only consider sound solvers.

There is a second notion of soundness however, which concerns the encoding. The encoding is the process of going from an input program (and specification) to whatever kind of system the solver can work on. This step will typically abstract the semantics of the program, as generally speaking we cannot represent its exact semantics in the solver's input language.

The process of encoding is sound if whenever we prove that the encoded program verifies some property Prop, then necessarily the original program verifies Prop as well. In case it is not clear, if the goal is formal verification then we need the encoding to be sound. Otherwise, a proof on the encoded program tells us nothing of the real program, i.e. the one we want to verify in the first place.

This is not to say that unsound encodings are necessarily useless. They can be useful if we are interested solely in finding bugs for instance. Since we will not try to prove anything, it is fine for the encoding to be unsound as long as it allows us to find actual/potential bugs.

Outro

I hope I got across the point that setting up a verification process in a (semi-)industrial context requires a great deal of inspection. It requires assessing very precisely what kind of program we want to analyze, and what kind of property we want to check. Widening the perimeter of programs/properties supported can be arbitrarily complex.

Another important point is that the actual verification framework should be written very carefully. While the solver is usually very trustworthy, any issue in the steps between the input program and specification and the solving (parsing, pre-processing and encoding) potentially voids any successful proof attempt. The solver must work on a correct encoding of the problem for the result to mean anything.

Note that the problem is less severe for failed proof attempts that produce a counterexample (an executable witness of a falsification of the property). Checking that the counterexample makes sense for the original program is easy and fast. But a proof of correctness relies on the encoding being sound and correctly implemented.

There are ways to mitigate this kind of problem. Soundness can be formally proved. The frontend can be made redundant by implementing it twice by two different teams in two different languages (two or more), and checking they produce exactly the same constraints. Solver-side, proof logging consists in having the solver log the logical steps of the actual proof it found so that they can be checked by one or more separate tools.

The following posts dive into SMT-based transition system induction, with some property strengthening at the end. We will first get to know SMT solvers, which are powerful, flexible and generally quite amazing tools. Next are (declarative) transition systems, which are the kind of programs we will analyze. They are relatively simple to understand and require little encoding to analyze them, meaning the encoding will be understandable when we look at it.

Next let's discuss bounded model checking, which on its own cannot (usually) prove anything: it just finds counterexamples (bugs). The three posts after that discuss basic and more advanced induction techniques.

SMT Solvers

SMT solvers are basic building blocks for most modern verification tools. While studying SMT solvers is particularly rewarding for developing such tools, understanding SMT forces to grasp concepts that are very useful even for high-level users. Later chapters will rely heavily on SMT solvers and readers are encouraged to run and modify examples themselves, or even create new ones.

Let's go over a few theory-level notions before we actually start playing with SMT solvers. A Satisfiability Modulo Theory (SMT) solver is a solver for establishing whether some constraints expressed in Many-Sorted First Order Logic (MSFOL) are satisfiable. Let's unpack this.

First, MSFOL is built on FOL (First Order Logic), which basically means "boolean formulas". For instance, a ∧ (false ∨ b ∨ c) is a FOL formula, where ∧ is conjunction (&&) and ∨ is disjunction (||). So this formula evaluates to true if and only if a is true and either b or c is true (since false tends not to be true). We can represent this formula as a tree, where leaves are boolean literals and nodes are boolean operators.

 ┌───∧───┐
 │       │
 a    ┌──∨──┬───────┐
      │     │       │
      │     │       │
    false   b       c

The leaves of the tree are atoms. MSFOL essentially extends FOL by allowing atoms to be formulas in other theories such as integers, strings, arrays, etc. For instance, with x and y integers and arr an array:

   ┌───∧─────┐
   │         │
 x > 7    ┌──∨────┬───────┐
          │       │       │
          │       │       │
        false   y ≤ x   arr[y] = x + 1

Note that the last atom, arr[y] = x + 1, mixes array selection arr[y] with addition over integers x + 1.

A brief discussion on notation and model theory

TL;DR: = is an operator over terms allowing to build formulas. We need a different symbol to express equivalence between terms: ≡. This operator is meta in the sense that it does not build MSFOL formulas, it just allows us humans to discuss term equivalence outside/above the MSFOL framework.

Notice that our formulas can mention the equality relation =. This relation lives the world of terms that we construct formulas with, for instance arr[y] = x + 1. Hence, we need a meta-notion of equality/equivalence to express the fact that two terms should be the same.

We use the ≡ relation over terms for this. For instance, (x + 1) ≡ (1 + x) or "x + 1 is equivalent to 1 + x" is not a formula, it is a (valid or invalid) statement that both terms are equivalent. In model theory, which we will not discuss much here, t₁ ≡ t₂ means "whatever the valuation of the variables in t₁ and t₂, both terms evaluate to the same value". This means that (x + 1) ≡ (1 + x) can be thought of as ∀ x, x + 1 = 1 + x, which is a valid (true) statement.

Z3

Examples in the next sections (and the next chapter) will rely on the Z3 SMT solver to actually run. You can build it from source or recover a binary from the release page. The version should not matter too much for what we'll do, but for reference this guide used v4.8.12.

From this point forward I assume readers have a Z3 binary called z3 in their path. That is, running the command z3 -version should not fail and produce an output similar to

Z3 version 4.8.13 - 64 bit

While I recommend Z3, other efficient solvers exist and include Alt-Ergo, CVC4 and Yices 2. Solvers tend to be good at distinct kinds of problem from each other, and verification frameworks routinely run several of them in parallel, wait for the quickest answer, and discard solver instances that are still running.

Satisfiability

Formula satisfiability is concerned about whether it is possible to make some formula evaluate to true. More precisely, is it possible to find a valuation for the variables appearing in the formula under which the formula is true. Such a valuation is called a model of the formula. Let us write a tiny example and start running Z3 to play with satisfiability directly.

To be precise, SAT stands for the boolean satisfiability problem, which deals with finding models for purely boolean formulas. "SMT" adds "Modulo Theory" to "Satisfiability" to specify that atoms of the formula can mention theories different from booleans (integers, reals, arrays, etc.) in its atoms, and that models must respect the rules of these theories.

SMT-LIB 2

For simplicity's sake, let's only allow atoms to mention integers. Consider the following formula.

(declare-const x Int)
(declare-const y Int)

   ┌───∧─────┐
   │         │
 x > 7    ┌──∨──────┐
          │         │
          │         │
        y = 2*x   x = 11

The first two lines declare "constants" x and y. As programmers, we can see them as "variables" in the sense that they represent an unknown value of type Int. This syntax comes from the SMT-LIB 2 standard, which is the standard scripting language for interacting with SMT solvers. Most, if not all, SMT solvers support SMT-LIB 2 input.

Of course, the ASCII art tree representing the formula is not legal SMT-LIB 2. An SMT-LIB 2 script declares constants (and more) and uses these constants to assert formulas, i.e. specify to the solver what the constraints are.

Also, SMT-LIB formulas are written using prefix notation (or Polish notation). For instance, y = 2*x would be written (= y (* 2 x)). This is a compromise between ease of printing/parsing and human readability. SMT-LIB is really meant to be used by programs to communicate, not for humans to actually write by hand. Still, it is readable enough for pedagogic and debugging purposes.

VS Code has an extension for SMT-LIB syntax highlighting (.smt2 files). The pieces of SMT-LIB code I will show in this book will not have syntax highlighting, unfortunately. I apologize for this problem, and encourage readers to copy these pieces of code in an editor that supports SMT-LIB using the button at the top-right of the code blocks.

Anyway, an SMT-LIB assertion of our running example would look like this:

(declare-const x Int)
(declare-const y Int)

(assert (and
	(> x 7)
	(or (= y (* 2 x)) (= x 11))
))

(check-sat)

The assert command feeds a constraint to the solver. Next, we can ask the solver to check the satisfiability of all the constraints (of which there is just one here) with check-sat.

Playing with Z3: `sat`

Let's now run Z3 on this tiny example. Create a file test.smt2 and copy the content of the SMT-LIB script above. No special option is needed and you should get the following output.

❯ z3 test.smt2
sat

Z3 simply answered sat, indicating that the formula is "satisfiable": there exists a model (a valuation of the variables) that make our constraints true. This is nice, but it would be better if Z3 could give us a model to make sure it is not lying to us (it's not). We can do so by adding a get-model command after the check-sat. (Note that get-model is only legal after a check-sat yielded sat.)

(declare-const x Int)
(declare-const y Int)

(assert (and
	(> x 7)
	(or (= y (* 2 x)) (= x 11))
))

(check-sat)
(get-model)

After updating test.smt2, running Z3 again will produce a model. You might not get exactly the same model as the one reported here depending on the precise version of Z3 you are using and possibly other factors (such as your operating system).

❯ z3 test.smt2
sat
(
  (define-fun y () Int
    16)
  (define-fun x () Int
    8)
)

The model is slightly cryptic. Z3 defines x and y as functions taking no arguments, which means that they are constants. This is because all functions are pure in SMT-LIB, meaning they always produce the same output when given the same inputs. Hence, a function with no arguments can only produce one value, and is therefore the same as a constant. In fact, (define-fun <ident> () <type> <val>) is the same as (define-const <ident> <type> <val>), and the (declare-const <ident> <type>) we used in the SMT-LIB script is equivalent to (declare-fun <ident> () <type>). Again, in SMT-LIB (and pure functional languages) a constant is just a function that takes no argument.

This valuation is a model because since x has value 8, then (> x 7) ≡ (> 8 7) holds and so does (= y (* 2 x)) ≡ (= 16 (* 2 8)) as y is 16 in the model.

Now, remember that we can assert more than one constraint, and that Z3 works on the conjunction of all constraints. In our running example, our only constraint is a conjunction, meaning we could write it as two constraints.

(declare-const x Int)
(declare-const y Int)

(assert (> x 7))
(assert (or (= y (* 2 x)) (= x 11)))

(check-sat)
(get-model)

Let's now add the constraint that y is an odd number: (= (mod y 2) 1). This should void the previous model, and more generally any model that relies on making (= y (* 2 x)) true to satisfy the constraints. (Since y would need to be both even and odd.)

(declare-const x Int)
(declare-const y Int)

(assert (> x 7))
(assert (or (= y (* 2 x)) (= x 11)))
(assert (= (mod y 2) 1))

(check-sat)
(get-model)

We now get

❯ z3 test.smt2
sat
(
  (define-fun x () Int
    11)
  (define-fun y () Int
    1)
)

As expected, Z3 now has to make the second constraint true through (= x 11).

Playing with Z3: `unsat`

Let's add another constraint to make these constraints unsatisfiable. In the latest version of our example, Z3 has no choice but to have x be 11 since it is the only way to verify the second constraint (because the third constraint prevents y from being even).

We can simply constrain x to be even (which prevents x to be 11), which we will write as "x cannot be odd".

(declare-const x Int)
(declare-const y Int)

(assert (> x 7))
(assert (or (= y (* 2 x)) (= x 11)))
(assert (= (mod y 2) 1))

(assert (not (= (mod x 2) 1)))

(check-sat)
(get-model)

Z3 knows exactly what we are doing and replies that the formula is unsatisfiable.

❯ z3 test.smt2
unsat
(error "line 11 column 10: model is not available")

We get an error though, because it does not make sense to ask for a model if the formula is unsatisfiable. "Unsatisfiable", or unsat, means "has no model" (i.e. no valuation of the variables can make all constraints true).

Now, what does this unsatisfiability result tell us? One way to see it is to consider the first three constraints as some form of context. That is, the first three constraints correspond to some point in a program where there are two unknown values x and y, and the first three constraints encode what we know to be true about these values.

The last constraint can be seen as a question. Say that at that point in the program, there is an assertion that x must be odd. We want to verify that this assert can never fail. From this point of view, then the latest version of our running example amounts to asking "given the context (first three constraints), is it possible for x to not be odd?". In other words, we are asking Z3 to find some values that both verify our context and falsify the program's assertion.

Z3 answers "no": in this context, it is not possible for x not to be odd. This means that Z3 proved for us that the program's assert statement can never fail (and can be compiled away).

What if, with different constraints, the negation of the program's assert statement was satisfiable? Then, as we saw in the previous section, Z3 can give us a model: a valuation of all the (relevant) variables involved in the check. this constitutes a counterexample, which shows how it is possible to verify the whole context but still falsify the program assertion (i.e satisfy the SMT-LIB-level (assert (not <program_assertion>))).

Outro

SMT solvers are extremely powerful, flexible and expressive tools. Powerful because they are highly optimized tools constantly improved by ongoing theoretical and practical research. Flexible because many different theories are available, allowing to manipulate integers, strings, arrays, algebraic data types, etc. And expressive because a great deal of verification problems are amenable to SMT without too much trouble.

One such verification problem is declarative transition system (induction-based) verification, as we will see in the following chapters.

The next section is optional, it is a repetition of the present section using mikino's version of SMT-LIB 2: hsmt. Hsmt is a Rust-flavored syntax for (a subset of) the SMT-LIB 2 scripting language. As we will see, mikino's primary functionality is performing SMT-based induction checks; hsmt is just a by-product feature that I thought could be useful for teaching what SMT is and how to interact with SMT solvers. Note that while mikino only supports a subset of SMT-LIB 2 (function definitions are not supported for example), it also adds new features such as conditional branching (if-then-else) over check-sat results.

If that's not interesting for you right now, feel free to move on directly to the next chapter.

SMT Scripts: Mikino

This section as well as most following ones rely on mikino, a nice tool I wrote for interacting with SMT solvers and perform induction-based analyses (which we will do soon). If you want to follow along just make sure you have mikino set up. Be careful that mikino requires Z3 to actually run, as discussed in the setup instructions.

Mikino has its own scripting language for interacting with SMT solvers. It is basically a Rust-flavored version of SMT-LIB 2 called hsmt (Human SMT). While readable, SMT-LIB 2 is designed to be written and parsed by programs, not humans. You probably noticed this yourself reading the previous section.

We want to emphasize that mikino is not an SMT solver: when running hsmt scripts, mikino acts as a thin layer between the hsmt code and Z3. Mikino translates your commands, passes them to Z3, and handles/prettifies the result of the command if any. Whenever we say mikino does something in this section, it's really Z3 doing through mikino.

We're going to go through what hsmt is shortly, but before we do know that you can run mikino demo --script demo.rs to generate a demo script file demo.rs which discusses more details about hsmt that we can cover here. For instance, the demo discusses conditional branching (if-then-else) over check-sat results (which SMT-LIB 2 does not have) which will not be mentioned here.

Basics

Consider the following formula.

vars {
   x y : int
}

   ┌───∧─────┐
   │         │
 x > 7    ┌──∨──────┐
          │         │
          │         │
        y = 2*x   x = 11

Of course, the ASCII art tree representing the formula is not legal hsmt. An hsmt script declares variables and uses them to assert formulas, i.e. specify to the solver what the constraints on these variables are.

As you already guessed the first lines in the snippet above declare integer variables x and y. vars block let you declare variables of type int, bool or rat(ional) as a comma-separated (with optional trailing comma) list:

#![allow(unused)]
fn main() {
vars {
   x y : int,
   flag1 : bool,
   flag2 : bool,
   z1 z2 z3 : rat,
}
}

Anyway, an hsmt assertion of our running example would look like this:

#![allow(unused)]
fn main() {
vars {
	x y : int
}

assert {
	(x > 7) ∧ (
		y = 2*x ∨ x = 11
	)
}

check_sat!()
}

All hsmt commands (vars, assert, check_sat, ...) accept their input either in a block { ... } or between parens ( ... ).

The assert command feeds a constraint to the solver as a constraint. Next, we can ask the solver to check the satisfiability of all the constraints (of which there is just one here) with check-sat.

Playing with mikino: `sat`

Let's now run mikino on this tiny example. Create a file test.rs and copy the content of the SMT-LIB script above. No special option is needed and you should get the following output.

> mikino script test.rs
sat
success

Mikino answered sat, indicating that the formula is "satisfiable": there exists a model (a valuation of the variables) that make our constraints (just one in this case) true. This is nice, but it would be better if mikino could give us a model to make sure it is not lying to us (it's not). We can do so by adding a get_model!() command after the check_sat!(). (Note that get_model!() is only legal after a check_sat!() yielded sat.)

vars {
	x y : int
}

assert {
	(x > 7) ∧ (
		y = 2*x ∨ x = 11
	)
}

check_sat!()
get_model!()

After updating test.rs, running mikino again will produce a model. You might not get exactly the same model as the one reported here depending on the precise version of mikino/Z3 you are using and possibly other factors (such as your operating system).

> mikino script test.rs
sat
model {
    x: 8,
    y: 16,
}
success

This valuation is a model because (> x 7) ≡ (> 8 7) holds ("is true") and so does (= y (* 2 x)) ≡ (= 16 (* 2 8)): all constraints are verified.

By the way, you might see a pattern here with the use of ! after some commands' name. It is not mandatory, but all commands that either i) can produce an output like check_sat, get_model, echo, println, or ii) exit/crash the script (exit, panic) can be written with a ! at the end like assert!(), println!("my message")... to make them stand out visually.

Now, we can assert more than one constraint. Mikino works on the conjunction of all constraints ---or at least Z3, behind the scene, does. In our running example, our only constraint is a conjunction, meaning we could write it as two constraints.

#![allow(unused)]
fn main() {
vars {
	x y : int
}

assert(x > 7)
assert(y = 2*x ∨ x = 11)

check_sat!()
get_model!()
}

> mikino script test.rs
sat
model {
    x: 8,
    y: 16,
}
success

Alternatively, assert actually takes as input a comma-separated list (with optional trailing comma) of expressions, understood as a conjunction. So this also works:

#![allow(unused)]
fn main() {
vars {
	x y : int
}

assert {
	x > 7,
	y = 2*x ∨ x = 11,
}

check_sat!()
get_model!()
}

> mikino script test.rs
sat
model {
    x: 8,
    y: 16,
}
success

Let's now add the constraint that y is an odd number: y % 2 = 1. This should void the previous model, and more generally any model that relies on making y = 2*x true to satisfy the constraints since y would need to be both even and odd.

#![allow(unused)]
fn main() {
vars {
	x y : int
}

assert {
	x > 7,
	y = 2*x ∨ x = 11,
	y % 2 = 1,
}

check_sat!()
get_model!()
}

We now get

> mikino script test.rs
sat
model {
    x: 11,
    y: 1,
}
success

As expected, the solver now has to make the second constraint true through x = 11.

Playing with mikino: `unsat`

Let's add another constraint to make our problem unsatisfiable. In the latest version of our example, the solver has no choice but to have x be 11 since it is the only way to verify the second constraint (because the third constraint prevents y from being even).

We can simply constrain x to be even (which prevents x from being 11), which we will write as "x cannot be odd".

#![allow(unused)]
fn main() {
vars {
	x y : int
}

assert {
	x > 7,
	y = 2*x ∨ x = 11,
	y % 2 = 1,
}

assert {
	¬(x % 2 = 1),
}

check_sat!()
get_model!()
}

Z3 knows exactly what we are doing and replies that the formula is unsatisfiable.

❯ z3 test.rs
unsat
|===| Error
| parse error at 18:1
|    | check_sat!()
| 18 | get_model!()<EOI>
|    | ^~~~ here
| - while requesting a model
| - smt-level error:
|   - solver error: "line 18 column 10: model is not available"
| - performing script step for file `./src/smt/code/ex_5.hsmt`
| - running `./src/smt/code/ex_5.hsmt` script
|===|

We get an error though, because it does not make sense to ask for a model if the formula is unsatisfiable. "Unsatisfiable", or unsat, means "has no model", i.e. no valuation of the variables can make all constraints true.

The last constraint can be seen as a question. Say that at that point in the program, there is an assertion that x must be odd. We want to verify that it can never fail. From this point of view, then the latest version of our running example amounts to asking "given the context (first three constraints), is it possible for x to not be odd?". In other words, we are asking the solver to find some values that both verify our context and falsify the program's assertion.

The solver answers "no": in this context, it is not possible for x not to be odd. This means that we proved for us that the program's assertion can never fail (and can be compiled away). More precisely, we proved that our encoding of the program's assertion can never fail. Whatever we then do with this information depends on how much trust we have in the encoding.

What if, with different constraints, the negation of the program's assert statement was satisfiable? Then, as we saw in the previous section, solvers can give us a model: a valuation of all the (relevant) variables involved in the check. this constitutes a counterexample, which shows how it is possible to verify the whole context but still falsify the program assertion, i.e satisfy assert { ¬ <program_assertion> }.

Outro

One such verification problem is declarative transition system (induction-based) verification, as we will see in the following chapters.

Transition Systems

This chapter is a bit abstract, there will be no fun manipulations 😿. The next chapter builds on this one and is nothing but fun manipulations 😺 on the notions and examples introduced here. Transition systems are the "objects" we will later analyze and are, in a sense, relatively close to pieces of actual code (loops). This chapter starts bridging the gap between the relatively high-level notion of transition system and SMT solvers which are relatively low-level tools.

A (declarative) transition system describes an infinite loop updating some state. The state can be understood as some variables storing some data. These variables are usually called state variables and they characterize the system completely. At each step, or iteration of the loop, the state is updated (the state can change). A loop, even an infinite loop, has to start somewhere. It may have more than one way to start itself: the initial states encapsulate all the different ways the loop can start.

Say we have a simple stopwatch system. It features a start_stop button (toggles counting) and a reset button. Say also this system counts time as an integer cnt. While start_stop and reset are inputs (users control whether they are pressed or not), cnt corresponds to the stopwatch's display: it is an output.

We also need an internal variable is_counting to remember whether we are counting or not: start_stop toggles counting, meaning we need to remember if we were previously counting or not to decide what a press of the start_stop button does. Hence, the state variables (svars) of our stopwatch are

#![allow(unused)]
fn main() {
svars {
	// inputs, `true` if pressed
	start_stop reset: bool,
	// internal variable
	is_counting: bool,
	// output
	cnt: int,
}
}

As we will see later, this is the actual syntax we will use once we start playing with the mikino induction-based checker.

The description of this system is

the system is initially not counting;
when not counting, a press on start_stop switch to counting mode (and conversely);
a press on reset resets the counter to 0;
when counting and not resetting, cnt keeps incrementing.

Expand this for a runnable implementation in Rust.

type Int = i64;
struct State {
    start_stop: bool,
    reset: bool,
    is_counting: bool,
    cnt: Int, // arbitrary precision integer (ℕ)
}
impl State {
    fn init(start_stop: bool, reset: bool, random_cnt: Int) -> State {
        State {
            start_stop,
            reset,
            // Initially not counting, unless `start_stop` is pressed
            // and triggers counting.
            is_counting: start_stop,
            cnt: if reset { 0 } else { random_cnt },
        }
    }
    fn step(&mut self, start_stop: bool, reset: bool) {
        self.start_stop = start_stop;
        self.reset = reset;
        // Need to toggle `self.is_counting`?
        if self.start_stop {
            self.is_counting = !self.is_counting
        }
        // `cnt` update
        self.cnt = if self.reset {
            0
        } else if self.is_counting {
            self.cnt + 1
        } else {
            self.cnt
        };
    }
    fn to_string(&self) -> String {
        format!(
            "cnt: {}, {}counting",
            self.cnt,
            if self.is_counting { "" } else { "not " }
        )
    }
}

fn main() {
    let mut state = State::init(false, false, -71);
    let mut step_count = 0;
    println!("initial state: {}", state.to_string());

    let mut step_show = |start_stop, reset, count_check| {
        if start_stop {
            println!("`start_stop` pressed")
        }
        if reset {
            println!("`reset` pressed")
        }
        state.step(start_stop, reset);
        step_count += 1;
        println!("@{} | {}", step_count, state.to_string());
        assert_eq!(state.cnt, count_check);
    };

    step_show(true, false, -70);
    step_show(false, false, -69);
    step_show(false, false, -68);
    step_show(false, false, -67);
    step_show(false, true, 0);
    step_show(false, false, 1);
    step_show(false, false, 2);
    step_show(false, false, 3);
    step_show(true, false, 3);
    step_show(false, false, 3);
    step_show(false, false, 3);
}

Initial Predicate

Let us think in terms of constraints: what must the values of the state variables verify to be a legal initial state? We only have one constraint, reset => cnt = 0. That is, if reset is true, then cnt must be 0, otherwise anything goes. Given the description of the system, this constraint captures the legal initial states and only the legal initial states.

This is called the init predicate of the transition system. The init predicate takes a state valuation as input, and is true if and only if that state valuation is a legal initial state. We can write it in pseudo-code as init(s) ≜ s.reset ⇒ s.cnt = 0 or, equivalently, init(s) ≜ ¬s.reset ∨ (s.cnt = 0): "either reset is false or cnt is 0".

It might seem like a detail, but you should not think of s.cnt = 0 as an assignment. It is really a constraint that evaluates to true or false depending on the value of s.cnt. If it helps, you can think of = as the usual == operator found in most programming languages.

Our initial predicate is not complete though. The specification also tells us that we are originally not counting, and that when start_stop is true we should toggle counting on/off. That is, the initial value of is_counting should be false when start_stop is false (not pressed), and true when start_stop is true (pressed). Hence, the initial value of is_counting is start_stop. Our initial predicate is thus

init(s) ≜ (s.reset ⇒ s.cnt = 0) ∧ (s.is_counting = s.start_stop)

Transition Relation

So at this point we have a notion of state (data) maintained by the transition system, and a predicate (formula) that is true on a state valuation if and only if it is a legal initial state. We are only missing the description of how the system evolves.

This is what the transition relation (a.k.a step relation) does. Its job is to examine the relation between two state valuations s and 's, and evaluate to true if and only 's is a legal successor of s. The first part of the transition relation deals with is_counting, which should be toggled by start_stop. This is a constraint, if 's is a successor of s then they should verify

's.start_stop ⇒ ('s.is_counting = ¬s.is_counting), and
¬'s.start_stop ⇒ ('s.is_counting = s.is_counting).

Note that we still have a constraint when start_stop is not pressed: the value should not change. If we did not constrain 's.is_counting in this case, then it would be unconstrained and thus could take any value. These two constraints are arguable more readable as

's.is_counting = if 's.start_stop { ¬s.is_counting } else { s.is_counting }.

Next, the system's description discusses how cnt evolves, which gives the following constraints:

's.reset ⇒ ('s.cnt = 0),
's.is_counting ⇒ ('s.cnt = s.cnt + 1), and
¬'s.is_counting ⇒ ('s.cnt = s.cnt).

Most readers might notice that these constraints will not work well together. Whenever reset is pressed cnt must be 0, and at the same time it must be either incremented or unchanged depending on the value of is_counting. In most cases, these constraints will have no solution.

Expand this for a concrete example of a conflict.

Say s.cnt = 1, and both 's.reset and 's.is_counting are true. Then by the first constraint, we must have 's.cnt = 0; by the second constraint, we must also have 's.cnt = 2. Hence, both constraints are in conflict and, together, they are unsatisfiable.

Assuming the order of the points in the description of the system matters, we can solve this problem by making the reset behavior preempt the behavior related to is_counting. We get

's.reset ⇒ ('s.cnt = 0),
('s.is_counting ∧ ¬'s.reset) ⇒ ('s.cnt = s.cnt + 1), and
(¬'s.is_counting ∧ ¬'s.reset) ⇒ ('s.cnt = s.cnt).

Alternatively, we can rewrite these constraints as

#![allow(unused)]
fn main() {
's.cnt =
	if 's.reset { 0 }
	else if 's.is_counting { s.cnt + 1 }
	else { s.cnt }
}

Our transition relation is thus

#![allow(unused)]
fn main() {
trans(s, 's) =
	  ( 's.start_stop ⇒ ('s.is_counting = ¬s.is_counting))
	∧ (¬'s.start_stop ⇒ ('s.is_counting =  s.is_counting))
	∧ (
		's.cnt =
			if 's.reset { 0 }
			else if 's.is_counting { s.cnt + 1 }
			else { s.cnt }
	)
}

Notice that trans only really constrains 's.is_counting and 's.cnt. This makes sense as the two other states variables 's.start_stop and 's.reset (both of type bool) are seen as inputs. Since they are not constrained, they can take any (boolean) value at all.

Notice also that, if we fix some values for 's.start_stop and 's.reset, then trans is deterministic: s, whatever it is, can only have one successor.

`'s.start_stop`	`'s.reset`	`'s.is_counting`	`'s.cnt`
`false`	`false`	`s.is_counting`	`if 's.is_counting { s.cnt + 1 } else { s.cnt }`
`true`	`false`	`¬s.is_counting`	`if 's.is_counting { s.cnt + 1 } else { s.cnt }`
`false`	`true`	`s.is_counting`	`0`
`true`	`true`	`¬s.is_counting`	`0`

So, there are at most four potential successors to any state s, depending on the (unconstrained) values of the two inputs.

SMT and Transition Systems

Time to use Z3 again: let's try to assert our transition relation so that we can use Z3 to answer questions about the system. To do this, we need to write our transition relation in SMT-LIB 2.

There's two new aspects of SMT-LIB 2 that will make things easier for us. First, SMT-LIB identifiers can be quoted which means they can have form |...| where ... is a sequence of pretty much any character but |. This is convenient as it allows us to write, for example, identifiers such as |s'.is_counting|. This will make things more readable, hopefully.

Second, SMT-LIB 2 allows us to define functions using the define-fun command. Its shape is

(define-fun <ident> ( <args> ) <type>
	<expression>
)

where <args> is zero or more arguments (<ident> <type>). For example:

(define-fun add_1 ( (n Int) ) Int
	(+ n 1)
)
(define-fun is_even ( (n Int) ) Bool
	(= (mod n 2) 0)
)

(declare-const n Int)
(assert
	(is_even (add_1 n))
)

; Is there an `n` such that `n + 1` is even? (yes)
(check-sat)
(get-model)

Running Z3, we obtain

> z3 test.smt2
sat
(
  (define-fun n () Int
    (- 1))
)

So, let's define a function for our transition relation. The definition is a bit daunting because, again, SMT-LIB 2 is really designed to be parsed by solvers. Human readability is not the main concern, but relatively small examples are quite readable if indented properly.

(define-fun trans
    (
        ; "Previous" state.
        (|s.start_stop| Bool)
        (|s.reset| Bool)
        (|s.is_counting| Bool)
        (|s.cnt| Int)
        ; "Next" state.
        (|s'.start_stop| Bool)
        (|s'.reset| Bool)
        (|s'.is_counting| Bool)
        (|s'.cnt| Int)
    )
    Bool

    (and
        (=> |s'.start_stop|
            (= |s'.is_counting| (not |s.is_counting|))
        )
        (=> (not |s'.start_stop|)
            (= |s'.is_counting| |s.is_counting|)
        )
        (= |s'.cnt|
            (ite |s'.reset|
                0
                (ite |s'.is_counting|
                    (+ |s.cnt| 1)
                    |s.cnt|
                )
            )
        )
    )
)

Full code in the Version 1 section below.

Now, if we want to use this transition relation function, we need to give ourselves actual state variables to apply it to. Let's switch notation to prepare for the more complex manipulations we will soon investigate. Let's distinguish state variables using indices: instead of referring to s and s' to distinguish between previous and next state, let's just say we have a state of index 0 and another one of index 1. So, instead of writing s.cnt and s'.cnt we can just write cnt_0 and cnt_1 respectively.

; "Previous" state.
(declare-const start_stop_0 Bool)
(declare-const reset_0 Bool)
(declare-const is_counting_0 Bool)
(declare-const cnt_0 Int)
; "Next" state.
(declare-const start_stop_1 Bool)
(declare-const reset_1 Bool)
(declare-const is_counting_1 Bool)
(declare-const cnt_1 Int)

We can now assert our transition relation over these two states, i.e. force state 1 to be a successor of state 0.

(assert (trans
    start_stop_0 reset_0 is_counting_0 cnt_0
    start_stop_1 reset_1 is_counting_1 cnt_1
))

Nice 😸. Let's see if we can force state 0 and the inputs of state 1 to have Z3 produce a new state that's a successor of state 0. For instance,

state 0: cnt is strictly greater than 7 and is_counting is false;
state 1: start_stop is pressed and reset is not.

(assert (and
    ; constraints over state 0
    (> cnt_0 7)
    (not is_counting_0)
    ; constraints over state 1's inputs
    start_stop_1
    (not reset_1)
))

(check-sat)
(get-model)

The check-sat command asks Z3 whether there exists a valuation of all state variables verifying all our constraints. Said constraints include that state 1 must be a legal successor of state 0.

Full code in the Version 1 section below.

> z3 test.smt2
sat
(
  (define-fun cnt_0 () Int
    8)
  (define-fun reset_1 () Bool
    false)
  (define-fun start_stop_1 () Bool
    true)
  (define-fun is_counting_0 () Bool
    false)
  (define-fun cnt_1 () Int
    9)
  (define-fun is_counting_1 () Bool
    true)
  (define-fun reset_0 () Bool
    false)
  (define-fun start_stop_0 () Bool
    false)
)

It works. In this model (yours might differ), Z3 decided to have cnt_0 be 8 which, given all the constraints, means that cnt_1 is 9. This is because is_counting_1 is true, which is a consequence of the last assertion we wrote (is_counting_0 is false and start_stop_1 is true).

Maybe we can ask for something more interesting, i.e. maybe we can actually prove something. Let's modify our last assertion: we keep the constraints over state 0 and replace state 1's by cnt_1 must be 0.

(assert (and
    ; constraints over state 0
    (> cnt_0 7)
    (not is_counting_0)
    ; constraints over state 1's inputs
    (= cnt_1 0)
))

(check-sat)
(get-model)

Note that this assertion replaces the one above where we constrained state 1's inputs.

The question we are asking Z3 is now "say cnt > 7 and we're not counting; is it possible then to have cnt = 0 in one transition?".

Full code in the Version 2 section below.

sat
(
  (define-fun start_stop_1 () Bool
    true)
  (define-fun reset_1 () Bool
    true)
  (define-fun is_counting_1 () Bool
    true)
  (define-fun cnt_0 () Int
    8)
  (define-fun cnt_1 () Int
    0)
  (define-fun is_counting_0 () Bool
    false)
  (define-fun reset_0 () Bool
    false)
  (define-fun start_stop_0 () Bool
    false)
)

Z3 answers "yes" (sat), and shows us that by pressing reset in state 1, then we have cnt = 0. That's fair, but what if we don't allow reset to be pressed in state 1?

(assert (and
    ; constraints over state 0
    (> cnt_0 7)
    (not is_counting_0)
    ; constraints over state 1's inputs
    (= cnt_1 0)
    (not reset_1)
))

(check-sat)

Readers comfortable with our toy stopwatch system know this should not be possible. If reset is not pressed, cnt can only increase or stay the same depending on whether the system is counting.

Humans (us) "knowing" this is not possible is not very valuable, as humans are notoriously great at being wrong. Let's just ask Z3 to prove (or disprove) what we know.

Full code in the Version 1 section below.

> z3 test.smt2
unsat

So, Z3's answer is that "there exists no valuation of the state variables verifying these constraints". That is, given the constraints on state 0, it is not possible to reach a state where cnt = 0 and reset is not pressed in one transition.

We can see this result as a consequence of a more abstract property of the system. That is, there are only three possible cnt values in the successor of any given state. Given cnt_0, cnt_1 can only be 0, cnt_0, or cnt_0 + 1.

Exercise: have Z3 prove this property by rewriting the last assertion of Version 3. Check out Version 4 for the solution. Hint below.

Hint.

Another way to look at what we want to prove is to say "it is not possible for cnt_1 to be anything else than 0, cnt_0, or cnt_0 + 1".

So, if we ask Z3 for a model where cnt_1 is none of these and the answer is unsat, then we would prove that cnt_1 cannot be anything but one of these three (not necessarily distinct) values.

Full Code For All Examples

Version 1

Expand this for the full code.

(define-fun trans
    (
        ; "Previous" state.
        (|s.start_stop| Bool)
        (|s.reset| Bool)
        (|s.is_counting| Bool)
        (|s.cnt| Int)
        ; "Next" state.
        (|s'.start_stop| Bool)
        (|s'.reset| Bool)
        (|s'.is_counting| Bool)
        (|s'.cnt| Int)
    )
    Bool

    (and
        (=> |s'.start_stop|
            (= |s'.is_counting| (not |s.is_counting|))
        )
        (=> (not |s'.start_stop|)
            (= |s'.is_counting| |s.is_counting|)
        )
        (= |s'.cnt|
            (ite |s'.reset|
                0
                (ite |s'.is_counting|
                    (+ |s.cnt| 1)
                    |s.cnt|
                )
            )
        )
    )
)

; "Previous" state.
(declare-const start_stop_0 Bool)
(declare-const reset_0 Bool)
(declare-const is_counting_0 Bool)
(declare-const cnt_0 Int)
; "Next" state.
(declare-const start_stop_1 Bool)
(declare-const reset_1 Bool)
(declare-const is_counting_1 Bool)
(declare-const cnt_1 Int)

(assert (trans
    start_stop_0 reset_0 is_counting_0 cnt_0
    start_stop_1 reset_1 is_counting_1 cnt_1
))

(assert (and
    ; constraints over state 0
    (> cnt_0 7)
    (not is_counting_0)
    ; constraints over state 1's inputs
    start_stop_1
    (not reset_1)
))

(check-sat)
(get-model)

Output:

> z3 test.smt2
sat
(
  (define-fun cnt_0 () Int
    8)
  (define-fun reset_1 () Bool
    false)
  (define-fun start_stop_1 () Bool
    true)
  (define-fun is_counting_0 () Bool
    false)
  (define-fun cnt_1 () Int
    9)
  (define-fun is_counting_1 () Bool
    true)
  (define-fun reset_0 () Bool
    false)
  (define-fun start_stop_0 () Bool
    false)
)

Version 2

Expand this for the full code.

(define-fun trans
    (
        ; "Previous" state.
        (|s.start_stop| Bool)
        (|s.reset| Bool)
        (|s.is_counting| Bool)
        (|s.cnt| Int)
        ; "Next" state.
        (|s'.start_stop| Bool)
        (|s'.reset| Bool)
        (|s'.is_counting| Bool)
        (|s'.cnt| Int)
    )
    Bool

    (and
        (=> |s'.start_stop|
            (= |s'.is_counting| (not |s.is_counting|))
        )
        (=> (not |s'.start_stop|)
            (= |s'.is_counting| |s.is_counting|)
        )
        (= |s'.cnt|
            (ite |s'.reset|
                0
                (ite |s'.is_counting|
                    (+ |s.cnt| 1)
                    |s.cnt|
                )
            )
        )
    )
)

; "Previous" state.
(declare-const start_stop_0 Bool)
(declare-const reset_0 Bool)
(declare-const is_counting_0 Bool)
(declare-const cnt_0 Int)
; "Next" state.
(declare-const start_stop_1 Bool)
(declare-const reset_1 Bool)
(declare-const is_counting_1 Bool)
(declare-const cnt_1 Int)

(assert (trans
    start_stop_0 reset_0 is_counting_0 cnt_0
    start_stop_1 reset_1 is_counting_1 cnt_1
))

(assert (and
    ; constraints over state 0
    (> cnt_0 7)
    (not is_counting_0)
    ; constraints over state 1's inputs
    (= cnt_1 0)
))

(check-sat)
(get-model)

Output:

> z3 test.smt2
sat
(
  (define-fun start_stop_1 () Bool
    true)
  (define-fun reset_1 () Bool
    true)
  (define-fun is_counting_1 () Bool
    true)
  (define-fun cnt_0 () Int
    8)
  (define-fun cnt_1 () Int
    0)
  (define-fun is_counting_0 () Bool
    false)
  (define-fun reset_0 () Bool
    false)
  (define-fun start_stop_0 () Bool
    false)
)

Version 3

Expand this for the full code.

(define-fun trans
    (
        ; "Previous" state.
        (|s.start_stop| Bool)
        (|s.reset| Bool)
        (|s.is_counting| Bool)
        (|s.cnt| Int)
        ; "Next" state.
        (|s'.start_stop| Bool)
        (|s'.reset| Bool)
        (|s'.is_counting| Bool)
        (|s'.cnt| Int)
    )
    Bool

    (and
        (=> |s'.start_stop|
            (= |s'.is_counting| (not |s.is_counting|))
        )
        (=> (not |s'.start_stop|)
            (= |s'.is_counting| |s.is_counting|)
        )
        (= |s'.cnt|
            (ite |s'.reset|
                0
                (ite |s'.is_counting|
                    (+ |s.cnt| 1)
                    |s.cnt|
                )
            )
        )
    )
)

; "Previous" state.
(declare-const start_stop_0 Bool)
(declare-const reset_0 Bool)
(declare-const is_counting_0 Bool)
(declare-const cnt_0 Int)
; "Next" state.
(declare-const start_stop_1 Bool)
(declare-const reset_1 Bool)
(declare-const is_counting_1 Bool)
(declare-const cnt_1 Int)

(assert (trans
    start_stop_0 reset_0 is_counting_0 cnt_0
    start_stop_1 reset_1 is_counting_1 cnt_1
))

(assert (and
    ; constraints over state 0
    (> cnt_0 7)
    (not is_counting_0)
    ; constraints over state 1's inputs
    (= cnt_1 0)
    (not reset_1)
))

(check-sat)

Output:

> z3 test.smt2
unsat

Version 4

Expand this for the full code.

(define-fun trans
    (
        ; "Previous" state.
        (|s.start_stop| Bool)
        (|s.reset| Bool)
        (|s.is_counting| Bool)
        (|s.cnt| Int)
        ; "Next" state.
        (|s'.start_stop| Bool)
        (|s'.reset| Bool)
        (|s'.is_counting| Bool)
        (|s'.cnt| Int)
    )
    Bool

    (and
        (=> |s'.start_stop|
            (= |s'.is_counting| (not |s.is_counting|))
        )
        (=> (not |s'.start_stop|)
            (= |s'.is_counting| |s.is_counting|)
        )
        (= |s'.cnt|
            (ite |s'.reset|
                0
                (ite |s'.is_counting|
                    (+ |s.cnt| 1)
                    |s.cnt|
                )
            )
        )
    )
)

; "Previous" state.
(declare-const start_stop_0 Bool)
(declare-const reset_0 Bool)
(declare-const is_counting_0 Bool)
(declare-const cnt_0 Int)
; "Next" state.
(declare-const start_stop_1 Bool)
(declare-const reset_1 Bool)
(declare-const is_counting_1 Bool)
(declare-const cnt_1 Int)

(assert (trans
    start_stop_0 reset_0 is_counting_0 cnt_0
    start_stop_1 reset_1 is_counting_1 cnt_1
))

(assert
    ; negate what we want to prove
    (not
        ; three possible values for `cnt_1` (not necessarily different)
        (or
            (= cnt_1 0)
            (= cnt_1 cnt_0)
            (= cnt_1 (+ cnt_0 1))
        )
    )
)

(check-sat)

Output:

> z3 test.smt2
unsat

Unrolling and BMC

Here we finally start doing things. We will perform a kind of analysis called BMC. While not a proof technique in general, it is a very useful falsification technique and paves the way towards induction.

In the previous chapter, we played with our running example using Z3 by

defining the transition relation as a define-fun,

Expand for a refresher on this definition.

(define-fun trans
    (
        ; "Previous" state.
        (|s.start_stop| Bool)
        (|s.reset| Bool)
        (|s.is_counting| Bool)
        (|s.cnt| Int)
        ; "Next" state.
        (|s'.start_stop| Bool)
        (|s'.reset| Bool)
        (|s'.is_counting| Bool)
        (|s'.cnt| Int)
    )
    Bool

    (and
        (=> |s'.start_stop|
            (= |s'.is_counting| (not |s.is_counting|))
        )
        (=> (not |s'.start_stop|)
            (= |s'.is_counting| |s.is_counting|)
        )
        (= |s'.cnt|
            (ite |s'.reset|
                0
                (ite |s'.is_counting|
                    (+ |s.cnt| 1)
                    |s.cnt|
                )
            )
        )
    )
)

declaring two states 0 and 1,

Expand for a refresher on these declarations.

; "Previous" state.
(declare-const start_stop_0 Bool)
(declare-const reset_0 Bool)
(declare-const is_counting_0 Bool)
(declare-const cnt_0 Int)
; "Next" state.
(declare-const start_stop_1 Bool)
(declare-const reset_1 Bool)
(declare-const is_counting_1 Bool)
(declare-const cnt_1 Int)

asserting the transition relation between state 0 and state 1, and

Expand for a refresher on this assertion.

(assert (trans
    start_stop_0 reset_0 is_counting_0 cnt_0
    start_stop_1 reset_1 is_counting_1 cnt_1
))

querying Z3 by constraining state 0 and/or state 1 to inspect the transition relation and prove some basic properties over it.

Expand for the last assertion and the queries.

(assert (and
    ; constraints over state 0
    (> cnt_0 7)
    (not is_counting_0)
    ; constraints over state 1's inputs
    start_stop_1
    (not reset_1)
))

(check-sat)
(get-model)

Unrolling

Now, this process of asserting the transition relation between two states 0 and 1 effectively enforces the constraint that state 1 must be a legal successor of state 0. This process is called unrolling the transition relation, or unrolling the system, or just unrolling.

So far, we have only unrolled once to relate state 0 and state 1. We can unroll more than once, simply by declaring more states and relate 0 to 1, 1 to 2, etc. by asserting the transition relation over the appropriate state variables.

Expand for an example of unrolling the system thrice.

; ANCHOR: all
; ANCHOR: trans_def
(define-fun trans
    (
        ; "Previous" state.
        (|s.start_stop| Bool)
        (|s.reset| Bool)
        (|s.is_counting| Bool)
        (|s.cnt| Int)
        ; "Next" state.
        (|s'.start_stop| Bool)
        (|s'.reset| Bool)
        (|s'.is_counting| Bool)
        (|s'.cnt| Int)
    )
    Bool

    (and
        (=> |s'.start_stop|
            (= |s'.is_counting| (not |s.is_counting|))
        )
        (=> (not |s'.start_stop|)
            (= |s'.is_counting| |s.is_counting|)
        )
        (= |s'.cnt|
            (ite |s'.reset|
                0
                (ite |s'.is_counting|
                    (+ |s.cnt| 1)
                    |s.cnt|
                )
            )
        )
    )
)
; ANCHOR_END: trans_def

; ANCHOR: states_def
; State 0.
(declare-const start_stop_0 Bool)
(declare-const reset_0 Bool)
(declare-const is_counting_0 Bool)
(declare-const cnt_0 Int)
; State 1.
(declare-const start_stop_1 Bool)
(declare-const reset_1 Bool)
(declare-const is_counting_1 Bool)
(declare-const cnt_1 Int)
; State 2.
(declare-const start_stop_2 Bool)
(declare-const reset_2 Bool)
(declare-const is_counting_2 Bool)
(declare-const cnt_2 Int)
; State 3.
(declare-const start_stop_3 Bool)
(declare-const reset_3 Bool)
(declare-const is_counting_3 Bool)
(declare-const cnt_3 Int)
; ANCHOR_END: states_def

; ANCHOR: unroll_1
(assert (trans
    start_stop_0 reset_0 is_counting_0 cnt_0
    start_stop_1 reset_1 is_counting_1 cnt_1
))
(assert (trans
    start_stop_1 reset_1 is_counting_1 cnt_1
    start_stop_2 reset_2 is_counting_2 cnt_2
))
(assert (trans
    start_stop_2 reset_2 is_counting_2 cnt_2
    start_stop_3 reset_3 is_counting_3 cnt_3
))
; ANCHOR_END: unroll_1

; ANCHOR: state_constraints
(assert (and
    ; starting from `cnt > 7`,
    (> cnt_0 7)
    ; can we reach a state where `cnt = 5` in three transitions?
    (= cnt_3 5)
))

(check-sat)
; ANCHOR_END: state_constraints
; ANCHOR_END: all

Output:

> z3 test.smt2
unsat

Reachability

Before we actually get to BMC, let's define a few notions. Remember that transition systems have state variables, and that a state is a valuation of all these state variables. Let's say a state s is reachable if the system, starting from one of its initial states, can reach s by applying its transition relation n times, where n is an arbitrary natural number.

Note that n can be 0, i.e. the initial states of a system are reachable, naturally.

This notion of reachability is usually extended to apply to state predicates. For instance, in the stopwatch system, we can say that the state predicate cnt > 5 is reachable: just start from 0 and keep counting.

Using this notion, we can talk about the set of all reachable states for a given system, called its reachable state space. This set can be infinite, and even when it's not, actually constructing this set for realistic systems tends to be impractical. A tool that tries to construct this set is called explicit-state. SMT-based approaches are almost always implicit-state, as SMT solvers reason at theory-level about booleans, integers... directly to assess whether a given formula is satisfiable. The only time actual values (and thus states) are produced is when the formula is satisfiable and we ask for a model.

While generally inefficient, tools such as TLA+ do manage to scale the explicit-state approach to impressively large systems. Also, it should be noted that when such a tool manages to terminate, i.e. compute the entire reachable state space, they are able to (dis)prove properties that are much more complex than anything we will do here. TLA+ for instance can reason about linear temporal logic formulas which are far beyond the scope of this book.

Let's introduce one more notion, that of invariants. Given some transition system, we can write down a state predicate (such as cnt ≥ 0) and wonder whether it holds (evaluates to true) on all reachable states. If it does, then that state predicate is an invariant of the system, or holds for the system.

From now on, we will be interested in transition systems with some candidate invariants. That is, we will have "properties" and we will have to (dis)prove that they are invariants for the system. We will say a system is safe if all the candidate invariants are actually invariants. Otherwise, the system is unsafe.

Fantastic Counterexamples and How to Find Them

When a candidate invariant I is not an actual invariant, it means there is at least one reachable state s that falsifies I, i.e. I(s) evaluates to false. Since s is a reachable state, it means that there exists a trace of states s_0, s_1, ... s_n such that

s_0 is an initial state, meaning init(s_0) is true,
∀ i ∈ [0, n[, s_i+1 is a successor of s_i, meaning trans(s_i, s_i+1) is true, and
s_n = s, meaning I(s_n) is false.

Assuming we are reporting to someone/something, we want to do better than just say unsafe when a candidate invariant does not hold for the system. Ideally, we should produce a witness of the candidate's falsification: a counterexample, which would be a trace of succeeding states leading to a state falsifying the candidate.

Thankfully, we have an SMT solver to do this. Can we actually explore the reachable state space and look for a falsification given what we have seen so far?

A first approach to doing this would be to write a bunch of assertions that are satisfiable if and only if there exists such a counterexample trace of some arbitrary length. Unfortunately, we cannot really do this as unrolling is a manual process: we declare state i, then assert the relation between state i-1 and state i. We cannot write a finite number of assertions that encode an arbitrary number of unrollings for the SMT solver to reason about. You can go ahead and try it, but it will not work. At least not without quantifiers (∀, ∃), which would not scale well at all.

Now that we are frustrated by this dead-end approach, let's forget about our ideal goal and try tackle something simpler: can we look for a falsification of the candidate invariants in the initial states?

Let's get back to our running stopwatch example, and add a candidate invariant: cnt ≥ 0. Recall that the stopwatch's initial predicate is

init(s) ≜ (s.reset ⇒ s.cnt = 0) ∧ (s.is_counting = s.start_stop)

Now, we need to design some assertions for the SMT solver such that they are satisfiable if and only if there exists an initial state that falsifies our candidate. This is quite similar to the unrolling we did in the previous chapter, where we wrote assertions that were satisfiable if and only if state 1 was a successor of state 0, and cnt_1 was something else than 0, cnt_0 or cnt_0 + 1.

Following the same approach, we first need to define-fun our initial state predicate.

(define-fun init
    (
        (|s.start_stop| Bool)
        (|s.reset| Bool)
        (|s.is_counting| Bool)
        (|s.cnt| Int)
    )
    Bool

    (and
        (= |s.is_counting| |s.start_stop|)
        (=> |s.reset| (= |s.cnt| 0))
    )
)

That was easy. Next up, declare a state so that we can assert init on it.

(declare-const start_stop_0 Bool)
(declare-const reset_0 Bool)
(declare-const is_counting_0 Bool)
(declare-const cnt_0 Int)

Then we write the init assertion.

(assert
    (init start_stop_0 reset_0 is_counting_0 cnt_0)
)

So easy. We want the SMT solver to look for a falsification of our candidate cnt ≥ 0, so we just assert that.

(assert
    (not (>= cnt_0 0))
)

(check-sat)
(get-model)

If Z3 answers sat to these constraints, it means it found some values for the state variables such that they

represent an actual initial state, and
falsify our candidate.

Full code in the Version 1 section below.

> z3 test.smt2
sat
(
  (define-fun reset_0 () Bool
    false)
  (define-fun cnt_0 () Int
    (- 1))
  (define-fun start_stop_0 () Bool
    false)
  (define-fun is_counting_0 () Bool
    false)
)

Did it work? Let's look at our initial predicate again:

init(s) ≜ (s.reset ⇒ s.cnt = 0) ∧ (s.is_counting = s.start_stop)

The specification of the system did not really say anything about the initial value cnt should have. At least not besides the fact that it should be 0 when reset is true. Hence, when reset is false, cnt is not constrained in any way. In a real program, one could see this as a use-before-init problem where we declare (but not initialize) a cnt variable, set it to 0 if reset is true, but do nothing otherwise: cnt could be anything (including an invalid integer).

So our system is unsafe: the candidate does not hold. The specification was not precise enough. Let's say from now on that the specification tells us cnt is initially an arbitrary positive integer. Let's fix our initial predicate.

(define-fun init
    (
        (|s.start_stop| Bool)
        (|s.reset| Bool)
        (|s.is_counting| Bool)
        (|s.cnt| Int)
    )
    Bool

    (and
        (= |s.is_counting| |s.start_stop|)
        (=> |s.reset| (= |s.cnt| 0))
        (>= |s.cnt| 0)
;       ^^^^^^^^^^^^^^~~~~ fixed the specification
    )
)

We do not need to change anything else, we can just run the same check on the updated initial predicate.

Full code in the Version 2 section below.

> z3 test.smt2
unsat

Perfect: by answering unsat, Z3 is telling us that it proved that no valuation of s_0 is such that it is an initial state and it falsifies the candidate invariant. We just proved something: no falsification of the candidate is reachable in 0 transitions. Nice.

Can we keep going? Is the candidate falsifiable in 1 transitions, or 7, or more? Of course we can, thanks to unrolling. We previously used unrolling to start from some arbitrary state s_0 and perform checks about its potential successor(s). If we just force s_0 to be initial, like we just did, we can then unroll once to ask Z3 whether a successor s_1 of s_0 can falsify the candidate. If not, we can unroll once more, and so on until we find a falsification.

Congratulations to us, we just invented BMC.

The stopwatch system has an infinite reachable state space since cnt can reach any integer value (just keep incrementing it). Start actually proving candidates in the next chapter, this one focuses solely on finding counterexamples.

BMC

Bounded Model-Checking (BMC) is a forward exploration of the reachable state space of a transition system. The term forward exploration refers to the fact that BMC starts from the initial states and explores the state space by unrolling the transition relation incrementally.

As a technique BMC is explicitly bounded: it explores the reachable state space up to some depth (number of unrollings). That is, as long as the reachable state space is infinite, BMC cannot prove anything because it will never finish exploring the state space. All it can do is disprove candidates.

By this point, I expect most readers to be able to write SMT-LIB code that corresponds to a BMC check for a given number of unrollings. Just to make sure, the BMC with Unrolling section showcases a BMC check where the transition relation is unrolled twice.

Warning: slightly (more) technical and practical discussion ahead. What follows is not mandatory to understand the upcoming chapters, but I think it is quite interesting and definitely mandatory for writing your own (efficient) verification engine.

Let's discuss a few practical points regarding BMC. Mainly, the fact that it is incremental and that what we do at a given step depends on the solver's previous answer. For instance, say we have several candidate invariants and we are checking whether we can falsify some of them by unrolling k times. Say also the solver answers yes (sat) and gives us a model. Then what we want to do is check which candidates are falsified (using the model), and keep BMC-ing the candidates that were not falsified. We got a counterexample for some of the candidates, but there might be a different counterexample at the same depth falsifying other candidates. If not (unsat), we move on and check the remaining candidates at k+1 and so on. Maybe they can be falsified by unrolling more than k times.

So, this whole process is interactive: what BMC does depends on what the solver previously said. In the next chapter, I will introduce mikino which is a tool that will perform BMC (and more) for us. The way mikino conducts BMC is by launching Z3 as a separate process and feed it definitions, declarations, assertions, check-sats and get-models on its standard input. Z3 produces answers on its standard output, which mikino looks at to decide if/how to continue and what to stream to the input of the Z3 process.

Based on what we have done so far, this would require restarting the solver each time. Say Z3 answers unsat when we unroll k times. It means that we have an assertion of the negation of the candidate(s) for s_k which made our whole SMT-LIB instance (all the assertions together) unsat: (assert (not (candidate s_k))). Now, this assertion is only there for our check at depth k, to ask for a falsification of the candidate(s). Still, we cannot move on and unroll at k+1: this assertion will still be there, and the instance will remain unsat.

So, instead of restarting Z3, we can make the assertion of the negation of the candidates conditional. That is, we can give ourselves a boolean flag that activates this assertion. Such a flag is called an activation literal, or actlit.

Say we are performing a BMC check at depth k. First, we need to declare this "boolean flag".

(declare-const actlit_k Bool)

Next, we write our assertion of the negation of the candidate(s) in such a way that actlit_k needs to be true for the assertion to be active.

(assert
	(=> actlit_k
		(not (and (candidate_1 s_k) (candidate_2 s_k) ...))
	)
)

Notice that if actlit_k is false, then this assertion is trivially true and thus does not contribute to whether other assertions are satisfiable. This is because false ⇒ P is always true, regardless of what P is. In particular, false ⇒ false is true.

The last thing we need now is to perform a check-sat assuming actlit_k is true. We could (assert actlit_k) but that would not solve our problem: we cannot go back and undo this assertion, hence the negation of the candidates is active, hence the whole instance is unsat.

Instead, we can use the check-sat-assuming SMT-LIB command. This command takes a list of boolean variables and forces to check-sat our assertions assuming these variables are true, but without actually asserting them. Meaning that, after the check-sat, these variables are still unconstrained.

In particular, it means we can perform a check-sat-assuming on actlit_k, and then just assert actlit_k to be false to effectively deactivate the assertion of the negation of the candidates.

This is all a bit abstract, let's see it in action on the stopwatch system. The BMC with Unrolling section shows an unrolling of the system at depth 2 with the corresponding check for candidate cnt ≥ 0, and just that check. Let's modify it so that it uses activation literals to perform all checks up to depth 2.

The first check to perform is at depth 0, so all we asserted so far is that state 0 is initial.

; State 0 is initial.
(assert
    (init start_stop_0 reset_0 is_counting_0 cnt_0)
)

Next we declare our activation literal for the upcoming check.

; Activation literal for the first check.
(declare-const actlit_0 Bool)

Then we conditionally assert the negation of the candidate.

; Conditional assertion of the negation of the candidate at 0.
(assert (=> actlit_0
    (not (>= cnt_0 0))
))

Then comes the check itself, using the brand new check-sat-assuming command we just discussed.

; Check-sat, assuming `actlit_0` is true.
(echo "; info: falsification at depth 0?")
(check-sat-assuming ( actlit_0 ))

Notice the use of the echo command which takes a string and causes the solver to output said string to its standard output. Remember that we will perform more than one check, so we use echo to keep track of what question the sat/unsat answers are for.

As we already saw, this check will produce unsat: there is no falsification of this candidate at depth 0 (or at any depth, but we have not proved that yet).

; Solver answers `unsat`, we want to unroll the system some more.
; Before we do that, we deactivate the actlit.
(assert (not actlit_0))
; At this point, the solver realized the conditional assertion
; of the negation of the candidate is trivially `true`, and will
; ignore it from now on.

As a sanity check, we can check-sat right after we deactivated actlit_0. We just got an unsat because we assumed actlit_0, so if the deactivation of the negation of the candidate failed then a regular check-sat would also yield unsat. If deactivation worked, we should get sat because (init s_0), our only active assertion, is sat.

(echo "; info: making sure assertion at 0 is not active anymore, expecting `sat`")
(check-sat)

We can now keep on unrolling and check-sat-assuming, since the assertion of the negation of the candidate should now be deactivated.

(assert
    (trans
        start_stop_0 reset_0 is_counting_0 cnt_0
        start_stop_1 reset_1 is_counting_1 cnt_1
    )
)
(declare-const actlit_1 Bool)
(assert (=> actlit_1
    (not (>= cnt_1 0))
))
(echo "; info: falsification at depth 1?")
(check-sat-assuming ( actlit_1 ))
(assert (not actlit_1))
(echo "; info: making sure assertion at 1 is not active anymore, expecting `sat`")
(check-sat)

We can keep going like that for as long as we want. Running Z3 on SMT-LIB code enforcing this methodology up to depth 2 produces the following output (see the BMC with Actlits section below for the full code).

; info: falsification at depth 0?
unsat
; info: making sure assertion at 0 is not active anymore, expecting `sat`
sat
; info: falsification at depth 1?
unsat
; info: making sure assertion at 1 is not active anymore, expecting `sat`
sat
; info: falsification at depth 2?
unsat
; info: making sure assertion at 2 is not active anymore, expecting `sat`
sat

Pretty nice 😸. Let's never do this again manually to preserve our own sanity, and move on to the next chapter where we will introduce mikino to do all of this automatically.

Full Code For All Examples

Version 1

Expand this for the full code.

(define-fun init
    (
        (|s.start_stop| Bool)
        (|s.reset| Bool)
        (|s.is_counting| Bool)
        (|s.cnt| Int)
    )
    Bool

    (and
        (= |s.is_counting| |s.start_stop|)
        (=> |s.reset| (= |s.cnt| 0))
    )
)

(declare-const start_stop_0 Bool)
(declare-const reset_0 Bool)
(declare-const is_counting_0 Bool)
(declare-const cnt_0 Int)

(assert
    (init start_stop_0 reset_0 is_counting_0 cnt_0)
)

(assert
    (not (>= cnt_0 0))
)

(check-sat)
(get-model)

Output:

> z3 test.smt2
sat
(
  (define-fun reset_0 () Bool
    false)
  (define-fun cnt_0 () Int
    (- 1))
  (define-fun start_stop_0 () Bool
    false)
  (define-fun is_counting_0 () Bool
    false)
)

Version 2

Expand this for the full code.

(define-fun init
    (
        (|s.start_stop| Bool)
        (|s.reset| Bool)
        (|s.is_counting| Bool)
        (|s.cnt| Int)
    )
    Bool

    (and
        (= |s.is_counting| |s.start_stop|)
        (=> |s.reset| (= |s.cnt| 0))
        (>= |s.cnt| 0)
;       ^^^^^^^^^^^^^^~~~~ fixed the specification
    )
)

(declare-const start_stop_0 Bool)
(declare-const reset_0 Bool)
(declare-const is_counting_0 Bool)
(declare-const cnt_0 Int)

(assert
    (init start_stop_0 reset_0 is_counting_0 cnt_0)
)

(assert
    (not (>= cnt_0 0))
)

(check-sat)

Output:

> z3 test.smt2
unsat

BMC with Unrolling

Expand this for the full code.

; Initial predicate.
(define-fun init
    (
        (|s.start_stop| Bool)
        (|s.reset| Bool)
        (|s.is_counting| Bool)
        (|s.cnt| Int)
    )
    Bool

    (and
        (= |s.is_counting| |s.start_stop|)
        (=> |s.reset| (= |s.cnt| 0))
        (>= |s.cnt| 0)
    )
)

; Transition relation.
(define-fun trans
    (
        ; "Previous" state.
        (|s.start_stop| Bool)
        (|s.reset| Bool)
        (|s.is_counting| Bool)
        (|s.cnt| Int)
        ; "Next" state.
        (|s'.start_stop| Bool)
        (|s'.reset| Bool)
        (|s'.is_counting| Bool)
        (|s'.cnt| Int)
    )
    Bool

    (and
        (=> |s'.start_stop|
            (= |s'.is_counting| (not |s.is_counting|))
        )
        (=> (not |s'.start_stop|)
            (= |s'.is_counting| |s.is_counting|)
        )
        (= |s'.cnt|
            (ite |s'.reset|
                0
                (ite |s'.is_counting|
                    (+ |s.cnt| 1)
                    |s.cnt|
                )
            )
        )
    )
)

; State 0.
(declare-const start_stop_0 Bool)
(declare-const reset_0 Bool)
(declare-const is_counting_0 Bool)
(declare-const cnt_0 Int)
; State 1.
(declare-const start_stop_1 Bool)
(declare-const reset_1 Bool)
(declare-const is_counting_1 Bool)
(declare-const cnt_1 Int)
; State 2.
(declare-const start_stop_2 Bool)
(declare-const reset_2 Bool)
(declare-const is_counting_2 Bool)
(declare-const cnt_2 Int)

; State 0 is initial.
(assert
    (init start_stop_0 reset_0 is_counting_0 cnt_0)
)

; State 1 is a successor of state 0.
(assert
    (trans
        start_stop_0 reset_0 is_counting_0 cnt_0
        start_stop_1 reset_1 is_counting_1 cnt_1
    )
)

; State 2 is a successor of state 1.
(assert
    (trans
        start_stop_1 reset_1 is_counting_1 cnt_1
        start_stop_2 reset_2 is_counting_2 cnt_2
    )
)

; State 2 must falsify the candidate.
(assert
    (not (>= cnt_2 0))
)

; Is this possible?
(check-sat)

Output:

> z3 test.smt2
unsat

BMC with Actlits

Expand this for the full code.

; Initial predicate.
(define-fun init
    (
        (|s.start_stop| Bool)
        (|s.reset| Bool)
        (|s.is_counting| Bool)
        (|s.cnt| Int)
    )
    Bool

    (and
        (= |s.is_counting| |s.start_stop|)
        (=> |s.reset| (= |s.cnt| 0))
        (>= |s.cnt| 0)
    )
)

; Transition relation.
(define-fun trans
    (
        ; "Previous" state.
        (|s.start_stop| Bool)
        (|s.reset| Bool)
        (|s.is_counting| Bool)
        (|s.cnt| Int)
        ; "Next" state.
        (|s'.start_stop| Bool)
        (|s'.reset| Bool)
        (|s'.is_counting| Bool)
        (|s'.cnt| Int)
    )
    Bool

    (and
        (=> |s'.start_stop|
            (= |s'.is_counting| (not |s.is_counting|))
        )
        (=> (not |s'.start_stop|)
            (= |s'.is_counting| |s.is_counting|)
        )
        (= |s'.cnt|
            (ite |s'.reset|
                0
                (ite |s'.is_counting|
                    (+ |s.cnt| 1)
                    |s.cnt|
                )
            )
        )
    )
)

; State 0.
(declare-const start_stop_0 Bool)
(declare-const reset_0 Bool)
(declare-const is_counting_0 Bool)
(declare-const cnt_0 Int)
; State 1.
(declare-const start_stop_1 Bool)
(declare-const reset_1 Bool)
(declare-const is_counting_1 Bool)
(declare-const cnt_1 Int)
; State 2.
(declare-const start_stop_2 Bool)
(declare-const reset_2 Bool)
(declare-const is_counting_2 Bool)
(declare-const cnt_2 Int)

; State 0 is initial.
(assert
    (init start_stop_0 reset_0 is_counting_0 cnt_0)
)

; Activation literal for the first check.
(declare-const actlit_0 Bool)
; Conditional assertion of the negation of the candidate at 0.
(assert (=> actlit_0
    (not (>= cnt_0 0))
))
; Check-sat, assuming `actlit_0` is true.
(echo "; info: falsification at depth 0?")
(check-sat-assuming ( actlit_0 ))
; Solver answers `unsat`, we want to unroll the system some more.
; Before we do that, we deactivate the actlit.
(assert (not actlit_0))
; At this point, the solver realized the conditional assertion
; of the negation of the candidate is trivially `true`, and will
; ignore it from now on.

(echo "; info: making sure assertion at 0 is not active anymore, expecting `sat`")
(check-sat)

(assert
    (trans
        start_stop_0 reset_0 is_counting_0 cnt_0
        start_stop_1 reset_1 is_counting_1 cnt_1
    )
)
(declare-const actlit_1 Bool)
(assert (=> actlit_1
    (not (>= cnt_1 0))
))
(echo "; info: falsification at depth 1?")
(check-sat-assuming ( actlit_1 ))
(assert (not actlit_1))
(echo "; info: making sure assertion at 1 is not active anymore, expecting `sat`")
(check-sat)

(assert
    (trans
        start_stop_1 reset_1 is_counting_1 cnt_1
        start_stop_2 reset_2 is_counting_2 cnt_2
    )
)
(declare-const actlit_2 Bool)
(assert (=> actlit_2
    (not (>= cnt_2 0))
))
(echo "; info: falsification at depth 2?")
(check-sat-assuming ( actlit_2 ))
(assert (not actlit_2))
(echo "; info: making sure assertion at 2 is not active anymore, expecting `sat`")
(check-sat)

Output:

> z3 test.smt2
; info: falsification at depth 0?
unsat
; info: making sure assertion at 0 is not active anymore, expecting `sat`
sat
; info: falsification at depth 1?
unsat
; info: making sure assertion at 1 is not active anymore, expecting `sat`
sat
; info: falsification at depth 2?
unsat
; info: making sure assertion at 2 is not active anymore, expecting `sat`
sat

BMC: Mikino

Mikino is a small transition system verification engine that relies on SMT solvers and everything we have seen so far (and will see later). It is designed to be relatively simple with user experience front and center: the goal is to have a tool that is gratifying to interact with to teach about induction-based verification.

Most examples from this point will rely on mikino, so I encourage you to install it so that you can mess around with my examples and get a better understanding. See the mikino appendix for setup instructions.

Input Format

Mikino takes as input a transition system in a format consistent but slightly different from what we have seen up to this point. Systems are written in files organized as follows, illustrated on our stopwatch running example.

First are state variable declarations. It is a list of declarations between braces introduced by the svars keyword and of form <var_1> <var_2> ... <var_n>: <type> with n ≥ 1.

#![allow(unused)]
fn main() {
/// State variables.
svars {
	/// Inputs of the system.
	start_stop reset: bool,
	/// Keeps track of whether we are counting.
	is_counting: bool,
	/// Counts time, output of the system.
	cnt: int,
}
}

Next is the initial predicate, introduced by the init keyword. Mikino does not support SMT-LIB-2-like (s-)expressions (anymore), and instead expects Rust-like expressions. Note that mikino supports common unicode operators such as ∧, ⋀, ∨, ⋁, ≥ and ⇒.

#![allow(unused)]
fn main() {
/// Initial predicate.
init {
	is_counting = start_stop,
	cnt ≥ 0,
	(reset ⇒ cnt = 0),
}
}

Here, we gave init a list of three comma-separated (with optional trailing comma) expressions. This list is understood as a conjunction ⋀, meaning the list above is equivalent to writing is_counting = start_stop ⋀ cnt ≥ 0 ⋀ (reset ⇒ cnt = 0).

The transition relation definition, introduced by the trans keyword, differs slightly. Remember that the transition relation relates two states: the previous one and the next one. In mikino, we refer to the previous version of a state variable svar by simply writing svar. If we want to refer to its next version, we must use the ' (prime) prefix operator: 'svar.

#![allow(unused)]
fn main() {
/// Transition relation.
trans {
	// The *next* value of `is_counting` is equal to...
	'is_counting = if 'start_stop {
		// ...if `'start_stop` is true, then the negation of
		// its *previous* value...
		¬is_counting
	} else {
		// ...otherwise, it is equal to its previous value.
		is_counting
	},
	'cnt = if 'reset {
		0
	} else if 'is_counting {
		cnt + 1
	} else {
		cnt
	},
}
}

trans also accepts a comma-separated list of expressions understood as a conjunction ⋀.

Last are the candidate invariants, sometimes called Proof Objectives, introduced by the candidates keyword. They are given as a comma-separated list of named candidates of shape "string describing the candidate": <expr>. The name of a candidate is what mikino will use to refer to that candidate in its output.

#![allow(unused)]
fn main() {
/// Candidate invariants.
candidates {
	"cnt is positive": cnt ≥ 0,
	"cnt ≤ 2": cnt ≤ 2,
	"cnt ≤ 4": cnt ≤ 4,
}
}

Mikino's input format is designed to look relatively pretty with Rust syntax highlighting (which is used in the snippets above). It is definitely not legal Rust syntax though, so make sure rustfmt does not run on it as it will fail.

Run BMC

Mikino is a proof engine, meaning that it can prove invariants over transition systems as we will see very soon. For now, let's just use its BMC mode. As discussed previously, BMC is not a proof technique (at least in infinite reachable state spaces), it is a refutation technique: the point of BMC is to produce counterexamples to candidate invariants thus disproving them.

Let's try mikino on the stopwatch system described above. The full code is available in the Version 1 section, the following assumes that code is in a test.mkn file. Notice that the candidates

#![allow(unused)]
fn main() {
/// Candidate invariants.
candidates {
	"cnt is positive": cnt ≥ 0,
	"cnt ≤ 2": cnt ≤ 2,
	"cnt ≤ 4": cnt ≤ 4,
}
}

feature "cnt is positive", which we will soon prove is an invariant of the system. Hence, mikino's BMC will not be able to find a counterexample for this candidate. We are thus going to run BMC with a maximum depth, i.e. we will give mikino a maximum number of unrollings to perform: 10. The remaining candidates however are falsifiable.

To put mikino in BMC mode, we need to pass it the bmc sub-command when we run it. We will also use the --bmc_max <int> flag that specifies a maximum BMC unrolling depth ≥ 0. If no maximum is given, mikino will run BMC until either all candidates are falsified or you end (Ctrl+C) the process manually (or it exhausts memory/time).

Mikino requires Z3 to run, you can retrieve a binary for your operating system on Z3's release page. Mikino, by default, assumes a Z3 binary is in your PATH with name z3. You can override this with the --z3_cmd command-line argument: mikino --z3_cmd "my_z3" ... or mikino --z3_cmd "./my_z3" ... if Z3 is not in your PATH but is in the current directory.

Let's try it. Mikino tries to improve its output's readability by using colors: unfortunately, this will not show in this plain text rendition. (As discussed when I introduced SMT, different versions of Z3 or even different operating system might produce different models. The same applies to mikino as its counterexamples are Z3 models.)

> mikino bmc --bmc_max 10 test.mkn
running BMC, looking for falsifications for 3 candidate(s)...
checking for falsifications at depth 0
found a falsification at depth 0:
- `cnt ≤ 2` = (<= cnt 2)
  |=| Step 0
  |         cnt = 3
  | is_counting = false
  |       reset = false
  |  start_stop = false
  |=|
found a falsification at depth 0:
- `cnt ≤ 4` = (<= cnt 4)
  |=| Step 0
  |         cnt = 5
  | is_counting = false
  |       reset = false
  |  start_stop = false
  |=|
checking for falsifications at depth 1
checking for falsifications at depth 2
checking for falsifications at depth 3
checking for falsifications at depth 4
checking for falsifications at depth 5
checking for falsifications at depth 6
checking for falsifications at depth 7
checking for falsifications at depth 8
checking for falsifications at depth 9
checking for falsifications at depth 10

|===| Bmc result
| - could not find falsifications for the following candidate(s)
|   `cnt is positive`
|
| - found a falsification for the following candidate(s)
|   `cnt ≤ 2`
|   `cnt ≤ 4`
|
| - system is unsafe
|===|

Pro tip: use the --smt_log <DIR> flag to specify a directory where mikino will create an SMT-LIB 2 file per solver it uses, and log all the commands issued to that solver. For instance,
> mikino bmc --smt_log smt_traces --bmc_max 10 test.mkn
> tree smt_traces/
smt_traces
└── bmc.smt2
This can be useful to inspect the exact checks mikino is performing and modify/relaunch them.

Mikino incrementally unrolls BMC just like we discussed in the previous chapter. It starts at depth 0, which means 0 transitions away from the initial states, which really means the initial states. Right away, it falsifies all our candidates but the first one. This is because of our initial predicate:

#![allow(unused)]
fn main() {
/// Initial predicate.
init {
	is_counting = start_stop,
	cnt ≥ 0,
	(reset ⇒ cnt = 0),
}
}

The system can start with any value for cnt as long as i) it is positive and ii) reset is not pressed. Mikino's output makes sense, but can we modify the system so that falsifiable candidates can only be falsified by unrolling more than 0 times?

We sure can, by changing init so that cnt always starts at 0.

#![allow(unused)]
fn main() {
/// Initial predicate.
init {
	is_counting = start_stop,
	cnt = 0,
}
}

We do not need to look at reset anymore since cnt will be 0 regardless. The full code for this new version is available in the Version 2 section. We run mikino in BMC mode again, and this time we get

> mikino bmc --bmc_max 10 test.mkn
running BMC, looking for falsifications for 3 candidate(s)...
checking for falsifications at depth 0
checking for falsifications at depth 1
checking for falsifications at depth 2
checking for falsifications at depth 3
found a falsification at depth 3:
- `cnt ≤ 2` = (<= cnt 2)
  |=| Step 0
  |         cnt = 0
  | is_counting = false
  |       reset = false
  |  start_stop = false
  |=| Step 1
  |         cnt = 1
  | is_counting = true
  |       reset = false
  |  start_stop = true
  |=| Step 2
  |         cnt = 2
  | is_counting = true
  |       reset = false
  |  start_stop = false
  |=| Step 3
  |         cnt = 3
  | is_counting = true
  |       reset = false
  |  start_stop = false
  |=|
checking for falsifications at depth 4
checking for falsifications at depth 5
found a falsification at depth 5:
- `cnt ≤ 4` = (<= cnt 4)
  |=| Step 0
  |         cnt = 0
  | is_counting = false
  |       reset = false
  |  start_stop = false
  |=| Step 1
  |         cnt = 1
  | is_counting = true
  |       reset = false
  |  start_stop = true
  |=| Step 2
  |         cnt = 2
  | is_counting = true
  |       reset = false
  |  start_stop = false
  |=| Step 3
  |         cnt = 3
  | is_counting = true
  |       reset = false
  |  start_stop = false
  |=| Step 4
  |         cnt = 4
  | is_counting = true
  |       reset = false
  |  start_stop = false
  |=| Step 5
  |         cnt = 5
  | is_counting = true
  |       reset = false
  |  start_stop = false
  |=|
checking for falsifications at depth 6
checking for falsifications at depth 7
checking for falsifications at depth 8
checking for falsifications at depth 9
checking for falsifications at depth 10

|===| Bmc result
| - could not find falsifications for the following candidate(s)
|   `cnt is positive`
|
| - found a falsification for the following candidate(s)
|   `cnt ≤ 2`
|   `cnt ≤ 4`
|
| - system is unsafe
|===|

Mikino is not able to falsify the falsifiable candidates in the initial states (depth 0, i.e. zero unrollings of the transition relation) anymore, which was the whole point of the modification to init we just made. Mikino proceeds to check for falsifications at increasing depth. Once it reaches depth 3, a falsification for cnt ≤ 2 is found and a counterexample is produced. The counterexample shows the whole trace, from an initial state to a state falsifying the candidate because cnt = 3 and 3 ≤ 2 is not true.

Mikino keeps going with the remaining candidates. Although it does not appear in the output, after finding a counterexample at depth 3 mikino checks the remaining candidates (without cnt ≤ 2) at depth 3. We got one counterexample for one candidate, but there might be a different counterexample for another candidate at the same depth.

This is not the case here, and mikino proceeds to unroll the transition relation some more. It finds another counterexample at depth 5 for cnt ≤ 4 and displays the whole trace, as expected.

Let's modify our candidates, full code available in the Version 3 section.

#![allow(unused)]
fn main() {
/// Candidate invariants, or "Proof Objectives" (`po_s`).
candidates {
	"cnt is positive": cnt ≥ 0,
	"reset works": reset ⇒ cnt = 0,
	"is_counting implies cnt > 0": (is_counting ⋀ ¬start_stop) ⇒ cnt > 0,
}
}

You can place your bets as to which of these candidates are actual invariants. The third candidate is a bit strange, we will discuss why it is written that way shortly. Again, BMC cannot prove that any of them are indeed invariants, but it can disprove some of them if it finds a counterexample at some depth.

> mikino bmc --bmc_max 10 test.mkn
running BMC, looking for falsifications for 3 candidate(s)...
checking for falsifications at depth 0
checking for falsifications at depth 1
found a falsification at depth 1:
- `is_counting implies cnt > 0` = (=> (and is_counting (not start_stop)) (> cnt 0))
  |=| Step 0
  |         cnt = 0
  | is_counting = true
  |       reset = false
  |  start_stop = true
  |=| Step 1
  |         cnt = 0
  | is_counting = true
  |       reset = true
  |  start_stop = false
  |=|
checking for falsifications at depth 2
checking for falsifications at depth 3
checking for falsifications at depth 4
checking for falsifications at depth 5
checking for falsifications at depth 6
checking for falsifications at depth 7
checking for falsifications at depth 8
checking for falsifications at depth 9
checking for falsifications at depth 10

|===| Bmc result
| - could not find falsifications for the following candidate(s)
|   `cnt is positive`
|   `reset works`
|
| - found a falsification for the following candidate(s)
|   `is_counting implies cnt > 0`
|
| - system is unsafe
|===|

Candidate is_counting implies cnt > 0 was falsified. The idea of this candidate is that, when the system is_counting, cnt should increase and thus be strictly positive (more on that in the note below). Mikino shows us this is not true however, because reset has higher priority in our transition relation and causes cnt to be 0 regardless of is_counting's value.

We had to somewhat artificially write the candidate as (is_counting ⋀ ¬start_stop) ⇒ cnt > 0. Based on the paragraph above, the is_counting ⋀ ¬start_stop part should really be is_counting. The problem with this is that we actually ignore is_counting in the initial state.

Hence, we would get a initial state counterexample where start_stop is true, meaning is_counting is true, but cnt ignores it and is just 0. As authors, we wanted to show a counterexample where reset prevents cnt from increasing despite start_stop being true, and thus had to distort the candidate a little bit.

A better way to write this candidate is is_counting ⇒ 'cnt > cnt. It would still be falsifiable, for the same reason and with the same counterexample, but it would make more sense. Sadly, mikino does not currently support "two-state candidates", i.e. candidates that refer to a previous state.

Checking two-state candidates differs slightly from regular (one-state) candidates in that they make no sense in the initial states (depth 0) because there is no previous state there. Hence, a two states invariant defined as two_state_expr is understood as being the expression true in the initial states (which holds, obviously), and two_state_expr at depth > 0 since there is a previous state to refer to.

Full Code for All Examples

Version 1

Expand this for the full code.

#![allow(unused)]
fn main() {
/// State variables.
svars {
	/// Inputs of the system.
	start_stop reset: bool,
	/// Keeps track of whether we are counting.
	is_counting: bool,
	/// Counts time, output of the system.
	cnt: int,
}

/// Initial predicate.
init {
	is_counting = start_stop,
	cnt ≥ 0,
	(reset ⇒ cnt = 0),
}

/// Transition relation.
trans {
	// The *next* value of `is_counting` is equal to...
	'is_counting = if 'start_stop {
		// ...if `'start_stop` is true, then the negation of
		// its *previous* value...
		¬is_counting
	} else {
		// ...otherwise, it is equal to its previous value.
		is_counting
	},
	'cnt = if 'reset {
		0
	} else if 'is_counting {
		cnt + 1
	} else {
		cnt
	},
}

/// Candidate invariants.
candidates {
	"cnt is positive": cnt ≥ 0,
	"cnt ≤ 2": cnt ≤ 2,
	"cnt ≤ 4": cnt ≤ 4,
}
}

Output:

> mikino bmc --bmc_max 10 test.mkn
running BMC, looking for falsifications for 3 candidate(s)...
checking for falsifications at depth 0
found a falsification at depth 0:
- `cnt ≤ 2` = (<= cnt 2)
  |=| Step 0
  |         cnt = 3
  | is_counting = false
  |       reset = false
  |  start_stop = false
  |=|
found a falsification at depth 0:
- `cnt ≤ 4` = (<= cnt 4)
  |=| Step 0
  |         cnt = 5
  | is_counting = false
  |       reset = false
  |  start_stop = false
  |=|
checking for falsifications at depth 1
checking for falsifications at depth 2
checking for falsifications at depth 3
checking for falsifications at depth 4
checking for falsifications at depth 5
checking for falsifications at depth 6
checking for falsifications at depth 7
checking for falsifications at depth 8
checking for falsifications at depth 9
checking for falsifications at depth 10

|===| Bmc result
| - could not find falsifications for the following candidate(s)
|   `cnt is positive`
|
| - found a falsification for the following candidate(s)
|   `cnt ≤ 2`
|   `cnt ≤ 4`
|
| - system is unsafe
|===|

Version 2

Expand this for the full code.

#![allow(unused)]
fn main() {
/// State variables.
svars {
	/// Inputs of the system.
	start_stop reset: bool,
	/// Keeps track of whether we are counting.
	is_counting: bool,
	/// Counts time, output of the system.
	cnt: int,
}

/// Initial predicate.
init {
	is_counting = start_stop,
	cnt = 0,
}

/// Transition relation.
trans {
	// The *next* value of `is_counting` is equal to...
	'is_counting = if 'start_stop {
		// ...if `'start_stop` is true, then the negation of
		// its *previous* value...
		¬is_counting
	} else {
		// ...otherwise, it is equal to its previous value.
		is_counting
	},
	'cnt = if 'reset {
		0
	} else if 'is_counting {
		cnt + 1
	} else {
		cnt
	},
}

/// Candidate invariants.
candidates {
	"cnt is positive": cnt ≥ 0,
	"cnt ≤ 2": cnt ≤ 2,
	"cnt ≤ 4": cnt ≤ 4,
}
}

Output:

> mikino bmc --bmc_max 10 test.mkn
running BMC, looking for falsifications for 3 candidate(s)...
checking for falsifications at depth 0
checking for falsifications at depth 1
checking for falsifications at depth 2
checking for falsifications at depth 3
found a falsification at depth 3:
- `cnt ≤ 2` = (<= cnt 2)
  |=| Step 0
  |         cnt = 0
  | is_counting = false
  |       reset = false
  |  start_stop = false
  |=| Step 1
  |         cnt = 1
  | is_counting = true
  |       reset = false
  |  start_stop = true
  |=| Step 2
  |         cnt = 2
  | is_counting = true
  |       reset = false
  |  start_stop = false
  |=| Step 3
  |         cnt = 3
  | is_counting = true
  |       reset = false
  |  start_stop = false
  |=|
checking for falsifications at depth 4
checking for falsifications at depth 5
found a falsification at depth 5:
- `cnt ≤ 4` = (<= cnt 4)
  |=| Step 0
  |         cnt = 0
  | is_counting = false
  |       reset = false
  |  start_stop = false
  |=| Step 1
  |         cnt = 1
  | is_counting = true
  |       reset = false
  |  start_stop = true
  |=| Step 2
  |         cnt = 2
  | is_counting = true
  |       reset = false
  |  start_stop = false
  |=| Step 3
  |         cnt = 3
  | is_counting = true
  |       reset = false
  |  start_stop = false
  |=| Step 4
  |         cnt = 4
  | is_counting = true
  |       reset = false
  |  start_stop = false
  |=| Step 5
  |         cnt = 5
  | is_counting = true
  |       reset = false
  |  start_stop = false
  |=|
checking for falsifications at depth 6
checking for falsifications at depth 7
checking for falsifications at depth 8
checking for falsifications at depth 9
checking for falsifications at depth 10

|===| Bmc result
| - could not find falsifications for the following candidate(s)
|   `cnt is positive`
|
| - found a falsification for the following candidate(s)
|   `cnt ≤ 2`
|   `cnt ≤ 4`
|
| - system is unsafe
|===|

Version 3

Expand this for the full code.

#![allow(unused)]
fn main() {
/// State variables.
svars {
	/// Inputs of the system.
	start_stop reset: bool,
	/// Keeps track of whether we are counting.
	is_counting: bool,
	/// Counts time, output of the system.
	cnt: int,
}

/// Initial predicate.
init {
	is_counting = start_stop,
	cnt = 0,
}

/// Transition relation.
trans {
	// The *next* value of `is_counting` is equal to...
	'is_counting = if 'start_stop {
		// ...if `'start_stop` is true, then the negation of
		// its *previous* value...
		¬is_counting
	} else {
		// ...otherwise, it is equal to its previous value.
		is_counting
	},
	'cnt = if 'reset {
		0
	} else if 'is_counting {
		cnt + 1
	} else {
		cnt
	},
}

/// Candidate invariants, or "Proof Objectives" (`po_s`).
candidates {
	"cnt is positive": cnt ≥ 0,
	"reset works": reset ⇒ cnt = 0,
	"is_counting implies cnt > 0": (is_counting ⋀ ¬start_stop) ⇒ cnt > 0,
}
}

Output:

> mikino bmc --bmc_max 10 test.mkn
running BMC, looking for falsifications for 3 candidate(s)...
checking for falsifications at depth 0
checking for falsifications at depth 1
found a falsification at depth 1:
- `is_counting implies cnt > 0` = (=> (and is_counting (not start_stop)) (> cnt 0))
  |=| Step 0
  |         cnt = 0
  | is_counting = true
  |       reset = false
  |  start_stop = true
  |=| Step 1
  |         cnt = 0
  | is_counting = true
  |       reset = true
  |  start_stop = false
  |=|
checking for falsifications at depth 2
checking for falsifications at depth 3
checking for falsifications at depth 4
checking for falsifications at depth 5
checking for falsifications at depth 6
checking for falsifications at depth 7
checking for falsifications at depth 8
checking for falsifications at depth 9
checking for falsifications at depth 10

|===| Bmc result
| - could not find falsifications for the following candidate(s)
|   `cnt is positive`
|   `reset works`
|
| - found a falsification for the following candidate(s)
|   `is_counting implies cnt > 0`
|
| - system is unsafe
|===|

Induction

Let's get a little bit abstract and meta. The incremental BMC approach we have seen in previous chapters can itself be seen as a transition system. To do this formally, we would need a whole bunch of notions from logics which are far beyond this book's scope. No matter, we can discuss BMC as a transition system informally, with words. Writing counterexample constantly is quite tedious, we will use the much shorter cex (plural cex-s) contraction instead. Also, assume there is only one candidate for simplicity.

We can see BMC as having a state: the unrolling depth k from the initial state at which it currently is. We can say it produces a boolean output that's true if a cex for the candidate exists at depth k. BMC's starting point is "check the initial states for a cex (of the candidate)", which we can rephrase as

init: unroll the system at depth 0 from the initial state and check for cex.

A BMC transition amounts to unrolling the transition relation one step further (depth k), and check for falsification at k. Rephrased to echo init's formulation, we get

trans(k-1, k): from an unrolling at k-1 from the initial states with no cex, unroll to k and check for a cex (with k > 0).

So now we have a representation of BMC as a transition system with its init predicate and trans relation.

It would be interesting to find a candidate invariant for BMC and try to prove it over the transition system representation of BMC we just introduced. As some readers have probably intuited, BMC actually has the property that it always finds the shortest cex possible in terms of depth (number of unrollings). More precisely, it finds one of them: if BMC produces a cex (trace of k states) of length k, there might be other cex-s of length k (and of length i > k). However, there cannot exist a shorter cex (of length i < k). More generally:

candidate(k): when BMC is unrolled at k from the initial states, then no cex of length 0 ≤ i < k exists.

To be clear, our goal is to find a way to prove that candidate is an invariant for BMC, which is represented as a transition system by the init predicate and trans relation above.

The question now is "How can we prove that BMC verifies candidate?", or "What would such a proof look like?". Back when we discussed transition system, we managed to prove a few properties regarding the stopwatch system's transition relation. For instance, we previously proved that assuming cnt_0 > 7, then we cannot have cnt_1 = 0 without reset_1 being true if state 1 is a successor of state 0.

So we could start building a proof for candidate by checking if it is a consequence of trans: is it true that trans(k-1, k) ⇒ candidate(k)?. Let's assume we have an unrolling at depth k-1 from the initial states with no cex; by trans, the next BMC step is to unroll to k and check for a cex at k. Looking at candidate now, is it the case that no cex of length i < k can exist?

Well no, looking only at the assumptions we made we cannot draw that conclusion: trans tells us there is no cex at k-1, but that's it. We know nothing of potential cex-s at i < k - 1. So, candidate is not a consequence of trans. All hope is not lost: our tiny proofs over the stopwatch system actually made assumptions about the previous state. "Assuming cnt_0 > 7, then we cannot have cnt_1 = 0 without ..."

Instead of checking if candidate is a consequence of trans (which it is not as we just saw) we could check trans preserves candidate. Since trans relates succeeding states k-1 and k, we say that trans preserves candidate if candidate(k-1) ∧ trans(k-1, k) ⇒ candidate(k). That is, "states verifying candidate cannot, in one application of trans, reach a state falsifying candidate".

Is it the case though? We take the same assumptions as above, when we looked at a transition from k-1 to k, and also assume candidate at k-1: "no cex of length i < k-1 exists". By trans, we unroll to k and check for a cex at k. Can there be cex of length i < k? No: trans tells us there was no cex at k-1, and our new candidate-assumption in the previous state tells us no cex of length i < kh-1 exists.

Sweet, trans preserves candidate: from a state verifying candidate, we can only reach states that also verify candidate. Hence, a state verifying candidate cannot lead to a state falsifying it by repeated applications of trans. Is this enough to decide candidate to be an invariant for BMC? No, unless we show all our initial states verify candidate.

Imagine for instance we got BMC wrong and started at depth 1 instead of 0, with exactly the same trans. Then, since we never checked for a cex at 0, candidate has no reason to be true at 1. More generally, if our initial states do not all verify candidate, then the fact that trans preserves candidate is not helpful because it says nothing about transitions from a state that does not verify candidate.

Do(es) BMC's initial state(s) verify candidate then? That is, when BMC is unrolled at 0 from the initial states, is it possible that a cex of length i with 0 ≤ i < 0 exists? Well, since there is no i such that 0 ≤ i < 0, then no.

Putting both results together we have

BMC's starting point verifies candidate, i.e. init ⇒ candidate(0), and
BMC's notion of transition preserves candidate, i.e. candidate(k-1) ∧ trans(k-1, k) ⇒ candidate(k).

Then, by induction, executions of BMC cannot ever falsify candidate.

One Last Short SMT Dive

To sum up, given a transition system 𝕋 with state variables s and specified by (init(s), trans(s, s')), we can invoke induction to prove that candidate(s) is an invariant for 𝕋 if we have shown both base and step:

base: for all s, init(s) ⇒ candidate(s);
step: for all s and s', candidate(s) ∧ trans(s, s') ⇒ candidate(s').

We can rephrase these two in terms of SMT solving and formula (un)satisfiability:

base: init(s) ∧ ¬candidate(s) is unsatisfiable;
step: candidate(s) ∧ trans(s, s') ∧ ¬candidate(s') is unsatisfiable.

We all know what this means: it is finally time to achieve our dream of proving that the stopwatch's counter is always positive. I will use the version that starts from cnt = 0, not the one where it can take an arbitrary positive value. Both versions work for this proof, but the former is better for obtaining non-trivial (length 0) counterexamples if we need to.

Readers eager to learn by doing can start from any of the previous SMT examples involving BMC and try to conduct the proof themselves. The SMT examples for BMC have definitions for both init and trans ready to use. The easy version consists in having an SMT-LIB script for the base case, and another one for the step case. Solution in the Stopwatch Base and Stopwatch Step sections.

Bonus points if you can do both with just one script, using activation literals. Perfect score if you can do both checks using only one activation literal, solely for the purpose of (de)activating init.

Perfect score solution in the Stopwatch Actlit section.

Base

SMT examples for BMC from previous chapters already have definitions for the stopwatch's init and trans. For convenience and readability, we define a candidate predicate over the system's counter:

(define-fun candidate ((|s.cnt| Int)) Bool
    (>= |s.cnt| 0)
)

In the base check, we are only concerned with the initial states. All we need to do

is declare our state variables,
assert that they are a legal initial state,
assert that they falsify our candidate, and
ask whether this is satisfiable.

(declare-const start_stop_0 Bool)
(declare-const reset_0 Bool)
(declare-const is_counting_0 Bool)
(declare-const cnt_0 Int)

(assert (init start_stop_0 reset_0 is_counting_0 cnt_0))
(assert (not (candidate cnt_0)))

; Is there a state that's initial but does not verify `candidate`?
(check-sat)

Z3 easily answers our question.

Full code in the Stopwatch Base section below.

> z3 test.smt2
unsat

Done: we proved the base case, step is next, let's move on.

Step

For the step check, which we are doing separately (in a different file) from base, we first need to declare two states since we need to check that trans preserves candidate.

; Previous state.
(declare-const start_stop_0 Bool)
(declare-const reset_0 Bool)
(declare-const is_counting_0 Bool)
(declare-const cnt_0 Int)
; Next state.
(declare-const start_stop_1 Bool)
(declare-const reset_1 Bool)
(declare-const is_counting_1 Bool)
(declare-const cnt_1 Int)

Next, we want to ask whether it is possible to have

state 0 verify candidate,
state 1 be a successor of state 0, and
state 0 falsify candidate.

(assert (candidate cnt_0))
(assert (trans
    start_stop_0 reset_0 is_counting_0 cnt_0
    start_stop_1 reset_1 is_counting_1 cnt_1
))
(assert (not (candidate cnt_1)))

; Is there a state verifying `candidate` that can
; reach a state falsifying it in one transition?
(check-sat)

And that's it. Unless Z3 decides to answer sat for some reason, we are done.

Full code in the Stopwatch Step section below.

> play drumroll.wav
> z3 test.smt2
unsat

Done and done. Both base and step hold, and thus we can finally invoke induction and conclude that cnt ≥ 0 is an invariant for the stopwatch system.

Before we move on to mikino's induction mode, some readers might want to check out Section Stopwatch Actlit below. In it, we conduct base and step in succession in a single file using an activation literal. That's not all we do however, there is a clever trick that we use for the checks. The trick is discussed in details in the comments.

Full Code For All Examples

Stopwatch Base

Expand this for the full code.

; Initial predicate.
(define-fun init
    (
        (|s.start_stop| Bool)
        (|s.reset| Bool)
        (|s.is_counting| Bool)
        (|s.cnt| Int)
    )
    Bool

    (and
        (= |s.is_counting| |s.start_stop|)
        (=> |s.reset| (= |s.cnt| 0))
        (>= |s.cnt| 0)
    )
)

(define-fun candidate ((|s.cnt| Int)) Bool
    (>= |s.cnt| 0)
)

(declare-const start_stop_0 Bool)
(declare-const reset_0 Bool)
(declare-const is_counting_0 Bool)
(declare-const cnt_0 Int)

(assert (init start_stop_0 reset_0 is_counting_0 cnt_0))
(assert (not (candidate cnt_0)))

; Is there a state that's initial but does not verify `candidate`?
(check-sat)

Output:

> z3 test.smt2
unsat

Stopwatch Step

Expand this for the full code.

; Initial predicate.
(define-fun init
    (
        (|s.start_stop| Bool)
        (|s.reset| Bool)
        (|s.is_counting| Bool)
        (|s.cnt| Int)
    )
    Bool

    (and
        (= |s.is_counting| |s.start_stop|)
        (=> |s.reset| (= |s.cnt| 0))
        (>= |s.cnt| 0)
    )
)
(define-fun trans
    (
        ; "Previous" state.
        (|s.start_stop| Bool)
        (|s.reset| Bool)
        (|s.is_counting| Bool)
        (|s.cnt| Int)
        ; "Next" state.
        (|s'.start_stop| Bool)
        (|s'.reset| Bool)
        (|s'.is_counting| Bool)
        (|s'.cnt| Int)
    )
    Bool

    (and
        (=> |s'.start_stop|
            (= |s'.is_counting| (not |s.is_counting|))
        )
        (=> (not |s'.start_stop|)
            (= |s'.is_counting| |s.is_counting|)
        )
        (= |s'.cnt|
            (ite |s'.reset|
                0
                (ite |s'.is_counting|
                    (+ |s.cnt| 1)
                    |s.cnt|
                )
            )
        )
    )
)

(define-fun candidate ((|s.cnt| Int)) Bool
    (>= |s.cnt| 0)
)

; Previous state.
(declare-const start_stop_0 Bool)
(declare-const reset_0 Bool)
(declare-const is_counting_0 Bool)
(declare-const cnt_0 Int)
; Next state.
(declare-const start_stop_1 Bool)
(declare-const reset_1 Bool)
(declare-const is_counting_1 Bool)
(declare-const cnt_1 Int)

(assert (candidate cnt_0))
(assert (trans
    start_stop_0 reset_0 is_counting_0 cnt_0
    start_stop_1 reset_1 is_counting_1 cnt_1
))
(assert (not (candidate cnt_1)))

; Is there a state verifying `candidate` that can
; reach a state falsifying it in one transition?
(check-sat)

Output:

> z3 test.smt2
unsat

Stopwatch Actlit

Expand this for the full code.

Until now, we performed the step check of an induction proof by giving ourselves a state 0 and a state 1 such that

trans(s_0, s_1): state 1 is state 0's successor,
candidate(s_0): state 0 verifies the candidate,
¬candidate(s_1): state 1 falsifies the candidate.

Now, the example below swaps the state indices 0 and 1. That is:

trans(s_1, s_0): state 0 is state 1's successor,
candidate(s_1): state 1 verifies the candidate,
¬candidate(s_0): state 0 falsifies the candidate.

This does not really change anything by itself, the check is same except that the indices have changed. We do need to be careful to extract the counterexample correctly though.

The reason we present this version is that this reverse-unrolling version lets us keep state 0 as the last state of the trace, i.e. the state on which the falsification occurs. In normal unrolling, if we wanted to unroll the transition relation more, we would need to introduce s_2, deactivate ¬candidate(s_1), assert candidate(s_1), and conditionally assert ¬candidate(s_2).

With reverse-unrolling we can just say s_2 is s_1's previous state, and assert candidate(s_2). We are not unrolling more than once here (a process called k-induction), but this reverse-unrolling trick is still convenient w.r.t. the base check. The base check asserts ¬candidate(s_0), which step also needs.

; Initial predicate.
(define-fun init
    (
        (|s.start_stop| Bool)
        (|s.reset| Bool)
        (|s.is_counting| Bool)
        (|s.cnt| Int)
    )
    Bool

    (and
        (= |s.is_counting| |s.start_stop|)
        (=> |s.reset| (= |s.cnt| 0))
        (>= |s.cnt| 0)
    )
)
(define-fun trans
    (
        ; "Previous" state.
        (|s.start_stop| Bool)
        (|s.reset| Bool)
        (|s.is_counting| Bool)
        (|s.cnt| Int)
        ; "Next" state.
        (|s'.start_stop| Bool)
        (|s'.reset| Bool)
        (|s'.is_counting| Bool)
        (|s'.cnt| Int)
    )
    Bool

    (and
        (=> |s'.start_stop|
            (= |s'.is_counting| (not |s.is_counting|))
        )
        (=> (not |s'.start_stop|)
            (= |s'.is_counting| |s.is_counting|)
        )
        (= |s'.cnt|
            (ite |s'.reset|
                0
                (ite |s'.is_counting|
                    (+ |s.cnt| 1)
                    |s.cnt|
                )
            )
        )
    )
)

(define-fun candidate ((|s.cnt| Int)) Bool
    (>= |s.cnt| 0)
)


(declare-const start_stop_0 Bool)
(declare-const reset_0 Bool)
(declare-const is_counting_0 Bool)
(declare-const cnt_0 Int)

; Wait, shouldn't this be under an activation literal?
(assert (not (candidate cnt_0)))
; No because we're being very clever. More on that in the
; step check below.

(echo "base check, expecting `unsat`")
(declare-const base_actlit Bool)
(assert (=> base_actlit
    (init start_stop_0 reset_0 is_counting_0 cnt_0)
))
(check-sat-assuming (base_actlit))


(declare-const start_stop_1 Bool)
(declare-const reset_1 Bool)
(declare-const is_counting_1 Bool)
(declare-const cnt_1 Int)

(echo "step check, expecting `unsat`")
(assert
    (trans
        ; State `1` is first?
        start_stop_1 reset_1 is_counting_1 cnt_1
        ; State `0` is its successor?
        start_stop_0 reset_0 is_counting_0 cnt_0
    )
)
(assert (candidate cnt_1))
; Most unhorthodox. We are reverse-unrolling™.
; When we checked for base above, we asserted `(not (candidate cnt_0))`
; **unconditionnaly**. So at this point, we have
; - candidate(s_1)
; - trans(s_1, s_0)
; - ¬candidate(s_0)
;
; By unrolling backwards, with `s_0` the *last* state, we can reverse-unroll
; without changing anything, just adding a state `s_2` and asserting
; `trans(s_2, s_1)`.
;
; This is useful when doing "k-induction", which requires unrolling more than
; once in step (and base), and because SMT-solvers work by **learning** facts
; about the SMT instance they work on. These facts are *kept between checks*.
; So, Z3 will learn facts from the three assertions above in the `check-sat`
; below. If we reverse-unroll once more by adding an `s_2` as the predecessor
; of `s_1`, then Z3 will be able to re-use facts it learnt since we only added
; to the instance, but did not change anything that was there.

(check-sat)

(echo "induction proof complete")

Output:

> z3 test.smt2
base check, expecting `unsat`
unsat
step check, expecting `unsat`
unsat
induction proof complete

Induction: Mikino and Step Cex-s

BMC is not the only thing mikino can do. It also has an induction mode which is activated with the check sub-command.

Pro tip: remember the --smt_log <DIR> flag from mikino's bmc mode? It specifies a directory where mikino will create one SMT-LIB 2 file per solver it uses, and log all the commands issued to that solver. Mikino's check mode has it too:
> mikino check --smt_log smt_traces test.mkn
> tree smt_traces/
smt_traces
├── base.smt2
└── step.smt2
This can be useful to inspect the exact checks mikino is performing and modify/relaunch them.

Let's make sure mikino is able to prove that cnt ≥ 0 on the stopwatch system. I am using the version of the system that starts at 0

#![allow(unused)]
fn main() {
/// Initial predicate.
init {
	is_counting = start_stop,
	cnt = 0,
}
}

with a cnt ≥ 0 candidate as well as a few falsifiable other candidates:

#![allow(unused)]
fn main() {
/// Candidate invariants, or "Proof Objectives" (`po_s`).
candidates {
	"cnt is positive": cnt ≥ 0,
	"cnt ≤ 2": cnt ≤ 2,
	"cnt ≤ 4": cnt ≤ 4,
}
}

Let's run mikino in check mode on this system, full code in the Full Code section.

> mikino check test.mkn
checking base case...
success: all candidate(s) hold in the base state

checking step case...
failed: the following candidate(s) are not inductive:
- `cnt ≤ 2` = (<= cnt 2)
  |=| Step k
  |         cnt = 2
  | is_counting = false
  |       reset = false
  |  start_stop = false
  |=| Step k + 1
  |         cnt = 3
  | is_counting = true
  |       reset = false
  |  start_stop = true
  |=|
- `cnt ≤ 4` = (<= cnt 4)
  |=| Step k
  |         cnt = 4
  | is_counting = true
  |       reset = false
  |  start_stop = false
  |=| Step k + 1
  |         cnt = 5
  | is_counting = true
  |       reset = false
  |  start_stop = false
  |=|

|===| Induction attempt result
| - all candidates hold in the initial state(s)
|
| - the following candidate(s) are not inductive (not preserved by the transition relation)
|   `cnt ≤ 2`
|   `cnt ≤ 4`
|
| - system might be unsafe, some candidate(s) are not inductive
|
| - the following candidate(s) hold in the initial state(s) and are inductive
|   and thus hold in all reachable states of the system:
|   `cnt is positive`
|===|

Looking just at the final result, mikino is telling us that all candidates hold in the initial state(s). So, the base part of the induction proof holds for all candidates. Next, mikino reports that two of the candidates are not preserved by the transition relation. Since the check part of the induction proof does not hold for these candidates, mikino does not know whether they hold and tells us that the system might be unsafe. Based on the checks mikino performed, it cannot decide whether they are invariants or not.

Last, mikino reports that cnt is positive is actually preserved by the transition relation meaning step, in addition to base, holds for this candidate. Mikino can thus conclude that it is an invariant for the system.

If we take a closer look at mikino's output during the step checks, we see that mikino is doing more that just saying some step checks failed. When they do, mikino also outputs a step counterexample (cex). Remember what a step check is: for any state k

assuming state k verifies candidate,
assuming state k+1 is a successor of state k,
is it possible that state k+1 falsifies candidate?

If it is possible, it means that there exists a state k verifying candidate which has a successor state k+1 falsifying candidate. Under the hood, this means the solver answered sat to mikino's step check-sat query, meaning mikino can invoke get-model for step cex: a pair of succeeding states showing that candidate is not necessarily preserved by the transition relation.

For candidate cnt ≥ 2 for instance, mikino lets us know that from a state where cnt = 2 which verifies the candidate, it is possible in one transition to reach a state where cnt = 3 which falsifies the candidate. Mikino gives us the values of all state variables so that we know how precisely the bad state can be reached. There might be more than one step cex, as is the case for candidate cnt ≥ 2: mikino (the SMT solver, really) decides to start counting in step k+1 in the step cex, but we could get the same result if we were already counting in step k.

This notion of step cex is important because, on real systems, candidates tend not to be inductive. We will discuss this in the next chapter, but a candidate can be an invariant without being inductive. There are various ways we can go about proving that a non-inductive candidate is an invariant, but most of them (including the one we will discuss soon) involve manually or automatically looking at step cex-s to understand why the candidate is not inductive and "act" accordingly. (The meaning of "act" depends on the actual technique used to get around non-inductiveness.)

Run BMC, Again

We can change the mikino command we used to instruct mikino to run BMC on the candidates it failed to prove. For instance, mikino check --bmc test.mkn will run BMC after the proof attempts in an attempt to falsify remaining candidates. More precisely, this command will run BMC without a maximum unrolling depth.

On this simple example, we already know the remaining candidates are falsifiable in a small number of transitions. When we do not have this information, it can be a good idea to specify a maximum unrolling depth with --bmc_max <int> just like we did in bmc mode. Note that using the --bmc_max flag automatically activates BMC, so we don't need the --bmc flag anymore.

On our example

#![allow(unused)]
fn main() {
/// Candidate invariants, or "Proof Objectives" (`po_s`).
candidates {
	"cnt is positive": cnt ≥ 0,
	"cnt ≤ 2": cnt ≤ 2,
	"cnt ≤ 4": cnt ≤ 4,
}
}

the last two candidates should be falsifiable at depth 3 and 5 respectively. Let's make sure this is the case.

> mikino check --bmc_max 5 test.mkn
checking base case...
success: all candidate(s) hold in the base state

checking step case...
failed: the following candidate(s) are not inductive:
- `cnt ≤ 2` = (<= cnt 2)
  |=| Step k
  |         cnt = 2
  | is_counting = false
  |       reset = false
  |  start_stop = false
  |=| Step k + 1
  |         cnt = 3
  | is_counting = true
  |       reset = false
  |  start_stop = true
  |=|
- `cnt ≤ 4` = (<= cnt 4)
  |=| Step k
  |         cnt = 4
  | is_counting = true
  |       reset = false
  |  start_stop = false
  |=| Step k + 1
  |         cnt = 5
  | is_counting = true
  |       reset = false
  |  start_stop = false
  |=|

|===| Induction attempt result
| - all candidates hold in the initial state(s)
|
| - the following candidate(s) are not inductive (not preserved by the transition relation)
|   `cnt ≤ 2`
|   `cnt ≤ 4`
|
| - system might be unsafe, some candidate(s) are not inductive
|
| - the following candidate(s) hold in the initial state(s) and are inductive
|   and thus hold in all reachable states of the system:
|   `cnt is positive`
|===|

running BMC, looking for falsifications for 2 candidate(s)...
checking for falsifications at depth 0
checking for falsifications at depth 1
checking for falsifications at depth 2
checking for falsifications at depth 3
found a falsification at depth 3:
- `cnt ≤ 2` = (<= cnt 2)
  |=| Step 0
  |         cnt = 0
  | is_counting = true
  |       reset = false
  |  start_stop = true
  |=| Step 1
  |         cnt = 1
  | is_counting = true
  |       reset = false
  |  start_stop = false
  |=| Step 2
  |         cnt = 2
  | is_counting = true
  |       reset = false
  |  start_stop = false
  |=| Step 3
  |         cnt = 3
  | is_counting = true
  |       reset = false
  |  start_stop = false
  |=|
checking for falsifications at depth 4
checking for falsifications at depth 5
found a falsification at depth 5:
- `cnt ≤ 4` = (<= cnt 4)
  |=| Step 0
  |         cnt = 0
  | is_counting = true
  |       reset = false
  |  start_stop = true
  |=| Step 1
  |         cnt = 1
  | is_counting = true
  |       reset = false
  |  start_stop = false
  |=| Step 2
  |         cnt = 2
  | is_counting = true
  |       reset = false
  |  start_stop = false
  |=| Step 3
  |         cnt = 3
  | is_counting = true
  |       reset = false
  |  start_stop = false
  |=| Step 4
  |         cnt = 4
  | is_counting = true
  |       reset = false
  |  start_stop = false
  |=| Step 5
  |         cnt = 5
  | is_counting = true
  |       reset = false
  |  start_stop = false
  |=|

|===| Bmc result
| - found a falsification for the following candidate(s)
|   `cnt ≤ 2`
|   `cnt ≤ 4`
|
| - system is unsafe
|===|

Full Code

Expand this for the full code.

#![allow(unused)]
fn main() {
/// State variables.
svars {
	/// Inputs of the system.
	start_stop reset: bool,
	/// Keeps track of whether we are counting.
	is_counting: bool,
	/// Counts time, output of the system.
	cnt: int,
}

/// Initial predicate.
init {
	is_counting = start_stop,
	cnt = 0,
}

/// Transition relation.
trans {
	// The *next* value of `is_counting` is equal to...
	'is_counting = if 'start_stop {
		// ...if `'start_stop` is true, then the negation of
		// its *previous* value...
		¬is_counting
	} else {
		// ...otherwise, it is equal to its previous value.
		is_counting
	},
	'cnt = if 'reset {
		0
	} else if 'is_counting {
		cnt + 1
	} else {
		cnt
	},
}

/// Candidate invariants, or "Proof Objectives" (`po_s`).
candidates {
	"cnt is positive": cnt ≥ 0,
	"cnt ≤ 2": cnt ≤ 2,
	"cnt ≤ 4": cnt ≤ 4,
}
}

Output:

> mikino bmc --bmc_max 10 test.mkn
checking base case...
success: all candidate(s) hold in the base state

checking step case...
failed: the following candidate(s) are not inductive:
- `cnt ≤ 2` = (<= cnt 2)
  |=| Step k
  |         cnt = 2
  | is_counting = false
  |       reset = false
  |  start_stop = false
  |=| Step k + 1
  |         cnt = 3
  | is_counting = true
  |       reset = false
  |  start_stop = true
  |=|
- `cnt ≤ 4` = (<= cnt 4)
  |=| Step k
  |         cnt = 4
  | is_counting = true
  |       reset = false
  |  start_stop = false
  |=| Step k + 1
  |         cnt = 5
  | is_counting = true
  |       reset = false
  |  start_stop = false
  |=|

|===| Induction attempt result
| - all candidates hold in the initial state(s)
|
| - the following candidate(s) are not inductive (not preserved by the transition relation)
|   `cnt ≤ 2`
|   `cnt ≤ 4`
|
| - system might be unsafe, some candidate(s) are not inductive
|
| - the following candidate(s) hold in the initial state(s) and are inductive
|   and thus hold in all reachable states of the system:
|   `cnt is positive`
|===|

Candidate Strengthening

Candidate strengthening is about making non-inductive candidates inductive (when possible). It is somewhat difficult to come up with an example that is

interesting for strengthening,

not too artificial, i.e. is relatively realistic for a developer, and

is accessible without too much explanation.

While not extremely complex, the central example of this chapter and the manipulations in general are going to be more involved than what we have discussed so far.

This chapter also touches on the very high complexity and potential undecidability of verification.

This chapter is quite technical, and a bit theoretical. It is recommended that you understand all the concepts introduced so far before diving into this chapter. Some understanding of Rust could help in places, although it is by no means mandatory.

We have seen two kinds of candidate up to this point:

inductive candidates, meaning induction can prove they are invariants, and
falsifiable candidates, which can be falsified by running BMC for long enough.

Not all invariants are inductive. Meaning it is possible to get a step counterexample, i.e. the transition relation does not preserve the candidate, even though the candidate is an invariant and no legal trace of states can falsify it.

Array Value Grouping

Let's switch gears and look at an actual piece of (Rust) code. Assume we have an array arr of statically-known size len of elements of type T (arr has type [T; len]. Say we also have an integer (usize) value grouping. What we want to do is fold over successive groups (sub-arrays) of length grouping of the elements of arr.

In practice, we want to have a type Wrap that stores arr and grouping, and exposes a fold function over values of type &[T] which is guaranteed to store exactly grouping elements. Fold implements an sliding, non-overlapping window of length grouping over arr. Here is what using it would look like.

fn main() {
    // `len` ~~~~~~v
    let arr: [f64; 6] = [0., 1., 2., 3., 4., 5.];
    // `grouping` ~~~~~~~~~~~~v
    let wrap = Wrap::new(arr, 3);
    let value_1 = wrap.fold(0., |acc, arr| {
        println!(
            "len: {} | arr[0]: {}, arr[1]: {}, arr[2]: {}",
            arr.len(),
            arr[0],
            arr[1],
            arr[2]
        );
        assert_eq!(arr.len(), 3);
        let new_acc = acc + arr[0] * arr[1] * arr[2];
        println!("acc: {}, new_acc: {}", acc, new_acc);
        new_acc
    });
    println!("fold result: {}", value_1);

    println!("\n---------------------\n");

    // `len` ~~~~~~v
    let arr: [f64; 6] = [0., 1., 2., 3., 4., 5.];
    // `grouping` ~~~~~~~~~~~~v
    let wrap = Wrap::new(arr, 2);
    let value_2 = wrap.fold(0., |acc, arr| {
        println!(
            "len: {} | arr[0]: {}, arr[1]: {}",
            arr.len(),
            arr[0],
            arr[1]
        );
        assert_eq!(arr.len(), 2);
        let new_acc = acc + arr[0] * arr[1];
        println!("acc: {}, new_acc: {}", acc, new_acc);
        new_acc
    });
    println!("fold result: {}", value_2);
}

Which produces

len: 3 | arr[0]: 0, arr[1]: 1, arr[2]: 2
acc: 0, new_acc: 0
len: 3 | arr[0]: 3, arr[1]: 4, arr[2]: 5
acc: 0, new_acc: 60
fold result: 60

---------------------

len: 2 | arr[0]: 0, arr[1]: 1
acc: 0, new_acc: 0
len: 2 | arr[0]: 2, arr[1]: 3
acc: 0, new_acc: 6
len: 2 | arr[0]: 4, arr[1]: 5
acc: 6, new_acc: 26
fold result: 26

Full code available below. For now let's turn to how the fold function would be implemented. Say init and next are fold's two arguments (initial value and fold function respectively). Then the body of fold could look something like

#![allow(unused)]
fn main() {
        let mut acc = init;
        let mut i = 0;
        while i < len {
            let next_i = i + grouping;
            acc = next(acc, &arr[i..next_i]);
            i = next_i
        }
        acc
}

local variable acc is initially init, and the loop updates its value with the result of the call to next;
the while loop increments an i index until it goes over len (length of arr);
at the end of each iteration, the new value of i is i + grouping;
the call to next gives it the current value of the accumulator, and a slice from i to i + grouping ---remember that n..m is the interval [n, m[: m is not included in the interval;
when we exit the loop, we return the final value of acc.

Full code for this example, requires some Rust knowledge.

#![allow(non_upper_case_globals)]

pub struct Wrap<T, const len: usize> {
    arr: [T; len],
    grouping: usize,
}
impl<T, const len: usize> Wrap<T, len> {
    /// Constructor.
    pub fn new(arr: [T; len], grouping: usize) -> Self {
        if len % grouping != 0 {
            panic!(
                "grouping value {} is not a multiple of array length ({})",
                grouping, len,
            );
        }
        if grouping < 1 {
            panic!("illegal grouping value {}, must be > 0", grouping)
        }
        Self { arr, grouping }
    }
    /// Grouped fold.
    pub fn fold<Acc>(&self, init: Acc, mut next: impl FnMut(Acc, &[T]) -> Acc) -> Acc {
        let (arr, grouping) = (&self.arr, self.grouping);
        let mut acc = init;
        let mut i = 0;
        while i < len {
            let next_i = i + grouping;
            acc = next(acc, &arr[i..next_i]);
            i = next_i
        }
        acc
    }
}

fn main() {
    // `len` ~~~~~~v
    let arr: [f64; 6] = [0., 1., 2., 3., 4., 5.];
    // `grouping` ~~~~~~~~~~~~v
    let wrap = Wrap::new(arr, 3);
    let value_1 = wrap.fold(0., |acc, arr| {
        println!(
            "len: {} | arr[0]: {}, arr[1]: {}, arr[2]: {}",
            arr.len(),
            arr[0],
            arr[1],
            arr[2]
        );
        assert_eq!(arr.len(), 3);
        let new_acc = acc + arr[0] * arr[1] * arr[2];
        println!("acc: {}, new_acc: {}", acc, new_acc);
        new_acc
    });
    println!("fold result: {}", value_1);

    println!("\n---------------------\n");

    // `len` ~~~~~~v
    let arr: [f64; 6] = [0., 1., 2., 3., 4., 5.];
    // `grouping` ~~~~~~~~~~~~v
    let wrap = Wrap::new(arr, 2);
    let value_2 = wrap.fold(0., |acc, arr| {
        println!(
            "len: {} | arr[0]: {}, arr[1]: {}",
            arr.len(),
            arr[0],
            arr[1]
        );
        assert_eq!(arr.len(), 2);
        let new_acc = acc + arr[0] * arr[1];
        println!("acc: {}, new_acc: {}", acc, new_acc);
        new_acc
    });
    println!("fold result: {}", value_2);
}

Now let's think about this a little bit. The value &arr[i..next_i], where next_i is i + grouping, does not always make sense: i + grouping might strictly superior to len (arr's length). This cannot happen if len is a multiple of grouping however, and actually Wrap's constructor checks for this.

#![allow(unused)]
fn main() {
    /// Constructor.
    pub fn new(arr: [T; len], grouping: usize) -> Self {
        if len % grouping != 0 {
            panic!(
                "grouping value {} is not a multiple of array length ({})",
                grouping, len,
            );
        }
        if grouping < 1 {
            panic!("illegal grouping value {}, must be > 0", grouping)
        }
}

There is also a check that grouping > 0, otherwise fold would not terminate when len > 0. So everything should be fine, right? Humans do not make very good proof engines, let's just prove it to make sure.

Encoding

You are encouraged to think about how you would encode this verification problem so that mikino can handle it. You will probably not going to succeed unless you are already very familiar with this kind of encoding. May read a paragraph below or two, think about it some more, read some more, etc.

Mikino does not accept Rust code, we need to encode what we want to check. Writing an encoder for (a subset of) of programming language is a very challenging task. It requires an exact understanding of the semantics of the language and the ability to design encoding rules that are guaranteed to preserve it, or at least preserve the part relevant for the analysis. So let's not do that and encode it by hand.

#![allow(unused)]
fn main() {
        let mut acc = init;
        let mut i = 0;
        while i < len {
            let next_i = i + grouping;
            acc = next(acc, &arr[i..next_i]);
            i = next_i
        }
        acc
}

What do we want to check, i.e. what does it mean for this code to make sense? It's really a matter of how i is related to len. Each iteration makes sense if the interval we use on arr is legal, meaning i < len and next_i = i + grouping ≤ len (interval is exclusive on its upper bound). We actually don't care about what's in arr, just that its length is len. Our encoding can safely ignore arr completely. Same for acc, its value is not relevant for fold to make sense in how it accesses arr. The only real state variable of interest in this loop is thus i.

There a whole bunch of additional properties we might want to prove. For instance, that arr slices do not overlap. The point is that, whatever we are interested in proving, we should remove everything that is not necessary as we encode the program. However, the encoding should at least be sound: proving an invariant in the encoding must entail it is an invariant for the original program.

Here, we are doing the encoding by hand and we can pick and choose what is encoded or left out. In an actual verification tool, the encoding process would be automatic. Such an automatic encoder might encode the whole semantics of the program (meaning dealing with arrays at SMT-level here) and hope for the best, or be clever enough to realize it can excise array-related things for this particular verification challenge. Writing a clever, automatic encoder is difficult and challenging, and can void all results if it is not sound.

Note that we have a few constants here: len and grouping do not change as the loop runs. Unfortunately mikino does not have a notion of constant yet (contributions are welcome), so we have to encode them as state variables along with i.

#![allow(unused)]
fn main() {
svars {
	len grouping: int,
	i: int,
	done: bool,
}
}

The surprise state variable done is a flag we are going to use to indicate whether the loop is done or not. This allows our system to never end, which is a useful property for technical reasons beyond the scope of this chapter.

We initialize the transition system encoding fold's loop, as follows.

#![allow(unused)]
fn main() {
init {
    len ≥ 0,
	grouping ≥ 1,
	i = 0,
	done = ¬(i < len),
	len % grouping = 0,
}
}

The first two simply constrain the values for len (usize, thus ≥ 0) and grouping (checked to be ≥ 1 by the constructor). Then i is constrained to be equal to its initial value, 0. The done flag is initially true if and only if i ≥ len, which basically means len is 0 ---arr is empty, the loop never starts.

Last, we have the assumption we need for the whole thing to work: len is a multiple of grouping, which Wrap's constructor checks.

The transition relation needs to do a few things. Our constants (encoded as state variables) need to keep their value, since if we left them unconstrained they could take any value. We also need to update the value of done, and finally that of i.

#![allow(unused)]
fn main() {
// Encodes iteration `(pre i)`, NOT iteration `i`. That is, `trans` encodes the
// iteration where we access `arr` with the interval `(pre i)..((pre i) + grouping)`.
trans {
	'grouping = grouping,
	'len = len,
	// NEW value of the `done` flag, if `true` there will be no further iteration.
    'done = ¬('i < 'len),
	if done {
		// just maintain the value;
		'i = i
	} else {
		// otherwise, `i` is incremented by `grouping`.
		'i = i + grouping
	},
}
}

Testing the Encoding

Before we do anything else, let's think of what happens if len = 8 and grouping = 4. Initially i = 0, then it should increase to i = 4, then to i = 8 at which point done = i ≥ len becomes true and the system stutters (its state variables stay the same forever).

We should make sure our encoding behaves like this. So, what we should ask mikino is "with len = 8 and grouping = 4, is it possible to reach a state such that i = len?". We can do this with BMC: since we want to reach len = 8 ∧ grouping = 4 ∧ i = len, we can just need ask BMC to try to falsify ¬(len = 8 ∧ grouping = 4 ∧ i = len).

#![allow(unused)]
fn main() {
candidates {
	"candidate": ¬(len = 8 ⋀ grouping = 4 ⋀ i = len),
}
}

Mikino yields

> mikino bmc test.mkn
running BMC, looking for falsifications for 1 candidate(s)...
checking for falsifications at depth 0
checking for falsifications at depth 1
checking for falsifications at depth 2
found a falsification at depth 2:
- `candidate` = (not (and (= len 8) (= grouping 4) (= i len)))
  |=| Step 0
  |     done = false
  | grouping = 4
  |        i = 0
  |      len = 8
  |=| Step 1
  |     done = false
  | grouping = 4
  |        i = 4
  |      len = 8
  |=| Step 2
  |     done = true
  | grouping = 4
  |        i = 8
  |      len = 8
  |=| Z3 produced the following unexpected values
  | div0 ((x!0 int) (x!1 int)) int = 2
  | mod0 ((x!0 int) (x!1 int)) int = 0
  |=|

|===| Bmc result
| - found a falsification for the following candidate(s)
|   `candidate`
|
| - system is unsafe
|===|

We got exactly what we expected, that's encouraging. Also, remember that we proved that BMC produces counterexamples of minimal length. Hence, no shorter trace of states can lead the system to falsify our property.

Full code available in the Version 1 section. You are encouraged to mess around with the example to get a better understanding of the encoding.

Mikino reports that Z3 produced unexpected values. This is not relevant for our discussion, but these functions are part of the model. Z3 is letting us know how it decided to handle division (modulo) by 0. I won't go into deeper details here for space constraints, but this is a consequence of the fact that our system uses non-linear arithmetic, and non-linear division in particular. A (system made of) formula(s) uses non-linear arithmetic if it uses multiplication/division involving more than one variable (x * y, x / y). As opposed to linear arithmetic which only allows one variable to be used (3 * x, x / 7, 0 / x).

SMT is not decidable when non-linear arithmetic is involved, but we will have more to say on that shortly as we will run into this exact problem.

Diving Head First

We start with trying to prove that the lower bound of the interval i..(i + grouping) used on arr is legal, meaning to prove that i < len. More precisely, ¬done ⇒ i < len since on exit (when done is true) we actually should have i = len; let's prove done ⇒ i = len as well.

#![allow(unused)]
fn main() {
candidates {
	"not done then i < len": ¬done ⇒ i < len,
	"done then i = len": done ⇒ i = len,
}
}

Full code in the Version 2 section. Running mikino in check mode, we get:

> mikino check test.mkn
checking base case...
success: all candidate(s) hold in the base state

checking step case...
failed: the following candidate(s) are not inductive:
- `done then i = len` = (=> done (= i len))
  |=| Step k
  |     done = false
  | grouping = 2
  |        i = (- 1)
  |      len = 0
  |=| Step k + 1
  |     done = true
  | grouping = 2
  |        i = 1
  |      len = 0
  |=|

|===| Induction attempt result
| - all candidates hold in the initial state(s)
|
| - the following candidate(s) are not inductive (not preserved by the transition relation)
|   `done then i = len`
|
| - system might be unsafe, some candidate(s) are not inductive
|
| - the following candidate(s) hold in the initial state(s) and are inductive
|   and thus hold in all reachable states of the system:
|   `not done then i < len`
|===|

Well, the good news is that the lower bound of our interval is always legal: mikino proved it. We get a counterexample (cex) for the second candidate though. A stupid cex too, as i is obviously positive. At least, it is obviously positive if you take into account the initial states (i = 0), which the step check of the induction proof does not do by definition. As far as the transition relation is concerned, there is no reason for i to be positive at some step k.

Your first reflex might be to add this constraint to the transition relation ((pre i) ≥ 0), which is a terrible idea. That's the encoding of the original code, you should not touch it as this would actively mask cex-s. Spurious cex-s in this case, but if you make any mistake when augmenting trans then you might block actual cex-s and safety proofs you might get would not say anything about the original system.

The reason why, in this case, it would be safe to add (pre i) ≥ 0 (don't do it though) is that it is an invariant, i.e. a consequence of the system's behavior. So there's no reason to force it on trans, we can just ask mikino to prove it instead.

#![allow(unused)]
fn main() {
candidates {
	"i ≥ 0": i ≥ 0,
	"not done then i < len": ¬done ⇒ i < len,
	"done then i = len": done ⇒ i = len,
}
}

Full code in the Version 3 section. Mikino tells us

> mikino check test.mkn
checking base case...
success: all candidate(s) hold in the base state

checking step case...
failed: the following candidate(s) are not inductive:
- `done then i = len` = (=> done (= i len))
  |=| Step k
  |     done = false
  | grouping = 2
  |        i = 0
  |      len = 1
  |=| Step k + 1
  |     done = true
  | grouping = 2
  |        i = 2
  |      len = 1
  |=|
- `i ≥ 0` = (>= i 0)
  |=| Step k
  |     done = false
  | grouping = (- 1)
  |        i = 0
  |      len = 1
  |=| Step k + 1
  |     done = false
  | grouping = (- 1)
  |        i = (- 1)
  |      len = 1
  |=|

|===| Induction attempt result
| - all candidates hold in the initial state(s)
|
| - the following candidate(s) are not inductive (not preserved by the transition relation)
|   `done then i = len`
|   `i ≥ 0`
|
| - system might be unsafe, some candidate(s) are not inductive
|
| - the following candidate(s) hold in the initial state(s) and are inductive
|   and thus hold in all reachable states of the system:
|   `not done then i < len`
|===|

Okay, now grouping is negative. There is a pattern emerging: mikino (induction, really) is stupid and needs to be told everything.

Strengthening 💪

When we add i ≥ 0 as a candidate, we are strengthening candidate done ⇒ i = len. That is, this candidate is not inductive on the raw system (made of init and trans). If we hope to prove it by induction, we have to try to prove a stronger version (done ⇒ i = len) ∧ lemma, for example with lemma ≝ i ≥ 0 in the previous example. We added the lemma as a separate candidate, but morally lemma was not really what we wanted to prove, it was just a lemma we added to help prove the main candidate (which failed). It did not work, but if we can find a lemma for which the proof goes through, then we won since the fact that (done ⇒ i = len) ∧ lemma is an invariant implies that done ⇒ i = len is an invariant.

We are about to strengthen this candidate manually, but maybe you can see why many induction-based proof engine have some form of invariant discovery. Such techniques aim at discovering potentially complex lemmas about the system that strengthen the candidates when they are not inductive.

We could keep on asking mikino for step cex-s and come up with a candidate that will hopefully block them. But we have been doing this whole thing wrong.

The first thing we should do is write everything we expect to be an invariant. For instance we know that len ≥ 0, and that grouping ≥ 1 and len % grouping = 0 (both checked in the constructor). Our first move should have been to write these candidates down (in addition to i ≥ 0) and make sure they are actually (inductive) invariants. Besides hopefully strengthening our original candidates (done ⇒ i = len and ¬done ⇒ i < len), we must check that they are invariants since if they are not something is very wrong ---the system, our encoding, our overall understanding, or all of the above.

Note that, if the encoding process was automatic, these candidates could have been generated automatically: len: usize implies len ≥ 0, same for i, and the checks in the constructor guarantee grouping ≥ 1 and len % grouping = 0 since neither len nor grouping ever change. As we will see, this is not enough, and we will need to add another (candidate) invariant that is less trivial to strengthen our real candidate successfully.

For now let's just add these new candidates

#![allow(unused)]
fn main() {
candidates {
	"not done then i < len": ¬done ⇒ i < len,
	"done then i = len": done ⇒ i = len,

	"i ≥ 0": i ≥ 0,
	// new
	"len ≥ 0": len ≥ 0,
	"grouping > 0": grouping > 0,
	"len grouping related": len % grouping = 0,
}
}

and run mikino. Full code in the Version 4 section.

> mikino check test.mkn
checking base case...
success: all candidate(s) hold in the base state

checking step case...
failed: the following candidate(s) are not inductive:
- `done then i = len` = (=> done (= i len))
  |=| Step k
  |     done = false
  | grouping = 2
  |        i = 3
  |      len = 4
  |=| Step k + 1
  |     done = true
  | grouping = 2
  |        i = 5
  |      len = 4
  |=| Z3 produced the following unexpected values
  | div0 ((x!0 int) (x!1 int)) int = 2
  | mod0 ((x!0 int) (x!1 int)) int = 0
  |=|

|===| Induction attempt result
| - all candidates hold in the initial state(s)
|
| - the following candidate(s) are not inductive (not preserved by the transition relation)
|   `done then i = len`
|
| - system might be unsafe, some candidate(s) are not inductive
|
| - the following candidate(s) hold in the initial state(s) and are inductive
|   and thus hold in all reachable states of the system:
|   `grouping > 0`
|   `i ≥ 0`
|   `len grouping related`
|   `len ≥ 0`
|   `not done then i < len`
|===|

At least the new candidates are actual (inductive) invariants. It was not enough to strengthen our real candidate, but the cex we got is interesting. With len = 4 and grouping = 2, the step check is able to go from i = 3 to i = 5 and falsify the main candidate.

The problem here, as you might have guessed, is currently i can really take any value as long as its positive: no (candidate) invariant constrain it besides i ≥ 0. Looking at the code for the loop again

#![allow(unused)]
fn main() {
        let mut acc = init;
        let mut i = 0;
        while i < len {
            let next_i = i + grouping;
            acc = next(acc, &arr[i..next_i]);
            i = next_i
        }
        acc
}

we see that i can only be a multiple of grouping. But we cannot know until we try to prove it. Also, will it strengthen our main candidate enough to make it inductive?

#![allow(unused)]
fn main() {
candidates {
	"not done then i < len": ¬done ⇒ i < len,
	"done then i = len": done ⇒ i = len,

	"i ≥ 0": i ≥ 0,
	"len ≥ 0": len ≥ 0,
	"grouping > 0": grouping > 0,
	"len grouping related": len % grouping = 0,
	// new
    "i % grouping = 0": i % grouping = 0,
}
}

We run mikino but, inconspicuously, we change the command used to run Z3 slightly (change z3 in the string to whatever the path to your Z3 binary is). Full code in the Version 5 section.

> mikino --z3_cmd "z3 -T:5" check test.mkn
checking base case...
success: all candidate(s) hold in the base state

checking step case...
|===| Error
| smt-level error:
| - smt solver reported `timeout`
| - during step check
|===|

Adding -T:5 to the Z3 command tells Z3 to timeout after five seconds. Feel free to increase the timeout, unless you are from the future and using a version Z3 that performs better on non-linear arithmetic, the step check will never end. Because of...

Undecidability

This small aside illustrates the importance of delimiting precisely the logical fragment in which your encoding takes place. That is, what the formulas mention: strings, arrays, non-linear arithmetic?

Verification is expensive; very expensive. SMT checks themselves are at least exp-time, meaning that if n is "the size of the problem", the complexity of SMT checks is at least 2ⁿ. Most SMT-based verification techniques end up being at least k-exp-time, also informally called tower of exponential, which is even worse than it sounds:

2^(2^(2^(2^(.....2ⁿ))))
^^^^^^^^^^^^^^^^^^
    `k` times

where k is some arbitrarily large constant specific to a given problem.

So that's not great. As it turns out, the hardware is now so efficient and the tools so carefully implemented and optimized that despite being k-exp-time, we can actually verify very interesting and complex systems. Still, given the complexity, we can only go so far.

One way around this high complexity is to analyze complex systems compositionally, which is akin to type-checking. When proving function f, which calls g, we can abstract g away if we have some specification for it, effectively replacing g's implementation by what the specification says it does. Then we prove g respects its specification, recursively.

This assumes we have a specification for sub-functions (g), and not just a single specification at the top-most level (f). Refining a top-level specification to generate specifications for the sub-functions is very difficult to do automatically (also manually).

To sum up, verification has at best a very high complexity. Still, in theory, if you had enough time and memory you could just wait for an arbitrary long time and actually get an answer. Unless you are in an undecidable logic fragment: you cannot know in advance if you will get an answer, even if you wait for an infinite amount of time and memory.

That's not great either, and in fact this is (probably) what happened to us on

#![allow(unused)]
fn main() {
candidates {
	"not done then i < len": ¬done ⇒ i < len,
	"done then i = len": done ⇒ i = len,

	"i ≥ 0": i ≥ 0,
	"len ≥ 0": len ≥ 0,
	"grouping > 0": grouping > 0,
	"len grouping related": len % grouping = 0,
	// new
    "i % grouping = 0": i % grouping = 0,
}
}

when we got

> mikino --z3_cmd "z3 -T:5" check test.mkn
checking base case...
success: all candidate(s) hold in the base state

checking step case...
|===| Error
| smt-level error:
| - smt solver reported `timeout`
| - during step check
|===|

We have been in an undecidable fragment all along (since we use non-linear arithmetic). But so far, we managed to only send Z3 checks it could handle. The last candidate we added, i % grouping = 0, apparently made our checks escape Z3's abilities.

And that's pretty much it, we will not prove done ⇒ i = len and probably not other interesting properties such as "the upper bound of the interval i..(i + grouping) must be ≤ len (interval exclusive on the upper bound)" (or simply i + grouping ≤ len) either.

Or maybe what we could do is...

Settling For The Next Best Thing

Our current system is very loose on what len and grouping could be. We cannot say much on grouping as it is given to the code at runtime. It can be anything (module the constructor's checks) and we have no control over it at compile-time (verification-time). But len is different.

It is actually not unknown at compile-time since it is a const, i.e. a value that can be computed when compiling ---at least when compiling a binary using this code, but not necessarily when compiling a library. See section Rust System for the full Rust code of the system. More precisely, different version of our case-study might be used: with len = 3, len = 7... But the point is that, due to how Rust works (monomorphization in particular), there is a finite number of actual len values and we know all of them. (Again, at least when compiling a binary.)

So, maybe, instead the loose constraint len ≥ 0 and trying to conduct a proof for any value of len (which does not work, as we have seen), we could check each possible value of len separately. Notice that len is used in a non-linear mod application, len % grouping:

#![allow(unused)]
fn main() {
candidates {
	"not done then i < len": ¬done ⇒ i < len,
	"done then i = len": done ⇒ i = len,

	"i ≥ 0": i ≥ 0,
	"len ≥ 0": len ≥ 0,
	"grouping > 0": grouping > 0,
	"len grouping related": len % grouping = 0,
	// new
    "i % grouping = 0": i % grouping = 0,
}
}

Checking for the concrete possible values of len instead would remove this non-linear mod and, maybe, simplify our checks enough that Z3 can handle them. Let's try with len = 8; we could remove the len state variable altogether, but we can try simply forcing it to be 8. To do this, first we need to change init slightly:

#![allow(unused)]
fn main() {
init {
    len = 8, // new
	grouping ≥ 1,
	i = 0,
	done = ¬(i < len),
	len % grouping = 0,
}
}

Nothing to do on trans, it does not mention len anyway. The candidate len ≥ 0 changes to become more precise though:

#![allow(unused)]
fn main() {
candidates {
	"not done then i < len": ¬done ⇒ i < len,
	"done then i = len": done ⇒ i = len,

	"i ≥ 0": i ≥ 0,
	"len is 8": len = 8, // changed
	"grouping > 0": grouping > 0,
	"len grouping related": len % grouping = 0,
    "i % grouping = 0": i % grouping = 0,
}
}

While we still have the non-linear len % grouping, the (candidate) invariant len = 8 might actually be enough for Z3 to handle the checks on this system. We shall see.

Full code in the Version 6 section. Crossing our fingers, we nervously run mikino:

> mikino --z3_cmd "z3 -T:5" check test.mkn
checking base case...
success: all candidate(s) hold in the base state

checking step case...
success: all candidate(s) are inductive

|===| Induction attempt result
| - all candidates hold in the initial state(s)
|
| - all candidates are inductive (preserved by the transition relation)
|
| - system is safe, all reachable states verify the candidate(s)
|===|

🎊 🎉 👏 🎊

Wrapping Up

We proved the lower bound of the interval in &arr[i..(i + grouping)] is legal 🎉. But that's not enough for the program to be safe, since we have not proved that the upper bound is legal. That is, prove that i + grouping ≤ len (interval still exclusive on the upper bound 😔).

By now you might be familiar enough with induction's step checks to be able to anticipate whether this candidate is going to be inductive or not.

#![allow(unused)]
fn main() {
candidates {
	"not done then i < len": ¬done ⇒ i < len,
	"not done then i + grouping ≤ len": // new
		¬done ⇒ i + grouping ≤ len,
	"done then i = len": done ⇒ i = len,

	"i ≥ 0": i ≥ 0,
	"len is 8": len = 8, // changed
	"grouping > 0": grouping > 0,
	"len grouping related": len % grouping = 0,
    "i % grouping = 0": i % grouping = 0,
}
}

Full code in the Version 7 section.

🥁🥁🥁🥁🥁🥁

> mikino --z3_cmd "z3 -T:5" check test.mkn
checking base case...
success: all candidate(s) hold in the base state

checking step case...
success: all candidate(s) are inductive

|===| Induction attempt result
| - all candidates hold in the initial state(s)
|
| - all candidates are inductive (preserved by the transition relation)
|
| - system is safe, all reachable states verify the candidate(s)
|===|

🎉

It might be disappointing that we had to choose a value for the length, i.e. that we did not prove that fold's array accesses are legal when len is 8. Unfortunately, in its current state, Z3 cannot handle to have len as an unknown value because of the non-linear applications of modulo.

This means that, assuming we are verifying a binary, we can conduct the same proof for all len values actually used by the program. It would be much better to verify fold for any length, but this illustrates the kind of trade-offs that are often necessary in a verification process due to the very high complexity (and sometimes undecidability) of the checks intrinsic to the verification approach.

Full Code for All Examples

Rust System

Expand this for the full code.

#![allow(non_upper_case_globals)]

pub struct Wrap<T, const len: usize> {
    arr: [T; len],
    grouping: usize,
}
impl<T, const len: usize> Wrap<T, len> {
    /// Constructor.
    pub fn new(arr: [T; len], grouping: usize) -> Self {
        if len % grouping != 0 {
            panic!(
                "grouping value {} is not a multiple of array length ({})",
                grouping, len,
            );
        }
        if grouping < 1 {
            panic!("illegal grouping value {}, must be > 0", grouping)
        }
        Self { arr, grouping }
    }
    /// Grouped fold.
    pub fn fold<Acc>(&self, init: Acc, mut next: impl FnMut(Acc, &[T]) -> Acc) -> Acc {
        let (arr, grouping) = (&self.arr, self.grouping);
        let mut acc = init;
        let mut i = 0;
        while i < len {
            let next_i = i + grouping;
            acc = next(acc, &arr[i..next_i]);
            i = next_i
        }
        acc
    }
}

fn main() {
    // `len` ~~~~~~v
    let arr: [f64; 6] = [0., 1., 2., 3., 4., 5.];
    // `grouping` ~~~~~~~~~~~~v
    let wrap = Wrap::new(arr, 3);
    let value_1 = wrap.fold(0., |acc, arr| {
        println!(
            "len: {} | arr[0]: {}, arr[1]: {}, arr[2]: {}",
            arr.len(),
            arr[0],
            arr[1],
            arr[2]
        );
        assert_eq!(arr.len(), 3);
        let new_acc = acc + arr[0] * arr[1] * arr[2];
        println!("acc: {}, new_acc: {}", acc, new_acc);
        new_acc
    });
    println!("fold result: {}", value_1);

    println!("\n---------------------\n");

    // `len` ~~~~~~v
    let arr: [f64; 6] = [0., 1., 2., 3., 4., 5.];
    // `grouping` ~~~~~~~~~~~~v
    let wrap = Wrap::new(arr, 2);
    let value_2 = wrap.fold(0., |acc, arr| {
        println!(
            "len: {} | arr[0]: {}, arr[1]: {}",
            arr.len(),
            arr[0],
            arr[1]
        );
        assert_eq!(arr.len(), 2);
        let new_acc = acc + arr[0] * arr[1];
        println!("acc: {}, new_acc: {}", acc, new_acc);
        new_acc
    });
    println!("fold result: {}", value_2);
}

Output:

len: 3 | arr[0]: 0, arr[1]: 1, arr[2]: 2
acc: 0, new_acc: 0
len: 3 | arr[0]: 3, arr[1]: 4, arr[2]: 5
acc: 0, new_acc: 60
fold result: 60

---------------------

len: 2 | arr[0]: 0, arr[1]: 1
acc: 0, new_acc: 0
len: 2 | arr[0]: 2, arr[1]: 3
acc: 0, new_acc: 6
len: 2 | arr[0]: 4, arr[1]: 5
acc: 6, new_acc: 26
fold result: 26

Version 1

Expand this for the full code.

#![allow(unused)]
fn main() {
svars {
	len grouping: int,
	i: int,
	done: bool,
}

init {
    len ≥ 0,
	grouping ≥ 1,
	i = 0,
	done = ¬(i < len),
	len % grouping = 0,
}

// Encodes iteration `(pre i)`, NOT iteration `i`. That is, `trans` encodes the
// iteration where we access `arr` with the interval `(pre i)..((pre i) + grouping)`.
trans {
	'grouping = grouping,
	'len = len,
	// NEW value of the `done` flag, if `true` there will be no further iteration.
    'done = ¬('i < 'len),
	if done {
		// just maintain the value;
		'i = i
	} else {
		// otherwise, `i` is incremented by `grouping`.
		'i = i + grouping
	},
}

candidates {
	"candidate": ¬(len = 8 ⋀ grouping = 4 ⋀ i = len),
}
}

Output:

> mikino check test.mkn
running BMC, looking for falsifications for 1 candidate(s)...
checking for falsifications at depth 0
checking for falsifications at depth 1
checking for falsifications at depth 2
found a falsification at depth 2:
- `candidate` = (not (and (= len 8) (= grouping 4) (= i len)))
  |=| Step 0
  |     done = false
  | grouping = 4
  |        i = 0
  |      len = 8
  |=| Step 1
  |     done = false
  | grouping = 4
  |        i = 4
  |      len = 8
  |=| Step 2
  |     done = true
  | grouping = 4
  |        i = 8
  |      len = 8
  |=| Z3 produced the following unexpected values
  | div0 ((x!0 int) (x!1 int)) int = 2
  | mod0 ((x!0 int) (x!1 int)) int = 0
  |=|

|===| Bmc result
| - found a falsification for the following candidate(s)
|   `candidate`
|
| - system is unsafe
|===|

Version 2

Expand this for the full code.

#![allow(unused)]
fn main() {
svars {
	len grouping: int,
	i: int,
	done: bool,
}

init {
    len ≥ 0,
	grouping ≥ 1,
	i = 0,
	done = ¬(i < len),
	len % grouping = 0,
}

// Encodes iteration `(pre i)`, NOT iteration `i`. That is, `trans` encodes the
// iteration where we access `arr` with the interval `(pre i)..((pre i) + grouping)`.
trans {
	'grouping = grouping,
	'len = len,
	// NEW value of the `done` flag, if `true` there will be no further iteration.
    'done = ¬('i < 'len),
	if done {
		// just maintain the value;
		'i = i
	} else {
		// otherwise, `i` is incremented by `grouping`.
		'i = i + grouping
	},
}

candidates {
	"not done then i < len": ¬done ⇒ i < len,
	"done then i = len": done ⇒ i = len,
}
}

Output:

> mikino check test.mkn
checking base case...
success: all candidate(s) hold in the base state

checking step case...
failed: the following candidate(s) are not inductive:
- `done then i = len` = (=> done (= i len))
  |=| Step k
  |     done = false
  | grouping = 2
  |        i = (- 1)
  |      len = 0
  |=| Step k + 1
  |     done = true
  | grouping = 2
  |        i = 1
  |      len = 0
  |=|

|===| Induction attempt result
| - all candidates hold in the initial state(s)
|
| - the following candidate(s) are not inductive (not preserved by the transition relation)
|   `done then i = len`
|
| - system might be unsafe, some candidate(s) are not inductive
|
| - the following candidate(s) hold in the initial state(s) and are inductive
|   and thus hold in all reachable states of the system:
|   `not done then i < len`
|===|

Version 3

Expand this for the full code.

#![allow(unused)]
fn main() {
svars {
	len grouping: int,
	i: int,
	done: bool,
}

init {
    len ≥ 0,
	grouping ≥ 1,
	i = 0,
	done = ¬(i < len),
	len % grouping = 0,
}

// Encodes iteration `(pre i)`, NOT iteration `i`. That is, `trans` encodes the
// iteration where we access `arr` with the interval `(pre i)..((pre i) + grouping)`.
trans {
	'grouping = grouping,
	'len = len,
	// NEW value of the `done` flag, if `true` there will be no further iteration.
    'done = ¬('i < 'len),
	if done {
		// just maintain the value;
		'i = i
	} else {
		// otherwise, `i` is incremented by `grouping`.
		'i = i + grouping
	},
}

candidates {
	"i ≥ 0": i ≥ 0,
	"not done then i < len": ¬done ⇒ i < len,
	"done then i = len": done ⇒ i = len,
}
}

Output:

> mikino check test.mkn
checking base case...
success: all candidate(s) hold in the base state

checking step case...
failed: the following candidate(s) are not inductive:
- `done then i = len` = (=> done (= i len))
  |=| Step k
  |     done = false
  | grouping = 2
  |        i = 0
  |      len = 1
  |=| Step k + 1
  |     done = true
  | grouping = 2
  |        i = 2
  |      len = 1
  |=|
- `i ≥ 0` = (>= i 0)
  |=| Step k
  |     done = false
  | grouping = (- 1)
  |        i = 0
  |      len = 1
  |=| Step k + 1
  |     done = false
  | grouping = (- 1)
  |        i = (- 1)
  |      len = 1
  |=|

|===| Induction attempt result
| - all candidates hold in the initial state(s)
|
| - the following candidate(s) are not inductive (not preserved by the transition relation)
|   `done then i = len`
|   `i ≥ 0`
|
| - system might be unsafe, some candidate(s) are not inductive
|
| - the following candidate(s) hold in the initial state(s) and are inductive
|   and thus hold in all reachable states of the system:
|   `not done then i < len`
|===|

Version 4

Expand this for the full code.

#![allow(unused)]
fn main() {
svars {
	len grouping: int,
	i: int,
	done: bool,
}

init {
    len ≥ 0,
	grouping ≥ 1,
	i = 0,
	done = ¬(i < len),
	len % grouping = 0,
}

// Encodes iteration `(pre i)`, NOT iteration `i`. That is, `trans` encodes the
// iteration where we access `arr` with the interval `(pre i)..((pre i) + grouping)`.
trans {
	'grouping = grouping,
	'len = len,
	// NEW value of the `done` flag, if `true` there will be no further iteration.
    'done = ¬('i < 'len),
	if done {
		// just maintain the value;
		'i = i
	} else {
		// otherwise, `i` is incremented by `grouping`.
		'i = i + grouping
	},
}

candidates {
	"not done then i < len": ¬done ⇒ i < len,
	"done then i = len": done ⇒ i = len,

	"i ≥ 0": i ≥ 0,
	// new
	"len ≥ 0": len ≥ 0,
	"grouping > 0": grouping > 0,
	"len grouping related": len % grouping = 0,
}
}

Output:

> mikino check test.mkn
checking base case...
success: all candidate(s) hold in the base state

checking step case...
failed: the following candidate(s) are not inductive:
- `done then i = len` = (=> done (= i len))
  |=| Step k
  |     done = false
  | grouping = 2
  |        i = 3
  |      len = 4
  |=| Step k + 1
  |     done = true
  | grouping = 2
  |        i = 5
  |      len = 4
  |=| Z3 produced the following unexpected values
  | div0 ((x!0 int) (x!1 int)) int = 2
  | mod0 ((x!0 int) (x!1 int)) int = 0
  |=|

|===| Induction attempt result
| - all candidates hold in the initial state(s)
|
| - the following candidate(s) are not inductive (not preserved by the transition relation)
|   `done then i = len`
|
| - system might be unsafe, some candidate(s) are not inductive
|
| - the following candidate(s) hold in the initial state(s) and are inductive
|   and thus hold in all reachable states of the system:
|   `grouping > 0`
|   `i ≥ 0`
|   `len grouping related`
|   `len ≥ 0`
|   `not done then i < len`
|===|

Version 5

Expand this for the full code.

#![allow(unused)]
fn main() {
svars {
	len grouping: int,
	i: int,
	done: bool,
}

init {
    len ≥ 0,
	grouping ≥ 1,
	i = 0,
	done = ¬(i < len),
	len % grouping = 0,
}

// Encodes iteration `(pre i)`, NOT iteration `i`. That is, `trans` encodes the
// iteration where we access `arr` with the interval `(pre i)..((pre i) + grouping)`.
trans {
	'grouping = grouping,
	'len = len,
	// NEW value of the `done` flag, if `true` there will be no further iteration.
    'done = ¬('i < 'len),
	if done {
		// just maintain the value;
		'i = i
	} else {
		// otherwise, `i` is incremented by `grouping`.
		'i = i + grouping
	},
}

candidates {
	"not done then i < len": ¬done ⇒ i < len,
	"done then i = len": done ⇒ i = len,

	"i ≥ 0": i ≥ 0,
	"len ≥ 0": len ≥ 0,
	"grouping > 0": grouping > 0,
	"len grouping related": len % grouping = 0,
	// new
    "i % grouping = 0": i % grouping = 0,
}
}

Output:

> mikino --z3_cmd "z3 -T:5" check test.mkn
checking base case...
success: all candidate(s) hold in the base state

checking step case...
|===| Error
| smt-level error:
| - smt solver reported `timeout`
| - during step check
|===|

Version 6

Expand this for the full code.

#![allow(unused)]
fn main() {
svars {
	len grouping: int,
	i: int,
	done: bool,
}

init {
    len = 8, // new
	grouping ≥ 1,
	i = 0,
	done = ¬(i < len),
	len % grouping = 0,
}

// Encodes iteration `(pre i)`, NOT iteration `i`. That is, `trans` encodes the
// iteration where we access `arr` with the interval `(pre i)..((pre i) + grouping)`.
trans {
	'grouping = grouping,
	'len = len,
	// NEW value of the `done` flag, if `true` there will be no further iteration.
    'done = ¬('i < 'len),
	if done {
		// just maintain the value;
		'i = i
	} else {
		// otherwise, `i` is incremented by `grouping`.
		'i = i + grouping
	},
}

candidates {
	"not done then i < len": ¬done ⇒ i < len,
	"done then i = len": done ⇒ i = len,

	"i ≥ 0": i ≥ 0,
	"len is 8": len = 8, // changed
	"grouping > 0": grouping > 0,
	"len grouping related": len % grouping = 0,
    "i % grouping = 0": i % grouping = 0,
}
}

Output:

> mikino check test.mkn
checking base case...
success: all candidate(s) hold in the base state

checking step case...
success: all candidate(s) are inductive

|===| Induction attempt result
| - all candidates hold in the initial state(s)
|
| - all candidates are inductive (preserved by the transition relation)
|
| - system is safe, all reachable states verify the candidate(s)
|===|

Version 7

Expand this for the full code.

#![allow(unused)]
fn main() {
svars {
	len grouping: int,
	i: int,
	done: bool,
}

init {
    len = 8, // new
	grouping ≥ 1,
	i = 0,
	done = ¬(i < len),
	len % grouping = 0,
}

// Encodes iteration `(pre i)`, NOT iteration `i`. That is, `trans` encodes the
// iteration where we access `arr` with the interval `(pre i)..((pre i) + grouping)`.
trans {
	'grouping = grouping,
	'len = len,
	// NEW value of the `done` flag, if `true` there will be no further iteration.
    'done = ¬('i < 'len),
	if done {
		// just maintain the value;
		'i = i
	} else {
		// otherwise, `i` is incremented by `grouping`.
		'i = i + grouping
	},
}

candidates {
	"not done then i < len": ¬done ⇒ i < len,
	"not done then i + grouping ≤ len": // new
		¬done ⇒ i + grouping ≤ len,
	"done then i = len": done ⇒ i = len,

	"i ≥ 0": i ≥ 0,
	"len is 8": len = 8, // changed
	"grouping > 0": grouping > 0,
	"len grouping related": len % grouping = 0,
    "i % grouping = 0": i % grouping = 0,
}
}

Output:

> mikino check test.mkn
checking base case...
success: all candidate(s) hold in the base state

checking step case...
success: all candidate(s) are inductive

|===| Induction attempt result
| - all candidates hold in the initial state(s)
|
| - all candidates are inductive (preserved by the transition relation)
|
| - system is safe, all reachable states verify the candidate(s)
|===|

Conclusion

If you have understood (most of) what we have discussed, congratulations 🎉. I hope some readers might be encouraged to develop cool verification tools, while others got enough of an understanding on the topic of verification to have a more expert usage of verification tools, if (and most likely when) they start using such tools as developers.

Transition systems are not the only way to encode program verification problems. Constrained Horn Clauses (CHC-s) are very popular at the time of writing, and for good reasons. Basically, CHC-s represent a program (or program-like structure) in a more fragmented way than transition systems. Techniques based on a CHC representation tend to have a fine-grain vision of the notion of transition, which allows for more precision (efficiency) in the verification approach built on top of it.

Besides pure induction, there are many other techniques that are worth looking into. A pretty important one is Property Directed Reachability (PDR), also known as Incremental Construction of Inductive Clauses for Indubitable Correctness (IC3). Unfortunately, PDR/IC3 is mostly discussed in academic papers and I could not find a presentation understandable without a serious background in formal logics. This is partially due to the fact that PDR is still quite recent, but also to its complex and intricate nature. Here are a few links though, all of them are PDF:

It should be noted that PDR is particularly interesting in the purely propositional case. That is, for systems that can be expressed using nothing but booleans. Systems using arithmetic, arrays, strings... are more difficult to handle because of one of the necessary PDR steps (pre-image computation), as well as certain crucial optimization that only apply on purely propositional formulas.

Appendix: Mikino

Mikino is written in Rust and is available as a Rust library

https://crates.io/crates/mikino_api
https://docs.rs/mikino_api/0.9.1/mikino_api

and a Rust birany

https://crates.io/crates/mikino

So, if you already have Rust installed on your system (or don't mind installing it) just make sure it is up-to-date and ask cargo to install mikino for you.

# update rust
> rustup self update
> rustup update

# install mikino, `-f` allows overwriting (updating)
# the previous mikino install if any
> cargo install -f mikino

Otherwise, head to mikino's release page and download the latest release for your operating system. The only other alternative is to build mikino from scratch.

Z3

Mikino requires the Z3 SMT solver. You can build it from source or recover a binary from the release page.

From this point forward I assume readers have a Z3 binary called z3 in their path. That is, running the command z3 -version should not fail and produce an output similar to

Z3 version 4.8.13 - 64 bit

Mikino, by default, assumes a Z3 binary is in your PATH with name z3. You can override this with the --z3_cmd command-line argument: mikino --z3_cmd "my_z3" ..., or mikino --z3_cmd "path/to/my_z3" ... if Z3 is not in your PATH.

Note that other efficient solvers exist such as Alt-Ergo, CVC4 and Yices 2. Solvers tend to be perform well on different kinds of problem, and verification frameworks routinely run several of them in parallel, wait for the quickest answer, and discard solver instances that are still running.

Build

You can also build mikino, it's actually quite easy. Install Rust or make sure it is up-to-date if it is installed already.

# update rust
> rustup self update
> rustup update

Clone mikino's (binary) repo, and cargo build it:

> clone https://github.com/OCamlPro/mikino_bin
> cd mikino_bin

# debug, unoptimized build
> cargo build
> ./target/debug/mikino -V
mikino 0.9.1

# release, optimized build
> cargo build --release
> ./target/release/mikino -V
mikino 0.9.1

Alternatively, you can ask cargo to install your local clone of the repo:

> clone https://github.com/OCamlPro/mikino_bin
> cargo install --path mikino_bin
> mikino -V
mikino 0.9.1

Verification For Dummies: SMT and Induction by OCamlPro