aboutsummaryrefslogtreecommitdiff
path: root/src/Experiments/NewPipeline/Arithmetic.v
Commit message (Expand)AuthorAge
* Prove that to_bytesmod partitionsGravatar Jason Gross2018-07-08
* Shuffle some ZUtil lemmas aroundGravatar Jason Gross2018-07-08
* Factor eval_reduce_square_exact a bit differentlyGravatar Jason Gross2018-07-03
* Fix hints, hopefullyGravatar Jason Gross2018-07-03
* cleanGravatar Jason Gross2018-07-03
* Finish reduce_square proofGravatar Jason Gross2018-07-03
* Try to fix square againGravatar Jason Gross2018-07-03
* Fix a typo, start on proofGravatar Jason Gross2018-07-03
* Fix a reification issueGravatar Jason Gross2018-07-03
* Try a different reduce_squareGravatar Jason Gross2018-07-03
* WIP better squareGravatar Jason Gross2018-07-03
* Add selectGravatar Jason Gross2018-07-03
* Allow passing functions to synthesize on the command line, and scmul for 25519Gravatar Jason Gross2018-07-03
* Pull out *2 in square, don't turn *2 into <<1Gravatar Jason Gross2018-07-03
* Start with a better template for carry_squareGravatar Jason Gross2018-07-03
* WIPGravatar Jason Gross2018-07-03
* Remove useless RequiresGravatar Jason Gross2018-06-28
* Add [freeze] to ArithmeticGravatar Jason Gross2018-06-21
* Add extend_to_length for non-uniform-length add, subGravatar Jason Gross2018-06-19
* Add a comment about subGravatar Jason Gross2018-06-18
* New pipeline, split among filesGravatar Jason Gross2018-06-17
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-29 20:49:24 +0000