chapter \<open>Generated by Lem from /tmp/sail/mips/mips_extras.lem.\<close>

theory "Mips_extras" 

imports 
 	 Main
	 "Lem_pervasives" 
	 "Lem_pervasives_extra" 
	 "Sail2_instr_kinds" 
	 "Sail2_values" 
	 "Sail2_prompt_monad" 
	 "Sail2_prompt" 
	 "Sail2_operators" 

begin 

(*open import Pervasives*)
(*open import Pervasives_extra*)
(*open import Sail2_instr_kinds*)
(*open import Sail2_values*)
(*open import Sail2_operators*)
(*open import Sail2_prompt_monad*)
(*open import Sail2_prompt*)

(*val MEMr             : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> monad 'regval 'b 'e*)
(*val MEMr_reserve     : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> monad 'regval 'b 'e*)
(*val MEMr_tag         : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> monad 'regval (bool * 'b) 'e*)
(*val MEMr_tag_reserve : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> monad 'regval (bool * 'b) 'e*)

definition MEMr  :: " 'a Bitvector_class \<Rightarrow> 'b Bitvector_class \<Rightarrow> 'a \<Rightarrow> int \<Rightarrow>('regval,'b,'e)monad "              where 
     " MEMr dict_Sail2_values_Bitvector_a dict_Sail2_values_Bitvector_b addr size1             = ( read_mem 
  dict_Sail2_values_Bitvector_a dict_Sail2_values_Bitvector_b Read_plain addr size1 )"

definition MEMr_reserve  :: " 'a Bitvector_class \<Rightarrow> 'b Bitvector_class \<Rightarrow> 'a \<Rightarrow> int \<Rightarrow>('regval,'b,'e)monad "      where 
     " MEMr_reserve dict_Sail2_values_Bitvector_a dict_Sail2_values_Bitvector_b addr size1     = ( read_mem 
  dict_Sail2_values_Bitvector_a dict_Sail2_values_Bitvector_b Read_reserve addr size1 )"


(*val read_tag_bool : forall 'regval 'a 'e. Bitvector 'a => 'a -> monad 'regval bool 'e*)
definition read_tag_bool  :: " 'a Bitvector_class \<Rightarrow> 'a \<Rightarrow>('regval,(bool),'e)monad "  where 
     " read_tag_bool dict_Sail2_values_Bitvector_a addr = (
  read_tag dict_Sail2_values_Bitvector_a addr \<bind> (\<lambda> t . 
  maybe_fail (''read_tag_bool'') (bool_of_bitU t)))"


(*val write_tag_bool : forall 'regval 'a 'e. Bitvector 'a => 'a -> bool -> monad 'regval unit 'e*)
definition write_tag_bool  :: " 'a Bitvector_class \<Rightarrow> 'a \<Rightarrow> bool \<Rightarrow>('regval,(unit),'e)monad "  where 
     " write_tag_bool dict_Sail2_values_Bitvector_a addr t = ( write_tag 
  dict_Sail2_values_Bitvector_a addr (bitU_of_bool t) \<bind>  
  (\<lambda>x .  (case  x of _ => return ()  )) )"


definition MEMr_tag  :: " 'a Bitvector_class \<Rightarrow> 'b Bitvector_class \<Rightarrow> 'a \<Rightarrow> int \<Rightarrow>('regval,(bool*'b),'e)monad "  where 
     " MEMr_tag dict_Sail2_values_Bitvector_a dict_Sail2_values_Bitvector_b addr size1 = (
  read_mem dict_Sail2_values_Bitvector_a dict_Sail2_values_Bitvector_b Read_plain addr size1 \<bind> (\<lambda> v . 
  read_tag_bool dict_Sail2_values_Bitvector_a addr \<bind> (\<lambda> t . 
  return (t, v))))"


definition MEMr_tag_reserve  :: " 'a Bitvector_class \<Rightarrow> 'b Bitvector_class \<Rightarrow> 'a \<Rightarrow> int \<Rightarrow>('regval,(bool*'b),'e)monad "  where 
     " MEMr_tag_reserve dict_Sail2_values_Bitvector_a dict_Sail2_values_Bitvector_b addr size1 = (
  read_mem dict_Sail2_values_Bitvector_a dict_Sail2_values_Bitvector_b Read_plain addr size1 \<bind> (\<lambda> v . 
  read_tag_bool dict_Sail2_values_Bitvector_a addr \<bind> (\<lambda> t . 
  return (t, v))))"



(*val MEMea                 : forall 'regval 'a 'e. Bitvector 'a => 'a -> integer -> monad 'regval unit 'e*)
(*val MEMea_conditional     : forall 'regval 'a 'e. Bitvector 'a => 'a -> integer -> monad 'regval unit 'e*)
(*val MEMea_tag             : forall 'regval 'a 'e. Bitvector 'a => 'a -> integer -> monad 'regval unit 'e*)
(*val MEMea_tag_conditional : forall 'regval 'a 'e. Bitvector 'a => 'a -> integer -> monad 'regval unit 'e*)

definition MEMea  :: " 'a Bitvector_class \<Rightarrow> 'a \<Rightarrow> int \<Rightarrow>('regval,(unit),'e)monad "                  where 
     " MEMea dict_Sail2_values_Bitvector_a addr size1                 = ( write_mem_ea 
  dict_Sail2_values_Bitvector_a Write_plain addr size1 )"

definition MEMea_conditional  :: " 'a Bitvector_class \<Rightarrow> 'a \<Rightarrow> int \<Rightarrow>('regval,(unit),'e)monad "      where 
     " MEMea_conditional dict_Sail2_values_Bitvector_a addr size1     = ( write_mem_ea 
  dict_Sail2_values_Bitvector_a Write_conditional addr size1 )"


definition MEMea_tag  :: " 'a Bitvector_class \<Rightarrow> 'a \<Rightarrow> int \<Rightarrow>('regval,(unit),'e)monad "              where 
     " MEMea_tag dict_Sail2_values_Bitvector_a addr size1             = ( write_mem_ea 
  dict_Sail2_values_Bitvector_a Write_plain addr size1 )"

definition MEMea_tag_conditional  :: " 'a Bitvector_class \<Rightarrow> 'a \<Rightarrow> int \<Rightarrow>('regval,(unit),'e)monad "  where 
     " MEMea_tag_conditional dict_Sail2_values_Bitvector_a addr size1 = ( write_mem_ea 
  dict_Sail2_values_Bitvector_a Write_conditional addr size1 )"



(*val MEMval                 : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> 'b -> monad 'regval unit 'e*)
(*val MEMval_conditional     : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> 'b -> monad 'regval bool 'e*)
(*val MEMval_tag             : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> bool -> 'b -> monad 'regval unit 'e*)
(*val MEMval_tag_conditional : forall 'regval 'a 'b 'e. Bitvector 'a, Bitvector 'b => 'a -> integer -> bool -> 'b -> monad 'regval bool 'e*)

definition MEMval  :: " 'a Bitvector_class \<Rightarrow> 'b Bitvector_class \<Rightarrow> 'a \<Rightarrow> int \<Rightarrow> 'b \<Rightarrow>('regval,(unit),'e)monad "                       where 
     " MEMval dict_Sail2_values_Bitvector_a dict_Sail2_values_Bitvector_b _ size1 v                      = ( write_mem_val 
  dict_Sail2_values_Bitvector_b v \<bind>  (\<lambda>x .  (case  x of _ => return ()  )) )"

definition MEMval_conditional  :: " 'a Bitvector_class \<Rightarrow> 'b Bitvector_class \<Rightarrow> 'a \<Rightarrow> int \<Rightarrow> 'b \<Rightarrow>('regval,(bool),'e)monad "           where 
     " MEMval_conditional dict_Sail2_values_Bitvector_a dict_Sail2_values_Bitvector_b _ size1 v          = ( write_mem_val 
  dict_Sail2_values_Bitvector_b v \<bind> (\<lambda> b .  return (if b then True else False)))"

definition MEMval_tag  :: " 'a Bitvector_class \<Rightarrow> 'b Bitvector_class \<Rightarrow> 'a \<Rightarrow> int \<Rightarrow> bool \<Rightarrow> 'b \<Rightarrow>('regval,(unit),'e)monad "              where 
     " MEMval_tag dict_Sail2_values_Bitvector_a dict_Sail2_values_Bitvector_b addr size1 t v             = ( write_mem_val 
  dict_Sail2_values_Bitvector_b v \<bind>  (\<lambda>x .  (case  x of
                    _ => write_tag_bool dict_Sail2_values_Bitvector_a addr t
                           \<bind>
                           (\<lambda>x .  (case  x of _ => return ()  ))
                )) )"

definition MEMval_tag_conditional  :: " 'a Bitvector_class \<Rightarrow> 'b Bitvector_class \<Rightarrow> 'a \<Rightarrow> int \<Rightarrow> bool \<Rightarrow> 'b \<Rightarrow>('regval,(bool),'e)monad "  where 
     " MEMval_tag_conditional dict_Sail2_values_Bitvector_a dict_Sail2_values_Bitvector_b addr size1 t v = ( write_mem_val 
  dict_Sail2_values_Bitvector_b v \<bind> (\<lambda> b .  write_tag_bool 
  dict_Sail2_values_Bitvector_a addr t \<bind>  (\<lambda>x .  (case  x of _ => return (if b then True else False) ))))"


(*val MEM_sync  : forall 'regval 'e. unit -> monad 'regval unit 'e*)

definition MEM_sync  :: " unit \<Rightarrow>('regval,(unit),'e)monad "  where 
     " MEM_sync _ = ( barrier Barrier_MIPS_SYNC )"


(* Some wrappers copied from aarch64_extras *)
(* TODO: Harmonise into a common library *)

definition get_slice_int_bl  :: " int \<Rightarrow> int \<Rightarrow> int \<Rightarrow>(bool)list "  where 
     " get_slice_int_bl len n lo = (
  (* TODO: Is this the intended behaviour? *)
  (let hi = ((lo + len) -( 1 :: int)) in
  (let bs = (bools_of_int (hi +( 1 :: int)) n) in
  subrange_list False bs hi lo)))"


(*val get_slice_int : forall 'a. Bitvector 'a => integer -> integer -> integer -> 'a*)
definition get_slice_int0  :: " 'a Bitvector_class \<Rightarrow> int \<Rightarrow> int \<Rightarrow> int \<Rightarrow> 'a "  where 
     " get_slice_int0 dict_Sail2_values_Bitvector_a len n lo = (
  (of_bools_method   dict_Sail2_values_Bitvector_a) (get_slice_int_bl len n lo))"


definition write_ram  :: " 'a Bitvector_class \<Rightarrow> 'b Bitvector_class \<Rightarrow> 'e \<Rightarrow> int \<Rightarrow> 'f \<Rightarrow> 'b \<Rightarrow> 'a \<Rightarrow>('d,(unit),'c)monad "  where 
     " write_ram dict_Sail2_values_Bitvector_a dict_Sail2_values_Bitvector_b _ size1 _ addr data = (
  MEMea dict_Sail2_values_Bitvector_b addr size1 \<then>
  MEMval dict_Sail2_values_Bitvector_b dict_Sail2_values_Bitvector_a addr size1 data )"


definition read_ram  :: " 'a Bitvector_class \<Rightarrow> 'c Bitvector_class \<Rightarrow> 'e \<Rightarrow> int \<Rightarrow> 'f \<Rightarrow> 'a \<Rightarrow>('d,'c,'b)monad "  where 
     " read_ram dict_Sail2_values_Bitvector_a dict_Sail2_values_Bitvector_c _ size1 _ addr = ( MEMr 
  dict_Sail2_values_Bitvector_a dict_Sail2_values_Bitvector_c addr size1 )"


definition string_of_int  :: " 'a Show_class \<Rightarrow> 'a \<Rightarrow> string "  where 
     " string_of_int dict_Show_Show_a = ((show_method   dict_Show_Show_a))"


definition shift_bits_left  :: " 'b Bitvector_class \<Rightarrow> 'd Bitvector_class \<Rightarrow> 'e Bitvector_class \<Rightarrow> 'd \<Rightarrow> 'e \<Rightarrow>('c,'b,'a)monad "  where 
     " shift_bits_left dict_Sail2_values_Bitvector_b dict_Sail2_values_Bitvector_d dict_Sail2_values_Bitvector_e v n = (
  (let r = (Option.bind (
  (unsigned_method   dict_Sail2_values_Bitvector_e) n) (\<lambda> n . (of_bits_method   dict_Sail2_values_Bitvector_b) (shiftl_bv dict_Sail2_values_Bitvector_d v n))) in
  maybe_fail (''shift_bits_left'') r))"

definition shift_bits_right  :: " 'b Bitvector_class \<Rightarrow> 'd Bitvector_class \<Rightarrow> 'e Bitvector_class \<Rightarrow> 'd \<Rightarrow> 'e \<Rightarrow>('c,'b,'a)monad "  where 
     " shift_bits_right dict_Sail2_values_Bitvector_b dict_Sail2_values_Bitvector_d dict_Sail2_values_Bitvector_e v n = (
  (let r = (Option.bind (
  (unsigned_method   dict_Sail2_values_Bitvector_e) n) (\<lambda> n . (of_bits_method   dict_Sail2_values_Bitvector_b) (shiftr_bv dict_Sail2_values_Bitvector_d v n))) in
  maybe_fail (''shift_bits_right'') r))"

definition shift_bits_right_arith  :: " 'b Bitvector_class \<Rightarrow> 'd Bitvector_class \<Rightarrow> 'e Bitvector_class \<Rightarrow> 'd \<Rightarrow> 'e \<Rightarrow>('c,'b,'a)monad "  where 
     " shift_bits_right_arith dict_Sail2_values_Bitvector_b dict_Sail2_values_Bitvector_d dict_Sail2_values_Bitvector_e v n = (
  (let r = (Option.bind (
  (unsigned_method   dict_Sail2_values_Bitvector_e) n) (\<lambda> n . (of_bits_method   dict_Sail2_values_Bitvector_b) (arith_shiftr_bv dict_Sail2_values_Bitvector_d v n))) in
  maybe_fail (''shift_bits_right_arith'') r))"


(* Use constants for undefined values for now *)
definition undefined_string  :: " unit \<Rightarrow>('b,(string),'a)monad "  where 
     " undefined_string _ = ( return (''''))"

definition undefined_unit  :: " unit \<Rightarrow>('b,(unit),'a)monad "  where 
     " undefined_unit _ = ( return ()  )"

definition undefined_int  :: " unit \<Rightarrow>('b,(int),'a)monad "  where 
     " undefined_int _ = ( return (( 0 :: int)::ii))"

(*val undefined_vector : forall 'rv 'a 'e. integer -> 'a -> monad 'rv (list 'a) 'e*)
definition undefined_vector  :: " int \<Rightarrow> 'a \<Rightarrow>('rv,('a list),'e)monad "  where 
     " undefined_vector len u = ( return (repeat [u] len))"

(*val undefined_bitvector : forall 'rv 'a 'e. Bitvector 'a => integer -> monad 'rv 'a 'e*)
definition undefined_bitvector  :: " 'a Bitvector_class \<Rightarrow> int \<Rightarrow>('rv,'a,'e)monad "  where 
     " undefined_bitvector dict_Sail2_values_Bitvector_a len = ( return (
  (of_bools_method   dict_Sail2_values_Bitvector_a) (repeat [False] len)))"

(*val undefined_bits : forall 'rv 'a 'e. Bitvector 'a => integer -> monad 'rv 'a 'e*)
definition undefined_bits  :: " 'a Bitvector_class \<Rightarrow> int \<Rightarrow>('rv,'a,'e)monad "  where 
     " undefined_bits dict_Sail2_values_Bitvector_a = ( 
  undefined_bitvector dict_Sail2_values_Bitvector_a )"

definition undefined_bit  :: " unit \<Rightarrow>('b,(bitU),'a)monad "  where 
     " undefined_bit _ = ( return B0 )"

definition undefined_real  :: " unit \<Rightarrow>('b,(real),'a)monad "  where 
     " undefined_real _ = ( return (realFromFrac(( 0 :: int))(( 1 :: int))))"

definition undefined_range  :: " 'a \<Rightarrow> 'd \<Rightarrow>('c,'a,'b)monad "  where 
     " undefined_range i j = ( return i )"

definition undefined_atom  :: " 'a \<Rightarrow>('c,'a,'b)monad "  where 
     " undefined_atom i = ( return i )"

definition undefined_nat  :: " unit \<Rightarrow>('b,(int),'a)monad "  where 
     " undefined_nat _ = ( return (( 0 :: int)::ii))"


definition skip  :: " unit \<Rightarrow>('b,(unit),'a)monad "  where 
     " skip _ = ( return ()  )"


(*val elf_entry : unit -> integer*)
definition elf_entry  :: " unit \<Rightarrow> int "  where 
     " elf_entry _ = (( 0 :: int))"


definition print_bits  :: " 'a Bitvector_class \<Rightarrow> string \<Rightarrow> 'a \<Rightarrow> unit "  where 
     " print_bits dict_Sail2_values_Bitvector_a msg bs = ( print_endline (msg @ (string_of_bv 
  dict_Sail2_values_Bitvector_a bs)))"

definition prerr_bits  :: " 'a Bitvector_class \<Rightarrow> string \<Rightarrow> 'a \<Rightarrow> unit "  where 
     " prerr_bits dict_Sail2_values_Bitvector_a msg bs = ( prerr_endline (msg @ (string_of_bv 
  dict_Sail2_values_Bitvector_a bs)))"


(*val prerr_string : string -> unit*)
definition prerr_string  :: " string \<Rightarrow> unit "  where 
     " prerr_string _ = ( ()  )"


(*val get_time_ns : unit -> integer*)
definition get_time_ns  :: " unit \<Rightarrow> int "  where 
     " get_time_ns _ = (( 0 :: int))"


(*val cycle_count : unit -> unit*)
definition cycle_count  :: " unit \<Rightarrow> unit "  where 
     " cycle_count _ = ( ()  )"

end