Commit f3c73937 authored by Joachim Bard's avatar Joachim Bard

testcase: proving bound using new formats (from SMTArith2.v)

parent a876dcb4
Require Import Flover.CertificateChecker.
Require Import Flover.SMTArith2.
Definition x0 :expr Q := Var Q 0.
Definition y1 :expr Q := Var Q 1.
Definition e1 :expr Q := Binop Plus x0 y1.
Definition e2 :expr Q := Binop Div e1 y1.
Definition C34 :expr Q := Const M64 ((17)#(5)).
Definition e5 :expr Q := Binop Plus e2 C34.
Definition Rete5 := Ret e5.
Definition defVars_fnc1 :FloverMap.t mType :=
(FloverMap.add (Var Q 1) (M64) (FloverMap.add (Var Q 0) (M64) (FloverMap.empty mType))).
Definition thePrecondition_fnc1: FloverMap.t intv :=
FloverMap.add x0 ((-3)#(1), (6)#(1)) (FloverMap.add y1 (2#1, 8#1) (FloverMap.empty intv)).
Definition absenv_fnc1 :analysisResult := Eval compute in
FloverMap.add e5 (( (29)#(10), (75821)#(10240)), (31656575032439604176368417020690028172637826983022229834977068248762132258095105)#(4767828205180598627806767057994257910674911537412415567148097160036817151091933841114427031552)) (FloverMap.add C34 (( (17)#(5), (17)#(5)), (17)#(45035996273704960)) (FloverMap.add e2 (( (-1)#(2), (8201)#(2048)), (2879632975312110162723860570159105251222262341380356792653971457)#(529335265084873566077879553980951356026419978008369989458181366086188773933056)) (FloverMap.add y1 (( (2)#(1), (8)#(1)), (1)#(1125899906842624)) (FloverMap.add e1 (( (-1)#(1), (14)#(1)), (126100789566373895)#(40564819207303340847894502572032)) (FloverMap.add y1 (( (2)#(1), (8)#(1)), (1)#(1125899906842624)) (FloverMap.add x0 (( (-3)#(1), (6)#(1)), (3)#(4503599627370496)) (FloverMap.empty (intv * error)))))))).
Definition querymap_fnc1 := Eval compute in
FloverMap.add e5 (nil) (FloverMap.add C34 (nil) (FloverMap.add e2 ((cons (AndQ (LessQ (ConstQ ((8201)#(2048))) (DivQ (PlusQ (VarQ 0) (VarQ 1)) (VarQ 1))) (AndQ (LessEqQ (VarQ 1) (ConstQ ((8)#(1)))) (AndQ (LessEqQ (ConstQ ((-3)#(1))) (VarQ 0)) (AndQ (LessEqQ (ConstQ ((2)#(1))) (VarQ 1)) (LessEqQ (VarQ 0) (ConstQ ((6)#(1)))))))) nil)) (FloverMap.add y1 (nil) (FloverMap.add e1 (nil) (FloverMap.add y1 (nil) (FloverMap.add x0 (nil) (FloverMap.empty (list SMTLogic)))))))).
Require Import Coq.Reals.Reals Coq.QArith.Qreals.
Require Import RealRangeArith.
Require Import Flover.Expressions.
Definition query :=
match FloverMap.find e2 querymap_fnc1 with
| Some (List.cons q _) => q
| _ => TrueQ
end.
(*
Definition prec :=
match query with
| AndQ q1 q2 => q2
| _ => TrueQ
end.
*)
Definition prec :=
AndQ (LessEqQ (ConstQ (-3 # 1)) (VarQ 0))
(AndQ (LessEqQ (VarQ 0) (ConstQ (6 # 1)))
(AndQ (LessEqQ (ConstQ (2 # 1)) (VarQ 1))
(AndQ (LessEqQ (VarQ 1) (ConstQ (8 # 1))) TrueQ))).
Definition bound :=
match query with
| AndQ q1 q2 => q1
| _ => TrueQ
end.
Compute prec.
Lemma prec_bound_correct E :
eval_smt_logic E query <-> eval_smt_logic E (AndQ prec bound).
Proof.
cbn. tauto.
Qed.
Lemma eval_smt_expr E e v :
eval_smt E e v -> eval_expr E (fun _ => Some REAL) (toRExp (SMTArith2Expr e)) v REAL.
Proof with try (right; apply Rabs_R0).
induction 1.
- now constructor.
- rewrite <- (delta_0_deterministic _ REAL 0)... constructor...
- rewrite <- (delta_0_deterministic _ REAL 0)... apply (Unop_neg (m:= REAL)); auto.
- rewrite <- (delta_0_deterministic _ REAL 0)...
apply (Binop_dist (m1:= REAL) (m2:=REAL)); auto... discriminate.
- rewrite <- (delta_0_deterministic _ REAL 0)...
apply (Binop_dist (m1:= REAL) (m2:=REAL)); auto... discriminate.
- rewrite <- (delta_0_deterministic _ REAL 0)...
apply (Binop_dist (m1:= REAL) (m2:=REAL)); auto... discriminate.
- rewrite <- (delta_0_deterministic _ REAL 0)...
apply (Binop_dist (m1:= REAL) (m2:=REAL)); auto...
Qed.
Lemma eval_expr_smt E Gamma e v :
eval_expr E (toRTMap Gamma) (toREval (toRExp (SMTArith2Expr e))) v REAL
-> eval_smt E e v.
Proof.
induction e in v |- *; cbn; intros H.
- inversion H. cbn. constructor.
- inversion H. cbn. constructor; auto.
- inversion H. cbn. constructor. destruct m; try discriminate. auto.
- inversion H. cbn. constructor.
+ apply IHe1. rewrite <- (toRTMap_eval_REAL _ H6). assumption.
+ apply IHe2. rewrite <- (toRTMap_eval_REAL _ H9). assumption.
- inversion H. cbn. constructor.
+ apply IHe1. rewrite <- (toRTMap_eval_REAL _ H6). assumption.
+ apply IHe2. rewrite <- (toRTMap_eval_REAL _ H9). assumption.
- inversion H. cbn. constructor.
+ apply IHe1. rewrite <- (toRTMap_eval_REAL _ H6). assumption.
+ apply IHe2. rewrite <- (toRTMap_eval_REAL _ H9). assumption.
- inversion H. cbn. constructor; auto.
+ apply IHe1. rewrite <- (toRTMap_eval_REAL _ H6). assumption.
+ apply IHe2. rewrite <- (toRTMap_eval_REAL _ H9). assumption.
Qed.
Lemma e2_to_smt : e2 = SMTArith2Expr (DivQ (PlusQ (VarQ 0) (VarQ 1)) (VarQ 1)).
Proof.
reflexivity.
Qed.
Lemma refute_bound E :
eval_precond E thePrecondition_fnc1
-> ~ eval_smt_logic E query
-> ~ eval_smt_logic E (LessQ (ConstQ ((8201)#(2048))) (DivQ (PlusQ (VarQ 0) (VarQ 1)) (VarQ 1))).
Proof.
intros P unsatQ B.
apply unsatQ. apply prec_bound_correct.
constructor.
- eapply checkPre_pre_smt. 2: exact P.
reflexivity.
- exact B.
Qed.
Theorem RangeBound_e2_sound E Gamma v :
eval_precond E thePrecondition_fnc1
-> ~ eval_smt_logic E query
-> eval_expr E (toRTMap Gamma) (toREval (toRExp e2)) v REAL
-> v <= Q2R ((8201)#(2048)).
Proof.
intros Psound unsatQ e2v.
rewrite e2_to_smt in e2v.
apply eval_expr_smt in e2v.
apply Rnot_lt_le. intros B.
eapply refute_bound. 1-2: eassumption.
eexists. exists v. repeat split. constructor. exact e2v. exact B.
Qed.
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