From 826dde759f315df1ac14e80334156f91bd96c5c7 Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Sun, 28 Nov 2021 16:50:28 -0800 Subject: [PATCH] Finish a draft of the UCC evaluator article --- code/dawn/DawnEval.v | 59 ++++++++++++++++++++++++++++++---------- content/blog/coq_dawn.md | 1 + 2 files changed, 46 insertions(+), 14 deletions(-) diff --git a/code/dawn/DawnEval.v b/code/dawn/DawnEval.v index 01417c3..00b5c4b 100644 --- a/code/dawn/DawnEval.v +++ b/code/dawn/DawnEval.v @@ -102,9 +102,9 @@ Proof. auto. + (* A quote doesn't have a next step, and so is final. *) apply chain_final. auto. - + (* In compoition, by induction, we know that the two sub-expressions produce + + (* In composition, 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 vs2; auto. + eapply eval_chain_merge; eauto. - intros i vs vs' Hsem. (* The evaluation chain depends on the specific intrinsic in use. *) inversion Hsem; subst; @@ -162,15 +162,15 @@ Proof. - 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 *) + + (* compose with one quoted value is not final, but an error. *) 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. *) + - (* Quote is always final, trivially, and the semantics match easily. *) simpl in Hev. injection Hev as Hinj; subst. solve_basic (). - - (* Compose is never final. *) + - (* Compose is never final, so we don't need to handle it here. *) simpl in Hev. destruct (eval_step vs e1); inversion Hev. Qed. @@ -181,23 +181,35 @@ Theorem eval_step_middle_sem : forall (e ei: expr) (vs vsi vs' : value_stack), Proof. intros e. induction e; intros ei vs vsi vs' Hev Hsem. - destruct i; ensure_valid_stack (). - + (* compose with one quoted value. *) + + (* compose with one quoted value; invalid. *) destruct v. inversion Hev. - + (* compose with two quoted values. *) + + (* compose with two quoted values; not a middle step. *) destruct v; destruct v0. inversion Hev. + (* Apply *) destruct v. injection Hev as Hinj; subst. solve_basic (). auto. - - inversion Hev. + - (* quoting an expression is not middle. *) + inversion Hev. - simpl in Hev. destruct (eval_step vs e1) eqn:Hev1. - + inversion Hev. - + injection Hev as Hinj; subst. inversion Hsem; subst. + + (* Step led to an error, which can't happen in a chain. *) + inversion Hev. + + (* Left expression makes a non-final step. Milk this for equalities first. *) + injection Hev as Hinj; subst. + (* The rest of the program (e_comp e e2) evaluates using our semantics, + which means that both e and e2 evaluate using our semantics. *) + inversion Hsem; subst. + (* By induction, e1 evaluates using our semantics if e does, which we just confirmed. *) specialize (IHe1 e vs vsi vs2 Hev1 H2). - eapply Sem_e_comp. apply IHe1. apply H4. - + injection Hev as Hinj; subst. + (* The composition rule can now be applied. *) + eapply Sem_e_comp; eauto. + + (* Left expression makes a final step. Milk this for equalities first. *) + injection Hev as Hinj; subst. + (* Using eval_step_final, we know that e1 evaluates to the intermediate + state given our semantics. *) specialize (eval_step_final_sem e1 vs vsi Hev1) as Hsem1. - eapply Sem_e_comp. apply Hsem1. apply Hsem. + (* The composition rule can now be applied. *) + eapply Sem_e_comp; eauto. Qed. Theorem eval_step_sem_back : forall (e : expr) (vs vs' : value_stack), @@ -210,7 +222,7 @@ Proof. Qed. Corollary eval_step_no_sem : forall (e : expr) (vs vs' : value_stack), - ~ (Sem_expr vs e vs') -> ~(eval_chain vs e vs'). + ~(Sem_expr vs e vs') -> ~(eval_chain vs e vs'). Proof. intros e vs vs' Hnsem Hch. specialize (eval_step_sem_back _ _ _ Hch). auto. @@ -221,3 +233,22 @@ Require Import ExtrHaskellBasic. Extraction Language Haskell. Set Extraction KeepSingleton. Extraction "UccGen.hs" expr eval_step true false or. + +Remark eval_swap_two_values : forall (vs vs' : value_stack), + eval_step vs (e_int swap) = final vs' -> exists v1 v2 vst, vs = v1 :: v2 :: vst /\ vs' = v2 :: v1 :: vst. +Proof. + intros vs vs' Hev. + (* Can't proceed until we know more about the stack. *) + destruct vs as [|v1 [|v2 vs]]. + - (* Invalid case; empty stack. *) inversion Hev. + - (* Invalid case; stack only has one value. *) inversion Hev. + - (* Valid case: the stack has two values. *) injection Hev. eauto. +Qed. + +Remark eval_swap_two_values' : forall (vs vs' : value_stack), + eval_step vs (e_int swap) = final vs' -> exists v1 v2 vst, vs = v1 :: v2 :: vst /\ vs' = v2 :: v1 :: vst. +Proof. + intros vs vs' Hev. + ensure_valid_stack (). + injection Hev. eauto. +Qed. diff --git a/content/blog/coq_dawn.md b/content/blog/coq_dawn.md index 8db138d..ce02a1f 100644 --- a/content/blog/coq_dawn.md +++ b/content/blog/coq_dawn.md @@ -2,6 +2,7 @@ title: "Formalizing Dawn in Coq" date: 2021-11-20T19:04:57-08:00 tags: ["Coq", "Dawn", "Programming Languages"] +description: "In this article, we use Coq to write down machine-checked semantics for the untyped concatenative calculus." --- The [_Foundations of Dawn_](https://www.dawn-lang.org/posts/foundations-ucc/) article came up