diff options
author | Jason Gross <jgross@mit.edu> | 2017-10-11 17:42:15 -0400 |
---|---|---|
committer | Jason Gross <jasongross9@gmail.com> | 2017-10-18 23:01:29 -0400 |
commit | 0fa367733f893d122bab99d3d0137da742c862f5 (patch) | |
tree | d9a1871bc12b82690c2c3cb9248cfea03214a357 /src/Specific/X2448/Karatsuba | |
parent | 73eb1fdc26d5e842c4e7cca28a10cea88d58958d (diff) |
Turn CurveParameters into a record
This is a first step towards removing module functors from the code
generation
After | File Name | Before || Change
---------------------------------------------------------------------------------------------
13m12.84s | Total | 13m13.24s || -0m00.39s
---------------------------------------------------------------------------------------------
2m09.48s | Specific/X25519/C64/ladderstep | 2m03.07s || +0m06.40s
1m08.48s | Specific/X2448/Karatsuba/C64/femul | 1m12.93s || -0m04.45s
1m33.58s | Specific/NISTP256/AMD64/femul | 1m30.93s || +0m02.64s
1m06.71s | Specific/X2555/C128/ladderstep | 1m09.55s || -0m02.84s
0m35.01s | Specific/X25519/C32/fesquare | 0m36.58s || -0m01.57s
1m02.68s | Specific/X25519/C32/femul | 1m02.39s || +0m00.28s
0m44.51s | Specific/X2448/Karatsuba/C64/Synthesis | 0m44.29s || +0m00.21s
0m31.30s | Specific/X25519/C32/Synthesis | 0m31.17s || +0m00.12s
0m26.73s | Specific/X25519/C32/freeze | 0m27.38s || -0m00.64s
0m22.81s | Specific/NISTP256/AMD128/femul | 0m23.28s || -0m00.47s
0m20.30s | Specific/NISTP256/AMD64/fesub | 0m20.02s || +0m00.28s
0m17.76s | Specific/NISTP256/AMD64/feadd | 0m17.70s || +0m00.06s
0m17.04s | Specific/X25519/C64/femul | 0m17.51s || -0m00.47s
0m15.18s | Specific/X25519/C64/freeze | 0m14.93s || +0m00.25s
0m15.14s | Specific/NISTP256/AMD64/feopp | 0m15.32s || -0m00.17s
0m14.72s | Specific/NISTP256/AMD64/fenz | 0m14.68s || +0m00.04s
0m14.50s | Specific/X25519/C64/fesquare | 0m14.54s || -0m00.03s
0m14.26s | Specific/NISTP256/AMD128/feadd | 0m14.48s || -0m00.22s
0m14.21s | Specific/NISTP256/AMD128/fesub | 0m14.43s || -0m00.21s
0m14.10s | Specific/NISTP256/AMD128/fenz | 0m14.07s || +0m00.02s
0m11.67s | Specific/NISTP256/AMD128/feopp | 0m11.67s || +0m00.00s
0m10.12s | Specific/X25519/C64/Synthesis | 0m10.42s || -0m00.30s
0m08.53s | Specific/NISTP256/AMD64/Synthesis | 0m08.44s || +0m00.08s
0m06.44s | Specific/X2555/C128/Synthesis | 0m06.30s || +0m00.14s
0m03.65s | Specific/NISTP256/AMD128/Synthesis | 0m03.60s || +0m00.04s
0m01.00s | Specific/X25519/C32/CurveParameters | 0m01.07s || -0m00.07s
0m00.98s | Specific/Framework/SynthesisFramework | 0m01.00s || -0m00.02s
0m00.80s | Specific/Framework/ArithmeticSynthesis/Freeze | 0m00.73s || +0m00.07s
0m00.79s | Specific/Framework/ArithmeticSynthesis/Defaults | 0m00.74s || +0m00.05s
0m00.78s | Specific/Framework/ArithmeticSynthesis/Karatsuba | 0m00.79s || -0m00.01s
0m00.75s | Specific/Framework/ArithmeticSynthesis/MontgomeryPackage | 0m00.71s || +0m00.04s
0m00.74s | Specific/Framework/ArithmeticSynthesis/Base | 0m00.77s || -0m00.03s
0m00.73s | Specific/Framework/ArithmeticSynthesis/FreezePackage | 0m00.69s || +0m00.04s
0m00.73s | Specific/Framework/MontgomeryReificationTypesPackage | 0m00.70s || +0m00.03s
0m00.72s | Specific/Framework/ReificationTypesPackage | 0m00.75s || -0m00.03s
0m00.70s | Specific/Framework/ArithmeticSynthesis/KaratsubaPackage | 0m00.70s || +0m00.00s
0m00.69s | Specific/Framework/ArithmeticSynthesis/DefaultsPackage | 0m00.70s || -0m00.01s
0m00.68s | Specific/Framework/ArithmeticSynthesis/SquareFromMul | 0m00.72s || -0m00.03s
0m00.66s | Specific/Framework/ArithmeticSynthesis/LadderstepPackage | 0m00.69s || -0m00.02s
0m00.65s | Specific/Framework/ArithmeticSynthesis/BasePackage | 0m00.66s || -0m00.01s
0m00.43s | Specific/X25519/C64/CurveParameters | 0m00.39s || +0m00.03s
0m00.34s | Specific/Framework/CurveParameters | 0m00.29s || +0m00.05s
0m00.32s | Specific/X2555/C128/CurveParameters | 0m00.30s || +0m00.02s
0m00.30s | Specific/NISTP256/AMD128/CurveParameters | 0m00.28s || +0m00.01s
0m00.30s | Specific/X2448/Karatsuba/C64/CurveParameters | 0m00.31s || -0m00.01s
0m00.30s | Specific/Framework/CurveParametersPackage | 0m00.29s || +0m00.01s
0m00.29s | Specific/NISTP256/AMD64/CurveParameters | 0m00.29s || +0m00.00s
0m00.26s | Specific/Framework/RawCurveParameters | N/A || +0m00.26s
Diffstat (limited to 'src/Specific/X2448/Karatsuba')
-rw-r--r-- | src/Specific/X2448/Karatsuba/C64/CurveParameters.v | 44 | ||||
-rw-r--r-- | src/Specific/X2448/Karatsuba/C64/Synthesis.v | 6 |
2 files changed, 24 insertions, 26 deletions
diff --git a/src/Specific/X2448/Karatsuba/C64/CurveParameters.v b/src/Specific/X2448/Karatsuba/C64/CurveParameters.v index cc8393d9b..7302294b8 100644 --- a/src/Specific/X2448/Karatsuba/C64/CurveParameters.v +++ b/src/Specific/X2448/Karatsuba/C64/CurveParameters.v @@ -1,4 +1,4 @@ -Require Import Crypto.Specific.Framework.CurveParameters. +Require Import Crypto.Specific.Framework.RawCurveParameters. Require Import Crypto.Util.LetIn. (*** @@ -6,29 +6,29 @@ Modulus : 2^448-2^224-1 Base: 56 ***) -Module Curve <: CurveParameters. - Definition sz : nat := 8%nat. - Definition bitwidth : Z := 64. - Definition s : Z := 2^448. - Definition c : list limb := [(1, 1); (2^224, 1)]. - Definition carry_chains : option (list (list nat)) := Eval vm_compute in Some [[3; 7]; [0; 4; 1; 5; 2; 6; 3; 7]; [4; 0]]%nat. +Definition curve : CurveParameters := + {| + sz := 8%nat; + bitwidth := 64; + s := 2^448; + c := [(1, 1); (2^224, 1)]; + carry_chains := Some [[3; 7]; [0; 4; 1; 5; 2; 6; 3; 7]; [4; 0]]%nat; - Definition a24 : option Z := None. - Definition coef_div_modulus : option nat := Some 2%nat. (* add 2*modulus before subtracting *) + a24 := None; + coef_div_modulus := Some 2%nat; - Definition goldilocks : bool := true. - Definition montgomery : bool := false. + goldilocks := Some true; + montgomery := false; - Definition mul_code : option (Z^sz -> Z^sz -> Z^sz) - := None. + mul_code := None; - Definition square_code : option (Z^sz -> Z^sz) - := None. + square_code := None; - Definition upper_bound_of_exponent : option (Z -> Z) := None. - Definition allowable_bit_widths : option (list nat) := None. - Definition freeze_extra_allowable_bit_widths : option (list nat) := None. - Definition modinv_fuel : option nat := None. - Ltac extra_prove_mul_eq := idtac. - Ltac extra_prove_square_eq := idtac. -End Curve. + upper_bound_of_exponent := None; + allowable_bit_widths := None; + freeze_extra_allowable_bit_widths := None; + modinv_fuel := None + |}. + +Ltac extra_prove_mul_eq _ := idtac. +Ltac extra_prove_square_eq _ := idtac. diff --git a/src/Specific/X2448/Karatsuba/C64/Synthesis.v b/src/Specific/X2448/Karatsuba/C64/Synthesis.v index 500671c90..4016ee71c 100644 --- a/src/Specific/X2448/Karatsuba/C64/Synthesis.v +++ b/src/Specific/X2448/Karatsuba/C64/Synthesis.v @@ -1,11 +1,9 @@ Require Import Crypto.Specific.Framework.SynthesisFramework. Require Import Crypto.Specific.X2448.Karatsuba.C64.CurveParameters. -Module Import T := MakeSynthesisTactics Curve. - Module P <: PrePackage. Definition package : Tag.Context. - Proof. make_Synthesis_package (). Defined. + Proof. make_Synthesis_package curve extra_prove_mul_eq extra_prove_square_eq. Defined. End P. -Module Export S := PackageSynthesis Curve P. +Module Export S := PackageSynthesis P. |