aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Expand)AuthorAge
* Fix comment-in-string issuesGravatar Jason Gross2017-06-29
* More C Notations for uin8_t-valued addcarryxGravatar Jason Gross2017-06-29
* Remove a [Check]Gravatar Jason Gross2017-06-29
* Use -std=gnu11 for older versions of gccGravatar Jason Gross2017-06-28
* match C code in Jacobian additionGravatar Andres Erbsen2017-06-27
* p256 compilation and benchmarks with manual kludgesGravatar Andres Erbsen2017-06-27
* proved eval_mod and eval_div (last remaining eval_ admits in Saturated)Gravatar jadep2017-06-27
* More proof fixingGravatar Jason Gross2017-06-26
* Add a comment for nonzero_cpsGravatar Jason Gross2017-06-26
* Fix a broken proofGravatar Jason Gross2017-06-26
* Factor out admitted proof into admitted lemmaGravatar Jason Gross2017-06-26
* Remove an admitGravatar Jason Gross2017-06-26
* make displayGravatar Jason Gross2017-06-26
* Add nonzero synthesisGravatar Jason Gross2017-06-26
* remove unused admit (has been moved to Tuple.v)Gravatar jadep2017-06-26
* indentationGravatar Jason Gross2017-06-25
* Prove map2_zselectGravatar Jason Gross2017-06-25
* Prove map2_appendGravatar Jason Gross2017-06-25
* Allow disabling adc-fusionGravatar Jason Gross2017-06-25
* make display on p256Gravatar Andres Erbsen2017-06-25
* Fixes #219Gravatar jadep2017-06-25
* write and prove Tuple.map2_cpsGravatar jadep2017-06-25
* make displayGravatar Jason Gross2017-06-25
* Convert adc to sbb when doing [0 - x]Gravatar Jason Gross2017-06-25
* Revert "Convert adc to sbb when doing [0 - x]"Gravatar Jason Gross2017-06-25
* Convert adc to sbb when doing [0 - x]Gravatar Jason Gross2017-06-24
* make displayGravatar Jason Gross2017-06-24
* Fix some things not being unfoldedGravatar Jason Gross2017-06-24
* make displayGravatar Jason Gross2017-06-24
* Propogate neg through constant multiplicationGravatar Jason Gross2017-06-24
* Clean up some montgomery wbw instantiation, make displayGravatar Jason Gross2017-06-24
* Remove admitsGravatar Jason Gross2017-06-24
* Fill in axioms for sub_then_maybe_add; this required fiddling with updated ar...Gravatar jadep2017-06-24
* made conditional_add a wrapper, defined and proved sub_then_maybe_addGravatar jadep2017-06-24
* Make a 'conditionals' section in Columns, and move conditional_add thereGravatar jadep2017-06-24
* make benchGravatar Andres Erbsen2017-06-23
* Weierstrass Jacobian mixed additionGravatar Andres Erbsen2017-06-23
* Fix an issue with notationsGravatar Jason Gross2017-06-22
* Add notation for logical orGravatar Jason Gross2017-06-22
* make displayGravatar Jason Gross2017-06-22
* Add (partially admitted) integration tests for add, sub, oppGravatar Jason Gross2017-06-22
* Fix a typo in push_Zmod that was causing loopingGravatar Jason Gross2017-06-22
* P256: Partial work on add, sub, oppGravatar Jason Gross2017-06-22
* Fix an [sz] that shouldn't have been removed in the previous commitGravatar Jason Gross2017-06-22
* P256: Keep around < eval N boundsGravatar Jason Gross2017-06-22
* Add sig_conj_by_impl2Gravatar Jason Gross2017-06-22
* Work around bug #5615 (constr not being updated)Gravatar Jason Gross2017-06-22
* move Specifi p256 files into their own directoryGravatar Andres Erbsen2017-06-22
* Fix some minor naming bugs in sig_assoc tacticsGravatar Jason Gross2017-06-22
* Add tighter bounds to MontgomeryP256{,_128}Gravatar Jason Gross2017-06-22