From 8ee588acd5dd3f07832f819f044ee512ae5d85ec Mon Sep 17 00:00:00 2001 From: jadep Date: Tue, 14 Feb 2017 12:02:01 -0500 Subject: Removed code that will be completely replaced in the future; replaced some pointencoding things with axioms pending pointencoding rewrite by Andres --- src/Experiments/Ed25519.v | 396 ++-------------------------------------------- 1 file changed, 11 insertions(+), 385 deletions(-) (limited to 'src/Experiments') diff --git a/src/Experiments/Ed25519.v b/src/Experiments/Ed25519.v index db28ffe34..1a1bc9490 100644 --- a/src/Experiments/Ed25519.v +++ b/src/Experiments/Ed25519.v @@ -121,60 +121,6 @@ Definition EToRep := Definition ZNWord sz x := Word.NToWord sz (BinInt.Z.to_N x). Definition WordNZ {sz} (w : Word.word sz) := BinInt.Z.of_N (Word.wordToN w). -(* TODO : - GF25519.pack does most of the work here, but the spec currently talks - about 256-bit words and [pack] makes a sequence of short (in this case - 32- and 31-bit) Zs. We should either automate this transformation or change - the spec. - *) -(* MOVE : pre-Specific *) -Definition feEnc (x : GF25519BoundedCommon.fe25519) : Word.word 255 := - let '(x7, x6, x5, x4, x3, x2, x1, x0) := - (GF25519BoundedCommon.proj1_wire_digits (GF25519Bounded.pack (GF25519Bounded.freeze x))) in - Word.combine (ZNWord 32 x0) - (Word.combine (ZNWord 32 x1) - (Word.combine (ZNWord 32 x2) - (Word.combine (ZNWord 32 x3) - (Word.combine (ZNWord 32 x4) - (Word.combine (ZNWord 32 x5) - (Word.combine (ZNWord 32 x6) (ZNWord 31 x7))))))). - -(* MOVE : pre-Specific *) -Definition feDec (w : Word.word 255) : option GF25519BoundedCommon.fe25519 := - let w0 := Word.split1 32 _ w in - let a0 := Word.split2 32 _ w in - let w1 := Word.split1 32 _ a0 in - let a1 := Word.split2 32 _ a0 in - let w2 := Word.split1 32 _ a1 in - let a2 := Word.split2 32 _ a1 in - let w3 := Word.split1 32 _ a2 in - let a3 := Word.split2 32 _ a2 in - let w4 := Word.split1 32 _ a3 in - let a4 := Word.split2 32 _ a3 in - let w5 := Word.split1 32 _ a4 in - let a5 := Word.split2 32 _ a4 in - let w6 := Word.split1 32 _ a5 in - let w7 := Word.split2 32 _ a5 in - let result := (GF25519Bounded.unpack (GF25519BoundedCommon.word31_to_unbounded_word w7, - GF25519BoundedCommon.word32_to_unbounded_word w6, - GF25519BoundedCommon.word32_to_unbounded_word w5, - GF25519BoundedCommon.word32_to_unbounded_word w4, - GF25519BoundedCommon.word32_to_unbounded_word w3, - GF25519BoundedCommon.word32_to_unbounded_word w2, - GF25519BoundedCommon.word32_to_unbounded_word w1, - GF25519BoundedCommon.word32_to_unbounded_word w0)) in - if GF25519BoundedCommon.w64eqb (GF25519Bounded.ge_modulus result) (GF25519BoundedCommon.ZToWord64 1) - then None else (Some result). - -Definition ERepEnc := - (PointEncoding.Kencode_point - (Ksign := feSign) - (Kenc := feEnc) - (Kpoint := Erep) - (Kpoint_to_coord := fun P => CompleteEdwardsCurve.E.coordinates - (ExtendedCoordinates.Extended.to_twisted P (field:=GF25519Bounded.field25519))) - ). - Definition SRep := SC25519.SRep. Definition S2Rep := SC25519.S2Rep. @@ -461,76 +407,6 @@ Proof. intuition assumption. Qed. -(* TODO : automate (after moving feEnc) or consider moving this and feSign_correct pre-specific *) -Lemma feEnc_correct : forall x, - PointEncoding.Fencode x = feEnc (GF25519BoundedCommon.encode x). -Proof. - cbv [feEnc PointEncoding.Fencode]; intros. - rewrite GF25519Bounded.pack_correct, GF25519Bounded.freeze_correct. - rewrite GF25519BoundedCommon.proj1_fe25519_encode. - match goal with |- appcontext [GF25519.pack ?x] => - remember (GF25519.pack x) end. - transitivity (ZNWord 255 (Pow2Base.decode_bitwise GF25519.wire_widths (Tuple.to_list 8 w))). - { cbv [ZNWord]. - do 2 apply f_equal. - subst w. - pose proof GF25519.freezePreconditions25519. - match goal with - |- appcontext [GF25519.freeze ?x ] => - let A := fresh "H" in - pose proof (ModularBaseSystemProofs.freeze_decode x) as A end. - pose proof (ge_modulus_freeze x); pose proof (bounded_freeze x). - repeat match goal with - | |- _ => rewrite Tuple.to_list_from_list - | |- _ => progress cbv [ModularBaseSystem.pack ModularBaseSystemList.pack] - | |- _ => progress rewrite ?GF25519.pack_correct, ?GF25519.freeze_correct, - ?ModularBaseSystemOpt.pack_correct, - ?ModularBaseSystemOpt.freeze_opt_correct by reflexivity - | |- _ => rewrite Pow2BaseProofs.decode_bitwise_spec - by (auto using Conversion.convert_bounded, - Conversion.length_convert; cbv [In GF25519.wire_widths]; - intuition omega) - | H : length ?ls = ?n |- appcontext [Tuple.from_list_default _ ?n ?ls] => - rewrite Tuple.from_list_default_eq with (pf := H) - | |- appcontext [Tuple.from_list_default _ ?n ?ls] => - assert (length ls = n) by - (rewrite ModularBaseSystemListProofs.length_freeze; - try rewrite Tuple.length_to_list; reflexivity) - | |- _ => rewrite <-Conversion.convert_correct by auto - end. - rewrite <-ModularBaseSystemProofs.Fdecode_decode_mod with (us := ModularBaseSystem.encode x) by apply ModularBaseSystemProofs.encode_rep. - match goal with H : _ = ?b |- ?b = _ => rewrite <-H; clear H end. - cbv [ModularBaseSystem.freeze]. - rewrite Tuple.to_list_from_list. - rewrite Z.mod_small by (apply ModularBaseSystemListProofs.ge_modulus_spec; auto; cbv; congruence). - f_equal. } - { assert (Pow2Base.bounded GF25519.wire_widths (Tuple.to_list 8 w)). - { subst w. - rewrite GF25519.pack_correct, ModularBaseSystemOpt.pack_correct. - cbv [ModularBaseSystem.pack ModularBaseSystemList.pack]. - rewrite Tuple.to_list_from_list. - apply Conversion.convert_bounded. } - { destruct w; - repeat match goal with p : (_ * Z)%type |- _ => destruct p end. - cbv [Tuple.to_list Tuple.to_list'] in *. - rewrite Pow2BaseProofs.bounded_iff in *. - (* TODO : Is there a better way to do this? *) - pose proof (H 0). - pose proof (H 1). - pose proof (H 2). - pose proof (H 3). - pose proof (H 4). - pose proof (H 5). - pose proof (H 6). - pose proof (H 7). - clear H. - cbv [GF25519.wire_widths nth_default nth_error value] in *. - repeat rewrite combine_ZNWord by (rewrite ?Znat.Nat2Z.inj_add; simpl Z.of_nat; repeat apply lor_shiftl_bounds; omega). - cbv - [ZNWord Z.lor Z.shiftl]. - rewrite Z.shiftl_0_l. - rewrite Z.lor_0_r. - reflexivity. } } -Qed. (* TODO : automate *) Lemma initial_bounds : forall x n, @@ -662,67 +538,6 @@ Proof. intuition subst; reflexivity. Qed. -(* MOVE : wherever feEnc goes *) -Lemma Proper_feEnc : Proper (GF25519BoundedCommon.eq ==> eq) feEnc. -Proof. - pose proof GF25519.freezePreconditions25519. - repeat intro; cbv [feEnc]. - rewrite !GF25519Bounded.pack_correct, !GF25519Bounded.freeze_correct. - rewrite !GF25519.freeze_correct, !ModularBaseSystemOpt.freeze_opt_correct - by (rewrite ?Tuple.length_to_list; reflexivity). - cbv [GF25519BoundedCommon.eq ModularBaseSystem.eq] in *. - match goal with - H : ModularBaseSystem.decode ?x = ModularBaseSystem.decode ?y |- _ => - let A := fresh "H" in - let HP := fresh "H" in - let HQ := fresh "H" in - pose proof (ModularBaseSystemProofs.freeze_canonical - (freeze_pre := GF25519.freezePreconditions25519) - x y (ModularBaseSystem.decode x) - (ModularBaseSystem.decode y) eq_refl eq_refl); - match type of A with ?P -> ?Q -> _ => - assert P as HP by apply initial_bounds; - assert Q as HQ by apply initial_bounds end; - specialize (A HP HQ); clear HP HQ; apply A in H - end. - repeat match goal with |- appcontext [GF25519.pack ?x] => remember (GF25519.pack x) end. - match goal with x : GF25519.wire_digits, y : GF25519.wire_digits |- _ => - assert (Tuple.fieldwise (n := length GF25519.wire_widths) eq x y) as Heqxy end. - { subst. - rewrite !convert_freezes. - erewrite !Tuple.from_list_default_eq. - rewrite !Tuple.from_list_to_list. - apply Proper_pack. - assumption. } - { cbv [length GF25519.wire_digits] in *. - repeat match goal with p : (_ * _)%type |- _ => destruct p end. - cbv [GF25519.wire_widths length Tuple.fieldwise Tuple.fieldwise' fst snd] in *. - repeat match goal with H : _ /\ _ |- _ => destruct H end; - subst; reflexivity. } - Grab Existential Variables. - rewrite Tuple.length_to_list; reflexivity. - rewrite Tuple.length_to_list; reflexivity. -Qed. - -Lemma ERepEnc_correct P : Eenc P = ERepEnc (EToRep P). -Proof. - cbv [Eenc ERepEnc EToRep sign Fencode]. - transitivity (PointEncoding.encode_point (b := 255) P); - [ | eapply (PointEncoding.Kencode_point_correct - (Ksign_correct := feSign_correct) - (Kenc_correct := feEnc_correct) - (Proper_Ksign := Proper_feSign) - (Proper_Kenc := Proper_feEnc)) - ]. - reflexivity. - Grab Existential Variables. - intros. - eapply @CompleteEdwardsCurveTheorems.E.Proper_coordinates. - { apply GF25519Bounded.field25519. } - { exact _. } - { apply ExtendedCoordinates.Extended.to_twisted_from_twisted. } -Qed. - Lemma ext_eq_correct : forall p q : Erep, ExtendedCoordinates.Extended.eq (field:=GF25519Bounded.field25519) p q <-> Tuple.fieldwise (n := 2) GF25519BoundedCommon.eq (extended_to_coord p) (extended_to_coord q). @@ -790,6 +605,10 @@ Proof. (* Time Qed. (* Finished transaction in 1646.167 secs (1645.753u,0.339s) (successful) *) *) Admitted. +Axiom ERepEnc : Erep -> Word.word b. +Axiom ERepEnc_correct : (forall P : E, Eenc P = ERepEnc (EToRep P)). +Axiom Proper_ERepEnc : Proper (ExtendedCoordinates.Extended.eq ==> eq) ERepEnc. + Definition sign := @EdDSARepChange.sign E (@CompleteEdwardsCurveTheorems.E.eq Fq (@eq Fq) (@ModularArithmetic.F.one q) (@ModularArithmetic.F.add q) (@ModularArithmetic.F.mul q) Spec.Ed25519.a Spec.Ed25519.d) @@ -842,7 +661,7 @@ Let sign_correct : forall pk sk {mlen} (msg:Word.word mlen), sign pk sk _ msg = (* Ahomom := *) Ahomom (* ERepEnc := *) ERepEnc (* ERepEnc_correct := *) ERepEnc_correct - (* Proper_ERepEnc := *) (PointEncoding.Proper_Kencode_point (Kpoint_eq_correct := ext_eq_correct) (Proper_Kenc := Proper_feEnc)) + (* Proper_ERepEnc := *) Proper_ERepEnc (* SRep := *) SRep (* SRepEq := *) SC25519.SRepEq (*(Tuple.fieldwise Logic.eq)*) (* H0 := *) SC25519.SRepEquiv (* Tuple.Equivalence_fieldwise*) @@ -925,7 +744,7 @@ Proof. split; break_match; intros; inversion_option; subst; f_equal; repeat match goal with | |- _ => rewrite !WordUtil.wordToN_NToWord_idempotent in * - by (apply ZToN_NPow2_lt; split; try omega; eapply Z.lt_le_trans; + by (apply N.ZToN_NPow2_lt; split; try omega; eapply Z.lt_le_trans; [ intuition eassumption | ]; cbv; congruence) | |- _ => rewrite WordUtil.NToWord_wordToN | |- _ => rewrite Z2N.id in * by omega @@ -950,26 +769,6 @@ Proof. unfold SRepDec, S2Rep, SC25519.S2Rep; intros; reflexivity. Qed. -Definition ERepDec := - (@PointEncoding.Kdecode_point - _ - GF25519BoundedCommon.fe25519 - GF25519BoundedCommon.eq - GF25519BoundedCommon.zero - GF25519BoundedCommon.one - GF25519Bounded.opp - GF25519Bounded.add - GF25519Bounded.sub - GF25519Bounded.mul - GF25519BoundedCommon.div - _ a d feSign - _ (ExtendedCoordinates.Extended.from_twisted - (field := GF25519Bounded.field25519) - (prm := twedprm_ERep) - ) - feDec GF25519Bounded.sqrt - ). - Lemma extended_to_coord_from_twisted: forall pt, Tuple.fieldwise (n := 2) GF25519BoundedCommon.eq (extended_to_coord (ExtendedCoordinates.Extended.from_twisted pt)) @@ -980,163 +779,6 @@ Proof. reflexivity. Qed. -(* MOVE : same place as feDec *) (* TODO : automate *) -Lemma feDec_correct : forall w : Word.word (pred b), - option_eq GF25519BoundedCommon.eq - (option_map GF25519BoundedCommon.encode - (PointEncoding.Fdecode w)) (feDec w). -Proof. - intros; cbv [PointEncoding.Fdecode feDec]. - Print GF25519BoundedCommon.eq. - rewrite <-GF25519BoundedCommon.word64eqb_Zeqb. - rewrite GF25519Bounded.ge_modulus_correct. - rewrite GF25519BoundedCommon.word64ToZ_ZToWord64 by - (rewrite GF25519BoundedCommon.unfold_Pow2_64; - cbv [GF25519BoundedCommon.Pow2_64]; omega). - rewrite GF25519.ge_modulus_correct. - rewrite ModularBaseSystemOpt.ge_modulus_opt_correct. - match goal with - |- appcontext [GF25519Bounded.unpack ?x] => - assert ((Z.of_N (Word.wordToN w)) = BaseSystem.decode (Pow2Base.base_from_limb_widths PseudoMersenneBaseParams.limb_widths) (Tuple.to_list 10 (GF25519BoundedCommon.proj1_fe25519 (GF25519Bounded.unpack x)))) end. - { - rewrite GF25519Bounded.unpack_correct. - rewrite GF25519.unpack_correct, ModularBaseSystemOpt.unpack_correct. - - cbv [GF25519BoundedCommon.proj1_wire_digits - GF25519BoundedCommon.wire_digitsWToZ - GF25519BoundedCommon.proj1_wire_digitsW - GF25519BoundedCommon.app_wire_digits - HList.mapt HList.mapt' - length GF25519.wire_widths - fst snd - ]. - - cbv [GF25519BoundedCommon.proj_word - GF25519BoundedCommon.word31_to_unbounded_word - GF25519BoundedCommon.word32_to_unbounded_word - GF25519BoundedCommon.word_to_unbounded_word - GF25519BoundedCommon.Build_bounded_word - GF25519BoundedCommon.Build_bounded_word' - ]. - rewrite !GF25519BoundedCommon.word64ToZ_ZToWord64 by - (rewrite GF25519BoundedCommon.unfold_Pow2_64; - cbv [GF25519BoundedCommon.Pow2_64]; - apply WordNZ_range; cbv; congruence). - rewrite !WordNZ_split1. - rewrite !WordNZ_split2. - simpl Z.of_nat. - cbv [ModularBaseSystem.eq]. - match goal with - |- appcontext [@ModularBaseSystem.unpack _ _ ?ls _ _ ?t] => - assert (Pow2Base.bounded ls (Tuple.to_list (length ls) t)) end. - { cbv [Pow2Base.bounded length]. - intros. - destruct (lt_dec i 8). - { cbv [Tuple.to_list Tuple.to_list' fst snd]. - assert (i = 0 \/ i = 1 \/ i = 2 \/ i = 3 \/ i = 4 \/ i = 5 \/ i = 6 \/ i = 7) by omega. - repeat match goal with H : (_ \/ _)%type |- _ => destruct H; subst end; - cbv [nth_default nth_error value]; try (apply pow2_mod_range; omega). - repeat apply shiftr_range; try omega; apply WordNZ_range_mono; cbv; - congruence. } - { rewrite !nth_default_out_of_bounds - by (rewrite ?Tuple.length_to_list; cbv [length]; omega). - rewrite Z.pow_0_r. omega. } } - cbv [ModularBaseSystem.unpack ModularBaseSystemList.unpack]. - rewrite Tuple.to_list_from_list. - rewrite <-Conversion.convert_correct by (auto || rewrite Tuple.to_list; reflexivity). - rewrite <-Pow2BaseProofs.decode_bitwise_spec by (auto || cbv [In]; intuition omega). - cbv [Tuple.to_list Tuple.to_list' length fst snd Pow2Base.decode_bitwise Pow2Base.decode_bitwise' nth_default nth_error value ]. - clear. - apply Z.bits_inj'. - intros. - rewrite Z.shiftl_0_l. - rewrite Z.lor_0_r. - repeat match goal with |- appcontext[@Word.wordToN (?x + ?y) w] => - change (@Word.wordToN (x + y) w) with (@Word.wordToN (pred b) w) end. - assert ( - 0 <= n < 32 \/ - 32 <= n < 64 \/ - 64 <= n < 96 \/ - 96 <= n < 128 \/ - 128 <= n < 160 \/ - 160 <= n < 192 \/ - 192 <= n < 224 \/ - 224 <= n < 256 \/ - 256 <= n)%Z by omega. - repeat match goal with H : (_ \/ _)%type |- _ => destruct H; subst end; - repeat match goal with - | |- _ => rewrite Z.lor_spec - | |- _ => rewrite Z.shiftl_spec by omega - | |- _ => rewrite Z.shiftr_spec by omega - | |- _ => rewrite Z.testbit_neg_r by omega - | |- _ => rewrite ZUtil.Z.testbit_pow2_mod by omega; - VerdiTactics.break_if; try omega - end; - repeat match goal with - | |- _ = (false || _)%bool => rewrite Bool.orb_false_l - | |- ?x = (?x || ?y)%bool => replace y with false; - [ rewrite Bool.orb_false_r; reflexivity | ] - | |- false = (?x || ?y)%bool => replace y with false; - [ rewrite Bool.orb_false_r; - replace x with false; [ reflexivity | ] - | ] - | |- false = Z.testbit _ _ => - rewrite Z.testbit_neg_r by omega; reflexivity - | |- Z.testbit ?w ?n = Z.testbit ?w ?m => - replace m with n by omega; reflexivity - | |- Z.testbit ?w ?n = (Z.testbit ?w ?m || _)%bool => - replace m with n by omega - end. - } - match goal with - |- option_eq _ (option_map _ (if Z_lt_dec ?a ?b then Some _ else None)) (if (?X =? 1)%Z then None else Some _) => - assert ((a < b)%Z <-> X = 0%Z) end. - { - rewrite ModularBaseSystemListProofs.ge_modulus_spec; - [ | cbv; congruence | rewrite Tuple.length_to_list; reflexivity | ]. - Focus 2. { - rewrite GF25519Bounded.unpack_correct. - rewrite GF25519.unpack_correct, ModularBaseSystemOpt.unpack_correct. - cbv [ModularBaseSystem.unpack]. - rewrite Tuple.to_list_from_list. - cbv [ModularBaseSystemList.unpack]. - apply Conversion.convert_bounded. - } Unfocus. - rewrite <-H. - intuition; try omega. - apply Znat.N2Z.is_nonneg. - } - - do 2 VerdiTactics.break_if; - [ - match goal with H: ?P, Hiff : ?P <-> ?x = 0%Z |- _ => - let A := fresh "H" in - pose proof ((proj1 Hiff) H) as A; - rewrite A in *; discriminate - end - | | reflexivity | - match goal with - H: ~ ?P, Hiff : ?P <-> ModularBaseSystemList.ge_modulus ?x = 0%Z - |- _ => - exfalso; apply H; apply Hiff; - destruct (ModularBaseSystemListProofs.ge_modulus_01 x) as [Hgm | Hgm]; - rewrite Hgm in *; try discriminate; reflexivity - end ]. - - cbv [option_map option_eq]. - cbv [GF25519BoundedCommon.eq]. - rewrite GF25519BoundedCommon.proj1_fe25519_encode. - cbv [ModularBaseSystem.eq]. - etransitivity. - Focus 2. { - cbv [ModularBaseSystem.decode ModularBaseSystemList.decode]. - cbv [length PseudoMersenneBaseParams.limb_widths GF25519.params25519] in H |- *. - rewrite <-H. - reflexivity. } Unfocus. - apply ModularBaseSystemProofs.encode_rep. - -Qed. - Lemma Fsqrt_minus1_correct : ModularArithmetic.F.mul Fsqrt_minus1 Fsqrt_minus1 = ModularArithmetic.F.opp @@ -1297,26 +939,6 @@ Proof. eapply f_equal. eapply f_equal. eapply f_equal. rewrite Hxy. reflexivity. Qed. -Lemma ERepDec_correct : forall w : Word.word b, - option_eq ExtendedCoordinates.Extended.eq (ERepDec w) (@option_map E Erep EToRep (Edec w)). -Proof. - exact (@PointEncoding.Kdecode_point_correct - (pred b) _ Spec.Ed25519.a Spec.Ed25519.d _ - GF25519.modulus_gt_2 bound_check255 - _ _ _ _ _ _ _ _ _ _ GF25519Bounded.field25519 - _ _ _ _ _ phi_a phi_d feSign feSign_correct _ - (ExtendedCoordinates.Extended.from_twisted - (field := GF25519Bounded.field25519) - (prm := twedprm_ERep)) - extended_to_coord - extended_to_coord_from_twisted - _ ext_eq_correct _ _ encode_eq_iff - feDec GF25519Bounded.sqrt _ _ feDec_correct - (@PrimeFieldTheorems.F.sqrt_5mod8 _ Fsqrt_minus1) - sqrt_correct - ). -Qed. - Lemma eq_enc_E_iff : forall (P_ : Word.word b) (P : E), Eenc P = P_ <-> Option.option_eq CompleteEdwardsCurveTheorems.E.eq (Edec P_) (Some P). @@ -1329,6 +951,10 @@ Proof. symmetry; eassumption. Qed. +Axiom ERepDec : Word.word b -> option Erep. +Axiom ERepDec_correct : forall w : Word.word b, + option_eq ExtendedCoordinates.Extended.eq (ERepDec w) (option_map EToRep (Edec w)). + Definition verify := @verify E b SHA512 B Erep ErepAdd (@ExtendedCoordinates.Extended.opp GF25519BoundedCommon.fe25519 GF25519BoundedCommon.eq GF25519BoundedCommon.zero @@ -1377,7 +1003,7 @@ Let verify_correct : (* Ahomom := *) Ahomom (* ERepEnc := *) ERepEnc (* ERepEnc_correct := *) ERepEnc_correct - (* Proper_ERepEnc := *) (PointEncoding.Proper_Kencode_point (Kpoint_eq_correct := ext_eq_correct) (Proper_Kenc := Proper_feEnc)) + (* Proper_ERepEnc := *) Proper_ERepEnc (* ERepDec := *) ERepDec (* ERepDec_correct := *) ERepDec_correct (* SRep := *) SRep (*(Tuple.tuple (Word.word 32) 8)*) -- cgit v1.2.3