Web-Projects/blog-static
1
0
Fork 0
Code Issues Pull Requests Releases Wiki Activity

Write a draft of the fixed point algorithm article

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2024-08-18 11:05:51 -10:00
parent 32fe8e5ee6
commit 0a90e8da29
1 changed files with 239 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

239
content/blog/04_spa_agda_fixedpoint.md Normal file
View File

@ -0,0 +1,239 @@
---
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!