diff --git a/src/Algebra/Group.v b/src/Algebra/Group.v index 363099bf900..ca4d76f59c9 100644 --- a/src/Algebra/Group.v +++ b/src/Algebra/Group.v @@ -87,16 +87,6 @@ Section Homomorphism. apply inv_unique. rewrite <- Monoid.homomorphism, left_inverse, homomorphism_id; reflexivity. Qed. - - Lemma compose_homomorphism - {H2 eq2 op2 id2 inv2} {groupH2:@group H2 eq2 op2 id2 inv2} - {phi2:H->H2}`{homom2:@Monoid.is_homomorphism H eq op H2 eq2 op2 phi2} - : @Monoid.is_homomorphism G EQ OP H2 eq2 op2 (fun x => phi2 (phi x)). - Proof. - split; repeat intro. - { do 2 rewrite homomorphism. f_equiv. } - { f_equiv. f_equiv. trivial. } - Qed. End Homomorphism. Section GroupByIsomorphism. diff --git a/src/Bedrock/End2End/X25519/GarageDoor.v b/src/Bedrock/End2End/X25519/GarageDoor.v index b1161ab8ec8..c20471049ed 100644 --- a/src/Bedrock/End2End/X25519/GarageDoor.v +++ b/src/Bedrock/End2End/X25519/GarageDoor.v @@ -172,10 +172,10 @@ Local Definition be2 z := rev (le_split 2 z). Local Coercion to_list : tuple >-> list. Local Coercion Z.b2z : bool >-> Z. -Definition state : Type := list byte * list byte. (* seed, xs25519 secret key *) +Record state := { prng_state : list byte ; x25519_ephemeral_secret : list byte }. -Definition garagedoor_iteration : state -> list (lightbulb_spec.OP _) -> state -> Prop := - fun '(seed, sk) ioh '(SEED, SK) => +Definition protocol_step : state -> list _ -> state -> Prop := + fun '(Build_state seed sk) ioh '(Build_state SEED SK) => (lightbulb_spec.lan9250_recv_no_packet _ ioh \/ lightbulb_spec.lan9250_recv_packet_too_long _ ioh \/ TracePredicate.concat TracePredicate.any (lightbulb_spec.spi_timeout _) ioh) /\ SEED=seed /\ SK=sk \/ @@ -232,7 +232,7 @@ Local Instance spec_of_memswap : spec_of "memswap" := spec_of_memswap. Local Instance spec_of_memequal : spec_of "memequal" := spec_of_memequal. -Definition memrep bs R : state -> map.rep(map:=SortedListWord.map _ _) -> Prop := fun '(seed, sk) m => +Definition memrep bs R : state -> map.rep(map:=SortedListWord.map _ _) -> Prop := fun '(Build_state seed sk) m => m =* seed$@(word.of_Z ST) * sk$@(word.add (word.of_Z ST) (word.of_Z 32)) * @@ -244,11 +244,11 @@ Definition memrep bs R : state -> map.rep(map:=SortedListWord.map _ _) -> Prop : Global Instance spec_of_loopfn : spec_of "loopfn" := fnspec! "loopfn" / seed sk bs R, - { requires t m := memrep bs R (seed, sk) m; - ensures T M := exists SEED SK BS, memrep BS R (SEED, SK) M /\ + { requires t m := memrep bs R (Build_state seed sk) m; + ensures T M := exists SEED SK BS, memrep BS R (Build_state SEED SK) M /\ exists iol, T = iol ++ t /\ exists ioh, SPI.mmio_trace_abstraction_relation ioh iol /\ - garagedoor_iteration (seed, sk) ioh (SEED, SK) }. + protocol_step (Build_state seed sk) ioh (Build_state SEED SK) }. Import ZnWords. Import coqutil.Tactics.autoforward. @@ -260,7 +260,7 @@ Local Existing Instance ChaCha20.spec_of_chacha20. Lemma loopfn_ok : program_logic_goal_for_function! loopfn. Proof. straightline. - cbv [memrep garagedoor_iteration] in *. + cbv [memrep protocol_step] in *. repeat straightline. rename H11 into Lseed. rename H12 into Lsk. rename H13 into H11. straightline_call; try ecancel_assumption; trivial; repeat straightline. diff --git a/src/Bedrock/End2End/X25519/GarageDoorTop.v b/src/Bedrock/End2End/X25519/GarageDoorTop.v index c4815029520..24904fba076 100644 --- a/src/Bedrock/End2End/X25519/GarageDoorTop.v +++ b/src/Bedrock/End2End/X25519/GarageDoorTop.v @@ -165,23 +165,29 @@ Lemma compiler_emitted_valid_instructions : bverify.bvalidInstructions Decode.RV32IM garagedoor_insns = true. Proof. vm_cast_no_check (eq_refl true). Qed. -Definition good_transitions (s : state)(t : Semantics.trace)(s' : state) := - exists ioh, SPI.mmio_trace_abstraction_relation ioh t /\ - (BootSeq +++ stateful garagedoor_iteration s s') ioh. -Definition good_trace t := exists s0 s, good_transitions s0 t s. +Import SPI riscv.Platform.RiscvMachine. +Definition only_mmio_satisfying P t := + exists mmios, mmio_trace_abstraction_relation mmios t /\ P mmios. + +Local Notation labeled_transitions := stateful. +Local Notation boot_seq := BootSeq. + +Definition protocol_invariant (s s' : state) (trace : list RiscvMachine.LogItem) := + only_mmio_satisfying (boot_seq +++ labeled_transitions protocol_step s s') trace. +Definition protocol_spec t := exists s s', protocol_invariant s s' t. Import ExprImpEventLoopSpec. Definition garagedoor_spec : ProgramSpec := {| datamem_start := MemoryLayout.heap_start ml; datamem_pastend := MemoryLayout.heap_pastend ml; - goodTrace := good_trace; - isReady t m := exists s0 s, good_transitions s0 t s /\ exists bs R, memrep bs R s m |}. + goodTrace := protocol_spec; + isReady t m := exists s s', protocol_invariant s' s t /\ exists bs R, memrep bs R s m |}. Lemma good_trace_from_isRead a a0 : isReady garagedoor_spec a a0 -> isReady garagedoor_spec a a0 /\ ExprImpEventLoopSpec.goodTrace garagedoor_spec a. Proof. - cbv [isReady goodTrace garagedoor_spec good_trace]; intuition eauto. + cbv [isReady goodTrace garagedoor_spec protocol_spec]; intuition eauto. case H as (?&?&?&?&?&H); eauto. Qed. @@ -214,10 +220,10 @@ Implicit Types mach : RiscvMachine. Local Coercion word.unsigned : word.rep >-> Z. Definition initial_conditions mach := - mach.(getPc) = code_start ml /\ + 0x20400000 = mach.(getPc) /\ + [] = mach.(getLog) /\ mach.(getNextPc) = word.add mach.(getPc) (word.of_Z 4) /\ regs_initialized (getRegs mach) /\ - mach.(getLog) = [] /\ (forall a : word32, code_start ml <= a < code_pastend ml -> In a (getXAddrs mach)) /\ valid_machine mach /\ (imem (code_start ml) (code_pastend ml) garagedoor_insns ⋆ @@ -233,7 +239,7 @@ Proof. eexists garagedoor_insns. eexists garagedoor_finfo. eexists garagedoor_stack_size. - rewrite garagedoor_compiler_result_ok; ssplit; trivial using compiler_emitted_valid_instructions. + rewrite garagedoor_compiler_result_ok; ssplit; trivial using compiler_emitted_valid_instructions; try congruence. 2,3:vm_compute; inversion 1. econstructor (* ProgramSatisfiesSpec *). 1: vm_compute; reflexivity. @@ -241,6 +247,7 @@ Proof. 3: instantiate (1:=snd loop). 1,3: exact eq_refl. 1,2: cbv [hl_inv]; intros; eapply MetricSemantics.of_metrics_free; eapply WeakestPreconditionProperties.sound_cmd. + 3: { eapply word.unsigned_inj. rewrite <-H. trivial. } all : repeat straightline; subst args. { cbv [LowerPipeline.mem_available LowerPipeline.ptsto_bytes] in *. @@ -266,7 +273,8 @@ Proof. rewrite <-(List.firstn_skipn 1520 (skipn 32 (skipn 64 anybytes))) in M. do 2 seprewrite_in @Array.bytearray_append M. rewrite ?firstn_length, ?skipn_length, ?Nat2Z.inj_min, ?Nat2Z.inj_sub, H6_emp0 in M. - cbv [isReady garagedoor_spec good_trace good_transitions]. eexists (_,_), (_,_); fwd. eauto. + cbv [isReady garagedoor_spec protocol_spec protocol_invariant only_mmio_satisfying]. + eexists (Build_state _ _), (Build_state _ _); fwd. eauto. { rewrite <-app_nil_l. eapply TracePredicate.concat_app; eauto. econstructor. } cbv [memrep]. ssplit. { use_sep_assumption. cancel. @@ -277,13 +285,13 @@ Proof. all : repeat rewrite ?firstn_length, ?skipn_length; try Lia.lia. } { match goal with H : goodTrace _ _ |- _ => clear H end. - cbv [isReady goodTrace good_trace garagedoor_spec] in *; repeat straightline. + cbv [isReady goodTrace protocol_spec protocol_invariant garagedoor_spec] in *; repeat straightline. DestructHead.destruct_head' state. Tactics.rapply WeakestPreconditionProperties.Proper_call; [|eapply link_loopfn]; try eassumption. intros ? ? ? ?; repeat straightline; eapply good_trace_from_isRead. eexists; fwd; try eassumption. - cbv [good_trace good_transitions] in *; repeat straightline. + cbv [protocol_spec protocol_invariant only_mmio_satisfying] in *; repeat straightline. { subst a. (eexists; split; [eapply Forall2_app; eauto|]). eapply stateful_app_r, stateful_singleton; eauto. } } Qed. @@ -291,7 +299,7 @@ Qed. Theorem garagedoor_invariant_proof: exists invariant: RiscvMachine -> Prop, (forall mach, initial_conditions mach -> invariant mach) /\ (forall mach, invariant mach -> run1 mach invariant) /\ - (forall mach, invariant mach -> exists extend, good_trace (getLog mach ;++ extend)). + (forall mach, invariant mach -> exists extend, protocol_spec (getLog mach ;++ extend)). Proof. exists (ll_inv compile_ext_call ml garagedoor_spec). unshelve epose proof compiler_invariant_proofs _ _ _ _ _ garagedoor_spec as HCI; shelve_unifiable; try exact _. @@ -305,10 +313,10 @@ Qed. Import OmniSmallstepCombinators. -Theorem garagedoor_correct mach : initial_conditions mach -> - always run1 (eventually run1 (fun mach' => good_trace mach'.(getLog))) mach. +Theorem garagedoor_correct : forall mach, initial_conditions mach -> + always run1 (eventually run1 (fun mach' => protocol_spec mach'.(getLog))) mach. Proof. - intros H%initial_conditions_sufficient; revert H. + intros ? H%initial_conditions_sufficient; revert H. unshelve Tactics.rapply @always_eventually_good_trace; trivial using ml_ok, @Naive.word32_ok. { eapply (naive_word_riscv_ok 5%nat). } { eapply @SortedListString.ok. } diff --git a/src/Curves/EdwardsMontgomery25519.v b/src/Curves/EdwardsMontgomery25519.v deleted file mode 100644 index d4182180777..00000000000 --- a/src/Curves/EdwardsMontgomery25519.v +++ /dev/null @@ -1,51 +0,0 @@ -Require Import Coq.ZArith.ZArith. Local Open Scope Z_scope. -Require Import Crypto.Spec.ModularArithmetic. Local Open Scope F_scope. -Require Import Crypto.Curves.EdwardsMontgomery. Import M. -Require Import Crypto.Curves.Edwards.TwistIsomorphism. -Require Import Crypto.Spec.Curve25519. - -Local Definition sqrtm1 : F p := F.pow (F.of_Z _ 2) ((N.pos p-1)/4). -Local Definition sqrt := PrimeFieldTheorems.F.sqrt_5mod8 sqrtm1. - -Import MontgomeryCurve CompleteEdwardsCurve. - -Local Definition a' := (M.a + (1 + 1)) / M.b. -Local Definition d' := (M.a - (1 + 1)) / M.b. -Definition r := sqrt (F.inv ((a' / M.b) / E.a)). - -Local Lemma is_twist : E.a * d' = a' * E.d. Proof. Decidable.vm_decide. Qed. -Local Lemma nonzero_a' : a' <> 0. Proof. Decidable.vm_decide. Qed. -Local Lemma r_correct : E.a = r * r * a'. Proof. Decidable.vm_decide. Qed. - -Definition Montgomery_of_Edwards (P : Curve25519.E.point) : Curve25519.M.point := - @of_Edwards _ _ _ _ _ _ _ _ _ _ field _ char_ge_3 M.a M.b M.b_nonzero a' d' eq_refl eq_refl nonzero_a' - (@E.point2_of_point1 _ _ _ _ _ _ _ _ _ _ field _ E.a E.d a' d' is_twist E.nonzero_a nonzero_a' r r_correct P). - -Definition Edwards_of_Montgomery (P : Curve25519.M.point) : Curve25519.E.point := - @E.point1_of_point2 _ _ _ _ _ _ _ _ _ _ field _ E.a E.d a' d' is_twist E.nonzero_a nonzero_a' r r_correct - (@to_Edwards _ _ _ _ _ _ _ _ _ _ field _ M.a M.b M.b_nonzero a' d' eq_refl eq_refl nonzero_a' P). - -Local Notation Eopp := ((@AffineProofs.E.opp _ _ _ _ _ _ _ _ _ _ field _ E.a E.d E.nonzero_a)). - -Local Arguments Hierarchy.commutative_group _ {_} _ {_ _}. -Local Arguments CompleteEdwardsCurve.E.add {_ _ _ _ _ _ _ _ _ _ _ _ _} _ _ {_ _ _}. -Local Arguments Monoid.is_homomorphism {_ _ _ _ _ _}. -Local Arguments to_Edwards {_ _ _ _ _ _ _ _ _ _ _ _ _ _ _} _ _ { _ _ _ }. -Local Arguments of_Edwards {_ _ _ _ _ _ _ _ _ _ _ _ _ _ _ _} _ _ { _ _ _ }. - -Lemma EdwardsMontgomery25519 : @Group.isomorphic_commutative_groups - Curve25519.E.point E.eq Curve25519.E.add Curve25519.E.zero Eopp Curve25519.M.point - M.eq Curve25519.M.add M.zero Curve25519.M.opp - Montgomery_of_Edwards Edwards_of_Montgomery. -Proof. - cbv [Montgomery_of_Edwards Edwards_of_Montgomery]. - epose proof E.twist_isomorphism(a1:=E.a)(a2:=a')(d1:=E.d)(d2:=d')(r:=r) as AB. - epose proof EdwardsMontgomeryIsomorphism(a:=Curve25519.M.a)(b:=Curve25519.M.b)as BC. - destruct AB as [A B ab ba], BC as [_ C bc cb]. - pose proof Group.compose_homomorphism(homom:=ab)(homom2:=bc) as ac. - pose proof Group.compose_homomorphism(homom:=cb)(homom2:=ba)(groupH2:=ltac:(eapply A)) as ca. - split; try exact ac; try exact ca; try exact A; try exact C. - Unshelve. - all : try (pose (@PrimeFieldTheorems.F.Decidable_square p prime_p eq_refl); Decidable.vm_decide). - all : try (eapply Hierarchy.char_ge_weaken; try apply ModularArithmeticTheorems.F.char_gt; Decidable.vm_decide). -Qed. diff --git a/src/Spec/Curve25519.v b/src/Spec/Curve25519.v index 2908a63c7a3..f8a7d55650d 100644 --- a/src/Spec/Curve25519.v +++ b/src/Spec/Curve25519.v @@ -82,17 +82,7 @@ Require Import Spec.CompleteEdwardsCurve. Module E. Definition a : F := F.opp 1. Definition d : F := F.div (F.opp (F.of_Z _ 121665)) (F.of_Z _ 121666). - - Lemma nonzero_a : a <> F.zero. Proof. Decidable.vm_decide. Qed. - Lemma square_a : exists sqrt_a, F.mul sqrt_a sqrt_a = a. - Proof. epose (@PrimeFieldTheorems.F.Decidable_square p prime_p eq_refl); Decidable.vm_decide. Qed. - Lemma nonsquare_d : forall x, F.mul x x <> d. - Proof. epose (@PrimeFieldTheorems.F.Decidable_square p prime_p eq_refl); Decidable.vm_decide. Qed. - Definition point := @E.point F eq F.one F.add F.mul a d. - Definition add := E.add(field:=field)(char_ge_3:=char_ge_3)(a:=a)(d:=d) - (nonzero_a:=nonzero_a)(square_a:=square_a)(nonsquare_d:=nonsquare_d). - Definition zero := E.zero(field:=field)(a:=a)(d:=d)(nonzero_a:=nonzero_a). Definition B : E.point. refine ( exist _ (F.of_Z _ 15112221349535400772501151409588531511454012693041857206046113283949847762202, F.div (F.of_Z _ 4) (F.of_Z _ 5)) _).