Finish IEE validator soundness in Coq

coq/ErrorValidation.v

@@ -2256,13 +2256,14 @@ Proof.
     + rename R into valid_rec.
       rewrite (typingSoundnessExp _ _  L0 eval_float_e) in *;
         simpl in *.
+      destruct (Gamma (Var Q n)) eqn:?; try congruence.
       match goal with
       | [ H: _ && _ = true |- _] => andb_to_prop H
       end.
       type_conv.
       destruct (IHf absenv (updEnv n v E1) (updEnv n vF E2) outVars fVars
                     (NatSet.add n dVars) vR elo ehi err P Gamma
-                    (updDefVars n m defVars))
+                    (updDefVars n m0 defVars))
         as [vF_res [m_res step_res]];
         eauto.
       { eapply ssa_equal_set; eauto.
@@ -2381,13 +2382,14 @@ Proof.
     rename R into valid_rec.
     rewrite (typingSoundnessExp _ _  L0 eval_float_e) in *;
       simpl in *.
+    destruct (Gamma (Var Q n)); try congruence.
     match goal with
     | [ H: _ && _ = true |- _] => andb_to_prop H
     end.
     type_conv.
     apply (IHf absenv (updEnv n v E1) (updEnv n v0 E2) outVars fVars
                (NatSet.add n dVars) vR vF mF elo ehi err P Gamma
-               (updDefVars n m defVars));
+               (updDefVars n m0 defVars));
       eauto.
     + eapply approxUpdBound; try auto.
       simpl in *.

coq/FPRangeValidator.v

@@ -68,7 +68,7 @@ Ltac prove_fprangeval m v L1 R:=
   destruct (Rle_lt_dec (Rabs v) (Q2R (maxValue m)))%R; lra.
 
 
-Theorem FpRangeValidator_sound:
+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 ->
@@ -151,8 +151,8 @@ Proof.
     prove_fprangeval m v L1 R.
 Qed.
 
-Lemma FPRangeValidatorCmd_sound (f:cmd Q) E1 E2 Gamma v vR m A tMap P fVars dVars
-      outVars:
+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 ->
@@ -187,113 +187,101 @@ Proof.
       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
-           \\ 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
+      - assert (tMap e = Some m)
+          by(eapply typingSoundnessExp; eauto).
+        match_pat (ssa _ _ _) (fun H => inversion H; subst; simpl in *).
+        destruct (A e) as [iv_e err_e] eqn:?;
+          destruct iv_e as [e_lo e_hi] eqn:?.
+        edestruct (validErrorbound_sound e (E1:=E1) (E2:=E2) (fVars:=fVars) (dVars := dVars) P (absenv:=A) (nR:=v0) (err:=err_e)) as [[vF_e [m_e eval_float_e]] err_bounded_e]; eauto.
+        + set_tac. split; try auto.
+          rewrite NatSet.remove_spec, NatSet.union_spec; split; try auto.
+          hnf; intros; subst.
+          set_tac.
+        + intros. apply H10; auto; set_tac.
+        + intros; apply H8; auto. rewrite <- NatSet.mem_spec; auto.
+        + intros. apply H9; set_tac. rewrite <- NatSet.union_spec; auto.
+        + edestruct (validIntervalbounds_sound e A P (fVars:=fVars) (dVars:=dVars) E1); eauto.
+          * intros. apply H10; auto; set_tac.
+          * set_tac. split; try auto.
+            rewrite NatSet.remove_spec, NatSet.union_spec; split; try auto.
+            hnf; intros; subst.
+            set_tac.
+          * intros. apply H8. rewrite NatSet.mem_spec in *; auto.
+          * intros. instantiate (1:= Gamma); apply H9. set_tac.
+            rewrite NatSet.union_spec in *; auto.
+          * rewrite H3 in *.
+            destruct (tMap (Var Q n)) eqn:?; simpl in *; try congruence.
+            rename x into vR_e.
+            destruct H4 as [eval_e_real bounded_vR_e].
+            rewrite <- (meps_0_deterministic (toRExp e) eval_e_real H20) in *; try auto.
+            andb_to_prop R5.
+            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.
+            { apply approxUpdBound; auto.
+              simpl in *.
+              apply Rle_trans with (r2:= Q2R err_e); try lra.
+              rewrite Heqp in *; simpl in *.
+              eapply err_bounded_e. eauto.
+              apply Qle_Rle.
+              rewrite Qeq_bool_iff in *.
+              rewrite R1. 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.
+              - rewrite NatSet.remove_spec, NatSet.union_spec.
+                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.
+                exfalso; apply H16; set_tac.
+              - apply H8; auto. }
+            { intros. unfold updDefVars.
+              destruct (v2 =? n) eqn:?; eauto.
+              apply H9. destruct H4; try auto.
+              rewrite NatSet.add_spec in H4.
+              rewrite Nat.eqb_neq in *.
+              destruct H4; subst; try congruence; auto. }
+            { intros. unfold updEnv.
+              destruct (v2 =? n) eqn:?.
+              - exists vR_e. rewrite Nat.eqb_eq in *; subst.
+                split; try auto.
+                destruct bounded_vR_e;
+                  rewrite Heqp in *; simpl in *.
+                  split.
+                + apply Rle_trans with (r2:=Q2R e_lo); try lra.
+                  apply Qle_Rle. rewrite Qeq_bool_iff in *; rewrite R4; lra.
+                + apply Rle_trans with (r2:=Q2R e_hi); try lra.
+                  apply Qle_Rle; rewrite Qeq_bool_iff in *; rewrite R3; lra.
+              - apply H10. rewrite Nat.eqb_neq in *.
+                rewrite NatSet.add_spec in H4.
+                destruct H4; try auto; subst; congruence. }
+            { 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.
+                rewrite NatSet.remove_spec, NatSet.union_spec.
+                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.
\ No newline at end of file

coq/IEEE_connection.v

-Require Import Coq.Reals.Reals Coq.QArith.QArith Coq.micromega.Psatz
+Require Import Coq.Reals.Reals Coq.QArith.QArith Coq.QArith.Qabs Coq.micromega.Psatz
         Coq.QArith.Qreals.
 Require Import Daisy.Expressions Daisy.Infra.RationalSimps
         Daisy.Infra.RealRationalProps.

coq/Typing.v

@@ -101,9 +101,10 @@ Fixpoint typeCheckCmd (c:cmd Q) (Gamma:nat -> option mType) (tMap:exp Q -> optio
   match c with
   | Let m x e g => if typeCheck e Gamma tMap
                   then
-                    match tMap e with
-                    | Some me =>  mTypeEq me m && typeCheckCmd g (updDefVars x me Gamma) tMap
-                    | _ => false
+                    match tMap e, tMap (Var Q x) with
+                    | Some me, Some mx =>  mTypeEq me m && mTypeEq m mx
+                                          && typeCheckCmd g (updDefVars x me Gamma) tMap
+                    | _, _ => false
                     end
                   else
                     false
@@ -260,6 +261,7 @@ Proof.
     specialize (IHc (updDefVars n m0 Gamma) (updEnv n v0 E)).
     simpl.
     rewrite e_type_m0 in R.
+    destruct (expTypes (Var Q n)) eqn:?; try congruence.
     andb_to_prop R.
     apply IHc; auto.
   - simpl in *.

hol4/TypingScript.sml

@@ -48,7 +48,7 @@ val typeCmd_def = Define `
 val typeMapCmd_def = Define `
   typeMapCmd (Gamma: num -> mType option) (f: real cmd) (f': real exp) : mType option =
     case f of
-      | Let m n e c => if f' = (Var n) then
+      | Let m n e c => if f' = (Var n) then (*FIXME: This may fail because n not in Gamma... *)
                            (case Gamma n of
                               | SOME m' => if isMorePrecise m m' then SOME m else NONE
                               | NONE => NONE)