Get started on a post about a UCC evaluator

code/dawn/Dawn.v

@@ -131,7 +131,7 @@ Ltac2 rec solve_basic () := Control.enter (fun _ =>
   | [|- 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_e_quote ?vs1 (e_quote ?e) ?vs2] => apply Sem_quote
+  | [|- Sem_expr ?vs1 (e_quote ?e) ?vs2] => apply Sem_e_quote
   | [_ : _ |- _] => ()
   end).
 

code/dawn/DawnEval.v

@@ -1,21 +1,22 @@
 Require Import Coq.Lists.List.
-Require Import Dawn.
+Require Import DawnV2.
 Require Import Coq.Program.Equality.
+From Ltac2 Require Import Ltac2.
 
 Inductive step_result :=
   | err
-  | middle (e : expr) (s : list expr)
-  | final (s : list expr).
+  | middle (e : expr) (s : value_stack)
+  | final (s : value_stack).
 
-Fixpoint eval_step (s : list expr) (e : expr) : step_result :=
+Fixpoint eval_step (s : value_stack) (e : expr) : step_result :=
   match e, s with
   | e_int swap, v' :: v :: vs => final (v :: v' :: vs)
   | e_int clone, v :: vs => final (v :: v :: vs)
   | e_int drop, v :: vs => final vs
-  | e_int quote, v :: vs => final (e_quote v :: vs)
-  | e_int compose, (e_quote v2) :: (e_quote v1) :: vs => final (e_quote (e_comp v1 v2) :: vs)
-  | e_int apply, (e_quote v1) :: vs => middle v1 vs
-  | e_quote e', vs => final (e_quote e' :: vs)
+  | e_int quote, v :: vs => final (v_quote (value_to_expr v) :: vs)
+  | e_int compose, (v_quote v2) :: (v_quote v1) :: vs => final (v_quote (e_comp v1 v2) :: vs)
+  | e_int apply, (v_quote v1) :: vs => middle v1 vs
+  | e_quote e', vs => final (v_quote e' :: vs)
   | e_comp e1 e2, vs =>
       match eval_step vs e1 with
       | final vs' => middle e2 vs'
@@ -25,12 +26,10 @@ Fixpoint eval_step (s : list expr) (e : expr) : step_result :=
   | _, _ => err
   end.
 
-Definition strip_value_list (vs : value_stack) := @map value expr (@projT1 expr IsValue) vs.
-
 Theorem eval_step_correct : forall (e : expr) (vs vs' : value_stack), Sem_expr vs e vs' ->
-  (eval_step (strip_value_list vs) e = final (strip_value_list vs')) \/
+  (eval_step vs e = final vs') \/
   (exists (ei : expr) (vsi : value_stack),
-    eval_step (strip_value_list vs) e = middle ei (strip_value_list vsi) /\
+    eval_step vs e = middle ei vsi /\
     Sem_expr vsi ei vs').
 Proof.
   intros e vs vs' Hsem.
@@ -38,9 +37,9 @@ Proof.
   induction Hsem.
   - inversion H; (* The expression is just an intrnsic. *)
     (* Dismiss all the straightforward "final" cases,
-       of which most intrinsics are *)
+       of which most intrinsics are. *)
     try (left; reflexivity).
-    (* We are in an intermediate / middle case. *)
+    (* Only apply remains; We are in an intermediate / middle case. *)
     right.
     (* The semantics guarantee that the expression in the
        quote evaluates to the final state. *)
@@ -62,26 +61,26 @@ Proof.
       eapply Sem_e_comp. apply Hsem'. apply Hsem2.
 Qed.
 
-Inductive eval_chain (s : list expr) (e : expr) (s' : list expr) : Prop :=
-  | chain_final (P : eval_step s e = final s')
-  | chain_middle (ei : expr) (si : list expr)
-      (P : eval_step s e = middle ei si) (rest : eval_chain si ei s').
+Inductive eval_chain (vs : value_stack) (e : expr) (vs' : value_stack) : Prop :=
+  | chain_final (P : eval_step vs e = final vs')
+  | chain_middle (ei : expr) (vsi : value_stack)
+      (P : eval_step vs e = middle ei vsi) (rest : eval_chain vsi ei vs').
 
-Lemma eval_chain_merge : forall (e1 e2 : expr) (s s' s'' : list expr),
-  eval_chain s e1 s' -> eval_chain s' e2 s'' -> eval_chain s (e_comp e1 e2) s''.
+Lemma eval_chain_merge : forall (e1 e2 : expr) (vs vs' vs'' : value_stack),
+  eval_chain vs e1 vs' -> eval_chain vs' e2 vs'' -> eval_chain vs (e_comp e1 e2) vs''.
 Proof.
-  intros e1 e2 s s' s'' ch1 ch2.
+  intros e1 e2 vs vs' vs'' ch1 ch2.
   induction ch1;
   eapply chain_middle; simpl; try (rewrite P); auto.
 Qed.
 
-Lemma eval_chain_split : forall (e1 e2 : expr) (s s'' : list expr),
-  eval_chain s (e_comp e1 e2) s'' -> exists s', (eval_chain s e1 s') /\ (eval_chain s' e2 s'').
+Lemma eval_chain_split : forall (e1 e2 : expr) (vs vs'' : value_stack),
+  eval_chain vs (e_comp e1 e2) vs'' -> exists vs', (eval_chain vs e1 vs') /\ (eval_chain vs' e2 vs'').
 Proof.
-  intros e1 e2 s ss'' ch.
-  dependent induction ch.
-  - simpl in P. destruct (eval_step s e1); inversion P.
-  - simpl in P. destruct (eval_step s e1) eqn:Hval; try (inversion P).
+  intros e1 e2 vs vss'' ch.
+  ltac1:(dependent induction ch).
+  - simpl in P. destruct (eval_step vs e1); inversion P.
+  - simpl in P. destruct (eval_step vs e1) eqn:Hval; try (inversion P).
     + injection P as Hinj; subst. specialize (IHch e e2 H0) as [s'0 [ch1 ch2]].
       eexists. split.
       * eapply chain_middle. apply Hval. apply ch1.
@@ -91,51 +90,10 @@ Proof.
       * apply ch.
 Qed.
 
-Theorem eval_step_preservation : forall (e : expr) (vs : value_stack) (s' : list expr),
-  ((exists e', eval_step (strip_value_list vs) e = middle e' s') ->
-    exists vs', (strip_value_list vs') = s') /\
-  ((eval_step (strip_value_list vs) e = final s') ->
-    exists vs', (strip_value_list vs') = s').
-Proof.
-  intros e vs. induction e; split.
-  - intros [e' Hst].
-    destruct i; try (destruct vs as [|v1 [|v2 vs]]; inversion Hst; fail).
-    * destruct vs as [|v1 [|v2 vs]]; inversion Hst;
-      destruct (projT1 v1); inversion H0.
-      destruct (projT1 v2); inversion H1.
-    * destruct vs as [|v1 vs]; inversion Hst.
-      destruct (projT1 v1); inversion H0.
-      eauto.
-  - intros Hst.
-    destruct i; try (destruct vs as [|v1 [|v2 vs]]; inversion Hst; fail).
-    * destruct vs as [|v1 [|v2 vs]]; inversion Hst. exists (v2 :: v1 :: vs). reflexivity.
-    * destruct vs as [|v1 vs]; inversion Hst. exists (v1 :: v1 :: vs). reflexivity.
-    * destruct vs as [|v1 vs]; inversion Hst. exists vs. reflexivity.
-    * destruct vs as [|v1 vs]; inversion Hst. exists (v_quote (projT1 v1) :: vs). reflexivity.
-    * destruct vs as [|v1 [|v2 vs]]; inversion Hst.
-      + destruct (projT1 v1); inversion H0.
-      + destruct (projT1 v1); destruct (projT1 v2); inversion H0.
-        exists (v_quote (e_comp e0 e) :: vs). reflexivity.
-    * destruct vs as [|v1 vs]; inversion Hst;
-      destruct (projT1 v1); inversion H0.
-  - intros [e' Hst]. inversion Hst.
-  - intros Hst. inversion Hst. exists (v_quote e :: vs). reflexivity.
-  - intros [e' Hst]. inversion Hst.
-    destruct (eval_step (strip_value_list vs) e1) eqn:Hst1.
-    * inversion H0.
-    * specialize (IHe1 s') as [IHe1 _]. apply IHe1. exists e.
-      injection H0 as Hinj; subst; auto.
-    * specialize (IHe1 s') as [_ IHe1]. apply IHe1. 
-      injection H0 as Hinj; subst; auto.
-  - intros Hst.
-    inversion Hst. destruct (eval_step (strip_value_list vs) e1); inversion H0.
-Qed.
-
-
 Theorem val_step_sem : forall (e : expr) (vs vs' : value_stack),
-  Sem_expr vs e vs' -> eval_chain (strip_value_list vs) e (strip_value_list vs')
+  Sem_expr vs e vs' -> eval_chain vs e vs'
 with eval_step_int : forall (i : intrinsic) (vs vs' : value_stack),
-  Sem_int vs i vs' -> eval_chain (strip_value_list vs) (e_int i) (strip_value_list vs').
+  Sem_int vs i vs' -> eval_chain vs (e_int i) vs'.
 Proof.
   - intros e vs vs' Hsem.
     induction Hsem.
@@ -146,7 +104,7 @@ Proof.
       apply chain_final. auto.
     + (* In compoition, by induction, we know that the two sub-expressions produce
          proper evaluation chains. Chains can be composed (via eval_chain_merge). *)
-      eapply eval_chain_merge with (strip_value_list vs2); auto.
+      eapply eval_chain_merge with vs2; auto.
   - intros i vs vs' Hsem.
     (* The evaluation chain depends on the specific intrinsic in use. *)
     inversion Hsem; subst;
@@ -154,71 +112,112 @@ Proof.
     try (apply chain_final; auto; fail).
     (* Only apply is non-final. The first step is popping the quote from the stack,
        and the rest of the steps are given by the evaluation of the code in the quote. *)
-    apply chain_middle with e (strip_value_list vs0); auto.
+    apply chain_middle with e vs0; auto.
+Qed.
+
+Ltac2 Type exn ::= [ | Not_intrinsic ].
+
+Ltac2 rec destruct_n (n : int) (vs : constr) : unit :=
+  if Int.le n 0 then () else
+    let v := Fresh.in_goal @v in
+    let vs' := Fresh.in_goal @vs in
+    destruct $vs as [|$v $vs']; Control.enter (fun () =>
+      try (destruct_n (Int.sub n 1) (Control.hyp vs'))
+    ).
+
+Ltac2 int_arity (int : constr) : int :=
+  match! int with
+  | swap => 2
+  | clone => 1
+  | drop => 1
+  | quote => 1
+  | compose => 2
+  | apply => 1
+  | _ => Control.throw Not_intrinsic
+  end.
+
+Ltac2 destruct_int_stack (int : constr) (va: constr) := destruct_n (int_arity int) va.
+
+Ltac2 ensure_valid_stack () := Control.enter (fun () =>
+  match! goal with
+  | [h : eval_step ?a (e_int ?b) = ?c |- _] =>
+      let h := Control.hyp h in
+      destruct_int_stack b a;
+      try (inversion $h; fail)
+  | [|- _ ] => ()
+  end).
+
+Theorem test : forall (vs vs': value_stack), eval_step vs (e_int swap) = final vs' ->
+  exists v1 v2 vs'', vs = v1 :: v2 :: vs'' /\ vs' = v2 :: v1 :: vs''.
+Proof.
+  intros s s' Heq.
+  ensure_valid_stack ().
+  simpl in Heq. injection Heq as Hinj. subst. eauto.
+Qed.
+
+Theorem eval_step_final_sem : forall (e : expr) (vs vs' : value_stack),
+  eval_step vs e = final vs' -> Sem_expr vs e vs'.
+Proof.
+  intros e vs vs' Hev. destruct e.
+  - destruct i; ensure_valid_stack ();
+    (* Get rid of trivial cases that match one-to-one. *)
+    simpl in Hev; try (injection Hev as Hinj; subst; solve_basic ()).
+    + (* compose with one quoted value *)
+      destruct v. inversion Hev.
+    + (* compose with two quoted values. *)
+      destruct v; destruct v0.
+      injection Hev as Hinj; subst; solve_basic ().
+    + (* Apply is not final. *) destruct v. inversion Hev.
+  - (* Quote is always final, trivially. *)
+    simpl in Hev. injection Hev as Hinj; subst. solve_basic ().
+  - (* Compose is never final. *)
+    simpl in Hev. destruct (eval_step vs e1); inversion Hev.
+Qed.
+
+Theorem eval_step_middle_sem : forall (e ei: expr) (vs vsi vs' : value_stack),
+  eval_step vs e = middle ei vsi ->
+  Sem_expr vsi ei vs' ->
+  Sem_expr vs e vs'.
+Proof.
+  intros e. induction e; intros ei vs vsi vs' Hev Hsem.
+  - destruct i; ensure_valid_stack ().
+    + (* compose with one quoted value. *)
+      destruct v. inversion Hev.
+    + (* compose with two quoted values. *)
+      destruct v; destruct v0. inversion Hev.
+    + (* Apply *)
+      destruct v. injection Hev as Hinj; subst.
+      solve_basic (). auto.
+  - inversion Hev.
+  - simpl in Hev.
+    destruct (eval_step vs e1) eqn:Hev1.
+    + inversion Hev.
+    + injection Hev as Hinj; subst. inversion Hsem; subst.
+      specialize (IHe1 e vs vsi vs2 Hev1 H2).
+      eapply Sem_e_comp. apply IHe1. apply H4.
+    + injection Hev as Hinj; subst.
+      specialize (eval_step_final_sem e1 vs vsi Hev1) as Hsem1.
+      eapply Sem_e_comp. apply Hsem1. apply Hsem.
 Qed.
 
 Theorem eval_step_sem_back : forall (e : expr) (vs vs' : value_stack),
-  eval_chain (strip_value_list vs) e (strip_value_list vs') -> Sem_expr vs e vs'
-with eval_step_int_back : forall (i : intrinsic) (vs vs' : value_stack),
-  eval_chain (strip_value_list vs) (e_int i) (strip_value_list vs') -> Sem_int vs i vs'.
+  eval_chain vs e vs' -> Sem_expr vs e vs'.
 Proof.
-  (* Thoughts: prove a "step value stack preservation" property. A step suggested by
-     eval_step will ensure the stack contains values if it contained values initially.
+  intros e vs vs' ch.
+  ltac1:(dependent induction ch).
+  - apply eval_step_final_sem. auto.
+  - specialize (eval_step_middle_sem e ei vs vsi vs' P IHch). auto.
+Qed.
 
-     Done! eval_step_preservation.
-
-     From there, by induction, a chain preserves value stacks. *)
-Admitted.
-
-
-Theorem eval_step_sem_not : forall (e : expr) (vs : value_stack),
-  ~ (exists vs', Sem_expr vs e vs') -> ~(exists vs', eval_chain (strip_value_list vs) e (strip_value_list vs'))
-with eval_step_int_not : forall (i : intrinsic) (vs : value_stack),
-  ~ (exists vs', Sem_int vs i vs') -> ~(exists vs', eval_chain (strip_value_list vs) (e_int i) (strip_value_list vs')).
+Corollary eval_step_no_sem : forall (e : expr) (vs vs' : value_stack),
+  ~ (Sem_expr vs e vs') -> ~(eval_chain vs e vs').
 Proof.
-(*
-  - intros e vs Hnsem [vs' Hev].
-    destruct e.
-    + specialize (eval_step_sem_not _ _ Hnsem). apply eval_step_sem_not.
-      eexists. apply Hev.
-    + apply Hnsem. eexists. apply Sem_e_quote.
-    + inversion Hev.
-      * simpl in P. destruct (eval_step (strip_value_list vs) e1); inversion P.
-      * specialize (eval_chain_split e1 e2 (strip_value_list vs) (strip_value_list vs') Hev) as [s' [ch1 ch2]].
-        assert (Hnboth : ~ (exists vsi, Sem_expr vs e1 vsi /\ Sem_expr vsi e2 vs')).
-        { intros [vsi [H1 H2]]. apply Hnsem. exists vs'. eapply Sem_e_comp. apply H1. apply H2. }
-
-        assert (Hncomp : ~ (exists vsi, Sem_expr vs e1 vsi) \/ exists vsi, Sem_expr vs e1 vsi /\ ~(Sem_expr vsi e2 vs')).
-        { 
-  - intros i vs Hnint [vs' Hev]. destruct i.
-    + destruct vs as [|v [|v' vs]]; inversion Hev; simpl in P; inversion P.
-      apply Hnint. eexists. apply Sem_swap.
-    + destruct vs as [|v vs]; inversion Hev; simpl in P; inversion P.
-      apply Hnint. eexists. apply Sem_clone.
-    + destruct vs as [|v vs]; inversion Hev; simpl in P; inversion P.
-      apply Hnint. eexists. apply Sem_drop.
-    + destruct vs as [|v vs]; inversion Hev; simpl in P; inversion P.
-      apply Hnint. eexists. apply Sem_quote.
-    + destruct vs as [|v [|v' vs]];
-      try (destruct v; destruct x);
-      try (destruct v'; destruct x0);
-      simpl in Hev; inversion Hev; simpl in P; inversion P; subst.
-      destruct i; destruct i0.
-      apply Hnint. eexists. apply Sem_compose.
-    + destruct vs as [|v vs].
-      * simpl in Hev; inversion Hev; simpl in P; inversion P.
-      * (* Monkey at keyboard mode engaged here. *)
-        destruct v eqn:Hv. destruct i eqn:Hi.
-        simpl in Hev; inversion Hev; simpl in P; inversion P.
-        injection P as Heq. subst.
-        assert (Hna : ~(exists vs', Sem_expr vs ei vs')).
-        { intros [vs'0 Hsem]. apply Hnint. eexists. apply Sem_apply. apply Hsem. }
-        specialize (eval_step_sem_not _ _ Hna). apply eval_step_sem_not. eexists.
-        apply rest.
- *)
-Admitted.
+  intros e vs vs' Hnsem Hch.
+  specialize (eval_step_sem_back _ _ _ Hch). auto.
+Qed.
 
 Require Extraction.
 Require Import ExtrHaskellBasic.
 Extraction Language Haskell.
-Extraction "UccGen.hs" eval_step true false or.
+Set Extraction KeepSingleton.
+Extraction "UccGen.hs" expr eval_step true false or.

code/dawn/DawnV2.v

@@ -0,0 +1,179 @@
+Require Import Coq.Lists.List.
+From Ltac2 Require Import Ltac2.
+
+Inductive intrinsic :=
+  | swap
+  | clone
+  | drop
+  | quote
+  | compose
+  | apply.
+
+Inductive expr :=
+  | e_int (i : intrinsic)
+  | e_quote (e : expr)
+  | e_comp (e1 e2 : expr).
+
+Definition e_compose (e : expr) (es : list expr) := fold_left e_comp es e.
+
+Inductive value := v_quote (e : expr).
+Definition value_stack := list value.
+
+Definition value_to_expr (v : value) : expr :=
+  match v with
+  | v_quote e => e_quote e
+  end.
+
+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 (value_to_expr 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'
+
+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.
+
+Definition false : expr := e_quote (e_int drop).
+Definition false_v : value := v_quote (e_int drop).
+
+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)).
+
+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.
+
+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.
+
+Definition or : expr := e_comp (e_int clone) (e_int apply).
+
+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.
+
+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.
+
+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.
+
+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.
+
+Theorem quote_2_correct : forall (v1 v2 : value) (vs : value_stack),
+    Sem_expr (v2 :: v1 :: vs) (quote_n 1) (v_quote (e_comp (value_to_expr v1) (value_to_expr 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.
+
+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 (value_to_expr v1) (e_comp (value_to_expr v2) (value_to_expr 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.
+
+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).
+
+Theorem quote_2_correct' : forall (v1 v2 : value) (vs : value_stack),
+    Sem_expr (v2 :: v1 :: vs) (quote_n 1) (v_quote (e_comp (value_to_expr v1) (value_to_expr 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 (value_to_expr v1) (e_comp (value_to_expr v2) (value_to_expr v3))) :: vs).
+Proof. intros. simpl. solve_basic (). Qed.
+
+Definition rotate_n (n : nat) := e_compose (quote_n n) (e_int swap :: e_int quote :: e_int compose :: e_int apply :: nil).
+
+Lemma eval_value : forall (v : value) (vs : value_stack),
+  Sem_expr vs (value_to_expr v) (v :: vs).
+Proof.
+  intros v vs.
+  destruct v. 
+  simpl. apply Sem_e_quote.
+Qed.
+
+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.
+
+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'.
+Proof.
+  intros e1 e2 e3 vs vs'.
+  split; intros Heval.
+  - inversion Heval; subst. inversion H4; subst.
+    eapply Sem_e_comp. eapply Sem_e_comp. apply H2. apply H3. apply H6.
+  - inversion Heval; subst. inversion H2; subst.
+    eapply Sem_e_comp. apply H3. eapply Sem_e_comp. apply H6. apply H4.
+Qed.

code/dawn/Ucc.hs

@@ -0,0 +1,64 @@
+module Ucc where
+import UccGen
+import Text.Parsec
+import Data.Functor.Identity
+import Control.Applicative hiding ((<|>))
+import System.IO
+
+instance Show Intrinsic where
+    show Swap = "swap"
+    show Clone = "clone"
+    show Drop = "drop"
+    show Quote = "quote"
+    show Compose = "compose"
+    show Apply = "apply"
+
+instance Show Expr where
+    show (E_int i) = show i
+    show (E_quote e) = "[" ++ show e ++ "]"
+    show (E_comp e1 e2) = show e1 ++ " " ++ show e2
+
+instance Show Value where
+    show (V_quote e) = show (E_quote e)
+
+type Parser a = ParsecT String () Identity a
+
+intrinsic :: Parser Intrinsic
+intrinsic = (<* spaces) $ foldl1 (<|>) $ map (\(s, i) -> try (string s >> return i))
+    [ ("swap", Swap)
+    , ("clone", Clone)
+    , ("drop", Drop)
+    , ("quote", Quote)
+    , ("compose", Compose)
+    , ("apply", Apply)
+    ]
+
+expression :: Parser Expr
+expression = foldl1 E_comp <$> many1 single
+    where
+        single
+            = (E_int <$> intrinsic)
+            <|> (fmap E_quote $ char '[' *> spaces *> expression <* char ']' <* spaces)
+
+parseExpression :: String -> Either ParseError Expr
+parseExpression = runParser expression () "<inline>"
+
+eval :: [Value] -> Expr -> Maybe [Value]
+eval s e =
+    case eval_step s e of
+        Err -> Nothing
+        Final s' -> Just s'
+        Middle e' s' -> eval s' e'
+
+main :: IO ()
+main = do
+    putStr "> "
+    hFlush stdout
+    str <- getLine
+    case parseExpression str of
+        Right e ->
+            case eval [] e of
+                Just st -> putStrLn $ show st
+                _ -> putStrLn "Evaluation error"
+        _ -> putStrLn "Parse error"
+    main

content/blog/coq_dawn_eval.md

@@ -0,0 +1,274 @@
+---
+title: "A Verified Evaluator for the Untyped Concatenative Calculus"
+date: 2021-11-27T20:24:57-08:00
+draft: true
+tags: ["Dawn", "Coq", "Programming Languages"]
+---
+
+Earlier, I wrote [an article]({{< relref "./coq_dawn" >}}) in which I used Coq to
+encode the formal semantics of [Dawn's Untyped Concatenative Calculus](https://www.dawn-lang.org/posts/foundations-ucc/),
+and to prove a few thing about the mini-language. Though I'm quite happy with how that turned out,
+my article was missing something that's present on the original Dawn page -- an evaluator. In this article, I'll define
+an evaluator function in Coq, prove that it's equivalent to Dawn's formal semantics,
+and extract all of this into usable Haskell code.
+
+### Changes Since Last Time
+In trying to write and verify this evaluator, I decided to make changes to the way I formalized
+the UCC. Remember how we used a predicate, `IsValue`, to tag expressions that were values?
+It turns out that this is a very cumbersome approach. For one thing, this formalization
+allows for the case in which the exact same expression is a value for two different
+reasons. Although `IsValue` has only one constructor (`Val_quote`), it's actually
+{{< sidenote "right" "hott-note" "not provable" >}}
+Interestingly, it's also not provable that any two proofs of \(a = b\) are equal,
+even though equality only has one constructor, \(\text{eq_refl}\ :\ a \rightarrow (a = a) \).
+Under the <a href="https://homotopytypetheory.org/book/">homotopic interpretation</a>
+of type theory, this corresponds to the fact that two paths from \(a\) to \(b\) need
+not be homotopic (continuously deformable) to each other.<br>
+<br>
+As an intuitive example, imagine wrapping a string around a pole. Holding the ends of
+the string in place, there's nothing you can do to "unwrap" the string. This string
+is thus not deformable into a string that starts and stops at the same points,
+but does not go around the pole.
+{{< /sidenote >}}
+that any two proofs of `IsValue e` are equal. I ended up getting into a lot of losing
+arguments with the Coq runtime about whether or not two stacks are actually the same.
+Also, some of the semantic rules expected a value on the stack with a particular proof
+for `IsValue`, and rejected the exact same stack with a generic value.
+
+Thus, I switched from our old implementation:
+
+{{< codelines "Coq" "dawn/Dawn.v" 19 22 >}}
+
+To the one I originally had in mind:
+
+{{< codelines "Coq" "dawn/DawnV2.v" 19 19 >}}
+
+I then had the following function to convert a value back into an equivalent expression:
+
+{{< codelines "Coq" "dawn/DawnV2.v" 22 25 >}}
+
+I replaced instances of `projT1` with instances of `value_to_expr`.
+
+### Where We Are
+At the end of my previous article, we ended up with a Coq encoding of the big-step
+[operational semantics](https://en.wikipedia.org/wiki/Operational_semantics)
+of UCC, as well as some proofs of correctness about the derived forms from
+the article (like \\(\\text{quote}_3\\) and \\(\\text{rotate}_3\\)). The trouble
+is, despite having our operational semantics, we can't make our Coq
+code run anything. This is for several reasons:
+
+1. Our definitions only let us to _confirm_ that given some
+   initial stack, a program ends up in some other final stack. We even have a
+   little `Ltac2` tactic to help us automate this kind of proof. However, in an evaluator,
+   the final stack is not known until the program finishes running. We can't
+   confirm the result of evaluation, we need to _find_ it.
+2. To address the first point, we could try write a function that takes a program
+   and an initial stack, and produces a final stack, as well as a proof that
+   the program would evaluate to this stack under our semantics. However,
+   it's quite easy to write a non-terminating UCC program, whereas functions
+   in Coq _have to terminate!_ We can't write a terminating function to
+   run non-terminating code.
+
+So, is there anything we can do? No, there isn't. Writing an evaluator in Coq
+is just not possible. The end, thank you for reading.
+
+Just kidding -- there's definitely a way to get our code evaluating, but it
+will look a little bit strange.
+
+### A Step-by-Step Evaluator
+The trick is to recognize that program evaluation
+occurs in steps. There may well be an infinite number of steps, if the program
+is non-terminating, but there's always a step we can take. That is, unless
+an invalid instruction is run, like trying to clone from an empty stack, or unless
+the program finished running. You don't need a non-terminating function to just
+give you a next step, if one exists. We can write such a function in Coq.
+
+Here's a new data type that encodes the three situations we mentioned in the
+previous paragraph. Its constructors (one per case) are as follows:
+
+1. `err` - there are no possible evaluation steps due to an error.
+3. `middle e s` - the evaluation took a step; the stack changed to `s`, and the rest of the program is `e`.
+2. `final s` - there are no possible evaluation steps because the evaluation is complete, 
+leaving a final stack `s`.
+
+{{< codelines "Coq" "dawn/DawnEval.v" 6 9 >}}
+
+We can now write a function that tries to execute a single step given an expression.
+
+{{< codelines "Coq" "dawn/DawnEval.v" 11 27 >}}
+
+Most intrinsics, by themselves, complete after just one step. For instance, a program
+consisting solely of \\(\\text{swap}\\) will either fail (if the stack doesn't have enough
+values), or it will swap the top two values and be done. We list only "correct" cases,
+and resort to a "catch-all" case on line 26 that returns an error. The one multi-step
+intrinsic is \\(\\text{apply}\\), which can evaluate an arbitrary expression from the stack.
+In this case, the "one step" consists of popping the quoted value from the stack; the
+"remaining program" is precisely the expression that was popped.
+
+Quoting an expression also always completes in one step (it simply places the quoted
+expression on the stack). The really interesting case is composition. Expressions
+are evaluated left-to-right, so we first determine what kind of step the left expression (`e1`)
+can take. We may need more than one step to finish up with `e1`, so there's a good chance it
+returns a "rest program" `e1'` and a stack `vs'`. If this happens, to complete evaluation of
+\\(e_1\\ e_2\\), we need to first finish evaluating \\(e_1'\\), and then evaluate \\(e_2\\).
+Thus, the "rest of the program" is \\(e_1'\\ e_2\\), or `e_comp e1' e2`. On the other hand,
+if `e1` finished evaluating, we still need to evaluate `e2`, so our "rest of the program"
+is \\(e_2\\), or `e2`. If evaluating `e1` led to an error, then so did evaluating `e_comp e1 e2`,
+and we return `err`.
+
+### Extracting Code
+Just knowing a single step is not enough to run the code. We need something that repeatedly
+tries to take a step, as long as it's possible. However, this part is once again
+not possible in Coq, as it brings back the possibility of non-termination. So if we can't use
+Coq, why don't we use another language? Coq's extraction mechanism allows us to do just that.
+
+I added the following code to the end of my file:
+
+{{< codelines "Coq" "dawn/DawnEval.v" 219 223 >}}
+
+Coq happily produces a new file, `UccGen.hs` with a lot of code. It's not exactly the most
+aesthetic; here's a quick peek:
+
+```Haskell
+data Intrinsic =
+   Swap
+ | Clone
+ | Drop
+ | Quote
+ | Compose
+ | Apply
+
+data Expr =
+   E_int Intrinsic
+ | E_quote Expr
+ | E_comp Expr Expr
+
+data Value =
+   V_quote Expr
+
+-- ... more
+```
+
+All that's left is to make a new file, `Ucc.hs`. I use a different file so that
+changes I make aren't overridden by Coq each time I run extraction. In this
+file, we place the "glue code" that tries running one step after another:
+
+{{< codelines "Coq" "dawn/Ucc.hs" 46 51 >}}
+
+Finally, loading up GHCi using `ghci Ucc.hs`, I can run the following commands:
+
+```
+ghci> fromList = foldl1 E_comp
+ghci> test = eval [] $ fromList [true, false, UccGen.or]
+ghci> :f test
+test = Just [V_quote (E_comp (E_int Swap) (E_int Drop))]
+```
+
+That is, applying `or` to `true` and `false` results a stack with only `true` on top.
+As expected, and proven by our semantics!
+
+### Proving Equivalence
+Okay, so `true false or` evaluates to `true`, much like our semantics claims.
+However, does our evaluator _always_ match the semantics? So far, we have not
+claimed or verified that it does. Let's try giving it a shot.
+
+The first thing we can do is show that if we have a proof that `e` takes
+initial stack `vs` to final stack `vs'`, then each
+`eval_step` "makes progress" towards `vs'` (it doesn't simply _return_
+`vs'`, since it only takes a single step and doesn't always complete
+the evaluation). We also want to show that if the semanics dictates
+`e` finishes in stack `vs'`, then `eval_step` will never return an error.
+Thus, we have two possibilities:
+
+* `eval_step` returns `final`. In this case, for it to match our semantics,
+  the final stack must be the same as `vs'`. Here's the relevant section
+  from the Coq file:
+
+  {{< codelines "Coq" "dawn/DawnEval.v" 30 30 >}}
+* `eval_step` returns `middle`. In this case, the "rest of the program" needs
+  to evaluate to `vs'` according to our semantics (otherwise, taking a step
+  has changed the program's final outcome, which should not happen).
+  We need to quantify the new variables (specifically, the "rest of the
+  program", which we'll call `ei`, and the "stack after one step", `vsi`),
+  for which we use Coq's `exists` clause. The whole relevant statement is as
+  follows:
+
+  {{< codelines "Coq" "dawn/DawnEval.v" 31 33 >}}
+
+The whole theorem claim is as follows:
+
+{{< codelines "Coq" "dawn/DawnEval.v" 29 33 >}}
+
+I have the Coq proof script for this (in fact, you can click the link
+at the top of the code block to view the original source file). However,
+there's something unsatisfying about this statement. In particular,
+how do we prove that an entire sequence of steps evaluates
+to something? We'd have to examine the first step, checking if
+it's a "final" step or a "middle" step; if it's a "middle" step,
+we'd have to move on to the "rest of the program" and repeat the process.
+Each time we'd have to "retrieve" `ei` and `vsi` from `eval_step_correct`,
+and feed it back to `eval_step`.
+
+I'll do you one better: how do we even _say_ that an expression "evaluates
+step-by-step to final stack `vs'`"? For one step, we can say:
+
+```Coq
+eval_step vs e = final vs'
+```
+
+For two steps, we'd have to assert the existence of an intermediate
+expression (the "rest of the program" after the first step):
+
+```Coq
+exists ei vsi,
+    eval_step vs e = middle ei vsi /\ (* First step to intermediate expression. *)
+    eval_step vsi ei = final vs' (* Second step to final state. *)
+```
+
+For three steps:
+
+```Coq
+exists ei1 ei2 vsi1 vsi2,
+    eval_step vs e = middle ei1 vsi1 /\ (* First step to intermediate expression. *)
+    eval_step vsi1 ei1 = middle ei2 vsi2 /\ (* Second intermediate step *)
+    eval_step vsi2 ei2 = final vs' (* Second step to final state. *)
+```
+
+This is awful! Not only is this a lot of writing, but it also makes various
+sequences of steps have a different "shape". This way, we can't make
+proofs about evalutions of an _arbitrary_ number of steps. Not all is lost, though: if we squint
+a little at the last example (three steps), a pattern starts to emerge.
+First, let's re-arrange the `exists` qualifiers:
+
+```Coq
+exists ei1 vsi1, eval_step vs e = middle ei1 vsi1 /\  (* Cons *)
+exists ei2 vsi2, eval_step vsi1 ei1 = middle ei2 vsi2 /\ (* Cons *)
+eval_step vsi2 ei2 = final vs' (* Nil *)
+```
+
+If you squint at this, it kind of looks like a list! The "empty"
+part of a list is the final step, while the "cons" part is a middle step. The
+analogy holds up for another reason: an "empty" sequence has zero intermediate
+expressions, while each "cons" introduces a single new intermediate
+program. Perhaps we can define a new data type that matches this? Indeed
+we can!
+
+{{< codelines "Coq" "dawn/DawnEval.v" 64 67 >}}
+
+The new data type is parameterized by the initial and final stacks, as well
+as the expression that starts in the former and ends in the latter.
+Then, consider the following _type_:
+
+```Coq
+eval_chain nil (e_comp (e_comp true false) or) (true :: nil)
+```
+
+This is the type of sequences (or chains) of steps corresponding to the
+evaluation of the program \\(\\text{true}\\ \\text{false}\\ \\text{or}\\),
+starting in an empty stack and evaluating to a stack with only true on top.
+Thus to say that an expression evaluates to some final stack `vs'`, in
+_some unknown number of steps_, it's sufficient to write:
+
+```Coq
+eval_chain vs e vs'
+```