From 615aeb72da7259eee2b4e3a676602a8223d6f8fd Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sun, 3 Nov 2024 16:58:06 -0800 Subject: [PATCH] Finish most of part 5 of SPA series Signed-off-by: Danila Fedorin --- content/blog/05_spa_agda_semantics/index.md | 69 ++++++++++++++++++++- 1 file changed, 68 insertions(+), 1 deletion(-) diff --git a/content/blog/05_spa_agda_semantics/index.md b/content/blog/05_spa_agda_semantics/index.md index 944fa17..f58d0a5 100644 --- a/content/blog/05_spa_agda_semantics/index.md +++ b/content/blog/05_spa_agda_semantics/index.md @@ -418,13 +418,52 @@ to evaluate the _expression_ that serves as the condition. We then had an additional premise that requires the truthiness of the resulting value \(v\). The rule for evaluating a conditional with a "false" branch is very similar. - {{< latex >}} \frac { \rho_1 , e \Downarrow v \quad v = 0 \quad \rho_1, s_2 \Rightarrow \rho_2} { \rho_1, \textbf{if}\ e\ \{ s_1 \}\ \textbf{else}\ \{ s_2 \}\ \Rightarrow \rho_2 } {{< /latex >}} +Now that we have rules for conditional statements, it will be surprisingly easy +to define the rules for `while` loops. A `while` loop will also have two rules, +one for when its condition is truthy and one for when it's falsey. However, +unlike the "false" case, a while loop will do nothing, leaving the environment +unchanged: + +{{< latex >}} +\frac + { \rho_1 , e \Downarrow v \quad v = 0 } + { \rho_1 , \textbf{while}\ e\ \{ s \}\ \Rightarrow \rho_1 } +{{< /latex >}} + +The trickiest rule is for when the condition of a `while` loop is true. +We evaluate the body once, starting in environment \(\rho_1\) and finishing +in \(\rho_2\), but then we're not done. In fact, we have to go back to the top, +and check the condition again, starting over. As a result, we include another +premise, that tells us that evaluating the loop starting at \(\rho_2\), we +eventually end in state \(\rho_3\). This encodes the "rest of the iterations" +in addition to the one we just performed. The environment \(\rho_3\) is our +final state, so that's what we use in the rule's conclusion. + +{{< latex >}} +\frac + { \rho_1 , e \Downarrow v \quad v \neq 0 \quad \rho_1 , s \Rightarrow \rho_2 \quad \rho_2 , \textbf{while}\ e\ \{ s \}\ \Rightarrow \rho_3 } + { \rho_1 , \textbf{while}\ e\ \{ s \}\ \Rightarrow \rho_3 } +{{< /latex >}} + +And that's it! We have now seen every rule that defines the little object language +I've been using for my Agda work. As with all the other rules we've seen, the +mathematical notation above can be directly translated into Agda: + +{{< codelines "Agda" "agda-spa/Language/Semantics.agda" 47 64 >}} + +Below is a Bergamot widget that implements these rules. Try the following program, +which computes the `x`th power of two, and stores it in `y`: + +``` +x = 5; y = 1; while (x) { y = y + y; x = x - 1 } +``` + {{< bergamot_widget id="stmt-widget" query="" prompt="step(extend(extend(extend(empty, x, 17), y, 42), z, 0), TERM, ?env)" modes="Statement:Statement" >}} hidden section "" { Eq @ eq(?x, ?x) <-; @@ -460,3 +499,31 @@ hidden section "" { EnvSkip @ inenv(?x, ?v_1, extend(?rho, ?y, ?v_2)) <- inenv(?x, ?v_1, ?rho), not(eq(?x, ?y)); } {{< /bergamot_widget >}} + +### Semantics as Ground Truth + +Prior to this post, we had been talking about using lattices and monotone +functions for program analysis. The key problem with using this framework to +define analyses is that there are many monotone functions that produce complete +nonsese; their output is, at best, unrelated to the program they're supposed +to analyze. We don't want to write such functions, since having incorrect +information about the programs in question is unhelpful. + +What does it mean for a function to produce correct information, though? +In the context of sign analysis, it would mean that if we say a variable `x` is `+`, +then evaluating the program will leave us in a state in which `x` is posive. +The semantics we defined in this post give us the "evaluating the program piece". +They establish what the programs _actually_ do, and we can use this ground +truth when checking that our analyses are correct. In subsequent posts, I will +prove the exact property I informally stated above: __for the program analyses +we define, things they "claim" about our program will match what actually happens +when executing the program using our semantics__. + +A piece of the puzzle still remains: how are we going to use the monotone +functions we've been talking so much about? We need to figure out what to feed +to our analyses before we can prove their correctness. + +I have an answer to that question: we will be using _control flow graphs_ (CFGs). +These are another program representation, one that's more commonly found in +compilers. I will show what they look like in the next post. I hope to see you +there!