aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Expand)AuthorAge
* 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
* Fix nth_default for the tip of v8.6Gravatar Jason Gross2017-04-28
* add nth_default on tupleGravatar jadep2017-04-28
* Add destruct_head'_sumGravatar Jason Gross2017-04-25
* Speed up [specialize_by_assumption]Gravatar Jason Gross2017-04-25
* Add reference to discussionsGravatar Jason Gross2017-04-25
* Add loop invariant framework for for-loopsGravatar Jason Gross2017-04-25
* Add Z2Nat.inj_0 to zsimplify_constGravatar Jason Gross2017-04-24
* More zutil lemmasGravatar Jason Gross2017-04-24
* Add some zutil lemmasGravatar Jason Gross2017-04-24
* use IntegrationTestSquare in C codeGravatar Andres Erbsen2017-04-22
* make displayGravatar Jason Gross2017-04-20
* Update C notationsGravatar Jason Gross2017-04-20
* Don't needlessly extend the context in CSEGravatar Jason Gross2017-04-17
* Also handle initial type in CSEGravatar Jason Gross2017-04-17
* Allow more transformations in pipelineGravatar Jason Gross2017-04-17
* Prove antisymmetry of CSE lebGravatar Jason Gross2017-04-17
* Fix a bad copy/paste of the recent commitGravatar Jason Gross2017-04-17
* Better error messages in case of reify_abs failureGravatar Jason Gross2017-04-17
* Respond to code review commentsGravatar Jason Gross2017-04-17
* Use the for-loop notation in Montgomery.XZGravatar Jason Gross2017-04-17
* Update ladderstep display logsGravatar Jason Gross2017-04-17
* Inline a24_sig in ladderstepGravatar Jason Gross2017-04-17
* Construct a24_sigGravatar Jason Gross2017-04-17
* Add a few more constants to ladderstep 130 displayGravatar Jason Gross2017-04-15
* Add CSE correctness files for Z-specializationGravatar Jason Gross2017-04-15
* Add more constant notationsGravatar Jason Gross2017-04-15
* Also unfold lift3_sigGravatar Jason Gross2017-04-15
* Update notation filesGravatar Jason Gross2017-04-15
* Generalize linearize a bit moreGravatar Jason Gross2017-04-15
* More robust pipelineGravatar Jason Gross2017-04-15
* More powerful inversion_zrangeGravatar Jason Gross2017-04-15
* Add a bit more power to side conditions in reflective_interp rewrite dbGravatar Jason Gross2017-04-15
* Generalize MapCastCorrect a bitGravatar Jason Gross2017-04-15
* Fix hint for SimplifyArithGravatar Jason Gross2017-04-15
* Update display of ladderstep130Gravatar Jason Gross2017-04-14
* Prelinearize so we can simplify more arithmetic in pipelineGravatar Jason Gross2017-04-14
* Better version of linearize without a-normal formGravatar Jason Gross2017-04-14
* Use 128/256 in ladderstep 130Gravatar Jason Gross2017-04-14
* 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
* Add support for cse-modulo-normalizationGravatar Jason Gross2017-04-14
* stronger ladderstep correctness proof courtesy TeoGravatar Andres Erbsen2017-04-14
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-26 18:59:35 +0000