106 lines
5.1 KiB
Markdown
106 lines
5.1 KiB
Markdown
---
|
|
title: "Implementing and Verifying \"Static Program Analysis\" in Agda, Part 2: Combining Lattices"
|
|
series: "Static Program Analysis in Agda"
|
|
date: 2024-04-13T14:23:03-07:01
|
|
draft: true
|
|
tags: ["Agda", "Programming Languages"]
|
|
---
|
|
|
|
In the previous post, I wrote about how lattices arise when tracking, comparing
|
|
and combining static information about programs. I then showed two simple lattices:
|
|
the natural numbers, and the (parameterized) "above-below" lattice, which
|
|
modified an arbitrary set with "bottom" and "top" elements (\(\bot\) and \(\top\)
|
|
respectively). One instance of the "above-below" lattice was the sign lattice,
|
|
which could be used to reason about the signs (positive, negative, or zero)
|
|
of variables in a program.
|
|
|
|
At the end of that post, I introduced a source of complexity: the "full"
|
|
lattices that we want to use for the program analysis aren't signs or numbers,
|
|
but maps of states and variables to lattices-based states. The full lattice
|
|
for sign analysis might something in the form:
|
|
|
|
{{< latex >}}
|
|
\text{Info} \triangleq \text{ProgramStates} \to (\text{Variables} \to \text{Sign})
|
|
{{< /latex >}}
|
|
|
|
Thus, we have to compare and find least upper bounds (e.g.) of not just
|
|
signs, but maps! Proving the various lattice laws for signs was not too
|
|
challenging, but for for a two-level map like \(\text{info}\) above, we'd
|
|
need to do a lot more work. We need tools to build up such complicated lattices!
|
|
|
|
The way to do this, it turns out, is by using simpler lattices as building blocks.
|
|
To start with, let's take a look at a very simple way of combining lattices:
|
|
taking the Cartesian product.
|
|
|
|
### The Cartesian Product Lattice
|
|
|
|
Suppose you have two lattices \(L_1\) and \(L_2\). As I covered in the previous
|
|
post, each lattice comes equipped with a "least upper bound" operator \((\sqcup)\)
|
|
and a "greatest lower bound" operator \((\sqcap)\). Since we now have two lattices,
|
|
let's use numerical suffixes to disambiguate between the operators
|
|
of the first and second lattice: \((\sqcup_1)\) will be the LUB operator of
|
|
the first lattice \(L_1\), and \((\sqcup_2)\) of the second lattice \(L_2\).
|
|
|
|
Then, let's take the Cartesian product of the elements of \(L_1\) and \(L_2\);
|
|
mathematically, we'll write this as \(L_1 \times L_2\), and in Agda, we can
|
|
just use the standard [`Data.Product`](https://agda.github.io/agda-stdlib/master/Data.Product.html)
|
|
module. In Agda, I'll define the lattice as another [parameterized module](https://agda.readthedocs.io/en/latest/language/module-system.html#parameterised-modules). Since both \(L_1\) and \(L_2\)
|
|
are lattices, this parameterized module will require `IsLattice` instances
|
|
for both types:
|
|
|
|
{{< codelines "Agda" "agda-spa/Lattice/Prod.agda" 1 7 >}}
|
|
|
|
Elements of \(L_1 \times L_2\) are in the form \((l_1, l_2)\), where
|
|
\(l_1 \in L_1\) and \(l_2 \in L_2\). The first thing we can get out of the
|
|
way is define what it means for two such elements to be equal. Recall that
|
|
we opted for a [custom equivalence relation]({{< relref "01_spa_agda_lattices#definitional-equality" >}})
|
|
instead of definitional equality to allow similar elements to be considered
|
|
equal; we'll have to define a similar relation for our new product lattice.
|
|
That's easy enough: we have an equality predicate `_≈₁_` that checks if an element
|
|
of \(L_1\) is equal to another, and we have `_≈₂_` that does the same for \(L_2\).
|
|
It's reasonable to say that _pairs_ of elements are equal if their respective
|
|
first and second elements are equal:
|
|
|
|
{{< latex >}}
|
|
(l_1, l_2) \approx (j_1, j_2) \iff l_1 \approx_1 j_1 \land l_2 \approx_2 j_2
|
|
{{< /latex >}}
|
|
|
|
In Agda:
|
|
|
|
{{< codelines "Agda" "agda-spa/Lattice/Prod.agda" 39 40 >}}
|
|
|
|
Verifying that this relation has the properties of an equivalence relation
|
|
boils down to the fact that `_≈₁_` and `_≈₂_` are themselves equivalence
|
|
relations.
|
|
|
|
{{< codelines "Agda" "agda-spa/Lattice/Prod.agda" 42 48 >}}
|
|
|
|
In fact, defining \((\sqcup)\) and \((\sqcap)\) by simply applying the
|
|
corresponding operators from \(L_1\) and \(L_2\) seems quite natural as well.
|
|
|
|
{{< latex >}}
|
|
(l_1, l_2) \sqcup (j_1, j_2) \triangleq (l_1 \sqcup_1 j_1, l_2 \sqcup_2 j_2) \\
|
|
(l_1, l_2) \sqcap (j_1, j_2) \triangleq (l_1 \sqcap_1 j_1, l_2 \sqcap_2 j_2)
|
|
{{< /latex >}}
|
|
|
|
In Agda:
|
|
|
|
{{< codelines "Agda" "agda-spa/Lattice/Prod.agda" 50 54 >}}
|
|
|
|
All that's left is to prove the various (semi)lattice properties. Intuitively,
|
|
we can see that since the "combined" operator `_≈_` just independently applies
|
|
the element operators `_≈₁_` and `_≈₂_`, as long as they are idempotent,
|
|
commutative, and associative, so is the "combined" operator itself.
|
|
Moreover, the proofs that `_⊔_` and `_⊓_` form semilattices are identical
|
|
up to replacing \((\sqcup)\) with \((\sqcap)\). Thus, in Agda, we can write
|
|
the code once, parameterizing it by the binary operators involved (and proofs
|
|
that these operators obey the semilattice laws).
|
|
|
|
{{< codelines "Agda" "agda-spa/Lattice/Prod.agda" 56 82 >}}
|
|
|
|
Similarly to the semilattice properties, proving lattice properties boils
|
|
down to applying the lattice properties of \(L_1\) and \(L_2\) to
|
|
individual components.
|
|
|
|
{{< codelines "Agda" "agda-spa/Lattice/Prod.agda" 84 96 >}}
|