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

Convert AoC Coq article to new math delimiters

Browse Source 
Signed-off-by: Danila Fedorin <danila.fedorin@gmail.com>
This commit is contained in:
Danila Fedorin 2024-05-13 18:16:20 -07:00
parent 74daeee140
commit 189422bf1e
1 changed files with 85 additions and 85 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

170
content/blog/01_aoc_coq.md
View File

@ -58,7 +58,7 @@ Here's another inference rule, this time with some mathematical notation instead
{n + 1 < m + 1} {n + 1 < m + 1}
{{< /latex >}} {{< /latex >}}
This one reads, "if \\(n\\) is less than \\(m\\), then \\(n+1\\) is less than \\(m+1\\)". We can use inference This one reads, "if \(n\) is less than \(m\), then \(n+1\) is less than \(m+1\)". We can use inference
rules to define various constructs. As an example, let's define what it means for a natural number to be even. rules to define various constructs. As an example, let's define what it means for a natural number to be even.
It takes two rules: It takes two rules:
@ -80,7 +80,7 @@ again we see that 4 is even, as well. We can continue this to determine that 6,
are even too. Never in this process will we visit the numbers 1 or 3 or 5, and that's good - they're not even! are even too. Never in this process will we visit the numbers 1 or 3 or 5, and that's good - they're not even!
Let's now extend this notion to programming languages, starting with a simple arithmetic language. Let's now extend this notion to programming languages, starting with a simple arithmetic language.
This language is made up of natural numbers and the \\(\square\\) operation, which represents the addition This language is made up of natural numbers and the \(\square\) operation, which represents the addition
of two numbers. Again, we need two rules: of two numbers. Again, we need two rules:
{{< latex >}} {{< latex >}}
@ -93,14 +93,14 @@ of two numbers. Again, we need two rules:
{e_1 \square e_2 \; \text{evaluates to} \; n_1 + n_2} {e_1 \square e_2 \; \text{evaluates to} \; n_1 + n_2}
{{< /latex >}} {{< /latex >}}
First, let me explain myself. I used \\(\square\\) to demonstrate two important points. First, languages can be made of First, let me explain myself. I used \(\square\) to demonstrate two important points. First, languages can be made of
any kind of characters we want; it's the rules that we define that give these languages meaning. any kind of characters we want; it's the rules that we define that give these languages meaning.
Second, while \\(\square\\) is the addition operation _in our language_, \\(+\\) is the _mathematical addition operator_. Second, while \(\square\) is the addition operation _in our language_, \(+\) is the _mathematical addition operator_.
They are not the same - we use the latter to define how the former works. They are not the same - we use the latter to define how the former works.
Finally, writing "evaluates to" gets quite tedious, especially for complex languages. Instead, Finally, writing "evaluates to" gets quite tedious, especially for complex languages. Instead,
PLT people use notation to make their semantics more concise. The symbol \\(\Downarrow\\) is commonly PLT people use notation to make their semantics more concise. The symbol \(\Downarrow\) is commonly
used to mean "evaluates to"; thus, \\(e \Downarrow v\\) reads "the expression \\(e\\) evaluates to the value \\(v\\). used to mean "evaluates to"; thus, \(e \Downarrow v\) reads "the expression \(e\) evaluates to the value \(v\).
Using this notation, our rules start to look like the following: Using this notation, our rules start to look like the following:
{{< latex >}} {{< latex >}}
@ -147,8 +147,8 @@ Inductive tinylang : Type :=
| box (e1 e2 : tinylang) : tinylang. | box (e1 e2 : tinylang) : tinylang.
``` ```
This defines the two elements of our example language: `number n` corresponds to \\(n\\), and `box e1 e2` corresponds This defines the two elements of our example language: `number n` corresponds to \(n\), and `box e1 e2` corresponds
to \\(e_1 \square e_2\\). Finally, we define the inference rules: to \(e_1 \square e_2\). Finally, we define the inference rules:
```Coq {linenos=true} ```Coq {linenos=true}
Inductive tinylang_sem : tinylang -> nat -> Prop := Inductive tinylang_sem : tinylang -> nat -> Prop :=
@ -158,7 +158,7 @@ Inductive tinylang_sem : tinylang -> nat -> Prop :=
tinylang_sem (box e1 e2) (n1 + n2). tinylang_sem (box e1 e2) (n1 + n2).
``` ```
When we wrote our rules earlier, by using arbitrary variables like \\(e_1\\) and \\(n_1\\), we implicitly meant When we wrote our rules earlier, by using arbitrary variables like \(e_1\) and \(n_1\), we implicitly meant
that our rules work for _any_ number or expression. When writing Coq we have to make this assumption explicit that our rules work for _any_ number or expression. When writing Coq we have to make this assumption explicit
by using `forall`. For instance, the rule on line 2 reads, "for any number `n`, the expression `n` evaluates to `n`". by using `forall`. For instance, the rule on line 2 reads, "for any number `n`, the expression `n` evaluates to `n`".
@ -167,8 +167,8 @@ by using `forall`. For instance, the rule on line 2 reads, "for any number `n`,
We've now written some example big-step operational semantics, both "on paper" and in Coq. Now, it's time to take a look at We've now written some example big-step operational semantics, both "on paper" and in Coq. Now, it's time to take a look at
the specific semantics of the language from Day 8! Our language consists of a few parts. the specific semantics of the language from Day 8! Our language consists of a few parts.
First, there are three opcodes: \\(\texttt{jmp}\\), \\(\\texttt{nop}\\), and \\(\\texttt{add}\\). Opcodes, combined First, there are three opcodes: \(\texttt{jmp}\), \(\texttt{nop}\), and \(\texttt{add}\). Opcodes, combined
with an integer, make up an instruction. For example, the instruction \\(\\texttt{add} \\; 3\\) will increase the with an integer, make up an instruction. For example, the instruction \(\texttt{add} \; 3\) will increase the
content of the accumulator by three. Finally, a program consists of a sequence of instructions; They're separated content of the accumulator by three. Finally, a program consists of a sequence of instructions; They're separated
by newlines in the puzzle input, but we'll instead separate them by semicolons. For example, here's a complete program. by newlines in the puzzle input, but we'll instead separate them by semicolons. For example, here's a complete program.
@ -181,17 +181,17 @@ it will add 0 to the accumulator (keeping it the same),
do nothing, and finally jump back to the beginning. At this point, it will try to run the addition instruction again, do nothing, and finally jump back to the beginning. At this point, it will try to run the addition instruction again,
which is not allowed; thus, the program will terminate. which is not allowed; thus, the program will terminate.
Did you catch that? The semantics of this language will require more information than just our program itself (which we'll denote by \\(p\\)). Did you catch that? The semantics of this language will require more information than just our program itself (which we'll denote by \(p\)).
* First, to evaluate the program we will need a program counter, \\(\\textit{c}\\). This program counter * First, to evaluate the program we will need a program counter, \(\textit{c}\). This program counter
will tell us the position of the instruction to be executed next. It can also point past the last instruction, will tell us the position of the instruction to be executed next. It can also point past the last instruction,
which means our program terminated successfully. which means our program terminated successfully.
* Next, we'll need the accumulator \\(a\\). Addition instructions can change the accumulator, and we will be interested * Next, we'll need the accumulator \(a\). Addition instructions can change the accumulator, and we will be interested
in the number that ends up in the accumulator when our program finishes executing. in the number that ends up in the accumulator when our program finishes executing.
* Finally, and more subtly, we'll need to keep track of the states we visited. For instance, * Finally, and more subtly, we'll need to keep track of the states we visited. For instance,
in the course of evaluating our program above, we encounter the \\((c, a)\\) pair of \\((0, 0)\\) twice: once in the course of evaluating our program above, we encounter the \((c, a)\) pair of \((0, 0)\) twice: once
at the beginning, and once at the end. However, whereas at the beginning we have not yet encountered the addition at the beginning, and once at the end. However, whereas at the beginning we have not yet encountered the addition
instruction, at the end we have, so the evaluation behaves differently. To make the proofs work better in Coq, instruction, at the end we have, so the evaluation behaves differently. To make the proofs work better in Coq,
we'll use a set \\(v\\) of we'll use a set \(v\) of
{{< sidenote "right" "allowed-note" "allowed (valid) program counters (as opposed to visited program counters)." >}} {{< sidenote "right" "allowed-note" "allowed (valid) program counters (as opposed to visited program counters)." >}}
Whereas the set of "visited" program counters keeps growing as our evaluation continues, Whereas the set of "visited" program counters keeps growing as our evaluation continues,
the set of "allowed" program counters keeps shrinking. Because the "allowed" set never stops shrinking, the set of "allowed" program counters keeps shrinking. Because the "allowed" set never stops shrinking,
@ -206,10 +206,10 @@ never changes; only the state does. So I propose this (rather unorthodox) notati
(c, a, v) \Rightarrow_p (c', a', v') (c, a, v) \Rightarrow_p (c', a', v')
{{< /latex >}} {{< /latex >}}
This reads, "after starting at program counter \\(c\\), accumulator \\(a\\), and set of valid addresses \\(v\\), This reads, "after starting at program counter \(c\), accumulator \(a\), and set of valid addresses \(v\),
the program \\(p\\) terminates with program counter \\(c'\\), accumulator \\(a'\\), and set of valid addresses \\(v'\\)". the program \(p\) terminates with program counter \(c'\), accumulator \(a'\), and set of valid addresses \(v'\)".
Before creating the inference rules for this evaluation relation, let's define the effect of evaluating a single Before creating the inference rules for this evaluation relation, let's define the effect of evaluating a single
instruction, using notation \\((c, a) \rightarrow_i (c', a')\\). An addition instruction changes the accumulator, instruction, using notation \((c, a) \rightarrow_i (c', a')\). An addition instruction changes the accumulator,
and increases the program counter by 1. and increases the program counter by 1.
{{< latex >}} {{< latex >}}
@ -240,8 +240,8 @@ is done evaluating, and is in a "failed" state.
{(c, a, v) \Rightarrow_{p} (c, a, v)} {(c, a, v) \Rightarrow_{p} (c, a, v)}
{{< /latex >}} {{< /latex >}}
We use \\(\\text{length}(p)\\) to represent the number of instructions in \\(p\\). Note the second premise: We use \(\text{length}(p)\) to represent the number of instructions in \(p\). Note the second premise:
even if our program counter \\(c\\) is not included in the valid set, if it's "past the end of the program", even if our program counter \(c\) is not included in the valid set, if it's "past the end of the program",
the program terminates in an "ok" state. the program terminates in an "ok" state.
{{< sidenote "left" "avoid-c-note" "Here's a rule for terminating in the \"ok\" state:" >}} {{< sidenote "left" "avoid-c-note" "Here's a rule for terminating in the \"ok\" state:" >}}
In the presented rule, we don't use the variable <code>c</code> all that much, and we know its concrete In the presented rule, we don't use the variable <code>c</code> all that much, and we know its concrete
@ -281,20 +281,20 @@ our program can take a step, and continue evaluating from there.
This is quite a rule. A lot of things need to work out for a program to evauate from a state that isn't This is quite a rule. A lot of things need to work out for a program to evauate from a state that isn't
currently the final state: currently the final state:
* The current program counter \\(c\\) must be valid. That is, it must be an element of \\(v\\). * The current program counter \(c\) must be valid. That is, it must be an element of \(v\).
* This program counter must correspond to an instruction \\(i\\) in \\(p\\), which we write as \\(p[c] = i\\). * This program counter must correspond to an instruction \(i\) in \(p\), which we write as \(p[c] = i\).
* This instruction must be executed, changing our program counter from \\(c\\) to \\(c'\\) and our * This instruction must be executed, changing our program counter from \(c\) to \(c'\) and our
accumulator from \\(a\\) to \\(a'\\). The set of valid instructions will no longer include \\(c\\), accumulator from \(a\) to \(a'\). The set of valid instructions will no longer include \(c\),
and will become \\(v - \\{c\\}\\). and will become \(v - \{c\}\).
* Our program must then finish executing, starting at state * Our program must then finish executing, starting at state
\\((c', a', v - \\{c\\})\\), and ending in some (unknown) state \\((c'', a'', v'')\\). \((c', a', v - \{c\})\), and ending in some (unknown) state \((c'', a'', v'')\).
If all of these conditions are met, our program, starting at \\((c, a, v)\\), will terminate in the state \\((c'', a'', v'')\\). This third rule completes our semantics; a program being executed will keep running instructions using the third rule, until it finally If all of these conditions are met, our program, starting at \((c, a, v)\), will terminate in the state \((c'', a'', v'')\). This third rule completes our semantics; a program being executed will keep running instructions using the third rule, until it finally
hits an invalid program counter (terminating with the first rule) or gets to the end of the program (terminating with the second rule). hits an invalid program counter (terminating with the first rule) or gets to the end of the program (terminating with the second rule).
#### Aside: Vectors and Finite \\(\mathbb{N}\\) #### Aside: Vectors and Finite \\(\\mathbb{N}\\)
We'll be getting to the Coq implementation of our semantics soon, but before we do: We'll be getting to the Coq implementation of our semantics soon, but before we do:
what type should \\(c\\) be? It's entirely possible for an instruction like \\(\\texttt{jmp} \\; -10000\\) what type should \(c\) be? It's entirely possible for an instruction like \(\texttt{jmp} \; -10000\)
to throw our program counter way before the first instruction of our program, so at first, it seems to throw our program counter way before the first instruction of our program, so at first, it seems
as though we should use an integer. But the prompt doesn't even specify what should happen in this as though we should use an integer. But the prompt doesn't even specify what should happen in this
case - it only says an instruction shouldn't be run twice. The "valid set", although it may help resolve case - it only says an instruction shouldn't be run twice. The "valid set", although it may help resolve
@ -302,7 +302,7 @@ this debate, is our invention, and isn't part of the original specification.
There is, however, something we can infer from this problem. Since the problem of jumping "too far behind" or There is, however, something we can infer from this problem. Since the problem of jumping "too far behind" or
"too far ahead" is never mentioned, we can assume that _all jumps will lead either to an instruction, "too far ahead" is never mentioned, we can assume that _all jumps will lead either to an instruction,
or right to the end of a program_. This means that \\(c\\) is a natural number, with or right to the end of a program_. This means that \(c\) is a natural number, with
{{< latex >}} {{< latex >}}
0 \leq c \leq \text{length}(p) 0 \leq c \leq \text{length}(p)
@ -322,9 +322,9 @@ inference rules, let's present two rules that define such a number:
{{< /latex >}} {{< /latex >}}
This is a variation of the [Peano encoding](https://wiki.haskell.org/Peano_numbers) of natural numbers. This is a variation of the [Peano encoding](https://wiki.haskell.org/Peano_numbers) of natural numbers.
It reads as follows: zero (\\(Z\\)) is a finite natural number less than any positive natural number \\(n\\). Then, if a finite natural number It reads as follows: zero (\(Z\)) is a finite natural number less than any positive natural number \(n\). Then, if a finite natural number
\\(f\\) is less than \\(n\\), then adding one to that number (using the successor function \\(S\\)) \(f\) is less than \(n\), then adding one to that number (using the successor function \(S\))
will create a natural number less than \\(n+1\\). We encode this in Coq as follows will create a natural number less than \(n+1\). We encode this in Coq as follows
([originally from here](https://coq.inria.fr/library/Coq.Vectors.Fin.html#t)): ([originally from here](https://coq.inria.fr/library/Coq.Vectors.Fin.html#t)):
```Coq ```Coq
@ -333,9 +333,9 @@ Inductive t : nat -> Set :=
| FS : forall {n}, t n -> t (S n). | FS : forall {n}, t n -> t (S n).
``` ```
The `F1` constructor here is equivalent to our \\(Z\\), and `FS` is equivalent to our \\(S\\). The `F1` constructor here is equivalent to our \(Z\), and `FS` is equivalent to our \(S\).
To represent positive natural numbers \\(\\mathbb{N}^+\\), we simply take a regular natural To represent positive natural numbers \(\mathbb{N}^+\), we simply take a regular natural
number from \\(\mathbb{N}\\) and find its successor using `S` (simply adding 1). Again, we have number from \(\mathbb{N}\) and find its successor using `S` (simply adding 1). Again, we have
to explicitly use `forall` in our type signatures. to explicitly use `forall` in our type signatures.
We can use a similar technique to represent a list with a known number of elements, known We can use a similar technique to represent a list with a known number of elements, known
@ -352,9 +352,9 @@ a vector:
{(x::\textit{xs}) : \text{Vec} \; t \; (n+1)} {(x::\textit{xs}) : \text{Vec} \; t \; (n+1)}
{{< /latex >}} {{< /latex >}}
These rules read: the empty list \\([]\\) is zero-length vector of any type \\(t\\). Then, These rules read: the empty list \([]\) is zero-length vector of any type \(t\). Then,
if we take an element \\(x\\) of type \\(t\\), and an \\(n\\)-long vector \\(\textit{xs}\\) of \\(t\\), if we take an element \(x\) of type \(t\), and an \(n\)-long vector \(\textit{xs}\) of \(t\),
then we can prepend \\(x\\) to \\(\textit{xs}\\) and get an \\((n+1)\\)-long vector of \\(t\\). then we can prepend \(x\) to \(\textit{xs}\) and get an \((n+1)\)-long vector of \(t\).
In Coq, we write this as follows ([originally from here](https://coq.inria.fr/library/Coq.Vectors.VectorDef.html#t)): In Coq, we write this as follows ([originally from here](https://coq.inria.fr/library/Coq.Vectors.VectorDef.html#t)):
```Coq ```Coq
@ -363,32 +363,32 @@ Inductive t A : nat -> Type :=
| cons : forall (h:A) (n:nat), t A n -> t A (S n). | cons : forall (h:A) (n:nat), t A n -> t A (S n).
``` ```
The `nil` constructor represents the empty list \\([]\\), and `cons` represents The `nil` constructor represents the empty list \([]\), and `cons` represents
the operation of prepending an element (called `h` in the code and \\(x\\) in our inference rules) the operation of prepending an element (called `h` in the code and \(x\) in our inference rules)
to another vector of length \\(n\\), which remains unnamed in the code but is called \\(\\textit{xs}\\) in our rules. to another vector of length \(n\), which remains unnamed in the code but is called \(\textit{xs}\) in our rules.
These two definitions work together quite well. For instance, suppose we have a vector of length \\(n\\). These two definitions work together quite well. For instance, suppose we have a vector of length \(n\).
If we were to access its elements by indices starting at 0, we'd be allowed to access indices 0 through \\(n-1\\). If we were to access its elements by indices starting at 0, we'd be allowed to access indices 0 through \(n-1\).
These are precisely the values of the finite natural numbers less than \\(n\\), \\(\\text{Fin} \\; n \\). These are precisely the values of the finite natural numbers less than \(n\), \(\text{Fin} \; n \).
Thus, given such an index \\(\\text{Fin} \\; n\\) and a vector \\(\\text{Vec} \\; t \\; n\\), we are guaranteed Thus, given such an index \(\text{Fin} \; n\) and a vector \(\text{Vec} \; t \; n\), we are guaranteed
to be able to retrieve the element at the given index! In our code, we will not have to worry about bounds checking. to be able to retrieve the element at the given index! In our code, we will not have to worry about bounds checking.
Of course, if our program has \\(n\\) elements, our program counter will be a finite number less than \\(n+1\\), Of course, if our program has \(n\) elements, our program counter will be a finite number less than \(n+1\),
since there's always the possibility of it pointing past the instructions, indicating that we've finished since there's always the possibility of it pointing past the instructions, indicating that we've finished
running the program. This leads to some minor complications: we can't safely access the program instruction running the program. This leads to some minor complications: we can't safely access the program instruction
at index \\(\\text{Fin} \\; (n+1)\\). We can solve this problem by considering two cases: at index \(\text{Fin} \; (n+1)\). We can solve this problem by considering two cases:
either our index points one past the end of the program (in which case its value is exactly the finite either our index points one past the end of the program (in which case its value is exactly the finite
representation of \\(n\\)), or it's less than \\(n\\), in which case we can "tighten" the upper bound, representation of \(n\)), or it's less than \(n\), in which case we can "tighten" the upper bound,
and convert that index into a \\(\\text{Fin} \\; n\\). We formalize it in a lemma: and convert that index into a \(\text{Fin} \; n\). We formalize it in a lemma:
{{< codelines "Coq" "aoc-2020/day8.v" 80 82 >}} {{< codelines "Coq" "aoc-2020/day8.v" 80 82 >}}
There's a little bit of a gotcha here. Instead of translating our above statement literally, There's a little bit of a gotcha here. Instead of translating our above statement literally,
and returning a value that's the result of "tightening" our input `f`, we return a value and returning a value that's the result of "tightening" our input `f`, we return a value
`f'` that can be "weakened" to `f`. This is because "tightening" is not a total function - `f'` that can be "weakened" to `f`. This is because "tightening" is not a total function -
it's not always possible to convert a \\(\\text{Fin} \\; (n+1)\\) into a \\(\\text{Fin} \\; n\\). it's not always possible to convert a \(\text{Fin} \; (n+1)\) into a \(\text{Fin} \; n\).
However, "weakening" \\(\\text{Fin} \\; n\\) _is_ a total function, since a number less than \\(n\\) However, "weakening" \(\text{Fin} \; n\) _is_ a total function, since a number less than \(n\)
is, by the transitive property of a total order, also less than \\(n+1\\). is, by the transitive property of a total order, also less than \(n+1\).
The Coq proof for this claim is as follows: The Coq proof for this claim is as follows:
@ -409,11 +409,11 @@ we assume is nonzero, since there isn't a natural number less than zero).
can itself be tightened. can itself be tightened.
* If it can't be tightened, then our smaller number is a finite representation of * If it can't be tightened, then our smaller number is a finite representation of
`n-1`. This, in turn, means that adding one to it will be the finite representation `n-1`. This, in turn, means that adding one to it will be the finite representation
of `n` (if \\(x\\) is equal to \\(n-1\\), then \\(x+1\\) is equal to \\(n\\)). of `n` (if \(x\) is equal to \(n-1\), then \(x+1\) is equal to \(n\)).
* If it _can_ be tightened, then so can the successor (if \\(x\\) is less * If it _can_ be tightened, then so can the successor (if \(x\) is less
than \\(n-1\\), then \\(x+1\\) is less than \\(n\\)). than \(n-1\), then \(x+1\) is less than \(n\)).
Next, let's talk about addition, specifically the kind of addition done by the \\(\\texttt{jmp}\\) instruction. Next, let's talk about addition, specifically the kind of addition done by the \(\texttt{jmp}\) instruction.
We can always add an integer to a natural number, but we can at best guarantee that the result We can always add an integer to a natural number, but we can at best guarantee that the result
will be an integer. For instance, we can add `-1000` to `1`, and get `-999`, which is _not_ a natural will be an integer. For instance, we can add `-1000` to `1`, and get `-999`, which is _not_ a natural
number. We implement this kind of addition in a function called `jump_t`: number. We implement this kind of addition in a function called `jump_t`:
@ -436,7 +436,7 @@ Now, suppose we wanted to write a function that _does_ return a valid program
counter after adding the offset to it. Since it's possible for this function to fail counter after adding the offset to it. Since it's possible for this function to fail
(for instance, if the offset is very negative), it has to return `option (fin (S n))`. (for instance, if the offset is very negative), it has to return `option (fin (S n))`.
That is, this function may either fail (returning `None`) or succeed, returning That is, this function may either fail (returning `None`) or succeed, returning
`Some f`, where `f` is of type `fin (S n)`, aka \\(\\text{Fin} \\; (n + 1)\\). Here's `Some f`, where `f` is of type `fin (S n)`, aka \(\text{Fin} \; (n + 1)\). Here's
the function in Coq (again, don't worry too much about the definition): the function in Coq (again, don't worry too much about the definition):
{{< codelines "Coq" "aoc-2020/day8.v" 61 61 >}} {{< codelines "Coq" "aoc-2020/day8.v" 61 61 >}}
@ -464,7 +464,7 @@ The star `*` is used here to represent a [product type](https://en.wikipedia.org
rather than arithmetic multiplication. Our state type accepts an argument, rather than arithmetic multiplication. Our state type accepts an argument,
`n`, much like a finite natural number or a vector. In fact, this `n` is passed on `n`, much like a finite natural number or a vector. In fact, this `n` is passed on
to the state's program counter and set types. Rightly, a state for a program to the state's program counter and set types. Rightly, a state for a program
of length \\(n\\) will not be of the same type as a state for a program of length \\(n+1\\). of length \(n\) will not be of the same type as a state for a program of length \(n+1\).
An instruction is also a tuple, but this time containing only two elements: the opcode and An instruction is also a tuple, but this time containing only two elements: the opcode and
the number. We write this as follows: the number. We write this as follows:
@ -479,11 +479,11 @@ definition:
{{< codelines "Coq" "aoc-2020/day8.v" 38 38 >}} {{< codelines "Coq" "aoc-2020/day8.v" 38 38 >}}
So far, so good! Finally, it's time to get started on the semantics themselves. So far, so good! Finally, it's time to get started on the semantics themselves.
We begin with the inductive definition of \\((\\rightarrow_i)\\). We begin with the inductive definition of \((\rightarrow_i)\).
I think this is fairly straightforward. However, we do use I think this is fairly straightforward. However, we do use
`t` instead of \\(n\\) from the rules, and we use `FS` `t` instead of \(n\) from the rules, and we use `FS`
instead of \\(+1\\). Also, we make the formerly implicit instead of \(+1\). Also, we make the formerly implicit
assumption that \\(c+n\\) is valid explicit, by assumption that \(c+n\) is valid explicit, by
providing a proof that `valid_jump_t pc t = Some pc'`. providing a proof that `valid_jump_t pc t = Some pc'`.
{{< codelines "Coq" "aoc-2020/day8.v" 103 110 >}} {{< codelines "Coq" "aoc-2020/day8.v" 103 110 >}}
@ -507,8 +507,8 @@ counter will be equal to the length of the program `n`,
so we use `nat_to_fin n`. On the other hand, if the program so we use `nat_to_fin n`. On the other hand, if the program
terminates in as stuck state, it must be that it terminated terminates in as stuck state, it must be that it terminated
at a program counter that points to an instruction. Thus, this at a program counter that points to an instruction. Thus, this
program counter is actually a \\(\\text{Fin} \\; n\\), and not program counter is actually a \(\text{Fin} \; n\), and not
a \\(\\text{Fin} \\ (n+1)\\), and is not in the set of allowed program counters. a \(\text{Fin} \ (n+1)\), and is not in the set of allowed program counters.
We use the same "weakening" trick we saw earlier to represent We use the same "weakening" trick we saw earlier to represent
this. this.
@ -518,8 +518,8 @@ Finally, we encode the three inference rules we came up with:
Notice that we fused two of the premises in the last rule. Notice that we fused two of the premises in the last rule.
Instead of naming the instruction at the current program Instead of naming the instruction at the current program
counter (by writing \\(p[c] = i\\)) and using it in another premise, we simply use counter (by writing \(p[c] = i\)) and using it in another premise, we simply use
`nth inp pc`, which corresponds to \\(p[c]\\) in our `nth inp pc`, which corresponds to \(p[c]\) in our
"paper" semantics. "paper" semantics.
Before we go on writing some actual proofs, we have Before we go on writing some actual proofs, we have
@ -532,12 +532,12 @@ start off, we'll define the notion of a "valid instruction", which is guaranteed
to keep the program counter in the correct range. to keep the program counter in the correct range.
There are a couple of ways to do this, but we'll use yet another definition based There are a couple of ways to do this, but we'll use yet another definition based
on inference rules. First, though, observe that the same instruction may be valid on inference rules. First, though, observe that the same instruction may be valid
for one program, and invalid for another. For instance, \\(\\texttt{jmp} \\; 100\\) for one program, and invalid for another. For instance, \(\texttt{jmp} \; 100\)
is perfectly valid for a program with thousands of instructions, but if it occurs is perfectly valid for a program with thousands of instructions, but if it occurs
in a program with only 3 instructions, it will certainly lead to disaster. Specifically, in a program with only 3 instructions, it will certainly lead to disaster. Specifically,
the validity of an instruction depends on the length of the program in which it resides, the validity of an instruction depends on the length of the program in which it resides,
and the program counter at which it's encountered. and the program counter at which it's encountered.
Thus, we refine our idea of validity to "being valid for a program of length \\(n\\) at program counter \\(f\\)". Thus, we refine our idea of validity to "being valid for a program of length \(n\) at program counter \(f\)".
For this, we can use the following two inference rules: For this, we can use the following two inference rules:
{{< latex >}} {{< latex >}}
@ -550,14 +550,14 @@ For this, we can use the following two inference rules:
{o \; t \; \text{valid for} \; n, c } {o \; t \; \text{valid for} \; n, c }
{{< /latex >}} {{< /latex >}}
The first rule states that if a program has length \\(n\\), then \\(\\texttt{add}\\) is valid The first rule states that if a program has length \(n\), then \(\texttt{add}\) is valid
at any program counter whose value is less than \\(n\\). This is because running at any program counter whose value is less than \(n\). This is because running
\\(\\texttt{add}\\) will increment the program counter \\(c\\) by 1, \(\texttt{add}\) will increment the program counter \(c\) by 1,
and thus, create a new program counter that's less than \\(n+1\\), and thus, create a new program counter that's less than \(n+1\),
which, as we discussed above, is perfectly valid. which, as we discussed above, is perfectly valid.
The second rule works for the other two instructions. It has an extra premise: The second rule works for the other two instructions. It has an extra premise:
the result of `jump_valid_t` (written as \\(J_v\\)) has to be \\(\\text{Some} \\; c'\\), the result of `jump_valid_t` (written as \(J_v\)) has to be \(\text{Some} \; c'\),
that is, `jump_valid_t` must succeed. Note that we require this even for no-ops, that is, `jump_valid_t` must succeed. Note that we require this even for no-ops,
since it later turns out that one of the them may be a jump after all. since it later turns out that one of the them may be a jump after all.
@ -568,26 +568,26 @@ We encode the rules in Coq as follows:
{{< codelines "Coq" "aoc-2020/day8.v" 152 157 >}} {{< codelines "Coq" "aoc-2020/day8.v" 152 157 >}}
Note that we have three rules instead of two. This is because we "unfolded" Note that we have three rules instead of two. This is because we "unfolded"
\\(o\\) from our second rule: rather than using set notation (or "or"), we \(o\) from our second rule: rather than using set notation (or "or"), we
just generated two rules that vary in nothing but the operation involved. just generated two rules that vary in nothing but the operation involved.
Of course, we must have that every instruction in a program is valid. Of course, we must have that every instruction in a program is valid.
We don't really need inference rules for this, as much as a "forall" quantifier. We don't really need inference rules for this, as much as a "forall" quantifier.
A program \\(p\\) of length \\(n\\) is valid if the following holds: A program \(p\) of length \(n\) is valid if the following holds:
{{< latex >}} {{< latex >}}
\forall (c : \text{Fin} \; n). p[c] \; \text{valid for} \; n, c \forall (c : \text{Fin} \; n). p[c] \; \text{valid for} \; n, c
{{< /latex >}} {{< /latex >}}
That is, for every possible in-bounds program counter \\(c\\), That is, for every possible in-bounds program counter \(c\),
the instruction at the program counter is valid. We can now the instruction at the program counter is valid. We can now
encode this in Coq, too: encode this in Coq, too:
{{< codelines "Coq" "aoc-2020/day8.v" 160 161 >}} {{< codelines "Coq" "aoc-2020/day8.v" 160 161 >}}
In the above, `n` is made implicit where possible. In the above, `n` is made implicit where possible.
Since \\(c\\) (called `pc` in the code) is of type \\(\\text{Fin} \\; n\\), there's no Since \(c\) (called `pc` in the code) is of type \(\text{Fin} \; n\), there's no
need to write \\(n\\) _again_. The curly braces tell Coq to infer that need to write \(n\) _again_. The curly braces tell Coq to infer that
argument where possible. argument where possible.
### Proving Termination ### Proving Termination
@ -613,7 +613,7 @@ The first proof is rather simple. The claim is:
> For our valid program, at any program counter `pc` > For our valid program, at any program counter `pc`
and accumulator `acc`, there must exist another program and accumulator `acc`, there must exist another program
counter `pc'` and accumulator `acc'` such that the counter `pc'` and accumulator `acc'` such that the
instruction evaluation relation \\((\rightarrow_i)\\) instruction evaluation relation \((\rightarrow_i)\)
connects the two. That is, valid addresses aside, connects the two. That is, valid addresses aside,
we can always make a step. we can always make a step.
@ -676,14 +676,14 @@ case analysis on `o`.
There are three possible cases we have to consider, There are three possible cases we have to consider,
one for each type of instruction. one for each type of instruction.
* If the instruction is \\(\\texttt{add}\\), we know * If the instruction is \(\texttt{add}\), we know
that `pc' = pc + 1` and `acc' = acc + t0`. That is, that `pc' = pc + 1` and `acc' = acc + t0`. That is,
the program counter is simply incremented, and the accumulator the program counter is simply incremented, and the accumulator
is modified with the number part of the instruction. is modified with the number part of the instruction.
* If the instruction is \\(\\texttt{nop}\\), the program * If the instruction is \(\texttt{nop}\), the program
coutner will again be incremented (`pc' = pc + 1`), coutner will again be incremented (`pc' = pc + 1`),
but the accumulator will stay the same, so `acc' = acc`. but the accumulator will stay the same, so `acc' = acc`.
* If the instruction is \\(\\texttt{jmp}\\), things are * If the instruction is \(\texttt{jmp}\), things are
more complicated. We must rely on the assumption more complicated. We must rely on the assumption
that our input is valid, which tells us that adding that our input is valid, which tells us that adding
`t0` to our `pc` will result in `Some f`, and not `None`. `t0` to our `pc` will result in `Some f`, and not `None`.
@ -737,7 +737,7 @@ counter that is not included in the valid set.
to a "next" state. to a "next" state.
Alternatively, we could say that one of the inference rules Alternatively, we could say that one of the inference rules
for \\((\\Rightarrow_p)\\) must apply. This is not the case if the input for \((\Rightarrow_p)\) must apply. This is not the case if the input
is not valid, since, as I said is not valid, since, as I said
before, an arbitrary input program can lead us to jump before, an arbitrary input program can lead us to jump
to a negative address (or to an address _way_ past the end of the program). to a negative address (or to an address _way_ past the end of the program).