aboutsummaryrefslogtreecommitdiff
path: root/src/Specific
Commit message (Collapse)AuthorAge
...
* More proof fixingGravatar Jason Gross2017-06-26
|
* Remove an admitGravatar Jason Gross2017-06-26
| | | | This proof should possibly be factored out and go elsewhere.....
* make displayGravatar Jason Gross2017-06-26
|
* Add nonzero synthesisGravatar Jason Gross2017-06-26
|
* make display on p256Gravatar Andres Erbsen2017-06-25
|
* make displayGravatar Jason Gross2017-06-25
|
* make displayGravatar Jason Gross2017-06-24
|
* Fix some things not being unfoldedGravatar Jason Gross2017-06-24
|
* make displayGravatar Jason Gross2017-06-24
|
* Clean up some montgomery wbw instantiation, make displayGravatar Jason Gross2017-06-24
|
* Remove admitsGravatar Jason Gross2017-06-24
|
* make benchGravatar Andres Erbsen2017-06-23
|
* Fix an issue with notationsGravatar Jason Gross2017-06-22
| | | | | CNotations breaks writing of Gallina and Ltac `match`. So we need to import it very, very late.
* make displayGravatar Jason Gross2017-06-22
|
* Add (partially admitted) integration tests for add, sub, oppGravatar Jason Gross2017-06-22
|
* P256: Partial work on add, sub, oppGravatar Jason Gross2017-06-22
| | | | Partial work towards #218
* 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
| | | | | | This closes #220 The code before the glue part of the pipeline is getting kind-of ugly...
* Add sig_conj_by_impl2Gravatar 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
|
* compile src/Specific/IntegrationTestMontgomeryP256.sGravatar Andres Erbsen2017-06-21
|
* Use is_bounded_by_None_repeat_In_iff_lt, remove axiomGravatar Jason Gross2017-06-20
| | | | This actually closes #211
* make displayGravatar Jason Gross2017-06-20
|
* make displayGravatar Jason Gross2017-06-20
|
* make displayGravatar Jason Gross2017-06-20
|
* Enable a-nf for montgomeryGravatar Jason Gross2017-06-20
| | | | This fixes adc-fusion, and closes #214.
* make displayGravatar Jason Gross2017-06-20
|
* make displayGravatar 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
|
* make benchGravatar Jason Gross2017-06-20
|
* check in icc-compiled IntegrationTestMontgomeryP256.sGravatar Andres Erbsen2017-06-20
|
* sed mulx appropriatelyGravatar Andres Erbsen2017-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
| | | | The native compiler was giving anomalies on travis.
* Improve mulmod_256 specsGravatar Jason Gross2017-06-19
| | | | Now they talk about F. Pair-programmed with Andres.
* Add smallness of output to montgomery synthesisGravatar Jason Gross2017-06-19
|
* make displayGravatar Jason Gross2017-06-18
|
* mulmod: sig type in terms of equivalence modulo pGravatar Jason Gross2017-06-18
|
* make displayGravatar Jason Gross2017-06-18
| | | | This closes #205
* Don't unfold MulSplitGravatar Jason Gross2017-06-18
| | | | This closes #205
* make displayGravatar Jason Gross2017-06-18
|
* Switch to using uint8_t rather than bool for adcGravatar Jason Gross2017-06-18
| | | | This closes #206
* Update wbw to work with new apiGravatar Jason Gross2017-06-18
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | @jadephilipoom the remaining context to prove is in src/Arithmetic/MontgomeryReduction/WordByWord/Definition.v and src/Arithmetic/MontgomeryReduction/WordByWord/Proofs.v: ```coq Local Notation conditional_subtract_cps := (@drop_high_cps R_numlimbs). (*Axiom conditional_subtract_cps : T (S R_numlimbs) -> forall {cpsT}, (T R_numlimbs -> cpsT) -> cpsT *)(* computes [arg - N] if [R <= arg], and drops high bit *) Axiom conditional_subtract : T (S R_numlimbs) -> T R_numlimbs (* computes [arg - N] if [R <= arg], and drops high bit *). Local Lemma small_add : forall n a b, small a -> small b -> small (@add n a b). Proof. intros; apply Saturated.small_add; auto; try lia. cbv [uweight]. rewrite ?Znat.Nat2Z.inj_succ, ?Z.pow_succ_r by lia. try nia. Admitted. Local Lemma small_add' : forall n a b, small a -> small b -> small (@add' n a b). Proof. intros; apply Saturated.small_add; auto; try lia. cbv [uweight]. rewrite !Znat.Nat2Z.inj_succ, !Z.pow_succ_r by lia. try nia. Admitted. Axiom conditional_subtract_cps_id : forall v cpsT f, @conditional_subtract_cps v cpsT f = f (@conditional_subtract _ v). Axiom small_scmul : forall (n : nat) (a : Z) (v : T n), small v -> 0 <= a < Z.pos r -> 0 <= eval v < R -> small (scmul a v). Axiom eval_conditional_subtract : forall v : T (S R_numlimbs), small v -> 0 <= eval v < eval N + Z.pos R -> eval (conditional_subtract v) = eval v + (if Z.pos R <=? eval v then - eval N else 0). Axiom small_conditional_subtract : forall v : T (S R_numlimbs), small v -> 0 <= eval v < eval N + Z.pos R -> small (conditional_subtract v). ```
* don't key benchmarks on cpu frequencyGravatar Andres Erbsen2017-06-18
|
* measurements.txt depends on scripts that generate itGravatar Andres Erbsen2017-06-18
|
* more sh portability fixes...Gravatar Andres Erbsen2017-06-18
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-04 10:55:11 +0000