Commit c2e75dee authored by Joachim Bard's avatar Joachim Bard

checking missing invariants for subdivs

parent 93e18826
...@@ -9,8 +9,24 @@ Require Import List FunInd Sorting.Permutation Sorting.Mergesort Orders. ...@@ -9,8 +9,24 @@ Require Import List FunInd Sorting.Permutation Sorting.Mergesort Orders.
Fixpoint resultLeq e (A1 A2: analysisResult) := Fixpoint resultLeq e (A1 A2: analysisResult) :=
match e with match e with
| Unop _ e1 | Downcast _ e1 => resultLeq e1 A1 A2 | Unop _ e1 | Downcast _ e1 => resultLeq e1 A1 A2
| Binop _ e1 e2 | Let _ _ e1 e2 => resultLeq e1 A1 A2 && resultLeq e2 A1 A2 | Binop b e1 e2 => resultLeq e1 A1 A2 && resultLeq e2 A1 A2 &&
match b with
| Div => match FloverMap.find e2 A2 with
| Some (iv2, err) =>
Qleb 0 err &&
(Qleb (snd iv2 + err) 0 && negb (Qeq_bool (snd iv2 + err) 0)
|| Qleb 0 (fst iv2 - err) && negb (Qeq_bool (fst iv2 - err) 0))
| _ => false
end
| _ => true
end
| Fma e1 e2 e3 => resultLeq e1 A1 A2 && resultLeq e2 A1 A2 && resultLeq e3 A1 A2 | Fma e1 e2 e3 => resultLeq e1 A1 A2 && resultLeq e2 A1 A2 && resultLeq e3 A1 A2
| Let _ x e1 e2 => resultLeq e1 A1 A2 && resultLeq e2 A1 A2 &&
match FloverMap.find (Var Q x) A2, FloverMap.find e1 A2 with
| Some (ivX, errX), Some (iv1, err1) =>
Qeqb (ivlo iv1) (ivlo ivX) && Qeqb (ivhi iv1) (ivhi ivX) && Qeqb err1 errX
| _, _ => false
end
| _ => true | _ => true
end && end &&
match FloverMap.find e A1, FloverMap.find e A2 with match FloverMap.find e A1, FloverMap.find e A2 with
...@@ -59,27 +75,36 @@ Proof. ...@@ -59,27 +75,36 @@ Proof.
rewrite Hfind in Hleq. Flover_compute. rewrite Hfind in Hleq. Flover_compute.
split; auto. kill_trivial_exists. exists vR. canonize_hyps; cbn in *. split; auto. kill_trivial_exists. exists vR. canonize_hyps; cbn in *.
repeat split; auto; lra. repeat split; auto; lra.
- intros H ((Hdiv & H1 & H2) & iv & err & vR & Hfind & Heval & Hiv). - intros H ((_ & H1 & H2) & iv & err & vR & Hfind & Heval & Hiv).
apply andb_true_iff in H as [H Hleq]. apply andb_true_iff in H as [H Hleq].
apply andb_true_iff in H as [H Hdiv].
apply andb_true_iff in H as [Hleq1 Hleq2]. apply andb_true_iff in H as [Hleq1 Hleq2].
rewrite Hfind in Hleq. Flover_compute. rewrite Hfind in Hleq.
(* destruct (FloverMap.find (Binop b e1 e2) A2) eqn: Hfind2; try congruence. *)
repeat split; auto. repeat split; auto.
+ intros -> ivA2 errA2 Hfind2. + intros -> ivA2 errA2 Hfind2.
edestruct (resultLeq_sound _ _ _ Hleq2) edestruct (resultLeq_sound _ _ _ Hleq2)
as (ivA1 & errA1 & ? & ? & Hfind1 & Hfind2' & Hsub & _). as (ivA1 & errA1 & ? & ? & Hfind1 & Hfind2' & Hsub & _).
rewrite Hfind2' in Hfind2. rewrite Hfind2' in Hfind2.
injection Hfind2. intros _ ->. injection Hfind2. intros -> ->.
specialize (Hdiv eq_refl ivA1 errA1 Hfind1). (* specialize (Hdiv eq_refl ivA1 errA1 Hfind1). *)
apply andb_true_iff in Hsub as [Hsub1 Hsub2]. apply andb_true_iff in Hsub as [Hsub1 Hsub2].
cbn in *. cbn in *.
unfold error in *.
rewrite Hfind2' in Hdiv.
apply orb_true_iff. apply orb_true_iff.
apply andb_true_iff in Hdiv as [Herr Hdiv].
apply orb_true_iff in Hdiv as [Hdiv | Hdiv]; [left | right]. apply orb_true_iff in Hdiv as [Hdiv | Hdiv]; [left | right].
* andb_to_prop Hdiv. * Flover_compute.
apply andb_true_iff. apply andb_true_iff.
admit. (* needs additional checks *) admit.
* admit. * admit.
+ kill_trivial_exists. exists vR. canonize_hyps; cbn in *. + destruct (FloverMap.find (Binop b e1 e2) A2) as [[iv2 err2]|] eqn: Hfind2; try congruence.
repeat split; auto; lra. kill_trivial_exists. exists vR.
apply andb_true_iff in Hleq as [Hsub _].
apply andb_true_iff in Hsub as [Hsub1 Hsub2].
canonize_hyps; cbn in *.
repeat split; auto; lra.
- intros H ((H1 & H2 & H3) & iv & err & vR & Hfind & Heval & Hiv). - intros H ((H1 & H2 & H3) & iv & err & vR & Hfind & Heval & Hiv).
apply andb_true_iff in H as [H Hleq]. apply andb_true_iff in H as [H Hleq].
apply andb_true_iff in H as [H Hleq3]. apply andb_true_iff in H as [H Hleq3].
...@@ -97,7 +122,9 @@ Proof. ...@@ -97,7 +122,9 @@ Proof.
apply andb_true_iff in H as [Hleq1 Hleq2]. apply andb_true_iff in H as [Hleq1 Hleq2].
rewrite Hfind in Hleq. Flover_compute. rewrite Hfind in Hleq. Flover_compute.
repeat split; auto. repeat split; auto.
+ admit. (* needs additional checker *) + repeat eexists. repeat split; eauto.
unfold Qeqb in *.
now rewrite L1, R2.
+ kill_trivial_exists. exists vR. canonize_hyps; cbn in *. + kill_trivial_exists. exists vR. canonize_hyps; cbn in *.
repeat split; auto; lra. repeat split; auto; lra.
Admitted. Admitted.
...@@ -147,13 +174,19 @@ Proof. ...@@ -147,13 +174,19 @@ Proof.
intros vFP mFP HevalFP. intros vFP mFP HevalFP.
specialize (Hall vFP mFP HevalFP). specialize (Hall vFP mFP HevalFP).
lra. lra.
- edestruct err_sound as ((Hdiv & H1 & H2) & Herr). - edestruct err_sound as ((_ & H1 & H2) & Herr).
cbn in Hleq. cbn in Hleq.
apply andb_true_iff in Hleq as [H Hleq]. apply andb_true_iff in Hleq as [H Hleq].
apply andb_true_iff in H as [H Hdiv].
apply andb_true_iff in H as [Hleq1 Hleq2]. apply andb_true_iff in H as [Hleq1 Hleq2].
split. split.
+ cbn in Hdiv. admit. + repeat split; auto.
intros -> iv2 err Hfind2.
unfold error in *.
rewrite Hfind2 in Hdiv.
now apply andb_true_iff in Hdiv as [_ Hdiv].
+ intros vR iv err Heval Hfind. + intros vR iv err Heval Hfind.
clear Hdiv.
Flover_compute. Flover_compute.
unfold error in *. unfold error in *.
assert (e0 = err) by congruence; subst. assert (e0 = err) by congruence; subst.
...@@ -193,12 +226,20 @@ Proof. ...@@ -193,12 +226,20 @@ Proof.
intros vFP mFP HevalFP. intros vFP mFP HevalFP.
specialize (Hall vFP mFP HevalFP). specialize (Hall vFP mFP HevalFP).
lra. lra.
- edestruct err_sound as ((H1 & Hx & H2) & Herr). - edestruct err_sound as ((H1 & _ & H2) & Herr).
cbn in Hleq. cbn in Hleq.
apply andb_true_iff in Hleq as [H Hleq]. apply andb_true_iff in Hleq as [H Hleq].
apply andb_true_iff in H as [H Hx].
apply andb_true_iff in H as [Hleq1 Hleq2]. apply andb_true_iff in H as [Hleq1 Hleq2].
split; auto. split; auto.
+ split; auto. split; auto. admit. + split; auto. split; auto.
intros iv1 err1 ivX errX Hfind1 HfindX.
unfold error in *.
rewrite Hfind1, HfindX in Hx.
apply andb_true_iff in Hx as [Hx Hxerr].
apply andb_true_iff in Hx as [Hx1 Hx2].
unfold Qeqb in *.
canonize_hyps. now repeat split.
+ intros vR iv err Heval Hfind. + intros vR iv err Heval Hfind.
Flover_compute. Flover_compute.
unfold error in *. unfold error in *.
...@@ -209,7 +250,7 @@ Proof. ...@@ -209,7 +250,7 @@ Proof.
intros vFP mFP HevalFP. intros vFP mFP HevalFP.
specialize (Hall vFP mFP HevalFP). specialize (Hall vFP mFP HevalFP).
lra. lra.
Admitted. Qed.
(* TODO: maybe put this somewhere else *) (* TODO: maybe put this somewhere else *)
Lemma approxEnv_empty_dVars A1 A2 Gamma fVars dVars E1 E2 : Lemma approxEnv_empty_dVars A1 A2 Gamma fVars dVars E1 E2 :
......
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