From 58972e8383e2e4ee9fab27771bccfffefce828d4 Mon Sep 17 00:00:00 2001 From: Jason Gross Date: Fri, 19 May 2017 18:31:29 -0400 Subject: Add adc -> sbb to arithmetic simplifer After | File Name | Before || Change --------------------------------------------------------------------------------------- 6m14.04s | Total | 6m23.68s || -0m09.63s --------------------------------------------------------------------------------------- 0m26.28s | Compilers/Z/ArithmeticSimplifierWf | 0m48.67s || -0m22.39s 0m25.64s | Compilers/Z/ArithmeticSimplifierInterp | 0m14.14s || +0m11.50s 2m17.60s | Specific/IntegrationTestLadderstep | 2m17.90s || -0m00.30s 0m56.48s | Compilers/Z/Named/RewriteAddToAdcInterp | 0m55.76s || +0m00.71s 0m54.26s | Specific/IntegrationTestLadderstep130 | 0m54.53s || -0m00.27s 0m15.89s | Specific/IntegrationTestFreeze | 0m15.07s || +0m00.82s 0m11.69s | Specific/IntegrationTestMul | 0m11.78s || -0m00.08s 0m10.62s | Specific/ArithmeticSynthesisTest | 0m10.59s || +0m00.02s 0m10.54s | Specific/IntegrationTestSub | 0m10.55s || -0m00.01s 0m08.98s | Specific/IntegrationTestSquare | 0m09.04s || -0m00.05s 0m06.05s | Arithmetic/Saturated | 0m06.02s || +0m00.03s 0m03.04s | Compilers/Z/RewriteAddToAdcInterp | 0m03.00s || +0m00.04s 0m02.60s | Compilers/Z/Bounds/Pipeline/Definition | 0m02.25s || +0m00.35s 0m01.52s | Util/ZUtil/AddGetCarry | 0m01.50s || +0m00.02s 0m00.74s | Arithmetic/MontgomeryReduction/WordByWord/Definition | 0m00.71s || +0m00.03s 0m00.62s | Compilers/Z/Bounds/Pipeline/ReflectiveTactics | 0m00.78s || -0m00.16s 0m00.59s | Compilers/Z/ArithmeticSimplifier | 0m00.42s || +0m00.17s 0m00.57s | Compilers/Z/Bounds/Pipeline | 0m00.60s || -0m00.03s 0m00.34s | Compilers/Z/ArithmeticSimplifierUtil | 0m00.37s || -0m00.02s --- src/Compilers/Z/ArithmeticSimplifier.v | 104 +++++++++++++++++++++ src/Compilers/Z/ArithmeticSimplifierInterp.v | 64 +++++++++++-- src/Compilers/Z/ArithmeticSimplifierWf.v | 133 ++++++++++++++++++++++----- src/Compilers/Z/Bounds/Pipeline/Definition.v | 7 +- src/Util/ZUtil/AddGetCarry.v | 4 + 5 files changed, 276 insertions(+), 36 deletions(-) (limited to 'src') diff --git a/src/Compilers/Z/ArithmeticSimplifier.v b/src/Compilers/Z/ArithmeticSimplifier.v index 7a2a73434..2690f2dfb 100644 --- a/src/Compilers/Z/ArithmeticSimplifier.v +++ b/src/Compilers/Z/ArithmeticSimplifier.v @@ -176,6 +176,110 @@ Section language. | _ => Op opc args end + | AddWithCarry TZ TZ TZ TZ as opc + => fun args + => match interp_as_expr_or_const args with + | Some (const_of c, const_of x, const_of y) + => Op (OpConst (interp_op _ _ opc (c, x, y))) TT + | Some (c, gen_expr x, y) + => let y' := match y with + | const_of y => if (y Some y + | gen_expr _ => None + end in + match y' with + | Some y => Op (SubWithBorrow TZ TZ TZ TZ) + (match c with + | const_of c => Op (OpConst (-c)) TT + | neg_expr c => c + | gen_expr c => Op (Opp TZ TZ) c + end, + x, y)%expr + | None => Op opc args + end + | _ => Op opc args + end + | AddWithGetCarry bw TZ TZ TZ TZ TZ as opc + => fun args + => match interp_as_expr_or_const args with + | Some (const_of c, const_of x, const_of y) + => let '(v, c) := interp_op _ _ opc (c, x, y) in + (Op (OpConst v) TT, Op (OpConst c) TT)%expr + | Some (c, gen_expr x, y) + => let y' := match y with + | const_of y => if (y Some y + | gen_expr _ => None + end in + match y' with + | Some y => LetIn (Op (SubWithGetBorrow bw TZ TZ TZ TZ TZ) + (match c with + | const_of c => Op (OpConst (-c)) TT + | neg_expr c => c + | gen_expr c => Op (Opp TZ TZ) c + end, + x, y)%expr) + (fun '(v, c) => (Var v, Op (Opp TZ TZ) (Var c))%expr) + | None => Op opc args + end + | _ => Op opc args + end + | SubWithBorrow TZ TZ TZ TZ as opc + => fun args + => match interp_as_expr_or_const args with + | Some (const_of c, const_of x, const_of y) + => Op (OpConst (interp_op _ _ opc (c, x, y))) TT + | Some (c, gen_expr x, y) + => let y' := match y with + | const_of y => if (y Some y + | gen_expr _ => None + end in + match y' with + | Some y => Op (AddWithCarry TZ TZ TZ TZ) + (match c with + | const_of c => Op (OpConst (-c)) TT + | neg_expr c => c + | gen_expr c => Op (Opp TZ TZ) c + end, + x, y)%expr + | None => Op opc args + end + | _ => Op opc args + end + | SubWithGetBorrow bw TZ TZ TZ TZ TZ as opc + => fun args + => match interp_as_expr_or_const args with + | Some (const_of c, const_of x, const_of y) + => let '(v, c) := interp_op _ _ opc (c, x, y) in + (Op (OpConst v) TT, Op (OpConst c) TT)%expr + | Some (c, gen_expr x, y) + => let y' := match y with + | const_of y => if (y Some y + | gen_expr _ => None + end in + match y' with + | Some y => LetIn (Op (AddWithGetCarry bw TZ TZ TZ TZ TZ) + (match c with + | const_of c => Op (OpConst (-c)) TT + | neg_expr c => c + | gen_expr c => Op (Opp TZ TZ) c + end, + x, y)%expr) + (fun '(v, c) => (Var v, Op (Opp TZ TZ) (Var c))%expr) + | None => Op opc args + end + | _ => Op opc args + end | Add _ _ _ as opc | Sub _ _ _ as opc | Mul _ _ _ as opc diff --git a/src/Compilers/Z/ArithmeticSimplifierInterp.v b/src/Compilers/Z/ArithmeticSimplifierInterp.v index 6eec2f2a4..1f638c076 100644 --- a/src/Compilers/Z/ArithmeticSimplifierInterp.v +++ b/src/Compilers/Z/ArithmeticSimplifierInterp.v @@ -10,6 +10,7 @@ Require Import Crypto.Compilers.Z.ArithmeticSimplifier. Require Import Crypto.Compilers.Z.ArithmeticSimplifierUtil. Require Import Crypto.Compilers.Z.Syntax.Equality. Require Import Crypto.Util.ZUtil. +Require Import Crypto.Util.ZUtil.AddGetCarry. Require Import Crypto.Util.Option. Require Import Crypto.Util.Prod. Require Import Crypto.Util.Sum. @@ -36,6 +37,7 @@ Local Ltac break_t_step := | progress inversion_prod | progress inversion_inverted_expr | progress inversion_flat_type + | progress subst_prod | progress destruct_head'_and | progress destruct_head'_prod | progress eliminate_hprop_eq @@ -72,6 +74,12 @@ Proof. | progress invert_op ]. } Qed. +Local Ltac rewrite_interp_as_expr_or_const_correct_base _ := + match goal with + | [ |- context[interpf _ ?e] ] + => erewrite !(@interp_as_expr_or_const_correct_base _ e) by eassumption; cbv beta iota + end. + Lemma interp_as_expr_or_const_correct_prod_base {A B} e (v : _ * _) : @interp_as_expr_or_const interp_base_type (Prod (Tbase A) (Tbase B)) e = Some v -> interpf interp_op e = (match fst v with @@ -90,9 +98,48 @@ Proof. | progress simpl in * | progress intros | break_t_step - | erewrite !interp_as_expr_or_const_correct_base by eassumption; cbv beta iota ]. + | rewrite_interp_as_expr_or_const_correct_base () ]. +Qed. + +Local Ltac rewrite_interp_as_expr_or_const_correct_prod_base _ := + match goal with + | [ |- context[interpf _ ?e] ] + => erewrite !(@interp_as_expr_or_const_correct_prod_base _ _ e) by eassumption; cbv beta iota + end. + +Lemma interp_as_expr_or_const_correct_prod3_base {A B C} e (v : _ * _ * _) + : @interp_as_expr_or_const interp_base_type (Prod (Prod (Tbase A) (Tbase B)) (Tbase C)) e = Some v + -> interpf interp_op e = (match fst (fst v) with + | const_of z => cast_const (t1:=TZ) z + | gen_expr e => interpf interp_op e + | neg_expr e => interpf interp_op (Op (Opp _ _) e) + end, + match snd (fst v) with + | const_of z => cast_const (t1:=TZ) z + | gen_expr e => interpf interp_op e + | neg_expr e => interpf interp_op (Op (Opp _ _) e) + end, + match snd v with + | const_of z => cast_const (t1:=TZ) z + | gen_expr e => interpf interp_op e + | neg_expr e => interpf interp_op (Op (Opp _ _) e) + end). +Proof. + invert_expr; + repeat first [ fin_t + | progress simpl in * + | progress intros + | break_t_step + | rewrite_interp_as_expr_or_const_correct_base () + | rewrite_interp_as_expr_or_const_correct_prod_base () ]. Qed. +Local Ltac rewrite_interp_as_expr_or_const_correct_prod3_base _ := + match goal with + | [ |- context[interpf _ ?e] ] + => erewrite !(@interp_as_expr_or_const_correct_prod3_base _ _ _ e) by eassumption; cbv beta iota + end. + Local Arguments Z.mul !_ !_. Local Arguments Z.add !_ !_. Local Arguments Z.sub !_ !_. @@ -104,17 +151,18 @@ Proof. apply InterpRewriteOp; intros; unfold simplify_op_expr. break_innermost_match; repeat first [ fin_t + | progress cbv [LetIn.Let_In] | progress simpl in * | progress subst - | erewrite !interp_as_expr_or_const_correct_prod_base by eassumption; cbv beta iota - | erewrite !interp_as_expr_or_const_correct_base by eassumption; cbv beta iota - | match goal with - | [ |- context[interpf _ ?e] ] - => erewrite !(@interp_as_expr_or_const_correct_base _ e) by eassumption; cbv beta iota - end + | progress subst_prod + | rewrite_interp_as_expr_or_const_correct_base () + | rewrite_interp_as_expr_or_const_correct_prod_base () + | rewrite_interp_as_expr_or_const_correct_prod3_base () | progress unfold interp_op, lift_op | progress Z.ltb_to_lt - | progress rewrite ?Z.land_0_l, ?Z.land_0_r, ?Z.lor_0_l, ?Z.lor_0_r ]. + | progress rewrite ?Z.land_0_l, ?Z.land_0_r, ?Z.lor_0_l, ?Z.lor_0_r + | rewrite !Z.sub_with_borrow_to_add_get_carry + | progress autorewrite with zsimplify_fast ]. Qed. Hint Rewrite @InterpSimplifyArith : reflective_interp. diff --git a/src/Compilers/Z/ArithmeticSimplifierWf.v b/src/Compilers/Z/ArithmeticSimplifierWf.v index 157cdfe8f..ff5068b89 100644 --- a/src/Compilers/Z/ArithmeticSimplifierWf.v +++ b/src/Compilers/Z/ArithmeticSimplifierWf.v @@ -28,7 +28,14 @@ Local Ltac fin_t := | reflexivity | congruence | assumption - | exfalso; assumption ]. + | exfalso; assumption + | match goal with + | [ |- _ /\ False ] => exfalso + | [ |- False /\ _ ] => exfalso + | [ |- _ /\ _ /\ False ] => exfalso + | [ |- _ /\ False /\ _ ] => exfalso + | [ |- False /\ _ /\ _ ] => exfalso + end ]. Local Ltac break_t_step := first [ progress subst | progress inversion_option @@ -43,6 +50,7 @@ Local Ltac break_t_step := | progress destruct_head'_sig | progress specialize_by reflexivity | progress eliminate_hprop_eq + | progress break_innermost_match_hyps_step | progress break_innermost_match_step | progress break_match_hyps | progress inversion_wf_constr ]. @@ -79,6 +87,18 @@ Proof. erewrite <- interp_as_expr_or_const_None_iff by eassumption; congruence. Qed. +Local Ltac pret_step := + first [ fin_t + | progress subst + | progress inversion_option + | progress inversion_prod + | progress simpl in * + | progress inversion_wf + | match goal with + | [ H : match interp_as_expr_or_const ?e with _ => _ end = Some _ |- _ ] + => is_var e; destruct (interp_as_expr_or_const e) eqn:? + end ]. + Lemma wff_interp_as_expr_or_const_base {var1 var2 t} {G e1 e2 v1 v2} (Hwf : @wff var1 var2 G (Tbase t) e1 e2) : @interp_as_expr_or_const var1 (Tbase t) e1 = Some v1 @@ -105,6 +125,12 @@ Proof. end ]. Qed. +Local Ltac pose_wff_base := + match goal with + | [ H1 : _ = Some _, H2 : _ = Some _, Hwf : wff _ _ _ |- _ ] + => pose proof (wff_interp_as_expr_or_const_base Hwf H1 H2); clear H1 H2 + end. + Lemma wff_interp_as_expr_or_const_prod_base {var1 var2 A B} {G e1 e2} {v1 v2 : _ * _} (Hwf : wff G e1 e2) : @interp_as_expr_or_const var1 (Prod (Tbase A) (Tbase B)) e1 = Some v1 @@ -132,39 +158,96 @@ Lemma wff_interp_as_expr_or_const_prod_base {var1 var2 A B} {G e1 e2} {v1 v2 : _ Proof. invert_one_expr e1; intros; break_innermost_match; intros; try exact I; try invert_one_expr e2; intros; break_innermost_match; intros; try exact I; - repeat first [ fin_t - | progress simpl in * + repeat first [ pret_step + | pose_wff_base | break_t_step - | match goal with - | [ H1 : _ = Some _, H2 : _ = Some _, Hwf : wff _ _ _ |- _ ] - => pose proof (wff_interp_as_expr_or_const_base Hwf H1 H2); clear H1 H2 - | [ |- and _ _ ] => split - end ]. + | apply conj ]. Qed. +Local Ltac pose_wff_prod := + match goal with + | [ H1 : _ = Some _, H2 : _ = Some _, Hwf : wff _ _ _ |- _ ] + => pose proof (wff_interp_as_expr_or_const_prod_base Hwf H1 H2); clear H1 H2 + end. + +Lemma wff_interp_as_expr_or_const_prod3_base {var1 var2 A B C} {G e1 e2} {v1 v2 : _ * _ * _} + (Hwf : wff G e1 e2) + : @interp_as_expr_or_const var1 (Prod (Prod (Tbase A) (Tbase B)) (Tbase C)) e1 = Some v1 + -> @interp_as_expr_or_const var2 (Prod (Prod (Tbase A) (Tbase B)) (Tbase C)) e2 = Some v2 + -> match fst (fst v1), fst (fst v2) with + | const_of z1, const_of z2 => z1 = z2 + | gen_expr e1, gen_expr e2 + | neg_expr e1, neg_expr e2 + => wff G e1 e2 + | const_of _, _ + | gen_expr _, _ + | neg_expr _, _ + => False + end + /\ match snd (fst v1), snd (fst v2) with + | const_of z1, const_of z2 => z1 = z2 + | gen_expr e1, gen_expr e2 + | neg_expr e1, neg_expr e2 + => wff G e1 e2 + | const_of _, _ + | gen_expr _, _ + | neg_expr _, _ + => False + end + /\ match snd v1, snd v2 with + | const_of z1, const_of z2 => z1 = z2 + | gen_expr e1, gen_expr e2 + | neg_expr e1, neg_expr e2 + => wff G e1 e2 + | const_of _, _ + | gen_expr _, _ + | neg_expr _, _ + => False + end. +Proof. + invert_one_expr e1; intros; break_innermost_match; intros; try exact I; + try invert_one_expr e2; intros; break_innermost_match; intros; try exact I; + repeat first [ pret_step + | pose_wff_base + | pose_wff_prod + | break_t_step + | apply conj ]. +Qed. + +Local Ltac pose_wff_prod3 := + match goal with + | [ H1 : _ = Some _, H2 : _ = Some _, Hwf : wff _ _ _ |- _ ] + => pose proof (wff_interp_as_expr_or_const_prod3_base Hwf H1 H2); clear H1 H2 + end. + Lemma Wf_SimplifyArith {t} (e : Expr t) (Hwf : Wf e) : Wf (SimplifyArith e). Proof. apply Wf_RewriteOp; [ | assumption ]. intros ???????? Hwf'; unfold simplify_op_expr; - break_innermost_match; repeat constructor; auto; - repeat first [ fin_t - | progress simpl in * - | progress subst - | progress Z.ltb_to_lt - | match goal with - | [ H1 : _ = Some _, H2 : _ = Some _, Hwf : wff _ _ _ |- _ ] - => pose proof (wff_interp_as_expr_or_const_base Hwf H1 H2); clear H1 H2 - | [ H1 : _ = Some _, H2 : _ = Some _, Hwf : wff _ _ _ |- _ ] - => pose proof (wff_interp_as_expr_or_const_prod_base Hwf H1 H2); clear H1 H2 - | [ H1 : _ = Some _, H2 : _ = None, Hwf : wff _ _ _ |- _ ] - => pose proof (interp_as_expr_or_const_Some_None Hwf H1 H2); clear H1 H2 - | [ H1 : _ = None, H2 : _ = Some _, Hwf : wff _ _ _ |- _ ] - => pose proof (interp_as_expr_or_const_None_Some Hwf H1 H2); clear H1 H2 - | [ |- wff _ _ _ ] => constructor - end - | break_t_step ]. + repeat match goal with + | [ H : ?T |- ?T ] => exact H + | [ H : False |- _ ] => exfalso; assumption + | [ H : false = true |- _ ] => exfalso; clear -H; discriminate + | [ H : true = false |- _ ] => exfalso; clear -H; discriminate + | _ => pose_wff_base + | _ => pose_wff_prod + | _ => pose_wff_prod3 + | _ => progress destruct_head'_and + | _ => progress subst + | [ H1 : _ = Some _, H2 : _ = None, Hwf : wff _ _ _ |- _ ] + => pose proof (interp_as_expr_or_const_Some_None Hwf H1 H2); clear H1 H2 + | [ H1 : _ = None, H2 : _ = Some _, Hwf : wff _ _ _ |- _ ] + => pose proof (interp_as_expr_or_const_None_Some Hwf H1 H2); clear H1 H2 + | [ |- wff _ (Op _ _) (LetIn _ _) ] => exfalso + | [ |- wff _ (LetIn _ _) (Op _ _) ] => exfalso + | [ |- wff _ (Pair _ _) (LetIn _ _) ] => exfalso + | [ |- wff _ (LetIn _ _) (Pair _ _) ] => exfalso + | [ |- wff _ _ _ ] => constructor; intros + | [ |- List.In _ _ ] => progress (simpl; auto) + | _ => break_innermost_match_step; simpl in * + end. Qed. Hint Resolve Wf_SimplifyArith : wf. diff --git a/src/Compilers/Z/Bounds/Pipeline/Definition.v b/src/Compilers/Z/Bounds/Pipeline/Definition.v index 8a43a0ec7..b0ec96dbb 100644 --- a/src/Compilers/Z/Bounds/Pipeline/Definition.v +++ b/src/Compilers/Z/Bounds/Pipeline/Definition.v @@ -89,12 +89,13 @@ Definition PostWfPipeline := Build_ProcessedReflectivePackage_from_option_sigma e input_bounds (let e := InlineConst e in - let e := SimplifyArith e in - let e := InlineConst e in - let e := SimplifyArith e in + let e := InlineConst (SimplifyArith e) in + let e := InlineConst (SimplifyArith e) in + let e := InlineConst (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 := InlineConst (SimplifyArith e) in (*let e := CSE false e in*) let e := MapCast _ e input_bounds in option_map diff --git a/src/Util/ZUtil/AddGetCarry.v b/src/Util/ZUtil/AddGetCarry.v index 0208207b3..34f5f2ea8 100644 --- a/src/Util/ZUtil/AddGetCarry.v +++ b/src/Util/ZUtil/AddGetCarry.v @@ -70,4 +70,8 @@ Module Z. reflexivity. Qed. + Lemma sub_with_borrow_to_add_get_carry c x y + : Z.sub_with_borrow c x y = Z.add_with_carry (-c) x (-y). + Proof. reflexivity. Qed. + End Z. -- cgit v1.2.3