See last lecture's notes for the start of the SMT unit.

## Continuing example

Continuing our example of an application from last time, consider this program in C, which tries to check the bounds of two variables and their sum:

#define MAX 16
void check_bounds(int a, int b) {
  if (a < MAX) {
    if (b < MAX) {
       if (a + b > 2*MAX) {
          printf("Error!\n");
          exit(1);
       } 
    }
  } 
}

:::success
Does this program ever crash with an error? If so, say when.
:::

<details>
<summary>Think, then click! </summary>
<br>

Yes, this could hit the error!

C's `int` type uses a two's complement signed representation. If both `a` and `b` are negative numbers, their sum can overflow to a position number that's greater than 32.
</details>
<br>

We can use an SMT solver to find a specific instance of this bug for us.

# The Z3 solver

The most popular SMT solver is one put out by Microsoft, called the [Z3 solver](https://microsoft.github.io/z3guide/docs/logic/intro/). Note that SMT solvers are also often "theorem provers"; more on this later. z3 won [an award in 2015](https://www.microsoft.com/en-us/research/blog/z3-wins-2015-acm-sigplan-award/) for "developing a software system that has had a lasting influence, reflected in contributions to concepts, in commercial acceptance, or both".

z3 can be used as a library within Python (and Rust, but we'll stick to Python for today).

To follow along in class, install z3 with:

pip3 install z3-solver

And update to the latest with:

pip install z3-solver --upgrade

You can then use Z3 within a Python file:

from z3 import * 

x = Int('x')
y = Int('y')
solve(x > 2, y < 10, x + 2*y == 7)

# Continuing example: bitvector bounds

We can model our previous example in Z3 by using the theory of bitvectors.

First, we can model this directly in the `SMT-LIB` format. This is a low-level format (you can think of it almost like an assembly code for verification and modeling tools). It uses a syntax with lots of parenthesis, like many functional programming languages (e.g., Lisp). We'll only briefly show this low-level `SMT-LIB` format; after this, we'll instead work with SMT via libraries in Python or Rust.

;; Create two new variables, that are 32-bit integers
(declare-const a (_ BitVec 32))
(declare-const b (_ BitVec 32))

;; Model if-statement 1:
;; Add a constraint that a < 16 (in hex)
;; "bvslt" is for "bitvector signed less than"
(assert (bvslt a #x00000010))

;; Model if-statement 2
;; Add a constraint that b < 16 (in hex)
(assert (bvslt b #x00000010))

;; Model if-statement 3:
;; Add a constraint that the sum of a+b < 32 (in hex)
(assert (bvsgt (bvadd a b) #x00000020))

;; Check if our model has any satisfying instances
(check-sat)

;; Print one such instance (see the note on terminology below)
(get-model)

If we save this file as `ex.smt`, we can run this as:

z3 ex.smt

Note, you may need to install `z3` as a separate utility (e.g., `brew install z3`) to run on this file; however, this is not necessary for the assignments in this class where we will use z3 as a library in Python or Rust.

:::info
*Terminology note:* In Alloy, we used the word model to describe the definitions and constraints you use to model a system. This is generally what the software-engineering community means by the word. The logic community, on the other hand, uses model to mean the same thing that we call an *instance* in Alloy or "assignment" in SAT latest homework: the assignment of values to variables that either satisfies or does not satisfy a set of constraints. Z3's "get model" uses the word "model" like a logician, not a software engineer, and it means the concrete assignment.
:::

# Python's z3 library

To make it easier to use z3 without writing code in the low-level format, the remaining examples will use Python's library for z3.

We can model our example now as this:

from z3 import *

# Create a new solver to add constraints to
s = Solver()

# Declare the 32-bit variables
a = BitVec('a', 32)
b = BitVec('b', 32)

# Add constraints. This type, the "<" operator is overloaded to also work for 
# bitvectors, without needing to use the special named version. It means the
# same thing; the library handles the conversion based on the declared types.
s.add(a < 0x00000010)
s.add(b < 0x00000010)
s.add(a + b > 0x00000020)
s.add(a == 0xffffffff)

# Similar to a check/run in Alloy
print(s.check())

# Similar to pressing the "see instance" button in Alloy
print(s.model())

# To print the value of b in hex
print(hex(int(str(s.model().evaluate(b)))))

# Different numeric types

z3 solvers use several different types to represent numbers. Let's go over a different between integers (mathematical, unbounded ones) and reals.

We'll do so with a question: is there an `x` such that `x` squared is in between 4 and 9?

For integers, we expect no! Let's see this in SMT:

# Goal: find an x where x^2 falls in between two square numbers, e.g,
# x^2 greater than 4 but less than 9
def demo_ints():
    s = Solver()
    x = Int('x')

    # Note: power doesn't work in this library, use *
    s.add(x*x > 4)
    s.add(x*x < 9)

    result = s.check() # returns either SAT or UNSAT

    # We can only print the instance if the result is SAT
    if result == sat:
        print(s.model())
    else: 
        print(result)

    # Integers: we expect no answer, get UNSAT result

When we run this, we get `unsat`, as we expected, since no such integer exists.

What if we change the example to use `Real` instead of `Int`?

def demo_reals():
    s = Solver()
    
    # Now: Real, not Int
    x = Real('x')
    s.add(x*x > 4)
    s.add(x*x < 9)

    result = s.check() 
    if result == sat:
        print(s.model())
    else: 
        print(result)
    # Now, we expect a result!

When we run this new version, we get:

[x = 5/2]

When we allow non-whole numbers, an `x` that meets these constraints does exist! Many such `x` values exist, we may get a different one if we run z3 multiple times or on multiple different computers.

:::info
What's the different between `BitVec` and `Int`?
:::

We can use z3 to show us the difference.

Consider these constraints: is there an `x` such that `x + 1 > x`?

If we use the `Int` type:

def bitvector_diff():
    s = Solver()
    x = Int('x')

    s.add((x + 1) < x)

    result = s.check() 
    if result == sat:
        print(s.model())
    else: 
        print(result)

We get unsat: there is no such `x`, as we expect.

But if we use the bitvector `BitVec` type:

def bitvector_diff():
    s = Solver()
    x = BitVec('x', 4)

    s.add((x + 1) < x)

    result = s.check()
    if result == sat:
        print(s.model())
    else: 
        print(result)

We get SAT! `[x = 7]`. 7 in 4 bits is `0111`. When we add 1, we get `1111`, which is `-1`!

In short: bitvectors model overflow, like actual machine integers that have a fixed number of bits.

Engineers using z3 have to decide: do they want their model to actually find overflow bugs? Then they should use the theory of bitvectors. Otherwise (or if they need other mathematical integer properties), they should use the theory of integers.

# Showing equivalence with SMT

A frequent modeling task is to show the equivalence of two representations. For example: are two hardware circuit designs equivalent? Does the unoptimized and optimized version of an algorithm produce the same result?

The most direct way to format an equivalence question as a human would be this:
:::info
For all inputs, are form $A$ and form $B$ equivalent?
:::

*For all* is a quantifier, like `all` in Alloy. Specifically, "for all" is a universal quantifier, while "there exists" is an existential quantifier.

It turns out that it's often easier for modeling systems to reason about existential quantifiers than universal ones: the solver just needs to find *one* instance to answer the question.

:::success
How can we formulate the equivalence question using "there exists" instead of "for all"?
:::

<details>
<summary>Think, then click! </summary>
<br>

As we saw earlier in CS340, we can convert this by thinking about what it means for a counterexample to exist.

In general, the statement "for all $x$, $P(x)$" where $P$ is some property asks if something is true for all $x$. For example, "for all Wellesley students, the student is in Workday."

We can instead formulate this question by asking if a counterexample exists (if a counterexample exists, the original statement is false; if a counterexample does not exist, then the original statement is true). "for all $x$, $P(x)$" = "Not (exists $y$, not $P(y)$)".
</details>
<br>

In terms of our equivalence question and SMT solvers, we can see if $A$ and $B$ are equivalent by asking: is there some world for which $A$ and $B$ are *not* equal? If the counterexample exists (the SMT solver returns SAT), then equivalence is **false**. If no counterexample exists (the SMT solver returns UNSAT), then equivalence is **true** (the outcome we usually want). More on this next time!

## Example: implies definition

We saw earlier in CS340 that logical `implies` can be expressed with `not` and `or`. Let's use z3 to show these two forms are equivalent:

# Example: the definition of "P IMPLIES Q"
# represent with "AND, OR, NOT"
        
def demo_implies_equiv():
    s = Solver()
    p = Bool('p')
    q = Bool('q')

    # For all p, q, does "p => q" mean the same as "(not p) or q"
    # Ask the same question: answer is answerable SAT/UNSAT 
    s.add(Not(Implies(p, q) == Or(Not(p), q)))
    print(s.check())
    # print(s.model())
    # UNSAT => no counterexample => equivalent (good)
    # SAT => FOUND counterexample => NOT equivalent (bad!!!!)

# Example: mixing quantifiers

In some cases, we need to combine (implicit) "there exists" quantifiers with explicit "for all" quantifiers.

Consider factoring integer polynomials:

def demo_int_factoring():
   # (x + ROOT1)(x + ROOT2) = x^2 - 4

    s = Solver()

    x = Int('x') # Use int because we just are doing math, not worrying about overflow
    r1 = Int('r1')
    r2 = Int('r2')

    rhs = (x*x) - 4
    lhs = (x + r1) * (x + r2)

    # If we try this, it works for *some* x, not *all* x
    # s.add(rhs == lhs)

    # print(s.check())
    # print(s.model())

    # What we want to say here: *there exists* some r1 and r2 such that *for all* x, 
    # (x - r1)(x + r2) = x^2 - 4 

    # For this mix of "there exists" and "for all", it's useful to have an explicit quantifier
    # in the SMT code itself

    # ForAll is an actual operator we can use in SMT

    s.add(ForAll(x, lhs == rhs))
    print(s.check())
    print(s.model())

We can repeat this with real numbers to find solutions in more cases (or no solutions in some cases):

def demo_real_factoring():
    s = Solver()

    x = Real('x') # Use real to not restrict to whole numbers
    r1 = Real('r1')
    r2 = Real('r2')

    lhs = (x + r1) * (x + r2)

    #  Find = x^2 - 198x - 39484

    rhs = (x*x) - 198*x - 39484

    s.add(ForAll(x, lhs == rhs))
    print(s.check())
    print(s.model())

#  demo_real_factoring()

def demo_real_factoring_unsat():
   # (x + ROOT1)(x + ROOT2) = x^2 - 4

    s = Solver()

    x = Real('x') # Use real to not restrict to whole numbers
    r1 = Real('r1')
    r2 = Real('r2')

    lhs = (x + r1) * (x + r2)

    #  Find = x^2 -2x + 5 | (b^2 - 4ac) 
    rhs = (x*x) - 2*x +5

    s.add(ForAll(x, lhs == rhs))
    print(s.check())
    # print(s.model())

demo_real_factoring_unsat()

# More on bounds

A Key Difference

Most SMT solvers don't have "bounds" in the same way Alloy does. You can declare a datatype that's bounded in size, but the addition of domains like mathematical integers or lists means that unless you're working in a very restricted space, the set of possible objects is infinite.

What does it mean to say "For all x of type A, P(x)is true?" In Alloy,
"all" has an upper bound, and so the quantifier can always be converted to a big, but finite, "and" constraint. But suppose the type is actual mathematical integers? There are infinitely many integers, which means the solver can't convert the quantifier to a (finite) boolean constraint.

SMT solvers, however, can use theory-specific reasoning to solve even problems on infinite domains!

## More on SMT solver internals

As we discussed earlier, SMT solvers involve coordination between a boolean SAT solver and theory-specifc solvers.

Let's walk through some examples of how this works[^1].

IF I have `x` and `y` in the theory of integers and I write `x > 3 or y > 5`, the SMT solver will convert this to a *boolean skeleton*, separating out the purely boolean operators, like `or`, and replacing all the theory terms with boolean variables. In this example, that might be `T1` or `T2`, where `T1` means `x > 3` and `T2` means `y > 5`. The SMT solver can now find an assignment to that boolean skeleton with a normal, boolean SAT-solver.

Suppose the solver finds `T1=True, T2=True`. Then, it can pass to the theory solver the following constraints:

x > 3
y > 5

If, instead, the solver found `T1=False, T2=True`, the theory solver would get the following:

x <= 3
y > 5

We can then solve each of these with a system of linear inequalities solver (think Wolfram Alpha).

We can think of a very basic SMT solver as following these 3 steps:

(1) make a boolean skeleton
(2) get an instance that satisfies the boolean skeleton
(3) ask the theory solver to solve the resulting system with its domain-specific knowledge
(3) if the result of (3) is unsat, or another solution is desired, restart from (2).

Modern SMT solvers have more integration between the boolean and theory solvers, but that's outside the scope of this course.

# Another Example Theory-Solver: Uninterpreted Functions With Equality

Consider these constraints:

! ( f(f(f(a))) != a or f(a) = a ) 
f(f(f(f(f(a))))) = a or f(f(a)) != f(f(f(f(a))))

:::success
Are these constraints satisfiable? Does there exist some value of `a` and`f` such that these constraints are satisfied?
:::

As before, we'll convert these to a boolean skeleton.

:::success
How many boolean variables should we have?
:::

Answer: 4, separated out like so:

!(T1 or T2)
T3 or T4

That is,
- `f(f(f(a))) != a` becomes `T1`
- `f(a) = a` becomes `T2`
- `f(f(f(f(f(a))))) = a` becomes `T3`
- `f(f(a)) != f(f(f(f(a))))` becomes `T4`

### An Unproductive Assignment

This boolean skeleton:

!(T1 or T2)
T3 or T4

Is satisfied by the assignment `T1=False, T2=False, T3=True, T4=False`. We then get a theory problem out. We'll use e.g. `f3(a)` to represent `f(f(f(a)))`. The theory solver then gets the following constraints:

f3(a) = a
f(a) != a
f5(a) = a
f2(a) = f4(a)

We'll solve this using the theory of uninterpreted functions.

One algorithm uses by the theory of uninterpreted functions is called *congruence closure*. The ideas behind congruence closure are used to build a data structure called "equality graphs" that has become popular both within SMT solvers, and in programming languages/formal methods research in general.

:::info
The guest speaker we have on April 24 will present work building on equalty-graphs, or e-graphs!
:::

We'll sketch out congruence closure by example. First, make a graph data structure where each term is a node:

[^1]: Examples and sketches from Tim Nelson's https://hackmd.io/@lfs/rynK3wZMh


Then, make (undirected) edges between the terms that our equality constraints say must be equal.Since `f3(a) = a`, we'd draw an edge between those nodes. And similarly between `f5(a) = a`:

But, we know that equality is transitive! So we have have also learned that `f5(a)` and `f3(a)` are equivalent.

We can now use properties of functions to build even more equalities. Since we know `f3(a)` is the same as `a`, we can substitute `a` for `f(f(f(a)))` inside `f(f(f(f(f(a)))))`, giving us that `f(f(a))` (which we're calling `f2(a)`) is equivalent to `a` as well, since `f5(a) = a`. And since equality is transitive, `f2(a)` equals all the other things that equal `a`:


And because `f2(a) = a`, we can substitute `a` for `f(f(a))` within `f(f(f(a)))`, to get `f(a) = a`.

:::danger
But this contradicts the second negative equality constraint `f(a) != a`! So we've found a contradiction. That means this particular assignment for the boolean skeleton is `UNSAT`.
:::


### A Productive Assignment

Another way of solving the boolean skeleton is with the assignment `T1=False, T2=False, T3=False, T4=True`, which gives us the theory problem:

f3(a) = a
f(a) != a
f5(a) != a
f2(a) != f4(a)

We'd proceed similarly, but this time, we'd fine there is a `SAT` solution. The solver can then just pick some concrete value: for example, that `f(i) = 0` for all `i`.