(** * Reflective Pipeline: Tactics that execute the pipeline *) (** N.B. This file should not need to be changed in normal modifications of the reflective transformations; to modify the transformations performed in the reflective pipeline; see Pipeline/Definition.v. If the input format of the pre-reflective goal changes, prefer adding complexity to Pipeline/Glue.v to transform the goal and hypotheses into a uniform syntax to 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. *) (** ** Preamble *) Require Import Coq.ZArith.ZArith. Require Import Crypto.Compilers.Syntax. Require Import Crypto.Compilers.Intros. Require Import Crypto.Compilers.Wf. Require Import Crypto.Compilers.WfReflective. Require Import Crypto.Compilers.RenameBinders. Require Import Crypto.Compilers.Eta. Require Import Crypto.Compilers.EtaInterp. Require Import Crypto.Compilers.Z.Syntax. Require Import Crypto.Compilers.Z.Syntax.Util. Require Import Crypto.Compilers.Z.Bounds.Interpretation. Require Import Crypto.Compilers.Z.Bounds.Relax. Require Import Crypto.Compilers.Reify. Require Import Crypto.Compilers.Z.Reify. Require Import Crypto.Compilers.InterpSideConditions. Require Import Crypto.Compilers.Z.InterpSideConditions. Require Import Crypto.Compilers.Z.Bounds.Pipeline.Definition. Require Import Crypto.Util.Tactics.Head. Require Import Crypto.Util.Tactics.SubstLet. Require Import Crypto.Util.Tactics.UnfoldArg. Require Import Crypto.Util.Tactics.UnifyAbstractReflexivity. Require Import Crypto.Util.FixedWordSizes. Require Import Crypto.Util.Option. Require Import bbv.WordScope. (** The final tactic in this file, [do_reflective_pipeline], takes a goal of the form << @Bounds.is_bounded_by (codomain T) bounds (fZ (cast_back_flat_const v)) /\ cast_back_flat_const fW = fZ (cast_back_flat_const v) >> where [fW] must be a context definition which is a single evar, and all other terms must be evar-free. It fully solves the goal, instantiating [fW] with an appropriately-unfolded (reflection-definition-free) version of [fZ (cast_back_flat_const v)] which has been transformed by the reflective pipeline. *) Module Export Exports. Export Crypto.Compilers.Reify. (* export for the instances for recursing under binders *) Export Crypto.Compilers.Z.Reify. (* export for the tactic redefinitions *) Export Crypto.Compilers.Z.Bounds.Pipeline.Definition.Exports. End Exports. (** ** Reification *) (** The [do_reify] tactic handles goals of the form << forall x, Interp _ ?e x = F >> by reifying [F]. *) Ltac do_reify := unfold_second_arg Tuple.tuple; unfold_second_arg Tuple.tuple'; cbv beta iota delta [Tuple.tuple Tuple.tuple'] in *; cbv beta iota delta [Syntax.interp_flat_type Syntax.interp_base_type]; reify_context_variables; Reify_rhs; reflexivity. (** ** Input Boundedness Side-Conditions *) (** The tactic [handle_bounds_from_hyps] handles goals of the form << Bounds.is_bounded_by (_, _, ..., _) _ >> by splitting them apart and looking in the context for hypotheses that prove the bounds. *) Ltac handle_bounds_from_hyps := repeat match goal with | _ => assumption | [ |- cast_back_flat_const _ = cast_back_flat_const _ ] => reflexivity | [ |- _ /\ _ ] => split | [ |- Bounds.is_bounded_by (_, _) _ ] => split end. (** ** Unfolding [Interp] *) (** The reduction strategies [interp_red], [extra_interp_red], and [constant_simplification] (the latter two defined in Pipeline/Definition.v) define the constants that get unfolded before instantiating the original evar with [Interp _ vm_computed_reified_expression arguments]. *) Declare Reduction interp_red := cbv [fst snd Interp (*InterpEta interp_op*) interp interp_eta interpf interpf_step interp_flat_type_eta interp_flat_type_eta_gen interp_flat_type interp_base_type interp_op SmartMap.SmartFlatTypeMap SmartMap.SmartFlatTypeMapUnInterp SmartMap.SmartFlatTypeMapInterp2 SmartMap.smart_interp_flat_map codomain domain lift_op Zinterp_op cast_const ZToInterp interpToZ ]. (** ** Solving Side-Conditions of Equality *) (** This section defines a number of different ways to solve goals of the form [LHS = RHS] where [LHS] may contain evars and [RHS] must not contain evars. Most tactics use [abstract] to reduce the load on [Defined] and to catch looping behavior early. *) (** The tactic [unify_abstract_cbv_interp_rhs_reflexivity] runs the interpretation reduction strategies in [RHS] and unifies the result with [LHS], and does not use the vm (and hence does not fully reduce things, which is important for efficiency). *) Ltac unify_abstract_cbv_interp_rhs_reflexivity := intros; clear; lazymatch goal with | [ |- ?LHS = ?RHS ] => let RHS' := (eval interp_red in RHS) in let RHS' := (eval extra_interp_red in RHS') in let RHS' := lazymatch do_constant_simplification with | true => (eval constant_simplification in RHS') | _ => RHS' end in unify LHS RHS'; abstract exact_no_check (eq_refl RHS') end. (** *** Boundedness Lemma Side Conditions *) (** The tactic [handle_boundedness_side_condition] unfolds relevant identifiers in the side-condition of the boundedness lemma. It then calls [boundedness_side_condition_solver], which can be overridden. *) (** The tactic [boundedness_side_condition_solver] attempts to solve the algebraic side conditions of the boundedness lemma; it leaves them over if it cannot solve them. *) Ltac boundedness_side_condition_solver := repeat match goal with | [ |- _ /\ _ ] => apply conj | [ |- ?x = ?x ] => reflexivity end; try abstract ring. Ltac handle_boundedness_side_condition := post_intro_interp_flat_type_intros; cbv [id fst snd InterpSideConditions Compilers.InterpSideConditions.InterpSideConditions interp_side_conditions interpf_side_conditions interpf_side_conditions_gen Z.Syntax.Util.interped_op_side_conditions ExprInversion.invert_Abs Syntax.interp_op Syntax.lift_op Syntax.Zinterp_op SmartMap.SmartFlatTypeMapUnInterp SmartMap.SmartValf SmartMap.SmartFlatTypeMapInterp2 Syntax.cast_const Syntax.ZToInterp Syntax.interpToZ]; cbv [PointedProp.and_pointed_Prop PointedProp.to_prop]; try match goal with | [ |- True ] => exact I end; boundedness_side_condition_solver. (** ** Assemble the parts of Pipeline.Definition, in Gallina *) (** In this section, we assemble [PreWfPipeline] and [PostWfPipeline], and add extra equality hypotheses to minimize the work we have to do in Ltac. *) (** *** Gallina assembly imports *) Require Import Crypto.Compilers.Syntax. Require Import Crypto.Compilers.SmartMap. Require Import Crypto.Compilers.Wf. Require Import Crypto.Compilers.WfReflectiveGen. Require Import Crypto.Compilers.WfReflective. Require Import Crypto.Compilers.Eta. Require Import Crypto.Compilers.EtaWf. Require Import Crypto.Compilers.EtaInterp. Require Import Crypto.Compilers.Z.Bounds.Pipeline.OutputType. Require Import Crypto.Compilers.Z.Bounds.Pipeline.Definition. Require Import Crypto.Compilers.Z.Syntax. Require Import Crypto.Compilers.Z.Syntax.Equality. Require Import Crypto.Compilers.Z.Syntax.Util. Require Import Crypto.Compilers.Z.Bounds.Interpretation. Require Import Crypto.Compilers.Z.Bounds.Relax. Require Import Crypto.Util.PointedProp. Require Import Crypto.Util.PartiallyReifiedProp. Require Import Crypto.Util.Equality. (** *** Gallina assembly *) Section with_round_up_list. Context {allowable_lgsz : list nat}. Local Notation pick_typeb := (@Bounds.bounds_to_base_type (Bounds.round_up_to_in_list allowable_lgsz)) (only parsing). Local Notation pick_type v := (SmartFlatTypeMap pick_typeb v). Context (opts : PipelineOptions) {t : type base_type} {input_bounds : interp_flat_type Bounds.interp_base_type (domain t)} {given_output_bounds : interp_flat_type Bounds.interp_base_type (codomain t)} {v' : interp_flat_type interp_base_type (pick_type input_bounds)} {fZ : interp_flat_type interp_base_type (domain t) -> interp_flat_type interp_base_type (codomain t)} {final_e_evar : interp_flat_type interp_base_type (pick_type given_output_bounds)}. Class PipelineEvars := { b : interp_flat_type Bounds.interp_base_type (codomain t); e' : Expr (pick_type input_bounds -> pick_type b); e_final_newtype : Expr (pick_type input_bounds -> pick_type given_output_bounds); e : Expr (domain t -> codomain t); e_pre_pkg : Expr (domain t -> codomain t); e_pkg : option (@ProcessedReflectivePackage allowable_lgsz) }. Context (evars : PipelineEvars) (** ** reification *) (rexpr_sig : { rexpr : Expr t | forall x, Interp rexpr x = fZ x }). Record PipelineSideConditions := { (** ** pre-wf pipeline *) He : e = PreWfPipeline (proj1_sig rexpr_sig); (** ** proving wf *) He_unnatize_for_wf : forall var, unnatize_expr 0 (ExprEta' e (fun t => (nat * var t)%type)) = ExprEta' e _; Hwf : forall var1 var2, let P := (@reflect_wfT base_type base_type_eq_semidec_transparent op op_beq var1 var2 nil _ _ (ExprEta' e _) (ExprEta' e _)) in trueify P = P; (** ** post-wf-pre-bounds-pipeline *) Hpost_wf_pre_bounds : e_pre_pkg = PostWfPreBoundsPipeline opts e; (** ** post-wf-pipeline *) Hpost : e_pkg = PostWfBoundsPipeline _ opts e e_pre_pkg input_bounds; Hpost_correct : Some {| OutputType.input_expr := e ; OutputType.input_bounds := input_bounds ; output_bounds := b ; output_expr := e' |} = e_pkg; (** ** bounds relaxation *) Hbounds_relax : Bounds.is_tighter_thanb b given_output_bounds = true; Hbounds_sane : pick_type given_output_bounds = pick_type b; Hbounds_sane_refl : e_final_newtype = eq_rect _ (fun t => Expr (Arrow (pick_type input_bounds) t)) e' _ (eq_sym Hbounds_sane); (** ** instantiation of original evar *) Hevar : final_e_evar = InterpEta (t:=Arrow _ _) Syntax.interp_op e_final_newtype v'; (** ** side conditions (boundedness) *) Hv1 : Bounds.is_bounded_by input_bounds (cast_back_flat_const v'); Hv2 : intros_interp_flat_type_Prop (fun v => PointedProp.to_prop (InterpSideConditions e_pre_pkg v)); }. Definition PipelineCorrect (side_conditions : PipelineSideConditions) : Bounds.is_bounded_by given_output_bounds (fZ (cast_back_flat_const v')) /\ cast_back_flat_const final_e_evar = fZ (cast_back_flat_const v'). Proof using All. destruct side_conditions as [He He_unnatize_for_wf Hwf Hpost_wf_pre_bounds Hpost Hpost_correct Hbounds_relax Hbounds_sane Hbounds_sane_refl Hevar Hv1 Hv2]. cbv [b e' e_final_newtype e e_pre_pkg e_pkg] in *. destruct evars as [b e' e_final_newtype e e_pre_pkg e_pkg]; clear evars. destruct rexpr_sig as [? Hrexpr]; clear rexpr_sig. assert (Hwf' : Wf e) by (apply (proj1 (@Wf_ExprEta'_iff _ _ _ e)); eapply reflect_Wf; [ .. | intros; split; [ eapply He_unnatize_for_wf | rewrite <- Hwf; apply trueify_true ] ]; auto using base_type_eq_semidec_is_dec, op_beq_bl). clear Hwf He_unnatize_for_wf. symmetry in Hpost_correct. subst; cbv [proj1_sig] in *. rewrite eq_InterpEta, <- Hrexpr. pose proof (introsP_interp_flat_type Hv2) as Hv2'. eapply PostWfPipelineCorrect in Hpost_correct; [ | solve [ eauto ].. ]. rewrite !@InterpPreWfPipeline in Hpost_correct. unshelve eapply relax_output_bounds; try eassumption; []. match goal with | [ |- context[Interp (@eq_rect ?A ?x ?P ?k ?y ?pf) ?v] ] => rewrite (@ap_transport A P _ x y pf (fun t e => Interp e v) k) end. rewrite <- transport_pp, concat_Vp; simpl. apply Hpost_correct. Qed. End with_round_up_list. (** ** Assembling the Pipeline, in Ltac *) (** The tactic [refine_with_pipeline_correct] uses the [PipelineCorrect] lemma to create side-conditions. It assumes the goal is in exactly the form given in the conclusion of the [PipelineCorrect] lemma. *) (** The [refine_PipelineSideConditions_constructor] subtactic splits up the [PipelineSideConditions] record goal into multiple subgoals, to be discharged by automation lower in this file ([solve_post_reified_side_conditions]). *) Ltac refine_PipelineSideConditions_constructor := lazymatch goal with | [ |- PipelineSideConditions ?opts ?evars _ ] => simple refine {| Hevar := _ |}; cbv [b e' e_final_newtype e e_pre_pkg e_pkg proj1_sig] end. Ltac refine_with_pipeline_correct opts := lazymatch goal with | [ |- _ /\ ?castback ?fW = ?fZ ?arg ] => let lem := open_constr:(@PipelineCorrect _ opts _ _ _ _ _ _ {| e_pkg := _ |}) in simple refine (lem _ _); subst fW fZ end; [ eexists | refine_PipelineSideConditions_constructor ]. (** The tactic [solve_side_conditions] uses the above reduction-and-proving-equality tactics to prove the side-conditions of [PipelineCorrect]. The order must match with [PipelineCorrect]. Which tactic to use was chosen in the following way: - The default is [unify_abstract_vm_compute_rhs_reflexivity] - If the [RHS] is already in [vm_compute]d form, use [unify_abstract_rhs_reflexivity] (saves a needless [vm_compute] which would be a costly no-op) - If the proof needs to be transparent and there are no evars and you want the user to see the fully [vm_compute]d term on error, use [vm_compute; reflexivity] - If the user should see an unreduced term and you're proving [_ = true], use [abstract vm_cast_no_check (eq_refl true)] - If you want to preserve binder names, use [unify_abstract_cbv_rhs_reflexivity] The other choices are tactics that are specialized to the specific side-condition for which they are used (reification, boundedness of input, reduction of [Interp], renaming). *) Ltac solve_post_reified_side_conditions := [> (** ** pre-wf pipeline *) unify_abstract_vm_compute_rhs_reflexivity | (** ** reflective wf side-condition 1 *) unify_abstract_vm_compute_rhs_reflexivity | (** ** reflective wf side-condition 2 *) unify_abstract_vm_compute_rhs_reflexivity | (** ** post-wf-pre-bounds-pipeline *) unify_abstract_vm_compute_rhs_reflexivity | (** ** post-wf pipeline *) unify_abstract_vm_compute_rhs_reflexivity | (** ** post-wf pipeline gives [Some _] *) unify_abstract_rhs_reflexivity | (** ** computed output bounds are not looser than the given output bounds *) (** we do subst and we don't [vm_compute] first because we want to get an error message that displays the bounds *) subst_let; clear; abstract vm_cast_no_check (eq_refl true) | (** ** types computed from given output bounds are the same as types computed from computed output bounds *) (** N.B. the proof must be exactly [eq_refl] because it's used in a later goal and needs to reduce *) subst_let; clear; vm_compute; reflexivity | (** ** removal of a cast across the equality proof above *) unify_abstract_compute_rhs_reflexivity | (** ** unfolding of [interp] constants *) unify_abstract_cbv_interp_rhs_reflexivity | (** ** boundedness of inputs *) abstract handle_bounds_from_hyps | (** ** boundedness side-condition *) handle_boundedness_side_condition ]. Ltac solve_side_conditions := [> (** ** reification *) do_reify | .. ]; solve_post_reified_side_conditions. (** ** The Entire Pipeline *) (** The [do_reflective_pipeline] tactic solves a goal of the form that is described at the top of this file, and is the public interface of this file. *) Ltac do_reflective_pipeline opts := refine_with_pipeline_correct opts; solve_side_conditions. Notation default_PipelineOptions := default_PipelineOptions.