path: root/prover_snapshots/hol4/lib/sail/sail2_state_monadScript.sml

(*Generated by Lem from ../../src/gen_lib/sail2_state_monad.lem.*)
open HolKernel Parse boolLib bossLib;
open lem_pervasives_extraTheory sail2_valuesTheory sail2_instr_kindsTheory;

val _ = numLib.prefer_num();



val _ = new_theory "sail2_state_monad"

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

(* 'a is result type *)

val _ = type_abbrev( "memstate" , ``: (num, memory_byte) fmap``);
val _ = type_abbrev( "tagstate" , ``: (num, bitU) fmap``);
(* type regstate = map string (vector bitU) *)

val _ = Hol_datatype `
(*  'regs *) sequential_state =
  <| regstate : 'regs;
     memstate : memstate;
     tagstate : tagstate |>`;


(*val init_state : forall 'regs. 'regs -> sequential_state 'regs*)
val _ = Define `
 ((init_state:'regs -> 'regs sequential_state) regs=
   (<| regstate := regs;
     memstate := FEMPTY;
     tagstate := FEMPTY |>))`;


val _ = Hol_datatype `
 ex =
    Failure of string
  | Throw of 'e`;


val _ = Hol_datatype `
 result =
    Value of 'a
  | Ex of ( 'e ex)`;


(* State, nondeterminism and exception monad with result value type 'a
   and exception type 'e. *)
val _ = type_abbrev((* ( 'a_regs, 'b_a, 'c_e) *) "monadS" , ``:'a_regs sequential_state -> (('b_a,'c_e)result #'a_regs sequential_state) set``);

(*val returnS : forall 'regs 'a 'e. 'a -> monadS 'regs 'a 'e*)
val _ = Define `
 ((returnS:'a -> 'regs sequential_state ->(('a,'e)result#'regs sequential_state)set) 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*)
val _ = Define `
 ((bindS:('regs sequential_state ->(('a,'e)result#'regs sequential_state)set) ->('a -> 'regs sequential_state ->(('b,'e)result#'regs sequential_state)set) -> 'regs sequential_state ->(('b,'e)result#'regs sequential_state)set) m f (s : 'regs sequential_state)=
   (BIGUNION (IMAGE (\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*)
val _ = Define `
 ((seqS:('regs sequential_state ->(((unit),'e)result#'regs sequential_state)set) ->('regs sequential_state ->(('b,'e)result#'regs sequential_state)set) -> 'regs sequential_state ->(('b,'e)result#'regs sequential_state)set) m n=  (bindS m (\u .  
  (case (u ) of ( (_ : unit) ) => n ))))`;


(*val chooseS : forall 'regs 'a 'e. SetType 'a => list 'a -> monadS 'regs 'a 'e*)
val _ = Define `
 ((chooseS:'a list -> 'regs sequential_state ->(('a,'e)result#'regs sequential_state)set) xs s=  (LIST_TO_SET (MAP (\ x .  (Value x, s)) xs)))`;


(*val readS : forall 'regs 'a 'e. (sequential_state 'regs -> 'a) -> monadS 'regs 'a 'e*)
val _ = Define `
 ((readS:('regs sequential_state -> 'a) -> 'regs sequential_state ->(('a,'e)result#'regs sequential_state)set) f=  (\ s .  returnS (f s) s))`;


(*val updateS : forall 'regs 'e. (sequential_state 'regs -> sequential_state 'regs) -> monadS 'regs unit 'e*)
val _ = Define `
 ((updateS:('regs sequential_state -> 'regs sequential_state) -> 'regs sequential_state ->(((unit),'e)result#'regs sequential_state)set) f=  (\ s .  returnS ()  (f s)))`;


(*val failS : forall 'regs 'a 'e. string -> monadS 'regs 'a 'e*)
val _ = Define `
 ((failS:string -> 'regs sequential_state ->(('a,'e)result#'regs sequential_state)set) msg s=  ({(Ex (Failure msg), s)}))`;


(*val choose_boolS : forall 'regval 'regs 'a 'e. unit -> monadS 'regs bool 'e*)
val _ = Define `
 ((choose_boolS:unit -> 'regs sequential_state ->(((bool),'e)result#'regs sequential_state)set) () =  (chooseS [F; T]))`;

val _ = Define `
 ((undefined_boolS:unit ->('c,(bool),'a)monadS)=  choose_boolS)`;


(*val exitS : forall 'regs 'e 'a. unit -> monadS 'regs 'a 'e*)
val _ = Define `
 ((exitS:unit -> 'regs sequential_state ->(('a,'e)result#'regs sequential_state)set) () =  (failS "exit"))`;


(*val throwS : forall 'regs 'a 'e. 'e -> monadS 'regs 'a 'e*)
val _ = Define `
 ((throwS:'e -> 'regs sequential_state ->(('a,'e)result#'regs sequential_state)set) 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*)
val _ = Define `
 ((try_catchS:('regs sequential_state ->(('a,'e1)result#'regs sequential_state)set) ->('e1 -> 'regs sequential_state ->(('a,'e2)result#'regs sequential_state)set) -> 'regs sequential_state ->(('a,'e2)result#'regs sequential_state)set) m h s=
   (BIGUNION (IMAGE (\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*)
val _ = Define `
 ((assert_expS:bool -> string -> 'regs sequential_state ->(((unit),'e)result#'regs sequential_state)set) exp msg=  (if exp 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". *)
val _ = type_abbrev((* ( 'a_regs, 'b_a, 'c_r, 'd_e) *) "monadRS" , ``:('a_regs,'b_a, (('c_r,'d_e)sum)) monadS``);

(*val early_returnS : forall 'regs 'a 'r 'e. 'r -> monadRS 'regs 'a 'r 'e*)
val _ = Define `
 ((early_returnS:'r -> 'regs sequential_state ->(('a,(('r,'e)sum))result#'regs sequential_state)set) r=  (throwS (INL r)))`;


(*val catch_early_returnS : forall 'regs 'a 'e. monadRS 'regs 'a 'a 'e -> monadS 'regs 'a 'e*)
val _ = Define `
 ((catch_early_returnS:('regs sequential_state ->(('a,(('a,'e)sum))result#'regs sequential_state)set) -> 'regs sequential_state ->(('a,'e)result#'regs sequential_state)set) m=
   (try_catchS m
    (\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*)
val _ = Define `
 ((liftRS:('regs sequential_state ->(('a,'e)result#'regs sequential_state)set) -> 'regs sequential_state ->(('a,(('r,'e)sum))result#'regs sequential_state)set) m=  (try_catchS m (\ 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*)
val _ = Define `
 ((try_catchRS:('regs sequential_state ->(('a,(('r,'e1)sum))result#'regs sequential_state)set) ->('e1 -> 'regs sequential_state ->(('a,(('r,'e2)sum))result#'regs sequential_state)set) -> 'regs sequential_state ->(('a,(('r,'e2)sum))result#'regs sequential_state)set) m h=
   (try_catchS m
    (\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*)
val _ = Define `
 ((maybe_failS:string -> 'a option -> 'regs sequential_state ->(('a,'e)result#'regs sequential_state)set) msg= 
  (\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*)
val _ = Define `
 ((read_tagS:'a Bitvector_class -> 'a ->('regs,(bitU),'e)monadS)dict_Sail2_values_Bitvector_a addr=  (bindS
  (maybe_failS "nat_of_bv" (nat_of_bv 
  dict_Sail2_values_Bitvector_a addr)) (\ addr . 
  readS (\ s .  option_CASE (FLOOKUP s.tagstate addr) B0 I))))`;


(* Read bytes from memory and return in little endian order *)
(*val get_mem_bytes : forall 'regs. nat -> nat -> sequential_state 'regs -> maybe (list memory_byte * bitU)*)
val _ = Define `
 ((get_mem_bytes:num -> num -> 'regs sequential_state ->(((bitU)list)list#bitU)option) addr sz s=
   (let addrs = (GENLIST (\ n .  addr + n) sz) in  
  let read_byte = (\ s addr .  FLOOKUP s.memstate addr) in
  let read_tag = (\ s addr .  option_CASE (FLOOKUP s.tagstate addr) B0 I) in
  OPTION_MAP
    (\ mem_val .  (mem_val, FOLDL and_bit B1 (MAP (read_tag s) addrs)))
    (just_list (MAP (read_byte s) addrs))))`;


(*val read_memt_bytesS : forall 'regs 'e. read_kind -> nat -> nat -> monadS 'regs (list memory_byte * bitU) 'e*)
val _ = Define `
 ((read_memt_bytesS:read_kind -> num -> num -> 'regs sequential_state ->((((memory_byte)list#bitU),'e)result#'regs sequential_state)set) _ addr sz=  (bindS
  (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*)
val _ = Define `
 ((read_mem_bytesS:read_kind -> num -> num -> 'regs sequential_state ->((((memory_byte)list),'e)result#'regs sequential_state)set) rk addr sz=  (bindS
  (read_memt_bytesS rk addr sz) (\p .  
  (case (p ) of ( (bytes, _) ) => returnS bytes ))))`;


(*val read_memtS : forall 'regs 'e 'a 'b. Bitvector 'a, Bitvector 'b => read_kind -> 'a -> integer -> monadS 'regs ('b * bitU) 'e*)
val _ = Define `
 ((read_memtS:'a Bitvector_class -> 'b Bitvector_class -> read_kind -> 'a -> int ->('regs,('b#bitU),'e)monadS)dict_Sail2_values_Bitvector_a dict_Sail2_values_Bitvector_b rk a sz=  (bindS
  (maybe_failS "nat_of_bv" (nat_of_bv 
  dict_Sail2_values_Bitvector_a a)) (\ a .  bindS
  (read_memt_bytesS rk a (nat_of_int sz)) (\ (bytes, tag) .  bindS
  (maybe_failS "bits_of_mem_bytes" (
  dict_Sail2_values_Bitvector_b.of_bits_method (bits_of_mem_bytes bytes))) (\ mem_val . 
  returnS (mem_val, tag))))))`;


(*val read_memS : forall 'regs 'e 'a 'b 'addrsize. Bitvector 'a, Bitvector 'b => read_kind -> 'addrsize -> 'a -> integer -> monadS 'regs 'b 'e*)
val _ = Define `
 ((read_memS:'a Bitvector_class -> 'b Bitvector_class -> read_kind -> 'addrsize -> 'a -> int ->('regs,'b,'e)monadS)dict_Sail2_values_Bitvector_a dict_Sail2_values_Bitvector_b rk addr_size a sz=  (bindS
  (read_memtS dict_Sail2_values_Bitvector_a dict_Sail2_values_Bitvector_b rk a sz) (\p .  (case (p ) of ( (bytes, _) ) => returnS bytes ))))`;


(*val excl_resultS : forall 'regs 'e. unit -> monadS 'regs bool 'e*)
val _ = Define `
 ((excl_resultS:unit ->('regs,(bool),'e)monadS)=
  (* 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 put_mem_bytes : forall 'regs. nat -> nat -> list memory_byte -> bitU -> sequential_state 'regs -> sequential_state 'regs*)
val _ = Define `
 ((put_mem_bytes:num -> num ->((bitU)list)list -> bitU -> 'regs sequential_state -> 'regs sequential_state) addr sz v tag s=
   (let addrs = (GENLIST (\ n .  addr + n) sz) in
  let a_v = (lem_list$list_combine addrs v) in  
  let write_byte = (\mem p .  (case (mem ,p ) of
                                  ( mem , (addr, v) ) => mem  |+ ( addr ,  
                                                        v )
                              )) in
  let write_tag = (\ mem addr .  mem  |+ ( addr ,  tag )) in
  ( s with<| memstate := (FOLDL write_byte s.memstate a_v);
  tagstate := (FOLDL write_tag s.tagstate addrs) |>)))`;


(*val write_memt_bytesS : forall 'regs 'e. write_kind -> nat -> nat -> list memory_byte -> bitU -> monadS 'regs bool 'e*)
val _ = Define `
 ((write_memt_bytesS:write_kind -> num -> num ->(memory_byte)list -> bitU -> 'regs sequential_state ->(((bool),'e)result#'regs sequential_state)set) _ addr sz v t=  (seqS
  (updateS (put_mem_bytes addr sz v t))
  (returnS T)))`;


(*val write_mem_bytesS : forall 'regs 'e. write_kind -> nat -> nat -> list memory_byte -> monadS 'regs bool 'e*)
val _ = Define `
 ((write_mem_bytesS:write_kind -> num -> num ->(memory_byte)list -> 'regs sequential_state ->(((bool),'e)result#'regs sequential_state)set) 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*)
val _ = Define `
 ((write_memtS:'a Bitvector_class -> 'b Bitvector_class -> write_kind -> 'a -> int -> 'b -> bitU ->('regs,(bool),'e)monadS)dict_Sail2_values_Bitvector_a dict_Sail2_values_Bitvector_b wk addr sz v t=
   ((case (nat_of_bv dict_Sail2_values_Bitvector_a addr, mem_bytes_of_bits 
  dict_Sail2_values_Bitvector_b v) of
      (SOME addr, SOME v) => write_memt_bytesS wk addr (nat_of_int sz) v t
    | _ => failS "write_mem"
  )))`;


(*val write_memS : forall 'regs 'e 'a 'b 'addrsize. Bitvector 'a, Bitvector 'b =>
  write_kind -> 'addrsize -> 'a -> integer -> 'b -> monadS 'regs bool 'e*)
val _ = Define `
 ((write_memS:'a Bitvector_class -> 'b Bitvector_class -> write_kind -> 'addrsize -> 'a -> int -> 'b ->('regs,(bool),'e)monadS)dict_Sail2_values_Bitvector_a dict_Sail2_values_Bitvector_b wk addr_size addr sz v=  (write_memtS 
  dict_Sail2_values_Bitvector_a dict_Sail2_values_Bitvector_b wk addr sz v B0))`;


(*val read_regS : forall 'regs 'rv 'a 'e. register_ref 'regs 'rv 'a -> monadS 'regs 'a 'e*)
val _ = Define `
 ((read_regS:('regs,'rv,'a)register_ref -> 'regs sequential_state ->(('a,'e)result#'regs sequential_state)set) reg=  (readS (\ s .  reg.read_from s.regstate)))`;


(* 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*)
val _ = Define `
 ((read_regvalS:(string -> 'regs -> 'rv option)#(string -> 'rv -> 'regs -> 'regs option) -> string -> 'regs sequential_state ->(('rv,'e)result#'regs sequential_state)set) (read, _) reg=  (bindS
  (readS (\ s .  read reg s.regstate)) (\x .  
  (case x of
        SOME v => returnS v
    | NONE => failS ( STRCAT "read_regvalS " reg)
  ))))`;


(*val write_regvalS : forall 'regs 'rv 'e.
  register_accessors 'regs 'rv -> string -> 'rv -> monadS 'regs unit 'e*)
val _ = Define `
 ((write_regvalS:(string -> 'regs -> 'rv option)#(string -> 'rv -> 'regs -> 'regs option) -> string -> 'rv -> 'regs sequential_state ->(((unit),'e)result#'regs sequential_state)set) (_, write) reg v=  (bindS
  (readS (\ s .  write reg v s.regstate)) (\x .  
  (case x of
        SOME rs' => updateS (\ s .  ( s with<| regstate := rs' |>))
    | NONE => failS ( STRCAT "write_regvalS " reg)
  ))))`;


(*val write_regS : forall 'regs 'rv 'a 'e. register_ref 'regs 'rv 'a -> 'a -> monadS 'regs unit 'e*)
val _ = Define `
 ((write_regS:('regs,'rv,'a)register_ref -> 'a -> 'regs sequential_state ->(((unit),'e)result#'regs sequential_state)set) reg v=
   (updateS (\ s .  ( s with<| regstate := (reg.write_to v s.regstate) |>))))`;


(* 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*)
val _ = Define `
 ((show_result:('a,'e)result -> string)= 
  (\x .  (case x of
               Value _ => "Value ()"
           | Ex (Failure msg) => STRCAT "Failure " msg
           | Ex (Throw _) => "Throw"
         )))`;


(*val prerr_results : forall 'a 'e 's. SetType 's => set (result 'a 'e * 's) -> unit*)
val _ = Define `
 ((prerr_results:(('a,'e)result#'s)set -> unit) rs=
   (let _ = (IMAGE (\p .  
  (case (p ) of ( (r, _) ) => let _ = (prerr_endline (show_result r)) in ()  )) rs) in
  () ))`;

val _ = export_theory()