blog-static/04_spa_agda_fixedpoint.md at 6048dc0b9c832e81397f95e04ae5c7325b9a0fe6

Danila Fedorin 3b9c2edcdd Write up the "verified" portion of the forward analysis

Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>

2024-12-25 19:03:51 -08:00

12 KiB

Raw Blame History

title

series

description

date

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. {#start-least}

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:

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:

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 recursion 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 \text{)}\ & & f(\bot) & \le & f(b) & = & b & \quad \implies & \text{(} b\ \text{is a fixed point, monotonicity of}\ f \text{)}\ & & f^2(\bot) & \le & f(b) & = & b & \quad \implies & \text{(} b\ \text{is a fixed point, monotonicity of}\ f \text{)}\ \ & & \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 least 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.

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.

Above, aᶠ is the output of fix:

What is a Program?

With the fixed point algorithm in hand, we have all the tools we need to define static program analyses:

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.
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.
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, to be precise). We will also need to specify how to evaluate these programs (provide the semantics 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!

12 KiB Raw Blame History

The Algorithm

Least Fixed Point

What is a Program?

12 KiB

Raw Blame History