Lean: Memory model

lib/concurrency_interface/common.sail

@@ -48,7 +48,7 @@ $sail_internal
 
 $target_set emulator_or_isla isla c ocaml interpreter systemverilog
 $target_set emulator c ocaml interpreter systemverilog
-$target_set prover lem coq
+$target_set prover lem coq lean
 
 $ifndef _CONCURRENCY_INTERFACE_COMMON
 $define _CONCURRENCY_INTERFACE_COMMON

lib/concurrency_interface/read_write.sail

@@ -53,6 +53,7 @@ $include <concurrency_interface/common.sail>
 
 $option -lem_extern_type Access_variety
 $option -coq_extern_type Access_variety
+$option -lean_extern_type Access_variety
 enum Access_variety = {
   AV_plain,
   AV_exclusive,
@@ -61,6 +62,7 @@ enum Access_variety = {
 
 $option -lem_extern_type Access_strength
 $option -coq_extern_type Access_strength
+$option -lean_extern_type Access_strength
 enum Access_strength = {
   AS_normal,
   AS_rel_or_acq, // Release or acquire
@@ -69,13 +71,15 @@ enum Access_strength = {
 
 $option -lem_extern_type Explicit_access_kind
 $option -coq_extern_type Explicit_access_kind
+$option -lean_extern_type Explicit_access_kind
 struct Explicit_access_kind = {
   variety : Access_variety,
   strength : Access_strength
 }
 
 $option -lem_extern_type Access_kind
 $option -coq_extern_type Access_kind
+$option -lean_extern_type Access_kind
 union Access_kind('arch_ak : Type) = {
   AK_explicit: Explicit_access_kind,
   AK_ifetch : unit, // Instruction fetch
@@ -85,6 +89,7 @@ union Access_kind('arch_ak : Type) = {
 
 $option -lem_extern_type Mem_read_request
 $option -coq_extern_type Mem_read_request
+$option -lean_extern_type Mem_read_request
 struct Mem_read_request('n : Int, 'vasize : Int, 'pa : Type, 'ts : Type,
                         'arch_ak : Type), 'n > 0 & 'vasize >= 0 = {
   access_kind : Access_kind('arch_ak),
@@ -181,6 +186,7 @@ with
 
 $option -lem_extern_type Mem_write_request
 $option -coq_extern_type Mem_write_request
+$option -lean_extern_type Mem_write_request
 struct Mem_write_request('n : Int, 'vasize : Int, 'pa : Type, 'ts : Type,
                          'arch_ak : Type), 'n > 0 & 'vasize >= 0 = {
   access_kind : Access_kind('arch_ak),

lib/result.sail

@@ -56,6 +56,7 @@ $include <option.sail>
 
 $option -lem_extern_type result
 $option -coq_extern_type result
+$option -lean_extern_type result
 union result('a : Type, 'b : Type) = {
     Ok : 'a,
     Err : 'b

src/sail_lean_backend/Sail/Sail.lean

@@ -1,4 +1,5 @@
 import Std.Data.DHashMap
+import Std.Data.HashMap
 namespace Sail
 
 section Regs
@@ -41,17 +42,30 @@ def trivialChoiceSource : ChoiceSource where
     | .fin _ => 0
     | .bitvector _ => 0
 
+class Arch where
+  va_size : Nat
+  pa : Type
+  arch_ak : Type
+  translation : Type
+  abort : Type
+  barrier : Type
+  cache_op : Type
+  tlb_op : Type
+  fault : Type
+  sys_reg_id : Type
+
 /- The Units are placeholders for a future implementation of the state monad some Sail functions use. -/
 inductive Error where
   | Exit
   | Unreachable
+  | UninitializedMemory
   | Assertion (s : String)
 open Error
 
 structure SequentialState (RegisterType : Register → Type) (c : ChoiceSource) where
   regs : Std.DHashMap Register RegisterType
   choiceState : c.α
-  mem : Unit
+  mem : Std.HashMap Nat (BitVec 8)
   tags : Unit
 
 inductive RegisterRef (RegisterType : Register → Type) : Type → Type where
@@ -113,6 +127,94 @@ def vectorUpdate (v : Vector α m) (n : Nat) (a : α) := v.set! n a
 def assert (p : Bool) (s : String) : PreSailM RegisterType c Unit :=
   if p then pure () else throw (Assertion s)
 
+section concurrency_interface
+
+inductive Access_variety where
+| AV_plain
+| AV_exclusive
+| AV_atomic_rmw
+export Access_variety (AV_plain AV_exclusive AV_atomic_rmw)
+
+inductive Access_strength where
+| AS_normal
+| AS_rel_or_acq
+| AS_acq_rcpc
+export Access_strength(AS_normal AS_rel_or_acq AS_acq_rcpc)
+
+structure Explicit_access_kind where
+  variety : Access_variety
+  strength : Access_strength
+
+inductive Access_kind (arch : Type) where
+  | AK_explicit (_ : Explicit_access_kind)
+  | AK_ifetch (_ : Unit)
+  | AK_ttw (_ : Unit)
+  | AK_arch (_ : arch)
+export Access_kind(AK_explicit AK_ifetch AK_ttw AK_arch)
+
+inductive Result (α : Type) (β : Type) where
+  | Ok (_ : α)
+  | Err (_ : β)
+export Result(Ok Err)
+
+structure Mem_read_request
+  (n : Nat) (vasize : Nat) (pa : Type) (ts : Type) (arch_ak : Type) where
+  access_kind : Access_kind arch_ak
+  va : (Option (BitVec vasize))
+  pa : pa
+  translation : ts
+  size : Int
+  tag : Bool
+
+structure Mem_write_request
+  (n : Nat) (vasize : Nat) (pa : Type) (ts : Type) (arch_ak : Type) where
+  access_kind : Access_kind arch_ak
+  va : (Option (BitVec vasize))
+  pa : pa
+  translation : ts
+  size : Int
+  value : (Option (BitVec (8 * n)))
+  tag : (Option Bool)
+
+def write_byte (addr : Nat) (value : BitVec 8) : PreSailM RegisterType c PUnit := do
+  modify fun s => { s with mem := s.mem.insert addr value }
+  pure ()
+
+def write_bytes (addr : Nat) (value : BitVec (8 * n)) : PreSailM RegisterType c Bool := do
+  let list := List.ofFn (λ i : Fin n => (addr + i, value.extractLsb' (8 * i) 8))
+  List.forM list (λ (a, v) => write_byte a v)
+  pure true
+
+def sail_mem_write [Arch] (req : Mem_write_request n vasize (BitVec pa_size) ts arch) : PreSailM RegisterType c (Result (Option Bool) Arch.abort) := do
+  let addr := req.pa.toNat
+  let b ← match req.value with
+    | some v => write_bytes addr v
+    | none => pure true
+  pure (Ok (some b))
+
+def read_byte (addr : Nat) : PreSailM RegisterType c (BitVec 8) := do
+  let .some s := (← get).mem.get? addr
+    | throw UninitializedMemory
+  pure s
+
+def read_bytes (size : Nat) (addr : Nat) : PreSailM RegisterType c ((BitVec (8 * size)) × (Option Bool)) :=
+  match size with
+  | 0 => pure (default, some true)
+  | n + 1 => do
+      let b ← read_byte addr
+      let (bytes, bool) ← read_bytes n (addr+1)
+      have h : 8 + 8 * n = 8 * (n + 1) := by omega
+      return (h ▸ b.append bytes, bool)
+
+def sail_mem_read [Arch] (req : Mem_read_request n vasize (BitVec pa_size) ts arch) : PreSailM RegisterType c (Result ((BitVec (8 * n)) × (Option Bool)) Arch.abort) := do
+  let addr := req.pa.toNat
+  let value ← read_bytes n addr
+  pure (Ok value)
+
+def sail_barrier (_ : α) : PreSailM RegisterType c Unit := pure ()
+
+end concurrency_interface
+
 end Regs
 
 namespace BitVec

src/sail_lean_backend/pretty_print_lean.ml

@@ -9,6 +9,9 @@ open Rewriter
 open PPrint
 open Pretty_print_common
 
+(* Command line options *)
+let opt_extern_types : string list ref = ref []
+
 type global_context = { effect_info : Effects.side_effect_info }
 
 type context = {
@@ -495,7 +498,7 @@ and doc_exp (as_monadic : bool) ctx (E_aux (e, (l, annot)) as full_exp) =
         (braces (space ^^ doc_exp false ctx exp ^^ string " with " ^^ separate (comma ^^ space) args ^^ space))
   | E_match (discr, brs) ->
       let cases = separate_map hardline (fun br -> doc_match_clause as_monadic ctx br) brs in
-      string "match " ^^ doc_exp (effectful (effect_of discr)) ctx discr ^^ string " with" ^^ hardline ^^ cases
+      string "match " ^^ doc_exp false ctx discr ^^ string " with" ^^ hardline ^^ cases
   | E_assign ((LE_aux (le_act, tannot) as le), e) -> (
       match le_act with
       | LE_id id | LE_typ (_, id) -> string "writeReg " ^^ doc_id_ctor id ^^ space ^^ doc_exp false ctx e
@@ -672,6 +675,8 @@ let rec doc_defs_rec ctx defs types docdefs =
   | [] -> (types, docdefs)
   | DEF_aux (DEF_fundef fdef, _) :: defs' ->
       doc_defs_rec ctx defs' types (docdefs ^^ group (doc_fundef ctx fdef) ^/^ hardline)
+  | DEF_aux (DEF_type tdef, _) :: defs' when List.mem (string_of_id (id_of_type_def tdef)) !opt_extern_types ->
+      doc_defs_rec ctx defs' types docdefs
   | DEF_aux (DEF_type tdef, _) :: defs' ->
       doc_defs_rec ctx defs' (types ^^ group (doc_typdef ctx tdef) ^/^ hardline) docdefs
   | DEF_aux (DEF_let (LB_aux (LB_val (pat, exp), _)), _) :: defs' ->
@@ -734,13 +739,38 @@ let doc_monad_abbrev (has_registers : bool) =
   in
   separate space [string "abbrev"; string "SailM"; coloneq; pp_register_type] ^^ hardline ^^ hardline
 
+let doc_instantiations ctx env =
+  let params = Monad_params.find_monad_parameters env in
+  match params with
+  | None -> empty
+  | Some params ->
+      nest 2
+        (separate hardline
+           [
+             string "instance : Arch where";
+             string "va_size := 64";
+             string "pa := " ^^ doc_typ ctx params.pa_type;
+             string "abort := " ^^ doc_typ ctx params.abort_type;
+             string "translation := " ^^ doc_typ ctx params.translation_summary_type;
+             string "fault := " ^^ doc_typ ctx params.fault_type;
+             string "tlb_op := " ^^ doc_typ ctx params.tlbi_type;
+             string "cache_op := " ^^ doc_typ ctx params.cache_op_type;
+             string "barrier := " ^^ doc_typ ctx params.barrier_type;
+             string "arch_ak := " ^^ doc_typ ctx params.arch_ak_type;
+             string "sys_reg_id := " ^^ doc_typ ctx params.sys_reg_id_type ^^ hardline;
+           ]
+        )
+      ^^ hardline
+
 let pp_ast_lean (env : Type_check.env) effect_info ({ defs; _ } as ast : Libsail.Type_check.typed_ast) o =
   let defs = remove_imports defs 0 in
   let regs = State.find_registers defs in
   let global = { effect_info } in
+  let ctx = initial_context env global in
   let has_registers = List.length regs > 0 in
   let register_refs = if has_registers then doc_reg_info env global regs else empty in
   let monad = doc_monad_abbrev has_registers in
-  let types, fundefs = doc_defs (initial_context env global) defs in
-  print o (types ^^ register_refs ^^ monad ^^ fundefs);
+  let instantiations = doc_instantiations ctx env in
+  let types, fundefs = doc_defs ctx defs in
+  print o (types ^^ register_refs ^^ monad ^^ instantiations ^^ fundefs);
   ()

src/sail_lean_backend/sail_plugin_lean.ml

@@ -85,6 +85,10 @@ let lean_options =
       Arg.Unit (fun () -> opt_lean_force_output := true),
       "removes the content of the output directory if it is non-empty"
     );
+    ( Flag.create ~prefix:["lean"] ~arg:"typename" "extern_type",
+      Arg.String Pretty_print_lean.(fun ty -> opt_extern_types := ty :: !opt_extern_types),
+      "do not generate a definition for the type"
+    );
   ]
 
 (* TODO[javra]: Currently these are the same as the Coq rewrites, we might want to change them. *)