11 files changed, 25 insertions, 15 deletions
diff --git a/src/Specific/X25519/C32/CurveParameters.v b/src/Specific/X25519/C32/CurveParameters.v
index e8a46ea9e..6324acfca 100644
--- a/src/Specific/X25519/C32/CurveParameters.v
+++ b/src/Specific/X25519/C32/CurveParameters.v
@@ -14,7 +14,7 @@ Module Curve <: CurveParameters.
   Definition carry_chains : option (list (list nat)) := Eval vm_compute in Some [seq 0 (pred sz); [0; 1]]%nat.
 
   Definition a24 : option Z := Some 121665.
-  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 := false.
 
@@ -245,6 +245,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/X25519/C32/Synthesis.v b/src/Specific/X25519/C32/Synthesis.v
index 3b9b35078..0b3336b20 100644
--- a/src/Specific/X25519/C32/Synthesis.v
+++ b/src/Specific/X25519/C32/Synthesis.v
@@ -3,12 +3,9 @@ Require Import Crypto.Specific.X25519.C32.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/X25519/C32/femul.v b/src/Specific/X25519/C32/femul.v
index 81bf1f255..bc62814e9 100644
--- a/src/Specific/X25519/C32/femul.v
+++ b/src/Specific/X25519/C32/femul.v
@@ -10,3 +10,5 @@ Proof.
   Time synthesize_mul ().
   Show Ltac Profile.
 Time Defined.
+
+Print Assumptions mul.
diff --git a/src/Specific/X25519/C32/fesquare.v b/src/Specific/X25519/C32/fesquare.v
index 3fa837bd2..2bea3bf8b 100644
--- a/src/Specific/X25519/C32/fesquare.v
+++ b/src/Specific/X25519/C32/fesquare.v
@@ -10,3 +10,5 @@ Proof.
   Time synthesize_square ().
   Show Ltac Profile.
 Time Defined.
+
+Print Assumptions square.
diff --git a/src/Specific/X25519/C32/freeze.v b/src/Specific/X25519/C32/freeze.v
index 9af1e8e0f..bac5a019f 100644
--- a/src/Specific/X25519/C32/freeze.v
+++ b/src/Specific/X25519/C32/freeze.v
@@ -10,3 +10,5 @@ Proof.
   Time synthesize_freeze ().
   Show Ltac Profile.
 Time Defined.
+
+Print Assumptions freeze.
diff --git a/src/Specific/X25519/C64/CurveParameters.v b/src/Specific/X25519/C64/CurveParameters.v
index 54c578a08..78db9dd8e 100644
--- a/src/Specific/X25519/C64/CurveParameters.v
+++ b/src/Specific/X25519/C64/CurveParameters.v
@@ -14,7 +14,7 @@ Module Curve <: CurveParameters.
   Definition carry_chains : option (list (list nat)) := Eval vm_compute in Some [seq 0 (pred sz); [0; 1]]%nat.
 
   Definition a24 : option Z := Some 121665.
-  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 := false.
 
@@ -62,6 +62,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/X25519/C64/Synthesis.v b/src/Specific/X25519/C64/Synthesis.v
index 3c3bac04d..2ea78caba 100644
--- a/src/Specific/X25519/C64/Synthesis.v
+++ b/src/Specific/X25519/C64/Synthesis.v
@@ -3,12 +3,9 @@ Require Import Crypto.Specific.X25519.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/X25519/C64/femul.v b/src/Specific/X25519/C64/femul.v
index 1e015ddd9..7292df912 100644
--- a/src/Specific/X25519/C64/femul.v
+++ b/src/Specific/X25519/C64/femul.v
@@ -10,3 +10,5 @@ Proof.
   Time synthesize_mul ().
   Show Ltac Profile.
 Time Defined.
+
+Print Assumptions mul.
diff --git a/src/Specific/X25519/C64/fesquare.v b/src/Specific/X25519/C64/fesquare.v
index cfad2d111..fa692f559 100644
--- a/src/Specific/X25519/C64/fesquare.v
+++ b/src/Specific/X25519/C64/fesquare.v
@@ -10,3 +10,5 @@ Proof.
   Time synthesize_square ().
   Show Ltac Profile.
 Time Defined.
+
+Print Assumptions square.
diff --git a/src/Specific/X25519/C64/freeze.v b/src/Specific/X25519/C64/freeze.v
index ef826dba5..2c7fe8b85 100644
--- a/src/Specific/X25519/C64/freeze.v
+++ b/src/Specific/X25519/C64/freeze.v
@@ -10,3 +10,5 @@ Proof.
   Time synthesize_freeze ().
   Show Ltac Profile.
 Time Defined.
+
+Print Assumptions freeze.
diff --git a/src/Specific/X25519/C64/ladderstep.v b/src/Specific/X25519/C64/ladderstep.v
index adb20912e..fc62c9317 100644
--- a/src/Specific/X25519/C64/ladderstep.v
+++ b/src/Specific/X25519/C64/ladderstep.v
@@ -1,6 +1,6 @@
 Require Import Crypto.Arithmetic.Core.
 Require Import Crypto.Arithmetic.PrimeFieldTheorems.
-Require Import Crypto.Specific.Framework.LadderstepSynthesisFramework.
+Require Import Crypto.Specific.Framework.ArithmeticSynthesis.Ladderstep.
 Require Import Crypto.Specific.X25519.C64.Synthesis.
 
 (* TODO : change this to field once field isomorphism happens *)
@@ -20,3 +20,5 @@ Proof.
   synthesize_xzladderstep ().
   Show Ltac Profile.
 Time Defined.
+
+Print Assumptions xzladderstep.