diff options
Diffstat (limited to 'src')
-rw-r--r-- | src/Specific/Ed25519.v | 73 |
1 files changed, 32 insertions, 41 deletions
diff --git a/src/Specific/Ed25519.v b/src/Specific/Ed25519.v index 12f31beeb..d9cfa6f05 100644 --- a/src/Specific/Ed25519.v +++ b/src/Specific/Ed25519.v @@ -225,13 +225,6 @@ Section Ed25519Frep. destruct b; trivial. Qed. - Create HintDb FRepOperations discriminated. - Hint Rewrite FRepMul_correct FRepAdd_correct FRepSub_correct FRepInv_correct FSRepPow_correct FRepOpp_correct : FRepOperations. - - Create HintDb EdDSA_opts discriminated. - Hint Rewrite FRepMul_correct FRepAdd_correct FRepSub_correct FRepInv_correct FSRepPow_correct FRepOpp_correct : EdDSA_opts. - - Local Ltac Let_In_unRep := match goal with | [ |- appcontext G[Let_In (unRep ?x) ?f] ] @@ -246,6 +239,22 @@ Section Ed25519Frep. reflexivity. Qed. + Lemma Let_app_In {A B T} (g:A->B) (f:B->T) (x:A) : + @Let_In _ (fun _ => T) (g x) f = + @Let_In _ (fun _ => T) x (fun p => f (g x)). + Proof. reflexivity. Qed. + + Lemma Let_app2_In {A B C D T} (g1:A->C) (g2:B->D) (f:C*D->T) (x:A) (y:B) : + @Let_In _ (fun _ => T) (g1 x, g2 y) f = + @Let_In _ (fun _ => T) (x, y) (fun p => f ((g1 (fst p), g2 (snd p)))). + Proof. reflexivity. Qed. + + Create HintDb FRepOperations discriminated. + Hint Rewrite FRepMul_correct FRepAdd_correct FRepSub_correct FRepInv_correct FSRepPow_correct FRepOpp_correct : FRepOperations. + + Create HintDb EdDSA_opts discriminated. + Hint Rewrite FRepMul_correct FRepAdd_correct FRepSub_correct FRepInv_correct FSRepPow_correct FRepOpp_correct : EdDSA_opts. + Lemma unifiedAddM1Rep_sig : forall a b : FRep * FRep * FRep * FRep, { unifiedAddM1Rep | rep2E unifiedAddM1Rep = unifiedAddM1' (rep2E a) (rep2E b) }. Proof. destruct a as [[[]]]; destruct b as [[[]]]. @@ -343,8 +352,8 @@ Section Ed25519Frep. = rep2E (((FRepOpp x, y), toRep z), FRepOpp t). Proof. rewrite <- commute_negateExtended'_rep2E; simpl; rewrite !rcFOK; reflexivity. Qed. - Hint Rewrite @F_mul_0_l commute_negateExtended'_rep2E_rrfr fold_rep2E_0fff (@fold_rep2E_ff1f (fst (proj1_sig B))) : EdDSA_opts. - Hint Rewrite <- unifiedAddM1Rep_correct erep2trep_correct (fun x y z bound => iter_op_proj rep2E unifiedAddM1Rep unifiedAddM1' x y z N.testbit_nat bound unifiedAddM1Rep_correct) : EdDSA_opts. + Hint Rewrite @F_mul_0_l commute_negateExtended'_rep2E_rrfr fold_rep2E_0fff (@fold_rep2E_ff1f (fst (proj1_sig B))) @if_F_eq_dec_if_F_eqb compare_enc (if_map unRep) (fun T => Let_app2_In (T := T) unRep unRep) @F_pow_2_r @unfoldDiv : EdDSA_opts. + Hint Rewrite <- unifiedAddM1Rep_correct erep2trep_correct (fun x y z bound => iter_op_proj rep2E unifiedAddM1Rep unifiedAddM1' x y z N.testbit_nat bound unifiedAddM1Rep_correct) FRep2wire_correct: EdDSA_opts. Lemma sharper_verify : forall pk l msg sig, { verify | verify = ed25519_verify pk l msg sig}. Proof. @@ -513,17 +522,13 @@ Section Ed25519Frep. eapply option_rect_Proper_nd; [|reflexivity..]. cbv beta delta [pointwise_relation]. intro. rewrite <-!(option_rect_option_map rep2F). eapply option_rect_Proper_nd; [|reflexivity..]. cbv beta delta [pointwise_relation]. intro. - rewrite !F_pow_2_r. + autorewrite with EdDSA_opts. rewrite <-(rcFOK 1%F). pattern Ed25519.d at 1. rewrite <-(rcFOK Ed25519.d) at 1. pattern Ed25519.a at 1. rewrite <-(rcFOK Ed25519.a) at 1. - rewrite !FRepMul_correct. - rewrite !FRepSub_correct. - rewrite !unfoldDiv. - rewrite !FRepInv_correct. - rewrite !FRepMul_correct. - (Let_In_unRep). rewrite <- (rcSOK (Z.to_N (Ed25519.q / 8 + 1))). + autorewrite with EdDSA_opts. + (Let_In_unRep). eapply Let_In_Proper_nd; [reflexivity|cbv beta delta [pointwise_relation]; intro]. etransitivity. Focus 2. eapply Let_In_Proper_nd; [|cbv beta delta [pointwise_relation]; intro;reflexivity]. { (* TODO: @@ -533,44 +538,30 @@ Section Ed25519Frep. (Let_In_unRep). etransitivity. Focus 2. eapply Let_In_Proper_nd; [reflexivity|cbv beta delta [pointwise_relation]; intro]. { set_evars. - rewrite !F_pow_2_r. - rewrite !FRepMul_correct. - rewrite if_F_eq_dec_if_F_eqb. - rewrite compare_enc. - rewrite <-!FRep2wire_correct. rewrite <-(rcFOK sqrt_minus1). - rewrite !FRepMul_correct. - rewrite (if_map rep2F). + autorewrite with EdDSA_opts. subst_evars. reflexivity. } Unfocus. - match goal with |- ?e = Let_In ?xval (fun x => rep2F (@?f x)) => change (e = rep2F (Let_In xval f)) end. + rewrite pull_Let_In. reflexivity. } Unfocus. - (Let_In_unRep). - eapply Let_In_Proper_nd; [reflexivity|cbv beta delta [pointwise_relation]; intro]. set_evars. - rewrite !F_pow_2_r. - rewrite !FRepMul_correct. - rewrite if_F_eq_dec_if_F_eqb. - rewrite compare_enc. - rewrite <-!FRep2wire_correct. - subst_evars. - lazymatch goal with |- _ = if ?b then ?t else ?f => apply (f_equal2 (fun x y => if b then x else y)) end; [|reflexivity]. + (Let_In_unRep). + + subst_evars. eapply Let_In_Proper_nd; [reflexivity|cbv beta delta [pointwise_relation]; intro]. set_evars. + + autorewrite with EdDSA_opts. - set_evars. - rewrite !FRepOpp_correct. - rewrite (if_map rep2F). - lazymatch goal with - |- ?e = Let_In (rep2F ?x, rep2F ?y) (fun p => @?r p) => - change (e = Let_In (x, y) (fun p => r (rep2F (fst p), rep2F (snd p)))); cbv beta zeta - end. subst_evars. + lazymatch goal with |- _ = if ?b then ?t else ?f => apply (f_equal2 (fun x y => if b then x else y)) end; [|reflexivity]. eapply Let_In_Proper_nd; [reflexivity|cbv beta delta [pointwise_relation]; intro]. + set_evars. unfold twistedToExtended. autorewrite with EdDSA_opts. progress cbv beta delta [erep2trep]. + subst_evars. reflexivity. } Unfocus. reflexivity. Defined. -End Ed25519Frep. +End Ed25519Frep.
\ No newline at end of file |