From 5607882d2906135b7f025a277386c37953584c14 Mon Sep 17 00:00:00 2001 From: = Date: Wed, 5 Apr 2017 14:39:22 +0200 Subject: [PATCH] Certificate checking Coq development is now finished? --- coq/CertificateChecker.v | 51 +- coq/Commands.v | 3 +- coq/Environments.v | 31 +- coq/ErrorBounds.v | 38 +- coq/ErrorValidation.v | 429 +++++++------ coq/Expressions.v | 63 +- coq/Infra/Abbrevs.v | 6 +- coq/IntervalValidation.v | 7 +- coq/Typing.v | 238 +++++++- coq/ssaPrgs.v | 569 +++++++++--------- .../daisy/analysis/ChoosePrecisionPhase.scala | 45 ++ 11 files changed, 908 insertions(+), 572 deletions(-) diff --git a/coq/CertificateChecker.v b/coq/CertificateChecker.v index d8631dd..9a000a9 100644 --- a/coq/CertificateChecker.v +++ b/coq/CertificateChecker.v @@ -12,9 +12,11 @@ Require Export Coq.QArith.QArith. Require Export Daisy.Infra.ExpressionAbbrevs Daisy.Commands. (** Certificate checking function **) -Definition CertificateChecker (e:exp Q) (absenv:analysisResult) (P:precond) := - if (validIntervalbounds e absenv P NatSet.empty) - then (validErrorbound e (fun (e:exp Q) => typeExpression e) absenv NatSet.empty) +Definition CertificateChecker (e:exp Q) (absenv:analysisResult) (P:precond) (defVars:nat -> option mType) := + if (typeCheck e defVars (typeMap defVars e)) then + if (validIntervalbounds e absenv P NatSet.empty) + then (validErrorbound e (typeMap defVars e) absenv NatSet.empty) + else false else false. (** @@ -22,16 +24,16 @@ Definition CertificateChecker (e:exp Q) (absenv:analysisResult) (P:precond) := Apart from assuming two executions, one in R and one on floats, we assume that the real valued execution respects the precondition. **) -Theorem Certificate_checking_is_sound (e:exp Q) (absenv:analysisResult) P: +Theorem Certificate_checking_is_sound (e:exp Q) (absenv:analysisResult) P defVars: forall (E1 E2:env) (vR:R) (vF:R) fVars m, - approxEnv E1 absenv fVars NatSet.empty E2 -> + approxEnv E1 defVars absenv fVars NatSet.empty E2 -> (forall v, NatSet.mem v fVars = true -> - exists vR, E1 v = Some (vR, M0) /\ + exists vR, E1 v = Some vR /\ (Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) -> NatSet.Subset (Expressions.usedVars e) fVars -> - eval_exp E1 (toREval (toRExp e)) vR M0 -> - eval_exp E2 (toRExp e) vF m -> - CertificateChecker e absenv P = true -> + eval_exp E1 (toREvalVars defVars) (toREval (toRExp e)) vR M0 -> + eval_exp E2 defVars (toRExp e) vF m -> + CertificateChecker e absenv P defVars = true -> (Rabs (vR - vF) <= Q2R (snd (absenv e)))%R. (** The proofs is a simple composition of the soundness proofs for the range @@ -47,33 +49,33 @@ Proof. destruct iv as [ivlo ivhi]. rewrite absenv_eq; simpl. eapply validErrorbound_sound; eauto. - - admit. (*eapply validTypeMap; eauto. *) - hnf. intros a in_diff. rewrite NatSet.diff_spec in in_diff. apply fVars_subset. destruct in_diff; auto. - - intros v m0 v_in_empty. + - intros v v_in_empty. rewrite NatSet.mem_spec in v_in_empty. inversion v_in_empty. -Admitted. -(* Qed. *) +Qed. -Definition CertificateCheckerCmd (f:cmd Q) (absenv:analysisResult) (P:precond) := - if (validIntervalboundsCmd f absenv P NatSet.empty) - then (validErrorboundCmd f (fun e => typeExpression e) absenv NatSet.empty) +Definition CertificateCheckerCmd (f:cmd Q) (absenv:analysisResult) (P:precond) defVars:= + if (typeCheckCmd f defVars (typeMapCmd defVars f)) + then if (validIntervalboundsCmd f absenv P NatSet.empty) + then (validErrorboundCmd f (typeMapCmd defVars f) absenv NatSet.empty) + else false else false. -Theorem Certificate_checking_cmds_is_sound (f:cmd Q) (absenv:analysisResult) P: +Theorem Certificate_checking_cmds_is_sound (f:cmd Q) (absenv:analysisResult) P defVars: forall (E1 E2:env) outVars vR vF fVars m, - approxEnv E1 absenv fVars NatSet.empty E2 -> + approxEnv E1 defVars absenv fVars NatSet.empty E2 -> (forall v, NatSet.mem v fVars= true -> - exists vR, E1 v = Some (vR, M0) /\ + exists vR, E1 v = Some vR /\ (Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) -> NatSet.Subset (Commands.freeVars f) fVars -> ssa f fVars outVars -> - bstep (toREvalCmd (toRCmd f)) E1 vR M0 -> - bstep (toRCmd f) E2 vF m -> - CertificateCheckerCmd f absenv P = true -> + bstep (toREvalCmd (toRCmd f)) E1 (toREvalVars defVars) vR M0 -> + bstep (toRCmd f) E2 defVars vF m -> + CertificateCheckerCmd f absenv P defVars = true -> (Rabs (vR - vF) <= Q2R (snd (absenv (getRetExp f))))%R. (** The proofs is a simple composition of the soundness proofs for the range @@ -90,7 +92,6 @@ Proof. destruct iv as [ivlo ivhi]. rewrite absenv_eq; simpl. eapply (validErrorboundCmd_sound); eauto. - - admit. (* eapply typeMapCmdValid; eauto.*) - instantiate (1 := outVars). eapply ssa_equal_set; try eauto. hnf. @@ -103,7 +104,7 @@ Proof. rewrite NatSet.diff_spec in in_diff. destruct in_diff. apply fVars_subset; auto. - - intros v m1 v_in_empty. + - intros v v_in_empty. rewrite NatSet.mem_spec in v_in_empty. inversion v_in_empty. -Admitted. \ No newline at end of file +Qed. \ No newline at end of file diff --git a/coq/Commands.v b/coq/Commands.v index f5f0ae9..4472279 100644 --- a/coq/Commands.v +++ b/coq/Commands.v @@ -52,7 +52,8 @@ Inductive sstep : cmd R -> env -> R -> cmd R -> env -> Prop := Inductive bstep : cmd R -> env -> (nat -> option mType) -> R -> mType -> Prop := let_b m m' x e s E v res defVars: eval_exp E defVars e v m -> - bstep s (updEnv x m v E) defVars res m' -> + defVars x = Some m -> + bstep s (updEnv x v E) defVars res m' -> bstep (Let m x e s) E defVars res m' |ret_b m e E v defVars: eval_exp E defVars e v m -> diff --git a/coq/Environments.v b/coq/Environments.v index bee30af..d8f89ad 100644 --- a/coq/Environments.v +++ b/coq/Environments.v @@ -12,24 +12,25 @@ It is necessary to have this relation, since two evaluations of the very same expression may yield different values for different machine epsilons (or environments that already only approximate each other) **) -Inductive approxEnv : env -> analysisResult -> NatSet.t -> NatSet.t -> env -> Prop := +Inductive approxEnv : env -> (nat -> option mType) -> analysisResult -> NatSet.t -> NatSet.t -> env -> Prop := |approxRefl A: - approxEnv emptyEnv A NatSet.empty NatSet.empty emptyEnv -|approxUpdFree E1 E2 A v1 v2 x fVars dVars m: - approxEnv E1 A fVars dVars E2 -> + approxEnv emptyEnv (fun n => None) A NatSet.empty NatSet.empty emptyEnv +|approxUpdFree E1 E2 defVars A v1 v2 x fVars dVars m: + approxEnv E1 defVars A fVars dVars E2 -> + defVars x = Some m -> (Rabs (v1 - v2) <= (Rabs v1) * Q2R (meps m))%R -> NatSet.mem x (NatSet.union fVars dVars) = false -> - approxEnv (updEnv x M0 v1 E1) A (NatSet.add x fVars) dVars (updEnv x m v2 E2) -|approxUpdBound E1 E2 A v1 v2 x fVars dVars m: - approxEnv E1 A fVars dVars E2 -> + approxEnv (updEnv x v1 E1) defVars A (NatSet.add x fVars) dVars (updEnv x v2 E2) +|approxUpdBound E1 E2 defVars A v1 v2 x fVars dVars: + approxEnv E1 defVars A fVars dVars E2 -> (Rabs (v1 - v2) <= Q2R (snd (A (Var Q x))))%R -> NatSet.mem x (NatSet.union fVars dVars) = false -> - approxEnv (updEnv x M0 v1 E1) A fVars (NatSet.add x dVars) (updEnv x m v2 E2). + approxEnv (updEnv x v1 E1) defVars A fVars (NatSet.add x dVars) (updEnv x v2 E2). -Inductive approxParams :env -> env -> Prop := -|approxParamRefl: - approxParams emptyEnv emptyEnv -|approxParamUpd E1 E2 m x v1 v2 : - approxParams E1 E2 -> - (Rabs (v1 - v2) <= Q2R (meps m))%R -> - approxParams (updEnv x M0 v1 E1) (updEnv x m v2 E2). +(* Inductive approxParams :env -> env -> Prop := *) +(* |approxParamRefl: *) +(* approxParams emptyEnv emptyEnv *) +(* |approxParamUpd E1 E2 m x v1 v2 : *) +(* approxParams E1 E2 -> *) +(* (Rabs (v1 - v2) <= Q2R (meps m))%R -> *) +(* approxParams (updEnv x M0 v1 E1) (updEnv x m v2 E2). *) diff --git a/coq/ErrorBounds.v b/coq/ErrorBounds.v index 0324fa6..603f63a 100644 --- a/coq/ErrorBounds.v +++ b/coq/ErrorBounds.v @@ -8,7 +8,7 @@ Require Import Daisy.Infra.Abbrevs Daisy.Infra.RationalSimps Daisy.Infra.RealSim Require Import Daisy.Environments Daisy.Infra.ExpressionAbbrevs. Lemma const_abs_err_bounded (n:R) (nR:R) (nF:R) (E1 E2:env) (absenv:analysisResult) (m:mType) defVars: - eval_exp E1 defVars (Const M0 n) nR M0 -> + eval_exp E1 (toREvalVars defVars) (Const M0 n) nR M0 -> eval_exp E2 defVars (Const m n) nF m -> (Rabs (nR - nF) <= Rabs n * (Q2R (meps m)))%R. Proof. @@ -45,12 +45,12 @@ Qed. Lemma add_abs_err_bounded (e1:exp Q) (e1R:R) (e1F:R) (e2:exp Q) (e2R:R) (e2F:R) (vR:R) (vF:R) (E1 E2:env) (err1 err2 :Q) (m m1 m2:mType) defVars: - eval_exp E1 defVars (toREval (toRExp e1)) e1R M0 -> + eval_exp E1 (toREvalVars defVars) (toREval (toRExp e1)) e1R M0 -> eval_exp E2 defVars (toRExp e1) e1F m1-> - eval_exp E1 defVars (toREval (toRExp e2)) e2R M0 -> + eval_exp E1 (toREvalVars defVars) (toREval (toRExp e2)) e2R M0 -> eval_exp E2 defVars (toRExp e2) e2F m2 -> - eval_exp E1 defVars (toREval (Binop Plus (toRExp e1) (toRExp e2))) vR M0 -> - eval_exp (updEnv 2 m2 e2F (updEnv 1 m1 e1F emptyEnv)) defVars (Binop Plus (Var R 1) (Var R 2)) vF m-> + eval_exp E1 (toREvalVars defVars) (toREval (Binop Plus (toRExp e1) (toRExp e2))) vR M0 -> + eval_exp (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) (fun n => if (n =? 2) then Some m2 else if (n =? 1) then Some m1 else defVars n) (Binop Plus (Var R 1) (Var R 2)) vF m-> (Rabs (e1R - e1F) <= Q2R err1)%R -> (Rabs (e2R - e2F) <= Q2R err2)%R -> (Rabs (vR - vF) <= Q2R err1 + Q2R err2 + (Rabs (e1F + e2F) * (Q2R (meps m))))%R. @@ -110,12 +110,12 @@ Qed. **) Lemma subtract_abs_err_bounded (e1:exp Q) (e1R:R) (e1F:R) (e2:exp Q) (e2R:R) (e2F:R) (vR:R) (vF:R) (E1 E2:env) err1 err2 (m m1 m2:mType) defVars: - eval_exp E1 defVars (toREval (toRExp e1)) e1R M0 -> + eval_exp E1 (toREvalVars defVars) (toREval (toRExp e1)) e1R M0 -> eval_exp E2 defVars (toRExp e1) e1F m1 -> - eval_exp E1 defVars (toREval (toRExp e2)) e2R M0 -> + eval_exp E1 (toREvalVars defVars) (toREval (toRExp e2)) e2R M0 -> eval_exp E2 defVars (toRExp e2) e2F m2 -> - eval_exp E1 defVars (toREval (Binop Sub (toRExp e1) (toRExp e2))) vR M0 -> - eval_exp (updEnv 2 m2 e2F (updEnv 1 m1 e1F emptyEnv)) defVars (Binop Sub (Var R 1) (Var R 2)) vF m -> + eval_exp E1 (toREvalVars defVars) (toREval (Binop Sub (toRExp e1) (toRExp e2))) vR M0 -> + eval_exp (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) (fun n => if (n =? 2) then Some m2 else if (n =? 1) then Some m1 else defVars n) (Binop Sub (Var R 1) (Var R 2)) vF m -> (Rabs (e1R - e1F) <= Q2R err1)%R -> (Rabs (e2R - e2F) <= Q2R err2)%R -> (Rabs (vR - vF) <= Q2R err1 + Q2R err2 + ((Rabs (e1F - e2F)) * (Q2R (meps m))))%R. @@ -169,12 +169,12 @@ Qed. Lemma mult_abs_err_bounded (e1:exp Q) (e1R:R) (e1F:R) (e2:exp Q) (e2R:R) (e2F:R) (vR:R) (vF:R) (E1 E2:env) (m m1 m2:mType) defVars: - eval_exp E1 defVars (toREval (toRExp e1)) e1R M0 -> + eval_exp E1 (toREvalVars defVars) (toREval (toRExp e1)) e1R M0 -> eval_exp E2 defVars (toRExp e1) e1F m1 -> - eval_exp E1 defVars (toREval (toRExp e2)) e2R M0 -> + eval_exp E1 (toREvalVars defVars) (toREval (toRExp e2)) e2R M0 -> eval_exp E2 defVars (toRExp e2) e2F m2 -> - eval_exp E1 defVars (toREval (Binop Mult (toRExp e1) (toRExp e2))) vR M0 -> - eval_exp (updEnv 2 m2 e2F (updEnv 1 m1 e1F emptyEnv)) defVars (Binop Mult (Var R 1) (Var R 2)) vF m-> + eval_exp E1 (toREvalVars defVars) (toREval (Binop Mult (toRExp e1) (toRExp e2))) vR M0 -> + eval_exp (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) (fun n => if (n =? 2) then Some m2 else if (n =? 1) then Some m1 else defVars n) (Binop Mult (Var R 1) (Var R 2)) vF m-> (Rabs (vR - vF) <= Rabs (e1R * e2R - e1F * e2F) + Rabs (e1F * e2F) * (Q2R (meps m)))%R. Proof. intros e1_real e1_float e2_real e2_float mult_real mult_float. @@ -218,12 +218,12 @@ Qed. Lemma div_abs_err_bounded (e1:exp Q) (e1R:R) (e1F:R) (e2:exp Q) (e2R:R) (e2F:R) (vR:R) (vF:R) (E1 E2:env) (m m1 m2:mType) defVars: - eval_exp E1 defVars (toREval (toRExp e1)) e1R M0 -> + eval_exp E1 (toREvalVars defVars) (toREval (toRExp e1)) e1R M0 -> eval_exp E2 defVars (toRExp e1) e1F m1 -> - eval_exp E1 defVars (toREval (toRExp e2)) e2R M0 -> + eval_exp E1 (toREvalVars defVars) (toREval (toRExp e2)) e2R M0 -> eval_exp E2 defVars (toRExp e2) e2F m2 -> - eval_exp E1 defVars (toREval (Binop Div (toRExp e1) (toRExp e2))) vR M0 -> - eval_exp (updEnv 2 m2 e2F (updEnv 1 m1 e1F emptyEnv)) defVars (Binop Div (Var R 1) (Var R 2)) vF m -> + eval_exp E1 (toREvalVars defVars) (toREval (Binop Div (toRExp e1) (toRExp e2))) vR M0 -> + eval_exp (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) (fun n => if (n =? 2) then Some m2 else if (n =? 1) then Some m1 else defVars n) (Binop Div (Var R 1) (Var R 2)) vF m -> (Rabs (vR - vF) <= Rabs (e1R / e2R - e1F / e2F) + Rabs (e1F / e2F) * (Q2R (meps m)))%R. Proof. intros e1_real e1_float e2_real e2_float div_real div_float. @@ -443,9 +443,9 @@ Proof. Qed. Lemma round_abs_err_bounded (e:exp R) (nR nF1 nF:R) (E1 E2: env) (err:R) (machineEpsilon m:mType) defVars: - eval_exp E1 defVars (toREval e) nR M0 -> + eval_exp E1 (toREvalVars defVars) (toREval e) nR M0 -> eval_exp E2 defVars e nF1 m -> - eval_exp (updEnv 1 m nF1 emptyEnv) defVars (toRExp (Downcast machineEpsilon (Var Q 1))) nF machineEpsilon-> + eval_exp (updEnv 1 nF1 emptyEnv) (fun n => if n =? 1 then Some m else defVars n) (toRExp (Downcast machineEpsilon (Var Q 1))) nF machineEpsilon-> (Rabs (nR - nF1) <= err)%R -> (Rabs (nR - nF) <= err + (Rabs nF1) * Q2R (meps machineEpsilon))%R. Proof. diff --git a/coq/ErrorValidation.v b/coq/ErrorValidation.v index 7a823c7..ba835ab 100644 --- a/coq/ErrorValidation.v +++ b/coq/ErrorValidation.v @@ -109,28 +109,28 @@ Qed. Lemma validErrorboundCorrectVariable: forall E1 E2 absenv (v:nat) nR nF e nlo nhi P fVars dVars m Gamma defVars, typeCheck (Var Q v) defVars Gamma = true -> - approxEnv E1 absenv fVars dVars E2 -> - eval_exp E1 defVars (toREval (toRExp (Var Q v))) nR M0 -> + approxEnv E1 defVars absenv fVars dVars E2 -> + eval_exp E1 (toREvalVars defVars) (toREval (toRExp (Var Q v))) nR M0 -> eval_exp E2 defVars (toRExp (Var Q v)) nF m -> validIntervalbounds (Var Q v) absenv P dVars = true -> validErrorbound (Var Q v) Gamma absenv dVars = true -> (forall v1, NatSet.mem v1 dVars = true -> - exists r, E1 v1 = Some (r, M0) /\ + exists r, E1 v1 = Some r /\ (Q2R (fst (fst (absenv (Var Q v1)))) <= r <= Q2R (snd (fst (absenv (Var Q v1)))))%R) -> (forall v1, NatSet.mem v1 fVars= true -> - exists r, E1 v1 = Some (r, M0) /\ + exists r, E1 v1 = Some r /\ (Q2R (fst (P v1)) <= r <= Q2R (snd (P v1)))%R) -> absenv (Var Q v) = ((nlo, nhi), e) -> (Rabs (nR - nF) <= (Q2R e))%R. Proof. intros * typing_ok approxCEnv eval_real eval_float bounds_valid error_valid dVars_sound P_valid absenv_var. simpl in eval_real; inversion eval_real; inversion eval_float; subst. - rename H2 into E1_v; - rename H7 into E2_v. + rename H1 into E1_v; + rename H6 into E2_v. simpl in error_valid. rewrite absenv_var in error_valid; simpl in error_valid; subst. - case_eq (Gamma (Var Q m v)); intros; rewrite H in error_valid; [ | inversion error_valid]. + case_eq (Gamma (Var Q v)); intros; rewrite H in error_valid; [ | inversion error_valid]. rewrite <- andb_lazy_alt in error_valid. andb_to_prop error_valid. rename L into error_pos. @@ -159,17 +159,17 @@ Proof. apply Qle_Rle in error_valid. eapply Rle_trans; eauto. rewrite Q2R_mult. - inversion typing_ok; subst. - rewrite H in H5; inversion H5; subst. + rewrite H5 in H1; inversion H1; subst. + rewrite H,H5 in typing_ok; apply EquivEqBoolEq in typing_ok; subst. clear H5 H3. apply Rmult_le_compat_r. { apply inj_eps_posR. } { rewrite <- maxAbs_impl_RmaxAbs. apply contained_leq_maxAbs. unfold contained; simpl. - assert ((toRExp (Var Q m x)) = Var R m x) by (simpl; auto). - rewrite <- H2 in eval_float. - pose proof (validIntervalbounds_sound A P (E:=fun y : nat => if y =? x then Some (nR, M0) else E1 y) (vR:=nR) typing_ok bounds_valid (fVars := (NatSet.add x fVars))) as valid_bounds_prf. + assert ((toRExp (Var Q x)) = Var R x) by (simpl; auto). + rewrite <- H3 in eval_float. + pose proof (validIntervalbounds_sound (Var Q x) A P (E:=fun y : nat => if y =? x then Some nR else E1 y) (vR:=nR) defVars bounds_valid (fVars := (NatSet.add x fVars))) as valid_bounds_prf. rewrite absenv_var in valid_bounds_prf; simpl in valid_bounds_prf. apply valid_bounds_prf; try auto. - intros v v_mem_diff. @@ -180,9 +180,9 @@ Proof. + apply IHapproxCEnv; try auto. * constructor; auto. * constructor; auto. - * intros v0 m2 mem_dVars. - specialize (dVars_sound v0 m2 mem_dVars). - destruct dVars_sound as [vR0 [mR0 iv_sound_val]]. + * intros v0 mem_dVars. + specialize (dVars_sound v0 mem_dVars). + destruct dVars_sound as [vR0 iv_sound_val]. case_eq (v0 =? x); intros case_mem; rewrite case_mem in iv_sound_val; simpl in iv_sound_val. { rewrite Nat.eqb_eq in case_mem; subst. @@ -191,7 +191,7 @@ Proof. as x_in_union by (rewrite NatSet.union_spec; auto). rewrite <- NatSet.mem_spec in x_in_union; rewrite x_in_union in *; congruence. } - { exists vR0, mR0; split; auto; destruct iv_sound_val as [E1_v0 iv_sound_val]; auto. } + { exists vR0. split; auto; destruct iv_sound_val as [E1_v0 iv_sound_val]; auto. } * intros v0 v0_fVar. assert (NatSet.mem v0 (NatSet.add x fVars) = true) as v0_in_add by (rewrite NatSet.mem_spec, NatSet.add_spec; rewrite NatSet.mem_spec in v0_fVar; auto). @@ -237,16 +237,16 @@ Proof. + rewrite <- NatSet.mem_spec in v_dVar. rewrite v_dVar in case_dVars. inversion case_dVars. } { rewrite not_in_add in error_valid; auto. } - * intros v0 m2 mem_dVars. - specialize (dVars_sound v0 m2). + * intros v0 mem_dVars. + specialize (dVars_sound v0). rewrite absenv_var in *; simpl in *. rewrite NatSet.mem_spec in mem_dVars. assert (NatSet.In v0 (NatSet.add x dVars)) as v0_in_add. { rewrite NatSet.add_spec. right; auto. } { rewrite <- NatSet.mem_spec in v0_in_add. specialize (dVars_sound v0_in_add). - destruct dVars_sound as [vR0 [mR0 [val_def iv_sound_val]]]. - exists vR0, mR0; split; auto. + destruct dVars_sound as [vR0 [val_def iv_sound_val]]. + exists vR0; split; auto. unfold updEnv in val_def; simpl in val_def. case_eq (v0 =? x); intros case_mem; rewrite case_mem in val_def; simpl in val_def. @@ -268,10 +268,10 @@ Proof. Qed. Lemma validErrorboundCorrectConstant: - forall E1 E2 absenv (n:Q) nR nF e nlo nhi dVars m Gamma, - eval_exp E1 (toREval (toRExp (Const m n))) nR M0 -> - eval_exp E2 (toRExp (Const m n)) nF m -> - validType Gamma (Const m n) m -> + forall E1 E2 absenv (n:Q) nR nF e nlo nhi dVars m Gamma defVars, + eval_exp E1 (toREvalVars defVars) (toREval (toRExp (Const m n))) nR M0 -> + eval_exp E2 defVars (toRExp (Const m n)) nF m -> + typeCheck (Const m n) defVars Gamma = true -> validErrorbound (Const m n) Gamma absenv dVars = true -> (Q2R nlo <= nR <= Q2R nhi)%R -> absenv (Const m n) = ((nlo,nhi),e) -> @@ -299,20 +299,22 @@ Proof. - rewrite Q2R_mult in error_valid. rewrite <- maxAbs_impl_RmaxAbs in error_valid; auto. inversion subexpr_ok; subst. - rewrite H in H6; inversion H6; subst; auto. + rewrite H in H4. apply EquivEqBoolEq in H4; subst; auto. Qed. Lemma validErrorboundCorrectAddition E1 E2 absenv (e1:exp Q) (e2:exp Q) (nR nR1 nR2 nF nF1 nF2 :R) (e err1 err2 :error) - (alo ahi e1lo e1hi e2lo e2hi:Q) dVars m m1 m2 Gamma: + (alo ahi e1lo e1hi e2lo e2hi:Q) dVars m m1 m2 Gamma defVars: m = computeJoin m1 m2 -> - eval_exp E1 (toREval (toRExp e1)) nR1 M0 -> - eval_exp E1 (toREval (toRExp e2)) nR2 M0 -> - eval_exp E1 (toREval (toRExp (Binop Plus e1 e2))) nR M0 -> - eval_exp E2 (toRExp e1) nF1 m1 -> - eval_exp E2 (toRExp e2) nF2 m2 -> - eval_exp (updEnv 2 m2 nF2 (updEnv 1 m1 nF1 emptyEnv)) (toRExp (Binop Plus (Var Q m1 1) (Var Q m2 2))) nF m -> - validType Gamma (Binop Plus e1 e2) m -> + eval_exp E1 (toREvalVars defVars) (toREval (toRExp e1)) nR1 M0 -> + eval_exp E1 (toREvalVars defVars) (toREval (toRExp e2)) nR2 M0 -> + eval_exp E1 (toREvalVars defVars) (toREval (toRExp (Binop Plus e1 e2))) nR M0 -> + eval_exp E2 defVars (toRExp e1) nF1 m1 -> + eval_exp E2 defVars (toRExp e2) nF2 m2 -> + eval_exp (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv)) + (fun n => if (n =? 2) then Some m2 else if (n =? 1) then Some m1 else defVars n) + (toRExp (Binop Plus (Var Q 1) (Var Q 2))) nF m -> + typeCheck (Binop Plus e1 e2) defVars Gamma = true -> validErrorbound (Binop Plus e1 e2) Gamma absenv dVars = true -> (Q2R e1lo <= nR1 <= Q2R e1hi)%R -> (Q2R e2lo <= nR2 <= Q2R e2hi)%R -> @@ -333,9 +335,17 @@ Proof. unfold validErrorbound in valid_error. rewrite absenv_add,absenv_e1,absenv_e2 in valid_error. case_eq (Gamma (Binop Plus e1 e2)); intros; rewrite H in valid_error; [ | inversion valid_error ]. - inversion subexpr_ok; subst. rewrite H in H7; inversion H7; subst. clear m4 m5 H3 H4 H7 H6. + simpl in subexpr_ok; rewrite H in subexpr_ok. + case_eq (Gamma e1); intros; rewrite H0 in subexpr_ok; [ | inversion subexpr_ok ]. + case_eq (Gamma e2); intros; rewrite H1 in subexpr_ok; [ | inversion subexpr_ok ]. + andb_to_prop subexpr_ok. + apply EquivEqBoolEq in L0; subst. + pose proof (typingSoundnessExp _ _ R0 e1_float). + pose proof (typingSoundnessExp _ _ R e2_float). + rewrite H0 in H2; rewrite H1 in H3; inversion H2; inversion H3; subst. + clear H2 H3 H0 H1. andb_to_prop valid_error. - rename R0 into valid_error. + rename R2 into valid_error. eapply Rle_trans. apply Rplus_le_compat_l. eapply Rmult_le_compat_r. @@ -378,15 +388,17 @@ Qed. Lemma validErrorboundCorrectSubtraction E1 E2 absenv (e1:exp Q) (e2:exp Q) (nR nR1 nR2 nF nF1 nF2 :R) (e err1 err2 :error) - (alo ahi e1lo e1hi e2lo e2hi:Q) dVars (m m1 m2:mType) Gamma: + (alo ahi e1lo e1hi e2lo e2hi:Q) dVars (m m1 m2:mType) Gamma defVars: m = computeJoin m1 m2 -> - eval_exp E1 (toREval (toRExp e1)) nR1 M0 -> - eval_exp E1 (toREval (toRExp e2)) nR2 M0 -> - eval_exp E1 (toREval (toRExp (Binop Sub e1 e2))) nR M0 -> - eval_exp E2 (toRExp e1) nF1 m1-> - eval_exp E2 (toRExp e2) nF2 m2 -> - eval_exp (updEnv 2 m2 nF2 (updEnv 1 m1 nF1 emptyEnv)) (toRExp (Binop Sub (Var Q m1 1) (Var Q m2 2))) nF m -> - validType Gamma (Binop Sub e1 e2) m -> + eval_exp E1 (toREvalVars defVars) (toREval (toRExp e1)) nR1 M0 -> + eval_exp E1 (toREvalVars defVars) (toREval (toRExp e2)) nR2 M0 -> + eval_exp E1 (toREvalVars defVars) (toREval (toRExp (Binop Sub e1 e2))) nR M0 -> + eval_exp E2 defVars (toRExp e1) nF1 m1-> + eval_exp E2 defVars (toRExp e2) nF2 m2 -> + eval_exp (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv)) + (fun n => if (n =? 2) then Some m2 else if (n =? 1) then Some m1 else defVars n) + (toRExp (Binop Sub (Var Q 1) (Var Q 2))) nF m -> + typeCheck (Binop Sub e1 e2) defVars Gamma = true -> validErrorbound (Binop Sub e1 e2) Gamma absenv dVars = true -> (Q2R e1lo <= nR1 <= Q2R e1hi)%R -> (Q2R e2lo <= nR2 <= Q2R e2hi)%R -> @@ -405,9 +417,17 @@ Proof. unfold validErrorbound in valid_error. rewrite absenv_sub,absenv_e1,absenv_e2 in valid_error. case_eq (Gamma (Binop Sub e1 e2)); intros; rewrite H in valid_error; [ | inversion valid_error ]. - inversion subexpr_ok; subst. rewrite H in H7; inversion H7; subst. clear m4 m5 H3 H4 H7 H6. + simpl in subexpr_ok; rewrite H in subexpr_ok. + case_eq (Gamma e1); intros; rewrite H0 in subexpr_ok; [ | inversion subexpr_ok ]. + case_eq (Gamma e2); intros; rewrite H1 in subexpr_ok; [ | inversion subexpr_ok ]. + andb_to_prop subexpr_ok. + apply EquivEqBoolEq in L0; subst. + pose proof (typingSoundnessExp _ _ R0 e1_float). + pose proof (typingSoundnessExp _ _ R e2_float). + rewrite H0 in H2; rewrite H1 in H3; inversion H2; inversion H3; subst. + clear H2 H3 H0 H1. andb_to_prop valid_error. - rename R0 into valid_error. + rename R2 into valid_error. apply Qle_bool_iff in valid_error. apply Qle_Rle in valid_error. repeat rewrite Q2R_plus in valid_error. @@ -455,15 +475,17 @@ Qed. Lemma validErrorboundCorrectMult E1 E2 absenv (e1:exp Q) (e2:exp Q) (nR nR1 nR2 nF nF1 nF2 :R) (e err1 err2 :error) - (alo ahi e1lo e1hi e2lo e2hi:Q) dVars (m m1 m2:mType) Gamma: + (alo ahi e1lo e1hi e2lo e2hi:Q) dVars (m m1 m2:mType) Gamma defVars: m = computeJoin m1 m2 -> - eval_exp E1 (toREval (toRExp e1)) nR1 M0 -> - eval_exp E1 (toREval (toRExp e2)) nR2 M0 -> - eval_exp E1 (toREval (toRExp (Binop Mult e1 e2))) nR M0 -> - eval_exp E2 (toRExp e1) nF1 m1 -> - eval_exp E2 (toRExp e2) nF2 m2 -> - eval_exp (updEnv 2 m2 nF2 (updEnv 1 m1 nF1 emptyEnv)) (toRExp (Binop Mult (Var Q m1 1) (Var Q m2 2))) nF m -> - validType Gamma (Binop Mult e1 e2) m -> + eval_exp E1 (toREvalVars defVars) (toREval (toRExp e1)) nR1 M0 -> + eval_exp E1 (toREvalVars defVars) (toREval (toRExp e2)) nR2 M0 -> + eval_exp E1 (toREvalVars defVars) (toREval (toRExp (Binop Mult e1 e2))) nR M0 -> + eval_exp E2 defVars (toRExp e1) nF1 m1 -> + eval_exp E2 defVars (toRExp e2) nF2 m2 -> + eval_exp (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv)) + (fun n => if (n =? 2) then Some m2 else if (n =? 1) then Some m1 else defVars n) + (toRExp (Binop Mult (Var Q 1) (Var Q 2))) nF m -> + typeCheck (Binop Mult e1 e2) defVars Gamma = true -> validErrorbound (Binop Mult e1 e2) Gamma absenv dVars = true -> (Q2R e1lo <= nR1 <= Q2R e1hi)%R -> (Q2R e2lo <= nR2 <= Q2R e2hi)%R -> @@ -482,9 +504,17 @@ Proof. unfold validErrorbound in valid_error. rewrite absenv_mult,absenv_e1,absenv_e2 in valid_error. case_eq (Gamma (Binop Mult e1 e2)); intros; rewrite H in valid_error; [ | inversion valid_error ]. - inversion subexpr_ok; subst. rewrite H in H7; inversion H7; subst. clear m4 m5 H3 H4 H7 H6. + simpl in subexpr_ok; rewrite H in subexpr_ok. + case_eq (Gamma e1); intros; rewrite H0 in subexpr_ok; [ | inversion subexpr_ok ]. + case_eq (Gamma e2); intros; rewrite H1 in subexpr_ok; [ | inversion subexpr_ok ]. + andb_to_prop subexpr_ok. + apply EquivEqBoolEq in L0; subst. + pose proof (typingSoundnessExp _ _ R0 e1_float). + pose proof (typingSoundnessExp _ _ R e2_float). + rewrite H0 in H2; rewrite H1 in H3; inversion H2; inversion H3; subst. + clear H2 H3 H0 H1. andb_to_prop valid_error. - rename R0 into valid_error. + rename R2 into valid_error. assert (0 <= Q2R err1)%R as err1_pos by (eapply (err_always_positive e1 Gamma absenv dVars); eauto). assert (0 <= Q2R err2)%R as err2_pos by (eapply (err_always_positive e2 Gamma absenv dVars); eauto). clear R L1. @@ -985,15 +1015,17 @@ Qed. Lemma validErrorboundCorrectDiv E1 E2 absenv (e1:exp Q) (e2:exp Q) (nR nR1 nR2 nF nF1 nF2 :R) (e err1 err2 :error) - (alo ahi e1lo e1hi e2lo e2hi:Q) dVars (m m1 m2:mType) Gamma: + (alo ahi e1lo e1hi e2lo e2hi:Q) dVars (m m1 m2:mType) Gamma defVars: m = computeJoin m1 m2 -> - eval_exp E1 (toREval (toRExp e1)) nR1 M0 -> - eval_exp E1 (toREval (toRExp e2)) nR2 M0 -> - eval_exp E1 (toREval (toRExp (Binop Div e1 e2))) nR M0 -> - eval_exp E2 (toRExp e1) nF1 m1 -> - eval_exp E2 (toRExp e2) nF2 m2 -> - eval_exp (updEnv 2 m2 nF2 (updEnv 1 m1 nF1 emptyEnv)) (toRExp (Binop Div (Var Q m1 1) (Var Q m2 2))) nF m -> - validType Gamma (Binop Div e1 e2) m -> + eval_exp E1 (toREvalVars defVars) (toREval (toRExp e1)) nR1 M0 -> + eval_exp E1 (toREvalVars defVars) (toREval (toRExp e2)) nR2 M0 -> + eval_exp E1 (toREvalVars defVars) (toREval (toRExp (Binop Div e1 e2))) nR M0 -> + eval_exp E2 defVars (toRExp e1) nF1 m1 -> + eval_exp E2 defVars (toRExp e2) nF2 m2 -> + eval_exp (updEnv 2 nF2 (updEnv 1 nF1 emptyEnv)) + (fun n => if (n =? 2) then Some m2 else if (n =? 1) then Some m1 else defVars n) + (toRExp (Binop Div (Var Q 1) (Var Q 2))) nF m -> + typeCheck (Binop Div e1 e2) defVars Gamma = true -> validErrorbound (Binop Div e1 e2) Gamma absenv dVars = true -> (Q2R e1lo <= nR1 <= Q2R e1hi)%R -> (Q2R e2lo <= nR2 <= Q2R e2hi)%R -> @@ -1013,13 +1045,17 @@ Proof. unfold validErrorbound in valid_error. rewrite absenv_div,absenv_e1,absenv_e2 in valid_error. case_eq (Gamma (Binop Div e1 e2)); intros; rewrite H in valid_error; [ | inversion valid_error ]. - inversion subexpr_ok; subst. rewrite H in H7; inversion H7; subst. clear m4 m5 H3 H4 H7 H6. - rename H into type_binop. + simpl in subexpr_ok; rewrite H in subexpr_ok. + case_eq (Gamma e1); intros; rewrite H0 in subexpr_ok; [ | inversion subexpr_ok ]. + case_eq (Gamma e2); intros; rewrite H1 in subexpr_ok; [ | inversion subexpr_ok ]. + andb_to_prop subexpr_ok. + apply EquivEqBoolEq in L0; subst. + pose proof (typingSoundnessExp _ _ R0 e1_float). + pose proof (typingSoundnessExp _ _ R e2_float). + rewrite H0 in H2; rewrite H1 in H3; inversion H2; inversion H3; subst. + clear H2 H3 H0 H1. andb_to_prop valid_error. - assert (validErrorbound e1 Gamma absenv dVars = true) as valid_err_e1 by auto; - assert (validErrorbound e2 Gamma absenv dVars = true) as valid_err_e2 by auto. - clear L1 R. - rename R1 into valid_error. + rename R3 into valid_error. rename L0 into no_div_zero_float. assert (contained nR1 (Q2R e1lo, Q2R e1hi)) as contained_intv1 by auto. pose proof (distance_gives_iv (a:=nR1) _ contained_intv1 err1_bounded). @@ -1050,7 +1086,7 @@ Proof. (* Error Propagation proof *) + clear absenv_e1 absenv_e2 valid_error eval_float eval_real e1_float e1_real e2_float e2_real absenv_div - valid_err_e1 valid_err_e2 E1 E2 absenv alo ahi nR nF e1 e2 e L subexpr_ok type_binop. + E1 E2 alo ahi nR nF e L. unfold IntervalArith.contained, widenInterval in *. simpl in *. rewrite Q2R_plus, Q2R_minus in no_div_zero_float. @@ -1087,7 +1123,7 @@ Proof. rewrite <- Q2R_plus in float_iv_neg. rewrite <- Q2R0_is_0 in float_iv_neg. rewrite <- Q2R0_is_0 in real_iv_neg. - pose proof (err_prop_inversion_neg float_iv_neg real_iv_neg err2_bounded valid_bounds_e2 H0 err2_pos) as err_prop_inv. + pose proof (err_prop_inversion_neg float_iv_neg real_iv_neg err2_bounded valid_bounds_e2 H1 err2_pos) as err_prop_inv. rewrite Q2R_plus in float_iv_neg. rewrite Q2R0_is_0 in float_iv_neg. rewrite Q2R0_is_0 in real_iv_neg. @@ -1526,7 +1562,7 @@ Proof. rewrite <- Q2R_minus in float_iv_pos. rewrite <- Q2R0_is_0 in float_iv_pos. rewrite <- Q2R0_is_0 in real_iv_pos. - pose proof (err_prop_inversion_pos float_iv_pos real_iv_pos err2_bounded valid_bounds_e2 H0 err2_pos) as err_prop_inv. + pose proof (err_prop_inversion_pos float_iv_pos real_iv_pos err2_bounded valid_bounds_e2 H1 err2_pos) as err_prop_inv. rewrite Q2R_minus in float_iv_pos. rewrite Q2R0_is_0 in float_iv_pos. rewrite Q2R0_is_0 in real_iv_pos. @@ -1848,20 +1884,20 @@ Proof. assert (IVhi (widenInterval (Q2R e2lo, Q2R e2hi) (Q2R err2)) < 0 \/ 0 < IVlo (widenInterval (Q2R e2lo, Q2R e2hi) (Q2R err2)))%R as no_div_zero_widen by (unfold widenInterval in *; simpl in *; rewrite Q2R_plus, Q2R_minus in no_div_zero_float; auto). - pose proof (IntervalArith.interval_division_valid no_div_zero_widen H H0) as valid_div_float. + pose proof (IntervalArith.interval_division_valid no_div_zero_widen H0 H1) as valid_div_float. unfold IntervalArith.contained, widenInterval in *; simpl in *. assert (e2lo - err2 == 0 -> False). * hnf; intros. destruct no_div_zero_float as [float_iv | float_iv]; rewrite <- Q2R0_is_0 in float_iv; apply Rlt_Qlt in float_iv; try lra. assert (Q2R e2lo - Q2R err2 <= Q2R e2hi + Q2R err2)%R by lra. - rewrite<- Q2R_minus, <- Q2R_plus in H4. - apply Rle_Qle in H4. lra. + rewrite<- Q2R_minus, <- Q2R_plus in H5. + apply Rle_Qle in H5. lra. * assert (e2hi + err2 == 0 -> False). { hnf; intros. destruct no_div_zero_float as [float_iv | float_iv]; rewrite <- Q2R0_is_0 in float_iv; apply Rlt_Qlt in float_iv; try lra. assert (Q2R e2lo - Q2R err2 <= Q2R e2hi + Q2R err2)%R by lra. - rewrite<- Q2R_minus, <- Q2R_plus in H5. - apply Rle_Qle in H5. lra. } + rewrite<- Q2R_minus, <- Q2R_plus in H6. + apply Rle_Qle in H6. lra. } { destruct valid_div_float. unfold RmaxAbsFun. apply Rmult_le_compat_r. @@ -1884,36 +1920,36 @@ Proof. + hnf; intros. destruct no_div_zero_float as [float_iv | float_iv]; try lra. assert (Q2R e2lo - Q2R err2 <= Q2R e2hi + Q2R err2)%R by lra. - rewrite<- Q2R_minus, <- Q2R_plus in H2. - apply Rle_Qle in H2. lra. + rewrite<- Q2R_minus, <- Q2R_plus in H3. + apply Rle_Qle in H3. lra. + assert (e2hi + err2 == 0 -> False). * hnf; intros. destruct no_div_zero_float as [float_iv | float_iv]; try lra. assert (Q2R e2lo - Q2R err2 <= Q2R e2hi + Q2R err2)%R by lra. - rewrite<- Q2R_minus, <- Q2R_plus in H3. - apply Rle_Qle in H3. lra. + rewrite<- Q2R_minus, <- Q2R_plus in H4. + apply Rle_Qle in H4. lra. * unfold widenIntv; simpl. hnf. intros. assert (forall a, Qabs a == 0 -> a == 0). - { intros. unfold Qabs in H4. destruct a. - rewrite <- Z.abs_0 in H4. inversion H4. rewrite Zmult_1_r in *. - rewrite Z.abs_0_iff in H6. - rewrite H6. rewrite Z.abs_0. hnf. simpl; auto. } + { intros. unfold Qabs in H5. destruct a. + rewrite <- Z.abs_0 in H5. inversion H5. rewrite Zmult_1_r in *. + rewrite Z.abs_0_iff in H7. + rewrite H7. rewrite Z.abs_0. hnf. simpl; auto. } { assert (minAbs (e2lo - err2, e2hi + err2) == 0 -> False). - unfold minAbs. unfold fst, snd. apply Q.min_case_strong. - + intros. apply H6; rewrite H5; auto. - + intros. apply H1. rewrite (H4 (e2lo-err2) H6). hnf. auto. - + intros. apply H2. rewrite H4; auto. hnf; auto. - - rewrite <- (Qmult_0_l (minAbs (e2lo - err2, e2hi + err2))) in H3. - rewrite (Qmult_inj_r) in H3; auto. } + + intros. apply H7; rewrite H6; auto. + + intros. apply H2. rewrite (H5 (e2lo-err2) H7). hnf. auto. + + intros. apply H3. rewrite H5; auto. hnf; auto. + - rewrite <- (Qmult_0_l (minAbs (e2lo - err2, e2hi + err2))) in H4. + rewrite (Qmult_inj_r) in H4; auto. } Qed. -Lemma validErrorboundCorrectRounding E1 E2 absenv (e: exp Q) (nR nF nF1: R) (err err':error) (elo ehi alo ahi: Q) dVars (m: mType) (machineEpsilon:mType) Gamma: - eval_exp E1 (toREval (toRExp e)) nR M0 -> - eval_exp E2 (toRExp e) nF1 m -> - eval_exp (updEnv 1 m nF1 emptyEnv) (toRExp (Downcast machineEpsilon (Var Q m 1))) nF machineEpsilon -> - validType Gamma (Downcast machineEpsilon e) machineEpsilon -> +Lemma validErrorboundCorrectRounding E1 E2 absenv (e: exp Q) (nR nF nF1: R) (err err':error) (elo ehi alo ahi: Q) dVars (m: mType) (machineEpsilon:mType) Gamma defVars: + eval_exp E1 (toREvalVars defVars) (toREval (toRExp e)) nR M0 -> + eval_exp E2 defVars (toRExp e) nF1 m -> + eval_exp (updEnv 1 nF1 emptyEnv) (fun n => if n =? 1 then Some m else defVars n) (toRExp (Downcast machineEpsilon (Var Q 1))) nF machineEpsilon -> + typeCheck (Downcast machineEpsilon e) defVars Gamma = true -> validErrorbound (Downcast machineEpsilon e) Gamma absenv dVars = true -> (Q2R elo <= nR <= Q2R ehi)%R -> absenv e = ((elo, ehi), err) -> @@ -1926,8 +1962,11 @@ Proof. rewrite absenv_rnd in valid_error. rewrite absenv_e in valid_error. case_eq (Gamma (Downcast machineEpsilon e)); intros; rewrite H in valid_error; [ | inversion valid_error ]. - inversion subexpr_ok; subst. rewrite H in H5; inversion H5; symmetry in H5; subst. clear m2 H2 H3 H5. - andb_to_prop valid_error. + simpl in subexpr_ok; rewrite H in subexpr_ok. + case_eq (Gamma e); intros; rewrite H0 in subexpr_ok; [ | inversion subexpr_ok ]. + andb_to_prop subexpr_ok. + apply EquivEqBoolEq in L0; subst. + andb_to_prop valid_error. simpl in *. eapply Rle_trans. eapply round_abs_err_bounded; eauto. @@ -1935,7 +1974,7 @@ Proof. pose proof (distance_gives_iv _ valid_intv_c err_bounded) as dgi. unfold IntervalArith.contained in dgi. destruct dgi as [dgi1 dgi2]; simpl in dgi1; simpl in dgi2. - apply (Rle_trans _ (Q2R err + Q2R (maxAbs (widenIntv (elo, ehi) err)) * Q2R (meps machineEpsilon)) _). + apply (Rle_trans _ (Q2R err + Q2R (maxAbs (widenIntv (elo, ehi) err)) * Q2R (meps m0)) _). + apply Rplus_le_compat_l. apply Rmult_le_compat_r. * rewrite <- Q2R0_is_0. @@ -1951,30 +1990,30 @@ Proof. rewrite Q2R_minus. rewrite Q2R_plus. split; assumption. - + apply Qle_bool_iff in R0. + + apply Qle_bool_iff in R2. rewrite <- Q2R_mult. rewrite <- Q2R_plus. apply Qle_Rle. assumption. Qed. -Lemma test E e v m m' Gamma: - eval_exp E (toRExp e) v m -> - validType Gamma e m' -> - m = m'. -Proof. - revert v m m'; induction e; intros * eval_e vt_e. - - inversion eval_e; subst; inversion vt_e; subst; auto. - - inversion eval_e; subst; inversion vt_e; subst; auto. - - inversion vt_e; subst; auto; inversion eval_e; subst. - + eapply IHe; eauto. - + eapply IHe; eauto. - - inversion vt_e; subst; inversion eval_e; subst; try auto. - assert (m0 = m1) by (eapply IHe1; eauto). - assert (m3 = m2) by (eapply IHe2; eauto). - subst; simpl; auto. - - inversion vt_e; subst; inversion eval_e; subst; auto. -Qed. +(* Lemma test E e v m m' Gamma: *) +(* eval_exp E (toRExp e) v m -> *) +(* validType Gamma e m' -> *) +(* m = m'. *) +(* Proof. *) +(* revert v m m'; induction e; intros * eval_e vt_e. *) +(* - inversion eval_e; subst; inversion vt_e; subst; auto. *) +(* - inversion eval_e; subst; inversion vt_e; subst; auto. *) +(* - inversion vt_e; subst; auto; inversion eval_e; subst. *) +(* + eapply IHe; eauto. *) +(* + eapply IHe; eauto. *) +(* - inversion vt_e; subst; inversion eval_e; subst; try auto. *) +(* assert (m0 = m1) by (eapply IHe1; eauto). *) +(* assert (m3 = m2) by (eapply IHe2; eauto). *) +(* subst; simpl; auto. *) +(* - inversion vt_e; subst; inversion eval_e; subst; auto. *) +(* Qed. *) (** Soundness theorem for the error bound validator. @@ -1982,19 +2021,19 @@ Qed. Each case requires the application of one of the soundness lemmata proven before **) Theorem validErrorbound_sound (e:exp Q): - forall E1 E2 fVars dVars absenv nR nF err P elo ehi m Gamma, - validType Gamma e m -> - approxEnv E1 absenv fVars dVars E2 -> + forall E1 E2 fVars dVars absenv nR nF err P elo ehi m Gamma defVars, + typeCheck e defVars Gamma = true -> + approxEnv E1 defVars absenv fVars dVars E2 -> NatSet.Subset (NatSet.diff (Expressions.usedVars e) dVars) fVars -> - eval_exp E1 (toREval (toRExp e)) nR M0 -> - eval_exp E2 (toRExp e) nF m -> + eval_exp E1 (toREvalVars defVars) (toREval (toRExp e)) nR M0 -> + eval_exp E2 defVars (toRExp e) nF m -> validErrorbound e Gamma absenv dVars = true -> validIntervalbounds e absenv P dVars = true -> - (forall v1 m1, NatSet.mem v1 dVars = true -> - exists vr mv1, E1 v1 = Some (vr, M0) /\ Gamma (Var Q mv1 v1) = Some m1 /\ - (Q2R (fst (fst (absenv (Var Q m1 v1)))) <= vr <= Q2R (snd (fst (absenv (Var Q m1 v1)))))%R) -> + (forall v1, NatSet.mem v1 dVars = true -> + exists vr, E1 v1 = Some vr /\ + (Q2R (fst (fst (absenv (Var Q v1)))) <= vr <= Q2R (snd (fst (absenv (Var Q v1)))))%R) -> (forall v, NatSet.mem v fVars= true -> - exists vR, E1 v = Some (vR, M0) /\ + exists vR, E1 v = Some vR /\ (Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) -> absenv e = ((elo,ehi),err) -> (Rabs (nR - nF) <= (Q2R err))%R. @@ -2004,23 +2043,28 @@ Proof. - inversion typing_ok; subst. eapply validErrorboundCorrectVariable; try eauto. - inversion typing_ok; subst. + case_eq (Gamma (Const m v)); intros; rewrite H in H0; [ | inversion H0 ]. + apply EquivEqBoolEq in H0; subst. + assert (eval_exp E2 defVars (toRExp (Const m1 v)) nF m1) by + (inversion eval_float; subst; econstructor; eauto). eapply validErrorboundCorrectConstant; eauto. + simpl in valid_intv. rewrite absenv_eq in valid_intv. simpl in eval_real; inversion eval_real; subst. - simpl in H3; rewrite Q2R0_is_0 in H3. + simpl in H4; rewrite Q2R0_is_0 in H4. rewrite delta_0_deterministic; auto. unfold isSupersetIntv in valid_intv; apply andb_true_iff in valid_intv; destruct valid_intv. simpl in H,H0. split; auto. - * apply Qle_bool_iff in H. apply (Qle_Rle _ _ H). - * apply Qle_bool_iff in H0. apply (Qle_Rle _ _ H0). + * apply Qle_bool_iff in H1. apply (Qle_Rle _ _ H1). + * apply Qle_bool_iff in H2. apply (Qle_Rle _ _ H2). - unfold validErrorbound in valid_error. rewrite absenv_eq in valid_error. case_eq (Gamma (Unop u e)); intros; rewrite H in valid_error; [ | inversion valid_error ]. andb_to_prop valid_error. inversion R. - - pose proof (ivbounds_approximatesPrecond_sound (f:=(Binop b e1 e2)) absenv P (Gamma:=Gamma) valid_intv) as env_approx_p. + - pose proof (ivbounds_approximatesPrecond_sound (Binop b e1 e2) absenv P valid_intv) as env_approx_p. + assert (typing_copy := typing_ok). assert (valid_error_copy := valid_error). simpl in valid_error. env_assert absenv e1 absenv_e1. @@ -2035,24 +2079,40 @@ Proof. rewrite iv_e2 in absenv_e2. rewrite absenv_eq, absenv_e1, absenv_e2 in valid_error. case_eq (Gamma (Binop b e1 e2)); intros; rewrite H in valid_error; [ | inversion valid_error ]. - assert(m0 = m) by (inversion typing_ok; subst; rewrite H in H7; inversion H7; subst; auto); subst. + simpl in typing_ok. rewrite H in typing_ok. + case_eq (Gamma e1); intros; rewrite H0 in typing_ok; [ | inversion typing_ok ]. + case_eq (Gamma e2); intros; rewrite H1 in typing_ok; [ | inversion typing_ok ]. + andb_to_prop typing_ok. apply EquivEqBoolEq in L0; subst. andb_to_prop valid_error. simpl in valid_intv. rewrite absenv_eq, absenv_e1, absenv_e2 in valid_intv. andb_to_prop valid_intv. inversion eval_real; subst. + destruct m0; destruct m3; inversion H5; clear H5. + + (* inversion eval_float; subst. *) + (* rename v0 into vF1. *) + (* rename v3 into vF2. *) + (* pose proof (validIntervalbounds_sound e1 absenv P (vR:=v1) defVars L2 valid_dVars (fVars:=fVars)) *) + (* as valid_bounds_e1. *) + (* rewrite absenv_e1 in valid_bounds_e1. *) + (* pose proof (validIntervalbounds_sound e2 absenv P (vR:=v2) defVars R4 valid_dVars (fVars:=fVars)) *) + (* as valid_bounds_e2. *) + (* rewrite absenv_e2 in valid_bounds_e2; *) + (* simpl in *. *) + (* rewrite Q2R0_is_0 in H6; apply Rabs_0_impl_eq in H6; subst. *) + (* unfold perturb; simpl. *) + (* assert (Rabs (v1 - vF1) <= Q2R err1 /\ Rabs (v2 - vF2) <= Q2R err2)%R. *) + + + apply binary_unfolding in eval_float. destruct eval_float as [vF1 [vF2 [ mF1 [mF2 [joinF12 [eval_e1 [eval_e2 eval_float ]]]]]]]. simpl in *. - destruct m1; destruct m2; inversion H3. - inversion typing_ok; subst. - assert (mF1 = m1) as m1eq by (eapply test; eauto). - assert (mF2 = m2) as m2eq by (eapply test; eauto). - symmetry in m1eq,m2eq; subst. - pose proof (validIntervalbounds_sound absenv P (vR:=v1) H5 L2 valid_dVars (fVars:=fVars)) + pose proof (validIntervalbounds_sound e1 absenv P (vR:=v1) defVars L2 valid_dVars (fVars:=fVars)) as valid_bounds_e1. rewrite absenv_e1 in valid_bounds_e1. - pose proof (validIntervalbounds_sound absenv P (vR:=v2) H9 R2 valid_dVars (fVars:=fVars)) + pose proof (validIntervalbounds_sound e2 absenv P (vR:=v2) defVars R4 valid_dVars (fVars:=fVars)) as valid_bounds_e2. rewrite absenv_e2 in valid_bounds_e2; simpl in *. @@ -2088,16 +2148,17 @@ Proof. apply fVars_subset. rewrite NatSet.diff_spec, NatSet.union_spec. split; try auto. } - * destruct H0, H1, H. destruct b. + * destruct H2, H3. destruct b. { eapply (validErrorboundCorrectAddition (e1:=e1) absenv); eauto. - simpl; apply valid_error_copy. (*TODO: something cleaner... *) } + simpl; apply valid_error_copy. } { eapply (validErrorboundCorrectSubtraction (e1:=e1) absenv); eauto. simpl; apply valid_error_copy. } { eapply (validErrorboundCorrectMult (e1 := e1) absenv); eauto. simpl; apply valid_error_copy. } { eapply (validErrorboundCorrectDiv (e1 := e1) absenv); eauto. - simpl; apply valid_error_copy. - - case_eq (Qleb ivhi2 0 && negb (Qeq_bool ivhi2 0) || Qleb 0 ivlo2 && negb (Qeq_bool ivlo2 0)); intros; rewrite H in R1; inversion R1. + - case_eq (Qleb ivhi2 0 && negb (Qeq_bool ivhi2 0) || Qleb 0 ivlo2 && negb (Qeq_bool ivlo2 0)); intros; + rewrite H7 in R3; inversion R3. auto. } - unfold validErrorbound in valid_error. rewrite absenv_eq in valid_error. @@ -2109,7 +2170,7 @@ Proof. andb_to_prop valid_intv. inversion eval_float; subst. simpl in eval_real. - eapply (validErrorboundCorrectRounding absenv dVars eval_real H6); eauto. + eapply (validErrorboundCorrectRounding absenv e dVars Gamma eval_real H6); eauto. + econstructor; eauto. constructor; auto. + simpl. @@ -2124,15 +2185,17 @@ Proof. simpl in typing_ok. simpl in fVars_subset. inversion typing_ok; subst. - pose proof (validIntervalbounds_sound absenv P (fVars:=fVars) (dVars:=dVars) (E:=E1) H4 L1 (vR:=nR) valid_dVars fVars_subset P_valid eval_real) as vIB_e. + pose proof (validIntervalbounds_sound e absenv P (fVars:=fVars) (dVars:=dVars) (E:=E1) defVars L1 (vR:=nR) valid_dVars fVars_subset P_valid eval_real) as vIB_e. rewrite <- Heqabsenv_e in vIB_e. simpl in vIB_e; auto. + assert (absenv e = (fst ive1, snd ive1, err1)) by (destruct ive1; simpl; auto). apply H0. + eapply IHe; eauto. - * inversion typing_ok; subst. - assert (m3 = m2) by (eapply test; eauto). - subst; auto. + * simpl in typing_ok. + rewrite H in typing_ok. + case_eq (Gamma e); intros; rewrite H0 in typing_ok; [ | inversion typing_ok ]. + andb_to_prop typing_ok. + auto. * assert (absenv e = (fst ive1, snd ive1, err1)) by (destruct ive1; simpl; auto). apply H0. Qed. @@ -2143,8 +2206,8 @@ Lemma validErrorbound_subset e tmap absenv dVars dVars': validErrorbound e tmap absenv dVars' = true. Proof. induction e; intros validBound_e_dV subset_dV; simpl in *; try auto. - - destruct (absenv (Var Q m n)); simpl in *. - case_eq (tmap (Var Q m n)); intros; rewrite H in validBound_e_dV; [ | inversion validBound_e_dV ]. + - destruct (absenv (Var Q n)); simpl in *. + case_eq (tmap (Var Q n)); intros; rewrite H in validBound_e_dV; [ | inversion validBound_e_dV ]. andb_to_prop validBound_e_dV. apply Is_true_eq_true; apply andb_prop_intro; split. + apply Is_true_eq_left in L; auto. @@ -2181,20 +2244,20 @@ Qed. Theorem validErrorboundCmd_sound (f:cmd Q) (absenv:analysisResult): - forall E1 E2 outVars fVars dVars vR vF elo ehi err P m Gamma, - validTypeCmd Gamma f m -> - approxEnv E1 absenv fVars dVars E2 -> + forall E1 E2 outVars fVars dVars vR vF elo ehi err P m Gamma defVars, + typeCheckCmd f defVars Gamma = true -> + approxEnv E1 defVars absenv fVars dVars E2 -> ssa f (NatSet.union fVars dVars) outVars -> NatSet.Subset (NatSet.diff (Commands.freeVars f) dVars) fVars -> - bstep (toREvalCmd (toRCmd f)) E1 vR M0 -> - bstep (toRCmd f) E2 vF m -> + bstep (toREvalCmd (toRCmd f)) E1 (toREvalVars defVars) vR M0 -> + bstep (toRCmd f) E2 defVars vF m -> validErrorboundCmd f Gamma absenv dVars = true -> validIntervalboundsCmd f absenv P dVars = true -> - (forall v1 m1, NatSet.mem v1 dVars = true -> - exists vR mv1, E1 v1 = Some (vR, M0) /\ Gamma (Var Q mv1 v1) = Some m1 /\ - (Q2R (fst (fst (absenv (Var Q m1 v1)))) <= vR <= Q2R (snd (fst (absenv (Var Q m1 v1)))))%R) -> + (forall v1, NatSet.mem v1 dVars = true -> + exists vR, E1 v1 = Some vR /\ + (Q2R (fst (fst (absenv (Var Q v1)))) <= vR <= Q2R (snd (fst (absenv (Var Q v1)))))%R) -> (forall v, NatSet.mem v fVars= true -> - exists vR, E1 v = Some (vR, M0) /\ + exists vR, E1 v = Some vR /\ (Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) -> absenv (getRetExp f) = ((elo,ehi),err) -> (Rabs (vR - vF) <= (Q2R err))%R. @@ -2204,15 +2267,15 @@ Proof. - simpl in eval_real, eval_float. inversion eval_float; inversion eval_real; subst. inversion ssa_f; subst. - assert (approxEnv (updEnv n M0 v0 E1) absenv fVars (NatSet.add n dVars) (updEnv n m v E2)). + assert (approxEnv (updEnv n v0 E1) defVars absenv fVars (NatSet.add n dVars) (updEnv n v E2)). + eapply approxUpdBound; try auto. * unfold validErrorboundCmd in valid_bounds. andb_to_prop valid_bounds. rename L0 into validErrorbound_e. rewrite Qeq_bool_iff in R0. - assert (snd (absenv (Var Q m n)) == snd (absenv (Var Q m n))) by apply Qeq_refl. + assert (snd (absenv (Var Q n)) == snd (absenv (Var Q n))) by apply Qeq_refl. pose proof (Qleb_comp _ _ R0 _ _ H). - assert (Qle (snd (absenv e)) (snd (absenv (Var Q m n)))). + assert (Qle (snd (absenv e)) (snd (absenv (Var Q n)))). { rewrite <- Qle_bool_iff. rewrite H0. rewrite Qle_bool_iff. @@ -2227,7 +2290,11 @@ Proof. destruct absenv_e as [iv [err_e absenv_e]]. destruct iv. eapply validErrorbound_sound; eauto. - - inversion type_f; subst; auto. + - simpl in type_f. + case_eq (Gamma (Var Q n)); intros; rewrite H2 in type_f; [ | inversion type_f ]. + case_eq (Gamma e); intros; rewrite H3 in type_f; [ | inversion type_f ]. + andb_to_prop type_f. + auto. - hnf. intros a a_in_diff. apply freeVars_subset. rewrite NatSet.diff_spec in *. @@ -2252,8 +2319,12 @@ Proof. rename R into valid_rec. simpl in valid_intv; andb_to_prop valid_intv. - eapply (IHf (updEnv n M0 v0 E1) (updEnv n m v E2) _ _ _ vR vF elo ehi err P); eauto. - * inversion type_f; subst; auto. + eapply (IHf (updEnv n v0 E1) (updEnv n v E2) _ _ _ vR vF elo ehi err P); eauto. + * simpl in type_f. + case_eq (Gamma (Var Q n)); intros; rewrite H0 in type_f; [ | inversion type_f ]. + case_eq (Gamma e); intros; rewrite H1 in type_f; [ | inversion type_f ]. + andb_to_prop type_f. + auto. * instantiate (1 := outVars). eapply ssa_equal_set; eauto. hnf. intros a; split; intros in_set. @@ -2270,7 +2341,7 @@ Proof. simpl. rewrite NatSet.diff_spec, NatSet.remove_spec, NatSet.union_spec. split; try auto. - * intros v1 m1 v1_mem. + * intros v1 v1_mem. unfold updEnv. case_eq (v1 =? n); intros v1_eq. { rename R1 into eq_lo; @@ -2281,21 +2352,20 @@ Proof. apply Qeq_eqR in eq_hi. inversion type_f; subst. apply Nat.eqb_eq in v1_eq; subst. - exists v0, m; split; try split; try auto; assert (m1 = m) by admit; subst. - - inversion H11; subst; auto. - - rewrite <- eq_lo, <- eq_hi. - eapply validIntervalbounds_sound; eauto. - hnf. intros a a_mem_diff. - rewrite NatSet.diff_spec in a_mem_diff. - destruct a_mem_diff as [a_mem_freeVars a_no_dVar]. - apply freeVars_subset. - simpl. rewrite NatSet.diff_spec, NatSet.remove_spec, NatSet.union_spec. - split; try auto. - split; try auto. - hnf; intros; subst. - specialize (H5 n a_mem_freeVars). - rewrite <- NatSet.mem_spec in H5. - rewrite H5 in *; congruence. } + exists v0; split; try auto. + rewrite <- eq_lo, <- eq_hi. + eapply validIntervalbounds_sound; eauto. + hnf. intros a a_mem_diff. + rewrite NatSet.diff_spec in a_mem_diff. + destruct a_mem_diff as [a_mem_freeVars a_no_dVar]. + apply freeVars_subset. + simpl. rewrite NatSet.diff_spec, NatSet.remove_spec, NatSet.union_spec. + split; try auto. + split; try auto. + hnf; intros; subst. + specialize (H5 n a_mem_freeVars). + rewrite <- NatSet.mem_spec in H5. + rewrite H5 in *; congruence. } { rewrite NatSet.mem_spec in v1_mem. rewrite NatSet.add_spec in v1_mem. rewrite Nat.eqb_neq in v1_eq. @@ -2321,5 +2391,4 @@ Proof. destruct absenv_e as [iv [err_e absenv_e]]. destruct iv. eapply validErrorbound_sound; eauto. - inversion type_f; subst; auto. -Admitted. \ No newline at end of file +Qed. \ No newline at end of file diff --git a/coq/Expressions.v b/coq/Expressions.v index eb8f72d..bdd1baf 100644 --- a/coq/Expressions.v +++ b/coq/Expressions.v @@ -205,13 +205,6 @@ Fixpoint toREval (e:exp R) := | Downcast _ e1 => (toREval e1) end. -Definition toREvalEnv (E:env) : env := - fun (n:nat) => - let s := (E n) in - match s with - | None => None - | Some (r, _) => Some (r, M0) - end. (** @@ -229,7 +222,7 @@ using a perturbation of the real valued computation by (1 + delta), where Inductive eval_exp (E:env) (defVars: nat -> option mType) :(exp R) -> R -> mType -> Prop := | Var_load m x v: defVars x = Some m -> - E x = Some (v, m) -> + E x = Some v -> eval_exp E defVars (Var R x) v m | Const_dist m n delta: Rle (Rabs delta) (Q2R (meps m)) -> @@ -340,19 +333,27 @@ Proof. Qed. +Fixpoint toREvalVars (d:nat -> option mType) (n:nat) := + match d n with + | Some m => Some M0 + | None => None + end. + + (** Helping lemma. Needed in soundness proof. For each evaluation of using an arbitrary epsilon, we can replace it by evaluating the subexpressions and then binding the result values to different variables in the Environment. -**) + **) + Lemma binary_unfolding b f1 f2 m E vF defVars: eval_exp E defVars (Binop b f1 f2) vF m -> exists vF1 vF2 m1 m2, m = computeJoin m1 m2 /\ eval_exp E defVars f1 vF1 m1 /\ eval_exp E defVars f2 vF2 m2 /\ - eval_exp (updEnv 2 m2 vF2 (updEnv 1 m1 vF1 emptyEnv)) + eval_exp (updEnv 2 vF2 (updEnv 1 vF1 emptyEnv)) (fun n => if (n =? 2) then Some m2 else if (n =? 1) then Some m1 else defVars n) (Binop b (Var R 1) (Var R 2)) vF m. Proof. @@ -366,28 +367,28 @@ Proof. eapply Var_load; eauto. Qed. -(* Analogous lemma for unary expressions. *) -Lemma unary_unfolding (e:exp R) (m:mType) (E:env) (v:R) defVars: - (eval_exp E defVars (Unop Inv e) v m -> - exists v1 m1, - eval_exp E defVars e v1 m1 /\ - eval_exp (updEnv 1 m1 v1 E) (fun n => if (n =? 1) then Some m1 else defVars n) (Unop Inv (Var R 1)) v m). -Proof. - intros eval_un. - inversion eval_un; subst. - exists v1; exists m. - repeat split; try auto. - econstructor; try auto. - pose proof (isMorePrecise_refl m). - econstructor; eauto. -Qed. +(* (* Analogous lemma for unary expressions. *) *) +(* Lemma unary_unfolding (e:exp R) (m:mType) (E:env) (v:R) defVars: *) +(* (eval_exp E defVars (Unop Inv e) v m -> *) +(* exists v1 m1, *) +(* eval_exp E defVars e v1 m1 /\ *) +(* eval_exp (updEnv 1 v1 E) (fun n => if (n =? 1) then Some m1 else defVars n) (Unop Inv (Var R 1)) v m). *) +(* Proof. *) +(* intros eval_un. *) +(* inversion eval_un; subst. *) +(* exists v1; exists m. *) +(* repeat split; try auto. *) +(* econstructor; try auto. *) +(* pose proof (isMorePrecise_refl m). *) +(* econstructor; eauto. *) +(* Qed. *) -(** - Using the parametric expressions, define boolean expressions for conditionals -**) -Inductive bexp (V:Type) : Type := - leq: exp V -> exp V -> bexp V -| less: exp V -> exp V -> bexp V. +(* (** *) +(* Using the parametric expressions, define boolean expressions for conditionals *) +(* **) *) +(* Inductive bexp (V:Type) : Type := *) +(* leq: exp V -> exp V -> bexp V *) +(* | less: exp V -> exp V -> bexp V. *) (** Define evaluation of boolean expressions diff --git a/coq/Infra/Abbrevs.v b/coq/Infra/Abbrevs.v index 5330daa..7f44dab 100644 --- a/coq/Infra/Abbrevs.v +++ b/coq/Infra/Abbrevs.v @@ -45,7 +45,7 @@ Definition precond :Type := nat -> intv. (** Abbreviation for the type of a variable environment, which should be a partial function **) -Definition env := nat -> option (R * mType). +Definition env := nat -> option R. (** The empty environment must return NONE for every variable @@ -55,7 +55,7 @@ Definition emptyEnv:env := fun _ => None. (** Define environment update function as abbreviation, for variable environments **) -Definition updEnv (x:nat) (mx:mType) (v: R) (E:env) (y:nat) := +Definition updEnv (x:nat) (v: R) (E:env) (y:nat) := if (y =? x) - then Some (v, mx) + then Some v else E y. \ No newline at end of file diff --git a/coq/IntervalValidation.v b/coq/IntervalValidation.v index 00c512e..650df82 100644 --- a/coq/IntervalValidation.v +++ b/coq/IntervalValidation.v @@ -170,19 +170,20 @@ Proof. unfold isSupersetIntv in *; simpl in *. apply le_neq_bool_to_lt_prop; auto. Qed. + Theorem validIntervalbounds_sound (f:exp Q) (absenv:analysisResult) (P:precond) fVars dVars (E:env) defVars: forall vR, (* validType Gamma f m -> *) validIntervalbounds f absenv P dVars = true -> (forall v, NatSet.mem v dVars = true -> - exists vR, E v = Some (vR, M0) /\ + exists vR, E v = Some vR /\ (Q2R (fst (fst (absenv (Var Q v)))) <= vR <= Q2R (snd (fst (absenv (Var Q v)))))%R) -> NatSet.Subset (NatSet.diff (Expressions.usedVars f) dVars) fVars -> (forall v, NatSet.mem v fVars = true -> - exists vR, E v = Some (vR, M0) /\ + exists vR, E v = Some vR /\ (Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R) -> - eval_exp E defVars (toREval (toRExp f)) vR M0 -> + eval_exp E (toREvalVars defVars) (toREval (toRExp f)) vR M0 -> (Q2R (fst (fst (absenv f))) <= vR <= Q2R (snd (fst (absenv f))))%R. Proof. induction f; intros vR valid_bounds valid_definedVars usedVars_subset valid_usedVars eval_f. diff --git a/coq/Typing.v b/coq/Typing.v index c84dd06..7f798ca 100644 --- a/coq/Typing.v +++ b/coq/Typing.v @@ -29,9 +29,11 @@ Fixpoint typeMap (defVars:nat -> option mType) (e:exp Q) (e': exp Q) : option mT | Unop u e1 => if expEqBool e e' then typeExpression defVars e else typeMap defVars e1 e' | Binop b e1 e2 => if expEqBool e e' then typeExpression defVars e else - match (typeMap defVars e1 e') with - | None => typeMap defVars e2 e' - | x => x + match (typeMap defVars e1 e'), (typeMap defVars e2 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 | Downcast m e1 => if expEqBool e e' then typeExpression defVars (Downcast m e1) else typeMap defVars e1 e' end. @@ -40,7 +42,7 @@ Fixpoint typeMap (defVars:nat -> option mType) (e:exp Q) (e': exp Q) : option mT Fixpoint typeCmd (defVars:nat -> option mType) (f:cmd Q): option mType := match f with |Let m n e c => match typeExpression defVars e with - |Some m' => if mTypeEqBool m m' then typeCmd (fun f => if (n =? f) then Some m else defVars f) c + |Some m' => if mTypeEqBool m m' then typeCmd defVars (*(fun f => if (n =? f) then Some m else defVars f)*) c else None |None => None end @@ -50,10 +52,10 @@ Fixpoint typeCmd (defVars:nat -> option mType) (f:cmd Q): option mType := Fixpoint typeMapCmd (defVars:nat -> option mType) (f:cmd Q) (f':exp Q) : option mType := match f with |Let m n e c => if expEqBool f' (Var Q n) then - match typeMap defVars e f' with - |None => None - |Some m1 => if mTypeEqBool m1 m then Some m else None - end + match defVars n with + | Some m' => if mTypeEqBool m m' then Some m else None + | None => None + end else let te := typeMap defVars e in let tc := typeMapCmd defVars c in @@ -99,7 +101,7 @@ Fixpoint typeCheck (e:exp Q) (defVars:nat -> option mType) (tMap: exp Q -> optio Fixpoint typeCheckCmd (c:cmd Q) (defVars:nat -> option mType) (tMap:exp Q -> option mType) : bool := match c with | Let m x e g => match tMap (Var Q x), tMap e with - | Some mx, Some me => (mTypeEqBool mx m) && (mTypeEqBool mx me) && typeCheckCmd g defVars tMap + | Some mx, Some me => (mTypeEqBool mx m) && (mTypeEqBool mx me) && typeCheck e defVars tMap && typeCheckCmd g defVars tMap | _, _ => false end | Ret e => typeCheck e defVars tMap @@ -294,12 +296,12 @@ Theorem typingSoundnessCmd c defVars E v m Gamma: bstep (toRCmd c) E defVars v m -> (*(typeMapCmd defVars c)*) Gamma (getRetExp c) = Some m. Proof. - revert E; induction c; intros * tc bc. + revert E defVars; induction c; intros * tc bc. - simpl in tc. case_eq (Gamma (Var Q n)); intros; rewrite H in tc; [ | inversion tc ]. case_eq (Gamma e); intros; rewrite H0 in tc; [ | inversion tc ]. andb_to_prop tc. - apply EquivEqBoolEq in L0; apply EquivEqBoolEq in R0; subst. + apply EquivEqBoolEq in L; apply EquivEqBoolEq in R1; subst. simpl. inversion bc; subst. eapply IHc; eauto. @@ -308,6 +310,220 @@ Proof. eapply typingSoundnessExp; eauto. Qed. +Lemma stupidlemma e defVars Gamma: + typeCheck e defVars Gamma = true -> + exists m, Gamma e = Some m. +Proof. + destruct e; intros * tc. + - simpl in *. + case_eq (Gamma (Var Q n)); intros; rewrite H in tc; [ | inversion tc ]. + eauto. + - simpl in *. + case_eq (Gamma (Const m q)); intros; rewrite H in tc; [ | inversion tc ]. + eauto. + - simpl in *. + case_eq (Gamma (Unop u e)); intros; rewrite H in tc; [ | inversion tc ]. + eauto. + - simpl in *; + case_eq (Gamma (Binop b e1 e2)); intros; rewrite H in tc; [ | inversion tc ]; eauto. + - simpl in *; + case_eq (Gamma (Downcast m e)); intros; rewrite H in tc; [ | inversion tc ]; eauto. +Qed. + +Fixpoint defVarsWellDefined (e:exp Q) (defVars:nat -> option mType) : bool := + NatSet.for_all (fun v => match defVars v with | Some m => true | _ => false end) (usedVars e). + +Fixpoint defVarsWellDefinedCmd c defVars : bool := + match c with + | Let m x e g => match defVars x with + | Some m' => mTypeEqBool m m' && defVarsWellDefined e defVars && defVarsWellDefinedCmd g defVars + | _ => false + end + | Ret e => defVarsWellDefined e defVars + end. + +(* Theorem typeExpressionChecks e defVars: *) +(* defVarsWellDefined e defVars = true -> *) +(* typeCheck e defVars (fun e => typeExpression defVars e) = true. *) +(* Proof. *) +(* intros defVars_wd. induction e. *) +(* - simpl in *. *) +(* apply NatSet.for_all_spec in defVars_wd; try auto. *) +(* Focus 2. intros a b c; rewrite c; auto. *) +(* specialize (defVars_wd n). *) +(* rewrite NatSet.singleton_spec in defVars_wd. *) +(* assert (n = n) by auto; specialize (defVars_wd H). *) +(* case_eq (defVars n); intros; rewrite H0 in defVars_wd; [ | inversion defVars_wd ]. *) +(* rewrite mTypeEqBool_refl; auto. *) +(* - simpl. *) +(* rewrite mTypeEqBool_refl; auto. *) +(* - simpl in *. *) +(* assert (defVarsWellDefined e defVars = true) by admit. *) +(* specialize (IHe H). *) +(* pose proof (stupidlemma _ _ _ IHe) as [me type_e]. *) +(* rewrite type_e, mTypeEqBool_refl; simpl. *) +(* auto. *) +(* - simpl in *. *) +(* assert (defVarsWellDefined e1 defVars = true) by admit. *) +(* specialize (IHe1 H). *) +(* assert (defVarsWellDefined e2 defVars = true) by admit. *) +(* specialize (IHe2 H0). *) +(* pose proof (stupidlemma _ _ _ IHe1) as [me1 type_e1]. *) +(* pose proof (stupidlemma _ _ _ IHe2) as [me2 type_e2]. *) +(* rewrite type_e1,type_e2,mTypeEqBool_refl; simpl; auto. *) +(* rewrite IHe1, IHe2; auto. *) +(* - *) +(* unfold typeCheck. *) + + +(* simpl in *. *) +(* assert (defVarsWellDefined e defVars = true) by admit. *) +(* specialize (IHe H). *) +(* pose proof (stupidlemma _ _ _ IHe) as [me type_e]. *) +(* rewrite type_e. *) +(* assert (typeExpression defVars (Downcast m e) = Some m). *) +(* { simpl; rewrite type_e. *) + + + + +(* Theorem typeMapChecks e defVars: *) +(* defVarsWellDefined e defVars = true -> *) +(* (*(forall v, NatSet.In v (usedVars e) -> exists m, defVars v = Some m) ->*) *) +(* typeCheck e defVars (typeMap defVars e) = true. *) +(* Proof. *) +(* intros defVars_wd; induction e; intros. *) +(* - simpl in *; rewrite <- beq_nat_refl. *) +(* rewrite NatSet.for_all_spec in defVars_wd. *) +(* + unfold NatSet.For_all in defVars_wd. *) +(* specialize (defVars_wd n). *) +(* rewrite NatSet.singleton_spec in defVars_wd. *) +(* assert (n = n) by auto; specialize (defVars_wd H). *) +(* case_eq (defVars n); intros; rewrite H0 in defVars_wd; [ | inversion defVars_wd ]. *) +(* rewrite mTypeEqBool_refl; auto. *) +(* + intros a b hyp; rewrite hyp; auto. *) +(* - simpl in *. *) +(* rewrite mTypeEqBool_refl, Qeq_bool_refl; simpl. *) +(* rewrite mTypeEqBool_refl; auto. *) +(* - simpl. *) +(* rewrite unopEqBool_refl, expEqBool_refl; simpl. *) +(* assert (defVarsWellDefined e defVars = true) by admit. *) +(* specialize (IHe H). *) +(* pose proof (stupidlemma _ _ _ IHe) as [m type_e]. *) +(* apply eqTypeExpression in type_e. *) +(* rewrite type_e. *) +(* case_eq (expEqBool (Unop u e) e); intros; simpl in H0; rewrite H0. *) +(* + admit. *) +(* + apply eqTypeExpression in type_e; rewrite type_e. *) +(* rewrite mTypeEqBool_refl; simpl. *) +(* eapply Gamma_strengthening. *) +(* Focus 2. eapply IHe. *) +(* intros e0 m0 type_e0. *) +(* case_eq (expEqBool (Unop u e) e0); intros; simpl in H1; rewrite H1. *) +(* * admit. *) +(* * auto. *) +(* - unfold typeCheck. *) +(* assert (defVarsWellDefined e1 defVars = true) by admit. *) +(* assert (defVarsWellDefined e2 defVars = true) by admit. *) +(* specialize (IHe1 H). *) +(* specialize (IHe2 H0). *) +(* pose proof (stupidlemma _ _ _ IHe1) as [m1 tMap_e1]. *) +(* pose proof (stupidlemma _ _ _ IHe2) as [m2 tMap_e2]. *) +(* assert (typeMap defVars (Binop b e1 e2) (Binop b e1 e2) = Some (computeJoin m1 m2)) as tMap_binop. *) +(* { simpl; rewrite binopEqBool_refl,?expEqBool_refl; simpl. *) +(* rewrite eqTypeExpression in tMap_e1, tMap_e2. *) +(* rewrite tMap_e1, tMap_e2. *) +(* auto. } *) +(* rewrite tMap_binop. *) +(* assert (typeMap defVars (Binop b e1 e2) e1 = Some m1). *) +(* { simpl. *) +(* assert (expEqBool (Binop b e1 e2) e1 = false) by admit; simpl in H1; rewrite H1. *) +(* rewrite tMap_e1. *) +(* Admitted. *) + + +(* Theorem typeMapCmdChecks c defVars: *) +(* defVarsWellDefinedCmd c defVars = true -> *) +(* typeCheckCmd c defVars (typeMapCmd defVars c) = true. *) +(* Proof. *) +(* intros defVars_wd; induction c; intros. *) +(* - unfold typeCheckCmd. *) +(* assert (typeMapCmd defVars (Let m n e c) (Var Q n) = Some m). *) +(* { unfold typeMapCmd. simpl; rewrite <- beq_nat_refl. *) +(* simpl in defVars_wd. *) +(* case_eq (defVars n); intros; rewrite H in defVars_wd; [ | inversion defVars_wd ]. *) +(* andb_to_prop defVars_wd. *) +(* rewrite L0; simpl; auto. } *) +(* rewrite H. *) +(* assert (typeMapCmd defVars (Let m n e c) e = Some m). *) +(* { simpl. *) +(* case_eq (expEqBool e (Var Q n)); intros. *) +(* - admit. *) +(* - *) +(* Admitted. *) + + + + +(* Theorem typeMapChecks2 e defVars Gamma: *) +(* (forall v, NatSet.In v (usedVars e) -> exists m, defVars v = Some m) -> *) +(* Gamma_stronger (typeMap defVars e) Gamma -> *) +(* typeCheck e defVars Gamma = true. *) +(* Proof. *) +(* intros defVars_wd gamma_st. *) +(* induction e; intros. *) +(* - simpl. *) +(* unfold Gamma_stronger in gamma_st. *) +(* specialize (gamma_st (Var Q n)); simpl in gamma_st. *) +(* rewrite <- beq_nat_refl in gamma_st. *) +(* simpl in defVars_wd. *) +(* specialize (defVars_wd n). *) +(* rewrite NatSet.singleton_spec in defVars_wd. *) +(* assert (n = n) by auto. *) +(* specialize (defVars_wd H). *) +(* destruct defVars_wd as [m defVars_wd]. *) +(* rewrite defVars_wd. *) +(* specialize (gamma_st _ defVars_wd). *) +(* rewrite gamma_st. *) +(* apply mTypeEqBool_refl. *) +(* - simpl. *) +(* unfold Gamma_stronger in gamma_st. *) +(* specialize (gamma_st (Const m v)); simpl in gamma_st. *) +(* rewrite mTypeEqBool_refl, Qeq_bool_refl in gamma_st; simpl in gamma_st. *) +(* specialize (gamma_st m). *) +(* assert (Some m = Some m) by auto. *) +(* rewrite (gamma_st H). *) +(* rewrite mTypeEqBool_refl; auto. *) +(* - simpl. *) +(* simpl in defVars_wd. *) +(* specialize (IHe defVars_wd). *) +(* assert (Gamma_stronger (typeMap defVars e) Gamma). *) +(* { *) +(* eapply Gamma_stronger_trans; eauto. *) +(* intros e0 m0 typemap_e. *) +(* simpl. *) +(* case_eq (expEqBool (Unop u e) e0); intros; simpl in H; rewrite H. *) +(* + admit. *) +(* + auto. } *) +(* specialize (IHe H); rewrite IHe; simpl. *) +(* unfold Gamma_stronger in gamma_st. *) +(* specialize (gamma_st (Unop u e)); simpl in gamma_st. *) +(* rewrite unopEqBool_refl, expEqBool_refl in gamma_st; simpl in gamma_st. *) +(* unfold Gamma_stronger in H. *) +(* pose proof (stupidlemma _ _ _ IHe) as [m type_e]. *) +(* rewrite type_e. *) +(* apply eqTypeExpression in type_e. *) +(* rewrite type_e. *) +(* case_eq (expEqBool (Unop u e) e); intros; simpl in H; rewrite H. *) +(* + admit. *) +(* + apply eqTypeExpression in type_e; rewrite type_e. *) +(* rewrite mTypeEqBool_refl; simpl. *) + + + + + + (* Lemma typeMapVarDet e m m' v: *) (* typeMap e (Var Q m v) = Some m' -> *) (* m = m'. *) diff --git a/coq/ssaPrgs.v b/coq/ssaPrgs.v index 39e28a9..0580620 100644 --- a/coq/ssaPrgs.v +++ b/coq/ssaPrgs.v @@ -178,7 +178,7 @@ Lemma ssa_shadowing_free m x y v v' e f inVars outVars E defVars: ssa (Let m x (toREval (toRExp e)) (toREvalCmd (toRCmd f))) inVars outVars -> NatSet.In y inVars -> eval_exp E defVars (toREval (toRExp e)) v M0 -> - forall E n, updEnv x m v (updEnv y m v' E) n = updEnv y m v' (updEnv x m v E) n. + forall E n, updEnv x v (updEnv y v' E) n = updEnv y v' (updEnv x v E) n. Proof. intros ssa_let y_free eval_e. inversion ssa_let; subst. @@ -230,25 +230,25 @@ Lemma shadowing_free_rewriting_cmd f E1 E2 vR defVars: bstep (toREvalCmd f) E1 defVars vR M0 <-> bstep (toREvalCmd f) E2 defVars vR M0. Proof. -revert E1 E2 vR. +revert E1 E2 defVars vR. induction f; intros E1 E2 vR agree_on_vars. - split; intros bstep_Let; inversion bstep_Let; subst. - + erewrite shadowing_free_rewriting_exp in H7; auto. + + erewrite shadowing_free_rewriting_exp in H8; auto. econstructor; eauto. rewrite <- IHf. - apply H8. + apply H10. intros n'; unfold updEnv. case_eq (n' =? n); auto. - + erewrite <- shadowing_free_rewriting_exp in H7; auto. + + erewrite <- shadowing_free_rewriting_exp in H8; auto. econstructor; eauto. rewrite IHf. - apply H8. + apply H10. intros n'; unfold updEnv. case_eq (n' =? n); auto. - split; intros bstep_Ret; inversion bstep_Ret; subst. - + erewrite shadowing_free_rewriting_exp in H0; auto. + + erewrite shadowing_free_rewriting_exp in H1; auto. constructor; auto. - + erewrite <- shadowing_free_rewriting_exp in H0; auto. + + erewrite <- shadowing_free_rewriting_exp in H1; auto. constructor; auto. Qed. @@ -256,12 +256,12 @@ Lemma dummy_bind_ok e v x v' inVars E defVars: NatSet.Subset (usedVars e) inVars -> NatSet.mem x inVars = false -> eval_exp E defVars (toREval (toRExp e)) v M0 -> - eval_exp (updEnv x M0 v' E) defVars (toREval (toRExp e)) v M0. + eval_exp (updEnv x v' E) defVars (toREval (toRExp e)) v M0. Proof. revert v x v' inVars E. induction e; intros v1 x v2 inVars E valid_vars x_not_free eval_e. - inversion eval_e; subst. - assert ((updEnv x M0 v2 E) n = E n). + assert ((updEnv x v2 E) n = E n). + unfold updEnv. case_eq (n =? x); try auto. intros n_eq_x. @@ -274,8 +274,7 @@ Proof. specialize (valid_vars x in_singleton). rewrite <- NatSet.mem_spec in valid_vars. rewrite valid_vars in *; congruence. - + econstructor. - eauto. + + econstructor; eauto. rewrite H; auto. - inversion eval_e; subst; constructor; auto. - inversion eval_e; subst; econstructor; eauto. @@ -303,288 +302,290 @@ Fixpoint exp_subst (e:exp Q) x e_new := | e => e end. -Lemma exp_subst_correct e e_sub E x v v_res defVars: - eval_exp E defVars (toREval (toRExp e_sub)) v M0 -> - eval_exp (updEnv x M0 v E) (fun n => if n =? x then Some M0 else defVars n) (toREval (toRExp e)) v_res M0 <-> - eval_exp E defVars (toREval (toRExp (exp_subst e x e_sub))) v_res M0. -Proof. - intros eval_e. - revert v_res. - induction e. - - intros v_res; split; [intros eval_upd | intros eval_subst]. - + unfold updEnv in eval_upd. simpl in *. - inversion eval_upd; subst. - case_eq (n =? x); intros; try auto. - * rewrite H in H1. - inversion H1; subst; auto. - * rewrite H in H1. - eapply Var_load; eauto. - rewrite H in H0; auto. - + simpl in eval_subst. - case_eq (n =? x); intros n_eq_case; - rewrite n_eq_case in eval_subst. - * simpl. - assert (updEnv x M0 v E n = Some (v_res, M0)). - { unfold updEnv; rewrite n_eq_case. - f_equal. assert (v = v_res) by (eapply meps_0_deterministic; eauto). rewrite H. auto. } - { econstructor; eauto. - rewrite n_eq_case; auto. } - * simpl. inversion eval_subst; subst. - assert (E n = updEnv x M0 v E n). - { unfold updEnv; rewrite n_eq_case; reflexivity. } - { rewrite H in H1. eapply Var_load; eauto. rewrite n_eq_case. auto. } - - intros v_res; split; [intros eval_upd | intros eval_subst]. - + inversion eval_upd; constructor; auto. - + inversion eval_subst; constructor; auto. - - split; [intros eval_upd | intros eval_subst]. - + inversion eval_upd; econstructor; auto; - rewrite <- IHe; auto. - + inversion eval_subst; constructor; try auto; - rewrite IHe; auto. - - intros v_res; split; [intros eval_upd | intros eval_subst]. - + inversion eval_upd; econstructor; auto; - destruct m1; destruct m2; inversion H2. - * rewrite <- IHe1; auto. - * rewrite <- IHe2; auto. - + inversion eval_subst; econstructor; auto; - destruct m1; destruct m2; inversion H2. - * rewrite IHe1; auto. - * rewrite IHe2; auto. - - split; [intros eval_upd | intros eval_subst]. - + rewrite <- IHe; auto. - + rewrite IHe; auto. -Qed. +(* Lemma exp_subst_correct e e_sub E x v v_res defVars: *) +(* eval_exp E defVars (toREval (toRExp e_sub)) v M0 -> *) +(* eval_exp (updEnv x v E) defVars (toREval (toRExp e)) v_res M0 <-> *) +(* eval_exp E defVars (toREval (toRExp (exp_subst e x e_sub))) v_res M0. *) +(* Proof. *) +(* intros eval_e. *) +(* revert v_res. *) +(* induction e. *) +(* - intros v_res; split; [intros eval_upd | intros eval_subst]. *) +(* + unfold updEnv in eval_upd. simpl in *. *) +(* inversion eval_upd; subst. *) +(* case_eq (n =? x); intros; try auto. *) +(* * rewrite H in H1. *) +(* inversion H1; subst; auto. *) +(* * rewrite H in H1. *) +(* eapply Var_load; eauto. *) +(* + simpl in eval_subst. *) +(* case_eq (n =? x); intros n_eq_case; *) +(* rewrite n_eq_case in eval_subst. *) +(* * simpl. *) +(* assert (updEnv x v E n = Some v_res). *) +(* { unfold updEnv; rewrite n_eq_case. *) +(* f_equal. assert (v = v_res) by (eapply meps_0_deterministic; eauto). rewrite H. auto. } *) +(* { econstructor; eauto. *) -Fixpoint map_subst (f:cmd Q) x e := - match f with - |Let m y e_y g => Let m y (exp_subst e_y x e) (map_subst g x e) - |Ret e_r => Ret (exp_subst e_r x e) - end. +(* rewrite n_eq_case; auto. } *) +(* * simpl. inversion eval_subst; subst. *) +(* assert (E n = updEnv x v E n). *) +(* { unfold updEnv; rewrite n_eq_case; reflexivity. } *) +(* { rewrite H in H1. eapply Var_load; eauto. rewrite n_eq_case. auto. } *) +(* - intros v_res; split; [intros eval_upd | intros eval_subst]. *) +(* + inversion eval_upd; constructor; auto. *) +(* + inversion eval_subst; constructor; auto. *) +(* - split; [intros eval_upd | intros eval_subst]. *) +(* + inversion eval_upd; econstructor; auto; *) +(* rewrite <- IHe; auto. *) +(* + inversion eval_subst; constructor; try auto; *) +(* rewrite IHe; auto. *) +(* - intros v_res; split; [intros eval_upd | intros eval_subst]. *) +(* + inversion eval_upd; econstructor; auto; *) +(* destruct m1; destruct m2; inversion H2. *) +(* * rewrite <- IHe1; auto. *) +(* * rewrite <- IHe2; auto. *) +(* + inversion eval_subst; econstructor; auto; *) +(* destruct m1; destruct m2; inversion H2. *) +(* * rewrite IHe1; auto. *) +(* * rewrite IHe2; auto. *) +(* - split; [intros eval_upd | intros eval_subst]. *) +(* + rewrite <- IHe; auto. *) +(* + rewrite IHe; auto. *) +(* Qed. *) -Lemma stepwise_substitution x e v f E vR inVars outVars defVars: - ssa (toREvalCmd (toRCmd f)) inVars outVars -> - NatSet.In x inVars -> - NatSet.Subset (usedVars e) inVars -> - eval_exp E defVars (toREval (toRExp e)) v M0 -> - bstep (toREvalCmd (toRCmd f)) (updEnv x M0 v E) (fun n => if (n =? x) then Some M0 else defVars n) vR M0 <-> - bstep (toREvalCmd (toRCmd (map_subst f x e))) E defVars vR M0. -Proof. - revert E e x vR inVars outVars. - induction f; intros E e0 x vR inVars outVars ssa_f x_free valid_vars_e eval_e. - - split; [ intros bstep_let | intros bstep_subst]. - + inversion bstep_let; subst. - inversion ssa_f; subst. - assert (forall E var, updEnv n M0 v0 (updEnv x M0 v E) var = updEnv x M0 v (updEnv n M0 v0 E) var). - * eapply ssa_shadowing_free. - apply ssa_f. - apply x_free. - eauto. - * erewrite (shadowing_free_rewriting_cmd _ _ _ _) in H8; try eauto. - simpl in *. - econstructor; eauto. - { rewrite <- exp_subst_correct; eauto. } - { rewrite <- IHf; eauto. - rewrite NatSet.add_spec; right; auto. - apply validVars_add; auto. - eapply dummy_bind_ok; eauto. } - + inversion bstep_subst; subst. - simpl in *. - inversion ssa_f; subst. - econstructor; try auto. - rewrite exp_subst_correct; eauto. - rewrite <- IHf in H8; eauto. - * rewrite <- shadowing_free_rewriting_cmd in H8; eauto. - eapply ssa_shadowing_free; eauto. - rewrite <- exp_subst_correct in H7; eauto. - * rewrite NatSet.add_spec; auto. - * apply validVars_add; auto. - * eapply dummy_bind_ok; eauto. - - split; [intros bstep_let | intros bstep_subst]. - + inversion bstep_let; subst. - simpl in *. - rewrite exp_subst_correct in H0; eauto. - constructor. assumption. - + inversion bstep_subst; subst. - simpl in *. - rewrite <- exp_subst_correct in H0; eauto. - econstructor; eauto. -Qed. +(* Fixpoint map_subst (f:cmd Q) x e := *) +(* match f with *) +(* |Let m y e_y g => Let m y (exp_subst e_y x e) (map_subst g x e) *) +(* |Ret e_r => Ret (exp_subst e_r x e) *) +(* end. *) -Fixpoint let_subst (f:cmd Q) := - match f with - | Let m x e1 g => - exp_subst (let_subst g) x e1 - | Ret e1 => e1 - end. +(* Lemma stepwise_substitution x e v f E vR inVars outVars defVars: *) +(* ssa (toREvalCmd (toRCmd f)) inVars outVars -> *) +(* NatSet.In x inVars -> *) +(* NatSet.Subset (usedVars e) inVars -> *) +(* eval_exp E defVars (toREval (toRExp e)) v M0 -> *) +(* bstep (toREvalCmd (toRCmd f)) (updEnv x v E) (fun n => if (n =? x) then Some M0 else defVars n) vR M0 <-> *) +(* bstep (toREvalCmd (toRCmd (map_subst f x e))) E defVars vR M0. *) +(* Proof. *) +(* revert E e x vR inVars outVars defVars. *) +(* induction f; intros E e0 x vR inVars outVars defVars ssa_f x_free valid_vars_e eval_e. *) +(* - split; [ intros bstep_let | intros bstep_subst]. *) +(* + inversion bstep_let; subst. *) +(* inversion ssa_f; subst. *) +(* assert (forall E var, updEnv n v0 (updEnv x v E) var = updEnv x v (updEnv n v0 E) var). *) +(* * eapply ssa_shadowing_free. *) +(* apply ssa_f. *) +(* apply x_free. *) +(* eauto. *) +(* * erewrite (shadowing_free_rewriting_cmd _ _ _ _) in H8; try eauto. *) +(* simpl in *. *) +(* econstructor; eauto. *) +(* { rewrite <- exp_subst_correct; eauto. } *) +(* { rewrite <- IHf; eauto. *) +(* admit. *) +(* rewrite NatSet.add_spec; right; auto. *) +(* apply validVars_add; auto. *) +(* eapply dummy_bind_ok; eauto. } *) +(* + inversion bstep_subst; subst. *) +(* simpl in *. *) +(* inversion ssa_f; subst. *) +(* econstructor; try auto. *) +(* rewrite exp_subst_correct; eauto. *) +(* rewrite <- IHf in H8; eauto. *) +(* * rewrite <- shadowing_free_rewriting_cmd in H8; eauto. *) +(* admit. *) +(* (* eapply ssa_shadowing_free; eauto. *) *) +(* (* rewrite <- exp_subst_correct in H7; eauto. *) *) +(* * rewrite NatSet.add_spec; auto. *) +(* * apply validVars_add; auto. *) +(* * eapply dummy_bind_ok; eauto. *) +(* - split; [intros bstep_let | intros bstep_subst]. *) +(* + inversion bstep_let; subst. *) +(* simpl in *. *) +(* rewrite exp_subst_correct in H0; eauto. *) +(* constructor. assumption. *) +(* + inversion bstep_subst; subst. *) +(* simpl in *. *) +(* rewrite <- exp_subst_correct in H0; eauto. *) +(* econstructor; eauto. *) +(* Admitted. *) -Lemma eval_subst_subexp E e' n e vR defVars: - NatSet.In n (usedVars e) -> - eval_exp E defVars (toREval (toRExp (exp_subst e n e'))) vR M0 -> - exists v, eval_exp E defVars (toREval (toRExp e')) v M0. -Proof. - revert E e' n vR. - induction e; - intros E e' n' vR n_fVar eval_subst; simpl in *; try eauto. - - case_eq (n =? n'); intros case_n; rewrite case_n in *; eauto. - rewrite NatSet.singleton_spec in n_fVar. - exfalso. - rewrite Nat.eqb_neq in case_n. - apply case_n; auto. - - inversion n_fVar. - - inversion eval_subst; subst; - eapply IHe; eauto. - - inversion eval_subst; subst. - rewrite NatSet.union_spec in n_fVar. - destruct m1; destruct m2; inversion H2. - destruct n_fVar as [n_fVar_e1 | n_fVare2]; - [eapply IHe1; eauto | eapply IHe2; eauto]. -Qed. +(* Fixpoint let_subst (f:cmd Q) := *) +(* match f with *) +(* | Let m x e1 g => *) +(* exp_subst (let_subst g) x e1 *) +(* | Ret e1 => e1 *) +(* end. *) -Lemma bstep_subst_subexp_any E e x f vR defVars: - NatSet.In x (liveVars f) -> - bstep (toREvalCmd (toRCmd (map_subst f x e))) E defVars vR M0 -> - exists E' v, eval_exp E' defVars (toREval (toRExp e)) v M0. -Proof. - revert E e x vR; - induction f; - intros E e' x vR x_live eval_f. - - inversion eval_f; subst. - simpl in x_live. - rewrite NatSet.union_spec in x_live. - destruct x_live as [x_used | x_live]. - + exists E. eapply eval_subst_subexp; eauto. - + eapply IHf; eauto. - - simpl in *. - inversion eval_f; subst. - exists E. eapply eval_subst_subexp; eauto. -Qed. +(* Lemma eval_subst_subexp E e' n e vR defVars: *) +(* NatSet.In n (usedVars e) -> *) +(* eval_exp E defVars (toREval (toRExp (exp_subst e n e'))) vR M0 -> *) +(* exists v, eval_exp E defVars (toREval (toRExp e')) v M0. *) +(* Proof. *) +(* revert E e' n vR. *) +(* induction e; *) +(* intros E e' n' vR n_fVar eval_subst; simpl in *; try eauto. *) +(* - case_eq (n =? n'); intros case_n; rewrite case_n in *; eauto. *) +(* rewrite NatSet.singleton_spec in n_fVar. *) +(* exfalso. *) +(* rewrite Nat.eqb_neq in case_n. *) +(* apply case_n; auto. *) +(* - inversion n_fVar. *) +(* - inversion eval_subst; subst; *) +(* eapply IHe; eauto. *) +(* - inversion eval_subst; subst. *) +(* rewrite NatSet.union_spec in n_fVar. *) +(* destruct m1; destruct m2; inversion H2. *) +(* destruct n_fVar as [n_fVar_e1 | n_fVare2]; *) +(* [eapply IHe1; eauto | eapply IHe2; eauto]. *) +(* Qed. *) -Lemma bstep_subst_subexp_ret E e x e' vR defVars: - NatSet.In x (liveVars (Ret e')) -> - bstep (toREvalCmd (toRCmd (map_subst (Ret e') x e))) E defVars vR M0 -> - exists v, eval_exp E defVars (toREval (toRExp e)) v M0. -Proof. - simpl; intros x_live bstep_ret. - inversion bstep_ret; subst. - eapply eval_subst_subexp; eauto. -Qed. +(* Lemma bstep_subst_subexp_any E e x f vR defVars: *) +(* NatSet.In x (liveVars f) -> *) +(* bstep (toREvalCmd (toRCmd (map_subst f x e))) E defVars vR M0 -> *) +(* exists E' v, eval_exp E' defVars (toREval (toRExp e)) v M0. *) +(* Proof. *) +(* revert E e x vR defVars; *) +(* induction f; *) +(* intros E e' x vR defVars x_live eval_f. *) +(* - inversion eval_f; subst. *) +(* simpl in x_live. *) +(* rewrite NatSet.union_spec in x_live. *) +(* destruct x_live as [x_used | x_live]. *) +(* + exists E. eapply eval_subst_subexp; eauto. *) +(* + eapply IHf; eauto. *) +(* Admitted. *) +(* - simpl in *. *) +(* inversion eval_f; subst. *) +(* exists E. eapply eval_subst_subexp; eauto. *) +(* Qed. *) -Lemma no_forward_refs V (f:cmd V) inVars outVars: - ssa f inVars outVars -> - forall v, NatSet.In v (definedVars f) -> - NatSet.mem v inVars = false. -Proof. - intros ssa_f; induction ssa_f; simpl. - - intros v v_defVar. - rewrite NatSet.add_spec in v_defVar. - destruct v_defVar as [v_x | v_defVar]. - + subst; auto. - + specialize (IHssa_f v v_defVar). - case_eq (NatSet.mem v inVars); intros mem_inVars; try auto. - assert (NatSet.mem v (NatSet.add x inVars) = true) by (rewrite NatSet.mem_spec, NatSet.add_spec, <- NatSet.mem_spec; auto). - congruence. - - intros v v_in_empty; inversion v_in_empty. -Qed. +(* Lemma bstep_subst_subexp_ret E e x e' vR defVars: *) +(* NatSet.In x (liveVars (Ret e')) -> *) +(* bstep (toREvalCmd (toRCmd (map_subst (Ret e') x e))) E defVars vR M0 -> *) +(* exists v, eval_exp E defVars (toREval (toRExp e)) v M0. *) +(* Proof. *) +(* simpl; intros x_live bstep_ret. *) +(* inversion bstep_ret; subst. *) +(* eapply eval_subst_subexp; eauto. *) +(* Qed. *) -Lemma bstep_subst_subexp_let E e x y e' g vR m defVars: - NatSet.In x (liveVars (Let m y e' g)) -> - (forall x, NatSet.In x (usedVars e) -> - exists v, E x = v) -> - bstep (toREvalCmd (toRCmd (map_subst (Let m y e' g) x e))) E defVars vR M0 -> - exists v, eval_exp E defVars (toREval (toRExp e)) v M0. -Proof. - revert E e x y e' vR; - induction g; - intros E e0 x y e' vR x_live uedVars_def bstep_f. - - simpl in *. - inversion bstep_f; subst. - specialize (IHg (updEnv y m v E) e0 x n e). - rewrite NatSet.union_spec in x_live. - destruct x_live as [x_used | x_live]. - + eapply eval_subst_subexp; eauto. - + edestruct IHg as [v0 eval_v0]; eauto. -Admitted. +(* Lemma no_forward_refs V (f:cmd V) inVars outVars: *) +(* ssa f inVars outVars -> *) +(* forall v, NatSet.In v (definedVars f) -> *) +(* NatSet.mem v inVars = false. *) +(* Proof. *) +(* intros ssa_f; induction ssa_f; simpl. *) +(* - intros v v_defVar. *) +(* rewrite NatSet.add_spec in v_defVar. *) +(* destruct v_defVar as [v_x | v_defVar]. *) +(* + subst; auto. *) +(* + specialize (IHssa_f v v_defVar). *) +(* case_eq (NatSet.mem v inVars); intros mem_inVars; try auto. *) +(* assert (NatSet.mem v (NatSet.add x inVars) = true) by (rewrite NatSet.mem_spec, NatSet.add_spec, <- NatSet.mem_spec; auto). *) +(* congruence. *) +(* - intros v v_in_empty; inversion v_in_empty. *) +(* Qed. *) -Theorem let_free_agree f E vR inVars outVars e defVars: - ssa f inVars outVars -> - (forall v, NatSet.In v (definedVars f) -> - NatSet.In v (liveVars f)) -> - let_subst f = e -> - bstep (toREvalCmd (toRCmd (Ret e))) E defVars vR M0 -> - bstep (toREvalCmd (toRCmd f)) E defVars vR M0. -Proof. - intros ssa_f. - revert E vR e; - induction ssa_f; - intros E vR e_subst dVars_live subst_step bstep_e; - simpl in *. - (* Let Case, prove that the value of the let binding must be used somewhere *) - - case_eq (let_subst s). - + intros e0 subst_s; rewrite subst_s in *. -Admitted. - (*inversion subst_step; subst. - clear subst_s subst_step. - inversion bstep_e; subst. - specialize (dVars_live x). - rewrite NatSet.add_spec in dVars_live. - assert (NatSet.In x (NatSet.union (usedVars e) (liveVars s))) - as x_used_or_live - by (apply dVars_live; auto). - rewrite NatSet.union_spec in x_used_or_live. - destruct x_used_or_live as [x_used | x_live]. - * specialize (H x x_used). - rewrite <- NatSet.mem_spec in H; congruence. - * +(* Lemma bstep_subst_subexp_let E e x y e' g vR m defVars: *) +(* NatSet.In x (liveVars (Let m y e' g)) -> *) +(* (forall x, NatSet.In x (usedVars e) -> *) +(* exists v, E x = v) -> *) +(* bstep (toREvalCmd (toRCmd (map_subst (Let m y e' g) x e))) E defVars vR M0 -> *) +(* exists v, eval_exp E defVars (toREval (toRExp e)) v M0. *) +(* Proof. *) +(* revert E e x y e' vR; *) +(* induction g; *) +(* intros E e0 x y e' vR x_live uedVars_def bstep_f. *) +(* - simpl in *. *) +(* inversion bstep_f; subst. *) +(* specialize (IHg (updEnv y m v E) e0 x n e). *) +(* rewrite NatSet.union_spec in x_live. *) +(* destruct x_live as [x_used | x_live]. *) +(* + eapply eval_subst_subexp; eauto. *) +(* + edestruct IHg as [v0 eval_v0]; eauto. *) +(* Admitted. *) - eapply let_b. - Focus 2. - eapply IHssa_f; try auto. *) +(* Theorem let_free_agree f E vR inVars outVars e defVars: *) +(* ssa f inVars outVars -> *) +(* (forall v, NatSet.In v (definedVars f) -> *) +(* NatSet.In v (liveVars f)) -> *) +(* let_subst f = e -> *) +(* bstep (toREvalCmd (toRCmd (Ret e))) E defVars vR M0 -> *) +(* bstep (toREvalCmd (toRCmd f)) E defVars vR M0. *) +(* Proof. *) +(* intros ssa_f. *) +(* revert E vR e; *) +(* induction ssa_f; *) +(* intros E vR e_subst dVars_live subst_step bstep_e; *) +(* simpl in *. *) +(* (* Let Case, prove that the value of the let binding must be used somewhere *) *) +(* - case_eq (let_subst s). *) +(* + intros e0 subst_s; rewrite subst_s in *. *) +(* Admitted. *) +(* (*inversion subst_step; subst. *) +(* clear subst_s subst_step. *) +(* inversion bstep_e; subst. *) +(* specialize (dVars_live x). *) +(* rewrite NatSet.add_spec in dVars_live. *) +(* assert (NatSet.In x (NatSet.union (usedVars e) (liveVars s))) *) +(* as x_used_or_live *) +(* by (apply dVars_live; auto). *) +(* rewrite NatSet.union_spec in x_used_or_live. *) +(* destruct x_used_or_live as [x_used | x_live]. *) +(* * specialize (H x x_used). *) +(* rewrite <- NatSet.mem_spec in H; congruence. *) +(* * *) -Theorem let_free_form f E vR inVars outVars e defVars: - ssa f inVars outVars -> - bstep (toREvalCmd (toRCmd f)) E defVars vR M0 -> - let_subst f = e -> - bstep (toREvalCmd (toRCmd (Ret e))) E defVars vR M0. -Proof. - revert E vR inVars outVars e; - induction f; - intros E vR inVars outVars e_subst ssa_f bstep_f subst_step. - - simpl. - inversion bstep_f; subst. - inversion ssa_f; subst. -Admitted. -(* 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 H7 subst_f_eq). - rewrite subst_f_eq in subst_step. - inversion IHf; subst. - constructor. - inversion subst_step. - subst. - rewrite <- exp_subst_correct; eauto. - + intros subst_eq; rewrite subst_eq in subst_step; inversion subst_step. - - inversion bstep_f; subst. - constructor. - simpl in *. - inversion subst_step; subst. - assumption. -Qed. - *) +(* eapply let_b. *) +(* Focus 2. *) +(* eapply IHssa_f; try auto. *) *) -(* -Lemma ssa_non_stuck (f:cmd Q) (inVars outVars:NatSet.t) (VarEnv:var_env) - (ParamEnv:param_env) (P:precond) (eps:R): - ssa Q f inVars outVars -> - (forall v, NatSet.In v (freeVars e) -> - (Q2R (ivlo (P v)) <= ParamEnv v <= Q2R (ivhi (P v))))%R -> - (forall v, NatSet.In v inVars -> - exists r, VarEnv v = Some r) -> - exists vR, - bstep (toRCmd f) VarEnv ParamEnv P eps (Nop R) vR. -Proof. - intros ssa_f; revert VarEnv ParamEnv P eps. - induction ssa_f; - intros VarEnv ParamEnv P eps fVars_live. - - - *) +(* Theorem let_free_form f E vR inVars outVars e defVars: *) +(* ssa f inVars outVars -> *) +(* bstep (toREvalCmd (toRCmd f)) E defVars vR M0 -> *) +(* let_subst f = e -> *) +(* bstep (toREvalCmd (toRCmd (Ret e))) E defVars vR M0. *) +(* Proof. *) +(* revert E vR inVars outVars e; *) +(* induction f; *) +(* intros E vR inVars outVars e_subst ssa_f bstep_f subst_step. *) +(* - simpl. *) +(* inversion bstep_f; subst. *) +(* inversion ssa_f; subst. *) +(* Admitted. *) +(* (* 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 H7 subst_f_eq). *) +(* rewrite subst_f_eq in subst_step. *) +(* inversion IHf; subst. *) +(* constructor. *) +(* inversion subst_step. *) +(* subst. *) +(* rewrite <- exp_subst_correct; eauto. *) +(* + intros subst_eq; rewrite subst_eq in subst_step; inversion subst_step. *) +(* - inversion bstep_f; subst. *) +(* constructor. *) +(* simpl in *. *) +(* inversion subst_step; subst. *) +(* assumption. *) +(* Qed. *) +(* *) *) +(* (* *) +(* Lemma ssa_non_stuck (f:cmd Q) (inVars outVars:NatSet.t) (VarEnv:var_env) *) +(* (ParamEnv:param_env) (P:precond) (eps:R): *) +(* ssa Q f inVars outVars -> *) +(* (forall v, NatSet.In v (freeVars e) -> *) +(* (Q2R (ivlo (P v)) <= ParamEnv v <= Q2R (ivhi (P v))))%R -> *) +(* (forall v, NatSet.In v inVars -> *) +(* exists r, VarEnv v = Some r) -> *) +(* exists vR, *) +(* bstep (toRCmd f) VarEnv ParamEnv P eps (Nop R) vR. *) +(* Proof. *) +(* intros ssa_f; revert VarEnv ParamEnv P eps. *) +(* induction ssa_f; *) +(* intros VarEnv ParamEnv P eps fVars_live. *) +(* - *) +(* *) *) \ No newline at end of file diff --git a/src/main/scala/daisy/analysis/ChoosePrecisionPhase.scala b/src/main/scala/daisy/analysis/ChoosePrecisionPhase.scala index ba5ad99..eac10f4 100644 --- a/src/main/scala/daisy/analysis/ChoosePrecisionPhase.scala +++ b/src/main/scala/daisy/analysis/ChoosePrecisionPhase.scala @@ -141,6 +141,51 @@ object ChoosePrecisionPhase extends DaisyPhase { prg.defs.map(fnc => (fnc.id.name -> buildIdentifierMapFunction(fnc))).toMap) } + // def typeCheckAndComplete(fnc:FunDef, varMap: Map[Identifier, Precision], defaultPrecision:Precision, constantPrecision:Precision, reporter:Reporter) : Map[Identifier, Precision] = { + + // def recurse(e:Expr, defPrec:Precision, cPrec:Precision, precMap:Map[Identifier, Precision]) : (Map[Identifier, Precision], Precision) = { + // e match { + // case Variable(id) => + // precMap.get(id) match { + // case Some(m) => (precMap, m) + // case None => (precMap + (id -> defPrec), defPrec) + // } + // case RealLiteral(r) => (precMap, cPrec) + // case ArithOperator(Seq(l, r), recons) => + // val (map_l, prec_l) = recurse(l, defPrec, cPrec, precMap) + // val (map_r, prec_r) = recurse(r, defPrec, cPrec, map_l) + // val prec = getUpperBound(prec_l, prec_r) + // (map_r, prec) + // case ArithOperator(Seq(u), recons) => + // recurse(u, defPrec, cPrec, precMap) + // case Let(id, value, body) => + // val (map_v, prec_v) = recurse(value, defPrec, cPrec, precMap) + // precMap.get(id) match { + // case Some(m) => + // if(m <= prec_v) + // recurse(body, defPrec, cPrec, map_v) + // else + // reporter.fatalError(s"Contradiction in typing of Let $id.") + // case None => + // recurse(body, defPrec, cPrec, map_v + (id -> prec_v)) + + // } + // } + // } + + // def checkParams(p:Seq[ValDef], defPrec:Precision, precMap:Map[Identifier, Precision]) : Map[Identifier, Precision] = { + // p.map(e => e match { case ValDef(v) => + // precMap.get(v) match { + // case None => (v -> defPrec) + // case Some(m) => + // }}).toMap + // } + + // val map_p = checkParams(fnc.params, defaultPrecision, varMap) + // val final_map = recurse(fnc.body + + // } + def parseFile(f:String, fncIdMap:Map[String, Identifier], varIdMap:Map[String, Map[String, Identifier]], reporter:Reporter, dummyId:Identifier) : Map[Identifier, Map[Identifier, Precision]] = { val bufferedSource = io.Source.fromFile(f) var currentFunction = "" -- GitLab