(* TODO: Flocq ops open machine_ieeeTheory binary_ieeeTheory lift_ieeeTheory realTheory *) Require Import Coq.QArith.QArith Coq.QArith.Qreals Coq.Reals.Reals Coq.micromega.Psatz. Require Import Daisy.Infra.MachineType Daisy.Typing Daisy.Infra.RealSimps Daisy.IntervalValidation Daisy.ErrorValidation Daisy.Commands Daisy.Environments Daisy.ssaPrgs Daisy.Infra.Ltacs Daisy.Infra.RealRationalProps. Fixpoint FPRangeValidator (e:exp Q) (A:analysisResult) typeMap dVars {struct e} : bool := match DaisyMap.find e typeMap, DaisyMap.find e A with |Some m, Some (iv_e, err_e) => let iv_e_float := widenIntv iv_e err_e in let recRes := match e with | Binop b e1 e2 => FPRangeValidator e1 A typeMap dVars && FPRangeValidator e2 A typeMap dVars | Fma e1 e2 e3 => FPRangeValidator e1 A typeMap dVars && FPRangeValidator e2 A typeMap dVars && FPRangeValidator e3 A typeMap dVars | Unop u e => FPRangeValidator e A typeMap dVars | Downcast m e => FPRangeValidator e A typeMap dVars | _ => true end in match e with | Var _ v => if NatSet.mem v dVars then true else if (validValue (ivhi iv_e_float) m && validValue (ivlo iv_e_float) m) then ((normal (ivlo iv_e_float) m) || (Qeq_bool (ivlo iv_e_float) 0)) && (normal (ivhi iv_e_float) m || (Qeq_bool (ivhi iv_e_float) 0)) && recRes else false | _ => if (validValue (ivhi iv_e_float) m && validValue (ivlo iv_e_float) m) then ((normal (ivlo iv_e_float) m) || (Qeq_bool (ivlo iv_e_float) 0)) && (normal (ivhi iv_e_float) m || (Qeq_bool (ivhi iv_e_float) 0)) && recRes else false end | _, _ => false end. Fixpoint FPRangeValidatorCmd (f:cmd Q) (A:analysisResult) typeMap dVars := match f with | Let m n e g => if FPRangeValidator e A typeMap dVars then FPRangeValidatorCmd g A typeMap (NatSet.add n dVars) else false | Ret e => FPRangeValidator e A typeMap dVars end. Ltac prove_fprangeval m v L1 R:= destruct m eqn:?; try auto; unfold normal, Normal, validValue, Denormal in *; canonize_hyps; rewrite orb_true_iff in *; destruct L1; destruct R; canonize_hyps; rewrite <- Rabs_eq_Qabs in *; Q2R_to_head; rewrite <- Q2R_minus, <- Q2R_plus in *; repeat (match goal with |H: _ = true |- _ => andb_to_prop H end); destruct (Req_dec v 0); try auto; destruct (Rle_lt_dec (Rabs v) (Q2R (minValue m)))%R (* denormal case *); try auto; destruct (Rle_lt_dec (Rabs v) (Q2R (maxValue m)))%R; lra. Theorem FPRangeValidator_sound: forall (e:exp Q) E1 E2 Gamma v m A tMap P fVars dVars, approxEnv E1 Gamma A fVars dVars E2 -> eval_exp E2 Gamma (toRExp e) v m -> typeCheck e Gamma tMap = true -> validIntervalbounds e A P dVars = true -> validErrorbound e tMap A dVars = true -> FPRangeValidator e A tMap dVars = true -> NatSet.Subset (NatSet.diff (usedVars e) dVars) fVars -> dVars_range_valid dVars E1 A -> fVars_P_sound fVars E1 P -> vars_typed (NatSet.union fVars dVars) Gamma -> (forall v, NatSet.In v dVars -> exists vF m, E2 v = Some vF /\ DaisyMap.find (Var Q v) tMap = Some m /\ validFloatValue vF m) -> validFloatValue v m. Proof. intros *. unfold FPRangeValidator. intros. assert (DaisyMap.find e tMap = Some m) as type_e by (eapply typingSoundnessExp; eauto). unfold validFloatValue. edestruct (validIntervalbounds_sound e (A:=A) (P:=P)) as [iv_e [err_e [vR[ map_e[eval_real vR_bounded]]]]]; eauto. destruct iv_e as [e_lo e_hi]. assert (Rabs (vR - v) <= Q2R (err_e))%R. { eapply validErrorbound_sound; eauto. } destruct (distance_gives_iv (a:=vR) v (e:=Q2R err_e) (Q2R e_lo, Q2R e_hi)) as [v_in_errIv]; try auto. simpl in *. assert (Rabs v <= Rabs (Q2R e_hi + Q2R err_e) \/ Rabs v <= Rabs (Q2R e_lo - Q2R err_e))%R as abs_bounded by (apply bounded_inAbs; auto). destruct e; unfold validFloatValue in *; cbn in *; rewrite type_e in *; cbn in *. - destruct (n mem dVars) eqn:?; simpl in *. + destruct (H9 n); try set_tac. destruct H12 as [m2 [env_eq [map_eq validVal]]]. inversion H0; subst. rewrite env_eq in H14; inversion H14; subst. rewrite map_eq in type_e; inversion type_e; subst; auto. + Daisy_compute. prove_fprangeval m v L1 R. - Daisy_compute. prove_fprangeval m v L1 R. - Daisy_compute; try congruence. type_conv; subst. prove_fprangeval m0 v L1 R. - Daisy_compute; try congruence. type_conv; subst. prove_fprangeval (join m0 m1) v L1 R. - Daisy_compute; try congruence. type_conv; subst. prove_fprangeval m v L1 R. - andb_to_prop H4. prove_fprangeval m v L1 R. Qed. Lemma FPRangeValidatorCmd_sound (f:cmd Q): forall E1 E2 Gamma v vR m A tMap P fVars dVars outVars, approxEnv E1 Gamma A fVars dVars E2 -> ssa f (NatSet.union fVars dVars) outVars -> bstep (toREvalCmd (toRCmd f)) E1 (toRMap Gamma) vR m -> bstep (toRCmd f) E2 Gamma v m -> typeCheckCmd f Gamma tMap = true -> validIntervalboundsCmd f A P dVars = true -> validErrorboundCmd f tMap A dVars = true -> FPRangeValidatorCmd f A tMap dVars = true -> NatSet.Subset (NatSet.diff (freeVars f) dVars) fVars -> dVars_range_valid dVars E1 A -> fVars_P_sound fVars E1 P -> vars_typed (NatSet.union fVars dVars) Gamma -> (forall v, NatSet.In v dVars -> exists vF m, E2 v = Some vF /\ DaisyMap.find (Var Q v) tMap = Some m /\ validFloatValue vF m) -> validFloatValue v m. Proof. induction f; intros; simpl in *; (match_pat (bstep _ _ (toRMap _) _ _) (fun H => inversion H; subst; simpl in *)); (match_pat (bstep _ _ Gamma _ _) (fun H => inversion H; subst; simpl in *)); repeat match goal with | H : _ = true |- _ => andb_to_prop H end. - assert (DaisyMap.find e tMap = Some m) by(eapply typingSoundnessExp; eauto). match_pat (ssa _ _ _) (fun H => inversion H; subst; simpl in *). Daisy_compute. edestruct (validIntervalbounds_sound e L1 (Gamma := Gamma)(P:= P) (A:=A) (fVars:=fVars) (dVars:=dVars) (E:=E1)) as [iv_e [err_e [vR_e [map_e [eval_e_real bounded_vR_e]]]]]; eauto. + set_tac. split; try auto. split; try auto. hnf; intros; subst; set_tac. + destr_factorize. edestruct (validErrorbound_sound e (E1:=E1) (E2:=E2) (fVars:=fVars) (dVars := dVars) (A:=A) (P:=P) tMap (nR:=v0) (err:=err_e) (elo:=q) (ehi:=q0)) as [[vF_e [m_e eval_float_e]] err_bounded_e]; eauto. * set_tac. split; try auto. split; try auto. hnf; intros; subst; set_tac. * rewrite <- (meps_0_deterministic (toRExp e) eval_e_real H20) in *; try auto. apply (IHf (updEnv n vR_e E1) (updEnv n v1 E2) (updDefVars n m Gamma) v vR m0 A tMap P fVars (NatSet.add n dVars) (outVars)); eauto. { eapply approxUpdBound; eauto. simpl in *. apply Rle_trans with (r2:= Q2R err_e); try lra. eapply err_bounded_e. eauto. apply Qle_Rle. rewrite Qeq_bool_iff in *. destruct i; inversion Heqo0; subst. rewrite R2. lra. } { eapply ssa_equal_set; eauto. hnf. intros a; split; intros in_set. - rewrite NatSet.add_spec, NatSet.union_spec; rewrite NatSet.union_spec, NatSet.add_spec in in_set. destruct in_set as [P1 | [ P2 | P3]]; auto. - rewrite NatSet.add_spec, NatSet.union_spec in in_set; rewrite NatSet.union_spec, NatSet.add_spec. destruct in_set as [P1 | [ P2 | P3]]; auto. } { eapply (swap_Gamma_bstep (Gamma1 := updDefVars n M0 (toRMap Gamma))); eauto. eauto using Rmap_updVars_comm. } { set_tac; split. - split; try auto. hnf; intros; subst. apply H5; rewrite NatSet.add_spec; auto. - hnf; intros. apply H5; rewrite NatSet.add_spec; auto. } { intros v2 v2_fVar. unfold updEnv. case_eq (v2 =? n); intros v2_eq. - apply Nat.eqb_eq in v2_eq; subst. set_tac. destruct v2_fVar as [? |[? ?]]; try congruence. exists vR_e, (q1,q2), e1; split; try auto. split; try auto. simpl; canonize_hyps. rewrite <- R4, <- R5. auto. - apply H8; try auto. set_tac. destruct v2_fVar as [v2_n | [? ?]]; try auto. rewrite Nat.eqb_neq in v2_eq; congruence. } { unfold fVars_P_sound. intros. unfold updEnv. destruct (v2 =? n) eqn:?; eauto. rewrite Nat.eqb_eq in *; subst. set_tac. exfalso; apply H18; set_tac. } { unfold vars_typed. intros. unfold updDefVars. destruct (v2 =? n) eqn:?; eauto. apply H10. rewrite NatSet.union_spec in *. destruct H4; try auto. rewrite NatSet.add_spec in H4. rewrite Nat.eqb_neq in *. destruct H4; subst; try congruence; auto. } { intros. unfold updEnv. type_conv; subst. destruct (v2 =? n) eqn:?; try rewrite Nat.eqb_eq in *; try rewrite Nat.eqb_neq in *. - exists v1; subst. exists m1; repeat split; try auto. eapply FPRangeValidator_sound; eauto. set_tac. split; try auto. split; try auto. hnf; intros; subst; set_tac. - apply H11. rewrite NatSet.add_spec in H4; destruct H4; auto; subst; congruence. } - eapply FPRangeValidator_sound; eauto. Qed.