chore: update comment syntax for Arm/State.lean

leanprover · Aug 1, 2024 · 9e8e198 · 9e8e198
1 parent 1d82625
commit 9e8e198
Show file tree

Hide file tree

Showing 2 changed files with 17 additions and 16 deletions.
diff --git a/Arm/State.lean b/Arm/State.lean
@@ -117,25 +117,28 @@ deriving DecidableEq, Repr
 
 @[ext]
 structure ArmState where
-  -- General-purpose registers: register 31 is the stack pointer.
+  /-- General-purpose registers: register 31 is the stack pointer. -/
   private gpr        : Store (BitVec 5) (BitVec 64)
-  -- SIMD/floating-point registers
+  /-- SIMD/floating-point registers -/
   private sfp        : Store (BitVec 5) (BitVec 128)
-  -- Program Counter
+  /-- Program Counter -/
   private pc         : BitVec 64
-  -- PState
+  /-- PState -/
   private pstate     : PState
-  -- Memory: maps 64-bit addresses to bytes
+  /-- Memory: maps 64-bit addresses to bytes -/
   private mem        : Store (BitVec 64) (BitVec 8)
-  -- Program: maps 64-bit addresses to 32-bit instructions.
-  -- Note that we have the following assumption baked into our machine model:
-  -- the program is always disjoint from the rest of the memory.
-  program    : Program
-
-  -- The error field is an artifact of this model; it is set to a
-  -- non-None value when some irrecoverable error is encountered
-  -- (e.g., an unimplemented instruction is hit). Any reasoning or
-  -- execution based off an erroneous state is invalid.
+  /--
+  Program: maps 64-bit addresses to 32-bit instructions.
+  Note that we have the following assumption baked into our machine model:
+  the program is always disjoint from the rest of the memory.
+  -/
+  program            : Program
+  /--
+  The error field is an artifact of this model; it is set to a
+  non-None value when some irrecoverable error is encountered
+  (e.g., an unimplemented instruction is hit). Any reasoning or
+  execution based off an erroneous state is invalid.
+  -/
   private error      : StateError
 deriving Repr
 

diff --git a/Proofs/Experiments/MemoryAliasing.lean b/Proofs/Experiments/MemoryAliasing.lean
@@ -6,8 +6,6 @@ Author(s): Shilpi Goel, Siddharth Bhat
 The goal is to eliminate the sorry, and to simplify the proof to a tactic invocation.
 -/
 import Arm
--- TODO(@bollu): make this visible from 'Arm'.
-import Arm.State
 import Arm.MemoryProofs
 
 theorem mem_automation_test