aboutsummaryrefslogtreecommitdiff
path: root/src/Specific
Commit message (Collapse)AuthorAge
* 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
|
* sh portability fixes in "make c"Gravatar Andres Erbsen2017-06-18
|
* remove unused extraction scriptGravatar Andres Erbsen2017-06-18
|
* "make bench", currently just X25519-C64 (closes #185)Gravatar Andres Erbsen2017-06-18
|
* compile X25519 C code from MakefileGravatar Andres Erbsen2017-06-18
|
* make display with new constantsGravatar Jason Gross2017-06-18
|
* make displayGravatar Jason Gross2017-06-18
|
* make displayGravatar Jason Gross2017-06-18
|
* Use uint128_t for 128-bit montgomeryGravatar Jason Gross2017-06-17
|
* make displayGravatar Jason Gross2017-06-17
|
* add 128-bit display fileGravatar Jason Gross2017-06-17
|
* Add 128-bit version of montgomery for testingGravatar Jason Gross2017-06-17
|
* make displayGravatar Jason Gross2017-06-17
| | | | No idea what's going on
* make displayGravatar Jason Gross2017-06-17
|
generated by cgit v1.2.3 (git 2.39.1) at 2024-07-08 14:56:33 +0000