Finish translation with CakeML, prove IEEE connection for expressions

hol4/IntervalValidationScript.sml

@@ -396,7 +396,105 @@ val validIntervalboundsCmd_sound = store_thm (
   \\ simp[Once getRetExp_def, Once toREvalCmd_def]
   \\ fs[] \\ find_exists_tac \\ fs[ret_b]);
 
-(*
+val validIntervalbounds_validates_iv = store_thm ("validIntervalbounds_validates_iv",
+  ``!(f:real expr) (A:analysisResult) (P:precond) (dVars:num_set).
+      (!v. v IN domain dVars ==>
+           ? iv err. FloverMapTree_find (Var v) A = SOME (iv,err) /\
+           valid iv) /\
+      validIntervalbounds f A P dVars ==>
+      ? iv err.
+      FloverMapTree_find f A = SOME (iv, err) /\
+      valid iv``,
+  Induct_on `f`
+  \\ rpt strip_tac
+  \\ Flover_compute ``validIntervalbounds``
+  >- (first_x_assum (qspecl_then [`n`] destruct)
+      \\ fs[domain_lookup, valid_def, isSupersetInterval_def, validIntervalbounds_def]
+      \\ rveq \\ fs[])
+  >- (fs[isSupersetInterval_def, valid_def, validIntervalbounds_def]
+      \\ irule REAL_LE_TRANS
+      \\ asm_exists_tac \\ conj_tac \\ fs[IVlo_def, IVhi_def]
+      \\ irule REAL_LE_TRANS \\ asm_exists_tac \\ fs[])
+  >- (fs[valid_def, IVlo_def, IVhi_def]
+      \\ irule REAL_LE_TRANS \\ asm_exists_tac \\ fs[])
+  >- (first_x_assum (qspecl_then [`A`, `P`, `dVars`] destruct)
+      \\ fs[]
+      \\ rveq \\ Cases_on `u`
+      >- (`valid (negateInterval iv)`
+            by (irule iv_neg_preserves_valid \\ fs[])
+          \\ fs[valid_def, isSupersetInterval_def]
+          \\ irule REAL_LE_TRANS
+          \\ asm_exists_tac \\ fs[]
+          \\ irule REAL_LE_TRANS
+          \\ asm_exists_tac \\ fs[])
+      >- (`valid (invertInterval iv)`
+            by (irule iv_inv_preserves_valid \\ fs[])
+          \\ fs[valid_def, isSupersetInterval_def]
+          >- (irule REAL_LE_TRANS
+              \\ asm_exists_tac \\ fs[]
+              \\ irule REAL_LE_TRANS
+              \\ asm_exists_tac \\ fs[])
+          \\ irule REAL_LE_TRANS
+          \\ asm_exists_tac \\ fs[]
+          \\ irule REAL_LE_TRANS
+          \\ asm_exists_tac \\ fs[]))
+  >- (rename1 `Binop b f1 f2`
+      \\ rpt (first_x_assum (qspecl_then [`A`, `P`, `dVars`] destruct) \\ fs[])
+      \\ rveq \\ fs[]
+      \\ rename1 `FloverMapTree_find f1 A = SOME (iv_f1, err_f1)`
+      \\ rename1 `FloverMapTree_find f2 A = SOME (iv_f2, err_f2)`
+      \\ fs[]
+      \\ Cases_on `b`
+      >- (`valid (addInterval iv_f1 iv_f2)`
+            by (irule iv_add_preserves_valid \\ fs[])
+          \\ fs[valid_def, isSupersetInterval_def]
+          \\ irule REAL_LE_TRANS
+          \\ asm_exists_tac \\ fs []
+          \\ irule REAL_LE_TRANS
+          \\ asm_exists_tac \\ fs [])
+      >- (`valid (subtractInterval iv_f1 iv_f2)`
+            by (irule iv_sub_preserves_valid \\ fs[])
+          \\ fs[valid_def, isSupersetInterval_def]
+          \\ irule REAL_LE_TRANS
+          \\ asm_exists_tac \\ fs []
+          \\ irule REAL_LE_TRANS
+          \\ asm_exists_tac \\ fs [])
+      >- (`valid (multInterval iv_f1 iv_f2)`
+            by (irule iv_mult_preserves_valid \\ fs[])
+          \\ fs[valid_def, isSupersetInterval_def]
+          \\ irule REAL_LE_TRANS
+          \\ asm_exists_tac \\ fs []
+          \\ irule REAL_LE_TRANS
+          \\ asm_exists_tac \\ fs [])
+      >- (`valid (divideInterval iv_f1 iv_f2)`
+            by (match_mp_tac iv_div_preserves_valid \\ fs[])
+          \\ fs[valid_def, isSupersetInterval_def]
+          \\ match_mp_tac REAL_LE_TRANS
+          \\ asm_exists_tac \\ fs []
+          \\ match_mp_tac REAL_LE_TRANS
+          \\ asm_exists_tac \\ fs []))
+  >- (rename1 `Fma f1 f2 f3`
+      \\ rpt (first_x_assum (qspecl_then [`A`, `P`, `dVars`] destruct) \\ fs[])
+      \\ rveq \\ fs[]
+      \\ rename1 `FloverMapTree_find f1 A = SOME (iv_f1, err_f1)`
+      \\ rename1 `FloverMapTree_find f2 A = SOME (iv_f2, err_f2)`
+      \\ rename1 `FloverMapTree_find f3 A = SOME (iv_f3, err_f3)`
+      \\ fs[]
+      \\ `valid (addInterval iv_f1 (multInterval iv_f2 iv_f3))`
+            by (irule iv_add_preserves_valid \\ fs[]
+                \\ irule iv_mult_preserves_valid \\ fs[])
+      \\ fs[valid_def, isSupersetInterval_def]
+      \\ irule REAL_LE_TRANS
+      \\ asm_exists_tac \\ fs []
+      \\ irule REAL_LE_TRANS
+      \\ asm_exists_tac \\ fs [])
+ >- (first_x_assum (qspecl_then [`A`, `P`, `dVars`] destruct) \\ fs[]
+      \\ fs[isSupersetInterval_def, IVlo_def, IVhi_def]
+      \\ rveq
+      \\ `FST iv = FST intv` by (metis_tac[REAL_LE_ANTISYM])
+      \\ `SND iv = SND intv` by (metis_tac[REAL_LE_ANTISYM])
+      \\ fs[valid_def, IVlo_def, IVhi_def]));
+
 val validIntervalbounds_noDivzero_real = store_thm("validIntervalbounds_noDivzero_real",
   ``!(f1 f2:real expr) A (P:precond) (dVars:num_set).
       validIntervalbounds (Binop Div f1 f2) A P dVars ==>
@@ -405,7 +503,6 @@ val validIntervalbounds_noDivzero_real = store_thm("validIntervalbounds_noDivzer
       noDivzero (SND iv) (FST iv)``,
   rpt strip_tac \\ Flover_compute ``validIntervalbounds``
   \\ fs[noDivzero_def, IVhi_def, IVlo_def]);
-*)
 
 val validRanges_validates_iv = store_thm (
   "validRanges_validates_iv",

hol4/transScript.sml

@@ -27,26 +27,10 @@ val real_div_side = prove(
   |> update_precondition;
 (* / translation of real_div *)
 
-val check_rec_def = Define `
-  check_rec (input:Token list) (num_fun:num)=
-  case num_fun of
-    | SUC n' =>
-      (case dParse input of
-         | SOME ((dCmd, P, A, Gamma, fBits),NIL) =>
-           if CertificateCheckerCmd dCmd A P Gamma fBits
-           then "True\n"
-           else "False\n"
-         | SOME ((dCmd, P, A, Gamma, fBits), residual) =>
-           if CertificateCheckerCmd dCmd A P Gamma fBits
-           then check_rec residual n'
-           else "False\n"
-         | NONE => pp input(*"parse failure\n"*))
-    | _ => "failure num of functions"`;
-
 val check_def = Define `
-check (f:real cmd) (P:precond) (A:analysisResult) Gamma fBits (n:num) =
+check (f:real cmd) (P:precond) (A:analysisResult) Gamma (n:num) =
 case n of
- | SUC n' => (CertificateCheckerCmd f A P Gamma fBits /\ check f P A Gamma fBits n')
+ | SUC n' => (CertificateCheckerCmd f A P Gamma /\ check f P A Gamma n')
  | _ => T`
 
 val check_all_def = Define `
@@ -54,8 +38,8 @@ val check_all_def = Define `
     case num_fun of
       | SUC n =>
         (case (dParse input) of
-          | SOME ((f,P,A, Gamma, fBits), residual) =>
-            if (check f P A Gamma fBits iters)
+          | SOME ((f,P,A, Gamma), residual) =>
+            if (check f P A Gamma iters)
                 then case residual of
                       | a:: b => check_all n iters residual
                       | NIL => "True\n"
@@ -402,8 +386,8 @@ val precond_errorbounds_true = prove (``
   \\ qexists_tac `P` \\ fs []);
 
 val precond_is_true = prove (
-  ``!f absenv P exprTypes fBits.
-      certificatecheckercmd_side f absenv P exprTypes fBits``,
+  ``!f absenv P exprTypes.
+      certificatecheckercmd_side f absenv P exprTypes``,
    once_rewrite_tac [certificatecheckercmd_side_def]
    \\ rpt gen_tac
    \\ strip_tac