diff options
| author | Alex Ozdemir <aozdemir@hmc.edu> | 2018-12-11 11:46:38 -0800 |
|---|---|---|
| committer | GitHub <noreply@github.com> | 2018-12-11 11:46:38 -0800 |
| commit | 1c114dc487d94d72ebf3453611c42b28777d6482 (patch) | |
| tree | a1d925be3874d86c8442566db4bc6e8b0e02fa9d /proofs/signatures/th_bv.plf | |
| parent | e1dc39321cd4ab29b436025badfb05714f5649b3 (diff) | |
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 <aozdemir@hmc.edu>
* Responding to Yoni's comments.
* Removed unused varaibles
Some tests declared `var`s which were unused.
Now they don't.
Diffstat (limited to 'proofs/signatures/th_bv.plf')
| -rw-r--r-- | proofs/signatures/th_bv.plf | 14 |
1 files changed, 0 insertions, 14 deletions
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)) |