aboutsummaryrefslogtreecommitdiff
path: root/src/Specific/MontgomeryP256_128.v
Commit message (Collapse)AuthorAge
* Factor out some of the preglue synthesis codeGravatar Jason Gross2017-07-08
| | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | | This makes it a bit more uniform, and hopefully more automatable and packageable. Unfortunately, there's still no spec for this part of the pipeline, so the tactics simply aggregate common patterns. Alas, this also makes things a bit slower; I suspect that [Defined] is the place where things are slower. After | File Name | Before || Change --------------------------------------------------------------------------------------- 13m51.14s | Total | 12m59.29s || +0m51.84s --------------------------------------------------------------------------------------- 1m54.18s | Specific/IntegrationTestKaratsubaMul | 1m43.12s || +0m11.06s 1m38.97s | Specific/IntegrationTestLadderstep130 | 1m30.26s || +0m08.70s 2m19.75s | Specific/NISTP256/AMD64/femul | 2m14.08s || +0m05.66s 0m39.90s | Specific/IntegrationTestMontgomeryP256_128 | 0m34.21s || +0m05.68s 0m21.95s | Specific/NISTP256/AMD64/fesub | 0m19.23s || +0m02.71s 0m21.37s | Specific/NISTP256/AMD64/feadd | 0m18.82s || +0m02.55s 0m21.02s | Specific/X25519/C64/femul | 0m18.32s || +0m02.69s 0m20.53s | Specific/IntegrationTestFreeze | 0m23.26s || -0m02.73s 0m18.28s | Specific/IntegrationTestMontgomeryP256_128_Sub | 0m15.32s || +0m02.96s 0m18.20s | Specific/IntegrationTestMontgomeryP256_128_Add | 0m15.52s || +0m02.67s 0m16.35s | Specific/IntegrationTestMontgomeryP256_128_Opp | 0m13.52s || +0m02.83s 0m13.92s | Specific/IntegrationTestMontgomeryP256_128_Nonzero | 0m11.84s || +0m02.08s 0m18.23s | Specific/NISTP256/AMD64/MontgomeryP256 | 0m16.62s || +0m01.60s 0m15.54s | Specific/IntegrationTestSub | 0m14.53s || +0m01.00s 0m14.78s | Specific/X25519/C64/fesquare | 0m13.13s || +0m01.64s 0m13.71s | Specific/NISTP256/AMD64/fenz | 0m12.69s || +0m01.02s 3m14.34s | Specific/X25519/C64/ladderstep | 3m14.32s || +0m00.02s 0m16.54s | Specific/NISTP256/AMD64/feopp | 0m16.48s || +0m00.05s 0m12.21s | Specific/MontgomeryP256_128 | 0m12.70s || -0m00.48s 0m00.73s | Specific/IntegrationTestTemporaryMiscCommon | 0m00.72s || +0m00.01s 0m00.64s | Specific/IntegrationTestDisplayCommon | 0m00.60s || +0m00.04s
* Fix misnamed references in Specific/ (broke after saturated arithetic reorg)Gravatar jadep2017-06-30
|
* Fix unfolding to not unfold sub_with_get_borrow in P256Gravatar Jason Gross2017-06-29
|
* More proof fixingGravatar Jason Gross2017-06-26
|
* Remove an admitGravatar Jason Gross2017-06-26
| | | | This proof should possibly be factored out and go elsewhere.....
* Add nonzero synthesisGravatar Jason Gross2017-06-26
|
* Clean up some montgomery wbw instantiation, make displayGravatar Jason Gross2017-06-24
|
* 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
* 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 tighter bounds to MontgomeryP256{,_128}Gravatar Jason Gross2017-06-22
|
* Make use of new conditional_subtractGravatar Jason Gross2017-06-20
|
* 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
|
* mulmod: sig type in terms of equivalence modulo pGravatar Jason Gross2017-06-18
|
* Don't unfold MulSplitGravatar Jason Gross2017-06-18
| | | | This closes #205
* 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). ```
* Use uint128_t for 128-bit montgomeryGravatar Jason Gross2017-06-17
|
* Add 128-bit version of montgomery for testingGravatar Jason Gross2017-06-17
generated by cgit v1.2.3 (git 2.39.1) at 2024-06-30 14:49:59 +0000