diff options
author | Robert Norton <rmn30@cam.ac.uk> | 2019-09-04 17:28:22 +0100 |
---|---|---|
committer | Robert Norton <rmn30@cam.ac.uk> | 2019-09-04 17:28:22 +0100 |
commit | e918e17c081bc24bbf2ae213c211b9dabc276324 (patch) | |
tree | 7621be42dcb86adfaf59f4351498dc7325f6bed2 /prover_snapshots/hol4/RV32/riscv_typesScript.sml | |
parent | 50033a227e89d679cd42b070e7e096586275357c (diff) | |
parent | 3d75de27c854072b82493a73e01c69d27624bf94 (diff) | |
download | sail-riscv-vmem_ext.zip sail-riscv-vmem_ext.tar.gz sail-riscv-vmem_ext.tar.bz2 |
Merge remote-tracking branch 'origin/master' into vmem_ext.vmem_ext
Diffstat (limited to 'prover_snapshots/hol4/RV32/riscv_typesScript.sml')
-rw-r--r-- | prover_snapshots/hol4/RV32/riscv_typesScript.sml | 2208 |
1 files changed, 2208 insertions, 0 deletions
diff --git a/prover_snapshots/hol4/RV32/riscv_typesScript.sml b/prover_snapshots/hol4/RV32/riscv_typesScript.sml new file mode 100644 index 0000000..14b1a48 --- /dev/null +++ b/prover_snapshots/hol4/RV32/riscv_typesScript.sml @@ -0,0 +1,2208 @@ +(*Generated by Lem from generated_definitions/lem/RV32/riscv_types.lem.*) +open HolKernel Parse boolLib bossLib; +open lem_pervasives_extraTheory sail2_instr_kindsTheory sail2_valuesTheory sail2_prompt_monadTheory sail2_operators_mwordsTheory sail2_promptTheory sail2_stringTheory; + +val _ = numLib.prefer_num(); + + + +val _ = new_theory "riscv_types" + +(*Generated by Sail from riscv.*) +(*open import Pervasives_extra*) +(*open import Sail2_instr_kinds*) +(*open import Sail2_values*) +(*open import Sail2_string*) +(*open import Sail2_operators_mwords*) +(*open import Sail2_prompt_monad*) +(*open import Sail2_prompt*) + + +val _ = type_abbrev((* 'n *) "bits" , ``: 'n words$word``); + +val _ = Hol_datatype ` + regfp = + RFull of (string) + | RSlice of ((string # ii # ii)) + | RSliceBit of ((string # ii)) + | RField of ((string # string))`; + + + + +val _ = type_abbrev( "regfps" , ``: regfp list``); + +val _ = Hol_datatype ` + niafp = + NIAFP_successor of (unit) + | NIAFP_concrete_address of ( 64 bits) + | NIAFP_indirect_address of (unit)`; + + + + +val _ = type_abbrev( "niafps" , ``: niafp list``); + +val _ = Hol_datatype ` + diafp = DIAFP_none of (unit) | DIAFP_concrete of ( 64 bits) | DIAFP_reg of (regfp)`; + + + + + + + + + + + + + + + + + + + + +val _ = type_abbrev( "xlenbits" , ``: 32 bits``); + +val _ = type_abbrev( "mem_meta" , ``: unit``); + + + +val _ = type_abbrev( "half" , ``: 16 bits``); + +val _ = type_abbrev( "word" , ``: 32 bits``); + +val _ = type_abbrev( "regidx" , ``: 5 bits``); + +val _ = type_abbrev( "cregidx" , ``: 3 bits``); + +val _ = type_abbrev( "csreg" , ``: 12 bits``); + +val _ = type_abbrev((* 'n *) "regno" , ``: int``); + +val _ = type_abbrev( "opcode" , ``: 7 bits``); + +val _ = type_abbrev( "imm12" , ``: 12 bits``); + +val _ = type_abbrev( "imm20" , ``: 20 bits``); + +val _ = type_abbrev( "amo" , ``: 1 bits``); + +val _ = Hol_datatype ` + Architecture = RV32 | RV64 | RV128`; + + + + +val _ = type_abbrev( "arch_xlen" , ``: 2 bits``); + +val _ = type_abbrev( "priv_level" , ``: 2 bits``); + +val _ = Hol_datatype ` + Privilege = User | Supervisor | Machine`; + + + + +val _ = Hol_datatype ` + amoop = AMOSWAP | AMOADD | AMOXOR | AMOAND | AMOOR | AMOMIN | AMOMAX | AMOMINU | AMOMAXU`; + + + + +val _ = Hol_datatype ` + bop = RISCV_BEQ | RISCV_BNE | RISCV_BLT | RISCV_BGE | RISCV_BLTU | RISCV_BGEU`; + + + + +val _ = Hol_datatype ` + csrop = CSRRW | CSRRS | CSRRC`; + + + + +val _ = Hol_datatype ` + iop = RISCV_ADDI | RISCV_SLTI | RISCV_SLTIU | RISCV_XORI | RISCV_ORI | RISCV_ANDI`; + + + + +val _ = Hol_datatype ` + rop = + RISCV_ADD + | RISCV_SUB + | RISCV_SLL + | RISCV_SLT + | RISCV_SLTU + | RISCV_XOR + | RISCV_SRL + | RISCV_SRA + | RISCV_OR + | RISCV_AND`; + + + + +val _ = Hol_datatype ` + ropw = RISCV_ADDW | RISCV_SUBW | RISCV_SLLW | RISCV_SRLW | RISCV_SRAW`; + + + + +val _ = Hol_datatype ` + sop = RISCV_SLLI | RISCV_SRLI | RISCV_SRAI`; + + + + +val _ = Hol_datatype ` + sopw = RISCV_SLLIW | RISCV_SRLIW | RISCV_SRAIW`; + + + + +val _ = Hol_datatype ` + uop = RISCV_LUI | RISCV_AUIPC`; + + + + +val _ = Hol_datatype ` + word_width = BYTE | HALF | WORD | DOUBLE`; + + + + +val _ = Hol_datatype ` + ast = + UTYPE of (( 20 bits # regidx # uop)) + | RISCV_JAL of (( 21 bits # regidx)) + | RISCV_JALR of (( 12 bits # regidx # regidx)) + | BTYPE of (( 13 bits # regidx # regidx # bop)) + | ITYPE of (( 12 bits # regidx # regidx # iop)) + | SHIFTIOP of (( 6 bits # regidx # regidx # sop)) + | RTYPE of ((regidx # regidx # regidx # rop)) + | LOAD of (( 12 bits # regidx # regidx # bool # word_width # bool # bool)) + | STORE of (( 12 bits # regidx # regidx # word_width # bool # bool)) + | ADDIW of (( 12 bits # regidx # regidx)) + | SHIFTW of (( 5 bits # regidx # regidx # sop)) + | RTYPEW of ((regidx # regidx # regidx # ropw)) + | SHIFTIWOP of (( 5 bits # regidx # regidx # sopw)) + | FENCE of (( 4 bits # 4 bits)) + | FENCE_TSO of (( 4 bits # 4 bits)) + | FENCEI of (unit) + | ECALL of (unit) + | MRET of (unit) + | SRET of (unit) + | EBREAK of (unit) + | WFI of (unit) + | SFENCE_VMA of ((regidx # regidx)) + | LOADRES of ((bool # bool # regidx # word_width # regidx)) + | STORECON of ((bool # bool # regidx # regidx # word_width # regidx)) + | AMO of ((amoop # bool # bool # regidx # regidx # word_width # regidx)) + | C_NOP of (unit) + | C_ADDI4SPN of ((cregidx # 8 bits)) + | C_LW of (( 5 bits # cregidx # cregidx)) + | C_LD of (( 5 bits # cregidx # cregidx)) + | C_SW of (( 5 bits # cregidx # cregidx)) + | C_SD of (( 5 bits # cregidx # cregidx)) + | C_ADDI of (( 6 bits # regidx)) + | C_JAL of ( 11 bits) + | C_ADDIW of (( 6 bits # regidx)) + | C_LI of (( 6 bits # regidx)) + | C_ADDI16SP of ( 6 bits) + | C_LUI of (( 6 bits # regidx)) + | C_SRLI of (( 6 bits # cregidx)) + | C_SRAI of (( 6 bits # cregidx)) + | C_ANDI of (( 6 bits # cregidx)) + | C_SUB of ((cregidx # cregidx)) + | C_XOR of ((cregidx # cregidx)) + | C_OR of ((cregidx # cregidx)) + | C_AND of ((cregidx # cregidx)) + | C_SUBW of ((cregidx # cregidx)) + | C_ADDW of ((cregidx # cregidx)) + | C_J of ( 11 bits) + | C_BEQZ of (( 8 bits # cregidx)) + | C_BNEZ of (( 8 bits # cregidx)) + | C_SLLI of (( 6 bits # regidx)) + | C_LWSP of (( 6 bits # regidx)) + | C_LDSP of (( 6 bits # regidx)) + | C_SWSP of (( 6 bits # regidx)) + | C_SDSP of (( 6 bits # regidx)) + | C_JR of (regidx) + | C_JALR of (regidx) + | C_MV of ((regidx # regidx)) + | C_EBREAK of (unit) + | C_ADD of ((regidx # regidx)) + | MUL of ((regidx # regidx # regidx # bool # bool # bool)) + | DIV0 of ((regidx # regidx # regidx # bool)) + | REM of ((regidx # regidx # regidx # bool)) + | MULW of ((regidx # regidx # regidx)) + | DIVW of ((regidx # regidx # regidx # bool)) + | REMW of ((regidx # regidx # regidx # bool)) + | CSR of (( 12 bits # regidx # regidx # bool # csrop)) + | URET of (unit) + | ILLEGAL of (word) + | C_ILLEGAL of (half)`; + + + + +val _ = Hol_datatype ` + Retired = RETIRE_SUCCESS | RETIRE_FAIL`; + + + + +val _ = Hol_datatype ` + AccessType = Read | Write | ReadWrite | Execute`; + + + + +val _ = type_abbrev( "exc_code" , ``: 8 bits``); + +val _ = Hol_datatype ` + InterruptType = + I_U_Software + | I_S_Software + | I_M_Software + | I_U_Timer + | I_S_Timer + | I_M_Timer + | I_U_External + | I_S_External + | I_M_External`; + + + + +val _ = Hol_datatype ` + ExceptionType = + E_Fetch_Addr_Align + | E_Fetch_Access_Fault + | E_Illegal_Instr + | E_Breakpoint + | E_Load_Addr_Align + | E_Load_Access_Fault + | E_SAMO_Addr_Align + | E_SAMO_Access_Fault + | E_U_EnvCall + | E_S_EnvCall + | E_Reserved_10 + | E_M_EnvCall + | E_Fetch_Page_Fault + | E_Load_Page_Fault + | E_Reserved_14 + | E_SAMO_Page_Fault + | E_CHERI`; + + + + +val _ = Hol_datatype ` + exception = Error_not_implemented of (string) | Error_internal_error of (unit)`; + + + + +val _ = type_abbrev( "tv_mode" , ``: 2 bits``); + +val _ = Hol_datatype ` + TrapVectorMode = TV_Direct | TV_Vector | TV_Reserved`; + + + + +val _ = type_abbrev( "ext_status" , ``: 2 bits``); + +val _ = Hol_datatype ` + ExtStatus = Off | Initial | Clean | Dirty`; + + + + +val _ = type_abbrev( "satp_mode" , ``: 4 bits``); + +val _ = Hol_datatype ` + SATPMode = Sbare | Sv32 | Sv39 | Sv48`; + + + + +val _ = type_abbrev( "csrRW" , ``: 2 bits``); + +val _ = type_abbrev( "regtype" , ``: xlenbits``); + +val _ = Hol_datatype ` + Misa = <| Misa_Misa_chunk_0 : 32 words$word |>`; + + + +val _ = Hol_datatype ` + SV48_PTE = <| SV48_PTE_SV48_PTE_chunk_0 : 64 words$word |>`; + + + +val _ = Hol_datatype ` + PTE_Bits = <| PTE_Bits_PTE_Bits_chunk_0 : 8 words$word |>`; + + + +val _ = Hol_datatype ` + Pmpcfg_ent = <| Pmpcfg_ent_Pmpcfg_ent_chunk_0 : 8 words$word |>`; + + + +val _ = Hol_datatype ` + Mstatus = <| Mstatus_Mstatus_chunk_0 : 32 words$word |>`; + + + +val _ = Hol_datatype ` + Sstatus = <| Sstatus_Sstatus_chunk_0 : 32 words$word |>`; + + + +val _ = Hol_datatype ` + Ustatus = <| Ustatus_Ustatus_chunk_0 : 32 words$word |>`; + + + +val _ = Hol_datatype ` + Minterrupts = <| Minterrupts_Minterrupts_chunk_0 : 32 words$word |>`; + + + +val _ = Hol_datatype ` + Sinterrupts = <| Sinterrupts_Sinterrupts_chunk_0 : 32 words$word |>`; + + + +val _ = Hol_datatype ` + Uinterrupts = <| Uinterrupts_Uinterrupts_chunk_0 : 32 words$word |>`; + + + +val _ = Hol_datatype ` + Medeleg = <| Medeleg_Medeleg_chunk_0 : 32 words$word |>`; + + + +val _ = Hol_datatype ` + Sedeleg = <| Sedeleg_Sedeleg_chunk_0 : 32 words$word |>`; + + + +val _ = Hol_datatype ` + Mtvec = <| Mtvec_Mtvec_chunk_0 : 32 words$word |>`; + + + +val _ = Hol_datatype ` + Satp32 = <| Satp32_Satp32_chunk_0 : 32 words$word |>`; + + + +val _ = Hol_datatype ` + Mcause = <| Mcause_Mcause_chunk_0 : 32 words$word |>`; + + + +val _ = Hol_datatype ` + Counteren = <| Counteren_Counteren_chunk_0 : 32 words$word |>`; + + + +val _ = Hol_datatype ` + Satp64 = <| Satp64_Satp64_chunk_0 : 64 words$word |>`; + + + +val _ = Hol_datatype ` + PmpAddrMatchType = OFF | TOR | NA4 | NAPOT`; + + + + +val _ = type_abbrev( "pmp_addr_range" , ``: ((xlenbits # xlenbits))option``); + +val _ = Hol_datatype ` + pmpAddrMatch = PMP_NoMatch | PMP_PartialMatch | PMP_Match`; + + + + +val _ = Hol_datatype ` + pmpMatch = PMP_Success | PMP_Continue | PMP_Fail`; + + + + +val _ = Hol_datatype ` + Ext_FetchAddr_Check = Ext_FetchAddr_OK of (xlenbits) | Ext_FetchAddr_Error of ('a)`; + + + + +val _ = Hol_datatype ` + Ext_ControlAddr_Check = Ext_ControlAddr_OK of (xlenbits) | Ext_ControlAddr_Error of ('a)`; + + + + +val _ = Hol_datatype ` + Ext_DataAddr_Check = Ext_DataAddr_OK of (xlenbits) | Ext_DataAddr_Error of ('a)`; + + + + +val _ = type_abbrev( "ext_fetch_addr_error" , ``: unit``); + +val _ = type_abbrev( "ext_control_addr_error" , ``: unit``); + +val _ = type_abbrev( "ext_data_addr_error" , ``: unit``); + +val _ = type_abbrev( "ext_exception" , ``: unit``); + +val _ = Hol_datatype ` + sync_exception = + <| sync_exception_trap : ExceptionType; + sync_exception_excinfo : xlenbits option; + sync_exception_ext : ext_exception option |>`; + + + +val _ = Hol_datatype ` + interrupt_set = + Ints_Pending of (xlenbits) | Ints_Delegated of (xlenbits) | Ints_Empty of (unit)`; + + + + +val _ = Hol_datatype ` + ctl_result = + CTL_TRAP of (sync_exception) | CTL_SRET of (unit) | CTL_MRET of (unit) | CTL_URET of (unit)`; + + + + +val _ = Hol_datatype ` + MemoryOpResult = MemValue of ('a) | MemException of (ExceptionType)`; + + + + +val _ = Hol_datatype ` + htif_cmd = <| htif_cmd_htif_cmd_chunk_0 : 64 words$word |>`; + + + +val _ = type_abbrev( "pteAttribs" , ``: 8 bits``); + +val _ = Hol_datatype ` + PTW_Error = PTW_Access | PTW_Invalid_PTE | PTW_No_Permission | PTW_Misaligned | PTW_PTE_Update`; + + + + +val _ = type_abbrev( "vaddr32" , ``: 32 bits``); + +val _ = type_abbrev( "paddr32" , ``: 34 bits``); + +val _ = type_abbrev( "pte32" , ``: 32 bits``); + +val _ = type_abbrev( "asid32" , ``: 9 bits``); + +val _ = Hol_datatype ` + SV32_Vaddr = <| SV32_Vaddr_SV32_Vaddr_chunk_0 : 32 words$word |>`; + + + +val _ = Hol_datatype ` + SV48_Vaddr = <| SV48_Vaddr_SV48_Vaddr_chunk_0 : 48 words$word |>`; + + + +val _ = Hol_datatype ` + SV48_Paddr = <| SV48_Paddr_SV48_Paddr_chunk_0 : 56 words$word |>`; + + + +val _ = Hol_datatype ` + SV32_Paddr = <| SV32_Paddr_SV32_Paddr_chunk_0 : 34 words$word |>`; + + + +val _ = Hol_datatype ` + SV32_PTE = <| SV32_PTE_SV32_PTE_chunk_0 : 32 words$word |>`; + + + +val _ = type_abbrev( "paddr64" , ``: 56 bits``); + +val _ = type_abbrev( "pte64" , ``: 64 bits``); + +val _ = type_abbrev( "asid64" , ``: 16 bits``); + +val _ = type_abbrev( "vaddr39" , ``: 39 bits``); + +val _ = Hol_datatype ` + SV39_Vaddr = <| SV39_Vaddr_SV39_Vaddr_chunk_0 : 39 words$word |>`; + + + +val _ = Hol_datatype ` + SV39_Paddr = <| SV39_Paddr_SV39_Paddr_chunk_0 : 56 words$word |>`; + + + +val _ = Hol_datatype ` + SV39_PTE = <| SV39_PTE_SV39_PTE_chunk_0 : 64 words$word |>`; + + + +val _ = type_abbrev( "vaddr48" , ``: 48 bits``); + +val _ = type_abbrev( "pte48" , ``: 64 bits``); + +val _ = Hol_datatype ` + PTW_Result = + PTW_Success of (('paddr # 'pte # 'paddr # ii # bool)) | PTW_Failure of (PTW_Error)`; + + + + +val _ = Hol_datatype ` + TR_Result = TR_Address of ('a_paddr) | TR_Failure of ('b_failure)`; + + + + +val _ = Hol_datatype ` +(* ( 'a_asidlen, 'b_valen, 'c_palen, 'd_ptelen) *) TLB_Entry = + <| TLB_Entry_asid :'a_asidlen bits; + TLB_Entry_global : bool; + TLB_Entry_vAddr :'b_valen bits; + TLB_Entry_pAddr :'c_palen bits; + TLB_Entry_vMatchMask :'b_valen bits; + TLB_Entry_vAddrMask :'b_valen bits; + TLB_Entry_pte :'d_ptelen bits; + TLB_Entry_pteAddr :'c_palen bits; + TLB_Entry_age : 64 bits |>`; + + + +val _ = type_abbrev( "TLB32_Entry" , ``: (9, 32, 34, 32) TLB_Entry``); + +val _ = Hol_datatype ` + FetchResult = + F_Ext_Error of (ext_fetch_addr_error) + | F_Base of (word) + | F_RVC of (half) + | F_Error of ((ExceptionType # xlenbits))`; + + + + +val _ = Hol_datatype ` + register_value = + Regval_vector of ((ii # bool # register_value list)) + | Regval_list of ( register_value list) + | Regval_option of ( register_value option) + | Regval_Counteren of (Counteren) + | Regval_Mcause of (Mcause) + | Regval_Medeleg of (Medeleg) + | Regval_Minterrupts of (Minterrupts) + | Regval_Misa of (Misa) + | Regval_Mstatus of (Mstatus) + | Regval_Mtvec of (Mtvec) + | Regval_Pmpcfg_ent of (Pmpcfg_ent) + | Regval_Privilege of (Privilege) + | Regval_Sedeleg of (Sedeleg) + | Regval_Sinterrupts of (Sinterrupts) + | Regval_TLB_Entry_9_32_34_32 of ( (9, 32, 34, 32)TLB_Entry) + | Regval_bool of (bool) + | Regval_vector_32_dec_bit of ( 32 words$word) + | Regval_vector_64_dec_bit of ( 64 words$word)`; + + + + +val _ = Hol_datatype ` + regstate = + <| satp : 32 words$word; + tlb32 : ( (9, 32, 34, 32)TLB_Entry)option; + htif_exit_code : 64 words$word; + htif_done : bool; + htif_tohost : 64 words$word; + mtimecmp : 64 words$word; + utval : 32 words$word; + ucause : Mcause; + uepc : 32 words$word; + uscratch : 32 words$word; + utvec : Mtvec; + pmpaddr15 : 32 words$word; + pmpaddr14 : 32 words$word; + pmpaddr13 : 32 words$word; + pmpaddr12 : 32 words$word; + pmpaddr11 : 32 words$word; + pmpaddr10 : 32 words$word; + pmpaddr9 : 32 words$word; + pmpaddr8 : 32 words$word; + pmpaddr7 : 32 words$word; + pmpaddr6 : 32 words$word; + pmpaddr5 : 32 words$word; + pmpaddr4 : 32 words$word; + pmpaddr3 : 32 words$word; + pmpaddr2 : 32 words$word; + pmpaddr1 : 32 words$word; + pmpaddr0 : 32 words$word; + pmp15cfg : Pmpcfg_ent; + pmp14cfg : Pmpcfg_ent; + pmp13cfg : Pmpcfg_ent; + pmp12cfg : Pmpcfg_ent; + pmp11cfg : Pmpcfg_ent; + pmp10cfg : Pmpcfg_ent; + pmp9cfg : Pmpcfg_ent; + pmp8cfg : Pmpcfg_ent; + pmp7cfg : Pmpcfg_ent; + pmp6cfg : Pmpcfg_ent; + pmp5cfg : Pmpcfg_ent; + pmp4cfg : Pmpcfg_ent; + pmp3cfg : Pmpcfg_ent; + pmp2cfg : Pmpcfg_ent; + pmp1cfg : Pmpcfg_ent; + pmp0cfg : Pmpcfg_ent; + tselect : 32 words$word; + stval : 32 words$word; + scause : Mcause; + sepc : 32 words$word; + sscratch : 32 words$word; + stvec : Mtvec; + sideleg : Sinterrupts; + sedeleg : Sedeleg; + mhartid : 32 words$word; + marchid : 32 words$word; + mimpid : 32 words$word; + mvendorid : 32 words$word; + minstret_written : bool; + minstret : 64 words$word; + mtime : 64 words$word; + mcycle : 64 words$word; + scounteren : Counteren; + mcounteren : Counteren; + mscratch : 32 words$word; + mtval : 32 words$word; + mepc : 32 words$word; + mcause : Mcause; + mtvec : Mtvec; + medeleg : Medeleg; + mideleg : Minterrupts; + mie : Minterrupts; + mip : Minterrupts; + mstatus : Mstatus; + misa : Misa; + cur_inst : 32 words$word; + cur_privilege : Privilege; + x31 : 32 words$word; + x30 : 32 words$word; + x29 : 32 words$word; + x28 : 32 words$word; + x27 : 32 words$word; + x26 : 32 words$word; + x25 : 32 words$word; + x24 : 32 words$word; + x23 : 32 words$word; + x22 : 32 words$word; + x21 : 32 words$word; + x20 : 32 words$word; + x19 : 32 words$word; + x18 : 32 words$word; + x17 : 32 words$word; + x16 : 32 words$word; + x15 : 32 words$word; + x14 : 32 words$word; + x13 : 32 words$word; + x12 : 32 words$word; + x11 : 32 words$word; + x10 : 32 words$word; + x9 : 32 words$word; + x8 : 32 words$word; + x7 : 32 words$word; + x6 : 32 words$word; + x5 : 32 words$word; + x4 : 32 words$word; + x3 : 32 words$word; + x2 : 32 words$word; + x1 : 32 words$word; + Xs : ( 32 words$word) list; + instbits : 32 words$word; + nextPC : 32 words$word; + PC : 32 words$word |>`; + + + + + +(*val Counteren_of_regval : register_value -> maybe Counteren*) + +val _ = Define ` + ((Counteren_of_regval:register_value ->(Counteren)option) merge_var= + ((case merge_var of Regval_Counteren (v) => SOME v | _ => NONE )))`; + + +(*val regval_of_Counteren : Counteren -> register_value*) + +val _ = Define ` + ((regval_of_Counteren:Counteren -> register_value) v= (Regval_Counteren v))`; + + +(*val Mcause_of_regval : register_value -> maybe Mcause*) + +val _ = Define ` + ((Mcause_of_regval:register_value ->(Mcause)option) merge_var= + ((case merge_var of Regval_Mcause (v) => SOME v | _ => NONE )))`; + + +(*val regval_of_Mcause : Mcause -> register_value*) + +val _ = Define ` + ((regval_of_Mcause:Mcause -> register_value) v= (Regval_Mcause v))`; + + +(*val Medeleg_of_regval : register_value -> maybe Medeleg*) + +val _ = Define ` + ((Medeleg_of_regval:register_value ->(Medeleg)option) merge_var= + ((case merge_var of Regval_Medeleg (v) => SOME v | _ => NONE )))`; + + +(*val regval_of_Medeleg : Medeleg -> register_value*) + +val _ = Define ` + ((regval_of_Medeleg:Medeleg -> register_value) v= (Regval_Medeleg v))`; + + +(*val Minterrupts_of_regval : register_value -> maybe Minterrupts*) + +val _ = Define ` + ((Minterrupts_of_regval:register_value ->(Minterrupts)option) merge_var= + ((case merge_var of Regval_Minterrupts (v) => SOME v | _ => NONE )))`; + + +(*val regval_of_Minterrupts : Minterrupts -> register_value*) + +val _ = Define ` + ((regval_of_Minterrupts:Minterrupts -> register_value) v= (Regval_Minterrupts v))`; + + +(*val Misa_of_regval : register_value -> maybe Misa*) + +val _ = Define ` + ((Misa_of_regval:register_value ->(Misa)option) merge_var= ((case merge_var of Regval_Misa (v) => SOME v | _ => NONE )))`; + + +(*val regval_of_Misa : Misa -> register_value*) + +val _ = Define ` + ((regval_of_Misa:Misa -> register_value) v= (Regval_Misa v))`; + + +(*val Mstatus_of_regval : register_value -> maybe Mstatus*) + +val _ = Define ` + ((Mstatus_of_regval:register_value ->(Mstatus)option) merge_var= + ((case merge_var of Regval_Mstatus (v) => SOME v | _ => NONE )))`; + + +(*val regval_of_Mstatus : Mstatus -> register_value*) + +val _ = Define ` + ((regval_of_Mstatus:Mstatus -> register_value) v= (Regval_Mstatus v))`; + + +(*val Mtvec_of_regval : register_value -> maybe Mtvec*) + +val _ = Define ` + ((Mtvec_of_regval:register_value ->(Mtvec)option) merge_var= ((case merge_var of Regval_Mtvec (v) => SOME v | _ => NONE )))`; + + +(*val regval_of_Mtvec : Mtvec -> register_value*) + +val _ = Define ` + ((regval_of_Mtvec:Mtvec -> register_value) v= (Regval_Mtvec v))`; + + +(*val Pmpcfg_ent_of_regval : register_value -> maybe Pmpcfg_ent*) + +val _ = Define ` + ((Pmpcfg_ent_of_regval:register_value ->(Pmpcfg_ent)option) merge_var= + ((case merge_var of Regval_Pmpcfg_ent (v) => SOME v | _ => NONE )))`; + + +(*val regval_of_Pmpcfg_ent : Pmpcfg_ent -> register_value*) + +val _ = Define ` + ((regval_of_Pmpcfg_ent:Pmpcfg_ent -> register_value) v= (Regval_Pmpcfg_ent v))`; + + +(*val Privilege_of_regval : register_value -> maybe Privilege*) + +val _ = Define ` + ((Privilege_of_regval:register_value ->(Privilege)option) merge_var= + ((case merge_var of Regval_Privilege (v) => SOME v | _ => NONE )))`; + + +(*val regval_of_Privilege : Privilege -> register_value*) + +val _ = Define ` + ((regval_of_Privilege:Privilege -> register_value) v= (Regval_Privilege v))`; + + +(*val Sedeleg_of_regval : register_value -> maybe Sedeleg*) + +val _ = Define ` + ((Sedeleg_of_regval:register_value ->(Sedeleg)option) merge_var= + ((case merge_var of Regval_Sedeleg (v) => SOME v | _ => NONE )))`; + + +(*val regval_of_Sedeleg : Sedeleg -> register_value*) + +val _ = Define ` + ((regval_of_Sedeleg:Sedeleg -> register_value) v= (Regval_Sedeleg v))`; + + +(*val Sinterrupts_of_regval : register_value -> maybe Sinterrupts*) + +val _ = Define ` + ((Sinterrupts_of_regval:register_value ->(Sinterrupts)option) merge_var= + ((case merge_var of Regval_Sinterrupts (v) => SOME v | _ => NONE )))`; + + +(*val regval_of_Sinterrupts : Sinterrupts -> register_value*) + +val _ = Define ` + ((regval_of_Sinterrupts:Sinterrupts -> register_value) v= (Regval_Sinterrupts v))`; + + +(*val TLB_Entry_9_32_34_32_of_regval : register_value -> maybe (TLB_Entry ty9 ty32 ty34 ty32)*) + +val _ = Define ` + ((TLB_Entry_9_32_34_32_of_regval:register_value ->(((9),(32),(34),(32))TLB_Entry)option) merge_var= + ((case merge_var of Regval_TLB_Entry_9_32_34_32 (v) => SOME v | _ => NONE )))`; + + +(*val regval_of_TLB_Entry_9_32_34_32 : TLB_Entry ty9 ty32 ty34 ty32 -> register_value*) + +val _ = Define ` + ((regval_of_TLB_Entry_9_32_34_32:((9),(32),(34),(32))TLB_Entry -> register_value) v= (Regval_TLB_Entry_9_32_34_32 v))`; + + +(*val bool_of_regval : register_value -> maybe bool*) + +val _ = Define ` + ((bool_of_regval:register_value ->(bool)option) merge_var= ((case merge_var of Regval_bool (v) => SOME v | _ => NONE )))`; + + +(*val regval_of_bool : bool -> register_value*) + +val _ = Define ` + ((regval_of_bool:bool -> register_value) v= (Regval_bool v))`; + + +(*val vector_32_dec_bit_of_regval : register_value -> maybe (mword ty32)*) + +val _ = Define ` + ((vector_32_dec_bit_of_regval:register_value ->((32)words$word)option) merge_var= + ((case merge_var of Regval_vector_32_dec_bit (v) => SOME v | _ => NONE )))`; + + +(*val regval_of_vector_32_dec_bit : mword ty32 -> register_value*) + +val _ = Define ` + ((regval_of_vector_32_dec_bit:(32)words$word -> register_value) v= (Regval_vector_32_dec_bit v))`; + + +(*val vector_64_dec_bit_of_regval : register_value -> maybe (mword ty64)*) + +val _ = Define ` + ((vector_64_dec_bit_of_regval:register_value ->((64)words$word)option) merge_var= + ((case merge_var of Regval_vector_64_dec_bit (v) => SOME v | _ => NONE )))`; + + +(*val regval_of_vector_64_dec_bit : mword ty64 -> register_value*) + +val _ = Define ` + ((regval_of_vector_64_dec_bit:(64)words$word -> register_value) v= (Regval_vector_64_dec_bit v))`; + + + + +(*val vector_of_regval : forall 'a. (register_value -> maybe 'a) -> register_value -> maybe (list 'a)*) +val _ = Define ` + ((vector_of_regval:(register_value -> 'a option) -> register_value ->('a list)option) of_regval1= + (\x . (case x of + Regval_vector (_, _, v) => just_list (MAP of_regval1 v) + | _ => NONE + )))`; + + +(*val regval_of_vector : forall 'a. ('a -> register_value) -> integer -> bool -> list 'a -> register_value*) +val _ = Define ` + ((regval_of_vector:('a -> register_value) -> int -> bool -> 'a list -> register_value) regval_of1 size1 is_inc xs= (Regval_vector (size1, is_inc, MAP regval_of1 xs)))`; + + +(*val list_of_regval : forall 'a. (register_value -> maybe 'a) -> register_value -> maybe (list 'a)*) +val _ = Define ` + ((list_of_regval:(register_value -> 'a option) -> register_value ->('a list)option) of_regval1= + (\x . (case x of + Regval_list v => just_list (MAP of_regval1 v) + | _ => NONE + )))`; + + +(*val regval_of_list : forall 'a. ('a -> register_value) -> list 'a -> register_value*) +val _ = Define ` + ((regval_of_list:('a -> register_value) -> 'a list -> register_value) regval_of1 xs= (Regval_list (MAP regval_of1 xs)))`; + + +(*val option_of_regval : forall 'a. (register_value -> maybe 'a) -> register_value -> maybe (maybe 'a)*) +val _ = Define ` + ((option_of_regval:(register_value -> 'a option) -> register_value ->('a option)option) of_regval1= + (\x . (case x of + Regval_option v => SOME (OPTION_BIND v of_regval1) + | _ => NONE + )))`; + + +(*val regval_of_option : forall 'a. ('a -> register_value) -> maybe 'a -> register_value*) +val _ = Define ` + ((regval_of_option:('a -> register_value) -> 'a option -> register_value) regval_of1 v= (Regval_option (OPTION_MAP regval_of1 v)))`; + + + +val _ = Define ` + ((satp_ref:((regstate),(register_value),((32)words$word))register_ref)= (<| + name := "satp"; + read_from := (\ s . s.satp); + write_to := (\ v s . (( s with<| satp := v |>))); + of_regval := (\ v . vector_32_dec_bit_of_regval v); + regval_of := (\ v . regval_of_vector_32_dec_bit v) |>))`; + + +val _ = Define ` + ((tlb32_ref:((regstate),(register_value),((((9),(32),(34),(32))TLB_Entry)option))register_ref)= (<| + name := "tlb32"; + read_from := (\ s . s.tlb32); + write_to := (\ v s . (( s with<| tlb32 := v |>))); + of_regval := (\ v . option_of_regval (\ v . TLB_Entry_9_32_34_32_of_regval v) v); + regval_of := (\ v . regval_of_option (\ v . regval_of_TLB_Entry_9_32_34_32 v) v) |>))`; + + +val _ = Define ` + ((htif_exit_code_ref:((regstate),(register_value),((64)words$word))register_ref)= (<| + name := "htif_exit_code"; + read_from := (\ s . s.htif_exit_code); + write_to := (\ v s . (( s with<| htif_exit_code := v |>))); + of_regval := (\ v . vector_64_dec_bit_of_regval v); + regval_of := (\ v . regval_of_vector_64_dec_bit v) |>))`; + + +val _ = Define ` + ((htif_done_ref:((regstate),(register_value),(bool))register_ref)= (<| + name := "htif_done"; + read_from := (\ s . s.htif_done); + write_to := (\ v s . (( s with<| htif_done := v |>))); + of_regval := (\ v . bool_of_regval v); + regval_of := (\ v . regval_of_bool v) |>))`; + + +val _ = Define ` + ((htif_tohost_ref:((regstate),(register_value),((64)words$word))register_ref)= (<| + name := "htif_tohost"; + read_from := (\ s . s.htif_tohost); + write_to := (\ v s . (( s with<| htif_tohost := v |>))); + of_regval := (\ v . vector_64_dec_bit_of_regval v); + regval_of := (\ v . regval_of_vector_64_dec_bit v) |>))`; + + +val _ = Define ` + ((mtimecmp_ref:((regstate),(register_value),((64)words$word))register_ref)= (<| + name := "mtimecmp"; + read_from := (\ s . s.mtimecmp); + write_to := (\ v s . (( s with<| mtimecmp := v |>))); + of_regval := (\ v . vector_64_dec_bit_of_regval v); + regval_of := (\ v . regval_of_vector_64_dec_bit v) |>))`; + + +val _ = Define ` + ((utval_ref:((regstate),(register_value),((32)words$word))register_ref)= (<| + name := "utval"; + read_from := (\ s . s.utval); + write_to := (\ v s . (( s with<| utval := v |>))); + of_regval := (\ v . vector_32_dec_bit_of_regval v); + regval_of := (\ v . regval_of_vector_32_dec_bit v) |>))`; + + +val _ = Define ` + ((ucause_ref:((regstate),(register_value),(Mcause))register_ref)= (<| + name := "ucause"; + read_from := (\ s . s.ucause); + write_to := (\ v s . (( s with<| ucause := v |>))); + of_regval := (\ v . Mcause_of_regval v); + regval_of := (\ v . regval_of_Mcause v) |>))`; + + +val _ = Define ` + ((uepc_ref:((regstate),(register_value),((32)words$word))register_ref)= (<| + name := "uepc"; + read_from := (\ s . s.uepc); + write_to := (\ v s . (( s with<| uepc := v |>))); + of_regval := (\ v . vector_32_dec_bit_of_regval v); + regval_of := (\ v . regval_of_vector_32_dec_bit v) |>))`; + + +val _ = Define ` + ((uscratch_ref:((regstate),(register_value),((32)words$word))register_ref)= (<| + name := "uscratch"; + read_from := (\ s . s.uscratch); + write_to := (\ v s . (( s with<| uscratch := v |>))); + of_regval := (\ v . vector_32_dec_bit_of_regval v); + regval_of := (\ v . regval_of_vector_32_dec_bit v) |>))`; + + +val _ = Define ` + ((utvec_ref:((regstate),(register_value),(Mtvec))register_ref)= (<| + name := "utvec"; + read_from := (\ s . s.utvec); + write_to := (\ v s . (( s with<| utvec := v |>))); + of_regval := (\ v . Mtvec_of_regval v); + regval_of := (\ v . regval_of_Mtvec v) |>))`; + + +val _ = Define ` + ((pmpaddr15_ref:((regstate),(register_value),((32)words$word))register_ref)= (<| + name := "pmpaddr15"; + read_from := (\ s . s.pmpaddr15); + write_to := (\ v s . (( s with<| pmpaddr15 := v |>))); + of_regval := (\ v . vector_32_dec_bit_of_regval v); + regval_of := (\ v . regval_of_vector_32_dec_bit v) |>))`; + + +val _ = Define ` + ((pmpaddr14_ref:((regstate),(register_value),((32)words$word))register_ref)= (<| + name := "pmpaddr14"; + read_from := (\ s . s.pmpaddr14); + write_to := (\ v s . (( s with<| pmpaddr14 := v |>))); + of_regval := (\ v . vector_32_dec_bit_of_regval v); + regval_of := (\ v . regval_of_vector_32_dec_bit v) |>))`; + + +val _ = Define ` + ((pmpaddr13_ref:((regstate),(register_value),((32)words$word))register_ref)= (<| + name := "pmpaddr13"; + read_from := (\ s . s.pmpaddr13); + write_to := (\ v s . (( s with<| pmpaddr13 := v |>))); + of_regval := (\ v . vector_32_dec_bit_of_regval v); + regval_of := (\ v . regval_of_vector_32_dec_bit v) |>))`; + + +val _ = Define ` + ((pmpaddr12_ref:((regstate),(register_value),((32)words$word))register_ref)= (<| + name := "pmpaddr12"; + read_from := (\ s . s.pmpaddr12); + write_to := (\ v s . (( s with<| pmpaddr12 := v |>))); + of_regval := (\ v . vector_32_dec_bit_of_regval v); + regval_of := (\ v . regval_of_vector_32_dec_bit v) |>))`; + + +val _ = Define ` + ((pmpaddr11_ref:((regstate),(register_value),((32)words$word))register_ref)= (<| + name := "pmpaddr11"; + read_from := (\ s . s.pmpaddr11); + write_to := (\ v s . (( s with<| pmpaddr11 := v |>))); + of_regval := (\ v . vector_32_dec_bit_of_regval v); + regval_of := (\ v . regval_of_vector_32_dec_bit v) |>))`; + + +val _ = Define ` + ((pmpaddr10_ref:((regstate),(register_value),((32)words$word))register_ref)= (<| + name := "pmpaddr10"; + read_from := (\ s . s.pmpaddr10); + write_to := (\ v s . (( s with<| pmpaddr10 := v |>))); + of_regval := (\ v . vector_32_dec_bit_of_regval v); + regval_of := (\ v . regval_of_vector_32_dec_bit v) |>))`; + + +val _ = Define ` + ((pmpaddr9_ref:((regstate),(register_value),((32)words$word))register_ref)= (<| + name := "pmpaddr9"; + read_from := (\ s . s.pmpaddr9); + write_to := (\ v s . (( s with<| pmpaddr9 := v |>))); + of_regval := (\ v . vector_32_dec_bit_of_regval v); + regval_of := (\ v . regval_of_vector_32_dec_bit v) |>))`; + + +val _ = Define ` + ((pmpaddr8_ref:((regstate),(register_value),((32)words$word))register_ref)= (<| + name := "pmpaddr8"; + read_from := (\ s . s.pmpaddr8); + write_to := (\ v s . (( s with<| pmpaddr8 := v |>))); + of_regval := (\ v . vector_32_dec_bit_of_regval v); + regval_of := (\ v . regval_of_vector_32_dec_bit v) |>))`; + + +val _ = Define ` + ((pmpaddr7_ref:((regstate),(register_value),((32)words$word))register_ref)= (<| + name := "pmpaddr7"; + read_from := (\ s . s.pmpaddr7); + write_to := (\ v s . (( s with<| pmpaddr7 := v |>))); + of_regval := (\ v . vector_32_dec_bit_of_regval v); + regval_of := (\ v . regval_of_vector_32_dec_bit v) |>))`; + + +val _ = Define ` + ((pmpaddr6_ref:((regstate),(register_value),((32)words$word))register_ref)= (<| + name := "pmpaddr6"; + read_from := (\ s . s.pmpaddr6); + write_to := (\ v s . (( s with<| pmpaddr6 := v |>))); + of_regval := (\ v . vector_32_dec_bit_of_regval v); + regval_of := (\ v . regval_of_vector_32_dec_bit v) |>))`; + + +val _ = Define ` + ((pmpaddr5_ref:((regstate),(register_value),((32)words$word))register_ref)= (<| + name := "pmpaddr5"; + read_from := (\ s . s.pmpaddr5); + write_to := (\ v s . (( s with<| pmpaddr5 := v |>))); + of_regval := (\ v . vector_32_dec_bit_of_regval v); + regval_of := (\ v . regval_of_vector_32_dec_bit v) |>))`; + + +val _ = Define ` + ((pmpaddr4_ref:((regstate),(register_value),((32)words$word))register_ref)= (<| + name := "pmpaddr4"; + read_from := (\ s . s.pmpaddr4); + write_to := (\ v s . (( s with<| pmpaddr4 := v |>))); + of_regval := (\ v . vector_32_dec_bit_of_regval v); + regval_of := (\ v . regval_of_vector_32_dec_bit v) |>))`; + + +val _ = Define ` + ((pmpaddr3_ref:((regstate),(register_value),((32)words$word))register_ref)= (<| + name := "pmpaddr3"; + read_from := (\ s . s.pmpaddr3); + write_to := (\ v s . (( s with<| pmpaddr3 := v |>))); + of_regval := (\ v . vector_32_dec_bit_of_regval v); + regval_of := (\ v . regval_of_vector_32_dec_bit v) |>))`; + + +val _ = Define ` + ((pmpaddr2_ref:((regstate),(register_value),((32)words$word))register_ref)= (<| + name := "pmpaddr2"; + read_from := (\ s . s.pmpaddr2); + write_to := (\ v s . (( s with<| pmpaddr2 := v |>))); + of_regval := (\ v . vector_32_dec_bit_of_regval v); + regval_of := (\ v . regval_of_vector_32_dec_bit v) |>))`; + + +val _ = Define ` + ((pmpaddr1_ref:((regstate),(register_value),((32)words$word))register_ref)= (<| + name := "pmpaddr1"; + read_from := (\ s . s.pmpaddr1); + write_to := (\ v s . (( s with<| pmpaddr1 := v |>))); + of_regval := (\ v . vector_32_dec_bit_of_regval v); + regval_of := (\ v . regval_of_vector_32_dec_bit v) |>))`; + + +val _ = Define ` + ((pmpaddr0_ref:((regstate),(register_value),((32)words$word))register_ref)= (<| + name := "pmpaddr0"; + read_from := (\ s . s.pmpaddr0); + write_to := (\ v s . (( s with<| pmpaddr0 := v |>))); + of_regval := (\ v . vector_32_dec_bit_of_regval v); + regval_of := (\ v . regval_of_vector_32_dec_bit v) |>))`; + + +val _ = Define ` + ((pmp15cfg_ref:((regstate),(register_value),(Pmpcfg_ent))register_ref)= (<| + name := "pmp15cfg"; + read_from := (\ s . s.pmp15cfg); + write_to := (\ v s . (( s with<| pmp15cfg := v |>))); + of_regval := (\ v . Pmpcfg_ent_of_regval v); + regval_of := (\ v . regval_of_Pmpcfg_ent v) |>))`; + + +val _ = Define ` + ((pmp14cfg_ref:((regstate),(register_value),(Pmpcfg_ent))register_ref)= (<| + name := "pmp14cfg"; + read_from := (\ s . s.pmp14cfg); + write_to := (\ v s . (( s with<| pmp14cfg := v |>))); + of_regval := (\ v . Pmpcfg_ent_of_regval v); + regval_of := (\ v . regval_of_Pmpcfg_ent v) |>))`; + + +val _ = Define ` + ((pmp13cfg_ref:((regstate),(register_value),(Pmpcfg_ent))register_ref)= (<| + name := "pmp13cfg"; + read_from := (\ s . s.pmp13cfg); + write_to := (\ v s . (( s with<| pmp13cfg := v |>))); + of_regval := (\ v . Pmpcfg_ent_of_regval v); + regval_of := (\ v . regval_of_Pmpcfg_ent v) |>))`; + + +val _ = Define ` + ((pmp12cfg_ref:((regstate),(register_value),(Pmpcfg_ent))register_ref)= (<| + name := "pmp12cfg"; + read_from := (\ s . s.pmp12cfg); + write_to := (\ v s . (( s with<| pmp12cfg := v |>))); + of_regval := (\ v . Pmpcfg_ent_of_regval v); + regval_of := (\ v . regval_of_Pmpcfg_ent v) |>))`; + + +val _ = Define ` + ((pmp11cfg_ref:((regstate),(register_value),(Pmpcfg_ent))register_ref)= (<| + name := "pmp11cfg"; + read_from := (\ s . s.pmp11cfg); + write_to := (\ v s . (( s with<| pmp11cfg := v |>))); + of_regval := (\ v . Pmpcfg_ent_of_regval v); + regval_of := (\ v . regval_of_Pmpcfg_ent v) |>))`; + + +val _ = Define ` + ((pmp10cfg_ref:((regstate),(register_value),(Pmpcfg_ent))register_ref)= (<| + name := "pmp10cfg"; + read_from := (\ s . s.pmp10cfg); + write_to := (\ v s . (( s with<| pmp10cfg := v |>))); + of_regval := (\ v . Pmpcfg_ent_of_regval v); + regval_of := (\ v . regval_of_Pmpcfg_ent v) |>))`; + + +val _ = Define ` + ((pmp9cfg_ref:((regstate),(register_value),(Pmpcfg_ent))register_ref)= (<| + name := "pmp9cfg"; + read_from := (\ s . s.pmp9cfg); + write_to := (\ v s . (( s with<| pmp9cfg := v |>))); + of_regval := (\ v . Pmpcfg_ent_of_regval v); + regval_of := (\ v . regval_of_Pmpcfg_ent v) |>))`; + + +val _ = Define ` + ((pmp8cfg_ref:((regstate),(register_value),(Pmpcfg_ent))register_ref)= (<| + name := "pmp8cfg"; + read_from := (\ s . s.pmp8cfg); + write_to := (\ v s . (( s with<| pmp8cfg := v |>))); + of_regval := (\ v . Pmpcfg_ent_of_regval v); + regval_of := (\ v . regval_of_Pmpcfg_ent v) |>))`; + + +val _ = Define ` + ((pmp7cfg_ref:((regstate),(register_value),(Pmpcfg_ent))register_ref)= (<| + name := "pmp7cfg"; + read_from := (\ s . s.pmp7cfg); + write_to := (\ v s . (( s with<| pmp7cfg := v |>))); + of_regval := (\ v . Pmpcfg_ent_of_regval v); + regval_of := (\ v . regval_of_Pmpcfg_ent v) |>))`; + + +val _ = Define ` + ((pmp6cfg_ref:((regstate),(register_value),(Pmpcfg_ent))register_ref)= (<| + name := "pmp6cfg"; + read_from := (\ s . s.pmp6cfg); + write_to := (\ v s . (( s with<| pmp6cfg := v |>))); + of_regval := (\ v . Pmpcfg_ent_of_regval v); + regval_of := (\ v . regval_of_Pmpcfg_ent v) |>))`; + + +val _ = Define ` + ((pmp5cfg_ref:((regstate),(register_value),(Pmpcfg_ent))register_ref)= (<| + name := "pmp5cfg"; + read_from := (\ s . s.pmp5cfg); + write_to := (\ v s . (( s with<| pmp5cfg := v |>))); + of_regval := (\ v . Pmpcfg_ent_of_regval v); + regval_of := (\ v . regval_of_Pmpcfg_ent v) |>))`; + + +val _ = Define ` + ((pmp4cfg_ref:((regstate),(register_value),(Pmpcfg_ent))register_ref)= (<| + name := "pmp4cfg"; + read_from := (\ s . s.pmp4cfg); + write_to := (\ v s . (( s with<| pmp4cfg := v |>))); + of_regval := (\ v . Pmpcfg_ent_of_regval v); + regval_of := (\ v . regval_of_Pmpcfg_ent v) |>))`; + + +val _ = Define ` + ((pmp3cfg_ref:((regstate),(register_value),(Pmpcfg_ent))register_ref)= (<| + name := "pmp3cfg"; + read_from := (\ s . s.pmp3cfg); + write_to := (\ v s . (( s with<| pmp3cfg := v |>))); + of_regval := (\ v . Pmpcfg_ent_of_regval v); + regval_of := (\ v . regval_of_Pmpcfg_ent v) |>))`; + + +val _ = Define ` + ((pmp2cfg_ref:((regstate),(register_value),(Pmpcfg_ent))register_ref)= (<| + name := "pmp2cfg"; + read_from := (\ s . s.pmp2cfg); + write_to := (\ v s . (( s with<| pmp2cfg := v |>))); + of_regval := (\ v . Pmpcfg_ent_of_regval v); + regval_of := (\ v . regval_of_Pmpcfg_ent v) |>))`; + + +val _ = Define ` + ((pmp1cfg_ref:((regstate),(register_value),(Pmpcfg_ent))register_ref)= (<| + name := "pmp1cfg"; + read_from := (\ s . s.pmp1cfg); + write_to := (\ v s . (( s with<| pmp1cfg := v |>))); + of_regval := (\ v . Pmpcfg_ent_of_regval v); + regval_of := (\ v . regval_of_Pmpcfg_ent v) |>))`; + + +val _ = Define ` + ((pmp0cfg_ref:((regstate),(register_value),(Pmpcfg_ent))register_ref)= (<| + name := "pmp0cfg"; + read_from := (\ s . s.pmp0cfg); + write_to := (\ v s . (( s with<| pmp0cfg := v |>))); + of_regval := (\ v . Pmpcfg_ent_of_regval v); + regval_of := (\ v . regval_of_Pmpcfg_ent v) |>))`; + + +val _ = Define ` + ((tselect_ref:((regstate),(register_value),((32)words$word))register_ref)= (<| + name := "tselect"; + read_from := (\ s . s.tselect); + write_to := (\ v s . (( s with<| tselect := v |>))); + of_regval := (\ v . vector_32_dec_bit_of_regval v); + regval_of := (\ v . regval_of_vector_32_dec_bit v) |>))`; + + +val _ = Define ` + ((stval_ref:((regstate),(register_value),((32)words$word))register_ref)= (<| + name := "stval"; + read_from := (\ s . s.stval); + write_to := (\ v s . (( s with<| stval := v |>))); + of_regval := (\ v . vector_32_dec_bit_of_regval v); + regval_of := (\ v . regval_of_vector_32_dec_bit v) |>))`; + + +val _ = Define ` + ((scause_ref:((regstate),(register_value),(Mcause))register_ref)= (<| + name := "scause"; + read_from := (\ s . s.scause); + write_to := (\ v s . (( s with<| scause := v |>))); + of_regval := (\ v . Mcause_of_regval v); + regval_of := (\ v . regval_of_Mcause v) |>))`; + + +val _ = Define ` + ((sepc_ref:((regstate),(register_value),((32)words$word))register_ref)= (<| + name := "sepc"; + read_from := (\ s . s.sepc); + write_to := (\ v s . (( s with<| sepc := v |>))); + of_regval := (\ v . vector_32_dec_bit_of_regval v); + regval_of := (\ v . regval_of_vector_32_dec_bit v) |>))`; + + +val _ = Define ` + ((sscratch_ref:((regstate),(register_value),((32)words$word))register_ref)= (<| + name := "sscratch"; + read_from := (\ s . s.sscratch); + write_to := (\ v s . (( s with<| sscratch := v |>))); + of_regval := (\ v . vector_32_dec_bit_of_regval v); + regval_of := (\ v . regval_of_vector_32_dec_bit v) |>))`; + + +val _ = Define ` + ((stvec_ref:((regstate),(register_value),(Mtvec))register_ref)= (<| + name := "stvec"; + read_from := (\ s . s.stvec); + write_to := (\ v s . (( s with<| stvec := v |>))); + of_regval := (\ v . Mtvec_of_regval v); + regval_of := (\ v . regval_of_Mtvec v) |>))`; + + +val _ = Define ` + ((sideleg_ref:((regstate),(register_value),(Sinterrupts))register_ref)= (<| + name := "sideleg"; + read_from := (\ s . s.sideleg); + write_to := (\ v s . (( s with<| sideleg := v |>))); + of_regval := (\ v . Sinterrupts_of_regval v); + regval_of := (\ v . regval_of_Sinterrupts v) |>))`; + + +val _ = Define ` + ((sedeleg_ref:((regstate),(register_value),(Sedeleg))register_ref)= (<| + name := "sedeleg"; + read_from := (\ s . s.sedeleg); + write_to := (\ v s . (( s with<| sedeleg := v |>))); + of_regval := (\ v . Sedeleg_of_regval v); + regval_of := (\ v . regval_of_Sedeleg v) |>))`; + + +val _ = Define ` + ((mhartid_ref:((regstate),(register_value),((32)words$word))register_ref)= (<| + name := "mhartid"; + read_from := (\ s . s.mhartid); + write_to := (\ v s . (( s with<| mhartid := v |>))); + of_regval := (\ v . vector_32_dec_bit_of_regval v); + regval_of := (\ v . regval_of_vector_32_dec_bit v) |>))`; + + +val _ = Define ` + ((marchid_ref:((regstate),(register_value),((32)words$word))register_ref)= (<| + name := "marchid"; + read_from := (\ s . s.marchid); + write_to := (\ v s . (( s with<| marchid := v |>))); + of_regval := (\ v . vector_32_dec_bit_of_regval v); + regval_of := (\ v . regval_of_vector_32_dec_bit v) |>))`; + + +val _ = Define ` + ((mimpid_ref:((regstate),(register_value),((32)words$word))register_ref)= (<| + name := "mimpid"; + read_from := (\ s . s.mimpid); + write_to := (\ v s . (( s with<| mimpid := v |>))); + of_regval := (\ v . vector_32_dec_bit_of_regval v); + regval_of := (\ v . regval_of_vector_32_dec_bit v) |>))`; + + +val _ = Define ` + ((mvendorid_ref:((regstate),(register_value),((32)words$word))register_ref)= (<| + name := "mvendorid"; + read_from := (\ s . s.mvendorid); + write_to := (\ v s . (( s with<| mvendorid := v |>))); + of_regval := (\ v . vector_32_dec_bit_of_regval v); + regval_of := (\ v . regval_of_vector_32_dec_bit v) |>))`; + + +val _ = Define ` + ((minstret_written_ref:((regstate),(register_value),(bool))register_ref)= (<| + name := "minstret_written"; + read_from := (\ s . s.minstret_written); + write_to := (\ v s . (( s with<| minstret_written := v |>))); + of_regval := (\ v . bool_of_regval v); + regval_of := (\ v . regval_of_bool v) |>))`; + + +val _ = Define ` + ((minstret_ref:((regstate),(register_value),((64)words$word))register_ref)= (<| + name := "minstret"; + read_from := (\ s . s.minstret); + write_to := (\ v s . (( s with<| minstret := v |>))); + of_regval := (\ v . vector_64_dec_bit_of_regval v); + regval_of := (\ v . regval_of_vector_64_dec_bit v) |>))`; + + +val _ = Define ` + ((mtime_ref:((regstate),(register_value),((64)words$word))register_ref)= (<| + name := "mtime"; + read_from := (\ s . s.mtime); + write_to := (\ v s . (( s with<| mtime := v |>))); + of_regval := (\ v . vector_64_dec_bit_of_regval v); + regval_of := (\ v . regval_of_vector_64_dec_bit v) |>))`; + + +val _ = Define ` + ((mcycle_ref:((regstate),(register_value),((64)words$word))register_ref)= (<| + name := "mcycle"; + read_from := (\ s . s.mcycle); + write_to := (\ v s . (( s with<| mcycle := v |>))); + of_regval := (\ v . vector_64_dec_bit_of_regval v); + regval_of := (\ v . regval_of_vector_64_dec_bit v) |>))`; + + +val _ = Define ` + ((scounteren_ref:((regstate),(register_value),(Counteren))register_ref)= (<| + name := "scounteren"; + read_from := (\ s . s.scounteren); + write_to := (\ v s . (( s with<| scounteren := v |>))); + of_regval := (\ v . Counteren_of_regval v); + regval_of := (\ v . regval_of_Counteren v) |>))`; + + +val _ = Define ` + ((mcounteren_ref:((regstate),(register_value),(Counteren))register_ref)= (<| + name := "mcounteren"; + read_from := (\ s . s.mcounteren); + write_to := (\ v s . (( s with<| mcounteren := v |>))); + of_regval := (\ v . Counteren_of_regval v); + regval_of := (\ v . regval_of_Counteren v) |>))`; + + +val _ = Define ` + ((mscratch_ref:((regstate),(register_value),((32)words$word))register_ref)= (<| + name := "mscratch"; + read_from := (\ s . s.mscratch); + write_to := (\ v s . (( s with<| mscratch := v |>))); + of_regval := (\ v . vector_32_dec_bit_of_regval v); + regval_of := (\ v . regval_of_vector_32_dec_bit v) |>))`; + + +val _ = Define ` + ((mtval_ref:((regstate),(register_value),((32)words$word))register_ref)= (<| + name := "mtval"; + read_from := (\ s . s.mtval); + write_to := (\ v s . (( s with<| mtval := v |>))); + of_regval := (\ v . vector_32_dec_bit_of_regval v); + regval_of := (\ v . regval_of_vector_32_dec_bit v) |>))`; + + +val _ = Define ` + ((mepc_ref:((regstate),(register_value),((32)words$word))register_ref)= (<| + name := "mepc"; + read_from := (\ s . s.mepc); + write_to := (\ v s . (( s with<| mepc := v |>))); + of_regval := (\ v . vector_32_dec_bit_of_regval v); + regval_of := (\ v . regval_of_vector_32_dec_bit v) |>))`; + + +val _ = Define ` + ((mcause_ref:((regstate),(register_value),(Mcause))register_ref)= (<| + name := "mcause"; + read_from := (\ s . s.mcause); + write_to := (\ v s . (( s with<| mcause := v |>))); + of_regval := (\ v . Mcause_of_regval v); + regval_of := (\ v . regval_of_Mcause v) |>))`; + + +val _ = Define ` + ((mtvec_ref:((regstate),(register_value),(Mtvec))register_ref)= (<| + name := "mtvec"; + read_from := (\ s . s.mtvec); + write_to := (\ v s . (( s with<| mtvec := v |>))); + of_regval := (\ v . Mtvec_of_regval v); + regval_of := (\ v . regval_of_Mtvec v) |>))`; + + +val _ = Define ` + ((medeleg_ref:((regstate),(register_value),(Medeleg))register_ref)= (<| + name := "medeleg"; + read_from := (\ s . s.medeleg); + write_to := (\ v s . (( s with<| medeleg := v |>))); + of_regval := (\ v . Medeleg_of_regval v); + regval_of := (\ v . regval_of_Medeleg v) |>))`; + + +val _ = Define ` + ((mideleg_ref:((regstate),(register_value),(Minterrupts))register_ref)= (<| + name := "mideleg"; + read_from := (\ s . s.mideleg); + write_to := (\ v s . (( s with<| mideleg := v |>))); + of_regval := (\ v . Minterrupts_of_regval v); + regval_of := (\ v . regval_of_Minterrupts v) |>))`; + + +val _ = Define ` + ((mie_ref:((regstate),(register_value),(Minterrupts))register_ref)= (<| + name := "mie"; + read_from := (\ s . s.mie); + write_to := (\ v s . (( s with<| mie := v |>))); + of_regval := (\ v . Minterrupts_of_regval v); + regval_of := (\ v . regval_of_Minterrupts v) |>))`; + + +val _ = Define ` + ((mip_ref:((regstate),(register_value),(Minterrupts))register_ref)= (<| + name := "mip"; + read_from := (\ s . s.mip); + write_to := (\ v s . (( s with<| mip := v |>))); + of_regval := (\ v . Minterrupts_of_regval v); + regval_of := (\ v . regval_of_Minterrupts v) |>))`; + + +val _ = Define ` + ((mstatus_ref:((regstate),(register_value),(Mstatus))register_ref)= (<| + name := "mstatus"; + read_from := (\ s . s.mstatus); + write_to := (\ v s . (( s with<| mstatus := v |>))); + of_regval := (\ v . Mstatus_of_regval v); + regval_of := (\ v . regval_of_Mstatus v) |>))`; + + +val _ = Define ` + ((misa_ref:((regstate),(register_value),(Misa))register_ref)= (<| + name := "misa"; + read_from := (\ s . s.misa); + write_to := (\ v s . (( s with<| misa := v |>))); + of_regval := (\ v . Misa_of_regval v); + regval_of := (\ v . regval_of_Misa v) |>))`; + + +val _ = Define ` + ((cur_inst_ref:((regstate),(register_value),((32)words$word))register_ref)= (<| + name := "cur_inst"; + read_from := (\ s . s.cur_inst); + write_to := (\ v s . (( s with<| cur_inst := v |>))); + of_regval := (\ v . vector_32_dec_bit_of_regval v); + regval_of := (\ v . regval_of_vector_32_dec_bit v) |>))`; + + +val _ = Define ` + ((cur_privilege_ref:((regstate),(register_value),(Privilege))register_ref)= (<| + name := "cur_privilege"; + read_from := (\ s . s.cur_privilege); + write_to := (\ v s . (( s with<| cur_privilege := v |>))); + of_regval := (\ v . Privilege_of_regval v); + regval_of := (\ v . regval_of_Privilege v) |>))`; + + +val _ = Define ` + ((x31_ref:((regstate),(register_value),((32)words$word))register_ref)= (<| + name := "x31"; + read_from := (\ s . s.x31); + write_to := (\ v s . (( s with<| x31 := v |>))); + of_regval := (\ v . vector_32_dec_bit_of_regval v); + regval_of := (\ v . regval_of_vector_32_dec_bit v) |>))`; + + +val _ = Define ` + ((x30_ref:((regstate),(register_value),((32)words$word))register_ref)= (<| + name := "x30"; + read_from := (\ s . s.x30); + write_to := (\ v s . (( s with<| x30 := v |>))); + of_regval := (\ v . vector_32_dec_bit_of_regval v); + regval_of := (\ v . regval_of_vector_32_dec_bit v) |>))`; + + +val _ = Define ` + ((x29_ref:((regstate),(register_value),((32)words$word))register_ref)= (<| + name := "x29"; + read_from := (\ s . s.x29); + write_to := (\ v s . (( s with<| x29 := v |>))); + of_regval := (\ v . vector_32_dec_bit_of_regval v); + regval_of := (\ v . regval_of_vector_32_dec_bit v) |>))`; + + +val _ = Define ` + ((x28_ref:((regstate),(register_value),((32)words$word))register_ref)= (<| + name := "x28"; + read_from := (\ s . s.x28); + write_to := (\ v s . (( s with<| x28 := v |>))); + of_regval := (\ v . vector_32_dec_bit_of_regval v); + regval_of := (\ v . regval_of_vector_32_dec_bit v) |>))`; + + +val _ = Define ` + ((x27_ref:((regstate),(register_value),((32)words$word))register_ref)= (<| + name := "x27"; + read_from := (\ s . s.x27); + write_to := (\ v s . (( s with<| x27 := v |>))); + of_regval := (\ v . vector_32_dec_bit_of_regval v); + regval_of := (\ v . regval_of_vector_32_dec_bit v) |>))`; + + +val _ = Define ` + ((x26_ref:((regstate),(register_value),((32)words$word))register_ref)= (<| + name := "x26"; + read_from := (\ s . s.x26); + write_to := (\ v s . (( s with<| x26 := v |>))); + of_regval := (\ v . vector_32_dec_bit_of_regval v); + regval_of := (\ v . regval_of_vector_32_dec_bit v) |>))`; + + +val _ = Define ` + ((x25_ref:((regstate),(register_value),((32)words$word))register_ref)= (<| + name := "x25"; + read_from := (\ s . s.x25); + write_to := (\ v s . (( s with<| x25 := v |>))); + of_regval := (\ v . vector_32_dec_bit_of_regval v); + regval_of := (\ v . regval_of_vector_32_dec_bit v) |>))`; + + +val _ = Define ` + ((x24_ref:((regstate),(register_value),((32)words$word))register_ref)= (<| + name := "x24"; + read_from := (\ s . s.x24); + write_to := (\ v s . (( s with<| x24 := v |>))); + of_regval := (\ v . vector_32_dec_bit_of_regval v); + regval_of := (\ v . regval_of_vector_32_dec_bit v) |>))`; + + +val _ = Define ` + ((x23_ref:((regstate),(register_value),((32)words$word))register_ref)= (<| + name := "x23"; + read_from := (\ s . s.x23); + write_to := (\ v s . (( s with<| x23 := v |>))); + of_regval := (\ v . vector_32_dec_bit_of_regval v); + regval_of := (\ v . regval_of_vector_32_dec_bit v) |>))`; + + +val _ = Define ` + ((x22_ref:((regstate),(register_value),((32)words$word))register_ref)= (<| + name := "x22"; + read_from := (\ s . s.x22); + write_to := (\ v s . (( s with<| x22 := v |>))); + of_regval := (\ v . vector_32_dec_bit_of_regval v); + regval_of := (\ v . regval_of_vector_32_dec_bit v) |>))`; + + +val _ = Define ` + ((x21_ref:((regstate),(register_value),((32)words$word))register_ref)= (<| + name := "x21"; + read_from := (\ s . s.x21); + write_to := (\ v s . (( s with<| x21 := v |>))); + of_regval := (\ v . vector_32_dec_bit_of_regval v); + regval_of := (\ v . regval_of_vector_32_dec_bit v) |>))`; + + +val _ = Define ` + ((x20_ref:((regstate),(register_value),((32)words$word))register_ref)= (<| + name := "x20"; + read_from := (\ s . s.x20); + write_to := (\ v s . (( s with<| x20 := v |>))); + of_regval := (\ v . vector_32_dec_bit_of_regval v); + regval_of := (\ v . regval_of_vector_32_dec_bit v) |>))`; + + +val _ = Define ` + ((x19_ref:((regstate),(register_value),((32)words$word))register_ref)= (<| + name := "x19"; + read_from := (\ s . s.x19); + write_to := (\ v s . (( s with<| x19 := v |>))); + of_regval := (\ v . vector_32_dec_bit_of_regval v); + regval_of := (\ v . regval_of_vector_32_dec_bit v) |>))`; + + +val _ = Define ` + ((x18_ref:((regstate),(register_value),((32)words$word))register_ref)= (<| + name := "x18"; + read_from := (\ s . s.x18); + write_to := (\ v s . (( s with<| x18 := v |>))); + of_regval := (\ v . vector_32_dec_bit_of_regval v); + regval_of := (\ v . regval_of_vector_32_dec_bit v) |>))`; + + +val _ = Define ` + ((x17_ref:((regstate),(register_value),((32)words$word))register_ref)= (<| + name := "x17"; + read_from := (\ s . s.x17); + write_to := (\ v s . (( s with<| x17 := v |>))); + of_regval := (\ v . vector_32_dec_bit_of_regval v); + regval_of := (\ v . regval_of_vector_32_dec_bit v) |>))`; + + +val _ = Define ` + ((x16_ref:((regstate),(register_value),((32)words$word))register_ref)= (<| + name := "x16"; + read_from := (\ s . s.x16); + write_to := (\ v s . (( s with<| x16 := v |>))); + of_regval := (\ v . vector_32_dec_bit_of_regval v); + regval_of := (\ v . regval_of_vector_32_dec_bit v) |>))`; + + +val _ = Define ` + ((x15_ref:((regstate),(register_value),((32)words$word))register_ref)= (<| + name := "x15"; + read_from := (\ s . s.x15); + write_to := (\ v s . (( s with<| x15 := v |>))); + of_regval := (\ v . vector_32_dec_bit_of_regval v); + regval_of := (\ v . regval_of_vector_32_dec_bit v) |>))`; + + +val _ = Define ` + ((x14_ref:((regstate),(register_value),((32)words$word))register_ref)= (<| + name := "x14"; + read_from := (\ s . s.x14); + write_to := (\ v s . (( s with<| x14 := v |>))); + of_regval := (\ v . vector_32_dec_bit_of_regval v); + regval_of := (\ v . regval_of_vector_32_dec_bit v) |>))`; + + +val _ = Define ` + ((x13_ref:((regstate),(register_value),((32)words$word))register_ref)= (<| + name := "x13"; + read_from := (\ s . s.x13); + write_to := (\ v s . (( s with<| x13 := v |>))); + of_regval := (\ v . vector_32_dec_bit_of_regval v); + regval_of := (\ v . regval_of_vector_32_dec_bit v) |>))`; + + +val _ = Define ` + ((x12_ref:((regstate),(register_value),((32)words$word))register_ref)= (<| + name := "x12"; + read_from := (\ s . s.x12); + write_to := (\ v s . (( s with<| x12 := v |>))); + of_regval := (\ v . vector_32_dec_bit_of_regval v); + regval_of := (\ v . regval_of_vector_32_dec_bit v) |>))`; + + +val _ = Define ` + ((x11_ref:((regstate),(register_value),((32)words$word))register_ref)= (<| + name := "x11"; + read_from := (\ s . s.x11); + write_to := (\ v s . (( s with<| x11 := v |>))); + of_regval := (\ v . vector_32_dec_bit_of_regval v); + regval_of := (\ v . regval_of_vector_32_dec_bit v) |>))`; + + +val _ = Define ` + ((x10_ref:((regstate),(register_value),((32)words$word))register_ref)= (<| + name := "x10"; + read_from := (\ s . s.x10); + write_to := (\ v s . (( s with<| x10 := v |>))); + of_regval := (\ v . vector_32_dec_bit_of_regval v); + regval_of := (\ v . regval_of_vector_32_dec_bit v) |>))`; + + +val _ = Define ` + ((x9_ref:((regstate),(register_value),((32)words$word))register_ref)= (<| + name := "x9"; + read_from := (\ s . s.x9); + write_to := (\ v s . (( s with<| x9 := v |>))); + of_regval := (\ v . vector_32_dec_bit_of_regval v); + regval_of := (\ v . regval_of_vector_32_dec_bit v) |>))`; + + +val _ = Define ` + ((x8_ref:((regstate),(register_value),((32)words$word))register_ref)= (<| + name := "x8"; + read_from := (\ s . s.x8); + write_to := (\ v s . (( s with<| x8 := v |>))); + of_regval := (\ v . vector_32_dec_bit_of_regval v); + regval_of := (\ v . regval_of_vector_32_dec_bit v) |>))`; + + +val _ = Define ` + ((x7_ref:((regstate),(register_value),((32)words$word))register_ref)= (<| + name := "x7"; + read_from := (\ s . s.x7); + write_to := (\ v s . (( s with<| x7 := v |>))); + of_regval := (\ v . vector_32_dec_bit_of_regval v); + regval_of := (\ v . regval_of_vector_32_dec_bit v) |>))`; + + +val _ = Define ` + ((x6_ref:((regstate),(register_value),((32)words$word))register_ref)= (<| + name := "x6"; + read_from := (\ s . s.x6); + write_to := (\ v s . (( s with<| x6 := v |>))); + of_regval := (\ v . vector_32_dec_bit_of_regval v); + regval_of := (\ v . regval_of_vector_32_dec_bit v) |>))`; + + +val _ = Define ` + ((x5_ref:((regstate),(register_value),((32)words$word))register_ref)= (<| + name := "x5"; + read_from := (\ s . s.x5); + write_to := (\ v s . (( s with<| x5 := v |>))); + of_regval := (\ v . vector_32_dec_bit_of_regval v); + regval_of := (\ v . regval_of_vector_32_dec_bit v) |>))`; + + +val _ = Define ` + ((x4_ref:((regstate),(register_value),((32)words$word))register_ref)= (<| + name := "x4"; + read_from := (\ s . s.x4); + write_to := (\ v s . (( s with<| x4 := v |>))); + of_regval := (\ v . vector_32_dec_bit_of_regval v); + regval_of := (\ v . regval_of_vector_32_dec_bit v) |>))`; + + +val _ = Define ` + ((x3_ref:((regstate),(register_value),((32)words$word))register_ref)= (<| + name := "x3"; + read_from := (\ s . s.x3); + write_to := (\ v s . (( s with<| x3 := v |>))); + of_regval := (\ v . vector_32_dec_bit_of_regval v); + regval_of := (\ v . regval_of_vector_32_dec_bit v) |>))`; + + +val _ = Define ` + ((x2_ref:((regstate),(register_value),((32)words$word))register_ref)= (<| + name := "x2"; + read_from := (\ s . s.x2); + write_to := (\ v s . (( s with<| x2 := v |>))); + of_regval := (\ v . vector_32_dec_bit_of_regval v); + regval_of := (\ v . regval_of_vector_32_dec_bit v) |>))`; + + +val _ = Define ` + ((x1_ref:((regstate),(register_value),((32)words$word))register_ref)= (<| + name := "x1"; + read_from := (\ s . s.x1); + write_to := (\ v s . (( s with<| x1 := v |>))); + of_regval := (\ v . vector_32_dec_bit_of_regval v); + regval_of := (\ v . regval_of_vector_32_dec_bit v) |>))`; + + +val _ = Define ` + ((Xs_ref:((regstate),(register_value),(((32)words$word)list))register_ref)= (<| + name := "Xs"; + read_from := (\ s . s.Xs); + write_to := (\ v s . (( s with<| Xs := v |>))); + of_regval := (\ v . vector_of_regval (\ v . vector_32_dec_bit_of_regval v) v); + regval_of := (\ v . regval_of_vector (\ v . regval_of_vector_32_dec_bit v)(( 32 : int)) F v) |>))`; + + +val _ = Define ` + ((instbits_ref:((regstate),(register_value),((32)words$word))register_ref)= (<| + name := "instbits"; + read_from := (\ s . s.instbits); + write_to := (\ v s . (( s with<| instbits := v |>))); + of_regval := (\ v . vector_32_dec_bit_of_regval v); + regval_of := (\ v . regval_of_vector_32_dec_bit v) |>))`; + + +val _ = Define ` + ((nextPC_ref:((regstate),(register_value),((32)words$word))register_ref)= (<| + name := "nextPC"; + read_from := (\ s . s.nextPC); + write_to := (\ v s . (( s with<| nextPC := v |>))); + of_regval := (\ v . vector_32_dec_bit_of_regval v); + regval_of := (\ v . regval_of_vector_32_dec_bit v) |>))`; + + +val _ = Define ` + ((PC_ref:((regstate),(register_value),((32)words$word))register_ref)= (<| + name := "PC"; + read_from := (\ s . s.PC); + write_to := (\ v s . (( s with<| PC := v |>))); + of_regval := (\ v . vector_32_dec_bit_of_regval v); + regval_of := (\ v . regval_of_vector_32_dec_bit v) |>))`; + + +(*val get_regval : string -> regstate -> maybe register_value*) +val _ = Define ` + ((get_regval:string -> regstate ->(register_value)option) reg_name s= + (if reg_name = "satp" then SOME (satp_ref.regval_of (satp_ref.read_from s)) else + if reg_name = "tlb32" then SOME (tlb32_ref.regval_of (tlb32_ref.read_from s)) else + if reg_name = "htif_exit_code" then SOME (htif_exit_code_ref.regval_of (htif_exit_code_ref.read_from s)) else + if reg_name = "htif_done" then SOME (htif_done_ref.regval_of (htif_done_ref.read_from s)) else + if reg_name = "htif_tohost" then SOME (htif_tohost_ref.regval_of (htif_tohost_ref.read_from s)) else + if reg_name = "mtimecmp" then SOME (mtimecmp_ref.regval_of (mtimecmp_ref.read_from s)) else + if reg_name = "utval" then SOME (utval_ref.regval_of (utval_ref.read_from s)) else + if reg_name = "ucause" then SOME (ucause_ref.regval_of (ucause_ref.read_from s)) else + if reg_name = "uepc" then SOME (uepc_ref.regval_of (uepc_ref.read_from s)) else + if reg_name = "uscratch" then SOME (uscratch_ref.regval_of (uscratch_ref.read_from s)) else + if reg_name = "utvec" then SOME (utvec_ref.regval_of (utvec_ref.read_from s)) else + if reg_name = "pmpaddr15" then SOME (pmpaddr15_ref.regval_of (pmpaddr15_ref.read_from s)) else + if reg_name = "pmpaddr14" then SOME (pmpaddr14_ref.regval_of (pmpaddr14_ref.read_from s)) else + if reg_name = "pmpaddr13" then SOME (pmpaddr13_ref.regval_of (pmpaddr13_ref.read_from s)) else + if reg_name = "pmpaddr12" then SOME (pmpaddr12_ref.regval_of (pmpaddr12_ref.read_from s)) else + if reg_name = "pmpaddr11" then SOME (pmpaddr11_ref.regval_of (pmpaddr11_ref.read_from s)) else + if reg_name = "pmpaddr10" then SOME (pmpaddr10_ref.regval_of (pmpaddr10_ref.read_from s)) else + if reg_name = "pmpaddr9" then SOME (pmpaddr9_ref.regval_of (pmpaddr9_ref.read_from s)) else + if reg_name = "pmpaddr8" then SOME (pmpaddr8_ref.regval_of (pmpaddr8_ref.read_from s)) else + if reg_name = "pmpaddr7" then SOME (pmpaddr7_ref.regval_of (pmpaddr7_ref.read_from s)) else + if reg_name = "pmpaddr6" then SOME (pmpaddr6_ref.regval_of (pmpaddr6_ref.read_from s)) else + if reg_name = "pmpaddr5" then SOME (pmpaddr5_ref.regval_of (pmpaddr5_ref.read_from s)) else + if reg_name = "pmpaddr4" then SOME (pmpaddr4_ref.regval_of (pmpaddr4_ref.read_from s)) else + if reg_name = "pmpaddr3" then SOME (pmpaddr3_ref.regval_of (pmpaddr3_ref.read_from s)) else + if reg_name = "pmpaddr2" then SOME (pmpaddr2_ref.regval_of (pmpaddr2_ref.read_from s)) else + if reg_name = "pmpaddr1" then SOME (pmpaddr1_ref.regval_of (pmpaddr1_ref.read_from s)) else + if reg_name = "pmpaddr0" then SOME (pmpaddr0_ref.regval_of (pmpaddr0_ref.read_from s)) else + if reg_name = "pmp15cfg" then SOME (pmp15cfg_ref.regval_of (pmp15cfg_ref.read_from s)) else + if reg_name = "pmp14cfg" then SOME (pmp14cfg_ref.regval_of (pmp14cfg_ref.read_from s)) else + if reg_name = "pmp13cfg" then SOME (pmp13cfg_ref.regval_of (pmp13cfg_ref.read_from s)) else + if reg_name = "pmp12cfg" then SOME (pmp12cfg_ref.regval_of (pmp12cfg_ref.read_from s)) else + if reg_name = "pmp11cfg" then SOME (pmp11cfg_ref.regval_of (pmp11cfg_ref.read_from s)) else + if reg_name = "pmp10cfg" then SOME (pmp10cfg_ref.regval_of (pmp10cfg_ref.read_from s)) else + if reg_name = "pmp9cfg" then SOME (pmp9cfg_ref.regval_of (pmp9cfg_ref.read_from s)) else + if reg_name = "pmp8cfg" then SOME (pmp8cfg_ref.regval_of (pmp8cfg_ref.read_from s)) else + if reg_name = "pmp7cfg" then SOME (pmp7cfg_ref.regval_of (pmp7cfg_ref.read_from s)) else + if reg_name = "pmp6cfg" then SOME (pmp6cfg_ref.regval_of (pmp6cfg_ref.read_from s)) else + if reg_name = "pmp5cfg" then SOME (pmp5cfg_ref.regval_of (pmp5cfg_ref.read_from s)) else + if reg_name = "pmp4cfg" then SOME (pmp4cfg_ref.regval_of (pmp4cfg_ref.read_from s)) else + if reg_name = "pmp3cfg" then SOME (pmp3cfg_ref.regval_of (pmp3cfg_ref.read_from s)) else + if reg_name = "pmp2cfg" then SOME (pmp2cfg_ref.regval_of (pmp2cfg_ref.read_from s)) else + if reg_name = "pmp1cfg" then SOME (pmp1cfg_ref.regval_of (pmp1cfg_ref.read_from s)) else + if reg_name = "pmp0cfg" then SOME (pmp0cfg_ref.regval_of (pmp0cfg_ref.read_from s)) else + if reg_name = "tselect" then SOME (tselect_ref.regval_of (tselect_ref.read_from s)) else + if reg_name = "stval" then SOME (stval_ref.regval_of (stval_ref.read_from s)) else + if reg_name = "scause" then SOME (scause_ref.regval_of (scause_ref.read_from s)) else + if reg_name = "sepc" then SOME (sepc_ref.regval_of (sepc_ref.read_from s)) else + if reg_name = "sscratch" then SOME (sscratch_ref.regval_of (sscratch_ref.read_from s)) else + if reg_name = "stvec" then SOME (stvec_ref.regval_of (stvec_ref.read_from s)) else + if reg_name = "sideleg" then SOME (sideleg_ref.regval_of (sideleg_ref.read_from s)) else + if reg_name = "sedeleg" then SOME (sedeleg_ref.regval_of (sedeleg_ref.read_from s)) else + if reg_name = "mhartid" then SOME (mhartid_ref.regval_of (mhartid_ref.read_from s)) else + if reg_name = "marchid" then SOME (marchid_ref.regval_of (marchid_ref.read_from s)) else + if reg_name = "mimpid" then SOME (mimpid_ref.regval_of (mimpid_ref.read_from s)) else + if reg_name = "mvendorid" then SOME (mvendorid_ref.regval_of (mvendorid_ref.read_from s)) else + if reg_name = "minstret_written" then SOME (minstret_written_ref.regval_of (minstret_written_ref.read_from s)) else + if reg_name = "minstret" then SOME (minstret_ref.regval_of (minstret_ref.read_from s)) else + if reg_name = "mtime" then SOME (mtime_ref.regval_of (mtime_ref.read_from s)) else + if reg_name = "mcycle" then SOME (mcycle_ref.regval_of (mcycle_ref.read_from s)) else + if reg_name = "scounteren" then SOME (scounteren_ref.regval_of (scounteren_ref.read_from s)) else + if reg_name = "mcounteren" then SOME (mcounteren_ref.regval_of (mcounteren_ref.read_from s)) else + if reg_name = "mscratch" then SOME (mscratch_ref.regval_of (mscratch_ref.read_from s)) else + if reg_name = "mtval" then SOME (mtval_ref.regval_of (mtval_ref.read_from s)) else + if reg_name = "mepc" then SOME (mepc_ref.regval_of (mepc_ref.read_from s)) else + if reg_name = "mcause" then SOME (mcause_ref.regval_of (mcause_ref.read_from s)) else + if reg_name = "mtvec" then SOME (mtvec_ref.regval_of (mtvec_ref.read_from s)) else + if reg_name = "medeleg" then SOME (medeleg_ref.regval_of (medeleg_ref.read_from s)) else + if reg_name = "mideleg" then SOME (mideleg_ref.regval_of (mideleg_ref.read_from s)) else + if reg_name = "mie" then SOME (mie_ref.regval_of (mie_ref.read_from s)) else + if reg_name = "mip" then SOME (mip_ref.regval_of (mip_ref.read_from s)) else + if reg_name = "mstatus" then SOME (mstatus_ref.regval_of (mstatus_ref.read_from s)) else + if reg_name = "misa" then SOME (misa_ref.regval_of (misa_ref.read_from s)) else + if reg_name = "cur_inst" then SOME (cur_inst_ref.regval_of (cur_inst_ref.read_from s)) else + if reg_name = "cur_privilege" then SOME (cur_privilege_ref.regval_of (cur_privilege_ref.read_from s)) else + if reg_name = "x31" then SOME (x31_ref.regval_of (x31_ref.read_from s)) else + if reg_name = "x30" then SOME (x30_ref.regval_of (x30_ref.read_from s)) else + if reg_name = "x29" then SOME (x29_ref.regval_of (x29_ref.read_from s)) else + if reg_name = "x28" then SOME (x28_ref.regval_of (x28_ref.read_from s)) else + if reg_name = "x27" then SOME (x27_ref.regval_of (x27_ref.read_from s)) else + if reg_name = "x26" then SOME (x26_ref.regval_of (x26_ref.read_from s)) else + if reg_name = "x25" then SOME (x25_ref.regval_of (x25_ref.read_from s)) else + if reg_name = "x24" then SOME (x24_ref.regval_of (x24_ref.read_from s)) else + if reg_name = "x23" then SOME (x23_ref.regval_of (x23_ref.read_from s)) else + if reg_name = "x22" then SOME (x22_ref.regval_of (x22_ref.read_from s)) else + if reg_name = "x21" then SOME (x21_ref.regval_of (x21_ref.read_from s)) else + if reg_name = "x20" then SOME (x20_ref.regval_of (x20_ref.read_from s)) else + if reg_name = "x19" then SOME (x19_ref.regval_of (x19_ref.read_from s)) else + if reg_name = "x18" then SOME (x18_ref.regval_of (x18_ref.read_from s)) else + if reg_name = "x17" then SOME (x17_ref.regval_of (x17_ref.read_from s)) else + if reg_name = "x16" then SOME (x16_ref.regval_of (x16_ref.read_from s)) else + if reg_name = "x15" then SOME (x15_ref.regval_of (x15_ref.read_from s)) else + if reg_name = "x14" then SOME (x14_ref.regval_of (x14_ref.read_from s)) else + if reg_name = "x13" then SOME (x13_ref.regval_of (x13_ref.read_from s)) else + if reg_name = "x12" then SOME (x12_ref.regval_of (x12_ref.read_from s)) else + if reg_name = "x11" then SOME (x11_ref.regval_of (x11_ref.read_from s)) else + if reg_name = "x10" then SOME (x10_ref.regval_of (x10_ref.read_from s)) else + if reg_name = "x9" then SOME (x9_ref.regval_of (x9_ref.read_from s)) else + if reg_name = "x8" then SOME (x8_ref.regval_of (x8_ref.read_from s)) else + if reg_name = "x7" then SOME (x7_ref.regval_of (x7_ref.read_from s)) else + if reg_name = "x6" then SOME (x6_ref.regval_of (x6_ref.read_from s)) else + if reg_name = "x5" then SOME (x5_ref.regval_of (x5_ref.read_from s)) else + if reg_name = "x4" then SOME (x4_ref.regval_of (x4_ref.read_from s)) else + if reg_name = "x3" then SOME (x3_ref.regval_of (x3_ref.read_from s)) else + if reg_name = "x2" then SOME (x2_ref.regval_of (x2_ref.read_from s)) else + if reg_name = "x1" then SOME (x1_ref.regval_of (x1_ref.read_from s)) else + if reg_name = "Xs" then SOME (Xs_ref.regval_of (Xs_ref.read_from s)) else + if reg_name = "instbits" then SOME (instbits_ref.regval_of (instbits_ref.read_from s)) else + if reg_name = "nextPC" then SOME (nextPC_ref.regval_of (nextPC_ref.read_from s)) else + if reg_name = "PC" then SOME (PC_ref.regval_of (PC_ref.read_from s)) else + NONE))`; + + +(*val set_regval : string -> register_value -> regstate -> maybe regstate*) +val _ = Define ` + ((set_regval:string -> register_value -> regstate ->(regstate)option) reg_name v s= + (if reg_name = "satp" then OPTION_MAP (\ v . satp_ref.write_to v s) (satp_ref.of_regval v) else + if reg_name = "tlb32" then OPTION_MAP (\ v . tlb32_ref.write_to v s) (tlb32_ref.of_regval v) else + if reg_name = "htif_exit_code" then OPTION_MAP (\ v . htif_exit_code_ref.write_to v s) (htif_exit_code_ref.of_regval v) else + if reg_name = "htif_done" then OPTION_MAP (\ v . htif_done_ref.write_to v s) (htif_done_ref.of_regval v) else + if reg_name = "htif_tohost" then OPTION_MAP (\ v . htif_tohost_ref.write_to v s) (htif_tohost_ref.of_regval v) else + if reg_name = "mtimecmp" then OPTION_MAP (\ v . mtimecmp_ref.write_to v s) (mtimecmp_ref.of_regval v) else + if reg_name = "utval" then OPTION_MAP (\ v . utval_ref.write_to v s) (utval_ref.of_regval v) else + if reg_name = "ucause" then OPTION_MAP (\ v . ucause_ref.write_to v s) (ucause_ref.of_regval v) else + if reg_name = "uepc" then OPTION_MAP (\ v . uepc_ref.write_to v s) (uepc_ref.of_regval v) else + if reg_name = "uscratch" then OPTION_MAP (\ v . uscratch_ref.write_to v s) (uscratch_ref.of_regval v) else + if reg_name = "utvec" then OPTION_MAP (\ v . utvec_ref.write_to v s) (utvec_ref.of_regval v) else + if reg_name = "pmpaddr15" then OPTION_MAP (\ v . pmpaddr15_ref.write_to v s) (pmpaddr15_ref.of_regval v) else + if reg_name = "pmpaddr14" then OPTION_MAP (\ v . pmpaddr14_ref.write_to v s) (pmpaddr14_ref.of_regval v) else + if reg_name = "pmpaddr13" then OPTION_MAP (\ v . pmpaddr13_ref.write_to v s) (pmpaddr13_ref.of_regval v) else + if reg_name = "pmpaddr12" then OPTION_MAP (\ v . pmpaddr12_ref.write_to v s) (pmpaddr12_ref.of_regval v) else + if reg_name = "pmpaddr11" then OPTION_MAP (\ v . pmpaddr11_ref.write_to v s) (pmpaddr11_ref.of_regval v) else + if reg_name = "pmpaddr10" then OPTION_MAP (\ v . pmpaddr10_ref.write_to v s) (pmpaddr10_ref.of_regval v) else + if reg_name = "pmpaddr9" then OPTION_MAP (\ v . pmpaddr9_ref.write_to v s) (pmpaddr9_ref.of_regval v) else + if reg_name = "pmpaddr8" then OPTION_MAP (\ v . pmpaddr8_ref.write_to v s) (pmpaddr8_ref.of_regval v) else + if reg_name = "pmpaddr7" then OPTION_MAP (\ v . pmpaddr7_ref.write_to v s) (pmpaddr7_ref.of_regval v) else + if reg_name = "pmpaddr6" then OPTION_MAP (\ v . pmpaddr6_ref.write_to v s) (pmpaddr6_ref.of_regval v) else + if reg_name = "pmpaddr5" then OPTION_MAP (\ v . pmpaddr5_ref.write_to v s) (pmpaddr5_ref.of_regval v) else + if reg_name = "pmpaddr4" then OPTION_MAP (\ v . pmpaddr4_ref.write_to v s) (pmpaddr4_ref.of_regval v) else + if reg_name = "pmpaddr3" then OPTION_MAP (\ v . pmpaddr3_ref.write_to v s) (pmpaddr3_ref.of_regval v) else + if reg_name = "pmpaddr2" then OPTION_MAP (\ v . pmpaddr2_ref.write_to v s) (pmpaddr2_ref.of_regval v) else + if reg_name = "pmpaddr1" then OPTION_MAP (\ v . pmpaddr1_ref.write_to v s) (pmpaddr1_ref.of_regval v) else + if reg_name = "pmpaddr0" then OPTION_MAP (\ v . pmpaddr0_ref.write_to v s) (pmpaddr0_ref.of_regval v) else + if reg_name = "pmp15cfg" then OPTION_MAP (\ v . pmp15cfg_ref.write_to v s) (pmp15cfg_ref.of_regval v) else + if reg_name = "pmp14cfg" then OPTION_MAP (\ v . pmp14cfg_ref.write_to v s) (pmp14cfg_ref.of_regval v) else + if reg_name = "pmp13cfg" then OPTION_MAP (\ v . pmp13cfg_ref.write_to v s) (pmp13cfg_ref.of_regval v) else + if reg_name = "pmp12cfg" then OPTION_MAP (\ v . pmp12cfg_ref.write_to v s) (pmp12cfg_ref.of_regval v) else + if reg_name = "pmp11cfg" then OPTION_MAP (\ v . pmp11cfg_ref.write_to v s) (pmp11cfg_ref.of_regval v) else + if reg_name = "pmp10cfg" then OPTION_MAP (\ v . pmp10cfg_ref.write_to v s) (pmp10cfg_ref.of_regval v) else + if reg_name = "pmp9cfg" then OPTION_MAP (\ v . pmp9cfg_ref.write_to v s) (pmp9cfg_ref.of_regval v) else + if reg_name = "pmp8cfg" then OPTION_MAP (\ v . pmp8cfg_ref.write_to v s) (pmp8cfg_ref.of_regval v) else + if reg_name = "pmp7cfg" then OPTION_MAP (\ v . pmp7cfg_ref.write_to v s) (pmp7cfg_ref.of_regval v) else + if reg_name = "pmp6cfg" then OPTION_MAP (\ v . pmp6cfg_ref.write_to v s) (pmp6cfg_ref.of_regval v) else + if reg_name = "pmp5cfg" then OPTION_MAP (\ v . pmp5cfg_ref.write_to v s) (pmp5cfg_ref.of_regval v) else + if reg_name = "pmp4cfg" then OPTION_MAP (\ v . pmp4cfg_ref.write_to v s) (pmp4cfg_ref.of_regval v) else + if reg_name = "pmp3cfg" then OPTION_MAP (\ v . pmp3cfg_ref.write_to v s) (pmp3cfg_ref.of_regval v) else + if reg_name = "pmp2cfg" then OPTION_MAP (\ v . pmp2cfg_ref.write_to v s) (pmp2cfg_ref.of_regval v) else + if reg_name = "pmp1cfg" then OPTION_MAP (\ v . pmp1cfg_ref.write_to v s) (pmp1cfg_ref.of_regval v) else + if reg_name = "pmp0cfg" then OPTION_MAP (\ v . pmp0cfg_ref.write_to v s) (pmp0cfg_ref.of_regval v) else + if reg_name = "tselect" then OPTION_MAP (\ v . tselect_ref.write_to v s) (tselect_ref.of_regval v) else + if reg_name = "stval" then OPTION_MAP (\ v . stval_ref.write_to v s) (stval_ref.of_regval v) else + if reg_name = "scause" then OPTION_MAP (\ v . scause_ref.write_to v s) (scause_ref.of_regval v) else + if reg_name = "sepc" then OPTION_MAP (\ v . sepc_ref.write_to v s) (sepc_ref.of_regval v) else + if reg_name = "sscratch" then OPTION_MAP (\ v . sscratch_ref.write_to v s) (sscratch_ref.of_regval v) else + if reg_name = "stvec" then OPTION_MAP (\ v . stvec_ref.write_to v s) (stvec_ref.of_regval v) else + if reg_name = "sideleg" then OPTION_MAP (\ v . sideleg_ref.write_to v s) (sideleg_ref.of_regval v) else + if reg_name = "sedeleg" then OPTION_MAP (\ v . sedeleg_ref.write_to v s) (sedeleg_ref.of_regval v) else + if reg_name = "mhartid" then OPTION_MAP (\ v . mhartid_ref.write_to v s) (mhartid_ref.of_regval v) else + if reg_name = "marchid" then OPTION_MAP (\ v . marchid_ref.write_to v s) (marchid_ref.of_regval v) else + if reg_name = "mimpid" then OPTION_MAP (\ v . mimpid_ref.write_to v s) (mimpid_ref.of_regval v) else + if reg_name = "mvendorid" then OPTION_MAP (\ v . mvendorid_ref.write_to v s) (mvendorid_ref.of_regval v) else + if reg_name = "minstret_written" then OPTION_MAP (\ v . minstret_written_ref.write_to v s) (minstret_written_ref.of_regval v) else + if reg_name = "minstret" then OPTION_MAP (\ v . minstret_ref.write_to v s) (minstret_ref.of_regval v) else + if reg_name = "mtime" then OPTION_MAP (\ v . mtime_ref.write_to v s) (mtime_ref.of_regval v) else + if reg_name = "mcycle" then OPTION_MAP (\ v . mcycle_ref.write_to v s) (mcycle_ref.of_regval v) else + if reg_name = "scounteren" then OPTION_MAP (\ v . scounteren_ref.write_to v s) (scounteren_ref.of_regval v) else + if reg_name = "mcounteren" then OPTION_MAP (\ v . mcounteren_ref.write_to v s) (mcounteren_ref.of_regval v) else + if reg_name = "mscratch" then OPTION_MAP (\ v . mscratch_ref.write_to v s) (mscratch_ref.of_regval v) else + if reg_name = "mtval" then OPTION_MAP (\ v . mtval_ref.write_to v s) (mtval_ref.of_regval v) else + if reg_name = "mepc" then OPTION_MAP (\ v . mepc_ref.write_to v s) (mepc_ref.of_regval v) else + if reg_name = "mcause" then OPTION_MAP (\ v . mcause_ref.write_to v s) (mcause_ref.of_regval v) else + if reg_name = "mtvec" then OPTION_MAP (\ v . mtvec_ref.write_to v s) (mtvec_ref.of_regval v) else + if reg_name = "medeleg" then OPTION_MAP (\ v . medeleg_ref.write_to v s) (medeleg_ref.of_regval v) else + if reg_name = "mideleg" then OPTION_MAP (\ v . mideleg_ref.write_to v s) (mideleg_ref.of_regval v) else + if reg_name = "mie" then OPTION_MAP (\ v . mie_ref.write_to v s) (mie_ref.of_regval v) else + if reg_name = "mip" then OPTION_MAP (\ v . mip_ref.write_to v s) (mip_ref.of_regval v) else + if reg_name = "mstatus" then OPTION_MAP (\ v . mstatus_ref.write_to v s) (mstatus_ref.of_regval v) else + if reg_name = "misa" then OPTION_MAP (\ v . misa_ref.write_to v s) (misa_ref.of_regval v) else + if reg_name = "cur_inst" then OPTION_MAP (\ v . cur_inst_ref.write_to v s) (cur_inst_ref.of_regval v) else + if reg_name = "cur_privilege" then OPTION_MAP (\ v . cur_privilege_ref.write_to v s) (cur_privilege_ref.of_regval v) else + if reg_name = "x31" then OPTION_MAP (\ v . x31_ref.write_to v s) (x31_ref.of_regval v) else + if reg_name = "x30" then OPTION_MAP (\ v . x30_ref.write_to v s) (x30_ref.of_regval v) else + if reg_name = "x29" then OPTION_MAP (\ v . x29_ref.write_to v s) (x29_ref.of_regval v) else + if reg_name = "x28" then OPTION_MAP (\ v . x28_ref.write_to v s) (x28_ref.of_regval v) else + if reg_name = "x27" then OPTION_MAP (\ v . x27_ref.write_to v s) (x27_ref.of_regval v) else + if reg_name = "x26" then OPTION_MAP (\ v . x26_ref.write_to v s) (x26_ref.of_regval v) else + if reg_name = "x25" then OPTION_MAP (\ v . x25_ref.write_to v s) (x25_ref.of_regval v) else + if reg_name = "x24" then OPTION_MAP (\ v . x24_ref.write_to v s) (x24_ref.of_regval v) else + if reg_name = "x23" then OPTION_MAP (\ v . x23_ref.write_to v s) (x23_ref.of_regval v) else + if reg_name = "x22" then OPTION_MAP (\ v . x22_ref.write_to v s) (x22_ref.of_regval v) else + if reg_name = "x21" then OPTION_MAP (\ v . x21_ref.write_to v s) (x21_ref.of_regval v) else + if reg_name = "x20" then OPTION_MAP (\ v . x20_ref.write_to v s) (x20_ref.of_regval v) else + if reg_name = "x19" then OPTION_MAP (\ v . x19_ref.write_to v s) (x19_ref.of_regval v) else + if reg_name = "x18" then OPTION_MAP (\ v . x18_ref.write_to v s) (x18_ref.of_regval v) else + if reg_name = "x17" then OPTION_MAP (\ v . x17_ref.write_to v s) (x17_ref.of_regval v) else + if reg_name = "x16" then OPTION_MAP (\ v . x16_ref.write_to v s) (x16_ref.of_regval v) else + if reg_name = "x15" then OPTION_MAP (\ v . x15_ref.write_to v s) (x15_ref.of_regval v) else + if reg_name = "x14" then OPTION_MAP (\ v . x14_ref.write_to v s) (x14_ref.of_regval v) else + if reg_name = "x13" then OPTION_MAP (\ v . x13_ref.write_to v s) (x13_ref.of_regval v) else + if reg_name = "x12" then OPTION_MAP (\ v . x12_ref.write_to v s) (x12_ref.of_regval v) else + if reg_name = "x11" then OPTION_MAP (\ v . x11_ref.write_to v s) (x11_ref.of_regval v) else + if reg_name = "x10" then OPTION_MAP (\ v . x10_ref.write_to v s) (x10_ref.of_regval v) else + if reg_name = "x9" then OPTION_MAP (\ v . x9_ref.write_to v s) (x9_ref.of_regval v) else + if reg_name = "x8" then OPTION_MAP (\ v . x8_ref.write_to v s) (x8_ref.of_regval v) else + if reg_name = "x7" then OPTION_MAP (\ v . x7_ref.write_to v s) (x7_ref.of_regval v) else + if reg_name = "x6" then OPTION_MAP (\ v . x6_ref.write_to v s) (x6_ref.of_regval v) else + if reg_name = "x5" then OPTION_MAP (\ v . x5_ref.write_to v s) (x5_ref.of_regval v) else + if reg_name = "x4" then OPTION_MAP (\ v . x4_ref.write_to v s) (x4_ref.of_regval v) else + if reg_name = "x3" then OPTION_MAP (\ v . x3_ref.write_to v s) (x3_ref.of_regval v) else + if reg_name = "x2" then OPTION_MAP (\ v . x2_ref.write_to v s) (x2_ref.of_regval v) else + if reg_name = "x1" then OPTION_MAP (\ v . x1_ref.write_to v s) (x1_ref.of_regval v) else + if reg_name = "Xs" then OPTION_MAP (\ v . Xs_ref.write_to v s) (Xs_ref.of_regval v) else + if reg_name = "instbits" then OPTION_MAP (\ v . instbits_ref.write_to v s) (instbits_ref.of_regval v) else + if reg_name = "nextPC" then OPTION_MAP (\ v . nextPC_ref.write_to v s) (nextPC_ref.of_regval v) else + if reg_name = "PC" then OPTION_MAP (\ v . PC_ref.write_to v s) (PC_ref.of_regval v) else + NONE))`; + + +val _ = Define ` + ((register_accessors:(string -> regstate ->(register_value)option)#(string -> register_value -> regstate ->(regstate)option))= (get_regval, set_regval))`; + + + +val _ = type_abbrev((* ( 'a, 'r) *) "MR" , ``: (regstate, 'a, 'r, exception)monadR``); +val _ = type_abbrev((* 'a *) "M" , ``: (regstate, 'a, exception)monad``); +val _ = export_theory() + |