aboutsummaryrefslogtreecommitdiff
path: root/prover_snapshots/hol4/RV32/riscv_typesScript.sml
diff options
context:
space:
mode:
Diffstat (limited to 'prover_snapshots/hol4/RV32/riscv_typesScript.sml')
-rw-r--r--prover_snapshots/hol4/RV32/riscv_typesScript.sml2208
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()
+
generated by cgit v1.1 at 2024-08-16 06:45:43 +0000