aboutsummaryrefslogtreecommitdiff
path: root/src/Experiments/NewPipeline/Arithmetic.v
Commit message (Expand)AuthorAge
* Add Z.land, Z.lor bounds stuff to zutil, also split up ZUtilGravatar Jason Gross2018-08-23
* Add Proof using to arithmetic proofsGravatar Jason Gross2018-08-07
* Montgomery reduction in new pipelineGravatar Jason Gross2018-07-21
* Thunk nat_rect for better perf, list_{rect=>case}Gravatar Jason Gross2018-07-17
* Remove a lemma that's been moved to NatUtilGravatar Jason Gross2018-07-17
* Add a stronger version of eval_reduceGravatar Jason Gross2018-07-14
* Make Z.div_mod_to_quot_rem strongerGravatar Jason Gross2018-07-10
* 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-21 09:11:34 +0000