aboutsummaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
* More WIP on register allocationGravatar Jason Gross2017-08-17
* Handle most of register allocationGravatar Jason Gross2017-08-14
* Handle equality in parsingGravatar Jason Gross2017-08-14
* Fixup header and footerGravatar Jason Gross2017-08-14
* Update scheduler to know about implicit mulx argGravatar Jason Gross2017-08-14
* Use a more realistic processor modelGravatar Jason Gross2017-08-13
* Revert "Revert "Subset compiler differently""Gravatar Jason Gross2017-08-13
* Revert "Subset compiler differently"Gravatar Jason Gross2017-08-13
* Subset compiler differentlyGravatar Jason Gross2017-08-13
* Add heuristic searchGravatar Jason Gross2017-08-13
* Add decidable equality with nilGravatar Jason Gross2017-08-13
* Update the graph makerGravatar Jason Gross2017-08-13
* Update exhaustive search compilerGravatar Jason Gross2017-08-13
* Add memoize.py to zinc compiler folderGravatar Jason Gross2017-08-11
* wip on register allocation in pythonGravatar Jason Gross2017-08-09
* Fix the sense of dependencies in zinc generationGravatar Jason Gross2017-08-09
* Get all scheduling done in one frameGravatar Jason Gross2017-08-09
* Fix wipGravatar Jason Gross2017-08-09
* Larger instruction window for zincGravatar Jason Gross2017-08-09
* Add a faster version of the zinc compilerGravatar Jason Gross2017-08-06
* Add initial stab at C-compilation by optimizationGravatar Jason Gross2017-08-06
* Update crypto-defects.mdGravatar Andres Erbsen2017-07-29
* Factor out some of the preglue synthesis codeGravatar Jason Gross2017-07-08
* Unfold tuple arguments in reflective pipelineGravatar Jason Gross2017-07-08
* Add cbv_runtime in Arithmetic/CoreGravatar Jason Gross2017-07-08
* Make some tactics a bit more powerfulGravatar Jason Gross2017-07-08
* Also test coq v8.7 on travisGravatar Jason Gross2017-07-08
* Fix Demo.vGravatar Jason Gross2017-07-08
* More fine-grained tactics importsGravatar Jason Gross2017-07-08
* More fine-grained importsGravatar Jason Gross2017-07-08
* Add UnfoldArgGravatar Jason Gross2017-07-08
* Update .gitignore with compilation outputsGravatar Jason Gross2017-07-08
* Fix format warning in gccGravatar Jason Gross2017-07-08
* Fix CSE_sym denoteGravatar Jason Gross2017-07-07
* Fix proofs broken by previous commitGravatar Jason Gross2017-07-07
* Stronger contextsGravatar Jason Gross2017-07-07
* README: recommend against Coq 8.5Gravatar Andres Erbsen2017-07-07
* Remove some admitted lemmasGravatar Jason Gross2017-07-07
* enforce use of [F.zero], [F.one]; prove Ed25519 admitsGravatar Andres Erbsen2017-07-07
* prove ModularArithmeticTheorems admitsGravatar Andres Erbsen2017-07-06
* Curves/Edwards/Affine: prove point compression admitsGravatar Andres Erbsen2017-07-06
* prove an admit in ArithmeticSynthesisTestGravatar Andres Erbsen2017-07-06
* make benchGravatar Andres Erbsen2017-07-06
* Don't remove Adam Langley when anonymizing repoGravatar Jason Gross2017-07-06
* make benchGravatar Jason Gross2017-07-06
* Fix a typo that ends up not matteringGravatar Jason Gross2017-07-06
* benchmark NISTZ256 with and without adxGravatar Andres Erbsen2017-07-05
* capture.sh require constant TSCGravatar Andres Erbsen2017-07-05
* s/bash/shGravatar Andres Erbsen2017-07-05
* make benchGravatar Andres Erbsen2017-07-05