From 0a90e8da293d55f22a9da72c61f92b3845c57e56 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sun, 18 Aug 2024 11:05:51 -1000 Subject: [PATCH] Write a draft of the fixed point algorithm article Signed-off-by: Danila Fedorin --- content/blog/04_spa_agda_fixedpoint.md | 239 +++++++++++++++++++++++++ 1 file changed, 239 insertions(+) create mode 100644 content/blog/04_spa_agda_fixedpoint.md diff --git a/content/blog/04_spa_agda_fixedpoint.md b/content/blog/04_spa_agda_fixedpoint.md new file mode 100644 index 0000000..84daa48 --- /dev/null +++ b/content/blog/04_spa_agda_fixedpoint.md @@ -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!