Bundle arguments to Barrett Reduction

1 files changed, 64 insertions, 9 deletions

diff --git a/src/ModularArithmetic/BarrettReduction/ZBounded.v b/src/ModularArithmetic/BarrettReduction/ZBounded.v
index 0c4142573..c9414fe01 100644
--- a/src/ModularArithmetic/BarrettReduction/ZBounded.v
+++ b/src/ModularArithmetic/BarrettReduction/ZBounded.v
@@ -16,15 +16,15 @@ Local Open Scope large_zlike_scope.
 Local Open Scope Z_scope.
 
 Section barrett.
-    Context (m b k μ offset : Z)
-            (m_pos : 0 < m)
-            (base_pos : 0 < b)
-            (k_good : m < b^k)
-            (μ_good : μ = b^(2*k) / m) (* [/] is [Z.div], which is truncated *)
-            (offset_nonneg : 0 <= offset)
-            (k_big_enough : offset <= k)
-            (m_small : 3 * m <= b^(k+offset))
-            (m_large : b^(k-offset) <= m + 1).
+  Context (m b k μ offset : Z)
+          (m_pos : 0 < m)
+          (base_pos : 0 < b)
+          (k_good : m < b^k)
+          (μ_good : μ = b^(2*k) / m) (* [/] is [Z.div], which is truncated *)
+          (offset_nonneg : 0 <= offset)
+          (k_big_enough : offset <= k)
+          (m_small : 3 * m <= b^(k+offset))
+          (m_large : b^(k-offset) <= m + 1).
   Context {ops : ZLikeOps (b^(k+offset)) (b^(k-offset)) m} {props : ZLikeProperties ops}
           (μ' : SmallT)
           (μ'_good : small_valid μ')
@@ -45,4 +45,59 @@ Section barrett.
     pull_zlike_decode; cbv zeta; pull_zlike_decode. (* Extra [cbv iota; pull_zlike_decode] to work around bug #4165 (https://coq.inria.fr/bugs/show_bug.cgi?id=4165) in 8.4 *)
     subst pr; split; [ reflexivity | exact _ ].
   Defined.
+
+  Definition barrett_reduce_function : LargeT -> SmallT
+    := Eval cbv [proj1_sig barrett_reduce]
+      in fun x => proj1_sig (barrett_reduce x).
+  Lemma barrett_reduce_correct x
+    : medium_valid x
+      -> decode_small (barrett_reduce_function x) = (decode_large x) mod m
+         /\ small_valid (barrett_reduce_function x).
+  Proof.
+    exact (proj2_sig (barrett_reduce x)).
+  Qed.
 End barrett.
+
+Module BarrettBundled.
+  Class BarrettParameters :=
+    { m : Z;
+      b : Z;
+      k : Z;
+      offset : Z;
+      μ := b ^ (2 * k) / m;
+      ops : ZLikeOps (b ^ (k + offset)) (b ^ (k - offset)) m;
+      μ' : SmallT }.
+  Global Existing Instance ops.
+
+  Class BarrettParametersCorrect {params : BarrettParameters} :=
+    { m_pos : 0 < m;
+      base_pos : 0 < b;
+      offset_nonneg : 0 <= offset;
+      k_big_enough : offset <= k;
+      m_small : 3 * m <= b ^ (k + offset);
+      m_large : b ^ (k - offset) <= m + 1;
+      props : ZLikeProperties ops;
+      μ'_good : small_valid μ';
+      μ'_eq : decode_small μ' = μ }.
+  Global Arguments BarrettParametersCorrect : clear implicits.
+  Global Existing Instance props.
+
+  Module Export functions.
+    Definition barrett_reduce_function_bundled {params : BarrettParameters}
+    : LargeT -> SmallT
+      := barrett_reduce_function m b k offset μ'.
+    Definition barrett_reduce_correct_bundled {params : BarrettParameters} {params_proofs : BarrettParametersCorrect params}
+      : forall x, medium_valid x
+                  -> decode_small (barrett_reduce_function_bundled x) = (decode_large x) mod m
+                     /\ small_valid (barrett_reduce_function_bundled x)
+      := @barrett_reduce_correct
+           m b k μ offset
+           m_pos base_pos eq_refl offset_nonneg
+           k_big_enough m_small m_large
+           ops props μ' μ'_good μ'_eq.
+  End functions.
+End BarrettBundled.
+Export BarrettBundled.functions.
+Global Existing Instance BarrettBundled.ops.
+Global Arguments BarrettBundled.BarrettParametersCorrect : clear implicits.
+Global Existing Instance BarrettBundled.props.