aboutsummaryrefslogtreecommitdiff
path: root/src/Specific/IntegrationTestLadderstep130.v
Commit message (Collapse)AuthorAge
* Don't rely on autogenerated namesGravatar Jason Gross2017-06-05
| | | | | | This fixes all of the private-names warnings emitted by compiling fiat-crypto with https://github.com/coq/coq/pull/268 (minus the ones in coqprime, which I didn't touch).
* Inline a24_sig in ladderstepGravatar Jason Gross2017-04-17
| | | | | Update the pipeline to be powerful enough to take advantage of this change by doing more simplification.
* Update display of ladderstep130Gravatar Jason Gross2017-04-14
|
* Use 128/256 in ladderstep 130Gravatar Jason Gross2017-04-14
|
* Add 130-bit 3-register synthesisGravatar Jason Gross2017-04-07
This one has fewer operations, and so will be faster to play with