aboutsummaryrefslogtreecommitdiff
path: root/src/Experiments/NewPipeline/Toplevel1.v
Commit message (Expand)AuthorAge
* new pipeline: refactor glue, split into more filesGravatar Jason Gross2019-01-05
* from_montgomery{_ => }mod, for consistency with other namingGravatar Jason Gross2018-12-24
* Add eval_freeze_to_bytesmod to push_evalGravatar Jason Gross2018-12-21
* Remove glue admits in Toplevel1Gravatar Jason Gross2018-12-20
* Move fancy rewrites after bounds analysisGravatar Jason Gross2018-12-12
* Base Dead Code Elim on Subst01Gravatar Jason Gross2018-11-15
* Update the post-bounds rewrite rulesGravatar Jason Gross2018-11-11
* Split off all of the arithmetic rules that need bounds infoGravatar Jason Gross2018-11-11
* Fix a bug in 8.7 compilationGravatar Jason Gross2018-10-30
* Refactor/generalize some pipeline definitions/proofsGravatar Jason Gross2018-10-30
* Add placeholder rewrite rules for rewriting after boundsGravatar Jason Gross2018-10-14
* Parameterize rewriter proofs over cast-outside-of-range behaviorGravatar Jason Gross2018-10-11
* Change naming for partitionGravatar jadep2018-09-17
* Finish interp proof of abstract interpretationGravatar Jason Gross2018-09-14
* Improve documentation of binariesGravatar Jason Gross2018-09-11
* Do less reduction in split_in_contextGravatar Jason Gross2018-08-29
* Add Z.land, Z.lor bounds stuff to zutil, also split up ZUtilGravatar Jason Gross2018-08-23
* Move a lemmaGravatar Jason Gross2018-08-13
* Fix a wrong bound computation (on negatives), fix a proofGravatar Jason Gross2018-08-13
* Finish relax interp proofsGravatar Jason Gross2018-08-07
* Fix an issue with the previous commitGravatar Jason Gross2018-08-07
* Start setting up abs-int interp proofsGravatar Jason Gross2018-08-06
* Finish AbsInt Wf proofsGravatar Jason Gross2018-08-04
* Generalize type.eqv a bitGravatar Jason Gross2018-07-30
* Integrate Wf and Interp proofsGravatar Jason Gross2018-07-30
* Move the associator pass to the rewriterGravatar Jason Gross2018-07-26
* Montgomery reduction in new pipelineGravatar Jason Gross2018-07-21
* vm_compute in peel_interp_appGravatar Jason Gross2018-07-18
* Better error message printingGravatar Jason Gross2018-07-12
* Make Z.div_mod_to_quot_rem strongerGravatar Jason Gross2018-07-10
* Remove nested proofsGravatar Jason Gross2018-07-03
* Add support for annotating generated C functions with commentsGravatar Jason Gross2018-07-03
* Synthesize selectznzGravatar Jason Gross2018-07-03
* Allow passing functions to synthesize on the command line, and scmul for 25519Gravatar Jason Gross2018-07-03
* No subst01 in mulmodGravatar Jason Gross2018-07-03
* Start with a better template for carry_squareGravatar Jason Gross2018-07-03
* Don't subst01 in squareGravatar Jason Gross2018-07-03
* synthesize squareGravatar Jason Gross2018-07-03
* WIPGravatar Jason Gross2018-07-03
* Pass around lists of strings for error messagesGravatar Jason Gross2018-06-17
* New pipeline, split among filesGravatar Jason Gross2018-06-17
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-29 19:52:50 +0000