From c0fe35f49d61207d16c6db79936e38edf9661a49 Mon Sep 17 00:00:00 2001
From: jadep <jadep@mit.edu>
Date: Mon, 1 Apr 2019 05:38:38 -0400
Subject: rename some things

---
 src/Fancy/Montgomery256.v                          |   3 +-
 src/PushButtonSynthesis/FancyMontgomeryReduction.v | 188 +++++++++++++++++++++
 .../FancyMontgomeryReductionReificationCache.v     |  24 +++
 src/PushButtonSynthesis/MontgomeryReduction.v      | 188 ---------------------
 .../MontgomeryReductionReificationCache.v          |  23 ---
 5 files changed, 213 insertions(+), 213 deletions(-)
 create mode 100644 src/PushButtonSynthesis/FancyMontgomeryReduction.v
 create mode 100644 src/PushButtonSynthesis/FancyMontgomeryReductionReificationCache.v
 delete mode 100644 src/PushButtonSynthesis/MontgomeryReduction.v
 delete mode 100644 src/PushButtonSynthesis/MontgomeryReductionReificationCache.v

(limited to 'src')

diff --git a/src/Fancy/Montgomery256.v b/src/Fancy/Montgomery256.v
index 2c692fb30..ee761cba9 100644
--- a/src/Fancy/Montgomery256.v
+++ b/src/Fancy/Montgomery256.v
@@ -7,8 +7,7 @@ Require Import Crypto.Fancy.Prod.
 Require Import Crypto.Fancy.Spec.
 Require Import Crypto.Language. Import Language.Compilers.
 Require Import Crypto.LanguageWf.
-Require Import Crypto.Arithmetic. (* For the MontgomeryReduction Module *)
-Require Import Crypto.PushButtonSynthesis.MontgomeryReduction.
+Require Import Crypto.PushButtonSynthesis.FancyMontgomeryReduction.
 Require Import Crypto.Util.Tactics.BreakMatch.
 Require Import Crypto.Util.ZUtil.EquivModulo.
 Require Import Crypto.Util.ZUtil.Tactics.LtbToLt.
diff --git a/src/PushButtonSynthesis/FancyMontgomeryReduction.v b/src/PushButtonSynthesis/FancyMontgomeryReduction.v
new file mode 100644
index 000000000..2a64fdebd
--- /dev/null
+++ b/src/PushButtonSynthesis/FancyMontgomeryReduction.v
@@ -0,0 +1,188 @@
+(** * Push-Button Synthesis of Montgomery Reduction *)
+Require Import Coq.Strings.String.
+Require Import Coq.ZArith.ZArith.
+Require Import Coq.micromega.Lia.
+Require Import Coq.Lists.List.
+Require Import Coq.derive.Derive.
+Require Import Crypto.Util.ErrorT.
+Require Import Crypto.Util.ListUtil.
+Require Import Crypto.Util.ZRange.
+Require Import Crypto.Util.ZUtil.Div.
+Require Import Crypto.Util.ZUtil.ModInv.
+Require Import Crypto.Util.ZUtil.Tactics.LtbToLt.
+Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo.
+Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall.
+Require Import Crypto.Language.
+Require Import Crypto.CStringification.
+Require Import Crypto.Arithmetic.Core.
+Require Import Crypto.Arithmetic.MongomeryReduction.
+Require Import Crypto.BoundsPipeline.
+Require Import Crypto.COperationSpecifications.
+Require Import Crypto.Fancy.Compiler.
+Require Import Crypto.PushButtonSynthesis.ReificationCache.
+Require Import Crypto.PushButtonSynthesis.Primitives.
+Require Import Crypto.PushButtonSynthesis.FancyMontgomeryReductionReificationCache.
+Require Import Crypto.PushButtonSynthesis.InvertHighLow.
+Require Import Crypto.PushButtonSynthesis.LegacySynthesisTactics.
+Import ListNotations.
+Local Open Scope Z_scope. Local Open Scope list_scope. Local Open Scope bool_scope.
+
+Import
+  Language.Compilers
+  CStringification.Compilers.
+Import Compilers.defaults.
+
+Import COperationSpecifications.Primitives.
+
+Import COperationSpecifications.MontgomeryReduction.
+
+Import Associational Positional MontgomeryReduction.
+
+Local Set Keyed Unification. (* needed for making [autorewrite] fast, c.f. COQBUG(https://github.com/coq/coq/issues/9283) *)
+
+Local Opaque reified_montred_gen. (* needed for making [autorewrite] not take a very long time *)
+
+Section rmontred.
+  Context (N R N' : Z) (n : nat)
+          (machine_wordsize : Z).
+
+  Let value_range := r[0 ~> (2^machine_wordsize - 1)%Z]%zrange.
+  Let flag_range := r[0 ~> 1]%zrange.
+  Let bound := Some value_range.
+  Let consts_list := [N; N'].
+  Let R' := match Z.modinv R N with
+            | Some R' => R'
+            | None => 0
+            end.
+
+  Definition possible_values_of_machine_wordsize
+    := [1; machine_wordsize / 2; machine_wordsize; 2 * machine_wordsize]%Z.
+  Local Arguments possible_values_of_machine_wordsize / .
+
+  Let possible_values := possible_values_of_machine_wordsize.
+
+  Let fancy_args
+    := (Some {| Pipeline.invert_low log2wordsize := invert_low log2wordsize consts_list;
+                Pipeline.invert_high log2wordsize := invert_high log2wordsize consts_list;
+                Pipeline.value_range := value_range;
+                Pipeline.flag_range := flag_range |}).
+
+  Lemma fancy_args_good
+    : match fancy_args with
+      | Some {| Pipeline.invert_low := il ; Pipeline.invert_high := ih |}
+        => (forall s v v' : Z, il s v = Some v' -> v = Z.land v' (2^(s/2)-1))
+           /\ (forall s v v' : Z, ih s v = Some v' -> v = Z.shiftr v' (s/2))
+      | None => True
+      end.
+  Proof.
+    cbv [fancy_args invert_low invert_high constant_to_scalar constant_to_scalar_single consts_list fold_right];
+      split; intros; break_innermost_match_hyps; Z.ltb_to_lt; subst; congruence.
+  Qed.
+  Local Hint Extern 1 => apply fancy_args_good: typeclass_instances. (* This is a kludge *)
+
+  (** Note: If you change the name or type signature of this
+        function, you will need to update the code in CLI.v *)
+  Definition check_args {T} (res : Pipeline.ErrorT T)
+    : Pipeline.ErrorT T
+    := fold_right
+         (fun '(b, e) k => if b:bool then Error e else k)
+         res
+         [
+            ((negb (1 <? R))%Z, Pipeline.Value_not_ltZ "R ≤ 1" 1 R);
+            ((n =? 0)%nat, Pipeline.Values_not_provably_distinctZ "n = 0" (Z.of_nat n) 0);
+            ((R' =? 0)%Z, Pipeline.No_modular_inverse "R⁻¹ mod N" R N);
+            (negb ((R * R') mod N =? 1 mod N)%Z, Pipeline.Values_not_provably_equalZ "(R * R') mod N ≠ 1 mod N" ((R * R') mod N) (1 mod N));
+            (negb ((N * N') mod R =? (-1) mod R)%Z, Pipeline.Values_not_provably_equalZ "(N * N') mod R ≠ (-1) mod R" ((N * N') mod R) ((-1) mod R));
+            (negb (2 ^ machine_wordsize =? R)%Z, Pipeline.Values_not_provably_equalZ "2^machine_wordsize ≠ R" (2^machine_wordsize) R);
+            ((negb (0 <? N))%Z, Pipeline.Value_not_ltZ "N ≤ 0" 0 N);
+            ((negb (N <? R))%Z, Pipeline.Value_not_ltZ "R ≤ N" R N);
+            ((negb (0 <=? N'))%Z, Pipeline.Value_not_leZ "N' < 0" 0 N');
+            ((negb (N' <? R))%Z, Pipeline.Value_not_ltZ "R ≤ N'" R N');
+            ((negb (2 <=? machine_wordsize))%Z, Pipeline.Value_not_leZ "machine_wordsize < 2" 2 machine_wordsize)].
+
+  Local Arguments Z.mul !_ !_.
+  Local Ltac use_curve_good_t :=
+    repeat first [ assumption
+                 | progress cbv [EquivModulo.Z.equiv_modulo]
+                 | progress rewrite ?Z.mul_0_r, ?Pos.mul_1_r, ?Z.mul_1_r in *
+                 | reflexivity
+                 | lia
+                 | progress cbn in *
+                 | progress intros
+                 | solve [ auto with zarith ]
+                 | rewrite Z.log2_pow2 by use_curve_good_t ].
+
+  Context (curve_good : check_args (Success tt) = Success tt).
+
+  Lemma use_curve_good
+    : 0 <= N < R
+      /\ 0 <= N' < R
+      /\ N <> 0
+      /\ R > 1
+      /\ EquivModulo.Z.equiv_modulo R (N * N') (-1)
+      /\ EquivModulo.Z.equiv_modulo N (R * R') 1
+      /\ n <> 0%nat
+      /\ 2 <= machine_wordsize
+      /\ 2 ^ machine_wordsize = R.
+  Proof using curve_good.
+    clear -curve_good.
+    cbv [check_args fold_right] in curve_good.
+    break_innermost_match_hyps; try discriminate.
+    rewrite Bool.negb_false_iff in *.
+    Z.ltb_to_lt.
+    rewrite NPeano.Nat.eqb_neq in *.
+    intros.
+    repeat apply conj.
+    { use_curve_good_t. }
+    { use_curve_good_t. }
+    { use_curve_good_t. }
+    { use_curve_good_t. }
+    { use_curve_good_t. }
+    { use_curve_good_t. }
+    { use_curve_good_t. }
+    { use_curve_good_t. }
+    { use_curve_good_t. }
+    { use_curve_good_t. }
+    { use_curve_good_t. }
+  Qed.
+
+  Definition montred
+    := Pipeline.BoundsPipeline
+         false (* subst01 *)
+         fancy_args (* fancy *)
+         possible_values
+         (reified_montred_gen
+            @ GallinaReify.Reify N @ GallinaReify.Reify R @ GallinaReify.Reify N' @ GallinaReify.Reify machine_wordsize)
+         (bound, (bound, tt))
+         bound.
+
+  Definition smontred (prefix : string)
+    : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos))
+    := Eval cbv beta in
+        FromPipelineToString
+          prefix "montred" montred
+          (fun _ _ _ => @nil string).
+
+  Local Ltac solve_montred_preconditions :=
+    repeat first [ lia
+           | apply use_curve_good
+           | progress (push_Zmod; pull_Zmod)
+           | progress autorewrite with zsimplify_fast
+           | rewrite Z.div_add' by lia
+           | rewrite Z.div_small by lia
+           | progress Z.rewrite_mod_small ].
+
+  Local Strategy -100 [montred]. (* needed for making Qed not take forever *)
+  Local Strategy -100 [montred' reified_montred_gen]. (* needed for making prove_correctness not take forever *)
+  Lemma montred_correct res (Hres : montred = Success res)
+    : montred_correct N R R' (expr.Interp (@ident.gen_interp cast_oor) res).
+  Proof using n curve_good.
+    cbv [montred_correct]; intros.
+    rewrite <- MontgomeryReduction.montred'_correct with (R:=R) (N':=N') (Zlog2R:=machine_wordsize) (n:=n) (lo:=lo) (hi:=hi) by solve_montred_preconditions.
+    prove_correctness' ltac:(fun _ => idtac) use_curve_good.
+    { cbv [ZRange.type.base.option.is_bounded_by ZRange.type.base.is_bounded_by bound is_bounded_by_bool value_range upper lower].
+      rewrite Bool.andb_true_iff, !Z.leb_le. lia. }
+    { cbv [ZRange.type.base.option.is_bounded_by ZRange.type.base.is_bounded_by bound is_bounded_by_bool value_range upper lower].
+      rewrite Bool.andb_true_iff, !Z.leb_le. lia. }
+  Qed.
+End rmontred.
diff --git a/src/PushButtonSynthesis/FancyMontgomeryReductionReificationCache.v b/src/PushButtonSynthesis/FancyMontgomeryReductionReificationCache.v
new file mode 100644
index 000000000..7a475a53a
--- /dev/null
+++ b/src/PushButtonSynthesis/FancyMontgomeryReductionReificationCache.v
@@ -0,0 +1,24 @@
+(** * Push-Button Snthesis of fancy mongomery reduction : Reification Cache *)
+Require Import Coq.ZArith.ZArith.
+Require Import Coq.derive.Derive.
+Require Import Crypto.Arithmetic.Core.
+Require Import Crypto.Arithmetic.FancyMontgomeryReduction.
+Require Import Crypto.PushButtonSynthesis.ReificationCache.
+Local Open Scope Z_scope.
+
+Import Associational Positional.
+
+Local Set Keyed Unification. (* needed for making [autorewrite] fast, c.f. COQBUG(https://github.com/coq/coq/issues/9283) *)
+
+Module Export MontgomeryReduction.
+  Derive reified_montred_gen
+         SuchThat (is_reification_of reified_montred_gen montred')
+         As reified_montred_gen_correct.
+  Proof. Time cache_reify (). Time Qed.
+  Module Export ReifyHints.
+    Hint Extern 1 (_ = _) => apply_cached_reification montred' (proj1 reified_montred_gen_correct) : reify_cache_gen.
+    Hint Immediate (proj2 reified_montred_gen_correct) : wf_gen_cache.
+    Hint Rewrite (proj1 reified_montred_gen_correct) : interp_gen_cache.
+  End ReifyHints.
+  Local Opaque reified_montred_gen. (* needed for making [autorewrite] not take a very long time *)
+End MontgomeryReduction.
diff --git a/src/PushButtonSynthesis/MontgomeryReduction.v b/src/PushButtonSynthesis/MontgomeryReduction.v
deleted file mode 100644
index d784ebc3c..000000000
--- a/src/PushButtonSynthesis/MontgomeryReduction.v
+++ /dev/null
@@ -1,188 +0,0 @@
-(** * Push-Button Synthesis of Montgomery Reduction *)
-Require Import Coq.Strings.String.
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.micromega.Lia.
-Require Import Coq.Lists.List.
-Require Import Coq.derive.Derive.
-Require Import Crypto.Util.ErrorT.
-Require Import Crypto.Util.ListUtil.
-Require Import Crypto.Util.ZRange.
-Require Import Crypto.Util.ZUtil.Div.
-Require Import Crypto.Util.ZUtil.ModInv.
-Require Import Crypto.Util.ZUtil.Tactics.LtbToLt.
-Require Import Crypto.Util.ZUtil.Tactics.PullPush.Modulo.
-Require Import Crypto.Util.ZUtil.Tactics.RewriteModSmall.
-Require Import Crypto.Language.
-Require Import Crypto.CStringification.
-Require Import Crypto.Arithmetic.Core.
-Require Import Crypto.Arithmetic.MongomeryReduction.
-Require Import Crypto.BoundsPipeline.
-Require Import Crypto.COperationSpecifications.
-Require Import Crypto.Fancy.Compiler.
-Require Import Crypto.PushButtonSynthesis.ReificationCache.
-Require Import Crypto.PushButtonSynthesis.Primitives.
-Require Import Crypto.PushButtonSynthesis.MontgomeryReductionReificationCache.
-Require Import Crypto.PushButtonSynthesis.InvertHighLow.
-Require Import Crypto.PushButtonSynthesis.LegacySynthesisTactics.
-Import ListNotations.
-Local Open Scope Z_scope. Local Open Scope list_scope. Local Open Scope bool_scope.
-
-Import
-  Language.Compilers
-  CStringification.Compilers.
-Import Compilers.defaults.
-
-Import COperationSpecifications.Primitives.
-
-Import COperationSpecifications.MontgomeryReduction.
-
-Import Associational Positional MontgomeryReduction.
-
-Local Set Keyed Unification. (* needed for making [autorewrite] fast, c.f. COQBUG(https://github.com/coq/coq/issues/9283) *)
-
-Local Opaque reified_montred_gen. (* needed for making [autorewrite] not take a very long time *)
-
-Section rmontred.
-  Context (N R N' : Z) (n : nat)
-          (machine_wordsize : Z).
-
-  Let value_range := r[0 ~> (2^machine_wordsize - 1)%Z]%zrange.
-  Let flag_range := r[0 ~> 1]%zrange.
-  Let bound := Some value_range.
-  Let consts_list := [N; N'].
-  Let R' := match Z.modinv R N with
-            | Some R' => R'
-            | None => 0
-            end.
-
-  Definition possible_values_of_machine_wordsize
-    := [1; machine_wordsize / 2; machine_wordsize; 2 * machine_wordsize]%Z.
-  Local Arguments possible_values_of_machine_wordsize / .
-
-  Let possible_values := possible_values_of_machine_wordsize.
-
-  Let fancy_args
-    := (Some {| Pipeline.invert_low log2wordsize := invert_low log2wordsize consts_list;
-                Pipeline.invert_high log2wordsize := invert_high log2wordsize consts_list;
-                Pipeline.value_range := value_range;
-                Pipeline.flag_range := flag_range |}).
-
-  Lemma fancy_args_good
-    : match fancy_args with
-      | Some {| Pipeline.invert_low := il ; Pipeline.invert_high := ih |}
-        => (forall s v v' : Z, il s v = Some v' -> v = Z.land v' (2^(s/2)-1))
-           /\ (forall s v v' : Z, ih s v = Some v' -> v = Z.shiftr v' (s/2))
-      | None => True
-      end.
-  Proof.
-    cbv [fancy_args invert_low invert_high constant_to_scalar constant_to_scalar_single consts_list fold_right];
-      split; intros; break_innermost_match_hyps; Z.ltb_to_lt; subst; congruence.
-  Qed.
-  Local Hint Extern 1 => apply fancy_args_good: typeclass_instances. (* This is a kludge *)
-
-  (** Note: If you change the name or type signature of this
-        function, you will need to update the code in CLI.v *)
-  Definition check_args {T} (res : Pipeline.ErrorT T)
-    : Pipeline.ErrorT T
-    := fold_right
-         (fun '(b, e) k => if b:bool then Error e else k)
-         res
-         [
-            ((negb (1 <? R))%Z, Pipeline.Value_not_ltZ "R ≤ 1" 1 R);
-            ((n =? 0)%nat, Pipeline.Values_not_provably_distinctZ "n = 0" (Z.of_nat n) 0);
-            ((R' =? 0)%Z, Pipeline.No_modular_inverse "R⁻¹ mod N" R N);
-            (negb ((R * R') mod N =? 1 mod N)%Z, Pipeline.Values_not_provably_equalZ "(R * R') mod N ≠ 1 mod N" ((R * R') mod N) (1 mod N));
-            (negb ((N * N') mod R =? (-1) mod R)%Z, Pipeline.Values_not_provably_equalZ "(N * N') mod R ≠ (-1) mod R" ((N * N') mod R) ((-1) mod R));
-            (negb (2 ^ machine_wordsize =? R)%Z, Pipeline.Values_not_provably_equalZ "2^machine_wordsize ≠ R" (2^machine_wordsize) R);
-            ((negb (0 <? N))%Z, Pipeline.Value_not_ltZ "N ≤ 0" 0 N);
-            ((negb (N <? R))%Z, Pipeline.Value_not_ltZ "R ≤ N" R N);
-            ((negb (0 <=? N'))%Z, Pipeline.Value_not_leZ "N' < 0" 0 N');
-            ((negb (N' <? R))%Z, Pipeline.Value_not_ltZ "R ≤ N'" R N');
-            ((negb (2 <=? machine_wordsize))%Z, Pipeline.Value_not_leZ "machine_wordsize < 2" 2 machine_wordsize)].
-
-  Local Arguments Z.mul !_ !_.
-  Local Ltac use_curve_good_t :=
-    repeat first [ assumption
-                 | progress cbv [EquivModulo.Z.equiv_modulo]
-                 | progress rewrite ?Z.mul_0_r, ?Pos.mul_1_r, ?Z.mul_1_r in *
-                 | reflexivity
-                 | lia
-                 | progress cbn in *
-                 | progress intros
-                 | solve [ auto with zarith ]
-                 | rewrite Z.log2_pow2 by use_curve_good_t ].
-
-  Context (curve_good : check_args (Success tt) = Success tt).
-
-  Lemma use_curve_good
-    : 0 <= N < R
-      /\ 0 <= N' < R
-      /\ N <> 0
-      /\ R > 1
-      /\ EquivModulo.Z.equiv_modulo R (N * N') (-1)
-      /\ EquivModulo.Z.equiv_modulo N (R * R') 1
-      /\ n <> 0%nat
-      /\ 2 <= machine_wordsize
-      /\ 2 ^ machine_wordsize = R.
-  Proof using curve_good.
-    clear -curve_good.
-    cbv [check_args fold_right] in curve_good.
-    break_innermost_match_hyps; try discriminate.
-    rewrite Bool.negb_false_iff in *.
-    Z.ltb_to_lt.
-    rewrite NPeano.Nat.eqb_neq in *.
-    intros.
-    repeat apply conj.
-    { use_curve_good_t. }
-    { use_curve_good_t. }
-    { use_curve_good_t. }
-    { use_curve_good_t. }
-    { use_curve_good_t. }
-    { use_curve_good_t. }
-    { use_curve_good_t. }
-    { use_curve_good_t. }
-    { use_curve_good_t. }
-    { use_curve_good_t. }
-    { use_curve_good_t. }
-  Qed.
-
-  Definition montred
-    := Pipeline.BoundsPipeline
-         false (* subst01 *)
-         fancy_args (* fancy *)
-         possible_values
-         (reified_montred_gen
-            @ GallinaReify.Reify N @ GallinaReify.Reify R @ GallinaReify.Reify N' @ GallinaReify.Reify machine_wordsize)
-         (bound, (bound, tt))
-         bound.
-
-  Definition smontred (prefix : string)
-    : string * (Pipeline.ErrorT (list string * ToString.C.ident_infos))
-    := Eval cbv beta in
-        FromPipelineToString
-          prefix "montred" montred
-          (fun _ _ _ => @nil string).
-
-  Local Ltac solve_montred_preconditions :=
-    repeat first [ lia
-           | apply use_curve_good
-           | progress (push_Zmod; pull_Zmod)
-           | progress autorewrite with zsimplify_fast
-           | rewrite Z.div_add' by lia
-           | rewrite Z.div_small by lia
-           | progress Z.rewrite_mod_small ].
-
-  Local Strategy -100 [montred]. (* needed for making Qed not take forever *)
-  Local Strategy -100 [montred' reified_montred_gen]. (* needed for making prove_correctness not take forever *)
-  Lemma montred_correct res (Hres : montred = Success res)
-    : montred_correct N R R' (expr.Interp (@ident.gen_interp cast_oor) res).
-  Proof using n curve_good.
-    cbv [montred_correct]; intros.
-    rewrite <- MontgomeryReduction.montred'_correct with (R:=R) (N':=N') (Zlog2R:=machine_wordsize) (n:=n) (lo:=lo) (hi:=hi) by solve_montred_preconditions.
-    prove_correctness' ltac:(fun _ => idtac) use_curve_good.
-    { cbv [ZRange.type.base.option.is_bounded_by ZRange.type.base.is_bounded_by bound is_bounded_by_bool value_range upper lower].
-      rewrite Bool.andb_true_iff, !Z.leb_le. lia. }
-    { cbv [ZRange.type.base.option.is_bounded_by ZRange.type.base.is_bounded_by bound is_bounded_by_bool value_range upper lower].
-      rewrite Bool.andb_true_iff, !Z.leb_le. lia. }
-  Qed.
-End rmontred.
diff --git a/src/PushButtonSynthesis/MontgomeryReductionReificationCache.v b/src/PushButtonSynthesis/MontgomeryReductionReificationCache.v
deleted file mode 100644
index 80af335df..000000000
--- a/src/PushButtonSynthesis/MontgomeryReductionReificationCache.v
+++ /dev/null
@@ -1,23 +0,0 @@
-(** * Push-Button Synthesis of Saturated Solinas: Reification Cache *)
-Require Import Coq.ZArith.ZArith.
-Require Import Coq.derive.Derive.
-Require Import Crypto.Arithmetic.FancyMontgomeryReduction.
-Require Import Crypto.PushButtonSynthesis.ReificationCache.
-Local Open Scope Z_scope.
-
-Import Associational Positional Arithmetic.MontgomeryReduction.
-
-Local Set Keyed Unification. (* needed for making [autorewrite] fast, c.f. COQBUG(https://github.com/coq/coq/issues/9283) *)
-
-Module Export MontgomeryReduction.
-  Derive reified_montred_gen
-         SuchThat (is_reification_of reified_montred_gen montred')
-         As reified_montred_gen_correct.
-  Proof. Time cache_reify (). Time Qed.
-  Module Export ReifyHints.
-    Hint Extern 1 (_ = _) => apply_cached_reification montred' (proj1 reified_montred_gen_correct) : reify_cache_gen.
-    Hint Immediate (proj2 reified_montred_gen_correct) : wf_gen_cache.
-    Hint Rewrite (proj1 reified_montred_gen_correct) : interp_gen_cache.
-  End ReifyHints.
-  Local Opaque reified_montred_gen. (* needed for making [autorewrite] not take a very long time *)
-End MontgomeryReduction.
-- 
cgit v1.2.3