From bc754c7a7d6caa8ed8d5a9badb3e6fa9a6f8acbf Mon Sep 17 00:00:00 2001 From: Danila Fedorin Date: Fri, 26 Nov 2021 01:40:04 -0800 Subject: [PATCH] Start working on a verified UCC evaluator. --- code/dawn/DawnEval.v | 224 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 224 insertions(+) create mode 100644 code/dawn/DawnEval.v diff --git a/code/dawn/DawnEval.v b/code/dawn/DawnEval.v new file mode 100644 index 0000000..69f16e1 --- /dev/null +++ b/code/dawn/DawnEval.v @@ -0,0 +1,224 @@ +Require Import Coq.Lists.List. +Require Import Dawn. +Require Import Coq.Program.Equality. + +Inductive step_result := + | err + | middle (e : expr) (s : list expr) + | final (s : list expr). + +Fixpoint eval_step (s : list expr) (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_comp e1 e2, vs => + match eval_step vs e1 with + | final vs' => middle e2 vs' + | middle e1' vs' => middle (e_comp e1' e2) vs' + | err => err + end + | _, _ => 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')) \/ + (exists (ei : expr) (vsi : value_stack), + eval_step (strip_value_list vs) e = middle ei (strip_value_list vsi) /\ + Sem_expr vsi ei vs'). +Proof. + intros e vs vs' Hsem. + (* Proceed by induction on the semantics. *) + induction Hsem. + - inversion H; (* The expression is just an intrnsic. *) + (* Dismiss all the straightforward "final" cases, + of which most intrinsics are *) + try (left; reflexivity). + (* We are in an intermediate / middle case. *) + right. + (* The semantics guarantee that the expression in the + quote evaluates to the final state. *) + exists e, vs0. auto. + - (* The expression is a quote. This is yet another final case. *) + left; reflexivity. + - (* The composition is never a final step, since we have to evaluate both + branches to "finish up". *) + destruct IHHsem1; right. + + (* If the left branch finihed, only the right branch needs to be evaluted. *) + simpl. rewrite H. exists e2, vs2. auto. + + (* Otherwise, the left branch has an intermediate evaluation, guaranteed + by induction to be consitent. *) + destruct H as [ei [vsi [Heval Hsem']]]. + (* We compose the remaining part of the left branch with the right branch. *) + exists (e_comp ei e2), vsi. simpl. + (* The evaluation is trivially to a "middle" state. *) + rewrite Heval. split. auto. + 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'). + +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''. +Proof. + intros e1 e2 s s' s'' 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''). +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). + + injection P as Hinj; subst. specialize (IHch e e2 H0) as [s'0 [ch1 ch2]]. + eexists. split. + * eapply chain_middle. apply Hval. apply ch1. + * apply ch2. + + subst. eexists. split. + * eapply chain_final. apply Hval. + * 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') +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'). +Proof. + - intros e vs vs' Hsem. + induction Hsem. + + (* This is an intrinsic, which is handled by the second + theorem, eval_step_int. This lemma is used here. *) + 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 + proper evaluation chains. Chains can be composed (via eval_chain_merge). *) + eapply eval_chain_merge with (strip_value_list vs2); auto. + - intros i vs vs' Hsem. + (* The evaluation chain depends on the specific intrinsic in use. *) + inversion Hsem; subst; + (* Most intrinsics produce a final value, and the evaluation chain is trivial. *) + 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. +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'. +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. + + 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')). +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. + +Require Extraction. +Require Import ExtrHaskellBasic. +Extraction Language Haskell. +Extraction "UccGen.hs" eval_step true false or.