WIP

coq/binary/Makefile

 bytes:
-	ocamlc -c CoqChecker.mli
+	ocamlc -c CoqChecker.ml
 	ocamlc -o coq_checker_bytes nums.cma big.ml CoqChecker.ml coq_main.ml
 native:
-	ocamlc -c CoqChecker.mli
+	ocamlc -c CoqChecker.ml
 	ocamlc -o coq_checker_native nums.cma big.ml CoqChecker.ml coq_main.ml
 
 all: bytes native

hol4/IEEE_connectionScript.sml

@@ -365,23 +365,36 @@ Induct \\ fs[Once typeMap_def] \\ rpt strip_tac \\ fs[Once typeExpression_def] )
 val typing_is_64bit = store_thm("typing_is_64bit",
   ``!e.
       noDowncast e /\ is64BitEval e /\ (!v. v IN domain(usedVars e) ==> Gamma v = SOME M64) ==>
-      (typeMap Gamma e) e  = SOME M64``
+      (typeMap Gamma e) e  = SOME M64``,
 Induct
 \\ rpt strip_tac \\ simp[Once typeMap_def] \\ fs[is64BitEval_def, noDowncast_def]
 >- (first_x_assum irule \\ fs[usedVars_def])
 >- (fs [Once typeExpression_def]
+    \\ rewrite_tac [GSYM typeMap_eq_typeExp]
     \\ first_x_assum irule
->- (
+    \\ fs[Once usedVars_def])
+>- (fs [Once typeExpression_def]
+    \\ rewrite_tac [ GSYM typeMap_eq_typeExp]
+    \\ `typeMap Gamma e e = SOME M64`
+         by (first_x_assum irule \\ rpt strip_tac \\ first_x_assum irule
+             \\ simp[Once usedVars_def, domain_union])
+    \\ `typeMap Gamma e' e' = SOME M64`
+         by (first_x_assum irule \\ rpt strip_tac \\ first_x_assum irule
+             \\ simp[Once usedVars_def, domain_union])
+    \\ fs[join_def]));
+
 
 val bstep_gives_IEEE2 = store_thm ("bstep_gives_IEEE2",
   ``!(e:word64 exp) E1 E2 Gamma vR A P fVars dVars .
-      typeCheck (toRExp e) Gamma (\_. SOME M64) /\
+      typeCheck (toRExp e) Gamma (typeMap Gamma (toRExp e)) /\
       approxEnv E1 Gamma A fVars dVars (toREnv E2) /\
       validIntervalbounds (toRExp e) A P dVars /\
-      validErrorbound (toRExp e) (\_. SOME M64) A dVars /\
-      FPRangeValidator (toRExp e) A (\_. SOME M64) /\
+      validErrorbound (toRExp e) (typeMap Gamma (toRExp e)) A dVars /\
+      FPRangeValidator (toRExp e) A (typeMap Gamma (toRExp e)) /\
       eval_exp (toREnv E2) Gamma (toRExp e) vR M64 /\
       domain (usedVars (toRExp e)) DIFF domain dVars ⊆ domain fVars ∧
+      is64BitEval (toRExp e) /\
+      noDowncast e /\
       (∀v.
         v ∈ domain fVars ⇒
         ∃vR. E1 v = SOME vR ∧ FST (P v) ≤ vR ∧ vR ≤ SND (P v)) ∧