Cleaned up PushButtonSynthesis/DettmanMultiplication.v

Replaced a bunch of references to (Z.log2_up s) with (Z.log2 s), since (in
the dettman_multiplication_mod_ops module) we now stipulate that s is a power
of 2.

Author: OwenConoly

src/Arithmetic/DettmanMultiplication.v

@@ -312,12 +312,12 @@ Module dettman_multiplication_mod_ops.
         (last_limb_width : nat)
         (p_nz : s - Associational.eval c <> 0)
         (n_gteq_4 : (4 <= n)%nat)
-        (last_limb_width_small : last_limb_width * n <= Z.log2_up s)
+        (last_limb_width_small : last_limb_width * n <= Z.log2 s)
         (last_limb_width_big : 1 <= last_limb_width)
         (s_power_of_2 : 2 ^ (Z.log2 s) = s).
 
-    (* I do want to have Z.log2_up s, not Z.log2_up (s - c) below.  We want to ensure that weight (n - 1) <= s <= weight limbs *)
-    Local Notation limbwidth_num' := (Z.log2_up s - last_limb_width).
+    (* I do want to have Z.log2 s, not Z.log2_up (s - c) below.  We want to ensure that weight (n - 1) <= s <= weight limbs *)
+    Local Notation limbwidth_num' := (Z.log2 s - last_limb_width).
     Local Notation limbwidth_den' := (n - 1). (* can't use Q here, or else reification doesn't work *)
 
     Context
@@ -333,7 +333,7 @@ Module dettman_multiplication_mod_ops.
     Definition mulmod := mulmod s c register_width n weight.
     Definition squaremod := squaremod s c register_width n weight.
 
-    Lemma n_small : n - 1 <= Z.log2_up s - last_limb_width.
+    Lemma n_small : n - 1 <= Z.log2 s - last_limb_width.
     Proof.
       replace (Z.of_nat n) with (Z.of_nat n - 1 + 1) in last_limb_width_small by lia.
       remember (Z.of_nat n - 1) as n'.
@@ -404,7 +404,7 @@ Module dettman_multiplication_mod_ops.
 
     Lemma s_gt_0 : 0 < s.
       assert (H: s <= 0 \/ 0 < s) by lia. destruct H as [H|H].
-      - apply Z.log2_up_nonpos in H. lia.
+      - apply Z.log2_nonpos in H. lia.
       - assumption.
     Qed.
 

src/PushButtonSynthesis/DettmanMultiplication.v

@@ -112,7 +112,7 @@ Section __.
   Local Instance no_select_size : no_select_size_opt := no_select_size_of_no_select machine_wordsize.
   Local Instance split_mul_to : split_mul_to_opt := split_mul_to_of_should_split_mul machine_wordsize possible_values.
   Local Instance split_multiret_to : split_multiret_to_opt := split_multiret_to_of_should_split_multiret machine_wordsize possible_values.
-  
+
   (** 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} (requests : list string) (res : Pipeline.ErrorT T)
@@ -122,26 +122,25 @@ Section __.
             (fun v => (true, v))
             [(negb (s - c =? 0), Pipeline.Values_not_provably_distinctZ "s - c <> 0" (s - c) 0)
              ; (4 <=? n, Pipeline.Value_not_leZ "4 <= n" 3 n)
-             ; (last_limb_width * n <=? Z.log2_up s, Pipeline.Value_not_leZ "last_limb_width * n <= Z.log2_up s" (last_limb_width * n) (Z.log2_up s))
+             ; (last_limb_width * n <=? Z.log2 s, Pipeline.Value_not_leZ "last_limb_width * n <= Z.log2 s" (last_limb_width * n) (Z.log2 s))
              ; (1 <=? last_limb_width, Pipeline.Value_not_leZ "1 <= last_limb_width" 1 last_limb_width)
              ; (2 ^ (Z.log2 s) =? s, Pipeline.Values_not_provably_equalZ "2 ^ (Z.log2 s) = s" (2 ^ Z.log2 s) s)
-             ; (Z.log2_up s - last_limb_width <=? (Z.to_nat machine_wordsize) * (n - 1), Pipeline.Value_not_leZ "Z.log2_up s - last_limb_width <= (Z.to_nat machine_wordsize) * (n - 1)" (Z.log2_up s - last_limb_width) (Z.to_nat machine_wordsize * (n - 1)))
-             ; (Z.log2 s <=? n * (Z.log2_up s - last_limb_width) / (n - 1), Pipeline.Value_not_leZ "Z.log2 s <= n * (Z.log2_up s - last_limb_width) / (n - 1)" (Z.log2 s) (n * (Z.log2_up s - last_limb_width) / (n - 1)))
+             ; (Z.log2 s - last_limb_width <=? (Z.to_nat machine_wordsize) * (n - 1), Pipeline.Value_not_leZ "Z.log2 s - last_limb_width <= (Z.to_nat machine_wordsize) * (n - 1)" (Z.log2 s - last_limb_width) (Z.to_nat machine_wordsize * (n - 1)))
+             ; (Z.log2 s <=? n * (Z.log2 s - last_limb_width) / (n - 1), Pipeline.Value_not_leZ "Z.log2 s <= n * (Z.log2 s - last_limb_width) / (n - 1)" (Z.log2 s) (n * (Z.log2 s - last_limb_width) / (n - 1)))
             ])
             res.
 
   Context (requests : list string)
     (curve_good : check_args requests (Success tt) = Success tt).
 
-  (* should probably use limbwidth_num, limbwidth_den to make this less confusing-looking *)
   Lemma use_curve_good
     : s - c <> 0
       /\ (4 <= n)
-      /\ last_limb_width * n <= Z.log2_up s
+      /\ last_limb_width * n <= Z.log2 s
       /\ 1 <= last_limb_width
       /\ 2 ^ (Z.log2 s) = s
-      /\ Z.log2_up s - last_limb_width <= (Z.to_nat machine_wordsize) * (n - 1)
-      /\ Z.log2 s <= n * (Z.log2_up s - last_limb_width) / (n - 1).
+      /\ Z.log2 s - last_limb_width <= (Z.to_nat machine_wordsize) * (n - 1)
+      /\ Z.log2 s <= n * (Z.log2 s - last_limb_width) / (n - 1).
   Proof using curve_good. prepare_use_curve_good (). Qed.
 
   Local Notation evalf := (eval weightf n).
@@ -157,7 +156,7 @@ Section __.
           summary
           correctness)
          (only parsing, at level 10, summary at next level, correctness at next level).
-  
+
   Definition mul
     := Pipeline.BoundsPipeline
          false (* subst01 *)