From 0816e06e8184229d46f2da14ed61ce92ee2d3bfa Mon Sep 17 00:00:00 2001 From: =?UTF-8?q?Rapha=C3=ABl=20Monat?= Date: Tue, 14 Mar 2017 11:33:04 +0100 Subject: [PATCH] new typing done with heiko / ! \ not compiling --- coq/Commands.v | 24 +++++- coq/ErrorValidation.v | 51 +++++++++--- coq/IntervalValidation.v | 6 -- coq/Typing.v | 170 ++++++++++++++++++++++++++++----------- coq/ssaPrgs.v | 20 ++--- 5 files changed, 194 insertions(+), 77 deletions(-) diff --git a/coq/Commands.v b/coq/Commands.v index d2b7eb4..317b149 100644 --- a/coq/Commands.v +++ b/coq/Commands.v @@ -14,6 +14,12 @@ Inductive cmd (V:Type) :Type := Let: mType -> nat -> exp V -> cmd V -> cmd V | Ret: exp V -> cmd V. +Fixpoint getRetExp (V:Type) (f:cmd V) := + match f with + |Let m x e g => getRetExp g + | Ret e => e + end. + Fixpoint toRCmd (f:cmd Q) := match f with @@ -46,15 +52,27 @@ Inductive sstep : cmd R -> env -> R -> cmd R -> env -> Prop := Define big step semantics for the Daisy language, terminating on a "returned" result value **) + +(* meaning of this -> mType ??? *) +(* Inductive bstep : cmd R -> env -> R -> mType -> Prop := *) +(* let_b m x e s E v res: *) +(* eval_exp E e v m -> *) +(* bstep s (updEnv x m v E) res m -> *) +(* bstep (Let m x e s) E res m *) +(* |ret_b m e E v: *) +(* eval_exp E e v m -> *) +(* bstep (Ret e) E v m. *) Inductive bstep : cmd R -> env -> R -> mType -> Prop := - let_b m x e s E v res: + let_b m m' x e s E v res: eval_exp E e v m -> - bstep s (updEnv x m v E) res m -> - bstep (Let m x e s) E res m + bstep s (updEnv x m v E) res m' -> + bstep (Let m x e s) E res m' |ret_b m e E v: eval_exp E e v m -> bstep (Ret e) E v m. + + (** The free variables of a command are all used variables of expressions without the let bound variables diff --git a/coq/ErrorValidation.v b/coq/ErrorValidation.v index ff11ed0..c9e54ff 100644 --- a/coq/ErrorValidation.v +++ b/coq/ErrorValidation.v @@ -2665,7 +2665,10 @@ Qed. Fixpoint typeExpressionCmd (f:cmd Q) (f':exp Q) : option mType := match f with |Let m n e c => if expEqBool f' (Var Q m n) then - Some m + match typeExpression e f' with + |None => None + |Some m1 => if mTypeEqBool m1 m then Some m else None + end else let te := typeExpression e in let tc := typeExpressionCmd c in @@ -2678,6 +2681,29 @@ Fixpoint typeExpressionCmd (f:cmd Q) (f':exp Q) : option mType := |Ret e => (typeExpression e) f' end. + +(* Lemma soundnessTypeCmd f n m0 m1 fV dV oV: *) +(* ssaPrg f (NatSet.union fV dV) oV -> *) +(* (typeExpressionCmd f) (Var Q m1 n) = Some m1 -> *) +(* (typeExpressionCmd f) (Var Q m0 n) = Some m0 -> *) +(* m1 = m0. *) +(* Proof. *) +(* revert f; induction f; intros. *) +(* - simpl in H0,H1. *) +(* case_eq (n =? n0); intros; rewrite H2 in H0, H1. *) +(* + admit. *) +(* + rewrite andb_false_r in H0, H1. *) +(* case_eq (typeExpression e (Var Q m1 n)); intros; case_eq (typeExpression e (Var Q m0 n)); intros; rewrite H3 in H0; rewrite H4 in H1. *) +(* * case_eq (typeExpressionCmd f (Var Q m1 n)); intros; case_eq (typeExpressionCmd f (Var Q m0 n)); intros; rewrite H5 in H0; rewrite H6 in H1. *) +(* { *) + +(* } *) + +(* case_eq (mTypeEqBool m1 m); intros; case_eq (mTypeEqBool m0 m); intros; rewrite H3 in H0; rewrite H in H1. *) +(* + *) + + + Fixpoint cmdEqBool (f f': cmd Q): bool := match f, f' with |Let m1 n1 e1 c1, Let m2 n2 e2 c2 => @@ -2696,7 +2722,8 @@ Fixpoint isSubCmd (f':cmd Q) (f:cmd Q): bool := Theorem validErrorboundCmd_sound (f:cmd Q) (absenv:analysisResult): - forall E1 E2 outVars fVars dVars vR vF elo ehi err P m, + forall E1 E2 outVars fVars dVars vR vF elo ehi err P m tEnv, + tEnv = typeExpressionCmd f -> approxEnv E1 absenv fVars dVars E2 -> ssaPrg f (NatSet.union fVars dVars) outVars -> NatSet.Subset (NatSet.diff (Commands.freeVars f) dVars) fVars -> @@ -2704,8 +2731,8 @@ Theorem validErrorboundCmd_sound (f:cmd Q) (absenv:analysisResult): bstep (toRCmd f) E2 vF m -> validErrorboundCmd f (* (typeExpressionCmd f) *) absenv dVars = true -> validIntervalboundsCmd f absenv P dVars = true -> - (forall e1 v1 m1, NatSet.mem v1 dVars = true -> - (typeExpressionCmd e1) (Var Q m1 v1) = Some m1 -> + (forall v1 m1, NatSet.mem v1 dVars = true -> + tEnv (Var Q m1 v1) = Some m1 -> exists vR, E1 v1 = Some (vR, M0) /\ (Q2R (fst (fst (absenv (Var Q m1 v1)))) <= vR <= Q2R (snd (fst (absenv (Var Q m1 v1)))))%R) -> (forall v, NatSet.mem v fVars= true -> @@ -2715,7 +2742,7 @@ Theorem validErrorboundCmd_sound (f:cmd Q) (absenv:analysisResult): (Rabs (vR - vF) <= (Q2R err))%R. Proof. induction f; - intros * (*type_f*) approxc1c2 ssa_f freeVars_subset eval_real eval_float (*issubcmd_ok*) valid_bounds valid_intv fVars_sound P_valid absenv_res. + intros * type_f approxc1c2 ssa_f freeVars_subset eval_real eval_float (*issubcmd_ok*) valid_bounds valid_intv fVars_sound P_valid absenv_res. - simpl in eval_real, eval_float. inversion eval_float; inversion eval_real; subst. inversion ssa_f; subst. @@ -2761,9 +2788,10 @@ Proof. - intros e0 v1 m2 natset typeexpr. - specialize (fVars_sound (Ret e0) v1 m2 natset). - assert (typeExpressionCmd (Ret e0) (Var Q m2 v1) = Some m2) by (simpl; auto). - apply fVars_sound; auto. + specialize (fVars_sound v1 m2 natset). + admit. + (*assert (typeExpressionCmd (Ret e0) (Var Q m2 v1) = Some m2) by (simpl; auto). + apply fVars_sound; auto.*) - instantiate (1 := q0). instantiate (1 := q). rewrite absenv_e; auto. } (* * inversion ssa_f; subst. @@ -2805,7 +2833,7 @@ Proof. simpl. rewrite NatSet.diff_spec, NatSet.remove_spec, NatSet.union_spec. split; try auto. - * intros e1 v1 m1 v1_mem typing_e1. + * intros v1 m1 v1_mem typing_e1. unfold updEnv. case_eq (v1 =? n); intros v1_eq. { rename R1 into eq_lo; @@ -2817,6 +2845,11 @@ Proof. apply Nat.eqb_eq in v1_eq; subst. exists v0; split; try auto. + (* Let n:m0 = e in f *) + (* typeExpressionCmd f (Var Q m1 n) = Some m1 *) + (* Want to prove: typeExpressionCmd f (Var Q m0 n) = Some m0 /\ m1 = m0. (because variable n is used in f). *) + + admit. diff --git a/coq/IntervalValidation.v b/coq/IntervalValidation.v index 6f12ea0..b650552 100644 --- a/coq/IntervalValidation.v +++ b/coq/IntervalValidation.v @@ -195,12 +195,6 @@ Proof. apply le_neq_bool_to_lt_prop; auto. Qed. -Fixpoint getRetExp (V:Type) (f:cmd V) := - match f with - |Let m x e g => getRetExp g - | Ret e => e - end. - Lemma validVarsUnfolding_l (E:env) (absenv:analysisResult) (f1 f2: exp Q) dVars (b:binop) m0: (typeExpression (Binop b f1 f2)) (Binop b f1 f2) = Some m0 -> (forall (v : NatSet.elt) (m : mType), diff --git a/coq/Typing.v b/coq/Typing.v index c209277..40a9670 100644 --- a/coq/Typing.v +++ b/coq/Typing.v @@ -1,49 +1,122 @@ Require Import Coq.Reals.Reals Coq.micromega.Psatz Coq.QArith.QArith Coq.QArith.Qreals Coq.MSets.MSets. -Require Import Daisy.Infra.RealRationalProps Daisy.Expressions Daisy.Infra.Ltacs. +Require Import Daisy.Infra.RealRationalProps Daisy.Expressions Daisy.Infra.Ltacs Daisy.Commands Daisy.ssaPrgs. Require Export Daisy.Infra.Abbrevs Daisy.Infra.RealSimps Daisy.Infra.NatSet Daisy.IntervalArithQ Daisy.IntervalArith Daisy.Infra.MachineType. (** -Now we want a TypeEnv function, taking an expression and returning a exp -> option mType +Now we want a TypeEnv function, taking an expression and returning a exp -> option mType Soundness property is: TypeEnv e = T -> eval_exp e E v m -> T e = m. -**) + **) -(** A good function computing a map of expression types **) -Fixpoint typeExpression (e:exp Q) (e':exp Q) : option mType := +Definition updTEnv (e:exp Q) (t:mType) (cont:exp Q-> option mType) := + (fun e' => + if expEqBool e e' + then Some t + else cont e'). + +Definition emptyTEnv :exp Q -> option mType := fun e => None. + +Fixpoint typeExpression_trec e (cont:exp Q -> option mType) : exp Q -> option mType := match e with - | Var _ m n => if expEqBool e e' then Some m else None - | Const m n => if expEqBool e e' then Some m else None + | Var _ m v => updTEnv e m cont + | Const m n => updTEnv e m cont | Unop u e1 => - let tE1 := typeExpression e1 in - if expEqBool e e' then (tE1 e1) - else (tE1 e') + let tEnv := typeExpression_trec e1 cont in + let t := tEnv e1 in + match t with + | Some m => updTEnv e m tEnv + | None => emptyTEnv + end | Binop b e1 e2 => - let tE1 := typeExpression e1 in - let tE2 := typeExpression e2 in - let m := match (tE1 e1), (tE2 e2) with - |Some m1, Some m2 => Some (computeJoin m1 m2) - |_, _ => None - end in - if expEqBool e e' then m - else match (tE1 e'), (tE2 e') with - |Some m1, Some m2 => if (mTypeEqBool m1 m2) then - Some m1 - else - None - |Some m1, None => Some m1 - |None, Some m2 => Some m2 - |None, None => None - end + let tEnv_e1 := typeExpression_trec e1 cont in + let tEnv_e2 := typeExpression_trec e2 tEnv_e1 in (* TODO: This may cause trouble e.g. in (x:F) + (x:D) *) + let (t_e1,t_e2) := (tEnv_e2 e1, tEnv_e2 e2) in + match t_e1, t_e2 with + |Some m, Some m' => updTEnv e (computeJoin m m') tEnv_e2 + | _, _ => emptyTEnv + end | Downcast m e1 => - let tE1 := typeExpression e1 in - let m := match (tE1 e1) with - | Some m1 => if (isMorePrecise m1 m) then Some m else None - | _ => None - end in - if expEqBool e e' then m - else (tE1 e') + let tEnv_e1 := typeExpression_trec e1 cont in + let t := tEnv_e1 e1 in + match t with + |Some m1 => if (isMorePrecise m1 m) then updTEnv e m tEnv_e1 + else emptyTEnv + |_ => emptyTEnv + end + end. + +Definition typeExpression e := typeExpression_trec e emptyTEnv. + +Definition updNatEnv (x:nat) (m:mType) (env: nat -> option mType) := + (fun n => if (n =? x) then Some m else (env n)). + +Definition emptyNatEnv :nat -> option mType := fun n => None. + + + +Fixpoint typeCmd_trec1 (f:cmd Q) (cont: exp Q -> option mType) (env: nat -> option mType) := + match f with + | Let m x e g => (* check that env x = None ? or this is already done by ssa ? *) + let gamma := typeExpression_trec e cont in + match (gamma e) with + | Some m' => if mTypeEqBool m m' then + (* hum. Should we just return tEnv_g ? *) + typeCmd_trec1 g gamma (updNatEnv x m' env) + else + emptyTEnv + | None => emptyTEnv + end + | Ret e => + typeExpression_trec e cont end. +(* Definition typeCmd f := typeCmd_trec1 f emptyTEnv emptyNatEnv. *) + +(* Eval compute in typeCmd (Let M32 1 (Const M32 (1#1)) (Ret (Binop Plus (Var Q M32 1) (Const M64 (2#1))))). *) +(* Eval compute in typeCmd (Let M64 1 (Const M32 (1#1)) (Ret (Binop Plus (Var Q M64 1) (Const M64 (2#1))))). *) +(* Eval compute in typeCmd (Let M64 1 (Const M32 (1#1)) (Ret (Binop Plus (Var Q M32 1) (Const M32 (2#1))))). *) + + + +(* do we need this env:nat -> option mType ? The updTEnv does the same kind of thing I guess... *) +(* issue here is that we may have (Var Q m x) and (Var Q m' x). But this should not happen... *) +Fixpoint typeCmd_trec2 (f:cmd Q) (cont: exp Q -> option mType) := + match f with + | Let m x e g => + let gamma := typeExpression_trec e cont in + match (gamma e) with + | Some m' => if mTypeEqBool m m' then + let newCont := updTEnv (Var Q m x) m gamma in + typeCmd_trec2 g newCont + else + emptyTEnv + | None => emptyTEnv + end + | Ret e => + typeExpression_trec e cont + end. + +Definition typeCmd f := typeCmd_trec2 f emptyTEnv. + +Eval compute in typeCmd (Let M32 1 (Const M32 (1#1)) (Ret (Binop Plus (Var Q M32 1) (Const M64 (2#1))))). +Eval compute in typeCmd (Let M64 1 (Const M32 (1#1)) (Ret (Binop Plus (Var Q M64 1) (Const M64 (2#1))))). +Eval compute in typeCmd (Let M64 1 (Const M32 (1#1)) (Ret (Binop Plus (Var Q M32 1) (Const M32 (2#1))))). + +Eval compute in typeCmd (Let M32 1 (Const M32 (1#1)) + (Let M64 1 (Const M64 (1#1)) + (Ret (Binop Plus (Var Q M32 1) (Var Q M64 1))))). + + +Theorem typeCmd_sound (f:cmd Q) inVars E v m: + validSSA f inVars = true -> + bstep (toRCmd f) E v m -> + typeCmd f (getRetExp f) = Some m. +Proof. +Admitted. + + + + (* NB: one might be tempted to prove the following lemma: *) (* Lemma typeExpressionPropagatesNone e e0: *) @@ -83,7 +156,7 @@ Proof. - assert (mTypeEqBool m0 m0 && (n =? n) = true) by (apply andb_true_iff; split; [ apply EquivEqBoolEq | rewrite <- beq_nat_refl ]; auto). rewrite H0. trivial. - - assert (mTypeEqBool m0 m0 && Qeq_bool v v = true). + - assert (mTypeEqBool m0 m0 && Qeq_bool v v = true). apply andb_true_iff; split; [apply EquivEqBoolEq; auto | apply Qeq_bool_iff; lra]. rewrite H0. auto. @@ -131,7 +204,7 @@ Proof. - apply IHe. simpl in H. auto. -Qed. +Qed. Lemma typingConstDet (e:exp Q) m m0 v: typeExpression e (Const m v) = Some m0 -> @@ -157,18 +230,18 @@ Proof. - apply IHe. simpl in H. auto. -Qed. +Qed. Fixpoint isSubExpression (e':exp Q) (e:exp Q) := orb (expEqBool e e') ( match e with |Var _ _ _ => false - |Const _ _ => false + |Const _ _ => false |Unop o1 e1 => isSubExpression e' e1 |Binop b e1 e2 => orb (isSubExpression e' e1) (isSubExpression e' e2) |Downcast m e1 => isSubExpression e' e1 end). - + Lemma typeNotSubExpr e e1: isSubExpression e1 e = false -> typeExpression e e1 = None. Proof. @@ -216,9 +289,9 @@ Proof. specialize (IHe1 H0). simpl; rewrite IHe1; auto. + specialize (IHe1 H0); simpl; rewrite IHe1; auto. - + specialize (IHe2 H1); simpl; rewrite IHe2. apply orb_true_r. + + specialize (IHe2 H1); simpl; rewrite IHe2. apply orb_true_r. - simpl; apply IHe; auto. -Qed. +Qed. Lemma typedIsSubExpr e f m: typeExpression e f = Some m -> @@ -261,13 +334,13 @@ Proof. simpl. rewrite IHe. apply orb_true_r. -Qed. +Qed. Lemma typedVarIsUsed e m m0 v: typeExpression e (Var Q m0 v) = Some m -> NatSet.In v (usedVars e). Proof. - intros; induction e. + intros; induction e. - simpl in *. case_eq (mTypeEqBool m1 m0 && (n =? v)); intros; auto; rewrite H0 in H. + andb_to_prop H0. @@ -290,7 +363,7 @@ Proof. + simpl in H; rewrite H1, H2 in H. inversion H. - apply IHe; auto. -Qed. +Qed. Lemma binop_type_unfolding b f1 f2 mf: @@ -312,7 +385,7 @@ Lemma binary_type_unfolding b e1 e2 f m: (typeExpression e1 f = Some m \/ typeExpression e2 f = Some m). Proof. intros notEq typeBinop. - assert (isSubExpression f (Binop b e1 e2) = true) as isSubExpr by (eapply typedIsSubExpr; eauto). + assert (isSubExpression f (Binop b e1 e2) = true) as isSubExpr by (eapply typedIsSubExpr; eauto). simpl in *. rewrite notEq in *. case_eq (typeExpression e1 f); intros; rewrite H in typeBinop. - case_eq (typeExpression e2 f); intros; rewrite H0 in typeBinop. @@ -361,7 +434,7 @@ Proof. case_eq (typeExpression e' e'); intros; rewrite H0 in H1; inversion H1; clear H5. case_eq (isMorePrecise m0 m1); intros; rewrite H4 in H1; inversion H1; subst; clear H1; auto. -Qed. +Qed. (* Lemma subExprRewriting e f1 f2: *) (* expEqBool f1 f2 = true -> *) @@ -447,14 +520,14 @@ Qed. (* - admit. *) (* - simpl; auto. *) (* Admitted. *) - + (* Lemma unary_type_unfolding u e f m: *) (* isSubExpression f e = true -> *) (* typeExpression (Unop u e) f = Some m -> *) (* typeExpression e f = Some m. *) (* Proof. *) (* Admitted. *) - + (* Lemma weakRewritingInTypeExpr e e' f m m': *) (* expEqBool e e' = true -> *) @@ -546,7 +619,7 @@ Proof. * case_eq (typeExpression f2 (Binop b e1 e2)); intros; rewrite H3 in H0; inversion H0; subst. apply IHf2; auto. - apply IHf; auto. -Qed. +Qed. @@ -609,4 +682,3 @@ Proof. rewrite (stupid _ _ H1). apply orb_true_r. Qed. - \ No newline at end of file diff --git a/coq/ssaPrgs.v b/coq/ssaPrgs.v index e554d08..7675289 100644 --- a/coq/ssaPrgs.v +++ b/coq/ssaPrgs.v @@ -235,16 +235,16 @@ Proof. revert E1 E2 vR. induction f; intros E1 E2 vR agree_on_vars. - split; intros bstep_Let; inversion bstep_Let; subst. - + erewrite shadowing_free_rewriting_exp in H5; auto. + + erewrite shadowing_free_rewriting_exp in H6; auto. econstructor; eauto. rewrite <- IHf. - apply H6. + apply H7. intros n'; unfold updEnv. case_eq (n' =? n); auto. - + erewrite <- shadowing_free_rewriting_exp in H5; auto. + + erewrite <- shadowing_free_rewriting_exp in H6; auto. econstructor; eauto. rewrite IHf. - apply H6. + apply H7. intros n'; unfold updEnv. case_eq (n' =? n); auto. - split; intros bstep_Ret; inversion bstep_Ret; subst. @@ -436,8 +436,8 @@ Proof. * eapply ssa_shadowing_free. apply ssa_f. apply x_free. - apply H5. - * erewrite (shadowing_free_rewriting_cmd _ _ _ _) in H6; try eauto. + apply H6. + * erewrite (shadowing_free_rewriting_cmd _ _ _ _) in H7; try eauto. simpl in *. econstructor; eauto. { rewrite <- exp_subst_correct; eauto. } @@ -450,10 +450,10 @@ Proof. inversion ssa_f; subst. econstructor; try auto. rewrite exp_subst_correct; eauto. - rewrite <- IHf in H6; eauto. - * rewrite <- shadowing_free_rewriting_cmd in H6; eauto. + rewrite <- IHf in H7; eauto. + * rewrite <- shadowing_free_rewriting_cmd in H7; eauto. eapply ssa_shadowing_free; eauto. - rewrite <- exp_subst_correct in H5; eauto. + rewrite <- exp_subst_correct in H6; eauto. * rewrite NatSet.add_spec; auto. * apply validVars_add; auto. * eapply dummy_bind_ok; eauto. @@ -493,7 +493,7 @@ Proof. simpl in subst_step. case_eq (let_subst f). + intros f_subst subst_f_eq. - specialize (IHf (updEnv n M0 v E) vR (NatSet.add n inVars) outVars f_subst H9 H6 subst_f_eq). + specialize (IHf (updEnv n M0 v E) vR (NatSet.add n inVars) outVars f_subst H9 H7 subst_f_eq). rewrite subst_f_eq in subst_step. inversion IHf; subst. constructor. -- GitLab