Make [freeze] proofs consider machine integer width and hard input bounds separately

3 files changed, 34 insertions, 40 deletions

diff --git a/src/ModularArithmetic/ModularBaseSystem.v b/src/ModularArithmetic/ModularBaseSystem.v
index 6df49173e..9d7ce7c1f 100644
--- a/src/ModularArithmetic/ModularBaseSystem.v
+++ b/src/ModularArithmetic/ModularBaseSystem.v
@@ -83,10 +83,10 @@ Section ModularBaseSystem.
 
   Definition eq (x y : digits) : Prop := decode x = decode y.
 
-  Definition freeze B (x : digits) : digits :=
-    from_list (freeze B [[x]]) (length_freeze length_to_list).
+  Definition freeze int_width (x : digits) : digits :=
+    from_list (freeze int_width [[x]]) (length_freeze length_to_list).
 
-  Definition eqb B (x y : digits) : bool := fieldwiseb Z.eqb (freeze B x) (freeze B y).
+  Definition eqb int_width (x y : digits) : bool := fieldwiseb Z.eqb (freeze int_width x) (freeze int_width y).
 
   (* Note : both of the following square root definitions will produce garbage output if the input is
             not square mod [modulus]. The caller should either provably only call them with square input,
@@ -95,10 +95,10 @@ Section ModularBaseSystem.
                   (chain_correct : fold_chain 0%N N.add chain (1%N :: nil) = Z.to_N (modulus / 4 + 1))
                   (x : digits) : digits := pow x chain.
 
-  Definition sqrt_5mod8 B powx powx_squared (chain : list (nat * nat))
+  Definition sqrt_5mod8 int_width powx powx_squared (chain : list (nat * nat))
                   (chain_correct : fold_chain 0%N N.add chain (1%N :: nil) = Z.to_N (modulus / 8 + 1))
                   (sqrt_minus1 x : digits) : digits :=
-    if eqb B powx_squared x then powx else mul sqrt_minus1 powx.
+    if eqb int_width powx_squared x then powx else mul sqrt_minus1 powx.
 
   Import Morphisms.
   Global Instance eq_Equivalence : Equivalence eq.
@@ -106,9 +106,9 @@ Section ModularBaseSystem.
     split; cbv [eq]; repeat intro; congruence.
   Qed.
 
-  Definition select B (b : Z) (x y : digits) :=
-    add (map (Z.land (neg B b)) x)
-        (map (Z.land (neg B (Z.lxor b 1))) x).
+  Definition select int_width (b : Z) (x y : digits) :=
+    add (map (Z.land (neg int_width b)) x)
+        (map (Z.land (neg int_width (Z.lxor b 1))) x).
 
   Context {target_widths} (target_widths_nonneg : forall x, In x target_widths -> 0 <= x)
           (bits_eq : sum_firstn limb_widths   (length limb_widths) =
diff --git a/src/ModularArithmetic/ModularBaseSystemOpt.v b/src/ModularArithmetic/ModularBaseSystemOpt.v
index d302f83a8..155698e56 100644
--- a/src/ModularArithmetic/ModularBaseSystemOpt.v
+++ b/src/ModularArithmetic/ModularBaseSystemOpt.v
@@ -905,30 +905,15 @@ Section Conversion.
 
 End Conversion.
 
-Section with_base.
-  Context {modulus} (prm : PseudoMersenneBaseParams modulus).
-  Local Notation base := (Pow2Base.base_from_limb_widths limb_widths).
-  Local Notation log_cap i := (nth_default 0 limb_widths i).
-
-  Record freezePreconditions int_width :=
-    mkFreezePreconditions {
-        lt_1_length_base : (1 < length base)%nat;
-        int_width_pos : 0 < int_width;
-        int_width_compat : forall w, In w limb_widths -> w < int_width;
-        c_pos : 0 < c;
-        c_reduce1 : c * (Z.ones (int_width - log_cap (pred (length base)))) < 2 ^ log_cap 0;
-        c_reduce2 : c < 2 ^ log_cap 0 - c;
-        two_pow_k_le_2modulus : 2 ^ k <= 2 * modulus
-      }.
-End with_base.
-Local Hint Resolve lt_1_length_base int_width_pos int_width_compat c_pos
-    c_reduce1 c_reduce2 two_pow_k_le_2modulus.
+Local Hint Resolve lt_1_length_limb_widths int_width_pos B_pos B_compat
+  c_reduce1 c_reduce2.
 
 Section Canonicalization.
   Context `{prm : PseudoMersenneBaseParams} {sc : SubtractionCoefficient}
     (* allows caller to precompute k and c *)
     (k_ c_ : Z) (k_subst : k = k_) (c_subst : c = c_)
-    {int_width} (preconditions : freezePreconditions prm int_width).
+    {int_width freeze_input_bound}
+    (preconditions : FreezePreconditions freeze_input_bound int_width).
   Local Notation digits := (tuple Z (length limb_widths)).
 
   Definition carry_full_3_opt_cps_sig
@@ -1072,7 +1057,8 @@ Section SquareRoots.
   Section SquareRoot5mod8.
   Context {ec : ExponentiationChain (modulus / 8 + 1)}.
   Context (sqrt_m1 : digits) (sqrt_m1_correct : rep (mul sqrt_m1 sqrt_m1) (F.opp 1%F)).
-  Context {int_width} (preconditions : freezePreconditions prm int_width).
+  Context {int_width freeze_input_bound}
+          (preconditions : FreezePreconditions freeze_input_bound int_width).
 
   Definition sqrt_5mod8_opt_sig (powx powx_squared us : digits) :
     { vs : digits |
diff --git a/src/ModularArithmetic/ModularBaseSystemProofs.v b/src/ModularArithmetic/ModularBaseSystemProofs.v
index 59a6f33db..197a0dca6 100644
--- a/src/ModularArithmetic/ModularBaseSystemProofs.v
+++ b/src/ModularArithmetic/ModularBaseSystemProofs.v
@@ -521,16 +521,18 @@ End CarryProofs.
 
 Hint Rewrite @length_carry_and_reduce @length_carry : distr_length.
 
-Class FreezePreconditions `{prm : PseudoMersenneBaseParams} B :=
+Class FreezePreconditions `{prm : PseudoMersenneBaseParams} B int_width :=
   {
     lt_1_length_limb_widths : (1 < length limb_widths)%nat;
+    int_width_pos : 0 < int_width;
+    B_le_int_width : B <= int_width;
     B_pos : 0 < B;
     B_compat : forall w, In w limb_widths -> w < B;
    (* on the first reduce step, we add at most one bit of width to the first digit *)
    c_reduce1 : c * ((2 ^ B) >> nth_default 0 limb_widths (pred (length limb_widths))) <= 2 ^ (nth_default 0 limb_widths 0);
    (* on the second reduce step, we add at most one bit of width to the first digit,
       and leave room to carry c one more time after the highest bit is carried *)
-   c_reduce2 : c <= 2 ^ (nth_default 0 limb_widths 0) - c
+   c_reduce2 : c <= 2 ^ (nth_default 0 limb_widths 0) - c;
   }.
 
 Section CanonicalizationProofs.
@@ -940,8 +942,14 @@ Section CanonicalizationProofs.
       congruence.
   Qed.
 
+  Lemma int_width_compat : forall x, In x limb_widths -> x < int_width.
+  Proof.
+    intros. apply B_compat in H.
+    eapply Z.lt_le_trans; eauto using B_le_int_width.
+  Qed.
+
   Lemma minimal_rep_freeze : forall u, initial_bounds u ->
-      minimal_rep (freeze B u).
+      minimal_rep (freeze int_width u).
   Proof.
     repeat match goal with
            | |- _ => progress (cbv [freeze ModularBaseSystemList.freeze])
@@ -952,12 +960,12 @@ Section CanonicalizationProofs.
            | |- _ => apply conditional_subtract_lt_modulus
            | |- _ => apply conditional_subtract_modulus_preserves_bounded
            | |- bounded _ (carry_full _) => apply bounded_iff
-           | |- _ => solve [auto using Z.lt_le_incl, B_pos, B_compat, lt_1_length_limb_widths, length_carry_full, length_to_list]
+           | |- _ => solve [auto using Z.lt_le_incl, int_width_pos, int_width_compat, lt_1_length_limb_widths, length_carry_full, length_to_list]
            end.
   Qed.
 
   Lemma freeze_decode : forall u,
-      BaseSystem.decode base (to_list _ (freeze B u)) mod modulus =
+      BaseSystem.decode base (to_list _ (freeze int_width u)) mod modulus =
       BaseSystem.decode base (to_list _ u) mod modulus.
   Proof.
     repeat match goal with
@@ -967,7 +975,7 @@ Section CanonicalizationProofs.
            | |- _ => rewrite Z.mod_add by (pose proof prime_modulus; prime_bound)
            | |- _ => rewrite to_list_from_list
            | |- _ => rewrite conditional_subtract_modulus_spec by
-                       auto using Z.lt_le_incl, B_pos, B_compat, lt_1_length_limb_widths, length_carry_full, length_to_list, ge_modulus_01
+                       (auto using Z.lt_le_incl, int_width_pos, int_width_compat, lt_1_length_limb_widths, length_carry_full, length_to_list, ge_modulus_01)
            end.
     rewrite !decode_mod_Fdecode by auto using length_carry_full, length_to_list.
     cbv [carry_full].
@@ -986,7 +994,7 @@ Section CanonicalizationProofs.
     rewrite from_list_to_list; reflexivity.
   Qed.
 
-  Lemma freeze_rep : forall u x, rep u x -> rep (freeze B u) x.
+  Lemma freeze_rep : forall u x, rep u x -> rep (freeze int_width u) x.
   Proof.
     cbv [rep]; intros.
     apply F.eq_to_Z_iff.
@@ -997,7 +1005,7 @@ Section CanonicalizationProofs.
   Lemma freeze_canonical : forall u v x y, rep u x -> rep v y ->
                                            initial_bounds u ->
                                            initial_bounds v ->
-    (x = y <-> fieldwise Logic.eq (freeze B u) (freeze B v)).
+    (x = y <-> fieldwise Logic.eq (freeze int_width u) (freeze int_width v)).
   Proof.
     intros; apply bounded_canonical; auto using freeze_rep, minimal_rep_freeze.
   Qed.
@@ -1022,7 +1030,7 @@ Section SquareRootProofs.
 
   Lemma eqb_true_iff : forall u v x y,
     bounded_by u freeze_input_bounds -> bounded_by v freeze_input_bounds ->
-    u ~= x -> v ~= y -> (x = y <-> eqb B u v = true).
+    u ~= x -> v ~= y -> (x = y <-> eqb int_width u v = true).
   Proof.
     cbv [eqb freeze_input_bounds]. intros.
     rewrite fieldwiseb_fieldwise by (apply Z.eqb_eq).
@@ -1031,10 +1039,10 @@ Section SquareRootProofs.
 
   Lemma eqb_false_iff : forall u v x y,
     bounded_by u freeze_input_bounds -> bounded_by v freeze_input_bounds ->
-    u ~= x -> v ~= y -> (x <> y <-> eqb B u v = false).
+    u ~= x -> v ~= y -> (x <> y <-> eqb int_width u v = false).
   Proof.
     intros.
-    case_eq (eqb B u v).
+    case_eq (eqb int_width u v).
     + rewrite <-eqb_true_iff by eassumption; split; intros;
         congruence || contradiction.
     + split; intros; auto.
@@ -1069,7 +1077,7 @@ Section SquareRootProofs.
     bounded_by powx_squared freeze_input_bounds ->
     ModularBaseSystem.eq powx (pow u chain) ->
     ModularBaseSystem.eq powx_squared (mul powx powx) ->
-    (sqrt_5mod8 B powx powx_squared chain chain_correct sqrt_m1 u) ~= F.sqrt_5mod8 (decode sqrt_m1) x.
+    (sqrt_5mod8 int_width powx powx_squared chain chain_correct sqrt_m1 u) ~= F.sqrt_5mod8 (decode sqrt_m1) x.
   Proof.
     cbv [sqrt_5mod8 F.sqrt_5mod8].
     intros.