From 7a223688d9195c4969cdcae0622170149dc7d660 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Sat, 13 May 2017 22:02:41 -0400 Subject: Add compiler optimization for add-with-carry This closes #171. It's unfortunately a bit fragile, and takes a really long time (about 60s) to prove correct, because Coq is bad at deep dependent pattern matching. We enable a-normal form for the freeze test, because the rewriter only works when the arguments to adc are var or const. --- src/Compilers/Z/Bounds/Pipeline/Definition.v | 4 + src/Compilers/Z/Named/RewriteAddToAdc.v | 97 +++++++++ src/Compilers/Z/Named/RewriteAddToAdcInterp.v | 281 ++++++++++++++++++++++++++ src/Compilers/Z/RewriteAddToAdc.v | 58 ++++++ src/Compilers/Z/RewriteAddToAdcInterp.v | 71 +++++++ src/Compilers/Z/RewriteAddToAdcWf.v | 35 ++++ src/Specific/IntegrationTestFreeze.v | 2 +- 7 files changed, 547 insertions(+), 1 deletion(-) create mode 100644 src/Compilers/Z/Named/RewriteAddToAdc.v create mode 100644 src/Compilers/Z/Named/RewriteAddToAdcInterp.v create mode 100644 src/Compilers/Z/RewriteAddToAdc.v create mode 100644 src/Compilers/Z/RewriteAddToAdcInterp.v create mode 100644 src/Compilers/Z/RewriteAddToAdcWf.v (limited to 'src') diff --git a/src/Compilers/Z/Bounds/Pipeline/Definition.v b/src/Compilers/Z/Bounds/Pipeline/Definition.v index e7c267d65..8a43a0ec7 100644 --- a/src/Compilers/Z/Bounds/Pipeline/Definition.v +++ b/src/Compilers/Z/Bounds/Pipeline/Definition.v @@ -65,6 +65,9 @@ Require Import Crypto.Compilers.LinearizeWf. Require Import Crypto.Compilers.Z.CommonSubexpressionEliminationInterp. Require Import Crypto.Compilers.Z.CommonSubexpressionEliminationWf.*) Require Import Crypto.Compilers.Z.ArithmeticSimplifierWf. +Require Import Crypto.Compilers.Z.RewriteAddToAdc. +Require Import Crypto.Compilers.Z.RewriteAddToAdcWf. +Require Import Crypto.Compilers.Z.RewriteAddToAdcInterp. Require Import Crypto.Compilers.Z.Bounds.MapCastByDeBruijn. Require Import Crypto.Compilers.Z.Bounds.MapCastByDeBruijnInterp. Require Import Crypto.Compilers.Z.Bounds.MapCastByDeBruijnWf. @@ -91,6 +94,7 @@ Definition PostWfPipeline let e := SimplifyArith e in let e := if opts.(anf) then ANormal e else e in let e := InlineConst e in + let e := RewriteAdc e in (*let e := CSE false e in*) let e := MapCast _ e input_bounds in option_map diff --git a/src/Compilers/Z/Named/RewriteAddToAdc.v b/src/Compilers/Z/Named/RewriteAddToAdc.v new file mode 100644 index 000000000..c64663c8b --- /dev/null +++ b/src/Compilers/Z/Named/RewriteAddToAdc.v @@ -0,0 +1,97 @@ +Require Import Coq.ZArith.ZArith. +Require Import Crypto.Compilers.Named.Context. +Require Import Crypto.Compilers.Syntax. +Require Import Crypto.Compilers.Z.Syntax. +Require Import Crypto.Compilers.Named.GetNames. +Require Crypto.Compilers.Named.Syntax. +Require Import Crypto.Util.LetIn. +Require Import Crypto.Util.Notations. + +Local Open Scope Z_scope. + +Section named. + Context {Name : Type} + (name_beq : Name -> Name -> bool). + Import Named.Syntax. + Local Notation flat_type := (flat_type base_type). + Local Notation type := (type base_type). + Local Notation exprf := (@exprf base_type op Name). + Local Notation expr := (@expr base_type op Name). + + Local Notation tZ := (Tbase TZ). + Local Notation ADC bw c x y := (Op (@AddWithGetCarry bw TZ TZ TZ TZ TZ) + (Pair (Pair (t1:=tZ) c (t2:=tZ) x) (t2:=tZ) y)). + Local Notation ADD bw x y := (ADC bw (Op (OpConst 0) TT) x y). + Local Notation ADX x y := (Op (@Add TZ TZ TZ) (Pair (t1:=tZ) x (t2:=tZ) y)). + Local Infix "=Z?" := Z.eqb. + Local Infix "=n?" := name_beq. + + Definition is_const_or_var {t} (v : exprf t) + := match v with + | Var _ _ => true + | Op _ _ (OpConst _ _) TT => true + | _ => false + end. + + Fixpoint name_list_has_duplicate (ls : list Name) : bool + := match ls with + | nil => false + | cons n ns + => orb (name_list_has_duplicate ns) + (List.fold_left orb (List.map (name_beq n) ns) false) + end. + + Definition do_rewrite + {t} (e : exprf t) + : option (exprf t) + := match e in Named.exprf _ _ _ t return option (exprf t) with + | (nlet (a2, c1) : tZ * tZ := (ADD bw1 a b as ex0) in P0) + => match P0 in Named.exprf _ _ _ t return option (exprf t) with + | (nlet (s , c2) : tZ * tZ := (ADD bw2 c0 (Var _ a2') as ex1) in P1) + => match P1 in Named.exprf _ _ _ t return option (exprf t) with + | (nlet c : tZ := (ADX (Var _ c1') (Var _ c2') as ex2) in P) + => if (((bw1 =Z? bw2) && (a2 =n? a2') && (c1 =n? c1') && (c2 =n? c2')) + && (is_const_or_var c0 && is_const_or_var a && is_const_or_var b) + && negb (name_list_has_duplicate (a2::c1::s::c2::c::nil ++ get_namesf c0 ++ get_namesf a ++ get_namesf b)%list)) + then Some (nlet (a2, c1) : tZ * tZ := ex0 in + nlet (s , c2) : tZ * tZ := ex1 in + nlet c : tZ := ex2 in + nlet (s, c) : tZ * tZ := ADC bw1 c0 a b in + P) + else None + | P1' => None + end + | P0' => None + end + | _ => None + end%core%nexpr%bool. + + Definition do_rewriteo {t} (e : exprf t) : exprf t + := match do_rewrite e with + | Some e' => e' + | None => e + end. + + Definition rewrite_exprf_prestep + (rewrite_exprf : forall {t} (e : exprf t), exprf t) + {t} (e : exprf t) + : exprf t + := match e in Named.exprf _ _ _ t return exprf t with + | TT => TT + | Var _ n => Var n + | Op _ _ opc args + => Op opc (@rewrite_exprf _ args) + | (nlet nx := ex in eC) + => (nlet nx := @rewrite_exprf _ ex in @rewrite_exprf _ eC) + | Pair tx ex ty ey + => Pair (@rewrite_exprf tx ex) (@rewrite_exprf ty ey) + end%nexpr. + + Fixpoint rewrite_exprf {t} (e : exprf t) : exprf t + := do_rewriteo (@rewrite_exprf_prestep (@rewrite_exprf) t e). + + Definition rewrite_expr {t} (e : expr t) : expr t + := match e in Named.expr _ _ _ t return expr t with + | Abs _ _ n f => Abs n (rewrite_exprf f) + end. +End named. diff --git a/src/Compilers/Z/Named/RewriteAddToAdcInterp.v b/src/Compilers/Z/Named/RewriteAddToAdcInterp.v new file mode 100644 index 000000000..91a73cfc6 --- /dev/null +++ b/src/Compilers/Z/Named/RewriteAddToAdcInterp.v @@ -0,0 +1,281 @@ +Require Import Coq.ZArith.ZArith. +Require Import Crypto.Compilers.Named.Context. +Require Import Crypto.Compilers.Named.ContextDefinitions. +Require Import Crypto.Compilers.Named.ContextProperties.Proper. +Require Import Crypto.Compilers.Syntax. +Require Import Crypto.Compilers.Z.Syntax. +Require Import Crypto.Compilers.Z.Syntax.Equality. +Require Import Crypto.Compilers.Z.Named.RewriteAddToAdc. +Require Import Crypto.Compilers.Named.Syntax. +Require Import Crypto.Util.Notations. +Require Import Crypto.Util.Option. +Require Import Crypto.Util.Tactics.DestructHead. +Require Import Crypto.Util.Tactics.BreakMatch. +Require Import Crypto.Util.Prod. +Require Import Crypto.Util.LetIn. +Require Import Crypto.Util.Bool. +Require Import Crypto.Util.ZUtil.AddGetCarry. +Require Import Crypto.Util.Decidable. + +Local Open Scope Z_scope. + +Section named. + Context {Name : Type} + {InterpContext : Context Name interp_base_type} + {InterpContextOk : ContextOk InterpContext} + (Name_beq : Name -> Name -> bool) + (Name_bl : forall n1 n2, Name_beq n1 n2 = true -> n1 = n2) + (Name_lb : forall n1 n2, n1 = n2 -> Name_beq n1 n2 = true). + + Local Notation exprf := (@exprf base_type op Name). + Local Notation expr := (@expr base_type op Name). + Local Notation do_rewrite := (@do_rewrite Name Name_beq). + Local Notation do_rewriteo := (@do_rewriteo Name Name_beq). + Local Notation rewrite_exprf := (@rewrite_exprf Name Name_beq). + Local Notation rewrite_exprf_prestep := (@rewrite_exprf_prestep Name). + Local Notation rewrite_expr := (@rewrite_expr Name Name_beq). + + Local Instance Name_dec : DecidableRel (@eq Name) + := dec_rel_of_bool_dec_rel Name_beq Name_bl Name_lb. + + Local Notation retT e re := + (forall (ctx : InterpContext) + v, + Named.interpf (interp_op:=interp_op) (ctx:=ctx) re = Some v + -> Named.interpf (interp_op:=interp_op) (ctx:=ctx) e = Some v) + (only parsing). + Local Notation tZ := (Tbase TZ). + Local Notation ADC bw c x y := (Op (@AddWithGetCarry bw TZ TZ TZ TZ TZ) + (Pair (Pair (t1:=tZ) c (t2:=tZ) x) (t2:=tZ) y)). + Local Notation ADD bw x y := (ADC bw (Op (OpConst 0) TT) x y). + Local Notation ADX x y := (Op (@Add TZ TZ TZ) (Pair (t1:=tZ) x (t2:=tZ) y)). + + Local Ltac simple_t_step := + first [ discriminate + | exact I + | progress intros + | progress subst + | progress inversion_option ]. + Local Ltac destruct_t_step := + first [ break_innermost_match_hyps_step + | break_innermost_match_step ]. + Local Ltac do_small_inversion e := + is_var e; + lazymatch type of e with + | exprf ?T + => revert dependent e; + let P := match goal with |- forall e, @?P e => P end in + intro e; + lazymatch T with + | Unit + => refine match e in Named.exprf _ _ _ t return match t return Named.exprf _ _ _ t -> _ with Unit => P | _ => fun _ => True end e with TT => _ | _ => _ end + | tZ + => refine match e in Named.exprf _ _ _ t return match t return Named.exprf _ _ _ t -> _ with tZ => P | _ => fun _ => True end e with TT => _ | _ => _ end + | (tZ * tZ)%ctype + => refine match e in Named.exprf _ _ _ t return match t return Named.exprf _ _ _ t -> _ with (tZ * tZ)%ctype => P | _ => fun _ => True end e with TT => _ | _ => _ end + | (tZ * tZ * tZ)%ctype + => refine match e in Named.exprf _ _ _ t return match t return Named.exprf _ _ _ t -> _ with (tZ * tZ * tZ)%ctype => P | _ => fun _ => True end e with TT => _ | _ => _ end + end; + try exact I + | op ?a ?T + => first [ is_var a; + move e at top; + revert dependent a; + let P := match goal with |- forall a e, @?P a e => P end in + intros a e; + lazymatch T with + | tZ + => refine match e in op a t return match t return op a t -> _ with tZ => P a | _ => fun _ => True end e with OpConst _ _ => _ | _ => _ end + | (tZ * tZ)%ctype + => refine match e in op a t return match t return op a t -> _ with (tZ * tZ)%ctype => P a | _ => fun _ => True end e with OpConst _ _ => _ | _ => _ end + end ]; + try exact I + end. + Local Ltac small_inversion_step _ := + match goal with + | [ H : match ?e with _ => _ end = Some _ |- _ ] => do_small_inversion e + | [ H : match ?e with _ => _ end = true |- _ ] => do_small_inversion e + | [ H : match ?e with _ => _ end _ = Some _ |- _ ] => do_small_inversion e + end. + + Local Ltac rewrite_lookupb_step := + first [ rewrite !lookupb_extendb_different in * by (assumption || congruence) + | rewrite !lookupb_extendb_same in * by assumption + | rewrite !lookupb_extendb_wrong_type in * by (assumption || congruence) + | match goal with + | [ H : context[lookupb (extendb _ _ _) _] |- _ ] => revert H + | [ |- context[lookupb (extendb _ ?n _) ?n'] ] + => (tryif constr_eq n n' then fail else idtac); + lazymatch goal with + | [ H : n = n' |- _ ] => fail + | [ H : n' = n |- _ ] => fail + | [ H : n <> n' |- _ ] => fail + | [ H : n' <> n |- _ ] => fail + | _ => destruct (dec (n = n')); subst + end + | [ |- context[lookupb (t:=?t0) (extendb (t:=?t1) _ _ _) _] ] + => (tryif constr_eq t0 t1 then fail else idtac); + lazymatch goal with + | [ H : t0 = t1 |- _ ] => fail + | [ H : t1 = t0 |- _ ] => fail + | [ H : t0 <> t1 |- _ ] => fail + | [ H : t1 <> t0 |- _ ] => fail + | _ => destruct (dec (t0 = t1)); subst + end + end ]. + Local Ltac rewrite_lookupb := repeat rewrite_lookupb_step. + + Local Ltac do_rewrite_adc' P := + let lem := open_constr:(Z.add_get_carry_to_add_with_get_carry_cps _ _ _ _ P) in + let T := type of lem in + let T := (eval cbv [Let_In Definitions.Z.add_with_get_carry Definitions.Z.add_with_get_carry Definitions.Z.get_carry Definitions.Z.add_get_carry] in T) in + etransitivity; [ | eapply (lem : T) ]; + try reflexivity. + Local Ltac do_rewrite_adc := + first [ do_rewrite_adc' uconstr:(fun a b => Some b) + | do_rewrite_adc' uconstr:(fun a b => Some a) ]. + + Lemma interpf_do_rewrite + {t} {e e' : exprf t} + (H : do_rewrite e = Some e') + : retT e e'. + Proof. + unfold do_rewrite in H; + repeat first [ simple_t_step + | small_inversion_step () + | destruct_t_step ]. + Time all:match goal with + | [ H : _ = ?x |- _ = ?x ] => rewrite <- H; clear H + end. + Time all:split_andb. + Time all:progress simpl @negb in *. + Time all:repeat match goal with + | [ H : Name_beq _ _ = true |- _ ] => apply Name_bl in H + | [ H : Z.eqb _ _ = true |- _ ] => apply Z.eqb_eq in H + end. + Time all:subst. + Local Ltac do_small_inversion_ctx := + repeat match goal with + | [ H : is_const_or_var ?e = true |- _ ] + => do_small_inversion e; break_innermost_match; intros; try exact I; + simpl in H; try solve [ clear -H; discriminate ] + | [ H : match ?e with _ => _ end = true |- _ ] + => do_small_inversion e; break_innermost_match; intros; try exact I; + simpl in H; try solve [ clear -H; discriminate ] + | [ H : match ?e with _ => _ end _ = true |- _ ] + => do_small_inversion e; break_innermost_match; intros; try exact I; + simpl in H; try solve [ clear -H; discriminate ] + end. + Time all:do_small_inversion_ctx. + Time all:simpl @negb in *. + Time all:rewrite !Bool.negb_orb in *. + Time all:split_andb. + Time all:rewrite !Bool.negb_true_iff in *. + Time all:repeat + match goal with + | [ H : Name_beq ?x ?y = false |- _ ] + => assert (x <> y) by (clear -H Name_lb; intro; rewrite Name_lb in H by assumption; congruence); + clear H + end. + Time all:subst. + Time all:simpl @interpf in *. + Time all:cbv [interp_op option_map lift_op Zinterp_op] in *; simpl in *. + Time all:unfold Let_In in * |- . + Time all:break_innermost_match; try reflexivity. + Local Ltac t_fin_step := + match goal with + | [ |- ?x = ?x ] => reflexivity + | [ H : ?x = Some _ |- context[?x] ] => rewrite H + | [ H : ?x = None |- context[?x] ] => rewrite H + | [ H : ?x = Some ?a, H' : ?x = Some ?b |- _ ] + => assert (a = b) by congruence; (subst a || subst b) + | _ => progress rewrite_lookupb + | _ => progress simpl in * + | _ => progress intros + | _ => progress subst + | _ => progress inversion_option + | [ |- (dlet x := _ in _) = (dlet y := _ in _) ] + => apply Proper_Let_In_nd_changebody_eq; intros ?? + | _ => progress unfold Let_In + | [ |- interpf ?x = interpf ?x ] + => eapply @interpf_Proper; [ eauto with typeclass_instances.. | intros ?? | reflexivity ] + | _ => progress break_innermost_match; try reflexivity + | _ => progress break_innermost_match_hyps; try reflexivity + | _ => progress break_match; try reflexivity + end. + Local Ltac t_fin := + repeat t_fin_step; + try do_rewrite_adc. + { Time t_fin. } + { Time t_fin. } + { Time t_fin. } + { Time t_fin. } + { Time t_fin. } + { Time t_fin. } + { Time t_fin. } + { Time t_fin. } + Time Qed. + + Lemma interpf_do_rewriteo + {t} {e : exprf t} + : retT e (do_rewriteo e). + Proof. + unfold do_rewriteo; intros *; break_innermost_match; try congruence. + apply interpf_do_rewrite; assumption. + Qed. + + Local Opaque RewriteAddToAdc.do_rewriteo. + Lemma interpf_rewrite_exprf + {t} (e : exprf t) + : retT e (rewrite_exprf e). + Proof. + pose t as T. + pose (rewrite_exprf_prestep (@rewrite_exprf) e) as E. + induction e; simpl in *; + intros ctx v H; + pose proof (interpf_do_rewriteo (t:=T) (e:=E) ctx v H); clear H; + subst T E; + repeat first [ assumption + | progress unfold option_map, Let_In in * + | progress simpl in * + | progress subst + | progress inversion_option + | apply (f_equal (@Some _)) + | break_innermost_match_step + | break_innermost_match_hyps_step + | congruence + | solve [ eauto ] + | match goal with + | [ IH : forall ctx v, interpf ?e = Some v -> _ = Some _, H' : interpf ?e = Some _ |- _ ] + => specialize (IH _ _ H') + | [ H : ?x = Some ?a, H' : ?x = Some ?b |- _ ] + => assert (a = b) by congruence; (subst a || subst b) + | [ |- ?rhs = Some _ ] + => lazymatch rhs with + | Some _ => fail + | None => fail + | _ => destruct rhs eqn:? + end + end ]. + Qed. + + Lemma interp_rewrite_expr + {t} (e : expr t) + : forall (ctx : InterpContext) + v x, + Named.interp (interp_op:=interp_op) (ctx:=ctx) (rewrite_expr e) x = Some v + -> Named.interp (interp_op:=interp_op) (ctx:=ctx) e x = Some v. + Proof. + unfold Named.interp, rewrite_expr; destruct e; simpl. + intros *; apply interpf_rewrite_exprf. + Qed. + + Lemma Interp_rewrite_expr + {t} (e : expr t) + : forall v x, + Named.Interp (Context:=InterpContext) (interp_op:=interp_op) (rewrite_expr e) x = Some v + -> Named.Interp (Context:=InterpContext) (interp_op:=interp_op) e x = Some v. + Proof. + intros *; apply interp_rewrite_expr. + Qed. +End named. diff --git a/src/Compilers/Z/RewriteAddToAdc.v b/src/Compilers/Z/RewriteAddToAdc.v new file mode 100644 index 000000000..5f3fc05c5 --- /dev/null +++ b/src/Compilers/Z/RewriteAddToAdc.v @@ -0,0 +1,58 @@ +Require Import Coq.ZArith.ZArith. +Require Import Crypto.Compilers.Named.Context. +Require Import Crypto.Compilers.Named.Syntax. +Require Import Crypto.Compilers.Named.InterpretToPHOAS. +Require Import Crypto.Compilers.Named.Compile. +Require Import Crypto.Compilers.Named.Wf. +Require Import Crypto.Compilers.Named.CountLets. +Require Import Crypto.Compilers.Named.PositiveContext. +Require Import Crypto.Compilers.Named.PositiveContext.Defaults. +Require Import Crypto.Compilers.Syntax. +Require Import Crypto.Compilers.ExprInversion. +Require Import Crypto.Compilers.Z.Syntax. +Require Import Crypto.Compilers.Z.Named.DeadCodeElimination. +Require Import Crypto.Compilers.Z.Named.RewriteAddToAdc. +Require Import Crypto.Util.PointedProp. +Require Import Crypto.Util.Decidable. + +(** N.B. This procedure only works when there are no nested lets, + i.e., nothing like [let x := let y := z in w] in the PHOAS syntax + tree. This is a limitation of [compile]. *) + +Local Open Scope bool_scope. + +Section language. + Local Notation PContext var := (PositiveContext _ var _ internal_base_type_dec_bl). + + Definition RewriteAdc {t} (e : Expr base_type op t) + : Expr base_type op t + := let is_good e' := match option_map (wf_unit (Context:=PContext _) empty) e' with + | Some (Some trivial) => true + | _ => false + end in + let interp_to_phoas := InterpToPHOAS (Context:=fun var => PContext var) + (fun _ t => Op (OpConst 0%Z) TT) in + let e' := compile (e _) (DefaultNamesFor e) in + let e' := option_map (rewrite_expr Pos.eqb) e' in + let good := is_good e' in + let e' := match e' with + | Some e' + => let ls := Named.default_names_for e' in + match EliminateDeadCode (Context:=PContext _) e' ls with + | Some e'' => Some e'' + | None => Some e' + end + | None => None + end in + let good := good && is_good e' in + if good + then let e' := option_map interp_to_phoas e' in + match e' with + | Some e' + => match t return Expr _ _ (Arrow (domain t) (codomain t)) -> Expr _ _ t with + | Arrow _ _ => fun x => x + end e' + | None => e + end + else e. +End language. diff --git a/src/Compilers/Z/RewriteAddToAdcInterp.v b/src/Compilers/Z/RewriteAddToAdcInterp.v new file mode 100644 index 000000000..4269cf09c --- /dev/null +++ b/src/Compilers/Z/RewriteAddToAdcInterp.v @@ -0,0 +1,71 @@ +Require Import Crypto.Compilers.Named.PositiveContext. +Require Import Crypto.Compilers.Named.PositiveContext.DefaultsProperties. +Require Import Crypto.Compilers.Named.ContextDefinitions. +Require Import Crypto.Compilers.Named.InterpretToPHOASInterp. +Require Import Crypto.Compilers.Named.CompileWf. +Require Import Crypto.Compilers.Named.CompileInterp. +Require Import Crypto.Compilers.Named.WfFromUnit. +Require Import Crypto.Compilers.Named.DeadCodeEliminationInterp. +Require Import Crypto.Compilers.Named.WfInterp. +Require Import Crypto.Compilers.Syntax. +Require Import Crypto.Compilers.Wf. +Require Import Crypto.Compilers.Z.Syntax. +Require Import Crypto.Compilers.Z.RewriteAddToAdc. +Require Import Crypto.Compilers.Z.Named.RewriteAddToAdcInterp. +Require Import Crypto.Util.Tactics.BreakMatch. +Require Import Crypto.Util.Decidable. +Require Import Crypto.Util.Bool. + +Section language. + Local Notation PContext var := (PositiveContext _ var _ internal_base_type_dec_bl). + + Lemma InterpRewriteAdc + {t} (e : Expr base_type op t) (Hwf : Wf e) + : forall x, Interp interp_op (RewriteAdc e) x = Interp interp_op e x. + Proof. + intro x; unfold RewriteAdc, option_map; break_innermost_match; try reflexivity; + match goal with |- ?x = ?y => cut (Some x = Some y); [ congruence | ] end; + (etransitivity; [ symmetry; eapply @Interp_InterpToPHOAS with (t:=Arrow _ _) | ]); + repeat + repeat + first [ lazymatch goal with + | [ H : DeadCodeElimination.EliminateDeadCode _ _ = Some ?e |- Syntax.Named.Interp ?e _ = Some _ ] + => let lhs := match goal with |- ?lhs = _ => lhs end in + let v := fresh in + (destruct lhs as [v|] eqn:?); + [ apply f_equal; eapply @InterpEliminateDeadCode with (Name_beq:=BinPos.Pos.eqb); + [ .. | eassumption | try eassumption | try eassumption ]; clear H | ] + | [ |- Syntax.Named.Interp (RewriteAddToAdc.rewrite_expr _ ?e) _ = Some _ ] + => let lhs := match goal with |- ?lhs = _ => lhs end in + let H := fresh in + destruct lhs eqn:H; [ apply (f_equal (@Some _)); eapply @Interp_rewrite_expr in H | ] + | [ H : Compile.compile (?e _) _ = Some ?e'', H' : Syntax.Named.Interp ?e'' ?x = Some ?v' |- ?v' = Interp ?interp_op' ?e ?x ] + => eapply @Interp_compile with (v:=x) (interp_op:=interp_op') in H + end + | intros; eapply (@PositiveContextOk _ _ base_type_beq internal_base_type_dec_bl internal_base_type_dec_lb) + | progress split_andb + | congruence + | tauto + | solve [ auto | eapply @BinPos.Pos.eqb_eq; auto ] + | eapply @Wf_from_unit + | eapply @dec_rel_of_bool_dec_rel + | eapply @internal_base_type_dec_lb + | eapply @internal_base_type_dec_bl + | eapply @InterpEliminateDeadCode; [ .. | eassumption | eassumption | ] + | apply name_list_unique_DefaultNamesFor + | progress intros + | rewrite !@lookupb_empty + | eapply @wf_from_unit with (uContext:=PContext _); [ .. | eassumption ] + | match goal with + | [ H : Syntax.Named.Interp ?e ?x = Some ?a, H' : Syntax.Named.Interp ?e ?x = Some ?b |- _ ] + => assert (a = b) by congruence; (subst a || subst b) + end + | lazymatch goal with + | [ |- Some _ = Some _ ] => fail + | [ |- None = Some _ ] => exfalso; eapply @wf_interp_not_None; [ .. | unfold Syntax.Named.Interp in *; eassumption ] + | [ |- ?x = Some _ ] => destruct x eqn:?; [ apply f_equal | ] + end ]. + Qed. +End language. + +Hint Rewrite @InterpRewriteAdc using solve_wf_side_condition : reflective_interp. diff --git a/src/Compilers/Z/RewriteAddToAdcWf.v b/src/Compilers/Z/RewriteAddToAdcWf.v new file mode 100644 index 000000000..3b9fb1ff5 --- /dev/null +++ b/src/Compilers/Z/RewriteAddToAdcWf.v @@ -0,0 +1,35 @@ +Require Import Crypto.Compilers.Named.PositiveContext. +Require Import Crypto.Compilers.Named.InterpretToPHOASWf. +Require Import Crypto.Compilers.Named.CompileWf. +Require Import Crypto.Compilers.Named.WfFromUnit. +Require Import Crypto.Compilers.Syntax. +Require Import Crypto.Compilers.Wf. +Require Import Crypto.Compilers.Z.Syntax. +Require Import Crypto.Compilers.Z.RewriteAddToAdc. +Require Import Crypto.Util.Tactics.BreakMatch. +Require Import Crypto.Util.Decidable. +Require Import Crypto.Util.Bool. + +Section language. + Local Hint Resolve internal_base_type_dec_lb internal_base_type_dec_lb dec_rel_of_bool_dec_rel : typeclass_instances. + + Lemma Wf_RewriteAdc {t} (e : Expr base_type op t) (Hwf : Wf e) + : Wf (RewriteAdc e). + Proof. + unfold RewriteAdc, option_map; break_innermost_match; + [ .. | solve [ intros var1 var2; destruct (Hwf var1 var2); auto with wf ] ]; + repeat first [ eapply @Wf_InterpToPHOAS with (t:=Arrow _ _) + | progress split_andb + | congruence + | intros; eapply @PositiveContextOk + | solve [ auto | eapply @BinPos.Pos.eqb_eq ] + | eapply @Wf_from_unit + | eapply @dec_rel_of_bool_dec_rel + | eapply @internal_base_type_dec_lb + | eapply @internal_base_type_dec_bl + | intros var1 var2; specialize (Hwf var1 var2); destruct Hwf; + constructor; assumption ]. + Qed. +End language. + +Hint Resolve Wf_RewriteAdc : wf. diff --git a/src/Specific/IntegrationTestFreeze.v b/src/Specific/IntegrationTestFreeze.v index 12f107be6..74731f6c6 100644 --- a/src/Specific/IntegrationTestFreeze.v +++ b/src/Specific/IntegrationTestFreeze.v @@ -71,7 +71,7 @@ Section BoundedField25p5. apply (fun f => proj2_sig_map (fun THIS_NAME_MUST_NOT_BE_UNDERSCORE_TO_WORK_AROUND_CONSTR_MATCHING_ANAOMLIES___BUT_NOTE_THAT_IF_THIS_NAME_IS_LOWERCASE_A___THEN_REIFICATION_STACK_OVERFLOWS___AND_I_HAVE_NO_IDEA_WHATS_GOING_ON p => f_equal f p)). (* jgross start here! *) (*Set Ltac Profiling.*) - Time refine_reflectively. (* Finished transaction in 5.792 secs (5.792u,0.004s) (successful) *) + Time refine_reflectively_with anf. (* Finished transaction in 5.792 secs (5.792u,0.004s) (successful) *) (*Show Ltac Profile.*) (* total time: 5.680s -- cgit v1.2.3