Lean: add a simp set for the Sail wrappers

The Lean support library defines wrappers to adapt the API from Sail to
the Lean standard library. This commit adds a simp set `simp_sail` to
simplify them away.

Author: ineol

src/bin/dune

@@ -273,6 +273,9 @@
   (%{workspace_root}/src/gen_lib/sail2_values.lem
    as
    src/gen_lib/sail2_values.lem)
+  (%{workspace_root}/src/sail_lean_backend/Sail/Attr.lean
+   as
+   src/sail_lean_backend/Sail/Attr.lean)
   (%{workspace_root}/src/sail_lean_backend/Sail/Sail.lean
    as
    src/sail_lean_backend/Sail/Sail.lean)

src/sail_lean_backend/Sail/Attr.lean

@@ -0,0 +1,3 @@
+import Lean
+
+register_simp_attr simp_sail

src/sail_lean_backend/Sail/Sail.lean

@@ -1,3 +1,5 @@
+import THE_MODULE_NAME.Sail.Attr
+
 import Std.Data.ExtDHashMap
 import Std.Data.ExtHashMap
 
@@ -7,73 +9,87 @@ namespace BitVec
 
 abbrev length {w : Nat} (_ : BitVec w) : Nat := w
 
+@[simp_sail]
 def signExtend {w : Nat} (x : BitVec w) (w' : Nat) : BitVec w' :=
   x.signExtend w'
 
+@[simp_sail]
 def zeroExtend {w : Nat} (x : BitVec w) (w' : Nat) : BitVec w' :=
   x.zeroExtend w'
 
+@[simp_sail]
 def truncate {w : Nat} (x : BitVec w) (w' : Nat) : BitVec w' :=
   x.truncate w'
 
+@[simp_sail]
 def truncateLsb {w : Nat} (x : BitVec w) (w' : Nat) : BitVec w' :=
   x.extractLsb' (w - w') w'
 
+@[simp_sail]
 def extractLsb {w : Nat} (x : BitVec w) (hi lo : Nat) : BitVec (hi - lo + 1) :=
   x.extractLsb hi lo
 
+@[simp_sail]
 def updateSubrange' {w : Nat} (x : BitVec w) (start len : Nat) (y : BitVec len) : BitVec w :=
   let mask := ~~~(((BitVec.allOnes len).zeroExtend w) <<< start)
   let y' := ((y.zeroExtend w) <<< start)
   (mask &&& x) ||| y'
 
+@[simp_sail]
 def slice {w : Nat} (x : BitVec w) (start len : Nat) : BitVec len :=
   x.extractLsb' start len
 
+@[simp_sail]
 def sliceBE {w : Nat} (x : BitVec w) (start len : Nat) : BitVec len :=
   x.extractLsb' (w - start - len) len
 
+@[simp_sail]
 def subrangeBE {w : Nat} (x : BitVec w) (lo hi : Nat) : BitVec (hi - lo + 1) :=
   x.extractLsb' (w - hi - 1) _
 
+@[simp_sail]
 def updateSubrange {w : Nat} (x : BitVec w) (hi lo : Nat) (y : BitVec (hi - lo + 1)) : BitVec w :=
   updateSubrange' x lo _ y
 
+@[simp_sail]
 def updateSubrangeBE {w : Nat} (x : BitVec w) (lo hi : Nat) (y : BitVec (hi - lo + 1)) : BitVec w :=
   updateSubrange' x (w - hi - 1) _ y
 
+@[simp_sail]
 def replicateBits {w : Nat} (x : BitVec w) (i : Nat) := BitVec.replicate i x
 
+@[simp_sail]
 def access {w : Nat} (x : BitVec w) (i : Nat) : BitVec 1 :=
   BitVec.ofBool x[i]!
 
+@[simp_sail]
 def accessBE {w : Nat} (x : BitVec w) (i : Nat) : BitVec 1 :=
   BitVec.ofBool x[w - i - 1]!
 
+@[simp_sail]
 def addInt {w : Nat} (x : BitVec w) (i : Int) : BitVec w :=
   x + BitVec.ofInt w i
 
+@[simp_sail]
 def subInt (x : BitVec w) (i : Int) : BitVec w :=
   x - BitVec.ofInt w i
 
-def countLeadingZeros (x : BitVec w) : Nat :=
-  if h : w = 0 || BitVec.msb x then
-    0
-  else
-    1 + countLeadingZeros (x.extractLsb' 0 (w - 1))
-  decreasing_by
-    simp only [Bool.or_eq_true, decide_eq_true_eq, not_or, Bool.not_eq_true] at h
-    omega
+@[simp_sail]
+def countLeadingZeros (x : BitVec w) : Nat := x.clz.toNat
 
+@[simp_sail]
 def countTrailingZeros (x : BitVec w) : Nat :=
   countLeadingZeros (x.reverse)
 
+@[simp_sail]
 def append' (x : BitVec n) (y : BitVec m) {mn}
     (hmn : mn = n + m := by (conv => rhs; simp); try rfl) : BitVec mn :=
   (x.append y).cast hmn.symm
 
+@[simp_sail]
 def update (x : BitVec m) (n : Nat) (b : BitVec 1) := updateSubrange' x n _ b
 
+@[simp_sail]
 def updateBE (x : BitVec m) (n : Nat) (b : BitVec 1) := updateSubrange' x (m - n - 1) _ b
 
 def toBin {w : Nat} (x : BitVec w) : String :=
@@ -85,6 +101,7 @@ def toFormatted {w : Nat} (x : BitVec w) : String :=
   else
     s!"0b{BitVec.toBin x}"
 
+@[simp_sail]
 def join1 (xs : List (BitVec 1)) : BitVec xs.length :=
   (BitVec.ofBoolListBE (xs.map fun x => x[0])).cast (by simp)
 
@@ -135,18 +152,23 @@ def valid_dec_bits (_ : Nat) (str : String) : Bool :=
   str.all fun x => x.toLower ∈
     ['0', '1', '2', '3', '4', '5', '6', '7', '8', '9']
 
+@[simp_sail]
 def shift_bits_left (bv : BitVec n) (sh : BitVec m) : BitVec n :=
   bv <<< sh
 
+@[simp_sail]
 def shift_bits_right (bv : BitVec n) (sh : BitVec m) : BitVec n :=
   bv >>> sh
 
+@[simp_sail]
 def shiftl (bv : BitVec n) (m : Nat) : BitVec n :=
   bv <<< m
 
+@[simp_sail]
 def shiftr (bv : BitVec n) (m : Nat) : BitVec n :=
   bv >>> m
 
+@[simp_sail]
 def pow2 := (2 ^ ·)
 
 namespace Nat
@@ -171,11 +193,13 @@ namespace Int
 
 def intAbs (x : Int) : Int := Int.ofNat (Int.natAbs x)
 
+@[simp_sail]
 def shiftl (a : Int) (n : Int) : Int :=
   match n with
   | Int.ofNat n => Sail.Nat.iterate (fun x => x * 2) n a
   | Int.negSucc n => Sail.Nat.iterate (fun x => x / 2) (n+1) a
 
+@[simp_sail]
 def shiftr (a : Int) (n : Int) : Int :=
   match n with
   | Int.ofNat n => Sail.Nat.iterate (fun x => x / 2) n a
@@ -194,12 +218,15 @@ def toHexUpper (i : Int) : String :=
 
 end Int
 
+@[simp_sail]
 def get_slice_int (len : Nat) (n : Int) (lo : Nat) : BitVec len :=
   BitVec.extractLsb' lo len (BitVec.ofInt (lo + len + 1) n)
 
+@[simp_sail]
 def set_slice_int (len : Nat) (n : Int) (lo : Nat) (x : BitVec len) : Int :=
   BitVec.toInt (BitVec.updateSubrange' (BitVec.ofInt len n) lo len x)
 
+@[simp_sail]
 def set_slice {n : Nat} (m : Nat) (bv : BitVec n) (start : Nat) (bv' : BitVec m) : BitVec n :=
   BitVec.updateSubrange' bv start m bv'
 
@@ -208,16 +235,20 @@ def String.leadingSpaces (s : String) : Nat :=
 
 abbrev Vector.length (_v : Vector α n) : Nat := n
 
+@[simp_sail]
 def vectorInit {n : Nat} (a : α) : Vector α n := Vector.replicate n a
 
+@[simp_sail]
 def vectorUpdate (v : Vector α m) (n : Nat) (a : α) := v.set! n a
 
+@[simp_sail]
 instance : HShiftLeft (BitVec w) Int (BitVec w) where
   hShiftLeft b i :=
     match i with
     | .ofNat n => BitVec.shiftLeft b n
     | .negSucc n => BitVec.ushiftRight b (n + 1)
 
+@[simp_sail]
 instance : HShiftRight (BitVec w) Int (BitVec w) where
   hShiftRight b i := b <<< (- i)
 
@@ -391,13 +422,15 @@ export RegisterRef (Reg)
 abbrev PreSailM (RegisterType : Register → Type) (c : ChoiceSource) (ue: Type) :=
   EStateM (Error ue) (SequentialState RegisterType c)
 
+@[simp_sail]
 def sailTryCatch (e : PreSailM RegisterType c ue α) (h : ue → PreSailM RegisterType c ue α) :
     PreSailM RegisterType c ue α :=
   EStateM.tryCatch e fun e =>
     match e with
     | .User u => h u
     | _ => EStateM.throw e
 
+@[simp_sail]
 def sailThrow (e : ue) : PreSailM RegisterType c ue α := EStateM.throw (.User e)
 
 def choose (p : Primitive) : PreSailM RegisterType c ue p.reflect :=
@@ -436,54 +469,66 @@ def internal_pick {α : Type} : List α → PreSailM RegisterType c ue α
     let idx ← choose <| .fin (as.length)
     pure <| (a :: as).get idx
 
+@[simp_sail]
 def writeReg (r : Register) (v : RegisterType r) : PreSailM RegisterType c ue PUnit :=
   modify fun s => { s with regs := s.regs.insert r v }
 
+@[simp_sail]
 def readReg (r : Register) : PreSailM RegisterType c ue (RegisterType r) := do
   let .some s := (← get).regs.get? r
     | throw .Unreachable
   pure s
 
+@[simp_sail]
 def readRegRef (reg_ref : @RegisterRef Register RegisterType α) : PreSailM RegisterType c ue α := do
   match reg_ref with | .Reg r => readReg r
 
+@[simp_sail]
 def writeRegRef (reg_ref : @RegisterRef Register RegisterType α) (a : α) :
   PreSailM RegisterType c ue Unit := do
   match reg_ref with | .Reg r => writeReg r a
 
+@[simp_sail]
 def reg_deref (reg_ref : @RegisterRef Register RegisterType α) : PreSailM RegisterType c ue α :=
   readRegRef reg_ref
 
+@[simp_sail]
 def assert (p : Bool) (s : String) : PreSailM RegisterType c ue Unit :=
   if p then pure () else throw (.Assertion s)
 
 section ConcurrencyInterface
 
+@[simp_sail]
 def writeByte (addr : Nat) (value : BitVec 8) : PreSailM RegisterType c ue PUnit := do
   modify fun s => { s with mem := s.mem.insert addr value }
 
+@[simp_sail]
 def writeBytes (addr : Nat) (value : BitVec (8 * n)) : PreSailM RegisterType c ue Bool := do
   let list := List.ofFn (λ i : Fin n => (addr + i.val, value.extractLsb' (8 * i.val) 8))
   List.forM list (λ (a, v) => writeByte a v)
   pure true
 
+@[simp_sail]
 def sail_mem_write [Arch] (req : Mem_write_request n vasize (BitVec pa_size) ts arch) : PreSailM RegisterType c ue (Result (Option Bool) Arch.abort) := do
   let addr := req.pa.toNat
   let b ← match req.value with
     | some v => writeBytes addr v
     | none => pure true
   pure (Ok (some b))
 
+@[simp_sail]
 def write_ram (addr_size data_size : Nat) (_hex_ram addr : BitVec addr_size) (value : BitVec (8 * data_size)) :
     PreSailM RegisterType c ue Unit := do
   let _ ← writeBytes addr.toNat value
   pure ()
 
+@[simp_sail]
 def readByte (addr : Nat) : PreSailM RegisterType c ue (BitVec 8) := do
   let .some s := (← get).mem.get? addr
     | throw (.OutOfMemoryRange addr)
   pure s
 
+@[simp_sail]
 def readBytes (size : Nat) (addr : Nat) : PreSailM RegisterType c ue ((BitVec (8 * size)) × Option Bool) :=
   match size with
   | 0 => pure (default, none)
@@ -497,26 +542,37 @@ def readBytes (size : Nat) (addr : Nat) : PreSailM RegisterType c ue ((BitVec (8
     have h : 8 * n + 8 = 8 * (n + 1) := by omega
     return (h ▸ bytes.append b, bool)
 
+@[simp_sail]
 def sail_mem_read [Arch] (req : Mem_read_request n vasize (BitVec pa_size) ts arch) : PreSailM RegisterType c ue (Result ((BitVec (8 * n)) × (Option Bool)) Arch.abort) := do
   let addr := req.pa.toNat
   let value ← readBytes n addr
   pure (Ok value)
 
+@[simp_sail]
 def read_ram (addr_size data_size : Nat) (_hex_ram addr : BitVec addr_size) : PreSailM RegisterType c ue (BitVec (8 * data_size)) := do
   let ⟨bytes, _⟩ ← readBytes data_size addr.toNat
   pure bytes
 
+@[simp_sail]
 def sail_barrier (_ : α) : PreSailM RegisterType c ue Unit := pure ()
+@[simp_sail]
 def sail_cache_op [Arch] (_ : Arch.cache_op) : PreSailM RegisterType c ue Unit := pure ()
+@[simp_sail]
 def sail_tlbi [Arch] (_ : Arch.tlb_op) : PreSailM RegisterType c ue Unit := pure ()
+@[simp_sail]
 def sail_translation_start [Arch] (_ : Arch.trans_start) : PreSailM RegisterType c ue Unit := pure ()
+@[simp_sail]
 def sail_translation_end [Arch] (_ : Arch.trans_end) : PreSailM RegisterType c ue Unit := pure ()
+@[simp_sail]
 def sail_take_exception [Arch] (_ : Arch.fault) : PreSailM RegisterType c ue Unit := pure ()
+@[simp_sail]
 def sail_return_exception [Arch] (_ : Arch.pa) : PreSailM RegisterType c ue Unit := pure ()
 
+@[simp_sail]
 def cycle_count (_ : Unit) : PreSailM RegisterType c ue Unit :=
   modify fun s => { s with cycleCount := s.cycleCount + 1 }
 
+@[simp_sail]
 def get_cycle_count (_ : Unit) : PreSailM RegisterType c ue Nat := do
   pure (← get).cycleCount
 
@@ -534,6 +590,7 @@ def print_bits_effect {w : Nat} (str : String) (x : BitVec w) : PreSailM Registe
 def print_endline_effect (str : String) : PreSailM RegisterType c ue Unit :=
   print_effect s!"{str}\n"
 
+@[simp_sail]
 def sailTryCatchE (e : ExceptT β (PreSailM RegisterType c ue) α) (h : ue → ExceptT β (PreSailM RegisterType c ue) α) : ExceptT β (PreSailM RegisterType c ue) α :=
   EStateM.tryCatch e fun e =>
     match e with

src/sail_lean_backend/Sail/Specialization.lean

@@ -3,8 +3,10 @@ import THE_MODULE_NAME.Defs
 
 namespace Sail
 
+@[simp_sail]
 def sailTryCatch (e : SailM α) (h : exception → SailM α) : SailM α := PreSail.sailTryCatch e h
 
+@[simp_sail]
 def sailThrow (e : exception) : SailM α := PreSail.sailThrow e
 
 abbrev undefined_unit (_ : Unit) : SailM Unit := PreSail.undefined_unit ()

src/sail_lean_backend/sail_plugin_lean.ml

@@ -247,8 +247,14 @@ open Sail
 
 let path_to_static_library sail_dir str = Filename.quote (sail_dir ^ "/src/sail_lean_backend/Sail/" ^ str ^ ".lean")
 
-let copy_from_static_library sail_dir lean_sail_dir str =
-  Unix.system ("cp " ^ path_to_static_library sail_dir str ^ " " ^ Filename.quote lean_sail_dir)
+let copy_from_static_library out_name_camel sail_dir lean_sail_dir str =
+  Unix.system
+    (Printf.sprintf "sed 's/THE_MODULE_NAME/%s/g' %s > %s.lean" out_name_camel (path_to_static_library sail_dir str)
+       (lean_sail_dir ^ "/" ^ str |> Filename.quote)
+    )
+  |> ignore
+
+(* Unix.system ("cp " ^ path_to_static_library sail_dir str ^ " " ^ Filename.quote lean_sail_dir) *)
 
 let print_function_file_prelude file out_name_camel (imp_refs : string list) =
   let _ =
@@ -292,9 +298,10 @@ let start_lean_output (out_name : string) (import_names : string list) (import_r
   if not (Sys.file_exists lean_src_dir) then Unix.mkdir lean_src_dir 0o775;
   let lean_sail_dir = lean_src_dir ^ "/Sail/" in
   Unix.mkdir lean_sail_dir 0o775;
-  let _ = copy_from_static_library sail_dir lean_sail_dir "BitVec" in
-  let _ = copy_from_static_library sail_dir lean_sail_dir "IntRange" in
-  let _ = copy_from_static_library sail_dir lean_sail_dir "Sail" in
+  let _ = copy_from_static_library out_name_camel sail_dir lean_sail_dir "Attr" in
+  let _ = copy_from_static_library out_name_camel sail_dir lean_sail_dir "BitVec" in
+  let _ = copy_from_static_library out_name_camel sail_dir lean_sail_dir "IntRange" in
+  let _ = copy_from_static_library out_name_camel sail_dir lean_sail_dir "Sail" in
   let real_numbers_file =
     if !opt_lean_real_numbers then "/src/sail_lean_backend/Sail/Real.lean"
     else "/src/sail_lean_backend/Sail/FakeReal.lean"