Session SPARCv8

Theory WordDecl

(*  Title:     State.thy
    Author:    David Sanán, Trinity College Dublin, 2012
*)

section "Word Declarations"

theory WordDecl
imports Main "HOL-Library.Word"
begin

text ‹
This theory provides len0› and len› instantiations 
for the most common used word sizes in the model (1,2,4,5,6,8,12,16,18,20,24,32,36).
The len0› class defines lengths that range from 0 upwards,
whilst the len› class caters for non-zero lengths.
Bit-operators like <<›, >>›, and›, or or› 
require a'::len› word instances,
while other word operations such @{term "ucast"} 
(gets an integer from a word) 
can be defined for len0› words. 

For each length N›, we:
   declare a type word_lengthN›;
   make it an instance of both length classes;
   and introduce a short type synonym wordN›, and a suitable translation.

In essence, this theory is just a lot of boilerplate.
\newpage
›

section "Words of length 1"

typedecl word_length1
instantiation word_length1 :: len0
begin
definition
  len1 [simp]: "len_of (x::word_length1 itself)  1"
instance .. 
end
instantiation word_length1 :: len
begin
instance by intro_classes simp
end
type_synonym word1 = "word_length1 word"
translations (type) "word1" <= (type) "word_length1 word"

subsection "Words of length 1's constants"

definition ONE::"word1"
where
"ONE  1"

definition ZERO::"word1"
where
"ZERO  0"

section "Words of length 2"

typedecl word_length2
instantiation word_length2 :: len0
begin
definition
  len2 [simp]: "len_of (x::word_length2 itself)  2"
instance .. 
end
instantiation word_length2 :: len
begin
instance by intro_classes simp
end
type_synonym word2 = "word_length2 word"
translations (type) "word2" <= (type) "word_length2 word"

section "Words of length 3"

typedecl word_length3
instantiation word_length3 :: len0
begin
definition
  len3 [simp]: "len_of (x::word_length3 itself)  3"
instance .. 
end
instantiation word_length3 :: len
begin
instance by intro_classes simp
end
type_synonym word3 = "word_length3 word"
translations (type) "word3" <= (type) "word_length3 word"

section "Words of length 4"

typedecl word_length4
instantiation word_length4 :: len0
begin
definition
  len4 [simp]: "len_of (x::word_length4 itself)  4"
instance .. 
end
instantiation word_length4 :: len
begin
instance by intro_classes simp
end
type_synonym word4 = "word_length4 word"
translations (type) "word4" <= (type) "word_length4 word"

section "Words of length 5"

typedecl word_length5
instantiation word_length5 :: len0
begin
definition
  len5 [simp]: "len_of (x::word_length5 itself)  5"
instance .. 
end
instantiation word_length5 :: len
begin
instance by intro_classes simp
end
type_synonym word5 = "word_length5 word"
translations (type) "word5" <= (type) "word_length5 word"

section "Words of length 6"

typedecl word_length6
instantiation word_length6 :: len0
begin
definition
  len6 [simp]: "len_of (x::word_length6 itself)  6"
instance .. 
end
instantiation word_length6 :: len
begin
instance by intro_classes simp
end
type_synonym word6 = "word_length6 word"
translations (type) "word6" <= (type) "word_length6 word"

section "Words of length 6"

typedecl word_length7
instantiation word_length7 :: len0
begin
definition
  len7 [simp]: "len_of (x::word_length7 itself)  7"
instance .. 
end
instantiation word_length7 :: len
begin
instance by intro_classes simp
end
type_synonym word7 = "word_length7 word"
translations (type) "word7" <= (type) "word_length7 word"

section "Words of length 8"

typedecl word_length8
instantiation word_length8 :: len0
begin
definition
  len8 [simp]: "len_of (x::word_length8 itself)  8"
instance .. 
end
instantiation word_length8 :: len
begin
instance by intro_classes simp
end
type_synonym word8 = "word_length8 word"
translations (type) "word8" <= (type) "word_length8 word"

section "Words of length 9"

typedecl word_length9
instantiation word_length9 :: len0
begin
definition
  len9 [simp]: "len_of (x::word_length9 itself)  9"
instance .. 
end
instantiation word_length9 :: len
begin
instance by intro_classes simp
end
type_synonym word9 = "word_length9 word"
translations (type) "word9" <= (type) "word_length9 word"

section "Words of length 10"

typedecl word_length10
instantiation word_length10 :: len0
begin
definition
  len10 [simp]: "len_of (x::word_length10 itself)  10"
instance .. 
end
instantiation word_length10 :: len
begin
instance by intro_classes simp
end
type_synonym word10 = "word_length10 word"
translations (type) "word10" <= (type) "word_length10 word"

section "Words of length 12"

typedecl word_length12
instantiation word_length12 :: len0
begin
definition
  len12 [simp]: "len_of (x::word_length12 itself)  12"
instance .. 
end
instantiation word_length12 :: len
begin
instance by intro_classes simp
end
type_synonym word12 = "word_length12 word"
translations (type) "word12" <= (type) "word_length12 word"

section "Words of length 13"

typedecl word_length13
instantiation word_length13 :: len0
begin
definition
  len13 [simp]: "len_of (x::word_length13 itself)  13"
instance .. 
end
instantiation word_length13 :: len
begin
instance by intro_classes simp
end
type_synonym word13 = "word_length13 word"
translations (type) "word13" <= (type) "word_length13 word"

section "Words of length 16"

typedecl word_length16
instantiation word_length16 :: len0
begin
definition
  len16 [simp]: "len_of (x::word_length16 itself)  16"
instance .. 
end
instantiation word_length16 :: len
begin
instance by intro_classes simp
end
type_synonym word16 = "word_length16 word"
translations (type) "word16" <= (type) "word_length16 word"

section "Words of length 18"

typedecl word_length18
instantiation word_length18 :: len0
begin
definition
  len18 [simp]: "len_of (x::word_length18 itself)  18"
instance .. 
end
instantiation word_length18 :: len
begin
instance by intro_classes simp
end
type_synonym word18 = "word_length18 word"
translations (type) "word18" <= (type) "word_length18 word"

section "Words of length 20"

typedecl word_length20
instantiation word_length20 :: len0
begin
definition
  len20 [simp]: "len_of (x::word_length20 itself)  20"
instance .. 
end
instantiation word_length20 :: len
begin
instance by intro_classes simp
end
type_synonym word20 = "word_length20 word"
translations (type) "word20" <= (type) "word_length20 word"

section "Words of length 22"

typedecl word_length22
instantiation word_length22 :: len0
begin
definition
  len22 [simp]: "len_of (x::word_length22 itself)  22"
instance .. 
end
instantiation word_length22 :: len
begin
instance by intro_classes simp
end
type_synonym word22 = "word_length22 word"
translations (type) "word22" <= (type) "word_length22 word"

section "Words of length 24"

typedecl word_length24
instantiation word_length24 :: len0
begin
definition
  len24 [simp]: "len_of (x::word_length24 itself)  24"
instance .. 
end
instantiation word_length24 :: len
begin
instance by intro_classes simp
end
type_synonym word24 = "word_length24 word"
translations (type) "word24" <= (type) "word_length24 word"

section "Words of length 30"

typedecl word_length30
instantiation word_length30 :: len0
begin
definition
  len30 [simp]: "len_of (x::word_length30 itself)  30"
instance .. 
end
instantiation word_length30 :: len
begin
instance by intro_classes simp
end
type_synonym word30 = "word_length30 word"
translations (type) "word30" <= (type) "word_length30 word"

section "Words of length 30"

typedecl word_length31
instantiation word_length31 :: len0
begin
definition
  len31 [simp]: "len_of (x::word_length31 itself)  31"
instance .. 
end
instantiation word_length31 :: len
begin
instance by intro_classes simp
end
type_synonym word31 = "word_length31 word"
translations (type) "word31" <= (type) "word_length31 word"

section "Words of length 32"

typedecl word_length32
instantiation word_length32 :: len0
begin
definition
  len32 [simp]: "len_of (x::word_length32 itself)  32"
instance .. 
end
instantiation word_length32 :: len
begin                            
instance by intro_classes simp
end
type_synonym word32 = "word_length32 word"
translations (type) "word32" <= (type) "word_length32 word"

section "Words of length 33"

typedecl word_length33
instantiation word_length33 :: len0
begin
definition
  len33 [simp]: "len_of (x::word_length33 itself)  33"
instance .. 
end
instantiation word_length33 :: len
begin                            
instance by intro_classes simp
end
type_synonym word33 = "word_length33 word"
translations (type) "word33" <= (type) "word_length33 word"

section "Words of length 36"

typedecl word_length36
instantiation word_length36 :: len0
begin
definition
  len36 [simp]: "len_of (x::word_length36 itself)  36"
instance ..
end
instantiation word_length36 :: len
begin
  instance by intro_classes simp
end
type_synonym word36 = "word_length36 word"
translations (type) "word36" <= (type) "word_length36 word"

section "Words of length 64"

typedecl word_length64
instantiation word_length64 :: len0
begin
definition
  len64 [simp]: "len_of (x::word_length64 itself)  64"
instance ..
end
instantiation word_length64 :: len
begin
  instance by intro_classes simp
end
type_synonym word64 = "word_length64 word"
translations (type) "word64" <= (type) "word_length64 word"

end



Theory Sparc_Types

(*
 * Copyright 2016, NTU
 *
 * This software may be distributed and modified according to the terms of
 * the BSD 2-Clause license. Note that NO WARRANTY is provided.
 * See "LICENSE_BSD2.txt" for details.
 *
 * Author: Zhe Hou, David Sanan. 
 *)

section ‹SPARC V8 architecture CPU model›
theory Sparc_Types    
imports Main "../lib/WordDecl" "Word_Lib.Traditional_Infix_Syntax"
begin

text ‹The following type definitions are taken from David Sanan's 
definitions for SPARC machines.›

type_synonym machine_word = word32
type_synonym byte = word8
type_synonym phys_address = word36

type_synonym virtua_address = word32
type_synonym page_address = word24
type_synonym offset = word12

type_synonym table_entry = word8

definition page_size :: "word32" where "page_size  4096"

type_synonym virtua_page_address = word20
type_synonym context_type = word8

type_synonym word_length_t1 = word_length8
type_synonym word_length_t2 = word_length6
type_synonym word_length_t3 = word_length6
type_synonym word_length_offset = word_length12
type_synonym word_length_page = word_length24
type_synonym word_length_phys_address = word_length36
type_synonym word_length_virtua_address = word_length32
type_synonym word_length_entry_type = word_length2
type_synonym word_length_machine_word = word_length32

definition length_machine_word :: "nat" 
 where "length_machine_word  LENGTH(word_length_machine_word)"

text_raw ‹\newpage›

section ‹CPU Register Definitions›

text‹
 The definitions below come from the SPARC Architecture Manual, Version 8.
 The LEON3 processor has been certified SPARC V8 conformant (2005).
›

definition leon3khz ::"word32"
where
"leon3khz  33000"

text ‹The following type definitions for MMU is taken from 
David Sanan's definitions for MMU.›

text‹
  The definitions below come from the UT699 LEON 3FT/SPARC V8 Microprocessor Functional Manual, 
   Aeroflex, June 20, 2012, p35.
›
datatype MMU_register
 = CR    ― ‹Control Register›
 | CTP   ― ‹ConText Pointer register›
 | CNR   ― ‹Context Register›
 | FTSR   ― ‹Fault Status Register›
 | FAR   ― ‹Fault Address Register›

lemma MMU_register_induct: 
  "P CR  P CTP  P CNR  P FTSR  P FAR 
    P x"
  by (cases x) auto

lemma UNIV_MMU_register [no_atp]: "UNIV = {CR, CTP, CNR, FTSR, FAR}"
   apply (safe)
   apply (case_tac x)
   apply (auto intro:MMU_register_induct)
  done


instantiation MMU_register :: enum begin

definition "enum_MMU_register = [ CR, CTP, CNR, FTSR, FAR ]"

definition
  "enum_all_MMU_register P  P CR  P CTP  P CNR  P FTSR  P FAR "
definition
  "enum_ex_MMU_register P  P CR  P CTP  P CNR  P FTSR  P FAR"

 instance proof
  qed (simp_all only: enum_MMU_register_def enum_all_MMU_register_def 
                      enum_ex_MMU_register_def UNIV_MMU_register, simp_all)
end
type_synonym MMU_context = "MMU_register  machine_word"

text PTE_flags› is the last 8 bits of a PTE. See page 242 of SPARCv8 manual.
 C - bit 7
 M - bit 6,
 R - bit 5
 ACC - bit 4~2
 ET - bit 1~0.›

type_synonym PTE_flags = word8

text @{term CPU_register} datatype is an enumeration with the CPU registers defined in the SPARC V8 
  architecture.
›
datatype CPU_register = 
   PSR   ― ‹Processor State Register›
 | WIM   ― ‹Window Invalid Mask›
 | TBR   ― ‹Trap Base Register›
 | Y     ― ‹Multiply/Divide Register›
 | PC    ― ‹Program Counter›
 | nPC   ― ‹next Program Counter›
 | DTQ   ― ‹Deferred-Trap Queue›
 | FSR   ― ‹Floating-Point State Register›
 | FQ    ― ‹Floating-Point Deferred-Trap Queue›
 | CSR   ― ‹Coprocessor State Register›
 | CQ    ― ‹Coprocessor Deferred-Trap Queue›
 (*| CCR   --   "Cache Control Register"*)
 | ASR "word5"  ― ‹Ancillary State Register›

text ‹The following two functions are dummies since we will not use 
        ASRs. Future formalisation may add more details to this.›

definition privileged_ASR :: "word5  bool"
where
"privileged_ASR r  False
"

definition illegal_instruction_ASR :: "word5  bool"
where
"illegal_instruction_ASR r  False
"

definition get_tt :: "word32  word8"
where
"get_tt tbr 
  ucast (((AND) tbr 0b00000000000000000000111111110000) >> 4)
"

text ‹Write the tt field of the TBR register. 
        Return the new value of TBR.›
definition write_tt :: "word8  word32  word32"
where
"write_tt new_tt_val tbr_val 
  let tmp = (AND) tbr_val 0b111111111111111111111000000001111 in
      (OR) tmp (((ucast new_tt_val)::word32) << 4)
"

text ‹Get the nth bit of WIM. This equals ((AND) WIM $2^n$). 
        N.B. the first bit of WIM is the 0th bit.›
definition get_WIM_bit :: "nat  word32  word1"
where
"get_WIM_bit n wim 
  let mask = ((ucast (0b1::word1))::word32) << n in
  ucast (((AND) mask wim) >> n)
"

definition get_CWP :: "word32  word5"
where
"get_CWP psr  
  ucast ((AND) psr 0b00000000000000000000000000011111) 
"

definition get_ET :: "word32  word1"
where
"get_ET psr  
  ucast (((AND) psr 0b00000000000000000000000000100000) >> 5) 
"

definition get_PIL :: "word32  word4"
where
"get_PIL psr  
  ucast (((AND) psr 0b00000000000000000000111100000000) >> 8) 
"

definition get_PS :: "word32  word1"
where
"get_PS psr  
  ucast (((AND) psr 0b00000000000000000000000001000000) >> 6) 
"

definition get_S :: "word32  word1"
where
"get_S psr  
  ⌦‹ucast (((AND) psr 0b00000000000000000000000010000000) >> 7)›
  if ((AND) psr (0b00000000000000000000000010000000::word32)) = 0 then 0
  else 1
"

definition get_icc_N :: "word32  word1"
where
"get_icc_N psr 
  ucast (((AND) psr 0b00000000100000000000000000000000) >> 23)
"

definition get_icc_Z :: "word32  word1"
where
"get_icc_Z psr 
  ucast (((AND) psr 0b00000000010000000000000000000000) >> 22)
"

definition get_icc_V :: "word32  word1"
where
"get_icc_V psr 
  ucast (((AND) psr 0b00000000001000000000000000000000) >> 21)
"

definition get_icc_C :: "word32  word1"
where
"get_icc_C psr 
  ucast (((AND) psr 0b00000000000100000000000000000000) >> 20)
"

definition update_S :: "word1  word32  word32"
where
"update_S s_val psr_val 
  let tmp0 = (AND) psr_val 0b11111111111111111111111101111111 in
  (OR) tmp0 (((ucast s_val)::word32) << 7)
"

text ‹Update the CWP field of PSR. 
        Return the new value of PSR.›
definition update_CWP :: "word5  word32  word32"
where
"update_CWP cwp_val psr_val 
  let tmp0 = (AND) psr_val (0b11111111111111111111111111100000::word32);
      s_val = ((ucast (get_S psr_val))::word1)
  in
  if s_val = 0 then  
    (AND) ((OR) tmp0 ((ucast cwp_val)::word32)) (0b11111111111111111111111101111111::word32)
  else
    (OR) ((OR) tmp0 ((ucast cwp_val)::word32)) (0b00000000000000000000000010000000::word32)
"

text ‹Update the the ET, CWP, and S fields of PSR. 
        Return the new value of PSR.›
definition update_PSR_rett :: "word5  word1  word1  word32  word32"
where
"update_PSR_rett cwp_val et_val s_val psr_val 
  let tmp0 = (AND) psr_val 0b11111111111111111111111101000000;
      tmp1 = (OR) tmp0 ((ucast cwp_val)::word32);
      tmp2 = (OR) tmp1 (((ucast et_val)::word32) << 5); 
      tmp3 = (OR) tmp2 (((ucast s_val)::word32) << 7)
  in  
  tmp3
"

definition update_PSR_exe_trap :: "word5  word1  word1  word32  word32"
where
"update_PSR_exe_trap cwp_val et_val ps_val psr_val 
  let tmp0 = (AND) psr_val 0b11111111111111111111111110000000;
      tmp1 = (OR) tmp0 ((ucast cwp_val)::word32);
      tmp2 = (OR) tmp1 (((ucast et_val)::word32) << 5); 
      tmp3 = (OR) tmp2 (((ucast ps_val)::word32) << 6)
  in  
  tmp3
"

text ‹Update the N, Z, V, C fields of PSR. 
        Return the new value of PSR.›
definition update_PSR_icc :: "word1  word1  word1  word1  word32  word32"
where
"update_PSR_icc n_val z_val v_val c_val psr_val 
  let
      n_val_32 = if n_val = 0 then 0 
                 else       (0b00000000100000000000000000000000::word32); 
      z_val_32 = if z_val = 0 then 0 
                 else       (0b00000000010000000000000000000000::word32); 
      v_val_32 = if v_val = 0 then 0 
                 else       (0b00000000001000000000000000000000::word32);
      c_val_32 = if c_val = 0 then 0 
                 else       (0b00000000000100000000000000000000::word32);
      tmp0 = (AND) psr_val (0b11111111000011111111111111111111::word32);
      tmp1 = (OR) tmp0 n_val_32;
      tmp2 = (OR) tmp1 z_val_32;
      tmp3 = (OR) tmp2 v_val_32;
      tmp4 = (OR) tmp3 c_val_32
  in
  tmp4
"

text ‹Update the ET, PIL fields of PSR. 
        Return the new value of PSR.›
definition update_PSR_et_pil :: "word1  word4  word32  word32"
where
"update_PSR_et_pil et pil psr_val 
  let tmp0 = (AND) psr_val 0b111111111111111111111000011011111;
      tmp1 = (OR) tmp0 (((ucast et)::word32) << 5);
      tmp2 = (OR) tmp1 (((ucast pil)::word32) << 8)
  in
  tmp2
"

text ‹
   SPARC V8 architecture is organized in windows of 32 user registers.
   The data stored in a register is defined as a 32 bits word @{term reg_type}:
›
type_synonym reg_type = "word32"

text ‹
  The access to the value of a CPU register of type @{term CPU_register} is
  defined by a total function @{term cpu_context}

type_synonym cpu_context = "CPU_register  reg_type"

text ‹
  User registers are defined with the type @{term user_reg} represented by a 5 bits word.
›

type_synonym user_reg_type = "word5"

definition PSR_S ::"reg_type"
where "PSR_S  6"
text ‹
  Each window context is defined by a total function @{term window_context} from @{term user_register} 
  to @{term reg_type} (32 bits word storing the actual value of the register).
›

type_synonym window_context = "user_reg_type  reg_type"
text ‹
  The number of windows is implementation dependent. 
  The LEON architecture is composed of 16 different windows (a 4 bits word).
›

definition NWINDOWS :: "int"
where "NWINDOWS  8"

text ‹Maximum number of windows is 32 in SPARCv8.›
type_synonym ('a) window_size = "'a word"

text ‹
Finally the user context is defined by another total function @{term user_context} from 
@{term window_size} to @{term window_context}. That is, the user context is a function taking as
argument a register set window and a register within that window, and it returns the value stored
in that user register.
›
type_synonym ('a) user_context = "('a) window_size  window_context"

datatype sys_reg = 
         CCR    ― ‹Cache control register›
        |ICCR   ― ‹Instruction cache configuration register›
        |DCCR   ― ‹Data cache configuration register›

type_synonym sys_context = "sys_reg  reg_type"

text‹
The memory model is defined by a total function from 32 bits words to 8 bits words
›
type_synonym asi_type = "word8"

text ‹
 The memory is defined as a function from page address to page, which is also defined
  as a function from physical address to @{term "machine_word"}

type_synonym mem_val_type = "word8"
type_synonym mem_context = "asi_type  phys_address  mem_val_type option"

type_synonym cache_tag = "word20"
type_synonym cache_line_size = "word12"
type_synonym cache_type = "(cache_tag × cache_line_size)"
type_synonym cache_context = "cache_type  mem_val_type option"

text ‹The delayed-write pool generated from write state register instructions.›
type_synonym delayed_write_pool = "(int × reg_type × CPU_register) list"

definition DELAYNUM :: "int"
where "DELAYNUM  0"

text ‹Convert a set to a list.›
definition list_of_set :: "'a set  'a list"
  where "list_of_set s = (SOME l. set l = s)"

lemma set_list_of_set: "finite s  set (list_of_set s) = s"
unfolding list_of_set_def 
by (metis (mono_tags) finite_list some_eq_ex)

type_synonym ANNUL = "bool"
type_synonym RESET_TRAP = "bool"
type_synonym EXECUTE_MODE = "bool"
type_synonym RESET_MODE = "bool"
type_synonym ERROR_MODE = "bool"
type_synonym TICC_TRAP_TYPE = "word7"
type_synonym INTERRUPT_LEVEL = "word3"
type_synonym STORE_BARRIER_PENDING = "bool"

text ‹The processor asserts this signal to ensure that the
memory system will not process another SWAP or
LDSTUB operation to the same memory byte.›
type_synonym pb_block_ldst_byte = "virtua_address  bool"

text‹The processor asserts this signal to ensure that the
memory system will not process another SWAP or
LDSTUB operation to the same memory word.›
type_synonym pb_block_ldst_word = "virtua_address  bool"

record sparc_state_var =
annul:: ANNUL
resett:: RESET_TRAP
exe:: EXECUTE_MODE
reset:: RESET_MODE
err:: ERROR_MODE
ticc:: TICC_TRAP_TYPE
itrpt_lvl:: INTERRUPT_LEVEL
st_bar:: STORE_BARRIER_PENDING
atm_ldst_byte:: pb_block_ldst_byte
atm_ldst_word:: pb_block_ldst_word

definition get_annul :: "sparc_state_var  bool"
where "get_annul v  annul v"

definition get_reset_trap :: "sparc_state_var  bool"
where "get_reset_trap v  resett v"

definition get_exe_mode :: "sparc_state_var  bool"
where "get_exe_mode v  exe v"

definition get_reset_mode :: "sparc_state_var  bool"
where "get_reset_mode v  reset v"

definition get_err_mode :: "sparc_state_var  bool"
where "get_err_mode v  err v"

definition get_ticc_trap_type :: "sparc_state_var  word7"
where "get_ticc_trap_type v  ticc v"

definition get_interrupt_level :: "sparc_state_var  word3"
where "get_interrupt_level v  itrpt_lvl v"

definition get_store_barrier_pending :: "sparc_state_var  bool"
where "get_store_barrier_pending v  st_bar v"

definition write_annul :: "bool  sparc_state_var  sparc_state_var"
where "write_annul b v  vannul := b"

definition write_reset_trap :: "bool  sparc_state_var  sparc_state_var"
where "write_reset_trap b v  vresett := b"

definition write_exe_mode :: "bool  sparc_state_var  sparc_state_var"
where "write_exe_mode b v  vexe := b"

definition write_reset_mode :: "bool  sparc_state_var  sparc_state_var"
where "write_reset_mode b v  vreset := b"

definition write_err_mode :: "bool  sparc_state_var  sparc_state_var"
where "write_err_mode b v  verr := b"

definition write_ticc_trap_type :: "word7  sparc_state_var  sparc_state_var"
where "write_ticc_trap_type w v  vticc := w"

definition write_interrupt_level :: "word3  sparc_state_var  sparc_state_var"
where "write_interrupt_level w v  vitrpt_lvl := w"

definition write_store_barrier_pending :: "bool  sparc_state_var  sparc_state_var"
where "write_store_barrier_pending b v  vst_bar := b"

text ‹Given a word7 value, find the highest bit,
        and fill the left bits to be the highest bit.›
definition sign_ext7::"word7  word32"
where
"sign_ext7 w  
  let highest_bit = ((AND) w 0b1000000) >> 6 in
  if highest_bit = 0 then
    (ucast w)::word32
  else (OR) ((ucast w)::word32) 0b11111111111111111111111110000000
"

definition zero_ext8 :: "word8  word32"
where
"zero_ext8 w  (ucast w)::word32
"

text ‹Given a word8 value, find the highest bit,
        and fill the left bits to be the highest bit.›
definition sign_ext8::"word8  word32"
where
"sign_ext8 w  
  let highest_bit = ((AND) w 0b10000000) >> 7 in
  if highest_bit = 0 then
    (ucast w)::word32
  else (OR) ((ucast w)::word32) 0b11111111111111111111111100000000
"

text ‹Given a word13 value, find the highest bit,
        and fill the left bits to be the highest bit.›
definition sign_ext13::"word13  word32"
where
"sign_ext13 w  
  let highest_bit = ((AND) w 0b1000000000000) >> 12 in
  if highest_bit = 0 then
    (ucast w)::word32
  else (OR) ((ucast w)::word32) 0b11111111111111111110000000000000
"

definition zero_ext16 :: "word16  word32"
where
"zero_ext16 w  (ucast w)::word32
"

text ‹Given a word16 value, find the highest bit,
        and fill the left bits to be the highest bit.›
definition sign_ext16::"word16  word32"
where
"sign_ext16 w  
  let highest_bit = ((AND) w 0b1000000000000000) >> 15 in
  if highest_bit = 0 then
    (ucast w)::word32
  else (OR) ((ucast w)::word32) 0b11111111111111110000000000000000
"

text ‹Given a word22 value, find the highest bit,
        and fill the left bits to tbe the highest bit.›
definition sign_ext22::"word22  word32"
where
"sign_ext22 w 
  let highest_bit = ((AND) w 0b1000000000000000000000) >> 21 in
  if highest_bit = 0 then
    (ucast w)::word32
  else (OR) ((ucast w)::word32) 0b11111111110000000000000000000000
"

text ‹Given a word24 value, find the highest bit,
        and fill the left bits to tbe the highest bit.›
definition sign_ext24::"word24  word32"
where
"sign_ext24 w 
  let highest_bit = ((AND) w 0b100000000000000000000000) >> 23 in
  if highest_bit = 0 then
    (ucast w)::word32
  else (OR) ((ucast w)::word32) 0b11111111000000000000000000000000
"

text‹
Operations to be defined.
The SPARC V8 architecture is composed of the following set of instructions:
   Load Integer Instructions
   Load Floating-point Instructions
   Load Coprocessor Instructions
   Store Integer Instructions
   Store Floating-point Instructions
   Store Coprocessor Instructions
   Atomic Load-Store Unsigned Byte Instructions
   SWAP Register With Memory Instruction
   SETHI Instructions
   NOP Instruction
   Logical Instructions
   Shift Instructions
   Add Instructions
   Tagged Add Instructions
   Subtract Instructions
   Tagged Subtract Instructions
   Multiply Step Instruction
   Multiply Instructions
   Divide Instructions
   SAVE and RESTORE Instructions
   Branch on Integer Condition Codes Instructions
   Branch on Floating-point Condition Codes Instructions
   Branch on Coprocessor Condition Codes Instructions
   Call and Link Instruction
   Jump and Link Instruction
   Return from Trap Instruction
   Trap on Integer Condition Codes Instructions
   Read State Register Instructions
   Write State Register Instructions
   STBAR Instruction
   Unimplemented Instruction
   Flush Instruction Memory
   Floating-point Operate (FPop) Instructions
   Convert Integer to Floating point Instructions
   Convert Floating point to Integer Instructions
   Convert Between Floating-point Formats Instructions
   Floating-point Move Instructions
   Floating-point Square Root Instructions
   Floating-point Add and Subtract Instructions
   Floating-point Multiply and Divide Instructions
   Floating-point Compare Instructions
   Coprocessor Operate Instructions
›

text ‹The CALL instruction.›
datatype call_type = CALL ― ‹Call and Link›

text ‹The SETHI instruction.›
datatype sethi_type = SETHI    ― ‹Set High 22 bits of r Register›

text ‹The NOP instruction.›
datatype nop_type = NOP      ― ‹No Operation›

text ‹The Branch on integer condition codes instructions.› 
datatype bicc_type = 
  BE       ― ‹Branch on Equal›
 | BNE      ― ‹Branch on Not Equal›
 | BGU      ― ‹Branch on Greater Unsigned›
 | BLE      ― ‹Branch on Less or Equal›
 | BL       ― ‹Branch on Less›
 | BGE      ― ‹Branch on Greater or Equal›
 | BNEG     ― ‹Branch on Negative›
 | BG       ― ‹Branch on Greater›
 | BCS      ― ‹Branch on Carry Set (Less than, Unsigned)›
 | BLEU     ― ‹Branch on Less or Equal Unsigned›
 | BCC      ― ‹Branch on Carry Clear (Greater than or Equal, Unsigned)›
 | BA       ― ‹Branch Always›
 | BN       ― ‹Branch Never› ― ‹Added for unconditional branches›
 | BPOS     ― ‹Branch on Positive›
 | BVC      ― ‹Branch on Overflow Clear›
 | BVS      ― ‹Branch on Overflow Set›

text ‹Memory instructions. That is, load and store.›
datatype load_store_type =
  LDSB     ― ‹Load Signed Byte›
 | LDUB     ― ‹Load Unsigned Byte›
 | LDUBA    ― ‹Load Unsigned Byte from Alternate space›
 | LDUH     ― ‹Load Unsigned Halfword›
 | LD       ― ‹Load Word›
 | LDA      ― ‹Load Word from Alternate space›
 | LDD      ― ‹Load Doubleword›
 | STB      ― ‹Store Byte›
 | STH      ― ‹Store Halfword›
 | ST       ― ‹Store Word›
 | STA      ― ‹Store Word into Alternate space›
 | STD      ― ‹Store Doubleword›
 | LDSBA    ― ‹Load Signed Byte from Alternate space›
 | LDSH     ― ‹Load Signed Halfword›
 | LDSHA    ― ‹Load Signed Halfword from Alternate space›
 | LDUHA    ― ‹Load Unsigned Halfword from Alternate space›
 | LDDA     ― ‹Load Doubleword from Alternate space›
 | STBA     ― ‹Store Byte into Alternate space›
 | STHA     ― ‹Store Halfword into Alternate space›
 | STDA     ― ‹Store Doubleword into Alternate space›
 | LDSTUB   ― ‹Atomic Load Store Unsigned Byte›
 | LDSTUBA  ― ‹Atomic Load Store Unsinged Byte in Alternate space›
 | SWAP     ― ‹Swap r Register with Mmemory›
 | SWAPA    ― ‹Swap r Register with Mmemory in Alternate space›
 | FLUSH    ― ‹Flush Instruction Memory›
 | STBAR    ― ‹Store Barrier›

text ‹Arithmetic instructions.›
datatype arith_type =
  ADD      ― ‹Add›
 | ADDcc    ― ‹Add and modify icc›
 | ADDX     ― ‹Add with Carry›
 | SUB      ― ‹Subtract›
 | SUBcc    ― ‹Subtract and modify icc›
 | SUBX     ― ‹Subtract with Carry›
 | UMUL     ― ‹Unsigned Integer Multiply›
 | SMUL     ― ‹Signed Integer Multiply›
 | SMULcc   ― ‹Signed Integer Multiply and modify icc›
 | UDIV     ― ‹Unsigned Integer Divide›
 | UDIVcc   ― ‹Unsigned Integer Divide and modify icc›
 | SDIV     ― ‹Signed Integer Divide› 
 | ADDXcc   ― ‹Add with Carry and modify icc›
 | TADDcc   ― ‹Tagged Add and modify icc›
 | TADDccTV ― ‹Tagged Add and modify icc and Trap on overflow›
 | SUBXcc   ― ‹Subtract with Carry and modify icc›
 | TSUBcc   ― ‹Tagged Subtract and modify icc›
 | TSUBccTV ― ‹Tagged Subtract and modify icc and Trap on overflow›
 | MULScc   ― ‹Multiply Step and modify icc›
 | UMULcc   ― ‹Unsigned Integer Multiply and modify icc›
 | SDIVcc   ― ‹Signed Integer Divide and modify icc›

text ‹Logical instructions.›
datatype logic_type =
  ANDs      ― ‹And›
 | ANDcc    ― ‹And and modify icc›
 | ANDN     ― ‹And Not›
 | ANDNcc   ― ‹And Not and modify icc›
 | ORs       ― ‹Inclusive-Or›
 | ORcc     ― ‹Inclusive-Or and modify icc›
 | ORN      ― ‹Inclusive Or Not›
 | XORs      ― ‹Exclusive-Or›
 | XNOR     ― ‹Exclusive-Nor›
 | ORNcc    ― ‹Inclusive-Or Not and modify icc›
 | XORcc    ― ‹Exclusive-Or and modify icc›
 | XNORcc   ― ‹Exclusive-Nor and modify icc›
 
text ‹Shift instructions.›
datatype shift_type =
  SLL      ― ‹Shift Left Logical›
 | SRL      ― ‹Shift Right Logical›
 | SRA      ― ‹Shift Right Arithmetic› 

text ‹Other Control-transfer instructions.›
datatype ctrl_type = 
  JMPL     ― ‹Jump and Link›
 | RETT     ― ‹Return from Trap›
 | SAVE     ― ‹Save caller's window›
 | RESTORE  ― ‹Restore caller's window› 

text ‹Access state registers instructions.›
datatype sreg_type =
  RDASR    ― ‹Read Ancillary State Register›
 | RDY      ― ‹Read Y Register›
 | RDPSR    ― ‹Read Processor State Register›
 | RDWIM    ― ‹Read Window Invalid Mask Register›
 | RDTBR    ― ‹Read Trap Base Regiser›
 | WRASR    ― ‹Write Ancillary State Register›
 | WRY      ― ‹Write Y Register›
 | WRPSR    ― ‹Write Processor State Register›
 | WRWIM    ― ‹Write Window Invalid Mask Register›
 | WRTBR    ― ‹Write Trap Base Register› 

text ‹Unimplemented instruction.›
datatype uimp_type = UNIMP    ― ‹Unimplemented› 

text ‹Trap on integer condition code instructions.›
datatype ticc_type =
 TA       ― ‹Trap Always›
 | TN       ― ‹Trap Never›
 | TNE      ― ‹Trap on Not Equal›
 | TE       ― ‹Trap on Equal›
 | TG       ― ‹Trap on Greater›
 | TLE      ― ‹Trap on Less or Equal›
 | TGE      ― ‹Trap on Greater or Equal›
 | TL       ― ‹Trap on Less›
 | TGU      ― ‹Trap on Greater Unsigned›
 | TLEU     ― ‹Trap on Less or Equal Unsigned›
 | TCC      ― ‹Trap on Carry Clear (Greater than or Equal, Unsigned)›
 | TCS      ― ‹Trap on Carry Set (Less Than, Unsigned)›
 | TPOS     ― ‹Trap on Postive›
 | TNEG     ― ‹Trap on Negative›
 | TVC      ― ‹Trap on Overflow Clear›
 | TVS      ― ‹Trap on Overflow Set›

datatype sparc_operation =
  call_type call_type
 | sethi_type sethi_type
 | nop_type nop_type
 | bicc_type bicc_type
 | load_store_type load_store_type
 | arith_type arith_type
 | logic_type logic_type
 | shift_type shift_type
 | ctrl_type ctrl_type
 | sreg_type sreg_type
 | uimp_type uimp_type
 | ticc_type ticc_type

datatype Trap = 
reset 
|data_store_error
|instruction_access_MMU_miss
|instruction_access_error
|r_register_access_error
|instruction_access_exception
|privileged_instruction
|illegal_instruction
|unimplemented_FLUSH
|watchpoint_detected
|fp_disabled
|cp_disabled
|window_overflow
|window_underflow
|mem_address_not_aligned
|fp_exception
|cp_exception
|data_access_error
|data_access_MMU_miss
|data_access_exception
|tag_overflow
|division_by_zero
|trap_instruction
|interrupt_level_n

datatype Exception =
― ‹The following are processor states that are not in the instruction model,›
― ‹but we MAY want to deal with these from hardware perspective.›
⌦‹|execute_mode›
⌦‹|reset_mode›
⌦‹|error_mode›
― ‹The following are self-defined exceptions.›
invalid_cond_f2
|invalid_op2_f2
|illegal_instruction2 ― ‹when i = 0› for load/store not from alternate space›
|invalid_op3_f3_op11
|case_impossible
|invalid_op3_f3_op10
|invalid_op_f3
|unsupported_instruction
|fetch_instruction_error
|invalid_trap_cond

end

Theory Lib

(*
 * Copyright 2014, NICTA
 *
 * This software may be distributed and modified according to the terms of
 * the BSD 2-Clause license. Note that NO WARRANTY is provided.
 * See "LICENSE_BSD2.txt" for details.
 *
 * @TAG(NICTA_BSD)
 *)

(*
   Miscellaneous library definitions and lemmas.
*)

(*chapter "Library"*)

theory Lib
imports Main
begin

lemma hd_map_simp:
  "b  []  hd (map a b) = a (hd b)"
  by (rule hd_map)

lemma tl_map_simp:
  "tl (map a b) = map a (tl b)"
  by (induct b,auto)

lemma Collect_eq:
  "{x. P x} = {x. Q x}  (x. P x = Q x)"
  by (rule iffI) auto

lemma iff_impI: "P  Q = R  (P  Q) = (P  R)" by blast

definition
  fun_app :: "('a  'b)  'a  'b" (infixr "$" 10) where
  "f $ x  f x"

declare fun_app_def [iff]

lemma fun_app_cong[fundef_cong]:
  " f x = f' x'   (f $ x) = (f' $ x')"
  by simp

lemma fun_app_apply_cong[fundef_cong]:
  "f x y = f' x' y'  (f $ x) y = (f' $ x') y'"
  by simp

lemma if_apply_cong[fundef_cong]:
  " P = P'; x = x'; P'  f x' = f' x'; ¬ P'  g x' = g' x' 
      (if P then f else g) x = (if P' then f' else g') x'"
  by simp

abbreviation (input) split :: "('a  'b  'c)  'a × 'b  'c" where
  "split  case_prod"

lemma split_apply_cong[fundef_cong]:
  " f (fst p) (snd p) s = f' (fst p') (snd p') s'   split f p s = split f' p' s'"
  by (simp add: split_def)

definition
  pred_conj :: "('a  bool)  ('a  bool)  ('a  bool)" (infixl "and" 35)
where
  "pred_conj P Q  λx. P x  Q x"

definition
  pred_disj :: "('a  bool)  ('a  bool)  ('a  bool)" (infixl "or" 30)
where
  "pred_disj P Q  λx. P x  Q x"

definition
  pred_neg :: "('a  bool)  ('a  bool)" ("not _" [40] 40)
where
  "pred_neg P  λx. ¬ P x"

definition "K  λx y. x"

definition
  zipWith :: "('a  'b  'c)  'a list  'b list  'c list" where
  "zipWith f xs ys  map (split f) (zip xs ys)"

primrec
  delete :: "'a  'a list  'a list"
where
  "delete y [] = []"
| "delete y (x#xs) = (if y=x then xs else x # delete y xs)"

primrec
  find :: "('a  bool)  'a list  'a option"
where
  "find f [] = None"
| "find f (x # xs) = (if f x then Some x else find f xs)"

definition
 "swp f  λx y. f y x"

primrec (nonexhaustive)
  theRight :: "'a + 'b  'b" where
  "theRight (Inr x) = x"

primrec (nonexhaustive)
  theLeft :: "'a + 'b  'a" where
  "theLeft (Inl x) = x"

definition
 "isLeft x  (y. x = Inl y)"

definition
 "isRight x  (y. x = Inr y)"

definition
 "const x  λy. x"

lemma tranclD2:
  "(x, y)  R+  z. (x, z)  R*  (z, y)  R"
  by (erule tranclE) auto

lemma linorder_min_same1 [simp]:
  "(min y x = y) = (y  (x::'a::linorder))"
  by (auto simp: min_def linorder_not_less)

lemma linorder_min_same2 [simp]:
  "(min x y = y) = (y  (x::'a::linorder))"
  by (auto simp: min_def linorder_not_le)

text ‹A combinator for pairing up well-formed relations.
        The divisor function splits the population in halves,
        with the True half greater than the False half, and
        the supplied relations control the order within the halves.›

definition
  wf_sum :: "('a  bool)  ('a × 'a) set  ('a × 'a) set  ('a × 'a) set"
where
  "wf_sum divisor r r' 
     ({(x, y). ¬ divisor x  ¬ divisor y}  r')
     {(x, y). ¬ divisor x  divisor y}
    ({(x, y). divisor x  divisor y}  r)"

lemma wf_sum_wf:
  " wf r; wf r'   wf (wf_sum divisor r r')"
  apply (simp add: wf_sum_def)
  apply (rule wf_Un)+
      apply (erule wf_Int2)
     apply (rule wf_subset
             [where r="measure (λx. If (divisor x) 1 0)"])
      apply simp
     apply clarsimp
    apply blast
   apply (erule wf_Int2)
  apply blast
  done

abbreviation(input)
 "option_map == map_option"

lemmas option_map_def = map_option_case

lemma False_implies_equals [simp]:
  "((False  P)  PROP Q)  PROP Q"
  apply (rule equal_intr_rule)
   apply (erule meta_mp)
   apply simp
  apply simp
  done

lemma split_paired_Ball:
  "(x  A. P x) = (x y. (x,y)  A  P (x,y))"
  by auto

lemma split_paired_Bex:
  "(x  A. P x) = (x y. (x,y)  A  P (x,y))"
  by auto

end

Theory DetMonad

(*
 * Copyright 2014, NICTA
 *
 * This software may be distributed and modified according to the terms of
 * the BSD 2-Clause license. Note that NO WARRANTY is provided.
 * See "LICENSE_BSD2.txt" for details.
 *
 * @TAG(NICTA_BSD)
 *)

(*
* Zhe Hou: I modified this file to model a deterministic monad instead of
* a non-deterministic monad. Features that are irrelevant to deterministic 
* moands are removed. I also removed the section for loops, which are not
* used in the modelling of the SPARC architecture.
*)

(* 
   Deterministic state and error monads with failure in Isabelle.
*)

(*chapter "Deterministic State Monad with Failure"*)

theory DetMonad
imports "../Lib"
begin

text ‹
  \label{c:monads}

  State monads are used extensively in the seL4 specification. They are
  defined below.
›

section "The Monad"

text ‹
  The basic type of the deterministic state monad with failure is
  very similar to the normal state monad. Instead of a pair consisting
  of result and new state, we return a pair coupled with
  a failure flag. The flag is @{const True} if the computation have failed. 
  Conversely, if the flag is @{const False}, the computation resulting in 
  the returned result have succeeded.› 
type_synonym ('s,'a) det_monad = "'s  ('a × 's) × bool"


text ‹
  The definition of fundamental monad functions return› and
  bind›. The monad function return x› does not change 
  the  state, does not fail, and returns x›.
› 
definition
  return :: "'a  ('s,'a) det_monad" where
  "return a  λs. ((a,s),False)"

text ‹
  The monad function bind f g›, also written f >>= g›,
  is the execution of @{term f} followed by the execution of g›.
  The function g› takes the result value \emph{and} the result
  state of f› as parameter. The definition says that the result of
  the combined operation is the result which is created
  by g› applied to the result of f›. The combined
  operation may have failed, if f› may have failed or g› may
  have failed on the result of f›.
›

text ‹
 David Sanan and Zhe Hou: The original definition of bind is very inefficient 
 when converted to executable code. Here we change it to a more efficient
 version for execution. The idea remains the same.
›

definition "h1 f s = f s"
definition "h2 g fs = (let (a,b) = fst (fs) in g a b)"
definition bind:: "('s, 'a) det_monad  ('a  ('s, 'b) det_monad)  
           ('s, 'b) det_monad" (infixl ">>=" 60)
where
"bind f g  λs. (
  let fs = h1 f s;
      v = h2 g fs
  in
  (fst v, (snd v  snd fs)))"

text ‹
  Sometimes it is convenient to write bind› in reverse order.
›
abbreviation(input)
  bind_rev :: "('c  ('a, 'b) det_monad)  ('a, 'c) det_monad  
               ('a, 'b) det_monad" (infixl "=<<" 60) where 
  "g =<< f  f >>= g"

text ‹
  The basic accessor functions of the state monad. get› returns
  the current state as result, does not fail, and does not change the state.
  put s› returns nothing (@{typ unit}), changes the current state
  to s› and does not fail.
›
definition
  get :: "('s,'s) det_monad" where
  "get  λs. ((s,s), False)"

definition
  put :: "'s  ('s, unit) det_monad" where
  "put s  λ_. (((),s), False)"

subsection "Failure"

text ‹The monad function that always fails. Returns the current 
  state and sets the failure flag.›
definition
  fail :: "'a  ('s, 'a) det_monad" where
 "fail a  λs. ((a,s), True)"

text ‹Assertions: fail if the property P› is not true›
definition
  assert :: "bool  ('a, unit) det_monad" where
 "assert P  if P then return () else fail ()"

text ‹An assertion that also can introspect the current state.›

definition
  state_assert :: "('s  bool)  ('s, unit) det_monad"
where
  "state_assert P  get >>= (λs. assert (P s))"

subsection "Generic functions on top of the state monad"

text ‹Apply a function to the current state and return the result
without changing the state.›
definition
  gets :: "('s  'a)  ('s, 'a) det_monad" where
 "gets f  get >>= (λs. return (f s))"

text ‹Modify the current state using the function passed in.›
definition
  modify :: "('s  's)  ('s, unit) det_monad" where
 "modify f  get >>= (λs. put (f s))"

lemma simpler_gets_def: "gets f = (λs. ((f s, s), False))"
  apply (simp add: gets_def return_def bind_def h1_def h2_def get_def)
  done

lemma simpler_modify_def:
  "modify f = (λs. (((), f s), False))"
  by (simp add: modify_def bind_def h1_def h2_def get_def put_def)

text ‹Execute the given monad when the condition is true, 
  return ()› otherwise.›
definition
  when1 :: "bool  ('s, unit) det_monad  
           ('s, unit) det_monad" where 
  "when1 P m  if P then m else return ()"

text ‹Execute the given monad unless the condition is true, 
  return ()› otherwise.›
definition 
  unless :: "bool  ('s, unit) det_monad  
            ('s, unit) det_monad" where
  "unless P m  when1 (¬P) m"

text ‹
  Perform a test on the current state, performing the left monad if
  the result is true or the right monad if the result is false.
›
definition
  condition :: "('s  bool)  ('s, 'r) det_monad  ('s, 'r) det_monad  ('s, 'r) det_monad"
where
  "condition P L R  λs. if (P s) then (L s) else (R s)"

notation (output)
  condition  ("(condition (_)//  (_)//  (_))" [1000,1000,1000] 1000)

subsection ‹The Monad Laws›

text ‹Each monad satisfies at least the following three laws.›

text @{term return} is absorbed at the left of a @{term bind}, 
  applying the return value directly:› 
lemma return_bind [simp]: "(return x >>= f) = f x"
  by (simp add: return_def bind_def h1_def h2_def)

text @{term return} is absorbed on the right of a @{term bind} 
lemma bind_return [simp]: "(m >>= return) = m"
  apply (rule ext)
  apply (simp add: bind_def h1_def h2_def return_def split_def)
  done
 
text @{term bind} is associative›
lemma bind_assoc: 
  fixes m :: "('a,'b) det_monad"
  fixes f :: "'b  ('a,'c) det_monad"
  fixes g :: "'c  ('a,'d) det_monad"
  shows "(m >>= f) >>= g  =  m >>= (λx. f x >>= g)"
  apply (unfold bind_def h1_def h2_def Let_def split_def)
  apply (rule ext)
  apply clarsimp
  done


section ‹Adding Exceptions›

text ‹
  The type @{typ "('s,'a) det_monad"} gives us determinism and
  failure. We now extend this monad with exceptional return values
  that abort normal execution, but can be handled explicitly.
  We use the sum type to indicate exceptions. 

  In @{typ "('s, 'e + 'a) det_monad"}, @{typ "'s"} is the state,
  @{typ 'e} is an exception, and @{typ 'a} is a normal return value.

  This new type itself forms a monad again. Since type classes in 
  Isabelle are not powerful enough to express the class of monads,
  we provide new names for the @{term return} and @{term bind} functions
  in this monad. We call them returnOk› (for normal return values)
  and bindE› (for composition). We also define throwError›
  to return an exceptional value.
›
definition
  returnOk :: "'a  ('s, 'e + 'a) det_monad" where
  "returnOk  return o Inr"

definition
  throwError :: "'e  ('s, 'e + 'a) det_monad" where
  "throwError  return o Inl"

text ‹
  Lifting a function over the exception type: if the input is an
  exception, return that exception; otherwise continue execution.
›
definition
  lift :: "('a  ('s, 'e + 'b) det_monad)  
           'e +'a  ('s, 'e + 'b) det_monad"
where
  "lift f v  case v of Inl e  throwError e
                      | Inr v'  f v'"

text ‹
  The definition of @{term bind} in the exception monad (new
  name bindE›): the same as normal @{term bind}, but 
  the right-hand side is skipped if the left-hand side
  produced an exception.
›
definition
  bindE :: "('s, 'e + 'a) det_monad  
            ('a  ('s, 'e + 'b) det_monad)  
            ('s, 'e + 'b) det_monad"  (infixl ">>=E" 60)
where
  "bindE f g  bind f (lift g)"


text ‹
  Lifting a normal deterministic monad into the 
  exception monad is achieved by always returning its
  result as normal result and never throwing an exception.
›
definition
  liftE :: "('s,'a) det_monad  ('s, 'e+'a) det_monad"
where
  "liftE f  f >>= (λr. return (Inr r))"


text ‹
  Since the underlying type and return› function changed, 
  we need new definitions for when and unless:
›
definition
  whenE :: "bool  ('s, 'e + unit) det_monad  
            ('s, 'e + unit) det_monad" 
  where
  "whenE P f  if P then f else returnOk ()"

definition
  unlessE :: "bool  ('s, 'e + unit) det_monad  
            ('s, 'e + unit) det_monad" 
  where
  "unlessE P f  if P then returnOk () else f"


text ‹
  Throwing an exception when the parameter is @{term None}, otherwise
  returning @{term "v"} for @{term "Some v"}.
›
definition
  throw_opt :: "'e  'a option  ('s, 'e + 'a) det_monad" where
  "throw_opt ex x  
  case x of None  throwError ex | Some v  returnOk v"

subsection "Monad Laws for the Exception Monad"

text ‹More direct definition of @{const liftE}:›
lemma liftE_def2:
  "liftE f = (λs. ((λ(v,s'). (Inr v, s'))  (fst (f s)), snd (f s)))"
  by (auto simp: Let_def liftE_def return_def split_def bind_def h1_def h2_def)
  
text ‹Left @{const returnOk} absorbtion over @{term bindE}:›
lemma returnOk_bindE [simp]: "(returnOk x >>=E f) = f x"
  apply (unfold bindE_def returnOk_def)
  apply (clarsimp simp: lift_def)
  done

lemma lift_return [simp]:
  "lift (return  Inr) = return"
  by (rule ext)
     (simp add: lift_def throwError_def split: sum.splits)

text ‹Right @{const returnOk} absorbtion over @{term bindE}:›
lemma bindE_returnOk [simp]: "(m >>=E returnOk) = m"
  by (simp add: bindE_def returnOk_def)

text ‹Associativity of @{const bindE}:›
lemma bindE_assoc:
  "(m >>=E f) >>=E g = m >>=E (λx. f x >>=E g)"
  apply (simp add: bindE_def bind_assoc)
  apply (rule arg_cong [where f="λx. m >>= x"])
  apply (rule ext)
  apply (case_tac x, simp_all add: lift_def throwError_def)
  done

text @{const returnOk} could also be defined via @{const liftE}:›
lemma returnOk_liftE:
  "returnOk x = liftE (return x)"
  by (simp add: liftE_def returnOk_def)

text ‹Execution after throwing an exception is skipped:›
lemma throwError_bindE [simp]:
  "(throwError E >>=E f) = throwError E"
  by (simp add: bindE_def bind_def h1_def h2_def throwError_def lift_def return_def)


section "Syntax"

text ‹This section defines traditional Haskell-like do-syntax 
  for the state monad in Isabelle.›

subsection "Syntax for the Nondeterministic State Monad"

text ‹We use K_bind› to syntactically indicate the 
  case where the return argument of the left side of a @{term bind}
  is ignored›
definition
  K_bind_def [iff]: "K_bind  λx y. x"

nonterminal
  dobinds and dobind and nobind

syntax
  "_dobind"    :: "[pttrn, 'a] => dobind"             ("(_ / _)" 10)
  ""           :: "dobind => dobinds"                 ("_")
  "_nobind"    :: "'a => dobind"                      ("_")
  "_dobinds"   :: "[dobind, dobinds] => dobinds"      ("(_);//(_)")

  "_do"        :: "[dobinds, 'a] => 'a"               ("(do ((_);//(_))//od)" 100)
translations
  "_do (_dobinds b bs) e"  == "_do b (_do bs e)"
  "_do (_nobind b) e"      == "b >>= (CONST K_bind e)"
  "do x  a; e od"        == "a >>= (λx. e)"  

text ‹Syntax examples:›
lemma "do x  return 1; 
          return (2::nat); 
          return x 
       od = 
       return 1 >>= 
       (λx. return (2::nat) >>= 
            K_bind (return x))" 
  by (rule refl)

lemma "do x  return 1; 
          return 2; 
          return x 
       od = return 1" 
  by simp

subsection "Syntax for the Exception Monad"

text ‹
  Since the exception monad is a different type, we
  need to syntactically distinguish it in the syntax.
  We use doE›/odE› for this, but can re-use
  most of the productions from do›/od›
  above.
›

syntax
  "_doE" :: "[dobinds, 'a] => 'a"  ("(doE ((_);//(_))//odE)" 100)

translations
  "_doE (_dobinds b bs) e"  == "_doE b (_doE bs e)"
  "_doE (_nobind b) e"      == "b >>=E (CONST K_bind e)"
  "doE x  a; e odE"       == "a >>=E (λx. e)"

text ‹Syntax examples:›
lemma "doE x  returnOk 1; 
           returnOk (2::nat); 
           returnOk x 
       odE =
       returnOk 1 >>=E 
       (λx. returnOk (2::nat) >>=E 
            K_bind (returnOk x))"
  by (rule refl)

lemma "doE x  returnOk 1; 
           returnOk 2; 
           returnOk x 
       odE = returnOk 1" 
  by simp



section "Library of Monadic Functions and Combinators"


text ‹Lifting a normal function into the monad type:›
definition
  liftM :: "('a  'b)  ('s,'a) det_monad  ('s, 'b) det_monad"
where
  "liftM f m  do x  m; return (f x) od"

text ‹The same for the exception monad:›
definition
  liftME :: "('a  'b)  ('s,'e+'a) det_monad  ('s,'e+'b) det_monad"
where
  "liftME f m  doE x  m; returnOk (f x) odE"

text ‹
  Run a sequence of monads from left to right, ignoring return values.›
definition
  sequence_x :: "('s, 'a) det_monad list  ('s, unit) det_monad" 
where
  "sequence_x xs  foldr (λx y. x >>= (λ_. y)) xs (return ())"

text ‹
  Map a monadic function over a list by applying it to each element
  of the list from left to right, ignoring return values.
›
definition
  mapM_x :: "('a  ('s,'b) det_monad)  'a list  ('s, unit) det_monad"
where
  "mapM_x f xs  sequence_x (map f xs)"

text ‹
  Map a monadic function with two parameters over two lists,
  going through both lists simultaneously, left to right, ignoring
  return values.
›
definition
  zipWithM_x :: "('a  'b  ('s,'c) det_monad)  
                 'a list  'b list  ('s, unit) det_monad"
where
  "zipWithM_x f xs ys  sequence_x (zipWith f xs ys)"


text ‹The same three functions as above, but returning a list of
return values instead of unit›
definition
  sequence :: "('s, 'a) det_monad list  ('s, 'a list) det_monad" 
where
  "sequence xs  let mcons = (λp q. p >>= (λx. q >>= (λy. return (x#y))))
                 in foldr mcons xs (return [])"

definition
  mapM :: "('a  ('s,'b) det_monad)  'a list  ('s, 'b list) det_monad"
where
  "mapM f xs  sequence (map f xs)"

definition
  zipWithM :: "('a  'b  ('s,'c) det_monad)  
                 'a list  'b list  ('s, 'c list) det_monad"
where
  "zipWithM f xs ys  sequence (zipWith f xs ys)"

definition
  foldM :: "('b  'a  ('s, 'a) det_monad)  'b list  'a  ('s, 'a) det_monad" 
where
  "foldM m xs a  foldr (λp q. q >>= m p) xs (return a) "

text ‹The sequence and map functions above for the exception monad,
with and without lists of return value›
definition
  sequenceE_x :: "('s, 'e+'a) det_monad list  ('s, 'e+unit) det_monad" 
where
  "sequenceE_x xs  foldr (λx y. doE _  x; y odE) xs (returnOk ())"

definition
  mapME_x :: "('a  ('s,'e+'b) det_monad)  'a list  
              ('s,'e+unit) det_monad"
where
  "mapME_x f xs  sequenceE_x (map f xs)"

definition
  sequenceE :: "('s, 'e+'a) det_monad list  ('s, 'e+'a list) det_monad" 
where
  "sequenceE xs  let mcons = (λp q. p >>=E (λx. q >>=E (λy. returnOk (x#y))))
                 in foldr mcons xs (returnOk [])"

definition
  mapME :: "('a  ('s,'e+'b) det_monad)  'a list  
              ('s,'e+'b list) det_monad"
where
  "mapME f xs  sequenceE (map f xs)"


text ‹Filtering a list using a monadic function as predicate:›
primrec
  filterM :: "('a  ('s, bool) det_monad)  'a list  ('s, 'a list) det_monad"
where
  "filterM P []       = return []"
| "filterM P (x # xs) = do
     b   P x;
     ys  filterM P xs; 
     return (if b then (x # ys) else ys)
   od"


section "Catching and Handling Exceptions"

text ‹
  Turning an exception monad into a normal state monad
  by catching and handling any potential exceptions:
›
definition
  catch :: "('s, 'e + 'a) det_monad 
            ('e  ('s, 'a) det_monad) 
            ('s, 'a) det_monad" (infix "<catch>" 10)
where
  "f <catch> handler 
     do x  f;
        case x of
          Inr b  return b
        | Inl e  handler e
     od"

text ‹
  Handling exceptions, but staying in the exception monad.
  The handler may throw a type of exceptions different from
  the left side.
›
definition
  handleE' :: "('s, 'e1 + 'a) det_monad 
               ('e1  ('s, 'e2 + 'a) det_monad) 
               ('s, 'e2 + 'a) det_monad" (infix "<handle2>" 10)
where
  "f <handle2> handler 
   do
      v  f;
      case v of
        Inl e  handler e
      | Inr v'  return (Inr v')
   od"

text ‹
  A type restriction of the above that is used more commonly in
  practice: the exception handle (potentially) throws exception
  of the same type as the left-hand side.
›
definition
  handleE :: "('s, 'x + 'a) det_monad  
              ('x  ('s, 'x + 'a) det_monad)  
              ('s, 'x + 'a) det_monad" (infix "<handle>" 10)
where
  "handleE  handleE'"


text ‹
  Handling exceptions, and additionally providing a continuation
  if the left-hand side throws no exception:
›
definition
  handle_elseE :: "('s, 'e + 'a) det_monad 
                   ('e  ('s, 'ee + 'b) det_monad) 
                   ('a  ('s, 'ee + 'b) det_monad) 
                   ('s, 'ee + 'b) det_monad"
  ("_ <handle> _ <else> _" 10)
where
  "f <handle> handler <else> continue 
   do v  f;
   case v of Inl e   handler e
           | Inr v'  continue v'
   od"

section "Hoare Logic"

subsection "Validity"

text ‹This section defines a Hoare logic for partial correctness for
  the deterministic state monad as well as the exception monad.
  The logic talks only about the behaviour part of the monad and ignores
  the failure flag.

  The logic is defined semantically. Rules work directly on the
  validity predicate.

  In the deterministic state monad, validity is a triple of precondition,
  monad, and postcondition. The precondition is a function from state to 
  bool (a state predicate), the postcondition is a function from return value
  to state to bool. A triple is valid if for all states that satisfy the
  precondition, all result values and result states that are returned by
  the monad satisfy the postcondition. Note that if the computation returns
  the empty set, the triple is trivially valid. This means @{term "assert P"} 
  does not require us to prove that @{term P} holds, but rather allows us
  to assume @{term P}! Proving non-failure is done via separate predicate and
  calculus (see below).
›
definition
  valid :: "('s  bool)  ('s,'a) det_monad  ('a  's  bool)  bool" 
  ("_/ _ /_")
where
  "P f Q  s. P s  (r s'. ((r,s') = fst (f s)  Q r s'))"

text ‹
  Validity for the exception monad is similar and build on the standard 
  validity above. Instead of one postcondition, we have two: one for
  normal and one for exceptional results.
›
definition
  validE :: "('s  bool)  ('s, 'a + 'b) det_monad  
             ('b  's  bool)  
             ('a  's  bool)  bool" 
("_/ _ /(_⦄,/ _)")
where
  "P f Q⦄,E  P f  λv s. case v of Inr r  Q r s | Inl e  E e s "


text ‹
  The following two instantiations are convenient to separate reasoning
  for exceptional and normal case.
›
definition
  validE_R :: "('s  bool)  ('s, 'e + 'a) det_monad  
               ('a  's  bool)  bool"
   ("_/ _ /_⦄, -")
where
 "P f Q⦄,-  validE P f Q (λx y. True)"

definition
  validE_E :: "('s  bool)   ('s, 'e + 'a) det_monad  
               ('e  's  bool)  bool"
   ("_/ _ /-, _")
where
 "P f -,Q  validE P f (λx y. True) Q"


text ‹Abbreviations for trivial preconditions:›
abbreviation(input)
  top :: "'a  bool" ("")
where
  "  λ_. True"

abbreviation(input)
  bottom :: "'a  bool" ("")
where
  "  λ_. False"

text ‹Abbreviations for trivial postconditions (taking two arguments):›
abbreviation(input)
  toptop :: "'a  'b  bool" ("⊤⊤")
where
 "⊤⊤  λ_ _. True"

abbreviation(input)
  botbot :: "'a  'b  bool" ("⊥⊥")
where
 "⊥⊥  λ_ _. False"

text ‹
  Lifting ∧› and ∨› over two arguments. 
  Lifting ∧› and ∨› over one argument is already
  defined (written and› and or›).
›
definition
  bipred_conj :: "('a  'b  bool)  ('a  'b  bool)  ('a  'b  bool)" 
  (infixl "And" 96)
where
  "bipred_conj P Q  λx y. P x y  Q x y"

definition
  bipred_disj :: "('a  'b  bool)  ('a  'b  bool)  ('a  'b  bool)" 
  (infixl "Or" 91)
where
  "bipred_disj P Q  λx y. P x y  Q x y"


subsection "Determinism"

text ‹A monad of type det_monad› is deterministic iff it
returns exactly one state and result and does not fail› 
definition
  det :: "('a,'s) det_monad  bool"
where
  "det f  s. r. f s = (r,False)" 

text ‹A deterministic det_monad› can be turned
  into a normal state monad:›
definition
  the_run_state :: "('s,'a) det_monad  's  'a × 's"
where
  "the_run_state M  λs. THE s'. fst (M s) = s'"


subsection "Non-Failure"

text ‹
  With the failure flag, we can formulate non-failure separately
  from validity. A monad m› does not fail under precondition
  P›, if for no start state in that precondition it sets
  the failure flag.
›
definition
  no_fail :: "('s  bool)  ('s,'a) det_monad  bool"
where
  "no_fail P m  s. P s  ¬ (snd (m s))"


text ‹
  It is often desired to prove non-failure and a Hoare triple
  simultaneously, as the reasoning is often similar. The following
  definitions allow such reasoning to take place.
›

definition
  validNF ::"('s  bool)  ('s,'a) det_monad  ('a  's  bool)  bool"
      ("_/ _ /_⦄!")
where
  "validNF P f Q  valid P f Q  no_fail P f"

definition
  validE_NF :: "('s  bool)  ('s, 'a + 'b) det_monad 
             ('b  's  bool) 
             ('a  's  bool)  bool"
  ("_/ _ /(_⦄,/ _⦄!)")
where
  "validE_NF P f Q E  validE P f Q E  no_fail P f"

lemma validE_NF_alt_def:
  " P  B  Q ⦄, E ⦄! =  P  B  λv s. case v of Inl e  E e s | Inr r  Q r s ⦄!"
  by (clarsimp simp: validE_NF_def validE_def validNF_def)

section "Basic exception reasoning"

text ‹
  The following predicates no_throw› and no_return› allow
  reasoning that functions in the exception monad either do
  no throw an exception or never return normally.
›

definition "no_throw P A   P  A  λ_ _. True ⦄, λ_ _. False "

definition "no_return P A   P  A λ_ _. False⦄,λ_ _. True "

end

Theory DetMonadLemmas

(*
 * Copyright 2014, NICTA
 *
 * This software may be distributed and modified according to the terms of
 * the BSD 2-Clause license. Note that NO WARRANTY is provided.
 * See "LICENSE_BSD2.txt" for details.
 *
 * @TAG(NICTA_BSD)
 *)

(* Zhe Hou: I removed the lemmas related to the definitions which are 
*  removed from DetMonad. That is, only those lemmas for deterministic
*  monads are kept here. 
*)

theory DetMonadLemmas
imports DetMonad
begin

section "General Lemmas Regarding the Deterministic State Monad"

subsection "Congruence Rules for the Function Package"

lemma bind_cong[fundef_cong]:
  " f = f'; v s s'. (v, s') = fst (f' s)  g v s' = g' v s'   f >>= g = f' >>= g'"
  apply (rule ext) 
  apply (auto simp: bind_def h1_def h2_def Let_def split_def intro: rev_image_eqI)
  done

lemma bind_apply_cong [fundef_cong]:
  " f s = f' s'; rv st. (rv, st) = fst (f' s')  g rv st = g' rv st 
        (f >>= g) s = (f' >>= g') s'"
  apply (simp add: bind_def h1_def h2_def)
  apply (auto simp: split_def intro: SUP_cong [OF refl] intro: rev_image_eqI)
  done

lemma bindE_cong[fundef_cong]:
  " M = M' ; v s s'. (Inr v, s') = fst (M' s)  N v s' = N' v s'   bindE M N = bindE M' N'"
  apply (simp add: bindE_def)
  apply (rule bind_cong)
   apply (rule refl)
  apply (unfold lift_def)
  apply (case_tac v, simp_all)
  done

lemma bindE_apply_cong[fundef_cong]:
  " f s = f' s'; rv st. (Inr rv, st) = fst (f' s')  g rv st = g' rv st  
   (f >>=E g) s = (f' >>=E g') s'"
  apply (simp add: bindE_def)
  apply (rule bind_apply_cong)
   apply assumption
  apply (case_tac rv, simp_all add: lift_def)
  done

lemma K_bind_apply_cong[fundef_cong]:
  " f st = f' st'   K_bind f arg st = K_bind f' arg' st'"
  by simp

lemma when_apply_cong[fundef_cong]:
  " C = C'; s = s'; C'  m s' = m' s'   whenE C m s = whenE C' m' s'"
  by (simp add: whenE_def)

lemma unless_apply_cong[fundef_cong]:
  " C = C'; s = s'; ¬ C'  m s' = m' s'   unlessE C m s = unlessE C' m' s'"
  by (simp add: unlessE_def)

lemma whenE_apply_cong[fundef_cong]:
  " C = C'; s = s'; C'  m s' = m' s'   whenE C m s = whenE C' m' s'"
  by (simp add: whenE_def)

lemma unlessE_apply_cong[fundef_cong]:
  " C = C'; s = s'; ¬ C'  m s' = m' s'   unlessE C m s = unlessE C' m' s'"
  by (simp add: unlessE_def)

subsection "Simplifying Monads"

lemma nested_bind [simp]:
  "do x  do y  f; return (g y) od; h x od =
   do y  f; h (g y) od"
  apply (clarsimp simp add: bind_def h1_def h2_def)
  apply (rule ext)
  apply (clarsimp simp add: Let_def split_def return_def)
  done

lemma assert_True [simp]:
  "assert True >>= f = f ()"
  by (simp add: assert_def)

lemma when_True_bind [simp]:
  "when1 True g >>= f = g >>= f"
  by (simp add: when1_def bind_def return_def)

lemma whenE_False_bind [simp]:
  "whenE False g >>=E f = f ()"
  by (simp add: whenE_def bindE_def returnOk_def lift_def)

lemma whenE_True_bind [simp]:
  "whenE True g >>=E f = g >>=E f"
  by (simp add: whenE_def bindE_def returnOk_def lift_def)

lemma when_True [simp]: "when1 True X = X"
  by (clarsimp simp: when1_def)

lemma when_False [simp]: "when1 False X = return ()"
  by (clarsimp simp: when1_def)

lemma unless_False [simp]: "unless False X = X"
  by (clarsimp simp: unless_def)

lemma unless_True [simp]: "unless True X = return ()"
  by (clarsimp simp: unless_def)

lemma unlessE_whenE:
  "unlessE P = whenE (~P)"
  by (rule ext)+ (simp add: unlessE_def whenE_def)

lemma unless_when:
  "unless P = when1 (~P)"
  by (rule ext)+ (simp add: unless_def when1_def)

lemma gets_to_return [simp]: "gets (λs. v) = return v"
  by (clarsimp simp: gets_def put_def get_def bind_def h1_def h2_def return_def)

lemma liftE_handleE' [simp]: "((liftE a) <handle2> b) = liftE a"
  apply (clarsimp simp: liftE_def handleE'_def)
  done

lemma liftE_handleE [simp]: "((liftE a) <handle> b) = liftE a"
  apply (unfold handleE_def)
  apply simp
  done

lemma condition_split:
  "P (condition C a b s) = ((((C s)  P (a s))  (¬ (C s)  P (b s))))"
  apply (clarsimp simp: condition_def)
  done

lemma condition_split_asm:
  "P (condition C a b s) = (¬ (C s  ¬ P (a s)  ¬ C s  ¬ P (b s)))"
  apply (clarsimp simp: condition_def)
  done

lemmas condition_splits = condition_split condition_split_asm

lemma condition_true_triv [simp]:
  "condition (λ_. True) A B = A"
  apply (rule ext)
  apply (clarsimp split: condition_splits)
  done

lemma condition_false_triv [simp]:
  "condition (λ_. False) A B = B"
  apply (rule ext)
  apply (clarsimp split: condition_splits)
  done

lemma condition_true: " P s   condition P A B s = A s"
  apply (clarsimp simp: condition_def)
  done

lemma condition_false: " ¬ P s   condition P A B s = B s"
  apply (clarsimp simp: condition_def)
  done

section "Low-level monadic reasoning"

lemma valid_make_schematic_post:
  "(s0.  λs. P s0 s  f  λrv s. Q s0 rv s ) 
    λs. s0. P s0 s  (rv s'. Q s0 rv s'  Q' rv s')  f  Q' "
  by (auto simp add: valid_def no_fail_def split: prod.splits)

lemma validNF_make_schematic_post:
  "(s0.  λs. P s0 s  f  λrv s. Q s0 rv s ⦄!) 
    λs. s0. P s0 s  (rv s'. Q s0 rv s'  Q' rv s')  f  Q' ⦄!"
  by (auto simp add: valid_def validNF_def no_fail_def split: prod.splits)

lemma validE_make_schematic_post:
  "(s0.  λs. P s0 s  f  λrv s. Q s0 rv s ⦄,  λrv s. E s0 rv s ) 
    λs. s0. P s0 s  (rv s'. Q s0 rv s'  Q' rv s')
         (rv s'. E s0 rv s'  E' rv s')  f  Q' ⦄,  E' "
  by (auto simp add: validE_def valid_def no_fail_def split: prod.splits sum.splits)

lemma validE_NF_make_schematic_post:
  "(s0.  λs. P s0 s  f  λrv s. Q s0 rv s ⦄,  λrv s. E s0 rv s ⦄!) 
    λs. s0. P s0 s  (rv s'. Q s0 rv s'  Q' rv s')
         (rv s'. E s0 rv s'  E' rv s')  f  Q' ⦄,  E' ⦄!"
  by (auto simp add: validE_NF_def validE_def valid_def no_fail_def split: prod.splits sum.splits)

lemma validNF_conjD1: " P  f  λrv s. Q rv s  Q' rv s ⦄!   P  f  Q ⦄!"
  by (fastforce simp: validNF_def valid_def no_fail_def)

lemma validNF_conjD2: " P  f  λrv s. Q rv s  Q' rv s ⦄!   P  f  Q' ⦄!"
  by (fastforce simp: validNF_def valid_def no_fail_def)

lemma exec_gets:
  "(gets f >>= m) s = m (f s) s"
  by (simp add: simpler_gets_def bind_def h1_def h2_def)

lemma in_gets:
  "(r, s') = fst (gets f s) = (r = f s  s' = s)"
  by (simp add: simpler_gets_def)

end

Theory RegistersOps

section‹Register Operations›
theory RegistersOps
imports Main "../lib/WordDecl" "Word_Lib.Traditional_Infix_Syntax"
begin

text‹
 This theory provides operations to get, set and clear bits in registers
›

section "Getting Fields"
  
text‹
  Get a field of type @{typ "'b::len word"} 
  starting at @{term "index"} from @{term "addr"} of type @{typ "'a::len word"}
definition get_field_from_word_a_b:: "'a::len word  nat  'b::len word"
 where
  "get_field_from_word_a_b addr index 
     let off = (size addr - LENGTH('b)) 
       in ucast ((addr << (off-index)) >> off)"

text‹
  Obtain, from addr of type @{typ "'a::len word"}, 
  another @{typ "'a::len word"} containing the field of length len›
  starting at index› in addr›. 
›
definition get_field_from_word_a_a:: "'a::len word  nat  nat  'a::len word"
 where
  "get_field_from_word_a_a addr index len 
     (addr << (size addr - (index+len)) >> (size addr - len))"

section "Setting Fields"

text‹
  Set the field of type @{typ "'b::len word"} 
  at index› from record›
  of type @{typ "'a::len word"}. 
›
definition set_field :: "'a::len word  'b::len word  nat  'a::len word"
 where 
  "set_field record field index 
     let mask:: ('a::len word) = (mask (size field)) << index 
      in  (record AND (NOT mask)) OR ((ucast field) << index)"


section "Clearing Fields"

text‹
  Zero the n› initial bits of addr›.
›
definition clear_n_bits:: "'a::len word  nat  'a::len word" 
 where
   "clear_n_bits addr n  addr AND (NOT (mask n))"

text‹
  Gets the natural value of a 32 bit mask 
›

definition get_nat_from_mask::"word32  nat  nat  (word32 × nat)" 
where
"
get_nat_from_mask w m v  if (w AND (mask m) =0) then (w>>m, v+m)
                          else (w,m)
"

definition get_nat_from_mask32::"word32 nat"
where
"get_nat_from_mask32 w  
                            if (w=0) then len_of TYPE (word_length32)
                            else
                                let (w,res) = get_nat_from_mask w 16 0 in
                                     let (w,res)= get_nat_from_mask w 8 res in
                                          let (w,res) = get_nat_from_mask w 4 res in
                                              let (w,res) = get_nat_from_mask w 2 res in
                                                  let (w,res) = get_nat_from_mask w 1 res in
                                                        res
"

end 

Theory MMU

(*  Title:     Memory.thy
    Author:    David Sanán, Trinity College Dublin, 2012
               Zhe Hou, NTU, 2016.
*)


section ‹Memory Management Unit (MMU)›

theory MMU
imports Main RegistersOps Sparc_Types
begin

section ‹MMU  Sizing› 

text‹
  We need some citation here for documentation about the MMU.
›
text‹The MMU uses the Address Space Identifiers (ASI) to control memory access.
ASI = 8, 10 are for user; ASI = 9, 11 are for supervisor.›

subsection "MMU Types"

type_synonym word_PTE_flags = word8
type_synonym word_length_PTE_flags = word_length8

subsection "MMU length values"

text‹Definitions for the length of the virtua address, page size,  
virtual translation tables indexes, virtual address offset and Page protection flags›


definition length_entry_type :: "nat" 
where "length_entry_type  LENGTH(word_length_entry_type)" 
definition length_phys_address:: "nat" 
where "length_phys_address  LENGTH(word_length_phys_address)"
definition length_virtua_address:: "nat" 
where "length_virtua_address  LENGTH(word_length_virtua_address)"
definition length_page:: "nat" where "length_page  LENGTH(word_length_page)"
definition length_t1:: "nat" where "length_t1  LENGTH(word_length_t1)"
definition length_t2:: "nat" where "length_t2  LENGTH(word_length_t2)"
definition length_t3:: "nat" where "length_t3  LENGTH(word_length_t3)"
definition length_offset:: "nat" where "length_offset  LENGTH(word_length_offset)"
definition length_PTE_flags :: "nat" where 
"length_PTE_flags  LENGTH(word_length_PTE_flags)"

subsection "MMU index values"

definition va_t1_index :: "nat" where "va_t1_index  length_virtua_address - length_t1"
definition va_t2_index :: "nat" where "va_t2_index  va_t1_index - length_t2"
definition va_t3_index :: "nat" where "va_t3_index  va_t2_index - length_t3"
definition va_offset_index :: "nat" where "va_offset_index  va_t3_index - length_offset"
definition pa_page_index :: "nat" 
where "pa_page_index  length_phys_address - length_page"
definition pa_offset_index :: "nat" where 
"pa_offset_index  pa_page_index -length_page"

section ‹MMU Definition›

record MMU_state =
   registers :: "MMU_context"
(*   contexts:: context_table*)

text ‹The following functions access MMU registers via addresses. 
  See UT699LEON3FT manual page 35.›

definition mmu_reg_val:: "MMU_state  virtua_address  machine_word option"
where "mmu_reg_val mmu_state addr 
  if addr = 0x000 then ― ‹MMU control register›
    Some ((registers mmu_state) CR)
  else if addr = 0x100 then ― ‹Context pointer register›
    Some ((registers mmu_state) CTP)
  else if addr = 0x200 then ― ‹Context register›
    Some ((registers mmu_state) CNR)
  else if addr = 0x300 then ― ‹Fault status register›
    Some ((registers mmu_state) FTSR)
  else if addr = 0x400 then ― ‹Fault address register›
    Some ((registers mmu_state) FAR)
  else None"

definition mmu_reg_mod:: "MMU_state  virtua_address  machine_word 
  MMU_state option" where
"mmu_reg_mod mmu_state addr w 
  if addr = 0x000 then ― ‹MMU control register›
    Some (mmu_stateregisters := (registers mmu_state)(CR := w))
  else if addr = 0x100 then ― ‹Context pointer register›
    Some (mmu_stateregisters := (registers mmu_state)(CTP := w))
  else if addr = 0x200 then ― ‹Context register›
    Some (mmu_stateregisters := (registers mmu_state)(CNR := w))
  else if addr = 0x300 then ― ‹Fault status register›
    Some (mmu_stateregisters := (registers mmu_state)(FTSR := w))
  else if addr = 0x400 then ― ‹Fault address register›
    Some (mmu_stateregisters := (registers mmu_state)(FAR := w))
  else None"

section ‹Virtual Memory›

subsection ‹MMU Auxiliary Definitions›

definition getCTPVal:: "MMU_state  machine_word"
where "getCTPVal mmu   (registers mmu) CTP"

definition getCNRVal::"MMU_state  machine_word"
where "getCNRVal mmu   (registers mmu) CNR"


text‹
 The physical context table address is got from the ConText Pointer register (CTP) and the 
Context Register (CNR) MMU registers. 
 The CTP is shifted to align it with 
the physical address (36 bits) and we add the table index given on CNR.
CTP is right shifted 2 bits, cast to phys address and left shifted 6 bytes 
to be aligned with the context register.  
CNR is 2 bits left shifted for alignment with the context table.
›

definition compose_context_table_addr :: "machine_word machine_word 
                                           phys_address"
where 
 "compose_context_table_addr ctp cnr 
     ((ucast (ctp >> 2)) << 6) + (ucast cnr << 2)"

subsection ‹Virtual Address Translation›

text‹Get the context table phys address from the MMU registers›
definition get_context_table_addr :: "MMU_state  phys_address"
where 
 "get_context_table_addr mmu 
      compose_context_table_addr (getCTPVal mmu) (getCNRVal mmu)"

definition va_list_index :: "nat list" where
"va_list_index  [va_t1_index,va_t2_index,va_t3_index,0]"

definition offset_index :: "nat list" where
"offset_index 
   [ length_machine_word
    , length_machine_word-length_t1
    , length_machine_word-length_t1-length_t2
    , length_machine_word-length_t1-length_t2-length_t3
    ]"

definition index_len_table :: "nat list" where "index_len_table  [8,6,6,0]"

definition n_context_tables :: "nat" where "n_context_tables  3"

text ‹The following are basic physical memory read functions. 
At this level we don't need the write memory yet.›

definition mem_context_val:: "asi_type  phys_address  
                      mem_context  mem_val_type option"
where
"mem_context_val asi add m  
  let asi8 = word_of_int 8;
      r1 = m asi add 
  in
  if r1 = None then
    m asi8 add
  else r1
"

text ‹Given an ASI (word8), an address (word32) addr, 
        read the 32bit value from the memory addresses 
        starting from address addr' where addr' = addr 
        exception that the last two bits are 0's. 
        That is, read the data from 
        addr', addr'+1, addr'+2, addr'+3.›
definition mem_context_val_w32 :: "asi_type  phys_address  
                           mem_context  word32 option"
where
"mem_context_val_w32 asi addr m 
  let addr' = (AND) addr 0b111111111111111111111111111111111100;
      addr0 = (OR) addr' 0b000000000000000000000000000000000000;
      addr1 = (OR) addr' 0b000000000000000000000000000000000001;
      addr2 = (OR) addr' 0b000000000000000000000000000000000010;
      addr3 = (OR) addr' 0b000000000000000000000000000000000011;
      r0 = mem_context_val asi addr0 m;
      r1 = mem_context_val asi addr1 m;
      r2 = mem_context_val asi addr2 m;
      r3 = mem_context_val asi addr3 m
  in
  if r0 = None  r1 = None  r2 = None  r3 = None then
    None
  else
    let byte0 = case r0 of Some v  v;
        byte1 = case r1 of Some v  v;
        byte2 = case r2 of Some v  v;
        byte3 = case r3 of Some v  v 
    in
    Some ((OR) ((OR) ((OR) ((ucast(byte0)) << 24) 
                              ((ucast(byte1)) << 16)) 
                       ((ucast(byte2)) << 8)) 
                (ucast(byte3)))
"

text @{term "get_addr_from_table"} browses the page description tables  
  until it finds a PTE (bits==suc (suc 0).

  If it is a PTE it aligns the 24 most significant bits of the entry
  with the most significant bits of the phys address and or-ed with the offset,
   which will vary depending on the entry level. 
 In the case we are looking at the last table level (level 3),
   the offset is aligned to 0 otherwise it will be 2.
  
 If the table entry is a PTD (bits== Suc 0),
  the index is obtained from the virtual address depending on the current level and or-ed with the PTD. 
›

function ptd_lookup:: "virtua_address  virtua_address 
mem_context  nat  (phys_address × PTE_flags) option" 
where "ptd_lookup va pt m lvl = (
  if lvl > 3 then None
  else 
    let thislvl_offset = (
      if lvl = 1 then (ucast ((ucast (va >> 24))::word8))::word32
      else if lvl = 2 then (ucast ((ucast (va >> 18))::word6))::word32
      else (ucast ((ucast (va >> 12))::word6))::word32);
        thislvl_addr = (OR) pt thislvl_offset;
        thislvl_data = mem_context_val_w32 (word_of_int 9) (ucast thislvl_addr) m
    in
    case thislvl_data of 
    Some v  (
      let et_val = (AND) v 0b00000000000000000000000000000011 in
      if et_val = 0 then ― ‹Invalid›
        None
      else if et_val = 1 then ― ‹Page Table Descriptor›
        let ptp = (AND) v 0b11111111111111111111111111111100 in
        ptd_lookup va ptp m (lvl+1)
      else if et_val = 2 then ― ‹Page Table Entry›
        let ppn = (ucast (v >> 8))::word24;
            va_offset = (ucast ((ucast va)::word12))::word36
        in
        Some (((OR) (((ucast ppn)::word36) << 12) va_offset), 
              ((ucast v)::word8))
      else ― ‹et_val = 3›, reserved.›
        None
    )
    |None  None)
"
by pat_completeness auto
termination  
by (relation "measure (λ (va, (pt, (m, lvl))). 4 - lvl)") auto

definition get_acc_flag:: "PTE_flags  word3" where
"get_acc_flag w8  (ucast (w8 >> 2))::word3"

definition mmu_readable:: "word3  asi_type  bool" where
"mmu_readable f asi 
  if uint asi  {8, 10} then
    if uint f  {0,1,2,3,5} then True
    else False
  else if uint asi  {9, 11} then
    if uint f  {0,1,2,3,5,6,7} then True
    else False
  else False
"

definition mmu_writable:: "word3  asi_type  bool" where
"mmu_writable f asi 
  if uint asi  {8, 10} then
    if uint f  {1,3} then True
    else False
  else if uint asi  {9, 11} then
    if uint f  {1,3,5,7} then True
    else False
  else False
"

definition virt_to_phys :: "virtua_address  MMU_state   mem_context  
                            (phys_address × PTE_flags) option"
where 
 "virt_to_phys va mmu m  
    let ctp_val = mmu_reg_val mmu (0x100);
        cnr_val = mmu_reg_val mmu (0x200);
        mmu_cr_val = (registers mmu) CR
    in
    if (AND) mmu_cr_val 1  0 then ― ‹MMU enabled.›
      case (ctp_val,cnr_val) of
      (Some v1, Some v2) 
        let context_table_entry = (OR) ((v1 >> 11) << 11)
            (((AND) v2 0b00000000000000000000000111111111) << 2);
            context_table_data = mem_context_val_w32 (word_of_int 9) 
              (ucast context_table_entry) m
        in (
        case context_table_data of
        Some lvl1_page_table 
          ptd_lookup va lvl1_page_table m 1
        |None  None)
      |_  None
    else Some ((ucast va), ((0b11101111)::word8)) 
"

text ‹
\newpage

The below function gives the initial values of MMU registers.
In particular, the MMU context register CR is 0 because:
We don't know the bits for IMPL, VER, and SC;
the bits for PSO are 0s because we use TSO;
the reserved bits are 0s;
we assume NF bits are 0s;
and most importantly, the E bit is 0 because when the machine 
starts up, MMU is disabled. 
An initial boot procedure (bootloader or something like that) should 
configure the MMU and then enable it if the OS uses MMU.›

definition MMU_registers_init :: "MMU_context"
where "MMU_registers_init r  0" 

definition mmu_setup :: "MMU_state"
where "mmu_setup  registers=MMU_registers_init"

end

Theory Sparc_State

(*
 * Copyright 2016, NTU
 *
 * This software may be distributed and modified according to the terms of
 * the BSD 2-Clause license. Note that NO WARRANTY is provided.
 * See "LICENSE_BSD2.txt" for details.
 *
 * Author: Zhe Hou, David Sanan.
 *)

section ‹SPARC V8 state model›
theory Sparc_State
imports Main Sparc_Types  "../lib/wp/DetMonadLemmas" MMU
begin                                                                    
section ‹state as a function›

record cpu_cache = 
dcache:: cache_context
icache:: cache_context

text‹
The state @{term sparc_state} is defined as a tuple @{term cpu_context}, 
@{term user_context}, @{term mem_context}, defining the state of the CPU registers, 
user registers, memory, cache, and delayed write pool respectively. 
Additionally, a boolean indicates whether the state is 
undefined or not.
›

record (overloaded) ('a) sparc_state =
cpu_reg:: cpu_context
user_reg:: "('a) user_context"
sys_reg:: sys_context
mem:: mem_context
mmu:: MMU_state
cache:: cpu_cache
dwrite:: delayed_write_pool
state_var:: sparc_state_var
traps:: "Trap set"
undef:: bool

section‹functions for state member access›

definition cpu_reg_val:: "CPU_register  ('a) sparc_state  reg_type"
where
"cpu_reg_val reg state  (cpu_reg state) reg"

definition cpu_reg_mod :: "word32  CPU_register  ('a) sparc_state  
                           ('a) sparc_state"
where "cpu_reg_mod data_w32 cpu state  
  statecpu_reg := ((cpu_reg state)(cpu := data_w32))"

text ‹r[0] = 0. Otherwise read the actual value.›
definition user_reg_val:: "('a) window_size  user_reg_type  ('a) sparc_state  reg_type"
where
"user_reg_val window ur state  
  if ur = 0 then 0
  else (user_reg state) window ur"

text ‹Write a global register. win should be initialised as NWINDOWS.›
fun (sequential) global_reg_mod :: "word32  nat  user_reg_type  
  ('a::len) sparc_state  ('a) sparc_state"
where
"global_reg_mod data_w32 0 ur state = state"
|
"global_reg_mod data_w32 win ur state = (
    let win_word = word_of_int (int (win-1));
        ns = stateuser_reg := 
          (user_reg state)(win_word := ((user_reg state) win_word)(ur := data_w32)) 
    in
    global_reg_mod data_w32 (win-1) ur ns
)"

text ‹Compute the next window.›
definition next_window :: "('a::len) window_size  ('a) window_size"
where
"next_window win 
  if (uint win) < (NWINDOWS - 1) then (win + 1)
  else 0
"

text ‹Compute the previous window.›
definition pre_window :: "('a::len) window_size  ('a::len) window_size"
where
"pre_window win 
  if (uint win) > 0 then (win - 1)
  else (word_of_int (NWINDOWS - 1))
"

text ‹write an output register. 
  Also write ur+16 of the previous window.›
definition out_reg_mod :: "word32  ('a::len) window_size  user_reg_type  
  ('a) sparc_state  ('a) sparc_state"
where
"out_reg_mod data_w32 win ur state 
  let state' = stateuser_reg :=
        (user_reg state)(win := ((user_reg state) win)(ur := data_w32));
      win' = pre_window win;
      ur' = ur + 16
  in
  state'user_reg := 
    (user_reg state')(win' := ((user_reg state') win')(ur' := data_w32))
"

text ‹Write a input register.
  Also write ur-16 of the next window.›
definition in_reg_mod :: "word32  ('a::len) window_size  user_reg_type 
  ('a) sparc_state  ('a) sparc_state"
where
"in_reg_mod data_w32 win ur state 
  let state' = stateuser_reg :=
    (user_reg state)(win := ((user_reg state) win)(ur := data_w32));
      win' = next_window win;
      ur' = ur - 16
  in
  state'user_reg :=
    (user_reg state')(win' := ((user_reg state') win')(ur' := data_w32))
"

text ‹Do not modify r[0].›
definition user_reg_mod :: "word32  ('a::len) window_size  user_reg_type  
 ('a) sparc_state  ('a) sparc_state"
where
"user_reg_mod data_w32 win ur state 
  if ur = 0 then state
  else if 0 < ur  ur < 8 then
    global_reg_mod data_w32 (nat NWINDOWS) ur state
  else if 7 < ur  ur < 16 then 
    out_reg_mod data_w32 win ur state
  else if 15 < ur  ur < 24 then
    stateuser_reg := 
      (user_reg state)(win := ((user_reg state) win)(ur := data_w32))
  else ⌦‹if 23 < ur ∧ ur < 32 then›
    in_reg_mod data_w32 win ur state
  ⌦‹else state›
"

definition sys_reg_val :: "sys_reg  ('a) sparc_state  reg_type"
where
"sys_reg_val reg state  (sys_reg state) reg"

definition sys_reg_mod :: "word32  sys_reg  
                          ('a) sparc_state  ('a) sparc_state"
where
"sys_reg_mod data_w32 sys state  statesys_reg := (sys_reg state)(sys := data_w32)"

text ‹The following fucntions deal with physical memory. 
N.B. Physical memory address in SPARCv8 is 36-bit.›

text ‹LEON3 doesn't distinguish ASI 8 and 9; 10 and 11 for read access
  for both user and supervisor. 
We recently discovered that the compiled machine code by
the sparc-elf compiler often reads asi = 10 (user data) 
when the actual content is store in asi = 8 (user instruction).
For testing purposes, we don't distinguish asi = 8,9,10,11
for reading access.›

definition mem_val:: "asi_type  phys_address  
                      ('a) sparc_state  mem_val_type option"
where
"mem_val asi add state  
  let asi8 = word_of_int 8;
      asi9 = word_of_int 9;
      asi10 = word_of_int 10;
      asi11 = word_of_int 11;
      r1 = (mem state) asi8 add
  in
  if r1 = None then
    let r2 = (mem state) asi9 add in
    if r2 = None then
      let r3 = (mem state) asi10 add in
      if r3 = None then 
        (mem state) asi11 add
      else r3
    else r2
  else r1
"

text ‹An alternative way to read values from memory. 
Some implementations may use this definition.›

definition mem_val_alt:: "asi_type  phys_address  
                      ('a) sparc_state  mem_val_type option"
where
"mem_val_alt asi add state  
  let r1 = (mem state) asi add; 
      asi8 = word_of_int 8;
      asi9 = word_of_int 9;
      asi10 = word_of_int 10;
      asi11 = word_of_int 11
  in
  if r1 = None  (uint asi) = 8 then
    let r2 = (mem state) asi9 add in
    r2
  else if r1 = None  (uint asi) = 9 then
    let r2 = (mem state) asi8 add in
    r2
  else if r1 = None  (uint asi) = 10 then
    let r2 = (mem state) asi11 add in
    if r2 = None then
      let r3 = (mem state) asi8 add in
      if r3 = None then
        (mem state) asi9 add        
      else r3
    else r2
  else if r1 = None  (uint asi) = 11 then
    let r2 = (mem state) asi10 add in
    if r2 = None then
      let r3 = (mem state) asi8 add in
      if r3 = None then
        (mem state) asi9 add        
      else r3
    else r2
  else r1"

definition mem_mod :: "asi_type  phys_address  mem_val_type  
                         ('a) sparc_state  ('a) sparc_state"
where
"mem_mod asi addr val state 
  let state1 = statemem := (mem state)
    (asi := ((mem state) asi)(addr := Some val))
  in ― ‹Only allow one of asi› 8 and 9 (10 and 11) to have value.›
  if (uint asi) = 8  (uint asi) = 10 then
    let asi2 = word_of_int ((uint asi) + 1) in
    state1mem := (mem state1)
      (asi2 := ((mem state1) asi2)(addr := None))
  else if (uint asi) = 9  (uint asi) = 11 then
    let asi2 = word_of_int ((uint asi) - 1) in
    state1mem := (mem state1)(asi2 := ((mem state1) asi2)(addr := None))
  else state1
"

text ‹An alternative way to write memory. This method insists that 
for each address, it can only hold a value in one of ASI = 8,9,10,11.›

definition mem_mod_alt :: "asi_type  phys_address  mem_val_type  
                         ('a) sparc_state  ('a) sparc_state"
where
"mem_mod_alt asi addr val state 
  let state1 = statemem := (mem state)
    (asi := ((mem state) asi)(addr := Some val));
    asi8 = word_of_int 8;
    asi9 = word_of_int 9;
    asi10 = word_of_int 10;
    asi11 = word_of_int 11
  in 
  ― ‹Only allow one of asi› 8, 9, 10, 11 to have value.›
  if (uint asi) = 8 then 
    let state2 = state1mem := (mem state1)
      (asi9 := ((mem state1) asi9)(addr := None));
     state3 = state2mem := (mem state2)
      (asi10 := ((mem state2) asi10)(addr := None));
     state4 = state3mem := (mem state3)
      (asi11 := ((mem state3) asi11)(addr := None))
    in
    state4
  else if (uint asi) = 9 then 
    let state2 = state1mem := (mem state1)
      (asi8 := ((mem state1) asi8)(addr := None));  
     state3 = state2mem := (mem state2)
      (asi10 := ((mem state2) asi10)(addr := None));
     state4 = state3mem := (mem state3)
      (asi11 := ((mem state3) asi11)(addr := None))
    in
    state4  
  else if (uint asi) = 10 then 
    let state2 = state1mem := (mem state1)
      (asi9 := ((mem state1) asi9)(addr := None));
     state3 = state2mem := (mem state2)
      (asi8 := ((mem state2) asi8)(addr := None));
     state4 = state3mem := (mem state3)
      (asi11 := ((mem state3) asi11)(addr := None))
    in
    state4
  else if (uint asi) = 11 then 
    let state2 = state1mem := (mem state1)
      (asi9 := ((mem state1) asi9)(addr := None));
     state3 = state2mem := (mem state2)
      (asi10 := ((mem state2) asi10)(addr := None));
     state4 = state3mem := (mem state3)
      (asi8 := ((mem state3) asi8)(addr := None))
    in
    state4
  else state1
"

text ‹Given an ASI (word8), an address (word32) addr, 
        read the 32bit value from the memory addresses 
        starting from address addr' where addr' = addr 
        exception that the last two bits are 0's. 
        That is, read the data from 
        addr', addr'+1, addr'+2, addr'+3.›
definition mem_val_w32 :: "asi_type  phys_address  
                           ('a) sparc_state  word32 option"
where
"mem_val_w32 asi addr state 
  let addr' = (AND) addr 0b111111111111111111111111111111111100;
      addr0 = addr';
      addr1 = addr' + 1;
      addr2 = addr' + 2;
      addr3 = addr' + 3;
      r0 = mem_val_alt asi addr0 state;
      r1 = mem_val_alt asi addr1 state;
      r2 = mem_val_alt asi addr2 state;
      r3 = mem_val_alt asi addr3 state
  in
  if r0 = None  r1 = None  r2 = None  r3 = None then
    None
  else
    let byte0 = case r0 of Some v  v;
        byte1 = case r1 of Some v  v;
        byte2 = case r2 of Some v  v;
        byte3 = case r3 of Some v  v 
    in
    Some ((OR) ((OR) ((OR) ((ucast(byte0)) << 24) 
                              ((ucast(byte1)) << 16)) 
                       ((ucast(byte2)) << 8)) 
                (ucast(byte3)))
"

text ‹
  Let addr'› be addr› with last two bits set to 0's.
  Write the 32bit data in the memory address addr'›
  (and the following 3 addresses). 
  byte_mask› decides which byte of the 32bits are written.
›
definition mem_mod_w32 :: "asi_type  phys_address  word4  word32  
                           ('a) sparc_state  ('a) sparc_state"
where
"mem_mod_w32 asi addr byte_mask data_w32 state 
  let addr' = (AND) addr 0b111111111111111111111111111111111100;
      addr0 = (OR) addr' 0b000000000000000000000000000000000000;
      addr1 = (OR) addr' 0b000000000000000000000000000000000001;
      addr2 = (OR) addr' 0b000000000000000000000000000000000010;
      addr3 = (OR) addr' 0b000000000000000000000000000000000011;
      byte0 = (ucast (data_w32 >> 24))::mem_val_type;
      byte1 = (ucast (data_w32 >> 16))::mem_val_type;
      byte2 = (ucast (data_w32 >> 8))::mem_val_type;
      byte3 = (ucast data_w32)::mem_val_type;
      s0 = if (((AND) byte_mask (0b1000::word4)) >> 3) = 1 then
              mem_mod asi addr0 byte0 state 
           else state;
      s1 = if (((AND) byte_mask (0b0100::word4)) >> 2) = 1 then
              mem_mod asi addr1 byte1 s0 
           else s0;
      s2 = if (((AND) byte_mask (0b0010::word4)) >> 1) = 1 then
              mem_mod asi addr2 byte2 s1 
           else s1;
      s3 = if ((AND) byte_mask (0b0001::word4)) = 1 then
              mem_mod asi addr3 byte3 s2 
           else s2
  in
  s3
"

text ‹The following functions deal with virtual addresses. 
These are based on functions written by David Sanan.›

definition load_word_mem :: "('a) sparc_state  virtua_address  asi_type  
                             machine_word option"
where "load_word_mem state va asi  
let pair = (virt_to_phys va (mmu state) (mem state)) in 
case pair of
  Some pair  ( 
    if mmu_readable (get_acc_flag (snd pair)) asi then 
      (mem_val_w32 asi (fst pair) state)
    else None)
  | None  None"

definition store_word_mem ::"('a) sparc_state  virtua_address  machine_word  
                             word4  asi_type  ('a) sparc_state option"
where "store_word_mem state va wd byte_mask asi  
let pair = (virt_to_phys va (mmu state) (mem state)) in 
case pair of
  Some pair  ( 
    if mmu_writable (get_acc_flag (snd pair)) asi then 
      Some (mem_mod_w32 asi (fst pair) byte_mask wd state)
    else None)
  | None  None"

definition icache_val:: "cache_type  ('a) sparc_state  mem_val_type option"
where "icache_val c state  icache (cache state) c"

definition dcache_val:: "cache_type  ('a) sparc_state  mem_val_type option"
where "dcache_val c state  dcache (cache state) c"

definition icache_mod :: "cache_type  mem_val_type  
                           ('a) sparc_state  ('a) sparc_state"
where "icache_mod c val state  
  statecache := ((cache state)
    icache := (icache (cache state))(c := Some val))
"

definition dcache_mod :: "cache_type  mem_val_type  
                           ('a) sparc_state  ('a) sparc_state"
where "dcache_mod c val state  
  statecache := ((cache state)
    dcache := (dcache (cache state))(c := Some val))
"

text ‹Check if the memory address is in the cache or not.›
definition icache_miss :: "virtua_address  ('a) sparc_state  bool"
where
"icache_miss addr state 
  let line_len = 12;
      tag = (ucast (addr >> line_len))::cache_tag;
      line = (ucast (0b0::word1))::cache_line_size 
  in
  if (icache_val (tag,line) state) = None then True 
  else False    
"

text ‹Check if the memory address is in the cache or not.›
definition dcache_miss :: "virtua_address  ('a) sparc_state  bool"
where
"dcache_miss addr state 
  let line_len = 12;
      tag = (ucast (addr >> line_len))::cache_tag;
      line = (ucast (0b0::word1))::cache_line_size 
  in
  if (dcache_val (tag,line) state) = None then True 
  else False    
"

definition read_data_cache:: "('a) sparc_state  virtua_address  machine_word option"
where "read_data_cache state va 
  let tag = (ucast (va >> 12))::word20;
       offset0 = (AND) ((ucast va)::word12) 0b111111111100;
       offset1 = (OR) offset0 0b000000000001;
       offset2 = (OR) offset0 0b000000000010;
       offset3 = (OR) offset0 0b000000000011;
       r0 = dcache_val (tag,offset0) state;
       r1 = dcache_val (tag,offset1) state;
       r2 = dcache_val (tag,offset2) state;
       r3 = dcache_val (tag,offset3) state
  in
  if r0 = None  r1 = None  r2 = None  r3 = None then
    None
  else
    let byte0 = case r0 of Some v  v;
        byte1 = case r1 of Some v  v;
        byte2 = case r2 of Some v  v;
        byte3 = case r3 of Some v  v 
    in
    Some ((OR) ((OR) ((OR) ((ucast(byte0)) << 24) 
                              ((ucast(byte1)) << 16)) 
                       ((ucast(byte2)) << 8)) 
                (ucast(byte3)))
"

definition read_instr_cache:: "('a) sparc_state  virtua_address  machine_word option"
where "read_instr_cache state va 
  let tag = (ucast (va >> 12))::word20;
       offset0 = (AND) ((ucast va)::word12) 0b111111111100;
       offset1 = (OR) offset0 0b000000000001;
       offset2 = (OR) offset0 0b000000000010;
       offset3 = (OR) offset0 0b000000000011;
       r0 = icache_val (tag,offset0) state;
       r1 = icache_val (tag,offset1) state;
       r2 = icache_val (tag,offset2) state;
       r3 = icache_val (tag,offset3) state
  in
  if r0 = None  r1 = None  r2 = None  r3 = None then
    None
  else
    let byte0 = case r0 of Some v  v;
        byte1 = case r1 of Some v  v;
        byte2 = case r2 of Some v  v;
        byte3 = case r3 of Some v  v 
    in
    Some ((OR) ((OR) ((OR) ((ucast(byte0)) << 24) 
                              ((ucast(byte1)) << 16)) 
                       ((ucast(byte2)) << 8)) 
                (ucast(byte3)))
"

definition add_data_cache :: "('a) sparc_state  virtua_address  machine_word  
  word4  ('a) sparc_state"
where 
 "add_data_cache state va word byte_mask  
   let tag = (ucast (va >> 12))::word20;
       offset0 = (AND) ((ucast va)::word12) 0b111111111100;
       offset1 = (OR) offset0 0b000000000001;
       offset2 = (OR) offset0 0b000000000010;
       offset3 = (OR) offset0 0b000000000011;
       byte0 = (ucast (word >> 24))::mem_val_type;
       byte1 = (ucast (word >> 16))::mem_val_type;
       byte2 = (ucast (word >> 8))::mem_val_type;
       byte3 = (ucast word)::mem_val_type;
       s0 = if (((AND) byte_mask (0b1000::word4)) >> 3) = 1 then
              dcache_mod (tag,offset0) byte0 state
            else state;
       s1 = if (((AND) byte_mask (0b0100::word4)) >> 2) = 1 then
              dcache_mod (tag,offset1) byte1 s0
            else s0;
       s2 = if (((AND) byte_mask (0b0010::word4)) >> 1) = 1 then
              dcache_mod (tag,offset2) byte2 s1
            else s1;
       s3 = if ((AND) byte_mask (0b0001::word4)) = 1 then
              dcache_mod (tag,offset3) byte3 s2
            else s2
   in s3
"

definition add_instr_cache :: "('a) sparc_state  virtua_address  machine_word  
  word4  ('a) sparc_state"
where 
 "add_instr_cache state va word byte_mask  
   let tag = (ucast (va >> 12))::word20;
       offset0 = (AND) ((ucast va)::word12) 0b111111111100;
       offset1 = (OR) offset0 0b000000000001;
       offset2 = (OR) offset0 0b000000000010;
       offset3 = (OR) offset0 0b000000000011;
       byte0 = (ucast (word >> 24))::mem_val_type;
       byte1 = (ucast (word >> 16))::mem_val_type;
       byte2 = (ucast (word >> 8))::mem_val_type;
       byte3 = (ucast word)::mem_val_type;
       s0 = if (((AND) byte_mask (0b1000::word4)) >> 3) = 1 then
              icache_mod (tag,offset0) byte0 state
            else state;
       s1 = if (((AND) byte_mask (0b0100::word4)) >> 2) = 1 then
              icache_mod (tag,offset1) byte1 s0
            else s0;
       s2 = if (((AND) byte_mask (0b0010::word4)) >> 1) = 1 then
              icache_mod (tag,offset2) byte2 s1
            else s1;
       s3 = if ((AND) byte_mask (0b0001::word4)) = 1 then
              icache_mod (tag,offset3) byte3 s2
            else s2
   in s3
"

definition empty_cache ::"cache_context" where "empty_cache c  None"

definition flush_data_cache:: "('a) sparc_state  ('a) sparc_state" where
"flush_data_cache state  statecache := ((cache state)dcache := empty_cache)"

definition flush_instr_cache:: "('a) sparc_state  ('a) sparc_state" where
"flush_instr_cache state  statecache := ((cache state)icache := empty_cache)"

definition flush_cache_all:: "('a) sparc_state  ('a) sparc_state" where
"flush_cache_all state  statecache := ((cache state)
  icache := empty_cache, dcache := empty_cache)"

text ‹Check if the FI or FD bit of CCR is 1. 
If FI is 1 then flush instruction cache. 
If FD is 1 then flush data cache.›
definition ccr_flush :: "('a) sparc_state  ('a) sparc_state"
where
"ccr_flush state 
  let ccr_val = sys_reg_val CCR state;
      ― ‹FI› is bit 21 of CCR›
      fi_val = ((AND) ccr_val (0b00000000001000000000000000000000)) >> 21;
      fd_val = ((AND) ccr_val (0b00000000010000000000000000000000)) >> 22;
      state1 = (if fi_val = 1 then flush_instr_cache state else state)
  in
  if fd_val = 1 then flush_data_cache state1 else state1"

definition get_delayed_pool :: "('a) sparc_state  delayed_write_pool"
where "get_delayed_pool state  dwrite state"

definition exe_pool :: "(int × reg_type × CPU_register)  (int × reg_type × CPU_register)"
where "exe_pool w  case w of (n,v,c)  ((n-1),v,c)"

text ‹Minus 1 to the delayed count for all the members in the set. 
        Assuming all members have delay > 0.›
primrec delayed_pool_minus :: "delayed_write_pool  delayed_write_pool"
where
"delayed_pool_minus [] = []"
|
"delayed_pool_minus (x#xs) = (exe_pool x)#(delayed_pool_minus xs)"

text ‹Add a delayed-write to the pool.›
definition delayed_pool_add :: "(int × reg_type × CPU_register)  
                                ('a) sparc_state  ('a) sparc_state"
where 
"delayed_pool_add dw s 
  let (i,v,cr) = dw in
  if i = 0 then ― ‹Write the value to the register immediately.›
    cpu_reg_mod v cr s
  else ― ‹Add to delayed write pool.›
    let curr_pool = get_delayed_pool s in
    sdwrite := curr_pool@[dw]"

text ‹Remove a delayed-write from the pool. 
        Assume that the delayed-write to be removed has delay 0.
        i.e., it has been executed.›
definition delayed_pool_rm :: "(int × reg_type × CPU_register)  
                               ('a) sparc_state  ('a) sparc_state"
where
"delayed_pool_rm dw s 
  let curr_pool = get_delayed_pool s in
  case dw of (n,v,cr)  
    (if n = 0 then
      sdwrite := List.remove1 dw curr_pool
     else s)
"

text ‹Remove all the entries with delay = 0, i.e., those that are written.›
primrec delayed_pool_rm_written :: "delayed_write_pool  delayed_write_pool"
where
"delayed_pool_rm_written [] = []"
|
"delayed_pool_rm_written (x#xs) = 
  (if fst x = 0 then delayed_pool_rm_written xs else x#(delayed_pool_rm_written xs))    
"

definition annul_val :: "('a) sparc_state  bool"
where "annul_val state  get_annul (state_var state)"

definition annul_mod :: "bool  ('a) sparc_state  ('a) sparc_state"
where "annul_mod b s  sstate_var := write_annul b (state_var s)"

definition reset_trap_val :: "('a) sparc_state  bool"
where "reset_trap_val state  get_reset_trap (state_var state)"

definition reset_trap_mod :: "bool  ('a) sparc_state  ('a) sparc_state"
where "reset_trap_mod b s  sstate_var := write_reset_trap b (state_var s)"

definition exe_mode_val :: "('a) sparc_state  bool"
where "exe_mode_val state  get_exe_mode (state_var state)"

definition exe_mode_mod :: "bool  ('a) sparc_state  ('a) sparc_state"
where "exe_mode_mod b s  sstate_var := write_exe_mode b (state_var s)"

definition reset_mode_val :: "('a) sparc_state  bool"
where "reset_mode_val state  get_reset_mode (state_var state)"

definition reset_mode_mod :: "bool  ('a) sparc_state  ('a) sparc_state"
where "reset_mode_mod b s  sstate_var := write_reset_mode b (state_var s)"

definition err_mode_val :: "('a) sparc_state  bool"
where "err_mode_val state  get_err_mode (state_var state)"

definition err_mode_mod :: "bool  ('a) sparc_state  ('a) sparc_state"
where "err_mode_mod b s  sstate_var := write_err_mode b (state_var s)"

definition ticc_trap_type_val :: "('a) sparc_state  word7"
where "ticc_trap_type_val state  get_ticc_trap_type (state_var state)"

definition ticc_trap_type_mod :: "word7  ('a) sparc_state  ('a) sparc_state"
where "ticc_trap_type_mod w s  sstate_var := write_ticc_trap_type w (state_var s)"

definition interrupt_level_val :: "('a) sparc_state  word3"
where "interrupt_level_val state  get_interrupt_level (state_var state)"

definition interrupt_level_mod :: "word3  ('a) sparc_state  ('a) sparc_state"
where "interrupt_level_mod w s  sstate_var := write_interrupt_level w (state_var s)"

definition store_barrier_pending_val :: "('a) sparc_state  bool"
where "store_barrier_pending_val state  
  get_store_barrier_pending (state_var state)"

definition store_barrier_pending_mod :: "bool  
  ('a) sparc_state  ('a) sparc_state"
where "store_barrier_pending_mod w s 
  sstate_var := write_store_barrier_pending w (state_var s)"

definition pb_block_ldst_byte_val :: "virtua_address  ('a) sparc_state
   bool"
where "pb_block_ldst_byte_val add state 
  (atm_ldst_byte (state_var state)) add"

definition pb_block_ldst_byte_mod :: "virtua_address  bool  
  ('a) sparc_state  ('a) sparc_state"
where "pb_block_ldst_byte_mod add b s 
  sstate_var := ((state_var s)
    atm_ldst_byte := (atm_ldst_byte (state_var s))(add := b))"

text ‹We only read the address such that add mod 4 = 0. 
  add mod 4 represents the current word.›
definition pb_block_ldst_word_val :: "virtua_address  ('a) sparc_state
   bool"
where "pb_block_ldst_word_val add state 
  let add0 = ((AND) add (0b11111111111111111111111111111100::word32)) in
  (atm_ldst_word (state_var state)) add0"

text ‹We only write the address such that add mod 4 = 0.
  add mod 4 represents the current word.›
definition pb_block_ldst_word_mod :: "virtua_address  bool  
  ('a) sparc_state  ('a) sparc_state"
where "pb_block_ldst_word_mod add b s 
  let add0 = ((AND) add (0b11111111111111111111111111111100::word32)) in
  sstate_var := ((state_var s)
    atm_ldst_word := (atm_ldst_word (state_var s))(add0 := b))"

definition get_trap_set :: "('a) sparc_state  Trap set"
where "get_trap_set state  (traps state)"

definition add_trap_set :: "Trap  ('a) sparc_state  ('a) sparc_state"
where "add_trap_set t s  straps := (traps s)  {t}"

definition emp_trap_set :: "('a) sparc_state  ('a) sparc_state"
where "emp_trap_set s  straps := {}"

definition state_undef:: "('a) sparc_state  bool"
where "state_undef state  (undef state)"

text ‹The memory_read› interface that conforms with the SPARCv8 manual.›
definition memory_read :: "asi_type  virtua_address  
                           ('a) sparc_state  
                           ((word32 option) × ('a) sparc_state)"
where "memory_read asi addr state 
  let asi_int = uint asi in ― ‹See Page 25 and 35 for ASI usage in LEON 3FT.›
  if asi_int = 1 then ― ‹Forced cache miss.›
    ― ‹Directly read from memory.›
    let r1 = load_word_mem state addr (word_of_int 8) in
    if r1 = None then
      let r2 = load_word_mem state addr (word_of_int 10) in
      if r2 = None then
        (None,state)
      else (r2,state)
    else (r1,state)
  else if asi_int = 2 then ― ‹System registers.›
    ― ‹See Table 19, Page 34 for System Register address map in LEON 3FT.›
    if uint addr = 0 then ― ‹Cache control register.›
      ((Some (sys_reg_val CCR state)), state)
    else if uint addr = 8 then ― ‹Instruction cache configuration register.›
      ((Some (sys_reg_val ICCR state)), state)
    else if uint addr = 12 then ― ‹Data cache configuration register.›
      ((Some (sys_reg_val DCCR state)), state)
    else ― ‹Invalid address.›
      (None, state)
  else if asi_int  {8,9} then ― ‹Access instruction memory.›
    let ccr_val = (sys_reg state) CCR in
    if ccr_val AND 1  0 then ― ‹Cache is enabled. Update cache.›
    ― ‹We don't go through the tradition, i.e., read from cache first,›
    ― ‹if the address is not cached, then read from memory,›
    ― ‹because performance is not an issue here.›
    ― ‹Thus we directly read from memory and update the cache.›
      let data = load_word_mem state addr asi in
      case data of
      Some w  (Some w,(add_instr_cache state addr w (0b1111::word4)))
      |None  (None, state)
    else ― ‹Cache is disabled. Just read from memory.›
      ((load_word_mem state addr asi),state)
  else if asi_int  {10,11} then ― ‹Access data memory.›
    let ccr_val = (sys_reg state) CCR in
    if ccr_val AND 1  0 then ― ‹Cache is enabled. Update cache.›
    ― ‹We don't go through the tradition, i.e., read from cache first,›
    ― ‹if the address is not cached, then read from memory,›
    ― ‹because performance is not an issue here.›
    ― ‹Thus we directly read from memory and update the cache.›
      let data = load_word_mem state addr asi in
      case data of
      Some w  (Some w,(add_data_cache state addr w (0b1111::word4)))
      |None  (None, state)
    else ― ‹Cache is disabled. Just read from memory.›
      ((load_word_mem state addr asi),state)
  ― ‹We don't access instruction cache tag. i.e., asi = 12›.›
  else if asi_int = 13 then ― ‹Read instruction cache data.›
    let cache_result = read_instr_cache state addr in
    case cache_result of
    Some w  (Some w, state)
    |None  (None, state)
  ― ‹We don't access data cache tag. i.e., asi = 14›.›
  else if asi_int = 15 then ― ‹Read data cache data.›
    let cache_result = read_data_cache state addr in
    case cache_result of
    Some w  (Some w, state)
    |None  (None, state)
  else if asi_int  {16,17} then ― ‹Flush entire instruction/data cache.›
    (None, state) ― ‹Has no effect for memory read.›
  else if asi_int  {20,21} then ― ‹MMU diagnostic cache access.›
    (None, state) ― ‹Not considered in this model.›
  else if asi_int = 24 then ― ‹Flush cache and TLB in LEON3.›
    ― ‹But is not used for memory read.›
    (None, state)
  else if asi_int = 25 then ― ‹MMU registers.›
    ― ‹Treat MMU registers as memory addresses that are not in the main memory.›
    ((mmu_reg_val (mmu state) addr), state) 
  else if asi_int = 28 then ― ‹MMU bypass.›
    ― ‹Directly use addr as a physical address.›
    ― ‹Append 0000 in the front of addr.›
    ― ‹In this case, (ucast addr) suffices.›
    ((mem_val_w32 asi (ucast addr) state), state)
  else if asi_int = 29 then ― ‹MMU diagnostic access.›
    (None, state) ― ‹Not considered in this model.›
  else ― ‹Not considered in this model.›
    (None, state)
"

text ‹Get the value of a memory address and an ASI.›
definition mem_val_asi:: "asi_type  phys_address  
                      ('a) sparc_state  mem_val_type option"
where "mem_val_asi asi add state  (mem state) asi add"

text ‹Check if an address is used in ASI 9 or 11.›
definition sup_addr :: "phys_address  ('a) sparc_state  bool"
where
"sup_addr addr state 
  let addr' = (AND) addr 0b111111111111111111111111111111111100;
      addr0 = (OR) addr' 0b000000000000000000000000000000000000;
      addr1 = (OR) addr' 0b000000000000000000000000000000000001;
      addr2 = (OR) addr' 0b000000000000000000000000000000000010;
      addr3 = (OR) addr' 0b000000000000000000000000000000000011;
      r0 = mem_val_asi 9 addr0 state;
      r1 = mem_val_asi 9 addr1 state;
      r2 = mem_val_asi 9 addr2 state;
      r3 = mem_val_asi 9 addr3 state;
      r4 = mem_val_asi 11 addr0 state;
      r5 = mem_val_asi 11 addr1 state;
      r6 = mem_val_asi 11 addr2 state;
      r7 = mem_val_asi 11 addr3 state
  in
  if r0 = None  r1 = None  r2 = None  r3 = None 
     r4 = None  r5 = None  r6 = None  r7 = None
  then False
  else True
"

text ‹The memory_write› interface that conforms with SPARCv8 manual.›
text ‹LEON3 forbids user to write an address in ASI 9 and 11.›
definition memory_write_asi :: "asi_type  virtua_address  word4  word32  
                            ('a) sparc_state  
                            ('a) sparc_state option"
where
"memory_write_asi asi addr byte_mask data_w32 state  
  let asi_int = uint asi; ― ‹See Page 25 and 35 for ASI usage in LEON 3FT.›
      psr_val = cpu_reg_val PSR state;
      s_val = get_S psr_val
  in 
  if asi_int = 1 then ― ‹Forced cache miss.›
    ― ‹Directly write to memory.›
    ― ‹Assuming writing into asi = 10›.›
    store_word_mem state addr data_w32 byte_mask (word_of_int 10) 
  else if asi_int = 2 then ― ‹System registers.›
    ― ‹See Table 19, Page 34 for System Register address map in LEON 3FT.›
    if uint addr = 0 then ― ‹Cache control register.›
      let s1 = (sys_reg_mod data_w32 CCR state) in
      ― ‹Flush the instruction cache if FI of CCR is 1;›
      ― ‹flush the data cache if FD of CCR is 1.›
      Some (ccr_flush s1)
    else if uint addr = 8 then ― ‹Instruction cache configuration register.›
      Some (sys_reg_mod data_w32 ICCR state)
    else if uint addr = 12 then ― ‹Data cache configuration register.›
      Some (sys_reg_mod data_w32 DCCR state)
    else ― ‹Invalid address.›
      None
  else if asi_int  {8,9} then ― ‹Access instruction memory.›
    ― ‹Write to memory. LEON3 does write-through. Both cache and the memory are updated.›
    let ns = add_instr_cache state addr data_w32 byte_mask in
    store_word_mem ns addr data_w32 byte_mask asi
  else if asi_int  {10,11} then ― ‹Access data memory.›
    ― ‹Write to memory. LEON3 does write-through. Both cache and the memory are updated.›
    let ns = add_data_cache state addr data_w32 byte_mask in
    store_word_mem ns addr data_w32 byte_mask asi
  ― ‹We don't access instruction cache tag. i.e., asi = 12›.›
  else if asi_int = 13 then ― ‹Write instruction cache data.›
    Some (add_instr_cache state addr data_w32 (0b1111::word4))
  ― ‹We don't access data cache tag. i.e., asi = 14.›
  else if asi_int = 15 then ― ‹Write data cache data.›
    Some (add_data_cache state addr data_w32 (0b1111::word4))
  else if asi_int = 16 then ― ‹Flush instruction cache.›
    Some (flush_instr_cache state)
  else if asi_int = 17 then ― ‹Flush data cache.›
    Some (flush_data_cache state)
  else if asi_int  {20,21} then ― ‹MMU diagnostic cache access.›
    None ― ‹Not considered in this model.›
  else if asi_int = 24 then ― ‹Flush TLB and cache in LEON3.›
    ― ‹We don't consider TLB here.›
    Some (flush_cache_all state)
  else if asi_int = 25 then ― ‹MMU registers.›
    ― ‹Treat MMU registers as memory addresses that are not in the main memory.›
    let mmu_state' = mmu_reg_mod (mmu state) addr data_w32 in
    case mmu_state' of
    Some mmus  Some (statemmu := mmus)
    |None  None 
  else if asi_int = 28 then ― ‹MMU bypass.›
    ― ‹Write to virtual address as physical address.›
    ― ‹Append 0000 in front of addr.›
    Some (mem_mod_w32 asi (ucast addr) byte_mask data_w32 state)
  else if asi_int = 29 then ― ‹MMU diagnostic access.›
    None ― ‹Not considered in this model.›
  else ― ‹Not considered in this model.›
    None
"

definition memory_write :: "asi_type  virtua_address  word4  word32  
                            ('a) sparc_state  
                            ('a) sparc_state option"
where
"memory_write asi addr byte_mask data_w32 state  
  let result = memory_write_asi asi addr byte_mask data_w32 state in
  case result of 
  None  None
  | Some s1  Some (store_barrier_pending_mod False s1)"

text ‹monad for sequential operations over the register representation›
type_synonym ('a,'e) sparc_state_monad = "(('a) sparc_state,'e) det_monad" 

text ‹Given a word32 value, a cpu register, 
        write the value in the cpu register.›
definition write_cpu :: "word32  CPU_register  ('a,unit) sparc_state_monad"
where "write_cpu w cr 
  do
    modify (λs. (cpu_reg_mod w cr s));
    return ()
  od"

definition write_cpu_tt :: "word8  ('a,unit) sparc_state_monad"
where "write_cpu_tt w 
  do
    tbr_val  gets (λs. (cpu_reg_val TBR s));
    new_tbr_val  gets (λs. (write_tt w tbr_val));
    write_cpu new_tbr_val TBR;
    return ()
  od"

text ‹Given a word32 value, a word4 window, a user register, 
        write the value in the user register. 
        N.B. CWP is a 5 bit value, but we only use the last 4 bits,
        since there are only 16 windows.›
definition write_reg :: "word32  ('a::len) word  user_reg_type  
  ('a,unit) sparc_state_monad"
where "write_reg w win ur 
  do
    modify (λs.(user_reg_mod w win ur s));
    return ()
  od"

definition set_annul :: "bool  ('a,unit) sparc_state_monad"
where "set_annul b 
  do
    modify (λs. (annul_mod b s));
    return ()
  od"

definition set_reset_trap :: "bool  ('a,unit) sparc_state_monad"
where "set_reset_trap b 
  do
    modify (λs. (reset_trap_mod b s));
    return ()
  od"

definition set_exe_mode :: "bool  ('a,unit) sparc_state_monad"
where "set_exe_mode b 
  do
    modify (λs. (exe_mode_mod b s));
    return ()
  od"

definition set_reset_mode :: "bool  ('a,unit) sparc_state_monad"
where "set_reset_mode b 
  do
    modify (λs. (reset_mode_mod b s));
    return ()
  od" 

definition set_err_mode :: "bool  ('a,unit) sparc_state_monad"
where "set_err_mode b 
  do
    modify (λs. (err_mode_mod b s));
    return ()
  od"

fun get_delayed_0 :: "(int × reg_type × CPU_register) list  
  (int × reg_type × CPU_register) list"
where
"get_delayed_0 [] = []"
|
"get_delayed_0 (x # xs) = 
  (if fst x = 0 then x # (get_delayed_0 xs)
  else get_delayed_0 xs)"

text ‹Get a list of delayed-writes with delay 0.›
definition get_delayed_write :: "delayed_write_pool  (int × reg_type × CPU_register) list"
where
"get_delayed_write dwp  get_delayed_0 dwp"

definition delayed_write :: "(int × reg_type × CPU_register)  ('a) sparc_state 
  ('a) sparc_state"
where "delayed_write dw s 
  let (n,v,r) = dw in
  if n = 0 then
    cpu_reg_mod v r s
  else s"

primrec delayed_write_all :: "(int × reg_type × CPU_register) list 
  ('a) sparc_state  ('a) sparc_state"
where "delayed_write_all [] s = s"
|"delayed_write_all (x # xs) s =
  delayed_write_all xs (delayed_write x s)"

primrec delayed_pool_rm_list :: "(int × reg_type × CPU_register) list 
  ('a) sparc_state  ('a) sparc_state"
where "delayed_pool_rm_list [] s = s"
|"delayed_pool_rm_list (x # xs) s =
  delayed_pool_rm_list xs (delayed_pool_rm x s)"

definition delayed_pool_write :: "('a) sparc_state  ('a) sparc_state"
where "delayed_pool_write s 
  let dwp0 = get_delayed_pool s;
      dwp1 = delayed_pool_minus dwp0;
      wl = get_delayed_write dwp1;
      s1 = delayed_write_all wl s;
      s2 = delayed_pool_rm_list wl s1 
  in s2"

definition raise_trap :: "Trap  ('a,unit) sparc_state_monad"
where "raise_trap t 
  do
    modify (λs. (add_trap_set t s));
    return ()
  od"

end

Theory Sparc_Instruction

(*
 * Copyright 2016, NTU
 *
 * This software may be distributed and modified according to the terms of
 * the BSD 2-Clause license. Note that NO WARRANTY is provided.
 * See "LICENSE_BSD2.txt" for details.
 *
 * Author: Zhe Hou, David Sanan.
 *)

section ‹SPARC instruction model›
theory Sparc_Instruction
imports Main Sparc_Types Sparc_State "HOL-Eisbach.Eisbach_Tools"
begin
text‹
This theory provides a formal model for assembly instruction to be executed in the model.

An instruction is defined as a tuple composed of a @{term sparc_operation} element,
defining the operation the instruction carries out, and a list of operands 
@{term inst_operand}. @{term inst_operand} can be a user register @{term user_reg} 
or a memory address @{term mem_add_type}.
›
datatype inst_operand = 
W5 word5
|W30 word30
|W22 word22
|Cond  word4
|Flag word1
|Asi asi_type
|Simm13 word13 
|Opf word9
|Imm7 word7

primrec get_operand_w5::"inst_operand  word5"
where "get_operand_w5 (W5 r) = r"

primrec get_operand_w30::"inst_operand  word30"
where "get_operand_w30 (W30 r) = r"

primrec get_operand_w22::"inst_operand  word22"
where "get_operand_w22 (W22 r) = r"

primrec get_operand_cond::"inst_operand  word4"
where "get_operand_cond (Cond r) = r"

primrec get_operand_flag::"inst_operand  word1"
where "get_operand_flag (Flag r) = r"

primrec get_operand_asi::"inst_operand  asi_type"
where "get_operand_asi (Asi r) = r"

primrec get_operand_simm13::"inst_operand  word13"
where "get_operand_simm13 (Simm13 r) = r"

primrec get_operand_opf::"inst_operand  word9"
where "get_operand_opf (Opf r) = r"

primrec get_operand_imm7:: "inst_operand  word7"
where "get_operand_imm7 (Imm7 r) = r"

type_synonym instruction = "(sparc_operation × inst_operand list)"

definition get_op::"word32  int"
where "get_op w  uint (w >> 30)"

definition get_op2::"word32  int"
where "get_op2 w  
  let mask_op2 = 0b00000001110000000000000000000000 in
  uint (((AND) mask_op2 w) >> 22)"

definition get_op3::"word32  int"
where "get_op3 w  
  let mask_op3 = 0b00000001111110000000000000000000 in 
  uint (((AND) mask_op3 w) >> 19)"

definition get_disp30::"word32  int"
where "get_disp30 w  
  let mask_disp30 = 0b00111111111111111111111111111111 in
  uint ((AND) mask_disp30 w)"

definition get_a::"word32  int"
where "get_a w 
  let mask_a = 0b00100000000000000000000000000000 in
  uint (((AND) mask_a w) >> 29)"

definition get_cond::"word32  int"
where "get_cond w 
  let mask_cond = 0b00011110000000000000000000000000 in
  uint (((AND) mask_cond w) >> 25)"

definition get_disp_imm22::"word32  int"
where "get_disp_imm22 w 
  let mask_disp_imm22 = 0b00000000001111111111111111111111 in
  uint ((AND) mask_disp_imm22 w)"

definition get_rd::"word32  int"
where "get_rd w 
  let mask_rd = 0b00111110000000000000000000000000 in
  uint (((AND) mask_rd w) >> 25)"

definition get_rs1::"word32  int"
where "get_rs1 w 
  let mask_rs1 = 0b00000000000001111100000000000000 in
  uint (((AND) mask_rs1 w) >> 14)"

definition get_i::"word32  int"
where "get_i w 
  let mask_i = 0b00000000000000000010000000000000 in
  uint (((AND) mask_i w) >> 13)"

definition get_opf::"word32  int"
where "get_opf w  
  let mask_opf = 0b00000000000000000011111111100000 in
  uint (((AND) mask_opf w) >> 5)"

definition get_rs2::"word32  int"
where "get_rs2 w 
  let mask_rs2 = 0b00000000000000000000000000011111 in
  uint ((AND) mask_rs2 w)"

definition get_simm13::"word32  int"
where "get_simm13 w 
  let mask_simm13 = 0b00000000000000000001111111111111 in
  uint ((AND) mask_simm13 w)"

definition get_asi::"word32  int"
where "get_asi w 
  let mask_asi = 0b00000000000000000001111111100000 in
  uint (((AND) mask_asi w) >> 5)"

definition get_trap_cond:: "word32  int"
where "get_trap_cond w 
  let mask_cond = 0b00011110000000000000000000000000 in
  uint (((AND) mask_cond w) >> 25)"

definition get_trap_imm7:: "word32  int"
where "get_trap_imm7 w 
  let mask_imm7 = 0b00000000000000000000000001111111 in
  uint ((AND) mask_imm7 w)"

definition parse_instr_f1::"word32  
  (Exception list + instruction)"
where ― ‹CALL›, with a single operand disp30+"00"›
"parse_instr_f1 w                                                      
  Inr (call_type CALL,[W30 (word_of_int (get_disp30 w))])"

definition parse_instr_f2::"word32  
  (Exception list + instruction)"
where "parse_instr_f2 w 
  let op2 = get_op2 w in
  if op2 = uint(0b100::word3) then ― ‹SETHI› or NOP›
    let rd = get_rd w in
    let imm22 = get_disp_imm22 w in
    if rd = 0  imm22 = 0 then ― ‹NOP›
      Inr (nop_type NOP,[])
    else ― ‹SETHI›, with operands [imm22,rd]›
      Inr (sethi_type SETHI,[(W22 (word_of_int imm22)),
                   (W5 (word_of_int rd))])
  else if op2 = uint(0b010::word3) then ― ‹Bicc›, with operands [a,disp22]›
    let cond = get_cond w in
    let flaga = Flag (word_of_int (get_a w)) in
    let disp22 = W22 (word_of_int (get_disp_imm22 w)) in
    if cond = uint(0b0001::word4) then ― ‹BE›
      Inr (bicc_type BE,[flaga,disp22])
    else if cond = uint(0b1001::word4) then ― ‹BNE›
      Inr (bicc_type BNE,[flaga,disp22])
    else if cond = uint(0b1100::word4) then ― ‹BGU›
      Inr (bicc_type BGU,[flaga,disp22])
    else if cond = uint(0b0010::word4) then ― ‹BLE›
      Inr (bicc_type BLE,[flaga,disp22])
    else if cond = uint(0b0011::word4) then ― ‹BL›
      Inr (bicc_type BL,[flaga,disp22])
    else if cond = uint(0b1011::word4) then ― ‹BGE›
      Inr (bicc_type BGE,[flaga,disp22])
    else if cond = uint(0b0110::word4) then ― ‹BNEG›
      Inr (bicc_type BNEG,[flaga,disp22])
    else if cond = uint(0b1010::word4) then ― ‹BG›
      Inr (bicc_type BG,[flaga,disp22])
    else if cond = uint(0b0101::word4) then ― ‹BCS›
      Inr (bicc_type BCS,[flaga,disp22])
    else if cond = uint(0b0100::word4) then ― ‹BLEU›
      Inr (bicc_type BLEU,[flaga,disp22])
    else if cond = uint(0b1101::word4) then ― ‹BCC›
      Inr (bicc_type BCC,[flaga,disp22])
    else if cond = uint(0b1000::word4) then ― ‹BA›
      Inr (bicc_type BA,[flaga,disp22])
    else if cond = uint(0b0000::word4) then ― ‹BN›
      Inr (bicc_type BN,[flaga,disp22])
    else if cond = uint(0b1110::word4) then ― ‹BPOS›
      Inr (bicc_type BPOS,[flaga,disp22])
    else if cond = uint(0b1111::word4) then ― ‹BVC›
      Inr (bicc_type BVC,[flaga,disp22])
    else if cond = uint(0b0111::word4) then ― ‹BVS›
      Inr (bicc_type BVS,[flaga,disp22])
    else Inl [invalid_cond_f2]
  else Inl [invalid_op2_f2]
"

text ‹We don't consider floating-point operations, 
        so we don't consider the third type of format 3.›
definition parse_instr_f3::"word32  (Exception list + instruction)"
where "parse_instr_f3 w 
  let this_op = get_op w in
  let rd = get_rd w in
  let op3 = get_op3 w in
  let rs1 = get_rs1 w in
  let flagi = get_i w in
  let asi = get_asi w in
  let rs2 = get_rs2 w in
  let simm13 = get_simm13 w in
  if this_op = uint(0b11::word2) then ― ‹Load and Store›
  ― ‹If an instruction accesses alternative space but flagi = 1›,›
  ― ‹may need to throw a trap.›
    if op3 = uint(0b001001::word6) then ― ‹LDSB›
      if flagi = 1 then ― ‹Operant list is [i,rs1,simm13,rd]›
         Inr (load_store_type LDSB,[(Flag (word_of_int flagi)),
                        (W5 (word_of_int rs1)),
                        (Simm13 (word_of_int simm13)),
                        (W5 (word_of_int rd))])
      else ― ‹Operant list is [i,rs1,rs2,rd]›
         Inr (load_store_type LDSB,[(Flag (word_of_int flagi)),
                        (W5 (word_of_int rs1)),
                        (W5 (word_of_int rs2)),
                        (W5 (word_of_int rd))])
    else if op3 = uint(0b011001::word6) then ― ‹LDSBA›
       Inr (load_store_type LDSBA,[(Flag (word_of_int flagi)),
                         (W5 (word_of_int rs1)),
                         (W5 (word_of_int rs2)),
                         (Asi (word_of_int asi)),
                         (W5 (word_of_int rd))])
    else if op3 = uint(0b001010::word6) then ― ‹LDSH›
      if flagi = 1 then ― ‹Operant list is [i,rs1,simm13,rd]›
         Inr (load_store_type LDSH,[(Flag (word_of_int flagi)),
                        (W5 (word_of_int rs1)),
                        (Simm13 (word_of_int simm13)),
                        (W5 (word_of_int rd))])
      else ― ‹Operant list is [i,rs1,rs2,rd]›
         Inr (load_store_type LDSH,[(Flag (word_of_int flagi)),
                        (W5 (word_of_int rs1)),
                        (W5 (word_of_int rs2)),
                        (W5 (word_of_int rd))])
    else if op3 = uint(0b011010::word6) then ― ‹LDSHA›
       Inr (load_store_type LDSHA,[(Flag (word_of_int flagi)),
                         (W5 (word_of_int rs1)),
                         (W5 (word_of_int rs2)),
                         (Asi (word_of_int asi)),
                         (W5 (word_of_int rd))])
    else if op3 = uint(0b000001::word6) then ― ‹LDUB›
      if flagi = 1 then ― ‹Operant list is [i,rs1,simm13,rd]›
         Inr (load_store_type LDUB,[(Flag (word_of_int flagi)),
                        (W5 (word_of_int rs1)),
                        (Simm13 (word_of_int simm13)),
                        (W5 (word_of_int rd))])
      else ― ‹Operant list is [i,rs1,rs2,rd]›
         Inr (load_store_type LDUB,[(Flag (word_of_int flagi)),
                        (W5 (word_of_int rs1)),
                        (W5 (word_of_int rs2)),
                        (W5 (word_of_int rd))])
    else if op3 = uint(0b010001::word6) then ― ‹LDUBA›
       Inr (load_store_type LDUBA,[(Flag (word_of_int flagi)),
                         (W5 (word_of_int rs1)),
                         (W5 (word_of_int rs2)),
                         (Asi (word_of_int asi)),
                         (W5 (word_of_int rd))])
    else if op3 = uint(0b000010::word6) then ― ‹LDUH›
      if flagi = 1 then ― ‹Operant list is [i,rs1,simm13,rd]›
         Inr (load_store_type LDUH,[(Flag (word_of_int flagi)),
                        (W5 (word_of_int rs1)),
                        (Simm13 (word_of_int simm13)),
                        (W5 (word_of_int rd))])
      else ― ‹Operant list is [i,rs1,rs2,rd]›
         Inr (load_store_type LDUH,[(Flag (word_of_int flagi)),
                        (W5 (word_of_int rs1)),
                        (W5 (word_of_int rs2)),
                        (W5 (word_of_int rd))])
    else if op3 = uint(0b010010::word6) then ― ‹LDUHA›
       Inr (load_store_type LDUHA,[(Flag (word_of_int flagi)),
                         (W5 (word_of_int rs1)),
                         (W5 (word_of_int rs2)),
                         (Asi (word_of_int asi)),
                         (W5 (word_of_int rd))])
    else if op3 = uint(0b000000::word6) then ― ‹LD›
      if flagi = 1 then ― ‹Operant list is [i,rs1,simm13,rd]›
         Inr (load_store_type LD,[(Flag (word_of_int flagi)),
                      (W5 (word_of_int rs1)),
                      (Simm13 (word_of_int simm13)),
                      (W5 (word_of_int rd))])
      else ― ‹Operant list is [i,rs1,rs2,rd]›
         Inr (load_store_type LD,[(Flag (word_of_int flagi)),
                      (W5 (word_of_int rs1)),
                      (W5 (word_of_int rs2)),
                      (W5 (word_of_int rd))])
    else if op3 = uint(0b010000::word6) then ― ‹LDA›
       Inr (load_store_type LDA,[(Flag (word_of_int flagi)),
                       (W5 (word_of_int rs1)),
                       (W5 (word_of_int rs2)),
                       (Asi (word_of_int asi)),
                       (W5 (word_of_int rd))])
    else if op3 = uint(0b000011::word6) then ― ‹LDD›
      if flagi = 1 then ― ‹Operant list is [i,rs1,simm13,rd]›
         Inr (load_store_type LDD,[(Flag (word_of_int flagi)),
                       (W5 (word_of_int rs1)),
                       (Simm13 (word_of_int simm13)),
                       (W5 (word_of_int rd))])
      else ― ‹Operant list is [i,rs1,rs2,rd]›
         Inr (load_store_type LDD,[(Flag (word_of_int flagi)),
                       (W5 (word_of_int rs1)),
                       (W5 (word_of_int rs2)),
                       (W5 (word_of_int rd))])
    else if op3 = uint(0b010011::word6) then ― ‹LDDA›
       Inr (load_store_type LDDA,[(Flag (word_of_int flagi)),
                         (W5 (word_of_int rs1)),
                         (W5 (word_of_int rs2)),
                         (Asi (word_of_int asi)),
                         (W5 (word_of_int rd))])
    else if op3 = uint(0b001101::word6) then ― ‹LDSTUB›
      if flagi = 1 then ― ‹Operant list is [i,rs1,simm13,rd]›
         Inr (load_store_type LDSTUB,[(Flag (word_of_int flagi)),
                      (W5 (word_of_int rs1)),
                      (Simm13 (word_of_int simm13)),
                      (W5 (word_of_int rd))])
      else ― ‹Operant list is [i,rs1,rs2,rd]›
         Inr (load_store_type LDSTUB,[(Flag (word_of_int flagi)),
                      (W5 (word_of_int rs1)),
                      (W5 (word_of_int rs2)),
                      (W5 (word_of_int rd))])
    else if op3 = uint(0b011101::word6) then ― ‹LDSTUBA›
       Inr (load_store_type LDSTUBA,[(Flag (word_of_int flagi)),
                       (W5 (word_of_int rs1)),
                       (W5 (word_of_int rs2)),
                       (Asi (word_of_int asi)),
                       (W5 (word_of_int rd))])
    else if op3 = uint(0b000101::word6) then ― ‹STB›
      if flagi = 1 then ― ‹Operant list is [i,rs1,simm13,rd]›
         Inr (load_store_type STB,[(Flag (word_of_int flagi)),
                       (W5 (word_of_int rs1)),
                       (Simm13 (word_of_int simm13)),
                       (W5 (word_of_int rd))])
      else ― ‹Operant list is [i,rs1,rs2,rd]›
         Inr (load_store_type STB,[(Flag (word_of_int flagi)),
                       (W5 (word_of_int rs1)),
                       (W5 (word_of_int rs2)),
                       (W5 (word_of_int rd))])
    else if op3 = uint(0b010101::word6) then ― ‹STBA›
       Inr (load_store_type STBA,[(Flag (word_of_int flagi)),
                       (W5 (word_of_int rs1)),
                       (W5 (word_of_int rs2)),
                       (Asi (word_of_int asi)),
                       (W5 (word_of_int rd))])
    else if op3 = uint(0b000110::word6) then ― ‹STH›
      if flagi = 1 then ― ‹Operant list is [i,rs1,simm13,rd]›
         Inr (load_store_type STH,[(Flag (word_of_int flagi)),
                       (W5 (word_of_int rs1)),
                       (Simm13 (word_of_int simm13)),
                       (W5 (word_of_int rd))])
      else ― ‹Operant list is [i,rs1,rs2,rd]›
         Inr (load_store_type STH,[(Flag (word_of_int flagi)),
                       (W5 (word_of_int rs1)),
                       (W5 (word_of_int rs2)),
                       (W5 (word_of_int rd))])
    else if op3 = uint(0b010110::word6) then ― ‹STHA›
       Inr (load_store_type STHA,[(Flag (word_of_int flagi)),
                       (W5 (word_of_int rs1)),
                       (W5 (word_of_int rs2)),
                       (Asi (word_of_int asi)),
                       (W5 (word_of_int rd))])
    else if op3 = uint(0b000100::word6) then ― ‹ST›
      if flagi = 1 then ― ‹Operant list is [i,rs1,simm13,rd]›
         Inr (load_store_type ST,[(Flag (word_of_int flagi)),
                      (W5 (word_of_int rs1)),
                      (Simm13 (word_of_int simm13)),
                      (W5 (word_of_int rd))])
      else ― ‹Operant list is [i,rs1,rs2,rd]›
         Inr (load_store_type ST,[(Flag (word_of_int flagi)),
                      (W5 (word_of_int rs1)),
                      (W5 (word_of_int rs2)),
                      (W5 (word_of_int rd))])
    else if op3 = uint(0b010100::word6) then ― ‹STA›
       Inr (load_store_type STA,[(Flag (word_of_int flagi)),
                       (W5 (word_of_int rs1)),
                       (W5 (word_of_int rs2)),
                       (Asi (word_of_int asi)),
                       (W5 (word_of_int rd))])
    else if op3 = uint(0b000111::word6) then ― ‹STD›
      if flagi = 1 then ― ‹Operant list is [i,rs1,simm13,rd]›
         Inr (load_store_type STD,[(Flag (word_of_int flagi)),
                       (W5 (word_of_int rs1)),
                       (Simm13 (word_of_int simm13)),
                       (W5 (word_of_int rd))])
      else ― ‹Operant list is [i,rs1,rs2,rd]›
         Inr (load_store_type STD,[(Flag (word_of_int flagi)),
                       (W5 (word_of_int rs1)),
                       (W5 (word_of_int rs2)),
                       (W5 (word_of_int rd))])
    else if op3 = uint(0b010111::word6) then ― ‹STDA›
       Inr (load_store_type STDA,[(Flag (word_of_int flagi)),
                       (W5 (word_of_int rs1)),
                       (W5 (word_of_int rs2)),
                       (Asi (word_of_int asi)),
                       (W5 (word_of_int rd))])
    else if op3 = uint(0b001111::word6) then ― ‹SWAP›
      if flagi = 1 then ― ‹Operant list is [i,rs1,simm13,rd]›
         Inr (load_store_type SWAP,[(Flag (word_of_int flagi)),
                       (W5 (word_of_int rs1)),
                       (Simm13 (word_of_int simm13)),
                       (W5 (word_of_int rd))])
      else ― ‹Operant list is [i,rs1,rs2,rd]›
         Inr (load_store_type SWAP,[(Flag (word_of_int flagi)),
                       (W5 (word_of_int rs1)),
                       (W5 (word_of_int rs2)),
                       (W5 (word_of_int rd))])
    else if op3 = uint(0b011111::word6) then ― ‹SWAPA›
       Inr (load_store_type SWAPA,[(Flag (word_of_int flagi)),
                       (W5 (word_of_int rs1)),
                       (W5 (word_of_int rs2)),
                       (Asi (word_of_int asi)),
                       (W5 (word_of_int rd))])
    else Inl [invalid_op3_f3_op11]
  else if this_op = uint(0b10::word2) then ― ‹Others›
    if op3 = uint(0b111000::word6) then ― ‹JMPL›
      if flagi = 0 then ― ‹return [i,rs1,rs2,rd]›
         Inr (ctrl_type JMPL,[(Flag (word_of_int flagi)),
                        (W5 (word_of_int rs1)),
                        (W5 (word_of_int rs2)),
                        (W5 (word_of_int rd))])
      else ― ‹return [i,rs1,simm13,rd]›
         Inr (ctrl_type JMPL,[(Flag (word_of_int flagi)),
                        (W5 (word_of_int rs1)),
                        (Simm13 (word_of_int simm13)),
                        (W5 (word_of_int rd))])
    else if op3 = uint(0b111001::word6) then ― ‹RETT›
      if flagi = 0 then ― ‹return [i,rs1,rs2]›
         Inr (ctrl_type RETT,[(Flag (word_of_int flagi)),
                        (W5 (word_of_int rs1)),
                        (W5 (word_of_int rs2))])
      else ― ‹return [i,rs1,simm13]›
         Inr (ctrl_type RETT,[(Flag (word_of_int flagi)),
                        (W5 (word_of_int rs1)),
                        (Simm13 (word_of_int simm13))])
    ― ‹The following are Read and Write instructions,›
    ― ‹only return [rs1,rd]› as operand.›
    else if op3 = uint(0b101000::word6)  rs1  0 then ― ‹RDASR›
      if rs1 = uint(0b01111::word6)  rd = 0 then ― ‹STBAR› is a special case of RDASR›
        Inr (load_store_type STBAR,[])
      else Inr (sreg_type RDASR,[(W5 (word_of_int rs1)),
                       (W5 (word_of_int rd))])
    else if op3 = uint(0b101000::word6)  rs1 = 0 then ― ‹RDY›
       Inr (sreg_type RDY,[(W5 (word_of_int rs1)),
                     (W5 (word_of_int rd))])
    else if op3 = uint(0b101001::word6) then ― ‹RDPSR›
       Inr (sreg_type RDPSR,[(W5 (word_of_int rs1)),
                       (W5 (word_of_int rd))])
    else if op3 = uint(0b101010::word6) then ― ‹RDWIM›
       Inr (sreg_type RDWIM,[(W5 (word_of_int rs1)),
                       (W5 (word_of_int rd))])
    else if op3 = uint(0b101011::word6) then ― ‹RDTBR›
       Inr (sreg_type RDTBR,[(W5 (word_of_int rs1)),
                       (W5 (word_of_int rd))])
    else if op3 = uint(0b110000::word6)  rd  0 then ― ‹WRASR›
      if flagi = 0 then ― ‹return [i,rs1,rs2,rd]›
         Inr (sreg_type WRASR,[(Flag (word_of_int flagi)),
                         (W5 (word_of_int rs1)),
                         (W5 (word_of_int rs2)),
                         (W5 (word_of_int rd))])
      else ― ‹return [i,rs1,simm13,rd]›
         Inr (sreg_type WRASR,[(Flag (word_of_int flagi)),
                         (W5 (word_of_int rs1)),
                         (Simm13 (word_of_int simm13)),
                         (W5 (word_of_int rd))])
    else if op3 = uint(0b110000::word6)  rd = 0 then ― ‹WRY›
      if flagi = 0 then ― ‹return [i,rs1,rs2,rd]›
         Inr (sreg_type WRY,[(Flag (word_of_int flagi)),
                       (W5 (word_of_int rs1)),
                       (W5 (word_of_int rs2)),
                       (W5 (word_of_int rd))])
      else ― ‹return [i,rs1,simm13,rd]›
         Inr (sreg_type WRY,[(Flag (word_of_int flagi)),
                       (W5 (word_of_int rs1)),
                       (Simm13 (word_of_int simm13)),
                       (W5 (word_of_int rd))])
    else if op3 = uint(0b110001::word6) then ― ‹WRPSR›
      if flagi = 0 then ― ‹return [i,rs1,rs2,rd]›
         Inr (sreg_type WRPSR,[(Flag (word_of_int flagi)),
                         (W5 (word_of_int rs1)),
                         (W5 (word_of_int rs2)),
                         (W5 (word_of_int rd))])
      else ― ‹return [i,rs1,simm13,rd]›
         Inr (sreg_type WRPSR,[(Flag (word_of_int flagi)),
                         (W5 (word_of_int rs1)),
                         (Simm13 (word_of_int simm13)),
                         (W5 (word_of_int rd))])
    else if op3 = uint(0b110010::word6) then ― ‹WRWIM›
      if flagi = 0 then ― ‹return [i,rs1,rs2,rd]›
         Inr (sreg_type WRWIM,[(Flag (word_of_int flagi)),
                         (W5 (word_of_int rs1)),
                         (W5 (word_of_int rs2)),
                         (W5 (word_of_int rd))])
      else ― ‹return [i,rs1,simm13,rd]›
         Inr (sreg_type WRWIM,[(Flag (word_of_int flagi)),
                         (W5 (word_of_int rs1)),
                         (Simm13 (word_of_int simm13)),
                         (W5 (word_of_int rd))])
    else if op3 = uint(0b110011::word6) then ― ‹WRTBR›
      if flagi = 0 then ― ‹return [i,rs1,rs2,rd]›
         Inr (sreg_type WRTBR,[(Flag (word_of_int flagi)),
                         (W5 (word_of_int rs1)),
                         (W5 (word_of_int rs2)),
                         (W5 (word_of_int rd))])
      else ― ‹return [i,rs1,simm13,rd]›
         Inr (sreg_type WRTBR,[(Flag (word_of_int flagi)),
                         (W5 (word_of_int rs1)),
                         (Simm13 (word_of_int simm13)),
                         (W5 (word_of_int rd))])
    ― ‹FLUSH› instruction›
    else if op3 = uint(0b111011::word6) then ― ‹FLUSH›
      if flagi = 0 then ― ‹return [1,rs1,rs2]›
         Inr (load_store_type FLUSH,[(Flag (word_of_int flagi)),
                         (W5 (word_of_int rs1)),
                         (W5 (word_of_int rs2))])
      else ― ‹return [i,rs1,simm13]›
         Inr (load_store_type FLUSH,[(Flag (word_of_int flagi)),
                         (W5 (word_of_int rs1)),
                         (Simm13 (word_of_int simm13))])
    ― ‹The following are arithmetic instructions.›
    else if op3 = uint(0b000001::word6) then ― ‹AND›
      if flagi = 0 then ― ‹return [i,rs1,rs2,rd]›
         Inr (logic_type ANDs,[(Flag (word_of_int flagi)),
                        (W5 (word_of_int rs1)),
                        (W5 (word_of_int rs2)),
                        (W5 (word_of_int rd))])
      else ― ‹return [i,rs1,simm13,rd]›
         Inr (logic_type ANDs,[(Flag (word_of_int flagi)),
                        (W5 (word_of_int rs1)),
                        (Simm13 (word_of_int simm13)),
                        (W5 (word_of_int rd))])
    else if op3 = uint(0b010001::word6) then ― ‹ANDcc›
      if flagi = 0 then ― ‹return [i,rs1,rs2,rd]›
         Inr (logic_type ANDcc,[(Flag (word_of_int flagi)),
                         (W5 (word_of_int rs1)),
                         (W5 (word_of_int rs2)),
                         (W5 (word_of_int rd))])
      else ― ‹return [i,rs1,simm13,rd]›
         Inr (logic_type ANDcc,[(Flag (word_of_int flagi)),
                         (W5 (word_of_int rs1)),
                         (Simm13 (word_of_int simm13)),
                         (W5 (word_of_int rd))])
    else if op3 = uint(0b000101::word6) then ― ‹ANDN›
      if flagi = 0 then ― ‹return [i,rs1,rs2,rd]›
         Inr (logic_type ANDN,[(Flag (word_of_int flagi)),
                        (W5 (word_of_int rs1)),
                        (W5 (word_of_int rs2)),
                        (W5 (word_of_int rd))])
      else ― ‹return [i,rs1,simm13,rd]›
         Inr (logic_type ANDN,[(Flag (word_of_int flagi)),
                        (W5 (word_of_int rs1)),
                        (Simm13 (word_of_int simm13)),
                        (W5 (word_of_int rd))])
    else if op3 = uint(0b010101::word6) then ― ‹ANDNcc›
      if flagi = 0 then ― ‹return [i,rs1,rs2,rd]›
         Inr (logic_type ANDNcc,[(Flag (word_of_int flagi)),
                          (W5 (word_of_int rs1)),
                          (W5 (word_of_int rs2)),
                          (W5 (word_of_int rd))])
      else ― ‹return [i,rs1,simm13,rd]›
         Inr (logic_type ANDNcc,[(Flag (word_of_int flagi)),
                          (W5 (word_of_int rs1)),
                          (Simm13 (word_of_int simm13)),
                          (W5 (word_of_int rd))])
    else if op3 = uint(0b000010::word6) then ― ‹OR›
      if flagi = 0 then ― ‹return [i,rs1,rs2,rd]›
         Inr (logic_type ORs,[(Flag (word_of_int flagi)),
                       (W5 (word_of_int rs1)),
                       (W5 (word_of_int rs2)),
                       (W5 (word_of_int rd))])
      else ― ‹return [i,rs1,simm13,rd]›
         Inr (logic_type ORs,[(Flag (word_of_int flagi)),
                       (W5 (word_of_int rs1)),
                       (Simm13 (word_of_int simm13)),
                       (W5 (word_of_int rd))])
    else if op3 = uint(0b010010::word6) then ― ‹ORcc›
      if flagi = 0 then ― ‹return [i,rs1,rs2,rd]›
         Inr (logic_type ORcc,[(Flag (word_of_int flagi)),
                        (W5 (word_of_int rs1)),
                        (W5 (word_of_int rs2)),
                        (W5 (word_of_int rd))])
      else ― ‹return [i,rs1,simm13,rd]›
         Inr (logic_type ORcc,[(Flag (word_of_int flagi)),
                        (W5 (word_of_int rs1)),
                        (Simm13 (word_of_int simm13)),
                        (W5 (word_of_int rd))])
    else if op3 = uint(0b000110::word6) then ― ‹ORN›
      if flagi = 0 then ― ‹return [i,rs1,rs2,rd]›
         Inr (logic_type ORN,[(Flag (word_of_int flagi)),
                       (W5 (word_of_int rs1)),
                       (W5 (word_of_int rs2)),
                       (W5 (word_of_int rd))])
      else ― ‹return [i,rs1,simm13,rd]›
         Inr (logic_type ORN,[(Flag (word_of_int flagi)),
                       (W5 (word_of_int rs1)),
                       (Simm13 (word_of_int simm13)),
                       (W5 (word_of_int rd))])
    else if op3 = uint(0b010110::word6) then ― ‹ORNcc›
      if flagi = 0 then ― ‹return [i,rs1,rs2,rd]›
         Inr (logic_type ORNcc,[(Flag (word_of_int flagi)),
                       (W5 (word_of_int rs1)),
                       (W5 (word_of_int rs2)),
                       (W5 (word_of_int rd))])
      else ― ‹return [i,rs1,simm13,rd]›
         Inr (logic_type ORNcc,[(Flag (word_of_int flagi)),
                       (W5 (word_of_int rs1)),
                       (Simm13 (word_of_int simm13)),
                       (W5 (word_of_int rd))])
    else if op3 = uint(0b000011::word6) then ― ‹XORs›
      if flagi = 0 then ― ‹return [i,rs1,rs2,rd]›
         Inr (logic_type XORs,[(Flag (word_of_int flagi)),
                        (W5 (word_of_int rs1)),
                        (W5 (word_of_int rs2)),
                        (W5 (word_of_int rd))])
      else ― ‹return [i,rs1,simm13,rd]›
         Inr (logic_type XORs,[(Flag (word_of_int flagi)),
                        (W5 (word_of_int rs1)),
                        (Simm13 (word_of_int simm13)),
                        (W5 (word_of_int rd))])
    else if op3 = uint(0b010011::word6) then ― ‹XORcc›
      if flagi = 0 then ― ‹return [i,rs1,rs2,rd]›
         Inr (logic_type XORcc,[(Flag (word_of_int flagi)),
                       (W5 (word_of_int rs1)),
                       (W5 (word_of_int rs2)),
                       (W5 (word_of_int rd))])
      else ― ‹return [i,rs1,simm13,rd]›
         Inr (logic_type XORcc,[(Flag (word_of_int flagi)),
                       (W5 (word_of_int rs1)),
                       (Simm13 (word_of_int simm13)),
                       (W5 (word_of_int rd))])
    else if op3 = uint(0b000111::word6) then ― ‹XNOR›
      if flagi = 0 then ― ‹return [i,rs1,rs2,rd]›
         Inr (logic_type XNOR,[(Flag (word_of_int flagi)),
                        (W5 (word_of_int rs1)),
                        (W5 (word_of_int rs2)),
                        (W5 (word_of_int rd))])
      else ― ‹return [i,rs1,simm13,rd]›
         Inr (logic_type XNOR,[(Flag (word_of_int flagi)),
                        (W5 (word_of_int rs1)),
                        (Simm13 (word_of_int simm13)),
                        (W5 (word_of_int rd))])
    else if op3 = uint(0b010111::word6) then ― ‹XNORcc›
      if flagi = 0 then ― ‹return [i,rs1,rs2,rd]›
         Inr (logic_type XNORcc,[(Flag (word_of_int flagi)),
                       (W5 (word_of_int rs1)),
                       (W5 (word_of_int rs2)),
                       (W5 (word_of_int rd))])
      else ― ‹return [i,rs1,simm13,rd]›
         Inr (logic_type XNORcc,[(Flag (word_of_int flagi)),
                       (W5 (word_of_int rs1)),
                       (Simm13 (word_of_int simm13)),
                       (W5 (word_of_int rd))])
    else if op3 = uint(0b100101::word6) then ― ‹SLL›
      if flagi = 0 then ― ‹return [i,rs1,rs2,rd]›
         Inr (shift_type SLL,[(Flag (word_of_int flagi)),
                       (W5 (word_of_int rs1)),
                       (W5 (word_of_int rs2)),
                       (W5 (word_of_int rd))])
      else ― ‹return [i,rs1,shcnt,rd]›
        let shcnt = rs2 in
         Inr (shift_type SLL,[(Flag (word_of_int flagi)),
                       (W5 (word_of_int rs1)),
                       (W5 (word_of_int shcnt)),
                       (W5 (word_of_int rd))])
    else if op3 = uint (0b100110::word6) then ― ‹SRL›
      if flagi = 0 then ― ‹return [i,rs1,rs2,rd]›
         Inr (shift_type SRL,[(Flag (word_of_int flagi)),
                       (W5 (word_of_int rs1)),
                       (W5 (word_of_int rs2)),
                       (W5 (word_of_int rd))])
      else ― ‹return [i,rs1,shcnt,rd]›
        let shcnt = rs2 in
         Inr (shift_type SRL,[(Flag (word_of_int flagi)),
                       (W5 (word_of_int rs1)),
                       (W5 (word_of_int shcnt)),
                       (W5 (word_of_int rd))])
    else if op3 = uint(0b100111::word6) then ― ‹SRA›
      if flagi = 0 then ― ‹return [i,rs1,rs2,rd]›
         Inr (shift_type SRA,[(Flag (word_of_int flagi)),
                       (W5 (word_of_int rs1)),
                       (W5 (word_of_int rs2)),
                       (W5 (word_of_int rd))])
      else ― ‹return [i,rs1,shcnt,rd]›
        let shcnt = rs2 in
         Inr (shift_type SRA,[(Flag (word_of_int flagi)),
                       (W5 (word_of_int rs1)),
                       (W5 (word_of_int shcnt)),
                       (W5 (word_of_int rd))])
    else if op3 = uint(0b000000::word6) then ― ‹ADD›
      if flagi = 0 then ― ‹return [i,rs1,rs2,rd]›
         Inr (arith_type ADD,[(Flag (word_of_int flagi)),
                       (W5 (word_of_int rs1)),
                       (W5 (word_of_int rs2)),
                       (W5 (word_of_int rd))])
      else ― ‹return [i,rs1,simm13,rd]›
         Inr (arith_type ADD,[(Flag (word_of_int flagi)),
                       (W5 (word_of_int rs1)),
                       (Simm13 (word_of_int simm13)),
                       (W5 (word_of_int rd))])
    else if op3 = uint(0b010000::word6) then ― ‹ADDcc›
      if flagi = 0 then ― ‹return [i,rs1,rs2,rd]›
         Inr (arith_type ADDcc,[(Flag (word_of_int flagi)),
                         (W5 (word_of_int rs1)),
                         (W5 (word_of_int rs2)),
                         (W5 (word_of_int rd))])
      else ― ‹return [i,rs1,simm13,rd]›
         Inr (arith_type ADDcc,[(Flag (word_of_int flagi)),
                         (W5 (word_of_int rs1)),
                         (Simm13 (word_of_int simm13)),
                         (W5 (word_of_int rd))])
    else if op3 = uint(0b001000::word6) then ― ‹ADDX›
      if flagi = 0 then ― ‹return [i,rs1,rs2,rd]›
         Inr (arith_type ADDX,[(Flag (word_of_int flagi)),
                        (W5 (word_of_int rs1)),
                        (W5 (word_of_int rs2)),
                        (W5 (word_of_int rd))])
      else ― ‹return [i,rs1,simm13,rd]›
         Inr (arith_type ADDX,[(Flag (word_of_int flagi)),
                        (W5 (word_of_int rs1)),
                        (Simm13 (word_of_int simm13)),
                        (W5 (word_of_int rd))])
    else if op3 = uint(0b011000::word6) then ― ‹ADDXcc›
      if flagi = 0 then ― ‹return [i,rs1,rs2,rd]›
         Inr (arith_type ADDXcc,[(Flag (word_of_int flagi)),
                        (W5 (word_of_int rs1)),
                        (W5 (word_of_int rs2)),
                        (W5 (word_of_int rd))])
      else ― ‹return [i,rs1,simm13,rd]›
         Inr (arith_type ADDXcc,[(Flag (word_of_int flagi)),
                        (W5 (word_of_int rs1)),
                        (Simm13 (word_of_int simm13)),
                        (W5 (word_of_int rd))])
    else if op3 = uint(0b100000::word6) then ― ‹TADDcc›
      if flagi = 0 then ― ‹return [i,rs1,rs2,rd]›
         Inr (arith_type TADDcc,[(Flag (word_of_int flagi)),
                        (W5 (word_of_int rs1)),
                        (W5 (word_of_int rs2)),
                        (W5 (word_of_int rd))])
      else ― ‹return [i,rs1,simm13,rd]›
         Inr (arith_type TADDcc,[(Flag (word_of_int flagi)),
                        (W5 (word_of_int rs1)),
                        (Simm13 (word_of_int simm13)),
                        (W5 (word_of_int rd))])
    else if op3 = uint(0b100010::word6) then ― ‹TADDccTV›
      if flagi = 0 then ― ‹return [i,rs1,rs2,rd]›
         Inr (arith_type TADDccTV,[(Flag (word_of_int flagi)),
                        (W5 (word_of_int rs1)),
                        (W5 (word_of_int rs2)),
                        (W5 (word_of_int rd))])
      else ― ‹return [i,rs1,simm13,rd]›
         Inr (arith_type TADDccTV,[(Flag (word_of_int flagi)),
                        (W5 (word_of_int rs1)),
                        (Simm13 (word_of_int simm13)),
                        (W5 (word_of_int rd))])
    else if op3 = uint(0b000100::word6) then ― ‹SUB›
      if flagi = 0 then ― ‹return [i,rs1,rs2,rd]›
         Inr (arith_type SUB,[(Flag (word_of_int flagi)),
                       (W5 (word_of_int rs1)),
                       (W5 (word_of_int rs2)),
                       (W5 (word_of_int rd))])
      else ― ‹return [i,rs1,simm13,rd]›
         Inr (arith_type SUB,[(Flag (word_of_int flagi)),
                       (W5 (word_of_int rs1)),
                       (Simm13 (word_of_int simm13)),
                       (W5 (word_of_int rd))])
    else if op3 = uint(0b010100::word6) then ― ‹SUBcc›
      if flagi = 0 then ― ‹return [i,rs1,rs2,rd]›
         Inr (arith_type SUBcc,[(Flag (word_of_int flagi)),
                         (W5 (word_of_int rs1)),
                         (W5 (word_of_int rs2)),
                         (W5 (word_of_int rd))])
      else ― ‹return [i,rs1,simm13,rd]›
         Inr (arith_type SUBcc,[(Flag (word_of_int flagi)),
                         (W5 (word_of_int rs1)),
                         (Simm13 (word_of_int simm13)),
                         (W5 (word_of_int rd))])
    else if op3 = uint(0b001100::word6) then ― ‹SUBX›
      if flagi = 0 then ― ‹return [i,rs1,rs2,rd]›
         Inr (arith_type SUBX,[(Flag (word_of_int flagi)),
                        (W5 (word_of_int rs1)),
                        (W5 (word_of_int rs2)),
                        (W5 (word_of_int rd))])
      else ― ‹return [i,rs1,simm13,rd]›
         Inr (arith_type SUBX,[(Flag (word_of_int flagi)),
                        (W5 (word_of_int rs1)),
                        (Simm13 (word_of_int simm13)),
                        (W5 (word_of_int rd))])
    else if op3 = uint(0b011100::word6) then ― ‹SUBXcc›
      if flagi = 0 then ― ‹return [i,rs1,rs2,rd]›
         Inr (arith_type SUBXcc,[(Flag (word_of_int flagi)),
                        (W5 (word_of_int rs1)),
                        (W5 (word_of_int rs2)),
                        (W5 (word_of_int rd))])
      else ― ‹return [i,rs1,simm13,rd]›
         Inr (arith_type SUBXcc,[(Flag (word_of_int flagi)),
                        (W5 (word_of_int rs1)),
                        (Simm13 (word_of_int simm13)),
                        (W5 (word_of_int rd))])
    else if op3 = uint(0b100001::word6) then ― ‹TSUBcc›
      if flagi = 0 then ― ‹return [i,rs1,rs2,rd]›
         Inr (arith_type TSUBcc,[(Flag (word_of_int flagi)),
                        (W5 (word_of_int rs1)),
                        (W5 (word_of_int rs2)),
                        (W5 (word_of_int rd))])
      else ― ‹return [i,rs1,simm13,rd]›
         Inr (arith_type TSUBcc,[(Flag (word_of_int flagi)),
                        (W5 (word_of_int rs1)),
                        (Simm13 (word_of_int simm13)),
                        (W5 (word_of_int rd))])
    else if op3 = uint(0b100011::word6) then ― ‹TSUBccTV›
      if flagi = 0 then ― ‹return [i,rs1,rs2,rd]›
         Inr (arith_type TSUBccTV,[(Flag (word_of_int flagi)),
                        (W5 (word_of_int rs1)),
                        (W5 (word_of_int rs2)),
                        (W5 (word_of_int rd))])
      else ― ‹return [i,rs1,simm13,rd]›
         Inr (arith_type TSUBccTV,[(Flag (word_of_int flagi)),
                        (W5 (word_of_int rs1)),
                        (Simm13 (word_of_int simm13)),
                        (W5 (word_of_int rd))])
    else if op3 = uint(0b100100::word6) then ― ‹MULScc›
      if flagi = 0 then ― ‹return [i,rs1,rs2,rd]›
         Inr (arith_type MULScc,[(Flag (word_of_int flagi)),
                        (W5 (word_of_int rs1)),
                        (W5 (word_of_int rs2)),
                        (W5 (word_of_int rd))])
      else ― ‹return [i,rs1,simm13,rd]›
         Inr (arith_type MULScc,[(Flag (word_of_int flagi)),
                        (W5 (word_of_int rs1)),
                        (Simm13 (word_of_int simm13)),
                        (W5 (word_of_int rd))])
    else if op3 = uint(0b001010::word6) then ― ‹UMUL›
      if flagi = 0 then ― ‹return [i,rs1,rs2,rd]›
         Inr (arith_type UMUL,[(Flag (word_of_int flagi)),
                        (W5 (word_of_int rs1)),
                        (W5 (word_of_int rs2)),
                        (W5 (word_of_int rd))])
      else ― ‹return [i,rs1,simm13,rd]›
         Inr (arith_type UMUL,[(Flag (word_of_int flagi)),
                        (W5 (word_of_int rs1)),
                        (Simm13 (word_of_int simm13)),
                        (W5 (word_of_int rd))])
    else if op3 = uint(0b011010::word6) then ― ‹UMULcc›
      if flagi = 0 then ― ‹return [i,rs1,rs2,rd]›
         Inr (arith_type UMULcc,[(Flag (word_of_int flagi)),
                        (W5 (word_of_int rs1)),
                        (W5 (word_of_int rs2)),
                        (W5 (word_of_int rd))])
      else ― ‹return [i,rs1,simm13,rd]›
         Inr (arith_type UMULcc,[(Flag (word_of_int flagi)),
                        (W5 (word_of_int rs1)),
                        (Simm13 (word_of_int simm13)),
                        (W5 (word_of_int rd))])
    else if op3 = uint(0b001011::word6) then ― ‹SMUL›
      if flagi = 0 then ― ‹return [i,rs1,rs2,rd]›
         Inr (arith_type SMUL,[(Flag (word_of_int flagi)),
                        (W5 (word_of_int rs1)),
                        (W5 (word_of_int rs2)),
                        (W5 (word_of_int rd))])
      else ― ‹return [i,rs1,simm13,rd]›
         Inr (arith_type SMUL,[(Flag (word_of_int flagi)),
                        (W5 (word_of_int rs1)),
                        (Simm13 (word_of_int simm13)),
                        (W5 (word_of_int rd))])
    else if op3 = uint(0b011011::word6) then ― ‹SMULcc›
      if flagi = 0 then ― ‹return [i,rs1,rs2,rd]›
         Inr (arith_type SMULcc,[(Flag (word_of_int flagi)),
                          (W5 (word_of_int rs1)),
                          (W5 (word_of_int rs2)),
                          (W5 (word_of_int rd))])
      else ― ‹return [i,rs1,simm13,rd]›
         Inr (arith_type SMULcc,[(Flag (word_of_int flagi)),
                          (W5 (word_of_int rs1)),
                          (Simm13 (word_of_int simm13)),
                          (W5 (word_of_int rd))])
    else if op3 = uint(0b001110::word6) then ― ‹UDIV›
      if flagi = 0 then ― ‹return [i,rs1,rs2,rd]›
         Inr (arith_type UDIV,[(Flag (word_of_int flagi)),
                        (W5 (word_of_int rs1)),
                        (W5 (word_of_int rs2)),
                        (W5 (word_of_int rd))])
      else ― ‹return [i,rs1,simm13,rd]›
         Inr (arith_type UDIV,[(Flag (word_of_int flagi)),
                        (W5 (word_of_int rs1)),
                        (Simm13 (word_of_int simm13)),
                        (W5 (word_of_int rd))])
    else if op3 = uint(0b011110::word6) then ― ‹UDIVcc›
      if flagi = 0 then ― ‹return [i,rs1,rs2,rd]›
         Inr (arith_type UDIVcc,[(Flag (word_of_int flagi)),
                          (W5 (word_of_int rs1)),
                          (W5 (word_of_int rs2)),
                          (W5 (word_of_int rd))])
      else ― ‹return [i,rs1,simm13,rd]›
         Inr (arith_type UDIVcc,[(Flag (word_of_int flagi)),
                          (W5 (word_of_int rs1)),
                          (Simm13 (word_of_int simm13)),
                          (W5 (word_of_int rd))])
    else if op3 = uint(0b001111::word6) then ― ‹SDIV›
      if flagi = 0 then ― ‹return [i,rs1,rs2,rd]›
         Inr (arith_type SDIV,[(Flag (word_of_int flagi)),
                        (W5 (word_of_int rs1)),
                        (W5 (word_of_int rs2)),
                        (W5 (word_of_int rd))])
      else ― ‹return [i,rs1,simm13,rd]›
         Inr (arith_type SDIV,[(Flag (word_of_int flagi)),
                        (W5 (word_of_int rs1)),
                        (Simm13 (word_of_int simm13)),
                        (W5 (word_of_int rd))])
    else if op3 = uint(0b011111::word6) then ― ‹SDIVcc›
      if flagi = 0 then ― ‹return [i,rs1,rs2,rd]›
         Inr (arith_type SDIVcc,[(Flag (word_of_int flagi)),
                        (W5 (word_of_int rs1)),
                        (W5 (word_of_int rs2)),
                        (W5 (word_of_int rd))])
      else ― ‹return [i,rs1,simm13,rd]›
         Inr (arith_type SDIVcc,[(Flag (word_of_int flagi)),
                        (W5 (word_of_int rs1)),
                        (Simm13 (word_of_int simm13)),
                        (W5 (word_of_int rd))])
    else if op3 = uint(0b111100::word6) then ― ‹SAVE›
      if flagi = 0 then ― ‹return [i,rs1,rs2,rd]›
         Inr (ctrl_type SAVE,[(Flag (word_of_int flagi)),
                        (W5 (word_of_int rs1)),
                        (W5 (word_of_int rs2)),
                        (W5 (word_of_int rd))])
      else ― ‹return [i,rs1,simm13,rd]›
         Inr (ctrl_type SAVE,[(Flag (word_of_int flagi)),
                        (W5 (word_of_int rs1)),
                        (Simm13 (word_of_int simm13)),
                        (W5 (word_of_int rd))])
    else if op3 = uint(0b111101::word6) then ― ‹RESTORE›
      if flagi = 0 then ― ‹return [i,rs1,rs2,rd]›
         Inr (ctrl_type RESTORE,[(Flag (word_of_int flagi)),
                           (W5 (word_of_int rs1)),
                           (W5 (word_of_int rs2)),
                           (W5 (word_of_int rd))])
      else ― ‹return [i,rs1,simm13,rd]›
         Inr (ctrl_type RESTORE,[(Flag (word_of_int flagi)),
                           (W5 (word_of_int rs1)),
                           (Simm13 (word_of_int simm13)),
                           (W5 (word_of_int rd))])
    else if op3 = uint(0b111010::word6) then ― ‹Ticc›
      let trap_cond = get_trap_cond w in
      let trap_imm7 = get_trap_imm7 w in
      if trap_cond = uint(0b1000::word4) then ― ‹TA›
        if flagi = 0 then ― ‹return [i,rs1,rs2]›
          Inr (ticc_type TA,[(Flag (word_of_int flagi)),
                   (W5 (word_of_int rs1)),
                   (W5 (word_of_int rs2))])
        else ― ‹return [i,rs1,trap_imm7]›
          Inr (ticc_type TA,[(Flag (word_of_int flagi)),
                    (W5 (word_of_int rs1)),
                    (Imm7 (word_of_int trap_imm7))])
      else if trap_cond = uint(0b0000::word4) then ― ‹TN›
        if flagi = 0 then ― ‹return [i,rs1,rs2]›
          Inr (ticc_type TN,[(Flag (word_of_int flagi)),
                   (W5 (word_of_int rs1)),
                   (W5 (word_of_int rs2))])
        else ― ‹return [i,rs1,trap_imm7]›
          Inr (ticc_type TN,[(Flag (word_of_int flagi)),
                    (W5 (word_of_int rs1)),
                    (Imm7 (word_of_int trap_imm7))])
      else if trap_cond = uint(0b1001::word4) then ― ‹TNE›
        if flagi = 0 then ― ‹return [i,rs1,rs2]›
          Inr (ticc_type TNE,[(Flag (word_of_int flagi)),
                   (W5 (word_of_int rs1)),
                   (W5 (word_of_int rs2))])
        else ― ‹return [i,rs1,trap_imm7]›
          Inr (ticc_type TNE,[(Flag (word_of_int flagi)),
                    (W5 (word_of_int rs1)),
                    (Imm7 (word_of_int trap_imm7))])
      else if trap_cond = uint(0b0001::word4) then ― ‹TE›
        if flagi = 0 then ― ‹return [i,rs1,rs2]›
          Inr (ticc_type TE,[(Flag (word_of_int flagi)),
                   (W5 (word_of_int rs1)),
                   (W5 (word_of_int rs2))])
        else ― ‹return [i,rs1,trap_imm7]›
          Inr (ticc_type TE,[(Flag (word_of_int flagi)),
                    (W5 (word_of_int rs1)),
                    (Imm7 (word_of_int trap_imm7))])
      else if trap_cond = uint(0b1010::word4) then ― ‹TG›
        if flagi = 0 then ― ‹return [i,rs1,rs2]›
          Inr (ticc_type TG,[(Flag (word_of_int flagi)),
                   (W5 (word_of_int rs1)),
                   (W5 (word_of_int rs2))])
        else ― ‹return [i,rs1,trap_imm7]›
          Inr (ticc_type TG,[(Flag (word_of_int flagi)),
                    (W5 (word_of_int rs1)),
                    (Imm7 (word_of_int trap_imm7))])
      else if trap_cond = uint(0b0010::word4) then ― ‹TLE›
        if flagi = 0 then ― ‹return [i,rs1,rs2]›
          Inr (ticc_type TLE,[(Flag (word_of_int flagi)),
                   (W5 (word_of_int rs1)),
                   (W5 (word_of_int rs2))])
        else ― ‹return [i,rs1,trap_imm7]›
          Inr (ticc_type TLE,[(Flag (word_of_int flagi)),
                    (W5 (word_of_int rs1)),
                    (Imm7 (word_of_int trap_imm7))])
      else if trap_cond = uint(0b1011::word4) then ― ‹TGE›
        if flagi = 0 then ― ‹return [i,rs1,rs2]›
          Inr (ticc_type TGE,[(Flag (word_of_int flagi)),
                   (W5 (word_of_int rs1)),
                   (W5 (word_of_int rs2))])
        else ― ‹return [i,rs1,trap_imm7]›
          Inr (ticc_type TGE,[(Flag (word_of_int flagi)),
                    (W5 (word_of_int rs1)),
                    (Imm7 (word_of_int trap_imm7))])
      else if trap_cond = uint(0b0011::word4) then ― ‹TL›
        if flagi = 0 then ― ‹return [i,rs1,rs2]›
          Inr (ticc_type TL,[(Flag (word_of_int flagi)),
                   (W5 (word_of_int rs1)),
                   (W5 (word_of_int rs2))])
        else ― ‹return [i,rs1,trap_imm7]›
          Inr (ticc_type TL,[(Flag (word_of_int flagi)),
                    (W5 (word_of_int rs1)),
                    (Imm7 (word_of_int trap_imm7))])
      else if trap_cond = uint(0b1100::word4) then ― ‹TGU›
        if flagi = 0 then ― ‹return [i,rs1,rs2]›
          Inr (ticc_type TGU,[(Flag (word_of_int flagi)),
                   (W5 (word_of_int rs1)),
                   (W5 (word_of_int rs2))])
        else ― ‹return [i,rs1,trap_imm7]›
          Inr (ticc_type TGU,[(Flag (word_of_int flagi)),
                    (W5 (word_of_int rs1)),
                    (Imm7 (word_of_int trap_imm7))])
      else if trap_cond = uint(0b0100::word4) then ― ‹TLEU›
        if flagi = 0 then ― ‹return [i,rs1,rs2]›
          Inr (ticc_type TLEU,[(Flag (word_of_int flagi)),
                   (W5 (word_of_int rs1)),
                   (W5 (word_of_int rs2))])
        else ― ‹return [i,rs1,trap_imm7]›
          Inr (ticc_type TLEU,[(Flag (word_of_int flagi)),
                    (W5 (word_of_int rs1)),
                    (Imm7 (word_of_int trap_imm7))])
      else if trap_cond = uint(0b1101::word4) then ― ‹TCC›
        if flagi = 0 then ― ‹return [i,rs1,rs2]›
          Inr (ticc_type TCC,[(Flag (word_of_int flagi)),
                   (W5 (word_of_int rs1)),
                   (W5 (word_of_int rs2))])
        else ― ‹return [i,rs1,trap_imm7]›
          Inr (ticc_type TCC,[(Flag (word_of_int flagi)),
                    (W5 (word_of_int rs1)),
                    (Imm7 (word_of_int trap_imm7))])
      else if trap_cond = uint(0b0101::word4) then ― ‹TCS›
        if flagi = 0 then ― ‹return [i,rs1,rs2]›
          Inr (ticc_type TCS,[(Flag (word_of_int flagi)),
                   (W5 (word_of_int rs1)),
                   (W5 (word_of_int rs2))])
        else ― ‹return [i,rs1,trap_imm7]›
          Inr (ticc_type TCS,[(Flag (word_of_int flagi)),
                    (W5 (word_of_int rs1)),
                    (Imm7 (word_of_int trap_imm7))])
      else if trap_cond = uint(0b1110::word4) then ― ‹TPOS›
        if flagi = 0 then ― ‹return [i,rs1,rs2]›
          Inr (ticc_type TPOS,[(Flag (word_of_int flagi)),
                   (W5 (word_of_int rs1)),
                   (W5 (word_of_int rs2))])
        else ― ‹return [i,rs1,trap_imm7]›
          Inr (ticc_type TPOS,[(Flag (word_of_int flagi)),
                    (W5 (word_of_int rs1)),
                    (Imm7 (word_of_int trap_imm7))])
      else if trap_cond = uint(0b0110::word4) then ― ‹TNEG›
        if flagi = 0 then ― ‹return [i,rs1,rs2]›
          Inr (ticc_type TNEG,[(Flag (word_of_int flagi)),
                   (W5 (word_of_int rs1)),
                   (W5 (word_of_int rs2))])
        else ― ‹return [i,rs1,trap_imm7]›
          Inr (ticc_type TNEG,[(Flag (word_of_int flagi)),
                    (W5 (word_of_int rs1)),
                    (Imm7 (word_of_int trap_imm7))])
      else if trap_cond = uint(0b1111::word4) then ― ‹TVC›
        if flagi = 0 then ― ‹return [i,rs1,rs2]›
          Inr (ticc_type TVC,[(Flag (word_of_int flagi)),
                   (W5 (word_of_int rs1)),
                   (W5 (word_of_int rs2))])
        else ― ‹return [i,rs1,trap_imm7]›
          Inr (ticc_type TVC,[(Flag (word_of_int flagi)),
                    (W5 (word_of_int rs1)),
                    (Imm7 (word_of_int trap_imm7))])
      else if trap_cond = uint(0b0111::word4) then ― ‹TVS›
        if flagi = 0 then ― ‹return [i,rs1,rs2]›
          Inr (ticc_type TVS,[(Flag (word_of_int flagi)),
                   (W5 (word_of_int rs1)),
                   (W5 (word_of_int rs2))])
        else ― ‹return [i,rs1,trap_imm7]›
          Inr (ticc_type TVS,[(Flag (word_of_int flagi)),
                    (W5 (word_of_int rs1)),
                    (Imm7 (word_of_int trap_imm7))])
      else Inl [invalid_trap_cond]     
    else Inl [invalid_op3_f3_op10]
  else Inl [invalid_op_f3]
"

text ‹Read the word32 value from the Program Counter in the current state. 
        Find the instruction in the memory address of the word32 value. 
        Return a word32 value of the insturction.›
definition fetch_instruction::"('a) sparc_state 
  (Exception list + word32)"
where "fetch_instruction s  
  ― ‹pc_val› is the 32-bit memory address of the instruction.›
  let pc_val = cpu_reg_val PC s;
      psr_val = cpu_reg_val PSR s;
      s_val = get_S psr_val;
      asi = if s_val = 0 then word_of_int 8 else word_of_int 9
  in
  ― ‹Check if pc_val› is aligned to 4-byte (32-bit) boundary.›
  ― ‹That is, check if the least significant two bits of›
  ― ‹pc_val› are 0s.›
    if uint((AND) (0b00000000000000000000000000000011) pc_val) = 0 then
    ― ‹Get the 32-bit value from the address of pc_val›
    ― ‹to the address of pc_val+3›
        let (mem_result,n_s) = memory_read asi pc_val s in
        case mem_result of 
         None  Inl [fetch_instruction_error]
        |Some v  Inr v
    else Inl [fetch_instruction_error]
"

text ‹Decode the word32 value of an instruction into 
        the name of the instruction and its operands.›
definition decode_instruction::"word32  
  Exception list + instruction"
where "decode_instruction w  
  let this_op = get_op w in 
  if this_op = uint(0b01::word2) then ― ‹Instruction format 1›
    parse_instr_f1 w
  else if this_op = uint(0b00::word2) then ― ‹Instruction format 2›
    parse_instr_f2 w
  else ― ‹op = 11 0r 10›, instruction format 3›
    parse_instr_f3 w
"

text ‹Get the current window from the PSR›
definition get_curr_win::"unit  ('a,('a::len window_size)) sparc_state_monad"
where "get_curr_win _  
  do
    curr_win  gets (λs. (ucast (get_CWP (cpu_reg_val PSR s))));
    return curr_win 
  od"

text ‹Operational semantics for CALL›
definition call_instr::"instruction  ('a::len,unit) sparc_state_monad"
where "call_instr instr 
  let op_list = snd instr;
      mem_addr = ((ucast (get_operand_w30 (op_list!0)))::word32) << 2
  in
  do
    curr_win  get_curr_win();
    pc_val  gets (λs. (cpu_reg_val PC s));
    npc_val  gets (λs. (cpu_reg_val nPC s));
    write_reg pc_val curr_win (word_of_int 15);
    write_cpu npc_val PC;
    write_cpu (pc_val + mem_addr) nPC;
    return ()
  od"

text‹Evaluate icc based on the bits N, Z, V, C in PSR 
       and the type of branching instruction. 
       See Sparcv8 manual Page 178.›
definition eval_icc::"sparc_operation  word1  word1  word1  word1  int"
where
"eval_icc instr_name n_val z_val v_val c_val 
    if instr_name = bicc_type BNE then
      if z_val = 0 then 1 else 0
    else if instr_name = bicc_type BE then 
      if z_val = 1 then 1 else 0
    else if instr_name = bicc_type BG then
      if ((OR) z_val (n_val XOR v_val)) = 0 then 1 else 0
    else if instr_name = bicc_type BLE then
      if ((OR) z_val (n_val XOR v_val)) = 1 then 1 else 0
    else if instr_name = bicc_type BGE then
      if (n_val XOR v_val) = 0 then 1 else 0
    else if instr_name = bicc_type BL then
      if (n_val XOR v_val) = 1 then 1 else 0
    else if instr_name = bicc_type BGU then
      if (c_val = 0  z_val = 0) then 1 else 0
    else if instr_name = bicc_type BLEU then
      if (c_val = 1  z_val = 1) then 1 else 0
    else if instr_name = bicc_type BCC then
      if c_val = 0 then 1 else 0
    else if instr_name = bicc_type BCS then
      if c_val = 1 then 1 else 0
    else if instr_name = bicc_type BNEG then
      if n_val = 1 then 1 else 0
    else if instr_name = bicc_type BA then 1
    else if instr_name = bicc_type BN then 0
    else if instr_name = bicc_type BPOS then
      if n_val = 0 then 1 else 0
    else if instr_name = bicc_type BVC then
      if v_val = 0 then 1 else 0
    else if instr_name = bicc_type BVS then
      if v_val = 1 then 1 else 0
    else -1
"

definition branch_instr_sub1:: "sparc_operation  ('a) sparc_state  int"
where "branch_instr_sub1 instr_name s 
  let n_val = get_icc_N ((cpu_reg s) PSR);
      z_val = get_icc_Z ((cpu_reg s) PSR);
      v_val = get_icc_V ((cpu_reg s) PSR);
      c_val = get_icc_C ((cpu_reg s) PSR)
  in
  eval_icc instr_name n_val z_val v_val c_val"

text ‹Operational semantics for Branching insturctions. 
        Return exception or a bool value for annulment. 
        If the bool value is 1, then the delay instruciton 
        is not executed, otherwise the delay instruction
        is executed.›
definition branch_instr::"instruction  ('a,unit) sparc_state_monad"
where "branch_instr instr 
  let instr_name = fst instr;
      op_list = snd instr;
      disp22 = get_operand_w22 (op_list!1);
      flaga = get_operand_flag (op_list!0)
  in
  do
    icc_val  gets( λs. (branch_instr_sub1 instr_name s));
    npc_val  gets (λs. (cpu_reg_val nPC s));
    pc_val  gets (λs. (cpu_reg_val PC s));
    write_cpu npc_val PC;    
    if icc_val = 1 then 
      do
        write_cpu (pc_val + (sign_ext24 (((ucast(disp22))::word24) << 2))) nPC;
        if (instr_name = bicc_type BA)  (flaga = 1) then 
          do
            set_annul True;
            return ()
          od
        else
          return ()
      od
    else ― ‹icc_val = 0›
      do
        write_cpu (npc_val + 4) nPC;
        if flaga = 1 then
          do                
            set_annul True;
            return ()
          od
        else return ()
      od
  od"

text ‹Operational semantics for NOP›
definition nop_instr::"instruction  ('a,unit) sparc_state_monad"
where "nop_instr instr  return ()"

text ‹Operational semantics for SETHI›
definition sethi_instr::"instruction  ('a::len,unit) sparc_state_monad"
where "sethi_instr instr 
  let op_list = snd instr;
      imm22 = get_operand_w22 (op_list!0); 
      rd = get_operand_w5 (op_list!1)
  in
  if rd  0 then
    do
      curr_win  get_curr_win();
      write_reg (((ucast(imm22))::word32) << 10) curr_win rd;
      return ()
    od
  else return ()
"

text ‹
  Get operand2› based on the flag i›, rs1›, rs2›, and simm13›.
  If i = 0› then operand2 = r[rs2]›,
  else operand2 = sign_ext13(simm13)›.
  op_list› should be [i,rs1,rs2,…]› or [i,rs1,simm13,…]›.
›
definition get_operand2::"inst_operand list  ('a::len) sparc_state
   virtua_address"
where "get_operand2 op_list s 
  let flagi = get_operand_flag (op_list!0);
      curr_win = ucast (get_CWP (cpu_reg_val PSR s))
  in
  if flagi = 0 then
    let rs2 = get_operand_w5 (op_list!2);
        rs2_val = user_reg_val curr_win rs2 s
    in rs2_val
  else
    let ext_simm13 = sign_ext13 (get_operand_simm13 (op_list!2)) in
    ext_simm13
"

text ‹
  Get operand2_val› based on the flag i›, rs1›, rs2›, and simm13›.
  If i = 0› then operand2_val = uint r[rs2]›,
  else operand2_val = sint sign_ext13(simm13)›.
  op_list› should be [i,rs1,rs2,…]› or [i,rs1,simm13,…]›.
›
definition get_operand2_val::"inst_operand list  ('a::len) sparc_state  int"
where "get_operand2_val op_list s 
  let flagi = get_operand_flag (op_list!0);
      curr_win = ucast (get_CWP (cpu_reg_val PSR s))
  in
  if flagi = 0 then
    let rs2 = get_operand_w5 (op_list!2);
        rs2_val = user_reg_val curr_win rs2 s
    in sint rs2_val
  else
    let ext_simm13 = sign_ext13 (get_operand_simm13 (op_list!2)) in
    sint ext_simm13
"

text ‹
  Get the address based on the flag i›, rs1›, rs2›, and simm13›.
  If i = 0› then addr = r[rs1] + r[rs2]›,
  else addr = r[rs1] + sign_ext13(simm13)›.
  op_list› should be [i,rs1,rs2,…]› or [i,rs1,simm13,…]›.
›
definition get_addr::"inst_operand list  ('a::len) sparc_state  virtua_address"
where "get_addr op_list s 
  let rs1 = get_operand_w5 (op_list!1);
      curr_win = ucast (get_CWP (cpu_reg_val PSR s));
      rs1_val = user_reg_val curr_win rs1 s;
      op2 = get_operand2 op_list s
  in
  (rs1_val + op2)
"

text ‹Operational semantics for JMPL›
definition jmpl_instr::"instruction  ('a::len,unit) sparc_state_monad"
where "jmpl_instr instr 
  let op_list = snd instr;
      rd = get_operand_w5 (op_list!3)      
  in
  do
    curr_win  get_curr_win();
    jmp_addr  gets (λs. (get_addr op_list s));
    if ((AND) jmp_addr 0b00000000000000000000000000000011)  0 then
      do
        raise_trap mem_address_not_aligned;
        return ()
      od
    else
      do
        rd_next_val  gets (λs. (if rd  0 then
                                    (cpu_reg_val PC s)
                                  else 
                                    user_reg_val curr_win rd s));
        write_reg rd_next_val curr_win rd;
        npc_val  gets (λs. (cpu_reg_val nPC s));
        write_cpu npc_val PC;
        write_cpu jmp_addr nPC;
        return ()
      od
  od"

text ‹Operational semantics for RETT›
definition rett_instr :: "instruction  ('a::len,unit) sparc_state_monad"
where "rett_instr instr 
  let op_list = snd instr in
  do
    psr_val  gets (λs. (cpu_reg_val PSR s));
    curr_win  gets (λs. (get_CWP (cpu_reg_val PSR s)));
    new_cwp  gets (λs. (word_of_int (((uint curr_win) + 1) mod NWINDOWS)));
    new_cwp_int  gets (λs. ((uint curr_win) + 1) mod NWINDOWS);
    addr  gets (λs. (get_addr op_list s));
    et_val  gets (λs. ((ucast (get_ET psr_val))::word1));
    s_val  gets (λs. ((ucast (get_S psr_val))::word1));
    ps_val  gets (λs. ((ucast (get_PS psr_val))::word1));
    wim_val  gets (λs. (cpu_reg_val WIM s));
    npc_val  gets (λs. (cpu_reg_val nPC s));
    if et_val = 1 then
      if s_val = 0 then 
        do
          raise_trap privileged_instruction;
          return ()
        od
      else
        do
          raise_trap illegal_instruction;
          return ()
        od
    else if s_val = 0 then
      do 
        write_cpu_tt (0b00000011::word8);
        set_exe_mode False;
        set_err_mode True;
        raise_trap privileged_instruction;
        fail ()
      od
    else if (get_WIM_bit (nat new_cwp_int) wim_val)  0 then
      do
        write_cpu_tt (0b00000110::word8);
        set_exe_mode False;
        set_err_mode True;
        raise_trap window_underflow;
        fail ()
      od
    else if ((AND) addr (0b00000000000000000000000000000011::word32))  0 then
      do
        write_cpu_tt (0b00000111::word8);
        set_exe_mode False;
        set_err_mode True;
        raise_trap mem_address_not_aligned;
        fail ()
      od
    else
      do
        write_cpu npc_val PC;
        write_cpu addr nPC;
        new_psr_val  gets (λs. (update_PSR_rett new_cwp 1 ps_val psr_val));
        write_cpu new_psr_val PSR;
        return ()
      od
  od"

definition save_retore_sub1 :: "word32  word5  word5  ('a::len,unit) sparc_state_monad"
where "save_retore_sub1 result new_cwp rd 
  do
  psr_val  gets (λs. (cpu_reg_val PSR s));
  new_psr_val  gets (λs. (update_CWP new_cwp psr_val));
  write_cpu new_psr_val PSR; ― ‹Change CWP› to the new window value.›
  write_reg result (ucast new_cwp) rd; ― ‹Write result in rd› of the new window.›
  return ()
  od"

text ‹Operational semantics for SAVE and RESTORE.›
definition save_restore_instr :: "instruction  ('a::len,unit) sparc_state_monad"
where "save_restore_instr instr 
  let instr_name = fst instr;
      op_list = snd instr;
      rd = get_operand_w5 (op_list!3)
  in
  do
    psr_val  gets (λs. (cpu_reg_val PSR s));
    curr_win  get_curr_win();
    wim_val  gets (λs. (cpu_reg_val WIM s));
    if instr_name = ctrl_type SAVE then 
      do
        new_cwp  gets (λs. ((word_of_int (((uint curr_win) - 1) mod NWINDOWS)))::word5);
        if (get_WIM_bit (unat new_cwp) wim_val)  0 then 
          do
            raise_trap window_overflow;
            return ()
          od
        else
          do
            result  gets (λs. (get_addr op_list s)); ― ‹operands are from the old window.›
            save_retore_sub1 result new_cwp rd
          od
      od
    else ― ‹instr_name = RESTORE›
      do
        new_cwp  gets (λs. ((word_of_int (((uint curr_win) + 1) mod NWINDOWS)))::word5);
        if (get_WIM_bit (unat new_cwp) wim_val)  0 then 
          do
            raise_trap window_underflow;
            return ()
          od
        else
          do
            result  gets (λs. (get_addr op_list s)); ― ‹operands are from the old window.›
            save_retore_sub1 result new_cwp rd
          od
      od
  od"

definition flush_cache_line :: "word32  ('a,unit) sparc_state_monad"
where "flush_cache_line  undefined"

definition flush_Ibuf_and_pipeline :: "word32  ('a,unit) sparc_state_monad"
where "flush_Ibuf_and_pipeline  undefined"

text ‹Operational semantics for FLUSH. 
        Flush the all the caches.›
definition flush_instr :: "instruction  ('a::len,unit) sparc_state_monad"
where "flush_instr instr 
  let op_list = snd instr in
  do
    addr  gets (λs. (get_addr op_list s));
    modify (λs. (flush_cache_all s));
    ⌦‹flush_cache_line(addr);›
    ⌦‹flush_Ibuf_and_pipeline(addr);›
    return ()
  od"

text ‹Operational semantics for read state register instructions. 
        We do not consider RDASR here.›
definition read_state_reg_instr :: "instruction  ('a::len,unit) sparc_state_monad"
where "read_state_reg_instr instr  
  let instr_name = fst instr;
      op_list = snd instr;
      rs1 = get_operand_w5 (op_list!0);
      rd = get_operand_w5 (op_list!1)
  in
  do  
    curr_win  get_curr_win();
    psr_val  gets (λs. (cpu_reg_val PSR s));
    s_val  gets (λs. (get_S psr_val));
    if (instr_name  {sreg_type RDPSR,sreg_type RDWIM,sreg_type RDTBR}  
        (instr_name = sreg_type RDASR  privileged_ASR rs1)) 
        ((ucast s_val)::word1) = 0 then
      do
        raise_trap privileged_instruction;
        return ()
      od
    else if illegal_instruction_ASR rs1 then 
      do