The Foundations of Dawn article came up on Lobsters recently. In this article, the author of Dawn defines a core calculus for the language, and provides its semantics. The core calculus is called the untyped concatenative calculus, or UCC. The definitions in the semantics seemed so clean and straightforward that I wanted to try my hand at translating them into machine-checked code. I am most familiar with Coq, and that’s what I reached for when making this attempt.

Defining the Syntax

Expressions and Intrinsics

This is mostly the easy part. A UCC expression is one of three things:

This is straightforward to define in Coq, but I’m going to make a little simplifying change. Instead of making “composition of nn expressions” a core language feature, I’ll only allow “composition of e1e_1 and e2e_2”, written e1 e2e_1\ e_2. This change does not in any way reduce the power of the language; we can still [note: The same expression can, of course, be written as e1  (en1 en)e_1\ \ldots\ (e_{n-1}\ e_n). So, which way should we really use when translating the many-expression composition from the Dawn article into the two-expression composition I am using here? Well, the answer is, it doesn't matter; expression composition is associative, so both ways effectively mean the same thing.

This is quite similar to what we do in algebra: the regular old addition operator, ++ is formally only defined for pairs of numbers, like a+ba+b. However, no one really bats an eye when we write 1+2+31+2+3, because we can just insert parentheses any way we like, and get the same result: (1+2)+3(1+2)+3 is the same as 1+(2+3)1+(2+3). ]
With that in mind, we can translate each of the three types of expressions in UCC into cases of an inductive data type in Coq.

From Dawn.v, lines 12 through 15
12
13
14
15
Inductive expr :=
  | e_int (i : intrinsic)
  | e_quote (e : expr)
  | e_comp (e1 e2 : expr).

Why do we need e_int? We do because a token like swap\text{swap} can be viewed as belonging to the set of intrinsics ii, or the set of expressions, ee. While writing down the rules in mathematical notation, what exactly the token means is inferred from context - clearly swap drop\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, 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).

The definition for intrinsics themselves is even simpler:

From Dawn.v, lines 4 through 10
 4
 5
 6
 7
 8
 9
10
Inductive intrinsic :=
  | swap
  | clone
  | drop
  | quote
  | compose
  | apply.

We simply define a constructor for each of the six intrinsics. Since none of the intrinsic names are reserved in Coq, we can just call our constructors exactly the same as their names in the written formalization.

Values and Value Stacks

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:

Inductive value :=
    | v_quot (e : expr).

Then, v_quot (e_int swap) would be the Coq translation of the expression [swap][\text{swap}]. However, I didn’t decide on this approach for two reasons:

I took instead the approach from Programming Language Foundations: a value is merely an expression for which some predicate, IsValue, holds. We will define this such that IsValue (e_quote e) is provable, but also such that here is no way to prove IsValue (e_int swap), since that expression is not a value. But what does “provable” mean, here?

By the Curry-Howard correspondence, a predicate is just a function that takes something and returns a type. Thus, if Even\text{Even} is a predicate, then Even 3\text{Even}\ 3 is actually a type. Since Even\text{Even} takes numbers in, it is a predicate on numbers. Our IsValue\text{IsValue} predicate will be a predicate on expressions, instead. In Coq, we can write this as:

From Dawn.v, line 19
19
Inductive IsValue : expr -> Prop :=

You might be thinking,

Huh, Prop? But you just said that predicates return types!

This is a good observation; In Coq, Prop is a special sort of type that corresponds to logical propositions. It’s special for a few reasons, but those reasons are beyond the scope of this post; for our purposes, it’s sufficient to think of IsValue e as a type.

Alright, so what good is this new IsValue e type? Well, we will define IsValue such that this type is only inhabited if e is a value according to the UCC specification. A type is inhabited if and only if we can find a value of that type. For instance, the type of natural numbers, nat, is inhabited, because any number, like 0, has this type. Uninhabited types are harder to come by, but take as an example the type 3 = 4, the type of proofs that three is equal to four. Three is not equal to four, so we can never find a proof of equality, and thus, 3 = 4 is uninhabited. As I said, IsValue e will only be inhabited if e is a value per the formal specification of UCC; specifically, this means that e is a quoted expression, like e_quote e'.

To this end, we define IsValue as follows:

From Dawn.v, lines 19 through 20
19
20
Inductive IsValue : expr -> Prop :=
  | Val_quote : forall {e : expr}, IsValue (e_quote e).

Now, IsValue is a new data type with only only constructor, ValQuote. For any expression e, this constructor creates a value of type IsValue (e_quote e). Two things are true here:

Thus, IsValue e is inhabited if and only if e is a UCC value, as we intended.

Just one more thing. A value is just an expression, but Coq only knows about this as long as there’s an IsValue instance around to vouch for it. To be able to reason about values, then, we will need both the expression and its IsValue proof. Thus, we define the type value to mean a pair of two things: an expression v and a proof that it’s a value, IsValue v:

From Dawn.v, line 22
22
Definition value := { v : expr & IsValue v }.

A value stack is just a list of values:

From Dawn.v, line 23
23
Definition value_stack := list value.

Semantics

Remember our IsValue predicate? Well, it’s not just any predicate, it’s a unary predicate. Unary means that it’s a predicate that only takes one argument, an expression in our case. However, this is far from the only type of predicate. Here are some examples:

Binary predicates are just functions of two inputs that return types. For instance, here’s what Coq has to say about the type of eq:

eq : ?A -> ?A -> Prop

By a similar logic, ternary predicates, much like UCC’s evaluation relation, are functions of three inputs. We can thus write the type of our evaluation relation as follows:

From Dawn.v, line 35
35
with Sem_expr : value_stack -> expr -> value_stack -> Prop :=

We define the constructors just like we did in our IsValue predicate. For each evaluation rule in UCC, such as:

V,v,v swap  V,v,v \langle V, v, v'\rangle\ \text{swap}\ \rightarrow\ \langle V, v', v \rangle

We introduce a constructor. For the swap rule mentioned above, the constructor looks like this:

From Dawn.v, line 28
28
  | Sem_swap : forall (v v' : value) (vs : value_stack), Sem_int (v' :: v :: vs) swap (v :: v' :: vs)

Although the stacks are written in reverse order (which is just a consequence of Coq’s list notation), I hope that the correspondence is fairly clear. If it’s not, try reading this rule out loud:

The rule Sem_swap says that for every two values v and v', and for any stack vs, evaluating swap in the original stack v' :: v :: vs, aka V,v,v\langle V, v, v'\rangle, results in a final stack v :: v' :: vs, aka V,v,v\langle V, v', v\rangle.

With that in mind, here’s a definition of a predicate Sem_int, the evaluation predicate for intrinsics:

From Dawn.v, lines 27 through 33
27
28
29
30
31
32
33
Inductive Sem_int : value_stack -> intrinsic -> value_stack -> Prop :=
  | Sem_swap : forall (v v' : value) (vs : value_stack), Sem_int (v' :: v :: vs) swap (v :: v' :: vs)
  | Sem_clone : forall (v : value) (vs : value_stack), Sem_int (v :: vs) clone (v :: v :: vs)
  | Sem_drop : forall (v : value) (vs : value_stack), Sem_int (v :: vs) drop vs
  | Sem_quote : forall (v : value) (vs : value_stack), Sem_int (v :: vs) quote ((v_quote (projT1 v)) :: vs)
  | Sem_compose : forall (e e' : expr) (vs : value_stack), Sem_int (v_quote e' :: v_quote e :: vs) compose (v_quote (e_comp e e') :: vs)
  | Sem_apply : forall (e : expr) (vs vs': value_stack), Sem_expr vs e vs' -> Sem_int (v_quote e :: vs) apply vs'

Hey, what’s all this with v_quote and projT1? It’s just a little bit of bookkeeping. Given a value – a pair of an expression e and a proof IsValue e – the function projT1 just returns the expression e. That is, it’s basically a way of converting a value back into an expression. The function v_quote takes us in the other direction: given an expression ee, it constructs a quoted expression [e][e], and combines it with a proof that the newly constructed quote is a value.

The above two function in combination help us define the quote intrinsic, which wraps a value on the stack in an additional layer of quotes. When we create a new quote, we need to push it onto the value stack, so it needs to be a value; we thus use v_quote. However, v_quote needs an expression to wrap in a quote, so we use projT1 to extract the expression from the value on top of the stack.

In addition to intrinsics, we also define the evaluation relation for actual expressions.

From Dawn.v, lines 35 through 39
35
36
37
38
39
with Sem_expr : value_stack -> expr -> value_stack -> Prop :=
  | Sem_e_int : forall (i : intrinsic) (vs vs' : value_stack), Sem_int vs i vs' -> Sem_expr vs (e_int i) vs'
  | Sem_e_quote : forall (e : expr) (vs : value_stack), Sem_expr vs (e_quote e) (v_quote e :: vs)
  | Sem_e_comp : forall (e1 e2 : expr) (vs1 vs2 vs3 : value_stack),
      Sem_expr vs1 e1 vs2 -> Sem_expr vs2 e2 vs3 -> Sem_expr vs1 (e_comp e1 e2) vs3.

Here, we may as well go through the three constructors to explain what they mean:

true\text{true}, false\text{false}, or\text{or} and Proofs

Now it’s time for some fun! The UCC language specification starts by defining two values: true and false. Why don’t we do the same thing?

UCC Spec Coq encoding
false\text{false}=[drop][\text{drop}]
From Dawn.v, lines 41 through 42
41
42
Definition false : expr := e_quote (e_int drop).
Definition false_v : value := v_quote (e_int drop).
true\text{true}=[swap drop][\text{swap} \ \text{drop}]
From Dawn.v, lines 44 through 45
44
45
Definition true : expr := e_quote (e_comp (e_int swap) (e_int drop)).
Definition true_v : value := v_quote (e_comp (e_int swap) (e_int drop)).

Let’s try prove that these two work as intended.

From Dawn.v, lines 47 through 53
47
48
49
50
51
52
53
Theorem false_correct : forall (v v' : value) (vs : value_stack), Sem_expr (v' :: v :: vs) (e_comp false (e_int apply)) (v :: vs).
Proof.
  intros v v' vs.
  eapply Sem_e_comp.
  - apply Sem_e_quote.
  - apply Sem_e_int. apply Sem_apply. apply Sem_e_int. apply Sem_drop.
Qed.

This is the first real proof in this article. Rather than getting into the technical details, I invite you to take a look at the “shape” of the proof:

Following these steps, we arrive at the fact that evaluating false on the stack simply drops the top element, as specified. The proof for true\text{true} is very similar in spirit:

From Dawn.v, lines 55 through 63
55
56
57
58
59
60
61
62
63
Theorem true_correct : forall (v v' : value) (vs : value_stack), Sem_expr (v' :: v :: vs) (e_comp true (e_int apply)) (v' :: vs).
Proof.
  intros v v' vs.
  eapply Sem_e_comp.
  - apply Sem_e_quote.
  - apply Sem_e_int. apply Sem_apply. eapply Sem_e_comp.
    * apply Sem_e_int. apply Sem_swap.
    * apply Sem_e_int. apply Sem_drop.
Qed.

We can also formalize the or\text{or} operator:

UCC Spec Coq encoding
or\text{or}=clone apply\text{clone}\ \text{apply}
From Dawn.v, line 65
65
Definition or : expr := e_comp (e_int clone) (e_int apply).

We can write two top-level proofs about how this works: the first says that or\text{or}, when the first argument is false\text{false}, just returns the second argument (this is in agreement with the truth table, since false\text{false} is the identity element of or\text{or}). The proof proceeds much like before:

From Dawn.v, lines 67 through 73
67
68
69
70
71
72
73
Theorem or_false_v : forall (v : value) (vs : value_stack), Sem_expr (false_v :: v :: vs) or (v :: vs).
Proof with apply Sem_e_int.
  intros v vs.
  eapply Sem_e_comp...
  - apply Sem_clone.
  - apply Sem_apply... apply Sem_drop.
Qed.

To shorten the proof a little bit, I used the Proof with construct from Coq, which runs an additional tactic (like apply) whenever ... is used. Because of this, in this proof writing apply Sem_apply... is the same as apply Sem_apply. apply Sem_e_int. Since the Sem_e_int rule is used a lot, this makes for a very convenient shorthand.

Similarly, we prove that or\text{or} applied to true\text{true} always returns true\text{true}.

From Dawn.v, lines 75 through 83
75
76
77
78
79
80
81
82
83
Theorem or_true : forall (v : value) (vs : value_stack), Sem_expr (true_v :: v :: vs) or (true_v :: vs).
Proof with apply Sem_e_int.
  intros v vs.
  eapply Sem_e_comp...
  - apply Sem_clone...
  - apply Sem_apply. eapply Sem_e_comp...
    * apply Sem_swap.
    * apply Sem_drop.
Qed.

Finally, the specific facts (like false or false\text{false}\ \text{or}\ \text{false} evaluating to false\text{false}) can be expressed using our two new proofs, or_false_v and or_true.

From Dawn.v, lines 85 through 88
85
86
87
88
Definition or_false_false := or_false_v false_v.
Definition or_false_true := or_false_v true_v.
Definition or_true_false := or_true false_v.
Definition or_true_true := or_true true_v.

Derived Expressions

Quotes

The UCC specification defines quoten\text{quote}_n to make it more convenient to quote multiple terms. For example, quote2\text{quote}_2 composes and quotes the first two values on the stack. This is defined in terms of other UCC expressions as follows:

quoten=quoten1 swap quote swap compose \text{quote}_n = \text{quote}_{n-1}\ \text{swap}\ \text{quote}\ \text{swap}\ \text{compose}

We can write this in Coq as follows:

From Dawn.v, lines 90 through 94
90
91
92
93
94
Fixpoint quote_n (n : nat) :=
  match n with
  | O => e_int quote
  | S n' => e_compose (quote_n n') (e_int swap :: e_int quote :: e_int swap :: e_int compose :: nil)
  end.

This definition diverges slightly from the one given in the UCC specification; particularly, UCC’s spec mentions that quoten\text{quote}_n is only defined for n1n \geq 1.However, this means that in our code, we’d have to somehow handle the error that would arise if the term quote0\text{quote}_0 is used. Instead, I defined quote_n n to simply mean quoten+1\text{quote}_{n+1}; thus, in Coq, no matter what n we use, we will have a valid expression, since quote_n 0 will simply correspond to quote1=quote\text{quote}_1 = \text{quote}.

We can now attempt to prove that this definition is correct by ensuring that the examples given in the specification are valid. We may thus write,

From Dawn.v, lines 96 through 106
 96
 97
 98
 99
100
101
102
103
104
105
106
Theorem quote_2_correct : forall (v1 v2 : value) (vs : value_stack),
    Sem_expr (v2 :: v1 :: vs) (quote_n 1) (v_quote (e_comp (projT1 v1) (projT1 v2)) :: vs).
Proof with apply Sem_e_int.
  intros v1 v2 vs. simpl.
  repeat (eapply Sem_e_comp)...
  - apply Sem_quote.
  - apply Sem_swap.
  - apply Sem_quote.
  - apply Sem_swap.
  - apply Sem_compose.
Qed.

We used a new tactic here, repeat, but overall, the structure of the proof is pretty straightforward: the definition of quote_n consists of many intrinsics, and we apply the corresponding rules one-by-one until we arrive at the final stack. Writing this proof was kind of boring, since I just had to see which intrinsic is being used in each step, and then write a line of apply code to handle that intrinsic. This gets worse for quote3\text{quote}_3:

From Dawn.v, lines 108 through 122
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
Theorem quote_3_correct : forall (v1 v2 v3 : value) (vs : value_stack),
  Sem_expr (v3 :: v2 :: v1 :: vs) (quote_n 2) (v_quote (e_comp (projT1 v1) (e_comp (projT1 v2) (projT1 v3))) :: vs).
Proof with apply Sem_e_int.
  intros v1 v2 v3 vs. simpl.
  repeat (eapply Sem_e_comp)...
  - apply Sem_quote.
  - apply Sem_swap.
  - apply Sem_quote.
  - apply Sem_swap.
  - apply Sem_compose.
  - apply Sem_swap.
  - apply Sem_quote.
  - apply Sem_swap.
  - apply Sem_compose.
Qed.

It’s so long! Instead, I decided to try out Coq’s Ltac2 mechanism to teach Coq how to write proofs like this itself. Here’s what I came up with:

From Dawn.v, lines 124 through 136
124
125
126
127
128
129
130
131
132
133
134
135
136
Ltac2 rec solve_basic () := Control.enter (fun _ =>
  match! goal with
  | [|- Sem_int ?vs1 swap ?vs2] => apply Sem_swap
  | [|- Sem_int ?vs1 clone ?vs2] => apply Sem_clone
  | [|- Sem_int ?vs1 drop ?vs2] => apply Sem_drop
  | [|- Sem_int ?vs1 quote ?vs2] => apply Sem_quote
  | [|- Sem_int ?vs1 compose ?vs2] => apply Sem_compose
  | [|- Sem_int ?vs1 apply ?vs2] => apply Sem_apply
  | [|- Sem_expr ?vs1 (e_comp ?e1 ?e2) ?vs2] => eapply Sem_e_comp; solve_basic ()
  | [|- Sem_expr ?vs1 (e_int ?e) ?vs2] => apply Sem_e_int; solve_basic ()
  | [|- Sem_expr ?vs1 (e_quote ?e) ?vs2] => apply Sem_e_quote
  | [_ : _ |- _] => ()
  end).

You don’t have to understand the details, but in brief, this checks what kind of proof we’re asking Coq to do (for instance, if we’re trying to prove that a swap\text{swap} instruction has a particular effect), and tries to apply a corresponding semantic rule. Thus, it will try Sem_swap if the expression is swap\text{swap}, Sem_clone if the expression is clone\text{clone}, and so on. Then, the two proofs become:

From Dawn.v, lines 138 through 144
138
139
140
141
142
143
144
Theorem quote_2_correct' : forall (v1 v2 : value) (vs : value_stack),
    Sem_expr (v2 :: v1 :: vs) (quote_n 1) (v_quote (e_comp (projT1 v1) (projT1 v2)) :: vs).
Proof. intros. simpl. solve_basic (). Qed.

Theorem quote_3_correct' : forall (v1 v2 v3 : value) (vs : value_stack),
  Sem_expr (v3 :: v2 :: v1 :: vs) (quote_n 2) (v_quote (e_comp (projT1 v1) (e_comp (projT1 v2) (projT1 v3))) :: vs).
Proof. intros. simpl. solve_basic (). Qed.

Rotations

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:

V v=V v \langle V \rangle\ v = \langle V\ v \rangle

Or, in Coq,

From Dawn.v, lines 148 through 149
148
149
Lemma eval_value : forall (v : value) (vs : value_stack),
  Sem_expr vs (projT1 v) (v :: vs).

This is the trick to how rotaten\text{rotate}_n works: it creates a quote of nn reordered and composed values on the stack, and then evaluates that quote. Since evaluating each value just places it on the stack, these values end up back on the stack, in the same order that they were in the quote. When writing the proof, solve_basic () gets us almost all the way to the end (evaluating a list of values against a stack). Then, we simply apply the composition rule over and over, following it up with eval_value to prove that the each value is just being placed back on the stack.

From Dawn.v, lines 156 through 168
156
157
158
159
160
161
162
163
164
165
166
167
168
Theorem rotate_3_correct : forall (v1 v2 v3 : value) (vs : value_stack),
  Sem_expr (v3 :: v2 :: v1 :: vs) (rotate_n 1) (v1 :: v3 :: v2 :: vs).
Proof.
  intros. unfold rotate_n. simpl. solve_basic ().
  repeat (eapply Sem_e_comp); apply eval_value.
Qed.

Theorem rotate_4_correct : forall (v1 v2 v3 v4 : value) (vs : value_stack),
  Sem_expr (v4 :: v3 :: v2 :: v1 :: vs) (rotate_n 2) (v1 :: v4 :: v3 :: v2 :: vs).
Proof.
  intros. unfold rotate_n. simpl. solve_basic ().
  repeat (eapply Sem_e_comp); apply eval_value.
Qed.

e_comp is Associative

When composing three expressions, which way of inserting parentheses is correct? Is it (e1 e2) e3(e_1\ e_2)\ e_3? Or is it e1 (e2 e3)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.

From Dawn.v, lines 170 through 171
170
171
Theorem e_comp_assoc : forall (e1 e2 e3 : expr) (vs vs' : value_stack),
  Sem_expr vs (e_comp e1 (e_comp e2 e3)) vs' <-> Sem_expr vs (e_comp (e_comp e1 e2) e3) vs'.

Conclusion

That’s all I’ve got in me for today. However, we got pretty far! The UCC specification says:

One of my long term goals for UCC is to democratize formal software verification in order to make it much more feasible and realistic to write perfect software.

I think that UCC is definitely getting there: formally defining the semantics outlined on the page was quite straightforward. We can now have complete confidence in the behavior of true\text{true}, false\text{false}, or\text{or}, quoten\text{quote}_n and rotaten\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 a little bit of tweaking to get from the written description of the language to code! I’m looking forward to reading the next post about the multistack concatenative calculus.