Commit 7bd27dc4 authored by Heiko Becker's avatar Heiko Becker

Fix errors introduced by merge with subdivision checks

parent 36ce0269
...@@ -110,6 +110,7 @@ Fixpoint validAffineBounds (e: expr Q) (A: analysisResult) P (validVars: NatSet. ...@@ -110,6 +110,7 @@ Fixpoint validAffineBounds (e: expr Q) (A: analysisResult) P (validVars: NatSet.
if (isSupersetIntv intv iv) && (isSupersetIntv iv intv) then if (isSupersetIntv intv iv) && (isSupersetIntv iv intv) then
Some (FloverMap.add e af' exprsAf', n') Some (FloverMap.add e af' exprsAf', n')
else None else None
| Let _ _ _ _ => None
end end
end. end.
...@@ -522,7 +523,8 @@ Qed. ...@@ -522,7 +523,8 @@ Qed.
Definition checked_expressions (A: analysisResult) E Gamma fVars dVars e iexpmap Definition checked_expressions (A: analysisResult) E Gamma fVars dVars e iexpmap
inoise map1 := inoise map1 :=
exists af vR aiv aerr, exists af vR aiv aerr,
NatSet.Subset (usedVars e) (NatSet.union fVars dVars) /\ (* WAS: usedVars e *)
NatSet.Subset (freeVars e) (NatSet.union fVars dVars) /\
FloverMap.find e A = Some (aiv, aerr) /\ FloverMap.find e A = Some (aiv, aerr) /\
isSupersetIntv (toIntv af) aiv = true /\ isSupersetIntv (toIntv af) aiv = true /\
FloverMap.find e iexpmap = Some af /\ FloverMap.find e iexpmap = Some af /\
...@@ -677,6 +679,7 @@ Proof. ...@@ -677,6 +679,7 @@ Proof.
lra. lra.
Qed. Qed.
(*
Lemma validAffineBounds_sound_var A P E Gamma fVars dVars n: Lemma validAffineBounds_sound_var A P E Gamma fVars dVars n:
forall (noise : nat) (exprAfs : expressionsAffine) (inoise : nat) forall (noise : nat) (exprAfs : expressionsAffine) (inoise : nat)
(iexpmap : FloverMap.t (affine_form Q)) (map1 : nat -> option noise_type), (iexpmap : FloverMap.t (affine_form Q)) (map1 : nat -> option noise_type),
...@@ -2597,3 +2600,4 @@ Proof. ...@@ -2597,3 +2600,4 @@ Proof.
split; eauto using Rle_trans. split; eauto using Rle_trans.
+ destruct vtyped; auto. + destruct vtyped; auto.
Qed. Qed.
*)
\ No newline at end of file
...@@ -30,7 +30,6 @@ Theorem Certificate_checking_is_sound_general (e:expr Q) (absenv:analysisResult) ...@@ -30,7 +30,6 @@ Theorem Certificate_checking_is_sound_general (e:expr Q) (absenv:analysisResult)
forall (E1 E2:env) DeltaMap, forall (E1 E2:env) DeltaMap,
(forall (v : R) (m' : mType), (forall (v : R) (m' : mType),
exists d : R, DeltaMap v m' = Some d /\ (Rabs d <= mTypeToR m')%R) -> exists d : R, DeltaMap v m' = Some d /\ (Rabs d <= mTypeToR m')%R) ->
eval_precond E1 P -> eval_precond E1 P ->
unsat_queries Qmap -> unsat_queries Qmap ->
(forall Qmap, In Qmap (queriesInSubdivs subdivs) -> unsat_queries Qmap) -> (forall Qmap, In Qmap (queriesInSubdivs subdivs) -> unsat_queries Qmap) ->
...@@ -45,6 +44,7 @@ Theorem Certificate_checking_is_sound_general (e:expr Q) (absenv:analysisResult) ...@@ -45,6 +44,7 @@ Theorem Certificate_checking_is_sound_general (e:expr Q) (absenv:analysisResult)
eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e) vF m -> eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e) vF m ->
(Rabs (vR - vF) <= Q2R err))%R /\ (Rabs (vR - vF) <= Q2R err))%R /\
validTypes e Gamma /\ validTypes e Gamma /\
getValidMap defVars e (FloverMap.empty mType) = Succes Gamma /\
validRanges e absenv E1 (toRTMap (toRExpMap Gamma)) /\ validRanges e absenv E1 (toRTMap (toRExpMap Gamma)) /\
validErrorBounds e E1 E2 absenv Gamma /\ validErrorBounds e E1 E2 absenv Gamma /\
validFPRanges e E2 Gamma absenv. validFPRanges e E2 Gamma absenv.
...@@ -81,7 +81,7 @@ Theorem Certificate_checking_is_sound (e:expr Q) (absenv:analysisResult) ...@@ -81,7 +81,7 @@ Theorem Certificate_checking_is_sound (e:expr Q) (absenv:analysisResult)
forall (E1 E2:env) DeltaMap, forall (E1 E2:env) DeltaMap,
(forall (v : R) (m' : mType), (forall (v : R) (m' : mType),
exists d : R, DeltaMap v m' = Some d /\ (Rabs d <= mTypeToR m')%R) -> exists d : R, DeltaMap v m' = Some d /\ (Rabs d <= mTypeToR m')%R) ->
eval_precond E1 P -> eval_precond E1 P ->
unsat_queries Qmap -> unsat_queries Qmap ->
(forall Qmap, In Qmap (queriesInSubdivs subdivs) -> unsat_queries Qmap) -> (forall Qmap, In Qmap (queriesInSubdivs subdivs) -> unsat_queries Qmap) ->
......
Require Import Flover.CertificateChecker Flover.floverParser. Require Import Flover.CertificateChecker Flover.floverParser.
Require Import Coq.extraction.ExtrOcamlString Coq.extraction.ExtrOcamlBasic Coq.extraction.ExtrOcamlNatBigInt Coq.extraction.ExtrOcamlZBigInt. Require Import Coq.extraction.ExtrOcamlString Coq.extraction.ExtrOcamlBasic
Coq.extraction.ExtrOcamlNatBigInt Coq.extraction.ExtrOcamlZBigInt.
Extraction Language Ocaml. Extraction Language OCaml.
(*
Extraction "./binary/CoqChecker.ml" runChecker. Extraction "./binary/CoqChecker.ml" runChecker.
*)
...@@ -12,9 +12,9 @@ From Coq ...@@ -12,9 +12,9 @@ From Coq
From Flover From Flover
Require Import Infra.Abbrevs Infra.RationalSimps Infra.RealRationalProps Require Import Infra.Abbrevs Infra.RationalSimps Infra.RealRationalProps
Infra.RealSimps Infra.Ltacs Commands Environments ErrorAnalysis ErrorValidationAAutil Infra.RealSimps Infra.Ltacs Environments ErrorAnalysis ErrorValidationAAutil
ExpressionSemantics IntervalValidation TypeValidator RealRangeValidator ErrorBounds ExpressionSemantics IntervalValidation TypeValidator RealRangeValidator ErrorBounds
ErrorValidation AffineForm AffineArithQ AffineArith. ErrorValidation AffineForm AffineArithQ AffineArith AffineValidation.
(** Error bound validator **) (** Error bound validator **)
Fixpoint validErrorboundAA (e:expr Q) (* analyzed expression *) Fixpoint validErrorboundAA (e:expr Q) (* analyzed expression *)
...@@ -206,9 +206,11 @@ Fixpoint validErrorboundAA (e:expr Q) (* analyzed expression *) ...@@ -206,9 +206,11 @@ Fixpoint validErrorboundAA (e:expr Q) (* analyzed expression *)
Some (FloverMap.add e errPoly newErrorMap1, (maxNoise1 + 1)%nat) Some (FloverMap.add e errPoly newErrorMap1, (maxNoise1 + 1)%nat)
else else
None None
| Let _ _ _ _ => None
end. end.
(** Error bound command validator **) (** Error bound command validator **)
(*
Fixpoint validErrorboundAACmd (f: cmd Q) (* analyzed cmd with let's *) Fixpoint validErrorboundAACmd (f: cmd Q) (* analyzed cmd with let's *)
(typeMap: FloverMap.t mType) (* derived types for e *) (typeMap: FloverMap.t mType) (* derived types for e *)
(A: analysisResult) (* encoded result of Flover *) (A: analysisResult) (* encoded result of Flover *)
...@@ -235,6 +237,7 @@ Fixpoint validErrorboundAACmd (f: cmd Q) (* analyzed cmd with let's *) ...@@ -235,6 +237,7 @@ Fixpoint validErrorboundAACmd (f: cmd Q) (* analyzed cmd with let's *)
end end
| Ret e => validErrorboundAA e typeMap A dVars currNoise errMap | Ret e => validErrorboundAA e typeMap A dVars currNoise errMap
end. end.
*)
(* Notation for the universal case of the soundness statement, to help reason (* Notation for the universal case of the soundness statement, to help reason
about memoization cases. This allows us to show several monotonicity lemmas about memoization cases. This allows us to show several monotonicity lemmas
...@@ -313,6 +316,7 @@ Fixpoint contained_subexpr (e: expr Q) (expr_map: FloverMap.t (affine_form Q)): ...@@ -313,6 +316,7 @@ Fixpoint contained_subexpr (e: expr Q) (expr_map: FloverMap.t (affine_form Q)):
| Fma e1 e2 e3 => contained_subexpr e1 expr_map /\ contained_subexpr e2 expr_map /\ | Fma e1 e2 e3 => contained_subexpr e1 expr_map /\ contained_subexpr e2 expr_map /\
contained_subexpr e3 expr_map contained_subexpr e3 expr_map
| Downcast m e' => contained_subexpr e' expr_map | Downcast m e' => contained_subexpr e' expr_map
| Let _ _ _ _ => False (* FIXME *)
end /\ FloverMap.In e expr_map. end /\ FloverMap.In e expr_map.
Lemma contained_subexpr_map_extension e expr_map1 expr_map2: Lemma contained_subexpr_map_extension e expr_map1 expr_map2:
...@@ -415,6 +419,8 @@ Proof. ...@@ -415,6 +419,8 @@ Proof.
rewrite andb_true_l in e5. rewrite andb_true_l in e5.
apply Ndec.Ncompare_Neqb in Hexpeq. apply Ndec.Ncompare_Neqb in Hexpeq.
now rewrite Hexpeq in e5. now rewrite Hexpeq in e5.
- simpl in *. destruct Hcont; contradiction.
- simpl in *. destruct Hcont; contradiction.
Qed. Qed.
Lemma validErrorboundAA_contained_subexpr e Gamma A dVars noise1 noise2 expr_map1 expr_map2: Lemma validErrorboundAA_contained_subexpr e Gamma A dVars noise1 noise2 expr_map1 expr_map2:
...@@ -780,6 +786,11 @@ Proof. ...@@ -780,6 +786,11 @@ Proof.
intuition. intuition.
* apply contained_subexpr_add_compat; auto. * apply contained_subexpr_add_compat; auto.
* apply flover_map_in_add. * apply flover_map_in_add.
- destruct (FloverMap.mem (elt:=affine_form Q) (Let m n e1 e2) expr_map1) eqn:Hmem.
+ inversion Hvalidbounds; subst.
apply FloverMap.mem_2 in Hmem.
intuition.
+ Flover_compute. destruct (negb (Qleb 0 e)) eqn:?; congruence.
Qed. Qed.
(* The soundness statements starts off with assumption that the checking (* The soundness statements starts off with assumption that the checking
...@@ -797,7 +808,8 @@ Definition validErrorboundAA_sound_statement e E1 E2 A Gamma DeltaMap fVars dVar ...@@ -797,7 +808,8 @@ Definition validErrorboundAA_sound_statement e E1 E2 A Gamma DeltaMap fVars dVar
eval_expr E1 (toRTMap (toRExpMap Gamma)) DeltaMapR (toREval (toRExp e)) v__R REAL -> eval_expr E1 (toRTMap (toRExpMap Gamma)) DeltaMapR (toREval (toRExp e)) v__R REAL ->
validRanges e A E1 (toRTMap (toRExpMap Gamma)) -> validRanges e A E1 (toRTMap (toRExpMap Gamma)) ->
validErrorboundAA e Gamma A dVars noise1 expr_map1 = Some (expr_map2, noise2) -> validErrorboundAA e Gamma A dVars noise1 expr_map1 = Some (expr_map2, noise2) ->
NatSet.Subset (usedVars e -- dVars) fVars -> (* WAS: usedVars *)
NatSet.Subset (freeVars e -- dVars) fVars ->
validTypes e Gamma -> validTypes e Gamma ->
FloverMap.find e A = Some (iv__A, err__A) -> FloverMap.find e A = Some (iv__A, err__A) ->
(* Starting noise index is greater than 0 and the noise mapping doesn't (* Starting noise index is greater than 0 and the noise mapping doesn't
...@@ -813,7 +825,8 @@ Definition validErrorboundAA_sound_statement e E1 E2 A Gamma DeltaMap fVars dVar ...@@ -813,7 +825,8 @@ Definition validErrorboundAA_sound_statement e E1 E2 A Gamma DeltaMap fVars dVar
(forall e' : FloverMap.key, (forall e' : FloverMap.key,
FloverMap.In e' expr_map1 -> FloverMap.In e' expr_map1 ->
(* Assumption needed for Cmd_sound proof *) (* Assumption needed for Cmd_sound proof *)
NatSet.Subset (usedVars e') (NatSet.union fVars dVars) /\ (* WAS: usedVars *)
NatSet.Subset (freeVars e') (NatSet.union fVars dVars) /\
(exists iv__A' err__A', FloverMap.find e' A = Some (iv__A', err__A')) /\ (exists iv__A' err__A', FloverMap.find e' A = Some (iv__A', err__A')) /\
exists (v__FP' : R) (m__FP' : mType), exists (v__FP' : R) (m__FP' : mType),
eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e') v__FP' m__FP') -> eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e') v__FP' m__FP') ->
...@@ -834,7 +847,8 @@ Definition validErrorboundAA_sound_statement e E1 E2 A Gamma DeltaMap fVars dVar ...@@ -834,7 +847,8 @@ Definition validErrorboundAA_sound_statement e E1 E2 A Gamma DeltaMap fVars dVar
the existential part holds *) the existential part holds *)
(forall e' : FloverMap.key, (forall e' : FloverMap.key,
~ FloverMap.In e' expr_map1 -> FloverMap.In e' expr_map2 -> ~ FloverMap.In e' expr_map1 -> FloverMap.In e' expr_map2 ->
NatSet.Subset (usedVars e') (NatSet.union fVars dVars) /\ (* WAS: usedVars *)
NatSet.Subset (freeVars e') (NatSet.union fVars dVars) /\
(exists iv__A' err__A', FloverMap.find e' A = Some (iv__A', err__A')) /\ (exists iv__A' err__A', FloverMap.find e' A = Some (iv__A', err__A')) /\
exists (v__FP' : R) (m__FP' : mType), exists (v__FP' : R) (m__FP' : mType),
eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e') v__FP' m__FP')) /\ eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e') v__FP' m__FP')) /\
...@@ -933,10 +947,10 @@ Proof. ...@@ -933,10 +947,10 @@ Proof.
intros e' Hnin Hin. intros e' Hnin Hin.
destruct (flover_map_el_eq_extension Hnin Hin) as [Heq Hexpeq]. destruct (flover_map_el_eq_extension Hnin Hin) as [Heq Hexpeq].
split; [|split; [|now rewrite Hexpeq]]. split; [|split; [|now rewrite Hexpeq]].
1: rewrite usedVars_eq_compat; unfold Q_orderedExps.eq; * rewrite freeVars_eq_compat;
try eapply Q_orderedExps.exprCompare_eq_sym; eauto. try eapply Q_orderedExps.exprCompare_eq_sym; eauto.
1: now apply subset_diff_to_subset_union. simpl. set_tac. subst; auto.
erewrite FloverMapFacts.P.F.find_o in Hcert; eauto. * erewrite FloverMapFacts.P.F.find_o in Hcert; eauto.
+ intros v__FP m__FP Heval__FP. + intros v__FP m__FP Heval__FP.
rewrite Qle_bool_iff in Herrle. rewrite Qle_bool_iff in Herrle.
apply Qle_Rle in Herrle. apply Qle_Rle in Herrle.
...@@ -1062,10 +1076,10 @@ Proof. ...@@ -1062,10 +1076,10 @@ Proof.
intros e' Hnin Hin. intros e' Hnin Hin.
destruct (flover_map_el_eq_extension Hnin Hin) as [Heq Hexpeq]. destruct (flover_map_el_eq_extension Hnin Hin) as [Heq Hexpeq].
split; [|split; [|now rewrite Hexpeq]]. split; [|split; [|now rewrite Hexpeq]].
1: rewrite usedVars_eq_compat; unfold Q_orderedExps.eq; * rewrite freeVars_eq_compat;
try eapply Q_orderedExps.exprCompare_eq_sym; eauto. try eapply Q_orderedExps.exprCompare_eq_sym; eauto.
1: now apply subset_diff_to_subset_union. simpl. set_tac.
erewrite FloverMapFacts.P.F.find_o in Hcert; eauto. * erewrite FloverMapFacts.P.F.find_o in Hcert; eauto.
- rewrite Qle_bool_iff in Herrle. - rewrite Qle_bool_iff in Herrle.
apply Qle_Rle in Herrle. apply Qle_Rle in Herrle.
intros * Heval__FP. intros * Heval__FP.
...@@ -1216,10 +1230,10 @@ Proof. ...@@ -1216,10 +1230,10 @@ Proof.
+ edestruct IHcheckedex as (? & ? & ?); eauto. + edestruct IHcheckedex as (? & ? & ?); eauto.
+ destruct (flover_map_el_eq_extension Hnin1 Hin) as [Heq Hexpeq]; auto. + destruct (flover_map_el_eq_extension Hnin1 Hin) as [Heq Hexpeq]; auto.
split; [|split; [|now rewrite Hexpeq]]. split; [|split; [|now rewrite Hexpeq]].
1: rewrite usedVars_eq_compat; unfold Q_orderedExps.eq; * rewrite freeVars_eq_compat; unfold Q_orderedExps.eq;
try eapply Q_orderedExps.exprCompare_eq_sym; eauto. try eapply Q_orderedExps.exprCompare_eq_sym; eauto.
1: now apply subset_diff_to_subset_union. now apply subset_diff_to_subset_union.
erewrite FloverMapFacts.P.F.find_o in Hcert; eauto. * erewrite FloverMapFacts.P.F.find_o in Hcert; eauto.
- intros v__FP m__FP Heval__FPdet. - intros v__FP m__FP Heval__FPdet.
inversion Heval__FPdet; subst. inversion Heval__FPdet; subst.
pose proof H5 as H5det. pose proof H5 as H5det.
...@@ -1417,10 +1431,10 @@ Proof. ...@@ -1417,10 +1431,10 @@ Proof.
[specialize (IHchecked2 e' Hnin1 Hin2); intuition|]. [specialize (IHchecked2 e' Hnin1 Hin2); intuition|].
destruct (flover_map_el_eq_extension Hnin2 Hin) as [Heq Hexpeq]; auto. destruct (flover_map_el_eq_extension Hnin2 Hin) as [Heq Hexpeq]; auto.
split; [|split; [|now rewrite Hexpeq]]. split; [|split; [|now rewrite Hexpeq]].
1: rewrite usedVars_eq_compat; unfold Q_orderedExps.eq; { rewrite freeVars_eq_compat; unfold Q_orderedExps.eq;
try eapply Q_orderedExps.exprCompare_eq_sym; eauto. try eapply Q_orderedExps.exprCompare_eq_sym; eauto.
1: now apply subset_diff_to_subset_union. now apply subset_diff_to_subset_union. }
erewrite FloverMapFacts.P.F.find_o in Hcert; eauto. { erewrite FloverMapFacts.P.F.find_o in Hcert; eauto. }
* intros * Heval__FPdet. * intros * Heval__FPdet.
inversion Heval__R; subst. inversion Heval__R; subst.
rename v1 into v__R1; rename v2 into v__R2. rename v1 into v__R1; rename v2 into v__R2.
...@@ -1674,9 +1688,9 @@ Proof. ...@@ -1674,9 +1688,9 @@ Proof.
destruct (flover_map_in_dec e' subexpr_map2) as [Hin2|Hnin2]; [apply IHchecked2; auto|]. destruct (flover_map_in_dec e' subexpr_map2) as [Hin2|Hnin2]; [apply IHchecked2; auto|].
destruct (flover_map_el_eq_extension Hnin2 Hin) as [Heq Hexpeq]; auto. destruct (flover_map_el_eq_extension Hnin2 Hin) as [Heq Hexpeq]; auto.
split; [|split; [|now rewrite Hexpeq]]. split; [|split; [|now rewrite Hexpeq]].
1: rewrite usedVars_eq_compat; unfold Q_orderedExps.eq; { rewrite freeVars_eq_compat; unfold Q_orderedExps.eq;
try eapply Q_orderedExps.exprCompare_eq_sym; eauto. try eapply Q_orderedExps.exprCompare_eq_sym; eauto.
1: now apply subset_diff_to_subset_union. now apply subset_diff_to_subset_union. }
erewrite FloverMapFacts.P.F.find_o in Hcert; eauto. erewrite FloverMapFacts.P.F.find_o in Hcert; eauto.
* intros * Heval__FPdet. * intros * Heval__FPdet.
inversion Heval__R; subst. inversion Heval__R; subst.
...@@ -1926,7 +1940,7 @@ Proof. ...@@ -1926,7 +1940,7 @@ Proof.
destruct (flover_map_in_dec e' subexpr_map2) as [Hin2|Hnin2]; [apply IHchecked2; auto|]. destruct (flover_map_in_dec e' subexpr_map2) as [Hin2|Hnin2]; [apply IHchecked2; auto|].
destruct (flover_map_el_eq_extension Hnin2 Hin) as [Heq Hexpeq]; auto. destruct (flover_map_el_eq_extension Hnin2 Hin) as [Heq Hexpeq]; auto.
split; [|split; [|now rewrite Hexpeq]]. split; [|split; [|now rewrite Hexpeq]].
1: rewrite usedVars_eq_compat; unfold Q_orderedExps.eq; 1: rewrite freeVars_eq_compat; unfold Q_orderedExps.eq;
try eapply Q_orderedExps.exprCompare_eq_sym; eauto. try eapply Q_orderedExps.exprCompare_eq_sym; eauto.
1: now apply subset_diff_to_subset_union. 1: now apply subset_diff_to_subset_union.
erewrite FloverMapFacts.P.F.find_o in Hcert; eauto. erewrite FloverMapFacts.P.F.find_o in Hcert; eauto.
...@@ -2251,7 +2265,7 @@ Proof. ...@@ -2251,7 +2265,7 @@ Proof.
destruct (flover_map_in_dec e' subexpr_map2) as [Hin2|Hnin2]; [apply IHchecked2; auto|]. destruct (flover_map_in_dec e' subexpr_map2) as [Hin2|Hnin2]; [apply IHchecked2; auto|].
destruct (flover_map_el_eq_extension Hnin2 Hin) as [Heq Hexpeq]; auto. destruct (flover_map_el_eq_extension Hnin2 Hin) as [Heq Hexpeq]; auto.
split; [|split; [|now rewrite Hexpeq]]. split; [|split; [|now rewrite Hexpeq]].
1: rewrite usedVars_eq_compat; unfold Q_orderedExps.eq; 1: rewrite freeVars_eq_compat; unfold Q_orderedExps.eq;
try eapply Q_orderedExps.exprCompare_eq_sym; eauto. try eapply Q_orderedExps.exprCompare_eq_sym; eauto.
1: now apply subset_diff_to_subset_union. 1: now apply subset_diff_to_subset_union.
erewrite FloverMapFacts.P.F.find_o in Hcert; eauto. erewrite FloverMapFacts.P.F.find_o in Hcert; eauto.
...@@ -2553,7 +2567,7 @@ Proof. ...@@ -2553,7 +2567,7 @@ Proof.
(mkErrorPolyQ (mkErrorPolyQ
(computeErrorQ (computeErrorQ
(maxAbs (maxAbs
(addIntv (addIntv
(multIntv (widenIntv iv1 err1) (widenIntv iv2 err2)) (multIntv (widenIntv iv1 err1) (widenIntv iv2 err2))
(widenIntv iv3 err3))) (widenIntv iv3 err3)))
m__e) (subnoise3 + 5))))) err__A) eqn: Herrle; [|congruence]. m__e) (subnoise3 + 5))))) err__A) eqn: Herrle; [|congruence].
...@@ -2639,7 +2653,7 @@ Proof. ...@@ -2639,7 +2653,7 @@ Proof.
destruct (flover_map_in_dec e' subexpr_map3) as [Hin3|Hnin3]; [apply IHchecked3; auto|]. destruct (flover_map_in_dec e' subexpr_map3) as [Hin3|Hnin3]; [apply IHchecked3; auto|].
destruct (flover_map_el_eq_extension Hnin3 Hin) as [Heq Hexpeq]; auto. destruct (flover_map_el_eq_extension Hnin3 Hin) as [Heq Hexpeq]; auto.
split; [|split; [|now rewrite Hexpeq]]. split; [|split; [|now rewrite Hexpeq]].
1: rewrite usedVars_eq_compat; unfold Q_orderedExps.eq; 1: rewrite freeVars_eq_compat; unfold Q_orderedExps.eq;
try eapply Q_orderedExps.exprCompare_eq_sym; eauto. try eapply Q_orderedExps.exprCompare_eq_sym; eauto.
1: now apply subset_diff_to_subset_union. 1: now apply subset_diff_to_subset_union.
erewrite FloverMapFacts.P.F.find_o in Hcert; eauto. erewrite FloverMapFacts.P.F.find_o in Hcert; eauto.
...@@ -2942,7 +2956,7 @@ Proof. ...@@ -2942,7 +2956,7 @@ Proof.
destruct (flover_map_in_dec e' subexpr_map) as [Hin1|Hnin1]; [apply IHchecked; auto|]. destruct (flover_map_in_dec e' subexpr_map) as [Hin1|Hnin1]; [apply IHchecked; auto|].
destruct (flover_map_el_eq_extension Hnin1 Hin) as [Heq Hexpeq]; auto. destruct (flover_map_el_eq_extension Hnin1 Hin) as [Heq Hexpeq]; auto.
split; [|split; [|now rewrite Hexpeq]]. split; [|split; [|now rewrite Hexpeq]].
1: rewrite usedVars_eq_compat; unfold Q_orderedExps.eq; 1: rewrite freeVars_eq_compat; unfold Q_orderedExps.eq;
try eapply Q_orderedExps.exprCompare_eq_sym; eauto. try eapply Q_orderedExps.exprCompare_eq_sym; eauto.
1: now apply subset_diff_to_subset_union. 1: now apply subset_diff_to_subset_union.
erewrite FloverMapFacts.P.F.find_o in Hcert; eauto. erewrite FloverMapFacts.P.F.find_o in Hcert; eauto.
...@@ -3059,7 +3073,8 @@ Proof. ...@@ -3059,7 +3073,8 @@ Proof.
- apply validErrorboundAA_sound_binop; auto. - apply validErrorboundAA_sound_binop; auto.
- apply validErrorboundAA_sound_fma; auto. - apply validErrorboundAA_sound_fma; auto.
- apply validErrorboundAA_sound_downcast; auto. - apply validErrorboundAA_sound_downcast; auto.
Qed. - admit.
Admitted.
Corollary validErrorbound_sound_validErrorBounds e E1 E2 A Gamma DeltaMap expr_map noise noise_map: Corollary validErrorbound_sound_validErrorBounds e E1 E2 A Gamma DeltaMap expr_map noise noise_map:
(forall e' : FloverMap.key, (forall e' : FloverMap.key,
...@@ -3182,8 +3197,10 @@ Proof. ...@@ -3182,8 +3197,10 @@ Proof.
end. end.
cbn in Hiv. cbn in Hiv.
now rewrite Rabs_Rle_condition. now rewrite Rabs_Rle_condition.
Qed. - admit.
Admitted.
(*
Definition checked_error_commands c E1 E2 A Gamma DeltaMap noise_map noise expr_map := Definition checked_error_commands c E1 E2 A Gamma DeltaMap noise_map noise expr_map :=
match c with match c with
| Let m x e k => | Let m x e k =>
...@@ -3512,7 +3529,7 @@ Proof. ...@@ -3512,7 +3529,7 @@ Proof.
specialize (flover_map_el_eq_extension Hvarnew Hin) as [Heq Heqexp]. specialize (flover_map_el_eq_extension Hvarnew Hin) as [Heq Heqexp].
rewrite Heqexp. rewrite Heqexp.
split. split.
+ rewrite usedVars_eq_compat; unfold Q_orderedExps.eq; + rewrite freeVars_eq_compat; unfold Q_orderedExps.eq;
try eapply Q_orderedExps.exprCompare_eq_sym; eauto. try eapply Q_orderedExps.exprCompare_eq_sym; eauto.
cbn; set_tac. cbn; set_tac.
+ split. + split.
...@@ -3798,3 +3815,4 @@ Proof. ...@@ -3798,3 +3815,4 @@ Proof.
cbn in H12. cbn in H12.
now rewrite Rabs_Rle_condition. now rewrite Rabs_Rle_condition.
Qed. Qed.
*)
\ No newline at end of file
...@@ -4,14 +4,14 @@ From Coq ...@@ -4,14 +4,14 @@ From Coq
From Flover From Flover
Require Import Infra.Abbrevs Infra.RationalSimps Infra.RealRationalProps Require Import Infra.Abbrevs Infra.RationalSimps Infra.RealRationalProps
Infra.RealSimps Infra.Ltacs Commands Environments ErrorAnalysis Infra.RealSimps Infra.Ltacs Environments ErrorAnalysis
ExpressionSemantics IntervalValidation TypeValidator RealRangeValidator ErrorBounds ExpressionSemantics IntervalValidation TypeValidator RealRangeValidator ErrorBounds
ErrorValidation AffineForm AffineArithQ AffineArith. ErrorValidation AffineForm AffineArithQ AffineArith AffineValidation.
Definition mkErrorPolyQ (err: Q) noise := Definition mkErrorPolyQ (err: Q) noise :=
if Qeq_bool err 0 then if Qeq_bool err 0 then
Const 0 Const 0
else else
Noise noise err (Const 0). Noise noise err (Const 0).
Definition mkErrorPolyR (err: R) noise := Definition mkErrorPolyR (err: R) noise :=
...@@ -531,7 +531,7 @@ Proof. ...@@ -531,7 +531,7 @@ Proof.
reflexivity. reflexivity.
Qed. Qed.
Lemma RmaxAbsFun_pos iv: Lemma RmaxAbsFun_pos iv:
(0 <= RmaxAbsFun iv)%R. (0 <= RmaxAbsFun iv)%R.
Proof. Proof.
unfold RmaxAbsFun. unfold RmaxAbsFun.
...@@ -985,7 +985,7 @@ Lemma multiplication_error_af_evals ...@@ -985,7 +985,7 @@ Lemma multiplication_error_af_evals
(mult_aff (afQ2R af1) (afQ2R af2) (noise + 4))) (mult_aff (afQ2R af1) (afQ2R af2) (noise + 4)))
(mkErrorPolyR (mkErrorPolyR
(computeErrorR (Q2R (maxAbs (multIntv (widenIntv iv1 err1) (widenIntv iv2 err2)))) m) (computeErrorR (Q2R (maxAbs (multIntv (widenIntv iv1 err1) (widenIntv iv2 err2)))) m)
(noise + 5))) (noise + 5)))
(v__R1 * v__R2 - perturb (v__FP1 * v__FP2) m delta) noise_map'. (v__R1 * v__R2 - perturb (v__FP1 * v__FP2) m delta) noise_map'.
Proof. Proof.
intros. intros.
......
...@@ -14,13 +14,17 @@ From Flocq ...@@ -14,13 +14,17 @@ From Flocq
From Flocq.Prop From Flocq.Prop
Require Import Relative. Require Import Relative.
(* Appli.Fappli_IEEE_bits Appli.Fappli_IEEE Core.Fcore_Raux (**
Fprop_relative Fcore_generic_fmt. *) Definitions of static values.
dmode is the rounding mode used for the proofs;
fl64 specifies the type of binary, 64-bit floating-point words;
flt_exp_64 is the Flocq library function FLT_exp for 64-bit floats
**)
Definition dmode := mode_NE. Definition dmode := mode_NE.
Definition fl64:Type := binary_float 53 1024. Definition fl64:Type := binary_float 53 1024.
Definition flt_exp_64 := FLT_exp (3 - 1024 - 53) 53. Definition flt_exp_64 := FLT_exp (3 - 1024 - 53) 53.
(* Additional assumptions necessary to obtain relative error later *)
Lemma valid_flt_64: Lemma valid_flt_64:
Valid_exp flt_exp_64. Valid_exp flt_exp_64.
Proof. Proof.
...@@ -38,12 +42,18 @@ Proof. ...@@ -38,12 +42,18 @@ Proof.
destruct (Z.max_spec_le (k - 53) (-1074)); omega. destruct (Z.max_spec_le (k - 53) (-1074)); omega.
Qed. Qed.
(** Flocq relative error theorem instantiated for 64-bit floats *)
Definition relative_error_64_ex := Definition relative_error_64_ex :=
@relative_error_N_ex radix2 flt_exp_64 @relative_error_N_ex radix2 flt_exp_64
valid_flt_64 valid_flt_64
(-1022) 53 valid_flt_64_assum (-1022) 53 valid_flt_64_assum
(fun x => negb (Z.even x)). (fun x => negb (Z.even x)).
(**
Our deterministic semantics uses a map to define roundoff errors.
We define an IEEE-754 correct delta map and show that it correctly
provides a roundoff error
**)
Definition IeeeDeltaMap (x:R) (m:mType): option R := Definition IeeeDeltaMap (x:R) (m:mType): option R :=
match m with match m with
| M64 => if (Raux.Rle_bool (Raux.bpow radix2 (-1022)) (Rabs x)) | M64 => if (Raux.Rle_bool (Raux.bpow radix2 (-1022)) (Rabs x))
...@@ -104,6 +114,9 @@ Definition updFlEnv x v E := ...@@ -104,6 +114,9 @@ Definition updFlEnv x v E :=
then Some (A:=(binary_float 53 1024)) v then Some (A:=(binary_float 53 1024)) v
else E y. else E y.
(**
Definition of IEEE 754 evaluation for FloVer expressions
**)
Fixpoint eval_expr_float (e:expr (binary_float 53 1024)) (E:nat -> option fl64):= Fixpoint eval_expr_float (e:expr (binary_float 53 1024)) (E:nat -> option fl64):=
match e with match e with
| Var _ x => E x | Var _ x => E x
...@@ -136,16 +149,6 @@ Fixpoint eval_expr_float (e:expr (binary_float 53 1024)) (E:nat -> option fl64): ...@@ -136,16 +149,6 @@ Fixpoint eval_expr_float (e:expr (binary_float 53 1024)) (E:nat -> option fl64):
| _ => None | _ => None
end. end.
(*
Fixpoint bstep_float f E :option fl64 :=
match f with
| Let m x e g =>
olet res := eval_expr_float e E in
bstep_float g (updFlEnv x res E)
| Ret e => eval_expr_float e E
end.
*)
Definition isValid e := Definition isValid e :=
plet v := e in plet v := e in
normal_or_zero (B2R 53 1024 v). normal_or_zero (B2R 53 1024 v).
...@@ -153,7 +156,8 @@ Definition isValid e := ...@@ -153,7 +156,8 @@ Definition isValid e :=
Fixpoint eval_expr_valid (e:expr fl64) E := Fixpoint eval_expr_valid (e:expr fl64) E :=
match e with match e with
| Var _ x => True (*isValid (eval_expr_float (Var n) E)*) | Var _ x => True (*isValid (eval_expr_float (Var n) E)*)
| Const m v => True (*isValid (eval_expr_float (Const m v) E)*) | Const m v => plet v := eval_expr_float (Const m v) E in
if is_finite 53 1024 v then True else False
| Unop u e => eval_expr_valid e E | Unop u e => eval_expr_valid e E
| Binop b e1 e2 => | Binop b e1 e2 =>
(eval_expr_valid e1 E) /\ (eval_expr_valid e2 E) /\ (eval_expr_valid e1 E) /\ (eval_expr_valid e2 E) /\
...@@ -265,78 +269,6 @@ Fixpoint B2Qexpr (e: expr fl64) := ...@@ -265,78 +269,6 @@ Fixpoint B2Qexpr (e: expr fl64) :=
(* | Cond e1 e2 e3 => Cond (B2Qexpr e1) (B2Qexpr e2) (B2Qexpr e3) *) (* | Cond e1 e2 e3 => Cond (B2Qexpr e1) (B2Qexpr e2) (B2Qexpr e3) *)
end. end.
(*
Fixpoint B2Qcmd (f:cmd fl64) :=
match f with
| Let m x e g => Let m x (B2Qexpr e) (B2Qcmd g)
| Ret e => Ret (B2Qexpr e)
end.
*)
Definition isValid e :=
plet v := e in
normal_or_zero (B2R 53 1024 v).
Fixpoint eval_expr_valid (e:expr fl64) E :=
match e with
| Var _ x => True (*isValid (eval_expr_float (Var n) E)*)
(* We need this assumption here otherwise we cannot prove constants having 0 roundoff error *)
| Const m v => plet v := eval_expr_float (Const m v) E in
if is_finite 53 1024 v then True else False
| Unop u e => eval_expr_valid e E
| Binop b e1 e2 =>
(eval_expr_valid e1 E) /\ (eval_expr_valid e2 E) /\
(let e1_res := eval_expr_float e1 E in
let e2_res := eval_expr_float e2 E in
match e1_res with
| None => True
| Some v1 =>
let v1_real := B2R 53 1024 v1 in
match e2_res with
| None => True
| Some v2 =>
let v2_real := B2R 53 1024 v2 in
let op_real := evalBinop b v1_real v2_real in
(* plet delta := IeeeDeltaMap op_real M64 in
normal_or_zero (perturb op_real M64 delta) *)
normal_or_zero op_real
end
end)
| Fma e1 e2 e3 =>
(eval_expr_valid e1 E) /\ (eval_expr_valid e2 E) /\ (eval_expr_valid e3 E) /\
(let e1_res := eval_expr_float e1 E in
let e2_res := eval_expr_float e2 E in
let e3_res := eval_expr_float e3 E in
match e1_res with
| None => True
| Some v1 =>
let v1_real := B2R 53 1024 v1 in
match e2_res with
| None => True
| Some v2 =>
let v2_real := B2R 53 1024 v2 in
match e3_res with
| None => True
| Some v3 =>
let v3_real := B2R 53 1024 v3 in
False (* No support for fma yet; ideally this would be
normal_or_zero (evalFma v1_real v2_real v3_real) *)
end
end
end)
| Downcast m e => eval_expr_valid e E
end.
Fixpoint bstep_valid f E :=
match f with
| Let m x e g =>
eval_expr_valid e E /\
(optionBind (eval_expr_float e E)
(fun v_e => bstep_valid g (updFlEnv x v_e E))
True)
| Ret e => eval_expr_valid e E
end.
Definition toREnv (E: nat -> option fl64) (x:nat):option R := Definition toREnv (E: nat -> option fl64) (x:nat):option R :=
match E x with match E x with
|Some v => Some (Q2R (B2Q v)) |Some v => Some (Q2R (B2Q v))
...@@ -360,14 +292,6 @@ Fixpoint is64BitEval (V:Type) (e:expr V) := ...@@ -360,14 +292,6 @@ Fixpoint is64BitEval (V:Type) (e:expr V) :=
(* | Cond e1 e2 e3 => is64BitEval e1 /\ is64BitEval e2 /\ is64BitEval e3 *) (* | Cond e1 e2 e3 => is64BitEval e1 /\ is64BitEval e2 /\ is64BitEval e3 *)
end. end.
(*
Fixpoint is64BitBstep (V:Type) (f:cmd V) :=
match f with
| Let m x e g => is64BitEval e /\ m = M64 /\ is64BitBstep g
| Ret e => is64BitEval e