aboutsummaryrefslogtreecommitdiff
path: root/src
Commit message (Expand)AuthorAge
...
* 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
* Account for future changes of #219Gravatar Jason Gross2017-06-22
* src/Demo.v: a 200-line introduction to BaseSystem ideasGravatar Andres Erbsen2017-06-21
* Prove In_to_list_left_tl, In_left_hd, to_list_left_appendGravatar Jason Gross2017-06-21
* Prove some admitted lemmas about uweightGravatar Jason Gross2017-06-21
* compile src/Specific/IntegrationTestMontgomeryP256.sGravatar Andres Erbsen2017-06-21
* Use is_bounded_by_None_repeat_In_iff_lt, remove axiomGravatar Jason Gross2017-06-20
* Add is_bounded_by_None_repeat_In_iff_ltGravatar Jason Gross2017-06-20
* make displayGravatar Jason Gross2017-06-20
* Also key adc->sbb on the carry-bit being negativeGravatar Jason Gross2017-06-20
* Add more simplification passes (de-doubling opp)Gravatar Jason Gross2017-06-20
* make displayGravatar Jason Gross2017-06-20
* Add more simplification passes (de-doubling opp)Gravatar Jason Gross2017-06-20
* make displayGravatar Jason Gross2017-06-20
* Enable a-nf for montgomeryGravatar Jason Gross2017-06-20
* make displayGravatar Jason Gross2017-06-20
* Add more Z-notationsGravatar Jason Gross2017-06-20
* make displayGravatar Jason Gross2017-06-20
* Add another fusion to adc-fusionGravatar Jason Gross2017-06-20
* changed number of limbs partway through conditional_sub; was n, now S nGravatar jadep2017-06-20
* Add fold_left_orb_true, fold_left_orb_pullGravatar Jason Gross2017-06-20
* Use solve_wf_side_condition to synch the depth of auto with wfGravatar Jason Gross2017-06-20
* make displayGravatar Jason Gross2017-06-20
* make display (new conditional_sub)Gravatar Jason Gross2017-06-20
* Make use of new conditional_subtractGravatar Jason Gross2017-06-20
* Remove duplicate [small p] hypothesis from small_conditional_subGravatar Jason Gross2017-06-20
* Add conditional_sub_id to uncps globallyGravatar Jason Gross2017-06-20
* Add more constant notationsGravatar Jason Gross2017-06-20
* Add is_bounded_by_None_repeat_In_iffGravatar Jason Gross2017-06-20
* make benchGravatar Jason Gross2017-06-20
* check in icc-compiled IntegrationTestMontgomeryP256.sGravatar Andres Erbsen2017-06-20
* sed mulx appropriatelyGravatar Andres Erbsen2017-06-20
* defined conditional_sub (see #207) -- small_conditional_sub admitted, eval_co...Gravatar jadep2017-06-20
* rename Columns.sub_cps to make it clear that no balance is addedGravatar jadep2017-06-20
* Don't depend on classical axioms for small_addGravatar Jason Gross2017-06-20
* Make use of new small_addGravatar Jason Gross2017-06-20
* Weaken preconditions on small_addGravatar Jason Gross2017-06-20
* Strip trailing whitespaceGravatar Jason Gross2017-06-20
* Better specs (F-based) for mulmodGravatar Jason Gross2017-06-19
* No small in MP256 spec (wrong place), s/native/vm/Gravatar Jason Gross2017-06-19
* Improve mulmod_256 specsGravatar Jason Gross2017-06-19
* [Require NatUtil] should not change [tauto]Gravatar Jason Gross2017-06-19
* Fix build errorGravatar Jason Gross2017-06-19
* fixed precondition on small_addGravatar jadep2017-06-19
* Add smallness of output to montgomery synthesisGravatar Jason Gross2017-06-19
* make displayGravatar Jason Gross2017-06-18
* Add more constantsGravatar Jason Gross2017-06-18
* mulmod: sig type in terms of equivalence modulo pGravatar Jason Gross2017-06-18
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-28 19:28:55 +0000