rewrote Testbit and factored out some necessary lemmas about 'uniform' bases (bases that are repeats of the same power of 2) into Pow2Base

4 files changed, 158 insertions, 53 deletions

diff --git a/src/ModularArithmetic/ExtendedBaseVector.v b/src/ModularArithmetic/ExtendedBaseVector.v
index 2a06d9c41..d4df6040f 100644
--- a/src/ModularArithmetic/ExtendedBaseVector.v
+++ b/src/ModularArithmetic/ExtendedBaseVector.v
@@ -3,7 +3,10 @@ Require Import List.
 Require Import Crypto.Util.ListUtil Crypto.Util.CaseUtil Crypto.Util.ZUtil.
 Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
 Require Import VerdiTactics.
-Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParams Crypto.ModularArithmetic.PseudoMersenneBaseParamProofs.
+Require Import Crypto.ModularArithmetic.Pow2Base.
+Require Import Crypto.ModularArithmetic.Pow2BaseProofs.
+Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParams.
+Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParamProofs.
 Require Crypto.BaseSystem.
 Local Open Scope Z_scope.
 
@@ -120,15 +123,12 @@ Section ExtendedBaseVector.
     unfold ext_base in *.
     rewrite app_length in H; rewrite map_length in H.
     repeat rewrite nth_default_app.
-    destruct (lt_dec i (length base));
-      destruct (lt_dec j (length base));
-      destruct (lt_dec (i + j) (length base));
-      try omega.
+    repeat break_if; try omega.
     { (* i < length base, j < length base, i + j < length base *)
-      apply BaseSystem.base_good; auto.
+      auto using BaseSystem.base_good.
     } { (* i < length base, j < length base, i + j >= length base *)
       rewrite (map_nth_default _ _ _ _ 0) by omega.
-      apply base_matches_modulus; omega.
+      apply (base_matches_modulus i j); rewrite <-base_length by auto using limb_widths_nonneg; omega.
     } { (* i < length base, j >= length base, i + j >= length base *)
       do 2 rewrite map_nth_default_base_high by omega.
       remember (j - length base)%nat as j'.
diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v
index c59e04ca6..7e33ab20f 100644
--- a/src/ModularArithmetic/ModularBaseSystemProofs.v
+++ b/src/ModularArithmetic/ModularBaseSystemProofs.v
@@ -2103,4 +2103,4 @@ Section CanonicalizationProofs.
     eapply minimal_rep_unique; eauto; rewrite freeze_length; assumption.
   Qed.
 
-End CanonicalizationProofs.
+End CanonicalizationProofs.
\ No newline at end of file
diff --git a/src/ModularArithmetic/Pow2BaseProofs.v b/src/ModularArithmetic/Pow2BaseProofs.v
index 1504ca0df..7538781c0 100644
--- a/src/ModularArithmetic/Pow2BaseProofs.v
+++ b/src/ModularArithmetic/Pow2BaseProofs.v
@@ -125,6 +125,28 @@ Section Pow2BaseProofs.
      congruence.
    Qed.
 
+   Lemma base_positive : forall b : Z, In b {base} -> b > 0.
+   Proof.
+     intros b In_b_base.
+     apply In_nth_error_value in In_b_base.
+     destruct In_b_base as [i nth_err_b].
+     apply nth_error_subst in nth_err_b.
+     rewrite nth_err_b.
+     apply Z.gt_lt_iff.
+     apply Z.pow_pos_nonneg; omega || auto using sum_firstn_limb_widths_nonneg.
+   Qed.
+
+   Lemma b0_1 : forall x : Z, limb_widths <> nil -> nth_default x {base} 0 = 1.
+   Proof.
+     case_eq limb_widths; intros; [congruence | reflexivity].
+   Qed.
+
+  Lemma base_from_limb_widths_cons : forall l0 l,
+    base_from_limb_widths (l0 :: l) = 1 :: map (Z.mul (two_p l0)) (base_from_limb_widths l).
+  Proof.
+    reflexivity.
+  Qed.
+
 End Pow2BaseProofs.
 
 Section BitwiseDecodeEncode.
@@ -192,6 +214,22 @@ Section BitwiseDecodeEncode.
     reflexivity.
   Qed.
 
+  Lemma decode_bitwise'_nil : forall i,
+    decode_bitwise' limb_widths nil i 0 = 0.
+  Proof.
+    induction i; intros.
+    + reflexivity.
+    + cbv [decode_bitwise'].
+      rewrite nth_default_nil, Z.shiftl_0_l.
+      apply IHi.
+  Qed.
+
+  Lemma decode_bitwise_nil : decode_bitwise limb_widths nil = 0.
+  Proof.
+    cbv [decode_bitwise].
+    apply decode_bitwise'_nil.
+  Qed.
+
   Lemma decode_bitwise'_succ : forall us i acc, bounded limb_widths us ->
     decode_bitwise' limb_widths us (S i) acc =
     decode_bitwise' limb_widths us i (acc * (2 ^ w[i]) + nth_default 0 us i).
@@ -253,7 +291,7 @@ Section BitwiseDecodeEncode.
     + simpl.
       destruct (lt_dec i (length limb_widths)).
       - rewrite IHc by omega.
-        do 2 (rewrite skipn_nth_default with (n := i) (d := 0) by (rewrite <-?base_length; omega)).
+        do 2 (rewrite skipn_nth_default with (n := i) (d := 0) by omega).
         unfold base_from_limb_widths; fold base_from_limb_widths.
         rewrite peel_decode.
         fold (BaseSystem.mul_each (two_p w[i])).
@@ -317,4 +355,88 @@ Section Conversion.
     reflexivity.
   Qed.
 
-End Conversion.
\ No newline at end of file
+End Conversion.
+
+Section UniformBase.
+  Context {width : Z} (limb_width_pos : 0 < width).
+  Context (limb_widths : list Z) (limb_widths_nonnil : limb_widths <> nil)
+    (limb_widths_uniform : forall w, In w limb_widths -> w = width).
+  Local Notation "{base}" := (base_from_limb_widths limb_widths).
+
+   Lemma bounded_uniform : forall us, (length us <= length limb_widths)%nat ->
+     (bounded limb_widths us <-> (forall u, In u us -> 0 <= u < 2 ^ width)).
+   Proof.
+     cbv [bounded]; split; intro A; intros.
+     + let G := fresh "G" in
+       match goal with H : In _ us |- _ =>
+         eapply In_nth in H; destruct H as [? G]; destruct G as [? G];
+         rewrite <-nth_default_eq in G; rewrite <-G end.
+       specialize (A x).
+       split; try eapply A.
+       eapply Z.lt_le_trans; try apply A.
+       apply nth_default_preserves_properties; [ | apply Z.pow_le_mono_r; omega ] .
+       intros; apply Z.eq_le_incl.
+       f_equal; auto.
+     + apply nth_default_preserves_properties_length_dep;
+         try solve [apply nth_default_preserves_properties; split; zero_bounds; rewrite limb_widths_uniform; auto || omega].
+      intros; apply nth_default_preserves_properties_length_dep; try solve [intros; omega].
+       let x := fresh "x" in intro x; intros;
+         replace x with width; try symmetry; auto.
+   Qed.
+
+  Lemma decode'_tl_base_shift' : forall us lw,
+    (forall w, In w lw -> w = width) ->
+    (length us <= length lw)%nat ->
+    BaseSystem.decode' (map (Z.mul (2 ^ width)) (base_from_limb_widths lw)) us =
+    (BaseSystem.decode' (1 :: map (Z.mul (2 ^ width)) (base_from_limb_widths lw)) us) << width.
+  Proof.
+    induction us; intros ? Hin Hlength.
+    + rewrite !decode_nil, Z.shiftl_0_l; reflexivity.
+    + edestruct (destruct_repeat lw) as [? | [tl_lw [Heq_lw tl_lw_uniform]]]; eauto.
+      - subst lw; rewrite !length_cons, nil_length0 in Hlength; omega.
+      - rewrite Heq_lw in Hlength |- *.
+        rewrite base_from_limb_widths_cons, decode'_cons, two_p_correct.
+        cbv [tl].
+        fold (BaseSystem.mul_each (2 ^ width)).
+        rewrite <-!mul_each_base, !mul_each_rep.
+        rewrite decode'_cons, Z.mul_add_distr_l.
+        rewrite Z.shiftl_mul_pow2 by omega. rewrite Z.mul_add_distr_r.
+        f_equal; try ring.
+        rewrite <-Z.mul_assoc. f_equal; try ring.
+        rewrite IHus by (simpl in Hlength; auto || omega).
+        rewrite Z.shiftl_mul_pow2 by omega.
+        reflexivity.
+  Qed.
+
+  Lemma decode_tl_base_shift : forall us, (length us < length limb_widths)%nat ->
+    BaseSystem.decode (tl {base}) us = BaseSystem.decode {base} us << width.
+  Proof.
+    intros ? Hlength.
+    edestruct (destruct_repeat limb_widths) as [? | [tl_lw [Heq_lw tl_lw_uniform]]];
+        eauto; try congruence.
+    rewrite Heq_lw in Hlength |- *.
+    rewrite base_from_limb_widths_cons, two_p_correct.
+    cbv [tl].
+    apply decode'_tl_base_shift';
+      auto; simpl in *; omega.
+  Qed.
+
+  Lemma decode_shift : forall us u0, (length (u0 :: us) <= length limb_widths)%nat ->
+    BaseSystem.decode {base} (u0 :: us) = u0 + ((BaseSystem.decode {base} us) << width).
+  Proof.
+    intros.
+    rewrite <-decode_tl_base_shift by (simpl in *; omega).
+    case_eq limb_widths; try congruence; intros.
+    rewrite base_from_limb_widths_cons, decode'_cons.
+    cbv [tl].
+    f_equal; ring.
+  Qed.
+
+  Lemma uniform_limb_widths_nonneg : forall w, In w limb_widths -> 0 <= w.
+  Proof.
+    intros.
+    apply Z.lt_le_incl.
+    replace w with width by (symmetry; auto).
+    assumption.
+  Qed.
+End UniformBase.
\ No newline at end of file
diff --git a/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v b/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v
index b1e88d605..e0a194c3b 100644
--- a/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v
+++ b/src/ModularArithmetic/PseudoMersenneBaseParamProofs.v
@@ -4,12 +4,14 @@ Require Import Crypto.Util.ListUtil Crypto.Util.CaseUtil Crypto.Util.ZUtil.
 Require Import Crypto.ModularArithmetic.PrimeFieldTheorems.
 Require Import VerdiTactics.
 Require Import Crypto.ModularArithmetic.PseudoMersenneBaseParams.
-Require Import Crypto.ModularArithmetic.Pow2Base Crypto.ModularArithmetic.Pow2BaseProofs.
+Require Import Crypto.ModularArithmetic.Pow2Base.
+Require Import Crypto.ModularArithmetic.Pow2BaseProofs.
 Require Crypto.BaseSystem.
 Local Open Scope Z_scope.
 
 Section PseudoMersenneBaseParamProofs.
   Context `{prm : PseudoMersenneBaseParams}.
+  Local Notation "{base}" := (base_from_limb_widths limb_widths).
 
   Lemma limb_widths_nonneg : forall w, In w limb_widths -> 0 <= w.
   Proof.
@@ -23,60 +25,36 @@ Section PseudoMersenneBaseParamProofs.
     apply sum_firstn_limb_widths_nonneg; auto.
   Qed. Hint Resolve k_nonneg.
 
-  Local Notation base := (base_from_limb_widths limb_widths).
-
-  Lemma base_length : length base = length limb_widths.
-  Proof.
-    auto using base_from_limb_widths_length.
-  Qed.
-
   Lemma base_matches_modulus: forall i j,
-    (i   <  length base)%nat ->
-    (j   <  length base)%nat ->
-    (i+j >= length base)%nat->
-    let b := nth_default 0 base in
-    let r := (b i * b j)  /   (2^k * b (i+j-length base)%nat) in
-              b i * b j = r * (2^k * b (i+j-length base)%nat).
+    (i   <  length limb_widths)%nat ->
+    (j   <  length limb_widths)%nat ->
+    (i+j >= length limb_widths)%nat->
+    let b := nth_default 0 {base} in
+    let r := (b i * b j)  /   (2^k * b (i+j-length {base})%nat) in
+              b i * b j = r * (2^k * b (i+j-length {base})%nat).
   Proof.
     intros.
     rewrite (Z.mul_comm r).
     subst r.
-    assert (i + j - length base < length base)%nat by omega.
+    assert (i + j - length limb_widths < length limb_widths)%nat by omega.
     rewrite Z.mul_div_eq by (apply Z.gt_lt_iff; apply Z.mul_pos_pos;
-      [ | subst b; rewrite nth_default_base; try assumption ];
-      zero_bounds; auto using sum_firstn_limb_widths_nonneg, limb_widths_nonneg).
+      subst b; rewrite ?nth_default_base; zero_bounds; rewrite ?base_from_limb_widths_length;
+      auto using sum_firstn_limb_widths_nonneg, limb_widths_nonneg).
     rewrite (Zminus_0_l_reverse (b i * b j)) at 1.
     f_equal.
     subst b.
-    repeat rewrite nth_default_base by auto.
+    repeat rewrite nth_default_base by (rewrite ?base_from_limb_widths_length; auto).
     do 2 rewrite <- Z.pow_add_r by auto using sum_firstn_limb_widths_nonneg.
     symmetry.
     apply Z.mod_same_pow.
     split.
     + apply Z.add_nonneg_nonneg; auto using sum_firstn_limb_widths_nonneg.
-    + rewrite base_length in * by auto.
-      apply limb_widths_match_modulus; auto.
+    + rewrite base_from_limb_widths_length; auto using limb_widths_nonneg, limb_widths_match_modulus.
   Qed.
 
-   Lemma base_positive : forall b : Z, In b base -> b > 0.
-   Proof.
-     intros b In_b_base.
-     apply In_nth_error_value in In_b_base.
-     destruct In_b_base as [i nth_err_b].
-     apply nth_error_subst in nth_err_b; [ | auto ].
-     rewrite nth_err_b.
-     apply Z.gt_lt_iff.
-     apply Z.pow_pos_nonneg; omega || auto using sum_firstn_limb_widths_nonneg.
-   Qed.
-
-   Lemma b0_1 : forall x : Z, nth_default x base 0 = 1.
-   Proof.
-     case_eq limb_widths; intros; [pose proof limb_widths_nonnil; congruence | reflexivity].
-   Qed.
-
    Lemma base_good : forall i j : nat,
-                (i + j < length base)%nat ->
-                let b := nth_default 0 base in
+                (i + j < length {base})%nat ->
+                let b := nth_default 0 {base} in
                 let r := b i * b j / b (i + j)%nat in
                 b i * b j = r * b (i + j)%nat.
    Proof.
@@ -89,13 +67,18 @@ Section PseudoMersenneBaseParamProofs.
      rewrite Z.mod_same_pow; try ring.
      split; [ auto using sum_firstn_limb_widths_nonneg | ].
      apply limb_widths_good.
-     rewrite <- base_length; assumption.
+     rewrite <-base_from_limb_widths_length; auto using limb_widths_nonneg.
    Qed.
 
-  Global Instance bv : BaseSystem.BaseVector base := {
-    base_positive := base_positive;
-    b0_1 := b0_1;
+  Lemma base_length : length {base} = length limb_widths.
+  Proof.
+    auto using base_from_limb_widths_length.
+  Qed.
+
+  Global Instance bv : BaseSystem.BaseVector {base} := {
+    base_positive := base_positive limb_widths_nonneg;
+    b0_1 := fun x => b0_1 x limb_widths_nonnil;
     base_good := base_good
   }.
 
-End PseudoMersenneBaseParamProofs.
+End PseudoMersenneBaseParamProofs.
\ No newline at end of file