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

Proofread and publish part 4

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2024-11-03 17:37:44 -08:00
parent 951aafc90a
commit 4fc1191d13
1 changed files with 9 additions and 9 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

18
content/blog/04_spa_agda_fixedpoint.md
View File

@ -4,12 +4,12 @@ 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.
algorithm that makes use of these lattices; this algorithm will be at the core
of this series.
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
@ -79,7 +79,7 @@ arrange the ones we've seen so far into a chain:
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
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.
@ -119,7 +119,7 @@ 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
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.
@ -147,11 +147,11 @@ 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{)}\\
& & \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 & \\
& & \vdots & & \vdots & & \vdots & & \\
\\
a & = & f^k(\bot) & \le & f(b) & = & b &
\end{array}
@ -159,7 +159,7 @@ a & = & f^k(\bot) & \le & f(b) & = & b &
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.
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'