aboutsummaryrefslogtreecommitdiff
Commit message (Expand)AuthorAge
* Split off a-normal form from flatteningGravatar Jason Gross2017-04-14
* Remove old versions of wordsize selectionGravatar Jason Gross2017-04-14
* Remove useless importGravatar Jason Gross2017-04-14
* Add CSE specialized to ZGravatar Jason Gross2017-04-14
* lemmas about ladderstep on zeroGravatar Andres Erbsen2017-04-14
* Add base_type_leb_totalGravatar Jason Gross2017-04-14
* Add some CSE propertiesGravatar Jason Gross2017-04-14
* Ask for leb on op codes and base types, not flat typesGravatar Jason Gross2017-04-14
* Unrevert the coq-scripts module againGravatar Jason Gross2017-04-14
* Add support for cse-modulo-normalizationGravatar Jason Gross2017-04-14
* stronger ladderstep correctness proof courtesy TeoGravatar Andres Erbsen2017-04-14
* Add hand-cse'd version of squareGravatar Jason Gross2017-04-14
* Add display of squareGravatar Jason Gross2017-04-14
* Update ladderstep displayGravatar Jason Gross2017-04-14
* Handle new ladderstep and square in dsiplayGravatar Jason Gross2017-04-14
* Add test for squareGravatar Jason Gross2017-04-14
* Add for-loop combinatorGravatar Jason Gross2017-04-14
* Update CSE proof with some help from AdamGravatar Jason Gross2017-04-14
* Clean up ladderstep goal with help from AndresGravatar Jason Gross2017-04-14
* Prove interp correctness of register reassignGravatar Jason Gross2017-04-13
* Add Named.Syntax.InterpGravatar Jason Gross2017-04-13
* X25519: wrap synthesized code in donna-c64, run SUPERCOP benchmarksGravatar Andres Erbsen2017-04-13
* Add lookupb_removeGravatar Jason Gross2017-04-13
* Add lookupb_removeb_sameGravatar Jason Gross2017-04-13
* Add lookupb_remove_not_inGravatar Jason Gross2017-04-13
* Update display logsGravatar Jason Gross2017-04-13
* Update display to not line-wrapGravatar Jason Gross2017-04-13
* Add ContextOnOkGravatar Jason Gross2017-04-13
* Remove dead code in commentsGravatar Jason Gross2017-04-13
* Update ladderstep displayGravatar Jason Gross2017-04-13
* Rewrite the ladderstep goalGravatar Jason Gross2017-04-13
* Handle implications in pipeline glueGravatar Jason Gross2017-04-13
* Add Util.Logic.ImplAndGravatar Jason Gross2017-04-13
* Add eexists_sig_etransitivity_for_rewrite_fun_RGravatar Jason Gross2017-04-13
* Add lift4_sig_sigGravatar Jason Gross2017-04-13
* Add eexists_sig_etransitivity_RGravatar Jason Gross2017-04-13
* Revert "update coq-scripts"Gravatar Jason Gross2017-04-13
* add CVE-2017-3732 to crypto-defects.mdGravatar Andres Erbsen2017-04-12
* update coq-scriptsGravatar Andres Erbsen2017-04-12
* Add commented out proof of equivalence in MxDHGravatar Jason Gross2017-04-12
* Add denoter for symbolic_exprGravatar Jason Gross2017-04-12
* SOp needs to hold the type of the arguments, for denoteGravatar Jason Gross2017-04-12
* Hold types in SFst and SSndGravatar Jason Gross2017-04-12
* More comment on Saturated.v, explaining representation and the [compact] oper...Gravatar jadep2017-04-11
* More WIP on CSE interpGravatar Jason Gross2017-04-11
* Extend cse context when inliningGravatar Jason Gross2017-04-11
* Add initial version of CSE interpGravatar Jason Gross2017-04-11
* Generalize prepend_prefixGravatar Jason Gross2017-04-10
* Fix missing 'by tac' in rewrite_hypGravatar Jason Gross2017-04-10
* Finish CSE_WfGravatar Jason Gross2017-04-10
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-03 00:21:38 +0000