paperify spec

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.

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.

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,14 +239,15 @@ 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.
   1: instantiate (1:=snd init).
   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,21 +285,21 @@ 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.
 
 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. }

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)) _).