From 866a4edeb17d18213b62ef124bf0f67eaaca10b8 Mon Sep 17 00:00:00 2001 From: jadep Date: Fri, 8 Feb 2019 09:37:47 -0500 Subject: fix Montgomery proof and clean up a little --- src/Fancy/Barrett256.v | 76 +++++++---------------------------------------- src/Fancy/Montgomery256.v | 43 +++++++++++---------------- src/Fancy/Prod.v | 11 +++++++ 3 files changed, 40 insertions(+), 90 deletions(-) (limited to 'src/Fancy') diff --git a/src/Fancy/Barrett256.v b/src/Fancy/Barrett256.v index 5bd2df9e7..e930272fa 100644 --- a/src/Fancy/Barrett256.v +++ b/src/Fancy/Barrett256.v @@ -264,62 +264,45 @@ Module Barrett256. rewrite interp_Mul256x256 with (tmp2 := extra_reg) by (try congruence; push_value_unused). repeat step_rhs. - rewrite mulhh_comm. + rewrite mulhh_comm by simplify_with_register_properties. repeat step_rhs. - rewrite mulll_comm. + rewrite mulll_comm by simplify_with_register_properties. repeat step_rhs. rewrite swap_add_chain by repeat match goal with | |- _ <> _ => congruence - | _ => rewrite reg_eqb_refl - | _ => rewrite reg_eqb_neq by congruence - | H : ?y = _ mod ?m |- 0 <= ?y < ?m => - rewrite H; apply Z.mod_pos_bound; omega + | _ => progress simplify_with_register_properties | |- _ = 2 ^ 256 => reflexivity | |- flags_unused _ _ => cbv [flags_unused]; intros; do 2 step; reflexivity end. - - Local Ltac simplify := - 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; omega - | _ => assumption - end. - repeat step_rhs. assert (0 < 2 ^ 256) by ZeroBounds.Z.zero_bounds. - rewrite add_comm by simplify. + rewrite add_comm by simplify_with_register_properties. step_rhs. - rewrite addc_comm by simplify. + rewrite addc_comm by simplify_with_register_properties. step_rhs. - rewrite add_comm by simplify. + rewrite add_comm by simplify_with_register_properties. step_rhs. - rewrite addc_comm by simplify. + 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. + rewrite mulhh_comm by simplify_with_register_properties. repeat step_rhs. - rewrite mulll_comm by simplify. + rewrite mulll_comm by simplify_with_register_properties. repeat step_rhs. - rewrite swap_add_chain - by + rewrite swap_add_chain; repeat match goal with | |- _ <> _ => congruence - | _ => rewrite reg_eqb_refl - | _ => rewrite reg_eqb_neq by congruence - | H : ?y = _ mod ?m |- 0 <= ?y < ?m => - rewrite H; apply Z.mod_pos_bound; omega + | _ => progress simplify_with_register_properties | |- _ = 2 ^ 256 => reflexivity | |- flags_unused _ _ => cbv [flags_unused]; intros; @@ -427,43 +410,6 @@ Eval cbv beta iota delta [Prod.MulMod Prod.Mul256x256] in Prod.MulMod. Ret x *) -(* Barrett generated code (equivalence with reference admitted) *) -Eval cbv beta iota delta [Barrett256.barrett_red256_alloc] in Barrett256.barrett_red256_alloc. -(* - = fun (xLow xHigh RegMuLow : register) (_ : positive) (_ : register) => - SELM r2 RegMuLow RegZero; - RSHI 255 r3 RegZero xHigh; - RSHI 255 r4 xHigh xLow; - MUL128UU r5 RegMuLow r4; - MUL128UL r6 r4 RegMuLow; - MUL128LU r7 r4 RegMuLow; - MUL128LL r8 RegMuLow r4; - ADD 128 r9 r8 r7; - ADDC (-128) r10 r5 r7; - ADD 128 r5 r9 r6; - ADDC (-128) r11 r10 r6; - ADD 0 r6 r4 r11; - ADDC 0 r12 RegZero r3; - ADD 0 r13 r2 r6; - ADDC 0 r14 RegZero r12; - RSHI 1 r15 r14 r13; - MUL128UU r16 RegMod r15; - MUL128LU r17 r15 RegMod; - MUL128UL r18 r15 RegMod; - MUL128LL r19 RegMod r15; - ADD 128 r20 r19 r18; - ADDC (-128) r21 r16 r18; - ADD 128 r22 r20 r17; - ADDC (-128) r23 r21 r17; - SUB 0 r24 xLow r22; - SUBC 0 r25 xHigh r23; - SELL r26 RegMod RegZero; - SUB 0 r27 r24 r26; - ADDM r28 r27 RegZero RegMod; - Ret r28 - *) -(* Note that the reference code and production code are the same except for a misplaced RSHI instruction; the current proof assumes that this RSHI commutes. *) - (* Uncomment to see proof statement and remaining admitted statements. *) (* Check Barrett256.prod_barrett_red256_correct. diff --git a/src/Fancy/Montgomery256.v b/src/Fancy/Montgomery256.v index 19415ad03..bf18124ed 100644 --- a/src/Fancy/Montgomery256.v +++ b/src/Fancy/Montgomery256.v @@ -180,12 +180,6 @@ Module Montgomery256. reflexivity. Qed. - (* TODO: could this be simplified? *) - 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 Notation interp := (interp reg_eqb wordmax cc_spec). Lemma montred256_alloc_equivalent errorP errorR cc_start_state start_context : forall lo hi y t1 t2 scratch RegPInv extra_reg, @@ -215,28 +209,27 @@ 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. - rewrite mullh_mulhl. - step. step. step. step. - - - rewrite interp_Mul256x256 with (tmp2:=extra_reg) by - (match goal with - | |- _ <> _ => congruence - | _ => push_value_unused - end). - - rewrite mulll_comm. - step. step. step. - rewrite mulhh_comm. - step. step. step. step. step. - rewrite add_comm by (cbn; solve_bounds). - step. - rewrite addc_comm by (cbn; solve_bounds). - step. step. step. step. + 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. + cbn; repeat progress rewrite ?reg_eqb_neq, ?reg_eqb_refl by congruence. reflexivity. diff --git a/src/Fancy/Prod.v b/src/Fancy/Prod.v index a3f72f17d..a46a7a4f0 100644 --- a/src/Fancy/Prod.v +++ b/src/Fancy/Prod.v @@ -375,4 +375,15 @@ 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