Commit 9f02d71b authored by Joachim Bard's avatar Joachim Bard

testcase for new format: (loQ, hiQ)

parent eef0aa07
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 :=
FloverMap.add e2 (FalseQ, (AndQ (AndQ (LessEqQ (VarQ 0) (ConstQ ((6)#(1)))) (AndQ (LessEqQ (VarQ 1) (ConstQ ((8)#(1)))) (AndQ (LessEqQ (ConstQ ((-3)#(1))) (VarQ 0)) (AndQ (LessEqQ (ConstQ ((2)#(1))) (VarQ 1)) TrueQ)))) (AndQ (LessQ (ConstQ ((8201)#(2048))) (DivQ (PlusQ (VarQ 0) (VarQ 1)) (VarQ 1))) TrueQ))) (FloverMap.empty (SMTLogic * SMTLogic)).
Require Import Coq.Reals.Reals Coq.QArith.Qreals.
Require Import RealRangeArith.
Require Import Flover.Expressions.
Definition loQ :=
match FloverMap.find e2 querymap_fnc1 with
| Some (q, _) => q
| _ => FalseQ
end.
Definition hiQ :=
match FloverMap.find e2 querymap_fnc1 with
| Some (_, q) => q
| _ => FalseQ
end.
Definition query := hiQ.
Definition prec :=
match query with
| AndQ q _ => q
| _ => TrueQ
end.
Definition prec_reorder :=
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 _ (AndQ q _) => q
| _ => TrueQ
end.
Lemma prec_bound_correct E :
eval_smt_logic E query <-> eval_smt_logic E (AndQ prec_reorder bound).
Proof.
cbn; tauto.
Qed.
Definition bound_expr :=
match bound with
| LessQ e (ConstQ r) => e
| LessQ (ConstQ r) e => e
| _ => ConstQ (0#1)
end.
Lemma e2_to_smt : e2 = SMTArith2Expr bound_expr.
Proof.
reflexivity.
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 H1 H2 H3.
rewrite e2_to_smt in H3.
eapply (RangeBound_high_sound (preQ:= prec_reorder) H1 _ _ H3).
Unshelve.
- reflexivity.
- intros H. apply H2. apply prec_bound_correct. exact H.
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