WIP FPRangeValidator state

hol4/FPRangeValidatorScript.sml

@@ -14,13 +14,14 @@ open machine_ieeeTheory binary_ieeeTheory lift_ieeeTheory realTheory
 
 open AbbrevsTheory MachineTypeTheory TypingTheory RealSimpsTheory IntervalArithTheory
      ExpressionsTheory DaisyTactics IntervalValidationTheory ErrorValidationTheory
+     CommandsTheory EnvironmentsTheory ssaPrgsTheory
 
 val _ = new_theory "FPRangeValidator";
 
 val _ = temp_overload_on("abs",``real$abs``);
 
 val FPRangeValidator_def = Define `
-  FPRangeValidator (e:real exp) A (typeMap: real exp -> mType option) =
+  FPRangeValidator (e:real exp) A typeMap dVars =
     case typeMap e of
       | SOME m =>
         let (iv_e, err_e) = A e in
@@ -28,21 +29,40 @@ val FPRangeValidator_def = Define `
         let recRes =
             case e of
               | Binop b e1 e2 =>
-                FPRangeValidator e1 A typeMap /\
-                FPRangeValidator e2 A typeMap
+                FPRangeValidator e1 A typeMap dVars /\
+                FPRangeValidator e2 A typeMap dVars
               | Unop u e =>
-                FPRangeValidator e A typeMap
-              | Downcast m e => FPRangeValidator e A typeMap
+                FPRangeValidator e A typeMap dVars
+              | Downcast m e => FPRangeValidator e A typeMap dVars
               | _ =>  T
         in
-            if (validValue (IVhi iv_e_float) m /\
-                validValue (IVlo iv_e_float) m)
-            then ((normal (IVlo iv_e_float) m) \/ ((IVlo iv_e_float) = 0) \/
-                 normal (IVhi iv_e_float) m \/ (IVhi iv_e_float) = 0) /\ recRes
-            else
-                F
+            (case e of
+              | Var v =>
+                  if (lookup v dVars = SOME ())
+                  then T
+                  else
+                      if (validValue (IVhi iv_e_float) m /\
+                          validValue (IVlo iv_e_float) m)
+                      then ((normal (IVlo iv_e_float) m) \/ ((IVlo iv_e_float) = 0) \/
+                            normal (IVhi iv_e_float) m \/ (IVhi iv_e_float) = 0) /\ recRes
+                      else
+                          F
+              | _ => if (validValue (IVhi iv_e_float) m /\
+                          validValue (IVlo iv_e_float) m)
+                      then ((normal (IVlo iv_e_float) m) \/ ((IVlo iv_e_float) = 0) \/
+                            normal (IVhi iv_e_float) m \/ (IVhi iv_e_float) = 0) /\ recRes
+                      else
+                          F)
       | NONE => F`;
 
+val FPRangeValidatorCmd_def = Define `
+  (FPRangeValidatorCmd ((Let m x e g):real cmd) A typeMap dVars =
+     if FPRangeValidator e A typeMap dVars
+     then FPRangeValidatorCmd g A typeMap (insert x () dVars)
+     else F) /\
+  (FPRangeValidatorCmd (Ret e) A typeMap dVars =
+   FPRangeValidator e A typeMap dVars)`;
+
 val enclosure_to_abs = store_thm (
   "enclosure_to_abs",
   ``!a b c.
@@ -86,22 +106,38 @@ val normal_enclosing = store_thm (
   \\ fs[]
   \\ RealArith.REAL_ASM_ARITH_TAC);
 
+val solve_tac =
+  rpt (qpat_x_assum `!x. _` kall_tac)
+  \\ Cases_on `v = 0` \\ TRY(every_case_tac \\ fs[] \\ FAIL_TAC"")
+  \\ Cases_on `denormal v m` \\ TRY (every_case_tac \\ fs[] \\ FAIL_TAC "")
+  \\ Cases_on `normal v m` \\ TRY (every_case_tac \\ fs[] \\ FAIL_TAC"")
+  \\ fs[normal_def, denormal_def, validValue_def] \\ rveq \\ fs[]
+  \\ TRY (RealArith.REAL_ASM_ARITH_TAC)
+  \\ fs []
+  \\ every_case_tac  \\ fs[]
+  \\ `abs v <= abs (FST (widenInterval (e_lo, e_hi) err_e)) \/
+        abs v <= abs (SND (widenInterval (e_lo, e_hi) err_e))`
+        by (fs[widenInterval_def, IVlo_def, IVhi_def] \\ RealArith.REAL_ASM_ARITH_TAC)
+  \\ every_case_tac \\ RealArith.REAL_ASM_ARITH_TAC;
+
 val FPRangeValidator_sound = store_thm (
   "FPRangeValidator_sound",
-  ``!e E1 E2 Gamma v m A tMap P fVars dVars.
+  ``!e E1 E2 Gamma v m A tMap P fVars (dVars:num_set).
       approxEnv E1 Gamma A fVars dVars E2 /\
       eval_exp E2 Gamma e v m /\
       typeCheck e Gamma tMap /\
       validIntervalbounds e A P dVars /\
       validErrorbound e tMap A dVars /\
-      FPRangeValidator e A tMap /\
+      FPRangeValidator e A tMap dVars /\
       domain (usedVars e) DIFF (domain dVars) SUBSET (domain fVars) /\
       (!v. v IN domain fVars ==>
          ?vR. E1 v = SOME vR /\ FST (P v) <= vR /\ vR  <= SND (P v)) /\
       (!v. v IN domain fVars \/ v IN domain dVars ==>
          ?m. Gamma v = SOME m) /\
       (!v. v IN domain dVars ==>
-         ?vR. E1 v = SOME vR /\ FST (FST (A (Var v))) <= vR /\ vR <= SND (FST (A (Var v)))) ==>
+         ?vR. E1 v = SOME vR /\ FST (FST (A (Var v))) <= vR /\ vR <= SND (FST (A (Var v)))) /\
+      (!(v:num). v IN domain dVars ==>
+        (?vF m. E2 v = SOME vF /\ tMap (Var v) = SOME m /\ validFloatValue vF m)) ==>
       validFloatValue v m``,
   once_rewrite_tac [FPRangeValidator_def] \\ rpt strip_tac
   \\`tMap e = SOME m`
@@ -127,16 +163,75 @@ val FPRangeValidator_sound = store_thm (
   \\ 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]
-  \\ rpt (qpat_x_assum `!x. _` kall_tac)
-  \\ Cases_on `v = 0` \\ TRY(every_case_tac \\ fs[] \\ FAIL_TAC"")
-  \\ Cases_on `denormal v m` \\ TRY (every_case_tac \\ fs[] \\ FAIL_TAC "")
-  \\ Cases_on `normal v m` \\ TRY (every_case_tac \\ fs[] \\ FAIL_TAC"")
-  \\ fs[normal_def, denormal_def, validValue_def] \\ rveq \\ fs[]
-  \\ TRY (RealArith.REAL_ASM_ARITH_TAC)
-  \\ every_case_tac  \\ fs[]
-      \\ `abs v <= abs (FST (widenInterval (e_lo, e_hi) err_e)) \/
-          abs v <= abs (SND (widenInterval (e_lo, e_hi) err_e))`
-        by (fs[widenInterval_def, IVlo_def, IVhi_def] \\ RealArith.REAL_ASM_ARITH_TAC)
-      \\ every_case_tac \\ RealArith.REAL_ASM_ARITH_TAC);
+  \\ 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);
+
+val FPRangeValidatorCmd_sound = store_thm (
+  "FPRangeValidatorCmd_sound",
+  ``!f E1 E2 Gamma v vR m A tMap P fVars dVars outVars.
+      approxEnv E1 Gamma A fVars dVars E2 ∧
+      ssa f (union fVars dVars) outVars /\
+      bstep (toREvalCmd f) E1 (toRMap Gamma) vR m /\
+      bstep f E2 Gamma v m ∧
+      typeCheckCmd f Gamma tMap ∧
+      validIntervalboundsCmd f A P dVars ∧
+      validErrorboundCmd f tMap A dVars ∧
+      FPRangeValidatorCmd f A tMap dVars ∧
+      domain (freeVars f) DIFF domain dVars ⊆ domain fVars ∧
+      (∀v.
+        v ∈ domain fVars ⇒
+        ∃vR. E1 v = SOME vR ∧ FST (P v) ≤ vR ∧ vR ≤ SND (P v)) ∧
+      (∀v. v ∈ domain fVars ∨ v ∈ domain dVars ⇒ ∃m. Gamma v = SOME m) ∧
+      (∀v.
+        v ∈ domain dVars ⇒
+        ∃vR.
+          E1 v = SOME vR ∧ FST (FST (A (Var v))) ≤ vR ∧
+          vR ≤ SND (FST (A (Var v)))) ∧
+      (∀v.
+        v ∈ domain dVars ⇒
+        ∃vF m.
+          E2 v = SOME vF ∧ tMap (Var v) = SOME m ∧
+          validFloatValue vF m) ⇒
+      validFloatValue v m``,
+  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[]
+      \\ first_x_assum
+           (qspecl_then [`updEnv n vR_e E1`, `updEnv n vF_e E2`,
+                         `updDefVars n m Gamma`, `v`, `vR`, `mF`, `A`, `tMap`, `P`,
+                         `fVars`, `insert n () dVars`, `outVars`]
+              impl_subgoal_tac)
+       >- (inversion `ssa _ _ _` ssa_cases
+           \\ 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])
+               \\ drule validErrorbound_sound
+               \\ rpt (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[]
+);
 
 val _ = export_theory();