Add enum sum types and a match expression
to teach structural induction over data and Z3’s datatype theory.
A sample program would be:
enum Option<T> { None, Some(T) }
fn get_or(a: Option<Int>, d: Int) -> Int
ensures result == d or result != d
{
match a {
None => d,
Some(v) => v,
}
}
Frml currently proves things about numbers and arrays
but never about the shape of a value.
Lists, options, and trees are where induction over data structures becomes real,
and the classic proofs
(list length, append associativity, map distributes over append)
are exactly what separates “checked the arithmetic” from “verified a data structure”.
Z3 has a native datatype sort,
so this is more a type-checker and visitor addition than new solver machinery.
It would sit as a datatype level above contracts,
and recursive types would reuse the existing decreases machinery.
Explicit Frame Clauses (modifies / reads)
Frml already infers written_params,
but the language gives the programmer no way to state what a call may touch.
An explicit, checked clause makes that contract visible:
This would teach the frame problem, modular verification, and information hiding.
The pedagogical payoff is the frame problem:
proving that a call does not change everything else.
A student who writes modifies a and then has the verifier flag an unlisted write
learns why modularity fails without framing,
and why “what may this function change?” is a first-class specification question
rather than an implementation detail.
It also becomes the bridge to the hardest topics:
aliasing and separation logic,
which the current “arrays are references but aliasing is forbidden” design
deliberately sidesteps.
Machine Integers (Bit Vectors) vs. Mathematical Integers
Frml’s Int is an unbounded mathematical integer,
so x + 1 > x is always true.
If we add a bounded type or a --int-model bitvector switch,
that theorem quietly breaks:
fn add_one(x: Int32) -> Bool
ensures x + 1 > x // false when x == Int32.max
This is arguably the most important caveat in applied verification:
the model is not the machine.
It teaches why SMT solvers are split into theories,
why overflow is a real bug class,
and why a verified program can still be wrong if the verification model diverges from the runtime.
It also gives a natural way to discuss the tradeoff,
since bit-vector reasoning is harder for the solver than integer arithmetic.
Ghost Code and Lemmas
The final idea is to extend the language
so that programmers can introduce names and functions that exist only in specifications:
ghost var count: Int = 0;
lemma append_len(a: List<Int>, b: List<Int>)
ensures length(a ++ b) == length(a) + length(b);
These ghost variables are the classic trick for proving properties
that the running program has no reason to record,
and lemmas are how a verified fact gets packaged and reused across functions
instead of being re-derived inline.
Together they teach that a proof is a structure of its own
that can be layered on top of,
but kept separate from,
the executable program,
and they unlock the “mathematical library” style of verification
that makes large programs tractable.
This composes naturally with the first feature idea,
since inductive lemmas over data types are the standard way to prove list properties.
fn main() -> Int
{
let a: Array<Int> = [1];
push(a, 2);
assert length(a) == 2;
return 0;
}
Built-in Functions
Frml’s built-in functions live in frml/builtins.py:
read(path: String) -> String returns the contents of a file
write(path: String, text: String) writes text to a file
print(text: String) writes text to standard output
split(text: String, sep: String) -> Array<String> splits text on a separator
args() -> Array<String> returns the command-line arguments
push(array, value) appends a value to an array
pop(array) -> value removes and returns the last element
TypeChecker.check_call first looks the name up in BUILTINS.
For a non-polymorphic built-in,
it checks the argument count and each argument type against the recorded signature,
then checks that a value-returning built-in is not used as a statement.
The same path is reached whether the built-in appears as a statement or as an expression.
push and pop are marked poly=True
because their signatures depend on the element type of the array argument:
_check_poly_builtin resolves them.
push(a, v) requires a to be an array variable and v to have a’s element type;
since it is a procedure, it returns no value.
pop(a) requires a to be an array variable,
returns a’s element type,
and cannot be used as a statement.
Both are also rejected inside specifications,
because a specification must describe a function without mutating arrays.
Verifying Built-Ins
The prover models most built-ins as uninterpreted values:
read becomes a fresh string,
split and args become fresh arrays of strings,
and print and write evaluate their arguments and then have no further effect.
The verifier can therefore prove nothing about a built-in’s contents,
which is sound because file contents and command-line arguments are external to the program.
push and pop are the only built-ins that mutate a program array,
so the prover treats them specially.
The prover models push(a, v) as appending v at the current length:
a = Store(a, length(a), v)
length(a) = length(a) + 1
There is no bounds obligation: appending is always legal.
The array variable is rebound to the new ArrayVal.
The prover models pop(a) as removing the last element:
result = a[length(a) - 1]
length(a) = length(a) - 1
Unlike push, pop emits an obligation that the array is non-empty:
hypotheses: current path
goal: 0 < length(a)
Popping an empty array is therefore a failed verification condition
rather than a runtime error.
Resizing in Loops
A loop that calls push or pop changes an array’s length,
so loop havoc must forget both the contents and the length.
A scalar assignment havocs the scalar’s value,
a fixed-size array assignment havocs the array’s contents but keeps its length,
and an array changed by push or pop havocs the contents and the length.
This is the same induction soundness argument as in the loop and array tutorials:
the invariant is the only information that survives the havoc.
Resizing Across Function Calls
The builtin prover also tracks which array parameters a callee resizes.
written_params contains the array parameters the callee writes,
and resized_params is the subset of written_params that the callee resizes with push or pop.
At a call site,
a written-but-not-resized array parameter gets a fresh post-array with the same length,
while a resized array parameter gets a fresh post-array with a fresh,
unknown length,
and the prover assumes that length is non-negative.
So How Do I Feel About This?
The short answer is “unsatisfied”.
I didn’t want to handle push and pop as special cases,
and I hoped to build some sort of effects system for I/O,
but this project is already larger than I originally intended it to be.
If some students want to take this on,
please reach out.
fn main() -> Int
{
let a: Array<Int> = [2, 3, 5];
assert a[2] == 5;
return length(a);
}
The array type checker subclasses the loop type checker
and adds visitors for the array syntax.
Everything scalar and every while loop is checked exactly as before;
the new visitors only handle array nodes.
Array Access
visit_ExprArrayAccess checks two things:
the expression being indexed must have an array type,
and the index must have type Int.
It then returns the array’s element type.
defvisit_ExprArrayAccess(self,expr,expected,allow_old,result_type):arr=expr.array.accept(self,None,allow_old,result_type)FrmlTypeError.fail(notarr.is_array(),f"array access expects an array but found {arr}",expr.pos,)idx=expr.index.accept(self,None,allow_old,result_type)FrmlTypeError.fail(idx!=INT,"array index must have type Int",expr.pos,)returnarr.elem
Array Literals
visit_ExprArrayLiteral requires every element to be a scalar (Int, Bool, or String)
and all elements to have the same type.
It returns Array<T> for that element type.
An empty literal [] has no elements from which to infer T,
so it is only accepted when the expected type is already known
from the surrounding let declaration, parameter type, or return type.
Array Assignment
visit_StmtArrayAssign checks a[i] = v,
requiring a to have an array type,
i to have type Int,
and v to have the array’s element type.
Array declarations
Scalar let declarations are inherited unchanged.
For an array declaration,
the checker requires the initializer to be either an array literal
or a call to a function that returns an array.
Array-to-array assignment such as let b: Array<Int> = a; is rejected,
because Frml treats arrays as references
and allowing that form would create two names for one array;
the language avoids that aliasing.
(If you want to extend Frml to handle this,
please give me a shout.)
Array Returns
A function may return an array,
but the checker rejects returning an array parameter directly
(again, to avoid aliasing issues).
Returning a literal, a function-local array, or a call that returns an array is fine.
defvisit_StmtReturn(self,stmt,ret):FrmlTypeError.fail((retisnotNoneandret.is_array()andstmt.expr.variable_name()inself.current_params),"cannot return an array parameter (arrays are references)",stmt.pos,)super().visit_StmtReturn(stmt,ret)
length(...)
visit_ExprLength requires its argument to be an array and returns Int.
The Prover’s Array Model
Arrays need more machinery than integers.
Representation
An array is a Z3 Array(Int, elem) plus a length.
The array maps integer indexes to element values,
and the length is a separate symbolic integer.
The prover stores an array as an ArrayVal,
which pairs the Z3 array term with its length.
State.arrays maps array variable names to ArrayVal values,
and State.old_arrays is the snapshot of those values at function entry.
Array Literals
An array literal like [3, 4] becomes a chain of Store operations:
Store(Store(fresh_array, 0, 3), 1, 4)
Its length is the literal 2.
An empty literal produces a fresh array over the expected element sort with length 0.
Access and Assignment
a[i] becomes z3.Select(arr.term, i),
and it also emits a bounds obligation 0 <= i and i < length(a).
a[i] = v becomes z3.Store(arr.term, i, v),
and it also emits a bounds obligation for i.
Bounds Obligations
Every array read and write produces:
hypotheses: current path
goal: 0 <= i and i < length(a)
For example, from increment_first:
goal: And(0 >= 0, 0 < a_len!2)
Array Equality
Frml a == b on two arrays is not a single Z3 equality:
the lengths must be equal,
and every element in range must be equal.
The prover builds:
length(a) == length(b)
and
forall i: 0 <= i and i < length(a) => a[i] == b[i]
old(...) with Arrays
old(e) means “the value of e at the moment the function was entered”.
The prover snapshots parameters at entry into old_vars and old_arrays.
At entry, a is a fresh array symbol a!1 with some length,
and old_arrays["a"] keeps that original a!1.
After the assignment,
state.arrays["a"] is the updated array,
so a[0] in the postcondition reads the updated array
while old(a[0]) reads the original a!1.
The emitted postcondition goal looks like:
Store(a!1, 0, a!1[0] + 1)[0] == a!1[0] + 1
Both sides simplify to the same value, so Z3 proves it.
Loops and Arrays
The array level inherits loop verification from the loop level.
The only difference is that havoc must also account for arrays.
(As a reminder,
this is how the prover forgets what a loop did to a variable.)
An assigned scalar becomes a fresh symbol of the same sort,
and an assigned array becomes a fresh array over the same index and element sorts,
keeping its length.
At the array language level,
lengths never change inside a loop because there is no push or pop (yet).
For a loop body that writes a[i],
the prover havocs the contents of a while preserving length(a).
This keeps the induction sound:
the inductive step does not silently assume which elements were already updated.
while i < length(a)
invariant forall j: Int :: 0 <= j and j < i => a[j] >= 0
{
a[i] = a[i] + 1;
i = i + 1;
}
After havoc,
a is a fresh array with the same length,
and the invariant is the only bridge from before the loop to after it.
Function Calls with Arrays
When one function calls another, the prover uses the callee’s contract.
Array Arguments
A callee may mutate an array argument.
written_params tracks which array parameters a function writes.
A written array gets a fresh post-array,
while a read-only array keeps the caller’s array unchanged.
After the call,
the caller’s array argument is updated to the callee’s post-array:
increment_first writes a[0], so a is in written_params.
At the call increment_first(xs),
the precondition length(a) > 0 becomes length(xs) > 0,
which Z3 proves from xs = [5] (length 1).
The prover creates a fresh post-array a_post!N with the same length,
assumes the postcondition a_post!N[0] == xs[0] + 1,
and rebinds xs to a_post!N.
The later check xs[0] == 6 uses that assumed relationship, so it holds.
Array Returns
A function may return an array, but as noted earlier,
it may only return a fresh one,
i.e.,
an array literal,
a call to another array-returning function,
or a function-local array variable.
At a call site,
the returned array is a fresh ArrayVal with an unknown length >= 0,
exactly like any other result.
The callee’s ensures are assumed,
and the well-formedness obligations inside them
like array bounds and non-zero divisors are suppressed,
because they are part of what is being assumed
rather than something the caller proves.
For example:
At the call,
primes becomes a fresh array
whose length is constrained by ensures length(result) == 4.
The later primes[3] is therefore in bounds,
and its value is 7 by the second ensures.
Quantifiers Over Arrays
Consider evaluating the body 0 <= i and i < length(a) => a[i] >= 0
inside forall i: Int :: ....
a[i] normally emits a bounds obligation 0 <= i and i < length(a)
because an out-of-bounds array read is a proof obligation at that program point.
Inside a quantifier there is no single program point:
i is a bound variable that ranges over all integers,
including ones for which 0 <= i and i < length(a) is false.
Emitting the bounds obligation there would ask Z3 to prove 0 <= i and i < length(a)
for an unconstrained i,
which is false,
so the verifier would wrongly reject the formula.
Instead,
the bounds are part of the quantified formula’s own hypothesis,
since the implication only requires a[i] to be well-defined when its left side is true.
The prover therefore increments _quant_depth while it evaluates a quantified body,
and array accesses and divisions inside that body
skip their bounds and division obligations while _quant_depth > 0.
The quantified body is still built as a Z3 term,
and Z3 reasons about the whole ForAll/Exists formula directly.
fn main() -> Int
{
let i: Int = 0;
while i < 3
invariant 0 <= i
invariant i <= 3
decreases 3 - i
{
i = i + 1;
}
return i;
}
The loop type checker adds one visitor to the existing code called visit_StmtWhile,
and the loop prover adds the same visitor plus the logic that turns a loop into obligations.
visit_StmtWhile checks four things:
the loop condition must have type Bool,
every invariant must have type Bool,
the decreases expression when present must have type Int,
and the loop body is type-checked in a fresh scope.
The in_spec flag is set while checking the loop’s specifications,
just as the contracts checker does for requires, ensures, and decreases clauses.
It has no effect on scalar loops,
but the loop checker keeps the pattern so that subsequent levels will inherit
the same behavior.
The body gets its own scope,
so variables declared inside the loop do not leak out of it.
Why Loops Are Hard
A loop runs an unknown number of times,
and the prover cannot execute the loop symbolically “until it ends”.
It therefore reasons about the loop inductively using invariants.
A loop invariant is a fact that is true before the first iteration and after every iteration;
if both hold,
the invariant is also true immediately after the loop exits.
The prover generates one obligation for each of those two moments,
plus a post-loop exit state for whatever code follows the loop.
The invariant tells the prover what is true at those moments,
but it does not say what value each variable has.
That is a real problem:
a loop that assigns to a variable may run any number of times,
so there is no single value the prover can hand to the rest of the proof.
The prover’s answer is to deliberately forget those values
as explained in the next section.
Causing Havoc
To havoc a variable is to replace its value with a fresh, unknown symbol,
deliberately forgetting everything the prover previously knew about it.
This is how the prover stays sound when a value is genuinely unknown:
rather than pretending to know the final value of an assigned variable,
it admits that it does not.
This is necessary and sound because a loop may run any number of times,
so we cannot know the exact final value of an assigned variable;
we only know what the invariant tells us about it.
The invariant is the only bridge from before the loop to after it.
Before checking the inductive step,
the prover scans the loop body and applies havoc to every scalar variable the body assigns.
A ScalarWriterCollector walks the body
and records every name that appears on the left of an assignment,
including assignments inside nested if and while statements.
It deliberately ignores let declarations inside the loop body,
because those names are local to a single iteration
and do not exist before the loop.
Each recorded name that already exists in the state is replaced with
a fresh symbol of the same Z3 sort:
fn count(n: Int) -> Int
requires n >= 0
ensures result == n
{
let i: Int = 0;
while i < n
invariant 0 <= i
invariant i <= n
decreases n - i
{
i = i + 1;
}
return i;
}
Verifying count emits seven obligations:
two initialization,
two preservation,
two termination,
and one final postcondition.
Initialization Obligations
Every invariant must hold before the first iteration.
With i = 0,
0 <= i becomes 0 <= 0
and i <= n becomes 0 <= n,
proved from requires n >= 0.
The prover evaluates each invariant in the state that reaches the while and emits:
hypotheses: current path
goal: invariant
Preservation Obligations
This is the inductive step,
which checks an arbitrary loop iteration,
not just the first one.
Havoc every scalar variable the loop body assigns:
i becomes a fresh, unknown symbol such as i!2,
which forgets whatever value i had on entry so the check is about an arbitrary iteration.
Assume the invariants and the loop condition, 0 <= i, i <= n, and i < n.
Run the loop body once symbolically, so i = i + 1 becomes i + 1.
Prove each invariant again for the after-body value.
For count, the two preservation obligations are:
(0 <= i and i <= n and i < n) => 0 <= i + 1
(0 <= i and i <= n and i < n) => i + 1 <= n
The second one uses i < n to prove i + 1 <= n.
Exit State
After the loop,
the prover must continue with a state that satisfies the invariant and the negated loop condition.
It havocs the modified variables again,
assumes the invariants,
and assumes not condition.
For count,
after the loop, i becomes a fresh symbol such as i!3,
and the path gains 0 <= i, i <= n, and not (i < n), so i >= n.
Together these force i == n,
and the following return i proves ensures result == n.
The body’s final value is deliberately not connected to the exit value;
the invariant is the only information that survives.
Termination with decreases
A decreases clause proves that a loop terminates.
It produces two obligations.
Before the Loop
Before the loop, the measure must be non-negative:
decreases >= 0
After the Body
After the body, the measure must strictly decrease:
new_decreases < old_decreases
For count, the measure is n - i.
On entry, n - 0 >= 0, proved from requires n >= 0.
After the body,
with the havoced i and the invariant and condition facts assumed,
n - (i + 1) < n - i simplifies to -1 < 0.
The strict-decrease check uses the same havoced i as the preservation check.
A loop without decreases is still accepted;
the verifier then proves partial correctness only.
It cannot prove the loop terminates.
A Broken Loop Invariant
A loop invariant must hold before the first iteration
and survive every execution of the loop body.
The example below survives the first iteration but not the second.
fn bad() -> Bool
{
let i: Int = 0;
while i < 3
invariant i <= 2
{
i = i + 1;
}
return true;
}
The initialization obligation is 0 <= 2, which holds.
The preservation obligation is built exactly like the preservation step in count:
havoc i into an arbitrary fresh symbol,
assume the invariant i <= 2 and the loop condition i < 3,
run the body i = i + 1 once to get the after-body value i + 1,
and prove i + 1 <= 2.
That gives the obligation:
(i <= 2 and i < 3) => i + 1 <= 2
Z3 finds a counterexample with i = 2.
Since 2 <= 2 is true,
the invariant holds before the iteration,
and since 2 < 3 is true,
the loop condition says to run another iteration,
but 2 + 1 <= 2 is false,
so the invariant is broken after the iteration.
The prover does not iterate the loop from 0 to 3;
the preservation check symbolically executes the body once on an arbitrary i,
and the counterexample i = 2 picks the arbitrary iteration
where that one step breaks the invariant.
The correct upper bound is i <= 3, because i reaches 3 before the loop exits.
The first post in this series introduced Frml,
a little procedural language I created
so that I could learn how program verification works.
The second explained how Frml checks simple scalar code;
this one explains how it checks programs with multiple functions.
As a reminder,
the scalar prover owns the engine and leaves two hooks for higher levels:
Contracts are the source of most hypotheses and goals.
At function entry,
every requires clause is evaluated,
the result is appended to the path,
and later obligations may assume it.
At every return,
every ensures clause is evaluated,
the result placeholder is replaced by the returned expression,
and the result becomes a goal checked against the current path.
Multiple requires clauses are and’ed,
one fact per clause in the path,
and multiple ensures clauses produce one obligation per clause.
For example:
fn max(a: Int, b: Int) -> Int
ensures result >= a
ensures result >= b
ensures result == a or result == b
{
if a >= b {
return a;
} else {
return b;
}
}
The if produces two end states,
and there are three ensures clauses,
so there are six postcondition obligations, three per branch.
The if branch goals are a >= a, a >= b, and a == a or a == b;
the else branch goals are b >= a, b >= b, and b == a or b == b.
Each is proved with the appropriate branch condition in the path.
check_postcondition turns an ensures clause into one obligation:
result_term supplies the term that result denotes inside the clause.
A Complete Trace
Let’s trace a tiny function through the whole machine:
fn double(x: Int) -> Int
ensures result == x + x
{
return x + x;
}
fn main() -> Int
{
return double(4);
}
verify_program builds the Prover and calls verify().
verify() sets current_fn = double and calls verify_function(double).
verify_function builds the entry state:
state.vars["x"] = Int("x!1"): a fresh integer symbol.
state.old_vars["x"] = Int("x!1"): the old(...) snapshot.
No requires, no decreases, so _assume_spec leaves the path [].
exec_stmt_seq([return x + x], state) starts with states = [state].
The single statement is return x + x, so exec_stmt calls visit_StmtReturn.
eval_rhs(x + x, state) falls through to eval_expr(x + x, state):
visit_ExprBinary sees the operator +.
The left x becomes Int("x!1"); the right x becomes Int("x!1").
It returns the Z3 term x!1 + x!1.
Back in visit_StmtReturn, value = x!1 + x!1.
_check_ensures runs for the single ensures result == x + x:
It calls check_postcondition, which evaluates result == x + x with
result_term = x!1 + x!1.
result looks up result_term, giving x!1 + x!1.
Each x looks up state.vars["x"], giving x!1.
The goal is the Z3 term (x!1 + x!1) == (x!1 + x!1).
One obligation is emitted with the empty path [].
visit_StmtReturn returns [], so states becomes [] and the loop breaks.
end_states == []; double has a return type and no fall-through path, so no
error is raised.
verify() records ProverResult("double", [the one obligation]).
verify_program hands the obligation to check_obligations, which asks Z3
to refute not (True => (x!1 + x!1) == (x!1 + x!1)). No value of x!1 makes
it true, so Z3 answers unsat and the obligation is VERIFIED.
old(...)
old(e) means “the value of e at the moment the function was entered”.
The prover snapshots parameters at entry into old_vars;
inside an ensures clause,
old(x) reads that snapshot rather than the current value.
For example:
fn bump(x: Int) -> Int
ensures result == old(x) + 1
{
x = x + 1;
return x;
}
At entry,
x is a fresh integer symbol x!1,
and old_vars["x"] keeps that original x!1.
After the assignment,
state.vars["x"] is the term x!1 + 1,
so x in the postcondition reads the updated value while old(x) reads the original x!1.
The emitted postcondition goal looks like:
x!1 + 1 == x!1 + 1
Both sides are the same term, so Z3 proves it.
Function Calls
When one function calls another, the prover uses the callee’s contract.
For a statement call f(args),
the prover proves the callee’s requires clauses under the caller’s current path,
assumes the callee’s ensures clauses,
and adds those assumptions to the caller’s path.
The caller never sees the callee’s body;
it only sees the callee’s contract.
For example:
fn inc(x: Int) -> Int
requires x >= 0
ensures result == x + 1
{ return x + 1; }
fn main() -> Int
{
return inc(41);
}
For the call inc(41),
the prover emits a precondition obligation 41 >= 0,
creates a fresh result inc_result!N,
and assumes inc_result!N == 41 + 1.
main returns that result, and the postcondition is proved.
Recursion
Recursive functions need a decreases clause.
At function entry,
_assume_spec emits decreases >= 0.
For factorial,
that is n >= 0, proved from requires n >= 0.
At a recursive call,
the callee’s requires clauses are proved at the call site.
For factorial(n - 1), the prover proves n - 1 >= 0.
model_call emits decreases_at_call < decreases_at_entry for a self-call.
This applies to statement calls;
for scalar self-calls inside expressions,
such as the recursive call in factorial below,
the current implementation proves the callee’s precondition
but does not emit the strict-decrease obligation.
fn factorial(n: Int) -> Int
requires n >= 0
ensures result >= 1
decreases n
{
if n == 0 {
return 1;
} else {
return n * factorial(n - 1);
}
}
The prover emits four obligations:
n >= 0 for the entry decreases n >= 0,
1 >= 1 for the base-case postcondition,
n - 1 >= 0 for the recursive call’s precondition,
and n * factorial_result >= 1 for the recursive postcondition.
Quantifiers
Frml supports forall and exists in specifications:
forall i: Int :: 0 <= i and i < 3 => i >= 0
The prover translates these to Z3 quantifiers:
forall becomes z3.ForAll([var], body)
and exists becomes z3.Exists([var], body).
The quantified variable becomes a fresh symbol,
and the body is evaluated with that variable added to the state.
In the example above,
the variable i becomes a fresh symbol added to the state,
the body becomes the Z3 term Implies(And(0 <= i, i < 3), i >= 0),
and the whole quantifier becomes z3.ForAll([i], body).
Similarly,
if exists was used,
the variable i would again become a fresh symbol,
the body would become And(0 <= i, i < 3, i == 2),
and the whole quantifier would become z3.Exists([i], body).
Both forms can appear in an ensures clause:
fn f() -> Bool
ensures result == (forall i: Int :: 0 <= i and i < 3 => i >= 0)
{ return true; }
fn g() -> Bool
ensures result == (exists i: Int :: 0 <= i and i < 3 and i == 2)
{ return true; }
Coming up on the anniversary of being laid off,
I’m thinking about what I’d like to do differently in year 2:
Find people in the east end of Toronto who want to play some jazz once a week.
I’m currently commuting to the west end to do that:
I enjoy playing, but the travel time is wearying.
If you’re interested, I’m easy to reach.
Find a small F&SF writers’ group, also in the east end, to swap crits with.
I’m currently getting great feedback from a friend,
but would like more perspectives and an excuse to drink coffee.
(Scribophile has been moderately useful,
Wattpad hardly at all.)
Again,
if you’re interested, please reach out.
Go on long bike rides.
A friend has been going on 50km+ rides this year;
it’ll take me a long time (and probably a new bike) to get up to that,
but it’s a shame not to be out on sunny days like today.
I started working on CATMAID a few weeks ago;
between teaching and other commitments I haven’t been able to immerse myself yet,
but I’m hoping to do that in November.
On the upside,
fixing bugs in software that scientists use is pretty rewarding.
On the other hand,
it’s all remote work,
and I miss being able to grab a cup of coffee with colleagues in person.
Over (almost) 12 months I sent more than 60 job applications,
which led to four interviews and three offers
(one of which I now wish I’d taken).
I don’t think I’m going to send CVs to people I don’t know any more,
but if something interesting comes up in Toronto,
see the note above about coffee with colleagues.
I’m using Jon Udell’s Bram to experiment with AI coding,
mostly so that I won’t just be recycling other people’s talking points
in discussions about the subject.
I expect I’ll keep doing this,
and hope to start contributing to the tool itself.
I’ve nominated myself for a seat on the Carpentries board.
I dithered about this for a long time,
but in the end decided that I’d regret not doing it.
Let’s see how the voting goes…
I’d like to run some undergraduate projects next semester.
I have students lined up for one of the games,
but am still looking for people for the others.
As always, please reach out if you’re interested
(or if you have students who might be).
Most of all,
I’d like to be happier in the coming year than I have been in the one gone past.
Losing my job just a few weeks after my daughter left home for university
put me in a tailspin.
I’ve dealt with depression off and on for years;
the last twelve months weren’t as bad as some dips,
but the trough has lasted longer.
Let’s see what the next year brings.
The first post in this series introduced Frml,
a little procedural language I created
so that I could learn how program verification works.
This post explains how Frml checks scalar-level programs
that have straight-line and branching code over scalar values
with no function calls, contracts, loops, or quantifiers.
The Prover’s Data Model
The prover tracks a program point with a State object.
State.vars holds the symbolic values of scalar variables,
and State.path holds every fact assumed to hold so far.
The prover never stores concrete numbers in variables;
it stores Z3 formulas about numbers.
For example,
x might hold the symbolic integer x!1 rather than the number 5,
where x!1 means “the first fresh symbol named x”.
An Obligation records one claim to prove.
Its kind can be assert or division at this level,
its description is the human readable text of the claim,
hyp is the list of hypothesis terms,
goal is the goal term,
and pos is the source position of the claim
(shown in --trace output).
Fresh Names
The prover keeps a counter and calls _fresh(name)
to get name!N with an increasing N,
so x!1, x!2, and x!3 are different symbols
even though they all relate to the source variable x.
This matters because when x is reassigned,
the old x!1 is not overwritten;
the new value becomes a new symbol such as x!5,
which keeps the symbolic execution correct.
For example, after the statement:
x = x + 1;
the state maps x to the term x!1 + 1, not to a number.
Operation
The prover works in two phases:
it generates obligations by walking the AST and collecting Obligation objects,
then checks them by handing each obligation to Z3 and turning the answers into outcomes.
verify() is the generation phase for the whole program:
verify verifies one function at a time in source order;
self.obligations is reset per function so obligations stay grouped by function.
verify_function() handles one function:
defverify_function(self,fn):state=State()# Entry state: fresh constants for the parameters.forpinfn.params:state.vars[p.name]=self._fresh_scalar(p.type,p.name)# Snapshot for `old(...)` (unused at this level; higher levels read it).state.old_vars=dict(state.vars)self._assume_spec(fn,state)# Run the body. Surviving states reached the end without `return`; for# a value-returning function that is an error.end_states=self.exec_stmt_seq(fn.body,state)iffn.return_typeisnotNone:ifend_states:raiseFrmlVerificationError(f"function {fn.name!r} has a path that does not return",fn.pos)else:forsinend_states:self._check_ensures(fn,s,None)
_assume_spec and _check_ensures do nothing at this language level
because there are no requires, ensures, or decreases clauses,
so the entry path is empty and the body’s fall-through is simply checked.
exec_stmt_seq returns the states of paths that fell off the end of the body.
A return produces no end state (see below),
so if a value-returning function has any end state,
some path never returned,
which is an error.
In exec_stmt_seq, states is the set of live paths,
starting with the single entry state,
and each statement maps every live state to zero or more successor states (see below).
exec_stmt calls stmt.accept(self, state),
which dispatches to visit_StmtAssign, visit_StmtIf, visit_StmtLet, and so on.
The “zero or more” matters because of return:
A return returns the empty list.
new_states.extend([]) adds nothing,
so that path is dropped from states;
execution stops there, exactly as it does at run time.
This is also what makes the verify_function fall-through check work,
since only paths that reach the end of the body survive in end_states.
exec_block is exec_stmt_seq plus scoping.
After a nested block (i.e., an if body) runs,
any variables introduced inside it are deleted from the resulting states,
so local declarations do not leak outward.
Expressions
Expressions use the same visitor pattern as statements:
expr.accept(...) calls visit_ExprBinary, visit_ExprVar, and so on.
Each visitor returns a Z3 term.
eval_expr never actually computes anything;
as noted above,
it translates a Frml expression into the Z3 formula that describes it
using the current symbolic state.
A Complete Trace
Let’s trace a complete verification:
fn main() -> Int
{
let x: Int = 3;
assert x > 0;
return 0;
}
verify_program builds the ScalarProver and calls verify().
verify() sets current_fn = main and calls verify_function(main).
verify_function builds the entry state: state.vars is empty (no
parameters), and the path is empty.
exec_stmt_seq([let, assert, return], state) starts with states = [state].
let x: Int = 3; evaluates the literal 3 and stores it in
state.vars["x"] as the Z3 integer 3 (not a fresh symbol).
At assert x > 0;, the prover evaluates the assertion expression:
x looks up the stored term 3.
> builds the Z3 term 3 > 0.
The prover emits one obligation:
kind: assert
description: assert (x > 0)
hypotheses: the current path (empty here)
goal: 3 > 0
return 0 drops the path, so end_states is empty and no error is raised.
verify() records ProverResult("main", [the one obligation]).
verify_program hands the obligation to check_obligations, which builds
the claim not (True => 3 > 0) and asks Z3 to satisfy it (see “The Z3 check
loop” below).
Z3 finds no assignment that makes not (3 > 0) true, so it returns unsat,
and the obligation is VERIFIED.
uv run frml check --trace examples/scalar/ex01_assign_then_assert.frml prints:
Variables:
the variable x becomes the term currently stored in state.vars["x"].
Operators:
a and b becomes z3.And(a, b) and so on for other unary and binary operators.
Division by zero is undefined,
the verifier turns it into another proof obligation.
n the prover evaluates a / b or a % b, it first emits:
hypotheses: current path
goal: b != 0
and then returns the Z3 division or modulo term. For example:
fn main() -> Int
{
let x: Int = 10;
let y: Int = 2;
if y != 0 {
assert x / y == 5;
}
return 0;
}
The if y != 0 guard puts y != 0 on the path before the division. The
division emits y != 0, which the path already contains, so Z3 proves it
immediately.
Branching
A conditional statement forks the symbolic execution.
The condition is evaluated once,
then the then branch continues with the condition added to the path,
while the else branch continues with not condition added to the path.
(If there is no else, the fall-through branch still gets not condition.)
The prover tracks a list of states, one per path through the code.
Here is the code that does the forking:
An assert statement produces a goal from the current path:
assert 1 < 2;
The prover evaluates the condition, emits an obligation with the current path
as hypotheses and the condition as goal, and if Z3 proves it, execution
continues with the fact now guaranteed.
The prover does not add the assertion to the path after checking
because assert is a check, not an assumption.
The programmer asserts what should already be true,
so the verifier must prove it from what came before.
Each obligation gets a fresh solver context via push and pop.
The empty hypothesis list becomes True.
With no hypotheses, the claim is goal alone, i.e. True => goal.
The code writes z3.BoolVal(True) so z3.And(*ob.hyp) always has a value,
because Z3’s And() is not defined over an empty argument list.
Z3 is asked to satisfy not (hyp => goal).
unsat means the claim holds,
sat means a counterexample exists,
and anything else is unknown.