Pipeline: reduce away reflective constants

This makes it so that the term that shows up when the reflective subgoal
is solved doesn't include things like [Interp]

2 files changed, 81 insertions, 4 deletions

diff --git a/src/Reflection/Z/Bounds/Pipeline/Definition.v b/src/Reflection/Z/Bounds/Pipeline/Definition.v
index a209213fe..dccd1d82b 100644
--- a/src/Reflection/Z/Bounds/Pipeline/Definition.v
+++ b/src/Reflection/Z/Bounds/Pipeline/Definition.v
@@ -123,3 +123,52 @@ Proof.
   (** Now handle word-size selection itself *)
   eapply MapCastCorrect; eauto with wf.
 Qed.
+
+
+(** ** Constant Simplification and Unfolding *)
+(** The reflective pipeline may introduce constants that you want to
+    unfold before instantiating the refined term; you can control that
+    here.  A number of reflection-specific constants are always
+    unfolded (in ReflectiveTactics.v).  Currently, we also reduce
+    expressions of the form [wordToZ (ZToWord Z_literal)], as
+    specified here. *)
+Require Import Coq.ZArith.ZArith.
+Require Import Crypto.Util.FixedWordSizes.
+Require Import Bedrock.Word.
+
+Module Export Exports. (* export unfolding strategy *)
+  (* iota is probably (hopefully?) the cheapest reduction.
+     Unfortunately, we can't say no-op here.  This is meant to be
+     extended. *)
+  Declare Reduction extra_interp_red := cbv iota.
+
+  (** Overload this to change reduction behavior of constants of the
+      form [wordToZ (ZToWord Z_literal)].  You might want to set this
+      to false if your term is very large, to speed things up. *)
+  Ltac do_constant_simplification := constr:(true).
+
+  Global Arguments ZToWord !_ !_ / .
+  Global Arguments wordToZ !_ !_ / .
+  Global Arguments word_case_dep _ !_ _ _ _ _ / .
+  Global Arguments ZToWord32 !_ / .
+  Global Arguments ZToWord64 !_ / .
+  Global Arguments ZToWord128 !_ / .
+  Global Arguments ZToWord_gen !_ !_ / .
+  Global Arguments word32ToZ !_ / .
+  Global Arguments word64ToZ !_ / .
+  Global Arguments word128ToZ !_ / .
+  Global Arguments wordToZ_gen !_ !_ / .
+  Global Arguments Z.to_N !_ / .
+  Global Arguments Z.of_N !_ / .
+  Global Arguments Word.NToWord !_ !_ / .
+  Global Arguments Word.wordToN !_ !_ / .
+  Global Arguments Word.posToWord !_ !_ / .
+  Global Arguments N.succ_double !_ / .
+  Global Arguments Word.wzero' !_ / .
+  Global Arguments N.double !_ .
+  Global Arguments Nat.pow !_ !_ / .
+  Global Arguments Nat.mul !_ !_ / .
+  Global Arguments Nat.add !_ !_ / .
+
+  Declare Reduction constant_simplification := cbn [FixedWordSizes.wordToZ FixedWordSizes.ZToWord word_case_dep ZToWord32 ZToWord64 ZToWord128 ZToWord_gen word32ToZ word64ToZ word128ToZ wordToZ_gen Word.NToWord Word.wordToN Word.posToWord Word.wzero' Z.to_N Z.of_N N.succ_double N.double Nat.pow Nat.mul Nat.add].
+End Exports.
diff --git a/src/Reflection/Z/Bounds/Pipeline/ReflectiveTactics.v b/src/Reflection/Z/Bounds/Pipeline/ReflectiveTactics.v
index 82f867b24..8af0bae4d 100644
--- a/src/Reflection/Z/Bounds/Pipeline/ReflectiveTactics.v
+++ b/src/Reflection/Z/Bounds/Pipeline/ReflectiveTactics.v
@@ -8,10 +8,13 @@
     modifying this file.  This file will need to be modified if you
     perform heavy changes in the shape of the generic or ℤ-specific
     reflective machinery itself, or if you find bugs or slowness. *)
+Require Import Coq.ZArith.ZArith.
 Require Import Crypto.Reflection.Syntax.
 Require Import Crypto.Reflection.Wf.
 Require Import Crypto.Reflection.WfReflective.
 Require Import Crypto.Reflection.RenameBinders.
+Require Import Crypto.Reflection.Eta.
+Require Import Crypto.Reflection.EtaInterp.
 Require Import Crypto.Reflection.Z.Syntax.
 Require Import Crypto.Reflection.Z.Syntax.Util.
 Require Import Crypto.Reflection.Z.Bounds.Interpretation.
@@ -22,7 +25,9 @@ Require Import Crypto.Reflection.Z.Bounds.Pipeline.OutputType.
 Require Import Crypto.Reflection.Z.Bounds.Pipeline.Definition.
 Require Import Crypto.Util.Tactics.Head.
 Require Import Crypto.Util.Tactics.SubstLet.
+Require Import Crypto.Util.FixedWordSizes.
 Require Import Crypto.Util.Option.
+Require Import Bedrock.Word.
 
 (** The final tactic in this file, [do_reflective_pipeline], takes a
     goal of the form
@@ -40,6 +45,7 @@ Require Import Crypto.Util.Option.
 Module Export Exports.
   Export Crypto.Reflection.Reify. (* export for the instances for recursing under binders *)
   Export Crypto.Reflection.Z.Reify. (* export for the tactic redefinitions *)
+  Export Crypto.Reflection.Z.Bounds.Pipeline.Definition.Exports.
 End Exports.
 
 Ltac assert_reflective :=
@@ -144,6 +150,12 @@ Ltac pretighten_bounds_from_correctness Hcorrectness :=
   end.
 Ltac tighten_bounds_from_correctness Hcorrectness :=
   pretighten_bounds_from_correctness Hcorrectness; posttighten_bounds.
+
+Declare Reduction interp_red := cbv [Interp InterpEta interp_op interp interp_eta interpf interpf_step interp_flat_type_eta interp_flat_type_eta_gen SmartMap.SmartFlatTypeMap codomain domain interp_flat_type interp_base_type SmartMap.smart_interp_flat_map lift_op Zinterp_op SmartMap.SmartFlatTypeMapUnInterp SmartMap.SmartFlatTypeMapInterp2 fst snd cast_const ZToInterp interpToZ].
+(* hopefully separating this out into a separate tactic will make it
+   show up in the Ltac profile *)
+Ltac clear_then_abstract_reflexivity x :=
+  clear; abstract exact_no_check (eq_refl x).
 Ltac specialize_Hcorrectness Hcorrectness :=
   lazymatch goal with
   | [ |- @Bounds.is_bounded_by (codomain ?T) ?bounds (Interp _ ?fZ ?v')
@@ -151,11 +163,27 @@ Ltac specialize_Hcorrectness Hcorrectness :=
     => let v := lazymatch v' with cast_back_flat_const ?v => v end in
        specialize (Hcorrectness v' v);
        lazymatch type of Hcorrectness with
-       | ?T -> Bounds.is_bounded_by _ _ /\ cast_back_flat_const ?fW' = _
-         => let fWev := (eval cbv delta [fW] in fW) in
-            unify fWev fW'; cut T
+       | ?T -> Bounds.is_bounded_by _ _
+               /\ cast_back_flat_const (@Interp ?base_type ?interp_base_type ?op ?interp_op ?fWT ?fW' ?args) = _
+         => cut T;
+            [ (let H := fresh in intro H; specialize (Hcorrectness H); clear H);
+              rewrite <- (@eq_InterpEta base_type interp_base_type op interp_op fWT fW' args) in Hcorrectness
+            | ]
        end;
-       [ let H := fresh in intro H; specialize (Hcorrectness H) | ]
+       [ lazymatch type of Hcorrectness with
+           Bounds.is_bounded_by _ _ /\ cast_back_flat_const ?fW' = _
+           => let fWev := (eval cbv delta [fW] in fW) in
+              let fW'_orig := fW' in
+              let fW' := (eval interp_red in fW') in
+              let fW' := (eval extra_interp_red in fW') in
+              let fW' := lazymatch do_constant_simplification with
+                         | true => (eval constant_simplification in fW')
+                         | _ => fW'
+                         end in
+              unify fWev fW';
+              replace fW with fW'_orig by clear_then_abstract_reflexivity fW
+         end
+       | ]
   end.
 Ltac handle_bounds_from_hyps :=
   repeat match goal with