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/smt.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/smt.plf')
| -rw-r--r-- | proofs/signatures/smt.plf | 16 |
1 files changed, 16 insertions, 0 deletions
diff --git a/proofs/signatures/smt.plf b/proofs/signatures/smt.plf index 06dc16153..57dc5bd1e 100644 --- a/proofs/signatures/smt.plf +++ b/proofs/signatures/smt.plf @@ -439,6 +439,22 @@ (holds C)) (holds (clc (neg v) C)))))))))) +;; Numeric primitives + +(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))) ;; Example: ;; |