diff options
Diffstat (limited to 'src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v')
| -rw-r--r-- | src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v | 62 |
1 files changed, 56 insertions, 6 deletions
diff --git a/src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v b/src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v index 1f82cb9f8..f132eb92a 100644 --- a/src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v +++ b/src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v @@ -22,6 +22,8 @@ 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. @@ -123,6 +125,45 @@ Ltac unify_abstract_cbv_interp_rhs_reflexivity := 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 := + (** TODO: This next bit, with repeat intros [? ?], could be done + with a single [apply], if we make the right lemma. We should + write that lemma. *) + cbv [PointedProp.to_prop Syntax.interp_flat_type Syntax.interp_base_type Syntax.domain Syntax.codomain]; + repeat match goal with + | [ |- forall x : _ * _, _ ] + => let a := fresh in let b := fresh in intros [a b]; revert a b + | [ |- forall x, _ ] + => let x := fresh "x" in intro x + end; + 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]; + 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], @@ -144,6 +185,7 @@ 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. @@ -164,6 +206,7 @@ Section with_round_up_list. {fZ} {final_e_evar : interp_flat_type Syntax.interp_base_type (pick_type given_output_bounds)} {e} + {e_pre_pkg} {e_pkg} (** ** reification *) (rexpr_sig : { rexpr : Expr base_type op t | forall x, Interp Syntax.interp_op rexpr x = fZ x }) @@ -174,8 +217,10 @@ Section with_round_up_list. (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 = PostWfPipeline _ opts e input_bounds) + (Hpost : e_pkg = PostWfBoundsPipeline _ opts e e_pre_pkg input_bounds) (Hpost_correct : Some {| input_expr := e ; input_bounds := input_bounds ; output_bounds := b ; output_expr := e' |} = e_pkg) (** ** renaming *) (Hrenaming : e_final = e') @@ -187,8 +232,9 @@ Section with_round_up_list. = eq_rect _ (fun t => Expr base_type op (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 condition *) - (Hv : Bounds.is_bounded_by input_bounds (cast_back_flat_const v')) + (** ** side conditions (boundedness) *) + (Hv1 : Bounds.is_bounded_by input_bounds (cast_back_flat_const v')) + (Hv2 : forall v, PointedProp.to_prop (InterpSideConditions e_pre_pkg v)) : 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. @@ -223,8 +269,8 @@ End with_round_up_list. Ltac refine_with_pipeline_correct opts := lazymatch goal with | [ |- _ /\ ?castback ?fW = ?fZ ?arg ] - => let lem := open_constr:(@PipelineCorrect _ opts _ _ _ _ _ _ _ _ _ _ _ _) in - simple refine (lem _ _ _ _ _ _ _ _ _ _ _ _); + => let lem := open_constr:(@PipelineCorrect _ opts _ _ _ _ _ _ _ _ _ _ _ _ _) in + simple refine (lem _ _ _ _ _ _ _ _ _ _ _ _ _ _); subst fW fZ end; [ eexists @@ -264,6 +310,8 @@ Ltac solve_side_conditions := 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 _] *) @@ -283,7 +331,9 @@ Ltac solve_side_conditions := (** ** unfolding of [interp] constants *) unify_abstract_cbv_interp_rhs_reflexivity | (** ** boundedness of inputs *) - abstract handle_bounds_from_hyps ]. + abstract handle_bounds_from_hyps | + (** ** boundedness side-condition *) + handle_boundedness_side_condition ]. (** ** The Entire Pipeline *) |