paperify spec

[andres-erbsen]

Definition protocol_step : state -> list _ -> state -> Prop. Admitted.
Definition protocol_spec t := exists s s', labeled_transitions protocol_step s s' t.
Definition io_spec : list LogItem -> Prop := only_mmio_satisfying (boot_seq +++ protocol_spec).

Definition initial_conditions mach := 0x20400000 = mach.(getPc) /\ [] = mach.(getLog) /\ ... .
Theorem garagedoor_correct : forall mach : RiscvMachine, initial_conditions mach ->
  always run1 (eventually run1 (fun mach' => io_spec mach'.(getLog))) mach.