reverted to the variation of the rewrite rule that caused observable changed

Author: OwenConoly

src/PushButtonSynthesis/DettmanMultiplication.v

@@ -104,15 +104,14 @@ Section __.
   Definition input_bounds : list (ZRange.type.option.interp base.type.Z)
     := fold_left (fun l i => Some r[0 ~> Qceiling (2 * input_magnitude * ((weightf (i + 1) / weightf i) - 1))]%zrange :: l) (seq 0 (n - 1)) [] ++
                  [Some r[0 ~> Qceiling (2 * input_magnitude * (2^last_limb_width - 1))]%zrange].
-  (*Definition output_bounds : list (ZRange.type.option.interp base.type.Z)
+  Definition output_bounds : list (ZRange.type.option.interp base.type.Z)
     := fold_left (fun l i => Some r[0 ~> Qceiling (2 * output_magnitude_first_limbs * ((weightf (i + 1) / weightf i) - 1))]%zrange :: l) (seq 0 (n - 1)) [] ++
          [Some r[0 ~> Qceiling (2 * output_magnitude_last_limb * (2^last_limb_width - 1))]%zrange].
-   *)
-  Definition output_bounds : list (ZRange.type.option.interp base.type.Z) :=
+  (*Definition output_bounds : list (ZRange.type.option.interp base.type.Z) :=
     match inbounds_multiplier with
     | Some _ => [None; None; None; None; None]
     | None => [None; None; None; None; None]
-    end.
+    end.*)
   Local Existing Instance default_translate_to_fancy.
   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.

src/Rewriter/Rules.v

@@ -338,8 +338,6 @@ Definition arith_with_casts_rewrite_rulesT (adc_no_carry_to_add : bool) : list (
                   rland.(upper) ∈ rm1
                   -> rland.(upper) = Z.ones (Z.succ (Z.log2 rland.(upper)))
                   -> (0 = rland.(lower))
-                  -> (rland <= rm1)%zrange
-                  -> (rm1 <= rland)%zrange
                   -> cstZ rland (Z.land v (cstZ rm1 ('rland.(upper)))) = cstZ rland v)
             ; (forall rland rm1 rv v,
                   (rv <= rland)%zrange -> -1 ∈ rm1