aboutsummaryrefslogtreecommitdiff
path: root/src/Specific/Framework/CurveParametersPackage.v
diff options
context:
space:
mode:
authorGravatar Jason Gross <jgross@mit.edu>2017-10-11 15:47:29 -0400
committerGravatar Jason Gross <jasongross9@gmail.com>2017-10-18 23:01:29 -0400
commit795c30b733163e1a1f05a0c5f5a8c36cc69a0a1d (patch)
tree533ae8bf84a4e9e0f0a75dc65a643033e1cfcbc0 /src/Specific/Framework/CurveParametersPackage.v
parent37f81dd333f42c64f782793ecc19d22a66f233eb (diff)
Reorganize the curve-specific synthesis framework
This brings in most of the changes that I made when figuring out how to integrate montgomery into the framework. The code is a bit slower because the we drop `Print Assumptions` at the bottom of each synthesis problem, to record that things are closed under the global context. If we remove this, we get back the time that we lost with this commit. After | File Name | Before || Change --------------------------------------------------------------------------------------------- 13m10.63s | Total | 11m51.91s || +1m18.71s --------------------------------------------------------------------------------------------- 1m15.83s | Specific/X2555/C128/ladderstep | 1m02.57s || +0m13.25s 1m03.07s | Specific/X25519/C32/femul | 0m54.99s || +0m08.07s 0m36.49s | Specific/X25519/C32/fesquare | 0m27.77s || +0m08.72s 1m08.99s | Specific/X2448/Karatsuba/C64/femul | 1m01.88s || +0m07.10s 0m26.82s | Specific/X25519/C32/freeze | 0m19.81s || +0m07.01s 2m06.29s | Specific/X25519/C64/ladderstep | 2m00.03s || +0m06.26s 0m17.48s | Specific/X25519/C64/femul | 0m10.81s || +0m06.67s 0m14.78s | Specific/X25519/C64/freeze | 0m08.19s || +0m06.58s 0m14.12s | Specific/X25519/C64/fesquare | 0m07.45s || +0m06.66s 1m48.54s | Specific/NISTP256/AMD64/femul | 1m51.58s || -0m03.04s 0m44.50s | Specific/X2448/Karatsuba/C64/Synthesis | 0m43.81s || +0m00.68s 0m31.40s | Specific/X25519/C32/Synthesis | 0m31.02s || +0m00.37s 0m25.72s | Specific/IntegrationTestMontgomeryP256_128 | 0m25.34s || +0m00.37s 0m18.36s | Specific/NISTP256/AMD64/fesub | 0m18.79s || -0m00.42s 0m16.45s | Specific/NISTP256/AMD64/feadd | 0m16.40s || +0m00.05s 0m15.15s | Specific/NISTP256/AMD64/feopp | 0m14.79s || +0m00.36s 0m12.27s | Specific/IntegrationTestMontgomeryP256_128_Sub | 0m11.90s || +0m00.36s 0m12.06s | Specific/IntegrationTestMontgomeryP256_128_Add | 0m11.89s || +0m00.16s 0m10.93s | Specific/IntegrationTestMontgomeryP256_128_Opp | 0m11.39s || -0m00.46s 0m10.12s | Specific/X25519/C64/Synthesis | 0m09.86s || +0m00.25s 0m09.86s | Specific/NISTP256/AMD64/fenz | 0m09.54s || +0m00.32s 0m09.40s | Specific/IntegrationTestMontgomeryP256_128_Nonzero | 0m09.16s || +0m00.24s 0m06.08s | Specific/X2555/C128/Synthesis | 0m05.72s || +0m00.36s 0m01.06s | Specific/Framework/SynthesisFramework | 0m00.98s || +0m00.08s 0m01.05s | Specific/X25519/C32/CurveParameters | 0m01.01s || +0m00.04s 0m00.88s | Specific/Framework/ReificationTypes | 0m00.84s || +0m00.04s N/A | Specific/Framework/ArithmeticSynthesisFramework | 0m00.82s || -0m00.82s 0m00.81s | Specific/Framework/ArithmeticSynthesis/Karatsuba | N/A || +0m00.81s 0m00.79s | Specific/Framework/ArithmeticSynthesis/SquareFromMul | N/A || +0m00.79s 0m00.79s | Specific/Framework/ArithmeticSynthesis/Base | N/A || +0m00.79s 0m00.79s | Specific/Framework/ArithmeticSynthesis/Freeze | N/A || +0m00.79s 0m00.78s | Specific/Framework/ArithmeticSynthesis/BasePackage | N/A || +0m00.78s 0m00.76s | Specific/Framework/IntegrationTestTemporaryMiscCommon | 0m00.78s || -0m00.02s 0m00.74s | Specific/Framework/ArithmeticSynthesis/HelperTactics | N/A || +0m00.74s 0m00.74s | Specific/Framework/ArithmeticSynthesis/KaratsubaPackage | N/A || +0m00.74s 0m00.73s | Specific/Framework/ArithmeticSynthesis/FreezePackage | N/A || +0m00.73s 0m00.72s | Specific/Framework/ReificationTypesPackage | N/A || +0m00.72s 0m00.70s | Specific/Framework/ArithmeticSynthesis/Defaults | N/A || +0m00.70s 0m00.69s | Specific/Framework/ArithmeticSynthesis/LadderstepPackage | N/A || +0m00.69s 0m00.69s | Specific/Framework/ArithmeticSynthesis/DefaultsPackage | N/A || +0m00.69s 0m00.68s | Specific/Framework/ArithmeticSynthesis/Ladderstep | N/A || +0m00.68s N/A | Specific/Framework/LadderstepSynthesisFramework | 0m00.68s || -0m00.68s 0m00.42s | Specific/Framework/IntegrationTestDisplayCommon | 0m00.39s || +0m00.02s 0m00.40s | Specific/X25519/C64/CurveParameters | 0m00.44s || -0m00.03s 0m00.34s | Specific/Framework/IntegrationTestDisplayCommonTactics | 0m00.35s || -0m00.00s 0m00.33s | Specific/X2555/C128/CurveParameters | 0m00.31s || +0m00.02s 0m00.33s | Specific/Framework/CurveParameters | 0m00.31s || +0m00.02s 0m00.33s | Specific/Framework/CurveParametersPackage | N/A || +0m00.33s 0m00.31s | Specific/X2448/Karatsuba/C64/CurveParameters | 0m00.32s || -0m00.01s 0m00.07s | Specific/Framework/Packages | N/A || +0m00.07s
Diffstat (limited to 'src/Specific/Framework/CurveParametersPackage.v')
-rw-r--r--src/Specific/Framework/CurveParametersPackage.v38
1 files changed, 38 insertions, 0 deletions
diff --git a/src/Specific/Framework/CurveParametersPackage.v b/src/Specific/Framework/CurveParametersPackage.v
new file mode 100644
index 000000000..782ccdd22
--- /dev/null
+++ b/src/Specific/Framework/CurveParametersPackage.v
@@ -0,0 +1,38 @@
+(* This file is autogenerated from CurveParameters.v by remake_packages.py *)
+Require Export Crypto.Specific.Framework.CurveParameters.
+Require Import Crypto.Specific.Framework.Packages.
+Require Import Crypto.Util.TagList.
+
+Ltac if_goldilocks pkg tac_true tac_false arg :=
+ let goldilocks := Tag.get pkg TAG.goldilocks in
+ let goldilocks := (eval vm_compute in (goldilocks : bool)) in
+ lazymatch goldilocks with
+ | true => tac_true arg
+ | false => tac_false arg
+ end.
+
+
+Module MakeCurveParametersPackage (PKG : PrePackage).
+ Module Import MakeCurveParametersPackageInternal := MakePackageBase PKG.
+
+ Ltac get_sz _ := get TAG.sz.
+ Notation sz := (ltac:(let v := get_sz () in exact v)) (only parsing).
+ Ltac get_bitwidth _ := get TAG.bitwidth.
+ Notation bitwidth := (ltac:(let v := get_bitwidth () in exact v)) (only parsing).
+ Ltac get_s _ := get TAG.s.
+ Notation s := (ltac:(let v := get_s () in exact v)) (only parsing).
+ Ltac get_c _ := get TAG.c.
+ Notation c := (ltac:(let v := get_c () in exact v)) (only parsing).
+ Ltac get_carry_chains _ := get TAG.carry_chains.
+ Notation carry_chains := (ltac:(let v := get_carry_chains () in exact v)) (only parsing).
+ Ltac get_a24 _ := get TAG.a24.
+ Notation a24 := (ltac:(let v := get_a24 () in exact v)) (only parsing).
+ Ltac get_coef_div_modulus _ := get TAG.coef_div_modulus.
+ Notation coef_div_modulus := (ltac:(let v := get_coef_div_modulus () in exact v)) (only parsing).
+ Ltac get_goldilocks _ := get TAG.goldilocks.
+ Notation goldilocks := (ltac:(let v := get_goldilocks () in exact v)) (only parsing).
+ Ltac get_modinv_fuel _ := get TAG.modinv_fuel.
+ Notation modinv_fuel := (ltac:(let v := get_modinv_fuel () in exact v)) (only parsing).
+ Ltac get_upper_bound_of_exponent _ := get TAG.upper_bound_of_exponent.
+ Notation upper_bound_of_exponent := (ltac:(let v := get_upper_bound_of_exponent () in exact v)) (only parsing).
+End MakeCurveParametersPackage.