# 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

(*
*
* This software may be distributed and modified according to the terms of
* the BSD 2-Clause license. Note that NO WARRANTY is provided.
*
* Author: Zhe Hou, David Sanan.
*)

section ‹SPARC V8 architecture CPU model›
theory Sparc_Types
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 offset = word12

type_synonym table_entry = word8

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

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_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 ≡ v⦇annul := b⦈"

definition write_reset_trap :: "bool ⇒ sparc_state_var ⇒ sparc_state_var"
where "write_reset_trap b v ≡ v⦇resett := b⦈"

definition write_exe_mode :: "bool ⇒ sparc_state_var ⇒ sparc_state_var"
where "write_exe_mode b v ≡ v⦇exe := b⦈"

definition write_reset_mode :: "bool ⇒ sparc_state_var ⇒ sparc_state_var"
where "write_reset_mode b v ≡ v⦇reset := b⦈"

definition write_err_mode :: "bool ⇒ sparc_state_var ⇒ sparc_state_var"
where "write_err_mode b v ≡ v⦇err := b⦈"

definition write_ticc_trap_type :: "word7 ⇒ sparc_state_var ⇒ sparc_state_var"
where "write_ticc_trap_type w v ≡ v⦇ticc := w⦈"

definition write_interrupt_level :: "word3 ⇒ sparc_state_var ⇒ sparc_state_var"
where "write_interrupt_level w v ≡ v⦇itrpt_lvl := w⦈"

definition write_store_barrier_pending :: "bool ⇒ sparc_state_var ⇒ sparc_state_var"
where "write_store_barrier_pending b v ≡ v⦇st_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:
▪ 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
▪ 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
▪ Return from Trap Instruction
▪ Trap on Integer Condition Codes 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.›
| LDUB     ― ‹Load Unsigned Byte›
| LDUBA    ― ‹Load Unsigned Byte from Alternate space›
| LDUH     ― ‹Load Unsigned Halfword›
| LDA      ― ‹Load Word from Alternate space›
| 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 =
| 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›
| 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 =
| 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›
| 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
| 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
|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

(*
*
* This software may be distributed and modified according to the terms of
* the BSD 2-Clause license. Note that NO WARRANTY is provided.
*
* @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'"

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 (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


(*
*
* This software may be distributed and modified according to the terms of
* the BSD 2-Clause license. Note that NO WARRANTY is provided.
*
* @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"*)

imports "../Lib"
begin

text ‹

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

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,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 ⇒
"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 ⇒
"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)

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 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

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
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 ⇒
where
"whenE P f ≡ if P then f else returnOk ()"

definition
unlessE :: "bool ⇒ ('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"

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"

text ‹Associativity of @{const bindE}:›
lemma bindE_assoc:
"(m >>=E f) >>=E g = m >>=E (λx. f x >>=E g)"
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)"

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"

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
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
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
definition
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
where
"sequenceE_x xs ≡ foldr (λx y. doE _ ← x; y odE) xs (returnOk ())"

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

definition
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 ⇒
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 ‹
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) ⇒
("_ <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 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"

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
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


(*
*
* This software may be distributed and modified according to the terms of
* the BSD 2-Clause license. Note that NO WARRANTY is provided.
*
* @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
*)

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 (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 (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'"

lemma unless_apply_cong[fundef_cong]:
"⟦ C = C'; s = s'; ¬ C' ⟹ m s' = m' s' ⟧ ⟹ unlessE C m s = unlessE C' m' s'"

lemma whenE_apply_cong[fundef_cong]:
"⟦ C = C'; s = s'; C' ⟹ m s' = m' s' ⟧ ⟹ whenE C m s = whenE C' m' s'"

lemma unlessE_apply_cong[fundef_cong]:
"⟦ C = C'; s = s'; ¬ C' ⟹ m s' = m' s' ⟧ ⟹ unlessE C m s = unlessE C' m' s'"

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 ()"

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

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)"

end


# Theory RegistersOps

section‹Register Operations›
theory RegistersOps
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
≡ 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›
›
definition get_field_from_word_a_a:: "'a::len word ⇒ nat ⇒ nat ⇒ 'a::len word"
where

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
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

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)
"

where
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_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"
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)
Some ((registers mmu_state) FAR)
else None"

definition mmu_reg_mod:: "MMU_state ⇒ virtua_address ⇒ machine_word ⇒
MMU_state option" where
if addr = 0x000 then ― ‹MMU control register›
Some (mmu_state⦇registers := (registers mmu_state)(CR := w)⦈)
else if addr = 0x100 then ― ‹Context pointer register›
Some (mmu_state⦇registers := (registers mmu_state)(CTP := w)⦈)
else if addr = 0x200 then ― ‹Context register›
Some (mmu_state⦇registers := (registers mmu_state)(CNR := w)⦈)
else if addr = 0x300 then ― ‹Fault status register›
Some (mmu_state⦇registers := (registers mmu_state)(FTSR := w)⦈)
Some (mmu_state⦇registers := (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.
›

where
≡ ((ucast (ctp >> 2)) << 6) + (ucast cnr << 2)"

text‹Get the context table phys address from the MMU registers›
where
≡ 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
let asi8 = word_of_int 8;
in
if r1 = None then
else r1
"

exception that the last two bits are 0's.
That is, read the data from
definition mem_context_val_w32 :: "asi_type ⇒ phys_address ⇒
mem_context ⇒ word32 option"
where
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.
›

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_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
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 ⇒
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

(*
*
* This software may be distributed and modified according to the terms of
* the BSD 2-Clause license. Note that NO WARRANTY is provided.
*
* Author: Zhe Hou, David Sanan.
*)

section ‹SPARC V8 state model›
theory Sparc_State
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.
›

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 ≡
state⦇cpu_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 = state⦇user_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' = state⦇user_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' = state⦇user_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
state⦇user_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 ≡ state⦇sys_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

definition mem_val:: "asi_type ⇒ phys_address ⇒
('a) sparc_state ⇒ mem_val_type option"
where
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
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
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
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
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 = state⦇mem := (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
state1⦇mem := (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
state1⦇mem := (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 = state⦇mem := (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 = state1⦇mem := (mem state1)
(asi9 := ((mem state1) asi9)(addr := None))⦈;
state3 = state2⦇mem := (mem state2)
(asi10 := ((mem state2) asi10)(addr := None))⦈;
state4 = state3⦇mem := (mem state3)
(asi11 := ((mem state3) asi11)(addr := None))⦈
in
state4
else if (uint asi) = 9 then
let state2 = state1⦇mem := (mem state1)
(asi8 := ((mem state1) asi8)(addr := None))⦈;
state3 = state2⦇mem := (mem state2)
(asi10 := ((mem state2) asi10)(addr := None))⦈;
state4 = state3⦇mem := (mem state3)
(asi11 := ((mem state3) asi11)(addr := None))⦈
in
state4
else if (uint asi) = 10 then
let state2 = state1⦇mem := (mem state1)
(asi9 := ((mem state1) asi9)(addr := None))⦈;
state3 = state2⦇mem := (mem state2)
(asi8 := ((mem state2) asi8)(addr := None))⦈;
state4 = state3⦇mem := (mem state3)
(asi11 := ((mem state3) asi11)(addr := None))⦈
in
state4
else if (uint asi) = 11 then
let state2 = state1⦇mem := (mem state1)
(asi9 := ((mem state1) asi9)(addr := None))⦈;
state3 = state2⦇mem := (mem state2)
(asi10 := ((mem state2) asi10)(addr := None))⦈;
state4 = state3⦇mem := (mem state3)
(asi8 := ((mem state3) asi8)(addr := None))⦈
in
state4
else state1
"

exception that the last two bits are 0's.
That is, read the data from
definition mem_val_w32 :: "asi_type ⇒ phys_address ⇒
('a) sparc_state ⇒ word32 option"
where
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 ‹
‹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
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
else state;
s1 = if (((AND) byte_mask (0b0100::word4)) >> 2) = 1 then
else s0;
s2 = if (((AND) byte_mask (0b0010::word4)) >> 1) = 1 then
else s1;
s3 = if ((AND) byte_mask (0b0001::word4)) = 1 then
else s2
in
s3
"

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

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 ≡
state⦇cache := ((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 ≡
state⦇cache := ((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
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
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
"

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)))
"

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)))
"

word4 ⇒ ('a) sparc_state"
where
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
"

word4 ⇒ ('a) sparc_state"
where
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 ≡ state⦇cache := ((cache state)⦇dcache := empty_cache⦈)⦈"

definition flush_instr_cache:: "('a) sparc_state ⇒ ('a) sparc_state" where
"flush_instr_cache state ≡ state⦇cache := ((cache state)⦇icache := empty_cache⦈)⦈"

definition flush_cache_all:: "('a) sparc_state ⇒ ('a) sparc_state" where
"flush_cache_all state ≡ state⦇cache := ((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
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
s⦇dwrite := 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
s⦇dwrite := 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 ≡ s⦇state_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 ≡ s⦇state_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 ≡ s⦇state_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 ≡ s⦇state_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 ≡ s⦇state_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 ≡ s⦇state_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 ≡ s⦇state_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 ≡
s⦇state_var := write_store_barrier_pending w (state_var s)⦈"

definition pb_block_ldst_byte_val :: "virtua_address ⇒ ('a) sparc_state
⇒ bool"

definition pb_block_ldst_byte_mod :: "virtua_address ⇒ bool ⇒
('a) sparc_state ⇒ ('a) sparc_state"
where "pb_block_ldst_byte_mod add b s ≡
s⦇state_var := ((state_var s)
⦇atm_ldst_byte := (atm_ldst_byte (state_var s))(add := b)⦈)⦈"

add mod 4 represents the current word.›
definition pb_block_ldst_word_val :: "virtua_address ⇒ ('a) sparc_state
⇒ bool"

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 ≡
s⦇state_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 ≡ s⦇traps := (traps s) ∪ {t}⦈"

definition emp_trap_set :: "('a) sparc_state ⇒ ('a) sparc_state"
where "emp_trap_set s ≡ s⦇traps := {}⦈"

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

text ‹The ‹memory_read› interface that conforms with the SPARCv8 manual.›
('a) sparc_state ⇒
((word32 option) × ('a) sparc_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.›
if r1 = None then
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)
(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,›
― ‹because performance is not an issue here.›
― ‹Thus we directly read from memory and update the cache.›
case data of
|None ⇒ (None, state)
else ― ‹Cache is disabled. Just read from memory.›
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,›
― ‹because performance is not an issue here.›
― ‹Thus we directly read from memory and update the cache.›
case data of
|None ⇒ (None, state)
else ― ‹Cache is disabled. Just read from memory.›
― ‹We don't access instruction cache tag. i.e., ‹asi = 12›.›
else if asi_int = 13 then ― ‹Read instruction cache data.›
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.›
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.›
else if asi_int = 28 then ― ‹MMU bypass.›
― ‹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"

text ‹Check if an address is used in ASI 9 or 11.›
where
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
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›.›
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)
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.›
else if asi_int ∈ {10,11} then ― ‹Access data memory.›
― ‹Write to memory. LEON3 does write-through. Both cache and the memory are updated.›
― ‹We don't access instruction cache tag. i.e., ‹asi = 12›.›
else if asi_int = 13 then ― ‹Write instruction cache data.›
― ‹We don't access data cache tag. i.e., asi = 14.›
else if asi_int = 15 then ― ‹Write data cache data.›
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 (state⦇mmu := mmus⦈)
|None ⇒ None
else if asi_int = 28 then ― ‹MMU bypass.›
― ‹Append 0000 in front of addr.›
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
case result of
None ⇒ None
| Some s1 ⇒ Some (store_barrier_pending_mod False s1)"

text ‹monad for sequential operations over the register representation›

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 ⇒
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
return ()
od"

end



# Theory Sparc_Instruction

(*
*
* This software may be distributed and modified according to the terms of
* the BSD 2-Clause license. Note that NO WARRANTY is provided.
*
* 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}
›
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 ≡
uint (((AND) mask_op2 w) >> 22)"

definition get_op3::"word32 ⇒ int"
where "get_op3 w ≡
uint (((AND) mask_op3 w) >> 19)"

definition get_disp30::"word32 ⇒ int"
where "get_disp30 w ≡

definition get_a::"word32 ⇒ int"
where "get_a w ≡
uint (((AND) mask_a w) >> 29)"

definition get_cond::"word32 ⇒ int"
where "get_cond w ≡
uint (((AND) mask_cond w) >> 25)"

definition get_disp_imm22::"word32 ⇒ int"
where "get_disp_imm22 w ≡

definition get_rd::"word32 ⇒ int"
where "get_rd w ≡
uint (((AND) mask_rd w) >> 25)"

definition get_rs1::"word32 ⇒ int"
where "get_rs1 w ≡
uint (((AND) mask_rs1 w) >> 14)"

definition get_i::"word32 ⇒ int"
where "get_i w ≡
uint (((AND) mask_i w) >> 13)"

definition get_opf::"word32 ⇒ int"
where "get_opf w ≡
uint (((AND) mask_opf w) >> 5)"

definition get_rs2::"word32 ⇒ int"
where "get_rs2 w ≡

definition get_simm13::"word32 ⇒ int"
where "get_simm13 w ≡

definition get_asi::"word32 ⇒ int"
where "get_asi w ≡
uint (((AND) mask_asi w) >> 5)"

definition get_trap_cond:: "word32 ⇒ int"
where "get_trap_cond w ≡
uint (((AND) mask_cond w) >> 25)"

definition get_trap_imm7:: "word32 ⇒ int"
where "get_trap_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]››
(W5 (word_of_int rs1)),
(Simm13 (word_of_int simm13)),
(W5 (word_of_int rd))])
else ― ‹Operant list is ‹[i,rs1,rs2,rd]››
(W5 (word_of_int rs1)),
(W5 (word_of_int rs2)),
(W5 (word_of_int rd))])
else if op3 = uint(0b011001::word6) then ― ‹‹LDSBA››
(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]››
(W5 (word_of_int rs1)),
(Simm13 (word_of_int simm13)),
(W5 (word_of_int rd))])
else ― ‹Operant list is ‹[i,rs1,rs2,rd]››
(W5 (word_of_int rs1)),
(W5 (word_of_int rs2)),
(W5 (word_of_int rd))])
else if op3 = uint(0b011010::word6) then ― ‹‹LDSHA››
(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]››
(W5 (word_of_int rs1)),
(Simm13 (word_of_int simm13)),
(W5 (word_of_int rd))])
else ― ‹Operant list is ‹[i,rs1,rs2,rd]››
(W5 (word_of_int rs1)),
(W5 (word_of_int rs2)),
(W5 (word_of_int rd))])
else if op3 = uint(0b010001::word6) then ― ‹‹LDUBA››
(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]››
(W5 (word_of_int rs1)),
(Simm13 (word_of_int simm13)),
(W5 (word_of_int rd))])
else ― ‹Operant list is ‹[i,rs1,rs2,rd]››
(W5 (word_of_int rs1)),
(W5 (word_of_int rs2)),
(W5 (word_of_int rd))])
else if op3 = uint(0b010010::word6) then ― ‹‹LDUHA››
(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]››
(W5 (word_of_int rs1)),
(Simm13 (word_of_int simm13)),
(W5 (word_of_int rd))])
else ― ‹Operant list is ‹[i,rs1,rs2,rd]››
(W5 (word_of_int rs1)),
(W5 (word_of_int rs2)),
(W5 (word_of_int rd))])
else if op3 = uint(0b010000::word6) then ― ‹‹LDA››
(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]››
(W5 (word_of_int rs1)),
(Simm13 (word_of_int simm13)),
(W5 (word_of_int rd))])
else ― ‹Operant list is ‹[i,rs1,rs2,rd]››
(W5 (word_of_int rs1)),
(W5 (word_of_int rs2)),
(W5 (word_of_int rd))])
else if op3 = uint(0b010011::word6) then ― ‹‹LDDA››
(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]››
(W5 (word_of_int rs1)),
(Simm13 (word_of_int simm13)),
(W5 (word_of_int rd))])
else ― ‹Operant list is ‹[i,rs1,rs2,rd]››
(W5 (word_of_int rs1)),
(W5 (word_of_int rs2)),
(W5 (word_of_int rd))])
else if op3 = uint(0b011101::word6) then ― ‹‹LDSTUBA››
(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]››
(W5 (word_of_int rs1)),
(Simm13 (word_of_int simm13)),
(W5 (word_of_int rd))])
else ― ‹Operant list is ‹[i,rs1,rs2,rd]››
(W5 (word_of_int rs1)),
(W5 (word_of_int rs2)),
(W5 (word_of_int rd))])
else if op3 = uint(0b010101::word6) then ― ‹‹STBA››
(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]››
(W5 (word_of_int rs1)),
(Simm13 (word_of_int simm13)),
(W5 (word_of_int rd))])
else ― ‹Operant list is ‹[i,rs1,rs2,rd]››
(W5 (word_of_int rs1)),
(W5 (word_of_int rs2)),
(W5 (word_of_int rd))])
else if op3 = uint(0b010110::word6) then ― ‹‹STHA››
(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]››
(W5 (word_of_int rs1)),
(Simm13 (word_of_int simm13)),
(W5 (word_of_int rd))])
else ― ‹Operant list is ‹[i,rs1,rs2,rd]››
(W5 (word_of_int rs1)),
(W5 (word_of_int rs2)),
(W5 (word_of_int rd))])
else if op3 = uint(0b010100::word6) then ― ‹‹STA››
(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]››
(W5 (word_of_int rs1)),
(Simm13 (word_of_int simm13)),
(W5 (word_of_int rd))])
else ― ‹Operant list is ‹[i,rs1,rs2,rd]››
(W5 (word_of_int rs1)),
(W5 (word_of_int rs2)),
(W5 (word_of_int rd))])
else if op3 = uint(0b010111::word6) then ― ‹‹STDA››
(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]››
(W5 (word_of_int rs1)),
(Simm13 (word_of_int simm13)),
(W5 (word_of_int rd))])
else ― ‹Operant list is ‹[i,rs1,rs2,rd]››
(W5 (word_of_int rs1)),
(W5 (word_of_int rs2)),
(W5 (word_of_int rd))])
else if op3 = uint(0b011111::word6) then ― ‹‹SWAPA››
(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››
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]››
(W5 (word_of_int rs1)),
(W5 (word_of_int rs2))])
else ― ‹return ‹[i,rs1,simm13]››
(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]››
(W5 (word_of_int rs1)),
(W5 (word_of_int rs2)),
(W5 (word_of_int rd))])
else ― ‹return ‹[i,rs1,simm13,rd]››
(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]››
(W5 (word_of_int rs1)),
(W5 (word_of_int rs2)),
(W5 (word_of_int rd))])
else ― ‹return ‹[i,rs1,simm13,rd]››
(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]››
(W5 (word_of_int rs1)),
(W5 (word_of_int rs2)),
(W5 (word_of_int rd))])
else ― ‹return ‹[i,rs1,simm13,rd]››
(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]››
(W5 (word_of_int rs1)),
(W5 (word_of_int rs2)),
(W5 (word_of_int rd))])
else ― ‹return ‹[i,rs1,simm13,rd]››
(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]››
(W5 (word_of_int rs1)),
(W5 (word_of_int rs2)),
(W5 (word_of_int rd))])
else ― ‹return ‹[i,rs1,simm13,rd]››
(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]››
(W5 (word_of_int rs1)),
(W5 (word_of_int rs2)),
(W5 (word_of_int rd))])
else ― ‹return ‹[i,rs1,simm13,rd]››
(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›
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;
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.›
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›
where "nop_instr instr ≡ return ()"

text ‹Operational semantics for SETHI›
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
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,…]›.
›
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›
where "jmpl_instr instr ≡
let op_list = snd instr;
rd = get_operand_w5 (op_list!3)
in
do
curr_win ← get_curr_win();
if ((AND) jmp_addr 0b00000000000000000000000000000011) ≠ 0 then
do
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;
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);
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;
fail ()
od
else
do
write_cpu npc_val PC;
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
modify (λs. (flush_cache_all s));
return ()
od"

text ‹Operational semantics for read state register instructions.
We do not consider RDASR here.›
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