Add eval_freeze_to_bytesmod to push_eval

2 files changed, 21 insertions, 2 deletions

diff --git a/src/Experiments/NewPipeline/Arithmetic.v b/src/Experiments/NewPipeline/Arithmetic.v
index 5ca573fa8..fed956121 100644
--- a/src/Experiments/NewPipeline/Arithmetic.v
+++ b/src/Experiments/NewPipeline/Arithmetic.v
@@ -2822,7 +2822,7 @@ Section freeze_mod_ops.
     split; apply eval_to_bytes || apply to_bytes_partitions; assumption.
   Qed.
 
-  Lemma eval_freeze_to_bytesmod
+  Lemma eval_freeze_to_bytesmod_and_partitions
     : forall (f : list Z)
         (Hf : length f = n)
         (Hf_bounded : 0 <= eval weight n f < 2 * m),
@@ -2838,6 +2838,24 @@ Section freeze_mod_ops.
     Z.div_mod_to_quot_rem; nia.
   Qed.
 
+  Lemma eval_freeze_to_bytesmod
+    : forall (f : list Z)
+        (Hf : length f = n)
+        (Hf_bounded : 0 <= eval weight n f < 2 * m),
+      (eval bytes_weight bytes_n (freeze_to_bytesmod f)) = (eval weight n f) mod m.
+  Proof using m_enc_correct Hs limbwidth_good Hn_nz c_small Hm_enc_len m_enc_bounded.
+    intros; now apply eval_freeze_to_bytesmod_and_partitions.
+  Qed.
+
+  Lemma freeze_to_bytesmod_partitions
+    : forall (f : list Z)
+        (Hf : length f = n)
+        (Hf_bounded : 0 <= eval weight n f < 2 * m),
+      freeze_to_bytesmod f = Partition.partition bytes_weight bytes_n (Positional.eval weight n f mod m).
+  Proof using m_enc_correct Hs limbwidth_good Hn_nz c_small Hm_enc_len m_enc_bounded.
+    intros; now apply eval_freeze_to_bytesmod_and_partitions.
+  Qed.
+
   Lemma eval_from_bytesmod
     : forall (f : list Z)
              (Hf : length f = bytes_n),
@@ -2848,6 +2866,7 @@ Section freeze_mod_ops.
     reflexivity.
   Qed.
 End freeze_mod_ops.
+Hint Rewrite eval_freeze_to_bytesmod : push_eval.
 
 Section primitives.
   Definition mulx (bitwidth : Z) := Eval cbv [Z.mul_split_at_bitwidth] in Z.mul_split_at_bitwidth bitwidth.
diff --git a/src/Experiments/NewPipeline/Toplevel1.v b/src/Experiments/NewPipeline/Toplevel1.v
index 957264d3f..b1eee614e 100644
--- a/src/Experiments/NewPipeline/Toplevel1.v
+++ b/src/Experiments/NewPipeline/Toplevel1.v
@@ -1885,7 +1885,7 @@ Module Import UnsaturatedSolinas.
           { apply Hto_bytesv; solve [ assumption | repeat split ]. }
           { cbn [type.for_each_lhs_of_arrow type_base type.andb_bool_for_each_lhs_of_arrow ZRange.type.option.is_bounded_by fst snd] in *.
             rewrite Bool.andb_true_iff in *; split_and'.
-            etransitivity; [ apply eval_freeze_to_bytesmod | f_equal; (eassumption || (symmetry; eassumption)) ];
+            etransitivity; [ apply eval_freeze_to_bytesmod_and_partitions | f_equal; (eassumption || (symmetry; eassumption)) ];
               auto; try omega.
             { erewrite Ring.length_is_bounded_by by eassumption; assumption. }
             { lazymatch goal with