aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Expand)AuthorAge
...
* Add DeadCodeEliminationInterpGravatar Jason Gross2017-05-15
* Add a stronger lemma to registerassigninterpGravatar Jason Gross2017-05-15
* use ladderstep from donna (2% faster?)Gravatar Andres Erbsen2017-05-15
* disable ANormal form, we now support expression output!Gravatar Andres Erbsen2017-05-14
* Add reserved java notationGravatar Jason Gross2017-05-14
* Add a reserved C notationGravatar Jason Gross2017-05-14
* update c.sh for new return notationGravatar Andres Erbsen2017-05-14
* Merge branch 'with-return' of https://github.com/JasonGross/fiat-crypto into ...Gravatar Andres Erbsen2017-05-14
|\
* | Add GetNamesGravatar Jason Gross2017-05-14
* | Add Named.default_names_forGravatar Jason Gross2017-05-14
| * make display (for return statement)Gravatar Jason Gross2017-05-14
| * Stick 'return' at the end of printed functionsGravatar Jason Gross2017-05-14
|/
* make display again (really not sure what's up)Gravatar Jason Gross2017-05-14
* make displayGravatar Jason Gross2017-05-14
* Add Named.CountLetsGravatar Jason Gross2017-05-14
* force carry intermediates to be bound earlyGravatar Andres Erbsen2017-05-14
* make display (ladderstep with specialize square)Gravatar Jason Gross2017-05-14
* Use specialized square in ladderstepGravatar Jason Gross2017-05-14
* Make proj1_sig square_sig take only one argumentGravatar Jason Gross2017-05-14
* Add Z/Named/DeadCodeElimination.vGravatar Jason Gross2017-05-14
* Split off EliminateDeadCodeGravatar Jason Gross2017-05-14
* make display without 0x0 * _Gravatar Jason Gross2017-05-14
* Do more arithmetic simplifyingGravatar Jason Gross2017-05-14
* specialize squaring earlierGravatar Andres Erbsen2017-05-14
* preserve common subexpressions in donna-derived codeGravatar Andres Erbsen2017-05-14
* Add support for more constantsGravatar Jason Gross2017-05-14
* applied micro-optimizations from donna with [transitivity] and [ring] (as per...Gravatar jadep2017-05-14
* Add constant, support pair-returning assignmentGravatar Jason Gross2017-05-14
* More debug info in reificationGravatar Jason Gross2017-05-14
* remove lingering [About]Gravatar jadephilipoom2017-05-14
* remove redundant definitionGravatar jadep2017-05-14
* make freeze use the correct versions of add_get_carry and zselectGravatar jadep2017-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
* Fix notation binding levels so types work in nletGravatar Jason Gross2017-05-14
* Add some reserved notationsGravatar Jason Gross2017-05-14
* Ooops, I mixed up Bind Scope and Delimit ScopeGravatar Jason Gross2017-05-14
* Fix some scopingGravatar Jason Gross2017-05-14
* Allow specifying type in nletGravatar Jason Gross2017-05-14
* Comment out CSE in pipelineGravatar Jason Gross2017-05-14
* CSE without inlining arithmetic expressionsGravatar Jason Gross2017-05-14
* Add Z.div_le_mono_nonnegGravatar Jason Gross2017-05-13
* Add mod_bound_min_maxGravatar Jason Gross2017-05-13
* Add proper lemma for add_with_carryGravatar Jason Gross2017-05-13
* Change definition of add_get_carryGravatar Jason Gross2017-05-13
* Add definitions for zselect and add_get_carryGravatar Jason Gross2017-05-13
* Add flatten_binding_list_SmartVarfMap2_pair_in_generalize2Gravatar Jason Gross2017-05-13
* Support destructuring dlet and sletGravatar Jason Gross2017-05-13
* Add Zdiv_0_r to zsimplifyGravatar Jason Gross2017-05-13
* Split off pull_Zmod, push_Zmod from ZUtilGravatar Jason Gross2017-05-13