Start working on a verified UCC evaluator.
This commit is contained in:
parent
84ad8d43b5
commit
bc754c7a7d
224
code/dawn/DawnEval.v
Normal file
224
code/dawn/DawnEval.v
Normal file
|
|
@ -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.
|
||||||
Loading…
Reference in New Issue
Block a user