From ae141ea08f9ae743650ee49722f97049459e40ba Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 21 Dec 2018 12:29:30 -0500 Subject: Add eval_freeze_to_bytesmod to push_eval --- src/Experiments/NewPipeline/Arithmetic.v | 21 ++++++++++++++++++++- src/Experiments/NewPipeline/Toplevel1.v | 2 +- 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 -- cgit v1.2.3