Prove soundness of FPRangeValidator, start working on Cmd soundness

coq/FPRangeValidator.v

 
 (* TODO: Flocq ops open machine_ieeeTheory binary_ieeeTheory lift_ieeeTheory realTheory *)
 
-Require Import Coq.QArith.QArith Coq.QArith.Qreals.
+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.
+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 typeMap e with
@@ -51,6 +51,23 @@ Fixpoint FPRangeValidatorCmd (f:cmd Q) (A:analysisResult) typeMap dVars :=
 | 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 ->
@@ -77,11 +94,13 @@ Proof.
   destruct (A e) as [iv_e err_e] eqn:?;
     destruct iv_e as [e_lo e_hi] eqn:?; simpl in *.
   assert (tMap e = Some m)
-    by (eapply typingSoundnessExp; eauto).
+    as type_e
+      by (eapply typingSoundnessExp; eauto).
   subst; simpl in *.
   unfold validFloatValue.
   assert (exists vR, eval_exp E1 (toRMap Gamma) (toREval (toRExp e)) vR M0 /\
-                Q2R (fst (fst (A e))) <= vR <= Q2R (snd (fst (A e))))%R.
+                Q2R (fst (fst (A e))) <= vR <= Q2R (snd (fst (A e))))%R
+         as eval_real_exists.
   { eapply validIntervalbounds_sound; eauto.
     - intros; apply H8.
       rewrite <- NatSet.mem_spec; auto.
@@ -90,28 +109,191 @@ Proof.
     - intros. apply H7.
       set_tac.
       rewrite <- NatSet.union_spec; auto. }
+  destruct eval_real_exists as [vR [eval_real vR_bounded]].
+  assert (Rabs (vR - v) <= Q2R (snd (A e)))%R.
+  { eapply validErrorbound_sound; eauto.
+    - intros * v1_dVar.
+      apply H8; set_tac.
+    - intros * v0_fVar.
+      apply H6. rewrite <- NatSet.mem_spec; auto.
+    - intros * v1_in_union.
+      apply H7; set_tac.
+      rewrite NatSet.union_spec in v1_in_union; auto.
+    - eauto ; instantiate (1:= e_hi).
+      instantiate (1:=e_lo). rewrite Heqp. reflexivity. }
+  rewrite Heqp in *; simpl in *.
+  destruct (distance_gives_iv (a:=vR) v (e:=Q2R err_e) (Q2R e_lo, Q2R e_hi))
+    as [v_in_errIv];
+    try auto.
+  unfold IVlo, IVhi in *; 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 *; simpl in *;
+      rewrite type_e, Heqp in *; simpl 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.
+    + andb_to_prop H4.
+      prove_fprangeval m v L1 R.
+  - andb_to_prop H4.
+    prove_fprangeval m v L1 R.
+  - andb_to_prop H4.
+    prove_fprangeval m v L1 R.
+  - andb_to_prop H4.
+    prove_fprangeval m v L1 R.
+  - andb_to_prop H4.
+    prove_fprangeval m v L1 R.
+Qed.
 
-  \\ `abs (vR - v) <= SND (A e)`
-       by (drule validErrorbound_sound
-           \\ rpt (disch_then drule)
-           \\ strip_tac
+Lemma FPRangeValidatorCmd_sound (f:cmd Q) 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 ->
+  (forall v,
+      NatSet.In v fVars ->
+      exists vR, E1 v = Some vR /\ Q2R (fst (P v)) <= vR <= Q2R (snd (P v)))%R ->
+  (forall v,
+      NatSet.In v fVars \/ NatSet.In v dVars ->
+      exists m, Gamma v = Some m) ->
+  (forall v,
+      NatSet.In v dVars ->
+      exists vR,
+        E1 v = Some vR /\ Q2R (ivlo (fst (A (Var Q v)))) <= vR /\
+        vR <= Q2R (ivhi(fst (A (Var Q v)))))%R ->
+  (forall v,
+      NatSet.In v dVars ->
+      exists vF m,
+        E2 v = Some vF /\ tMap (Var Q v) = 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.
+
+
+  Induct
+  \\ simp[Once toREvalCmd_def, Once validIntervalboundsCmd_def,
+          Once validErrorboundCmd_def, Once FPRangeValidatorCmd_def,
+          Once typeCheckCmd_def, Once freeVars_def, FPRangeValidatorCmd_def]
+  \\ rpt strip_tac
+  >- (rpt (inversion `bstep (Let _ _ _ _) _ _ _ _` bstep_cases)
+      \\ rename1 `bstep (toREvalCmd f) (updEnv n vR_e E1) _ _ mR`
+      \\ rename1 `bstep f (updEnv n vF E2) _ _ mF`
+      \\ `tMap e = SOME m`
+            by (drule typingSoundnessExp
+                \\ rpt (disch_then drule)
+                \\ fs[])
+      \\ fs[]
+      \\ inversion `ssa _ _ _` ssa_cases
+      \\ drule validErrorbound_sound
+      \\ disch_then drule
+      \\ disch_then (qspecl_then [`vR_e`, `SND (A e)`, `P`, `FST(FST (A e))`, `SND(FST (A e))`] impl_subgoal_tac)
+      >- (fs[] \\ conj_tac \\ TRY (first_x_assum MATCH_ACCEPT_TAC)
+          \\ fs[DIFF_DEF, SUBSET_DEF] \\ rpt strip_tac \\ first_x_assum irule
+          \\ fs[domain_union]
+          \\ CCONTR_TAC \\ fs[] \\ rveq
+          \\ first_x_assum (qspec_then `n` assume_tac)
+          \\ res_tac)
+      \\ fs[]
+      \\ drule validIntervalbounds_sound
+      \\ rpt (disch_then drule)
+      \\ disch_then (qspecl_then [`fVars`, `Gamma`] impl_subgoal_tac)
+      >- (fs[] \\ conj_tac \\ TRY (first_x_assum MATCH_ACCEPT_TAC)
+          \\ fs[DIFF_DEF, SUBSET_DEF] \\ rpt strip_tac \\ first_x_assum irule
+          \\ fs[domain_union]
+          \\ CCONTR_TAC \\ fs[] \\ rveq
+          \\ first_x_assum (qspec_then `n` assume_tac)
+          \\ res_tac)
+      \\ Cases_on `tMap (Var n)` \\ fs[]
+      \\ `vR_e = vR'` by metis_tac[meps_0_deterministic]
+      \\ rveq
+      \\ rename1 `vR_e <= SND (FST _)`
+      \\ first_x_assum
+           (qspecl_then [`updEnv n vR_e E1`, `updEnv n vF E2`,
+                         `updDefVars n m Gamma`, `v`, `vR`, `mF`, `A`, `tMap`, `P`,
+                         `fVars`, `insert n () dVars`, `outVars`]
+              impl_subgoal_tac)
+       >- (fs[] \\ rpt conj_tac
+           >- (irule approxUpdBound \\ fs[lookup_NONE_domain]
+               \\ qpat_x_assum `A e = A (Var n)` (fn thm => once_rewrite_tac [GSYM thm])
+               \\ first_x_assum (qspecl_then [`vF`, `m`] irule)
+               \\ qexists_tac `m` \\ fs[])
+           >- (irule ssa_equal_set
+               \\ qexists_tac `insert n () (union fVars dVars)`
+               \\ conj_tac \\ TRY (fs[] \\ FAIL_TAC "")
+               \\ rewrite_tac [domain_union, domain_insert]
+               \\ rewrite_tac [UNION_DEF, INSERT_DEF]
+               \\ fs[EXTENSION]
+               \\ rpt strip_tac
+               \\ metis_tac[])
+           >- (irule swap_Gamma_bstep
+               \\ qexists_tac `updDefVars n M0 (toRMap Gamma)` \\ fs[]
+               \\ MATCH_ACCEPT_TAC Rmap_updVars_comm)
+           >- (fs[DIFF_DEF, domain_insert, SUBSET_DEF]
+               \\ rpt strip_tac \\ first_x_assum irule
+               \\ simp[Once freeVars_def]
+               \\ once_rewrite_tac [domain_union]
+               \\ fs[]
+               \\ rw_thm_asm `x IN domain (freeVars f)` freeVars_def
+               \\ fs[])
+           >- (rpt strip_tac \\ simp[updEnv_def]
+               \\ IF_CASES_TAC \\ fs[]
+               \\ rveq
+               \\ fs[domain_union])
+           >- (rpt strip_tac \\ fs[updDefVars_def]
+               \\ TOP_CASE_TAC \\ fs[])
+           >- (rpt gen_tac \\ disch_then assume_tac
+               \\ fs[updEnv_def] \\ rveq \\ fs[]
+               >- (qpat_x_assum `A e = A (Var n)` (fn thm => fs[GSYM thm]))
+               \\ TOP_CASE_TAC \\ rveq \\  fs[]
+               \\ qpat_x_assum `A e = A (Var n)` (fn thm => fs[GSYM thm]))
+           \\ rpt strip_tac
+           \\ fs[updEnv_def] \\ rveq \\ fs[]
+           >- (qpat_x_assum `eval_exp E2 Gamma e nF _` kall_tac
+               \\ drule FPRangeValidator_sound
+               \\ rpt (disch_then drule)
+               \\ disch_then irule \\ fs[]
+               \\ fs[DIFF_DEF, domain_insert, SUBSET_DEF]
+               \\ rpt strip_tac \\ first_x_assum irule
+               \\ simp[Once freeVars_def]
+               \\ once_rewrite_tac [domain_union]
+               \\ fs[]
+               \\ CCONTR_TAC \\ fs[] \\ rveq
+               \\ first_x_assum (qspec_then `n` assume_tac)
+               \\ res_tac)
+           \\ TOP_CASE_TAC \\ fs[]
            \\ qpat_x_assum `eval_exp E2 Gamma e nF _` kall_tac
-           \\ first_x_assum drule
-           \\ rw_asm_star `A e = _`)
-  \\ rw_asm_star `A e = _`
-  \\ qspecl_then [`vR`, `v`, `err_e`, `(e_lo,e_hi)`]
-       impl_subgoal_tac
-       (SIMP_RULE std_ss [contained_def, widenInterval_def] distance_gives_iv)
-  \\ fs[IVlo_def, IVhi_def]
-  \\ Cases_on `e`
-  >- (fs[]
-      >- (fs[validFloatValue_def]
-          \\ first_x_assum (qspecl_then [`n`] impl_subgoal_tac) \\ fs[domain_lookup]
-          \\ `tMap (Var n)  = SOME m` by (drule typingSoundnessExp  \\ rpt (disch_then drule)
-                                          \\ fs[])
-          \\ qpat_x_assum `tMap (Var n) = SOME _` (fn thm => fs[thm])
-          \\ inversion `eval_exp E2 _ _ _ _` eval_exp_cases
-          \\ qpat_x_assum `E2 n = SOME v` (fn thm => fs[thm])
-          \\ rveq  \\ fs[])
-      \\ solve_tac)
-  \\ solve_tac);
+           \\ drule FPRangeValidator_sound
+           \\ rpt (disch_then drule)
+           \\ disch_then irule \\ fs[]
+           \\ fs[DIFF_DEF, domain_insert, SUBSET_DEF]
+           \\ rpt strip_tac \\ first_x_assum irule
+           \\ simp[Once freeVars_def]
+           \\ once_rewrite_tac [domain_union]
+           \\ fs[]
+           \\ CCONTR_TAC \\ fs[] \\ rveq
+           \\ first_x_assum (qspec_then `n` assume_tac)
+           \\ res_tac)
+       \\ fs[])
+  \\ rpt (inversion `bstep (Ret _) _ _ _ _` bstep_cases)
+  \\ drule FPRangeValidator_sound
+  \\ rpt (disch_then drule)
+  \\ fs[]);
\ No newline at end of file

coq/IEEE_connection.v

@@ -5,33 +5,38 @@ Require Import Daisy.Expressions Daisy.Infra.RationalSimps
 Require Import Flocq.Appli.Fappli_IEEE_bits Flocq.Appli.Fappli_IEEE
         Flocq.Core.Fcore_Raux Flocq.Prop.Fprop_relative.
 
-Definition valid_div a b (f:binary_float a b):=
-  match f with
-  |B754_finite _ _ _ _ _ _ => true
-  |_ => false
+Fixpoint eval_exp_float (e:exp (binary_float 53 1024)) (E:nat -> option (binary_float 53 1024)):=
+  match e with
+  | Var _ x => E x
+  | Const m v => Some v
+  | Unop Neg e =>
+    match eval_exp_float e E with
+    |Some v1 => Some (b64_opp v1)
+    |_ => None
+    end
+  | Unop Inv e => None
+  | Binop b e1 e2 =>
+    match eval_exp_float e1 E, eval_exp_float e2 E with
+    | Some f1, Some f2 =>
+      match b with
+      | Plus => Some (b64_plus mode_NE f1 f2)
+      | Sub => Some (b64_minus mode_NE f1 f2)
+      | Mult => Some (b64_mult mode_NE f1 f2)
+      | Div => Some (b64_div mode_NE f1 f2)
+      end
+    |_ , _ => None
+    end
+  | _ => None
   end.
 
-(* Fixpoint eval_exp_float (e:exp (binary_float 53 1024)) (E:nat -> option (binary_float 53 1024)):= *)
-(*   match e with *)
-(*   |Const c => if (is_finite 53 1024 c) then Some c else None *)
-(*   |Var _ x => E x *)
-(*   |Binop b e1 e2 => *)
-(*    match eval_exp_float e1 E, eval_exp_float e2 E with *)
-(*    |Some f1, Some f2 => *)
-(*     if (is_finite 53 1024 f1 && is_finite 53 1024 f2) *)
-(*     then *)
-(*       match b with *)
-(*       |Plus => Some (b64_plus mode_NE f1 f2) *)
-(*       |Sub => Some (b64_minus mode_NE f1 f2) *)
-(*       |Mult => Some (b64_mult mode_NE f1 f2) *)
-(*       |Div => if (valid_div f2) then Some (b64_div mode_NE f1 f2) else None *)
-(*       end *)
-(*     else *)
-(*       None *)
-(*      |_ , _ => None *)
-(*    end *)
-(*    | _ => None *)
-(*   end. *)
+Definition optionLift (A B:Type) (e:option A) (some_cont:A -> B) (none_cont:B) :=
+  match e with
+  | Some v => some_cont v
+  | None => none_cont
+  end.
+
+Definition normal_or_zero v :=
+  Qeq_bool v 0 || Qle_bool (minValue M64) (Qabs v).
 
 (* Lemma eval_exp_float_finite e E: *)
 (*   forall v, eval_exp_float e E = Some v -> *)

coq/Infra/Ltacs.v

@@ -32,6 +32,18 @@ Ltac canonize_Q_to_R :=
 
 Ltac canonize_hyps := repeat canonize_Q_prop; repeat canonize_Q_to_R.
 
+Ltac Q2R_to_head_step :=
+  match goal with
+  | [ H: context[Q2R ?a + Q2R ?b] |- _] => rewrite <- Q2R_plus in H
+  | [ H: context[Q2R ?a - Q2R ?b] |- _] => rewrite <- Q2R_minus in H
+  | [ H: context[Q2R ?a * Q2R ?b] |- _] => rewrite <- Q2R_minus in H
+  | [ |- context[Q2R ?a + Q2R ?b]] => rewrite <- Q2R_plus
+  | [ |- context[Q2R ?a - Q2R ?b]] => rewrite <- Q2R_minus
+  | [ |- context[Q2R ?a * Q2R ?b]] => rewrite <- Q2R_minus
+  end.
+
+Ltac Q2R_to_head := repeat Q2R_to_head_step.
+
 Ltac NatSet_simp hyp :=
   try rewrite NatSet.mem_spec in hyp;
   try rewrite NatSet.equal_spec in hyp;
@@ -66,4 +78,13 @@ Ltac destruct_if :=
     intros name;
     rewrite name in *;
     try congruence
-  end .
\ No newline at end of file
+  end.
+
+(* HOL4 Style patter matching tactics *)
+Tactic Notation "lift " tactic(t) :=
+  fun H => t H.
+
+Tactic Notation "match_pat" open_constr(pat) tactic(t) :=
+  match goal with
+  | [H: ?ty |- _ ] => unify pat ty; t H
+  end.
\ No newline at end of file

coq/Infra/MachineType.v

@@ -184,13 +184,13 @@ Definition normal (v:Q) (m:mType) :=
   Qle_bool (minValue m) (Qabs v) && Qle_bool (Qabs v) (maxValue m).
 
 Definition denormal (v:Q) (m:mType) :=
-  Qle_bool (minValue m) (Qabs v) && Qle_bool (Qabs v) (maxValue m).
+  Qle_bool (Qabs v) (minValue m) && negb (Qeq_bool v 0).
 
 Definition Normal (v:R) (m:mType) :=
   (Q2R (minValue m) <= (Rabs v) /\ (Rabs v) <= Q2R (maxValue m))%R.
 
 Definition Denormal (v:R) (m:mType) :=
-  (Q2R (minValue m) <= (Rabs v) /\ (Rabs v) <= Q2R (maxValue m))%R.
+  ((Rabs v) <= Q2R (minValue m) /\ ~ (v = 0))%R.
 (**
   Predicate that is true if and only if the given value v is a valid
   floating-point value according to the the type m.

coq/Infra/RealRationalProps.v

@@ -149,4 +149,13 @@ Lemma Rabs_0_equiv:
   (Rbasic_fun.Rabs 0 <= Q2R 0)%R.
 Proof.
   rewrite Q2R0_is_0, Rbasic_fun.Rabs_R0; lra.
+Qed.
+
+Lemma bounded_inAbs a b c:
+  (a <= b <= c -> (Rabs b <= Rabs c) \/ Rabs b <= Rabs a)%R.
+Proof.
+  intros.
+  unfold Rabs.
+  destruct (Rcase_abs b); destruct (Rcase_abs c); destruct (Rcase_abs a);
+    lra.
 Qed.
\ No newline at end of file