From 4db4b9619318970a0228954f64a61123c4961910 Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Tue, 9 Oct 2018 21:47:31 +0100
Subject: Monad refactoring in Lem shallow embedding

- Merge tag reading/writing outcomes into memory value reading/writing outcomes
- Add effective address to Write_mem; this duplicates information in the
  Write_ea outcome that should come before, but it makes the effective address
  more conveniently available in events and traces, and it allows the following
  simplification in the state monad:
- Remove write_ea field from state record; the effective address is now
  expected as a parameter to the write_memS function
- Remove last_exclusive_operation_was_load field from state record; this was
  used to keep track of exclusive loads, but this was a a relatively coarse
  approximation anyway, so it might make more sense to track this in
  (architecture-specific) Sail code.  Overall, the state record now simply
  contains the fields regstate, memstate, tagstate.
---
 src/gen_lib/sail2_prompt_monad.lem  | 110 +++++++++++++++++++-----------------
 src/gen_lib/sail2_state_lifting.lem |  28 +++++----
 src/gen_lib/sail2_state_monad.lem   |  93 +++++++++++++-----------------
 3 files changed, 110 insertions(+), 121 deletions(-)

diff --git a/src/gen_lib/sail2_prompt_monad.lem b/src/gen_lib/sail2_prompt_monad.lem
index 78b1615e..991d3895 100644
--- a/src/gen_lib/sail2_prompt_monad.lem
+++ b/src/gen_lib/sail2_prompt_monad.lem
@@ -8,19 +8,17 @@ type address = list bitU
 
 type monad 'regval 'a 'e =
   | Done of 'a
-  (* Read a number of bytes from memory, returned in little endian order *)
-  | Read_mem of read_kind * address * nat * (list memory_byte -> monad 'regval 'a 'e)
-  (* Read the tag of a memory address *)
-  | Read_tag of address * (bitU -> monad 'regval 'a 'e)
-  (* Tell the system a write is imminent, at address lifted, of size nat *)
+  (* Read a number of bytes from memory, returned in little endian order,
+     together with a tag. *)
+  | Read_mem of read_kind * address * nat * ((list memory_byte * bitU) -> monad 'regval 'a 'e)
+  (* Tell the system a write is imminent, at the given address and with the
+     given size. *)
   | Write_ea of write_kind * address * nat * monad 'regval 'a 'e
   (* Request the result of store-exclusive *)
   | Excl_res of (bool -> monad 'regval 'a 'e)
-  (* Request to write memory at last signalled address. Memory value should be 8
-     times the size given in ea signal, given in little endian order *)
-  | Write_memv of list memory_byte * (bool -> monad 'regval 'a 'e)
-  (* Request to write the tag at given address. *)
-  | Write_tag of address * bitU * (bool -> monad 'regval 'a 'e)
+  (* Request to write a memory value of the given size together with a tag
+     at the given address. *)
+  | Write_mem of write_kind * address * nat * list memory_byte * bitU * (bool -> monad 'regval 'a 'e)
   (* Tell the system to dynamically recalculate dependency footprint *)
   | Footprint of monad 'regval 'a 'e
   (* Request a memory barrier *)
@@ -38,26 +36,36 @@ type monad 'regval 'a 'e =
   (* Exception of type 'e *)
   | Exception of 'e
 
+type event 'regval =
+  | E_read_mem of read_kind * address * nat * (list memory_byte * bitU)
+  | E_write_mem of write_kind * address * nat * list memory_byte * bitU * bool
+  | E_write_ea of write_kind * address * nat
+  | E_excl_res of bool
+  | E_barrier of barrier_kind
+  | E_footprint
+  | E_read_reg of register_name * 'regval
+  | E_write_reg of register_name * 'regval
+  | E_undefined of bool
+  | E_print of string
+
 val return : forall 'rv 'a 'e. 'a -> monad 'rv 'a 'e
 let return a = Done a
 
 val bind : forall 'rv 'a 'b 'e. monad 'rv 'a 'e -> ('a -> monad 'rv 'b 'e) -> monad 'rv 'b 'e
 let rec bind m f = match m with
   | Done a -> f a
-  | Read_mem rk a sz k -> Read_mem rk a sz (fun v -> bind (k v) f)
-  | Read_tag a k ->       Read_tag a       (fun v -> bind (k v) f)
-  | Write_memv descr k -> Write_memv descr (fun v -> bind (k v) f)
-  | Write_tag a t k ->    Write_tag a t    (fun v -> bind (k v) f)
-  | Read_reg descr k ->   Read_reg descr   (fun v -> bind (k v) f)
-  | Excl_res k ->         Excl_res         (fun v -> bind (k v) f)
-  | Undefined k ->        Undefined        (fun v -> bind (k v) f)
-  | Write_ea wk a sz k -> Write_ea wk a sz (bind k f)
-  | Footprint k ->        Footprint        (bind k f)
-  | Barrier bk k ->       Barrier bk       (bind k f)
-  | Write_reg r v k ->    Write_reg r v    (bind k f)
-  | Print msg k ->        Print msg        (bind k f)
-  | Fail descr ->         Fail descr
-  | Exception e ->        Exception e
+  | Read_mem rk a sz k ->      Read_mem rk a sz      (fun v -> bind (k v) f)
+  | Write_mem wk a sz v t k -> Write_mem wk a sz v t (fun v -> bind (k v) f)
+  | Read_reg descr k ->        Read_reg descr        (fun v -> bind (k v) f)
+  | Excl_res k ->              Excl_res              (fun v -> bind (k v) f)
+  | Undefined k ->             Undefined             (fun v -> bind (k v) f)
+  | Write_ea wk a sz k ->      Write_ea wk a sz      (bind k f)
+  | Footprint k ->             Footprint             (bind k f)
+  | Barrier bk k ->            Barrier bk            (bind k f)
+  | Write_reg r v k ->         Write_reg r v         (bind k f)
+  | Print msg k ->             Print msg             (bind k f)
+  | Fail descr ->              Fail descr
+  | Exception e ->             Exception e
 end
 
 val exit : forall 'rv 'a 'e. unit -> monad 'rv 'a 'e
@@ -74,21 +82,19 @@ let throw e = Exception e
 
 val try_catch : forall 'rv 'a 'e1 'e2. monad 'rv 'a 'e1 -> ('e1 -> monad 'rv 'a 'e2) -> monad 'rv 'a 'e2
 let rec try_catch m h = match m with
-  | Done a ->             Done a
-  | Read_mem rk a sz k -> Read_mem rk a sz (fun v -> try_catch (k v) h)
-  | Read_tag a k ->       Read_tag a       (fun v -> try_catch (k v) h)
-  | Write_memv descr k -> Write_memv descr (fun v -> try_catch (k v) h)
-  | Write_tag a t k ->    Write_tag a t    (fun v -> try_catch (k v) h)
-  | Read_reg descr k ->   Read_reg descr   (fun v -> try_catch (k v) h)
-  | Excl_res k ->         Excl_res         (fun v -> try_catch (k v) h)
-  | Undefined k ->        Undefined        (fun v -> try_catch (k v) h)
-  | Write_ea wk a sz k -> Write_ea wk a sz (try_catch k h)
-  | Footprint k ->        Footprint        (try_catch k h)
-  | Barrier bk k ->       Barrier bk       (try_catch k h)
-  | Write_reg r v k ->    Write_reg r v    (try_catch k h)
-  | Print msg k ->        Print msg        (try_catch k h)
-  | Fail descr ->         Fail descr
-  | Exception e ->        h e
+  | Done a -> Done a
+  | Read_mem rk a sz k ->      Read_mem rk a sz      (fun v -> try_catch (k v) h)
+  | Write_mem wk a sz v t k -> Write_mem wk a sz v t (fun v -> try_catch (k v) h)
+  | Read_reg descr k ->        Read_reg descr        (fun v -> try_catch (k v) h)
+  | Excl_res k ->              Excl_res              (fun v -> try_catch (k v) h)
+  | Undefined k ->             Undefined             (fun v -> try_catch (k v) h)
+  | Write_ea wk a sz k ->      Write_ea wk a sz      (try_catch k h)
+  | Footprint k ->             Footprint             (try_catch k h)
+  | Barrier bk k ->            Barrier bk            (try_catch k h)
+  | Write_reg r v k ->         Write_reg r v         (try_catch k h)
+  | Print msg k ->             Print msg             (try_catch k h)
+  | Fail descr ->              Fail descr
+  | Exception e ->             h e
 end
 
 (* For early return, we abuse exceptions by throwing and catching
@@ -126,19 +132,19 @@ let maybe_fail msg = function
   | Nothing -> Fail msg
 end
 
-val read_mem_bytes : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monad 'rv (list memory_byte) 'e
+val read_mem_bytes : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monad 'rv (list memory_byte * bitU) 'e
 let read_mem_bytes rk addr sz =
   Read_mem rk (bits_of addr) (nat_of_int sz) return
 
-val read_mem : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monad 'rv 'b 'e
+val read_mem : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monad 'rv ('b * bitU) 'e
 let read_mem rk addr sz =
   bind
     (read_mem_bytes rk addr sz)
-    (fun bytes ->
-       maybe_fail "bits_of_mem_bytes" (of_bits (bits_of_mem_bytes bytes)))
-
-val read_tag : forall 'rv 'a 'e. Bitvector 'a => 'a -> monad 'rv bitU 'e
-let read_tag addr = Read_tag (bits_of addr) return
+    (fun (bytes, tag) ->
+       match of_bits (bits_of_mem_bytes bytes) with
+         | Just v -> return (v, tag)
+         | Nothing -> Fail "bits_of_mem_bytes"
+       end)
 
 val excl_result : forall 'rv 'e. unit -> monad 'rv bool 'e
 let excl_result () =
@@ -148,15 +154,13 @@ let excl_result () =
 val write_mem_ea : forall 'rv 'a 'e. Bitvector 'a => write_kind -> 'a -> integer -> monad 'rv unit 'e
 let write_mem_ea wk addr sz = Write_ea wk (bits_of addr) (nat_of_int sz) (Done ())
 
-val write_mem_val : forall 'rv 'a 'e. Bitvector 'a => 'a -> monad 'rv bool 'e
-let write_mem_val v = match mem_bytes_of_bits v with
-  | Just v -> Write_memv v return
-  | Nothing -> Fail "write_mem_val"
+val write_mem : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b =>
+  write_kind -> 'a -> integer -> 'b -> bitU -> monad 'rv bool 'e
+let write_mem wk addr sz v tag = match mem_bytes_of_bits v with
+  | Just v -> Write_mem wk (bits_of addr) (nat_of_int sz) v tag return
+  | Nothing -> Fail "write_mem"
 end
 
-val write_tag : forall 'rv 'a 'e. Bitvector 'a => 'a -> bitU -> monad 'rv bool 'e
-let write_tag addr b = Write_tag (bits_of addr) b return
-
 val read_reg : forall 's 'rv 'a 'e. register_ref 's 'rv 'a -> monad 'rv 'a 'e
 let read_reg reg =
   let k v =
diff --git a/src/gen_lib/sail2_state_lifting.lem b/src/gen_lib/sail2_state_lifting.lem
index 039343e2..42e2c0f3 100644
--- a/src/gen_lib/sail2_state_lifting.lem
+++ b/src/gen_lib/sail2_state_lifting.lem
@@ -9,19 +9,17 @@ open import {isabelle} `Sail2_state_monad_lemmas`
 
 val liftState : forall 'regval 'regs 'a 'e. register_accessors 'regs 'regval -> monad 'regval 'a 'e -> monadS 'regs 'a 'e
 let rec liftState ra s = match s with
-  | (Done a)             -> returnS a
-  | (Read_mem rk a sz k) -> bindS (read_mem_bytesS rk a sz) (fun v -> liftState ra (k v))
-  | (Read_tag t k)       -> bindS (read_tagS t)             (fun v -> liftState ra (k v))
-  | (Write_memv a k)     -> bindS (write_mem_bytesS a)      (fun v -> liftState ra (k v))
-  | (Write_tag a t k)    -> bindS (write_tagS a t)          (fun v -> liftState ra (k v))
-  | (Read_reg r k)       -> bindS (read_regvalS ra r)       (fun v -> liftState ra (k v))
-  | (Excl_res k)         -> bindS (excl_resultS ())         (fun v -> liftState ra (k v))
-  | (Undefined k)        -> bindS (undefined_boolS ())      (fun v -> liftState ra (k v))
-  | (Write_ea wk a sz k) -> seqS (write_mem_eaS wk a sz)    (liftState ra k)
-  | (Write_reg r v k)    -> seqS (write_regvalS ra r v)     (liftState ra k)
-  | (Footprint k)        -> liftState ra k
-  | (Barrier _ k)        -> liftState ra k
-  | (Print _ k)          -> liftState ra k (* TODO *)
-  | (Fail descr)         -> failS descr
-  | (Exception e)        -> throwS e
+  | (Done a)                  -> returnS a
+  | (Read_mem rk a sz k)      -> bindS (read_mem_bytesS rk a sz)      (fun v -> liftState ra (k v))
+  | (Write_mem wk a sz v t k) -> bindS (write_mem_bytesS wk a sz v t) (fun v -> liftState ra (k v))
+  | (Read_reg r k)            -> bindS (read_regvalS ra r)            (fun v -> liftState ra (k v))
+  | (Excl_res k)              -> bindS (excl_resultS ())              (fun v -> liftState ra (k v))
+  | (Undefined k)             -> bindS (undefined_boolS ())           (fun v -> liftState ra (k v))
+  | (Write_reg r v k)         -> seqS (write_regvalS ra r v)          (liftState ra k)
+  | (Write_ea _ _ _ k)        -> liftState ra k
+  | (Footprint k)             -> liftState ra k
+  | (Barrier _ k)             -> liftState ra k
+  | (Print _ k)               -> liftState ra k (* TODO *)
+  | (Fail descr)              -> failS descr
+  | (Exception e)             -> throwS e
 end
diff --git a/src/gen_lib/sail2_state_monad.lem b/src/gen_lib/sail2_state_monad.lem
index 30b296cc..89b29fa5 100644
--- a/src/gen_lib/sail2_state_monad.lem
+++ b/src/gen_lib/sail2_state_monad.lem
@@ -11,17 +11,13 @@ type tagstate = map integer bitU
 type sequential_state 'regs =
   <| regstate : 'regs;
      memstate : memstate;
-     tagstate : tagstate;
-     write_ea : maybe (write_kind * integer * integer);
-     last_exclusive_operation_was_load : bool |>
+     tagstate : tagstate |>
 
 val init_state : forall 'regs. 'regs -> sequential_state 'regs
 let init_state regs =
   <| regstate = regs;
      memstate = Map.empty;
-     tagstate = Map.empty;
-     write_ea = Nothing;
-     last_exclusive_operation_was_load = false |>
+     tagstate = Map.empty |>
 
 type ex 'e =
   | Failure of string
@@ -124,66 +120,57 @@ let read_tagS addr =
   readS (fun s -> fromMaybe B0 (Map.lookup addr s.tagstate)))
 
 (* Read bytes from memory and return in little endian order *)
-val read_mem_bytesS : forall 'regs 'e 'a. Bitvector 'a => read_kind -> 'a -> nat -> monadS 'regs (list memory_byte) 'e
-let read_mem_bytesS read_kind addr sz =
+val read_mem_bytesS : forall 'regs 'e 'a. Bitvector 'a => read_kind -> 'a -> nat -> monadS 'regs (list memory_byte * bitU) 'e
+let read_mem_bytesS _ addr sz =
   maybe_failS "unsigned" (unsigned addr) >>$= (fun addr ->
   let sz = integerFromNat sz in
   let addrs = index_list addr (addr+sz-1) 1 in
   let read_byte s addr = Map.lookup addr s.memstate in
-  readS (fun s -> just_list (List.map (read_byte s) addrs)) >>$= (function
-    | Just mem_val ->
-       updateS (fun s ->
-         if read_is_exclusive read_kind
-         then <| s with last_exclusive_operation_was_load = true |>
-         else s) >>$
-       returnS mem_val
-    | Nothing -> failS "read_memS"
+  let read_tag s addr = Map.findWithDefault addr B0 s.tagstate in
+  readS (fun s ->
+    (just_list (List.map (read_byte s) addrs),
+     List.foldl and_bit B1 (List.map (read_tag s) addrs))) >>$=
+  (function
+    | (Just mem_val, tag) -> returnS (mem_val, tag)
+    | _ -> failS "read_memS"
   end))
 
-val read_memS : forall 'regs 'e 'a 'b. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monadS 'regs 'b 'e
+val read_memS : forall 'regs 'e 'a 'b. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monadS 'regs ('b * bitU) 'e
 let read_memS rk a sz =
-  read_mem_bytesS rk a (nat_of_int sz) >>$= (fun bytes ->
-  maybe_failS "bits_of_mem_bytes" (of_bits (bits_of_mem_bytes bytes)))
+  read_mem_bytesS rk a (nat_of_int sz) >>$= (fun (bytes, tag) ->
+  maybe_failS "bits_of_mem_bytes" (of_bits (bits_of_mem_bytes bytes)) >>$= (fun mem_val ->
+  returnS (mem_val, tag)))
 
 val excl_resultS : forall 'regs 'e. unit -> monadS 'regs bool 'e
-let excl_resultS () =
-  readS (fun s -> s.last_exclusive_operation_was_load) >>$= (fun excl_load ->
-  updateS (fun s -> <| s with last_exclusive_operation_was_load = false |>) >>$
-  chooseS (if excl_load then {false; true} else {false}))
-
-val write_mem_eaS : forall 'regs 'e 'a. Bitvector 'a => write_kind -> 'a -> nat -> monadS 'regs unit 'e
-let write_mem_eaS write_kind addr sz =
+let excl_resultS =
+  (* TODO: This used to be more deterministic, checking a flag in the state
+     whether an exclusive load has occurred before.  However, this does not
+     seem very precise; it might be safer to overapproximate the possible
+     behaviours by always making a nondeterministic choice. *)
+  undefined_boolS
+
+(* Write little-endian list of bytes to given address *)
+val write_mem_bytesS : forall 'regs 'e 'a. Bitvector 'a => write_kind -> 'a -> nat -> list memory_byte -> bitU -> monadS 'regs bool 'e
+let write_mem_bytesS _ addr sz v t =
   maybe_failS "unsigned" (unsigned addr) >>$= (fun addr ->
   let sz = integerFromNat sz in
-  updateS (fun s -> <| s with write_ea = Just (write_kind, addr, sz) |>))
-
-(* Write little-endian list of bytes to previously announced address *)
-val write_mem_bytesS : forall 'regs 'e. list memory_byte -> monadS 'regs bool 'e
-let write_mem_bytesS v =
-  readS (fun s -> s.write_ea) >>$= (function
-      | Nothing -> failS "write ea has not been announced yet"
-      | Just (_, addr, sz) ->
-         let addrs = index_list addr (addr+sz-1) 1 in
-         (*let v = external_mem_value (bits_of v) in*)
-         let a_v = List.zip addrs v in
-         let write_byte mem (addr, v) = Map.insert addr v mem in
-         updateS (fun s ->
-           <| s with memstate = List.foldl write_byte s.memstate a_v |>) >>$
-         returnS true
-    end)
-
-val write_mem_valS : forall 'regs 'e 'a. Bitvector 'a => 'a -> monadS 'regs bool 'e
-let write_mem_valS v = match mem_bytes_of_bits v with
-  | Just v -> write_mem_bytesS v
-  | Nothing -> failS "write_mem_val"
+  let addrs = index_list addr (addr+sz-1) 1 in
+  (*let v = external_mem_value (bits_of v) in*)
+  let a_v = List.zip addrs v in
+  let write_byte mem (addr, v) = Map.insert addr v mem in
+  let write_tag mem addr = Map.insert addr t mem in
+  updateS (fun s ->
+    <| s with memstate = List.foldl write_byte s.memstate a_v;
+              tagstate = List.foldl write_tag s.tagstate addrs |>) >>$
+  returnS true)
+
+val write_memS : forall 'regs 'e 'a 'b. Bitvector 'a, Bitvector 'b =>
+  write_kind -> 'a -> nat -> 'b -> bitU -> monadS 'regs bool 'e
+let write_memS wk addr sz v t = match mem_bytes_of_bits v with
+  | Just v -> write_mem_bytesS wk addr sz v t
+  | Nothing -> failS "write_mem"
 end
 
-val write_tagS : forall 'regs 'a 'e. Bitvector 'a => 'a -> bitU -> monadS 'regs bool 'e
-let write_tagS addr t =
-   maybe_failS "unsigned" (unsigned addr) >>$= (fun addr ->
-   updateS (fun s -> <| s with tagstate = Map.insert addr t s.tagstate |>) >>$
-   returnS true)
-
 val read_regS : forall 'regs 'rv 'a 'e. register_ref 'regs 'rv 'a -> monadS 'regs 'a 'e
 let read_regS reg = readS (fun s -> reg.read_from s.regstate)
 
-- 
cgit v1.2.3


From 05c03453c25f1c259670283a9a92a6c21c9ec319 Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Fri, 19 Oct 2018 12:02:20 +0100
Subject: Fix Isabelle library

---
 lib/isabelle/Sail2_prompt_monad_lemmas.thy | 76 +++++++++++-------------------
 lib/isabelle/Sail2_state_lemmas.thy        | 24 ++++++----
 lib/isabelle/Sail2_state_monad_lemmas.thy  | 21 +++++----
 3 files changed, 55 insertions(+), 66 deletions(-)

diff --git a/lib/isabelle/Sail2_prompt_monad_lemmas.thy b/lib/isabelle/Sail2_prompt_monad_lemmas.thy
index 25eb9f52..406b5871 100644
--- a/lib/isabelle/Sail2_prompt_monad_lemmas.thy
+++ b/lib/isabelle/Sail2_prompt_monad_lemmas.thy
@@ -30,42 +30,17 @@ lemma All_try_catch_dom: "try_catch_dom (m, h)"
 termination try_catch using All_try_catch_dom by auto
 lemmas try_catch_induct[case_names Done Read_mem Write_memv Read_reg Excl_res Write_ea Barrier Write_reg Fail Exception] = try_catch.induct
 
-datatype 'regval event =
-  (* Request to read memory *)
-    e_read_mem read_kind "bitU list" nat "memory_byte list"
-  | e_read_tag "bitU list" bitU
-  (* Write is imminent, at address lifted, of size nat *)
-  | e_write_ea write_kind "bitU list" nat
-  (* Request the result of store-exclusive *)
-  | e_excl_res bool
-  (* Request to write memory at last signalled address. Memory value should be 8
-     times the size given in ea signal *)
-  | e_write_memv "memory_byte list" bool
-  | e_write_tag "bitU list" bitU bool
-  (* Tell the system to dynamically recalculate dependency footprint *)
-  | e_footprint
-  (* Request a memory barrier *)
-  | e_barrier " barrier_kind "
-  (* Request to read register *)
-  | e_read_reg string 'regval
-  (* Request to write register *)
-  | e_write_reg string 'regval
-  | e_undefined bool
-  | e_print string
-
 inductive_set T :: "(('rv, 'a, 'e) monad \<times> 'rv event \<times> ('rv, 'a, 'e) monad) set" where
-  Read_mem: "((Read_mem rk addr sz k), e_read_mem rk addr sz v, k v) \<in> T"
-| Read_tag: "((Read_tag addr k), e_read_tag addr v, k v) \<in> T"
-| Write_ea: "((Write_ea wk addr sz k), e_write_ea wk addr sz, k) \<in> T"
-| Excl_res: "((Excl_res k), e_excl_res r, k r) \<in> T"
-| Write_memv: "((Write_memv v k), e_write_memv v r, k r) \<in> T"
-| Write_tag: "((Write_tag a v k), e_write_tag a v r, k r) \<in> T"
-| Footprint: "((Footprint k), e_footprint, k) \<in> T"
-| Barrier: "((Barrier bk k), e_barrier bk, k) \<in> T"
-| Read_reg: "((Read_reg r k), e_read_reg r v, k v) \<in> T"
-| Write_reg: "((Write_reg r v k), e_write_reg r v, k) \<in> T"
-| Undefined: "((Undefined k), e_undefined v, k v) \<in> T"
-| Print: "((Print msg k), e_print msg, k) \<in> T"
+  Read_mem: "((Read_mem rk addr sz k), E_read_mem rk addr sz v, k v) \<in> T"
+| Write_ea: "((Write_ea wk addr sz k), E_write_ea wk addr sz, k) \<in> T"
+| Excl_res: "((Excl_res k), E_excl_res r, k r) \<in> T"
+| Write_mem: "((Write_mem wk addr sz v t k), E_write_mem wk addr sz v t r, k r) \<in> T"
+| Footprint: "((Footprint k), E_footprint, k) \<in> T"
+| Barrier: "((Barrier bk k), E_barrier bk, k) \<in> T"
+| Read_reg: "((Read_reg r k), E_read_reg r v, k v) \<in> T"
+| Write_reg: "((Write_reg r v k), E_write_reg r v, k) \<in> T"
+| Undefined: "((Undefined k), E_undefined v, k v) \<in> T"
+| Print: "((Print msg k), E_print msg, k) \<in> T"
 
 inductive_set Traces :: "(('rv, 'a, 'e) monad \<times> 'rv event list \<times> ('rv, 'a, 'e) monad) set" where
   Nil: "(s, [], s) \<in> Traces"
@@ -85,25 +60,28 @@ lemma Traces_cases:
   fixes m :: "('rv, 'a, 'e) monad"
   assumes Run: "(m, t, m') \<in> Traces"
   obtains (Nil) a where "m = m'" and "t = []"
-  | (Read_mem) rk addr s k t' v where "m = Read_mem rk addr s k" and "t = e_read_mem rk addr s v # t'" and "(k v, t', m') \<in> Traces"
-  | (Read_tag) addr k t' v where "m = Read_tag addr k" and "t = e_read_tag addr v # t'" and "(k v, t', m') \<in> Traces"
-  | (Write_memv) val k t' v where "m = Write_memv val k" and "t = e_write_memv val v # t'" and "(k v, t', m') \<in> Traces"
-  | (Write_tag) a val k t' v where "m = Write_tag a val k" and "t = e_write_tag a val v # t'" and "(k v, t', m') \<in> Traces"
-  | (Barrier) bk k t' v where "m = Barrier bk k" and "t = e_barrier bk # t'" and "(k, t', m') \<in> Traces"
-  | (Read_reg) reg k t' v where "m = Read_reg reg k" and "t = e_read_reg reg v # t'" and "(k v, t', m') \<in> Traces"
-  | (Excl_res) k t' v where "m = Excl_res k" and "t = e_excl_res v # t'" and "(k v, t', m') \<in> Traces"
-  | (Write_ea) wk addr s k t' where "m = Write_ea wk addr s k" and "t = e_write_ea wk addr s # t'" and "(k, t', m') \<in> Traces"
-  | (Footprint) k t' where "m = Footprint k" and "t = e_footprint # t'" and "(k, t', m') \<in> Traces"
-  | (Write_reg) reg v k t' where "m = Write_reg reg v k" and "t = e_write_reg reg v # t'" and "(k, t', m') \<in> Traces"
-  | (Undefined) xs v k t' where "m = Undefined k" and "t = e_undefined v # t'" and "(k v, t', m') \<in> Traces"
-  | (Print) msg k t' where "m = Print msg k" and "t = e_print msg # t'" and "(k, t', m') \<in> Traces"
+  | (Read_mem) rk addr s k t' v tag where "m = Read_mem rk addr s k" and "t = E_read_mem rk addr s (v, tag) # t'" and "(k (v, tag), t', m') \<in> Traces"
+  | (Write_mem) wk addr sz val tag k t' v where "m = Write_mem wk addr sz val tag k" and "t = E_write_mem wk addr sz val tag v # t'" and "(k v, t', m') \<in> Traces"
+  | (Barrier) bk k t' v where "m = Barrier bk k" and "t = E_barrier bk # t'" and "(k, t', m') \<in> Traces"
+  | (Read_reg) reg k t' v where "m = Read_reg reg k" and "t = E_read_reg reg v # t'" and "(k v, t', m') \<in> Traces"
+  | (Excl_res) k t' v where "m = Excl_res k" and "t = E_excl_res v # t'" and "(k v, t', m') \<in> Traces"
+  | (Write_ea) wk addr s k t' where "m = Write_ea wk addr s k" and "t = E_write_ea wk addr s # t'" and "(k, t', m') \<in> Traces"
+  | (Footprint) k t' where "m = Footprint k" and "t = E_footprint # t'" and "(k, t', m') \<in> Traces"
+  | (Write_reg) reg v k t' where "m = Write_reg reg v k" and "t = E_write_reg reg v # t'" and "(k, t', m') \<in> Traces"
+  | (Undefined) xs v k t' where "m = Undefined k" and "t = E_undefined v # t'" and "(k v, t', m') \<in> Traces"
+  | (Print) msg k t' where "m = Print msg k" and "t = E_print msg # t'" and "(k, t', m') \<in> Traces"
 proof (use Run in \<open>cases m t m' set: Traces\<close>)
   case Nil
   then show ?thesis by (auto intro: that(1))
 next
   case (Step e m'' t')
-  from \<open>(m, e, m'') \<in> T\<close> and \<open>t = e # t'\<close> and \<open>(m'', t', m') \<in> Traces\<close>
-  show ?thesis by (cases m e m'' rule: T.cases; elim that; blast)
+  note t = \<open>t = e # t'\<close>
+  note m' = \<open>(m'', t', m') \<in> Traces\<close>
+  from \<open>(m, e, m'') \<in> T\<close> and t and m'
+  show ?thesis proof (cases m e m'' rule: T.cases)
+    case (Read_mem rk addr sz k v)
+    then show ?thesis using t m' by (cases v; elim that; blast)
+  qed (elim that; blast)+
 qed
 
 abbreviation Run :: "('rv, 'a, 'e) monad \<Rightarrow> 'rv event list \<Rightarrow> 'a \<Rightarrow> bool"
diff --git a/lib/isabelle/Sail2_state_lemmas.thy b/lib/isabelle/Sail2_state_lemmas.thy
index ba69d0d8..25d4edea 100644
--- a/lib/isabelle/Sail2_state_lemmas.thy
+++ b/lib/isabelle/Sail2_state_lemmas.thy
@@ -18,7 +18,7 @@ lemma Value_liftState_Run:
   assumes "(Value a, s') \<in> liftState r m s"
   obtains t where "Run m t a"
   by (use assms in \<open>induction r m arbitrary: s s' rule: liftState.induct\<close>;
-      auto simp add: failS_def throwS_def returnS_def simp del: read_regvalS.simps;
+      simp add: failS_def throwS_def returnS_def del: read_regvalS.simps;
       blast elim: Value_bindS_elim)
 
 lemmas liftState_if_distrib[liftState_simp] = if_distrib[where f = "liftState ra" for ra]
@@ -82,7 +82,10 @@ lemma liftState_read_mem_BC:
   assumes "unsigned_method BC_bitU_list (bits_of_method BCa a) = unsigned_method BCa a"
   shows "liftState r (read_mem BCa BCb rk a sz) = read_memS BCa BCb rk a sz"
   using assms
-  by (auto simp: read_mem_def read_mem_bytes_def read_memS_def read_mem_bytesS_def maybe_failS_def liftState_simp split: option.splits)
+  by (auto simp: read_mem_def read_mem_bytes_def read_memS_def read_mem_bytesS_def maybe_failS_def
+                 prod.case_distrib option.case_distrib[where h = "liftState r"]
+                 option.case_distrib[where h = "\<lambda>c. c \<bind>\<^sub>S f" for f] liftState_simp
+           cong: option.case_cong)
 
 lemma liftState_read_mem[liftState_simp]:
   "\<And>a. liftState r (read_mem BC_mword BC_mword rk a sz) = read_memS BC_mword BC_mword rk a sz"
@@ -91,17 +94,22 @@ lemma liftState_read_mem[liftState_simp]:
 
 lemma liftState_write_mem_ea_BC:
   assumes "unsigned_method BC_bitU_list (bits_of_method BCa a) = unsigned_method BCa a"
-  shows "liftState r (write_mem_ea BCa rk a sz) = write_mem_eaS BCa rk a (nat sz)"
-  using assms by (auto simp: write_mem_ea_def write_mem_eaS_def)
+  shows "liftState r (write_mem_ea BCa rk a sz) = returnS ()"
+  using assms by (auto simp: write_mem_ea_def)
 
 lemma liftState_write_mem_ea[liftState_simp]:
-  "\<And>a. liftState r (write_mem_ea BC_mword rk a sz) = write_mem_eaS BC_mword rk a (nat sz)"
-  "\<And>a. liftState r (write_mem_ea BC_bitU_list rk a sz) = write_mem_eaS BC_bitU_list rk a (nat sz)"
+  "\<And>a. liftState r (write_mem_ea BC_mword rk a sz) = returnS ()"
+  "\<And>a. liftState r (write_mem_ea BC_bitU_list rk a sz) = returnS ()"
   by (auto simp: liftState_write_mem_ea_BC)
 
+lemma write_mem_bytesS_def_BC_bitU_list_BC_mword[simp]:
+  "write_mem_bytesS BC_bitU_list wk (bits_of_method BC_mword addr) sz v t =
+   write_mem_bytesS BC_mword wk addr sz v t"
+  by (auto simp: write_mem_bytesS_def)
+
 lemma liftState_write_mem_val[liftState_simp]:
-  "liftState r (write_mem_val BC v) = write_mem_valS BC v"
-  by (auto simp: write_mem_val_def write_mem_valS_def liftState_simp split: option.splits)
+  "liftState r (write_mem BC_mword BCv wk addr sz v t) = write_memS BC_mword BCv wk addr sz v t"
+  by (auto simp: write_mem_def write_memS_def liftState_simp split: option.splits)
 
 lemma liftState_read_reg_readS:
   assumes "\<And>s. Option.bind (get_regval' (name reg) s) (of_regval reg) = Some (read_from reg s)"
diff --git a/lib/isabelle/Sail2_state_monad_lemmas.thy b/lib/isabelle/Sail2_state_monad_lemmas.thy
index 3a286c10..b2fde7ba 100644
--- a/lib/isabelle/Sail2_state_monad_lemmas.thy
+++ b/lib/isabelle/Sail2_state_monad_lemmas.thy
@@ -205,24 +205,27 @@ lemma no_throw_basic_builtins[simp]:
 
 lemmas ignore_throw_option_case_distrib =
   option.case_distrib[where h = "\<lambda>c. ignore_throw c s" and option = "c s" for c s]
+  option.case_distrib[where h = "\<lambda>c. ignore_throw c" and option = "c" for c]
+
+lemma ignore_throw_let_distrib: "ignore_throw (let x = y in f x) = (let x = y in ignore_throw (f x))"
+  by auto
 
 lemma no_throw_mem_builtins:
   "\<And>BC rk a sz s. ignore_throw (read_mem_bytesS BC rk a sz) s = read_mem_bytesS BC rk a sz s"
   "\<And>BC a s. ignore_throw (read_tagS BC a) s = read_tagS BC a s"
-  "\<And>BC wk a sz s. ignore_throw (write_mem_eaS BC wk a sz) s = write_mem_eaS BC wk a sz s"
-  "\<And>v s. ignore_throw (write_mem_bytesS v) s = write_mem_bytesS v s"
-  "\<And>BC v s. ignore_throw (write_mem_valS BC v) s = write_mem_valS BC v s"
-  "\<And>BC a t s. ignore_throw (write_tagS BC a t) s = write_tagS BC a t s"
+  "\<And>BC wk addr sz v t s. ignore_throw (write_mem_bytesS BC wk addr sz v t) s = write_mem_bytesS BC wk addr sz v t s"
+  "\<And>BC_a BC_v wk addr sz v t s. ignore_throw (write_memS BC_a BC_v wk addr sz v t) s = write_memS BC_a BC_v wk addr sz v t s"
   "\<And>s. ignore_throw (excl_resultS ()) s = excl_resultS () s"
   "\<And>s. ignore_throw (undefined_boolS ()) s = undefined_boolS () s"
-  unfolding read_mem_bytesS_def read_memS_def read_tagS_def write_mem_eaS_def
-  unfolding write_mem_valS_def write_mem_bytesS_def write_tagS_def
-  unfolding excl_resultS_def undefined_boolS_def
+  unfolding read_mem_bytesS_def read_memS_def read_tagS_def write_memS_def
+  unfolding write_mem_bytesS_def
+  unfolding excl_resultS_def undefined_boolS_def maybe_failS_def
+  unfolding ignore_throw_bindS
   by (auto cong: bindS_cong bindS_ext_cong ignore_throw_cong option.case_cong
-           simp: option.case_distrib prod.case_distrib ignore_throw_option_case_distrib comp_def)
+           simp: prod.case_distrib ignore_throw_option_case_distrib ignore_throw_let_distrib comp_def)
 
 lemma no_throw_read_memS: "ignore_throw (read_memS BCa BCb rk a sz) s = read_memS BCa BCb rk a sz s"
-  by (auto simp: read_memS_def no_throw_mem_builtins cong: bindS_ext_cong)
+  by (auto simp: read_memS_def no_throw_mem_builtins prod.case_distrib comp_def cong: bindS_ext_cong)
 
 lemma no_throw_read_regvalS: "ignore_throw (read_regvalS r reg_name) s = read_regvalS r reg_name s"
   by (cases r) (auto simp: option.case_distrib cong: bindS_cong option.case_cong)
-- 
cgit v1.2.3


From 10cb6bf0b0c37ccf7ec1bc222ed0a694fd815843 Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Tue, 23 Oct 2018 11:28:39 +0100
Subject: Add helper functions in Sail Lem library

Running traces, directly accessing memory state
---
 src/gen_lib/sail2_prompt_monad.lem  | 58 +++++++++++++++++++++++++++++++++++++
 src/gen_lib/sail2_state_lifting.lem | 27 +++++++++++++++--
 src/gen_lib/sail2_state_monad.lem   | 37 ++++++++++++-----------
 3 files changed, 102 insertions(+), 20 deletions(-)

diff --git a/src/gen_lib/sail2_prompt_monad.lem b/src/gen_lib/sail2_prompt_monad.lem
index 991d3895..5a6d2aef 100644
--- a/src/gen_lib/sail2_prompt_monad.lem
+++ b/src/gen_lib/sail2_prompt_monad.lem
@@ -48,6 +48,8 @@ type event 'regval =
   | E_undefined of bool
   | E_print of string
 
+type trace 'regval = list (event 'regval)
+
 val return : forall 'rv 'a 'e. 'a -> monad 'rv 'a 'e
 let return a = Done a
 
@@ -218,6 +220,62 @@ let barrier bk = Barrier bk (Done ())
 val footprint : forall 'rv 'e. unit -> monad 'rv unit 'e
 let footprint _ = Footprint (Done ())
 
+(* Event traces *)
+
+val emitEvent : forall 'regval 'a 'e. Eq 'regval => monad 'regval 'a 'e -> event 'regval -> maybe (monad 'regval 'a 'e)
+let emitEvent m e = match (e, m) with
+  | (E_read_mem rk a sz v, Read_mem rk' a' sz' k) ->
+     if rk' = rk && a' = a && sz' = sz then Just (k v) else Nothing
+  | (E_write_mem wk a sz v tag r, Write_mem wk' a' sz' v' tag' k) ->
+     if wk' = wk && a' = a && sz' = sz && v' = v && tag' = tag then Just (k r) else Nothing
+  | (E_read_reg r v, Read_reg r' k) ->
+     if r' = r then Just (k v) else Nothing
+  | (E_write_reg r v, Write_reg r' v' k) ->
+     if r' = r && v' = v then Just k else Nothing
+  | (E_write_ea wk a sz, Write_ea wk' a' sz' k) ->
+     if wk' = wk && a' = a && sz' = sz then Just k else Nothing
+  | (E_barrier bk, Barrier bk' k) ->
+     if bk' = bk then Just k else Nothing
+  | (E_print m, Print m' k) ->
+     if m' = m then Just k else Nothing
+  | (E_excl_res v, Excl_res k) -> Just (k v)
+  | (E_undefined v, Undefined k) -> Just (k v)
+  | (E_footprint, Footprint k) -> Just k
+  | _ -> Nothing
+end
+
+val runTrace : forall 'regval 'a 'e. Eq 'regval => trace 'regval -> monad 'regval 'a 'e -> maybe (monad 'regval 'a 'e)
+let rec runTrace t m = match t with
+  | [] -> Just m
+  | e :: t' -> Maybe.bind (emitEvent m e) (runTrace t')
+end
+
+val final : forall 'regval 'a 'e. monad 'regval 'a 'e -> bool
+let final = function
+  | Done _ -> true
+  | Fail _ -> true
+  | Exception _ -> true
+  | _ -> false
+end
+
+val hasTrace : forall 'regval 'a 'e. Eq 'regval => trace 'regval -> monad 'regval 'a 'e -> bool
+let hasTrace t m = match runTrace t m with
+  | Just m -> final m
+  | Nothing -> false
+end
+
+val hasException : forall 'regval 'a 'e. Eq 'regval => trace 'regval -> monad 'regval 'a 'e -> bool
+let hasException t m = match runTrace t m with
+  | Just (Exception _) -> true
+  | _ -> false
+end
+
+val hasFailure : forall 'regval 'a 'e. Eq 'regval => trace 'regval -> monad 'regval 'a 'e -> bool
+let hasFailure t m = match runTrace t m with
+  | Just (Fail _) -> true
+  | _ -> false
+end
+
 (* Define a type synonym that also takes the register state as a type parameter,
    in order to make switching to the state monad without changing generated
    definitions easier, see also lib/hol/prompt_monad.lem. *)
diff --git a/src/gen_lib/sail2_state_lifting.lem b/src/gen_lib/sail2_state_lifting.lem
index 42e2c0f3..314c562d 100644
--- a/src/gen_lib/sail2_state_lifting.lem
+++ b/src/gen_lib/sail2_state_lifting.lem
@@ -5,10 +5,9 @@ open import Sail2_prompt
 open import Sail2_state_monad
 open import {isabelle} `Sail2_state_monad_lemmas`
 
-(* State monad wrapper around prompt monad *)
-
+(* Lifting from prompt monad to state monad *)
 val liftState : forall 'regval 'regs 'a 'e. register_accessors 'regs 'regval -> monad 'regval 'a 'e -> monadS 'regs 'a 'e
-let rec liftState ra s = match s with
+let rec liftState ra m = match m with
   | (Done a)                  -> returnS a
   | (Read_mem rk a sz k)      -> bindS (read_mem_bytesS rk a sz)      (fun v -> liftState ra (k v))
   | (Write_mem wk a sz v t k) -> bindS (write_mem_bytesS wk a sz v t) (fun v -> liftState ra (k v))
@@ -23,3 +22,25 @@ let rec liftState ra s = match s with
   | (Fail descr)              -> failS descr
   | (Exception e)             -> throwS e
 end
+
+val runTraceS : forall 'regval 'regs 'a 'e. Eq 'regval => register_accessors 'regs 'regval -> trace 'regval -> sequential_state 'regs -> maybe (sequential_state 'regs)
+let rec runTraceS ra t s =
+  match t with
+  | [] -> Just s
+  | E_read_mem _ addr sz (v, tag) :: t' ->
+     Maybe.bind (unsigned addr) (fun addr ->
+     Maybe.bind (get_mem_bytes addr sz s) (fun (v', tag') ->
+     if v' = v && tag' = tag then runTraceS ra t' s else Nothing))
+  | E_write_mem _ addr sz v tag _ :: t' ->
+     Maybe.bind (unsigned addr) (fun addr ->
+     runTraceS ra t' (put_mem_bytes addr sz v tag s))
+  | E_read_reg r v :: t' ->
+     let (read_reg, _) = ra in
+     Maybe.bind (read_reg r s.regstate) (fun v' ->
+     if v' = v then runTraceS ra t' s else Nothing)
+  | E_write_reg r v :: t' ->
+     let (_, write_reg) = ra in
+     Maybe.bind (write_reg r v s.regstate) (fun s' ->
+     runTraceS ra t' <| s with regstate = s' |>)
+  | _ :: t' -> runTraceS ra t' s
+end
diff --git a/src/gen_lib/sail2_state_monad.lem b/src/gen_lib/sail2_state_monad.lem
index 89b29fa5..84ae86d8 100644
--- a/src/gen_lib/sail2_state_monad.lem
+++ b/src/gen_lib/sail2_state_monad.lem
@@ -120,20 +120,21 @@ let read_tagS addr =
   readS (fun s -> fromMaybe B0 (Map.lookup addr s.tagstate)))
 
 (* Read bytes from memory and return in little endian order *)
-val read_mem_bytesS : forall 'regs 'e 'a. Bitvector 'a => read_kind -> 'a -> nat -> monadS 'regs (list memory_byte * bitU) 'e
-let read_mem_bytesS _ addr sz =
-  maybe_failS "unsigned" (unsigned addr) >>$= (fun addr ->
+val get_mem_bytes : forall 'regs. integer -> nat -> sequential_state 'regs -> maybe (list memory_byte * bitU)
+let get_mem_bytes addr sz s =
   let sz = integerFromNat sz in
   let addrs = index_list addr (addr+sz-1) 1 in
   let read_byte s addr = Map.lookup addr s.memstate in
   let read_tag s addr = Map.findWithDefault addr B0 s.tagstate in
-  readS (fun s ->
-    (just_list (List.map (read_byte s) addrs),
-     List.foldl and_bit B1 (List.map (read_tag s) addrs))) >>$=
-  (function
-    | (Just mem_val, tag) -> returnS (mem_val, tag)
-    | _ -> failS "read_memS"
-  end))
+  Maybe.map
+    (fun mem_val -> (mem_val, List.foldl and_bit B1 (List.map (read_tag s) addrs)))
+    (just_list (List.map (read_byte s) addrs))
+
+val read_mem_bytesS : forall 'regs 'e 'a. Bitvector 'a => read_kind -> 'a -> nat -> monadS 'regs (list memory_byte * bitU) 'e
+let read_mem_bytesS _ addr sz =
+  maybe_failS "unsigned" (unsigned addr) >>$= (fun addr ->
+  readS (get_mem_bytes addr sz) >>$=
+  maybe_failS "read_memS")
 
 val read_memS : forall 'regs 'e 'a 'b. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monadS 'regs ('b * bitU) 'e
 let read_memS rk a sz =
@@ -150,18 +151,20 @@ let excl_resultS =
   undefined_boolS
 
 (* Write little-endian list of bytes to given address *)
-val write_mem_bytesS : forall 'regs 'e 'a. Bitvector 'a => write_kind -> 'a -> nat -> list memory_byte -> bitU -> monadS 'regs bool 'e
-let write_mem_bytesS _ addr sz v t =
-  maybe_failS "unsigned" (unsigned addr) >>$= (fun addr ->
+val put_mem_bytes : forall 'regs. integer -> nat -> list memory_byte -> bitU -> sequential_state 'regs -> sequential_state 'regs
+let put_mem_bytes addr sz v t s =
   let sz = integerFromNat sz in
   let addrs = index_list addr (addr+sz-1) 1 in
-  (*let v = external_mem_value (bits_of v) in*)
   let a_v = List.zip addrs v in
   let write_byte mem (addr, v) = Map.insert addr v mem in
   let write_tag mem addr = Map.insert addr t mem in
-  updateS (fun s ->
-    <| s with memstate = List.foldl write_byte s.memstate a_v;
-              tagstate = List.foldl write_tag s.tagstate addrs |>) >>$
+  <| s with memstate = List.foldl write_byte s.memstate a_v;
+            tagstate = List.foldl write_tag s.tagstate addrs |>
+
+val write_mem_bytesS : forall 'regs 'e 'a. Bitvector 'a => write_kind -> 'a -> nat -> list memory_byte -> bitU -> monadS 'regs bool 'e
+let write_mem_bytesS _ addr sz v t =
+  maybe_failS "unsigned" (unsigned addr) >>$= (fun addr ->
+  updateS (put_mem_bytes addr sz v t) >>$
   returnS true)
 
 val write_memS : forall 'regs 'e 'a 'b. Bitvector 'a, Bitvector 'b =>
-- 
cgit v1.2.3


From d733aa5c7409c645807589d268c0b80055bf671d Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Tue, 20 Nov 2018 18:32:37 +0000
Subject: Use nat instead of (list bitU) for addresses in monad outcomes

Removes some friction by back-and-forth conversion when handling events
---
 lib/isabelle/Sail2_state_lemmas.thy       | 12 +++++-----
 lib/isabelle/Sail2_state_monad_lemmas.thy |  4 ++--
 src/gen_lib/sail2_prompt_monad.lem        | 34 ++++++++++++++++-----------
 src/gen_lib/sail2_state_lifting.lem       |  6 ++---
 src/gen_lib/sail2_state_monad.lem         | 38 +++++++++++++++----------------
 src/gen_lib/sail2_values.lem              |  3 +++
 6 files changed, 52 insertions(+), 45 deletions(-)

diff --git a/lib/isabelle/Sail2_state_lemmas.thy b/lib/isabelle/Sail2_state_lemmas.thy
index 25d4edea..edcd9593 100644
--- a/lib/isabelle/Sail2_state_lemmas.thy
+++ b/lib/isabelle/Sail2_state_lemmas.thy
@@ -93,19 +93,19 @@ lemma liftState_read_mem[liftState_simp]:
   by (auto simp: liftState_read_mem_BC)
 
 lemma liftState_write_mem_ea_BC:
-  assumes "unsigned_method BC_bitU_list (bits_of_method BCa a) = unsigned_method BCa a"
+  assumes "unsigned_method BCa a = Some a'"
   shows "liftState r (write_mem_ea BCa rk a sz) = returnS ()"
-  using assms by (auto simp: write_mem_ea_def)
+  using assms by (auto simp: write_mem_ea_def nat_of_bv_def maybe_fail_def)
 
-lemma liftState_write_mem_ea[liftState_simp]:
+(*lemma liftState_write_mem_ea[liftState_simp]:
   "\<And>a. liftState r (write_mem_ea BC_mword rk a sz) = returnS ()"
   "\<And>a. liftState r (write_mem_ea BC_bitU_list rk a sz) = returnS ()"
-  by (auto simp: liftState_write_mem_ea_BC)
+  by (auto simp: liftState_write_mem_ea_BC)*)
 
-lemma write_mem_bytesS_def_BC_bitU_list_BC_mword[simp]:
+(*lemma write_mem_bytesS_def_BC_bitU_list_BC_mword[simp]:
   "write_mem_bytesS BC_bitU_list wk (bits_of_method BC_mword addr) sz v t =
    write_mem_bytesS BC_mword wk addr sz v t"
-  by (auto simp: write_mem_bytesS_def)
+  by (auto simp: write_mem_bytesS_def)*)
 
 lemma liftState_write_mem_val[liftState_simp]:
   "liftState r (write_mem BC_mword BCv wk addr sz v t) = write_memS BC_mword BCv wk addr sz v t"
diff --git a/lib/isabelle/Sail2_state_monad_lemmas.thy b/lib/isabelle/Sail2_state_monad_lemmas.thy
index b2fde7ba..6fb5e7ef 100644
--- a/lib/isabelle/Sail2_state_monad_lemmas.thy
+++ b/lib/isabelle/Sail2_state_monad_lemmas.thy
@@ -211,9 +211,9 @@ lemma ignore_throw_let_distrib: "ignore_throw (let x = y in f x) = (let x = y in
   by auto
 
 lemma no_throw_mem_builtins:
-  "\<And>BC rk a sz s. ignore_throw (read_mem_bytesS BC rk a sz) s = read_mem_bytesS BC rk a sz s"
+  "\<And>BC rk a sz s. ignore_throw (read_mem_bytesS rk a sz) s = read_mem_bytesS rk a sz s"
   "\<And>BC a s. ignore_throw (read_tagS BC a) s = read_tagS BC a s"
-  "\<And>BC wk addr sz v t s. ignore_throw (write_mem_bytesS BC wk addr sz v t) s = write_mem_bytesS BC wk addr sz v t s"
+  "\<And>BC wk addr sz v t s. ignore_throw (write_mem_bytesS wk addr sz v t) s = write_mem_bytesS wk addr sz v t s"
   "\<And>BC_a BC_v wk addr sz v t s. ignore_throw (write_memS BC_a BC_v wk addr sz v t) s = write_memS BC_a BC_v wk addr sz v t s"
   "\<And>s. ignore_throw (excl_resultS ()) s = excl_resultS () s"
   "\<And>s. ignore_throw (undefined_boolS ()) s = undefined_boolS () s"
diff --git a/src/gen_lib/sail2_prompt_monad.lem b/src/gen_lib/sail2_prompt_monad.lem
index 5a6d2aef..ae1f2cd8 100644
--- a/src/gen_lib/sail2_prompt_monad.lem
+++ b/src/gen_lib/sail2_prompt_monad.lem
@@ -9,16 +9,17 @@ type address = list bitU
 type monad 'regval 'a 'e =
   | Done of 'a
   (* Read a number of bytes from memory, returned in little endian order,
-     together with a tag. *)
-  | Read_mem of read_kind * address * nat * ((list memory_byte * bitU) -> monad 'regval 'a 'e)
+     together with a tag.  The first nat specifies the address, the second
+     the number of bytes. *)
+  | Read_mem of read_kind * nat * nat * ((list memory_byte * bitU) -> monad 'regval 'a 'e)
   (* Tell the system a write is imminent, at the given address and with the
      given size. *)
-  | Write_ea of write_kind * address * nat * monad 'regval 'a 'e
+  | Write_ea of write_kind * nat * nat * monad 'regval 'a 'e
   (* Request the result of store-exclusive *)
   | Excl_res of (bool -> monad 'regval 'a 'e)
   (* Request to write a memory value of the given size together with a tag
      at the given address. *)
-  | Write_mem of write_kind * address * nat * list memory_byte * bitU * (bool -> monad 'regval 'a 'e)
+  | Write_mem of write_kind * nat * nat * list memory_byte * bitU * (bool -> monad 'regval 'a 'e)
   (* Tell the system to dynamically recalculate dependency footprint *)
   | Footprint of monad 'regval 'a 'e
   (* Request a memory barrier *)
@@ -37,9 +38,9 @@ type monad 'regval 'a 'e =
   | Exception of 'e
 
 type event 'regval =
-  | E_read_mem of read_kind * address * nat * (list memory_byte * bitU)
-  | E_write_mem of write_kind * address * nat * list memory_byte * bitU * bool
-  | E_write_ea of write_kind * address * nat
+  | E_read_mem of read_kind * nat * nat * (list memory_byte * bitU)
+  | E_write_mem of write_kind * nat * nat * list memory_byte * bitU * bool
+  | E_write_ea of write_kind * nat * nat
   | E_excl_res of bool
   | E_barrier of barrier_kind
   | E_footprint
@@ -136,7 +137,9 @@ end
 
 val read_mem_bytes : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monad 'rv (list memory_byte * bitU) 'e
 let read_mem_bytes rk addr sz =
-  Read_mem rk (bits_of addr) (nat_of_int sz) return
+  bind
+    (maybe_fail "nat_of_bv" (nat_of_bv addr))
+    (fun addr -> Read_mem rk addr (nat_of_int sz) return)
 
 val read_mem : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monad 'rv ('b * bitU) 'e
 let read_mem rk addr sz =
@@ -154,14 +157,19 @@ let excl_result () =
   Excl_res k
 
 val write_mem_ea : forall 'rv 'a 'e. Bitvector 'a => write_kind -> 'a -> integer -> monad 'rv unit 'e
-let write_mem_ea wk addr sz = Write_ea wk (bits_of addr) (nat_of_int sz) (Done ())
+let write_mem_ea wk addr sz =
+  bind
+    (maybe_fail "nat_of_bv" (nat_of_bv addr))
+    (fun addr -> Write_ea wk addr (nat_of_int sz) (Done ()))
 
 val write_mem : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b =>
   write_kind -> 'a -> integer -> 'b -> bitU -> monad 'rv bool 'e
-let write_mem wk addr sz v tag = match mem_bytes_of_bits v with
-  | Just v -> Write_mem wk (bits_of addr) (nat_of_int sz) v tag return
-  | Nothing -> Fail "write_mem"
-end
+let write_mem wk addr sz v tag =
+  match (mem_bytes_of_bits v, nat_of_bv addr) with
+    | (Just v, Just addr) ->
+       Write_mem wk addr (nat_of_int sz) v tag return
+    | _ -> Fail "write_mem"
+  end
 
 val read_reg : forall 's 'rv 'a 'e. register_ref 's 'rv 'a -> monad 'rv 'a 'e
 let read_reg reg =
diff --git a/src/gen_lib/sail2_state_lifting.lem b/src/gen_lib/sail2_state_lifting.lem
index 314c562d..3cc396f2 100644
--- a/src/gen_lib/sail2_state_lifting.lem
+++ b/src/gen_lib/sail2_state_lifting.lem
@@ -28,12 +28,10 @@ let rec runTraceS ra t s =
   match t with
   | [] -> Just s
   | E_read_mem _ addr sz (v, tag) :: t' ->
-     Maybe.bind (unsigned addr) (fun addr ->
      Maybe.bind (get_mem_bytes addr sz s) (fun (v', tag') ->
-     if v' = v && tag' = tag then runTraceS ra t' s else Nothing))
+     if v' = v && tag' = tag then runTraceS ra t' s else Nothing)
   | E_write_mem _ addr sz v tag _ :: t' ->
-     Maybe.bind (unsigned addr) (fun addr ->
-     runTraceS ra t' (put_mem_bytes addr sz v tag s))
+     runTraceS ra t' (put_mem_bytes addr sz v tag s)
   | E_read_reg r v :: t' ->
      let (read_reg, _) = ra in
      Maybe.bind (read_reg r s.regstate) (fun v' ->
diff --git a/src/gen_lib/sail2_state_monad.lem b/src/gen_lib/sail2_state_monad.lem
index 84ae86d8..6c1cd4bd 100644
--- a/src/gen_lib/sail2_state_monad.lem
+++ b/src/gen_lib/sail2_state_monad.lem
@@ -4,8 +4,8 @@ open import Sail2_values
 
 (* 'a is result type *)
 
-type memstate = map integer memory_byte
-type tagstate = map integer bitU
+type memstate = map nat memory_byte
+type tagstate = map nat bitU
 (* type regstate = map string (vector bitU) *)
 
 type sequential_state 'regs =
@@ -116,31 +116,30 @@ end
 
 val read_tagS : forall 'regs 'a 'e. Bitvector 'a => 'a -> monadS 'regs bitU 'e
 let read_tagS addr =
-  maybe_failS "unsigned" (unsigned addr) >>$= (fun addr ->
+  maybe_failS "nat_of_bv" (nat_of_bv addr) >>$= (fun addr ->
   readS (fun s -> fromMaybe B0 (Map.lookup addr s.tagstate)))
 
 (* Read bytes from memory and return in little endian order *)
-val get_mem_bytes : forall 'regs. integer -> nat -> sequential_state 'regs -> maybe (list memory_byte * bitU)
+val get_mem_bytes : forall 'regs. nat -> nat -> sequential_state 'regs -> maybe (list memory_byte * bitU)
 let get_mem_bytes addr sz s =
-  let sz = integerFromNat sz in
-  let addrs = index_list addr (addr+sz-1) 1 in
+  let addrs = genlist (fun n -> addr + n) sz in
   let read_byte s addr = Map.lookup addr s.memstate in
   let read_tag s addr = Map.findWithDefault addr B0 s.tagstate in
   Maybe.map
     (fun mem_val -> (mem_val, List.foldl and_bit B1 (List.map (read_tag s) addrs)))
     (just_list (List.map (read_byte s) addrs))
 
-val read_mem_bytesS : forall 'regs 'e 'a. Bitvector 'a => read_kind -> 'a -> nat -> monadS 'regs (list memory_byte * bitU) 'e
+val read_mem_bytesS : forall 'regs 'e. read_kind -> nat -> nat -> monadS 'regs (list memory_byte * bitU) 'e
 let read_mem_bytesS _ addr sz =
-  maybe_failS "unsigned" (unsigned addr) >>$= (fun addr ->
   readS (get_mem_bytes addr sz) >>$=
-  maybe_failS "read_memS")
+  maybe_failS "read_memS"
 
 val read_memS : forall 'regs 'e 'a 'b. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monadS 'regs ('b * bitU) 'e
 let read_memS rk a sz =
+  maybe_failS "nat_of_bv" (nat_of_bv a) >>$= (fun a ->
   read_mem_bytesS rk a (nat_of_int sz) >>$= (fun (bytes, tag) ->
   maybe_failS "bits_of_mem_bytes" (of_bits (bits_of_mem_bytes bytes)) >>$= (fun mem_val ->
-  returnS (mem_val, tag)))
+  returnS (mem_val, tag))))
 
 val excl_resultS : forall 'regs 'e. unit -> monadS 'regs bool 'e
 let excl_resultS =
@@ -151,28 +150,27 @@ let excl_resultS =
   undefined_boolS
 
 (* Write little-endian list of bytes to given address *)
-val put_mem_bytes : forall 'regs. integer -> nat -> list memory_byte -> bitU -> sequential_state 'regs -> sequential_state 'regs
+val put_mem_bytes : forall 'regs. nat -> nat -> list memory_byte -> bitU -> sequential_state 'regs -> sequential_state 'regs
 let put_mem_bytes addr sz v t s =
-  let sz = integerFromNat sz in
-  let addrs = index_list addr (addr+sz-1) 1 in
+  let addrs = genlist (fun n -> addr + n) sz in
   let a_v = List.zip addrs v in
   let write_byte mem (addr, v) = Map.insert addr v mem in
   let write_tag mem addr = Map.insert addr t mem in
   <| s with memstate = List.foldl write_byte s.memstate a_v;
             tagstate = List.foldl write_tag s.tagstate addrs |>
 
-val write_mem_bytesS : forall 'regs 'e 'a. Bitvector 'a => write_kind -> 'a -> nat -> list memory_byte -> bitU -> monadS 'regs bool 'e
+val write_mem_bytesS : forall 'regs 'e. write_kind -> nat -> nat -> list memory_byte -> bitU -> monadS 'regs bool 'e
 let write_mem_bytesS _ addr sz v t =
-  maybe_failS "unsigned" (unsigned addr) >>$= (fun addr ->
   updateS (put_mem_bytes addr sz v t) >>$
-  returnS true)
+  returnS true
 
 val write_memS : forall 'regs 'e 'a 'b. Bitvector 'a, Bitvector 'b =>
   write_kind -> 'a -> nat -> 'b -> bitU -> monadS 'regs bool 'e
-let write_memS wk addr sz v t = match mem_bytes_of_bits v with
-  | Just v -> write_mem_bytesS wk addr sz v t
-  | Nothing -> failS "write_mem"
-end
+let write_memS wk addr sz v t =
+  match (nat_of_bv addr, mem_bytes_of_bits v) with
+    | (Just addr, Just v) -> write_mem_bytesS wk addr sz v t
+    | _ -> failS "write_mem"
+  end
 
 val read_regS : forall 'regs 'rv 'a 'e. register_ref 'regs 'rv 'a -> monadS 'regs 'a 'e
 let read_regS reg = readS (fun s -> reg.read_from s.regstate)
diff --git a/src/gen_lib/sail2_values.lem b/src/gen_lib/sail2_values.lem
index 8957f0dd..fa1e8426 100644
--- a/src/gen_lib/sail2_values.lem
+++ b/src/gen_lib/sail2_values.lem
@@ -625,6 +625,9 @@ let extz_bv n v = extz_bits n (bits_of v)
 val exts_bv : forall 'a. Bitvector 'a => integer -> 'a -> list bitU
 let exts_bv n v = exts_bits n (bits_of v)
 
+val nat_of_bv : forall 'a. Bitvector 'a => 'a -> maybe nat
+let nat_of_bv v = Maybe.map nat_of_int (unsigned v)
+
 val string_of_bv : forall 'a. Bitvector 'a => 'a -> string
 let string_of_bv v = show_bitlist (bits_of v)
 
-- 
cgit v1.2.3


From c0f8dd2e676c4ce987c73392506dff8872a364ef Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Thu, 29 Nov 2018 15:13:50 +0000
Subject: Add some helper lemmas to Isabelle lib

---
 lib/isabelle/Sail2_state_lemmas.thy  | 121 ++++++++++++++++++++++++++++++++++-
 lib/isabelle/Sail2_values_lemmas.thy |  28 ++++++++
 src/gen_lib/sail2_prompt_monad.lem   |   2 +
 src/gen_lib/sail2_state_lifting.lem  |  34 ++++++----
 4 files changed, 170 insertions(+), 15 deletions(-)

diff --git a/lib/isabelle/Sail2_state_lemmas.thy b/lib/isabelle/Sail2_state_lemmas.thy
index edcd9593..c7d55d31 100644
--- a/lib/isabelle/Sail2_state_lemmas.thy
+++ b/lib/isabelle/Sail2_state_lemmas.thy
@@ -2,6 +2,8 @@ theory Sail2_state_lemmas
   imports Sail2_state Sail2_state_lifting
 begin
 
+text \<open>Monad lifting\<close>
+
 lemma All_liftState_dom: "liftState_dom (r, m)"
   by (induction m) (auto intro: liftState.domintros)
 termination liftState using All_liftState_dom by auto
@@ -309,7 +311,7 @@ proof (use assms in \<open>induction vars "liftState r \<circ> cond" "liftState
   qed auto
 qed
 
-(* Simplification rules for monadic Boolean connectives *)
+text \<open>Simplification rules for monadic Boolean connectives\<close>
 
 lemma if_return_return[simp]: "(if a then return True else return False) = return a" by auto
 
@@ -392,4 +394,121 @@ lemma Run_and_boolM_E:
 lemma maybe_failS_Some[simp]: "maybe_failS msg (Some v) = returnS v"
   by (auto simp: maybe_failS_def)
 
+text \<open>Event traces\<close>
+
+lemma Some_eq_bind_conv: "Some x = Option.bind f g \<longleftrightarrow> (\<exists>y. f = Some y \<and> g y = Some x)"
+  unfolding bind_eq_Some_conv[symmetric] by auto
+
+lemma if_then_Some_eq_Some: "((if b then Some x else None) = Some y) \<longleftrightarrow> (b \<and> y = x)"
+  by auto
+
+lemma emitEventS_update_cases:
+  assumes "emitEventS ra e s = Some s'"
+  obtains
+    (Write_mem) wk addr sz v tag r
+      where "e = E_write_mem wk addr sz v tag r"
+        and "s' = put_mem_bytes addr sz v tag s"
+  | (Write_reg) r v rs'
+      where "e = E_write_reg r v" and "(snd ra) r v (regstate s) = Some rs'"
+        and "s' = s\<lparr>regstate := rs'\<rparr>"
+  | (Read) "s' = s"
+  using assms
+  by (elim emitEventS.elims) (auto simp: Some_eq_bind_conv bind_eq_Some_conv if_then_Some_eq_Some)
+
+lemma runTraceS_singleton[simp]: "runTraceS ra [e] s = emitEventS ra e s"
+  by (cases "emitEventS ra e s"; auto)
+
+lemma runTraceS_ConsE:
+  assumes "runTraceS ra (e # t) s = Some s'"
+  obtains s'' where "emitEventS ra e s = Some s''" and "runTraceS ra t s'' = Some s'"
+  using assms by (auto simp: bind_eq_Some_conv)
+
+lemma runTraceS_ConsI:
+  assumes "emitEventS ra e s = Some s'" and "runTraceS ra t s' = Some s''"
+  shows "runTraceS ra (e # t) s = Some s''"
+  using assms by auto
+
+lemma runTraceS_Cons_tl:
+  assumes "emitEventS ra e s = Some s'"
+  shows "runTraceS ra (e # t) s = runTraceS ra t s'"
+  using assms by (elim emitEventS.elims) (auto simp: Some_eq_bind_conv bind_eq_Some_conv)
+
+lemma runTraceS_appendE:
+  assumes "runTraceS ra (t @ t') s = Some s'"
+  obtains s'' where "runTraceS ra t s = Some s''" and "runTraceS ra t' s'' = Some s'"
+proof -
+  have "\<exists>s''. runTraceS ra t s = Some s'' \<and> runTraceS ra t' s'' = Some s'"
+  proof (use assms in \<open>induction t arbitrary: s\<close>)
+    case (Cons e t)
+    from Cons.prems
+    obtain s_e where "emitEventS ra e s = Some s_e" and "runTraceS ra (t @ t') s_e = Some s'"
+      by (auto elim: runTraceS_ConsE simp: bind_eq_Some_conv)
+    with Cons.IH[of s_e] show ?case by (auto intro: runTraceS_ConsI)
+  qed auto
+  then show ?thesis using that by blast
+qed
+
+lemma runTraceS_nth_split:
+  assumes "runTraceS ra t s = Some s'" and n: "n < length t"
+  obtains s1 s2 where "runTraceS ra (take n t) s = Some s1"
+    and "emitEventS ra (t ! n) s1 = Some s2"
+    and "runTraceS ra (drop (Suc n) t) s2 = Some s'"
+proof -
+  have "runTraceS ra (take n t @ t ! n # drop (Suc n) t) s = Some s'"
+    using assms
+    by (auto simp: id_take_nth_drop[OF n, symmetric])
+  then show thesis by (blast elim: runTraceS_appendE runTraceS_ConsE intro: that)
+qed
+
+text \<open>Memory accesses\<close>
+
+lemma get_mem_bytes_put_mem_bytes_same_addr:
+  assumes "length v = sz"
+  shows "get_mem_bytes addr sz (put_mem_bytes addr sz v tag s) = Some (v, if sz > 0 then tag else B1)"
+proof (unfold assms[symmetric], induction v rule: rev_induct)
+  case Nil
+  then show ?case by (auto simp: get_mem_bytes_def)
+next
+  case (snoc x xs)
+  then show ?case
+    by (cases tag)
+       (auto simp: get_mem_bytes_def put_mem_bytes_def Let_def and_bit_eq_iff foldl_and_bit_eq_iff
+             cong: option.case_cong split: if_splits option.splits)
+qed
+
+lemma memstate_put_mem_bytes:
+  assumes "length v = sz"
+  shows "memstate (put_mem_bytes addr sz v tag s) addr' =
+         (if addr' \<in> {addr..<addr+sz} then Some (v ! (addr' - addr)) else memstate s addr')"
+  unfolding assms[symmetric]
+  by (induction v rule: rev_induct) (auto simp: put_mem_bytes_def nth_Cons nth_append Let_def)
+
+lemma tagstate_put_mem_bytes:
+  assumes "length v = sz"
+  shows "tagstate (put_mem_bytes addr sz v tag s) addr' =
+         (if addr' \<in> {addr..<addr+sz} then Some tag else tagstate s addr')"
+  unfolding assms[symmetric]
+  by (induction v rule: rev_induct) (auto simp: put_mem_bytes_def nth_Cons nth_append Let_def)
+
+lemma get_mem_bytes_cong:
+  assumes "\<forall>addr'. addr \<le> addr' \<and> addr' < addr + sz \<longrightarrow>
+                   (memstate s' addr' = memstate s addr' \<and> tagstate s' addr' = tagstate s addr')"
+  shows "get_mem_bytes addr sz s' = get_mem_bytes addr sz s"
+proof (use assms in \<open>induction sz\<close>)
+  case 0
+  then show ?case by (auto simp: get_mem_bytes_def)
+next
+  case (Suc sz)
+  then show ?case
+    by (auto simp: get_mem_bytes_def Let_def
+             intro!: map_option_cong map_cong foldl_cong
+                     arg_cong[where f = just_list] arg_cong2[where f = and_bit])
+qed
+
+lemma get_mem_bytes_tagged_tagstate:
+  assumes "get_mem_bytes addr sz s = Some (v, B1)"
+  shows "\<forall>addr' \<in> {addr..<addr + sz}. tagstate s addr' = Some B1"
+  using assms
+  by (auto simp: get_mem_bytes_def foldl_and_bit_eq_iff Let_def split: option.splits)
+
 end
diff --git a/lib/isabelle/Sail2_values_lemmas.thy b/lib/isabelle/Sail2_values_lemmas.thy
index 576cd8ea..27a6952f 100644
--- a/lib/isabelle/Sail2_values_lemmas.thy
+++ b/lib/isabelle/Sail2_values_lemmas.thy
@@ -123,6 +123,9 @@ lemma nth_upto[simp]: "i + int n \<le> j \<Longrightarrow> [i..j] ! n = i + int
 
 declare index_list.simps[simp del]
 
+lemma genlist_add_upt[simp]: "genlist ((+) start) len = [start..<start + len]"
+  by (auto simp: genlist_def map_add_upt add.commute cong: map_cong)
+
 lemma just_list_map_Some[simp]: "just_list (map Some v) = Some v" by (induction v) auto
 
 lemma just_list_None_iff[simp]: "just_list xs = None \<longleftrightarrow> None \<in> set xs"
@@ -151,6 +154,31 @@ next
   then show ?case by (auto simp: repeat.simps)
 qed
 
+lemma and_bit_B1[simp]: "and_bit B1 b = b"
+  by (cases b) auto
+
+lemma and_bit_idem[simp]: "and_bit b b = b"
+  by (cases b) auto
+
+lemma and_bit_eq_iff:
+  "and_bit b b' = B0 \<longleftrightarrow> (b = B0 \<or> b' = B0)"
+  "and_bit b b' = BU \<longleftrightarrow> (b = BU \<or> b' = BU) \<and> b \<noteq> B0 \<and> b' \<noteq> B0"
+  "and_bit b b' = B1 \<longleftrightarrow> (b = B1 \<and> b' = B1)"
+  by (cases b; cases b'; auto)+
+
+lemma foldl_and_bit_eq_iff:
+  shows "foldl and_bit b bs = B0 \<longleftrightarrow> (b = B0 \<or> B0 \<in> set bs)" (is ?B0)
+    and "foldl and_bit b bs = B1 \<longleftrightarrow> (b = B1 \<and> set bs \<subseteq> {B1})" (is ?B1)
+    and "foldl and_bit b bs = BU \<longleftrightarrow> (b = BU \<or> BU \<in> set bs) \<and> b \<noteq> B0 \<and> B0 \<notin> set bs" (is ?BU)
+proof -
+  have "?B0 \<and> ?B1 \<and> ?BU"
+  proof (induction bs arbitrary: b)
+    case (Cons b' bs)
+    show ?case using Cons.IH by (cases b; cases b') auto
+  qed auto
+  then show ?B0 and ?B1 and ?BU by auto
+qed
+
 lemma bool_of_bitU_simps[simp]:
   "bool_of_bitU B0 = Some False"
   "bool_of_bitU B1 = Some True"
diff --git a/src/gen_lib/sail2_prompt_monad.lem b/src/gen_lib/sail2_prompt_monad.lem
index ae1f2cd8..7503ca22 100644
--- a/src/gen_lib/sail2_prompt_monad.lem
+++ b/src/gen_lib/sail2_prompt_monad.lem
@@ -258,6 +258,8 @@ let rec runTrace t m = match t with
   | e :: t' -> Maybe.bind (emitEvent m e) (runTrace t')
 end
 
+declare {isabelle} termination_argument runTrace = automatic
+
 val final : forall 'regval 'a 'e. monad 'regval 'a 'e -> bool
 let final = function
   | Done _ -> true
diff --git a/src/gen_lib/sail2_state_lifting.lem b/src/gen_lib/sail2_state_lifting.lem
index 3cc396f2..0e7addbb 100644
--- a/src/gen_lib/sail2_state_lifting.lem
+++ b/src/gen_lib/sail2_state_lifting.lem
@@ -23,22 +23,28 @@ let rec liftState ra m = match m with
   | (Exception e)             -> throwS e
 end
 
-val runTraceS : forall 'regval 'regs 'a 'e. Eq 'regval => register_accessors 'regs 'regval -> trace 'regval -> sequential_state 'regs -> maybe (sequential_state 'regs)
-let rec runTraceS ra t s =
-  match t with
-  | [] -> Just s
-  | E_read_mem _ addr sz (v, tag) :: t' ->
+val emitEventS : forall 'regval 'regs 'a 'e. Eq 'regval => register_accessors 'regs 'regval -> event 'regval -> sequential_state 'regs -> maybe (sequential_state 'regs)
+let emitEventS ra e s = match e with
+  | E_read_mem _ addr sz (v, tag) ->
      Maybe.bind (get_mem_bytes addr sz s) (fun (v', tag') ->
-     if v' = v && tag' = tag then runTraceS ra t' s else Nothing)
-  | E_write_mem _ addr sz v tag _ :: t' ->
-     runTraceS ra t' (put_mem_bytes addr sz v tag s)
-  | E_read_reg r v :: t' ->
+     if v' = v && tag' = tag then Just s else Nothing)
+  | E_write_mem _ addr sz v tag _ ->
+     Just (put_mem_bytes addr sz v tag s)
+  | E_read_reg r v ->
      let (read_reg, _) = ra in
      Maybe.bind (read_reg r s.regstate) (fun v' ->
-     if v' = v then runTraceS ra t' s else Nothing)
-  | E_write_reg r v :: t' ->
+     if v' = v then Just s else Nothing)
+  | E_write_reg r v ->
      let (_, write_reg) = ra in
-     Maybe.bind (write_reg r v s.regstate) (fun s' ->
-     runTraceS ra t' <| s with regstate = s' |>)
-  | _ :: t' -> runTraceS ra t' s
+     Maybe.bind (write_reg r v s.regstate) (fun rs' ->
+     Just <| s with regstate = rs' |>)
+  | _ -> Just s
 end
+
+val runTraceS : forall 'regval 'regs 'a 'e. Eq 'regval => register_accessors 'regs 'regval -> trace 'regval -> sequential_state 'regs -> maybe (sequential_state 'regs)
+let rec runTraceS ra t s = match t with
+  | [] -> Just s
+  | e :: t' -> Maybe.bind (emitEventS ra e s) (runTraceS ra t')
+end
+
+declare {isabelle} termination_argument runTraceS = automatic
-- 
cgit v1.2.3


From 17334803f125e3b839fdb7a780989d8eba555555 Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Thu, 29 Nov 2018 17:58:15 +0000
Subject: Add separate outcome/event for tagged memory loads

Lets one distinguish in a trace whether an instruction tried to read
tagged memory or just read data without caring about the tag;  this is
useful for formulating predicates on traces.
---
 lib/isabelle/Sail2_prompt_monad_lemmas.thy |  6 ++-
 lib/isabelle/Sail2_state_lemmas.thy        | 27 ++++++----
 lib/isabelle/Sail2_state_monad_lemmas.thy  | 14 ++---
 src/gen_lib/sail2_prompt_monad.lem         | 82 +++++++++++++++++++-----------
 src/gen_lib/sail2_state_lifting.lem        | 36 +++++++------
 src/gen_lib/sail2_state_monad.lem          | 20 ++++++--
 6 files changed, 113 insertions(+), 72 deletions(-)

diff --git a/lib/isabelle/Sail2_prompt_monad_lemmas.thy b/lib/isabelle/Sail2_prompt_monad_lemmas.thy
index 406b5871..c59fc62f 100644
--- a/lib/isabelle/Sail2_prompt_monad_lemmas.thy
+++ b/lib/isabelle/Sail2_prompt_monad_lemmas.thy
@@ -32,6 +32,7 @@ lemmas try_catch_induct[case_names Done Read_mem Write_memv Read_reg Excl_res Wr
 
 inductive_set T :: "(('rv, 'a, 'e) monad \<times> 'rv event \<times> ('rv, 'a, 'e) monad) set" where
   Read_mem: "((Read_mem rk addr sz k), E_read_mem rk addr sz v, k v) \<in> T"
+| Read_tagged_mem: "((Read_tagged_mem rk addr sz k), E_read_tagged_mem rk addr sz v, k v) \<in> T"
 | Write_ea: "((Write_ea wk addr sz k), E_write_ea wk addr sz, k) \<in> T"
 | Excl_res: "((Excl_res k), E_excl_res r, k r) \<in> T"
 | Write_mem: "((Write_mem wk addr sz v t k), E_write_mem wk addr sz v t r, k r) \<in> T"
@@ -60,7 +61,8 @@ lemma Traces_cases:
   fixes m :: "('rv, 'a, 'e) monad"
   assumes Run: "(m, t, m') \<in> Traces"
   obtains (Nil) a where "m = m'" and "t = []"
-  | (Read_mem) rk addr s k t' v tag where "m = Read_mem rk addr s k" and "t = E_read_mem rk addr s (v, tag) # t'" and "(k (v, tag), t', m') \<in> Traces"
+  | (Read_mem) rk addr s k t' v where "m = Read_mem rk addr s k" and "t = E_read_mem rk addr s v # t'" and "(k v, t', m') \<in> Traces"
+  | (Read_tagged_mem) rk addr s k t' v tag where "m = Read_tagged_mem rk addr s k" and "t = E_read_tagged_mem rk addr s (v, tag) # t'" and "(k (v, tag), t', m') \<in> Traces"
   | (Write_mem) wk addr sz val tag k t' v where "m = Write_mem wk addr sz val tag k" and "t = E_write_mem wk addr sz val tag v # t'" and "(k v, t', m') \<in> Traces"
   | (Barrier) bk k t' v where "m = Barrier bk k" and "t = E_barrier bk # t'" and "(k, t', m') \<in> Traces"
   | (Read_reg) reg k t' v where "m = Read_reg reg k" and "t = E_read_reg reg v # t'" and "(k v, t', m') \<in> Traces"
@@ -79,7 +81,7 @@ next
   note m' = \<open>(m'', t', m') \<in> Traces\<close>
   from \<open>(m, e, m'') \<in> T\<close> and t and m'
   show ?thesis proof (cases m e m'' rule: T.cases)
-    case (Read_mem rk addr sz k v)
+    case (Read_tagged_mem rk addr sz k v)
     then show ?thesis using t m' by (cases v; elim that; blast)
   qed (elim that; blast)+
 qed
diff --git a/lib/isabelle/Sail2_state_lemmas.thy b/lib/isabelle/Sail2_state_lemmas.thy
index c7d55d31..77f4ac5a 100644
--- a/lib/isabelle/Sail2_state_lemmas.thy
+++ b/lib/isabelle/Sail2_state_lemmas.thy
@@ -80,19 +80,20 @@ lemma liftState_bool_of_bitU_nondet[liftState_simp]:
   "liftState r (bool_of_bitU_nondet b) = bool_of_bitU_nondetS b"
   by (cases b; auto simp: bool_of_bitU_nondet_def bool_of_bitU_nondetS_def liftState_simp)
 
-lemma liftState_read_mem_BC:
-  assumes "unsigned_method BC_bitU_list (bits_of_method BCa a) = unsigned_method BCa a"
-  shows "liftState r (read_mem BCa BCb rk a sz) = read_memS BCa BCb rk a sz"
-  using assms
-  by (auto simp: read_mem_def read_mem_bytes_def read_memS_def read_mem_bytesS_def maybe_failS_def
+lemma liftState_read_tagged_mem[liftState_simp]:
+  shows "liftState r (read_tagged_mem BCa BCb rk a sz) = read_tagged_memS BCa BCb rk a sz"
+  by (auto simp: read_tagged_mem_def read_tagged_mem_bytes_def maybe_failS_def read_tagged_memS_def
                  prod.case_distrib option.case_distrib[where h = "liftState r"]
                  option.case_distrib[where h = "\<lambda>c. c \<bind>\<^sub>S f" for f] liftState_simp
-           cong: option.case_cong)
+           split: option.splits intro: bindS_cong)
 
 lemma liftState_read_mem[liftState_simp]:
-  "\<And>a. liftState r (read_mem BC_mword BC_mword rk a sz) = read_memS BC_mword BC_mword rk a sz"
-  "\<And>a. liftState r (read_mem BC_bitU_list BC_bitU_list rk a sz) = read_memS BC_bitU_list BC_bitU_list rk a sz"
-  by (auto simp: liftState_read_mem_BC)
+  shows "liftState r (read_mem BCa BCb rk a sz) = read_memS BCa BCb rk a sz"
+  by (auto simp: read_mem_def read_mem_bytes_def read_memS_def read_mem_bytesS_def maybe_failS_def
+                 read_tagged_memS_def
+                 prod.case_distrib option.case_distrib[where h = "liftState r"]
+                 option.case_distrib[where h = "\<lambda>c. c \<bind>\<^sub>S f" for f] liftState_simp
+           split: option.splits intro: bindS_cong)
 
 lemma liftState_write_mem_ea_BC:
   assumes "unsigned_method BCa a = Some a'"
@@ -399,7 +400,10 @@ text \<open>Event traces\<close>
 lemma Some_eq_bind_conv: "Some x = Option.bind f g \<longleftrightarrow> (\<exists>y. f = Some y \<and> g y = Some x)"
   unfolding bind_eq_Some_conv[symmetric] by auto
 
-lemma if_then_Some_eq_Some: "((if b then Some x else None) = Some y) \<longleftrightarrow> (b \<and> y = x)"
+lemma if_then_Some_eq_Some_iff: "((if b then Some x else None) = Some y) \<longleftrightarrow> (b \<and> y = x)"
+  by auto
+
+lemma Some_eq_if_then_Some_iff: "(Some y = (if b then Some x else None)) \<longleftrightarrow> (b \<and> y = x)"
   by auto
 
 lemma emitEventS_update_cases:
@@ -413,7 +417,8 @@ lemma emitEventS_update_cases:
         and "s' = s\<lparr>regstate := rs'\<rparr>"
   | (Read) "s' = s"
   using assms
-  by (elim emitEventS.elims) (auto simp: Some_eq_bind_conv bind_eq_Some_conv if_then_Some_eq_Some)
+  by (elim emitEventS.elims)
+     (auto simp: Some_eq_bind_conv bind_eq_Some_conv if_then_Some_eq_Some_iff Some_eq_if_then_Some_iff)
 
 lemma runTraceS_singleton[simp]: "runTraceS ra [e] s = emitEventS ra e s"
   by (cases "emitEventS ra e s"; auto)
diff --git a/lib/isabelle/Sail2_state_monad_lemmas.thy b/lib/isabelle/Sail2_state_monad_lemmas.thy
index 6fb5e7ef..12452ca4 100644
--- a/lib/isabelle/Sail2_state_monad_lemmas.thy
+++ b/lib/isabelle/Sail2_state_monad_lemmas.thy
@@ -211,22 +211,22 @@ lemma ignore_throw_let_distrib: "ignore_throw (let x = y in f x) = (let x = y in
   by auto
 
 lemma no_throw_mem_builtins:
-  "\<And>BC rk a sz s. ignore_throw (read_mem_bytesS rk a sz) s = read_mem_bytesS rk a sz s"
+  "\<And>rk a sz s. ignore_throw (read_mem_bytesS rk a sz) s = read_mem_bytesS rk a sz s"
+  "\<And>rk a sz s. ignore_throw (read_tagged_mem_bytesS rk a sz) s = read_tagged_mem_bytesS rk a sz s"
   "\<And>BC a s. ignore_throw (read_tagS BC a) s = read_tagS BC a s"
+  "\<And>BCa BCv rk a sz s. ignore_throw (read_memS BCa BCv rk a sz) s = read_memS BCa BCv rk a sz s"
+  "\<And>BCa BCv rk a sz s. ignore_throw (read_tagged_memS BCa BCv rk a sz) s = read_tagged_memS BCa BCv rk a sz s"
   "\<And>BC wk addr sz v t s. ignore_throw (write_mem_bytesS wk addr sz v t) s = write_mem_bytesS wk addr sz v t s"
-  "\<And>BC_a BC_v wk addr sz v t s. ignore_throw (write_memS BC_a BC_v wk addr sz v t) s = write_memS BC_a BC_v wk addr sz v t s"
+  "\<And>BCa BCv wk addr sz v t s. ignore_throw (write_memS BCa BCv wk addr sz v t) s = write_memS BCa BCv wk addr sz v t s"
   "\<And>s. ignore_throw (excl_resultS ()) s = excl_resultS () s"
   "\<And>s. ignore_throw (undefined_boolS ()) s = undefined_boolS () s"
-  unfolding read_mem_bytesS_def read_memS_def read_tagS_def write_memS_def
+  unfolding read_mem_bytesS_def read_tagged_mem_bytesS_def read_tagged_memS_def read_memS_def read_tagS_def write_memS_def
   unfolding write_mem_bytesS_def
   unfolding excl_resultS_def undefined_boolS_def maybe_failS_def
   unfolding ignore_throw_bindS
   by (auto cong: bindS_cong bindS_ext_cong ignore_throw_cong option.case_cong
            simp: prod.case_distrib ignore_throw_option_case_distrib ignore_throw_let_distrib comp_def)
 
-lemma no_throw_read_memS: "ignore_throw (read_memS BCa BCb rk a sz) s = read_memS BCa BCb rk a sz s"
-  by (auto simp: read_memS_def no_throw_mem_builtins prod.case_distrib comp_def cong: bindS_ext_cong)
-
 lemma no_throw_read_regvalS: "ignore_throw (read_regvalS r reg_name) s = read_regvalS r reg_name s"
   by (cases r) (auto simp: option.case_distrib cong: bindS_cong option.case_cong)
 
@@ -234,7 +234,7 @@ lemma no_throw_write_regvalS: "ignore_throw (write_regvalS r reg_name v) s = wri
   by (cases r) (auto simp: option.case_distrib cong: bindS_cong option.case_cong)
 
 lemmas no_throw_builtins[simp] =
-  no_throw_mem_builtins no_throw_read_regvalS no_throw_write_regvalS no_throw_read_memS
+  no_throw_mem_builtins no_throw_read_regvalS no_throw_write_regvalS
 
 (* end *)
 
diff --git a/src/gen_lib/sail2_prompt_monad.lem b/src/gen_lib/sail2_prompt_monad.lem
index 7503ca22..079375a3 100644
--- a/src/gen_lib/sail2_prompt_monad.lem
+++ b/src/gen_lib/sail2_prompt_monad.lem
@@ -9,9 +9,10 @@ type address = list bitU
 type monad 'regval 'a 'e =
   | Done of 'a
   (* Read a number of bytes from memory, returned in little endian order,
-     together with a tag.  The first nat specifies the address, the second
+     with or without a tag.  The first nat specifies the address, the second
      the number of bytes. *)
-  | Read_mem of read_kind * nat * nat * ((list memory_byte * bitU) -> monad 'regval 'a 'e)
+  | Read_mem of read_kind * nat * nat * (list memory_byte -> monad 'regval 'a 'e)
+  | Read_tagged_mem of read_kind * nat * nat * ((list memory_byte * bitU) -> monad 'regval 'a 'e)
   (* Tell the system a write is imminent, at the given address and with the
      given size. *)
   | Write_ea of write_kind * nat * nat * monad 'regval 'a 'e
@@ -38,7 +39,8 @@ type monad 'regval 'a 'e =
   | Exception of 'e
 
 type event 'regval =
-  | E_read_mem of read_kind * nat * nat * (list memory_byte * bitU)
+  | E_read_mem of read_kind * nat * nat * list memory_byte
+  | E_read_tagged_mem of read_kind * nat * nat * (list memory_byte * bitU)
   | E_write_mem of write_kind * nat * nat * list memory_byte * bitU * bool
   | E_write_ea of write_kind * nat * nat
   | E_excl_res of bool
@@ -57,18 +59,19 @@ let return a = Done a
 val bind : forall 'rv 'a 'b 'e. monad 'rv 'a 'e -> ('a -> monad 'rv 'b 'e) -> monad 'rv 'b 'e
 let rec bind m f = match m with
   | Done a -> f a
-  | Read_mem rk a sz k ->      Read_mem rk a sz      (fun v -> bind (k v) f)
-  | Write_mem wk a sz v t k -> Write_mem wk a sz v t (fun v -> bind (k v) f)
-  | Read_reg descr k ->        Read_reg descr        (fun v -> bind (k v) f)
-  | Excl_res k ->              Excl_res              (fun v -> bind (k v) f)
-  | Undefined k ->             Undefined             (fun v -> bind (k v) f)
-  | Write_ea wk a sz k ->      Write_ea wk a sz      (bind k f)
-  | Footprint k ->             Footprint             (bind k f)
-  | Barrier bk k ->            Barrier bk            (bind k f)
-  | Write_reg r v k ->         Write_reg r v         (bind k f)
-  | Print msg k ->             Print msg             (bind k f)
-  | Fail descr ->              Fail descr
-  | Exception e ->             Exception e
+  | Read_mem rk a sz k ->        Read_mem rk a sz        (fun v -> bind (k v) f)
+  | Read_tagged_mem rk a sz k -> Read_tagged_mem rk a sz (fun v -> bind (k v) f)
+  | Write_mem wk a sz v t k ->   Write_mem wk a sz v t   (fun v -> bind (k v) f)
+  | Read_reg descr k ->          Read_reg descr          (fun v -> bind (k v) f)
+  | Excl_res k ->                Excl_res                (fun v -> bind (k v) f)
+  | Undefined k ->               Undefined               (fun v -> bind (k v) f)
+  | Write_ea wk a sz k ->        Write_ea wk a sz        (bind k f)
+  | Footprint k ->               Footprint               (bind k f)
+  | Barrier bk k ->              Barrier bk              (bind k f)
+  | Write_reg r v k ->           Write_reg r v           (bind k f)
+  | Print msg k ->               Print msg               (bind k f)
+  | Fail descr ->                Fail descr
+  | Exception e ->               Exception e
 end
 
 val exit : forall 'rv 'a 'e. unit -> monad 'rv 'a 'e
@@ -86,18 +89,19 @@ let throw e = Exception e
 val try_catch : forall 'rv 'a 'e1 'e2. monad 'rv 'a 'e1 -> ('e1 -> monad 'rv 'a 'e2) -> monad 'rv 'a 'e2
 let rec try_catch m h = match m with
   | Done a -> Done a
-  | Read_mem rk a sz k ->      Read_mem rk a sz      (fun v -> try_catch (k v) h)
-  | Write_mem wk a sz v t k -> Write_mem wk a sz v t (fun v -> try_catch (k v) h)
-  | Read_reg descr k ->        Read_reg descr        (fun v -> try_catch (k v) h)
-  | Excl_res k ->              Excl_res              (fun v -> try_catch (k v) h)
-  | Undefined k ->             Undefined             (fun v -> try_catch (k v) h)
-  | Write_ea wk a sz k ->      Write_ea wk a sz      (try_catch k h)
-  | Footprint k ->             Footprint             (try_catch k h)
-  | Barrier bk k ->            Barrier bk            (try_catch k h)
-  | Write_reg r v k ->         Write_reg r v         (try_catch k h)
-  | Print msg k ->             Print msg             (try_catch k h)
-  | Fail descr ->              Fail descr
-  | Exception e ->             h e
+  | Read_mem rk a sz k ->        Read_mem rk a sz        (fun v -> try_catch (k v) h)
+  | Read_tagged_mem rk a sz k -> Read_tagged_mem rk a sz (fun v -> try_catch (k v) h)
+  | Write_mem wk a sz v t k ->   Write_mem wk a sz v t   (fun v -> try_catch (k v) h)
+  | Read_reg descr k ->          Read_reg descr          (fun v -> try_catch (k v) h)
+  | Excl_res k ->                Excl_res                (fun v -> try_catch (k v) h)
+  | Undefined k ->               Undefined               (fun v -> try_catch (k v) h)
+  | Write_ea wk a sz k ->        Write_ea wk a sz        (try_catch k h)
+  | Footprint k ->               Footprint               (try_catch k h)
+  | Barrier bk k ->              Barrier bk              (try_catch k h)
+  | Write_reg r v k ->           Write_reg r v           (try_catch k h)
+  | Print msg k ->               Print msg               (try_catch k h)
+  | Fail descr ->                Fail descr
+  | Exception e ->               h e
 end
 
 (* For early return, we abuse exceptions by throwing and catching
@@ -135,19 +139,35 @@ let maybe_fail msg = function
   | Nothing -> Fail msg
 end
 
-val read_mem_bytes : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monad 'rv (list memory_byte * bitU) 'e
+val read_tagged_mem_bytes : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monad 'rv (list memory_byte * bitU) 'e
+let read_tagged_mem_bytes rk addr sz =
+  bind
+    (maybe_fail "nat_of_bv" (nat_of_bv addr))
+    (fun addr -> Read_tagged_mem rk addr (nat_of_int sz) return)
+
+val read_tagged_mem : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monad 'rv ('b * bitU) 'e
+let read_tagged_mem rk addr sz =
+  bind
+    (read_tagged_mem_bytes rk addr sz)
+    (fun (bytes, tag) ->
+       match of_bits (bits_of_mem_bytes bytes) with
+         | Just v -> return (v, tag)
+         | Nothing -> Fail "bits_of_mem_bytes"
+       end)
+
+val read_mem_bytes : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monad 'rv (list memory_byte) 'e
 let read_mem_bytes rk addr sz =
   bind
     (maybe_fail "nat_of_bv" (nat_of_bv addr))
     (fun addr -> Read_mem rk addr (nat_of_int sz) return)
 
-val read_mem : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monad 'rv ('b * bitU) 'e
+val read_mem : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monad 'rv 'b 'e
 let read_mem rk addr sz =
   bind
     (read_mem_bytes rk addr sz)
-    (fun (bytes, tag) ->
+    (fun bytes ->
        match of_bits (bits_of_mem_bytes bytes) with
-         | Just v -> return (v, tag)
+         | Just v -> return v
          | Nothing -> Fail "bits_of_mem_bytes"
        end)
 
diff --git a/src/gen_lib/sail2_state_lifting.lem b/src/gen_lib/sail2_state_lifting.lem
index 0e7addbb..07a6215b 100644
--- a/src/gen_lib/sail2_state_lifting.lem
+++ b/src/gen_lib/sail2_state_lifting.lem
@@ -8,28 +8,32 @@ open import {isabelle} `Sail2_state_monad_lemmas`
 (* Lifting from prompt monad to state monad *)
 val liftState : forall 'regval 'regs 'a 'e. register_accessors 'regs 'regval -> monad 'regval 'a 'e -> monadS 'regs 'a 'e
 let rec liftState ra m = match m with
-  | (Done a)                  -> returnS a
-  | (Read_mem rk a sz k)      -> bindS (read_mem_bytesS rk a sz)      (fun v -> liftState ra (k v))
-  | (Write_mem wk a sz v t k) -> bindS (write_mem_bytesS wk a sz v t) (fun v -> liftState ra (k v))
-  | (Read_reg r k)            -> bindS (read_regvalS ra r)            (fun v -> liftState ra (k v))
-  | (Excl_res k)              -> bindS (excl_resultS ())              (fun v -> liftState ra (k v))
-  | (Undefined k)             -> bindS (undefined_boolS ())           (fun v -> liftState ra (k v))
-  | (Write_reg r v k)         -> seqS (write_regvalS ra r v)          (liftState ra k)
-  | (Write_ea _ _ _ k)        -> liftState ra k
-  | (Footprint k)             -> liftState ra k
-  | (Barrier _ k)             -> liftState ra k
-  | (Print _ k)               -> liftState ra k (* TODO *)
-  | (Fail descr)              -> failS descr
-  | (Exception e)             -> throwS e
+  | (Done a)                    -> returnS a
+  | (Read_mem rk a sz k)        -> bindS (read_mem_bytesS rk a sz)        (fun v -> liftState ra (k v))
+  | (Read_tagged_mem rk a sz k) -> bindS (read_tagged_mem_bytesS rk a sz) (fun v -> liftState ra (k v))
+  | (Write_mem wk a sz v t k)   -> bindS (write_mem_bytesS wk a sz v t)   (fun v -> liftState ra (k v))
+  | (Read_reg r k)              -> bindS (read_regvalS ra r)              (fun v -> liftState ra (k v))
+  | (Excl_res k)                -> bindS (excl_resultS ())                (fun v -> liftState ra (k v))
+  | (Undefined k)               -> bindS (undefined_boolS ())             (fun v -> liftState ra (k v))
+  | (Write_reg r v k)           -> seqS (write_regvalS ra r v)            (liftState ra k)
+  | (Write_ea _ _ _ k)          -> liftState ra k
+  | (Footprint k)               -> liftState ra k
+  | (Barrier _ k)               -> liftState ra k
+  | (Print _ k)                 -> liftState ra k (* TODO *)
+  | (Fail descr)                -> failS descr
+  | (Exception e)               -> throwS e
 end
 
 val emitEventS : forall 'regval 'regs 'a 'e. Eq 'regval => register_accessors 'regs 'regval -> event 'regval -> sequential_state 'regs -> maybe (sequential_state 'regs)
 let emitEventS ra e s = match e with
-  | E_read_mem _ addr sz (v, tag) ->
+  | E_read_mem _ addr sz v ->
+     Maybe.bind (get_mem_bytes addr sz s) (fun (v', _) ->
+     if v' = v then Just s else Nothing)
+  | E_read_tagged_mem _ addr sz (v, tag) ->
      Maybe.bind (get_mem_bytes addr sz s) (fun (v', tag') ->
      if v' = v && tag' = tag then Just s else Nothing)
-  | E_write_mem _ addr sz v tag _ ->
-     Just (put_mem_bytes addr sz v tag s)
+  | E_write_mem _ addr sz v tag success ->
+     if success then Just (put_mem_bytes addr sz v tag s) else Nothing
   | E_read_reg r v ->
      let (read_reg, _) = ra in
      Maybe.bind (read_reg r s.regstate) (fun v' ->
diff --git a/src/gen_lib/sail2_state_monad.lem b/src/gen_lib/sail2_state_monad.lem
index 6c1cd4bd..8626052f 100644
--- a/src/gen_lib/sail2_state_monad.lem
+++ b/src/gen_lib/sail2_state_monad.lem
@@ -129,18 +129,28 @@ let get_mem_bytes addr sz s =
     (fun mem_val -> (mem_val, List.foldl and_bit B1 (List.map (read_tag s) addrs)))
     (just_list (List.map (read_byte s) addrs))
 
-val read_mem_bytesS : forall 'regs 'e. read_kind -> nat -> nat -> monadS 'regs (list memory_byte * bitU) 'e
-let read_mem_bytesS _ addr sz =
+val read_tagged_mem_bytesS : forall 'regs 'e. read_kind -> nat -> nat -> monadS 'regs (list memory_byte * bitU) 'e
+let read_tagged_mem_bytesS _ addr sz =
   readS (get_mem_bytes addr sz) >>$=
   maybe_failS "read_memS"
 
-val read_memS : forall 'regs 'e 'a 'b. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monadS 'regs ('b * bitU) 'e
-let read_memS rk a sz =
+val read_mem_bytesS : forall 'regs 'e. read_kind -> nat -> nat -> monadS 'regs (list memory_byte) 'e
+let read_mem_bytesS rk addr sz =
+  read_tagged_mem_bytesS rk addr sz >>$= (fun (bytes, _) ->
+  returnS bytes)
+
+val read_tagged_memS : forall 'regs 'e 'a 'b. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monadS 'regs ('b * bitU) 'e
+let read_tagged_memS rk a sz =
   maybe_failS "nat_of_bv" (nat_of_bv a) >>$= (fun a ->
-  read_mem_bytesS rk a (nat_of_int sz) >>$= (fun (bytes, tag) ->
+  read_tagged_mem_bytesS rk a (nat_of_int sz) >>$= (fun (bytes, tag) ->
   maybe_failS "bits_of_mem_bytes" (of_bits (bits_of_mem_bytes bytes)) >>$= (fun mem_val ->
   returnS (mem_val, tag))))
 
+val read_memS : forall 'regs 'e 'a 'b. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monadS 'regs 'b 'e
+let read_memS rk a sz =
+  read_tagged_memS rk a sz >>$= (fun (bytes, _) ->
+  returnS bytes)
+
 val excl_resultS : forall 'regs 'e. unit -> monadS 'regs bool 'e
 let excl_resultS =
   (* TODO: This used to be more deterministic, checking a flag in the state
-- 
cgit v1.2.3


From 747999f5c9f9234d04ef9e574a415a88e2bcb52b Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Fri, 30 Nov 2018 18:28:32 +0000
Subject: Rename Undefined outcome to Choose

It is used for nondeterministic choice, so Undefined might be
misleading.
---
 lib/isabelle/Hoare.thy                         | 22 +++++++++++++++-------
 lib/isabelle/ROOT                              |  2 +-
 lib/isabelle/Sail2_operators_mwords_lemmas.thy |  4 ++--
 lib/isabelle/Sail2_prompt_monad_lemmas.thy     |  8 +++++---
 lib/isabelle/Sail2_state_lemmas.thy            | 12 ++++++++++++
 lib/isabelle/Sail2_state_monad_lemmas.thy      |  6 +++---
 src/gen_lib/sail2_prompt.lem                   | 26 ++++++++++++++++++++------
 src/gen_lib/sail2_prompt_monad.lem             | 19 ++++++++++++-------
 src/gen_lib/sail2_state.lem                    | 16 +++++++++++++---
 src/gen_lib/sail2_state_lifting.lem            |  2 +-
 src/gen_lib/sail2_state_monad.lem              |  9 +++++----
 11 files changed, 89 insertions(+), 37 deletions(-)

diff --git a/lib/isabelle/Hoare.thy b/lib/isabelle/Hoare.thy
index 76750117..98b7d077 100644
--- a/lib/isabelle/Hoare.thy
+++ b/lib/isabelle/Hoare.thy
@@ -164,7 +164,7 @@ qed
 lemma PrePost_assert_expS[intro, PrePost_atomI]: "PrePost (if c then P (Value ()) else P (Ex (Failure m))) (assert_expS c m) P"
   unfolding PrePost_def assert_expS_def by (auto simp: returnS_def failS_def)
 
-lemma PrePost_chooseS[intro, PrePost_atomI]: "PrePost (\<lambda>s. \<forall>x \<in> xs. Q (Value x) s) (chooseS xs) Q"
+lemma PrePost_chooseS[intro, PrePost_atomI]: "PrePost (\<lambda>s. \<forall>x \<in> set xs. Q (Value x) s) (chooseS xs) Q"
   by (auto simp: PrePost_def chooseS_def)
 
 lemma PrePost_failS[intro, PrePost_atomI]: "PrePost (Q (Ex (Failure msg))) (failS msg) Q"
@@ -381,7 +381,7 @@ lemma PrePostE_exitS[PrePostE_atomI, intro]: "PrePostE (E (Failure ''exit'')) (e
   unfolding exitS_def PrePostE_def PrePost_def failS_def by auto
 
 lemma PrePostE_chooseS[intro, PrePostE_atomI]:
-  "PrePostE (\<lambda>s. \<forall>x \<in> xs. Q x s) (chooseS xs) Q E"
+  "PrePostE (\<lambda>s. \<forall>x \<in> set xs. Q x s) (chooseS xs) Q E"
   unfolding PrePostE_def by (auto intro: PrePost_strengthen_pre)
 
 lemma PrePostE_throwS[PrePostE_atomI]: "PrePostE (E (Throw e)) (throwS e) Q E"
@@ -488,11 +488,11 @@ lemma PrePostE_liftState_untilM_pure_cond:
   shows "PrePostE (Inv Q vars) (liftState r (untilM vars (return \<circ> cond) body)) Q E"
   using assms by (intro PrePostE_liftState_untilM) (auto simp: comp_def liftState_simp)
 
-lemma PrePostE_undefined_boolS[PrePostE_atomI]:
+lemma PrePostE_choose_boolS_any[PrePostE_atomI]:
   "PrePostE (\<lambda>s. \<forall>b. Q b s)
-            (undefined_boolS unit) Q E"
-  unfolding undefined_boolS_def seqS_def
-  by (auto intro: PrePostE_strengthen_pre PrePostE_chooseS)
+            (choose_boolS unit) Q E"
+  unfolding choose_boolS_def seqS_def
+  by (auto intro: PrePostE_strengthen_pre)
 
 lemma PrePostE_bool_of_bitU_nondetS_any:
   "PrePostE (\<lambda>s. \<forall>b. Q b s) (bool_of_bitU_nondetS b) Q E"
@@ -507,11 +507,19 @@ lemma PrePostE_bools_of_bits_nondetS_any:
             PrePostE_bool_of_bitU_nondetS_any)+)
      auto
 
+lemma PrePostE_choose_boolsS_any:
+  "PrePostE (\<lambda>s. \<forall>bs. Q bs s) (choose_boolsS n) Q E"
+  unfolding choose_boolsS_def genlistS_def Let_def
+  by (rule PrePostE_weaken_post[where B = "\<lambda>_ s. \<forall>bs. Q bs s"], rule PrePostE_strengthen_pre,
+      (rule PrePostE_foreachS_invariant[OF PrePostE_strengthen_pre] PrePostE_bindS PrePostE_returnS
+            PrePostE_choose_boolS_any)+)
+     auto
+
 lemma PrePostE_internal_pick:
   "xs \<noteq> [] \<Longrightarrow> PrePostE (\<lambda>s. \<forall>x \<in> set xs. Q x s) (internal_pickS xs) Q E"
   unfolding internal_pickS_def Let_def
   by (rule PrePostE_strengthen_pre,
-      (rule PrePostE_compositeI PrePostE_atomI PrePostE_bools_of_bits_nondetS_any)+)
+      (rule PrePostE_compositeI PrePostE_atomI PrePostE_choose_boolsS_any)+)
      (auto split: option.splits)
 
 end
diff --git a/lib/isabelle/ROOT b/lib/isabelle/ROOT
index 545e47c4..fb73a673 100644
--- a/lib/isabelle/ROOT
+++ b/lib/isabelle/ROOT
@@ -2,7 +2,7 @@ session "Sail" = "LEM" +
   options [browser_info, document = pdf, document_output = "output"]
   sessions
     "HOL-Eisbach"
-  theories [document = false]
+  theories
     Sail2_values_lemmas
     Sail2_prompt
     Sail2_state_lemmas
diff --git a/lib/isabelle/Sail2_operators_mwords_lemmas.thy b/lib/isabelle/Sail2_operators_mwords_lemmas.thy
index fd54c93a..3e8dcb2f 100644
--- a/lib/isabelle/Sail2_operators_mwords_lemmas.thy
+++ b/lib/isabelle/Sail2_operators_mwords_lemmas.thy
@@ -55,7 +55,7 @@ lemma bool_of_bitU_monadic_simps[simp]:
   "bool_of_bitU_fail BU = Fail ''bool_of_bitU''"
   "bool_of_bitU_nondet B0 = return False"
   "bool_of_bitU_nondet B1 = return True"
-  "bool_of_bitU_nondet BU = undefined_bool ()"
+  "bool_of_bitU_nondet BU = choose_bool ''bool_of_bitU''"
   unfolding bool_of_bitU_fail_def bool_of_bitU_nondet_def
   by auto
 
@@ -68,7 +68,7 @@ lemma update_vec_dec_simps[simp]:
   "update_vec_dec_fail w i BU = Fail ''bool_of_bitU''"
   "update_vec_dec_nondet w i B0 = return (set_bit w (nat i) False)"
   "update_vec_dec_nondet w i B1 = return (set_bit w (nat i) True)"
-  "update_vec_dec_nondet w i BU = undefined_bool () \<bind> (\<lambda>b. return (set_bit w (nat i) b))"
+  "update_vec_dec_nondet w i BU = choose_bool ''bool_of_bitU'' \<bind> (\<lambda>b. return (set_bit w (nat i) b))"
   "update_vec_dec w i B0 = set_bit w (nat i) False"
   "update_vec_dec w i B1 = set_bit w (nat i) True"
   unfolding update_vec_dec_maybe_def update_vec_dec_fail_def update_vec_dec_nondet_def update_vec_dec_def
diff --git a/lib/isabelle/Sail2_prompt_monad_lemmas.thy b/lib/isabelle/Sail2_prompt_monad_lemmas.thy
index c59fc62f..54f58fad 100644
--- a/lib/isabelle/Sail2_prompt_monad_lemmas.thy
+++ b/lib/isabelle/Sail2_prompt_monad_lemmas.thy
@@ -40,7 +40,7 @@ inductive_set T :: "(('rv, 'a, 'e) monad \<times> 'rv event \<times> ('rv, 'a, '
 | Barrier: "((Barrier bk k), E_barrier bk, k) \<in> T"
 | Read_reg: "((Read_reg r k), E_read_reg r v, k v) \<in> T"
 | Write_reg: "((Write_reg r v k), E_write_reg r v, k) \<in> T"
-| Undefined: "((Undefined k), E_undefined v, k v) \<in> T"
+| Choose: "((Choose descr k), E_choose descr v, k v) \<in> T"
 | Print: "((Print msg k), E_print msg, k) \<in> T"
 
 inductive_set Traces :: "(('rv, 'a, 'e) monad \<times> 'rv event list \<times> ('rv, 'a, 'e) monad) set" where
@@ -70,7 +70,7 @@ lemma Traces_cases:
   | (Write_ea) wk addr s k t' where "m = Write_ea wk addr s k" and "t = E_write_ea wk addr s # t'" and "(k, t', m') \<in> Traces"
   | (Footprint) k t' where "m = Footprint k" and "t = E_footprint # t'" and "(k, t', m') \<in> Traces"
   | (Write_reg) reg v k t' where "m = Write_reg reg v k" and "t = E_write_reg reg v # t'" and "(k, t', m') \<in> Traces"
-  | (Undefined) xs v k t' where "m = Undefined k" and "t = E_undefined v # t'" and "(k v, t', m') \<in> Traces"
+  | (Choose) descr v k t' where "m = Choose descr k" and "t = E_choose descr v # t'" and "(k v, t', m') \<in> Traces"
   | (Print) msg k t' where "m = Print msg k" and "t = E_print msg # t'" and "(k, t', m') \<in> Traces"
 proof (use Run in \<open>cases m t m' set: Traces\<close>)
   case Nil
@@ -185,8 +185,10 @@ lemma bind_cong[fundef_cong]:
 
 lemma liftR_read_reg[simp]: "liftR (read_reg reg) = read_reg reg" by (auto simp: read_reg_def liftR_def split: option.splits)
 lemma try_catch_return[simp]: "try_catch (return x) h = return x" by (auto simp: return_def)
+lemma try_catch_choose_bool[simp]: "try_catch (choose_bool descr) h = choose_bool descr" by (auto simp: choose_bool_def)
+lemma liftR_choose_bool[simp]: "liftR (choose_bool descr) = choose_bool descr" by (auto simp: choose_bool_def liftR_def)
 lemma liftR_return[simp]: "liftR (return x) = return x" by (auto simp: liftR_def)
-lemma liftR_undefined_bool[simp]: "liftR (undefined_bool ()) = undefined_bool ()" by (auto simp: undefined_bool_def liftR_def)
+lemma liftR_undefined_bool[simp]: "liftR (undefined_bool ()) = undefined_bool ()" by (auto simp: undefined_bool_def)
 lemma assert_exp_True_return[simp]: "assert_exp True msg = return ()" by (auto simp: assert_exp_def return_def)
 
 end
diff --git a/lib/isabelle/Sail2_state_lemmas.thy b/lib/isabelle/Sail2_state_lemmas.thy
index 77f4ac5a..d99dfc85 100644
--- a/lib/isabelle/Sail2_state_lemmas.thy
+++ b/lib/isabelle/Sail2_state_lemmas.thy
@@ -45,6 +45,9 @@ lemma liftState_barrier[liftState_simp]: "liftState r (barrier bk) = returnS ()"
   by (auto simp: barrier_def)
 lemma liftState_footprint[liftState_simp]: "liftState r (footprint ()) = returnS ()"
   by (auto simp: footprint_def)
+lemma liftState_choose_bool[liftState_simp]: "liftState r (choose_bool descr) = choose_boolS ()"
+  by (auto simp: choose_bool_def liftState_simp)
+declare undefined_boolS_def[simp]
 lemma liftState_undefined[liftState_simp]: "liftState r (undefined_bool ()) = undefined_boolS ()"
   by (auto simp: undefined_bool_def liftState_simp)
 lemma liftState_maybe_fail[liftState_simp]: "liftState r (maybe_fail msg x) = maybe_failS msg x"
@@ -149,6 +152,14 @@ lemma liftState_foreachM[liftState_simp]:
   by (induction xs vars "\<lambda>x vars. liftState r (body x vars)" rule: foreachS.induct)
      (auto simp: liftState_simp cong: bindS_cong)
 
+lemma liftState_genlistM[liftState_simp]:
+  "liftState r (genlistM f n) = genlistS (liftState r \<circ> f) n"
+  by (auto simp: genlistM_def genlistS_def liftState_simp cong: bindS_cong)
+
+lemma liftState_choose_bools[liftState_simp]:
+  "liftState r (choose_bools descr n) = choose_boolsS n"
+  by (auto simp: choose_bools_def choose_boolsS_def liftState_simp comp_def)
+
 lemma liftState_bools_of_bits_nondet[liftState_simp]:
   "liftState r (bools_of_bits_nondet bs) = bools_of_bits_nondetS bs"
   unfolding bools_of_bits_nondet_def bools_of_bits_nondetS_def
@@ -157,6 +168,7 @@ lemma liftState_bools_of_bits_nondet[liftState_simp]:
 lemma liftState_internal_pick[liftState_simp]:
   "liftState r (internal_pick xs) = internal_pickS xs"
   by (auto simp: internal_pick_def internal_pickS_def liftState_simp comp_def
+                 chooseM_def
                  option.case_distrib[where h = "liftState r"]
            simp del: repeat.simps
            cong: option.case_cong)
diff --git a/lib/isabelle/Sail2_state_monad_lemmas.thy b/lib/isabelle/Sail2_state_monad_lemmas.thy
index 12452ca4..ca7e5751 100644
--- a/lib/isabelle/Sail2_state_monad_lemmas.thy
+++ b/lib/isabelle/Sail2_state_monad_lemmas.thy
@@ -38,10 +38,9 @@ lemma bindS_updateS: "bindS (updateS f) m = (\<lambda>s. m () (f s))"
 lemma bindS_assertS_True[simp]: "bindS (assert_expS True msg) f = f ()"
   by (auto simp: assert_expS_def)
 
-lemma bindS_chooseS_returnS[simp]: "bindS (chooseS xs) (\<lambda>x. returnS (f x)) = chooseS (f ` xs)"
+lemma bindS_chooseS_returnS[simp]: "bindS (chooseS xs) (\<lambda>x. returnS (f x)) = chooseS (map f xs)"
   by (intro ext) (auto simp: bindS_def chooseS_def returnS_def)
 
-
 lemma result_cases:
   fixes r :: "('a, 'e) result"
   obtains (Value) a where "r = Value a"
@@ -198,9 +197,10 @@ lemma no_throw_basic_builtins[simp]:
   "\<And>f. ignore_throw (readS f) = readS f"
   "\<And>f. ignore_throw (updateS f) = updateS f"
   "ignore_throw (chooseS xs) = chooseS xs"
+  "ignore_throw (choose_boolS ()) = choose_boolS ()"
   "ignore_throw (failS msg) = failS msg"
   "ignore_throw (maybe_failS msg x) = maybe_failS msg x"
-  unfolding ignore_throw_def returnS_def chooseS_def maybe_failS_def failS_def readS_def updateS_def
+  unfolding ignore_throw_def returnS_def chooseS_def maybe_failS_def failS_def readS_def updateS_def choose_boolS_def
   by (intro ext; auto split: option.splits)+
 
 lemmas ignore_throw_option_case_distrib =
diff --git a/src/gen_lib/sail2_prompt.lem b/src/gen_lib/sail2_prompt.lem
index e01cc051..3cde7ade 100644
--- a/src/gen_lib/sail2_prompt.lem
+++ b/src/gen_lib/sail2_prompt.lem
@@ -38,6 +38,11 @@ end
 
 declare {isabelle} termination_argument foreachM = automatic
 
+val genlistM : forall 'a 'rv 'e. (nat -> monad 'rv 'a 'e) -> nat -> monad 'rv (list 'a) 'e
+let genlistM f n =
+  let indices = genlist (fun n -> n) n in
+  foreachM indices [] (fun n xs -> (f n >>= (fun x -> return (xs ++ [x]))))
+
 val and_boolM : forall 'rv 'e. monad 'rv bool 'e -> monad 'rv bool 'e -> monad 'rv bool 'e
 let and_boolM l r = l >>= (fun l -> if l then r else return false)
 
@@ -55,7 +60,7 @@ val bool_of_bitU_nondet : forall 'rv 'e. bitU -> monad 'rv bool 'e
 let bool_of_bitU_nondet = function
   | B0 -> return false
   | B1 -> return true
-  | BU -> undefined_bool ()
+  | BU -> choose_bool "bool_of_bitU"
 end
 
 val bools_of_bits_nondet : forall 'rv 'e. list bitU -> monad 'rv (list bool) 'e
@@ -93,16 +98,25 @@ let rec untilM vars cond body =
   cond vars >>= fun cond_val ->
   if cond_val then return vars else untilM vars cond body
 
-val internal_pick : forall 'rv 'a 'e. list 'a -> monad 'rv 'a 'e
-let internal_pick xs =
-  (* Use sufficiently many undefined bits and convert into an index into the list *)
-  bools_of_bits_nondet (repeat [BU] (length_list xs)) >>= fun bs ->
+val choose_bools : forall 'rv 'e. string -> nat -> monad 'rv (list bool) 'e
+let choose_bools descr n = genlistM (fun _ -> choose_bool descr) n
+
+val choose : forall 'rv 'a 'e. string -> list 'a -> monad 'rv 'a 'e
+let choose descr xs =
+  (* Use sufficiently many nondeterministically chosen bits and convert into an
+     index into the list *)
+  choose_bools descr (List.length xs) >>= fun bs ->
   let idx = (natFromNatural (nat_of_bools bs)) mod List.length xs in
   match index xs idx with
     | Just x -> return x
-    | Nothing -> Fail "internal_pick"
+    | Nothing -> Fail ("choose " ^ descr)
   end
 
+declare {isabelle} rename function choose = chooseM
+
+val internal_pick : forall 'rv 'a 'e. list 'a -> monad 'rv 'a 'e
+let internal_pick xs = choose "internal_pick" xs
+
 (*let write_two_regs r1 r2 vec =
   let is_inc =
     let is_inc_r1 = is_inc_of_reg r1 in
diff --git a/src/gen_lib/sail2_prompt_monad.lem b/src/gen_lib/sail2_prompt_monad.lem
index 079375a3..c6249d7a 100644
--- a/src/gen_lib/sail2_prompt_monad.lem
+++ b/src/gen_lib/sail2_prompt_monad.lem
@@ -29,8 +29,10 @@ type monad 'regval 'a 'e =
   | Read_reg of register_name * ('regval -> monad 'regval 'a 'e)
   (* Request to write register *)
   | Write_reg of register_name * 'regval * monad 'regval 'a 'e
-  (* Request to choose a Boolean, e.g. to resolve an undefined bit *)
-  | Undefined of (bool -> monad 'regval 'a 'e)
+  (* Request to choose a Boolean, e.g. to resolve an undefined bit. The string
+     argument may be used to provide information to the system about what the
+     Boolean is going to be used for. *)
+  | Choose of string * (bool -> monad 'regval 'a 'e)
   (* Print debugging or tracing information *)
   | Print of string * monad 'regval 'a 'e
   (*Result of a failed assert with possible error message to report*)
@@ -48,7 +50,7 @@ type event 'regval =
   | E_footprint
   | E_read_reg of register_name * 'regval
   | E_write_reg of register_name * 'regval
-  | E_undefined of bool
+  | E_choose of string * bool
   | E_print of string
 
 type trace 'regval = list (event 'regval)
@@ -64,7 +66,7 @@ let rec bind m f = match m with
   | Write_mem wk a sz v t k ->   Write_mem wk a sz v t   (fun v -> bind (k v) f)
   | Read_reg descr k ->          Read_reg descr          (fun v -> bind (k v) f)
   | Excl_res k ->                Excl_res                (fun v -> bind (k v) f)
-  | Undefined k ->               Undefined               (fun v -> bind (k v) f)
+  | Choose descr k ->            Choose descr            (fun v -> bind (k v) f)
   | Write_ea wk a sz k ->        Write_ea wk a sz        (bind k f)
   | Footprint k ->               Footprint               (bind k f)
   | Barrier bk k ->              Barrier bk              (bind k f)
@@ -77,8 +79,11 @@ end
 val exit : forall 'rv 'a 'e. unit -> monad 'rv 'a 'e
 let exit () = Fail "exit"
 
+val choose_bool : forall 'rv 'e. string -> monad 'rv bool 'e
+let choose_bool descr = Choose descr return
+
 val undefined_bool : forall 'rv 'e. unit -> monad 'rv bool 'e
-let undefined_bool () = Undefined return
+let undefined_bool () = choose_bool "undefined_bool"
 
 val assert_exp : forall 'rv 'e. bool -> string -> monad 'rv unit 'e
 let assert_exp exp msg = if exp then Done () else Fail msg
@@ -94,7 +99,7 @@ let rec try_catch m h = match m with
   | Write_mem wk a sz v t k ->   Write_mem wk a sz v t   (fun v -> try_catch (k v) h)
   | Read_reg descr k ->          Read_reg descr          (fun v -> try_catch (k v) h)
   | Excl_res k ->                Excl_res                (fun v -> try_catch (k v) h)
-  | Undefined k ->               Undefined               (fun v -> try_catch (k v) h)
+  | Choose descr k ->            Choose descr            (fun v -> try_catch (k v) h)
   | Write_ea wk a sz k ->        Write_ea wk a sz        (try_catch k h)
   | Footprint k ->               Footprint               (try_catch k h)
   | Barrier bk k ->              Barrier bk              (try_catch k h)
@@ -267,7 +272,7 @@ let emitEvent m e = match (e, m) with
   | (E_print m, Print m' k) ->
      if m' = m then Just k else Nothing
   | (E_excl_res v, Excl_res k) -> Just (k v)
-  | (E_undefined v, Undefined k) -> Just (k v)
+  | (E_choose descr v, Choose descr' k) -> if descr' = descr then Just (k v) else Nothing
   | (E_footprint, Footprint k) -> Just k
   | _ -> Nothing
 end
diff --git a/src/gen_lib/sail2_state.lem b/src/gen_lib/sail2_state.lem
index f703dead..ec787764 100644
--- a/src/gen_lib/sail2_state.lem
+++ b/src/gen_lib/sail2_state.lem
@@ -28,6 +28,11 @@ end
 
 declare {isabelle} termination_argument foreachS = automatic
 
+val genlistS : forall 'a 'rv 'e. (nat -> monadS 'rv 'a 'e) -> nat -> monadS 'rv (list 'a) 'e
+let genlistS f n =
+  let indices = genlist (fun n -> n) n in
+  foreachS indices [] (fun n xs -> (f n >>$= (fun x -> returnS (xs ++ [x]))))
+
 val and_boolS : forall 'rv 'e. monadS 'rv bool 'e -> monadS 'rv bool 'e -> monadS 'rv bool 'e
 let and_boolS l r = l >>$= (fun l -> if l then r else returnS false)
 
@@ -84,12 +89,17 @@ let rec untilS vars cond body s =
   (cond vars >>$= (fun cond_val s'' ->
   if cond_val then returnS vars s'' else untilS vars cond body s'')) s')) s
 
+val choose_boolsS : forall 'rv 'e. nat -> monadS 'rv (list bool) 'e
+let choose_boolsS n = genlistS (fun _ -> choose_boolS ()) n
+
+(* TODO: Replace by chooseS and prove equivalence to prompt monad version *)
 val internal_pickS : forall 'rv 'a 'e. list 'a -> monadS 'rv 'a 'e
 let internal_pickS xs =
-  (* Use sufficiently many undefined bits and convert into an index into the list *)
-  bools_of_bits_nondetS (repeat [BU] (length_list xs)) >>$= fun bs ->
+  (* Use sufficiently many nondeterministically chosen bits and convert into an
+     index into the list *)
+  choose_boolsS (List.length xs) >>$= fun bs ->
   let idx = (natFromNatural (nat_of_bools bs)) mod List.length xs in
   match index xs idx with
     | Just x -> returnS x
-    | Nothing -> failS "internal_pick"
+    | Nothing -> failS "choose internal_pick"
   end
diff --git a/src/gen_lib/sail2_state_lifting.lem b/src/gen_lib/sail2_state_lifting.lem
index 07a6215b..c227e89b 100644
--- a/src/gen_lib/sail2_state_lifting.lem
+++ b/src/gen_lib/sail2_state_lifting.lem
@@ -14,7 +14,7 @@ let rec liftState ra m = match m with
   | (Write_mem wk a sz v t k)   -> bindS (write_mem_bytesS wk a sz v t)   (fun v -> liftState ra (k v))
   | (Read_reg r k)              -> bindS (read_regvalS ra r)              (fun v -> liftState ra (k v))
   | (Excl_res k)                -> bindS (excl_resultS ())                (fun v -> liftState ra (k v))
-  | (Undefined k)               -> bindS (undefined_boolS ())             (fun v -> liftState ra (k v))
+  | (Choose _ k)                -> bindS (choose_boolS ())                (fun v -> liftState ra (k v))
   | (Write_reg r v k)           -> seqS (write_regvalS ra r v)            (liftState ra k)
   | (Write_ea _ _ _ k)          -> liftState ra k
   | (Footprint k)               -> liftState ra k
diff --git a/src/gen_lib/sail2_state_monad.lem b/src/gen_lib/sail2_state_monad.lem
index 8626052f..b2a7bb31 100644
--- a/src/gen_lib/sail2_state_monad.lem
+++ b/src/gen_lib/sail2_state_monad.lem
@@ -47,8 +47,8 @@ let seqS m n = bindS m (fun (_ : unit) -> n)
 let inline (>>$=) = bindS
 let inline (>>$) = seqS
 
-val chooseS : forall 'regs 'a 'e. SetType 'a => set 'a -> monadS 'regs 'a 'e
-let chooseS xs s = Set.map (fun x -> (Value x, s)) xs
+val chooseS : forall 'regs 'a 'e. SetType 'a => list 'a -> monadS 'regs 'a 'e
+let chooseS xs s = Set.fromList (List.map (fun x -> (Value x, s)) xs)
 
 val readS : forall 'regs 'a 'e. (sequential_state 'regs -> 'a) -> monadS 'regs 'a 'e
 let readS f = (fun s -> returnS (f s) s)
@@ -59,8 +59,9 @@ let updateS f = (fun s -> returnS () (f s))
 val failS : forall 'regs 'a 'e. string -> monadS 'regs 'a 'e
 let failS msg s = {(Ex (Failure msg), s)}
 
-val undefined_boolS : forall 'regval 'regs 'a 'e. unit -> monadS 'regs bool 'e
-let undefined_boolS () = chooseS {false; true}
+val choose_boolS : forall 'regval 'regs 'a 'e. unit -> monadS 'regs bool 'e
+let choose_boolS () = chooseS [false; true]
+let undefined_boolS = choose_boolS
 
 val exitS : forall 'regs 'e 'a. unit -> monadS 'regs 'a 'e
 let exitS () = failS "exit"
-- 
cgit v1.2.3


From b4495040178bc7552acc76c14de7151583456ee6 Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Mon, 3 Dec 2018 12:42:32 +0000
Subject: Make names of memory r/w events more consistent

Use E_read_memt for reading tagged memory, as in sail2_impl_base.lem,
and rename E_write_mem to E_write_memt, since it always writes a tag.
---
 lib/isabelle/Sail2_prompt_monad_lemmas.thy | 10 ++--
 lib/isabelle/Sail2_state_lemmas.thy        | 10 ++--
 lib/isabelle/Sail2_state_monad_lemmas.thy  |  6 +--
 src/gen_lib/sail2_prompt_monad.lem         | 76 +++++++++++++++---------------
 src/gen_lib/sail2_state_lifting.lem        | 32 ++++++-------
 src/gen_lib/sail2_state_monad.lem          | 14 +++---
 6 files changed, 74 insertions(+), 74 deletions(-)

diff --git a/lib/isabelle/Sail2_prompt_monad_lemmas.thy b/lib/isabelle/Sail2_prompt_monad_lemmas.thy
index 54f58fad..500d260d 100644
--- a/lib/isabelle/Sail2_prompt_monad_lemmas.thy
+++ b/lib/isabelle/Sail2_prompt_monad_lemmas.thy
@@ -32,10 +32,10 @@ lemmas try_catch_induct[case_names Done Read_mem Write_memv Read_reg Excl_res Wr
 
 inductive_set T :: "(('rv, 'a, 'e) monad \<times> 'rv event \<times> ('rv, 'a, 'e) monad) set" where
   Read_mem: "((Read_mem rk addr sz k), E_read_mem rk addr sz v, k v) \<in> T"
-| Read_tagged_mem: "((Read_tagged_mem rk addr sz k), E_read_tagged_mem rk addr sz v, k v) \<in> T"
+| Read_memt: "((Read_memt rk addr sz k), E_read_memt rk addr sz v, k v) \<in> T"
 | Write_ea: "((Write_ea wk addr sz k), E_write_ea wk addr sz, k) \<in> T"
 | Excl_res: "((Excl_res k), E_excl_res r, k r) \<in> T"
-| Write_mem: "((Write_mem wk addr sz v t k), E_write_mem wk addr sz v t r, k r) \<in> T"
+| Write_memt: "((Write_memt wk addr sz v t k), E_write_memt wk addr sz v t r, k r) \<in> T"
 | Footprint: "((Footprint k), E_footprint, k) \<in> T"
 | Barrier: "((Barrier bk k), E_barrier bk, k) \<in> T"
 | Read_reg: "((Read_reg r k), E_read_reg r v, k v) \<in> T"
@@ -62,8 +62,8 @@ lemma Traces_cases:
   assumes Run: "(m, t, m') \<in> Traces"
   obtains (Nil) a where "m = m'" and "t = []"
   | (Read_mem) rk addr s k t' v where "m = Read_mem rk addr s k" and "t = E_read_mem rk addr s v # t'" and "(k v, t', m') \<in> Traces"
-  | (Read_tagged_mem) rk addr s k t' v tag where "m = Read_tagged_mem rk addr s k" and "t = E_read_tagged_mem rk addr s (v, tag) # t'" and "(k (v, tag), t', m') \<in> Traces"
-  | (Write_mem) wk addr sz val tag k t' v where "m = Write_mem wk addr sz val tag k" and "t = E_write_mem wk addr sz val tag v # t'" and "(k v, t', m') \<in> Traces"
+  | (Read_memt) rk addr s k t' v tag where "m = Read_memt rk addr s k" and "t = E_read_memt rk addr s (v, tag) # t'" and "(k (v, tag), t', m') \<in> Traces"
+  | (Write_memt) wk addr sz val tag k t' v where "m = Write_memt wk addr sz val tag k" and "t = E_write_memt wk addr sz val tag v # t'" and "(k v, t', m') \<in> Traces"
   | (Barrier) bk k t' v where "m = Barrier bk k" and "t = E_barrier bk # t'" and "(k, t', m') \<in> Traces"
   | (Read_reg) reg k t' v where "m = Read_reg reg k" and "t = E_read_reg reg v # t'" and "(k v, t', m') \<in> Traces"
   | (Excl_res) k t' v where "m = Excl_res k" and "t = E_excl_res v # t'" and "(k v, t', m') \<in> Traces"
@@ -81,7 +81,7 @@ next
   note m' = \<open>(m'', t', m') \<in> Traces\<close>
   from \<open>(m, e, m'') \<in> T\<close> and t and m'
   show ?thesis proof (cases m e m'' rule: T.cases)
-    case (Read_tagged_mem rk addr sz k v)
+    case (Read_memt rk addr sz k v)
     then show ?thesis using t m' by (cases v; elim that; blast)
   qed (elim that; blast)+
 qed
diff --git a/lib/isabelle/Sail2_state_lemmas.thy b/lib/isabelle/Sail2_state_lemmas.thy
index d99dfc85..05ae99ee 100644
--- a/lib/isabelle/Sail2_state_lemmas.thy
+++ b/lib/isabelle/Sail2_state_lemmas.thy
@@ -83,9 +83,9 @@ lemma liftState_bool_of_bitU_nondet[liftState_simp]:
   "liftState r (bool_of_bitU_nondet b) = bool_of_bitU_nondetS b"
   by (cases b; auto simp: bool_of_bitU_nondet_def bool_of_bitU_nondetS_def liftState_simp)
 
-lemma liftState_read_tagged_mem[liftState_simp]:
-  shows "liftState r (read_tagged_mem BCa BCb rk a sz) = read_tagged_memS BCa BCb rk a sz"
-  by (auto simp: read_tagged_mem_def read_tagged_mem_bytes_def maybe_failS_def read_tagged_memS_def
+lemma liftState_read_memt[liftState_simp]:
+  shows "liftState r (read_memt BCa BCb rk a sz) = read_memtS BCa BCb rk a sz"
+  by (auto simp: read_memt_def read_memt_bytes_def maybe_failS_def read_memtS_def
                  prod.case_distrib option.case_distrib[where h = "liftState r"]
                  option.case_distrib[where h = "\<lambda>c. c \<bind>\<^sub>S f" for f] liftState_simp
            split: option.splits intro: bindS_cong)
@@ -93,7 +93,7 @@ lemma liftState_read_tagged_mem[liftState_simp]:
 lemma liftState_read_mem[liftState_simp]:
   shows "liftState r (read_mem BCa BCb rk a sz) = read_memS BCa BCb rk a sz"
   by (auto simp: read_mem_def read_mem_bytes_def read_memS_def read_mem_bytesS_def maybe_failS_def
-                 read_tagged_memS_def
+                 read_memtS_def
                  prod.case_distrib option.case_distrib[where h = "liftState r"]
                  option.case_distrib[where h = "\<lambda>c. c \<bind>\<^sub>S f" for f] liftState_simp
            split: option.splits intro: bindS_cong)
@@ -422,7 +422,7 @@ lemma emitEventS_update_cases:
   assumes "emitEventS ra e s = Some s'"
   obtains
     (Write_mem) wk addr sz v tag r
-      where "e = E_write_mem wk addr sz v tag r"
+      where "e = E_write_memt wk addr sz v tag r"
         and "s' = put_mem_bytes addr sz v tag s"
   | (Write_reg) r v rs'
       where "e = E_write_reg r v" and "(snd ra) r v (regstate s) = Some rs'"
diff --git a/lib/isabelle/Sail2_state_monad_lemmas.thy b/lib/isabelle/Sail2_state_monad_lemmas.thy
index ca7e5751..d870c4a8 100644
--- a/lib/isabelle/Sail2_state_monad_lemmas.thy
+++ b/lib/isabelle/Sail2_state_monad_lemmas.thy
@@ -212,15 +212,15 @@ lemma ignore_throw_let_distrib: "ignore_throw (let x = y in f x) = (let x = y in
 
 lemma no_throw_mem_builtins:
   "\<And>rk a sz s. ignore_throw (read_mem_bytesS rk a sz) s = read_mem_bytesS rk a sz s"
-  "\<And>rk a sz s. ignore_throw (read_tagged_mem_bytesS rk a sz) s = read_tagged_mem_bytesS rk a sz s"
+  "\<And>rk a sz s. ignore_throw (read_memt_bytesS rk a sz) s = read_memt_bytesS rk a sz s"
   "\<And>BC a s. ignore_throw (read_tagS BC a) s = read_tagS BC a s"
   "\<And>BCa BCv rk a sz s. ignore_throw (read_memS BCa BCv rk a sz) s = read_memS BCa BCv rk a sz s"
-  "\<And>BCa BCv rk a sz s. ignore_throw (read_tagged_memS BCa BCv rk a sz) s = read_tagged_memS BCa BCv rk a sz s"
+  "\<And>BCa BCv rk a sz s. ignore_throw (read_memtS BCa BCv rk a sz) s = read_memtS BCa BCv rk a sz s"
   "\<And>BC wk addr sz v t s. ignore_throw (write_mem_bytesS wk addr sz v t) s = write_mem_bytesS wk addr sz v t s"
   "\<And>BCa BCv wk addr sz v t s. ignore_throw (write_memS BCa BCv wk addr sz v t) s = write_memS BCa BCv wk addr sz v t s"
   "\<And>s. ignore_throw (excl_resultS ()) s = excl_resultS () s"
   "\<And>s. ignore_throw (undefined_boolS ()) s = undefined_boolS () s"
-  unfolding read_mem_bytesS_def read_tagged_mem_bytesS_def read_tagged_memS_def read_memS_def read_tagS_def write_memS_def
+  unfolding read_mem_bytesS_def read_memt_bytesS_def read_memtS_def read_memS_def read_tagS_def write_memS_def
   unfolding write_mem_bytesS_def
   unfolding excl_resultS_def undefined_boolS_def maybe_failS_def
   unfolding ignore_throw_bindS
diff --git a/src/gen_lib/sail2_prompt_monad.lem b/src/gen_lib/sail2_prompt_monad.lem
index c6249d7a..cf2fd151 100644
--- a/src/gen_lib/sail2_prompt_monad.lem
+++ b/src/gen_lib/sail2_prompt_monad.lem
@@ -12,7 +12,7 @@ type monad 'regval 'a 'e =
      with or without a tag.  The first nat specifies the address, the second
      the number of bytes. *)
   | Read_mem of read_kind * nat * nat * (list memory_byte -> monad 'regval 'a 'e)
-  | Read_tagged_mem of read_kind * nat * nat * ((list memory_byte * bitU) -> monad 'regval 'a 'e)
+  | Read_memt of read_kind * nat * nat * ((list memory_byte * bitU) -> monad 'regval 'a 'e)
   (* Tell the system a write is imminent, at the given address and with the
      given size. *)
   | Write_ea of write_kind * nat * nat * monad 'regval 'a 'e
@@ -20,7 +20,7 @@ type monad 'regval 'a 'e =
   | Excl_res of (bool -> monad 'regval 'a 'e)
   (* Request to write a memory value of the given size together with a tag
      at the given address. *)
-  | Write_mem of write_kind * nat * nat * list memory_byte * bitU * (bool -> monad 'regval 'a 'e)
+  | Write_memt of write_kind * nat * nat * list memory_byte * bitU * (bool -> monad 'regval 'a 'e)
   (* Tell the system to dynamically recalculate dependency footprint *)
   | Footprint of monad 'regval 'a 'e
   (* Request a memory barrier *)
@@ -42,8 +42,8 @@ type monad 'regval 'a 'e =
 
 type event 'regval =
   | E_read_mem of read_kind * nat * nat * list memory_byte
-  | E_read_tagged_mem of read_kind * nat * nat * (list memory_byte * bitU)
-  | E_write_mem of write_kind * nat * nat * list memory_byte * bitU * bool
+  | E_read_memt of read_kind * nat * nat * (list memory_byte * bitU)
+  | E_write_memt of write_kind * nat * nat * list memory_byte * bitU * bool
   | E_write_ea of write_kind * nat * nat
   | E_excl_res of bool
   | E_barrier of barrier_kind
@@ -61,19 +61,19 @@ let return a = Done a
 val bind : forall 'rv 'a 'b 'e. monad 'rv 'a 'e -> ('a -> monad 'rv 'b 'e) -> monad 'rv 'b 'e
 let rec bind m f = match m with
   | Done a -> f a
-  | Read_mem rk a sz k ->        Read_mem rk a sz        (fun v -> bind (k v) f)
-  | Read_tagged_mem rk a sz k -> Read_tagged_mem rk a sz (fun v -> bind (k v) f)
-  | Write_mem wk a sz v t k ->   Write_mem wk a sz v t   (fun v -> bind (k v) f)
-  | Read_reg descr k ->          Read_reg descr          (fun v -> bind (k v) f)
-  | Excl_res k ->                Excl_res                (fun v -> bind (k v) f)
-  | Choose descr k ->            Choose descr            (fun v -> bind (k v) f)
-  | Write_ea wk a sz k ->        Write_ea wk a sz        (bind k f)
-  | Footprint k ->               Footprint               (bind k f)
-  | Barrier bk k ->              Barrier bk              (bind k f)
-  | Write_reg r v k ->           Write_reg r v           (bind k f)
-  | Print msg k ->               Print msg               (bind k f)
-  | Fail descr ->                Fail descr
-  | Exception e ->               Exception e
+  | Read_mem rk a sz k ->       Read_mem rk a sz       (fun v -> bind (k v) f)
+  | Read_memt rk a sz k ->      Read_memt rk a sz      (fun v -> bind (k v) f)
+  | Write_memt wk a sz v t k -> Write_memt wk a sz v t (fun v -> bind (k v) f)
+  | Read_reg descr k ->         Read_reg descr         (fun v -> bind (k v) f)
+  | Excl_res k ->               Excl_res               (fun v -> bind (k v) f)
+  | Choose descr k ->           Choose descr           (fun v -> bind (k v) f)
+  | Write_ea wk a sz k ->       Write_ea wk a sz       (bind k f)
+  | Footprint k ->              Footprint              (bind k f)
+  | Barrier bk k ->             Barrier bk             (bind k f)
+  | Write_reg r v k ->          Write_reg r v          (bind k f)
+  | Print msg k ->              Print msg              (bind k f)
+  | Fail descr ->               Fail descr
+  | Exception e ->              Exception e
 end
 
 val exit : forall 'rv 'a 'e. unit -> monad 'rv 'a 'e
@@ -94,19 +94,19 @@ let throw e = Exception e
 val try_catch : forall 'rv 'a 'e1 'e2. monad 'rv 'a 'e1 -> ('e1 -> monad 'rv 'a 'e2) -> monad 'rv 'a 'e2
 let rec try_catch m h = match m with
   | Done a -> Done a
-  | Read_mem rk a sz k ->        Read_mem rk a sz        (fun v -> try_catch (k v) h)
-  | Read_tagged_mem rk a sz k -> Read_tagged_mem rk a sz (fun v -> try_catch (k v) h)
-  | Write_mem wk a sz v t k ->   Write_mem wk a sz v t   (fun v -> try_catch (k v) h)
-  | Read_reg descr k ->          Read_reg descr          (fun v -> try_catch (k v) h)
-  | Excl_res k ->                Excl_res                (fun v -> try_catch (k v) h)
-  | Choose descr k ->            Choose descr            (fun v -> try_catch (k v) h)
-  | Write_ea wk a sz k ->        Write_ea wk a sz        (try_catch k h)
-  | Footprint k ->               Footprint               (try_catch k h)
-  | Barrier bk k ->              Barrier bk              (try_catch k h)
-  | Write_reg r v k ->           Write_reg r v           (try_catch k h)
-  | Print msg k ->               Print msg               (try_catch k h)
-  | Fail descr ->                Fail descr
-  | Exception e ->               h e
+  | Read_mem rk a sz k ->       Read_mem rk a sz       (fun v -> try_catch (k v) h)
+  | Read_memt rk a sz k ->      Read_memt rk a sz      (fun v -> try_catch (k v) h)
+  | Write_memt wk a sz v t k -> Write_memt wk a sz v t (fun v -> try_catch (k v) h)
+  | Read_reg descr k ->         Read_reg descr         (fun v -> try_catch (k v) h)
+  | Excl_res k ->               Excl_res               (fun v -> try_catch (k v) h)
+  | Choose descr k ->           Choose descr           (fun v -> try_catch (k v) h)
+  | Write_ea wk a sz k ->       Write_ea wk a sz       (try_catch k h)
+  | Footprint k ->              Footprint              (try_catch k h)
+  | Barrier bk k ->             Barrier bk             (try_catch k h)
+  | Write_reg r v k ->          Write_reg r v          (try_catch k h)
+  | Print msg k ->              Print msg              (try_catch k h)
+  | Fail descr ->               Fail descr
+  | Exception e ->              h e
 end
 
 (* For early return, we abuse exceptions by throwing and catching
@@ -144,16 +144,16 @@ let maybe_fail msg = function
   | Nothing -> Fail msg
 end
 
-val read_tagged_mem_bytes : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monad 'rv (list memory_byte * bitU) 'e
-let read_tagged_mem_bytes rk addr sz =
+val read_memt_bytes : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monad 'rv (list memory_byte * bitU) 'e
+let read_memt_bytes rk addr sz =
   bind
     (maybe_fail "nat_of_bv" (nat_of_bv addr))
-    (fun addr -> Read_tagged_mem rk addr (nat_of_int sz) return)
+    (fun addr -> Read_memt rk addr (nat_of_int sz) return)
 
-val read_tagged_mem : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monad 'rv ('b * bitU) 'e
-let read_tagged_mem rk addr sz =
+val read_memt : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monad 'rv ('b * bitU) 'e
+let read_memt rk addr sz =
   bind
-    (read_tagged_mem_bytes rk addr sz)
+    (read_memt_bytes rk addr sz)
     (fun (bytes, tag) ->
        match of_bits (bits_of_mem_bytes bytes) with
          | Just v -> return (v, tag)
@@ -192,7 +192,7 @@ val write_mem : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b =>
 let write_mem wk addr sz v tag =
   match (mem_bytes_of_bits v, nat_of_bv addr) with
     | (Just v, Just addr) ->
-       Write_mem wk addr (nat_of_int sz) v tag return
+       Write_memt wk addr (nat_of_int sz) v tag return
     | _ -> Fail "write_mem"
   end
 
@@ -259,7 +259,7 @@ val emitEvent : forall 'regval 'a 'e. Eq 'regval => monad 'regval 'a 'e -> event
 let emitEvent m e = match (e, m) with
   | (E_read_mem rk a sz v, Read_mem rk' a' sz' k) ->
      if rk' = rk && a' = a && sz' = sz then Just (k v) else Nothing
-  | (E_write_mem wk a sz v tag r, Write_mem wk' a' sz' v' tag' k) ->
+  | (E_write_memt wk a sz v tag r, Write_memt wk' a' sz' v' tag' k) ->
      if wk' = wk && a' = a && sz' = sz && v' = v && tag' = tag then Just (k r) else Nothing
   | (E_read_reg r v, Read_reg r' k) ->
      if r' = r then Just (k v) else Nothing
diff --git a/src/gen_lib/sail2_state_lifting.lem b/src/gen_lib/sail2_state_lifting.lem
index c227e89b..a055bfe0 100644
--- a/src/gen_lib/sail2_state_lifting.lem
+++ b/src/gen_lib/sail2_state_lifting.lem
@@ -8,20 +8,20 @@ open import {isabelle} `Sail2_state_monad_lemmas`
 (* Lifting from prompt monad to state monad *)
 val liftState : forall 'regval 'regs 'a 'e. register_accessors 'regs 'regval -> monad 'regval 'a 'e -> monadS 'regs 'a 'e
 let rec liftState ra m = match m with
-  | (Done a)                    -> returnS a
-  | (Read_mem rk a sz k)        -> bindS (read_mem_bytesS rk a sz)        (fun v -> liftState ra (k v))
-  | (Read_tagged_mem rk a sz k) -> bindS (read_tagged_mem_bytesS rk a sz) (fun v -> liftState ra (k v))
-  | (Write_mem wk a sz v t k)   -> bindS (write_mem_bytesS wk a sz v t)   (fun v -> liftState ra (k v))
-  | (Read_reg r k)              -> bindS (read_regvalS ra r)              (fun v -> liftState ra (k v))
-  | (Excl_res k)                -> bindS (excl_resultS ())                (fun v -> liftState ra (k v))
-  | (Choose _ k)                -> bindS (choose_boolS ())                (fun v -> liftState ra (k v))
-  | (Write_reg r v k)           -> seqS (write_regvalS ra r v)            (liftState ra k)
-  | (Write_ea _ _ _ k)          -> liftState ra k
-  | (Footprint k)               -> liftState ra k
-  | (Barrier _ k)               -> liftState ra k
-  | (Print _ k)                 -> liftState ra k (* TODO *)
-  | (Fail descr)                -> failS descr
-  | (Exception e)               -> throwS e
+  | (Done a)                   -> returnS a
+  | (Read_mem rk a sz k)       -> bindS (read_mem_bytesS rk a sz)      (fun v -> liftState ra (k v))
+  | (Read_memt rk a sz k)      -> bindS (read_memt_bytesS rk a sz)     (fun v -> liftState ra (k v))
+  | (Write_memt wk a sz v t k) -> bindS (write_mem_bytesS wk a sz v t) (fun v -> liftState ra (k v))
+  | (Read_reg r k)             -> bindS (read_regvalS ra r)            (fun v -> liftState ra (k v))
+  | (Excl_res k)               -> bindS (excl_resultS ())              (fun v -> liftState ra (k v))
+  | (Choose _ k)               -> bindS (choose_boolS ())              (fun v -> liftState ra (k v))
+  | (Write_reg r v k)          -> seqS (write_regvalS ra r v)          (liftState ra k)
+  | (Write_ea _ _ _ k)         -> liftState ra k
+  | (Footprint k)              -> liftState ra k
+  | (Barrier _ k)              -> liftState ra k
+  | (Print _ k)                -> liftState ra k (* TODO *)
+  | (Fail descr)               -> failS descr
+  | (Exception e)              -> throwS e
 end
 
 val emitEventS : forall 'regval 'regs 'a 'e. Eq 'regval => register_accessors 'regs 'regval -> event 'regval -> sequential_state 'regs -> maybe (sequential_state 'regs)
@@ -29,10 +29,10 @@ let emitEventS ra e s = match e with
   | E_read_mem _ addr sz v ->
      Maybe.bind (get_mem_bytes addr sz s) (fun (v', _) ->
      if v' = v then Just s else Nothing)
-  | E_read_tagged_mem _ addr sz (v, tag) ->
+  | E_read_memt _ addr sz (v, tag) ->
      Maybe.bind (get_mem_bytes addr sz s) (fun (v', tag') ->
      if v' = v && tag' = tag then Just s else Nothing)
-  | E_write_mem _ addr sz v tag success ->
+  | E_write_memt _ addr sz v tag success ->
      if success then Just (put_mem_bytes addr sz v tag s) else Nothing
   | E_read_reg r v ->
      let (read_reg, _) = ra in
diff --git a/src/gen_lib/sail2_state_monad.lem b/src/gen_lib/sail2_state_monad.lem
index b2a7bb31..18e57b30 100644
--- a/src/gen_lib/sail2_state_monad.lem
+++ b/src/gen_lib/sail2_state_monad.lem
@@ -130,26 +130,26 @@ let get_mem_bytes addr sz s =
     (fun mem_val -> (mem_val, List.foldl and_bit B1 (List.map (read_tag s) addrs)))
     (just_list (List.map (read_byte s) addrs))
 
-val read_tagged_mem_bytesS : forall 'regs 'e. read_kind -> nat -> nat -> monadS 'regs (list memory_byte * bitU) 'e
-let read_tagged_mem_bytesS _ addr sz =
+val read_memt_bytesS : forall 'regs 'e. read_kind -> nat -> nat -> monadS 'regs (list memory_byte * bitU) 'e
+let read_memt_bytesS _ addr sz =
   readS (get_mem_bytes addr sz) >>$=
   maybe_failS "read_memS"
 
 val read_mem_bytesS : forall 'regs 'e. read_kind -> nat -> nat -> monadS 'regs (list memory_byte) 'e
 let read_mem_bytesS rk addr sz =
-  read_tagged_mem_bytesS rk addr sz >>$= (fun (bytes, _) ->
+  read_memt_bytesS rk addr sz >>$= (fun (bytes, _) ->
   returnS bytes)
 
-val read_tagged_memS : forall 'regs 'e 'a 'b. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monadS 'regs ('b * bitU) 'e
-let read_tagged_memS rk a sz =
+val read_memtS : forall 'regs 'e 'a 'b. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monadS 'regs ('b * bitU) 'e
+let read_memtS rk a sz =
   maybe_failS "nat_of_bv" (nat_of_bv a) >>$= (fun a ->
-  read_tagged_mem_bytesS rk a (nat_of_int sz) >>$= (fun (bytes, tag) ->
+  read_memt_bytesS rk a (nat_of_int sz) >>$= (fun (bytes, tag) ->
   maybe_failS "bits_of_mem_bytes" (of_bits (bits_of_mem_bytes bytes)) >>$= (fun mem_val ->
   returnS (mem_val, tag))))
 
 val read_memS : forall 'regs 'e 'a 'b. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monadS 'regs 'b 'e
 let read_memS rk a sz =
-  read_tagged_memS rk a sz >>$= (fun (bytes, _) ->
+  read_memtS rk a sz >>$= (fun (bytes, _) ->
   returnS bytes)
 
 val excl_resultS : forall 'regs 'e. unit -> monadS 'regs bool 'e
-- 
cgit v1.2.3


From df0e02bc0c8259962f25d4c175fa950391695ab6 Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Mon, 3 Dec 2018 16:03:24 +0000
Subject: Add Write_mem event/outcome without tag

The inter-instruction semantics is responsible for correctly handling memory
writes without tags; the lifting to the state monad handles it as writing a
value with a zero tag bit.
---
 lib/isabelle/Sail2_prompt_monad_lemmas.thy |  2 ++
 lib/isabelle/Sail2_state_lemmas.thy        | 13 +++++++++----
 lib/isabelle/Sail2_state_monad_lemmas.thy  | 10 ++++++----
 src/gen_lib/sail2_prompt_monad.lem         | 21 ++++++++++++++++++---
 src/gen_lib/sail2_state_lifting.lem        | 17 ++++++++++-------
 src/gen_lib/sail2_state_monad.lem          | 23 +++++++++++++++--------
 6 files changed, 60 insertions(+), 26 deletions(-)

diff --git a/lib/isabelle/Sail2_prompt_monad_lemmas.thy b/lib/isabelle/Sail2_prompt_monad_lemmas.thy
index 500d260d..3658296b 100644
--- a/lib/isabelle/Sail2_prompt_monad_lemmas.thy
+++ b/lib/isabelle/Sail2_prompt_monad_lemmas.thy
@@ -35,6 +35,7 @@ inductive_set T :: "(('rv, 'a, 'e) monad \<times> 'rv event \<times> ('rv, 'a, '
 | Read_memt: "((Read_memt rk addr sz k), E_read_memt rk addr sz v, k v) \<in> T"
 | Write_ea: "((Write_ea wk addr sz k), E_write_ea wk addr sz, k) \<in> T"
 | Excl_res: "((Excl_res k), E_excl_res r, k r) \<in> T"
+| Write_mem: "((Write_mem wk addr sz v k), E_write_mem wk addr sz v r, k r) \<in> T"
 | Write_memt: "((Write_memt wk addr sz v t k), E_write_memt wk addr sz v t r, k r) \<in> T"
 | Footprint: "((Footprint k), E_footprint, k) \<in> T"
 | Barrier: "((Barrier bk k), E_barrier bk, k) \<in> T"
@@ -63,6 +64,7 @@ lemma Traces_cases:
   obtains (Nil) a where "m = m'" and "t = []"
   | (Read_mem) rk addr s k t' v where "m = Read_mem rk addr s k" and "t = E_read_mem rk addr s v # t'" and "(k v, t', m') \<in> Traces"
   | (Read_memt) rk addr s k t' v tag where "m = Read_memt rk addr s k" and "t = E_read_memt rk addr s (v, tag) # t'" and "(k (v, tag), t', m') \<in> Traces"
+  | (Write_mem) wk addr sz val k v t' where "m = Write_mem wk addr sz val k" and "t = E_write_mem wk addr sz val v # t'" and "(k v, t', m') \<in> Traces"
   | (Write_memt) wk addr sz val tag k t' v where "m = Write_memt wk addr sz val tag k" and "t = E_write_memt wk addr sz val tag v # t'" and "(k v, t', m') \<in> Traces"
   | (Barrier) bk k t' v where "m = Barrier bk k" and "t = E_barrier bk # t'" and "(k, t', m') \<in> Traces"
   | (Read_reg) reg k t' v where "m = Read_reg reg k" and "t = E_read_reg reg v # t'" and "(k v, t', m') \<in> Traces"
diff --git a/lib/isabelle/Sail2_state_lemmas.thy b/lib/isabelle/Sail2_state_lemmas.thy
index 05ae99ee..8b189f7a 100644
--- a/lib/isabelle/Sail2_state_lemmas.thy
+++ b/lib/isabelle/Sail2_state_lemmas.thy
@@ -113,9 +113,14 @@ lemma liftState_write_mem_ea_BC:
    write_mem_bytesS BC_mword wk addr sz v t"
   by (auto simp: write_mem_bytesS_def)*)
 
-lemma liftState_write_mem_val[liftState_simp]:
-  "liftState r (write_mem BC_mword BCv wk addr sz v t) = write_memS BC_mword BCv wk addr sz v t"
-  by (auto simp: write_mem_def write_memS_def liftState_simp split: option.splits)
+lemma liftState_write_memt[liftState_simp]:
+  "liftState r (write_memt BCa BCv wk addr sz v t) = write_memtS BCa BCv wk addr sz v t"
+  by (auto simp: write_memt_def write_memtS_def liftState_simp split: option.splits)
+
+lemma liftState_write_mem[liftState_simp]:
+  "liftState r (write_mem BCa BCv wk addr sz v) = write_memS BCa BCv wk addr sz v"
+  by (auto simp: write_mem_def write_memS_def write_memtS_def write_mem_bytesS_def liftState_simp
+           split: option.splits)
 
 lemma liftState_read_reg_readS:
   assumes "\<And>s. Option.bind (get_regval' (name reg) s) (of_regval reg) = Some (read_from reg s)"
@@ -422,7 +427,7 @@ lemma emitEventS_update_cases:
   assumes "emitEventS ra e s = Some s'"
   obtains
     (Write_mem) wk addr sz v tag r
-      where "e = E_write_memt wk addr sz v tag r"
+      where "e = E_write_memt wk addr sz v tag r \<or> (e = E_write_mem wk addr sz v r \<and> tag = B0)"
         and "s' = put_mem_bytes addr sz v tag s"
   | (Write_reg) r v rs'
       where "e = E_write_reg r v" and "(snd ra) r v (regstate s) = Some rs'"
diff --git a/lib/isabelle/Sail2_state_monad_lemmas.thy b/lib/isabelle/Sail2_state_monad_lemmas.thy
index d870c4a8..1e9f50cc 100644
--- a/lib/isabelle/Sail2_state_monad_lemmas.thy
+++ b/lib/isabelle/Sail2_state_monad_lemmas.thy
@@ -216,12 +216,14 @@ lemma no_throw_mem_builtins:
   "\<And>BC a s. ignore_throw (read_tagS BC a) s = read_tagS BC a s"
   "\<And>BCa BCv rk a sz s. ignore_throw (read_memS BCa BCv rk a sz) s = read_memS BCa BCv rk a sz s"
   "\<And>BCa BCv rk a sz s. ignore_throw (read_memtS BCa BCv rk a sz) s = read_memtS BCa BCv rk a sz s"
-  "\<And>BC wk addr sz v t s. ignore_throw (write_mem_bytesS wk addr sz v t) s = write_mem_bytesS wk addr sz v t s"
-  "\<And>BCa BCv wk addr sz v t s. ignore_throw (write_memS BCa BCv wk addr sz v t) s = write_memS BCa BCv wk addr sz v t s"
+  "\<And>BC wk addr sz v s. ignore_throw (write_mem_bytesS wk addr sz v) s = write_mem_bytesS wk addr sz v s"
+  "\<And>BC wk addr sz v t s. ignore_throw (write_memt_bytesS wk addr sz v t) s = write_memt_bytesS wk addr sz v t s"
+  "\<And>BCa BCv wk addr sz v s. ignore_throw (write_memS BCa BCv wk addr sz v) s = write_memS BCa BCv wk addr sz v s"
+  "\<And>BCa BCv wk addr sz v t s. ignore_throw (write_memtS BCa BCv wk addr sz v t) s = write_memtS BCa BCv wk addr sz v t s"
   "\<And>s. ignore_throw (excl_resultS ()) s = excl_resultS () s"
   "\<And>s. ignore_throw (undefined_boolS ()) s = undefined_boolS () s"
-  unfolding read_mem_bytesS_def read_memt_bytesS_def read_memtS_def read_memS_def read_tagS_def write_memS_def
-  unfolding write_mem_bytesS_def
+  unfolding read_mem_bytesS_def read_memt_bytesS_def read_memtS_def read_memS_def read_tagS_def
+  unfolding write_memS_def write_memtS_def write_mem_bytesS_def write_memt_bytesS_def
   unfolding excl_resultS_def undefined_boolS_def maybe_failS_def
   unfolding ignore_throw_bindS
   by (auto cong: bindS_cong bindS_ext_cong ignore_throw_cong option.case_cong
diff --git a/src/gen_lib/sail2_prompt_monad.lem b/src/gen_lib/sail2_prompt_monad.lem
index cf2fd151..7a55056c 100644
--- a/src/gen_lib/sail2_prompt_monad.lem
+++ b/src/gen_lib/sail2_prompt_monad.lem
@@ -18,8 +18,9 @@ type monad 'regval 'a 'e =
   | Write_ea of write_kind * nat * nat * monad 'regval 'a 'e
   (* Request the result of store-exclusive *)
   | Excl_res of (bool -> monad 'regval 'a 'e)
-  (* Request to write a memory value of the given size together with a tag
-     at the given address. *)
+  (* Request to write a memory value of the given size at the given address,
+     with or without a tag. *)
+  | Write_mem of write_kind * nat * nat * list memory_byte * (bool -> monad 'regval 'a 'e)
   | Write_memt of write_kind * nat * nat * list memory_byte * bitU * (bool -> monad 'regval 'a 'e)
   (* Tell the system to dynamically recalculate dependency footprint *)
   | Footprint of monad 'regval 'a 'e
@@ -43,6 +44,7 @@ type monad 'regval 'a 'e =
 type event 'regval =
   | E_read_mem of read_kind * nat * nat * list memory_byte
   | E_read_memt of read_kind * nat * nat * (list memory_byte * bitU)
+  | E_write_mem of write_kind * nat * nat * list memory_byte * bool
   | E_write_memt of write_kind * nat * nat * list memory_byte * bitU * bool
   | E_write_ea of write_kind * nat * nat
   | E_excl_res of bool
@@ -63,6 +65,7 @@ let rec bind m f = match m with
   | Done a -> f a
   | Read_mem rk a sz k ->       Read_mem rk a sz       (fun v -> bind (k v) f)
   | Read_memt rk a sz k ->      Read_memt rk a sz      (fun v -> bind (k v) f)
+  | Write_mem wk a sz v k ->    Write_mem wk a sz v    (fun v -> bind (k v) f)
   | Write_memt wk a sz v t k -> Write_memt wk a sz v t (fun v -> bind (k v) f)
   | Read_reg descr k ->         Read_reg descr         (fun v -> bind (k v) f)
   | Excl_res k ->               Excl_res               (fun v -> bind (k v) f)
@@ -96,6 +99,7 @@ let rec try_catch m h = match m with
   | Done a -> Done a
   | Read_mem rk a sz k ->       Read_mem rk a sz       (fun v -> try_catch (k v) h)
   | Read_memt rk a sz k ->      Read_memt rk a sz      (fun v -> try_catch (k v) h)
+  | Write_mem wk a sz v k ->    Write_mem wk a sz v    (fun v -> try_catch (k v) h)
   | Write_memt wk a sz v t k -> Write_memt wk a sz v t (fun v -> try_catch (k v) h)
   | Read_reg descr k ->         Read_reg descr         (fun v -> try_catch (k v) h)
   | Excl_res k ->               Excl_res               (fun v -> try_catch (k v) h)
@@ -188,8 +192,17 @@ let write_mem_ea wk addr sz =
     (fun addr -> Write_ea wk addr (nat_of_int sz) (Done ()))
 
 val write_mem : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b =>
+  write_kind -> 'a -> integer -> 'b -> monad 'rv bool 'e
+let write_mem wk addr sz v =
+  match (mem_bytes_of_bits v, nat_of_bv addr) with
+    | (Just v, Just addr) ->
+       Write_mem wk addr (nat_of_int sz) v return
+    | _ -> Fail "write_mem"
+  end
+
+val write_memt : forall 'rv 'a 'b 'e. Bitvector 'a, Bitvector 'b =>
   write_kind -> 'a -> integer -> 'b -> bitU -> monad 'rv bool 'e
-let write_mem wk addr sz v tag =
+let write_memt wk addr sz v tag =
   match (mem_bytes_of_bits v, nat_of_bv addr) with
     | (Just v, Just addr) ->
        Write_memt wk addr (nat_of_int sz) v tag return
@@ -259,6 +272,8 @@ val emitEvent : forall 'regval 'a 'e. Eq 'regval => monad 'regval 'a 'e -> event
 let emitEvent m e = match (e, m) with
   | (E_read_mem rk a sz v, Read_mem rk' a' sz' k) ->
      if rk' = rk && a' = a && sz' = sz then Just (k v) else Nothing
+  | (E_write_mem wk a sz v r, Write_mem wk' a' sz' v' k) ->
+     if wk' = wk && a' = a && sz' = sz && v' = v then Just (k r) else Nothing
   | (E_write_memt wk a sz v tag r, Write_memt wk' a' sz' v' tag' k) ->
      if wk' = wk && a' = a && sz' = sz && v' = v && tag' = tag then Just (k r) else Nothing
   | (E_read_reg r v, Read_reg r' k) ->
diff --git a/src/gen_lib/sail2_state_lifting.lem b/src/gen_lib/sail2_state_lifting.lem
index a055bfe0..98a5390d 100644
--- a/src/gen_lib/sail2_state_lifting.lem
+++ b/src/gen_lib/sail2_state_lifting.lem
@@ -9,13 +9,14 @@ open import {isabelle} `Sail2_state_monad_lemmas`
 val liftState : forall 'regval 'regs 'a 'e. register_accessors 'regs 'regval -> monad 'regval 'a 'e -> monadS 'regs 'a 'e
 let rec liftState ra m = match m with
   | (Done a)                   -> returnS a
-  | (Read_mem rk a sz k)       -> bindS (read_mem_bytesS rk a sz)      (fun v -> liftState ra (k v))
-  | (Read_memt rk a sz k)      -> bindS (read_memt_bytesS rk a sz)     (fun v -> liftState ra (k v))
-  | (Write_memt wk a sz v t k) -> bindS (write_mem_bytesS wk a sz v t) (fun v -> liftState ra (k v))
-  | (Read_reg r k)             -> bindS (read_regvalS ra r)            (fun v -> liftState ra (k v))
-  | (Excl_res k)               -> bindS (excl_resultS ())              (fun v -> liftState ra (k v))
-  | (Choose _ k)               -> bindS (choose_boolS ())              (fun v -> liftState ra (k v))
-  | (Write_reg r v k)          -> seqS (write_regvalS ra r v)          (liftState ra k)
+  | (Read_mem rk a sz k)       -> bindS (read_mem_bytesS rk a sz)       (fun v -> liftState ra (k v))
+  | (Read_memt rk a sz k)      -> bindS (read_memt_bytesS rk a sz)      (fun v -> liftState ra (k v))
+  | (Write_mem wk a sz v k)    -> bindS (write_mem_bytesS wk a sz v)    (fun v -> liftState ra (k v))
+  | (Write_memt wk a sz v t k) -> bindS (write_memt_bytesS wk a sz v t) (fun v -> liftState ra (k v))
+  | (Read_reg r k)             -> bindS (read_regvalS ra r)             (fun v -> liftState ra (k v))
+  | (Excl_res k)               -> bindS (excl_resultS ())               (fun v -> liftState ra (k v))
+  | (Choose _ k)               -> bindS (choose_boolS ())               (fun v -> liftState ra (k v))
+  | (Write_reg r v k)          -> seqS (write_regvalS ra r v)           (liftState ra k)
   | (Write_ea _ _ _ k)         -> liftState ra k
   | (Footprint k)              -> liftState ra k
   | (Barrier _ k)              -> liftState ra k
@@ -32,6 +33,8 @@ let emitEventS ra e s = match e with
   | E_read_memt _ addr sz (v, tag) ->
      Maybe.bind (get_mem_bytes addr sz s) (fun (v', tag') ->
      if v' = v && tag' = tag then Just s else Nothing)
+  | E_write_mem _ addr sz v success ->
+     if success then Just (put_mem_bytes addr sz v B0 s) else Nothing
   | E_write_memt _ addr sz v tag success ->
      if success then Just (put_mem_bytes addr sz v tag s) else Nothing
   | E_read_reg r v ->
diff --git a/src/gen_lib/sail2_state_monad.lem b/src/gen_lib/sail2_state_monad.lem
index 18e57b30..3042700c 100644
--- a/src/gen_lib/sail2_state_monad.lem
+++ b/src/gen_lib/sail2_state_monad.lem
@@ -162,27 +162,34 @@ let excl_resultS =
 
 (* Write little-endian list of bytes to given address *)
 val put_mem_bytes : forall 'regs. nat -> nat -> list memory_byte -> bitU -> sequential_state 'regs -> sequential_state 'regs
-let put_mem_bytes addr sz v t s =
+let put_mem_bytes addr sz v tag s =
   let addrs = genlist (fun n -> addr + n) sz in
   let a_v = List.zip addrs v in
   let write_byte mem (addr, v) = Map.insert addr v mem in
-  let write_tag mem addr = Map.insert addr t mem in
+  let write_tag mem addr = Map.insert addr tag mem in
   <| s with memstate = List.foldl write_byte s.memstate a_v;
             tagstate = List.foldl write_tag s.tagstate addrs |>
 
-val write_mem_bytesS : forall 'regs 'e. write_kind -> nat -> nat -> list memory_byte -> bitU -> monadS 'regs bool 'e
-let write_mem_bytesS _ addr sz v t =
+val write_memt_bytesS : forall 'regs 'e. write_kind -> nat -> nat -> list memory_byte -> bitU -> monadS 'regs bool 'e
+let write_memt_bytesS _ addr sz v t =
   updateS (put_mem_bytes addr sz v t) >>$
   returnS true
 
-val write_memS : forall 'regs 'e 'a 'b. Bitvector 'a, Bitvector 'b =>
-  write_kind -> 'a -> nat -> 'b -> bitU -> monadS 'regs bool 'e
-let write_memS wk addr sz v t =
+val write_mem_bytesS : forall 'regs 'e. write_kind -> nat -> nat -> list memory_byte -> monadS 'regs bool 'e
+let write_mem_bytesS wk addr sz v = write_memt_bytesS wk addr sz v B0
+
+val write_memtS : forall 'regs 'e 'a 'b. Bitvector 'a, Bitvector 'b =>
+  write_kind -> 'a -> integer -> 'b -> bitU -> monadS 'regs bool 'e
+let write_memtS wk addr sz v t =
   match (nat_of_bv addr, mem_bytes_of_bits v) with
-    | (Just addr, Just v) -> write_mem_bytesS wk addr sz v t
+    | (Just addr, Just v) -> write_memt_bytesS wk addr (nat_of_int sz) v t
     | _ -> failS "write_mem"
   end
 
+val write_memS : forall 'regs 'e 'a 'b. Bitvector 'a, Bitvector 'b =>
+  write_kind -> 'a -> integer -> 'b -> monadS 'regs bool 'e
+let write_memS wk addr sz v = write_memtS wk addr sz v B0
+
 val read_regS : forall 'regs 'rv 'a 'e. register_ref 'regs 'rv 'a -> monadS 'regs 'a 'e
 let read_regS reg = readS (fun s -> reg.read_from s.regstate)
 
-- 
cgit v1.2.3


From 886cff213039c034bc78408ea52689514e0c9a69 Mon Sep 17 00:00:00 2001
From: Thomas Bauereiss
Date: Thu, 3 Jan 2019 18:31:04 +0000
Subject: Add a few helper lemmas

---
 lib/isabelle/Sail2_prompt_monad_lemmas.thy | 220 ++++++++++++++++++++++++++---
 src/gen_lib/sail2_prompt_monad.lem         |   2 +
 2 files changed, 206 insertions(+), 16 deletions(-)

diff --git a/lib/isabelle/Sail2_prompt_monad_lemmas.thy b/lib/isabelle/Sail2_prompt_monad_lemmas.thy
index 3658296b..1fde3287 100644
--- a/lib/isabelle/Sail2_prompt_monad_lemmas.thy
+++ b/lib/isabelle/Sail2_prompt_monad_lemmas.thy
@@ -44,6 +44,9 @@ inductive_set T :: "(('rv, 'a, 'e) monad \<times> 'rv event \<times> ('rv, 'a, '
 | Choose: "((Choose descr k), E_choose descr v, k v) \<in> T"
 | Print: "((Print msg k), E_print msg, k) \<in> T"
 
+lemma emitEvent_iff_T: "emitEvent m e = Some m' \<longleftrightarrow> (m, e, m') \<in> T"
+  by (cases e) (auto simp: emitEvent_def elim: T.cases intro: T.intros split: monad.splits)
+
 inductive_set Traces :: "(('rv, 'a, 'e) monad \<times> 'rv event list \<times> ('rv, 'a, 'e) monad) set" where
   Nil: "(s, [], s) \<in> Traces"
 | Step: "\<lbrakk>(s, e, s'') \<in> T; (s'', t, s') \<in> Traces\<rbrakk> \<Longrightarrow> (s, e # t, s') \<in> Traces"
@@ -58,6 +61,12 @@ lemmas Traces_ConsI = T.intros[THEN Step, rotated]
 inductive_cases Traces_NilE[elim]: "(s, [], s') \<in> Traces"
 inductive_cases Traces_ConsE[elim]: "(s, e # t, s') \<in> Traces"
 
+lemma runTrace_iff_Traces: "runTrace t m = Some m' \<longleftrightarrow> (m, t, m') \<in> Traces"
+  by (induction t m rule: runTrace.induct; fastforce simp: bind_eq_Some_conv emitEvent_iff_T)
+
+lemma hasTrace_iff_Traces_final: "hasTrace t m \<longleftrightarrow> (\<exists>m'. (m, t, m') \<in> Traces \<and> final m')"
+  by (auto simp: hasTrace_def runTrace_iff_Traces[symmetric] split: option.splits)
+
 lemma Traces_cases:
   fixes m :: "('rv, 'a, 'e) monad"
   assumes Run: "(m, t, m') \<in> Traces"
@@ -91,10 +100,29 @@ qed
 abbreviation Run :: "('rv, 'a, 'e) monad \<Rightarrow> 'rv event list \<Rightarrow> 'a \<Rightarrow> bool"
   where "Run s t a \<equiv> (s, t, Done a) \<in> Traces"
 
-lemma Run_appendI:
+lemma final_cases:
+  assumes "final m"
+  obtains (Done) a where "m = Done a" | (Fail) f where "m = Fail f" | (Ex) e where "m = Exception e"
+  using assms by (cases m) (auto simp: final_def)
+
+lemma hasTraces_elim:
+  assumes "hasTrace t m"
+  obtains m' where "(m, t, m') \<in> Traces" and "final m'"
+  using assms
+  unfolding hasTrace_iff_Traces_final
+  by blast
+
+lemma hasTrace_cases:
+  assumes "hasTrace t m"
+  obtains (Run) a where "Run m t a"
+  | (Fail) f where "(m, t, Fail f) \<in> Traces"
+  | (Ex) e where "(m, t, Exception e) \<in> Traces"
+  using assms by (elim hasTraces_elim final_cases) auto
+
+lemma Traces_appendI:
   assumes "(s, t1, s') \<in> Traces"
-    and "Run s' t2 a"
-  shows "Run s (t1 @ t2) a"
+    and "(s', t2, s'') \<in> Traces"
+  shows "(s, t1 @ t2, s'') \<in> Traces"
 proof (use assms in \<open>induction t1 arbitrary: s\<close>)
   case (Cons e t1)
   then show ?case by (elim Traces_ConsE) auto
@@ -107,20 +135,188 @@ lemma bind_DoneE:
 
 lemma bind_T_cases:
   assumes "(bind m f, e, s') \<in> T"
-  obtains (Done) a where "m = Done a"
+  obtains (Done) a where "m = Done a" and "(f a, e, s') \<in> T"
   | (Bind) m' where "s' = bind m' f" and "(m, e, m') \<in> T"
-  using assms by (cases; blast elim: bind.elims)
+  using assms by (cases; fastforce elim: bind.elims)
 
-lemma Run_bindI:
+lemma Traces_bindI:
   fixes m :: "('r, 'a, 'e) monad"
   assumes "Run m t1 a1"
-    and "Run (f a1) t2 a2"
-  shows "Run (m \<bind> f) (t1 @ t2) a2"
+    and "(f a1, t2, m') \<in> Traces"
+  shows "(m \<bind> f, t1 @ t2, m') \<in> Traces"
 proof (use assms in \<open>induction m t1 "Done a1 :: ('r, 'a, 'e) monad" rule: Traces.induct\<close>)
   case (Step s e s'' t)
   then show ?case by (elim T.cases) auto
 qed auto
 
+lemma Run_DoneE:
+  assumes "Run (Done a) t a'"
+  obtains "t = []" and "a' = a"
+  using assms by (auto elim: Traces.cases T.cases)
+
+lemma Run_Done_iff_Nil[simp]: "Run (Done a) t a' \<longleftrightarrow> t = [] \<and> a' = a"
+  by (auto elim: Run_DoneE)
+
+lemma Run_Nil_iff_Done: "Run m [] a \<longleftrightarrow> m = Done a"
+  by auto
+
+lemma Traces_Nil_iff: "(m, [], m') \<in> Traces \<longleftrightarrow> m' = m"
+  by auto
+
+lemma bind_Traces_cases:
+  assumes "(m \<bind> f, t, m') \<in> Traces"
+  obtains (Left) m'' where "(m, t, m'') \<in> Traces" and "m' = m'' \<bind> f"
+  | (Bind) tm am tf where "t = tm @ tf" and "Run m tm am" and "(f am, tf, m') \<in> Traces"
+proof (use assms in \<open>induction "bind m f" t m' arbitrary: m rule: Traces.induct\<close>)
+  case Nil
+  then show ?case by (auto simp: Traces_Nil_iff)
+next
+  case (Step e s'' t s')
+  note IH = Step(3)
+  note Left' = Step(4)
+  note Bind' = Step(5)
+  show thesis
+  proof (use \<open>(m \<bind> f, e, s'') \<in> T\<close> in \<open>cases rule: bind_T_cases\<close>)
+    case (Done a)
+    then show ?thesis using \<open>(s'', t, s') \<in> Traces\<close> Step(5)[of "[]" "e # t" a] by auto
+  next
+    case (Bind m')
+    show ?thesis
+    proof (rule IH)
+      show "s'' = m' \<bind> f" using Bind by blast
+    next
+      fix m''
+      assume "(m', t, m'') \<in> Traces" and "s' = m'' \<bind> f"
+      then show thesis using \<open>(m, e, m') \<in> T\<close> Left'[of m''] by auto
+    next
+      fix tm tf am
+      assume "t = tm @ tf" and "Run m' tm am" and "(f am, tf, s') \<in> Traces"
+      then show thesis using \<open>(m, e, m') \<in> T\<close> Bind'[of "e # tm" tf am] by auto
+    qed
+  qed
+qed
+
+lemma final_bind_cases:
+  assumes "final (m \<bind> f)"
+  obtains (Done) a where "m = Done a" and "final (f a)"
+  | (Fail) msg where "m = Fail msg"
+  | (Ex) e where "m = Exception e"
+  using assms by (cases m) (auto simp: final_def)
+
+lemma hasFailure_iff_Traces_Fail: "hasFailure t m \<longleftrightarrow> (\<exists>msg. (m, t, Fail msg) \<in> Traces)"
+  by (auto simp: hasFailure_def runTrace_iff_Traces[symmetric] split: option.splits monad.splits)
+
+lemma hasException_iff_Traces_Exception: "hasException t m \<longleftrightarrow> (\<exists>e. (m, t, Exception e) \<in> Traces)"
+  by (auto simp: hasException_def runTrace_iff_Traces[symmetric] split: option.splits monad.splits)
+
+lemma hasTrace_bind_cases:
+  assumes "hasTrace t (m \<bind> f)"
+  obtains (Bind) tm am tf where "t = tm @ tf" and "Run m tm am" and "hasTrace tf (f am)"
+  | (Fail) "hasFailure t m"
+  | (Ex) "hasException t m"
+proof -
+  from assms obtain m' where t: "(m \<bind> f, t, m') \<in> Traces" and m': "final m'"
+    by (auto simp: hasTrace_iff_Traces_final)
+  note [simp] = hasTrace_iff_Traces_final hasFailure_iff_Traces_Fail hasException_iff_Traces_Exception
+  from t show thesis
+  proof (cases rule: bind_Traces_cases)
+    case (Left m'')
+    then show ?thesis
+      using m' Fail Ex Bind[of t "[]"]
+      by (fastforce elim!: final_bind_cases)
+  next
+    case (Bind tm am tf)
+    then show ?thesis
+      using m' that
+      by fastforce
+  qed
+qed
+
+lemma try_catch_T_cases:
+  assumes "(try_catch m h, e, m') \<in> T"
+  obtains (NoEx) m'' where "(m, e, m'') \<in> T" and "m' = try_catch m'' h"
+  | (Ex) ex where "m = Exception ex" and "(h ex, e, m') \<in> T"
+  using assms
+  by (cases m) (auto elim!: T.cases)
+
+lemma try_catch_Traces_cases:
+  assumes "(try_catch m h, t, mtc) \<in> Traces"
+  obtains (NoEx) m' where "(m, t, m') \<in> Traces" and "mtc = try_catch m' h"
+  | (Ex) tm ex th where "(m, tm, Exception ex) \<in> Traces" and "(h ex, th, mtc) \<in> Traces" and "t = tm @ th"
+proof (use assms in \<open>induction "try_catch m h" t mtc arbitrary: m rule: Traces.induct\<close>)
+  case Nil
+  then show ?case by auto
+next
+  case (Step e mtc' t mtc)
+  note e = \<open>(try_catch m h, e, mtc') \<in> T\<close>
+  note t = \<open>(mtc', t, mtc) \<in> Traces\<close>
+  note IH = Step(3)
+  note NoEx_ConsE = Step(4)
+  note Ex_ConsE = Step(5)
+  show ?case
+  proof (use e in \<open>cases rule: try_catch_T_cases\<close>)
+    case (NoEx m1)
+    show ?thesis
+    proof (rule IH)
+      show "mtc' = try_catch m1 h" using NoEx by auto
+    next
+      fix m'
+      assume "(m1, t, m') \<in> Traces" and "mtc = try_catch m' h"
+      then show ?thesis
+        using NoEx NoEx_ConsE[of m']
+        by auto
+    next
+      fix tm ex th
+      assume "(m1, tm, Exception ex) \<in> Traces" and "(h ex, th, mtc) \<in> Traces" and "t = tm @ th"
+      then show ?thesis
+        using NoEx Ex_ConsE[of "e # tm" ex th]
+        by auto
+    qed
+  next
+    case (Ex ex)
+    then show ?thesis
+      using t Ex_ConsE[of "[]" ex "e # t"]
+      by auto
+  qed
+qed
+
+lemma Done_Traces_iff[simp]: "(Done a, t, m') \<in> Traces \<longleftrightarrow> t = [] \<and> m' = Done a"
+  by (auto elim: Traces_cases)
+
+lemma Fail_Traces_iff[simp]: "(Fail msg, t, m') \<in> Traces \<longleftrightarrow> t = [] \<and> m' = Fail msg"
+  by (auto elim: Traces_cases)
+
+lemma Exception_Traces_iff[simp]: "(Exception e, t, m') \<in> Traces \<longleftrightarrow> t = [] \<and> m' = Exception e"
+  by (auto elim: Traces_cases)
+
+lemma Read_reg_TracesE:
+  assumes "(Read_reg r k, t, m') \<in> Traces"
+  obtains (Nil) "t = []" and "m' = Read_reg r k"
+  | (Cons) v t' where "t = E_read_reg r v # t'" and "(k v, t', m') \<in> Traces"
+  using assms
+  by (auto elim: Traces_cases)
+
+lemma Write_reg_TracesE:
+  assumes "(Write_reg r v k, t, m') \<in> Traces"
+  obtains (Nil) "t = []" and "m' = Write_reg r v k"
+  | (Cons) t' where "t = E_write_reg r v # t'" and "(k, t', m') \<in> Traces"
+  using assms
+  by (auto elim: Traces_cases)
+
+lemma Write_ea_TracesE:
+  assumes "(Write_ea wk addr sz k, t, m') \<in> Traces"
+  obtains (Nil) "t = []" and "m' = Write_ea wk addr sz k"
+  | (Cons) t' where "t = E_write_ea wk addr sz # t'" and "(k, t', m') \<in> Traces"
+  using assms
+  by (auto elim: Traces_cases)
+
+lemma Write_memt_TracesE:
+  assumes "(Write_memt wk addr sz v tag k, t, m') \<in> Traces"
+  obtains (Nil) "t = []" and "m' = Write_memt wk addr sz v tag k"
+  | (Cons) t' r where "t = E_write_memt wk addr sz v tag r # t'" and "(k r, t', m') \<in> Traces"
+  using assms
+  by (auto elim: Traces_cases)
+
 lemma Run_bindE:
   fixes m :: "('rv, 'b, 'e) monad" and a :: 'a
   assumes "Run (bind m f) t a"
@@ -145,14 +341,6 @@ next
   qed
 qed
 
-lemma Run_DoneE:
-  assumes "Run (Done a) t a'"
-  obtains "t = []" and "a' = a"
-  using assms by (auto elim: Traces.cases T.cases)
-
-lemma Run_Done_iff_Nil[simp]: "Run (Done a) t a' \<longleftrightarrow> t = [] \<and> a' = a"
-  by (auto elim: Run_DoneE)
-
 lemma Run_bindE_ignore_trace:
   assumes "Run (m \<bind> f) t a"
   obtains tm tf am where "Run m tm am" and "Run (f am) tf a"
diff --git a/src/gen_lib/sail2_prompt_monad.lem b/src/gen_lib/sail2_prompt_monad.lem
index 7a55056c..e0ac09f6 100644
--- a/src/gen_lib/sail2_prompt_monad.lem
+++ b/src/gen_lib/sail2_prompt_monad.lem
@@ -272,6 +272,8 @@ val emitEvent : forall 'regval 'a 'e. Eq 'regval => monad 'regval 'a 'e -> event
 let emitEvent m e = match (e, m) with
   | (E_read_mem rk a sz v, Read_mem rk' a' sz' k) ->
      if rk' = rk && a' = a && sz' = sz then Just (k v) else Nothing
+  | (E_read_memt rk a sz vt, Read_memt rk' a' sz' k) ->
+     if rk' = rk && a' = a && sz' = sz then Just (k vt) else Nothing
   | (E_write_mem wk a sz v r, Write_mem wk' a' sz' v' k) ->
      if wk' = wk && a' = a && sz' = sz && v' = v then Just (k r) else Nothing
   | (E_write_memt wk a sz v tag r, Write_memt wk' a' sz' v' tag' k) ->
-- 
cgit v1.2.3