From 0c004b2e8503cce224dbc9fafb8968cae855f553 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sat, 20 Nov 2021 23:36:45 -0800 Subject: [PATCH] Edit the Dawn post a bit --- content/blog/coq_dawn.md | 21 +++++++++++---------- 1 file changed, 11 insertions(+), 10 deletions(-) diff --git a/content/blog/coq_dawn.md b/content/blog/coq_dawn.md index 827985b..1f2b763 100644 --- a/content/blog/coq_dawn.md +++ b/content/blog/coq_dawn.md @@ -14,7 +14,7 @@ and that's what I reached for when making this attempt. ### Defining the Syntax #### Expressions and Intrinsics -For the most part, this is the easy part. A Dawn expression is one of three things: +This is mostly the easy part. A Dawn expression is one of three things: * An "intrinsic", written \\(i\\), which is akin to a built-in function or command. * A "quote", written \\([e]\\), which takes a Dawn expression \\(e\\) and moves it onto the stack (Dawn is stack-based). @@ -45,7 +45,7 @@ Why do we need `e_int`? We do because a token like \\(\\text{swap}\\) can be vie as belonging to the set of intrinsics \\(i\\), or the set of expressions, \\(e\\). While writing down the rules in mathematical notation, what exactly the token means is inferred from context - clearly \\(\\text{swap}\\ \\text{drop}\\) is an expression built from two other expressions. In statically-typed -functional languages (like Coq or Haskell), however, the same expression can't belong to two different, +functional languages like Coq or Haskell, however, the same expression can't belong to two different, arbitrary types. Thus, to turn an intrinsic into an expression, we need to wrap it up in a constructor, which we called `e_int` here. Other than that, `e_quote` accepts as argument another expression, `e` (the thing being quoted), and `e_comp` accepts two expressions, `e1` and `e2` (the two sub-expressions being composed). @@ -59,7 +59,7 @@ names are reserved in Coq, we can just call our constructors exactly the same as in the written formalization. #### Values and Value Stacks -Values are up next. My initial temptation was to define a value much like +Values are up next. My initial thought was to define a value much like I defined an intrinsic expression: by wrapping an expression in a constructor for a new data type. Something like: @@ -245,7 +245,7 @@ I invite you to take a look at the "shape" of the proof: `Sem_e_int`, which handles the intrinsic case. This, in turn, requires that we show the effect of the intrinsic itself; the `apply` intrinsic evaluates the quoted expression on the stack. - The quoted expression is contains the body of false, or \\(\\text{drop}\\). This is + The quoted expression contains the body of false, or \\(\\text{drop}\\). This is once again an intrinsic, so we use `Sem_e_int`; the intrinsic in question is \\(\\text{drop}\\), so the `Sem_drop` rule takes care of that. @@ -277,7 +277,7 @@ Similarly, we prove that \\(\\text{or}\\) applied to \\(\\text{true}\\) always r {{< codelines "Coq" "dawn/Dawn.v" 75 83 >}} -Finally, the specific facts (like \\(\\text{false}\\ \\text{or} \\text{false}\\) evaluating to \\(\\text{false}\\)) +Finally, the specific facts (like \\(\\text{false}\\ \\text{or}\\ \\text{false}\\) evaluating to \\(\\text{false}\\)) can be expressed using our two new proofs, `or_false_v` and `or_true`. {{< codelines "Coq" "dawn/Dawn.v" 85 88 >}} @@ -292,7 +292,7 @@ on the stack. This is defined in terms of other Dawn expressions as follows: \text{quote}_n = \text{quote}_{n-1}\ \text{swap}\ \text{quote}\ \text{swap}\ \text{compose} {{< /latex >}} -We can define this in Coq as follows: +We can write this in Coq as follows: {{< codelines "Coq" "dawn/Dawn.v" 90 94 >}} @@ -330,7 +330,7 @@ Thus, it will try `Sem_swap` if the expression is \\(\\text{swap}\\), {{< codelines "Coq" "dawn/Dawn.v" 138 144 >}} #### Rotations -There's a little trick to formalizing rotations. There's an important property of values: +There's a little trick to formalizing rotations. Values have an important property: when a value is run against a stack, all it does is place itself on a stack. We can state this as follows: @@ -353,21 +353,22 @@ placed back on the stack. {{< codelines "Coq" "dawn/Dawn.v" 156 168 >}} ### `e_comp` is Associative -When composing three expressions, which way of pressing parentheses is correct? -Is it \\((e_1\\ e_2)\\ e_3\\)? Or is it \\(e_1\\ (e_2\\ e_3)\\)? Well, neither! +When composing three expressions, which way of inserting parentheses is correct? +Is it \\((e_1\\ e_2)\\ e_3\\)? Or is it \\(e_1\\ (e_2\\ e_3)\\)? Well, both! Expression composition is associative, which means that the order of the parentheses doesn't matter. We state this in the following theorem, which says that the two ways of writing the composition, if they evaluate to anything, evaluate to the same thing. {{< codelines "Coq" "dawn/Dawn.v" 170 171 >}} +### Conclusion That's all I've got in me for today. However, we got pretty far! The Dawn specification says: > One of my long term goals for Dawn is to democratize formal software verification in order to make it much more feasible and realistic to write perfect software. I think that Dawn is definitely getting there: formally defining the semantics outlined -on the page was quite straightforward! We can now have complete confidence in the behavior +on the page was quite straightforward. We can now have complete confidence in the behavior of \\(\\text{true}\\), \\(\\text{false}\\), \\(\\text{or}\\), \\(\\text{quote}_n\\) and \\(\\text{rotate}_n\\). The proof of associativity is also enough to possibly argue for simplifying the core calculus' syntax even more. All of this we got from an official source, with only