diff options
Diffstat (limited to 'src/Specific/X2448/Karatsuba')
| -rw-r--r-- | src/Specific/X2448/Karatsuba/C64/CurveParameters.v | 3 | ||||
| -rw-r--r-- | src/Specific/X2448/Karatsuba/C64/Synthesis.v | 9 | ||||
| -rw-r--r-- | src/Specific/X2448/Karatsuba/C64/femul.v | 2 |
3 files changed, 7 insertions, 7 deletions
diff --git a/src/Specific/X2448/Karatsuba/C64/CurveParameters.v b/src/Specific/X2448/Karatsuba/C64/CurveParameters.v index aa8fd5614..9fe08de2c 100644 --- a/src/Specific/X2448/Karatsuba/C64/CurveParameters.v +++ b/src/Specific/X2448/Karatsuba/C64/CurveParameters.v @@ -14,7 +14,7 @@ Module Curve <: CurveParameters. 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 a24 : option Z := None. - Definition coef_div_modulus : nat := 2%nat. (* add 2*modulus before subtracting *) + Definition coef_div_modulus : option nat := Some 2%nat. (* add 2*modulus before subtracting *) Definition goldilocks : bool := true. @@ -27,6 +27,7 @@ Module Curve <: CurveParameters. 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. diff --git a/src/Specific/X2448/Karatsuba/C64/Synthesis.v b/src/Specific/X2448/Karatsuba/C64/Synthesis.v index 8ea8aa5c9..500671c90 100644 --- a/src/Specific/X2448/Karatsuba/C64/Synthesis.v +++ b/src/Specific/X2448/Karatsuba/C64/Synthesis.v @@ -3,12 +3,9 @@ Require Import Crypto.Specific.X2448.Karatsuba.C64.CurveParameters. Module Import T := MakeSynthesisTactics Curve. -Module P <: SynthesisPrePackage. - Definition Synthesis_package' : Synthesis_package'_Type. - Proof. make_synthesis_package (). Defined. - - Definition Synthesis_package - := Eval cbv [Synthesis_package' projT2] in projT2 Synthesis_package'. +Module P <: PrePackage. + Definition package : Tag.Context. + Proof. make_Synthesis_package (). Defined. End P. Module Export S := PackageSynthesis Curve P. diff --git a/src/Specific/X2448/Karatsuba/C64/femul.v b/src/Specific/X2448/Karatsuba/C64/femul.v index 2f890a88f..07dd9b26d 100644 --- a/src/Specific/X2448/Karatsuba/C64/femul.v +++ b/src/Specific/X2448/Karatsuba/C64/femul.v @@ -10,3 +10,5 @@ Proof. Time synthesize_mul (). Show Ltac Profile. Time Defined. + +Print Assumptions mul. |