fiat-crypto - fast, formally verified cryptography

	Commit message (Collapse)	Author	Age
*	Factor out some of the preglue synthesis code	Jason Gross	2017-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)	jadep	2017-06-30
\|
*	P256: Keep around < eval N bounds	Jason Gross	2017-06-22
\| \| \| \| \| \|	This closes #220 The code before the glue part of the pipeline is getting kind-of ugly...
*	Use is_bounded_by_None_repeat_In_iff_lt, remove axiom	Jason Gross	2017-06-20
\| \| \| \|	This actually closes #211
*	Enable a-nf for montgomery	Jason Gross	2017-06-20
\| \| \| \|	This fixes adc-fusion, and closes #214.
*	Better specs (F-based) for mulmod	Jason Gross	2017-06-19
\|
*	mulmod: sig type in terms of equivalence modulo p	Jason Gross	2017-06-18
\|
*	Switch to using uint8_t rather than bool for adc	Jason Gross	2017-06-18
\| \| \| \|	This closes #206
*	Update wbw to work with new api	Jason Gross	2017-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 montgomery	Jason Gross	2017-06-17
\|
*	Add 128-bit version of montgomery for testing	Jason Gross	2017-06-17