aboutsummaryrefslogtreecommitdiff
path: root/src/Experiments/SimplyTypedArithmetic.v
Commit message (Expand)AuthorAge
* remove old pipelineGravatar Andres Erbsen2019-01-09
* Do less reduction in split_in_contextGravatar Jason Gross2018-08-29
* Fix proofs broken by changes to cc_m proofsGravatar Jason Gross2018-08-24
* Add Z.land, Z.lor bounds stuff to zutil, also split up ZUtilGravatar Jason Gross2018-08-23
* Make Z.div_mod_to_quot_rem strongerGravatar Jason Gross2018-07-10
* Shuffle some ZUtil lemmas aroundGravatar Jason Gross2018-07-08
* Minor refactoringGravatar Jason Gross2018-06-13
* fix over-indented lineGravatar Jade Philipoom2018-05-31
* prove prefancy->fancy for barrett special caseGravatar Jade Philipoom2018-05-31
* move around some Lets so that 8.8 doesn't errorGravatar Jade Philipoom2018-05-31
* relocate ok_expr tactics and fix an admit with a silly bounds relaxation hackGravatar Jade Philipoom2018-05-31
* Proved pre-fancy barrett reduction correct (except 1 admit for boundsGravatar Jade Philipoom2018-05-31
* temporary workaround for #352Gravatar Jade Philipoom2018-05-31
* Define machine model, write prefancy->fancy pass, and prove Montgomery code c...Gravatar Jade Philipoom2018-05-31
* [WIP] shifting addsGravatar Jade Philipoom2018-05-31
* change order of additions so that they a) make more sense and b) are more sui...Gravatar Jade Philipoom2018-05-31
* tweak binders so that shifts from base conversion get inlinedGravatar Jade Philipoom2018-05-31
* remove unneeded comment and extra whitespaceGravatar Jade Philipoom2018-05-31
* end-to-end proof for montgomeryGravatar Jade Philipoom2018-05-31
* Proofs for pre-fancy pass (could use cleanup)Gravatar Jade Philipoom2018-05-31
* proofs for straightline pass (with admits for some depth stuff that should be...Gravatar Jade Philipoom2018-05-31
* finish pushing through changes to dummy and factor out identifier matchGravatar Jade Philipoom2018-05-07
* replace dummy_var with dummy_arrow and change style of straightline tests to ...Gravatar Jade Philipoom2018-05-07
* clean up shared notations and constant-rewriting logic for prefancyGravatar Jade Philipoom2018-05-07
* prefancy now works on barrett (modulo add-opp=>sub)Gravatar Jade Philipoom2018-05-07
* Move straightline and prefancy stuff above barrett reductionGravatar Jade Philipoom2018-05-07
* Translating to 'pre-fancy' form now works on MontgomeryGravatar Jade Philipoom2018-05-07
* move depth to a more sensible locationGravatar Jade Philipoom2018-05-07
* Translation to straightline code now works correctly on montgomery256Gravatar Jade Philipoom2018-05-07
* Translation to straightline code (first attempts, mostly working)Gravatar Jade Philipoom2018-05-07
* fix the placement of a dlet to make more senseGravatar Jade Philipoom2018-05-07
* un-hardcode # of reductionsGravatar Jade Philipoom2018-04-30
* print saturated mulmod for p192 on 32-bit, add note about p256Gravatar Jade Philipoom2018-04-30
* fixed too-many-additions problem by fixing number of limbs in from_associationalGravatar Jade Philipoom2018-04-30
* Fix some carry logicGravatar Jade Philipoom2018-04-30
* First stab at generating code for saturated solinas modularGravatar Jade Philipoom2018-04-30
* fix commentGravatar Jade Philipoom2018-04-30
* Fix bounds analysis for saturated ops and remove unneeded commentGravatar Jade Philipoom2018-04-30
* first stab at reifying barrettGravatar Jade Philipoom2018-04-30
* fix definitions of saturated operations to avoid unnecessary work, and make M...Gravatar Jade Philipoom2018-04-30
* tweak definition of flatten to use an index rather than check the length of t...Gravatar Jade Philipoom2018-04-30
* fix the placement of a dlet to make more senseGravatar Jade Philipoom2018-04-30
* In reassocation, don't reassociate additionsGravatar Jason Gross2018-04-26
* Fix a printoutGravatar Jason Gross2018-04-26
* Revert most of "Make reassociation optional"Gravatar Jason Gross2018-04-26
* Make reassociation optionalGravatar Jason Gross2018-04-26
* Compute tight bounds in a different wayGravatar Jason Gross2018-04-26
* Don't introduce extra lambdas and apps in uncurryGravatar Jason Gross2018-04-26
* Add some Positional Hint RewritesGravatar Jason Gross2018-04-26
* pass-through after Jason's reviewGravatar Jade Philipoom2018-04-19
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-11 17:29:04 +0000