FF CakeML and finish porting of proofs to new finite maps for analysis result and type map

hol4/CertificateCheckerScript.sml

@@ -106,7 +106,7 @@ val CertificateCmd_checking_is_sound = store_thm ("CertificateCmd_checking_is_so
   \\ rpt strip_tac
   \\ `?outVars. ssa f (freeVars f) outVars` by (match_mp_tac validSSA_sound \\ fs[])
   \\ qspecl_then
-       [`f`, `A`, `E1`, `freeVars f`, `LN`, `outVars`, `elo`, `ehi`, `err`, `P`, `defVars`]
+       [`f`, `A`, `E1`, `freeVars f`, `LN`, `outVars`, `P`, `defVars`]
        destruct validIntervalboundsCmd_sound
   \\ fs[dVars_range_valid_def, vars_typed_def, fVars_P_sound_def]
   \\ qspecl_then

hol4/DaisyMapScript.sml

 open preamble
-open MachineTypeTheory ExpressionAbbrevsTheory
+open MachineTypeTheory ExpressionAbbrevsTheory DaisyTactics
 
 val _ = new_theory "DaisyMap";
 
@@ -32,6 +32,7 @@ val expCompare_def = Define `
         else (if u1 = Neg then Lt else Gt)
       | Unop _ _, Binop _ _ _ => Lt
       | Unop _ _, Downcast _ _ => Lt
+      | Unop _ _, Fma _ _ _ => Lt
       | Unop _ _, _ => Gt
       | Downcast m1 e1, Downcast m2 e2 =>
           if m1 = m2
@@ -59,7 +60,24 @@ val expCompare_def = Define `
                   | Lt => Lt
                   | Gt => Gt)
              | _ => res)
-     |_ , _ => Gt`;
+      | Fma e1 e2 e3, Fma e4 e5 e6 =>
+        (case expCompare e1 e4 of
+         | Eq =>
+           (case expCompare e2 e5 of
+           | Eq => expCompare e3 e6
+           | Lt => Lt
+           | Gt => Gt)
+         | Lt => Lt
+         | Gt => Gt)
+      | _ , Fma e1 e2 e3 => Lt
+      | Fma e1 e2 e3, _ => Gt
+      |_ , _ => Gt`;
+
+val expCompare_refl = store_thm (
+  "expCompare_refl",
+  ``!e. expCompare e e = Eq``,
+  Induct \\ rpt strip_tac \\ simp[ Once expCompare_def]
+  \\ Cases_on `b` \\ fs[] );
 
 val DaisyMapList_insert_def = Define `
   (DaisyMapList_insert e k NIL = [(e,k)]) /\
@@ -81,12 +99,12 @@ val DaisyMapTree_insert_def = Define `
   (DaisyMapTree_insert e k (Leaf (e1,k1)) =
      case (expCompare e e1) of
             | Lt => Node (e1,k1) (Leaf (e,k)) (LeafN)
-            | Eq => Leaf (e1,k1)
+            | Eq => Leaf (e1,k)
             | Gt => Node (e1,k1) (LeafN) (Leaf (e,k))) /\
   (DaisyMapTree_insert e k (Node (e1,k1) tl tr) =
      case (expCompare e e1) of
             | Lt => Node (e1,k1) (DaisyMapTree_insert e k tl) tr
-            | Eq => (Node (e1, k1) tl tr)
+            | Eq => (Node (e1, k) tl tr)
             | Gt => Node (e1,k1) tl (DaisyMapTree_insert e k tr))`;
 
 val DaisyMapTree_find_def = Define `
@@ -108,6 +126,28 @@ val DaisyMapTree_mem_def = Define `
 val DaisyMapTree_empty_def = Define `
   DaisyMapTree_empty = LeafN `;
 
+val DaisyMapTree_find_injective = store_thm (
+  "DaisyMapTree_find_injective",
+  ``!e a b Tree.
+      DaisyMapTree_find e Tree = SOME a /\
+      DaisyMapTree_find e Tree = SOME b ==>
+      a = b``,
+  rpt strip_tac
+  \\ Cases_on `Tree` \\ fs[DaisyMapTree_find_def]);
+
+val DaisyMapTree_correct = store_thm (
+  "DaisyMapTree_correct",
+  ``!Tree k v.
+      DaisyMapTree_find k (DaisyMapTree_insert k v Tree) = SOME v``,
+  Induct_on `Tree`
+  \\ fs[DaisyMapTree_find_def, DaisyMapTree_insert_def]
+  \\ rpt strip_tac \\ fs[expCompare_refl]
+  >- (Cases_on `a` \\ fs[DaisyMapTree_insert_def]
+      \\ Cases_on `expCompare k q` \\ fs[DaisyMapTree_find_def]
+      \\ first_x_assum irule \\ fs[])
+  \\ Cases_on `a` \\ fs[DaisyMapTree_insert_def]
+  \\ Cases_on `expCompare k q` \\ fs[DaisyMapTree_find_def, expCompare_refl]);
+
 val _ = type_abbrev ("typeMap", ``:(real exp # mType) binTree``);
 val _ = type_abbrev ("analysisResult", ``:(real exp # ((real # real) # real)) binTree``);
 

hol4/IntervalValidationScript.sml

@@ -379,7 +379,7 @@ val swap_Gamma_bstep = store_thm (
   >- (irule swap_Gamma_eval_exp \\ qexists_tac `Gamma1` \\ fs[]));
 
 val validIntervalboundsCmd_sound = store_thm ("validIntervalboundsCmd_sound",
-  ``!f A E fVars dVars outVars elo ehi err P Gamma.
+  ``!f A E fVars dVars outVars P Gamma.
       ssa f (union fVars dVars) outVars /\
       dVars_range_valid dVars E A /\
       fVars_P_sound fVars E P /\

hol4/TypingScript.sml

@@ -30,8 +30,6 @@ val typeExpression_def = Define `
         | SOME m1 => if (morePrecise m1 m) then SOME m else NONE
         | NONE => NONE`;
 
-!eval_funs;
-
 add_unevaluated_function ``typeExpression``;
 
 val typeMap_def = Define `

cakeml @ 80074542

-Subproject commit 19c41e5bac090d86a4245e2b6054ef710c42a402
+Subproject commit 800745426c5c2ef2f5c5475c26640641dd222f04

hol4/transScript.sml

 open preamble
-open simpLib (* realTheory  *)realLib RealArith stringTheory
+open simpLib realTheory realLib RealArith stringTheory
 
 open ml_translatorTheory ml_translatorLib cfTacticsLib basisProgTheory
 
@@ -234,9 +234,12 @@ val validerrorboundcmd_side_def = fetch "-" "validerrorboundcmd_side_def";
 val certificatecheckercmd_side_def = fetch "-" "certificatecheckercmd_side_def";
 
 val precond_validIntervalbounds_true = prove (
-  ``!e absenv P (dVars:num_set).
-      (!v. v IN (domain dVars) ==> valid (FST (absenv (Var v)))) ==>
-      validintervalbounds_side e absenv P dVars``,
+  ``!e A P (dVars:num_set).
+      (!v. v IN (domain dVars) ==>
+        ?iv err.
+          DaisyMapTree_find (Var v) A = SOME (iv, err) /\
+          valid iv) ==>
+      validintervalbounds_side e A P dVars``,
   recInduct validIntervalbounds_ind
   \\ rw[]
   \\ once_rewrite_tac [validintervalbounds_side_def]
@@ -245,37 +248,37 @@ val precond_validIntervalbounds_true = prove (
   >- (once_rewrite_tac [GSYM noDivzero_def]
       \\ rpt strip_tac
       \\ rveq
-      \\ `valid (FST(absenv e))`
-           by (irule validIntervalbounds_validates_iv
-               \\ qexistsl_tac [`P`, `validVars`]
-               \\ fs[])
+      \\ rename1 `DaisyMapTree_find e absenv = SOME (iv_e, err_e)`
+      \\ `valid iv_e`
+           by (drule validIntervalbounds_validates_iv
+               \\ disch_then (qspecl_then [`e`, `P`] destruct)
+               \\ fs[] \\ rveq \\ fs[])
       \\ once_rewrite_tac [invertinterval_side_def]
-      \\ rw_asm `absenv e = _`
-      \\ Cases_on `x2` \\ rename1 `absenv e = ((elo,ehi),err)`
-      \\ qpat_x_assum `!v. _` kall_tac
-      \\ qpat_x_assum `!intv. _` kall_tac
-      \\ fs [IVlo_def, IVhi_def, valid_def, noDivzero_def]
+      \\ rpt (qpat_x_assum `!v. _` kall_tac)
+      \\ fs [valid_def, noDivzero_def]
       \\ REAL_ASM_ARITH_TAC)
   >- (once_rewrite_tac [GSYM noDivzero_def]
       \\ rpt strip_tac
       \\ rveq
       \\ once_rewrite_tac [divideinterval_side_def]
       \\ once_rewrite_tac [invertinterval_side_def]
-      \\ `valid (FST(absenv e0))`
-           by (irule validIntervalbounds_validates_iv
-               \\ qexistsl_tac [`P`, `validVars`]
-               \\ fs[])
-      \\ Cases_on `x4` \\ rename1 `absenv e0 = ((elo,ehi),err)`
-      \\ qpat_x_assum `!v. _` kall_tac
-      \\ rpt (qpat_x_assum `!intv. _` kall_tac)
-      \\ qpat_x_assum `absenv e0 = _` (fn thm => fs [thm])
-      \\ fs [IVlo_def, IVhi_def, valid_def, noDivzero_def]
+      \\ rename1 `DaisyMapTree_find e0 absenv = SOME (iv_e, err_e)`
+      \\ `valid iv_e`
+           by (drule validIntervalbounds_validates_iv
+               \\ disch_then (qspecl_then [`e0`, `P`] destruct)
+               \\ fs[] \\ rveq \\ fs[])
+      \\ once_rewrite_tac [invertinterval_side_def]
+      \\ rpt (qpat_x_assum `!v. _` kall_tac)
+      \\ fs [valid_def, noDivzero_def]
       \\ REAL_ASM_ARITH_TAC));
 
 val precond_validIntervalboundsCmd_true = prove (
-  ``!f absenv P (dVars:num_set).
-      (!v. v IN (domain dVars) ==> valid (FST (absenv (Var v)))) ==>
-      validintervalboundscmd_side f absenv P dVars``,
+  ``!f A P (dVars:num_set).
+      (!v. v IN (domain dVars) ==>
+        ?iv err.
+          DaisyMapTree_find (Var v) A = SOME (iv, err) /\
+          valid iv) ==>
+      validintervalboundscmd_side f A P dVars``,
   recInduct validIntervalboundsCmd_ind
   \\ rpt strip_tac
   \\ once_rewrite_tac [validintervalboundscmd_side_def]
@@ -289,10 +292,13 @@ val precond_validIntervalboundsCmd_true = prove (
       \\ fs []));
 
 val precond_validErrorbound_true = prove (``
-  !P f expTypes absenv (dVars:num_set).
-    (!v. v IN (domain dVars) ==> valid (FST (absenv (Var v)))) /\
-    validIntervalbounds f absenv P dVars ==>
-    validerrorbound_side f expTypes absenv dVars ``,
+  !P f expTypes A (dVars:num_set).
+      (!v. v IN (domain dVars) ==>
+        ?iv err.
+          DaisyMapTree_find (Var v) A = SOME (iv, err) /\
+          valid iv) /\
+    validIntervalbounds f A P dVars ==>
+    validerrorbound_side f expTypes A dVars ``,
   gen_tac
   \\ recInduct validErrorbound_ind
   \\ rpt gen_tac
@@ -302,82 +308,77 @@ val precond_validErrorbound_true = prove (``
   \\ once_rewrite_tac [GSYM noDivzero_def]
   \\ rpt gen_tac \\ disch_then (fn thm => fs [thm] \\ ASSUME_TAC thm)
   \\ rpt gen_tac
-  \\ ntac 2 (disch_then ASSUME_TAC)
+  \\ disch_then ASSUME_TAC
+  \\ rpt gen_tac
+  \\ rpt (disch_then assume_tac)
   \\ rpt gen_tac
   \\ conj_tac
   >- (rpt strip_tac
       \\ rveq
       \\ fs[]
       \\ first_x_assum irule
-      \\ rw_thm_asm `validIntervalbounds _ _ _ _` validIntervalbounds_def
-      \\ rw_asm_star `absenv _ = _`
-      \\ Cases_on `absenv x15`
-      \\ fs [])
+      \\ Daisy_compute ``validIntervalbounds``)
   \\ conj_tac
   >- (disch_then (fn thm => fs [thm] \\ ASSUME_TAC thm)
       \\ conj_tac
-      >- (conj_tac \\ first_x_assum match_mp_tac
+      >- (conj_tac \\ rpt strip_tac \\ first_x_assum match_mp_tac
           \\ fs [Once validIntervalbounds_def])
-      >- (disch_then ASSUME_TAC
-          \\ rpt gen_tac
-          \\ disch_then (fn thm => fs [thm] \\ ASSUME_TAC thm)
-          \\ rpt gen_tac
-          \\ disch_then (fn thm => fs [thm] \\ ASSUME_TAC thm)
-          \\ rpt (disch_then ASSUME_TAC)
-          \\ rveq
-          \\ rename1 `absenv (Binop Div e1 e2) = (ivDiv, errDiv)`
-          \\ rename1 `absenv e1 = (ive1,err1)`
-          \\ Cases_on `ive1` \\ rename1 `absenv e1 = ((e1lo,e1hi), err1)`
-          \\ rename1 `absenv e2 = (ive2,err2)`
-          \\ Cases_on `ive2` \\ rename1 `absenv e2 = ((e2lo,e2hi), err2)`
-          \\ rewrite_tac [divideinterval_side_def, widenInterval_def, minAbsFun_def, invertinterval_side_def, IVlo_def, IVhi_def]
-          \\ `valid (FST(absenv e1)) /\ valid (FST(absenv e2))`
-               by (conj_tac \\ drule validIntervalbounds_validates_iv
-                   >- (disch_then match_mp_tac
-                       \\ qexists_tac `P`
-                       \\ fs [Once validIntervalbounds_def])
-                   >- (disch_then match_mp_tac
-                       \\ qexists_tac `P`
-                       \\ fs [Once validIntervalbounds_def]))
-          \\ rw_asm `absenv e1 = _`
-          \\ rw_asm `absenv e2 = _`
-          \\ qpat_x_assum `!v. _` kall_tac
-          \\ `0 <= err2`
-               by (drule err_always_positive
-                 \\ disch_then (fn thm => qspecl_then [`e2lo,e2hi`, `err2`] match_mp_tac thm)
-                 \\ fs [])
-        \\ `e2lo - err2 <> 0 /\ e2hi + err2 <> 0`
-             by (fs [noDivzero_def, IVlo_def, IVhi_def, widenInterval_def, valid_def]
-                 \\ conj_tac \\ REAL_ASM_ARITH_TAC)
-        \\ `noDivzero (SND (FST (absenv e2))) (FST (FST (absenv e2)))`
-             by (drule validIntervalbounds_noDivzero_real
-                 \\ fs [])
-        \\ `abs (e2lo - err2) <> 0 /\ abs (e2hi + err2) <> 0`
-             by (REAL_ASM_ARITH_TAC)
-        \\ `min (abs (e2lo - err2)) (abs (e2hi + err2)) <> 0`
-             by (fs [min_def]
-                 \\ Cases_on `abs (e2lo - err2) <= abs (e2hi + err2)`
-                 \\ fs [] \\ REAL_ASM_ARITH_TAC)
-        \\ qpat_x_assum `absenv e2 = _` (fn thm => fs [thm])
-        \\ fs [noDivzero_def, valid_def, IVhi_def, IVlo_def]
-        \\ REAL_ASM_ARITH_TAC))
+      \\ disch_then assume_tac
+      \\ rpt gen_tac
+      \\ disch_then (fn thm => fs [thm] \\ ASSUME_TAC thm)
+      \\ rpt gen_tac
+      \\ disch_then (fn thm => fs [thm] \\ ASSUME_TAC thm)
+      \\ rpt (disch_then ASSUME_TAC)
+      \\ ntac 2 (rpt gen_tac \\ rpt (disch_then assume_tac))
+      \\ rveq
+      \\ rename1 `Binop Div e1 e2`
+      \\ rename1 `DaisyMapTree_find e1 A = SOME (iv_e1, err1)`
+      \\ rename1 `DaisyMapTree_find e2 A = SOME (iv_e2, err2)`
+      \\ rewrite_tac [divideinterval_side_def, widenInterval_def,
+                  minAbsFun_def, invertinterval_side_def, IVlo_def,
+                  IVhi_def]
+      \\ `valid iv_e1 /\ valid iv_e2`
+           by (conj_tac \\ drule validIntervalbounds_validates_iv
+               >- (disch_then (qspecl_then [`e1`, `P`] destruct)
+                   \\ fs [Once validIntervalbounds_def] \\ rveq \\ fs[])
+               \\ disch_then (qspecl_then [`e2`, `P`] destruct)
+               \\ fs [Once validIntervalbounds_def] \\ rveq \\ fs[])
+      \\ qpat_x_assum `!v. _` kall_tac
+      \\ `0 <= err2`
+           by (drule err_always_positive
+               \\ disch_then (fn thm => qspecl_then [`iv_e2`, `err2`] match_mp_tac thm)
+               \\ fs [])
+      \\ `FST iv_e2 - err2 <> 0 /\ SND iv_e2 + err2 <> 0`
+         by (fs [noDivzero_def, IVlo_def, IVhi_def, widenInterval_def, valid_def]
+             \\ conj_tac \\ REAL_ASM_ARITH_TAC)
+      \\ `noDivzero (SND iv_e2) (FST iv_e2)`
+         by (drule validIntervalbounds_noDivzero_real
+             \\ fs [])
+      \\ `abs (FST iv_e2 - err2) <> 0 /\ abs (SND iv_e2 + err2) <> 0`
+         by (REAL_ASM_ARITH_TAC)
+      \\ `min (abs (FST iv_e2 - err2)) (abs (SND iv_e2 + err2)) <> 0`
+         by (fs [min_def]
+             \\ Cases_on `abs (FST iv_e2 - err2) <= abs (SND iv_e2 + err2)`
+             \\ fs [] \\ REAL_ASM_ARITH_TAC)
+      \\ fs [noDivzero_def, valid_def, IVhi_def, IVlo_def]
+      \\ REAL_ASM_ARITH_TAC)
   \\ conj_tac
-  >- (disch_then (fn thm => fs [thm] \\ ASSUME_TAC thm)
-      \\ rpt conj_tac \\ first_x_assum match_mp_tac
-          \\ fs [Once validIntervalbounds_def])
+  >- (rpt strip_tac
+      \\ rveq
+      \\ Daisy_compute ``validIntervalbounds``
+      \\ first_x_assum irule \\ fs[])
   \\ rpt strip_tac
-  \\ rveq
-  \\ fs[]
-  \\ first_x_assum irule
-  \\ rw_thm_asm `validIntervalbounds _ _ _ _` validIntervalbounds_def
-  \\ rw_asm_star `absenv _ = _`
-  \\ rw_asm_star `absenv (Downcast _ _) = _`);
+  \\ rveq \\ Daisy_compute ``validIntervalbounds``
+  \\ first_x_assum irule \\ fs[]);
 
 val precond_errorbounds_true = prove (``
-  !P f expTypes absenv dVars.
-    (!v. v IN domain dVars ==> valid (FST (absenv (Var v)))) /\
-    validIntervalboundsCmd f absenv P dVars ==>
-    validerrorboundcmd_side f expTypes absenv dVars``,
+  !P f expTypes A dVars.
+    (!v. v IN (domain dVars) ==>
+      ?iv err.
+        DaisyMapTree_find (Var v) A = SOME (iv, err) /\
+        valid iv) /\
+    validIntervalboundsCmd f A P dVars ==>
+    validerrorboundcmd_side f expTypes A dVars``,
   gen_tac
   \\ recInduct validErrorboundCmd_ind
   \\ rpt strip_tac
@@ -386,18 +387,17 @@ val precond_errorbounds_true = prove (``
   >- (rpt strip_tac
       >- (irule precond_validErrorbound_true \\ fs[]
           \\ qexists_tac `P` \\ fs [])
-      >- (first_x_assum irule
-          \\ rpt (conj_tac)
-          \\ fs[]
-          >- (gen_tac
-              \\ Cases_on `v = n` \\ fs[]
-              \\ rveq
-              \\ rw_sym_asm `env e = _`
-              \\ drule validIntervalbounds_validates_iv
-              \\ disch_then drule \\ fs[])
-          >- (Cases_on `c` \\ fs [Once validIntervalboundsCmd_def])))
-  >- (irule precond_validErrorbound_true \\ fs[]
-      \\ qexists_tac `P` \\ fs []));
+      \\ first_x_assum irule
+      \\ rpt (conj_tac)
+      \\ fs[]
+      >- (gen_tac
+          \\ Cases_on `v = n` \\ fs[]
+          \\ rveq
+          \\ drule validIntervalbounds_validates_iv
+          \\ disch_then drule \\ fs[])
+      \\ Cases_on `c` \\ fs [Once validIntervalboundsCmd_def])
+  \\ irule precond_validErrorbound_true \\ fs[]
+  \\ qexists_tac `P` \\ fs []);
 
 val precond_is_true = prove (
   ``!f absenv P expTypes.
@@ -424,6 +424,7 @@ recInduct str_of_num_ind
 \\ match_mp_tac LESS_TRANS
 \\ qexists_tac `10 + 48` \\ fs []) |> update_precondition;
 
+
 val res = translate runChecker_def;
 
 (* -- I/O routines from here onwards -- *)