Commit 981aa890 authored by Joachim Bard's avatar Joachim Bard

simplifications and fixing compile issues

parent 858945d3
......@@ -1140,7 +1140,7 @@ Theorem IEEE_connection_expr e A P qMap E1 E2 defVars DeltaMap:
noDowncast (B2Qexpr e) ->
eval_expr_valid e E2 ->
unsat_queries qMap ->
P_intv_sound E1 P ->
eval_precond E1 P ->
CertificateChecker (B2Qexpr e) A P qMap defVars = true ->
exists Gamma, (* m, currently = M64 *)
approxEnv E1 Gamma A (usedVars (B2Qexpr e)) (NatSet.empty) (toREnv E2) ->
......@@ -1210,7 +1210,7 @@ Theorem IEEE_connection_cmd (f:cmd fl64) (A:analysisResult) P qMap
noDowncastFun (B2Qcmd f) ->
bstep_valid f E2 ->
unsat_queries qMap ->
P_intv_sound E1 P ->
eval_precond E1 P ->
CertificateCheckerCmd (B2Qcmd f) A P qMap defVars = true ->
exists Gamma,
approxEnv E1 (toRExpMap Gamma) A (freeVars (B2Qcmd f)) NatSet.empty (toREnv E2) ->
......
......@@ -30,21 +30,19 @@ Theorem RangeValidator_sound (e : expr Q) (A : analysisResult) (P : precond)
unsat_queries Qmap ->
validRanges e A E (toRTMap (toRExpMap Gamma)).
Proof.
intros.
intros range_valid dVars_valid affine_dVars_valid types_valid pre_valid unsat_qs.
unfold RangeValidator in *.
destruct P as [Piv C].
destruct (validIntervalbounds e A Piv dVars) eqn: Hivcheck.
- eapply validIntervalbounds_sound; set_tac; eauto.
unfold eval_precond in *. tauto.
(* unfold dVars_range_valid; intros; set_tac. *)
now destruct pre_valid.
- pose (iexpmap := (FloverMap.empty (affine_form Q))).
pose (inoise := 1%nat).
epose (imap := (fun _ : nat => None)).
fold iexpmap inoise imap in H, H1.
cbn in H. rewrite Hivcheck in H.
fold iexpmap inoise imap in range_valid, affine_dVars_valid.
cbn in range_valid. rewrite Hivcheck in range_valid.
destruct (validAffineBounds e A Piv dVars iexpmap inoise) eqn: Hafcheck.
2: now eapply validSMTIntervalbounds_sound; set_tac; eauto.
clear H.
destruct p as [exprAfs noise].
pose proof (validAffineBounds_sound) as sound_affine.
assert ((forall e' : FloverMap.key,
......@@ -56,10 +54,10 @@ Proof.
assert (1 > 0)%nat as Hinoise by omega.
eassert (forall n : nat, (n >= 1)%nat -> imap n = None) as Himap by trivial.
assert (NatSet.Subset (usedVars e -- dVars) (usedVars e)) as Hsubset by set_tac.
destruct H3 as [Hpre _].
specialize (sound_affine e A Piv (usedVars e) dVars E Gamma
exprAfs noise iexpmap inoise imap
Hchecked Hinoise Himap Hafcheck H1 Hsubset Hpre)
destruct pre_valid as [Hpre _].
specialize (sound_affine e A Piv (usedVars e) dVars E Gamma exprAfs noise iexpmap
inoise imap Hchecked Hinoise Himap Hafcheck
affine_dVars_valid Hsubset Hpre)
as [map2 [af [vR [aiv [aerr sound_affine]]]]]; intuition.
Qed.
......@@ -86,14 +84,13 @@ Theorem RangeValidatorCmd_sound (f : cmd Q) (A : analysisResult) (P : precond)
unsat_queries Qmap ->
validRangesCmd f A E (toRTMap (toRExpMap Gamma)).
Proof.
intros ranges_valid; intros.
intros ranges_valid ssa_valid dVars_valid affine_dVars_valid pre_valid preVars_free ? ? ?.
unfold RangeValidatorCmd in ranges_valid.
destruct P as [Piv C].
destruct (validIntervalboundsCmd f A Piv dVars) eqn:iv_valid.
- eapply validIntervalboundsCmd_sound; eauto.
+ unfold eval_precond in *. tauto.
+ unfold preVars in *. eapply NatSetProps.subset_trans.
apply NatSetProps.union_subset_1. eauto.
- destruct pre_valid. eapply validIntervalboundsCmd_sound; eauto.
revert preVars_free. apply NatSetProps.subset_trans.
unfold preVars. apply NatSetProps.union_subset_1.
- pose (iexpmap := (FloverMap.empty (affine_form Q))).
pose (inoise := 1%nat).
epose (imap := (fun _ : nat => None)).
......@@ -102,6 +99,7 @@ Proof.
destruct (validAffineBoundsCmd f A Piv dVars iexpmap inoise) eqn: Hafcheck.
2: now (eapply validSMTIntervalboundsCmd_sound; eauto).
destruct p as [exprAfs noise].
destruct pre_valid as [pre_valid _].
pose proof (validAffineBoundsCmd_sound) as sound_affine.
assert ((forall e' : FloverMap.key,
(exists af : affine_form Q, FloverMap.find (elt:=affine_form Q) e' iexpmap = Some af) ->
......@@ -111,11 +109,10 @@ Proof.
congruence).
assert (1 > 0)%nat as Hinoise by omega.
eassert (forall n : nat, (n >= 1)%nat -> imap n = None) as Himap by trivial.
specialize (sound_affine f A Piv fVars dVars outVars E Gamma
exprAfs noise iexpmap inoise imap
Hchecked Hinoise Himap Hafcheck H H1 H4)
specialize (sound_affine f A Piv fVars dVars outVars E Gamma exprAfs noise iexpmap
inoise imap Hchecked Hinoise Himap Hafcheck ssa_valid
affine_dVars_valid)
as [map2 [af [vR [aiv [aerr sound_affine]]]]]; intuition.
+ unfold preVars in *. eapply NatSetProps.subset_trans.
apply NatSetProps.union_subset_1. eauto.
+ unfold eval_precond in *. tauto.
revert preVars_free. eapply NatSetProps.subset_trans.
apply NatSetProps.union_subset_1.
Qed.
......@@ -309,9 +309,9 @@ Definition parseIV (input:list Token) :option (intv * list Token) :=
| _ => None
end.
Definition defaultPre : precond := FloverMap.empty intv.
Definition defaultPreIntv : precondIntv := FloverMap.empty intv.
Definition updPre (n:nat) (iv:intv) (P:precond) : precond :=
Definition updPre (n:nat) (iv:intv) (P:precondIntv) : precondIntv :=
FloverMap.add (Var Q n) iv P.
(** Precondition parser:
......@@ -319,7 +319,7 @@ Definition updPre (n:nat) (iv:intv) (P:precond) : precond :=
PRECOND ::= DCOND DVAR DCONST FRACTION FRACTION PRECOND | EPSILON
The beginning of the precondition is marked by the DPRE token
**)
Fixpoint parsePrecondRec (input:list Token) (fuel:nat) :option (precond * list Token) :=
Fixpoint parsePrecondRec (input:list Token) (fuel:nat) :option (precondIntv * list Token) :=
match fuel with
|S fuel' =>
match input with
......@@ -328,7 +328,7 @@ Fixpoint parsePrecondRec (input:list Token) (fuel:nat) :option (precond * list T
| Some (iv, precondRest) =>
match parsePrecondRec precondRest fuel' with
| Some (P, tokRest) => Some (updPre (N.to_nat n) iv P, tokRest)
| None => Some (updPre (N.to_nat n) iv defaultPre, precondRest)
| None => Some (updPre (N.to_nat n) iv defaultPreIntv, precondRest)
end
| _ => None
end
......@@ -337,9 +337,14 @@ Fixpoint parsePrecondRec (input:list Token) (fuel:nat) :option (precond * list T
|_ => None
end.
Definition parsePrecond (input :list Token) fuel :=
Definition parsePrecond (input :list Token) fuel : option (precond * list Token) :=
match input with
| DPRE :: tokRest => parsePrecondRec tokRest fuel
| DPRE :: tokRest =>
match parsePrecondRec tokRest fuel with
(* TODO parse addition constraints *)
| Some (Piv, rest) => Some ((Piv, TrueQ), rest)
| _ => None
end
| _ => None
end.
......
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