Commit bac7151e authored by Joachim Bard's avatar Joachim Bard

Merge remote-tracking branch 'upstream/master'

merge with Nikita's changes
parents 923d82d0 cad900bc
...@@ -30,8 +30,8 @@ Definition CertificateChecker (e:expr Q) (absenv:analysisResult) ...@@ -30,8 +30,8 @@ Definition CertificateChecker (e:expr Q) (absenv:analysisResult)
**) **)
Theorem Certificate_checking_is_sound (e:expr Q) (absenv:analysisResult) P Qmap defVars: Theorem Certificate_checking_is_sound (e:expr Q) (absenv:analysisResult) P Qmap defVars:
forall (E1 E2:env) DeltaMap, forall (E1 E2:env) DeltaMap,
(forall (e' : expr R) (m' : mType), (forall (v : R) (m' : mType),
exists d : R, DeltaMap e' 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 ->
CertificateChecker e absenv P Qmap defVars = true -> CertificateChecker e absenv P Qmap defVars = true ->
...@@ -79,11 +79,11 @@ Proof. ...@@ -79,11 +79,11 @@ Proof.
destruct iv_e as [elo ehi]. destruct iv_e as [elo ehi].
exists Gamma; intros approxE1E2. exists Gamma; intros approxE1E2.
assert (dVars_contained NatSet.empty (FloverMap.empty (affine_form Q))) as Hdvars assert (dVars_contained NatSet.empty (FloverMap.empty (affine_form Q))) as Hdvars
by (unfold dVars_contained; intros * Hset; clear - Hset; set_tac). by (unfold dVars_contained; intros * Hset; clear - Hset; set_tac).
pose proof (RoundoffErrorValidator_sound e _ deltas_matched H approxE1E2 H1 eval_real R pose proof (RoundoffErrorValidator_sound e H approxE1E2 H1 eval_real R
valid_e map_e Hdvars) as Hsound. valid_e map_e Hdvars) as Hsound.
unfold validErrorBounds in Hsound. unfold validErrorBounds in Hsound.
eapply validErrorBounds_single in Hsound; eauto. eapply validErrorBoundsRec_single in Hsound; eauto.
destruct Hsound as [[vF [mF eval_float]] err_bounded]; auto. destruct Hsound as [[vF [mF eval_float]] err_bounded]; auto.
exists (elo, ehi), err_e, vR, vF, mF; repeat split; auto. exists (elo, ehi), err_e, vR, vF, mF; repeat split; auto.
Qed. Qed.
...@@ -105,8 +105,8 @@ Definition CertificateCheckerCmd (f:cmd Q) (absenv:analysisResult) (P: precond) ...@@ -105,8 +105,8 @@ Definition CertificateCheckerCmd (f:cmd Q) (absenv:analysisResult) (P: precond)
Theorem Certificate_checking_cmds_is_sound (f:cmd Q) (absenv:analysisResult) P Qmap Theorem Certificate_checking_cmds_is_sound (f:cmd Q) (absenv:analysisResult) P Qmap
defVars DeltaMap: defVars DeltaMap:
forall (E1 E2:env), forall (E1 E2:env),
(forall (e' : expr R) (m' : mType), (forall (v : R) (m' : mType),
exists d : R, DeltaMap e' 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 ->
CertificateCheckerCmd f absenv P Qmap defVars = true -> CertificateCheckerCmd f absenv P Qmap defVars = true ->
...@@ -160,7 +160,7 @@ Proof. ...@@ -160,7 +160,7 @@ Proof.
destruct iv as [f_lo f_hi]. destruct iv as [f_lo f_hi].
pose proof RoundoffErrorValidatorCmd_sound as Hsound. pose proof RoundoffErrorValidatorCmd_sound as Hsound.
eapply validErrorBoundsCmd_single in Hsound; eauto. eapply validErrorBoundsCmdRec_single in Hsound; eauto.
- specialize Hsound as ((vF & mF & eval_float) & ?). - specialize Hsound as ((vF & mF & eval_float) & ?).
exists (f_lo, f_hi), err, vR, vF, mF; repeat split; try auto. exists (f_lo, f_hi), err, vR, vF, mF; repeat split; try auto.
- eapply ssa_equal_set. 2: exact ssa_f_small. - eapply ssa_equal_set. 2: exact ssa_f_small.
......
...@@ -48,7 +48,7 @@ Inductive sstep : cmd R -> env -> R -> cmd R -> env -> Prop := ...@@ -48,7 +48,7 @@ Inductive sstep : cmd R -> env -> R -> cmd R -> env -> Prop :=
Define big step semantics for the Flover language, terminating on a "returned" Define big step semantics for the Flover language, terminating on a "returned"
result value result value
**) **)
Inductive bstep : cmd R -> env -> (expr R -> option mType) -> (expr R -> mType -> option R) -> Inductive bstep : cmd R -> env -> (expr R -> option mType) -> (R -> mType -> option R) ->
R -> mType -> Prop := R -> mType -> Prop :=
let_b m m' x e s E v res defVars DeltaMap: let_b m m' x e s E v res defVars DeltaMap:
eval_expr E defVars DeltaMap e v m -> eval_expr E defVars DeltaMap e v m ->
......
...@@ -4,17 +4,17 @@ From Coq ...@@ -4,17 +4,17 @@ From Coq
From Flover From Flover
Require Import Commands ExpressionSemantics Environments RealRangeArith TypeValidator. Require Import Commands ExpressionSemantics Environments RealRangeArith TypeValidator.
Fixpoint validErrorBounds (e:expr Q) E1 E2 A Gamma DeltaMap :Prop := Fixpoint validErrorBoundsRec (e:expr Q) E1 E2 A Gamma DeltaMap :Prop :=
(match e with (match e with
| Unop u e => validErrorBounds e E1 E2 A Gamma DeltaMap | Unop u e => validErrorBoundsRec e E1 E2 A Gamma DeltaMap
| Downcast m e => validErrorBounds e E1 E2 A Gamma DeltaMap | Downcast m e => validErrorBoundsRec e E1 E2 A Gamma DeltaMap
| Binop b e1 e2 => | Binop b e1 e2 =>
validErrorBounds e1 E1 E2 A Gamma DeltaMap /\ validErrorBoundsRec e1 E1 E2 A Gamma DeltaMap /\
validErrorBounds e2 E1 E2 A Gamma DeltaMap validErrorBoundsRec e2 E1 E2 A Gamma DeltaMap
| Fma e1 e2 e3 => | Fma e1 e2 e3 =>
validErrorBounds e1 E1 E2 A Gamma DeltaMap /\ validErrorBoundsRec e1 E1 E2 A Gamma DeltaMap /\
validErrorBounds e2 E1 E2 A Gamma DeltaMap /\ validErrorBoundsRec e2 E1 E2 A Gamma DeltaMap /\
validErrorBounds e3 E1 E2 A Gamma DeltaMap validErrorBoundsRec e3 E1 E2 A Gamma DeltaMap
| _ => True | _ => True
end) /\ end) /\
forall v__R (iv: intv) (err: error), forall v__R (iv: intv) (err: error),
...@@ -26,8 +26,14 @@ Fixpoint validErrorBounds (e:expr Q) E1 E2 A Gamma DeltaMap :Prop := ...@@ -26,8 +26,14 @@ Fixpoint validErrorBounds (e:expr Q) E1 E2 A Gamma DeltaMap :Prop :=
eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e) v__FP m__FP -> eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e) v__FP m__FP ->
(Rabs (v__R - v__FP) <= (Q2R err))%R). (Rabs (v__R - v__FP) <= (Q2R err))%R).
Lemma validErrorBounds_single e E1 E2 A Gamma DeltaMap: Definition validErrorBounds e E1 E2 A Gamma: Prop :=
validErrorBounds e E1 E2 A Gamma DeltaMap -> forall DeltaMap,
(forall (v : R) (m' : mType),
exists d : R, DeltaMap v m' = Some d /\ (Rabs d <= mTypeToR m')%R) ->
validErrorBoundsRec e E1 E2 A Gamma DeltaMap.
Lemma validErrorBoundsRec_single e E1 E2 A Gamma DeltaMap:
validErrorBoundsRec e E1 E2 A Gamma DeltaMap ->
forall v__R iv err, forall v__R iv err,
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 ->
FloverMap.find e A = Some (iv, err) -> FloverMap.find e A = Some (iv, err) ->
...@@ -39,13 +45,13 @@ Lemma validErrorBounds_single e E1 E2 A Gamma DeltaMap: ...@@ -39,13 +45,13 @@ Lemma validErrorBounds_single e E1 E2 A Gamma DeltaMap:
Proof. Proof.
intros validError_e; intros validError_e;
intros; destruct e; cbn in *; split; intros; destruct e; cbn in *; split;
destruct validError_e as (? & ? & ?); eauto. edestruct validError_e as (? & ? & ?); eauto.
Qed. Qed.
Fixpoint validErrorBoundsCmd (c: cmd Q) E1 E2 A Gamma DeltaMap: Prop := Fixpoint validErrorBoundsCmdRec (c: cmd Q) E1 E2 A Gamma DeltaMap: Prop :=
match c with match c with
| Let m x e k => | Let m x e k =>
validErrorBounds e E1 E2 A Gamma DeltaMap /\ validErrorBoundsRec e E1 E2 A Gamma DeltaMap /\
(exists iv_e err_e iv_x err_x, (exists iv_e err_e iv_x err_x,
FloverMap.find e A = Some (iv_e, err_e) /\ FloverMap.find e A = Some (iv_e, err_e) /\
FloverMap.find (Var Q x) A = Some (iv_x, err_x) /\ FloverMap.find (Var Q x) A = Some (iv_x, err_x) /\
...@@ -53,8 +59,8 @@ Fixpoint validErrorBoundsCmd (c: cmd Q) E1 E2 A Gamma DeltaMap: Prop := ...@@ -53,8 +59,8 @@ Fixpoint validErrorBoundsCmd (c: cmd Q) E1 E2 A Gamma DeltaMap: Prop :=
(forall v__R v__FP, (forall v__R v__FP,
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 ->
eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e) v__FP m -> eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e) v__FP m ->
validErrorBoundsCmd k (updEnv x v__R E1) (updEnv x v__FP E2) A Gamma DeltaMap) validErrorBoundsCmdRec k (updEnv x v__R E1) (updEnv x v__FP E2) A Gamma DeltaMap)
| Ret e => validErrorBounds e E1 E2 A Gamma DeltaMap | Ret e => validErrorBoundsRec e E1 E2 A Gamma DeltaMap
end /\ end /\
forall v__R (iv: intv) (err: error), forall v__R (iv: intv) (err: error),
bstep (toREvalCmd (toRCmd c)) E1 (toRTMap (toRExpMap Gamma)) DeltaMapR v__R REAL -> bstep (toREvalCmd (toRCmd c)) E1 (toRTMap (toRExpMap Gamma)) DeltaMapR v__R REAL ->
...@@ -65,8 +71,14 @@ Fixpoint validErrorBoundsCmd (c: cmd Q) E1 E2 A Gamma DeltaMap: Prop := ...@@ -65,8 +71,14 @@ Fixpoint validErrorBoundsCmd (c: cmd Q) E1 E2 A Gamma DeltaMap: Prop :=
bstep (toRCmd c) E2 (toRExpMap Gamma) DeltaMap v__FP m__FP -> bstep (toRCmd c) E2 (toRExpMap Gamma) DeltaMap v__FP m__FP ->
(Rabs (v__R - v__FP) <= (Q2R err))%R). (Rabs (v__R - v__FP) <= (Q2R err))%R).
Lemma validErrorBoundsCmd_single c E1 E2 A Gamma DeltaMap: Definition validErrorBoundsCmd (c: cmd Q) E1 E2 A Gamma: Prop :=
validErrorBoundsCmd c E1 E2 A Gamma DeltaMap -> forall DeltaMap,
(forall (v : R) (m' : mType),
exists d : R, DeltaMap v m' = Some d /\ (Rabs d <= mTypeToR m')%R) ->
validErrorBoundsCmdRec c E1 E2 A Gamma DeltaMap.
Lemma validErrorBoundsCmdRec_single c E1 E2 A Gamma DeltaMap:
validErrorBoundsCmdRec c E1 E2 A Gamma DeltaMap ->
forall v__R (iv: intv) (err: error), forall v__R (iv: intv) (err: error),
bstep (toREvalCmd (toRCmd c)) E1 (toRTMap (toRExpMap Gamma)) DeltaMapR v__R REAL -> bstep (toREvalCmd (toRCmd c)) E1 (toRTMap (toRExpMap Gamma)) DeltaMapR v__R REAL ->
FloverMap.find (getRetExp c) A = Some (iv, err) -> FloverMap.find (getRetExp c) A = Some (iv, err) ->
...@@ -78,5 +90,5 @@ Lemma validErrorBoundsCmd_single c E1 E2 A Gamma DeltaMap: ...@@ -78,5 +90,5 @@ Lemma validErrorBoundsCmd_single c E1 E2 A Gamma DeltaMap:
Proof. Proof.
intros validError_e; intros validError_e;
intros; destruct c; cbn in *; split; intros; destruct c; cbn in *; split;
destruct validError_e as (? & ? & ?); eauto. edestruct validError_e as (? & ? & ?); eauto.
Qed. Qed.
...@@ -43,8 +43,8 @@ Lemma add_abs_err_bounded (e1:expr Q) (e1R:R) (e1F:R) (e2:expr Q) (e2R:R) (e2F:R ...@@ -43,8 +43,8 @@ Lemma add_abs_err_bounded (e1:expr Q) (e1R:R) (e1F:R) (e2:expr Q) (e2R:R) (e2F:R
eval_expr (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) eval_expr (updEnv 2 e2F (updEnv 1 e1F emptyEnv))
(updDefVars (Binop Plus (Var R 1) (Var R 2)) m (updDefVars (Binop Plus (Var R 1) (Var R 2)) m
(updDefVars (Var R 2) m2 (updDefVars (Var R 1) m1 defVars))) (updDefVars (Var R 2) m2 (updDefVars (Var R 1) m1 defVars)))
(fun x _ => if R_orderedExps.eq_dec x (Binop Plus (Var R 1) (Var R 2)) (fun x _ => if Req_dec_sum x (evalBinop Plus e1F e2F)
then DeltaMap (Binop Plus (toRExp e1) (toRExp e2)) m then DeltaMap (evalBinop Plus e1F e2F) m
else None) else None)
(Binop Plus (Var R 1) (Var R 2)) vF m -> (Binop Plus (Var R 1) (Var R 2)) vF m ->
(Rabs (e1R - e1F) <= Q2R err1)%R -> (Rabs (e1R - e1F) <= Q2R err1)%R ->
...@@ -116,8 +116,8 @@ Lemma subtract_abs_err_bounded (e1:expr Q) (e1R:R) (e1F:R) (e2:expr Q) (e2R:R) ...@@ -116,8 +116,8 @@ Lemma subtract_abs_err_bounded (e1:expr Q) (e1R:R) (e1F:R) (e2:expr Q) (e2R:R)
eval_expr (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) eval_expr (updEnv 2 e2F (updEnv 1 e1F emptyEnv))
(updDefVars (Binop Sub (Var R 1) (Var R 2)) m (updDefVars (Binop Sub (Var R 1) (Var R 2)) m
(updDefVars (Var R 2) m2 (updDefVars (Var R 1) m1 defVars))) (updDefVars (Var R 2) m2 (updDefVars (Var R 1) m1 defVars)))
(fun x _ => if R_orderedExps.eq_dec x (Binop Sub (Var R 1) (Var R 2)) (fun x _ => if Req_dec_sum x (evalBinop Sub e1F e2F)
then DeltaMap (Binop Sub (toRExp e1) (toRExp e2)) m then DeltaMap (evalBinop Sub e1F e2F) m
else None) else None)
(Binop Sub (Var R 1) (Var R 2)) vF m -> (Binop Sub (Var R 1) (Var R 2)) vF m ->
(Rabs (e1R - e1F) <= Q2R err1)%R -> (Rabs (e1R - e1F) <= Q2R err1)%R ->
...@@ -194,8 +194,8 @@ Lemma mult_abs_err_bounded (e1:expr Q) (e1R:R) (e1F:R) (e2:expr Q) (e2R:R) (e2F: ...@@ -194,8 +194,8 @@ Lemma mult_abs_err_bounded (e1:expr Q) (e1R:R) (e1F:R) (e2:expr Q) (e2R:R) (e2F:
eval_expr (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) eval_expr (updEnv 2 e2F (updEnv 1 e1F emptyEnv))
(updDefVars (Binop Mult (Var R 1) (Var R 2)) m (updDefVars (Binop Mult (Var R 1) (Var R 2)) m
(updDefVars (Var R 2) m2 (updDefVars (Var R 1) m1 defVars))) (updDefVars (Var R 2) m2 (updDefVars (Var R 1) m1 defVars)))
(fun x _ => if R_orderedExps.eq_dec x (Binop Mult (Var R 1) (Var R 2)) (fun x _ => if Req_dec_sum x (evalBinop Mult e1F e2F)
then DeltaMap (Binop Mult (toRExp e1) (toRExp e2)) m then DeltaMap (evalBinop Mult e1F e2F) m
else None) else None)
(Binop Mult (Var R 1) (Var R 2)) vF m -> (Binop Mult (Var R 1) (Var R 2)) vF m ->
(Rabs (vR - vF) <= Rabs (e1R * e2R - e1F * e2F) + computeErrorR (e1F * e2F) m)%R. (Rabs (vR - vF) <= Rabs (e1R * e2R - e1F * e2F) + computeErrorR (e1F * e2F) m)%R.
...@@ -245,8 +245,8 @@ Lemma div_abs_err_bounded (e1:expr Q) (e1R:R) (e1F:R) (e2:expr Q) (e2R:R) (e2F:R ...@@ -245,8 +245,8 @@ Lemma div_abs_err_bounded (e1:expr Q) (e1R:R) (e1F:R) (e2:expr Q) (e2R:R) (e2F:R
eval_expr (updEnv 2 e2F (updEnv 1 e1F emptyEnv)) eval_expr (updEnv 2 e2F (updEnv 1 e1F emptyEnv))
(updDefVars (Binop Div (Var R 1) (Var R 2)) m (updDefVars (Binop Div (Var R 1) (Var R 2)) m
(updDefVars (Var R 2) m2 (updDefVars (Var R 1) m1 defVars))) (updDefVars (Var R 2) m2 (updDefVars (Var R 1) m1 defVars)))
(fun x _ => if R_orderedExps.eq_dec x (Binop Div (Var R 1) (Var R 2)) (fun x _ => if Req_dec_sum x (evalBinop Div e1F e2F)
then DeltaMap (Binop Div (toRExp e1) (toRExp e2)) m then DeltaMap (evalBinop Div e1F e2F) m
else None) else None)
(Binop Div (Var R 1) (Var R 2)) vF m -> (Binop Div (Var R 1) (Var R 2)) vF m ->
(Rabs (vR - vF) <= Rabs (e1R / e2R - e1F / e2F) + computeErrorR (e1F / e2F) m)%R. (Rabs (vR - vF) <= Rabs (e1R / e2R - e1F / e2F) + computeErrorR (e1F / e2F) m)%R.
...@@ -301,8 +301,8 @@ Lemma fma_abs_err_bounded (e1:expr Q) (e1R:R) (e1F:R) (e2:expr Q) (e2R:R) (e2F:R ...@@ -301,8 +301,8 @@ Lemma fma_abs_err_bounded (e1:expr Q) (e1R:R) (e1F:R) (e2:expr Q) (e2R:R) (e2F:R
(updDefVars (Fma (Var R 1) (Var R 2) (Var R 3)) m (updDefVars (Fma (Var R 1) (Var R 2) (Var R 3)) m
(updDefVars (Var R 3) m3 (updDefVars (Var R 3) m3
(updDefVars (Var R 2) m2 (updDefVars (Var R 1) m1 defVars)))) (updDefVars (Var R 2) m2 (updDefVars (Var R 1) m1 defVars))))
(fun x _ => if R_orderedExps.eq_dec x (Fma (Var R 1) (Var R 2) (Var R 3)) (fun x _ => if Req_dec_sum x (evalFma e1F e2F e3F)
then DeltaMap (Fma (toRExp e1) (toRExp e2) (toRExp e3)) m then DeltaMap (evalFma e1F e2F e3F) m
else None) else None)
(Fma (Var R 1) (Var R 2) (Var R 3)) vF m -> (Fma (Var R 1) (Var R 2) (Var R 3)) vF m ->
(Rabs (vR - vF) <= Rabs ((e1R * e2R - e1F * e2F) + (e3R - e3F)) + computeErrorR (e1F * e2F + e3F ) m)%R. (Rabs (vR - vF) <= Rabs ((e1R * e2R - e1F * e2F) + (e3R - e3F)) + computeErrorR (e1F * e2F + e3F ) m)%R.
...@@ -366,8 +366,8 @@ Lemma round_abs_err_bounded (e:expr R) (nR nF1 nF:R) (E1 E2: env) (err:R) ...@@ -366,8 +366,8 @@ Lemma round_abs_err_bounded (e:expr R) (nR nF1 nF:R) (E1 E2: env) (err:R)
eval_expr (updEnv 1 nF1 emptyEnv) eval_expr (updEnv 1 nF1 emptyEnv)
(updDefVars (Downcast mEps (Var R 1)) mEps (updDefVars (Downcast mEps (Var R 1)) mEps
(updDefVars (Var R 1) m defVars)) (updDefVars (Var R 1) m defVars))
(fun x _ => if R_orderedExps.eq_dec x (Downcast mEps (Var R 1)) (fun x _ => if Req_dec_sum x nF1
then DeltaMap (Downcast mEps e) mEps then DeltaMap nF1 mEps
else None) else None)
(toRExp (Downcast mEps (Var Q 1))) nF mEps-> (toRExp (Downcast mEps (Var Q 1))) nF mEps->
(Rabs (nR - nF1) <= err)%R -> (Rabs (nR - nF1) <= err)%R ->
......
This diff is collapsed.
...@@ -236,6 +236,11 @@ Fixpoint validErrorboundAACmd (f: cmd Q) (* analyzed cmd with let's *) ...@@ -236,6 +236,11 @@ Fixpoint validErrorboundAACmd (f: cmd Q) (* analyzed cmd with let's *)
| 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
about memoization cases. This allows us to show several monotonicity lemmas
that simplify the soundness proofs. This definition is just an extract from
the full soundness statement, for elaboration on the used assumptions and the
goal, find that statement below *)
Definition checked_error_expressions (e: expr Q) E1 E2 A Gamma DeltaMap Definition checked_error_expressions (e: expr Q) E1 E2 A Gamma DeltaMap
noise_map noise expr_map := noise_map noise expr_map :=
forall v__R v__FP m__FP (iv__A: intv) (err__A: error), forall v__R v__FP m__FP (iv__A: intv) (err__A: error),
...@@ -777,12 +782,17 @@ Proof. ...@@ -777,12 +782,17 @@ Proof.
* apply flover_map_in_add. * apply flover_map_in_add.
Qed. Qed.
(* The soundness statements starts off with assumption that the checking
function succeeds and then also maintains several invariants. We require
these invariants because of the checker function dependency on the current
noise index and its memoization of the previosly computed polynomials. We
explain these invariants in-line below. *)
Definition validErrorboundAA_sound_statement e E1 E2 A Gamma DeltaMap fVars dVars := Definition validErrorboundAA_sound_statement e E1 E2 A Gamma DeltaMap fVars dVars :=
forall (expr_map1 expr_map2 : FloverMap.t (affine_form Q)) forall (expr_map1 expr_map2 : FloverMap.t (affine_form Q))
(noise_map1 : nat -> option noise_type) (noise1 noise2 : nat) (v__R : R) (noise_map1 : nat -> option noise_type) (noise1 noise2 : nat) (v__R : R)
(iv__A : intv) (err__A : error), (iv__A : intv) (err__A : error),
(forall (e' : expr R) (m' : mType), (forall (v : R) (m' : mType),
exists d : R, DeltaMap e' m' = Some d /\ (Rabs d <= mTypeToR m')%R) -> exists d : R, DeltaMap v m' = Some d /\ (Rabs d <= mTypeToR m')%R) ->
approxEnv E1 (toRExpMap Gamma) A fVars dVars E2 -> approxEnv E1 (toRExpMap Gamma) A fVars dVars E2 ->
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)) ->
...@@ -790,39 +800,74 @@ Definition validErrorboundAA_sound_statement e E1 E2 A Gamma DeltaMap fVars dVar ...@@ -790,39 +800,74 @@ Definition validErrorboundAA_sound_statement e E1 E2 A Gamma DeltaMap fVars dVar
NatSet.Subset (usedVars e -- dVars) fVars -> NatSet.Subset (usedVars 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
map it and anything above to a noise value *)
(0 < noise1)%nat -> (0 < noise1)%nat ->
(forall n0 : nat, (n0 >= noise1)%nat -> noise_map1 n0 = None) -> (forall n0 : nat, (n0 >= noise1)%nat -> noise_map1 n0 = None) ->
(* If a var is a dVar, we know it's in expr_map and invoke the corresponding
preconditions (described below) *)
dVars_contained dVars expr_map1 -> dVars_contained dVars expr_map1 ->
(* Precondition:
Memoization for the existential case of the goal: if we checked the expression
already, we know that there is an execution and certificate results for it *)
(forall e' : FloverMap.key, (forall e' : FloverMap.key,
FloverMap.In e' expr_map1 -> FloverMap.In e' expr_map1 ->
(* Assumption needed for Cmd_sound proof *)
NatSet.Subset (usedVars e') (NatSet.union fVars dVars) /\ NatSet.Subset (usedVars 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') ->
(* Precondition:
Memoization for the universal case of the goal -- note that
`checked_error_expressions` track only that case: if we checked
the expression already, then, if we provide the execution in
finite precision and the certificate results, we will know that
the execution's error is bounded *)
(forall e' : FloverMap.key, (forall e' : FloverMap.key,
FloverMap.In e' expr_map1 -> FloverMap.In e' expr_map1 ->
checked_error_expressions e' E1 E2 A Gamma DeltaMap noise_map1 noise1 expr_map1) -> checked_error_expressions e' E1 E2 A Gamma DeltaMap noise_map1 noise1 expr_map1) ->
(* THE EXESTENTIAL CASE OF THE GOAL *)
((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) /\
(* Invariant of the existential case:
our given expr_map1 is updated only with the expressions for which
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) /\ NatSet.Subset (usedVars 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')) /\
(* UNIVERSAL CASE OF THE GOAL *)
(forall (v__FP : R) (m__FP : mType), (forall (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 ->
(* For the given evaluation we can find a polynomial and an
error bound with a monotonic extension of noise_map1 to
noise_map2 *)
exists (af : affine_form Q) (err__af : R) (noise_map2 : noise_mapping), exists (af : affine_form Q) (err__af : R) (noise_map2 : noise_mapping),
(* Invariant: the checker function only adds new polynomials
to the expr_map, never removes something from it *)
contained_flover_map expr_map1 expr_map2 /\ contained_flover_map expr_map1 expr_map2 /\
(* Noise index invariants: the checker function returns new
noise that is not used in already produced polynomials *)
(noise1 <= noise2)%nat /\ (noise1 <= noise2)%nat /\
fresh noise2 (afQ2R af) /\ fresh noise2 (afQ2R af) /\
(* Invariant: noise_map is incrementally updated *)
contained_map noise_map1 noise_map2 /\ contained_map noise_map1 noise_map2 /\
(forall n0 : nat, (n0 >= noise2)%nat -> noise_map2 n0 = None) /\ (forall n0 : nat, (n0 >= noise2)%nat -> noise_map2 n0 = None) /\
FloverMap.find (elt:=affine_form Q) e expr_map2 = Some af /\ FloverMap.find (elt:=affine_form Q) e expr_map2 = Some af /\
(* To show that the error is bounded by the polynomial, we say that
the polynomial's range is bounded by err__af, which has a value
less or equal to the certificate error, and that the polynomial
captures any difference between real and finite-precision
evaluations *)
(0 <= err__af)%R /\ (0 <= err__af)%R /\
toInterval (afQ2R af) = ((- err__af)%R, err__af) /\ toInterval (afQ2R af) = ((- err__af)%R, err__af) /\
(err__af <= Q2R err__A)%R /\ (err__af <= Q2R err__A)%R /\
af_evals (afQ2R af) (v__R - v__FP) noise_map2 /\ af_evals (afQ2R af) (v__R - v__FP) noise_map2 /\
(* Invariant of the universal case:
our given expr_map1 is updated only with the expressions for which
the universal part (the conclusion directly above) 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 ->
checked_error_expressions e' E1 E2 A Gamma DeltaMap noise_map2 noise2 expr_map2)). checked_error_expressions e' E1 E2 A Gamma DeltaMap noise_map2 noise2 expr_map2)).
...@@ -1008,7 +1053,7 @@ Proof. ...@@ -1008,7 +1053,7 @@ Proof.
eval_expr E2 (toRExpMap Gamma) DeltaMap eval_expr E2 (toRExpMap Gamma) DeltaMap
(toRExp (Expressions.Const m v)) v__FP m__FP). (toRExp (Expressions.Const m v)) v__FP m__FP).
{ {
specialize (Hdeltamap (toRExp (Expressions.Const m v)) m) specialize (Hdeltamap (Q2R v) m)
as (delta' & Hdelta & Hdelta'). as (delta' & Hdelta & Hdelta').
exists (perturb (Q2R v) m delta'), m. exists (perturb (Q2R v) m delta'), m.
eapply Const_dist' with (delta := delta'); auto. eapply Const_dist' with (delta := delta'); auto.
...@@ -1351,7 +1396,7 @@ Proof. ...@@ -1351,7 +1396,7 @@ Proof.
assert (exists (v__FP : R) (m__FP : mType), assert (exists (v__FP : R) (m__FP : mType),
eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp (Binop Plus e1 e2)) v__FP m__FP) as H. eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp (Binop Plus e1 e2)) v__FP m__FP) as H.
{ {
specialize (Hdeltamap (toRExp (Binop Plus e1 e2)) m__e) specialize (Hdeltamap (evalBinop Plus nF1 nF2) m__e)
as (delta' & Hdelta & Hdelta'). as (delta' & Hdelta & Hdelta').
eexists; exists m__e. eexists; exists m__e.
eapply Binop_dist' with (delta := delta'); eauto. eapply Binop_dist' with (delta := delta'); eauto.
...@@ -1615,7 +1660,7 @@ Proof. ...@@ -1615,7 +1660,7 @@ Proof.
assert (exists (v__FP : R) (m__FP : mType), assert (exists (v__FP : R) (m__FP : mType),
eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp (Binop Sub e1 e2)) v__FP m__FP). eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp (Binop Sub e1 e2)) v__FP m__FP).
{ {
specialize (Hdeltamap (toRExp (Binop Sub e1 e2)) m__e) specialize (Hdeltamap (evalBinop Sub nF1 nF2) m__e)
as (delta' & Hdelta & Hdelta'). as (delta' & Hdelta & Hdelta').
eexists; exists m__e. eexists; exists m__e.
eapply Binop_dist' with (delta := delta'); eauto. eapply Binop_dist' with (delta := delta'); eauto.
...@@ -1867,7 +1912,7 @@ Proof. ...@@ -1867,7 +1912,7 @@ Proof.
assert (exists (v__FP : R) (m__FP : mType), assert (exists (v__FP : R) (m__FP : mType),
eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp (Binop Mult e1 e2)) v__FP m__FP). eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp (Binop Mult e1 e2)) v__FP m__FP).
{ {
specialize (Hdeltamap (toRExp (Binop Mult e1 e2)) m__e) specialize (Hdeltamap (evalBinop Mult nF1 nF2) m__e)
as (delta' & Hdelta & Hdelta'). as (delta' & Hdelta & Hdelta').
eexists; exists m__e. eexists; exists m__e.
eapply Binop_dist' with (delta := delta'); eauto. eapply Binop_dist' with (delta := delta'); eauto.
...@@ -2180,7 +2225,7 @@ Proof. ...@@ -2180,7 +2225,7 @@ Proof.
assert (exists (v__FP : R) (m__FP : mType), assert (exists (v__FP : R) (m__FP : mType),
eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp (Binop Div e1 e2)) v__FP m__FP). eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp (Binop Div e1 e2)) v__FP m__FP).
{ {
specialize (Hdeltamap (toRExp (Binop Div e1 e2)) m__e) specialize (Hdeltamap (evalBinop Div nF1 nF2) m__e)
as (delta' & Hdelta & Hdelta'). as (delta' & Hdelta & Hdelta').
eexists; exists m__e. eexists; exists m__e.
eapply Binop_dist' with (delta := delta'); eauto. eapply Binop_dist' with (delta := delta'); eauto.
...@@ -2580,7 +2625,7 @@ Proof. ...@@ -2580,7 +2625,7 @@ Proof.
assert (exists (v__FP : R) (m__FP : mType), assert (exists (v__FP : R) (m__FP : mType),
eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp (Fma e1 e2 e3)) v__FP m__FP). eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp (Fma e1 e2 e3)) v__FP m__FP).
{ {
specialize (Hdeltamap (toRExp (Fma e1 e2 e3)) m__e) specialize (Hdeltamap (evalFma nF1 nF2 nF3) m__e)
as (delta' & Hdelta & Hdelta'). as (delta' & Hdelta & Hdelta').
eexists; exists m__e. eexists; exists m__e.
eapply Fma_dist' with (delta:= delta'); eauto. eapply Fma_dist' with (delta:= delta'); eauto.
...@@ -2882,7 +2927,7 @@ Proof. ...@@ -2882,7 +2927,7 @@ Proof.
assert (exists (v__FP : R) (m__FP : mType), assert (exists (v__FP : R) (m__FP : mType),
eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp (Downcast m__e e)) v__FP m__FP). eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp (Downcast m__e e)) v__FP m__FP).
{ {
specialize (Hdeltamap (toRExp (Downcast m__e e)) m__e) specialize (Hdeltamap nF m__e)
as (delta' & Hdelta & Hdelta'). as (delta' & Hdelta & Hdelta').
exists (perturb nF m__e delta'), m__e. exists (perturb nF m__e delta'), m__e.
eapply Downcast_dist' with (delta := delta'); eauto. eapply Downcast_dist' with (delta := delta'); eauto.
...@@ -3023,7 +3068,7 @@ Corollary validErrorbound_sound_validErrorBounds e E1 E2 A Gamma DeltaMap expr_m ...@@ -3023,7 +3068,7 @@ Corollary validErrorbound_sound_validErrorBounds e E1 E2 A Gamma DeltaMap expr_m
eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e') v__FP' m__FP') /\ eval_expr E2 (toRExpMap Gamma) DeltaMap (toRExp e') v__FP' m__FP') /\
checked_error_expressions e' E1 E2 A Gamma DeltaMap noise_map noise expr_map) -> checked_error_expressions e' E1 E2 A Gamma DeltaMap noise_map noise expr_map) ->
contained_subexpr e expr_map -> contained_subexpr e expr_map ->
validErrorBounds e E1 E2 A Gamma DeltaMap. validErrorBoundsRec e E1 E2 A Gamma DeltaMap.
Proof. Proof.
induction e; intros Hchecked Hsubexpr. induction e; intros Hchecked Hsubexpr.
- split; [trivial|]. - split; [trivial|].
...@@ -3061,6 +3106,7 @@ Proof. ...@@ -3061,6 +3106,7 @@ Proof.
- cbn.