aboutsummaryrefslogtreecommitdiff
path: root/src/Experiments/NewPipeline/Arithmetic.v
Commit message (Expand)AuthorAge
* move src/Experiments/NewPipeline/ to src/Gravatar Andres Erbsen2019-01-09
* Prove that convert_bases partitionsGravatar Jason Gross2019-01-03
* Remove WBW Mont lemmas from push_evalGravatar Jason Gross2018-12-26
* Add eval_* lemmas for WBW Mont Arith operationsGravatar Jason Gross2018-12-26
* from_montgomery{_ => }mod, for consistency with other namingGravatar Jason Gross2018-12-24
* Add correctness in arithmetic for mulx, addcarryx, subborrowxGravatar Jason Gross2018-12-21
* Add eval_freeze_to_bytesmod to push_evalGravatar Jason Gross2018-12-21
* Add length_encode_no_reduce to distr_lengthGravatar Jason Gross2018-12-21
* Add `Proof using` directives in ArithmeticGravatar Jason Gross2018-12-21
* Fix a few minor things in ArithmeticGravatar Jason Gross2018-12-21
* remove unneeded lemma and do some micro-performance-optimization at one stick...Gravatar jadep2018-12-21
* remove proof duplicationGravatar jadep2018-12-21
* fix hints and [Proof using] statements so that proofs go throughGravatar jadep2018-12-21
* prove [small_sub_then_maybe_add]Gravatar jadep2018-12-21
* prove [eval_sub_then_maybe_add]Gravatar jadep2018-12-21
* fix hints and [Proof using] statements so that proofs go throughGravatar jadep2018-12-21
* prove [small_conditional_sub]Gravatar jadep2018-12-21
* prove [eval_conditional_sub]Gravatar jadep2018-12-21
* move weight proofs up above Positional so they can be used to prove eval_drop...Gravatar jadep2018-12-21
* modify a proof because in 8.7 [auto] doesn't solve the goalGravatar jadep2018-12-21
* prove admitGravatar jadep2018-12-21
* prove admitGravatar jadep2018-12-21
* Add uweight_partition_unique, move weight_1 to uweight_1, add Positional.eval...Gravatar Jason Gross2018-12-20
* 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
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-09 12:49:59 +0000