diff options
Diffstat (limited to 'proofs/signatures/th_lira.plf')
| -rw-r--r-- | proofs/signatures/th_lira.plf | 43 |
1 files changed, 43 insertions, 0 deletions
diff --git a/proofs/signatures/th_lira.plf b/proofs/signatures/th_lira.plf index 4be9c6015..ab0da8735 100644 --- a/proofs/signatures/th_lira.plf +++ b/proofs/signatures/th_lira.plf @@ -353,3 +353,46 @@ (! is_affy (is_aff y aff_y) (! a (^ (aff_mul_c aff_y x) aff_z) (is_aff (*_Real y (a_real x)) aff_z)))))))) + +;; ========================== ;; +;; Bounds on Affine Functions ;; +;; ========================== ;; + +; Bounds that an affine function might satisfy +(declare bound type) +(declare bound_pos bound) ; > 0 +(declare bound_non_neg bound) ; >= 0 + +; formulas over affine functions +; the statement that `a` satisfies `b` for all inputs +(declare bounded_aff (! a aff (! b bound formula))) + +; Sum of two bounds (the bound satisfied by the sum of two functions satifying +; the input bounds) +(program bound_add ((b bound) (b2 bound)) bound + (match b + (bound_pos bound_pos) + (bound_non_neg b2))) + +; The implication of `a1` satisfying `b` and `a2` satisfying `b2`, obtained by +; summing the inequalities. +(program bounded_aff_add ((a1 aff) (b bound) (a2 aff) (b2 bound)) formula + (bounded_aff (aff_add a1 a2) (bound_add b b2))) + + +; The implication of scaling the inequality of `a1` satisfying `b`. +(program bounded_aff_mul_c ((a1 aff) (b bound) (c mpq)) formula + (match (mpq_ispos c) + (tt (bounded_aff (aff_mul_c a1 c) b)) + (ff (fail formula)))) + +; Does an affine function actuall satisfy a bound, for all inputs? +(program bound_respected ((b bound) (a aff)) bool + (match a + ((aff_cons c combo) + (match combo + (lc_null + (match b + (bound_pos (mpq_ispos c)) + (bound_non_neg (mp_ifneg c ff tt)))) + (default tt))))) |