From 0235c25dd1d28658a3bb8e5ed5221dfba8296116 Mon Sep 17 00:00:00 2001 From: jadep Date: Fri, 8 Feb 2019 12:22:14 -0500 Subject: cleanup --- src/Fancy/Barrett256.v | 135 ++++++++++++++-------------------------------- src/Fancy/Montgomery256.v | 52 +++++++++--------- src/Fancy/Prod.v | 35 +++++++----- 3 files changed, 89 insertions(+), 133 deletions(-) (limited to 'src/Fancy') diff --git a/src/Fancy/Barrett256.v b/src/Fancy/Barrett256.v index f7151a283..ffe9a4942 100644 --- a/src/Fancy/Barrett256.v +++ b/src/Fancy/Barrett256.v @@ -182,48 +182,6 @@ Module Barrett256. reflexivity. Qed. - Local Ltac solve_bounds := - match goal with - | H : ?a = ?b mod ?c |- 0 <= ?a < ?c => rewrite H; apply Z.mod_pos_bound; omega - | _ => assumption - end. - Local Ltac results_equiv := - match goal with - |- ?lhs = ?rhs => - match lhs with - context [spec ?li ?largs ?lcc] => - match rhs with - context [spec ?ri ?rargs ?rcc] => - replace (spec li largs lcc) with (spec ri rargs rcc) - end - end - end. - Local Ltac simplify_cc := - match goal with - |- context [CC.update ?to_write ?result ?cc_spec ?old_state] => - let e := eval cbv -[spec cc_spec CC.cc_l CC.cc_m CC.cc_z CC.cc_c] in - (CC.update to_write result cc_spec old_state) in - change (CC.update to_write result cc_spec old_state) with e - end. - Ltac remember_single_result := - match goal with |- context [(spec ?i ?args ?cc) mod ?w] => - let x := fresh "x" in - let y := fresh "y" in - let Heqx := fresh "Heqx" in - remember (spec i args cc) as x eqn:Heqx; - remember (x mod w) as y - end. - Local Ltac step := - match goal with - |- interp _ _ _ (Instr ?i ?rd1 ?args1 ?cont1) ?cc1 ?ctx1 = - interp _ _ _ (Instr ?i ?rd2 ?args2 ?cont2) ?cc2 ?ctx2 => - rewrite (interp_step _ _ i rd1 args1 cont1); - rewrite (interp_step _ _ i rd2 args2 cont2) - end; - cbn - [interp spec cc_spec]; - repeat progress rewrite ?reg_eqb_neq, ?reg_eqb_refl by congruence; - results_equiv; [ remember_single_result; repeat simplify_cc | try reflexivity ]. - Local Notation interp := (interp reg_eqb wordmax cc_spec). Lemma barrett_red256_alloc_equivalent errorP errorR cc_start_state start_context : forall x xHigh RegMuLow scratchp1 scratchp2 scratchp3 scratchp4 scratchp5 extra_reg, @@ -256,62 +214,51 @@ Module Barrett256. | H : ~ False |- _ => clear H end. - repeat step_lhs. - - - repeat step_rhs. - rewrite interp_Mul256x256 with (tmp2 := extra_reg) by - (try congruence; push_value_unused). - repeat step_rhs. - rewrite mulhh_comm by simplify_with_register_properties. - repeat step_rhs. - rewrite mulll_comm by simplify_with_register_properties. - repeat step_rhs. + Ltac simplify_with_register_properties ::= + repeat + match goal with + | _ => rewrite reg_eqb_refl + | _ => rewrite reg_eqb_neq by (assumption || congruence) + | H:?y = _ mod ?m |- 0 <= ?y < _ => rewrite H; apply Z.mod_pos_bound; lia + | _ => assumption + end. + Ltac cleanup ::= + cbn-[Spec.interp spec cc_spec]; simplify_with_register_properties; + cbv[CC.update in_dec list_rec list_rect CC.code_dec]; cbn[CC.cc_c CC.cc_m CC.cc_z CC.cc_l]. - rewrite swap_add_chain - by - repeat match goal with - | |- _ <> _ => congruence - | _ => progress simplify_with_register_properties - | |- _ = 2 ^ 256 => reflexivity - | |- flags_unused _ _ => - cbv [flags_unused]; intros; - do 2 step; reflexivity - end. - repeat step_rhs. - assert (0 < 2 ^ 256) by ZeroBounds.Z.zero_bounds. - rewrite add_comm by simplify_with_register_properties. - step_rhs. - rewrite addc_comm by simplify_with_register_properties. - step_rhs. - rewrite add_comm by simplify_with_register_properties. - step_rhs. - rewrite addc_comm by simplify_with_register_properties. - step_rhs. - repeat step_rhs. - rewrite interp_Mul256x256 with (tmp2 := extra_reg) by - (try congruence; push_value_unused). - repeat step_rhs. - rewrite mulhh_comm by simplify_with_register_properties. - repeat step_rhs. - rewrite mulll_comm by simplify_with_register_properties. - repeat step_rhs. - - rewrite swap_add_chain; - repeat match goal with - | |- _ <> _ => congruence - | _ => progress simplify_with_register_properties - | |- _ = 2 ^ 256 => reflexivity - | |- flags_unused _ _ => - cbv [flags_unused]; intros; - repeat (step; try reflexivity) - end. - - repeat step_rhs. + Ltac prove_programs_equivalent := + repeat step_lhs; (* remember the results of each step on the LHS *) + repeat match goal with + | _ => step_rhs + | |- ?x = ?x => reflexivity + | _ => rewrite mulhh_comm by simplify_with_register_properties; step_rhs + | _ => rewrite mulll_comm by simplify_with_register_properties; step_rhs + | _ => rewrite add_comm by simplify_with_register_properties; step_rhs + | _ => rewrite addc_comm by simplify_with_register_properties; step_rhs + | _ => rewrite mullh_mulhl; step_rhs + | _ => rewrite <-mullh_mulhl; step_rhs + end. + Time repeat match goal with + | _ => progress prove_programs_equivalent + | _ => rewrite interp_Mul256x256 with (tmp2 := extra_reg) by + (match goal with + | |- _ <> _ => assumption || congruence + | _ => push_value_unused + end) + | _ => + rewrite swap_add_chain by + repeat match goal with + | |- _ <> _ => assumption || congruence + | _ => progress simplify_with_register_properties + | |- _ = 2 ^ 256 => reflexivity + | |- flags_unused _ _ => + cbv [flags_unused]; intros; prove_programs_equivalent (* TODO: there is probably a faster way to do this one *) + end + end. cbv [Spec.interp]. - rewrite !reg_eqb_refl. + simplify_with_register_properties. reflexivity. Qed. diff --git a/src/Fancy/Montgomery256.v b/src/Fancy/Montgomery256.v index bf18124ed..a4b27c561 100644 --- a/src/Fancy/Montgomery256.v +++ b/src/Fancy/Montgomery256.v @@ -101,6 +101,15 @@ Module Montgomery256. | |- of_prefancy_scalar _ _ _ _ = _ => cbn; solve [eauto] end. + (* TODO(jgross): switch out casts *) + (* might need to use CheckCasts.interp_eqv_without_casts? *) + Lemma swap_casts lo hi : + expr.interp (@ident.gen_interp cast_oor) + (invert_expr.smart_App_curried (montred256 (type.interp base.interp)) (lo, (hi, tt))) = + expr.interp (@ident.interp) + (invert_expr.smart_App_curried (montred256 (type.interp base.interp)) (lo, (hi, tt))). + Admitted. + Lemma montred256_fancy_correct : forall lo hi error, 0 <= lo < R -> @@ -149,11 +158,8 @@ Module Montgomery256. econstructor. valid_expr_subgoal. } { cbn - [montred256]. cbv [id]. f_equal. - (* TODO(jgross): switch out casts *) - (* might need to use CheckCasts.interp_eqv_without_casts? *) - replace (@ident.gen_interp cast_oor) with (@ident.interp) by admit. - reflexivity. } - Admitted. + apply swap_casts. } + Qed. Import Spec.Registers. @@ -209,29 +215,21 @@ Module Montgomery256. | H : ~ False |- _ => clear H end. - (* TODO: the manual steps here can probably be replaced with a - tactic *) - - repeat step_lhs. - rewrite interp_Mul256 with (tmp2:=extra_reg) by (congruence || push_value_unused). - - rewrite mullh_mulhl. - step_rhs. - rewrite <-mullh_mulhl. - repeat step_rhs. - - rewrite interp_Mul256x256 with (tmp2:=extra_reg) by (congruence || push_value_unused). - rewrite mulhh_comm by simplify_with_register_properties. - repeat step_rhs. - rewrite mulll_comm by simplify_with_register_properties. - repeat step_rhs. - rewrite add_comm by simplify_with_register_properties. - step_rhs. - rewrite addc_comm by simplify_with_register_properties. - repeat step_rhs. - + Time repeat match goal with + | _ => progress prove_programs_equivalent + | _ => rewrite interp_Mul256 with (tmp2 := extra_reg) by + (match goal with + | |- _ <> _ => assumption || congruence + | _ => push_value_unused + end) + | _ => rewrite interp_Mul256x256 with (tmp2 := extra_reg) by + (match goal with + | |- _ <> _ => assumption || congruence + | _ => push_value_unused + end) + end. - cbn; repeat progress rewrite ?reg_eqb_neq, ?reg_eqb_refl by congruence. + cbn [Spec.interp]; simplify_with_register_properties. reflexivity. Qed. diff --git a/src/Fancy/Prod.v b/src/Fancy/Prod.v index a46a7a4f0..de5680727 100644 --- a/src/Fancy/Prod.v +++ b/src/Fancy/Prod.v @@ -85,9 +85,19 @@ Section Prod. (Ret x))))))))))))))). End Prod. +(* Solves subgoals for commutativity proofs and simplifies register +lookup expressions *) +Ltac simplify_with_register_properties := + repeat + match goal with + | _ => rewrite reg_eqb_refl + | _ => rewrite reg_eqb_neq by (assumption || congruence) + | H:?y = _ mod ?m |- 0 <= ?y < _ => rewrite H; apply Z.mod_pos_bound; lia + | _ => assumption + end. Ltac cleanup := cbn - [interp spec cc_spec]; - rewrite ?reg_eqb_refl, ?reg_eqb_neq by congruence; + simplify_with_register_properties; cbv [CC.update in_dec list_rec list_rect CC.code_dec]; cbn [CC.cc_c CC.cc_m CC.cc_z CC.cc_l]. @@ -110,6 +120,18 @@ Ltac step_rhs := | H : ?y = (?x mod ?m)%Z |- context [(?x mod ?m)%Z] => rewrite <-H end. +Ltac prove_programs_equivalent := + repeat step_lhs; (* remember the results of each step on the LHS *) + repeat match goal with + | _ => step_rhs + | |- ?x = ?x => reflexivity + | _ => rewrite mulhh_comm by simplify_with_register_properties; step_rhs + | _ => rewrite mulll_comm by simplify_with_register_properties; step_rhs + | _ => rewrite add_comm by simplify_with_register_properties; step_rhs + | _ => rewrite addc_comm by simplify_with_register_properties; step_rhs + | _ => rewrite mullh_mulhl; step_rhs + | _ => rewrite <-mullh_mulhl; step_rhs + end. Section ProdEquiv. Context (wordmax : Z). @@ -375,15 +397,4 @@ Ltac push_value_unused := | _ => apply not_in_cons; split; [ try assumption; symmetry; assumption | ] | _ => apply in_nil - end. - -(* Solves subgoals for commutativity proofs and simplifies register -lookup expressions *) -Ltac simplify_with_register_properties := - repeat match goal with - | _ => rewrite reg_eqb_refl - | _ => rewrite reg_eqb_neq by congruence - | H : ?y = _ mod ?m |- 0 <= ?y < _ => - rewrite H; apply Z.mod_pos_bound; lia - | _ => assumption end. \ No newline at end of file -- cgit v1.2.3