Merge with IEEE connection that has been proven in HOL4, as well as adding...

Merge with IEEE connection that has been proven in HOL4, as well as adding implementation of IEEE range validator in Coq and HOL4.

coq/CertificateChecker.v

@@ -6,7 +6,7 @@
 **)
 Require Import Coq.Reals.Reals Coq.QArith.Qreals.
 Require Import Daisy.Infra.RealSimps Daisy.Infra.RationalSimps Daisy.Infra.RealRationalProps Daisy.Infra.Ltacs.
-Require Import Daisy.IntervalValidation Daisy.ErrorValidation Daisy.Environments Daisy.Typing.
+Require Import Daisy.IntervalValidation Daisy.ErrorValidation Daisy.Environments Daisy.Typing Daisy.FPRangeValidator.
 
 Require Export Coq.QArith.QArith.
 Require Export Daisy.Infra.ExpressionAbbrevs Daisy.Commands.
@@ -14,7 +14,7 @@ Require Export Daisy.Infra.ExpressionAbbrevs Daisy.Commands.
 (** Certificate checking function **)
 Definition CertificateChecker (e:exp Q) (absenv:analysisResult) (P:precond) (defVars:nat -> option mType) :=
   if (typeCheck e defVars (typeMap defVars e)) then
-    if (validIntervalbounds e absenv P NatSet.empty)
+    if (validIntervalbounds e absenv P NatSet.empty) && FPRangeValidator e absenv (typeMap defVars e) NatSet.empty
     then (validErrorbound e (typeMap defVars e) absenv NatSet.empty)
     else false
   else false.
@@ -63,19 +63,21 @@ Proof.
   assert (NatSet.Subset (usedVars e -- NatSet.empty) (Expressions.usedVars e)).
   { hnf; intros a in_empty.
     set_tac. }
-  assert (forall v, (v) mem (NatSet.empty) = true -> exists vR : R, E1 v = Some vR /\ (Q2R (fst (fst (absenv (Var Q v)))) <= vR <= Q2R (snd (fst (absenv (Var Q v)))))%R).
+  rename R into validFPRanges.
+  assert (forall v, (v) mem (NatSet.empty) = true -> exists vR :R, E1 v = Some vR /\ (Q2R (fst (fst (absenv (Var Q v)))) <= vR <= Q2R (snd (fst (absenv (Var Q v)))))%R).
   { intros v v_in_empty.
     rewrite NatSet.mem_spec in v_in_empty.
     inversion v_in_empty. }
   edestruct validIntervalbounds_sound as [vR [eval_real real_bounds_e]]; eauto.
-  destruct (validErrorbound_sound e P (typeMap defVars e) L approxE1E2 H0 eval_real R0 L0 H1 P_valid H absenv_eq) as [[vF [mF eval_float]] err_bounded]; auto.
+  destruct (validErrorbound_sound e P (typeMap defVars e) L approxE1E2 H0 eval_real R0 L1 H1 P_valid H absenv_eq) as [[vF [mF eval_float]] err_bounded]; auto.
   exists vR; exists vF; exists mF; split; auto.
 Qed.
 
 Definition CertificateCheckerCmd (f:cmd Q) (absenv:analysisResult) (P:precond) defVars:=
   if (typeCheckCmd f defVars (typeMapCmd defVars f) && validSSA f (freeVars f))
   then
-    if (validIntervalboundsCmd f absenv P NatSet.empty)
+    if (validIntervalboundsCmd f absenv P NatSet.empty) &&
+       FPRangeValidatorCmd f absenv (typeMapCmd defVars f) NatSet.empty
     then (validErrorboundCmd f (typeMapCmd defVars f) absenv NatSet.empty)
     else false
   else false.
@@ -114,6 +116,7 @@ Proof.
   { eapply ssa_equal_set; try eauto.
     apply NatSetProps.empty_union_2.
     apply NatSet.empty_spec. }
+  rename R into validFPRanges.
   assert (forall v, (v) mem (NatSet.empty) = true ->
                exists vR : R,
                  E1 v = Some vR /\ (Q2R (fst (fst (absenv (Var Q v)))) <= vR <= Q2R (snd (fst (absenv (Var Q v)))))%R) as no_dVars_valid.

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/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.
 Require Import Flocq.Appli.Fappli_IEEE_bits Flocq.Appli.Fappli_IEEE
         Flocq.Core.Fcore_Raux Flocq.Prop.Fprop_relative.
 
-Definition valid_div a b (f:binary_float a b):=
-  match f with
-  |B754_finite _ _ _ _ _ _ => true
-  |_ => false
+Fixpoint eval_exp_float (e:exp (binary_float 53 1024)) (E:nat -> option (binary_float 53 1024)):=
+  match e with
+  | Var _ x => E x
+  | Const m v => Some v
+  | Unop Neg e =>
+    match eval_exp_float e E with
+    |Some v1 => Some (b64_opp v1)
+    |_ => None
+    end
+  | Unop Inv e => None
+  | Binop b e1 e2 =>
+    match eval_exp_float e1 E, eval_exp_float e2 E with
+    | Some f1, Some f2 =>
+      match b with
+      | Plus => Some (b64_plus mode_NE f1 f2)
+      | Sub => Some (b64_minus mode_NE f1 f2)
+      | Mult => Some (b64_mult mode_NE f1 f2)
+      | Div => Some (b64_div mode_NE f1 f2)
+      end
+    |_ , _ => None
+    end
+  | _ => None
   end.
 
-(* Fixpoint eval_exp_float (e:exp (binary_float 53 1024)) (E:nat -> option (binary_float 53 1024)):= *)
-(*   match e with *)
-(*   |Const c => if (is_finite 53 1024 c) then Some c else None *)
-(*   |Var _ x => E x *)
-(*   |Binop b e1 e2 => *)
-(*    match eval_exp_float e1 E, eval_exp_float e2 E with *)
-(*    |Some f1, Some f2 => *)
-(*     if (is_finite 53 1024 f1 && is_finite 53 1024 f2) *)
-(*     then *)
-(*       match b with *)
-(*       |Plus => Some (b64_plus mode_NE f1 f2) *)
-(*       |Sub => Some (b64_minus mode_NE f1 f2) *)
-(*       |Mult => Some (b64_mult mode_NE f1 f2) *)
-(*       |Div => if (valid_div f2) then Some (b64_div mode_NE f1 f2) else None *)
-(*       end *)
-(*     else *)
-(*       None *)
-(*      |_ , _ => None *)
-(*    end *)
-(*    | _ => None *)
-(*   end. *)
+Definition optionLift (A B:Type) (e:option A) (some_cont:A -> B) (none_cont:B) :=
+  match e with
+  | Some v => some_cont v
+  | None => none_cont
+  end.
+
+Definition normal_or_zero v :=
+  Qeq_bool v 0 || Qle_bool (minValue M64) (Qabs v).
 
 (* Lemma eval_exp_float_finite e E: *)
 (*   forall v, eval_exp_float e E = Some v -> *)

coq/Infra/Ltacs.v

@@ -32,6 +32,18 @@ Ltac canonize_Q_to_R :=
 
 Ltac canonize_hyps := repeat canonize_Q_prop; repeat canonize_Q_to_R.
 
+Ltac Q2R_to_head_step :=
+  match goal with
+  | [ H: context[Q2R ?a + Q2R ?b] |- _] => rewrite <- Q2R_plus in H
+  | [ H: context[Q2R ?a - Q2R ?b] |- _] => rewrite <- Q2R_minus in H
+  | [ H: context[Q2R ?a * Q2R ?b] |- _] => rewrite <- Q2R_minus in H
+  | [ |- context[Q2R ?a + Q2R ?b]] => rewrite <- Q2R_plus
+  | [ |- context[Q2R ?a - Q2R ?b]] => rewrite <- Q2R_minus
+  | [ |- context[Q2R ?a * Q2R ?b]] => rewrite <- Q2R_minus
+  end.
+
+Ltac Q2R_to_head := repeat Q2R_to_head_step.
+
 Ltac NatSet_simp hyp :=
   try rewrite NatSet.mem_spec in hyp;
   try rewrite NatSet.equal_spec in hyp;
@@ -66,4 +78,13 @@ Ltac destruct_if :=
     intros name;
     rewrite name in *;
     try congruence
-  end .
\ No newline at end of file
+  end.
+
+(* HOL4 Style patter matching tactics *)
+Tactic Notation "lift " tactic(t) :=
+  fun H => t H.
+
+Tactic Notation "match_pat" open_constr(pat) tactic(t) :=
+  match goal with
+  | [H: ?ty |- _ ] => unify pat ty; t H
+  end.
\ No newline at end of file

coq/Infra/MachineType.v

@@ -11,7 +11,7 @@ Require Import Daisy.Infra.RealRationalProps.
 (**
    Define machine precision as datatype
  **)
-Inductive mType: Type := M0 | M32 | M64 | M128 | M256.
+Inductive mType: Type := M0 | M16 | M32 | M64. (*| M128 | M256*)
 
 (**
   Injection of machine types into Q
@@ -19,12 +19,14 @@ Inductive mType: Type := M0 | M32 | M64 | M128 | M256.
 Definition mTypeToQ (e:mType) :Q :=
   match e with
   | M0 => 0
+  | M16 => (Qpower (2#1) (Zneg 11))
   | M32 => (Qpower (2#1) (Zneg 24))
   | M64 => (Qpower (2#1) (Zneg 53))
+  (*
   (* the epsilons below match what is used internally in daisy,
   although these value do not match the IEEE standard *)
   | M128 => (Qpower (2#1) (Zneg 105))
-  | M256 => (Qpower (2#1) (Zneg 211))
+  | M256 => (Qpower (2#1) (Zneg 211)) *)
   end.
 
 Arguments mTypeToQ _/.
@@ -49,10 +51,11 @@ Qed.
 Definition mTypeEq (m1:mType) (m2:mType) :=
   match m1, m2 with
   | M0, M0 => true
+  | M16, M16 => true
   | M32, M32 => true
   | M64, M64 => true
-  | M128, M128 => true
-  | M256, M256 => true
+  (* | M128, M128 => true *)
+  (* | M256, M256 => true *)
   | _, _ => false
   end.
 
@@ -141,4 +144,67 @@ Definition join (m1:mType) (m2:mType) :=
 (*   unfold join. *)
 (*   intros. *)
 (*   destruct m1, m2; simpl in *; cbv in *; try congruence; try auto. *)
-(* Qed. *)
\ No newline at end of file
+(* Qed. *)
+
+Definition maxExponent (m:mType) :Z :=
+  match m with
+  | M0 => 0
+  | M16 => 15
+  | M32 => 127
+  | M64 => 1023
+  end.
+
+Definition minExponentPos (m:mType) :Z :=
+  match m with
+  | M0 => 0
+  | M16 => 14
+  | M32 => 126
+  | M64 => 1022
+  end.
+
+(**
+Goldberg - Handbook of Floating-Point Arithmetic: (p.183)
+(𝛃 - 𝛃^(1 - p)) * 𝛃^(e_max)
+
+which simplifies to 2^(e_max) for base 2
+**)
+Definition maxValue (m:mType) :=
+  Qpower (2#1) (maxExponent m).
+
+Definition minValue (m:mType) :=
+  Qinv (Qpower (2#1) (minExponentPos m)).
+
+(** Goldberg - Handbook of Floating-Point Arithmetic: (p.183)
+  𝛃^(e_min -p + 1) = 𝛃^(e_min -1) for base 2
+**)
+Definition minDenormalValue (m:mType) :=
+  Qinv (Qpower (2#1) (minExponentPos m - 1)).
+
+Definition normal (v:Q) (m:mType) :=
+  Qle_bool (minValue m) (Qabs v) && Qle_bool (Qabs v) (maxValue m).
+
+Definition denormal (v:Q) (m:mType) :=
+  Qle_bool (Qabs v) (minValue m) && negb (Qeq_bool v 0).
+
+Definition Normal (v:R) (m:mType) :=
+  (Q2R (minValue m) <= (Rabs v) /\ (Rabs v) <= Q2R (maxValue m))%R.
+
+Definition Denormal (v:R) (m:mType) :=
+  ((Rabs v) <= Q2R (minValue m) /\ ~ (v = 0))%R.
+(**
+  Predicate that is true if and only if the given value v is a valid
+  floating-point value according to the the type m.
+  Since we use the 1 + 𝝳 abstraction, the value must either be
+  in normal range or 0.
+**)
+Definition validFloatValue (v:R) (m:mType) :=
+  match m with
+  | M0 => True
+  | _ => Normal v m \/ Denormal v m \/ v = 0%R
+  end.
+
+Definition validValue (v:Q) (m:mType) :=
+  match m with
+  | M0 => true
+  | _ => Qle_bool (Qabs v) (maxValue m)
+  end.
\ No newline at end of file

coq/Infra/RealRationalProps.v

@@ -149,4 +149,13 @@ Lemma Rabs_0_equiv:
   (Rbasic_fun.Rabs 0 <= Q2R 0)%R.
 Proof.
   rewrite Q2R0_is_0, Rbasic_fun.Rabs_R0; lra.
+Qed.
+
+Lemma bounded_inAbs a b c:
+  (a <= b <= c -> (Rabs b <= Rabs c) \/ Rabs b <= Rabs a)%R.
+Proof.
+  intros.
+  unfold Rabs.
+  destruct (Rcase_abs b); destruct (Rcase_abs c); destruct (Rcase_abs a);
+    lra.
 Qed.
\ No newline at end of file

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 *.

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/CertificateCheckerScript.sml

@@ -5,10 +5,11 @@
    as shown in the soundness theorem.
 **)
 open preamble
-open simpLib realTheory realLib RealArith
-open AbbrevsTheory ExpressionsTheory RealSimpsTheory DaisyTactics
-open ExpressionAbbrevsTheory ErrorBoundsTheory IntervalArithTheory
-open IntervalValidationTheory ErrorValidationTheory ssaPrgsTheory
+
+open simpLib realTheory realLib RealArith RealSimpsTheory
+open AbbrevsTheory ExpressionsTheory DaisyTactics ExpressionAbbrevsTheory
+     ErrorBoundsTheory IntervalArithTheory IntervalValidationTheory
+     ErrorValidationTheory ssaPrgsTheory FPRangeValidatorTheory
 
 val _ = new_theory "CertificateChecker";
 val _ = temp_overload_on("abs",``real$abs``);
@@ -17,7 +18,7 @@ val _ = temp_overload_on("abs",``real$abs``);
 val CertificateChecker_def = Define
   `CertificateChecker (e:real exp) (absenv:analysisResult) (P:precond) (defVars: num -> mType option)=
    if (typeCheck e defVars (typeMap defVars e)) then
-       if (validIntervalbounds e absenv P LN) then
+       if (validIntervalbounds e absenv P LN /\ FPRangeValidator e absenv (typeMap defVars e) LN) then
            (validErrorbound e (typeMap defVars e) absenv LN)
        else F
    else F`;
@@ -25,7 +26,7 @@ val CertificateChecker_def = Define
 val CertificateCheckerCmd_def = Define
   `CertificateCheckerCmd (f:real cmd) (absenv:analysisResult) (P:precond) defVars =
         if (typeCheckCmd f defVars (typeMapCmd defVars f) /\ validSSA f (freeVars f)) then
-            if (validIntervalboundsCmd f absenv P LN) then
+            if ((validIntervalboundsCmd f absenv P LN) /\ FPRangeValidatorCmd f absenv (typeMapCmd defVars f) LN) then
                 (validErrorboundCmd f (typeMapCmd defVars f) absenv LN)
             else F
         else F`;
@@ -51,7 +52,7 @@ val Certificate_checking_is_sound = store_thm ("Certificate_checking_is_sound",
         eval_exp E2 defVars e vF m /\
         (!vF m.
            eval_exp E2 defVars e vF m ==>
-           abs (vR - vF) <= (SND (absenv e)))``,
+           abs (vR - vF) <= (SND (absenv e)) /\ validFloatValue vF m)``,
 (**
    The proofs is a simple composition of the soundness proofs for the range
    validator and the error bound validator.
@@ -72,12 +73,16 @@ val Certificate_checking_is_sound = store_thm ("Certificate_checking_is_sound",
        destruct validErrorbound_sound
   \\ fs[]
   \\ qexistsl_tac [`vR`, `nF`, `m`] \\ fs[]
-  \\ rpt strip_tac \\ first_x_assum irule \\ fs[]
-  \\ asm_exists_tac \\ fs[]);
+  \\ rpt strip_tac
+  >- (first_x_assum irule \\ fs[]
+      \\ asm_exists_tac \\ fs[])
+  \\ irule FPRangeValidator_sound
+  \\ qexistsl_tac [`absenv`, `E1`, `E2`, `defVars`, `P`, `LN`,`e`, `fVars`, `typeMap defVars e`]
+  \\ fs[]);
 
 val CertificateCmd_checking_is_sound = store_thm ("CertificateCmd_checking_is_sound",
   ``!(f:real cmd) (absenv:analysisResult) (P:precond) defVars
-     (E1 E2:env) (outVars:num_set) fVars.
+     (E1 E2:env) (fVars:num_set).
       approxEnv E1 defVars absenv (freeVars f) LN E2 /\
       (!v.
           v IN (domain (freeVars f)) ==>

hol4/CommandsScript.sml

@@ -3,7 +3,7 @@
  **)
 open preamble
 open simpLib realTheory realLib RealArith
-open AbbrevsTheory ExpressionAbbrevsTheory MachineTypeTheory
+open AbbrevsTheory ExpressionsTheory ExpressionAbbrevsTheory MachineTypeTheory
 
 val _ = new_theory "Commands";
 
@@ -68,4 +68,17 @@ val definedVars_def = Define `
       |Let m (x:num) e g => insert x () (definedVars g)
       |Ret e => LN`;
 
+val bstep_eq_env = store_thm (
+  "bstep_eq_env",
+  ``!f E1 E2 Gamma v m.
+      (!x. E1 x = E2 x) /\
+      bstep f E1 Gamma v m ==>
+      bstep f E2 Gamma v m``,
+  Induct \\ rpt strip_tac \\ fs[bstep_cases]
+  >- (qexists_tac `v'` \\ conj_tac
+      \\ TRY (drule eval_eq_env \\ disch_then drule \\ fs[] \\ FAIL_TAC"")
+      \\ first_x_assum irule \\ qexists_tac `updEnv n v' E1` \\ fs[]
+      \\ rpt strip_tac \\ fs[updEnv_def])
+  \\ irule eval_eq_env \\ asm_exists_tac \\ fs[]);
+
 val _ = export_theory ();

hol4/ErrorValidationScript.sml

@@ -2554,6 +2554,7 @@ val validErrorboundCmd_gives_eval = store_thm (
            by (irule typingSoundnessExp
                \\ qexistsl_tac [`E2`, `Gamma`, `vF`] \\ fs[])
       \\ fs[]
+      \\ Cases_on `expTypes (Var n)` \\ fs[]
       \\ `?vF_res m_res. bstep f (updEnv n vF E2) (updDefVars n mF Gamma) vF_res m_res`
            by (first_x_assum irule
                \\ qexistsl_tac [`updEnv n v E1`, `P`, `absenv`,
@@ -2664,7 +2665,7 @@ val validErrorboundCmd_sound = store_thm ("validErrorboundCmd_sound",
       \\ rw_thm_asm `validIntervalboundsCmd _ _ _ _` validIntervalboundsCmd_def
       \\ rw_thm_asm `typeCheckCmd _ _ _` typeCheckCmd_def
       \\ `expTypes e = SOME m` by (irule typingSoundnessExp \\ qexistsl_tac [`E2`, `Gamma`, `vf`] \\ fs[])
-      \\ fs[]
+      \\ Cases_on `expTypes (Var n)` \\ fs[]
       \\ qexistsl_tac [`absenv`, `updEnv n vr E1`, `updEnv n vf E2`, `outVars`,
                        `fVars`, `insert n () dVars`, `elo`, `ehi`, `P`, `m'`,
                        `expTypes`, `updDefVars n m Gamma`]

hol4/ExpressionsScript.sml

@@ -290,6 +290,26 @@ val binary_unfolding = store_thm("binary_unfolding",
   fs [updEnv_def,updDefVars_def,join_def,eval_exp_cases,APPLY_UPDATE_THM,PULL_EXISTS]
   \\ metis_tac []);
 
+val eval_eq_env = store_thm (
+  "eval_eq_env",
+  ``!e E1 E2 Gamma v m.
+      (!x. E1 x = E2 x) /\
+      eval_exp E1 Gamma e v m ==>
+      eval_exp E2 Gamma e v m``,
+  Induct \\ rpt strip_tac \\ fs[eval_exp_cases]
+  >- (`E1 n = E2 n` by (first_x_assum irule)
+      \\ fs[])
+  >- (qexists_tac `delta'` \\ fs[])
+  >- (rveq \\ qexists_tac `v1` \\ fs[]
+      \\ first_x_assum drule \\ disch_then irule \\ fs[])
+  >- (rveq \\ qexists_tac `v1` \\ fs[]
+      \\ qexists_tac `delta'` \\ fs[]
+      \\ first_x_assum drule \\ disch_then irule \\ fs[])
+  >- (rveq \\ qexistsl_tac [`m1`, `m2`, `v1`, `v2`, `delta'`]
+      \\ fs[] \\ conj_tac \\ first_x_assum irule \\ asm_exists_tac \\ fs[])
+  >- (rveq \\ qexistsl_tac [`m1'`, `v1`, `delta'`] \\ fs[]
+      \\ first_x_assum drule \\ disch_then irule \\ fs[]));
+
 (* (** *)
 (*   Analogous lemma for unary expressions *)
 (* **) *)

hol4/Holmakefile

-INCLUDES = $(HOLDIR)/examples/machine-code/hoare-triple Infra cakeml/translator cakeml/basis cakeml/characteristic
+INCLUDES = $(HOLDIR)/examples/machine-code/hoare-triple Infra cakeml/translator cakeml/basis cakeml/characteristic cakeml/misc
 OPTIONS = QUIT_ON_FAILURE
 
 ifdef POLY

hol4/Infra/DaisyTactics.sml

@@ -95,4 +95,11 @@ fun destruct th =
       SUBGOAL_THEN hyp_to_prove (fn thm => STRIP_ASSUME_TAC (MP th thm))
   end
 
+fun impl_subgoal_tac th =
+  let
+      val hyp_to_prove = lhand (concl th)
+  in
+      SUBGOAL_THEN hyp_to_prove (fn thm => assume_tac (MP th thm))
+  end
+
 end

hol4/Infra/Holmakefile

-INCLUDES = $(HOLDIR)/examples/machine-code/hoare-triple ../cakeml/basis ../cakeml/characteristic
+INCLUDES = $(HOLDIR)/examples/machine-code/hoare-triple ../cakeml/basis ../cakeml/characteristic ../cakeml/misc
 OPTIONS = QUIT_ON_FAILURE

hol4/Infra/MachineTypeScript.sml

@@ -117,12 +117,18 @@ val minValue_def = Define `
 **)
 
 val minDenormalValue_def = Define `
-  minDenormalValue (m:mType) = 1 / (2 pow (minExponentPos m))`;
+  minDenormalValue (m:mType) = 1 / (2 pow (minExponentPos m - 1))`;
 
 val normal_def = Define `
   normal (v:real) (m:mType) =
     (minValue m <= abs v /\ abs v <= maxValue m)`;
 
+val denormal_def = Define `
+  denormal (v:real) (m:mType) =
+    case m of
+      | M0 => F
+      | _ => ((abs v) < (minValue m) /\ v <> 0)`;
+
 (**
   Predicate that is true if and only if the given value v is a valid
   floating-point value according to the the type m.
@@ -133,6 +139,12 @@ val validFloatValue_def = Define `
   validFloatValue (v:real) (m:mType) =
    case m of
     | M0 => T
-    | _ => normal v m \/ v = 0`
+    | _ => normal v m \/ denormal v m \/ v = 0`
+
+val validValue_def = Define `
+  validValue (v:real) (m:mType) =
+    case m of
+      | M0 => T
+      | _ => abs v <= maxValue m`;
 
 val _ = export_theory();

hol4/IntervalValidationScript.sml

@@ -468,36 +468,6 @@ val Rmap_updVars_comm = store_thm (
   \\ rpt strip_tac
   \\ Cases_on `x = n` \\ fs[]);
 
-(* val eval_exp_Rmap_updVars_comm = store_thm ( *)
-(*   "eval_exp_Rmap_updVars_comm", *)
-(*   ``!E e v n Gamma. *)
-(*       eval_exp E (toRMap (updDefVars n M0 Gamma)) (toREval e) v M0 ==> *)
-(*       eval_exp E (updDefVars n M0 (toRMap Gamma)) (toREval e) v M0``, *)
-(*   Induct_on `e` *)
-(*   \\ rpt strip_tac \\ simp[Once toREval_def] *)
-(*   >- (fs [toREval_def] \\ inversion `eval_exp _ _ _ _ _` eval_exp_cases *)
-(*       \\ irule Var_load \\ fs[] *)
-(*       \\ rw_sym_asm `_ = SOME M0` *)
-(*       \\ irule Rmap_updVars_comm) *)
-(*   >- (fs [toREval_def] \\ inversion `eval_exp _ _ _ _ _` eval_exp_cases *)
-(*       \\ irule Const_dist' \\ fs[] *)
-(*       \\ qexists_tac `delta` \\ fs[]) *)
-(*   >- (rw_thm_asm `eval_exp _ _ _ _ _` toREval_def *)
-(*       \\ fs[] \\ inversion `eval_exp _ _ _ _ _` eval_exp_cases *)
-(*       \\ fs[] \\ res_tac *)
-(*       >- (irule Unop_neg' *)
-(*           \\ qexistsl_tac [`M0`, `v1`] \\ fs[]) *)
-(*       >- (irule Unop_inv' *)
-(*           \\ qexistsl_tac [`delta`, `M0`, `v1`] \\ fs[])) *)
-(*   >- (rw_thm_asm `eval_exp _ _ _ _ _` toREval_def *)
-(*       \\ fs [] \\ inversion `eval_exp _ _ _ _ _` eval_exp_cases *)
-(*       \\ `m1 = M0 /\ m2 = M0` by (irule M0_join_is_M0 \\ fs[]) *)
-(*       \\ fs[] \\ res_tac *)
-(*       \\ irule Binop_dist' *)
-(*       \\ qexistsl_tac [`delta`, `M0`, `M0`, `v1`, `v2`] \\ fs[join_def, mTypeToQ_def]) *)
-(*   >- (rw_thm_asm `eval_exp _ _ _ _ _` toREval_def *)
-(*       \\ fs[])); *)
-
 val swap_Gamma_eval_exp = store_thm (
   "swap_Gamma_exp_exp",
   ``!e E vR m Gamma1 Gamma2.

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)
@@ -92,8 +92,9 @@ val typeCheckCmd_def = Define `
     case c of
       | Let m x e g =>  if (typeCheck e Gamma tMap)
                         then
-                            case tMap e of
-                              | SOME me => me = m /\ typeCheckCmd g (updDefVars x me Gamma) tMap
+                            case tMap e, tMap (Var x) of
+                              | SOME me, SOME mx =>
+                                  mx = m /\ me = m /\ typeCheckCmd g (updDefVars x me Gamma) tMap
                               | _ => F
                         else F
       | Ret e => typeCheck e Gamma tMap`