paperify spec

src/Bedrock/End2End/X25519/GarageDoor.v

@@ -172,10 +172,16 @@ 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) =>
+Local Notation MMIO := (string * word.rep * word.rep)%type.
+Goal True.
+  pose (lightbulb_spec.lan9250_writepacket Naive.word32 :
+   list Init.Byte.byte -> list MMIO -> Prop).
+Abort.
+
+Definition protocol_step : state -> list MMIO -> 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 +238,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 +250,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 +266,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,24 +165,72 @@ 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_spec l := exists s s', labeled_transitions protocol_step s s' l.
+Definition io_spec : list LogItem -> Prop := only_mmio_satisfying (boot_seq +++ protocol_spec).
 
 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 := io_spec;
+  isReady t m := exists s s', only_mmio_satisfying (boot_seq +++ labeled_transitions protocol_step s' s) t /\ exists bs R, memrep bs R s m |}.
+
+Import DestructHead.
+Lemma only_mmio_satisfying_app P Q t :
+  only_mmio_satisfying (P +++ Q) t <->
+  (only_mmio_satisfying P +++ only_mmio_satisfying Q) t.
+Proof.
+  cbv [only_mmio_satisfying mmio_trace_abstraction_relation]; split; intros;
+    repeat (destruct_head' @ex; destruct_head' @Logic.and; destruct_head' @concat);
+    subst; eauto using Forall2_app, concat_app.
+  eapply Forall2_app_inv_l in H; case H as (?&?&?&?&?); subst.
+  eapply concat_app; eauto.
+Qed.
+Lemma only_mmio_satisfying_ex [A] P t :
+  only_mmio_satisfying (fun t => exists x : A, P x t) t <->
+  exists x : A, only_mmio_satisfying (P x) t.
+Proof.
+  cbv [only_mmio_satisfying mmio_trace_abstraction_relation]; split; intros;
+    repeat (destruct_head' @ex; destruct_head' @Logic.and);
+    eauto using Forall2_app.
+Qed.
+Import Coq.Classes.Morphisms.
+Global Instance Proper_only_mmio_satisfying : 
+  Proper (Morphisms.pointwise_relation _ iff ==> Morphisms.pointwise_relation _ iff) only_mmio_satisfying.
+Proof.
+  cbv [only_mmio_satisfying mmio_trace_abstraction_relation].
+  split; intros (?&?&?); eexists; split; eauto; eapply H; eauto.
+Qed.
+Lemma concat_ex_r A B P Q (t : list A) :
+  Morphisms.pointwise_relation (list A) iff
+  (P +++ (fun t => exists x : B, Q x t)) (fun t => exists x : B, (P +++ Q x) t).
+Proof.
+  repeat intro;
+  unfold "+++"; split; intros;
+    repeat (destruct_head' @ex; destruct_head' @Logic.and; destruct_head' @concat);
+    subst; eauto 6.
+Qed.
 
-Lemma good_trace_from_isRead a a0 : isReady garagedoor_spec a a0 ->
+Lemma good_trace_from_isReady 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.
-  case H as (?&?&?&?&?&H); eauto.
+  cbv [isReady goodTrace garagedoor_spec io_spec protocol_spec]; intuition eauto;
+    repeat (destruct_head' @ex; destruct_head' @Logic.and).
+  eapply Proper_only_mmio_satisfying.
+  { intros ?. eapply concat_ex_r; eauto. }
+  eapply only_mmio_satisfying_ex; eexists.
+  eapply Proper_only_mmio_satisfying.
+  { intros ?. eapply concat_ex_r; eauto. }
+  eapply only_mmio_satisfying_ex; eexists.
+  eauto.
 Qed.
 
 Lemma link_initfn : spec_of_initfn (map.of_list funcs).
@@ -210,14 +258,19 @@ Import bedrock2.Map.Separation. Local Open Scope sep_scope.
 Require Import bedrock2.ReversedListNotations.
 Local Notation run1 := (mcomp_sat (run1 Decode.RV32IM)).
 Local Notation RiscvMachine := MetricRiscvMachine.
+Goal True.
+  pose (run1 : RiscvMachine -> (RiscvMachine -> Prop) -> Prop).
+  pose (always(iset:=Decode.RV32IM) : (RiscvMachine -> Prop) -> RiscvMachine -> Prop).
+Abort.
+
 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 +286,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 *.
@@ -259,14 +313,15 @@ Proof.
         Morphisms.f_equiv. }
       { rewrite firstn_length, skipn_length. Lia.lia. }
       { Lia.lia. } }
-    intros ? m ? ?; repeat straightline; eapply good_trace_from_isRead.
+    intros ? m ? ?; repeat straightline; eapply good_trace_from_isReady.
     subst a; rewrite app_nil_r.
     lazymatch goal with H: sep _ _ m |- _ => rename H into M end.
     rewrite <-(List.firstn_skipn 0x20 (List.firstn _ anybytes)) in M.
     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 io_spec 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 +332,22 @@ 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 io_spec 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.
+    intros ? ? ? ?; repeat straightline; eapply good_trace_from_isReady.
     eexists; fwd; try eassumption.
-    cbv [good_trace good_transitions] in *; repeat straightline.
+    cbv [only_mmio_satisfying protocol_spec io_spec] in *; repeat straightline.
+    try move H6 at bottom.
     { 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, io_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 +361,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 : RiscvMachine, initial_conditions mach ->
+  always run1 (eventually run1 (fun mach' => io_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. }