Sail2_state_monad.thy

chapter \<open>Generated by Lem from \<open>../../src/gen_lib/sail2_state_monad.lem\<close>.\<close>

theory "Sail2_state_monad" 

imports
  Main
  "LEM.Lem_pervasives_extra"
  "Sail2_instr_kinds"
  "Sail2_values"

begin 

(*open import Pervasives_extra*)
(*open import Sail2_instr_kinds*)
(*open import Sail2_values*)

(* 'a is result type *)

type_synonym memstate =" (int, memory_byte) Map.map "
type_synonym tagstate =" (int, bitU) Map.map "
(* type regstate = map string (vector bitU) *)

record 'regs sequential_state =
  
 regstate ::" 'regs " 

     memstate ::" memstate " 

     tagstate ::" tagstate " 

     write_ea ::"  (write_kind * int * int)option " 

     last_exclusive_operation_was_load ::" bool " 


(*val init_state : forall 'regs. 'regs -> sequential_state 'regs*)
definition init_state  :: " 'regs \<Rightarrow> 'regs sequential_state "  where 
     " init_state regs = (
  (| regstate = regs,
     memstate = Map.empty,
     tagstate = Map.empty,
     write_ea = None,
     last_exclusive_operation_was_load = False |) )"


datatype 'e ex =
    Failure " string "
  | Throw " 'e "

datatype( 'a, 'e) result =
    Value " 'a "
  | Ex " ( 'e ex)"

(* State, nondeterminism and exception monad with result value type 'a
   and exception type 'e. *)
type_synonym( 'regs, 'a, 'e) monadS =" 'regs sequential_state \<Rightarrow> ( ('a, 'e)result * 'regs sequential_state) set "

(*val returnS : forall 'regs 'a 'e. 'a -> monadS 'regs 'a 'e*)
definition returnS  :: " 'a \<Rightarrow> 'regs sequential_state \<Rightarrow>(('a,'e)result*'regs sequential_state)set "  where 
     " returnS a s = ( {(Value a,s)})"


(*val bindS : forall 'regs 'a 'b 'e. monadS 'regs 'a 'e -> ('a -> monadS 'regs 'b 'e) -> monadS 'regs 'b 'e*)
definition bindS  :: "('regs sequential_state \<Rightarrow>(('a,'e)result*'regs sequential_state)set)\<Rightarrow>('a \<Rightarrow> 'regs sequential_state \<Rightarrow>(('b,'e)result*'regs sequential_state)set)\<Rightarrow> 'regs sequential_state \<Rightarrow>(('b,'e)result*'regs sequential_state)set "  where 
     " bindS m f (s :: 'regs sequential_state) = (
  \<Union> (Set.image (\<lambda>x .  
  (case  x of   (Value a, s') => f a s' | (Ex e, s') => {(Ex e, s')} )) (m s)))"


(*val seqS: forall 'regs 'b 'e. monadS 'regs unit 'e -> monadS 'regs 'b 'e -> monadS 'regs 'b 'e*)
definition seqS  :: "('regs sequential_state \<Rightarrow>(((unit),'e)result*'regs sequential_state)set)\<Rightarrow>('regs sequential_state \<Rightarrow>(('b,'e)result*'regs sequential_state)set)\<Rightarrow> 'regs sequential_state \<Rightarrow>(('b,'e)result*'regs sequential_state)set "  where 
     " seqS m n = ( bindS m ( \<lambda>x .  
  (case  x of (_ :: unit) => n )))"


(*val chooseS : forall 'regs 'a 'e. SetType 'a => set 'a -> monadS 'regs 'a 'e*)
definition chooseS  :: " 'a set \<Rightarrow> 'regs sequential_state \<Rightarrow>(('a,'e)result*'regs sequential_state)set "  where 
     " chooseS xs s = ( Set.image (\<lambda> x .  (Value x, s)) xs )"


(*val readS : forall 'regs 'a 'e. (sequential_state 'regs -> 'a) -> monadS 'regs 'a 'e*)
definition readS  :: "('regs sequential_state \<Rightarrow> 'a)\<Rightarrow> 'regs sequential_state \<Rightarrow>(('a,'e)result*'regs sequential_state)set "  where 
     " readS f = ( (\<lambda> s .  returnS (f s) s))"


(*val updateS : forall 'regs 'e. (sequential_state 'regs -> sequential_state 'regs) -> monadS 'regs unit 'e*)
definition updateS  :: "('regs sequential_state \<Rightarrow> 'regs sequential_state)\<Rightarrow> 'regs sequential_state \<Rightarrow>(((unit),'e)result*'regs sequential_state)set "  where 
     " updateS f = ( (\<lambda> s .  returnS ()  (f s)))"


(*val failS : forall 'regs 'a 'e. string -> monadS 'regs 'a 'e*)
definition failS  :: " string \<Rightarrow> 'regs sequential_state \<Rightarrow>(('a,'e)result*'regs sequential_state)set "  where 
     " failS msg s = ( {(Ex (Failure msg), s)})"


(*val undefined_boolS : forall 'regval 'regs 'a 'e. unit -> monadS 'regs bool 'e*)
definition undefined_boolS  :: " unit \<Rightarrow> 'regs sequential_state \<Rightarrow>(((bool),'e)result*'regs sequential_state)set "  where 
     " undefined_boolS _ = ( chooseS {False, True})"


(*val exitS : forall 'regs 'e 'a. unit -> monadS 'regs 'a 'e*)
definition exitS  :: " unit \<Rightarrow> 'regs sequential_state \<Rightarrow>(('a,'e)result*'regs sequential_state)set "  where 
     " exitS _ = ( failS (''exit''))"


(*val throwS : forall 'regs 'a 'e. 'e -> monadS 'regs 'a 'e*)
definition throwS  :: " 'e \<Rightarrow> 'regs sequential_state \<Rightarrow>(('a,'e)result*'regs sequential_state)set "  where 
     " throwS e s = ( {(Ex (Throw e), s)})"


(*val try_catchS : forall 'regs 'a 'e1 'e2. monadS 'regs 'a 'e1 -> ('e1 -> monadS 'regs 'a 'e2) ->  monadS 'regs 'a 'e2*)
definition try_catchS  :: "('regs sequential_state \<Rightarrow>(('a,'e1)result*'regs sequential_state)set)\<Rightarrow>('e1 \<Rightarrow> 'regs sequential_state \<Rightarrow>(('a,'e2)result*'regs sequential_state)set)\<Rightarrow> 'regs sequential_state \<Rightarrow>(('a,'e2)result*'regs sequential_state)set "  where 
     " try_catchS m h s = (
  \<Union> (Set.image (\<lambda>x .  
  (case  x of
        (Value a, s') => returnS a s'
    | (Ex (Throw e), s') => h e s'
    | (Ex (Failure msg), s') => {(Ex (Failure msg), s')}
  )) (m s)))"


(*val assert_expS : forall 'regs 'e. bool -> string -> monadS 'regs unit 'e*)
definition assert_expS  :: " bool \<Rightarrow> string \<Rightarrow> 'regs sequential_state \<Rightarrow>(((unit),'e)result*'regs sequential_state)set "  where 
     " assert_expS exp1 msg = ( if exp1 then returnS ()  else failS msg )"


(* For early return, we abuse exceptions by throwing and catching
   the return value. The exception type is either 'r 'e, where Right e
   represents a proper exception and Left r an early return of value r. *)
type_synonym( 'regs, 'a, 'r, 'e) monadRS =" ('regs, 'a, ( ('r, 'e)sum)) monadS "

(*val early_returnS : forall 'regs 'a 'r 'e. 'r -> monadRS 'regs 'a 'r 'e*)
definition early_returnS  :: " 'r \<Rightarrow> 'regs sequential_state \<Rightarrow>(('a,(('r,'e)sum))result*'regs sequential_state)set "  where 
     " early_returnS r = ( throwS (Inl r))"


(*val catch_early_returnS : forall 'regs 'a 'e. monadRS 'regs 'a 'a 'e -> monadS 'regs 'a 'e*)
definition catch_early_returnS  :: "('regs sequential_state \<Rightarrow>(('a,(('a,'e)sum))result*'regs sequential_state)set)\<Rightarrow> 'regs sequential_state \<Rightarrow>(('a,'e)result*'regs sequential_state)set "  where 
     " catch_early_returnS m = (
  try_catchS m
    (\<lambda>x .  (case  x of   Inl a => returnS a | Inr e => throwS e )))"


(* Lift to monad with early return by wrapping exceptions *)
(*val liftRS : forall 'a 'r 'regs 'e. monadS 'regs 'a 'e -> monadRS 'regs 'a 'r 'e*)
definition liftRS  :: "('regs sequential_state \<Rightarrow>(('a,'e)result*'regs sequential_state)set)\<Rightarrow> 'regs sequential_state \<Rightarrow>(('a,(('r,'e)sum))result*'regs sequential_state)set "  where 
     " liftRS m = ( try_catchS m (\<lambda> e .  throwS (Inr e)))"


(* Catch exceptions in the presence of early returns *)
(*val try_catchRS : forall 'regs 'a 'r 'e1 'e2. monadRS 'regs 'a 'r 'e1 -> ('e1 -> monadRS 'regs 'a 'r 'e2) ->  monadRS 'regs 'a 'r 'e2*)
definition try_catchRS  :: "('regs sequential_state \<Rightarrow>(('a,(('r,'e1)sum))result*'regs sequential_state)set)\<Rightarrow>('e1 \<Rightarrow> 'regs sequential_state \<Rightarrow>(('a,(('r,'e2)sum))result*'regs sequential_state)set)\<Rightarrow> 'regs sequential_state \<Rightarrow>(('a,(('r,'e2)sum))result*'regs sequential_state)set "  where 
     " try_catchRS m h = (
  try_catchS m
    (\<lambda>x .  (case  x of   Inl r => throwS (Inl r) | Inr e => h e )))"


(*val maybe_failS : forall 'regs 'a 'e. string -> maybe 'a -> monadS 'regs 'a 'e*)
definition maybe_failS  :: " string \<Rightarrow> 'a option \<Rightarrow> 'regs sequential_state \<Rightarrow>(('a,'e)result*'regs sequential_state)set "  where 
     " maybe_failS msg = ( \<lambda>x .  
  (case  x of   Some a => returnS a | None => failS msg ) )"


(*val read_tagS : forall 'regs 'a 'e. Bitvector 'a => 'a -> monadS 'regs bitU 'e*)
definition read_tagS  :: " 'a Bitvector_class \<Rightarrow> 'a \<Rightarrow>('regs,(bitU),'e)monadS "  where 
     " read_tagS dict_Sail2_values_Bitvector_a addr = ( bindS
  (maybe_failS (''unsigned'') (
  (unsigned_method   dict_Sail2_values_Bitvector_a) addr)) (\<lambda> addr . 
  readS (\<lambda> s .  case_option B0 id ((tagstate   s) addr))))"


(* 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*)
definition read_mem_bytesS  :: " 'a Bitvector_class \<Rightarrow> read_kind \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow>('regs,(((bitU)list)list),'e)monadS "  where 
     " read_mem_bytesS dict_Sail2_values_Bitvector_a read_kind addr sz = ( bindS
  (maybe_failS (''unsigned'') (
  (unsigned_method   dict_Sail2_values_Bitvector_a) addr)) (\<lambda> addr . 
  (let sz = (int sz) in
  (let addrs = (index_list addr ((addr+sz)-( 1 :: int))(( 1 :: int))) in  
  (let read_byte = (\<lambda> s addr .  (memstate   s) addr) in
  bindS (readS (\<lambda> s .  just_list (List.map (read_byte s) addrs)))
    (\<lambda>x .  (case  x of
                         Some mem_val => seqS
                                           (updateS
                                              (\<lambda> s . 
                                               if read_is_exclusive read_kind
                                               then
                                                 ( s (| last_exclusive_operation_was_load := True |))
                                               else s)) (returnS mem_val)
                     | None => failS (''read_memS'')
                   )))))))"


(*val read_memS : forall 'regs 'e 'a 'b. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monadS 'regs 'b 'e*)
definition read_memS  :: " 'a Bitvector_class \<Rightarrow> 'b Bitvector_class \<Rightarrow> read_kind \<Rightarrow> 'a \<Rightarrow> int \<Rightarrow>('regs,'b,'e)monadS "  where 
     " read_memS dict_Sail2_values_Bitvector_a dict_Sail2_values_Bitvector_b rk a sz = ( bindS
  (read_mem_bytesS dict_Sail2_values_Bitvector_a rk a (nat_of_int sz)) (\<lambda> bytes . 
  maybe_failS (''bits_of_mem_bytes'') (
  (of_bits_method   dict_Sail2_values_Bitvector_b) (bits_of_mem_bytes bytes))))"


(*val excl_resultS : forall 'regs 'e. unit -> monadS 'regs bool 'e*)
definition excl_resultS  :: " unit \<Rightarrow>('regs,(bool),'e)monadS "  where 
     " excl_resultS _ = ( bindS
  (readS (\<lambda> s . (last_exclusive_operation_was_load   s))) (\<lambda> excl_load .  seqS
  (updateS (\<lambda> s .  ( s (| 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*)
definition write_mem_eaS  :: " 'a Bitvector_class \<Rightarrow> write_kind \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow>('regs,(unit),'e)monadS "  where 
     " write_mem_eaS dict_Sail2_values_Bitvector_a write_kind addr sz = ( bindS
  (maybe_failS (''unsigned'') (
  (unsigned_method   dict_Sail2_values_Bitvector_a) addr)) (\<lambda> addr . 
  (let sz = (int sz) in
  updateS (\<lambda> s .  ( s (| write_ea := (Some (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*)
definition write_mem_bytesS  :: "((bitU)list)list \<Rightarrow>('regs,(bool),'e)monadS "  where 
     " write_mem_bytesS v = ( bindS
  (readS (\<lambda> s . (write_ea   s))) (\<lambda>x .  
  (case  x of
        None => failS (''write ea has not been announced yet'')
    | Some (_, addr, sz) =>
  (let addrs = (index_list addr ((addr + sz) - ( 1 :: int)) (( 1 :: int))) in
  (*let v = external_mem_value (bits_of v) in*)
  (let a_v = (List.zip addrs v) in
  (let write_byte = (\<lambda>mem p .  (case  (mem ,p ) of
                                           ( mem , (addr, v) ) => map_update
                                                                    addr 
                                                                  v mem
                                       )) in
  seqS
    (updateS
       (\<lambda> s . 
        ( s (| memstate := (List.foldl write_byte (memstate   s) a_v) |))))
    (returnS True))))
  )))"


(*val write_mem_valS : forall 'regs 'e 'a. Bitvector 'a => 'a -> monadS 'regs bool 'e*)
definition write_mem_valS  :: " 'a Bitvector_class \<Rightarrow> 'a \<Rightarrow> 'regs sequential_state \<Rightarrow>(((bool),'e)result*'regs sequential_state)set "  where 
     " write_mem_valS dict_Sail2_values_Bitvector_a v = ( (case  mem_bytes_of_bits 
  dict_Sail2_values_Bitvector_a v of
    Some v => write_mem_bytesS v
  | None => failS (''write_mem_val'')
))"


(*val write_tagS : forall 'regs 'a 'e. Bitvector 'a => 'a -> bitU -> monadS 'regs bool 'e*)
definition write_tagS  :: " 'a Bitvector_class \<Rightarrow> 'a \<Rightarrow> bitU \<Rightarrow>('regs,(bool),'e)monadS "  where 
     " write_tagS dict_Sail2_values_Bitvector_a addr t = ( bindS
   (maybe_failS (''unsigned'') (
  (unsigned_method   dict_Sail2_values_Bitvector_a) addr)) (\<lambda> addr .  seqS
   (updateS (\<lambda> s .  ( s (| tagstate := (map_update addr t(tagstate   s)) |))))
   (returnS True)))"


(*val read_regS : forall 'regs 'rv 'a 'e. register_ref 'regs 'rv 'a -> monadS 'regs 'a 'e*)
definition read_regS  :: "('regs,'rv,'a)register_ref \<Rightarrow> 'regs sequential_state \<Rightarrow>(('a,'e)result*'regs sequential_state)set "  where 
     " read_regS reg = ( readS (\<lambda> s . (read_from   reg)(regstate   s)))"


(* TODO
let read_reg_range reg i j state =
  let v = slice (get_reg state (name_of_reg reg)) i j in
  [(Value (vec_to_bvec v),state)]
let read_reg_bit reg i state =
  let v = access (get_reg state (name_of_reg reg)) i in
  [(Value v,state)]
let read_reg_field reg regfield =
  let (i,j) = register_field_indices reg regfield in
  read_reg_range reg i j
let read_reg_bitfield reg regfield =
  let (i,_) = register_field_indices reg regfield in
  read_reg_bit reg i *)

(*val read_regvalS : forall 'regs 'rv 'e.
  register_accessors 'regs 'rv -> string -> monadS 'regs 'rv 'e*)
fun read_regvalS  :: "(string \<Rightarrow> 'regs \<Rightarrow> 'rv option)*(string \<Rightarrow> 'rv \<Rightarrow> 'regs \<Rightarrow> 'regs option)\<Rightarrow> string \<Rightarrow>('regs,'rv,'e)monadS "  where 
     " read_regvalS (read, _) reg = ( bindS
  (readS (\<lambda> s .  read reg(regstate   s))) (\<lambda>x .  
  (case  x of
        Some v => returnS v
    | None => failS ((''read_regvalS '') @ reg)
  )))"


(*val write_regvalS : forall 'regs 'rv 'e.
  register_accessors 'regs 'rv -> string -> 'rv -> monadS 'regs unit 'e*)
fun write_regvalS  :: "(string \<Rightarrow> 'regs \<Rightarrow> 'rv option)*(string \<Rightarrow> 'rv \<Rightarrow> 'regs \<Rightarrow> 'regs option)\<Rightarrow> string \<Rightarrow> 'rv \<Rightarrow>('regs,(unit),'e)monadS "  where 
     " write_regvalS (_, write1) reg v = ( bindS
  (readS (\<lambda> s .  write1 reg v(regstate   s))) (\<lambda>x .  
  (case  x of
        Some rs' => updateS (\<lambda> s .  ( s (| regstate := rs' |)))
    | None => failS ((''write_regvalS '') @ reg)
  )))"


(*val write_regS : forall 'regs 'rv 'a 'e. register_ref 'regs 'rv 'a -> 'a -> monadS 'regs unit 'e*)
definition write_regS  :: "('regs,'rv,'a)register_ref \<Rightarrow> 'a \<Rightarrow> 'regs sequential_state \<Rightarrow>(((unit),'e)result*'regs sequential_state)set "  where 
     " write_regS reg v = (
  updateS (\<lambda> s .  ( s (| regstate := ((write_to   reg) v(regstate   s)) |))))"


(* TODO
val update_reg : forall 'regs 'rv 'a 'b 'e. register_ref 'regs 'rv 'a -> ('a -> 'b -> 'a) -> 'b -> monadS 'regs unit 'e
let update_reg reg f v state =
  let current_value = get_reg state reg in
  let new_value = f current_value v in
  [(Value (), set_reg state reg new_value)]

let write_reg_field reg regfield = update_reg reg regfield.set_field

val update_reg_range : forall 'regs 'rv 'a 'b. Bitvector 'a, Bitvector 'b => register_ref 'regs 'rv 'a -> integer -> integer -> 'a -> 'b -> 'a
let update_reg_range reg i j reg_val new_val = set_bits (reg.is_inc) reg_val i j (bits_of new_val)
let write_reg_range reg i j = update_reg reg (update_reg_range reg i j)

let update_reg_pos reg i reg_val x = update_list reg.is_inc reg_val i x
let write_reg_pos reg i = update_reg reg (update_reg_pos reg i)

let update_reg_bit reg i reg_val bit = set_bit (reg.is_inc) reg_val i (to_bitU bit)
let write_reg_bit reg i = update_reg reg (update_reg_bit reg i)

let update_reg_field_range regfield i j reg_val new_val =
  let current_field_value = regfield.get_field reg_val in
  let new_field_value = set_bits (regfield.field_is_inc) current_field_value i j (bits_of new_val) in
  regfield.set_field reg_val new_field_value
let write_reg_field_range reg regfield i j = update_reg reg (update_reg_field_range regfield i j)

let update_reg_field_pos regfield i reg_val x =
  let current_field_value = regfield.get_field reg_val in
  let new_field_value = update_list regfield.field_is_inc current_field_value i x in
  regfield.set_field reg_val new_field_value
let write_reg_field_pos reg regfield i = update_reg reg (update_reg_field_pos regfield i)

let update_reg_field_bit regfield i reg_val bit =
  let current_field_value = regfield.get_field reg_val in
  let new_field_value = set_bit (regfield.field_is_inc) current_field_value i (to_bitU bit) in
  regfield.set_field reg_val new_field_value
let write_reg_field_bit reg regfield i = update_reg reg (update_reg_field_bit regfield i)*)

(* TODO Add Show typeclass for value and exception type *)
(*val show_result : forall 'a 'e. result 'a 'e -> string*)
definition show_result  :: "('a,'e)result \<Rightarrow> string "  where 
     " show_result = ( \<lambda>x .  
  (case  x of
        Value _ => (''Value ()'')
    | Ex (Failure msg) => (''Failure '') @ msg
    | Ex (Throw _) => (''Throw'')
  ) )"


(*val prerr_results : forall 'a 'e 's. SetType 's => set (result 'a 'e * 's) -> unit*)
definition prerr_results  :: "(('a,'e)result*'s)set \<Rightarrow> unit "  where 
     " prerr_results rs = (
  (let _ = (Set.image ( \<lambda>x .  
  (case  x of (r, _) => (let _ = (prerr_endline (show_result r)) in () ) )) rs) in
  () ))"

end