-
Notifications
You must be signed in to change notification settings - Fork 2
Commit
This commit does not belong to any branch on this repository, and may belong to a fork outside of the repository.
feat: add more real world tests (#477)
* Add euc / oob / shf / stp examples These examples are not yet complete, however, as they require test traces as well. * Add MMIO example Again, this is not yet complete because we don't have traces for it. * Add real-world traces These are based off the unit tests used for the linea-tracer. This second batch of traces are appended and include traces taken from the replay tests.
- Loading branch information
1 parent
01aa174
commit d1958a1
Showing
24 changed files
with
28,805 additions
and
124 deletions.
There are no files selected for viewing
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Large diffs are not rendered by default.
Oops, something went wrong.
This file was deleted.
Oops, something went wrong.
Empty file.
Large diffs are not rendered by default.
Oops, something went wrong.
File renamed without changes.
Large diffs are not rendered by default.
Oops, something went wrong.
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
Original file line number | Diff line number | Diff line change |
---|---|---|
@@ -0,0 +1,56 @@ | ||
(module euc) | ||
|
||
(defcolumns | ||
(IOMF :binary@prove) | ||
(CT :i8) | ||
(CT_MAX :i8) | ||
(DIVIDEND :i64) | ||
(DIVISOR :i64) | ||
(QUOTIENT :i64) | ||
(REMAINDER :i64) | ||
(CEIL :i64) | ||
(DONE :binary) | ||
(DIVISOR_BYTE :byte@prove) | ||
(QUOTIENT_BYTE :byte@prove) | ||
(REMAINDER_BYTE :byte@prove)) | ||
|
||
(defconst | ||
MMEDIUM 8) | ||
|
||
(module euc) | ||
|
||
(defconst | ||
MAX_INPUT_LENGTH MMEDIUM) | ||
|
||
(defconstraint first-row (:domain {0}) | ||
(vanishes! IOMF)) | ||
|
||
(defconstraint heartbeat () | ||
(if-zero IOMF | ||
(begin (vanishes! DONE) | ||
(vanishes! (next CT))) | ||
(begin (eq! (next IOMF) 1) | ||
(if-zero (- CT_MAX CT) | ||
(begin (eq! DONE 1) | ||
(vanishes! (next CT))) | ||
(begin (vanishes! DONE) | ||
(will-inc! CT 1)))))) | ||
|
||
(defconstraint ctmax () | ||
(eq! (~ (- CT MAX_INPUT_LENGTH)) | ||
1)) | ||
|
||
(defconstraint counter-constancies () | ||
(counter-constancy CT CT_MAX)) | ||
|
||
(defconstraint byte-decomposition () | ||
(begin (byte-decomposition CT DIVISOR DIVISOR_BYTE) | ||
(byte-decomposition CT QUOTIENT QUOTIENT_BYTE) | ||
(byte-decomposition CT REMAINDER REMAINDER_BYTE))) | ||
|
||
(defconstraint result (:guard DONE) | ||
(begin (eq! DIVIDEND | ||
(+ (* DIVISOR QUOTIENT) REMAINDER)) | ||
(if-zero (* DIVIDEND REMAINDER) | ||
(eq! CEIL QUOTIENT) | ||
(eq! CEIL (+ QUOTIENT 1))))) |
Oops, something went wrong.