aboutsummaryrefslogtreecommitdiff
path: root/src/Experiments/NewPipeline/Arithmetic.v
Commit message (Expand)AuthorAge
* Fix the s-adjustment for saturated solinasGravatar Jason Gross2018-11-06
* Revert "Factor out a common computation to fix n² behavior"Gravatar Jason Gross2018-11-06
* Factor out a common computation to fix n² behaviorGravatar Jason Gross2018-11-06
* Use a better strategy in Rows.sat_reduceGravatar Jason Gross2018-11-06
* Compatibility with coq PR #8457Gravatar Frédéric Besson2018-09-25
* remove unneeded proofGravatar jadep2018-09-17
* redo all Rows correctness proofs using partition and sanity, remove now-unuse...Gravatar jadep2018-09-17
* remove now-unused nth_default hintsGravatar jadep2018-09-17
* fix up flatten partitioning proofs so that they don't use nth_defaultGravatar jadep2018-09-17
* remove commented-out code that is now clearly unneededGravatar jadep2018-09-17
* re-fix syntax so it works on older Coq versionsGravatar jadep2018-09-17
* prove small_div axiomGravatar jadep2018-09-17
* prove eval_mod axiom and clean up eval_div proofGravatar jadep2018-09-17
* use recursive partition to prove eval_div axiomGravatar jadep2018-09-17
* add a recursive definition of partition and prove it equivalentGravatar jadep2018-09-17
* move partition and its proofs to a new module and use it for correctness of C...Gravatar jadep2018-09-17
* change deprecated 'Focus 2' to '2:'Gravatar jadep2018-09-17
* 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-07-04 13:10:23 +0000