From 1c114dc487d94d72ebf3453611c42b28777d6482 Mon Sep 17 00:00:00 2001 From: Alex Ozdemir Date: Tue, 11 Dec 2018 11:46:38 -0800 Subject: LRAT signature (#2731) * LRAT signature Added an LRAT signature. It is almost entirely side-conditions, but it works. There is also a collection of tests for it. You can run them by invoking ``` lfscc smt.plf sat.plf lrat.plf lrat_test.plf ``` * Update proofs/signatures/lrat.plf per Yoni's suggestion. Co-Authored-By: alex-ozdemir * Responding to Yoni's comments. * Removed unused varaibles Some tests declared `var`s which were unused. Now they don't. --- proofs/signatures/th_bv.plf | 14 -------------- 1 file changed, 14 deletions(-) (limited to 'proofs/signatures/th_bv.plf') diff --git a/proofs/signatures/th_bv.plf b/proofs/signatures/th_bv.plf index 6012e052a..934951a86 100644 --- a/proofs/signatures/th_bv.plf +++ b/proofs/signatures/th_bv.plf @@ -3,20 +3,6 @@ (declare trust-bad (th_holds false)) ; helper stuff -(program mpz_sub ((x mpz) (y mpz)) mpz - (mp_add x (mp_mul (~1) y))) - -(program mp_ispos ((x mpz)) formula - (mp_ifneg x false true)) - -(program mpz_eq ((x mpz) (y mpz)) formula - (mp_ifzero (mpz_sub x y) true false)) - -(program mpz_lt ((x mpz) (y mpz)) formula - (mp_ifneg (mpz_sub x y) true false)) - -(program mpz_lte ((x mpz) (y mpz)) formula - (mp_ifneg (mpz_sub x y) true (mpz_eq x y))) (program mpz_ ((x mpz) (y mpz)) formula (mp_ifzero (mpz_sub x y) true false)) -- cgit v1.2.3