aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Expand)AuthorAge
...
* | | Skeleton for add/subtract chains (see #222)Gravatar jadep2017-06-29
* | | Add wrappers for subborrow and add_with_get_carry so they work when it is not...Gravatar jadep2017-06-29
| | * make displayGravatar Jason Gross2017-06-29
| | * change notation `_ == _ ? _ : _ ` to `cmovznz(_, _, _)`Gravatar Jason Gross2017-06-29
| |/ |/|
* | 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
| * Fix comment-in-string issuesGravatar Jason Gross2017-06-29
| * make displayGravatar Jason Gross2017-06-29
| * More C Notations for uin8_t-valued addcarryxGravatar Jason Gross2017-06-29
| * Fix the sense of op_{get,with}_carry in SaturatedGravatar Jason Gross2017-06-29
| * Fix unfolding to not unfold sub_with_get_borrow in P256Gravatar Jason Gross2017-06-29
| * Adapt to new arguments of saturated thingsGravatar Jason Gross2017-06-29
| * Fix type signatures of saturated things for WBWGravatar Jason Gross2017-06-29
| * new add/carry chain logic with admitted proofsGravatar jadep2017-06-29
| * Skeleton for add/subtract chains (see #222)Gravatar jadep2017-06-28
| * Add wrappers for subborrow and add_with_get_carry so they work when it is not...Gravatar jadep2017-06-28
|/
* 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