diff options
Diffstat (limited to 'src/Compilers/Z')
| -rw-r--r-- | src/Compilers/Z/Bounds/Interpretation.v | 2 | ||||
| -rw-r--r-- | src/Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy.v | 3 | ||||
| -rw-r--r-- | src/Compilers/Z/Bounds/InterpretationLemmas/PullCast.v | 7 | ||||
| -rw-r--r-- | src/Compilers/Z/Bounds/MapCastByDeBruijnInterp.v | 6 | ||||
| -rw-r--r-- | src/Compilers/Z/Bounds/Pipeline/Definition.v | 58 | ||||
| -rw-r--r-- | src/Compilers/Z/Bounds/Pipeline/ReflectiveTactics.v | 62 | ||||
| -rw-r--r-- | src/Compilers/Z/MapCastByDeBruijnInterp.v | 12 |
7 files changed, 116 insertions, 34 deletions
diff --git a/src/Compilers/Z/Bounds/Interpretation.v b/src/Compilers/Z/Bounds/Interpretation.v index 7b1254138..66145080c 100644 --- a/src/Compilers/Z/Bounds/Interpretation.v +++ b/src/Compilers/Z/Bounds/Interpretation.v @@ -156,7 +156,7 @@ Module Import Bounds. Definition id_with_alt {T1 T2 Tout} (x : interp_base_type T1) (y : interp_base_type T2) : interp_base_type Tout := truncation_bounds match T1, T2, Tout with - | TZ, TZ, TZ => (*y*)x + | TZ, TZ, TZ => y | _, _, _ => x end. End with_bitwidth. diff --git a/src/Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy.v b/src/Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy.v index c0172c67a..e7ec688d3 100644 --- a/src/Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy.v +++ b/src/Compilers/Z/Bounds/InterpretationLemmas/IsBoundedBy.v @@ -9,6 +9,7 @@ Require Import Crypto.Compilers.Z.Bounds.InterpretationLemmas.Tactics. Require Import Crypto.Compilers.SmartMap. Require Import Crypto.Util.ZUtil. Require Import Crypto.Util.ZUtil.Stabilization. +Require Import Crypto.Util.PointedProp. Require Import Crypto.Util.Bool. Require Import Crypto.Util.FixedWordSizesEquality. Require Import Crypto.Util.Tactics.DestructHead. @@ -332,7 +333,7 @@ Lemma is_bounded_by_interp_op t tR (opc : op t tR) (bs : interp_flat_type Bounds.interp_base_type _) (v : interp_flat_type interp_base_type _) (H : Bounds.is_bounded_by bs v) - (*H_side : interped_op_side_conditions opc v = true*) + (H_side : to_prop (interped_op_side_conditions opc v)) : Bounds.is_bounded_by (Bounds.interp_op opc bs) (Syntax.interp_op _ _ opc v). Proof. destruct opc; diff --git a/src/Compilers/Z/Bounds/InterpretationLemmas/PullCast.v b/src/Compilers/Z/Bounds/InterpretationLemmas/PullCast.v index 38ed60038..1701b4688 100644 --- a/src/Compilers/Z/Bounds/InterpretationLemmas/PullCast.v +++ b/src/Compilers/Z/Bounds/InterpretationLemmas/PullCast.v @@ -11,6 +11,7 @@ Require Import Crypto.Util.ZUtil. Require Import Crypto.Util.Bool. Require Import Crypto.Util.FixedWordSizesEquality. Require Import Crypto.Util.Option. +Require Import Crypto.Util.PointedProp. Require Import Crypto.Util.Tactics.BreakMatch. Require Import Crypto.Util.Tactics.DestructHead. Require Import Crypto.Util.Tactics.SpecializeBy. @@ -31,7 +32,8 @@ Section with_round_up. : forall t tR (opc : op t tR) (bs : interp_flat_type Bounds.interp_base_type _) (v : interp_flat_type interp_base_type _) - (H : Bounds.is_bounded_by bs v), + (H : Bounds.is_bounded_by bs v) + (Hside : to_prop (interped_op_side_conditions opc v)), Bounds.is_bounded_by (Bounds.interp_op opc bs) (Syntax.interp_op _ _ opc v)). Context {round_up : nat -> option nat}. @@ -132,6 +134,7 @@ Section with_round_up. (H : Bounds.is_bounded_by bs (SmartFlatTypeMapUnInterp (fun (t1 : base_type) (b0 : Bounds.interp_base_type t1) => cast_const) v)) + (Hside : to_prop (interped_op_side_conditions opc (cast_back_flat_const v))) : interp_op t tR opc (cast_back_flat_const v) = cast_back_flat_const (interp_op (pick_type bs) (pick_type (Bounds.interp_op opc bs)) (genericize_op opc) v). Proof. @@ -151,7 +154,9 @@ Section with_round_up. | match goal with | [ H : forall v, _ <= ?f v <= _ /\ _ -> _ |- context[?f ?v'] ] => specialize (H v') + | _ => progress specialize_by_assumption | _ => progress specialize_by auto + | [ H : forall v : unit, _ |- _ ] => specialize (H tt) | [ H : forall v : _ * _, _ /\ _ -> _ |- _ ] => specialize (fun v1 v2 p1 p2 => H (v1, v2) (conj p1 p2)); cbn [fst snd] in H; diff --git a/src/Compilers/Z/Bounds/MapCastByDeBruijnInterp.v b/src/Compilers/Z/Bounds/MapCastByDeBruijnInterp.v index 330075ee5..28e305a8f 100644 --- a/src/Compilers/Z/Bounds/MapCastByDeBruijnInterp.v +++ b/src/Compilers/Z/Bounds/MapCastByDeBruijnInterp.v @@ -5,10 +5,12 @@ Require Import Crypto.Compilers.Relations. Require Import Crypto.Compilers.Z.MapCastByDeBruijnInterp. Require Import Crypto.Compilers.Z.Syntax. Require Import Crypto.Compilers.Z.Syntax.Util. +Require Import Crypto.Compilers.Z.InterpSideConditions. Require Import Crypto.Compilers.Z.Bounds.Interpretation. Require Import Crypto.Compilers.Z.Bounds.InterpretationLemmas.IsBoundedBy. Require Import Crypto.Compilers.Z.Bounds.InterpretationLemmas.PullCast. Require Import Crypto.Compilers.Z.Bounds.MapCastByDeBruijn. +Require Import Crypto.Util.PointedProp. Lemma MapCastCorrect {round_up} @@ -16,7 +18,8 @@ Lemma MapCastCorrect (Hwf : Wf e) (input_bounds : interp_flat_type Bounds.interp_base_type (domain t)) : forall {b} e' (He':MapCast round_up e input_bounds = Some (existT _ b e')) - v v' (Hv : Bounds.is_bounded_by input_bounds v /\ cast_back_flat_const v' = v), + v v' (Hv : Bounds.is_bounded_by input_bounds v /\ cast_back_flat_const v' = v) + (Hside : to_prop (InterpSideConditions e v)), Interp (@Bounds.interp_op) e input_bounds = b /\ Bounds.is_bounded_by b (Interp interp_op e v) /\ cast_back_flat_const (Interp interp_op e' v') = (Interp interp_op e v). @@ -34,6 +37,7 @@ Lemma MapCastCorrect_eq (input_bounds : interp_flat_type Bounds.interp_base_type (domain t)) : forall {b} e' (He':MapCast round_up e input_bounds = Some (existT _ b e')) v v' (Hv : Bounds.is_bounded_by input_bounds v /\ cast_back_flat_const v' = v) + (Hside : to_prop (InterpSideConditions e v)) (Hevb : evb = Interp (@Bounds.interp_op) e input_bounds) (Hev : ev = Interp interp_op e v), evb = b diff --git a/src/Compilers/Z/Bounds/Pipeline/Definition.v b/src/Compilers/Z/Bounds/Pipeline/Definition.v index 5408c944c..88492074b 100644 --- a/src/Compilers/Z/Bounds/Pipeline/Definition.v +++ b/src/Compilers/Z/Bounds/Pipeline/Definition.v @@ -79,26 +79,37 @@ Require Import Crypto.Util.Sigma.MapProjections. Record PipelineOptions := { anf : bool }. Definition default_PipelineOptions := {| anf := false |}. -(** Do not change the name or the type of this definition *) -Definition PostWfPipeline - round_up +(** Do not change the name or the type of these two definitions *) +(** The definition [PostWfPreBoundsPipeline] is for the part of the + pipeline that comes before [MapCast]; it must preserve the type of + the expression. *) +Definition PostWfPreBoundsPipeline (opts : PipelineOptions) {t} (e : Expr base_type op t) + : Expr base_type op t + := let e := InlineConst e in + let e := InlineConst (SimplifyArith false e) in + let e := InlineConst (SimplifyArith false e) in + let e := InlineConst (SimplifyArith false e) in + let e := if opts.(anf) then InlineConst (ANormal e) else e in + let e := RewriteAdc e in + let e := InlineConstAndOpp (Linearize (SimplifyArith true e)) in + let e := if opts.(anf) then InlineConstAndOpp (ANormal e) else e in + let e := InlineConstAndOpp (Linearize (SimplifyArith true e)) in + (*let e := CSE false e in*) + e. +(** The definition [PostWfBoundsPipeline] is for the part of the + pipeline that begins with [MapCast]. *) +Definition PostWfBoundsPipeline + round_up + (opts : PipelineOptions) + {t} (e0 : Expr base_type op t) + (e : Expr base_type op t) (input_bounds : interp_flat_type Bounds.interp_base_type (domain t)) : option (@ProcessedReflectivePackage round_up) := Build_ProcessedReflectivePackage_from_option_sigma - e input_bounds - (let e := InlineConst e in - let e := InlineConst (SimplifyArith false e) in - let e := InlineConst (SimplifyArith false e) in - let e := InlineConst (SimplifyArith false e) in - let e := if opts.(anf) then InlineConst (ANormal e) else e in - let e := RewriteAdc e in - let e := InlineConstAndOpp (Linearize (SimplifyArith true e)) in - let e := if opts.(anf) then InlineConstAndOpp (ANormal e) else e in - let e := InlineConstAndOpp (Linearize (SimplifyArith true e)) in - (*let e := CSE false e in*) - let e := MapCast _ e input_bounds in + e0 input_bounds + (let e := MapCast _ e input_bounds in option_map (projT2_map (fun b e' @@ -107,24 +118,27 @@ Definition PostWfPipeline e')) e). -(** *** Correctness proof of the Pre-Wf Pipeline *) +(** *** Correctness proof of the Post-Wf Pipeline *) (** Do not change the statement of this lemma. *) Require Import Crypto.Compilers.Wf. Require Import Crypto.Compilers.Equality. Require Import Crypto.Compilers.SmartMap. Require Import Crypto.Compilers.Z.Syntax.Util. +Require Import Crypto.Compilers.Z.InterpSideConditions. Require Import Crypto.Util.Tactics.BreakMatch. Require Import Crypto.Util.Option. Require Import Crypto.Util.Sigma. Require Import Crypto.Util.Prod. Require Import Crypto.Util.HProp. Require Import Crypto.Util.Decidable. +Require Import Crypto.Util.PointedProp. 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). + Local Opaque to_prop InterpSideConditions. Definition PostWfPipelineCorrect opts @@ -132,23 +146,25 @@ Section with_round_up_list. (e : Expr base_type op t) (input_bounds : interp_flat_type Bounds.interp_base_type (domain t)) (Hwf : Wf e) - {b e'} (He : PostWfPipeline _ opts e input_bounds - = Some {| input_expr := e ; input_bounds := input_bounds ; output_bounds := b ; output_expr := e' |}) + (e' := PostWfPreBoundsPipeline opts e) + {b e''} (He' : PostWfBoundsPipeline _ opts e e' input_bounds + = Some {| input_expr := e ; input_bounds := input_bounds ; output_bounds := b ; output_expr := e'' |}) (v : interp_flat_type Syntax.interp_base_type (domain t)) (v' : interp_flat_type Syntax.interp_base_type (pick_type input_bounds)) (Hv : Bounds.is_bounded_by input_bounds v /\ cast_back_flat_const v' = v) + (Hside : to_prop (InterpSideConditions e' v)) : Bounds.is_bounded_by b (Interp interp_op e v) - /\ cast_back_flat_const (Interp interp_op e' v') = Interp interp_op e v. + /\ cast_back_flat_const (Interp interp_op e'' v') = Interp interp_op e v. Proof. (** These first two lines probably shouldn't change much *) - unfold PostWfPipeline, Build_ProcessedReflectivePackage_from_option_sigma, option_map, projT2_map in *. + unfold PostWfBoundsPipeline, PostWfPreBoundsPipeline, Build_ProcessedReflectivePackage_from_option_sigma, option_map, projT2_map in *; subst e'. repeat (break_match_hyps || inversion_option || inversion_ProcessedReflectivePackage || inversion_sigma || eliminate_hprop_eq || inversion_prod || simpl in * || subst). (** Now handle all the transformations that come after the word-size selection *) all:autorewrite with reflective_interp. (** Now handle word-size selection *) - all:(eapply MapCastCorrect_eq; [ | eassumption | eassumption | .. ]; + all:(eapply MapCastCorrect_eq; [ | eassumption | eassumption | assumption | .. ]; [ solve [ auto 60 with wf ] | reflexivity | ]). (** Now handle all the transformations that come before the word-size selection *) all:repeat autorewrite with reflective_interp; reflexivity. 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 *) diff --git a/src/Compilers/Z/MapCastByDeBruijnInterp.v b/src/Compilers/Z/MapCastByDeBruijnInterp.v index cd145c6fa..068c74ef2 100644 --- a/src/Compilers/Z/MapCastByDeBruijnInterp.v +++ b/src/Compilers/Z/MapCastByDeBruijnInterp.v @@ -4,7 +4,10 @@ Require Import Crypto.Compilers.SmartMap. Require Import Crypto.Compilers.Relations. Require Import Crypto.Compilers.MapCastByDeBruijnInterp. Require Import Crypto.Compilers.Z.Syntax. +Require Import Crypto.Compilers.Z.Syntax.Util. Require Import Crypto.Compilers.Z.MapCastByDeBruijn. +Require Import Crypto.Compilers.Z.InterpSideConditions. +Require Import Crypto.Util.PointedProp. Section language. Context {interp_base_type_bounds : base_type -> Type} @@ -22,12 +25,14 @@ Section language. Context (interp_op_bounds_correct : forall t tR opc bs (v : interp_flat_type interp_base_type t) - (H : inbounds t bs v), + (H : inbounds t bs v) + (Hside : to_prop (interped_op_side_conditions opc v)), inbounds tR (interp_op_bounds t tR opc bs) (interp_op t tR opc v)) (pull_cast_back : forall t tR opc bs (v : interp_flat_type interp_base_type (pick_type bs)) - (H : inbounds t bs (cast_back t bs v)), + (H : inbounds t bs (cast_back t bs v)) + (Hside : to_prop (interped_op_side_conditions opc (cast_back t bs v))), interp_op t tR opc (cast_back t bs v) = cast_back _ _ (interp_op _ _ (cast_op _ _ opc bs) v)). @@ -40,7 +45,8 @@ Section language. (Hwf : Wf e) (input_bounds : interp_flat_type interp_base_type_bounds (domain t)) : forall {b} e' (He':MapCast e input_bounds = Some (existT _ b e')) - v v' (Hv : @inbounds _ input_bounds v /\ cast_back _ _ v' = v), + v v' (Hv : @inbounds _ input_bounds v /\ cast_back _ _ v' = v) + (Hside : to_prop (InterpSideConditions e v)), Interp interp_op_bounds e input_bounds = b /\ @inbounds _ b (Interp interp_op e v) /\ cast_back _ _ (Interp interp_op e' v') = (Interp interp_op e v). |