Commit 21020dd3 authored by Nikita Zyuzin's avatar Nikita Zyuzin

Admit failing proofs until compilation succeeds

parent a15329f3
......@@ -149,6 +149,6 @@ Proof.
pose proof (validRangesCmd_single _ _ _ _ valid_f) as valid_single.
destruct valid_single as [iv [ err [vR [map_f [eval_real bounded_real_f]]]]].
destruct iv as [f_lo f_hi].
edestruct (RoundoffErrorValidatorCmd_sound) as [[vF [mF eval_float]] ?]; eauto.
edestruct (RoundoffErrorValidatorCmd_sound) as [[vF [mF eval_float]] ?]; eauto; [admit|].
exists (f_lo, f_hi), err, vR, vF, mF; repeat split; try auto.
Qed.
Admitted.
......@@ -1218,10 +1218,11 @@ Proof.
{ eapply validTypes_exec; eauto. }
subst.
edestruct eval_expr_gives_IEEE; eauto.
- admit.
- intros. set_tac.
- destruct H4 as [eval_float_f eval_rel].
repeat eexists; eauto.
Qed.
Admitted.
Theorem IEEE_connection_cmd (f:cmd fl64) (A:analysisResult) P
defVars E1 E2:
......@@ -1279,6 +1280,7 @@ Proof.
destruct valid_single as [iv [ err [vR [map_f [eval_real bounded_real_f]]]]].
destruct iv as [f_lo f_hi].
edestruct (RoundoffErrorValidator.RoundoffErrorValidatorCmd_sound) as [[vF [mF eval_float]] ?]; eauto.
1: admit.
assert (M64 = mF).
{ pose proof H0 as validT.
eapply validTypesCmd_single in H0.
......@@ -1288,7 +1290,8 @@ Proof.
congruence. }
subst.
edestruct bstep_gives_IEEE; eauto.
- admit.
- intros; set_tac.
- destruct H2.
repeat eexists; eauto.
Qed.
Admitted.
......@@ -7,10 +7,13 @@ From Flover
Definition RoundoffErrorValidator (e:expr Q) (tMap:FloverMap.t mType)
(A:analysisResult) (dVars:NatSet.t) :=
(* if *)
validErrorbound e tMap A dVars.
(*then true *)
(* else validAffineErrorBounds e A tMap dVars *)
if
validErrorbound e tMap A dVars
then true
else match validErrorboundAA e tMap A dVars 1 (FloverMap.empty (affine_form Q)) with
| Some _ => true
| None => false
end.
Theorem RoundoffErrorValidator_sound:
forall (e : expr Q) (E1 E2 : env) (fVars dVars : NatSet.t) (A : analysisResult)
......@@ -30,14 +33,17 @@ Theorem RoundoffErrorValidator_sound:
Proof.
intros. cbn in *.
eapply validErrorbound_sound; eauto.
Qed.
Admitted.
Definition RoundoffErrorValidatorCmd (f:cmd Q) (tMap:FloverMap.t mType)
(A:analysisResult) (dVars:NatSet.t) :=
(* if *)
validErrorboundCmd f tMap A dVars.
(*then true *)
(* else validAffineErrorboundsCmd e A tMap dVars ... *)
if
validErrorboundCmd f tMap A dVars
then true
else match validErrorboundAACmd f tMap A dVars 1 (FloverMap.empty (affine_form Q)) with
| Some _ => true
| None => false
end.
Theorem RoundoffErrorValidatorCmd_sound f:
forall A E1 E2 outVars fVars dVars vR elo ehi err Gamma,
......@@ -60,4 +66,4 @@ Proof.
split.
- eapply validErrorboundCmd_gives_eval; eauto.
- intros. eapply validErrorboundCmd_sound; eauto.
Qed.
Admitted.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment