From bde056be1c65a77f0f5ca4389edc910b530ed436 Mon Sep 17 00:00:00 2001 From: Alex Ozdemir Date: Sat, 25 Jan 2020 18:59:50 -0800 Subject: [PATCH] Axioms for affine function bounds. Tests. (#3632) * Axioms for affine function bounds. Tests. * Apply suggestions from code review Co-Authored-By: yoni206 * Clarify descriptions of th_lira tests Thanks, Yoni! Co-authored-by: yoni206 --- proofs/signatures/th_lira.plf | 61 +++++- proofs/signatures/th_lira_test.plf | 339 +++++++++++++++++++++++++++++ 2 files changed, 399 insertions(+), 1 deletion(-) create mode 100644 proofs/signatures/th_lira_test.plf diff --git a/proofs/signatures/th_lira.plf b/proofs/signatures/th_lira.plf index ab0da8735..145980b24 100644 --- a/proofs/signatures/th_lira.plf +++ b/proofs/signatures/th_lira.plf @@ -386,7 +386,7 @@ (tt (bounded_aff (aff_mul_c a1 c) b)) (ff (fail formula)))) -; Does an affine function actuall satisfy a bound, for all inputs? +; Does an affine function actuall satisfy a bound, for some input? (program bound_respected ((b bound) (a aff)) bool (match a ((aff_cons c combo) @@ -396,3 +396,62 @@ (bound_pos (mpq_ispos c)) (bound_non_neg (mp_ifneg c ff tt)))) (default tt))))) + +;; =================================== ;; +;; Axioms for bounded affine functions ;; +;; =================================== ;; + +; Always true (used as a initial value when summing many bounds together) +(declare bounded_aff_ax_0_>=_0 + (th_holds (bounded_aff (aff_cons 0/1 lc_null) bound_non_neg))) + +; Contradiction axiom: an affine function that does not respect its bounds +(declare bounded_aff_contra + (! a aff ; Omit + (! b bound ; Omit + (! pf (th_holds (bounded_aff a b)) + (! sc (^ (bound_respected b a) ff) + (th_holds false)))))) + +; Rule for summing two affine bounds to get a third +(declare bounded_aff_add + (! a1 aff ; Omit + (! a2 aff ; Omit + (! b bound ; Omit + (! b2 bound ; Omit + (! ba_sum formula ; Omit + (! pf_a1 (th_holds (bounded_aff a1 b)) + (! pf_a2 (th_holds (bounded_aff a2 b2)) + (! sc (^ (bounded_aff_add a1 b a2 b2) ba_sum) + (th_holds ba_sum)))))))))) + +; Rule for scaling an affine bound +(declare bounded_aff_mul_c + (! a aff ; Omit + (! b bound ; Omit + (! ba formula ; Omit + (! c mpq + (! pf_a (th_holds (bounded_aff a b)) + (! sc (^ (bounded_aff_mul_c a b c) ba) + (th_holds ba)))))))) + + +; [y >= x] implies that the aff. function y - x is >= 0 +(declare aff_>=_from_term + (! y (term Real) ; Omit + (! x (term Real) ; Omit + (! p aff ; Omit + (! pf_affine (is_aff (-_Real y x) p) + (! pf_term_bound (th_holds (>=_Real y x)) + (th_holds (bounded_aff p bound_non_neg)))))))) + +; not [y >= x] implies that the aff. function -(y - x) is > 0 +(declare aff_>_from_term + (! y (term Real) ; Omit + (! x (term Real) ; Omit + (! p aff ; Omit + (! p_n aff ; Omit + (! pf_affine (is_aff (-_Real y x) p) + (! pf_term_bound (th_holds (not (>=_Real y x))) + (! sc_neg (^ (aff_neg p) p_n) + (th_holds (bounded_aff p_n bound_pos)))))))))) diff --git a/proofs/signatures/th_lira_test.plf b/proofs/signatures/th_lira_test.plf new file mode 100644 index 000000000..9b041e0c5 --- /dev/null +++ b/proofs/signatures/th_lira_test.plf @@ -0,0 +1,339 @@ +; Depends On: th_lira.plf +;; Proof (from predicates on linear polynomials) that the following imply bottom +; +; -x - 1/2 y + 2 >= 0 +; x + y - 8 >= 0 +; x - y + 0 >= 0 +; +(check + ; Variables + (% x real_var + (% y real_var + ; linear combinations + (@ m1 (lc_cons (~ 1/1) (av_from_real x) (lc_cons (~ 1/2) (av_from_real y) lc_null)) + (@ m2 (lc_cons 1/1 (av_from_real x) (lc_cons 1/1 (av_from_real y) lc_null)) + (@ m3 (lc_cons 1/1 (av_from_real x) (lc_cons (~ 1/1) (av_from_real y) lc_null)) + ; affine functions + (@ p1 (aff_cons 2/1 m1) + (@ p2 (aff_cons (~ 8/1) m2) + (@ p3 (aff_cons 0/1 m3) + ; Proofs of affine bounds + (% pf_nonneg_1 (th_holds (bounded_aff p1 bound_non_neg)) + (% pf_nonneg_2 (th_holds (bounded_aff p2 bound_non_neg)) + (% pf_nonneg_3 (th_holds (bounded_aff p3 bound_non_neg)) + (: + (th_holds false) + (bounded_aff_contra _ _ + (bounded_aff_add _ _ _ _ _ + (bounded_aff_mul_c _ _ _ 4/1 pf_nonneg_1) + (bounded_aff_add _ _ _ _ _ + (bounded_aff_mul_c _ _ _ 3/1 pf_nonneg_2) + (bounded_aff_add _ _ _ _ _ + (bounded_aff_mul_c _ _ _ 1/1 pf_nonneg_3) + bounded_aff_ax_0_>=_0))))) + ))))) + )))) + )) +) + +;; Proof (from predicates on real terms) that the following imply bottom +; +; -x - 1/2 y >= 2 +; x + y >= 8 +; x - y >= 0 +; +(check + ; Declarations + ; Variables + (% x real_var + (% y real_var + ; real predicates + (@ f1 (>=_Real (+_Real (*_Real (a_real (~ 1/1)) (term_real_var x)) (*_Real (a_real (~ 1/2)) (term_real_var y))) (a_real (~ 2/1))) + (@ f2 (>=_Real (+_Real (*_Real (a_real 1/1) (term_real_var x)) (*_Real (a_real 1/1) (term_real_var y))) (a_real 8/1)) + (@ f3 (>=_Real (+_Real (*_Real (a_real 1/1) (term_real_var x)) (*_Real (a_real (~ 1/1)) (term_real_var y))) (a_real 0/1)) + ; proof of real predicates + (% pf_f1 (th_holds f1) + (% pf_f2 (th_holds f2) + (% pf_f3 (th_holds f3) + + + ; Normalization + ; real term -> linear polynomial normalization witnesses + (@ n1 (aff_>=_from_term _ _ _ + (is_aff_- _ _ _ _ _ + (is_aff_+ _ _ _ _ _ + (is_aff_mul_c_L _ _ _ (~ 1/1) (is_aff_var_real x)) + (is_aff_mul_c_L _ _ _ (~ 1/2) (is_aff_var_real y))) + (is_aff_const (~ 2/1))) + pf_f1) + (@ n2 (aff_>=_from_term _ _ _ + (is_aff_- _ _ _ _ _ + (is_aff_+ _ _ _ _ _ + (is_aff_mul_c_L _ _ _ 1/1 (is_aff_var_real x)) + (is_aff_mul_c_L _ _ _ 1/1 (is_aff_var_real y))) + (is_aff_const 8/1)) + pf_f2) + (@ n3 (aff_>=_from_term _ _ _ + (is_aff_- _ _ _ _ _ + (is_aff_+ _ _ _ _ _ + (is_aff_mul_c_L _ _ _ 1/1 (is_aff_var_real x)) + (is_aff_mul_c_L _ _ _ (~ 1/1) (is_aff_var_real y))) + (is_aff_const 0/1)) + pf_f3) + + ; derivation of a contradiction using farkas coefficients + (: + (th_holds false) + (bounded_aff_contra _ _ + (bounded_aff_add _ _ _ _ _ + (bounded_aff_mul_c _ _ _ 4/1 n1) + (bounded_aff_add _ _ _ _ _ + (bounded_aff_mul_c _ _ _ 3/1 n2) + (bounded_aff_add _ _ _ _ _ + (bounded_aff_mul_c _ _ _ 1/1 n3) + bounded_aff_ax_0_>=_0))))) + ))) + ))) + ))) + )) +) + +;; Term proof, 2 premises of the form (>=), one of the form (not >=) +;; Proof (from predicates on real terms) that the following imply bottom +; +; -x + y >= 2 +; x + y >= 2 +; not[ y >= -2] => [y < -2] => [-y > 2] +; +(check + ; Declarations + ; Variables + (% x real_var + (% y real_var + ; real predicates + (@ f1 (>=_Real + (+_Real (*_Real (a_real (~ 1/1)) (term_real_var x)) (term_real_var y)) + (a_real 2/1)) + (@ f2 (>=_Real + (+_Real (term_real_var x) (term_real_var y)) + (a_real 2/1)) + (@ f3 (not (>=_Real (term_real_var y) (a_real (~ 2/1)))) + + ; Normalization + ; proof of real predicates + (% pf_f1 (th_holds f1) + (% pf_f2 (th_holds f2) + (% pf_f3 (th_holds f3) + ; real term -> linear polynomial normalization witnesses + (@ n1 (aff_>=_from_term _ _ _ + (is_aff_- _ _ _ _ _ + (is_aff_+ _ _ _ _ _ + (is_aff_mul_c_L _ _ _ (~ 1/1) (is_aff_var_real x)) + (is_aff_var_real y)) + (is_aff_const 2/1)) + pf_f1) + (@ n2 (aff_>=_from_term _ _ _ + (is_aff_- _ _ _ _ _ + (is_aff_+ _ _ _ _ _ + (is_aff_var_real x) + (is_aff_var_real y)) + (is_aff_const 2/1)) + pf_f2) + (@ n3 (aff_>_from_term _ _ _ _ + (is_aff_- _ _ _ _ _ + (is_aff_var_real y) + (is_aff_const (~ 2/1))) + pf_f3) + + ; derivation of a contradiction using farkas coefficients + (: + (th_holds false) + (bounded_aff_contra _ _ + (bounded_aff_add _ _ _ _ _ + (bounded_aff_mul_c _ _ _ 1/1 n1) + (bounded_aff_add _ _ _ _ _ + (bounded_aff_mul_c _ _ _ 1/1 n2) + (bounded_aff_add _ _ _ _ _ + (bounded_aff_mul_c _ _ _ 2/1 n3) + bounded_aff_ax_0_>=_0))))) + ))) + ))) + ))) + )) +) + +;; Term proof, 2 premises of the form (>=), one of the form (not >=) +;; x is a real, +;; y is an integer +;; Proof (from predicates on real terms) that the following imply bottom +; +; -x + y >= 2 +; x + y >= 2 +; not[ y >= -2] => [y < -2] => [-y > 2] +; +(check + ; Declarations + ; Variables + (% x real_var + (% y int_var + ; real predicates + (@ f1 (>=_Real + (+_Real (*_Real (a_real (~ 1/1)) (term_real_var x)) (term_int_to_real (term_int_var y))) + (a_real 2/1)) + (@ f2 (>=_Real + (+_Real (term_real_var x) (term_int_to_real (term_int_var y))) + (a_real 2/1)) + (@ f3 (not (>=_IntReal (term_int_var y) (a_real (~ 2/1)))) + + ; Normalization + ; proof of real predicates + (% pf_f1 (th_holds f1) + (% pf_f2 (th_holds f2) + (% pf_f3 (th_holds f3) + ; real term -> linear polynomial normalization witnesses + (@ n1 (aff_>=_from_term _ _ _ + (is_aff_- _ _ _ _ _ + (is_aff_+ _ _ _ _ _ + (is_aff_mul_c_L _ _ _ (~ 1/1) (is_aff_var_real x)) + (is_aff_var_int y)) + (is_aff_const 2/1)) + (pf_reified_arith_pred _ _ pf_f1)) + (@ n2 (aff_>=_from_term _ _ _ + (is_aff_- _ _ _ _ _ + (is_aff_+ _ _ _ _ _ + (is_aff_var_real x) + (is_aff_var_int y)) + (is_aff_const 2/1)) + (pf_reified_arith_pred _ _ pf_f2)) + (@ n3 (aff_>_from_term _ _ _ _ + (is_aff_- _ _ _ _ _ + (is_aff_var_int y) + (is_aff_const (~ 2/1))) + (pf_reified_arith_pred _ _ pf_f3)) + + ; derivation of a contradiction using farkas coefficients + (: + (th_holds false) + (bounded_aff_contra _ _ + (bounded_aff_add _ _ _ _ _ + (bounded_aff_mul_c _ _ _ 1/1 n1) + (bounded_aff_add _ _ _ _ _ + (bounded_aff_mul_c _ _ _ 1/1 n2) + (bounded_aff_add _ _ _ _ _ + (bounded_aff_mul_c _ _ _ 2/1 n3) + bounded_aff_ax_0_>=_0))))) + ))) + ))) + ))) + )) +) + +;; Term proof, 2 premises of the form (>=), one of the form (not >=) +;; x is a real, +;; y is an integer, and needs tightening +;; Proof (from predicates on real terms) that the following imply bottom +; +; -x >= -1/2 +; x + y >= 0 +; not[ y >= 0] => [y < 0] => [-y >= 1] +; +(check + ; Declarations + ; Variables + (% x real_var + (% y int_var + ; real predicates + (@ f1 (>=_Real + (*_Real (a_real (~ 1/1)) (term_real_var x)) + (a_real (~ 1/2))) + (@ f2 (>=_Real + (+_Real (term_real_var x) (term_int_to_real (term_int_var y))) + (a_real 0/1)) + (@ f3 (not (>=_IntReal (*_Int (a_int 1) (term_int_var y)) (a_real 0/1))) + + ; Normalization + ; proof of real predicates + (% pf_f1 (th_holds f1) + (% pf_f2 (th_holds f2) + (% pf_f3 (th_holds f3) + ; real term -> linear polynomial normalization witnesses + (@ n1 (aff_>=_from_term _ _ _ + (is_aff_- _ _ _ _ _ + (is_aff_mul_c_L _ _ _ (~ 1/1) (is_aff_var_real x)) + (is_aff_const (~ 1/2))) + (pf_reified_arith_pred _ _ pf_f1)) + (@ n2 (aff_>=_from_term _ _ _ + (is_aff_- _ _ _ _ _ + (is_aff_+ _ _ _ _ _ + (is_aff_var_real x) + (is_aff_var_int y)) + (is_aff_const 0/1)) + (pf_reified_arith_pred _ _ pf_f2)) + (@ n3 (aff_>=_from_term _ _ _ + (is_aff_- _ _ _ _ _ + (is_aff_mul_c_L _ _ _ (~ 1/1) (is_aff_var_int y)) + (is_aff_const 1/1)) + (pf_reified_arith_pred _ _ + (tighten_not_>=_IntReal _ _ _ _ (check_neg_of_greatest_integer_below 1 0/1) pf_f3))) + + ; derivation of a contradiction using farkas coefficients + (: + (th_holds false) + (bounded_aff_contra _ _ + (bounded_aff_add _ _ _ _ _ + (bounded_aff_mul_c _ _ _ 1/1 n1) + (bounded_aff_add _ _ _ _ _ + (bounded_aff_mul_c _ _ _ 1/1 n2) + (bounded_aff_add _ _ _ _ _ + (bounded_aff_mul_c _ _ _ 1/1 n3) + bounded_aff_ax_0_>=_0))))) + ))) + ))) + ))) + )) +) + +;; Term proof, with integer y, that needs to be strictly and non-strictly tightened. +;; Proof (from predicates on real terms) that the following imply bottom +; y >= 1/2 => y >= 1 +; not[ y >= 0] => [y < 0] => [-y >= 1] +; +(check + ; Declarations + ; Variables + (% y int_var + ; real predicates + (@ f1 (>=_IntReal (*_Int (a_int 1) (term_int_var y)) (a_real 1/2)) + (@ f2 (not (>=_IntReal (*_Int (a_int 1) (term_int_var y)) (a_real 0/1))) + + ; Normalization + ; proof of real predicates + (% pf_f1 (th_holds f1) + (% pf_f2 (th_holds f2) + ; real term -> linear polynomial normalization witnesses + (@ n1 (aff_>=_from_term _ _ _ + (is_aff_- _ _ _ _ _ + (is_aff_mul_c_L _ _ _ 1/1 (is_aff_var_int y)) + (is_aff_const 1/1)) + (pf_reified_arith_pred _ _ + (tighten_>=_IntReal _ _ 1 pf_f1))) + (@ n2 (aff_>=_from_term _ _ _ + (is_aff_- _ _ _ _ _ + (is_aff_mul_c_L _ _ _ (~ 1/1) (is_aff_var_int y)) + (is_aff_const 1/1)) + (pf_reified_arith_pred _ _ + (tighten_not_>=_IntReal _ _ _ _ (check_neg_of_greatest_integer_below 1 0/1) pf_f2))) + + ; derivation of a contradiction using farkas coefficients + (: + (th_holds false) + (bounded_aff_contra _ _ + (bounded_aff_add _ _ _ _ _ + (bounded_aff_mul_c _ _ _ 1/1 n1) + (bounded_aff_add _ _ _ _ _ + (bounded_aff_mul_c _ _ _ 1/1 n2) + bounded_aff_ax_0_>=_0))) + ))) + ))) + )) +) -- 2.30.2