aboutsummaryrefslogtreecommitdiff
path: root/_CoqProject
Commit message (Expand)AuthorAge
* Add experimental loopsGravatar Jason Gross2017-06-02
* Add compiler optimization for add-with-carryGravatar Jason Gross2017-05-17
* Add reflective machinery for adc, zselectGravatar Jason Gross2017-05-17
* Add context_equiv and prove some Proper lemmasGravatar Jason Gross2017-05-16
* Add Named.ExprInversionGravatar Jason Gross2017-05-15
* Add Wf_from_unitGravatar Jason Gross2017-05-15
* Add src/Compilers/Z/Named/DeadCodeEliminationInterp.vGravatar Jason Gross2017-05-15
* Add DeadCodeEliminationInterpGravatar Jason Gross2017-05-15
* Add GetNamesGravatar Jason Gross2017-05-14
* Add Named.CountLetsGravatar Jason Gross2017-05-14
* make update-_CoqProjectGravatar Jason Gross2017-05-14
* Add support for more constantsGravatar Jason Gross2017-05-14
* add wrapper for add_get_carry and proofs for add_get_carry and zselectGravatar jadep2017-05-14
* Add lemma justifying compiler optimization for adcGravatar Jason Gross2017-05-14
* Split off pull_Zmod, push_Zmod from ZUtilGravatar Jason Gross2017-05-13
* Split off more ZUtil thingsGravatar Jason Gross2017-05-13
* Split off more of ZUtilGravatar Jason Gross2017-05-13
* Split off more of ZUtilGravatar Jason Gross2017-05-13
* Split off ZUtil initial hint databasesGravatar Jason Gross2017-05-13
* Split off Proper ZUtil lemmasGravatar Jason Gross2017-05-12
* Split off notation and defs in ZUtilGravatar Jason Gross2017-05-12
* Initial stab at word-by-word montgomeryGravatar Jason Gross2017-05-01
* Prove relationship between `xzladderstep` and M.add (#162)Gravatar Andres Erbsen2017-04-28
* clean elliptic curve proofs, use par: in WeierstrassAffineProofsGravatar Andres Erbsen2017-04-28
* Add loop invariant framework for for-loopsGravatar Jason Gross2017-04-25
* Add CSE correctness files for Z-specializationGravatar Jason Gross2017-04-15
* Remove old versions of wordsize selectionGravatar Jason Gross2017-04-14
* Add CSE specialized to ZGravatar Jason Gross2017-04-14
* Add some CSE propertiesGravatar Jason Gross2017-04-14
* Add test for squareGravatar Jason Gross2017-04-14
* Add for-loop combinatorGravatar Jason Gross2017-04-14
* Prove interp correctness of register reassignGravatar Jason Gross2017-04-13
* Add Util.Logic.ImplAndGravatar Jason Gross2017-04-13
* Add denoter for symbolic_exprGravatar Jason Gross2017-04-12
* Add initial version of CSE interpGravatar Jason Gross2017-04-11
* Finish most of wf for CSEGravatar Jason Gross2017-04-10
* Add AListContext, WeakListContextGravatar Jason Gross2017-04-10
* Split off Compilers.Named.ContextGravatar Jason Gross2017-04-10
* Split off ZUtil.Stabilization, finish IsBoundedBy!Gravatar Jason Gross2017-04-09
* Split up Compilers/Z/Bounds/InterpretationLemmasGravatar Jason Gross2017-04-07
* Parameterize bounds analysis over round_upGravatar Jason Gross2017-04-07
* Add display for ladderstep 130-bitGravatar Jason Gross2017-04-07
* Add 130-bit 3-register synthesisGravatar Jason Gross2017-04-07
* Add Display files and targetsGravatar Jason Gross2017-04-07
* Add IntegrationTestLadderstep.vGravatar Jason Gross2017-04-07
* make update-_CoqProjectGravatar Jason Gross2017-04-07
* Merge branch 'rename-everything'. Closes #14.Gravatar Andres Erbsen2017-04-06
|\
| * rename-everythingGravatar Andres Erbsen2017-04-06
| * remove unused filesGravatar Andres Erbsen2017-04-06
* | Add IntegrationTest for SubGravatar Jason Gross2017-04-06
generated by cgit v1.2.3 (git 2.39.1) at 2024-05-02 10:25:46 +0000