Compare commits
No commits in common. "0a90e8da293d55f22a9da72c61f92b3845c57e56" and "7ccbaa7829d1abac6cffc520d654647e9abd4df1" have entirely different histories.
0a90e8da29
...
7ccbaa7829
|
|
@ -1 +1 @@
|
||||||
Subproject commit 828b652d3b9266e27ef7cf5a8a7fb82e3fd3133f
|
Subproject commit f0da9a902005b24db4e03a89c2862493735467c4
|
||||||
|
|
@ -1,239 +0,0 @@
|
||||||
---
|
|
||||||
title: "Implementing and Verifying \"Static Program Analysis\" in Agda, Part 4: The Fixed-Point Algorithm"
|
|
||||||
series: "Static Program Analysis in Agda"
|
|
||||||
description: "In this post, I give a top-level overview of my work on formally verified static analyses"
|
|
||||||
date: 2024-08-10T17:37:42-07:00
|
|
||||||
tags: ["Agda", "Programming Languages"]
|
|
||||||
draft: true
|
|
||||||
---
|
|
||||||
|
|
||||||
In the preivous post we looked at lattices of finite height, which are a crucial
|
|
||||||
ingredient to our static analyses. In this post, I will describe the specific
|
|
||||||
algorithm that makes use of these lattices that will be at the core of it all.
|
|
||||||
|
|
||||||
Lattice-based static analyses tend to operate by iteratively combining facts
|
|
||||||
from the program into new ones. For instance, when analyzing `y = 1 + 2`, we
|
|
||||||
take the (trivial) facts that the numbers one and two are positive, and combine
|
|
||||||
them into the knowledge that `y` is positive as well. If another line of code
|
|
||||||
reads `x = y + 1`, we then apply our new knowledge of `y` to determine the sign
|
|
||||||
of `x`, too. Combining facs in this manner gives us more information, which we
|
|
||||||
can then continue to apply to learn more about the program.
|
|
||||||
|
|
||||||
A static program analyzer, however, is a very practical thing. Although in
|
|
||||||
mathemaitics we may allow ourselves to delve into infinite algorithms, we have
|
|
||||||
no such luxury while trying to, say, compile some code. As a result, after
|
|
||||||
a certain point, we need to stop our iterative (re)combination of facts. In
|
|
||||||
an ideal world, that point would be when we know we have found out everything we
|
|
||||||
could about the program. A corollary to that would be that this point must
|
|
||||||
be guaranteed to eventually occur, lest we keep looking for it indenfinitely.
|
|
||||||
|
|
||||||
The fixed-point algorithm does this for us. If we describe our analysis as
|
|
||||||
a monotonic function over a finite-height lattice, this algorithm gives
|
|
||||||
us a surefire way to find out facts about our program that constitute "complete"
|
|
||||||
information that can't be re-inspected to find out more. The algorithm is guaranteed
|
|
||||||
to terminate, which means that we will not get stuck in an infinite loop.
|
|
||||||
|
|
||||||
### The Algorithm
|
|
||||||
Take a lattice \(L\) and a monotonic function \(f\). We've
|
|
||||||
[talked about monotonicity before]({{< relref "01_spa_agda_lattices#define-monotonicity" >}}),
|
|
||||||
but it's easy to re-state. Specifically, a function is monotonic if the following
|
|
||||||
rule holds true:
|
|
||||||
|
|
||||||
{{< latex >}}
|
|
||||||
\textbf{if}\ a \le b\ \textbf{then}\ f(a) \le f(b)
|
|
||||||
{{< /latex >}}
|
|
||||||
|
|
||||||
Recall that the less-than relation on lattices in our case
|
|
||||||
[encodes specificity]({{< relref "01_spa_agda_lattices#specificity" >}}).
|
|
||||||
In particular, if elements of our lattice describe our program, than smaller
|
|
||||||
elements should provide more precise descriptions (where "`x` is potive"
|
|
||||||
is more precise than "`x` has any sign", for example). Viewed through this
|
|
||||||
lens, monotonicity means that more specific inputs produce more specific outputs.
|
|
||||||
That seems reasonable.
|
|
||||||
|
|
||||||
Now, let's start with the least element of our lattice, denoted \(\bot\).
|
|
||||||
A lattice of finite height is guaranteed to have such an element. If it didn't,
|
|
||||||
we could always extend chains by tacking on a smaller element to their bottom,
|
|
||||||
and then the lattice wouldn't have a finite height anymore.
|
|
||||||
|
|
||||||
Now, apply \(f\) to \(\bot\) to get \(f(\bot)\). Since \(\bot\) is the least
|
|
||||||
element, it must be true that \(\bot \le f(\bot)\). Now, if it's "less than or equal",
|
|
||||||
is it "less than", or is "equal")? If it's the latter, we have \(\bot = f(\bot)\).
|
|
||||||
This means we've found a fixed point: given our input \(\bot\) our analysis \(f\)
|
|
||||||
produced no new information, and we're done. Otherwise, we are not done, but we
|
|
||||||
know that \(\bot < f(\bot)\), which will be helpful shortly.
|
|
||||||
|
|
||||||
Continuing the "less than" case, we can apply \(f\) again, this time to \(f(\bot)\).
|
|
||||||
This gives us \(f(f(\bot))\). Since \(f\) is monotonic and \(\bot \le f(\bot)\), we know
|
|
||||||
also that \(f(\bot) \le f(f(\bot))\). Again, ask "which is it?", and as before, if
|
|
||||||
\(f(\bot) = f(f(\bot))\), we have found a fixed point. Otherwise, we know that
|
|
||||||
\(f(\bot) < f(f(\bot))\).
|
|
||||||
|
|
||||||
We can keep doing this. Notice that with each step, we are either done
|
|
||||||
(having found a fixed point) or we have a new inequality in our hands. We can
|
|
||||||
arrange the ones we've seen so far into a chain:
|
|
||||||
|
|
||||||
{{< latex >}}
|
|
||||||
\bot < f(\bot) < f(f(\bot)) < ...
|
|
||||||
{{< /latex >}}
|
|
||||||
|
|
||||||
Each time we fail to find a fixed point, we add one element to our chain, growing
|
|
||||||
it. But if our lattice \(L\) has a finite height, that means eventually this
|
|
||||||
process will have to stop; the chain can't grow forever; eventually, we will
|
|
||||||
have to find a value such that \(v = f(v)\). Thus, our algorithm is guaranteed
|
|
||||||
to terminate, and give a fixed point.
|
|
||||||
|
|
||||||
I implemented the iterative process of applying \(f\) using a recursive function.
|
|
||||||
Agda has a termination checker, to which the logic above --- which proves that
|
|
||||||
iteration will eventually finish --- is not at all obvious. The trick to
|
|
||||||
getting it to work was to use a notion of "gas": an always-decreasing value
|
|
||||||
that serves as one of the functions' arguments. Since the value is always decreasing
|
|
||||||
in size, the termination checker is satisfied.
|
|
||||||
|
|
||||||
This works by observing that we already have a rough idea of the maximum number
|
|
||||||
of times our function will recurse; that would be the height of the lattice.
|
|
||||||
After that, we would be building an impossibly long chain. So, we'll give the
|
|
||||||
function a "budget" of that many iterations, plus one more. Since the chain
|
|
||||||
increases once each time the budget shrinks (indicating recursion), running
|
|
||||||
out of our "gas" will mean that we built an impossibly long chain --- it
|
|
||||||
will provably never happen.
|
|
||||||
|
|
||||||
In all, the recursive function is as follows:
|
|
||||||
|
|
||||||
{{< codelines "Agda" "agda-spa/Fixedpoint.agda" 53 64 >}}
|
|
||||||
|
|
||||||
The first case handles running out of gas, arguing by bottom-elimination (contradiction).
|
|
||||||
The second case follows the algorithm I've described pretty closely; it
|
|
||||||
applies \(f\) to an existing value, checks if the result is equal (equivalent)
|
|
||||||
to the original, and if it isn't, it grows the existing chain of elements
|
|
||||||
and invokes the step function rescurisvely with the grown chain and less gas.
|
|
||||||
|
|
||||||
The recursive function implements a single "step" of the process (applying `f`,
|
|
||||||
comparing for equality, returning the fixed point if one was found). All that's
|
|
||||||
left is to kick off the process using \(\bot\). This is what `fix` does:
|
|
||||||
|
|
||||||
{{< codelines "Agda" "agda-spa/Fixedpoint.agda" 66 67 >}}
|
|
||||||
|
|
||||||
This functions is responsible for providing gas to `doStep`; as I mentioned above,
|
|
||||||
it provides just a bit more gas than the maximum-length chain, which means that
|
|
||||||
if the gas is exhausted, we've certainly arrived at a contradiction. It also
|
|
||||||
provides an initial chain onto which `doStep` will keep tacking on new inequalities
|
|
||||||
as it finds them. Since we haven't found any yet, this is the single-element
|
|
||||||
chain of \(\bot\). The last thing is does is set up the reursion invariant
|
|
||||||
(that the sum of the gas and the chain length is constant), and provides
|
|
||||||
a proof that \(\bot \le f(\bot)\). This function always returns a fixed point.
|
|
||||||
|
|
||||||
### Least Fixed Point
|
|
||||||
Functions can have many fixed points. Take the identity function that simply
|
|
||||||
returns its argument unchanged; this function has a fixed point for every
|
|
||||||
element in its domain, since, for example, \(\text{id}(1) = 1\), \(\text{id}(2) = 2\), etc.
|
|
||||||
The fixed point found by our algorithm above is somewhat special among the
|
|
||||||
possible fixed points of \(f\): it is the _least fixed point_ of the function.
|
|
||||||
Call our fixed point \(a\); if there's another point \(b\) such that \(b=f(b)\),
|
|
||||||
then the fixed point we found must be less than or equal to \(b\) (that is,
|
|
||||||
\(a \le b\)). This is important given our interpretation of "less than" as "more specific":
|
|
||||||
the fixedpoint algorithm produces the most specific possible information about
|
|
||||||
our program given the rules of our analysis.
|
|
||||||
|
|
||||||
The proof is simple; suppose that it took \(k\) iterations of calling \(f\)
|
|
||||||
to arrive at our fixed point. This gives us:
|
|
||||||
|
|
||||||
{{< latex >}}
|
|
||||||
a = \underbrace{f(f(...(f(}_{k\ \text{times}}\bot)))) = f^k(\bot)
|
|
||||||
{{< /latex >}}
|
|
||||||
|
|
||||||
Now, take our other fixed point \(b\). Since \(\bot\) is the least element of
|
|
||||||
the lattice, we have \(\bot \le b\).
|
|
||||||
|
|
||||||
{{< latex >}}
|
|
||||||
\begin{array}{ccccccccr}
|
|
||||||
& & \bot & \le & & & b \quad \implies & \text{(monotonicity of $f$)}\\
|
|
||||||
& & f(\bot) & \le & f(b) & = & b \quad \implies & \text{($b$ is a fixed point, monotonicity of $f$)}\\
|
|
||||||
& & f^2(\bot) & \le & f(b) & = & b \quad \implies & \text{($b$ is a fixed point, monotonicity of $f$)}\\
|
|
||||||
\\
|
|
||||||
& & \vdots & & \vdots & & \vdots & \\
|
|
||||||
\\
|
|
||||||
a & = & f^k(\bot) & \le & f(b) & = & b &
|
|
||||||
\end{array}
|
|
||||||
{{< /latex >}}
|
|
||||||
|
|
||||||
Because of the monotonicity of \(f\), each time we apply it, it preserves the
|
|
||||||
less-than relationship that started with \(\bot \le b\). Doing that \(k\) times,
|
|
||||||
we verify that \(a\) is our fixed point.
|
|
||||||
|
|
||||||
To convince Agda of this proof, we once again get in an argument with the termination
|
|
||||||
checker, which ends the same way it did last time: with us using the notion of 'gas'
|
|
||||||
to ensure that the repeated application of \(f\) eventually ends. Since we're
|
|
||||||
interested in verifying that `doStep` producdes the least fixed point, we formulate
|
|
||||||
the proof in terms of `doStep` applied to various arguments.
|
|
||||||
|
|
||||||
{{< codelines "Agda" "agda-spa/Fixedpoint.agda" 76 84 >}}
|
|
||||||
|
|
||||||
As with `doStep`, this function takes as arguments the amount of gas `g` and
|
|
||||||
a partially-built chain `c`, which gets appended to for each failed equality
|
|
||||||
comparison. In addition, however, this function takes another arbitrary fixed
|
|
||||||
point `b`, which is greater than the current input to `doStep` (which is
|
|
||||||
a value \(f^i(\bot\)\) for some \(i\)). It then proves that when `doStep` terminates
|
|
||||||
(which will be with a value in the form \(f^k(\bot)\)), this value will still
|
|
||||||
be smaller than `b`. Since it is a proof about `doStep`, `stepPreservesLess`
|
|
||||||
proceeds by the same case analysis as its subject, and has a very similar (albeit
|
|
||||||
simpler) structure. In short, though, it encodes the relatively informal proof
|
|
||||||
I gave above.
|
|
||||||
|
|
||||||
Just like with `doStep`, I define a helper function for `stepPreservesLess` that
|
|
||||||
kicks off its recursive invocations.
|
|
||||||
|
|
||||||
{{< codelines "Agda" "agda-spa/Fixedpoint.agda" 86 87 >}}
|
|
||||||
|
|
||||||
Above, `aᶠ` is the output of `fix`:
|
|
||||||
|
|
||||||
{{< codelines "Agda" "agda-spa/Fixedpoint.agda" 69 70 >}}
|
|
||||||
|
|
||||||
### What is a Program?
|
|
||||||
With the fixed point algorithm in hand, we have all the tools we need to define
|
|
||||||
static program analyses:
|
|
||||||
|
|
||||||
1. We've created a collection of "lattice builders", which allow us to combine
|
|
||||||
various lattice building blocks into more complicated structures; these
|
|
||||||
structures are advanced enough to represent the information about our programs.
|
|
||||||
2. We've figured out a way (our fixed point algorithm) to repeatedly apply
|
|
||||||
an inference function to our programs and eventually produce results.
|
|
||||||
This algorithm requires some additional properties from our latttices.
|
|
||||||
3. We've proven that our lattice builders create lattices with these properties,
|
|
||||||
making it possible to use them to construct functions fit for our fixed point
|
|
||||||
algorithm.
|
|
||||||
|
|
||||||
All that's left is to start defining monotonic functions over lattices! Except,
|
|
||||||
what are we analyzing? We've focused a fair bit on the theory of lattices,
|
|
||||||
but we haven't yet defined even a tiny piece of the language that our programs
|
|
||||||
will be analyzing. We will start with programs like this:
|
|
||||||
|
|
||||||
```
|
|
||||||
x = 42
|
|
||||||
y = 1
|
|
||||||
if y {
|
|
||||||
x = -1;
|
|
||||||
} else {
|
|
||||||
x = -2;
|
|
||||||
}
|
|
||||||
```
|
|
||||||
|
|
||||||
We will need to model these programs in Agda by describing them as trees
|
|
||||||
([Abstract Syntax Trees](https://en.wikipedia.org/wiki/Abstract_syntax_tree), to be
|
|
||||||
precise). We will also need to specify how to evaluate these programs (provide
|
|
||||||
the [semantics](https://en.wikipedia.org/wiki/Semantics_(computer_science)) of
|
|
||||||
our language). We will use big-step (also known as "natural") operational semantics
|
|
||||||
to do so; here's an example rule:
|
|
||||||
|
|
||||||
{{< latex >}}
|
|
||||||
\frac{\rho_1, e \Downarrow z \quad \neg (z = 0) \quad \rho_1,s_1 \Downarrow \rho_2}
|
|
||||||
{\rho_1, \textbf{if}\ e\ \textbf{then}\ s_1\ \textbf{else}\ s_2\ \Downarrow\ \rho_2}
|
|
||||||
{{< /latex >}}
|
|
||||||
|
|
||||||
The above reads:
|
|
||||||
|
|
||||||
> If the condition of an `if`-`else` statement evaluates to a nonzero value,
|
|
||||||
> then to evaluate the statement, you evaluate its `then` branch.
|
|
||||||
|
|
||||||
In the next post, we'll talk more about how these rules work, and define
|
|
||||||
the remainder of them to give our language life. See you then!
|
|
||||||
Loading…
Reference in New Issue
Block a user