whitespace, etc

mit-plv · Aug 5, 2024 · 4f49507 · 4f49507
1 parent 92a3acb
commit 4f49507
Show file tree

Hide file tree

Showing 4 changed files with 7 additions and 9 deletions.
diff --git a/src/riscv/Platform/Minimal.v b/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;

diff --git a/src/riscv/Platform/MinimalMMIO.v b/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 :

diff --git a/src/riscv/Platform/RiscvMachine.v b/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.

diff --git a/src/riscv/Spec/Machine.v b/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;