whitespace, etc

src/riscv/Platform/Minimal.v

@@ -46,7 +46,7 @@ Section Riscv.
     m <- fail_if_None (Memory.store_bytes n mach.(getMem) a v);
     update (fun mach =>
               withXAddrs (invalidateWrittenXAddrs n a mach.(getXAddrs)) (withMem m mach)).
-  
+
   Instance IsRiscvMachine: RiscvProgram (OState RiscvMachine) word :=  {
       getRegister reg :=
         if Z.eq_dec reg Register0 then
@@ -99,7 +99,7 @@ Section Riscv.
       (* fail hard if exception is thrown because at the moment, we want to prove that
          code output by the compiler never throws exceptions *)
       endCycleEarly{A: Type} := fail_hard;
-    }. Print leakEvent. Print withLeakageEvent. Print RiscvMachine.
+  }.
 
   Instance IsRiscvMachineWithLeakage: @RiscvProgramWithLeakage _ _ _ (OState RiscvMachine) _ _ _ :=  {
       RVP := IsRiscvMachine;

src/riscv/Platform/MinimalMMIO.v

@@ -209,7 +209,7 @@ Section Riscv.
         ssplit; eauto; simpl;
         change removeXAddr with (@List.removeb word word.eqb);
         rewrite ?ListSet.of_list_removeb;
-      intuition eauto 10 using preserve_undef_on, disjoint_diff_l.
+        intuition eauto 10 using preserve_undef_on, disjoint_diff_l.
   Qed.
 
   Lemma interpret_action_total'{memOk: map.ok Mem} a s post :

src/riscv/Platform/MinimalMMIO_Post.v

@@ -3,6 +3,7 @@ Require Import Coq.ZArith.ZArith.
 Require Import riscv.Utility.Monads.
 Require Import riscv.Utility.MonadNotations.
 Require Import riscv.Spec.Decode.
+Require Import riscv.Spec.LeakageOfInstr.
 Require Import riscv.Spec.Machine.
 Require Import riscv.Utility.Utility.
 Require Import riscv.Spec.Primitives.
@@ -117,7 +118,10 @@ Section Riscv.
 
   Instance IsRiscvMachineWithLeakage: @RiscvProgramWithLeakage _ _ _ (Post RiscvMachine) _ _ _ := {|
       RVP := IsRiscvMachine;
-      leakEvent _ := fun _ _ => False;
+      leakEvent e := fun mach post => match e with
+                                      | Some e => post tt (withLeakageEvent e mach)
+                                      | None => forall X (x : X), post tt (withLeakageEvent (anything x) mach)
+                                      end;
   |}.
 
   Definition MinimalMMIOPrimitivesParams: PrimitivesParams (Post RiscvMachine) RiscvMachine := {|

src/riscv/Platform/RiscvMachine.v

@@ -175,15 +175,15 @@ Section Machine.
 
     Definition withLogItems: list LogItem -> RiscvMachine -> RiscvMachine :=
       fun items '(mkRiscvMachine regs pc nextPC mem xAddrs log trace) =>
-                 mkRiscvMachine regs pc nextPC mem xAddrs (items ++ log) trace.
+                  mkRiscvMachine regs pc nextPC mem xAddrs (items ++ log) trace.
 
     Definition withLeakageEvent: LeakageEvent -> RiscvMachine -> RiscvMachine :=
       fun event '(mkRiscvMachine regs pc nextPC mem xAddrs log trace) =>
-                 mkRiscvMachine regs pc nextPC mem xAddrs log (event :: trace).
+                  mkRiscvMachine regs pc nextPC mem xAddrs log (event :: trace).
 
     Definition withLeakageEvents: list LeakageEvent -> RiscvMachine -> RiscvMachine :=
       fun events '(mkRiscvMachine regs pc nextPC mem xAddrs log trace) =>
-                 mkRiscvMachine regs pc nextPC mem xAddrs log (events ++ trace).
+                   mkRiscvMachine regs pc nextPC mem xAddrs log (events ++ trace).
 
     Definition Z32s_to_bytes(l: list Z): list byte :=
       List.flat_map (fun z => HList.tuple.to_list (LittleEndian.split 4 z)) l.

src/riscv/Spec/Machine.v

@@ -67,9 +67,7 @@ Class RiscvProgram{M}{t}`{Monad M}`{MachineWidth t} := mkRiscvProgram {
   endCycleEarly: forall A, M A;
 }.
 
-Class RiscvProgramWithLeakage
-  {width} {BW : Bitwidth width} {word: word.word width}
-  {M}{t}{MM}{MWt}:=
+Class RiscvProgramWithLeakage{width}{BW : Bitwidth width}{word: word.word width}{M}{t}{MM}{MWt} :=
   mkRiscvProgramWithLeakage {
       RVP :> @RiscvProgram M t MM MWt;
       leakEvent : (option LeakageEvent) -> M unit;