Commit 3f4d2136 authored by Heiko Becker's avatar Heiko Becker

Merge latest changes from master

parents d945a600 faf90b7f
......@@ -25,6 +25,7 @@ Proof.
rewrite Q2R0_is_0; lra.
Qed.
Lemma add_abs_err_bounded (e1:exp Q) (e1R:R) (e1F:R) (e2:exp Q) (e2R:R) (e2F:R)
(vR:R) (vF:R) (E1 E2:env) (err1 err2 :Q) (m m1 m2:mType) defVars:
eval_exp E1 (toRMap defVars) (toREval (toRExp e1)) e1R M0 ->
......@@ -42,8 +43,9 @@ Proof.
intros e1_real e1_float e2_real e2_float plus_real plus_float bound_e1 bound_e2.
(* Prove that e1R and e2R are the correct values and that vR is e1R + e2R *)
inversion plus_real; subst.
destruct m0; destruct m3; inversion H2;
simpl in H3; rewrite Q2R0_is_0 in H3; auto.
assert (m0 = M0) by (eapply toRMap_eval_M0; eauto).
assert (m3 = M0) by (eapply toRMap_eval_M0; eauto).
subst; simpl in H3; rewrite Q2R0_is_0 in H3; auto.
rewrite delta_0_deterministic in plus_real; auto.
rewrite (delta_0_deterministic (evalBinop Plus v1 v2) delta); auto.
unfold evalBinop in *; simpl in *.
......@@ -109,8 +111,9 @@ Proof.
intros e1_real e1_float e2_real e2_float sub_real sub_float bound_e1 bound_e2.
(* Prove that e1R and e2R are the correct values and that vR is e1R + e2R *)
inversion sub_real; subst;
destruct m0; destruct m3; inversion H2;
simpl in H3; rewrite Q2R0_is_0 in H3; auto.
assert (m0 = M0) by (eapply toRMap_eval_M0; eauto).
assert (m3 = M0) by (eapply toRMap_eval_M0; eauto).
subst; simpl in H3; rewrite Q2R0_is_0 in H3; auto.
rewrite delta_0_deterministic in sub_real; auto.
rewrite delta_0_deterministic; auto.
unfold evalBinop in *; simpl in *.
......@@ -168,8 +171,9 @@ Proof.
intros e1_real e1_float e2_real e2_float mult_real mult_float.
(* Prove that e1R and e2R are the correct values and that vR is e1R * e2R *)
inversion mult_real; subst;
destruct m0; destruct m3; inversion H2;
simpl in H3; rewrite Q2R0_is_0 in H3; auto.
assert (m0 = M0) by (eapply toRMap_eval_M0; eauto).
assert (m3 = M0) by (eapply toRMap_eval_M0; eauto).
subst; simpl in H3; rewrite Q2R0_is_0 in H3; auto.
rewrite delta_0_deterministic in mult_real; auto.
rewrite delta_0_deterministic; auto.
unfold evalBinop in *; simpl in *.
......@@ -219,8 +223,9 @@ Proof.
intros e1_real e1_float e2_real e2_float div_real div_float.
(* Prove that e1R and e2R are the correct values and that vR is e1R * e2R *)
inversion div_real; subst;
destruct m0; destruct m3; inversion H2;
simpl in H3; rewrite Q2R0_is_0 in H3; auto.
assert (m0 = M0) by (eapply toRMap_eval_M0; eauto).
assert (m3 = M0) by (eapply toRMap_eval_M0; eauto).
subst; simpl in H3; rewrite Q2R0_is_0 in H3; auto.
rewrite delta_0_deterministic in div_real; auto.
rewrite delta_0_deterministic; auto.
unfold evalBinop in *; simpl in *.
......
......@@ -2075,8 +2075,7 @@ Proof.
end.
type_conv.
inversion eval_real; subst.
apply M0_join_is_M0 in H2.
destruct H2; subst.
assert (m2 = M0 /\ m3 = M0) as [? ?] by (split; eapply toRMap_eval_M0; eauto); subst.
destruct (IHe1 E1 E2 fVars dVars absenv v1 err1 P ivlo1 ivhi1 Gamma defVars)
as [[vF1 [mF1 eval_float_e1]] bounded_e1];
try auto; set_tac.
......@@ -2122,7 +2121,7 @@ Proof.
+ intros * eval_float.
clear eval_float_e1 eval_float_e2.
inversion eval_float; subst.
eapply (binary_unfolding _ H2 H4 H8) in eval_float; try auto.
eapply (binary_unfolding _ H4 H5 H9) in eval_float; try auto.
destruct b.
* eapply (validErrorboundCorrectAddition (e1:=e1) absenv); eauto.
{ simpl.
......
......@@ -336,6 +336,27 @@ Fixpoint usedVars (V:Type) (e:exp V) :NatSet.t :=
| _ => NatSet.empty
end.
Lemma toRMap_eval_M0 f v E Gamma m:
eval_exp E (toRMap Gamma) (toREval f) v m -> m = M0.
Proof.
revert v E Gamma m.
induction f; intros * eval_f; inversion eval_f; subst;
repeat
match goal with
| H: context[toRMap _ _] |- _ => unfold toRMap in H
| H: context[match ?Gamma ?v with | _ => _ end ] |- _ => destruct (Gamma v) eqn:?
| H: Some ?m1 = Some ?m2 |- _ => inversion H; try auto
| H: None = Some ?m |- _ => inversion H
end; try auto.
- eapply IHf; eauto.
- eapply IHf; eauto.
- assert (m1 = M0)
by (eapply IHf1; eauto).
assert (m2 = M0)
by (eapply IHf2; eauto);
subst; auto.
Qed.
(**
If |delta| <= 0 then perturb v delta is exactly v.
**)
......@@ -352,8 +373,8 @@ Evaluation with 0 as machine epsilon is deterministic
**)
Lemma meps_0_deterministic (f:exp R) (E:env) Gamma:
forall v1 v2,
eval_exp E Gamma (toREval f) v1 M0 ->
eval_exp E Gamma (toREval f) v2 M0 ->
eval_exp E (toRMap Gamma) (toREval f) v1 M0 ->
eval_exp E (toRMap Gamma) (toREval f) v2 M0 ->
v1 = v2.
Proof.
induction f;
......@@ -372,8 +393,11 @@ Proof.
rewrite Q2R0_is_0 in *;
repeat (rewrite delta_0_deterministic; try auto).
- inversion ev1; inversion ev2; subst.
apply M0_join_is_M0 in H11; apply M0_join_is_M0 in H2.
destruct H2, H11; subst.
assert (m0 = M0) by (eapply toRMap_eval_M0; eauto).
assert (m3 = M0) by (eapply toRMap_eval_M0; eauto).
assert (m1 = M0) by (eapply toRMap_eval_M0; eauto).
assert (m2 = M0) by (eapply toRMap_eval_M0; eauto).
subst.
rewrite (IHf1 v0 v4); try auto.
rewrite (IHf2 v3 v5); try auto.
simpl in *.
......
......@@ -133,12 +133,12 @@ Qed.
has to happen in 64 bits
**)
Definition join (m1:mType) (m2:mType) :=
if (isMorePrecise m1 m2) then m2 else m1.
Lemma M0_join_is_M0 m1 m2:
join m1 m2 = M0 -> m1 = M0 /\ m2 = M0.
Proof.
unfold join.
intros.
destruct m1, m2; simpl in *; cbv in *; try congruence; try auto.
Qed.
\ No newline at end of file
if (isMorePrecise m1 m2) then m1 else m2.
(* Lemma M0_join_is_M0 m1 m2: *)
(* join m1 m2 = M0 -> m1 = M0 /\ m2 = M0. *)
(* Proof. *)
(* unfold join. *)
(* intros. *)
(* destruct m1, m2; simpl in *; cbv in *; try congruence; try auto. *)
(* Qed. *)
\ No newline at end of file
......@@ -4,7 +4,7 @@ function display_help {
echo " generate Makefile.coq for this directory"
echo ""
echo -e " --help\t Show this text"
echo -e " --timing\t Use timing scripts"
echo -e " --timing\t Use timing scripts"
}
TIMING=
......@@ -12,7 +12,7 @@ while [ $# != 0 ]; do
case "$1" in
--help) display_help;;
--timing) TIMING=yes;;
*)
*)
esac
shift
done
......@@ -39,12 +39,12 @@ echo "Found Coq version $coq_ver."
echo "-R . Daisy" > _CoqProject
find . -path ./attic -prune -o -name "*.v" -print >> _CoqProject
find . -path ./attic -prune -o -path ./output -prune -o -name "*.v" -print >> _CoqProject
coq_makefile -f _CoqProject -o Makefile
sed -i -- 's/TIMECMD=/TIMECMD?=/g' Makefile
echo 'ifeq ($(wildcard time.rb)$(wildcard .timing),time.rb.timing)
export TIMECMD=@./time.rb $(if $(findstring j,$(MAKEFLAGS)),--parallel,)
export TIMECMD=@./time.rb $(if $(findstring j,$(MAKEFLAGS)),--parallel,)
endif' >>Makefile
Require Import Coq.Strings.Ascii Coq.Strings.String Coq.Lists.List Coq.Reals.Reals.
Require Import CertificateChecker.
Require Import CertificateChecker Infra.MachineType.
Import Coq.Lists.List.ListNotations.
......@@ -10,6 +10,8 @@ Inductive Token:Type :=
| DPRE
| DABS
| DCOND
| DGAMMA
| DTYPE:mType -> Token
| DVAR
| DCONST: N -> Token
| DNEG
......@@ -92,6 +94,14 @@ match fuel with
| "PRE" => DPRE :: lex input'' fuel'
| "ABS" => DABS :: lex input'' fuel'
| "Var" => DVAR :: lex input'' fuel'
| "MTYPE" => let ts := lex input'' fuel' in
(match ts with
|DCONST 32 :: ts' => DTYPE M32 :: ts'
|DCONST 64 :: ts' => DTYPE M64 :: ts'
(* | DCONST 128 :: ts' => DTYPE M128 :: ts' *)
(* | DCONST 256 :: ts' => DTYPE M256 :: ts' *)
| _ => []
end)
| _ => []
end
else
......@@ -120,6 +130,13 @@ Fixpoint str_of_num (n:nat) (m:nat):=
|_ => ""
end .
Fixpoint type_to_string (m:mType) :=
match m with
|M32 => "MTYPE 32"
|M64 => "MTYPE 64"
| _ => "" (* FIXME *)
end.
(*
Definition pp_token (token:Token) :=
match token with
......@@ -156,15 +173,15 @@ Fixpoint parseExp (tokList:list Token) (fuel:nat):option (exp Q * list Token) :=
match fuel with
|S fuel' =>
match tokList with
| DCONST n :: DFRAC :: DCONST m :: tokRest =>
| DTYPE t :: DCONST n :: DFRAC :: DCONST m :: tokRest =>
match m with
|N0 => None
|Npos p => Some (Const (Z.of_N n # p), tokRest)
|Npos p => Some (Const t (Z.of_N n # p), tokRest)
end
| DVAR :: DCONST n :: tokRest => Some (Var Q (N.to_nat n), tokRest)
| DNEG :: tokRest =>
match (parseExp tokRest fuel') with
| Some (Const c, tokRest) => Some (Const (- c), tokRest)
| Some (Const m c, tokRest) => Some (Const m (- c), tokRest)
| Some (e1,tokRest') => Some (Unop Neg e1, tokRest')
| None => None
end
......@@ -220,7 +237,7 @@ Fixpoint parseLet input fuel:option (cmd Q * list Token) :=
|S fuel' =>
match input with
(* We already have a valid let binding *)
| DVAR :: DCONST n :: expLetRest =>
| DVAR :: DTYPE m :: DCONST n :: expLetRest =>
(* so we parse an expression *)
match parseExp expLetRest fuel with
| Some (e, letRest) =>
......@@ -230,7 +247,7 @@ Fixpoint parseLet input fuel:option (cmd Q * list Token) :=
(* Parse it *)
match (parseLet letBodyRest fuel') with
(* And construct a result from it *)
| Some (letCmd, arbRest) => Some (Let (N.to_nat n) e letCmd, arbRest)
| Some (letCmd, arbRest) => Some (Let m (N.to_nat n) e letCmd, arbRest)
| _ => None
end
(* But if we have a return *)
......@@ -238,7 +255,7 @@ Fixpoint parseLet input fuel:option (cmd Q * list Token) :=
(* parse only this *)
match (parseRet retBodyRest fuel) with
(* and construct the result *)
| Some (retCmd, arbRest) => Some (Let (N.to_nat n) e retCmd, arbRest)
| Some (retCmd, arbRest) => Some (Let m (N.to_nat n) e retCmd, arbRest)
| _ => None
end
| _ => None (* fail if there is no continuation for the let *)
......@@ -312,7 +329,7 @@ Definition parsePrecond (input :list Token) fuel :=
Definition defaultAbsenv:analysisResult := fun e => (mkIntv 0 0 ,0).
Definition updAbsenv (e:exp Q) (iv:intv) (err:Q) (A:analysisResult):=
fun e' => if expEqBool e e' then (iv, err) else A e'.
fun e' => if expEq e e' then (iv, err) else A e'.
(** Abstract environment parser:
The abstract environment should be encoded in the following format:
......@@ -351,6 +368,24 @@ Definition parseAbsEnv (input:list Token) fuel :=
| _ => None
end.
Definition defaultGamma := fun n:nat => None:option mType.
Fixpoint parseGammaRec (input: list Token) : option ((nat -> option mType) * list Token) :=
match input with
| DVAR :: DCONST n :: DTYPE m :: inputRest =>
match parseGammaRec inputRest with
| Some (Gamma, rest) => Some (updDefVars (N.to_nat n) m Gamma, rest)
| None => None
end
| _ => Some (defaultGamma, input)
end.
Definition parseGamma (input:list Token) :=
match input with
| DGAMMA :: tokenRest => parseGammaRec tokenRest
| _ => None
end.
Definition dParse (input:list Token) fuel :=
let cmdParse :=
match input with
......@@ -365,20 +400,80 @@ Definition dParse (input:list Token) fuel :=
| DPRE :: preRest =>
match parsePrecond tokRest fuel with
| Some (P, absenvRest) =>
match parseAbsEnv absenvRest fuel with
| Some (A, residual) => Some ((dCmd, P, A), residual)
match absenvRest with
| DABS :: absRest =>
match parseAbsEnv absRest fuel with
| Some (A, residual) =>
match parseGamma residual with
| Some (Gamma, residual) => Some ((dCmd,P,A,Gamma),residual)
| _ => None
end
| _ => None
end
| DGAMMA :: absRest =>
match parseGamma absRest with
| Some (Gamma, residual) =>
match parseAbsEnv residual fuel with
| Some (A,residual) => Some ((dCmd, P, A, Gamma), residual)
| _ => None
end
| _ => None
end
| _ => None
end
| None => None
| _ => None
end
| DABS :: absRest =>
match parseAbsEnv tokRest fuel with
| Some (A, precondRest) =>
match parsePrecond precondRest fuel with
| Some (P, residual) => Some ((dCmd, P, A),residual)
| Some (A, absenvRest) =>
match absenvRest with
| DPRE :: absRest =>
match parsePrecond absRest fuel with
| Some (P, residual) =>
match parseGamma residual with
| Some (Gamma, residual) => Some ((dCmd,P,A,Gamma),residual)
| _ => None
end
| _ => None
end
| DGAMMA :: absRest =>
match parseGamma absRest with
| Some (Gamma, residual) =>
match parsePrecond residual fuel with
| Some (P,residual) => Some ((dCmd, P, A, Gamma), residual)
| _ => None
end
| _ => None
end
| _ => None
end
| _ => None
end
| DGAMMA :: absRest =>
match parseGamma tokRest with
| Some (Gamma, absenvRest) =>
match absenvRest with
| DPRE :: absRest =>
match parsePrecond absRest fuel with
| Some (P, residual) =>
match parseAbsEnv residual fuel with
| Some (A, residual) => Some ((dCmd,P,A,Gamma),residual)
| _ => None
end
| _ => None
end
| DABS :: absRest =>
match parseAbsEnv absRest fuel with
| Some (A, residual) =>
match parsePrecond residual fuel with
| Some (P,residual) => Some ((dCmd, P, A, Gamma), residual)
| _ => None
end
| _ => None
end
| _ => None
end
| None => None
| _ => None
end
| _ => None
end
......@@ -389,12 +484,12 @@ Fixpoint check_rec (input:list Token) (num_fun:nat) fuel:=
match num_fun with
| S n' =>
match dParse input fuel with
| Some ((dCmd, P, A), []) =>
if CertificateCheckerCmd dCmd A P
| Some ((dCmd, P, A, Gamma), []) =>
if CertificateCheckerCmd dCmd A P Gamma
then "True\n"
else "False\n"
| Some ((dCmd, P, A), residual) =>
if CertificateCheckerCmd dCmd A P
| Some ((dCmd, P, A, Gamma), residual) =>
if CertificateCheckerCmd dCmd A P Gamma
then check_rec residual n' fuel
else "False\n"
| None => "parse failure\n"
......@@ -408,9 +503,9 @@ Fixpoint str_length s :=
|"" => O
end.
Fixpoint check (f:cmd Q) (P:precond) (A:analysisResult) (n:nat) :=
Fixpoint check (f:cmd Q) (P:precond) (A:analysisResult) Gamma (n:nat) :=
match n with
|S n' => CertificateCheckerCmd f A P && (check f P A n')
|S n' => CertificateCheckerCmd f A P Gamma && (check f P A Gamma n')
|_ => true
end.
......@@ -418,8 +513,8 @@ Fixpoint check_all (num_fun:nat) (iters:nat) (input:list Token) fuel:=
match num_fun with
|S nf =>
match (dParse input fuel) with
|Some ((f,P,A), residual) =>
if (check f P A iters)
|Some ((f,P,A, Gamma), residual) =>
if (check f P A Gamma iters)
then
match residual with
|a :: b => check_all nf iters residual fuel
......
......@@ -12,6 +12,7 @@ open AbbrevsTheory ExpressionsTheory DaisyTactics ExpressionAbbrevsTheory
ErrorValidationTheory ssaPrgsTheory FPRangeValidatorTheory
val _ = new_theory "CertificateChecker";
val _ = temp_overload_on("abs",``real$abs``);
(** Certificate checking function **)
val CertificateChecker_def = Define
......
......@@ -4,6 +4,8 @@ open AbbrevsTheory ExpressionAbbrevsTheory RealSimpsTheory CommandsTheory DaisyT
val _ = new_theory "Environments";
val _ = temp_overload_on("abs",``real$abs``);
val (approxEnv_rules, approxEnv_ind, approxEnv_cases) = Hol_reln `
(!(defVars: num -> mType option) (A:analysisResult).
approxEnv emptyEnv defVars A LN LN emptyEnv) /\
......
......@@ -11,6 +11,7 @@ open ExpressionAbbrevsTheory EnvironmentsTheory
val _ = new_theory "ErrorBounds";
val _ = Parse.hide "delta"; (* so that it can be used as a variable *)
val _ = temp_overload_on("abs",``real$abs``);
val const_abs_err_bounded = store_thm ("const_abs_err_bounded",
``!(n:real) (nR:real) (nF:real) (E1 E2:env) (m:mType) (defVars: num -> mType option).
......
......@@ -15,6 +15,7 @@ open IntervalValidationTheory EnvironmentsTheory CommandsTheory ssaPrgsTheory
val _ = new_theory "ErrorValidation";
val _ = Parse.hide "delta"; (* so that it can be used as a variable *)
val _ = temp_overload_on("abs",``real$abs``);
val validErrorbound_def = Define `
validErrorbound e (typeMap: real exp -> mType option) (absenv:analysisResult) (dVars:num_set)=
......
......@@ -10,6 +10,7 @@ val _ = ParseExtras.temp_tight_equality()
val _ = new_theory "Expressions";
val _ = temp_overload_on("abs",``real$abs``);
(**
EXPRESSIONS WILL use binary operators.
Define them first
......
......@@ -9,6 +9,8 @@ open realTheory realLib sptreeTheory
val _ = new_theory "MachineType";
val _ = temp_overload_on("abs",``real$abs``);
val _ = Datatype `
mType = M0 | M16 | M32 | M64(* | M128 | M256 *)`;
......
......@@ -8,6 +8,9 @@ open AbbrevsTheory ExpressionsTheory RealSimpsTheory;
val _ = new_theory "IntervalArith";
val _ = temp_overload_on("abs",``real$abs``);
val _ = temp_overload_on("max",``real$max``);
val _ = temp_overload_on("min",``real$min``);
(**
Define validity of an interval, requiring that the lower bound is less than or equal to the upper bound.
Containement is defined such that if x is contained in the interval, it must lie between the lower and upper bound.
......
......@@ -14,6 +14,9 @@ open sptreeLib sptreeTheory
val _ = new_theory "IntervalValidation";
val _ = Parse.hide "delta"; (* so that it can be used as a variable *)
val _ = temp_overload_on("abs",``real$abs``);
val _ = temp_overload_on("max",``real$max``);
val _ = temp_overload_on("min",``real$min``);
val validIntervalbounds_def = Define `
validIntervalbounds f (absenv:analysisResult) (P:precond) (validVars:num_set) =
......
......@@ -5,6 +5,9 @@ val _ = ParseExtras.temp_tight_equality()
val _ = new_theory "RealSimps";
val _ = temp_overload_on("abs",``real$abs``);
val _ = temp_overload_on("max",``real$max``);
val abs_leq_zero = store_thm (
"abs_leq_zero[simp]",
``!v. abs v <= 0 <=> v = 0``,
......
open preamble
open machine_ieeeTheory binary_ieeeTheory lift_ieeeTheory realTheory
open MachineTypeTheory ExpressionsTheory RealSimpsTheory DaisyTactics CertificateCheckerTheory
open FPRangeValidatorTheory IntervalValidationTheory TypingTheory ErrorValidationTheory IntervalArithTheory AbbrevsTheory
val f64_plus_preserves_finite = store_thm ("f64_plus_preserves_finite",
``!f1 f2.
fp64_isFinite (fp64_add dmode f1 f2) ==>
fp64_isFinite f1 /\ fp64_isFinite f2 ``,
rw [fp64_isFinite_def, fp64_add_def, fp64_to_float_float_to_fp64,
float_add_def, float_is_finite_def]
\\ Cases_on `float_value (fp64_to_float f1)`
\\ Cases_on `float_value (fp64_to_float f2)`
\\ fs [float_values]);
val f64_sub_preserves_finite = store_thm ("f64_plus_preserves_finite",
``!f1 f2.
fp64_isFinite (fp64_sub dmode f1 f2) ==>
fp64_isFinite f1 /\ fp64_isFinite f2 ``,
rw [fp64_isFinite_def, fp64_sub_def, fp64_to_float_float_to_fp64,
float_sub_def, float_is_finite_def]
\\ Cases_on `float_value (fp64_to_float f1)` \\ Cases_on `float_value (fp64_to_float f2)`
\\ fs [float_values]
\\ Cases_on `float_value (float_negate (fp64_to_float f2))`
\\ fs [float_values]
\\ `(fp64_to_float f2).Exponent = UINT_MAXw`
by (fs [float_value_def]
\\ Cases_on `(fp64_to_float f2).Exponent = -(1w)`
\\ Cases_on `(fp64_to_float f2).Significand = 0w`
\\ fs [])
\\ `(fp64_to_float f2).Significand = 0w`
by (fs [float_value_def]
\\ Cases_on `(fp64_to_float f2).Exponent = -(1w)`
\\ Cases_on `(fp64_to_float f2).Significand = 0w`
\\ fs [])
\\ fs [float_negate_def, float_value_def]);
val f64_mul_preserves_finite = store_thm ("f64_plus_preserves_finite",
``!f1 f2.
fp64_isFinite (fp64_mul dmode f1 f2) ==>
fp64_isFinite f1 /\ fp64_isFinite f2 ``,
rw [fp64_isFinite_def, fp64_mul_def, fp64_to_float_float_to_fp64,
float_mul_def, float_is_finite_def]
\\ Cases_on `float_value (fp64_to_float f1)` \\ Cases_on `float_value (fp64_to_float f2)`
\\ fs [float_values]
\\ Cases_on `r = 0`
\\ fs [float_values]);
val f64_div_preserves_finite = store_thm ("f64_plus_preserves_finite",
``!f1 f2.
fp64_isFinite (fp64_div dmode f1 f2) /\
(float_value (fp64_to_float f2) = Infinity ==> F)==>
fp64_isFinite f1 /\ fp64_isFinite f2 ``,
rw [fp64_isFinite_def, fp64_div_def, fp64_to_float_float_to_fp64,
float_div_def, float_is_finite_def]
\\ Cases_on `float_value (fp64_to_float f1)` \\ Cases_on `float_value (fp64_to_float f2)`
\\ fs [float_values]
\\ Cases_on `r = 0`
\\ fs [float_values]);
val real_to_float_float_id = Q.prove (
`!f.
fp64_isFinite f /\
fp64_isNormal f /\
~ fp64_isZero f ==>
float_to_fp64 (real_to_float dmode (float_to_real (fp64_to_float f))) = f`,
rpt strip_tac
\\ fs[fp64_isFinite_def, fp64_isZero_def, fp64_isNormal_def]
\\ fs[real_to_float_id]
\\ fs[float_to_fp64_fp64_to_float]);
``!ff:half.
validFloatValue (float_to_real ff) M16 ==>
float_to_real ((float_round roundTiesToEven F (float_to_real ff)):single) = float_to_real ((float_round roundTiesToEven F (float_to_real ff)):half)``
rw[]
\\ fs[validFloatValue_def]
>- (`float_is_finite ff` by (irule normal16_to_real_implies_finiteness \\ fs[])
\\ Q.ISPEC_THEN `ff` impl_subgoal_tac round_float_to_real_id \\ fs[]
>- (cheat)
\\ `float_value ff = Float (float_to_real ff)` by (irule normal16_is_float_value \\ fs[])
\\ Cases_on `float_to_real ff = 0`
\\ fs[]
>- (`2 * abs 0 <= ulp (:10#5)`
by (fs[ulp_def, ULP_def])
\\ `2 * abs 0 <= ulp (:23#8)`
by (fs[ulp_def, ULP_def])
\\ fs[round_roundTiesToEven_is_plus_zero, zero_to_real])
\\ rw[float_round_def, zero_to_real, float_is_zero_to_real]
>- (fs[round_def]
\\ every_case_tac \\ fs[]
\\ rveq
\\ TRY (
fs[float_minus_infinity_def, float_plus_infinity_def, float_to_real_def, threshold_def, float_negate_def, float_value_def]
\\ FAIL_TAC "")
\\ qpat_x_assum `closest_such _ _ _ = _` MP_TAC
(* \\ qpat_x_assum `float_to_real (closest_such _ _ _) = _` MP_TAC *)
\\ fs[closest_such_def]
\\ SELECT_ELIM_TAC
\\ rw[]
>- (qexists_tac `ff`
\\ rw[is_closest_def, IN_DEF, realTheory.ABS_POS]
\\ first_x_assum (qspec_then `ff` mp_tac)
\\ fs[realTheory.REAL_SUB_REFL]
\\ strip_tac
\\ fs[float_to_real_eq]
\\ rveq
\\ rfs[]
\\ fs[float_is_zero_to_real])
\\ CCONTR_TAC \\ fs[] \\ rveq
\\ fs[is_closest_def, IN_DEF]
(* (* \\ qpat_x_assum `!x._ ` (qspec_then `ff` assume_tac) mp_tac *) *)
\\ fs[]
\\ qpat_x_assum `float_to_real _ = _` mp_tac
\\ SELECT_ELIM_TAC
\\ rw[]
cheat
>- (Cases_on `ff`
\\ qexists_tac `float c (0w @@ c0) (0w @@ c1)`
\\ rw[is_closest_def, IN_DEF, realTheory.ABS_POS, word_concat_0]
>- (fs[float_is_finite_def, float_value_def]
\\ every_case_tac \\ fs[float_Significand, float_Exponent, float_Sign, float_to_real_def]
(* \\ CCONTR_TAC \\ fs[] \\ rveq *)
(* \\ qpat_x_assum `!b. float_is_finite b ==> _` (qspec_then `x` impl_subgoal_tac) *)
(* \\ fs[] *)
(* \\ fs[] *)
(* ) *)
Subproject commit a3168cbd02b216a95d2d567f39674fedaed0b1b2
Subproject commit 9f7a2e8b53e4f091ae49340aed425376ed30ae26
......@@ -82,8 +82,8 @@ val lex_def = tDefine "lex" `
(case ts of
| DCONST 32 :: ts' => DTYPE M32 :: ts'
| DCONST 64 :: ts' => DTYPE M64 :: ts'
| DCONST 128 :: ts' => DTYPE M128 :: ts'
| DCONST 256 :: ts' => DTYPE M256 :: ts'
(* | DCONST 128 :: ts' => DTYPE M128 :: ts' *)
(* | DCONST 256 :: ts' => DTYPE M256 :: ts' *)
| _ => NIL)
| "Gamma" => DGAMMA :: lex input''
| _ => NIL
......@@ -111,10 +111,11 @@ val str_of_num_def = Define `
else STRING (CHR ( (n MOD 10) + 48)) (str_of_num (n DIV 10))`
val type_to_string = Define `
(type_to_string (M16) = "MTYPE 16") /\
(type_to_string (M32) = "MTYPE 32") /\
(type_to_string (M64) = "MTYPE 64") /\
(type_to_string (M128) = "MTYPE 128") /\
(type_to_string (M256) = "MTYPE 256")`;
(type_to_string (M64) = "MTYPE 64")`; (* FIXME *)
(* (type_to_string (M128) = "MTYPE 128") /\ *)
(* (type_to_string (M256) = "MTYPE 256")`; *)
val pp_token_def = Define `
pp_token (token:Token) =
......@@ -144,9 +145,9 @@ val str_join_def = Define `
(str_join (STRING c s1) s2 = STRING c (str_join s1 s2)) /\
(str_join "" s2 = s2)`;
val str_join_empty = store_thm ("str_join_empty",
``!s. str_join s "" = s``,
Induct \\ fs[str_join_def]);
(* val str_join_empty = store_thm ("str_join_empty", *)
(* ``!s. str_join s "" = s``, *)
(* Induct \\ fs[str_join_def]); *)
(* Pretty Printer for Tokens *)
val pp_def = Define `
......