Write a draft of the fixed point algorithm article

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

code/agda-spa

@@ -1 +1 @@
-Subproject commit f0da9a902005b24db4e03a89c2862493735467c4
+Subproject commit 828b652d3b9266e27ef7cf5a8a7fb82e3fd3133f

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!