Merge pull request #49 from JasonGross/bounded-z-like

Specify a type of bounded integers for modular arithmetic

4 files changed, 240 insertions, 0 deletions

diff --git a/_CoqProject b/_CoqProject
index 307a752fd..2840c3b91 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -50,10 +50,13 @@ src/ModularArithmetic/PrimeFieldTheorems.v
 src/ModularArithmetic/PseudoMersenneBaseParamProofs.v
 src/ModularArithmetic/PseudoMersenneBaseParams.v
 src/ModularArithmetic/Tutorial.v
+src/ModularArithmetic/ZBounded.v
 src/ModularArithmetic/BarrettReduction/Z.v
+src/ModularArithmetic/BarrettReduction/ZBounded.v
 src/ModularArithmetic/BarrettReduction/ZGeneralized.v
 src/ModularArithmetic/BarrettReduction/ZHandbook.v
 src/ModularArithmetic/Montgomery/Z.v
+src/ModularArithmetic/Montgomery/ZBounded.v
 src/ModularArithmetic/Montgomery/ZProofs.v
 src/Spec/CompleteEdwardsCurve.v
 src/Spec/EdDSA.v
diff --git a/src/ModularArithmetic/BarrettReduction/ZBounded.v b/src/ModularArithmetic/BarrettReduction/ZBounded.v
new file mode 100644
index 000000000..0c4142573
--- /dev/null
+++ b/src/ModularArithmetic/BarrettReduction/ZBounded.v
@@ -0,0 +1,48 @@
+(*** Barrett Reduction *)
+(** This file implements Barrett Reduction on [ZLikeOps].  We follow
+    [BarretReduction/ZHandbook.v]. *)
+Require Import Coq.ZArith.ZArith Coq.Lists.List Coq.Classes.Morphisms Coq.micromega.Psatz.
+Require Import Crypto.ModularArithmetic.BarrettReduction.ZHandbook.
+Require Import Crypto.ModularArithmetic.Pow2Base.
+Require Import Crypto.ModularArithmetic.ExtendedBaseVector.
+Require Import Crypto.ModularArithmetic.ZBounded.
+Require Import Crypto.BaseSystem.
+Require Import Crypto.Util.ZUtil.
+Require Import Crypto.Util.Tactics.
+Require Import Crypto.Util.Notations.
+
+Local Open Scope small_zlike_scope.
+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 {ops : ZLikeOps (b^(k+offset)) (b^(k-offset)) m} {props : ZLikeProperties ops}
+          (μ' : SmallT)
+          (μ'_good : small_valid μ')
+          (μ'_eq : decode_small μ' = μ).
+
+  Definition barrett_reduce : forall x : LargeT,
+      { barrett_reduce : SmallT
+      | medium_valid x
+        -> decode_small barrett_reduce = (decode_large x) mod m
+           /\ small_valid barrett_reduce }.
+  Proof.
+    intro x. evar (pr : SmallT); exists pr. intros x_valid.
+    assert (0 <= decode_large x < b^(k+offset) * b^(k-offset)) by auto using decode_medium_valid.
+    assert (0 <= decode_large x < b^(2 * k)) by (autorewrite with pull_Zpow zsimplify in *; omega).
+    assert ((decode_large x) mod b^(k-offset) < b^(k-offset)) by auto with zarith omega.
+    rewrite (barrett_reduction_small m b (decode_large x) k μ offset) by omega.
+    rewrite <- μ'_eq.
+    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.
+End barrett.
diff --git a/src/ModularArithmetic/Montgomery/ZBounded.v b/src/ModularArithmetic/Montgomery/ZBounded.v
new file mode 100644
index 000000000..9295d5bc4
--- /dev/null
+++ b/src/ModularArithmetic/Montgomery/ZBounded.v
@@ -0,0 +1,43 @@
+(*** Montgomery Multiplication *)
+(** This file implements Montgomery Form, Montgomery Reduction, and
+    Montgomery Multiplication on [ZLikeOps].  We follow [Montgomery/Z.v]. *)
+Require Import Coq.ZArith.ZArith Coq.Lists.List Coq.Classes.Morphisms Coq.micromega.Psatz.
+Require Import Crypto.ModularArithmetic.Montgomery.Z.
+Require Import Crypto.ModularArithmetic.Montgomery.ZProofs.
+Require Import Crypto.ModularArithmetic.Pow2Base.
+Require Import Crypto.ModularArithmetic.ExtendedBaseVector.
+Require Import Crypto.ModularArithmetic.ZBounded.
+Require Import Crypto.BaseSystem.
+Require Import Crypto.Util.ZUtil.
+Require Import Crypto.Util.Tactics.
+Require Import Crypto.Util.Notations.
+
+Local Open Scope small_zlike_scope.
+Local Open Scope large_zlike_scope.
+Local Open Scope Z_scope.
+
+Section montgomery.
+  Context (small_bound modulus : Z) {ops : ZLikeOps small_bound small_bound modulus} {props : ZLikeProperties ops}
+          (modulus' : SmallT)
+          (modulus'_valid : small_valid modulus')
+          (modulus_nonzero : modulus <> 0).
+
+  Definition partial_reduce : forall v : LargeT,
+      { partial_reduce : SmallT
+      | large_valid v
+        -> decode_small partial_reduce = Montgomery.Z.partial_reduce modulus small_bound (decode_small modulus') (decode_large v)
+           /\ small_valid partial_reduce }.
+  Proof.
+    intro T. evar (pr : SmallT); exists pr. intros T_valid.
+    assert (0 <= decode_large T < small_bound * small_bound) by auto using decode_large_valid.
+    assert (0 <= decode_small (Mod_SmallBound T) < small_bound) by auto using decode_small_valid, Mod_SmallBound_valid.
+    assert (0 <= decode_small modulus' < small_bound) by auto using decode_small_valid.
+    assert (0 <= decode_small modulus_digits < small_bound) by auto using decode_small_valid, modulus_digits_valid.
+    assert (0 <= modulus) by apply (modulus_nonneg _).
+    assert (modulus < small_bound) by (rewrite <- modulus_digits_correct; omega).
+    rewrite <- partial_reduce_alt_eq by omega.
+    cbv [Montgomery.Z.partial_reduce Montgomery.Z.partial_reduce_alt Montgomery.Z.prereduce].
+    pull_zlike_decode.
+    subst pr; split; [ reflexivity | exact _ ].
+  Defined.
+End montgomery.
diff --git a/src/ModularArithmetic/ZBounded.v b/src/ModularArithmetic/ZBounded.v
new file mode 100644
index 000000000..def7dcb77
--- /dev/null
+++ b/src/ModularArithmetic/ZBounded.v
@@ -0,0 +1,146 @@
+(*** Bounded ℤ-Like Types *)
+(** This file specifies a ℤ-like type of bounded integers, with
+    operations for Montgomery Reduction and Barrett Reduction. *)
+Require Import Coq.ZArith.ZArith.
+Require Import Crypto.Util.ZUtil.
+Require Import Crypto.Util.Tactics.
+Require Import Crypto.Util.Notations.
+
+Local Open Scope Z_scope.
+
+Class ZLikeOps (small_bound smaller_bound : Z) (modulus : Z) :=
+  {
+    LargeT : Type;
+    SmallT : Type;
+    modulus_digits : SmallT;
+    decode_large : LargeT -> Z;
+    decode_small : SmallT -> Z;
+    Mod_SmallBound : LargeT -> SmallT;
+    DivBy_SmallBound : LargeT -> SmallT;
+    DivBy_SmallerBound : LargeT -> SmallT;
+    Mul : SmallT -> SmallT -> LargeT;
+    CarryAdd : LargeT -> LargeT -> bool * LargeT;
+    CarrySubSmall : SmallT -> SmallT -> bool * SmallT;
+    ConditionalSubtract : bool -> SmallT -> SmallT;
+    ConditionalSubtractModulus : SmallT -> SmallT
+  }.
+
+Delimit Scope small_zlike_scope with small_zlike.
+Delimit Scope large_zlike_scope with large_zlike.
+Local Open Scope small_zlike_scope.
+Local Open Scope large_zlike_scope.
+Local Open Scope Z_scope.
+Bind Scope small_zlike_scope with SmallT.
+Bind Scope large_zlike_scope with LargeT.
+Arguments decode_large (_ _ _)%Z _ _%large_zlike.
+Arguments decode_small (_ _ _)%Z _ _%small_zlike.
+Arguments Mod_SmallBound (_ _ _)%Z _ _%large_zlike.
+Arguments DivBy_SmallBound (_ _ _)%Z _ _%large_zlike.
+Arguments DivBy_SmallerBound (_ _ _)%Z _ _%large_zlike.
+Arguments Mul (_ _ _)%Z _ (_ _)%small_zlike.
+Arguments CarryAdd (_ _ _)%Z _ (_ _)%large_zlike.
+Arguments CarrySubSmall (_ _ _)%Z _ (_ _)%large_zlike.
+Arguments ConditionalSubtract (_ _ _)%Z _ _%bool _%small_zlike.
+Arguments ConditionalSubtractModulus (_ _ _)%Z _ _%small_zlike.
+
+Infix "*" := Mul : large_zlike_scope.
+Notation "x + y" := (snd (CarryAdd x y)) : large_zlike_scope.
+
+Class ZLikeProperties {small_bound smaller_bound modulus : Z} (Zops : ZLikeOps small_bound smaller_bound modulus) :=
+  {
+    large_valid : LargeT -> Prop;
+    medium_valid : LargeT -> Prop;
+    small_valid : SmallT -> Prop;
+    decode_large_valid : forall v, large_valid v -> 0 <= decode_large v < small_bound * small_bound;
+    decode_medium_valid : forall v, medium_valid v -> 0 <= decode_large v < small_bound * smaller_bound;
+    medium_to_large_valid : forall v, medium_valid v -> large_valid v;
+    decode_small_valid : forall v, small_valid v -> 0 <= decode_small v < small_bound;
+    modulus_digits_valid : small_valid modulus_digits;
+    modulus_digits_correct : decode_small modulus_digits = modulus;
+    Mod_SmallBound_valid : forall v, large_valid v -> small_valid (Mod_SmallBound v);
+    Mod_SmallBound_correct
+    : forall v, large_valid v -> decode_small (Mod_SmallBound v) = decode_large v mod small_bound;
+    DivBy_SmallBound_valid : forall v, large_valid v -> small_valid (DivBy_SmallBound v);
+    DivBy_SmallBound_correct
+    : forall v, large_valid v -> decode_small (DivBy_SmallBound v) = decode_large v / small_bound;
+    DivBy_SmallerBound_valid : forall v, medium_valid v -> small_valid (DivBy_SmallerBound v);
+    DivBy_SmallerBound_correct
+    : forall v, medium_valid v -> decode_small (DivBy_SmallerBound v) = decode_large v / smaller_bound;
+    Mul_valid : forall x y, small_valid x -> small_valid y -> large_valid (Mul x y);
+    Mul_correct
+    : forall x y, small_valid x -> small_valid y -> decode_large (Mul x y) = decode_small x * decode_small y;
+    CarryAdd_valid : forall x y, large_valid x -> large_valid y -> large_valid (snd (CarryAdd x y));
+    CarryAdd_correct_fst
+    : forall x y, large_valid x -> large_valid y -> fst (CarryAdd x y) = (small_bound * small_bound <=? decode_large x + decode_large y);
+    CarryAdd_correct_snd
+    : forall x y, large_valid x -> large_valid y -> decode_large (snd (CarryAdd x y)) = (decode_large x + decode_large y) mod (small_bound * small_bound);
+    CarrySubSmall_valid : forall x y, small_valid x -> small_valid y -> small_valid (snd (CarrySubSmall x y));
+    CarrySubSmall_correct_fst
+    : forall x y, small_valid x -> small_valid y -> fst (CarrySubSmall x y) = (decode_small x - decode_small y <? 0);
+    CarrySubSmall_correct_snd
+    : forall x y, small_valid x -> small_valid y -> decode_small (snd (CarrySubSmall x y)) = (decode_small x - decode_small y) mod small_bound;
+    ConditionalSubtract_valid : forall b x, small_valid x  -> small_valid (ConditionalSubtract b x);
+    ConditionalSubtract_correct
+    : forall b x, small_valid x -> decode_small (ConditionalSubtract b x)
+                                 = if b then (decode_small x - decode_small modulus_digits) mod small_bound else decode_small x;
+    ConditionalSubtractModulus_valid : forall x, small_valid x -> small_valid (ConditionalSubtractModulus x);
+    ConditionalSubtractModulus_correct
+    : forall x, small_valid x -> decode_small (ConditionalSubtractModulus x)
+                                 = if (decode_small x <? decode_small modulus_digits) then decode_small x else decode_small x - decode_small modulus_digits
+  }.
+
+Arguments ZLikeProperties [small_bound smaller_bound modulus] Zops, small_bound smaller_bound modulus {Zops}.
+
+Existing Class large_valid.
+Existing Class medium_valid.
+Existing Class small_valid.
+Existing Instances Mod_SmallBound_valid DivBy_SmallerBound_valid DivBy_SmallBound_valid Mul_valid CarryAdd_valid CarrySubSmall_valid ConditionalSubtract_valid ConditionalSubtractModulus_valid modulus_digits_valid medium_to_large_valid.
+
+Lemma modulus_nonneg {small_bound smaller_bound modulus} (Zops : ZLikeOps small_bound smaller_bound modulus) {_ : ZLikeProperties Zops} : 0 <= modulus.
+Proof.
+  pose proof (decode_small_valid _ modulus_digits_valid) as H.
+  rewrite modulus_digits_correct in H.
+  omega.
+Qed.
+
+Create HintDb push_zlike_decode discriminated.
+Create HintDb pull_zlike_decode discriminated.
+Hint Rewrite @Mod_SmallBound_correct @DivBy_SmallBound_correct @DivBy_SmallerBound_correct @Mul_correct @CarryAdd_correct_fst @CarryAdd_correct_snd @CarrySubSmall_correct_fst @CarrySubSmall_correct_snd  @ConditionalSubtract_correct @ConditionalSubtractModulus_correct @modulus_digits_correct using solve [ typeclasses eauto ] : push_zlike_decode.
+Hint Rewrite <- @Mod_SmallBound_correct @DivBy_SmallBound_correct @DivBy_SmallerBound_correct @Mul_correct @CarryAdd_correct_fst @CarryAdd_correct_snd @CarrySubSmall_correct_fst @CarrySubSmall_correct_snd @ConditionalSubtract_correct @ConditionalSubtractModulus_correct @modulus_digits_correct using solve [ typeclasses eauto ] : pull_zlike_decode.
+
+Ltac get_modulus :=
+  match goal with
+  | [ _ : ZLikeOps _ _ ?modulus |- _ ] => modulus
+  end.
+
+Ltac push_zlike_decode :=
+  let modulus := get_modulus in
+  repeat first [ erewrite !Mod_SmallBound_correct by typeclasses eauto
+               | erewrite !DivBy_SmallBound_correct by typeclasses eauto
+               | erewrite !DivBy_SmallerBound_correct by typeclasses eauto
+               | erewrite !Mul_correct by typeclasses eauto
+               | erewrite !CarryAdd_correct_fst by typeclasses eauto
+               | erewrite !CarryAdd_correct_snd by typeclasses eauto
+               | erewrite !CarrySubSmall_correct_fst by typeclasses eauto
+               | erewrite !CarrySubSmall_correct_snd by typeclasses eauto
+               | erewrite !ConditionalSubtract_correct by typeclasses eauto
+               | erewrite !ConditionalSubtractModulus_correct by typeclasses eauto
+               | erewrite !(@modulus_digits_correct _ modulus _ _) by typeclasses eauto ].
+Ltac pull_zlike_decode :=
+  let modulus := get_modulus in
+  repeat first [ match goal with
+                 | [ |- context G[modulus] ]
+                   => let G' := context G[decode_small modulus_digits] in
+                      cut G'; [ rewrite !modulus_digits_correct by typeclasses eauto; exact (fun x => x) | ]
+                 end
+               | erewrite <- !Mod_SmallBound_correct by typeclasses eauto
+               | erewrite <- !DivBy_SmallBound_correct by typeclasses eauto
+               | erewrite <- !DivBy_SmallerBound_correct by typeclasses eauto
+               | erewrite <- !Mul_correct by typeclasses eauto
+               | erewrite <- !CarryAdd_correct_fst by typeclasses eauto
+               | erewrite <- !CarryAdd_correct_snd by typeclasses eauto
+               | erewrite <- !ConditionalSubtract_correct by typeclasses eauto
+               | erewrite <- !CarrySubSmall_correct_fst by typeclasses eauto
+               | erewrite <- !CarrySubSmall_correct_snd by typeclasses eauto
+               | erewrite <- !ConditionalSubtractModulus_correct by typeclasses eauto
+               | erewrite <- !(@modulus_digits_correct _ modulus _ _) by typeclasses eauto ].