Support p256 / montgomery in json format

Extra time comes from adding AMD128 to NISTP256, mostly.

After     | File Name                                                | Before    || Change
---------------------------------------------------------------------------------------------
13m25.13s | Total                                                    | 13m30.82s || -0m05.69s
---------------------------------------------------------------------------------------------
   N/A    | Specific/IntegrationTestMontgomeryP256_128               | 0m25.42s  || -0m25.42s
0m22.75s  | Specific/NISTP256/AMD128/femul                           |    N/A    || +0m22.75s
1m31.64s  | Specific/NISTP256/AMD64/femul                            | 1m52.42s  || -0m20.78s
0m14.46s  | Specific/NISTP256/AMD128/fesub                           |    N/A    || +0m14.46s
0m14.25s  | Specific/NISTP256/AMD128/feadd                           |    N/A    || +0m14.25s
0m14.12s  | Specific/NISTP256/AMD128/fenz                            |    N/A    || +0m14.11s
   N/A    | Specific/NISTP256/AMD64/MontgomeryP256                   | 0m13.00s  || -0m13.00s
   N/A    | Specific/IntegrationTestMontgomeryP256_128_Sub           | 0m12.40s  || -0m12.40s
   N/A    | Specific/IntegrationTestMontgomeryP256_128_Add           | 0m11.99s  || -0m11.99s
0m11.74s  | Specific/NISTP256/AMD128/feopp                           |    N/A    || +0m11.74s
   N/A    | Specific/IntegrationTestMontgomeryP256_128_Opp           | 0m11.22s  || -0m11.22s
   N/A    | Specific/IntegrationTestMontgomeryP256_128_Nonzero       | 0m09.27s  || -0m09.26s
   N/A    | Specific/MontgomeryP256_128                              | 0m09.26s  || -0m09.25s
0m08.42s  | Specific/NISTP256/AMD64/Synthesis                        |    N/A    || +0m08.41s
0m14.67s  | Specific/NISTP256/AMD64/fenz                             | 0m09.98s  || +0m04.68s
0m04.12s  | Specific/Framework/ArithmeticSynthesis/Montgomery        |    N/A    || +0m04.12s
0m03.58s  | Specific/NISTP256/AMD128/Synthesis                       |    N/A    || +0m03.58s
1m10.78s  | Specific/X2555/C128/ladderstep                           | 1m08.36s  || +0m02.42s
1m02.10s  | Specific/X25519/C32/femul                                | 1m00.59s  || +0m01.50s
0m43.59s  | Specific/X2448/Karatsuba/C64/Synthesis                   | 0m44.86s  || -0m01.26s
0m34.97s  | Specific/X25519/C32/fesquare                             | 0m35.98s  || -0m01.00s
0m20.10s  | Specific/NISTP256/AMD64/fesub                            | 0m18.37s  || +0m01.73s
0m17.61s  | Specific/NISTP256/AMD64/feadd                            | 0m15.94s  || +0m01.67s
2m09.77s  | Specific/X25519/C64/ladderstep                           | 2m09.79s  || -0m00.01s
1m11.70s  | Specific/X2448/Karatsuba/C64/femul                       | 1m11.60s  || +0m00.10s
0m32.14s  | Specific/X25519/C32/Synthesis                            | 0m31.70s  || +0m00.44s
0m27.94s  | Specific/X25519/C32/freeze                               | 0m28.06s  || -0m00.11s
0m17.62s  | Specific/X25519/C64/femul                                | 0m17.41s  || +0m00.21s
0m15.21s  | Specific/X25519/C64/freeze                               | 0m14.74s  || +0m00.47s
0m14.86s  | Specific/NISTP256/AMD64/feopp                            | 0m14.96s  || -0m00.10s
0m14.58s  | Specific/X25519/C64/fesquare                             | 0m14.06s  || +0m00.51s
0m10.10s  | Specific/X25519/C64/Synthesis                            | 0m09.78s  || +0m00.32s
0m06.22s  | Specific/X2555/C128/Synthesis                            | 0m06.17s  || +0m00.04s
0m01.01s  | Specific/X25519/C32/CurveParameters                      | 0m01.05s  || -0m00.04s
0m00.99s  | Specific/Framework/SynthesisFramework                    | 0m01.08s  || -0m00.09s
0m00.79s  | Specific/Framework/MontgomeryReificationTypes            |    N/A    || +0m00.79s
0m00.78s  | Specific/Framework/ArithmeticSynthesis/SquareFromMul     | 0m00.70s  || +0m00.08s
0m00.78s  | Specific/Framework/ArithmeticSynthesis/Karatsuba         | 0m00.75s  || +0m00.03s
0m00.76s  | Specific/Framework/ArithmeticSynthesis/MontgomeryPackage |    N/A    || +0m00.76s
0m00.75s  | Specific/Framework/IntegrationTestTemporaryMiscCommon    | 0m00.80s  || -0m00.05s
0m00.75s  | Specific/Framework/MontgomeryReificationTypesPackage     |    N/A    || +0m00.75s
0m00.73s  | Specific/Framework/ArithmeticSynthesis/Defaults          | 0m00.75s  || -0m00.02s
0m00.72s  | Specific/Framework/ReificationTypesPackage               | 0m00.70s  || +0m00.02s
0m00.72s  | Specific/Framework/ArithmeticSynthesis/Base              | 0m00.73s  || -0m00.01s
0m00.72s  | Specific/Framework/ArithmeticSynthesis/BasePackage       | 0m00.69s  || +0m00.03s
0m00.72s  | Specific/Framework/ArithmeticSynthesis/LadderstepPackage | 0m00.76s  || -0m00.04s
0m00.70s  | Specific/Framework/ArithmeticSynthesis/Freeze            | 0m00.75s  || -0m00.05s
0m00.70s  | Specific/Framework/ArithmeticSynthesis/KaratsubaPackage  | 0m00.77s  || -0m00.07s
0m00.69s  | Specific/Framework/ArithmeticSynthesis/DefaultsPackage   | 0m00.71s  || -0m00.02s
0m00.67s  | Specific/Framework/ArithmeticSynthesis/FreezePackage     | 0m00.74s  || -0m00.06s
0m00.43s  | Specific/X25519/C64/CurveParameters                      | 0m00.43s  || +0m00.00s
0m00.38s  | Specific/Framework/IntegrationTestDisplayCommon          | 0m00.40s  || -0m00.02s
0m00.38s  | Specific/Framework/IntegrationTestDisplayCommonTactics   | 0m00.37s  || +0m00.01s
0m00.34s  | Specific/Framework/CurveParameters                       | 0m00.32s  || +0m00.02s
0m00.33s  | Specific/X2555/C128/CurveParameters                      | 0m00.33s  || +0m00.00s
0m00.32s  | Specific/NISTP256/AMD128/CurveParameters                 |    N/A    || +0m00.32s
0m00.32s  | Specific/X2448/Karatsuba/C64/CurveParameters             | 0m00.33s  || -0m00.01s
0m00.31s  | Specific/Framework/CurveParametersPackage                | 0m00.33s  || -0m00.02s
0m00.30s  | Specific/NISTP256/AMD64/CurveParameters                  |    N/A    || +0m00.30s

1 files changed, 458 insertions, 0 deletions

diff --git a/src/Specific/Framework/ArithmeticSynthesis/MontgomeryPackage.v b/src/Specific/Framework/ArithmeticSynthesis/MontgomeryPackage.v
new file mode 100644
index 000000000..4980f09b9
--- /dev/null
+++ b/src/Specific/Framework/ArithmeticSynthesis/MontgomeryPackage.v
@@ -0,0 +1,458 @@
+(* This file is autogenerated from Montgomery.v by remake_packages.py *)
+Require Import Crypto.Specific.Framework.CurveParametersPackage.
+Require Import Crypto.Specific.Framework.ArithmeticSynthesis.BasePackage.
+Require Import Crypto.Specific.Framework.ArithmeticSynthesis.DefaultsPackage.
+Require Import Crypto.Specific.Framework.ArithmeticSynthesis.FreezePackage.
+Require Import Crypto.Specific.Framework.ArithmeticSynthesis.LadderstepPackage.
+Require Export Crypto.Specific.Framework.ArithmeticSynthesis.Montgomery.
+Require Import Crypto.Specific.Framework.Packages.
+Require Import Crypto.Util.TagList.
+
+Module TAG.
+  Inductive tags := m' | r' | m'_correct | r'_correct | m_enc_correct_montgomery | r'_pow_correct | montgomery_to_F | r_big | m_big | m_enc_small | map_m_enc | mul_ext | add_ext | sub_ext | opp_ext | nonzero_ext | mul_bounded | add_bounded | sub_bounded | opp_bounded | nonzero_sig.
+End TAG.
+
+Ltac add_m' pkg :=
+  if_montgomery
+    pkg
+    ltac:(fun _ => let modinv_fuel := Tag.get pkg TAG.modinv_fuel in
+                   let m := Tag.get pkg TAG.m in
+                   let r := Tag.get pkg TAG.r in
+                   let m' := fresh "m'" in
+                   let m' := pose_m' modinv_fuel m r m' in
+                   Tag.update pkg TAG.m' m')
+    ltac:(fun _ => pkg)
+    ().
+Ltac add_r' pkg :=
+  if_montgomery
+    pkg
+    ltac:(fun _ => let modinv_fuel := Tag.get pkg TAG.modinv_fuel in
+                   let m := Tag.get pkg TAG.m in
+                   let r := Tag.get pkg TAG.r in
+                   let r' := fresh "r'" in
+                   let r' := pose_r' modinv_fuel m r r' in
+                   Tag.update pkg TAG.r' r')
+    ltac:(fun _ => pkg)
+    ().
+Ltac add_m'_correct pkg :=
+  if_montgomery
+    pkg
+    ltac:(fun _ => let m := Tag.get pkg TAG.m in
+                   let m' := Tag.get pkg TAG.m' in
+                   let r := Tag.get pkg TAG.r in
+                   let m'_correct := fresh "m'_correct" in
+                   let m'_correct := pose_m'_correct m m' r m'_correct in
+                   Tag.update pkg TAG.m'_correct m'_correct)
+    ltac:(fun _ => pkg)
+    ().
+Ltac add_r'_correct pkg :=
+  if_montgomery
+    pkg
+    ltac:(fun _ => let m := Tag.get pkg TAG.m in
+                   let r := Tag.get pkg TAG.r in
+                   let r' := Tag.get pkg TAG.r' in
+                   let r'_correct := fresh "r'_correct" in
+                   let r'_correct := pose_r'_correct m r r' r'_correct in
+                   Tag.update pkg TAG.r'_correct r'_correct)
+    ltac:(fun _ => pkg)
+    ().
+Ltac add_m_enc_correct_montgomery pkg :=
+  if_montgomery
+    pkg
+    ltac:(fun _ => let m := Tag.get pkg TAG.m in
+                   let sz := Tag.get pkg TAG.sz in
+                   let r := Tag.get pkg TAG.r in
+                   let m_enc := Tag.get pkg TAG.m_enc in
+                   let m_enc_correct_montgomery := fresh "m_enc_correct_montgomery" in
+                   let m_enc_correct_montgomery := pose_m_enc_correct_montgomery m sz r m_enc m_enc_correct_montgomery in
+                   Tag.update pkg TAG.m_enc_correct_montgomery m_enc_correct_montgomery)
+    ltac:(fun _ => pkg)
+    ().
+Ltac add_r'_pow_correct pkg :=
+  if_montgomery
+    pkg
+    ltac:(fun _ => let r' := Tag.get pkg TAG.r' in
+                   let sz := Tag.get pkg TAG.sz in
+                   let r := Tag.get pkg TAG.r in
+                   let m_enc := Tag.get pkg TAG.m_enc in
+                   let r'_pow_correct := fresh "r'_pow_correct" in
+                   let r'_pow_correct := pose_r'_pow_correct r' sz r m_enc r'_pow_correct in
+                   Tag.update pkg TAG.r'_pow_correct r'_pow_correct)
+    ltac:(fun _ => pkg)
+    ().
+Ltac add_montgomery_to_F pkg :=
+  if_montgomery
+    pkg
+    ltac:(fun _ => let sz := Tag.get pkg TAG.sz in
+                   let m := Tag.get pkg TAG.m in
+                   let r' := Tag.get pkg TAG.r' in
+                   let montgomery_to_F := fresh "montgomery_to_F" in
+                   let montgomery_to_F := pose_montgomery_to_F sz m r' montgomery_to_F in
+                   Tag.update pkg TAG.montgomery_to_F montgomery_to_F)
+    ltac:(fun _ => pkg)
+    ().
+Ltac add_r_big pkg :=
+  if_montgomery
+    pkg
+    ltac:(fun _ => let r := Tag.get pkg TAG.r in
+                   let r_big := fresh "r_big" in
+                   let r_big := pose_r_big r r_big in
+                   Tag.update pkg TAG.r_big r_big)
+    ltac:(fun _ => pkg)
+    ().
+Ltac add_m_big pkg :=
+  if_montgomery
+    pkg
+    ltac:(fun _ => let m := Tag.get pkg TAG.m in
+                   let m_big := fresh "m_big" in
+                   let m_big := pose_m_big m m_big in
+                   Tag.update pkg TAG.m_big m_big)
+    ltac:(fun _ => pkg)
+    ().
+Ltac add_m_enc_small pkg :=
+  if_montgomery
+    pkg
+    ltac:(fun _ => let sz := Tag.get pkg TAG.sz in
+                   let r := Tag.get pkg TAG.r in
+                   let m_enc := Tag.get pkg TAG.m_enc in
+                   let m_enc_small := fresh "m_enc_small" in
+                   let m_enc_small := pose_m_enc_small sz r m_enc m_enc_small in
+                   Tag.update pkg TAG.m_enc_small m_enc_small)
+    ltac:(fun _ => pkg)
+    ().
+Ltac add_map_m_enc pkg :=
+  if_montgomery
+    pkg
+    ltac:(fun _ => let sz := Tag.get pkg TAG.sz in
+                   let r := Tag.get pkg TAG.r in
+                   let m_enc := Tag.get pkg TAG.m_enc in
+                   let map_m_enc := fresh "map_m_enc" in
+                   let map_m_enc := pose_map_m_enc sz r m_enc map_m_enc in
+                   Tag.update pkg TAG.map_m_enc map_m_enc)
+    ltac:(fun _ => pkg)
+    ().
+Ltac add_mul_ext pkg :=
+  if_montgomery
+    pkg
+    ltac:(fun _ => let r := Tag.get pkg TAG.r in
+                   let sz := Tag.get pkg TAG.sz in
+                   let m := Tag.get pkg TAG.m in
+                   let m_enc := Tag.get pkg TAG.m_enc in
+                   let r' := Tag.get pkg TAG.r' in
+                   let r'_correct := Tag.get pkg TAG.r'_correct in
+                   let m' := Tag.get pkg TAG.m' in
+                   let m'_correct := Tag.get pkg TAG.m'_correct in
+                   let m_enc_correct_montgomery := Tag.get pkg TAG.m_enc_correct_montgomery in
+                   let r_big := Tag.get pkg TAG.r_big in
+                   let m_big := Tag.get pkg TAG.m_big in
+                   let m_enc_small := Tag.get pkg TAG.m_enc_small in
+                   let montgomery_to_F := Tag.get pkg TAG.montgomery_to_F in
+                   let mul_ext := fresh "mul_ext" in
+                   let mul_ext := pose_mul_ext r sz m m_enc r' r'_correct m' m'_correct m_enc_correct_montgomery r_big m_big m_enc_small montgomery_to_F mul_ext in
+                   Tag.update pkg TAG.mul_ext mul_ext)
+    ltac:(fun _ => pkg)
+    ().
+Ltac add_add_ext pkg :=
+  if_montgomery
+    pkg
+    ltac:(fun _ => let r := Tag.get pkg TAG.r in
+                   let sz := Tag.get pkg TAG.sz in
+                   let m := Tag.get pkg TAG.m in
+                   let m_enc := Tag.get pkg TAG.m_enc in
+                   let r' := Tag.get pkg TAG.r' in
+                   let m_enc_correct_montgomery := Tag.get pkg TAG.m_enc_correct_montgomery in
+                   let r_big := Tag.get pkg TAG.r_big in
+                   let m_big := Tag.get pkg TAG.m_big in
+                   let m_enc_small := Tag.get pkg TAG.m_enc_small in
+                   let montgomery_to_F := Tag.get pkg TAG.montgomery_to_F in
+                   let add_ext := fresh "add_ext" in
+                   let add_ext := pose_add_ext r sz m m_enc r' m_enc_correct_montgomery r_big m_big m_enc_small montgomery_to_F add_ext in
+                   Tag.update pkg TAG.add_ext add_ext)
+    ltac:(fun _ => pkg)
+    ().
+Ltac add_sub_ext pkg :=
+  if_montgomery
+    pkg
+    ltac:(fun _ => let r := Tag.get pkg TAG.r in
+                   let sz := Tag.get pkg TAG.sz in
+                   let m := Tag.get pkg TAG.m in
+                   let m_enc := Tag.get pkg TAG.m_enc in
+                   let r' := Tag.get pkg TAG.r' in
+                   let m_enc_correct_montgomery := Tag.get pkg TAG.m_enc_correct_montgomery in
+                   let r_big := Tag.get pkg TAG.r_big in
+                   let m_enc_small := Tag.get pkg TAG.m_enc_small in
+                   let map_m_enc := Tag.get pkg TAG.map_m_enc in
+                   let montgomery_to_F := Tag.get pkg TAG.montgomery_to_F in
+                   let sub_ext := fresh "sub_ext" in
+                   let sub_ext := pose_sub_ext r sz m m_enc r' m_enc_correct_montgomery r_big m_enc_small map_m_enc montgomery_to_F sub_ext in
+                   Tag.update pkg TAG.sub_ext sub_ext)
+    ltac:(fun _ => pkg)
+    ().
+Ltac add_opp_ext pkg :=
+  if_montgomery
+    pkg
+    ltac:(fun _ => let r := Tag.get pkg TAG.r in
+                   let sz := Tag.get pkg TAG.sz in
+                   let m := Tag.get pkg TAG.m in
+                   let m_enc := Tag.get pkg TAG.m_enc in
+                   let r' := Tag.get pkg TAG.r' in
+                   let m_enc_correct_montgomery := Tag.get pkg TAG.m_enc_correct_montgomery in
+                   let r_big := Tag.get pkg TAG.r_big in
+                   let m_enc_small := Tag.get pkg TAG.m_enc_small in
+                   let map_m_enc := Tag.get pkg TAG.map_m_enc in
+                   let montgomery_to_F := Tag.get pkg TAG.montgomery_to_F in
+                   let opp_ext := fresh "opp_ext" in
+                   let opp_ext := pose_opp_ext r sz m m_enc r' m_enc_correct_montgomery r_big m_enc_small map_m_enc montgomery_to_F opp_ext in
+                   Tag.update pkg TAG.opp_ext opp_ext)
+    ltac:(fun _ => pkg)
+    ().
+Ltac add_nonzero_ext pkg :=
+  if_montgomery
+    pkg
+    ltac:(fun _ => let r := Tag.get pkg TAG.r in
+                   let sz := Tag.get pkg TAG.sz in
+                   let m := Tag.get pkg TAG.m in
+                   let m_enc := Tag.get pkg TAG.m_enc in
+                   let r' := Tag.get pkg TAG.r' in
+                   let m_enc_correct_montgomery := Tag.get pkg TAG.m_enc_correct_montgomery in
+                   let r'_pow_correct := Tag.get pkg TAG.r'_pow_correct in
+                   let r_big := Tag.get pkg TAG.r_big in
+                   let m_big := Tag.get pkg TAG.m_big in
+                   let montgomery_to_F := Tag.get pkg TAG.montgomery_to_F in
+                   let nonzero_ext := fresh "nonzero_ext" in
+                   let nonzero_ext := pose_nonzero_ext r sz m m_enc r' m_enc_correct_montgomery r'_pow_correct r_big m_big montgomery_to_F nonzero_ext in
+                   Tag.update pkg TAG.nonzero_ext nonzero_ext)
+    ltac:(fun _ => pkg)
+    ().
+Ltac add_mul_sig pkg :=
+  if_montgomery
+    pkg
+    ltac:(fun _ => let r := Tag.get pkg TAG.r in
+                   let sz := Tag.get pkg TAG.sz in
+                   let montgomery_to_F := Tag.get pkg TAG.montgomery_to_F in
+                   let mul_ext := Tag.get pkg TAG.mul_ext in
+                   let mul_sig := fresh "mul_sig" in
+                   let mul_sig := pose_mul_sig r sz montgomery_to_F mul_ext mul_sig in
+                   Tag.update pkg TAG.mul_sig mul_sig)
+    ltac:(fun _ => pkg)
+    ().
+Ltac add_mul_bounded pkg :=
+  if_montgomery
+    pkg
+    ltac:(fun _ => let r := Tag.get pkg TAG.r in
+                   let sz := Tag.get pkg TAG.sz in
+                   let m_enc := Tag.get pkg TAG.m_enc in
+                   let montgomery_to_F := Tag.get pkg TAG.montgomery_to_F in
+                   let mul_ext := Tag.get pkg TAG.mul_ext in
+                   let mul_sig := Tag.get pkg TAG.mul_sig in
+                   let mul_bounded := fresh "mul_bounded" in
+                   let mul_bounded := pose_mul_bounded r sz m_enc montgomery_to_F mul_ext mul_sig mul_bounded in
+                   Tag.update pkg TAG.mul_bounded mul_bounded)
+    ltac:(fun _ => pkg)
+    ().
+Ltac add_add_sig pkg :=
+  if_montgomery
+    pkg
+    ltac:(fun _ => let r := Tag.get pkg TAG.r in
+                   let sz := Tag.get pkg TAG.sz in
+                   let m_enc := Tag.get pkg TAG.m_enc in
+                   let montgomery_to_F := Tag.get pkg TAG.montgomery_to_F in
+                   let add_ext := Tag.get pkg TAG.add_ext in
+                   let add_sig := fresh "add_sig" in
+                   let add_sig := pose_add_sig r sz m_enc montgomery_to_F add_ext add_sig in
+                   Tag.update pkg TAG.add_sig add_sig)
+    ltac:(fun _ => pkg)
+    ().
+Ltac add_add_bounded pkg :=
+  if_montgomery
+    pkg
+    ltac:(fun _ => let r := Tag.get pkg TAG.r in
+                   let sz := Tag.get pkg TAG.sz in
+                   let m_enc := Tag.get pkg TAG.m_enc in
+                   let montgomery_to_F := Tag.get pkg TAG.montgomery_to_F in
+                   let add_ext := Tag.get pkg TAG.add_ext in
+                   let add_sig := Tag.get pkg TAG.add_sig in
+                   let add_bounded := fresh "add_bounded" in
+                   let add_bounded := pose_add_bounded r sz m_enc montgomery_to_F add_ext add_sig add_bounded in
+                   Tag.update pkg TAG.add_bounded add_bounded)
+    ltac:(fun _ => pkg)
+    ().
+Ltac add_sub_sig pkg :=
+  if_montgomery
+    pkg
+    ltac:(fun _ => let r := Tag.get pkg TAG.r in
+                   let sz := Tag.get pkg TAG.sz in
+                   let m_enc := Tag.get pkg TAG.m_enc in
+                   let montgomery_to_F := Tag.get pkg TAG.montgomery_to_F in
+                   let sub_ext := Tag.get pkg TAG.sub_ext in
+                   let sub_sig := fresh "sub_sig" in
+                   let sub_sig := pose_sub_sig r sz m_enc montgomery_to_F sub_ext sub_sig in
+                   Tag.update pkg TAG.sub_sig sub_sig)
+    ltac:(fun _ => pkg)
+    ().
+Ltac add_sub_bounded pkg :=
+  if_montgomery
+    pkg
+    ltac:(fun _ => let r := Tag.get pkg TAG.r in
+                   let sz := Tag.get pkg TAG.sz in
+                   let m_enc := Tag.get pkg TAG.m_enc in
+                   let montgomery_to_F := Tag.get pkg TAG.montgomery_to_F in
+                   let sub_ext := Tag.get pkg TAG.sub_ext in
+                   let sub_sig := Tag.get pkg TAG.sub_sig in
+                   let sub_bounded := fresh "sub_bounded" in
+                   let sub_bounded := pose_sub_bounded r sz m_enc montgomery_to_F sub_ext sub_sig sub_bounded in
+                   Tag.update pkg TAG.sub_bounded sub_bounded)
+    ltac:(fun _ => pkg)
+    ().
+Ltac add_opp_sig pkg :=
+  if_montgomery
+    pkg
+    ltac:(fun _ => let r := Tag.get pkg TAG.r in
+                   let sz := Tag.get pkg TAG.sz in
+                   let m_enc := Tag.get pkg TAG.m_enc in
+                   let montgomery_to_F := Tag.get pkg TAG.montgomery_to_F in
+                   let opp_ext := Tag.get pkg TAG.opp_ext in
+                   let opp_sig := fresh "opp_sig" in
+                   let opp_sig := pose_opp_sig r sz m_enc montgomery_to_F opp_ext opp_sig in
+                   Tag.update pkg TAG.opp_sig opp_sig)
+    ltac:(fun _ => pkg)
+    ().
+Ltac add_opp_bounded pkg :=
+  if_montgomery
+    pkg
+    ltac:(fun _ => let r := Tag.get pkg TAG.r in
+                   let sz := Tag.get pkg TAG.sz in
+                   let m_enc := Tag.get pkg TAG.m_enc in
+                   let montgomery_to_F := Tag.get pkg TAG.montgomery_to_F in
+                   let opp_ext := Tag.get pkg TAG.opp_ext in
+                   let opp_sig := Tag.get pkg TAG.opp_sig in
+                   let opp_bounded := fresh "opp_bounded" in
+                   let opp_bounded := pose_opp_bounded r sz m_enc montgomery_to_F opp_ext opp_sig opp_bounded in
+                   Tag.update pkg TAG.opp_bounded opp_bounded)
+    ltac:(fun _ => pkg)
+    ().
+Ltac add_nonzero_sig pkg :=
+  if_montgomery
+    pkg
+    ltac:(fun _ => let r := Tag.get pkg TAG.r in
+                   let sz := Tag.get pkg TAG.sz in
+                   let m := Tag.get pkg TAG.m in
+                   let m_enc := Tag.get pkg TAG.m_enc in
+                   let montgomery_to_F := Tag.get pkg TAG.montgomery_to_F in
+                   let nonzero_ext := Tag.get pkg TAG.nonzero_ext in
+                   let nonzero_sig := fresh "nonzero_sig" in
+                   let nonzero_sig := pose_nonzero_sig r sz m m_enc montgomery_to_F nonzero_ext nonzero_sig in
+                   Tag.update pkg TAG.nonzero_sig nonzero_sig)
+    ltac:(fun _ => pkg)
+    ().
+Ltac add_ring pkg :=
+  if_montgomery
+    pkg
+    ltac:(fun _ => let ring := fresh "ring" in
+                   let ring := pose_ring ring in
+                   Tag.update pkg TAG.ring ring)
+    ltac:(fun _ => pkg)
+    ().
+Ltac add_carry_sig pkg :=
+  if_montgomery
+    pkg
+    ltac:(fun _ => let carry_sig := fresh "carry_sig" in
+                   let carry_sig := pose_carry_sig carry_sig in
+                   Tag.update pkg TAG.carry_sig carry_sig)
+    ltac:(fun _ => pkg)
+    ().
+Ltac add_freeze_sig pkg :=
+  if_montgomery
+    pkg
+    ltac:(fun _ => let freeze_sig := fresh "freeze_sig" in
+                   let freeze_sig := pose_freeze_sig freeze_sig in
+                   Tag.update pkg TAG.freeze_sig freeze_sig)
+    ltac:(fun _ => pkg)
+    ().
+Ltac add_Mxzladderstep_sig pkg :=
+  if_montgomery
+    pkg
+    ltac:(fun _ => let Mxzladderstep_sig := fresh "Mxzladderstep_sig" in
+                   let Mxzladderstep_sig := pose_Mxzladderstep_sig Mxzladderstep_sig in
+                   Tag.update pkg TAG.Mxzladderstep_sig Mxzladderstep_sig)
+    ltac:(fun _ => pkg)
+    ().
+Ltac add_Montgomery_package pkg :=
+  let pkg := add_m' pkg in
+  let pkg := add_r' pkg in
+  let pkg := add_m'_correct pkg in
+  let pkg := add_r'_correct pkg in
+  let pkg := add_m_enc_correct_montgomery pkg in
+  let pkg := add_r'_pow_correct pkg in
+  let pkg := add_montgomery_to_F pkg in
+  let pkg := add_r_big pkg in
+  let pkg := add_m_big pkg in
+  let pkg := add_m_enc_small pkg in
+  let pkg := add_map_m_enc pkg in
+  let pkg := add_mul_ext pkg in
+  let pkg := add_add_ext pkg in
+  let pkg := add_sub_ext pkg in
+  let pkg := add_opp_ext pkg in
+  let pkg := add_nonzero_ext pkg in
+  let pkg := add_mul_sig pkg in
+  let pkg := add_mul_bounded pkg in
+  let pkg := add_add_sig pkg in
+  let pkg := add_add_bounded pkg in
+  let pkg := add_sub_sig pkg in
+  let pkg := add_sub_bounded pkg in
+  let pkg := add_opp_sig pkg in
+  let pkg := add_opp_bounded pkg in
+  let pkg := add_nonzero_sig pkg in
+  let pkg := add_ring pkg in
+  let pkg := add_carry_sig pkg in
+  let pkg := add_freeze_sig pkg in
+  let pkg := add_Mxzladderstep_sig pkg in
+  Tag.strip_local pkg.
+
+
+Module MakeMontgomeryPackage (PKG : PrePackage).
+  Module Import MakeMontgomeryPackageInternal := MakePackageBase PKG.
+
+  Ltac get_m' _ := get TAG.m'.
+  Notation m' := (ltac:(let v := get_m' () in exact v)) (only parsing).
+  Ltac get_r' _ := get TAG.r'.
+  Notation r' := (ltac:(let v := get_r' () in exact v)) (only parsing).
+  Ltac get_m'_correct _ := get TAG.m'_correct.
+  Notation m'_correct := (ltac:(let v := get_m'_correct () in exact v)) (only parsing).
+  Ltac get_r'_correct _ := get TAG.r'_correct.
+  Notation r'_correct := (ltac:(let v := get_r'_correct () in exact v)) (only parsing).
+  Ltac get_m_enc_correct_montgomery _ := get TAG.m_enc_correct_montgomery.
+  Notation m_enc_correct_montgomery := (ltac:(let v := get_m_enc_correct_montgomery () in exact v)) (only parsing).
+  Ltac get_r'_pow_correct _ := get TAG.r'_pow_correct.
+  Notation r'_pow_correct := (ltac:(let v := get_r'_pow_correct () in exact v)) (only parsing).
+  Ltac get_montgomery_to_F _ := get TAG.montgomery_to_F.
+  Notation montgomery_to_F := (ltac:(let v := get_montgomery_to_F () in exact v)) (only parsing).
+  Ltac get_r_big _ := get TAG.r_big.
+  Notation r_big := (ltac:(let v := get_r_big () in exact v)) (only parsing).
+  Ltac get_m_big _ := get TAG.m_big.
+  Notation m_big := (ltac:(let v := get_m_big () in exact v)) (only parsing).
+  Ltac get_m_enc_small _ := get TAG.m_enc_small.
+  Notation m_enc_small := (ltac:(let v := get_m_enc_small () in exact v)) (only parsing).
+  Ltac get_map_m_enc _ := get TAG.map_m_enc.
+  Notation map_m_enc := (ltac:(let v := get_map_m_enc () in exact v)) (only parsing).
+  Ltac get_mul_ext _ := get TAG.mul_ext.
+  Notation mul_ext := (ltac:(let v := get_mul_ext () in exact v)) (only parsing).
+  Ltac get_add_ext _ := get TAG.add_ext.
+  Notation add_ext := (ltac:(let v := get_add_ext () in exact v)) (only parsing).
+  Ltac get_sub_ext _ := get TAG.sub_ext.
+  Notation sub_ext := (ltac:(let v := get_sub_ext () in exact v)) (only parsing).
+  Ltac get_opp_ext _ := get TAG.opp_ext.
+  Notation opp_ext := (ltac:(let v := get_opp_ext () in exact v)) (only parsing).
+  Ltac get_nonzero_ext _ := get TAG.nonzero_ext.
+  Notation nonzero_ext := (ltac:(let v := get_nonzero_ext () in exact v)) (only parsing).
+  Ltac get_mul_bounded _ := get TAG.mul_bounded.
+  Notation mul_bounded := (ltac:(let v := get_mul_bounded () in exact v)) (only parsing).
+  Ltac get_add_bounded _ := get TAG.add_bounded.
+  Notation add_bounded := (ltac:(let v := get_add_bounded () in exact v)) (only parsing).
+  Ltac get_sub_bounded _ := get TAG.sub_bounded.
+  Notation sub_bounded := (ltac:(let v := get_sub_bounded () in exact v)) (only parsing).
+  Ltac get_opp_bounded _ := get TAG.opp_bounded.
+  Notation opp_bounded := (ltac:(let v := get_opp_bounded () in exact v)) (only parsing).
+  Ltac get_nonzero_sig _ := get TAG.nonzero_sig.
+  Notation nonzero_sig := (ltac:(let v := get_nonzero_sig () in exact v)) (only parsing).
+End MakeMontgomeryPackage.