diff options
Diffstat (limited to 'src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v')
| -rw-r--r-- | src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v | 362 |
1 files changed, 0 insertions, 362 deletions
diff --git a/src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v b/src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v deleted file mode 100644 index 9193ea17f..000000000 --- a/src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v +++ /dev/null @@ -1,362 +0,0 @@ -(** * 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. |