diff options
author | Andres Erbsen <andreser@mit.edu> | 2016-10-12 23:52:25 -0400 |
---|---|---|
committer | Andres Erbsen <andreser@mit.edu> | 2016-10-12 23:52:25 -0400 |
commit | 92c3123f4e3421de86d655cd39945a1fc6147c8f (patch) | |
tree | 21167fcb7c31079d456ee3696236f2228d84a7cd | |
parent | c4fd919c6598517105ec39ce1c0d487553a99420 (diff) |
refactor scalar multiplication thoery, implement SRepERepMul
-rw-r--r-- | src/Algebra.v | 244 | ||||
-rw-r--r-- | src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v | 6 | ||||
-rw-r--r-- | src/CompleteEdwardsCurve/ExtendedCoordinates.v | 10 | ||||
-rw-r--r-- | src/EdDSARepChange.v | 2 | ||||
-rw-r--r-- | src/Encoding/PointEncoding.v | 2 | ||||
-rw-r--r-- | src/Experiments/Ed25519.v | 31 | ||||
-rw-r--r-- | src/Util/IterAssocOp.v | 30 |
7 files changed, 188 insertions, 137 deletions
diff --git a/src/Algebra.v b/src/Algebra.v index 9db169816..c0d7dfbe2 100644 --- a/src/Algebra.v +++ b/src/Algebra.v @@ -148,6 +148,14 @@ Section Algebra. End AddMul. End Algebra. +Section ZeroNeqOne. + Context {T eq zero one} `{@is_zero_neq_one T eq zero one} `{Equivalence T eq}. + + Lemma one_neq_zero : not (eq one zero). + Proof. + intro HH; symmetry in HH. auto using zero_neq_one. + Qed. +End ZeroNeqOne. Module Monoid. Section Monoid. @@ -192,16 +200,106 @@ Module Monoid. Qed. End Monoid. + + Section Homomorphism. + Context {T EQ OP ID} {monoidT: @monoid T EQ OP ID }. + Context {T' eq op id} {monoidT': @monoid T' eq op id }. + Context {phi:T->T'}. + Local Infix "=" := eq. Local Infix "=" := eq : type_scope. + Class is_homomorphism := + { + homomorphism : forall a b, phi (OP a b) = op (phi a) (phi b); + + is_homomorphism_phi_proper : Proper (respectful EQ eq) phi + }. + Global Existing Instance is_homomorphism_phi_proper. + End Homomorphism. End Monoid. -Section ZeroNeqOne. - Context {T eq zero one} `{@is_zero_neq_one T eq zero one} `{Equivalence T eq}. +Module ScalarMult. + Section ScalarMultProperties. + Context {G eq add zero} `{monoidG:@monoid G eq add zero}. + Context {mul:nat->G->G}. + Local Infix "=" := eq : type_scope. Local Infix "=" := eq. + Local Infix "+" := add. Local Infix "*" := mul. + Class is_scalarmult := + { + scalarmult_0_l : forall P, 0 * P = zero; + scalarmult_S_l : forall n P, S n * P = P + n * P; - Lemma one_neq_zero : not (eq one zero). - Proof. - intro HH; symmetry in HH. auto using zero_neq_one. - Qed. -End ZeroNeqOne. + scalarmult_Proper : Proper (Logic.eq==>eq==>eq) mul + }. + Global Existing Instance scalarmult_Proper. + Context `{mul_is_scalarmult:is_scalarmult}. + + Fixpoint scalarmult_ref (n:nat) (P:G) {struct n} := + match n with + | O => zero + | S n' => add P (scalarmult_ref n' P) + end. + + Global Instance Proper_scalarmult_ref : Proper (Logic.eq==>eq==>eq) scalarmult_ref. + Proof. + repeat intro; subst. + match goal with [n:nat |- _ ] => induction n; simpl @scalarmult_ref; [reflexivity|] end. + repeat match goal with [H:_ |- _ ] => rewrite H end; reflexivity. + Qed. + + Lemma scalarmult_ext : forall n P, mul n P = scalarmult_ref n P. + induction n; simpl @scalarmult_ref; intros; rewrite <-?IHn; (apply scalarmult_0_l || apply scalarmult_S_l). + Qed. + + Lemma scalarmult_1_l : forall P, 1*P = P. + Proof. intros. rewrite scalarmult_S_l, scalarmult_0_l, right_identity; reflexivity. Qed. + + Lemma scalarmult_add_l : forall (n m:nat) (P:G), ((n + m)%nat * P = n * P + m * P). + Proof. + induction n; intros; + rewrite ?scalarmult_0_l, ?scalarmult_S_l, ?plus_Sn_m, ?plus_O_n, ?scalarmult_S_l, ?left_identity, <-?associative, <-?IHn; reflexivity. + Qed. + + Lemma scalarmult_zero_r : forall m, m * zero = zero. + Proof. induction m; rewrite ?scalarmult_S_l, ?scalarmult_0_l, ?left_identity, ?IHm; try reflexivity. Qed. + + Lemma scalarmult_assoc : forall (n m : nat) P, n * (m * P) = (m * n)%nat * P. + Proof. + induction n; intros. + { rewrite <-mult_n_O, !scalarmult_0_l. reflexivity. } + { rewrite scalarmult_S_l, <-mult_n_Sm, <-Plus.plus_comm, scalarmult_add_l. + rewrite IHn. reflexivity. } + Qed. + + Lemma scalarmult_times_order : forall l B, l*B = zero -> forall n, (l * n) * B = zero. + Proof. intros ? ? Hl ?. rewrite <-scalarmult_assoc, Hl, scalarmult_zero_r. reflexivity. Qed. + + Lemma scalarmult_mod_order : forall l B, l <> 0%nat -> l*B = zero -> forall n, n mod l * B = n * B. + Proof. + intros ? ? Hnz Hmod ?. + rewrite (NPeano.Nat.div_mod n l Hnz) at 2. + rewrite scalarmult_add_l, scalarmult_times_order, left_identity by auto. reflexivity. + Qed. + End ScalarMultProperties. + + Section ScalarMultHomomorphism. + Context {G EQ ADD ZERO} {monoidG:@monoid G EQ ADD ZERO}. + Context {H eq add zero} {monoidH:@monoid H eq add zero}. + Local Infix "=" := eq : type_scope. Local Infix "=" := eq : eq_scope. + Context {MUL} {MUL_is_scalarmult:@is_scalarmult G EQ ADD ZERO MUL }. + Context {mul} {mul_is_scalarmult:@is_scalarmult H eq add zero mul }. + Context {phi} {homom:@Monoid.is_homomorphism G EQ ADD H eq add phi}. + Context (phi_ZERO:phi ZERO = zero). + + Lemma homomorphism_scalarmult : forall n P, phi (MUL n P) = mul n (phi P). + Proof. + setoid_rewrite scalarmult_ext. + induction n; intros; simpl; rewrite ?Monoid.homomorphism, ?IHn; easy. + Qed. + End ScalarMultHomomorphism. + + Global Instance scalarmult_ref_is_scalarmult {G eq add zero} `{@monoid G eq add zero} + : @is_scalarmult G eq add zero (@scalarmult_ref G add zero). + Proof. split; try exact _; intros; reflexivity. Qed. +End ScalarMult. Module Group. Section BasicProperties. @@ -279,30 +377,37 @@ Module Group. Section Homomorphism. Context {G EQ OP ID INV} {groupG:@group G EQ OP ID INV}. Context {H eq op id inv} {groupH:@group H eq op id inv}. - Context {phi:G->H}. + Context {phi:G->H}`{homom:@Monoid.is_homomorphism G EQ OP H eq op phi}. Local Infix "=" := eq. Local Infix "=" := eq : type_scope. - Class is_homomorphism := - { - homomorphism : forall a b, phi (OP a b) = op (phi a) (phi b); - - is_homomorphism_phi_proper : Proper (respectful EQ eq) phi - }. - Global Existing Instance is_homomorphism_phi_proper. - Context `{is_homomorphism}. - Lemma homomorphism_id : phi ID = id. Proof. assert (Hii: op (phi ID) (phi ID) = op (phi ID) id) by - (rewrite <- homomorphism, left_identity, right_identity; reflexivity). + (rewrite <- Monoid.homomorphism, left_identity, right_identity; reflexivity). rewrite cancel_left in Hii; exact Hii. Qed. Lemma homomorphism_inv x : phi (INV x) = inv (phi x). Proof. apply inv_unique. - rewrite <- homomorphism, left_inverse, homomorphism_id; reflexivity. + rewrite <- Monoid.homomorphism, left_inverse, homomorphism_id; reflexivity. Qed. + + Section ScalarMultHomomorphism. + Context {MUL} {MUL_is_scalarmult:@ScalarMult.is_scalarmult G EQ OP ID MUL }. + Context {mul} {mul_is_scalarmult:@ScalarMult.is_scalarmult H eq op id mul }. + Lemma homomorphism_scalarmult n P : phi (MUL n P) = mul n (phi P). + Proof. eapply ScalarMult.homomorphism_scalarmult, homomorphism_id. Qed. + + Import ScalarMult. + Lemma opp_mul : forall n P, inv (mul n P) = mul n (inv P). + Proof. + induction n; intros. + { rewrite !scalarmult_0_l, Group.inv_id; reflexivity. } + { rewrite <-NPeano.Nat.add_1_l, Plus.plus_comm at 1. + rewrite scalarmult_add_l, scalarmult_1_l, Group.inv_op, scalarmult_S_l, Group.cancel_left; eauto. } + Qed. + End ScalarMultHomomorphism. End Homomorphism. Section Homomorphism_rev. @@ -340,7 +445,7 @@ Module Group. Qed. Definition homomorphism_from_redundant_representation - : @is_homomorphism G EQ OP H eq op phi. + : @Monoid.is_homomorphism G EQ OP H eq op phi. Proof. split; repeat intro; apply phi'_eq; rewrite ?phi'_op, ?phi'_phi_id; easy. Qed. @@ -358,7 +463,7 @@ Module Group. {phi_op : forall a b, eq (phi (OP a b)) (op (phi a) (phi b))} {phi_inv : forall a, eq (phi (INV a)) (inv (phi a))} {phi_id : eq (phi ID) id} - : @group H eq op id inv. + : @group H eq op id inv. Proof. repeat split; eauto with core typeclass_instances; intros; repeat match goal with @@ -370,7 +475,7 @@ Module Group. end end; repeat rewrite <-?phi_op, <-?phi_inv, <-?phi_id; - f_equiv; auto using associative, left_identity, right_identity, left_inverse, right_inverse. + f_equiv; auto using associative, left_identity, right_identity, left_inverse, right_inverse. Qed. Lemma isomorphism_to_subgroup_group @@ -384,7 +489,7 @@ Module Group. {phi_op : forall a b, eq (phi (OP a b)) (op (phi a) (phi b))} {phi_inv : forall a, eq (phi (INV a)) (inv (phi a))} {phi_id : eq (phi ID) id} - : @group G EQ OP ID INV. + : @group G EQ OP ID INV. Proof. repeat split; eauto with core typeclass_instances; intros; eapply eq_phi_EQ; @@ -398,101 +503,24 @@ Module Group. Context {H eq op id inv} {groupH:@group H eq op id inv}. Context {K eqK opK idK invK} {groupK:@group K eqK opK idK invK}. Context {phi:G->H} {phi':H->K} - {Hphi:@is_homomorphism G EQ OP H eq op phi} - {Hphi':@is_homomorphism H eq op K eqK opK phi'}. + {Hphi:@Monoid.is_homomorphism G EQ OP H eq op phi} + {Hphi':@Monoid.is_homomorphism H eq op K eqK opK phi'}. Lemma is_homomorphism_compose {phi'':G->K} (Hphi'' : forall x, eqK (phi' (phi x)) (phi'' x)) - : @is_homomorphism G EQ OP K eqK opK phi''. + : @Monoid.is_homomorphism G EQ OP K eqK opK phi''. Proof. split; repeat intro; rewrite <- !Hphi''. - { rewrite !homomorphism; reflexivity. } + { rewrite !Monoid.homomorphism; reflexivity. } { apply Hphi', Hphi; assumption. } Qed. Global Instance is_homomorphism_compose_refl - : @is_homomorphism G EQ OP K eqK opK (fun x => phi' (phi x)) + : @Monoid.is_homomorphism G EQ OP K eqK opK (fun x => phi' (phi x)) := is_homomorphism_compose (fun x => reflexivity _). End HomomorphismComposition. End Group. -Module ScalarMult. - Section ScalarMultProperties. - Context {G eq add zero} `{@monoid G eq add zero}. - Context {mul:nat->G->G}. - Local Infix "=" := eq : type_scope. Local Infix "=" := eq. - Local Infix "+" := add. Local Infix "*" := mul. - Class is_scalarmult := - { - scalarmult_0_l : forall P, 0 * P = zero; - scalarmult_S_l : forall n P, S n * P = P + n * P; - - scalarmult_Proper : Proper (Logic.eq==>eq==>eq) mul - }. - Global Existing Instance scalarmult_Proper. - Context `{is_scalarmult}. - - Fixpoint scalarmult_ref (n:nat) (P:G) {struct n} := - match n with - | O => zero - | S n' => add P (scalarmult_ref n' P) - end. - - Global Instance Proper_scalarmult_ref : Proper (Logic.eq==>eq==>eq) scalarmult_ref. - Proof. - repeat intro; subst. - match goal with [n:nat |- _ ] => induction n; simpl @scalarmult_ref; [reflexivity|] end. - repeat match goal with [H:_ |- _ ] => rewrite H end; reflexivity. - Qed. - - Lemma scalarmult_ext : forall n P, mul n P = scalarmult_ref n P. - induction n; simpl @scalarmult_ref; intros; rewrite <-?IHn; (apply scalarmult_0_l || apply scalarmult_S_l). - Qed. - - Lemma scalarmult_1_l : forall P, 1*P = P. - Proof. intros. rewrite scalarmult_S_l, scalarmult_0_l, right_identity; reflexivity. Qed. - - Lemma scalarmult_add_l : forall (n m:nat) (P:G), ((n + m)%nat * P = n * P + m * P). - Proof. - induction n; intros; - rewrite ?scalarmult_0_l, ?scalarmult_S_l, ?plus_Sn_m, ?plus_O_n, ?scalarmult_S_l, ?left_identity, <-?associative, <-?IHn; reflexivity. - Qed. - - Lemma scalarmult_zero_r : forall m, m * zero = zero. - Proof. induction m; rewrite ?scalarmult_S_l, ?scalarmult_0_l, ?left_identity, ?IHm; try reflexivity. Qed. - - Lemma scalarmult_assoc : forall (n m : nat) P, n * (m * P) = (m * n)%nat * P. - Proof. - induction n; intros. - { rewrite <-mult_n_O, !scalarmult_0_l. reflexivity. } - { rewrite scalarmult_S_l, <-mult_n_Sm, <-Plus.plus_comm, scalarmult_add_l. - rewrite IHn. reflexivity. } - Qed. - - Lemma scalarmult_times_order : forall l B, l*B = zero -> forall n, (l * n) * B = zero. - Proof. intros ? ? Hl ?. rewrite <-scalarmult_assoc, Hl, scalarmult_zero_r. reflexivity. Qed. - - Lemma scalarmult_mod_order : forall l B, l <> 0%nat -> l*B = zero -> forall n, n mod l * B = n * B. - Proof. - intros ? ? Hnz Hmod ?. - rewrite (NPeano.Nat.div_mod n l Hnz) at 2. - rewrite scalarmult_add_l, scalarmult_times_order, left_identity by auto. reflexivity. - Qed. - Context {opp} {group:@group G eq add zero opp}. - - Lemma opp_mul : forall n P, opp (n * P) = n * (opp P). - induction n; intros. - { rewrite !scalarmult_0_l, Group.inv_id; reflexivity. } - { rewrite <-NPeano.Nat.add_1_l, Plus.plus_comm at 1. - rewrite scalarmult_add_l, scalarmult_1_l, Group.inv_op, scalarmult_S_l, Group.cancel_left; eauto. } - Qed. - End ScalarMultProperties. - - Global Instance scalarmult_ref_is_scalarmult {G eq add zero} `{@monoid G eq add zero} - : @is_scalarmult G eq add zero (@scalarmult_ref G add zero). - Proof. split; try exact _; intros; reflexivity. Qed. -End ScalarMult. - Require Coq.nsatz.Nsatz. Ltac dropAlgebraSyntax := @@ -606,7 +634,7 @@ Module Ring. Class is_homomorphism := { - homomorphism_is_homomorphism : Group.is_homomorphism (phi:=phi) (OP:=ADD) (op:=add) (EQ:=EQ) (eq:=eq); + homomorphism_is_homomorphism : Monoid.is_homomorphism (phi:=phi) (OP:=ADD) (op:=add) (EQ:=EQ) (eq:=eq); homomorphism_mul : forall x y, phi (MUL x y) = mul (phi x) (phi y); homomorphism_one : phi ONE = one }. @@ -615,7 +643,7 @@ Module Ring. Context `{is_homomorphism}. Lemma homomorphism_add : forall x y, phi (ADD x y) = add (phi x) (phi y). - Proof. apply Group.homomorphism. Qed. + Proof. apply Monoid.homomorphism. Qed. Definition homomorphism_opp : forall x, phi (OPP x) = opp (phi x) := (Group.homomorphism_inv (INV:=OPP) (inv:=opp)). @@ -623,7 +651,7 @@ Module Ring. Lemma homomorphism_sub : forall x y, phi (SUB x y) = sub (phi x) (phi y). Proof. intros. - rewrite !ring_sub_definition, Group.homomorphism, homomorphism_opp. reflexivity. + rewrite !ring_sub_definition, Monoid.homomorphism, homomorphism_opp. reflexivity. Qed. End Homomorphism. diff --git a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v index be0a80d1f..e90aad0d8 100644 --- a/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v +++ b/src/CompleteEdwardsCurve/CompleteEdwardsCurveTheorems.v @@ -160,17 +160,17 @@ Module E. Next Obligation. destruct P as [ [? ?] ?]; simpl. rewrite_strat bottomup hints field_homomorphism. - eauto using is_homomorphism_phi_proper; assumption. + eauto using Monoid.is_homomorphism_phi_proper; assumption. Qed. Context {point_phi:Fpoint->Kpoint} {point_phi_Proper:Proper (eq==>eq) point_phi} {point_phi_correct: forall (P:point), eq (point_phi P) (ref_phi P)}. - Lemma lift_homomorphism : @Group.is_homomorphism Fpoint eq add Kpoint eq add point_phi. + Lemma lift_homomorphism : @Monoid.is_homomorphism Fpoint eq add Kpoint eq add point_phi. Proof. repeat match goal with - | |- Group.is_homomorphism => split + | |- Monoid.is_homomorphism => split | |- _ => intro | |- _ /\ _ => split | [H: _ /\ _ |- _ ] => destruct H diff --git a/src/CompleteEdwardsCurve/ExtendedCoordinates.v b/src/CompleteEdwardsCurve/ExtendedCoordinates.v index 189c4d08b..ab52445ca 100644 --- a/src/CompleteEdwardsCurve/ExtendedCoordinates.v +++ b/src/CompleteEdwardsCurve/ExtendedCoordinates.v @@ -135,7 +135,7 @@ Module Extended. transitivity (to_twisted x + to_twisted x0)%E; rewrite to_twisted_add, ?H, ?H0; reflexivity. Qed. - Lemma homomorphism_to_twisted : @Group.is_homomorphism point eq add Epoint E.eq E.add to_twisted. + Lemma homomorphism_to_twisted : @Monoid.is_homomorphism point eq add Epoint E.eq E.add to_twisted. Proof. split; trivial using Proper_to_twisted, to_twisted_add. Qed. Lemma add_from_twisted P Q : eq (from_twisted (P + Q)%E) (add (from_twisted P) (from_twisted Q)). @@ -145,7 +145,7 @@ Module Extended. symmetry; assumption. Qed. - Lemma homomorphism_from_twisted : @Group.is_homomorphism Epoint E.eq E.add point eq add from_twisted. + Lemma homomorphism_from_twisted : @Monoid.is_homomorphism Epoint E.eq E.add point eq add from_twisted. Proof. split; trivial using Proper_from_twisted, add_from_twisted. Qed. Definition zero : point := from_twisted E.zero. @@ -235,17 +235,17 @@ Module Extended. Next Obligation. destruct P as [ [ [ [ ] ? ] ? ] [ ? [ ? ? ] ] ]; unfold onCurve in *; simpl. (rewrite_strat bottomup hints field_homomorphism); try assumption. - eauto 10 using is_homomorphism_phi_proper, phi_nonzero. + eauto 10 using Monoid.is_homomorphism_phi_proper, phi_nonzero. Qed. Context {point_phi:Fpoint->Kpoint} {point_phi_Proper:Proper (eq==>eq) point_phi} {point_phi_correct: forall (P:Fpoint), eq (point_phi P) (ref_phi P)}. - Lemma lift_homomorphism : @Group.is_homomorphism Fpoint eq (add(a_eq_minus1:=HFa)(Htwice_d:=HFdd)) Kpoint eq (add(a_eq_minus1:=HKa)(Htwice_d:=HKdd)) point_phi. + Lemma lift_homomorphism : @Monoid.is_homomorphism Fpoint eq (add(a_eq_minus1:=HFa)(Htwice_d:=HFdd)) Kpoint eq (add(a_eq_minus1:=HKa)(Htwice_d:=HKdd)) point_phi. Proof. repeat match goal with - | |- Group.is_homomorphism => split + | |- Monoid.is_homomorphism => split | |- _ => intro | |- _ /\ _ => split | [H: _ /\ _ |- _ ] => destruct H diff --git a/src/EdDSARepChange.v b/src/EdDSARepChange.v index 5bbea7f48..1efa0d689 100644 --- a/src/EdDSARepChange.v +++ b/src/EdDSARepChange.v @@ -1,7 +1,7 @@ Require Import Crypto.Util.FixCoqMistakes. Require Import Crypto.Spec.EdDSA Bedrock.Word. Require Import Coq.Classes.Morphisms Coq.Relations.Relation_Definitions. -Require Import Crypto.Algebra. Import Group ScalarMult. +Require Import Crypto.Algebra. Import Monoid Group ScalarMult. Require Import Crypto.Util.Decidable Crypto.Util.Option Crypto.Util.Tactics. Require Import Coq.omega.Omega. Require Import Crypto.Util.Notations. diff --git a/src/Encoding/PointEncoding.v b/src/Encoding/PointEncoding.v index 92ba91a6d..10d4387a2 100644 --- a/src/Encoding/PointEncoding.v +++ b/src/Encoding/PointEncoding.v @@ -126,7 +126,7 @@ Section PointEncoding. {phi_sqrt : forall x, Keq (phi (Fsqrt x)) (Ksqrt (phi x))} {Fsqrt_square : forall x root, eq x (F.mul root root) -> eq (Fsqrt x) root}. - Lemma point_phi_homomorphism: @Algebra.Group.is_homomorphism + Lemma point_phi_homomorphism: @Algebra.Monoid.is_homomorphism Fpoint E.eq Fpoint_add Kpoint Kpoint_eq Kpoint_add point_phi. Proof. diff --git a/src/Experiments/Ed25519.v b/src/Experiments/Ed25519.v index 718d8435d..1deb5fa80 100644 --- a/src/Experiments/Ed25519.v +++ b/src/Experiments/Ed25519.v @@ -4,6 +4,7 @@ Require Import Crypto.Util.Decidable. Require Crypto.Specific.GF25519. Require Crypto.CompleteEdwardsCurve.ExtendedCoordinates. Require Crypto.Encoding.PointEncoding. +Require Crypto.Util.IterAssocOp. Import Morphisms. Context {H: forall n : nat, Word.word n -> Word.word (b + b)}. @@ -127,6 +128,8 @@ Let ERepEnc := (ExtendedCoordinates.Extended.to_twisted P)) ). +Let SRep := Tuple.tuple (Word.word 32) 8. + Let S2Rep := fun (x : ModularArithmetic.F.F l) => Tuple.map (ZNWord 32) (Tuple.from_list_default (BinInt.Z.of_nat 0) 8 @@ -150,6 +153,28 @@ Let ErepAdd := a d GF25519.field25519 twedprm_ERep _ eq_a_minus1 twice_d (eq_refl _) ). +Axiom SRep_testbit : SRep -> nat -> bool. +Axiom ERepSel : bool -> Erep -> Erep -> Erep. + +Let SRepERepMul : SRep -> Erep -> Erep := + IterAssocOp.iter_op + (op:=ErepAdd) + (id:=ExtendedCoordinates.Extended.zero(field:=GF25519.field25519)(prm:=twedprm_ERep)) + (scalar:=SRep) + SRep_testbit + (sel:=ERepSel) + (BinInt.Z.to_nat (BinInt.Z.log2_up l)) +. + +Lemma SRepERepMul_correct n P : + ExtendedCoordinates.Extended.eq + (EToRep (CompleteEdwardsCurve.E.mul n P)) + (SRepERepMul (S2Rep (ModularArithmetic.F.of_nat l n)) (EToRep P)). +Proof. + pose proof @IterAssocOp.iter_op_correct. + pose proof @Algebra.ScalarMult.homomorphism_scalarmult. +Abort. + (* TODO : unclear what we're doing with the placeholder [feEnc] at the moment, so leaving this admitted for now *) Lemma feEnc_correct : forall x, @@ -232,13 +257,13 @@ Check @sign_correct (* ERepEnc := *) ERepEnc (* ERepEnc_correct := *) ERepEnc_correct (* Proper_ERepEnc := *) (PointEncoding.Proper_Kencode_point (Kpoint_eq_correct := ext_eq_correct) (Proper_Kenc := Proper_feEnc)) - (* SRep := *) (Tuple.tuple (Word.word 32) 8) + (* SRep := *) SRep (* SRepEq := *) (Tuple.fieldwise Logic.eq) (* H0 := *) Tuple.Equivalence_fieldwise (* S2Rep := *) S2Rep (* SRepDecModL := *) _ (* SRepDecModL_correct := *) _ - (* SRepERepMul := *) _ + (* SRepERepMul := *) SRepERepMul (* SRepERepMul_correct := *) _ (* Proper_SRepERepMul := *) _ (* SRepEnc := *) _ @@ -355,7 +380,7 @@ Check @verify_correct (* S2Rep := *) S2Rep (* SRepDecModL := *) _ (* SRepDecModL_correct := *) _ - (* SRepERepMul := *) _ + (* SRepERepMul := *) SRepERepMul (* SRepERepMul_correct := *) _ (* Proper_SRepERepMul := *) _ (* SRepDec := *) _ diff --git a/src/Util/IterAssocOp.v b/src/Util/IterAssocOp.v index 1d553bd55..53d3a14d5 100644 --- a/src/Util/IterAssocOp.v +++ b/src/Util/IterAssocOp.v @@ -11,19 +11,14 @@ Section IterAssocOp. Context {T eq op id} {moinoid : @monoid T eq op id} {scalar : Type} (scToN : scalar -> N) (testbit : scalar -> nat -> bool) - (testbit_spec : forall x i, testbit x i = N.testbit_nat (scToN x) i). + (testbit_correct : forall x i, testbit x i = N.testbit_nat (scToN x) i). + Local Infix "===" := eq. Local Infix "===" := eq : type_scope. - Fixpoint nat_iter_op n a : T := - match n with - | 0%nat => id - | S n' => op a (nat_iter_op n' a) - end. + Local Notation nat_iter_op := (ScalarMult.scalarmult_ref (add:=op) (zero:=id)). - Lemma nat_iter_op_plus : forall m n a, + Lemma nat_iter_op_plus m n a : op (nat_iter_op m a) (nat_iter_op n a) === nat_iter_op (m + n) a. - Proof. - induction m; intros; simpl; rewrite ?left_identity, <-?IHm, ?associative; reflexivity. - Qed. + Proof. symmetry; eapply ScalarMult.scalarmult_add_l. Qed. Definition N_iter_op n a := match n with @@ -46,6 +41,8 @@ Section IterAssocOp. induction n using N.peano_ind; intros; rewrite ?N2Nat.inj_succ, ?N_iter_op_succ, ?IHn; reflexivity. Qed. + Context {sel:bool->T->T->T} {sel_correct:forall b x y, sel b x y = if b then y else x}. + Fixpoint funexp {A} (f : A -> A) (a : A) (exp : nat) : A := match exp with | O => a @@ -55,9 +52,10 @@ Section IterAssocOp. Definition test_and_op sc a (state : nat * T) := let '(i, acc) := state in let acc2 := op acc acc in + let acc2a := op a acc2 in match i with | O => (0, acc) - | S i' => (i', if testbit sc i' then op a acc2 else acc2) + | S i' => (i', sel (testbit sc i') acc2 acc2a) end. Definition iter_op bound sc a : T := @@ -125,8 +123,9 @@ Section IterAssocOp. destruct i; [ apply Hpre | ]. simpl. rewrite Nshiftr_succ. + rewrite sel_correct. case_eq (testbit sc i); intro testbit_eq; simpl; - rewrite testbit_spec in testbit_eq; rewrite testbit_eq; + rewrite testbit_correct in testbit_eq; rewrite testbit_eq; rewrite Hpre, <- plus_n_O, nat_iter_op_plus; reflexivity. Qed. @@ -138,7 +137,7 @@ Section IterAssocOp. Qed. Lemma funexp_test_and_op_index : forall n a x acc y, - fst (funexp (test_and_op n a) (x, acc) y) === x - y. + fst (funexp (test_and_op n a) (x, acc) y) = x - y. Proof. induction y; simpl; rewrite <- ?Minus.minus_n_O; try reflexivity. match goal with |- context[funexp ?a ?b ?c] => destruct (funexp a b c) as [i acc'] end. @@ -181,7 +180,7 @@ Section IterAssocOp. auto. Qed. - Lemma iter_op_spec : forall sc a bound, N.size_nat (scToN sc) <= bound -> + Lemma iter_op_correct : forall sc a bound, N.size_nat (scToN sc) <= bound -> iter_op bound sc a === nat_iter_op (N.to_nat (scToN sc)) a. Proof. intros. @@ -192,5 +191,4 @@ Section IterAssocOp. rewrite Nshiftr_size by auto. reflexivity. Qed. - -End IterAssocOp. +End IterAssocOp.
\ No newline at end of file |