wrote a version of the rewrite rule that works! need to put it in its own pass now.

Author: OwenConoly

fiat-c/src/secp256k1_dettman_64.c

@@ -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/PushButtonSynthesis/DettmanMultiplication.v

@@ -337,14 +337,14 @@ Definition arith_with_casts_rewrite_rulesT (adc_no_carry_to_add : bool) : list (
                   0 ∈ rland -> 0 ∈ r0
                   -> cstZ rland (Z.land (cstZ r0 ('0)) (cstZ rv v)) = cstZ r0 ('0))
                 (* try to use lower bounds = 0, rland.upper divides rv.upper to remove double cast. *)
-            ; (forall rland rm1 rv v,
+            (*; (forall rland rm1 rv v,
                   rland.(upper) ∈ rm1
                   -> rland.(upper) = Z.ones (Z.succ (Z.log2 rland.(upper)))
                   -> 0 = rland.(lower)
                   -> 0 = rv.(lower)
                   -> 0 <= rv.(upper)
                   -> (rv.(upper) + 1) mod (rland.(upper) + 1) = 0
-                  -> cstZ rland (Z.land (cstZ rv v) (cstZ rm1 ('rland.(upper)))) = cstZ rland v)
+                  -> cstZ rland (Z.land (cstZ rv v) (cstZ rm1 ('rland.(upper)))) = cstZ rland v)*)
             ; (forall rland rm1 rv v,
                   (rv <= rland)%zrange -> -1 ∈ rm1
                   -> cstZ rland (Z.land (cstZ rv v) (cstZ rm1 ('-1))) = cstZ rv v)
@@ -1060,7 +1060,17 @@ Section with_bitwidth.
           [mymap dont_do_again []
            ; mymap
                do_again
-               [(forall A B x y, @fst A B (x, y) = x)
+               [
+                 (* owen put this here, and he needs to remove it. *)
+                 (forall rland rm1 rv v,
+                       rland.(upper) ∈ rm1
+                       -> rland.(upper) = Z.ones (Z.succ (Z.log2 rland.(upper)))
+                       -> 0 = rland.(lower)
+                       -> 0 = rv.(lower)
+                       -> 0 <= rv.(upper)
+                       -> (rv.(upper) + 1) mod (rland.(upper) + 1) = 0
+                       -> cstZ rland (Z.land (cstZ rv v) (cstZ rm1 ('rland.(upper)))) = cstZ rland v)
+                ; (forall A B x y, @fst A B (x, y) = x)
                 ; (forall A B x y, @snd A B (x, y) = y)
                     (** In order to avoid tautological compares, we need to deal with carry/borrows being 0 *)
                 ; (forall r0 s x y r1 r2,

src/Rewriter/Rules.v

@@ -570,7 +570,7 @@ Lemma arith_with_casts_rewrite_rules_proofs (adc_no_carry_to_add : bool)
 Proof using Type.
   start_proof; auto; intros; try lia.
   all: repeat interp_good_t_step_related.
-  11: { replace (ident.cast rland v) with (ident.cast rland (ident.cast rv v)).
+  (*11: { replace (ident.cast rland v) with (ident.cast rland (ident.cast rv v)).
         - interp_good_t_step_arith. interp_good_t_step_arith. rewrite Z.land_ones.
           + replace (2 ^ Z.succ (Z.log2 (upper rland))) with (upper rland + 1).
             -- rewrite <- ident.cast_out_of_bounds_simple_0_mod.
@@ -592,7 +592,7 @@ Proof using Type.
           + lia.
           + Search Z.ones. rewrite H0. apply Ones.Z.ones_nonneg.
             remember (Z.log2_nonneg (upper)). lia.
-  }
+  }*)
            (* Search Z.ones. rewrite H0. apply Ones.Z.ones_nonneg.
             remember (Z.log2_nonneg (upper)). lia.
   }
@@ -861,6 +861,30 @@ Proof using Type.
     by (intros; apply Z.pow_gt_lin_r; auto with zarith).
 
   start_proof; auto; intros; try lia.
+  1: {
+    replace (ident.cast rland v) with (ident.cast rland (ident.cast rv v)).
+    - interp_good_t_step_arith. interp_good_t_step_arith. rewrite Z.land_ones.
+          + replace (2 ^ Z.succ (Z.log2 (upper rland))) with (upper rland + 1).
+            -- rewrite <- ident.cast_out_of_bounds_simple_0_mod.
+               ++ destruct rland. simpl in *. subst. apply ident.cast_idempotent.
+               ++ rewrite H2. apply Ones.Z.ones_nonneg. remember (Z.log2_nonneg (upper rland)). lia.
+            -- remember (Z.log2 _) as x. rewrite H2. subst. rewrite Z.ones_equiv. lia.
+          + remember (Z.log2_nonneg (upper rland)). lia.
+        - Search ident.cast. destruct rland. destruct rv. simpl in *. subst.
+          (*Search ident.cast. Search ZRange.normalize.
+          repeat rewrite <- (ident.cast_normalize r[0~>upper]).
+          repeat rewrite <- (ident.cast_normalize r[0~>upper0]).*)
+          Check ident.cast_out_of_bounds_simple_0_mod.
+          repeat rewrite ident.cast_out_of_bounds_simple_0_mod.
+          + Search ((_ mod _) mod _). rewrite <- Z.mod_div_mod_full.
+            -- reflexivity.
+            -- Search Z.divide. rewrite <- Z.mod_divide_full. assumption.
+          + Search Z.ones. rewrite H2. apply Ones.Z.ones_nonneg.
+            remember (Z.log2_nonneg (upper)). lia.
+          + lia.
+          + Search Z.ones. rewrite H2. apply Ones.Z.ones_nonneg.
+            remember (Z.log2_nonneg (upper)). lia.
+  }
   all: repeat interp_good_t_step_related.
   all: systematically_handle_casts; autorewrite with zsimplify_fast; try reflexivity.
   all: subst; rewrite !ident.platform_specific_cast_0_is_mod, ?Z.sub_add, ?Z.mod_mod by lia; try reflexivity.