From b3ccf7046ff2f975c3e6de0c9f2ff0b8799d2a56 Mon Sep 17 00:00:00 2001 From: Joachim Bard Date: Tue, 16 Oct 2018 18:07:41 +0200 Subject: [PATCH] testcase: proving bound by hand; 1 open lemma --- coq/smt_bottom_up.v | 111 ++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 111 insertions(+) create mode 100644 coq/smt_bottom_up.v diff --git a/coq/smt_bottom_up.v b/coq/smt_bottom_up.v new file mode 100644 index 0000000..93ebf31 --- /dev/null +++ b/coq/smt_bottom_up.v @@ -0,0 +1,111 @@ +Require Import Flover.CertificateChecker. +Require Import Flover.SMTArith. +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:precond := fun (n:nat) => +if n =? 0 then ( (-3)#(1), (6)#(1)) else if n =? 1 then ( (2)#(1), (8)#(1)) else (0#1,0#1). + +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 + | _ => EqualsQ (ConstQ (0#1)) (ConstQ (1#1)) (* 0 == 1 *) + end. + +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 e v : + eval_expr E (fun _ => Some REAL) (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. admit. + + apply IHe2. admit. + - inversion H. cbn. constructor. + + apply IHe1. admit. + + apply IHe2. admit. + - inversion H. cbn. constructor. + + apply IHe1. admit. + + apply IHe2. admit. + - inversion H. cbn. constructor; auto. + + apply IHe1. admit. + + apply IHe2. admit. +Admitted. + +Lemma e2_to_smt : e2 = SMTArith2Expr (DivQ (PlusQ (VarQ 0) (VarQ 1)) (VarQ 1)). +Proof. + reflexivity. +Qed. + +Lemma refute_bound E : + fVars_P_sound (usedVars e2) 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. cbn. repeat constructor. + - exact B. + - destruct (P 1%nat) as [v1 [H0 H1]]. now cbn; set_tac. + eapply LessEqQ_eval. 1-2: constructor; eauto. apply H1. + - destruct (P 0%nat) as [v1 [H0 H1]]. now cbn; set_tac. + eapply LessEqQ_eval. 1-2: constructor; eauto. apply H1. + - destruct (P 1%nat) as [v1 [H0 H1]]. now cbn; set_tac. + eapply LessEqQ_eval. 1-2: constructor; eauto. apply H1. + - destruct (P 0%nat) as [v1 [H0 H1]]. now cbn; set_tac. + eapply LessEqQ_eval. 1-2: constructor; eauto. apply H1. +Qed. + +Theorem RangeBound_e2_sound E v : + fVars_P_sound (usedVars e2) E thePrecondition_fnc1 + -> ~ eval_smt_logic E query + -> eval_expr E (fun _ => Some REAL) (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. + eapply LessQ_eval. 3: exact B. constructor. assumption. +Qed. + +Print Assumptions RangeBound_e2_sound. -- GitLab