From ed7bd2abd3e0ef7d7b994113da7187da2debfe31 Mon Sep 17 00:00:00 2001 From: jadep Date: Mon, 10 Dec 2018 14:48:11 -0500 Subject: WIP: prove that barrett_red256 is a valid expression modulo some issues with rewrite rules (too-tight bound on RSHI and ADDC (0,x,y) not being converted to ADD (x,y) --- src/Experiments/NewPipeline/Toplevel2.v | 263 ++++++++++++++++++++++++++++---- 1 file changed, 232 insertions(+), 31 deletions(-) (limited to 'src/Experiments/NewPipeline/Toplevel2.v') diff --git a/src/Experiments/NewPipeline/Toplevel2.v b/src/Experiments/NewPipeline/Toplevel2.v index 652dd2d53..117381c8c 100644 --- a/src/Experiments/NewPipeline/Toplevel2.v +++ b/src/Experiments/NewPipeline/Toplevel2.v @@ -2144,6 +2144,11 @@ Module Fancy. valid_scalar x -> valid_scalar y -> valid_ident r (new_cc_to_name r MUL128UU) (ident.fancy_mulhh 256) (x, y)%expr_pat + | valid_fancy_rshi : + forall r imm x y, + valid_scalar x -> + valid_scalar y -> + valid_ident r (new_cc_to_name r (RSHI imm)) (ident.fancy_rshi 256 imm) (x, y)%expr_pat | valid_fancy_selc : forall r c x y, (of_prefancy_scalar (t:= base.type.type_base tZ) c = r CC.C) -> @@ -2173,10 +2178,27 @@ Module Fancy. valid_ident r (new_cc_to_name r ADDM) ident.fancy_addm (x, y, m)%expr_pat . + Check valid_ident. + Check + (forall s d idc r rf x f e, + valid_ident r rf idc x -> + LetInAppIdentZZ s d (uint256, r[0~>1]) (expr.Ident idc) x f = e). Inductive valid_expr : forall t, (CC.code -> name) -> (* the last variables that wrote to each flag *) @cexpr var t -> Prop := + | valid_LetInZ_loosen : + forall s d idc r rf x f u ia, + valid_ident r rf idc x -> + 0 < u < wordmax -> + (forall x, valid_expr _ (rf x) (f x)) -> + of_prefancy_ident idc x = Some ia -> + (forall cc ctx, + (forall n v, consts v = Some n -> ctx n = v) -> + (forall n, ctx n mod wordmax = ctx n) -> + let args := Tuple.map ctx (projT2 ia) in + spec (projT1 ia) args cc mod wordmax = spec (projT1 ia) args cc mod (u+1)) -> + valid_expr _ r (LetInAppIdentZ s d r[0~>u] (expr.Ident idc) x f) | valid_LetInZ : forall s d idc r rf x f, valid_ident r rf idc x -> @@ -2185,7 +2207,9 @@ Module Fancy. | valid_LetInZZ : forall s d idc r rf x f, valid_ident r rf idc x -> - (forall x, valid_expr _ (rf x) (f x)) -> + (forall x : var (type.base (base.type.type_base tZ * base.type.type_base tZ)%etype), + fst x = snd x -> + valid_expr _ (rf x) (f x)) -> valid_expr _ r (LetInAppIdentZZ s d (uint256, r[0~>1]) (expr.Ident idc) x f) | valid_Ret : forall r x, @@ -2448,6 +2472,54 @@ Module Fancy. (forall n0 : name, consts 0 = Some n0 -> cctx n0 = false) /\ (forall n1 : name, consts 1 = Some n1 -> cctx n1 = true). + Lemma of_prefancy_identZ_loosen_correct {s} idc: + forall (x : @cexpr var _) i ctx G cc cctx x2 r rf f u, + @valid_ident (type.base s) (type_base tZ) r rf idc x -> + LanguageWf.Compilers.expr.wf G (#idc @ x)%expr_pat x2 -> + LanguageWf.Compilers.expr.wf G #(ident.Z_cast r[0~>u]) f -> + 0 < u < wordmax -> + cc_good cc cctx ctx r -> + (forall n v, consts v = Some n -> In (existZ (n, v)) G) -> + (forall t v1 v2, In (existT _ (type.base t) (v1, v2)) G -> interp_base ctx cctx v1 = v2) -> + (forall n, ctx n mod wordmax = ctx n) -> + of_prefancy_ident idc x = Some i -> + (spec (projT1 i) (Tuple.map ctx (projT2 i)) cc mod wordmax = spec (projT1 i) (Tuple.map ctx (projT2 i)) cc mod (u+1)) -> + spec (projT1 i) (Tuple.map ctx (projT2 i)) cc mod wordmax = (cinterp f (cinterp x2)). + Proof. + Time + inversion 1; inversion 1; cbn [of_prefancy_ident]; hammer; (simplify_ident; [ ]). (* TODO : suuuuuper slow *) + all: + rewrite cast_mod by omega; + match goal with + | H : context [spec _ _ _ mod _ = _] |- ?x mod wordmax = _ mod ?m => + replace (x mod wordmax) with (x mod m) by auto + end. + all: cbn - [Z.shiftl wordmax]; cbv [cc_good] in *; destruct_head'_and; + repeat match goal with + | H : CC.cc_c _ = _ |- _ => rewrite H + | H : CC.cc_m _ = _ |- _ => rewrite H + | H : CC.cc_l _ = _ |- _ => rewrite H + | H : CC.cc_z _ = _ |- _ => rewrite H + | H: of_prefancy_scalar _ = ?r ?c |- _ => rewrite <-H + | _ => progress rewrite ?cc_m_zselect, ?cc_l_zselect by auto + | _ => progress rewrite ?Z.add_modulo_correct, ?Z.geb_leb by auto + | |- context [cinterp ?x] => + erewrite of_prefancy_scalar_correct with (e2:=x) by eauto + | |- context [cinterp ?x] => + erewrite <-of_prefancy_scalar_carry with (e:=x) by eauto + | |- context [if _ (of_prefancy_scalar _) then _ else _ ] => + cbv [Z.zselect Z.b2z]; + break_innermost_match; Z.ltb_to_lt; try reflexivity; + congruence + end; try reflexivity. + + { (* RSHI case *) + cbv [Z.rshi]. + rewrite Z.land_ones, Z.shiftl_mul_pow2 by (cbv; congruence). + change (2 ^ Z.log2 wordmax) with wordmax. + break_innermost_match; try congruence; [ ]. autorewrite with zsimplify_fast. + repeat (f_equal; try ring). } + Qed. Lemma of_prefancy_identZ_correct {s} idc: forall (x : @cexpr var _) i ctx G cc cctx x2 r rf f, @valid_ident (type.base s) (type_base tZ) r rf idc x -> @@ -2460,26 +2532,8 @@ Module Fancy. of_prefancy_ident idc x = Some i -> spec (projT1 i) (Tuple.map ctx (projT2 i)) cc mod wordmax = (cinterp f (cinterp x2)). Proof. - Time - inversion 1; inversion 1; cbn [of_prefancy_ident]; hammer; (simplify_ident; [ ]); (* TODO : suuuuuper slow *) - cbn - [Z.shiftl]; cbv [cc_good] in *; destruct_head'_and; - repeat match goal with - | H : CC.cc_c _ = _ |- _ => rewrite H - | H : CC.cc_m _ = _ |- _ => rewrite H - | H : CC.cc_l _ = _ |- _ => rewrite H - | H : CC.cc_z _ = _ |- _ => rewrite H - | H: of_prefancy_scalar _ = ?r ?c |- _ => rewrite <-H - | _ => progress rewrite ?cc_m_zselect, ?cc_l_zselect by auto - | _ => progress rewrite ?Z.add_modulo_correct, ?Z.geb_leb by auto - | |- context [cinterp ?x] => - erewrite of_prefancy_scalar_correct with (e2:=x) by eauto - | |- context [cinterp ?x] => - erewrite <-of_prefancy_scalar_carry with (e:=x) by eauto - | |- context [if _ (of_prefancy_scalar _) then _ else _ ] => - cbv [Z.zselect Z.b2z]; - break_innermost_match; Z.ltb_to_lt; try reflexivity; - congruence - end; reflexivity. + intros; eapply of_prefancy_identZ_loosen_correct; try eassumption; [ | ]. + { cbn; omega. } { intros; f_equal; ring. } Qed. Lemma of_prefancy_identZZ_correct' {s} idc: forall (x : @cexpr var _) i ctx G cc cctx x2 r rf f, @@ -2669,7 +2723,7 @@ Module Fancy. cbn [of_prefancy of_prefancy_step]; intros; match goal with H : context [interp_base _ _ _ = _] |- _ => pose proof (H (base.type.type_base base.type.Z)) end; - try solve [prove_Ret]; [ | ]; hammer; + try solve [prove_Ret]; [ | | ]; hammer; match goal with | H : context [interp (of_prefancy _ _) _ _ = _] |- interp _ ?cc' ?ctx' = _ => @@ -2699,7 +2753,11 @@ Module Fancy. | _ => solve [eauto using Z.mod_small, b2z_range] | _ => progress autorewrite with zsimplify_fast | _ => progress side_cond - end; [ | ]. + end; [ | | ]. + { cbn - [cc_spec]; cbv [id]; cbn - [cc_spec]. + inversion wf_x; hammer. + erewrite of_prefancy_identZ_loosen_correct by eauto. + reflexivity. } { cbn - [cc_spec]; cbv [id]; cbn - [cc_spec]. inversion wf_x; hammer. erewrite of_prefancy_identZ_correct by eassumption. @@ -2854,6 +2912,11 @@ Module Fancy. end. Qed. + Lemma make_ctx_cases consts_list n : + make_ctx consts_list n = 0 \/ + In (n, make_ctx consts_list n) consts_list. + Proof. induction consts_list; cbn; ez. Qed. + Lemma only_integers consts_list t v1 v2 : In (existT (fun t : type => (var positive t * type.interp base.interp t)%type) (type.base t) (v1, v2)%zrange) (make_pairs consts_list) -> @@ -2868,11 +2931,23 @@ Module Fancy. Proof. intro H; apply only_integers in H. congruence. Qed. + Definition make_cc last_wrote ctx carry_flag : CC.state := + {| CC.cc_c := carry_flag; + CC.cc_m := cc_spec CC.M (ctx (last_wrote CC.M)); + CC.cc_l := cc_spec CC.L (ctx (last_wrote CC.L)); + CC.cc_z := cc_spec CC.Z (ctx (last_wrote CC.Z) + + (if (last_wrote CC.C =? last_wrote CC.Z)%positive + then wordmax * Z.b2z carry_flag else 0)); + |}. + + Hint Resolve Pos.lt_trans Pos.lt_irrefl Pos.lt_succ_diag_r Pos.eqb_refl. Hint Resolve in_or_app. Hint Resolve make_consts_ok make_pairs_ok make_ctx_ok no_pairs. (* TODO : probably not all of these preconditions are necessary -- prune them sometime *) - Lemma of_Expr_correct next_name consts_list arg_list error cc + Lemma of_Expr_correct next_name consts_list arg_list error + (carry_flag : bool) + (last_wrote : CC.code -> positive) (* variables which last wrote to each flag; put RegZero if flag empty *) t (e : Expr t) (x1 : type.for_each_lhs_of_arrow (var positive) t) (x2 : type.for_each_lhs_of_arrow _ t) result : @@ -2880,19 +2955,29 @@ Module Fancy. let e2 := (invert_expr.smart_App_curried (e _) x2) in let ctx := make_ctx (consts_list ++ arg_list) in let consts := make_consts consts_list in + let cc := make_cc last_wrote ctx carry_flag in let G := make_pairs consts_list ++ make_pairs arg_list in + (forall c, last_wrote c < next_name)%positive -> (forall n v, In (n, v) (consts_list ++ arg_list) -> (n < next_name)%positive) -> + (In (last_wrote CC.C, Z.b2z carry_flag) consts_list) -> (forall n v1 v2, In (n, v1) (consts_list ++ arg_list) -> In (n, v2) (consts_list ++ arg_list) -> v1 = v2) (* no duplicate names *) -> (forall v1 v2, In (v1, v2) consts_list -> v2 mod 2 ^ 256 = v2) -> (forall v1 v2, In (v1, v2) arg_list -> v2 mod 2 ^ 256 = v2) -> (LanguageWf.Compilers.expr.wf G e1 e2) -> - valid_expr _ consts _ e1 -> + valid_expr _ error consts _ last_wrote e1 -> interp_if_Z e2 = Some result -> interp Pos.eqb wordmax cc_spec (of_Expr next_name consts e x1 error) cc ctx = result. Proof. cbv [of_Expr]; intros. - eapply of_prefancy_correct with (name_lt := Pos.lt) (cctx := fun _ => false); cbv [id]; eauto; + eapply of_prefancy_correct with (name_lt := Pos.lt) + (cctx := fun n => if (n =? last_wrote CC.C)%positive + then carry_flag + else match make_consts consts_list 1 with + | Some n1 => (n =? n1)%positive + | _ => false + end); + cbv [id]; eauto; try apply Pos.eqb_neq; intros; try solve [apply make_ctx_ok; auto; apply make_pairs_ok; cbv [make_pairs]; rewrite map_app; auto ]; @@ -2904,6 +2989,26 @@ Module Fancy. | _ => solve [eauto] | _ => solve [exfalso; eauto] end. + (* TODO : clean this up *) + { cbv [cc_good make_cc]; repeat split; intros; + [ rewrite Pos.eqb_refl; reflexivity | | ]; + break_innermost_match; try rewrite Pos.eqb_eq in *; subst; try reflexivity; + repeat match goal with + | H : make_consts _ _ = Some _ |- _ => + apply make_consts_ok, make_pairs_ok in H + | _ => apply Pos.eqb_neq; intro; subst + | _ => inversion_option; congruence + end; + match goal with + | H : In (?n, ?x) consts_list, H': In (?n, ?y) consts_list, + H'' : forall n x y, In (n,x) _ -> In (n,y) _ -> x = y |- _ => + assert (x = y) by (eapply H''; eauto) + end; destruct carry_flag; cbn [Z.b2z] in *; congruence. } + { match goal with |- context [make_ctx ?l ?n] => + let H := fresh in + destruct (make_ctx_cases l n) as [H | H]; + [ rewrite H | apply in_app_or in H; destruct H ] + end; eauto. } Qed. End Proofs. End Fancy. @@ -3416,7 +3521,28 @@ Module Barrett256. interp (invert_expr.smart_App_curried e (x1, (x2, tt))) = interp e x1 x2. Admitted. - Lemma barrett_red256_fancy_correct cc_start_state : + Lemma loosen_rshi_subgoal (ctx : positive -> Z) (n z: positive) cc : + ctx z = 0 -> + ctx n mod 2^256 = ctx n -> + Fancy.spec (Fancy.RSHI 255) (Tuple.map (n:=2) ctx (z, n)) cc mod 2 ^ 256 = + Fancy.spec (Fancy.RSHI 255) (Tuple.map (n:=2) ctx (z, n)) cc mod (1+1). + Proof. + intros Hz Hn. cbn [Tuple.map Tuple.map' fst snd]. rewrite Hz, <-Hn. + replace (1+1) with 2 by omega. assert (2 < 2^256) by (cbn; omega). + cbn [Fancy.spec Fancy.RSHI]. autorewrite with zsimplify_fast. + rewrite Z.shiftr_div_pow2 by omega. + match goal with |- context [(?x / ?d) mod _] => + assert (0 <= x / d < 2); + [ | rewrite !(Z.mod_small (x / d)) by omega; reflexivity ] + end. + split; [ solve [Z.zero_bounds] | ]. + apply Z.div_lt_upper_bound; [ cbn; omega | ]. + eapply Z.lt_le_trans; [ apply Z.mod_pos_bound; cbn; omega | ]. + cbn; omega. + Qed. + + (* TODO: don't rely on the C, M, and L flags *) + Lemma barrett_red256_fancy_correct : forall xLow xHigh error, 0 <= xLow < 2 ^ machine_wordsize -> 0 <= xHigh < M -> @@ -3427,7 +3553,15 @@ Module Barrett256. let RegxLow := 5%positive in let consts_list := [(RegMuLow, muLow); (RegMod, M); (RegZero, 0)] in let arg_list := [(RegxHigh, xHigh); (RegxLow, xLow)] in - Fancy.interp Pos.eqb Fancy.wordmax Fancy.cc_spec (barrett_red256_fancy RegxLow RegxHigh RegMuLow RegMod RegZero error) cc_start_state (Fancy.make_ctx (consts_list ++ arg_list)) = (xLow + 2 ^ machine_wordsize * xHigh) mod M. + let ctx := Fancy.make_ctx (consts_list ++ arg_list) in + let carry_flag := false in (* TODO: don't rely on this value, given it's unused *) + let last_wrote := (fun x : Fancy.CC.code => + match x with + | Fancy.CC.C => RegZero + | _ => RegxHigh (* xHigh needs to have written M; others unused *) + end) in + let cc := Fancy.make_cc last_wrote ctx carry_flag in + Fancy.interp Pos.eqb Fancy.wordmax Fancy.cc_spec (barrett_red256_fancy RegxLow RegxHigh RegMuLow RegMod RegZero error) cc ctx = (xLow + 2 ^ machine_wordsize * xHigh) mod M. Proof. intros. rewrite barrett_red256_fancy_eq. @@ -3435,14 +3569,21 @@ Module Barrett256. rewrite <-barrett_red256_correct_full by auto. eapply Fancy.of_Expr_correct with (x2 := (xLow, (xHigh, tt))). { cbn; intros; subst RegZero RegMod RegMuLow RegxHigh RegxLow. - intuition; Prod.inversion_prod; subst; cbv; congruence. } + intuition; Prod.inversion_prod; subst; cbv. break_innermost_match; congruence. } { cbn; intros; subst RegZero RegMod RegMuLow RegxHigh RegxLow. - intuition; Prod.inversion_prod; subst; congruence. } + intuition; Prod.inversion_prod; subst; cbv; congruence. } + { cbn; intros; subst RegZero RegMod RegMuLow RegxHigh RegxLow. tauto. } { cbn; intros; subst RegZero RegMod RegMuLow RegxHigh RegxLow. intuition; Prod.inversion_prod; subst; cbv; congruence. } { cbn; intros; subst RegZero RegMod RegMuLow RegxHigh RegxLow. match goal with |- context [_ mod ?m] => change m with (2 ^ machine_wordsize) end. assert (M < 2 ^ machine_wordsize) by (cbv; congruence). + assert (0 <= muLow < 2 ^ machine_wordsize) by (split; cbv; congruence). + intuition; Prod.inversion_prod; subst; apply Z.mod_small; omega. } + { cbn; intros; subst RegZero RegMod RegMuLow RegxHigh RegxLow. + match goal with |- context [_ mod ?m] => change m with (2 ^ machine_wordsize) end. + assert (M < 2 ^ machine_wordsize) by (cbv; congruence). + assert (0 <= muLow < 2 ^ machine_wordsize) by (split; cbv; congruence). intuition; Prod.inversion_prod; subst; apply Z.mod_small; omega. } { cbn. repeat match goal with @@ -3450,7 +3591,67 @@ Module Barrett256. | _ => progress step | _ => econstructor end. } - { admit. (* valid_expr *) } + { cbn. cbv [muLow M]. + About Fancy.of_prefancy_scalar. + Ltac sub := + repeat match goal with + | _ => progress intros + | |- context [Fancy.valid_ident] => econstructor + | |- context[Fancy.valid_scalar] => econstructor + | |- context [Fancy.valid_carry] => econstructor + | _ => reflexivity + | |- _ <> None => cbn; congruence + | |- Fancy.of_prefancy_scalar _ _ _ _ = _ => cbn; solve [eauto] + end. + + econstructor; [ solve [sub] | intros ]. + econstructor; [ solve [sub] | intros ]. + eapply Fancy.valid_LetInZ_loosen; try solve [sub]; + [ cbn; omega | | intros; apply loosen_rshi_subgoal; solve [eauto] ]. + econstructor; [ solve [sub] | intros ]. + econstructor; [ solve [sub] | intros ]. + econstructor; [ solve [sub] | intros ]. + econstructor; [ solve [sub] | intros ]. + econstructor; [ solve [sub] | intros ]. + econstructor; [ solve [sub] | intros ]. + econstructor. + { sub. cbn. admit. + (* TODO : This needs to be ADD, not ADDC 0! Fix in fancy rewrite rules! *) } + intros. + econstructor; [ solve [sub] | intros ]. + econstructor. + { sub. cbn. admit. + (* TODO : This needs to be ADD, not ADDC 0! Fix in fancy rewrite rules! *) } + intros. + econstructor. + { sub. admit. + (* TODO: this is the too-tight RSHI cast *) } + econstructor. + { sub. cbn. admit. + (* TODO : This needs to be ADD, not ADDC 0! Fix in fancy rewrite rules! *) } + intros. + econstructor; [ solve [sub] | intros ]. + econstructor; [ solve [sub] | intros ]. + econstructor; [ solve [sub] | intros ]. + econstructor; [ solve [sub] | intros ]. + econstructor; [ solve [sub] | intros ]. + econstructor; [ solve [sub] | intros ]. + econstructor. + { sub. cbn. admit. + (* TODO : This needs to be ADD, not ADDC 0! Fix in fancy rewrite rules! *) } + intros. + econstructor; [ solve [sub] | intros ]. + econstructor. + { sub. cbn. admit. + (* TODO : This needs to be ADD, not ADDC 0! Fix in fancy rewrite rules! *) } + intros. + econstructor; [ solve [sub] | intros ]. + econstructor; [ solve [sub] | intros ]. + econstructor; [ solve [sub] | intros ]. + econstructor; [ solve [sub] | intros ]. + econstructor; [ solve [sub] | intros ]. + econstructor; [ solve [sub] | intros ]. + econstructor. sub. } { cbn - [barrett_red256]. cbv [id]. cbv [expr.Interp]. -- cgit v1.2.3