diff options
Diffstat (limited to 'snapshots/isabelle/cheri/Cheri.thy')
| -rw-r--r-- | snapshots/isabelle/cheri/Cheri.thy | 822 |
1 files changed, 413 insertions, 409 deletions
diff --git a/snapshots/isabelle/cheri/Cheri.thy b/snapshots/isabelle/cheri/Cheri.thy index af6852b6..e4f28651 100644 --- a/snapshots/isabelle/cheri/Cheri.thy +++ b/snapshots/isabelle/cheri/Cheri.thy @@ -1,18 +1,18 @@ -chapter \<open>Generated by Lem from cheri.lem.\<close> +chapter \<open>Generated by Lem from \<open>cheri.lem\<close>.\<close> theory "Cheri" -imports - Main - "Lem_pervasives_extra" - "Sail2_instr_kinds" - "Sail2_values" - "Sail2_string" - "Sail2_operators_mwords" - "Sail2_prompt_monad" - "Sail2_prompt" - "Cheri_types" - "Mips_extras" +imports + Main + "LEM.Lem_pervasives_extra" + "Sail.Sail2_instr_kinds" + "Sail.Sail2_values" + "Sail.Sail2_string" + "Sail.Sail2_operators_mwords" + "Sail.Sail2_prompt_monad" + "Sail.Sail2_prompt" + "Cheri_types" + "Mips_extras" begin @@ -31,6 +31,12 @@ definition cap_size :: " int " where " cap_size = ( (( 32 :: int)::ii))" +(*val eq_unit : unit -> unit -> bool*) + +definition eq_unit :: " unit \<Rightarrow> unit \<Rightarrow> bool " where + " eq_unit g__20 g__21 = ( True )" + + @@ -48,7 +54,7 @@ definition neq_bool :: " bool \<Rightarrow> bool \<Rightarrow> bool " where definition undefined_option :: " 'a \<Rightarrow>((register_value),('a option),(exception))monad " where " undefined_option typ_a = ( undefined_unit () \<bind> (\<lambda> (u_0 :: unit) . - (let (u_1 :: 'a) = typ_a in + (let u_1 = typ_a in internal_pick [Some u_1,None])))" @@ -94,7 +100,8 @@ definition MIPS_write :: "(64)Word.word \<Rightarrow> int \<Rightarrow>('p8_tim (vec_of_bits [B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0, B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0, B0,B0,B0,B0,B0,B0,B0,B0,B0,B0] - :: 64 Word.word) addr data )" + :: 64 Word.word) addr data \<then> + return () )" (*val __MIPS_read : forall 'p8_times_n_ . Size 'p8_times_n_ => mword ty64 -> integer -> M (mword 'p8_times_n_)*) @@ -1135,20 +1142,20 @@ definition TLBIndexMax :: "(6)Word.word " where (*val MAX : integer -> integer*) -definition MAX :: " int \<Rightarrow> int " where - " MAX n = ( ((pow2 n)) - (( 1 :: int)::ii))" +definition MAX0 :: " int \<Rightarrow> int " where + " MAX0 n = ( ((pow2 n)) - (( 1 :: int)::ii))" definition MAX_U64 :: " int " where - " MAX_U64 = ( MAX (( 64 :: int)::ii))" + " MAX_U64 = ( MAX0 (( 64 :: int)::ii))" definition MAX_VA :: " int " where - " MAX_VA = ( MAX (( 40 :: int)::ii))" + " MAX_VA = ( MAX0 (( 40 :: int)::ii))" definition MAX_PA :: " int " where - " MAX_PA = ( MAX (( 36 :: int)::ii))" + " MAX_PA = ( MAX0 (( 36 :: int)::ii))" (*val undefined_TLBEntry : unit -> M TLBEntry*) @@ -2203,7 +2210,7 @@ definition wGPR :: "(5)Word.word \<Rightarrow>(64)Word.word \<Rightarrow>((regi " wGPR idx v = ( (let i = (Word.uint idx) in if (((i \<noteq> (( 0 :: int)::ii)))) then - read_reg GPR_ref \<bind> (\<lambda> (w__0 :: ( 64 Word.word) list) . + read_reg GPR_ref \<bind> (\<lambda> (w__0 :: ( 64 bits) list) . write_reg GPR_ref ((update_list_dec w__0 i v :: ( 64 Word.word) list))) else return () ))" @@ -2317,7 +2324,7 @@ definition SignalExceptionMIPS :: " Exception \<Rightarrow>(64)Word.word \<Righ ((if ((\<not> ((bits_to_bool ((get_StatusReg_EXL w__0 :: 1 Word.word)))))) then (read_reg inBranchDelay_ref :: ( 1 Word.word) M) \<bind> (\<lambda> (w__1 :: 1 bits) . if ((bit_to_bool ((access_vec_dec w__1 (( 0 :: int)::ii))))) then - (read_reg PC_ref :: ( 64 Word.word) M) \<bind> (\<lambda> (w__2 :: 64 Word.word) . + (read_reg PC_ref :: ( 64 Word.word) M) \<bind> (\<lambda> (w__2 :: 64 bits) . write_reg CP0EPC_ref ((sub_vec_int w__2 (( 4 :: int)::ii) :: 64 Word.word)) \<then> set_CauseReg_BD CP0Cause_ref (vec_of_bits [B1] :: 1 Word.word)) else @@ -2503,7 +2510,7 @@ definition SignalException :: " Exception \<Rightarrow>((register_value),'o,(ex read_reg CP0Status_ref \<bind> (\<lambda> (w__0 :: StatusReg) . ((if ((\<not> ((bits_to_bool ((get_StatusReg_EXL w__0 :: 1 Word.word)))))) then (read_reg PC_ref :: ( 64 Word.word) M) \<bind> (\<lambda> pc . - (read_reg PCC_ref :: ( 257 Word.word) M) \<bind> (\<lambda> (w__1 :: 257 Word.word) . + (read_reg PCC_ref :: ( 257 Word.word) M) \<bind> (\<lambda> (w__1 :: CapReg) . (let pcc = (capRegToCapStruct w__1) in (let (success, epcc) = (setCapOffset pcc pc) in if success then write_reg EPCC_ref ((capStructToCapReg epcc :: 257 Word.word)) @@ -2522,7 +2529,7 @@ definition SignalException :: " Exception \<Rightarrow>((register_value),'o,(ex (write_reg nextPCC_ref w__2 \<then> (read_reg KCC_ref :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__3 :: CapReg) . (write_reg delayedPCC_ref w__3 \<then> - (read_reg KCC_ref :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__4 :: 257 Word.word) . + (read_reg KCC_ref :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__4 :: CapReg) . (let base = (getCapBase ((capRegToCapStruct w__4))) in SignalExceptionMIPS ex ((to_bits ((make_the_value (( 64 :: int)::ii) :: 64 itself)) base :: 64 Word.word))))))))" @@ -2593,7 +2600,7 @@ definition undefined_AccessLevel :: " unit \<Rightarrow>((register_value),(Acce " undefined_AccessLevel _ = ( internal_pick [User,Supervisor,Kernel])" -(*val int_of_AccessLevel : AccessLevel -> ii*) +(*val int_of_AccessLevel : AccessLevel -> integer*) fun int_of_AccessLevel :: " AccessLevel \<Rightarrow> int " where " int_of_AccessLevel User = ( (( 0 :: int)::ii))" @@ -2626,8 +2633,8 @@ definition getAccessLevel :: " unit \<Rightarrow>((register_value),(AccessLevel if w__2 then return Kernel else read_reg CP0Status_ref \<bind> (\<lambda> (w__3 :: StatusReg) . - (let p__31 = ((get_StatusReg_KSU w__3 :: 2 Word.word)) in - (let b__0 = p__31 in + (let p__19 = ((get_StatusReg_KSU w__3 :: 2 Word.word)) in + (let b__0 = p__19 in return (if (((b__0 = (vec_of_bits [B0,B0] :: 2 Word.word)))) then Kernel else if (((b__0 = (vec_of_bits [B0,B1] :: 2 Word.word)))) then Supervisor else if (((b__0 = (vec_of_bits [B1,B0] :: 2 Word.word)))) then User @@ -2653,16 +2660,16 @@ definition checkCP0Access :: " unit \<Rightarrow>((register_value),(unit),(exce definition incrementCP0Count :: " unit \<Rightarrow>((register_value),(unit),(exception))monad " where " incrementCP0Count _ = ( (read_reg TLBRandom_ref :: ( 6 Word.word) M) \<bind> (\<lambda> (w__0 :: TLBIndexT) . - (read_reg TLBWired_ref :: ( 6 Word.word) M) \<bind> (\<lambda> (w__1 :: 6 Word.word) . + (read_reg TLBWired_ref :: ( 6 Word.word) M) \<bind> (\<lambda> (w__1 :: TLBIndexT) . (if (((w__0 = w__1))) then return TLBIndexMax else - (read_reg TLBRandom_ref :: ( 6 Word.word) M) \<bind> (\<lambda> (w__2 :: 6 Word.word) . + (read_reg TLBRandom_ref :: ( 6 Word.word) M) \<bind> (\<lambda> (w__2 :: TLBIndexT) . return ((sub_vec_int w__2 (( 1 :: int)::ii) :: 6 Word.word)))) \<bind> (\<lambda> (w__3 :: 6 Word.word) . (write_reg TLBRandom_ref w__3 \<then> - (read_reg CP0Count_ref :: ( 32 Word.word) M)) \<bind> (\<lambda> (w__4 :: 32 Word.word) . + (read_reg CP0Count_ref :: ( 32 Word.word) M)) \<bind> (\<lambda> (w__4 :: 32 bits) . (write_reg CP0Count_ref ((add_vec_int w__4 (( 1 :: int)::ii) :: 32 Word.word)) \<then> (read_reg CP0Count_ref :: ( 32 Word.word) M)) \<bind> (\<lambda> (w__5 :: 32 bits) . - (read_reg CP0Compare_ref :: ( 32 Word.word) M) \<bind> (\<lambda> (w__6 :: 32 Word.word) . + (read_reg CP0Compare_ref :: ( 32 Word.word) M) \<bind> (\<lambda> (w__6 :: 32 bits) . ((if (((w__5 = w__6))) then read_reg CP0Cause_ref \<bind> (\<lambda> (w__7 :: CauseReg) . set_CauseReg_IP CP0Cause_ref @@ -2907,7 +2914,7 @@ definition extsv :: " int \<Rightarrow>('n::len)Word.word \<Rightarrow>('m::len definition slice_mask :: " int \<Rightarrow> int \<Rightarrow> int \<Rightarrow>('n::len)Word.word " where " slice_mask (n__tv :: int) i l = ( - (let (one :: 'n bits) = ((extzv n__tv (vec_of_bits [B1] :: 1 Word.word) :: ( 'n::len)Word.word)) in + (let one = ((extzv n__tv (vec_of_bits [B1] :: 1 Word.word) :: ( 'n::len)Word.word)) in (shiftl ((sub_vec ((shiftl one l :: ( 'n::len)Word.word)) one :: ( 'n::len)Word.word)) i :: ( 'n::len)Word.word)))" @@ -2924,8 +2931,7 @@ definition is_zero_subrange :: "('n::len)Word.word \<Rightarrow> int \<Rightarr definition is_ones_subrange :: "('n::len)Word.word \<Rightarrow> int \<Rightarrow> int \<Rightarrow> bool " where " is_ones_subrange xs i j = ( - (let (m :: 'n bits) = - ((slice_mask ((int (size xs))) j ((((j - i)) + (( 1 :: int)::ii))) :: ( 'n::len)Word.word)) in + (let m = ((slice_mask ((int (size xs))) j ((((j - i)) + (( 1 :: int)::ii))) :: ( 'n::len)Word.word)) in (((and_vec xs m :: ( 'n::len)Word.word)) = m)))" @@ -3062,7 +3068,7 @@ definition unsigned_subrange :: "('n::len)Word.word \<Rightarrow> int \<Rightar definition zext_ones :: " int \<Rightarrow> int \<Rightarrow>('n::len)Word.word " where " zext_ones (n__tv :: int) m = ( - (let (v :: 'n bits) = ((extsv n__tv (vec_of_bits [B1] :: 1 Word.word) :: ( 'n::len)Word.word)) in + (let v = ((extsv n__tv (vec_of_bits [B1] :: 1 Word.word) :: ( 'n::len)Word.word)) in (shiftr v ((((int (size v))) - m)) :: ( 'n::len)Word.word)))" @@ -3213,8 +3219,8 @@ definition TLBTranslateC :: "(64)Word.word \<Rightarrow> MemAccessType \<Righta ((subrange_vec_dec vAddr (( 28 :: int)::ii) (( 0 :: int)::ii) :: 29 Word.word)) :: 32 Word.word)) :: 64 Word.word))) - else (case (True, b__1) of (g__29, g__30) => (Kernel, None) ) - | (g__29, g__30) => (Kernel, None) + else (case (True, b__1) of (g__17, g__18) => (Kernel, None) ) + | (g__17, g__18) => (Kernel, None) ) else if (((b__0 = (vec_of_bits [B1,B0] :: 2 Word.word)))) then (Kernel, @@ -3315,13 +3321,13 @@ definition undefined_CapStruct :: " unit \<Rightarrow>((register_value),(CapStr " undefined_CapStruct _ = ( undefined_bool () \<bind> (\<lambda> (w__0 :: bool) . (undefined_bitvector - instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 8 :: int)::ii) :: ( 8 Word.word) M) \<bind> (\<lambda> (w__1 :: 8 bits) . + instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 8 :: int)::ii) :: ( 8 Word.word) M) \<bind> (\<lambda> (w__1 :: 8 Word.word) . (undefined_bitvector - instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 24 :: int)::ii) :: ( 24 Word.word) M) \<bind> (\<lambda> (w__2 :: 24 bits) . + instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 24 :: int)::ii) :: ( 24 Word.word) M) \<bind> (\<lambda> (w__2 :: 24 Word.word) . (undefined_bitvector - instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 16 :: int)::ii) :: ( 16 Word.word) M) \<bind> (\<lambda> (w__3 :: 16 bits) . + instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 16 :: int)::ii) :: ( 16 Word.word) M) \<bind> (\<lambda> (w__3 :: 16 Word.word) . (undefined_bitvector - instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 4 :: int)::ii) :: ( 4 Word.word) M) \<bind> (\<lambda> (w__4 :: 4 bits) . + instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 4 :: int)::ii) :: ( 4 Word.word) M) \<bind> (\<lambda> (w__4 :: 4 Word.word) . undefined_bool () \<bind> (\<lambda> (w__5 :: bool) . undefined_bool () \<bind> (\<lambda> (w__6 :: bool) . undefined_bool () \<bind> (\<lambda> (w__7 :: bool) . @@ -3335,11 +3341,11 @@ definition undefined_CapStruct :: " unit \<Rightarrow>((register_value),(CapStr undefined_bool () \<bind> (\<lambda> (w__15 :: bool) . undefined_bool () \<bind> (\<lambda> (w__16 :: bool) . (undefined_bitvector - instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 64 :: int)::ii) :: ( 64 Word.word) M) \<bind> (\<lambda> (w__17 :: 64 bits) . + instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 64 :: int)::ii) :: ( 64 Word.word) M) \<bind> (\<lambda> (w__17 :: 64 Word.word) . (undefined_bitvector - instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 64 :: int)::ii) :: ( 64 Word.word) M) \<bind> (\<lambda> (w__18 :: 64 bits) . + instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 64 :: int)::ii) :: ( 64 Word.word) M) \<bind> (\<lambda> (w__18 :: 64 Word.word) . (undefined_bitvector - instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 64 :: int)::ii) :: ( 64 Word.word) M) \<bind> (\<lambda> (w__19 :: 64 bits) . + instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 64 :: int)::ii) :: ( 64 Word.word) M) \<bind> (\<lambda> (w__19 :: 64 Word.word) . return ((| CapStruct_tag = w__0, CapStruct_padding = w__1, CapStruct_otype = w__2, @@ -3557,7 +3563,7 @@ definition CapRegs :: "(((regstate),(register_value),((257)Word.word))register_ definition max_otype :: " int " where - " max_otype = ( MAX (( 24 :: int)::ii))" + " max_otype = ( MAX0 (( 24 :: int)::ii))" definition have_cp2 :: " bool " where @@ -3854,7 +3860,7 @@ definition raise_c2_exception_noreg :: " CapEx \<Rightarrow>((register_value),' definition pcc_access_system_regs :: " unit \<Rightarrow>((register_value),(bool),(exception))monad " where " pcc_access_system_regs _ = ( - (read_reg PCC_ref :: ( 257 Word.word) M) \<bind> (\<lambda> (w__0 :: 257 Word.word) . + (read_reg PCC_ref :: ( 257 Word.word) M) \<bind> (\<lambda> (w__0 :: CapReg) . (let pcc = (capRegToCapStruct w__0) in return(CapStruct_access_system_regs pcc))))" @@ -3868,7 +3874,7 @@ definition register_inaccessible :: "(5)Word.word \<Rightarrow>((register_value " register_inaccessible r = ( or_boolM (and_boolM (return (((r = IDCNO)))) - ((read_reg inCCallDelay_ref :: ( 1 Word.word) M) \<bind> (\<lambda> (w__0 :: 1 Word.word) . + ((read_reg inCCallDelay_ref :: ( 1 Word.word) M) \<bind> (\<lambda> (w__0 :: 1 bits) . return ((bits_to_bool w__0))))) (and_boolM (return ((((((r = KR1CNO))) \<or> ((((((r = KR2CNO))) \<or> ((((((r = KDCNO))) \<or> ((((((r = KCCNO))) \<or> (((r = EPCCNO)))))))))))))))) @@ -3993,7 +3999,7 @@ definition checkDDCPerms :: " CapStruct \<Rightarrow> MemAccessType \<Rightarro definition addrWrapper :: "(64)Word.word \<Rightarrow> MemAccessType \<Rightarrow> WordType \<Rightarrow>((register_value),((64)Word.word),(exception))monad " where " addrWrapper addr accessType width = ( - (read_reg DDC_ref :: ( 257 Word.word) M) \<bind> (\<lambda> (w__0 :: 257 Word.word) . + (read_reg DDC_ref :: ( 257 Word.word) M) \<bind> (\<lambda> (w__0 :: CapReg) . (let ddc = (capRegToCapStruct w__0) in checkDDCPerms ddc accessType \<then> ((let cursor = (getCapCursor ddc) in @@ -4014,7 +4020,7 @@ definition addrWrapper :: "(64)Word.word \<Rightarrow> MemAccessType \<Rightarr definition addrWrapperUnaligned :: "(64)Word.word \<Rightarrow> MemAccessType \<Rightarrow> WordTypeUnaligned \<Rightarrow>((register_value),((64)Word.word),(exception))monad " where " addrWrapperUnaligned addr accessType width = ( - (read_reg DDC_ref :: ( 257 Word.word) M) \<bind> (\<lambda> (w__0 :: 257 Word.word) . + (read_reg DDC_ref :: ( 257 Word.word) M) \<bind> (\<lambda> (w__0 :: CapReg) . (let ddc = (capRegToCapStruct w__0) in checkDDCPerms ddc accessType \<then> ((let cursor = (getCapCursor ddc) in @@ -4044,7 +4050,7 @@ definition addrWrapperUnaligned :: "(64)Word.word \<Rightarrow> MemAccessType \ definition TranslatePC :: "(64)Word.word \<Rightarrow>((register_value),((64)Word.word),(exception))monad " where " TranslatePC vAddr = ( (incrementCP0Count () \<then> - (read_reg PCC_ref :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__0 :: 257 Word.word) . + (read_reg PCC_ref :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__0 :: CapReg) . (let pcc = (capRegToCapStruct w__0) in (let base = (getCapBase pcc) in (let top1 = (getCapTop pcc) in @@ -4105,7 +4111,7 @@ definition cp2_next_pc :: " unit \<Rightarrow>((register_value),(unit),(excepti " cp2_next_pc _ = ( (read_reg nextPCC_ref :: ( 257 Word.word) M) \<bind> (\<lambda> (w__0 :: CapReg) . (write_reg PCC_ref w__0 \<then> - (read_reg inBranchDelay_ref :: ( 1 Word.word) M)) \<bind> (\<lambda> (w__1 :: 1 Word.word) . + (read_reg inBranchDelay_ref :: ( 1 Word.word) M)) \<bind> (\<lambda> (w__1 :: 1 bits) . if ((bits_to_bool w__1)) then (read_reg delayedPCC_ref :: ( 257 Word.word) M) \<bind> (\<lambda> (w__2 :: CapReg) . write_reg nextPCC_ref w__2) @@ -4117,81 +4123,81 @@ definition cp2_next_pc :: " unit \<Rightarrow>((register_value),(unit),(excepti definition capToString :: " CapStruct \<Rightarrow>((register_value),(string),(exception))monad " where " capToString cap = ( skip () \<then> - return (((op@) ('' t:'') - (((op@) (if(CapStruct_tag cap) then (''1'') else (''0'')) - (((op@) ('' s:'') - (((op@) (if(CapStruct_sealed cap) then (''1'') else (''0'')) - (((op@) ('' perms:'') - (((op@) + return (((@) ('' t:'') + (((@) (if(CapStruct_tag cap) then (''1'') else (''0'')) + (((@) ('' s:'') + (((@) (if(CapStruct_sealed cap) then (''1'') else (''0'')) + (((@) ('' perms:'') + (((@) ((string_of_bits ((concat_vec (vec_of_bits [B0] :: 1 Word.word) ((getCapPerms cap :: 31 Word.word)) :: 32 Word.word)))) - (((op@) ('' type:'') - (((op@) ((string_of_bits(CapStruct_otype cap))) - (((op@) ('' offset:'') - (((op@) + (((@) ('' type:'') + (((@) ((string_of_bits(CapStruct_otype cap))) + (((@) ('' offset:'') + (((@) ((string_of_bits ((to_bits ((make_the_value (( 64 :: int)::ii) :: 64 itself)) ((getCapOffset cap)) :: 64 Word.word)))) - (((op@) ('' base:'') - (((op@) + (((@) ('' base:'') + (((@) ((string_of_bits ((to_bits ((make_the_value (( 64 :: int)::ii) :: 64 itself)) ((getCapBase cap)) :: 64 Word.word)))) - (((op@) ('' length:'') + (((@) ('' length:'') ((string_of_bits ((to_bits ((make_the_value (( 64 :: int)::ii) :: 64 itself)) ((min ((getCapLength cap)) - ((MAX (( 64 :: int)::ii))))) + ((MAX0 (( 64 :: int)::ii))))) :: 64 Word.word)))))))))))))))))))))))))))))))" definition dump_cp2_state :: " unit \<Rightarrow>((register_value),(unit),(exception))monad " where " dump_cp2_state _ = ( - (read_reg PCC_ref :: ( 257 Word.word) M) \<bind> (\<lambda> (w__0 :: 257 Word.word) . + (read_reg PCC_ref :: ( 257 Word.word) M) \<bind> (\<lambda> (w__0 :: CapReg) . capToString ((capRegToCapStruct w__0)) \<bind> (\<lambda> (w__1 :: string) . - (let (_ :: unit) = (print_endline (((op@) (''DEBUG CAP PCC'') w__1))) in + (let (_ :: unit) = (print_endline (((@) (''DEBUG CAP PCC'') w__1))) in ((foreachM (index_list (( 0 :: int)::ii) (( 31 :: int)::ii) (( 1 :: int)::ii)) () (\<lambda> i unit_var . readCapReg ((to_bits ((make_the_value (( 5 :: int)::ii) :: 5 itself)) i :: 5 Word.word)) \<bind> (\<lambda> (w__2 :: CapStruct) . capToString w__2 \<bind> (\<lambda> (w__3 :: string) . return ((let _ = - (print_endline (((op@) (''DEBUG CAP REG '') (((op@) ((string_of_int + (print_endline (((@) (''DEBUG CAP REG '') (((@) ((string_of_int instance_Show_Show_Num_integer_dict i)) w__3))))) in () )))))) \<then> - (read_reg DDC_ref :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__4 :: 257 Word.word) . + (read_reg DDC_ref :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__4 :: CapReg) . capToString ((capRegToCapStruct w__4)) \<bind> (\<lambda> (w__5 :: string) . - (let (_ :: unit) = (print_endline (((op@) (''DEBUG CAP HWREG 00'') w__5))) in - (read_reg CTLSU_ref :: ( 257 Word.word) M) \<bind> (\<lambda> (w__6 :: 257 Word.word) . + (let (_ :: unit) = (print_endline (((@) (''DEBUG CAP HWREG 00'') w__5))) in + (read_reg CTLSU_ref :: ( 257 Word.word) M) \<bind> (\<lambda> (w__6 :: CapReg) . capToString ((capRegToCapStruct w__6)) \<bind> (\<lambda> (w__7 :: string) . - (let (_ :: unit) = (print_endline (((op@) (''DEBUG CAP HWREG 01'') w__7))) in - (read_reg CTLSP_ref :: ( 257 Word.word) M) \<bind> (\<lambda> (w__8 :: 257 Word.word) . + (let (_ :: unit) = (print_endline (((@) (''DEBUG CAP HWREG 01'') w__7))) in + (read_reg CTLSP_ref :: ( 257 Word.word) M) \<bind> (\<lambda> (w__8 :: CapReg) . capToString ((capRegToCapStruct w__8)) \<bind> (\<lambda> (w__9 :: string) . - (let (_ :: unit) = (print_endline (((op@) (''DEBUG CAP HWREG 08'') w__9))) in - (read_reg KR1C_ref :: ( 257 Word.word) M) \<bind> (\<lambda> (w__10 :: 257 Word.word) . + (let (_ :: unit) = (print_endline (((@) (''DEBUG CAP HWREG 08'') w__9))) in + (read_reg KR1C_ref :: ( 257 Word.word) M) \<bind> (\<lambda> (w__10 :: CapReg) . capToString ((capRegToCapStruct w__10)) \<bind> (\<lambda> (w__11 :: string) . - (let (_ :: unit) = (print_endline (((op@) (''DEBUG CAP HWREG 22'') w__11))) in - (read_reg KR2C_ref :: ( 257 Word.word) M) \<bind> (\<lambda> (w__12 :: 257 Word.word) . + (let (_ :: unit) = (print_endline (((@) (''DEBUG CAP HWREG 22'') w__11))) in + (read_reg KR2C_ref :: ( 257 Word.word) M) \<bind> (\<lambda> (w__12 :: CapReg) . capToString ((capRegToCapStruct w__12)) \<bind> (\<lambda> (w__13 :: string) . - (let (_ :: unit) = (print_endline (((op@) (''DEBUG CAP HWREG 23'') w__13))) in - (read_reg KCC_ref :: ( 257 Word.word) M) \<bind> (\<lambda> (w__14 :: 257 Word.word) . + (let (_ :: unit) = (print_endline (((@) (''DEBUG CAP HWREG 23'') w__13))) in + (read_reg KCC_ref :: ( 257 Word.word) M) \<bind> (\<lambda> (w__14 :: CapReg) . capToString ((capRegToCapStruct w__14)) \<bind> (\<lambda> (w__15 :: string) . - (let (_ :: unit) = (print_endline (((op@) (''DEBUG CAP HWREG 29'') w__15))) in - (read_reg KDC_ref :: ( 257 Word.word) M) \<bind> (\<lambda> (w__16 :: 257 Word.word) . + (let (_ :: unit) = (print_endline (((@) (''DEBUG CAP HWREG 29'') w__15))) in + (read_reg KDC_ref :: ( 257 Word.word) M) \<bind> (\<lambda> (w__16 :: CapReg) . capToString ((capRegToCapStruct w__16)) \<bind> (\<lambda> (w__17 :: string) . - (let (_ :: unit) = (print_endline (((op@) (''DEBUG CAP HWREG 30'') w__17))) in - (read_reg EPCC_ref :: ( 257 Word.word) M) \<bind> (\<lambda> (w__18 :: 257 Word.word) . + (let (_ :: unit) = (print_endline (((@) (''DEBUG CAP HWREG 30'') w__17))) in + (read_reg EPCC_ref :: ( 257 Word.word) M) \<bind> (\<lambda> (w__18 :: CapReg) . capToString ((capRegToCapStruct w__18)) \<bind> (\<lambda> (w__19 :: string) . - return ((print_endline (((op@) (''DEBUG CAP HWREG 31'') w__19)))))))))))))))))))))))))))))))" + return ((print_endline (((@) (''DEBUG CAP HWREG 31'') w__19)))))))))))))))))))))))))))))))" (*val extendLoad : forall 'sz . Size 'sz => mword 'sz -> bool -> mword ty64*) @@ -4273,98 +4279,98 @@ definition TLBWriteEntry :: "(6)Word.word \<Rightarrow>((register_value),(unit) definition decode :: "(32)Word.word \<Rightarrow>(ast)option " where " decode v__0 = ( if (((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B1,B1,B0,B0,B1] :: 6 Word.word)))) then - (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in + (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (imm :: imm16) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 0 :: int)::ii) :: 16 Word.word)) in Some (DADDIU (rs,rt,imm))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0] :: 6 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 0 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B1,B0,B1,B1,B0,B1] :: 11 Word.word))))))) then - (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in + (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rd :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in Some (DADDU (rs,rt,rd))))) else if (((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B1,B1,B0,B0,B0] :: 6 Word.word)))) then - (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in + (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (imm :: imm16) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 0 :: int)::ii) :: 16 Word.word)) in Some (DADDI (rs,rt,imm))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0] :: 6 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 0 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B1,B0,B1,B1,B0,B0] :: 11 Word.word))))))) then - (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in + (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rd :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in Some (DADD (rs,rt,rd))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0] :: 6 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 0 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B1,B0,B0,B0,B0,B0] :: 11 Word.word))))))) then - (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in + (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rd :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in Some (ADD (rs,rt,rd))))) else if (((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B0,B1,B0,B0,B0] :: 6 Word.word)))) then - (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in + (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (imm :: imm16) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 0 :: int)::ii) :: 16 Word.word)) in Some (ADDI (rs,rt,imm))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0] :: 6 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 0 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B1,B0,B0,B0,B0,B1] :: 11 Word.word))))))) then - (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in + (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rd :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in Some (ADDU (rs,rt,rd))))) else if (((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B0,B1,B0,B0,B1] :: 6 Word.word)))) then - (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in + (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (imm :: imm16) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 0 :: int)::ii) :: 16 Word.word)) in Some (ADDIU (rs,rt,imm))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0] :: 6 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 0 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B1,B0,B1,B1,B1,B1] :: 11 Word.word))))))) then - (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in + (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rd :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in Some (DSUBU (rs,rt,rd))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0] :: 6 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 0 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B1,B0,B1,B1,B1,B0] :: 11 Word.word))))))) then - (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in + (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rd :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in Some (DSUB (rs,rt,rd))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0] :: 6 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 0 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B1,B0,B0,B0,B1,B0] :: 11 Word.word))))))) then - (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in + (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rd :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in Some (SUB (rs,rt,rd))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0] :: 6 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 0 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B1,B0,B0,B0,B1,B1] :: 11 Word.word))))))) then - (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in + (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rd :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in Some (SUBU (rs,rt,rd))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0] :: 6 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 0 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B1,B0,B0,B1,B0,B0] :: 11 Word.word))))))) then - (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in + (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rd :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in Some (AND0 (rs,rt,rd))))) else if (((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B0,B1,B1,B0,B0] :: 6 Word.word)))) then - (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in + (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (imm :: imm16) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 0 :: int)::ii) :: 16 Word.word)) in Some (ANDI (rs,rt,imm))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0] :: 6 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 0 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B1,B0,B0,B1,B0,B1] :: 11 Word.word))))))) then - (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in + (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rd :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in Some (OR0 (rs,rt,rd))))) else if (((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B0,B1,B1,B0,B1] :: 6 Word.word)))) then - (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in + (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (imm :: imm16) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 0 :: int)::ii) :: 16 Word.word)) in Some (ORI (rs,rt,imm))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0] :: 6 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 0 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B1,B0,B0,B1,B1,B1] :: 11 Word.word))))))) then - (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in + (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rd :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in Some (NOR (rs,rt,rd))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0] :: 6 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 0 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B1,B0,B0,B1,B1,B0] :: 11 Word.word))))))) then - (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in + (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rd :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in Some (XOR0 (rs,rt,rd))))) else if (((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B0,B1,B1,B1,B0] :: 6 Word.word)))) then - (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in + (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (imm :: imm16) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 0 :: int)::ii) :: 16 Word.word)) in Some (XORI (rs,rt,imm))))) else if (((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 21 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B0,B1,B1,B1,B1,B0,B0,B0,B0,B0] :: 11 Word.word)))) then @@ -4372,108 +4378,108 @@ definition decode :: "(32)Word.word \<Rightarrow>(ast)option " where (let (imm :: imm16) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 0 :: int)::ii) :: 16 Word.word)) in Some (LUI (rt,imm)))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 21 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0] :: 11 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 5 :: int)::ii) (( 0 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B1,B1,B1,B0,B0,B0] :: 6 Word.word))))))) then + (let (sa :: 5 bits) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 6 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in (let (rd :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in - (let (sa :: 5 bits) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 6 :: int)::ii) :: 5 Word.word)) in Some (DSLL (rt,rd,sa))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 21 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0] :: 11 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 5 :: int)::ii) (( 0 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B1,B1,B1,B1,B0,B0] :: 6 Word.word))))))) then + (let (sa :: 5 bits) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 6 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in (let (rd :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in - (let (sa :: 5 bits) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 6 :: int)::ii) :: 5 Word.word)) in Some (DSLL32 (rt,rd,sa))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0] :: 6 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 0 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0,B1,B0,B1,B0,B0] :: 11 Word.word))))))) then - (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in + (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rd :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in Some (DSLLV (rs,rt,rd))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 21 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0] :: 11 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 5 :: int)::ii) (( 0 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B1,B1,B1,B0,B1,B1] :: 6 Word.word))))))) then + (let (sa :: 5 bits) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 6 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in (let (rd :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in - (let (sa :: 5 bits) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 6 :: int)::ii) :: 5 Word.word)) in Some (DSRA (rt,rd,sa))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 21 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0] :: 11 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 5 :: int)::ii) (( 0 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B1,B1,B1,B1,B1,B1] :: 6 Word.word))))))) then + (let (sa :: 5 bits) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 6 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in (let (rd :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in - (let (sa :: 5 bits) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 6 :: int)::ii) :: 5 Word.word)) in Some (DSRA32 (rt,rd,sa))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0] :: 6 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 0 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0,B1,B0,B1,B1,B1] :: 11 Word.word))))))) then - (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in + (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rd :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in Some (DSRAV (rs,rt,rd))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 21 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0] :: 11 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 5 :: int)::ii) (( 0 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B1,B1,B1,B0,B1,B0] :: 6 Word.word))))))) then + (let (sa :: 5 bits) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 6 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in (let (rd :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in - (let (sa :: 5 bits) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 6 :: int)::ii) :: 5 Word.word)) in Some (DSRL (rt,rd,sa))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 21 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0] :: 11 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 5 :: int)::ii) (( 0 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B1,B1,B1,B1,B1,B0] :: 6 Word.word))))))) then + (let (sa :: 5 bits) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 6 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in (let (rd :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in - (let (sa :: 5 bits) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 6 :: int)::ii) :: 5 Word.word)) in Some (DSRL32 (rt,rd,sa))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0] :: 6 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 0 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0,B1,B0,B1,B1,B0] :: 11 Word.word))))))) then - (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in + (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rd :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in Some (DSRLV (rs,rt,rd))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 21 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0] :: 11 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 5 :: int)::ii) (( 0 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0] :: 6 Word.word))))))) then + (let (sa :: regno) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 6 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in (let (rd :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in - (let (sa :: regno) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 6 :: int)::ii) :: 5 Word.word)) in Some (SLL (rt,rd,sa))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0] :: 6 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 0 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0,B0,B0,B1,B0,B0] :: 11 Word.word))))))) then - (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in + (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rd :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in Some (SLLV (rs,rt,rd))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 21 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0] :: 11 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 5 :: int)::ii) (( 0 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B1,B1] :: 6 Word.word))))))) then + (let (sa :: regno) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 6 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in (let (rd :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in - (let (sa :: regno) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 6 :: int)::ii) :: 5 Word.word)) in Some (SRA (rt,rd,sa))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0] :: 6 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 0 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0,B0,B0,B1,B1,B1] :: 11 Word.word))))))) then - (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in + (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rd :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in Some (SRAV (rs,rt,rd))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 21 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0] :: 11 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 5 :: int)::ii) (( 0 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B1,B0] :: 6 Word.word))))))) then + (let (sa :: regno) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 6 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in (let (rd :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in - (let (sa :: regno) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 6 :: int)::ii) :: 5 Word.word)) in Some (SRL (rt,rd,sa))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0] :: 6 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 0 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0,B0,B0,B1,B1,B0] :: 11 Word.word))))))) then - (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in + (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rd :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in Some (SRLV (rs,rt,rd))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0] :: 6 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 0 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B1,B0,B1,B0,B1,B0] :: 11 Word.word))))))) then - (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in + (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rd :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in Some (SLT (rs,rt,rd))))) else if (((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B0,B1,B0,B1,B0] :: 6 Word.word)))) then - (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in + (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (imm :: imm16) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 0 :: int)::ii) :: 16 Word.word)) in Some (SLTI (rs,rt,imm))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0] :: 6 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 0 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B1,B0,B1,B0,B1,B1] :: 11 Word.word))))))) then - (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in + (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rd :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in Some (SLTU (rs,rt,rd))))) else if (((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B0,B1,B0,B1,B1] :: 6 Word.word)))) then - (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in + (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (imm :: imm16) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 0 :: int)::ii) :: 16 Word.word)) in Some (SLTIU (rs,rt,imm))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0] :: 6 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 0 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0,B0,B1,B0,B1,B1] :: 11 Word.word))))))) then - (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in + (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rd :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in Some (MOVN (rs,rt,rd))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0] :: 6 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 0 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0,B0,B1,B0,B1,B0] :: 11 Word.word))))))) then - (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in + (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rd :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in Some (MOVZ (rs,rt,rd))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 16 :: int)::ii) :: 16 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0] :: 16 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 0 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0,B1,B0,B0,B0,B0] :: 11 Word.word))))))) then @@ -4491,69 +4497,69 @@ definition decode :: "(32)Word.word \<Rightarrow>(ast)option " where (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in Some (MTLO rs)) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B1,B1,B1,B0,B0] :: 6 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 0 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0,B0,B0,B0,B1,B0] :: 11 Word.word))))))) then - (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in + (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rd :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in Some (MUL (rs,rt,rd))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0] :: 6 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 0 :: int)::ii) :: 16 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B1,B1,B0,B0,B0] :: 16 Word.word))))))) then - (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in + (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in Some (MULT (rs,rt)))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0] :: 6 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 0 :: int)::ii) :: 16 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B1,B1,B0,B0,B1] :: 16 Word.word))))))) then - (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in + (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in Some (MULTU (rs,rt)))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0] :: 6 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 0 :: int)::ii) :: 16 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B1,B1,B1,B0,B0] :: 16 Word.word))))))) then - (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in + (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in Some (DMULT (rs,rt)))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0] :: 6 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 0 :: int)::ii) :: 16 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B1,B1,B1,B0,B1] :: 16 Word.word))))))) then - (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in + (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in Some (DMULTU (rs,rt)))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B1,B1,B1,B0,B0] :: 6 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 0 :: int)::ii) :: 16 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0] :: 16 Word.word))))))) then - (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in + (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in Some (MADD (rs,rt)))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B1,B1,B1,B0,B0] :: 6 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 0 :: int)::ii) :: 16 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B1] :: 16 Word.word))))))) then - (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in + (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in Some (MADDU (rs,rt)))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B1,B1,B1,B0,B0] :: 6 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 0 :: int)::ii) :: 16 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B1,B0,B0] :: 16 Word.word))))))) then - (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in + (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in Some (MSUB (rs,rt)))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B1,B1,B1,B0,B0] :: 6 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 0 :: int)::ii) :: 16 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B1,B0,B1] :: 16 Word.word))))))) then - (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in + (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in Some (MSUBU (rs,rt)))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0] :: 6 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 0 :: int)::ii) :: 16 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B1,B1,B0,B1,B0] :: 16 Word.word))))))) then - (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in + (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in Some (DIV (rs,rt)))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0] :: 6 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 0 :: int)::ii) :: 16 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B1,B1,B0,B1,B1] :: 16 Word.word))))))) then - (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in + (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in Some (DIVU (rs,rt)))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0] :: 6 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 0 :: int)::ii) :: 16 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B1,B1,B1,B1,B0] :: 16 Word.word))))))) then - (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in + (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in Some (DDIV (rs,rt)))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0] :: 6 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 0 :: int)::ii) :: 16 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B1,B1,B1,B1,B1] :: 16 Word.word))))))) then - (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in + (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in Some (DDIVU (rs,rt)))) else if (((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B1,B0] :: 6 Word.word)))) then (let (offset :: 26 bits) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 0 :: int)::ii) :: 26 Word.word)) in @@ -4569,23 +4575,23 @@ definition decode :: "(32)Word.word \<Rightarrow>(ast)option " where (let (rd :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in Some (JALR (rs,rd)))) else if (((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B0,B0,B1,B0,B0] :: 6 Word.word)))) then - (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in + (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (imm :: imm16) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 0 :: int)::ii) :: 16 Word.word)) in Some (BEQ (rs,rt,imm,False,False))))) else if (((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B1,B0,B1,B0,B0] :: 6 Word.word)))) then - (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in + (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (imm :: imm16) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 0 :: int)::ii) :: 16 Word.word)) in Some (BEQ (rs,rt,imm,False,True))))) else if (((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B0,B0,B1,B0,B1] :: 6 Word.word)))) then - (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in + (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (imm :: imm16) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 0 :: int)::ii) :: 16 Word.word)) in Some (BEQ (rs,rt,imm,True,False))))) else if (((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B1,B0,B1,B0,B1] :: 6 Word.word)))) then - (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in + (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (imm :: imm16) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 0 :: int)::ii) :: 16 Word.word)) in Some (BEQ (rs,rt,imm,True,True))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B1] :: 6 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0] :: 5 Word.word))))))) then @@ -4645,28 +4651,28 @@ definition decode :: "(32)Word.word \<Rightarrow>(ast)option " where :: 32 Word.word)))) then Some (WAIT () ) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0] :: 6 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 5 :: int)::ii) (( 0 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B1,B1,B0,B0,B0,B0] :: 6 Word.word))))))) then - (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in + (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in Some (TRAPREG (rs,rt,GE)))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0] :: 6 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 5 :: int)::ii) (( 0 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B1,B1,B0,B0,B0,B1] :: 6 Word.word))))))) then - (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in + (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in Some (TRAPREG (rs,rt,GEU)))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0] :: 6 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 5 :: int)::ii) (( 0 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B1,B1,B0,B0,B1,B0] :: 6 Word.word))))))) then - (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in + (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in Some (TRAPREG (rs,rt,LT')))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0] :: 6 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 5 :: int)::ii) (( 0 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B1,B1,B0,B0,B1,B1] :: 6 Word.word))))))) then - (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in + (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in Some (TRAPREG (rs,rt,LTU)))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0] :: 6 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 5 :: int)::ii) (( 0 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B1,B1,B0,B1,B0,B0] :: 6 Word.word))))))) then - (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in + (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in Some (TRAPREG (rs,rt,EQ')))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0] :: 6 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 5 :: int)::ii) (( 0 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B1,B1,B0,B1,B1,B0] :: 6 Word.word))))))) then - (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in + (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in Some (TRAPREG (rs,rt,NE)))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B1] :: 6 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) = (vec_of_bits [B0,B1,B1,B0,B0] :: 5 Word.word))))))) then (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in @@ -4693,137 +4699,137 @@ definition decode :: "(32)Word.word \<Rightarrow>(ast)option " where (let (imm :: imm16) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 0 :: int)::ii) :: 16 Word.word)) in Some (TRAPIMM (rs,imm,LTU)))) else if (((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B1,B0,B0,B0,B0,B0] :: 6 Word.word)))) then - (let (base :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in (let (offset :: imm16) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 0 :: int)::ii) :: 16 Word.word)) in + (let (base :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in Some (Load (B,True,False,base,rt,offset))))) else if (((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B1,B0,B0,B1,B0,B0] :: 6 Word.word)))) then - (let (base :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in (let (offset :: imm16) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 0 :: int)::ii) :: 16 Word.word)) in + (let (base :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in Some (Load (B,False,False,base,rt,offset))))) else if (((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B1,B0,B0,B0,B0,B1] :: 6 Word.word)))) then - (let (base :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in (let (offset :: imm16) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 0 :: int)::ii) :: 16 Word.word)) in + (let (base :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in Some (Load (H,True,False,base,rt,offset))))) else if (((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B1,B0,B0,B1,B0,B1] :: 6 Word.word)))) then - (let (base :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in (let (offset :: imm16) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 0 :: int)::ii) :: 16 Word.word)) in + (let (base :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in Some (Load (H,False,False,base,rt,offset))))) else if (((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B1,B0,B0,B0,B1,B1] :: 6 Word.word)))) then - (let (base :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in (let (offset :: imm16) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 0 :: int)::ii) :: 16 Word.word)) in + (let (base :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in Some (Load (W,True,False,base,rt,offset))))) else if (((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B1,B0,B0,B1,B1,B1] :: 6 Word.word)))) then - (let (base :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in (let (offset :: imm16) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 0 :: int)::ii) :: 16 Word.word)) in + (let (base :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in Some (Load (W,False,False,base,rt,offset))))) else if (((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B1,B1,B0,B1,B1,B1] :: 6 Word.word)))) then - (let (base :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in (let (offset :: imm16) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 0 :: int)::ii) :: 16 Word.word)) in + (let (base :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in Some (Load (D,False,False,base,rt,offset))))) else if (((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B1,B1,B0,B0,B0,B0] :: 6 Word.word)))) then - (let (base :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in (let (offset :: imm16) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 0 :: int)::ii) :: 16 Word.word)) in + (let (base :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in Some (Load (W,True,True,base,rt,offset))))) else if (((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B1,B1,B0,B1,B0,B0] :: 6 Word.word)))) then - (let (base :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in (let (offset :: imm16) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 0 :: int)::ii) :: 16 Word.word)) in + (let (base :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in Some (Load (D,False,True,base,rt,offset))))) else if (((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B1,B0,B1,B0,B0,B0] :: 6 Word.word)))) then - (let (base :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in (let (offset :: imm16) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 0 :: int)::ii) :: 16 Word.word)) in + (let (base :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in Some (Store (B,False,base,rt,offset))))) else if (((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B1,B0,B1,B0,B0,B1] :: 6 Word.word)))) then - (let (base :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in (let (offset :: imm16) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 0 :: int)::ii) :: 16 Word.word)) in + (let (base :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in Some (Store (H,False,base,rt,offset))))) else if (((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B1,B0,B1,B0,B1,B1] :: 6 Word.word)))) then - (let (base :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in (let (offset :: imm16) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 0 :: int)::ii) :: 16 Word.word)) in + (let (base :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in Some (Store (W,False,base,rt,offset))))) else if (((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B1,B1,B1,B1,B1,B1] :: 6 Word.word)))) then - (let (base :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in (let (offset :: imm16) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 0 :: int)::ii) :: 16 Word.word)) in + (let (base :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in Some (Store (D,False,base,rt,offset))))) else if (((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B1,B1,B1,B0,B0,B0] :: 6 Word.word)))) then - (let (base :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in (let (offset :: imm16) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 0 :: int)::ii) :: 16 Word.word)) in + (let (base :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in Some (Store (W,True,base,rt,offset))))) else if (((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B1,B1,B1,B1,B0,B0] :: 6 Word.word)))) then - (let (base :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in (let (offset :: imm16) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 0 :: int)::ii) :: 16 Word.word)) in + (let (base :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in Some (Store (D,True,base,rt,offset))))) else if (((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B1,B0,B0,B0,B1,B0] :: 6 Word.word)))) then - (let (base :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in (let (offset :: imm16) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 0 :: int)::ii) :: 16 Word.word)) in + (let (base :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in Some (LWL (base,rt,offset))))) else if (((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B1,B0,B0,B1,B1,B0] :: 6 Word.word)))) then - (let (base :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in (let (offset :: imm16) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 0 :: int)::ii) :: 16 Word.word)) in + (let (base :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in Some (LWR (base,rt,offset))))) else if (((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B1,B0,B1,B0,B1,B0] :: 6 Word.word)))) then - (let (base :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in (let (offset :: imm16) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 0 :: int)::ii) :: 16 Word.word)) in + (let (base :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in Some (SWL (base,rt,offset))))) else if (((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B1,B0,B1,B1,B1,B0] :: 6 Word.word)))) then - (let (base :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in (let (offset :: imm16) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 0 :: int)::ii) :: 16 Word.word)) in + (let (base :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in Some (SWR (base,rt,offset))))) else if (((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B1,B1,B0,B1,B0] :: 6 Word.word)))) then - (let (base :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in (let (offset :: imm16) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 0 :: int)::ii) :: 16 Word.word)) in + (let (base :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in Some (LDL (base,rt,offset))))) else if (((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B1,B1,B0,B1,B1] :: 6 Word.word)))) then - (let (base :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in (let (offset :: imm16) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 0 :: int)::ii) :: 16 Word.word)) in + (let (base :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in Some (LDR (base,rt,offset))))) else if (((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B1,B0,B1,B1,B0,B0] :: 6 Word.word)))) then - (let (base :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in (let (offset :: imm16) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 0 :: int)::ii) :: 16 Word.word)) in + (let (base :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in Some (SDL (base,rt,offset))))) else if (((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B1,B0,B1,B1,B0,B1] :: 6 Word.word)))) then - (let (base :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in (let (offset :: imm16) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 0 :: int)::ii) :: 16 Word.word)) in + (let (base :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in Some (SDR (base,rt,offset))))) else if (((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B1,B0,B1,B1,B1,B1] :: 6 Word.word)))) then - (let (base :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (op1 :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in (let (imm :: imm16) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 0 :: int)::ii) :: 16 Word.word)) in + (let (base :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in Some (CACHE (base,op1,imm))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 11 :: int)::ii) :: 21 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0] :: 21 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 5 :: int)::ii) (( 0 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B0,B1,B1,B1,B1] :: 6 Word.word))))))) then Some (SYNC () ) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 21 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B1,B0,B0,B0,B0,B0,B0,B0,B0,B0] :: 11 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 3 :: int)::ii) :: 8 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0,B0,B0] :: 8 Word.word))))))) then + (let (sel :: 3 bits) = ((subrange_vec_dec v__0 (( 2 :: int)::ii) (( 0 :: int)::ii) :: 3 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in (let (rd :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in - (let (sel :: 3 bits) = ((subrange_vec_dec v__0 (( 2 :: int)::ii) (( 0 :: int)::ii) :: 3 Word.word)) in Some (MFC0 (rt,rd,sel,False))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 21 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B1,B0,B0,B0,B0,B0,B0,B0,B0,B1] :: 11 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 3 :: int)::ii) :: 8 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0,B0,B0] :: 8 Word.word))))))) then + (let (sel :: 3 bits) = ((subrange_vec_dec v__0 (( 2 :: int)::ii) (( 0 :: int)::ii) :: 3 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in (let (rd :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in - (let (sel :: 3 bits) = ((subrange_vec_dec v__0 (( 2 :: int)::ii) (( 0 :: int)::ii) :: 3 Word.word)) in Some (MFC0 (rt,rd,sel,True))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 21 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B1,B0,B0,B0,B0,B0,B0,B1,B0,B0] :: 11 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 0 :: int)::ii) :: 16 Word.word)) = (vec_of_bits [B1,B0,B1,B1,B1,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0] :: 16 Word.word))))))) then @@ -4832,14 +4838,14 @@ definition decode :: "(32)Word.word \<Rightarrow>(ast)option " where then Some (HCF () ) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 21 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B1,B0,B0,B0,B0,B0,B0,B1,B0,B0] :: 11 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 3 :: int)::ii) :: 8 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0,B0,B0] :: 8 Word.word))))))) then + (let (sel :: 3 bits) = ((subrange_vec_dec v__0 (( 2 :: int)::ii) (( 0 :: int)::ii) :: 3 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in (let (rd :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in - (let (sel :: 3 bits) = ((subrange_vec_dec v__0 (( 2 :: int)::ii) (( 0 :: int)::ii) :: 3 Word.word)) in Some (MTC0 (rt,rd,sel,False))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 21 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B1,B0,B0,B0,B0,B0,B0,B1,B0,B1] :: 11 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 3 :: int)::ii) :: 8 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0,B0,B0] :: 8 Word.word))))))) then + (let (sel :: 3 bits) = ((subrange_vec_dec v__0 (( 2 :: int)::ii) (( 0 :: int)::ii) :: 3 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in (let (rd :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in - (let (sel :: 3 bits) = ((subrange_vec_dec v__0 (( 2 :: int)::ii) (( 0 :: int)::ii) :: 3 Word.word)) in Some (MTC0 (rt,rd,sel,True))))) else if (((v__0 = (vec_of_bits [B0,B1,B0,B0,B0,B0,B1,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0, B0,B0,B0,B0,B0,B0,B1,B0] @@ -4906,96 +4912,96 @@ definition decode :: "(32)Word.word \<Rightarrow>(ast)option " where (let (rt :: regno) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 6 :: int)::ii) :: 5 Word.word)) in Some (CSetCause rt)) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 21 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B1,B0,B0,B1,B0,B0,B0,B1,B0,B0] :: 11 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 5 :: int)::ii) (( 0 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0] :: 6 Word.word))))))) then + (let (rt :: regno) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 6 :: int)::ii) :: 5 Word.word)) in (let (cd1 :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in (let (cb :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in - (let (rt :: regno) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 6 :: int)::ii) :: 5 Word.word)) in Some (CAndPerm (cd1,cb,rt))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 21 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B1,B0,B0,B1,B0,B0,B1,B1,B0,B0] :: 11 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 5 :: int)::ii) (( 0 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0] :: 6 Word.word))))))) then (let (rd :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in - (let (cb :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in (let (ct :: regno) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 6 :: int)::ii) :: 5 Word.word)) in + (let (cb :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in Some (CToPtr (rd,cb,ct))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 21 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B1,B0,B0,B1,B0,B0,B1,B1,B1,B0] :: 11 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 5 :: int)::ii) (( 0 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0] :: 6 Word.word))))))) then (let (rd :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in - (let (cb :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in (let (ct :: regno) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 6 :: int)::ii) :: 5 Word.word)) in + (let (cb :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in Some (CPtrCmp (rd,cb,ct,CEQ))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 21 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B1,B0,B0,B1,B0,B0,B1,B1,B1,B0] :: 11 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 5 :: int)::ii) (( 0 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B1] :: 6 Word.word))))))) then (let (rd :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in - (let (cb :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in (let (ct :: regno) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 6 :: int)::ii) :: 5 Word.word)) in + (let (cb :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in Some (CPtrCmp (rd,cb,ct,CNE))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 21 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B1,B0,B0,B1,B0,B0,B1,B1,B1,B0] :: 11 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 5 :: int)::ii) (( 0 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B1,B0] :: 6 Word.word))))))) then (let (rd :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in - (let (cb :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in (let (ct :: regno) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 6 :: int)::ii) :: 5 Word.word)) in + (let (cb :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in Some (CPtrCmp (rd,cb,ct,CLT))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 21 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B1,B0,B0,B1,B0,B0,B1,B1,B1,B0] :: 11 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 5 :: int)::ii) (( 0 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B1,B1] :: 6 Word.word))))))) then (let (rd :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in - (let (cb :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in (let (ct :: regno) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 6 :: int)::ii) :: 5 Word.word)) in + (let (cb :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in Some (CPtrCmp (rd,cb,ct,CLE))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 21 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B1,B0,B0,B1,B0,B0,B1,B1,B1,B0] :: 11 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 5 :: int)::ii) (( 0 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B0,B0,B1,B0,B0] :: 6 Word.word))))))) then (let (rd :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in - (let (cb :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in (let (ct :: regno) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 6 :: int)::ii) :: 5 Word.word)) in + (let (cb :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in Some (CPtrCmp (rd,cb,ct,CLTU))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 21 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B1,B0,B0,B1,B0,B0,B1,B1,B1,B0] :: 11 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 5 :: int)::ii) (( 0 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B0,B0,B1,B0,B1] :: 6 Word.word))))))) then (let (rd :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in - (let (cb :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in (let (ct :: regno) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 6 :: int)::ii) :: 5 Word.word)) in + (let (cb :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in Some (CPtrCmp (rd,cb,ct,CLEU))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 21 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B1,B0,B0,B1,B0,B0,B1,B1,B1,B0] :: 11 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 5 :: int)::ii) (( 0 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B0,B0,B1,B1,B0] :: 6 Word.word))))))) then (let (rd :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in - (let (cb :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in (let (ct :: regno) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 6 :: int)::ii) :: 5 Word.word)) in + (let (cb :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in Some (CPtrCmp (rd,cb,ct,CEXEQ))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 21 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B1,B0,B0,B1,B0,B0,B1,B1,B1,B0] :: 11 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 5 :: int)::ii) (( 0 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B0,B0,B1,B1,B1] :: 6 Word.word))))))) then (let (rd :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in - (let (cb :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in (let (ct :: regno) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 6 :: int)::ii) :: 5 Word.word)) in + (let (cb :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in Some (CPtrCmp (rd,cb,ct,CNEXEQ))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 21 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B1,B0,B0,B1,B0,B0,B1,B1,B0,B1] :: 11 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 5 :: int)::ii) (( 0 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0] :: 6 Word.word))))))) then + (let (rt :: regno) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 6 :: int)::ii) :: 5 Word.word)) in (let (cd1 :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in (let (cb :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in - (let (rt :: regno) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 6 :: int)::ii) :: 5 Word.word)) in Some (CIncOffset (cd1,cb,rt))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 21 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B1,B0,B0,B1,B0,B0,B1,B1,B0,B1] :: 11 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 5 :: int)::ii) (( 0 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B1] :: 6 Word.word))))))) then + (let (rt :: regno) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 6 :: int)::ii) :: 5 Word.word)) in (let (cd1 :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in (let (cb :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in - (let (rt :: regno) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 6 :: int)::ii) :: 5 Word.word)) in Some (CSetOffset (cd1,cb,rt))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 21 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B1,B0,B0,B1,B0,B0,B0,B0,B0,B1] :: 11 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 5 :: int)::ii) (( 0 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0] :: 6 Word.word))))))) then + (let (rt :: regno) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 6 :: int)::ii) :: 5 Word.word)) in (let (cd1 :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in (let (cb :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in - (let (rt :: regno) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 6 :: int)::ii) :: 5 Word.word)) in Some (CSetBounds (cd1,cb,rt))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 21 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B1,B0,B0,B1,B0,B0,B0,B1,B0,B0] :: 11 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 0 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0,B0,B0,B1,B0,B1] :: 11 Word.word))))))) then (let (cd1 :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in (let (cb :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in Some (CClearTag (cd1,cb)))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 21 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B1,B0,B0,B1,B0,B0,B0,B1,B0,B0] :: 11 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 5 :: int)::ii) (( 0 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B0,B0,B1,B1,B1] :: 6 Word.word))))))) then + (let (rt :: regno) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 6 :: int)::ii) :: 5 Word.word)) in (let (cd1 :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in (let (cb :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in - (let (rt :: regno) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 6 :: int)::ii) :: 5 Word.word)) in Some (CFromPtr (cd1,cb,rt))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 21 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B1,B0,B0,B1,B0,B0,B1,B0,B1,B1] :: 11 Word.word)))) \<and> ((((((((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0] :: 5 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 5 :: int)::ii) (( 0 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0] :: 6 Word.word)))))))))) then - (let (cs :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 6 :: int)::ii) :: 5 Word.word)) in + (let (cs :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in Some (CCheckPerm (cs,rt)))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 21 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B1,B0,B0,B1,B0,B0,B1,B0,B1,B1] :: 11 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 0 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B1] :: 11 Word.word))))))) then (let (cs :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in (let (cb :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in Some (CCheckType (cs,cb)))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 21 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B1,B0,B0,B1,B0,B0,B0,B0,B1,B0] :: 11 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 5 :: int)::ii) (( 0 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0] :: 6 Word.word))))))) then - (let (cd1 :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in - (let (cs :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in (let (ct :: regno) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 6 :: int)::ii) :: 5 Word.word)) in + (let (cs :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in + (let (cd1 :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in Some (CSeal (cd1,cs,ct))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 21 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B1,B0,B0,B1,B0,B0,B0,B0,B1,B1] :: 11 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 5 :: int)::ii) (( 0 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0] :: 6 Word.word))))))) then - (let (cd1 :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in - (let (cs :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in (let (ct :: regno) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 6 :: int)::ii) :: 5 Word.word)) in + (let (cs :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in + (let (cd1 :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in Some (CUnseal (cd1,cs,ct))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 21 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B1,B0,B0,B1,B0,B0,B0,B1,B1,B1] :: 11 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 0 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0] :: 11 Word.word))))))) then (let (cd1 :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in @@ -5021,8 +5027,8 @@ definition decode :: "(32)Word.word \<Rightarrow>(ast)option " where (let (cb :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in Some (CJALR ((vec_of_bits [B0,B0,B0,B0,B0] :: 5 Word.word),cb,False))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 21 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B1,B0,B0,B1,B0,B0,B0,B0,B0,B0] :: 11 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 0 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B1,B0,B0,B0,B1,B1,B1,B1,B1,B1] :: 11 Word.word))))))) then - (let (cs :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in + (let (cs :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in Some (CCheckPerm (cs,rt)))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 21 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B1,B0,B0,B1,B0,B0,B0,B0,B0,B0] :: 11 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 0 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B1,B0,B0,B1,B1,B1,B1,B1,B1,B1] :: 11 Word.word))))))) then (let (cs :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in @@ -5033,8 +5039,8 @@ definition decode :: "(32)Word.word \<Rightarrow>(ast)option " where (let (cb :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in Some (CClearTag (cd1,cb)))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 21 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B1,B0,B0,B1,B0,B0,B0,B0,B0,B0] :: 11 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 0 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B1,B0,B1,B0,B1,B1,B1,B1,B1,B1] :: 11 Word.word))))))) then - (let (cd1 :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in (let (cs :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in + (let (cd1 :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in Some (CMOVX (cd1,cs,(vec_of_bits [B0,B0,B0,B0,B0] :: 5 Word.word),False)))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 21 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B1,B0,B0,B1,B0,B0,B0,B0,B0,B0] :: 11 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 0 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B1,B1,B0,B0,B1,B1,B1,B1,B1,B1] :: 11 Word.word))))))) then (let (cd1 :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in @@ -5069,165 +5075,165 @@ definition decode :: "(32)Word.word \<Rightarrow>(ast)option " where (let (cb :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in Some (CGetOffset (rd,cb)))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 21 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B1,B0,B0,B1,B0,B0,B0,B0,B0,B0] :: 11 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 0 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B0,B1,B1,B1,B1,B1,B1,B1,B1,B1] :: 11 Word.word))))))) then - (let (cd1 :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in (let (rs :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in + (let (cd1 :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in Some (CGetPCCSetOffset (cd1,rs)))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 21 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B1,B0,B0,B1,B0,B0,B0,B0,B0,B0] :: 11 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 0 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B1,B1,B0,B1,B1,B1,B1,B1,B1,B1] :: 11 Word.word))))))) then - (let (cd1 :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in (let (sel :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in + (let (cd1 :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in Some (CReadHwr (cd1,sel)))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 21 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B1,B0,B0,B1,B0,B0,B0,B0,B0,B0] :: 11 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 0 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B1,B1,B1,B0,B1,B1,B1,B1,B1,B1] :: 11 Word.word))))))) then - (let (cb :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in (let (sel :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in + (let (cb :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in Some (CWriteHwr (cb,sel)))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 21 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B1,B0,B0,B1,B0,B0,B0,B0,B0,B0] :: 11 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 0 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B1,B1,B1,B1,B1,B1,B1,B1,B1,B1] :: 11 Word.word))))))) then - (let (cb :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in (let (sel :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in + (let (cb :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in Some (CGetAddr (cb,sel)))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 21 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B1,B0,B0,B1,B0,B0,B0,B0,B0,B0] :: 11 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 5 :: int)::ii) (( 0 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B0,B1,B0,B1,B1] :: 6 Word.word))))))) then - (let (cd1 :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in - (let (cs :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in (let (ct :: regno) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 6 :: int)::ii) :: 5 Word.word)) in + (let (cs :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in + (let (cd1 :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in Some (CSeal (cd1,cs,ct))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 21 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B1,B0,B0,B1,B0,B0,B0,B0,B0,B0] :: 11 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 5 :: int)::ii) (( 0 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B0,B1,B1,B0,B0] :: 6 Word.word))))))) then - (let (cd1 :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in - (let (cs :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in (let (ct :: regno) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 6 :: int)::ii) :: 5 Word.word)) in + (let (cs :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in + (let (cd1 :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in Some (CUnseal (cd1,cs,ct))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 21 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B1,B0,B0,B1,B0,B0,B0,B0,B0,B0] :: 11 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 5 :: int)::ii) (( 0 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B0,B1,B1,B0,B1] :: 6 Word.word))))))) then - (let (cd1 :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in - (let (cs :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 6 :: int)::ii) :: 5 Word.word)) in + (let (cs :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in + (let (cd1 :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in Some (CAndPerm (cd1,cs,rt))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 21 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B1,B0,B0,B1,B0,B0,B0,B0,B0,B0] :: 11 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 5 :: int)::ii) (( 0 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B0,B1,B1,B1,B1] :: 6 Word.word))))))) then - (let (cd1 :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in - (let (cs :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 6 :: int)::ii) :: 5 Word.word)) in + (let (cs :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in + (let (cd1 :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in Some (CSetOffset (cd1,cs,rt))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 21 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B1,B0,B0,B1,B0,B0,B0,B0,B0,B0] :: 11 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 5 :: int)::ii) (( 0 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B0,B1,B0,B0,B0] :: 6 Word.word))))))) then - (let (cd1 :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in - (let (cs :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 6 :: int)::ii) :: 5 Word.word)) in + (let (cs :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in + (let (cd1 :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in Some (CSetBounds (cd1,cs,rt))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 21 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B1,B0,B0,B1,B0,B0,B0,B0,B0,B0] :: 11 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 5 :: int)::ii) (( 0 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B0,B1,B0,B0,B1] :: 6 Word.word))))))) then - (let (cd1 :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in - (let (cs :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 6 :: int)::ii) :: 5 Word.word)) in + (let (cs :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in + (let (cd1 :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in Some (CSetBoundsExact (cd1,cs,rt))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 21 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B1,B0,B0,B1,B0,B0,B0,B0,B0,B0] :: 11 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 5 :: int)::ii) (( 0 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B1,B0,B0,B0,B1] :: 6 Word.word))))))) then + (let (rt :: regno) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 6 :: int)::ii) :: 5 Word.word)) in (let (cd1 :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in (let (cb :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in - (let (rt :: regno) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 6 :: int)::ii) :: 5 Word.word)) in Some (CIncOffset (cd1,cb,rt))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 21 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B1,B0,B0,B1,B0,B0,B0,B0,B0,B0] :: 11 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 5 :: int)::ii) (( 0 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B1,B1,B1,B0,B1] :: 6 Word.word))))))) then + (let (ct :: regno) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 6 :: int)::ii) :: 5 Word.word)) in (let (cd1 :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in (let (cb :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in - (let (ct :: regno) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 6 :: int)::ii) :: 5 Word.word)) in Some (CBuildCap (cd1,cb,ct))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 21 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B1,B0,B0,B1,B0,B0,B0,B0,B0,B0] :: 11 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 5 :: int)::ii) (( 0 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B1,B1,B1,B1,B0] :: 6 Word.word))))))) then + (let (ct :: regno) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 6 :: int)::ii) :: 5 Word.word)) in (let (cd1 :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in (let (cb :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in - (let (ct :: regno) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 6 :: int)::ii) :: 5 Word.word)) in Some (CCopyType (cd1,cb,ct))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 21 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B1,B0,B0,B1,B0,B0,B0,B0,B0,B0] :: 11 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 5 :: int)::ii) (( 0 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B1,B1,B1,B1,B1] :: 6 Word.word))))))) then - (let (cd1 :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in - (let (cs :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in (let (ct :: regno) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 6 :: int)::ii) :: 5 Word.word)) in + (let (cs :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in + (let (cd1 :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in Some (CCSeal (cd1,cs,ct))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 21 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B1,B0,B0,B1,B0,B0,B0,B0,B0,B0] :: 11 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 5 :: int)::ii) (( 0 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B1,B0,B0,B1,B0] :: 6 Word.word))))))) then (let (rd :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in - (let (cb :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in (let (ct :: regno) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 6 :: int)::ii) :: 5 Word.word)) in + (let (cb :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in Some (CToPtr (rd,cb,ct))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 21 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B1,B0,B0,B1,B0,B0,B0,B0,B0,B0] :: 11 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 5 :: int)::ii) (( 0 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B1,B0,B0,B1,B1] :: 6 Word.word))))))) then + (let (rs :: regno) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 6 :: int)::ii) :: 5 Word.word)) in (let (cd1 :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in (let (cb :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in - (let (rs :: regno) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 6 :: int)::ii) :: 5 Word.word)) in Some (CFromPtr (cd1,cb,rs))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 21 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B1,B0,B0,B1,B0,B0,B0,B0,B0,B0] :: 11 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 5 :: int)::ii) (( 0 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B0,B1,B0,B1,B0] :: 6 Word.word))))))) then (let (rt :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in - (let (cb :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in (let (cs :: regno) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 6 :: int)::ii) :: 5 Word.word)) in + (let (cb :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in Some (CSub (rt,cb,cs))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 21 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B1,B0,B0,B1,B0,B0,B0,B0,B0,B0] :: 11 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 5 :: int)::ii) (( 0 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B1,B1,B0,B1,B1] :: 6 Word.word))))))) then - (let (cd1 :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in - (let (cs :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in (let (rs :: regno) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 6 :: int)::ii) :: 5 Word.word)) in + (let (cs :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in + (let (cd1 :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in Some (CMOVX (cd1,cs,rs,False))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 21 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B1,B0,B0,B1,B0,B0,B0,B0,B0,B0] :: 11 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 5 :: int)::ii) (( 0 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B1,B1,B1,B0,B0] :: 6 Word.word))))))) then - (let (cd1 :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in - (let (cs :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in (let (rs :: regno) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 6 :: int)::ii) :: 5 Word.word)) in + (let (cs :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in + (let (cd1 :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in Some (CMOVX (cd1,cs,rs,True))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 21 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B1,B0,B0,B1,B0,B0,B0,B0,B0,B0] :: 11 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 5 :: int)::ii) (( 0 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B1,B0,B1,B0,B0] :: 6 Word.word))))))) then (let (rd :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in - (let (cb :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in (let (cs :: regno) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 6 :: int)::ii) :: 5 Word.word)) in + (let (cb :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in Some (CPtrCmp (rd,cb,cs,CEQ))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 21 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B1,B0,B0,B1,B0,B0,B0,B0,B0,B0] :: 11 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 5 :: int)::ii) (( 0 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B1,B0,B1,B0,B1] :: 6 Word.word))))))) then (let (rd :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in - (let (cb :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in (let (cs :: regno) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 6 :: int)::ii) :: 5 Word.word)) in + (let (cb :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in Some (CPtrCmp (rd,cb,cs,CNE))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 21 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B1,B0,B0,B1,B0,B0,B0,B0,B0,B0] :: 11 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 5 :: int)::ii) (( 0 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B1,B0,B1,B1,B0] :: 6 Word.word))))))) then (let (rd :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in - (let (cb :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in (let (cs :: regno) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 6 :: int)::ii) :: 5 Word.word)) in + (let (cb :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in Some (CPtrCmp (rd,cb,cs,CLT))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 21 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B1,B0,B0,B1,B0,B0,B0,B0,B0,B0] :: 11 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 5 :: int)::ii) (( 0 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B1,B0,B1,B1,B1] :: 6 Word.word))))))) then (let (rd :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in - (let (cb :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in (let (cs :: regno) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 6 :: int)::ii) :: 5 Word.word)) in + (let (cb :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in Some (CPtrCmp (rd,cb,cs,CLE))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 21 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B1,B0,B0,B1,B0,B0,B0,B0,B0,B0] :: 11 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 5 :: int)::ii) (( 0 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B1,B1,B0,B0,B0] :: 6 Word.word))))))) then (let (rd :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in - (let (cb :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in (let (cs :: regno) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 6 :: int)::ii) :: 5 Word.word)) in + (let (cb :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in Some (CPtrCmp (rd,cb,cs,CLTU))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 21 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B1,B0,B0,B1,B0,B0,B0,B0,B0,B0] :: 11 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 5 :: int)::ii) (( 0 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B1,B1,B0,B0,B1] :: 6 Word.word))))))) then (let (rd :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in - (let (cb :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in (let (cs :: regno) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 6 :: int)::ii) :: 5 Word.word)) in + (let (cb :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in Some (CPtrCmp (rd,cb,cs,CLEU))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 21 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B1,B0,B0,B1,B0,B0,B0,B0,B0,B0] :: 11 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 5 :: int)::ii) (( 0 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B1,B1,B0,B1,B0] :: 6 Word.word))))))) then (let (rd :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in - (let (cb :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in (let (cs :: regno) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 6 :: int)::ii) :: 5 Word.word)) in + (let (cb :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in Some (CPtrCmp (rd,cb,cs,CEXEQ))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 21 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B1,B0,B0,B1,B0,B0,B0,B0,B0,B0] :: 11 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 5 :: int)::ii) (( 0 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B1,B0,B0,B0,B0,B1] :: 6 Word.word))))))) then (let (rd :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in - (let (cb :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in (let (cs :: regno) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 6 :: int)::ii) :: 5 Word.word)) in + (let (cb :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in Some (CPtrCmp (rd,cb,cs,CNEXEQ))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 21 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B1,B0,B0,B1,B0,B0,B0,B0,B0,B0] :: 11 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 5 :: int)::ii) (( 0 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B1,B0,B0,B0,B0,B0] :: 6 Word.word))))))) then (let (rd :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in - (let (cb :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in (let (ct :: regno) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 6 :: int)::ii) :: 5 Word.word)) in + (let (cb :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in Some (CTestSubset (rd,cb,ct))))) else if (((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 21 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B1,B0,B0,B1,B0,B0,B1,B0,B0,B1] :: 11 Word.word)))) then - (let (cd1 :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in (let (imm :: 16 bits) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 0 :: int)::ii) :: 16 Word.word)) in + (let (cd1 :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in Some (CBX (cd1,imm,True)))) else if (((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 21 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B1,B0,B0,B1,B0,B0,B1,B0,B1,B0] :: 11 Word.word)))) then - (let (cd1 :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in (let (imm :: 16 bits) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 0 :: int)::ii) :: 16 Word.word)) in + (let (cd1 :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in Some (CBX (cd1,imm,False)))) else if (((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 21 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B1,B0,B0,B1,B0,B1,B0,B0,B0,B1] :: 11 Word.word)))) then - (let (cd1 :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in (let (imm :: 16 bits) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 0 :: int)::ii) :: 16 Word.word)) in + (let (cd1 :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in Some (CBZ (cd1,imm,False)))) else if (((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 21 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B1,B0,B0,B1,B0,B1,B0,B0,B1,B0] :: 11 Word.word)))) then - (let (cd1 :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in (let (imm :: 16 bits) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 0 :: int)::ii) :: 16 Word.word)) in + (let (cd1 :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in Some (CBZ (cd1,imm,True)))) else if (((v__0 = (vec_of_bits [B0,B1,B0,B0,B1,B0,B0,B0,B1,B0,B1,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B1,B1,B1, B1,B1,B1,B1,B1,B1,B1,B1] :: 32 Word.word)))) then Some (CReturn () ) else if (((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 21 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B1,B0,B0,B1,B0,B0,B0,B1,B0,B1] :: 11 Word.word)))) then + (let (selector :: 11 bits) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 0 :: int)::ii) :: 11 Word.word)) in (let (cs :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in (let (cb :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in - (let (selector :: 11 bits) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 0 :: int)::ii) :: 11 Word.word)) in Some (CCall (cs,cb,selector))))) else if (((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 16 :: int)::ii) :: 16 Word.word)) = (vec_of_bits [B0,B1,B0,B0,B1,B0,B0,B1,B1,B1,B1,B0,B0,B0,B0,B0] :: 16 Word.word)))) then (let (imm :: 16 bits) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 0 :: int)::ii) :: 16 Word.word)) in @@ -5242,56 +5248,56 @@ definition decode :: "(32)Word.word \<Rightarrow>(ast)option " where (let (imm :: 16 bits) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 0 :: int)::ii) :: 16 Word.word)) in Some (ClearRegs (CHi,imm))) else if (((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 21 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B1,B0,B0,B1,B0,B1,B0,B0,B1,B1] :: 11 Word.word)))) then + (let (imm :: 11 bits) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 0 :: int)::ii) :: 11 Word.word)) in (let (cd1 :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in (let (cb :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in - (let (imm :: 11 bits) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 0 :: int)::ii) :: 11 Word.word)) in Some (CIncOffsetImmediate (cd1,cb,imm))))) else if (((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 21 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B1,B0,B0,B1,B0,B1,B0,B1,B0,B0] :: 11 Word.word)))) then + (let (imm :: 11 bits) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 0 :: int)::ii) :: 11 Word.word)) in (let (cd1 :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in (let (cb :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in - (let (imm :: 11 bits) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 0 :: int)::ii) :: 11 Word.word)) in Some (CSetBoundsImmediate (cd1,cb,imm))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B1,B1,B0,B0,B1,B0] :: 6 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 2 :: int)::ii) (( 0 :: int)::ii) :: 3 Word.word)) = (vec_of_bits [B0,B0,B0] :: 3 Word.word))))))) then - (let (rd :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in - (let (cb :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in + (let (rd :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (offset :: 8 bits) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 3 :: int)::ii) :: 8 Word.word)) in + (let (cb :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in Some (CLoad (rd,cb,rt,offset,False,B,False)))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B1,B1,B0,B0,B1,B0] :: 6 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 2 :: int)::ii) (( 0 :: int)::ii) :: 3 Word.word)) = (vec_of_bits [B1,B0,B0] :: 3 Word.word))))))) then - (let (rd :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in - (let (cb :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in + (let (rd :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (offset :: 8 bits) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 3 :: int)::ii) :: 8 Word.word)) in + (let (cb :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in Some (CLoad (rd,cb,rt,offset,True,B,False)))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B1,B1,B0,B0,B1,B0] :: 6 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 2 :: int)::ii) (( 0 :: int)::ii) :: 3 Word.word)) = (vec_of_bits [B0,B0,B1] :: 3 Word.word))))))) then - (let (rd :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in - (let (cb :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in + (let (rd :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (offset :: 8 bits) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 3 :: int)::ii) :: 8 Word.word)) in + (let (cb :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in Some (CLoad (rd,cb,rt,offset,False,H,False)))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B1,B1,B0,B0,B1,B0] :: 6 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 2 :: int)::ii) (( 0 :: int)::ii) :: 3 Word.word)) = (vec_of_bits [B1,B0,B1] :: 3 Word.word))))))) then - (let (rd :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in - (let (cb :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in + (let (rd :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (offset :: 8 bits) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 3 :: int)::ii) :: 8 Word.word)) in + (let (cb :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in Some (CLoad (rd,cb,rt,offset,True,H,False)))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B1,B1,B0,B0,B1,B0] :: 6 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 2 :: int)::ii) (( 0 :: int)::ii) :: 3 Word.word)) = (vec_of_bits [B0,B1,B0] :: 3 Word.word))))))) then - (let (rd :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in - (let (cb :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in + (let (rd :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (offset :: 8 bits) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 3 :: int)::ii) :: 8 Word.word)) in + (let (cb :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in Some (CLoad (rd,cb,rt,offset,False,W,False)))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B1,B1,B0,B0,B1,B0] :: 6 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 2 :: int)::ii) (( 0 :: int)::ii) :: 3 Word.word)) = (vec_of_bits [B1,B1,B0] :: 3 Word.word))))))) then - (let (rd :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in - (let (cb :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in + (let (rd :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (offset :: 8 bits) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 3 :: int)::ii) :: 8 Word.word)) in + (let (cb :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in Some (CLoad (rd,cb,rt,offset,True,W,False)))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B1,B1,B0,B0,B1,B0] :: 6 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 2 :: int)::ii) (( 0 :: int)::ii) :: 3 Word.word)) = (vec_of_bits [B0,B1,B1] :: 3 Word.word))))))) then - (let (rd :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in - (let (cb :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in + (let (rd :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (offset :: 8 bits) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 3 :: int)::ii) :: 8 Word.word)) in + (let (cb :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in Some (CLoad (rd,cb,rt,offset,False,D,False)))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 21 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B1,B0,B0,B1,B0,B1,B0,B0,B0,B0] :: 11 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 0 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0,B0,B1,B0,B0,B0] :: 11 Word.word))))))) then (let (rd :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in @@ -5336,75 +5342,75 @@ definition decode :: "(32)Word.word \<Rightarrow>(ast)option " where B0,B0] :: 8 Word.word),False,D,True)))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B1,B1,B1,B0,B1,B0] :: 6 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 2 :: int)::ii) (( 0 :: int)::ii) :: 3 Word.word)) = (vec_of_bits [B0,B0,B0] :: 3 Word.word))))))) then - (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in - (let (cb :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in + (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (offset :: 8 bits) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 3 :: int)::ii) :: 8 Word.word)) in + (let (cb :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in Some (CStore (rs,cb,rt,(vec_of_bits [B0,B0,B0,B0,B0] :: 5 Word.word),offset,B,False)))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B1,B1,B1,B0,B1,B0] :: 6 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 2 :: int)::ii) (( 0 :: int)::ii) :: 3 Word.word)) = (vec_of_bits [B0,B0,B1] :: 3 Word.word))))))) then - (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in - (let (cb :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in + (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (offset :: 8 bits) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 3 :: int)::ii) :: 8 Word.word)) in + (let (cb :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in Some (CStore (rs,cb,rt,(vec_of_bits [B0,B0,B0,B0,B0] :: 5 Word.word),offset,H,False)))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B1,B1,B1,B0,B1,B0] :: 6 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 2 :: int)::ii) (( 0 :: int)::ii) :: 3 Word.word)) = (vec_of_bits [B0,B1,B0] :: 3 Word.word))))))) then - (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in - (let (cb :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in + (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (offset :: 8 bits) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 3 :: int)::ii) :: 8 Word.word)) in + (let (cb :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in Some (CStore (rs,cb,rt,(vec_of_bits [B0,B0,B0,B0,B0] :: 5 Word.word),offset,W,False)))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B1,B1,B1,B0,B1,B0] :: 6 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 2 :: int)::ii) (( 0 :: int)::ii) :: 3 Word.word)) = (vec_of_bits [B0,B1,B1] :: 3 Word.word))))))) then - (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in - (let (cb :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in + (let (rs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (offset :: 8 bits) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 3 :: int)::ii) :: 8 Word.word)) in + (let (cb :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in Some (CStore (rs,cb,rt,(vec_of_bits [B0,B0,B0,B0,B0] :: 5 Word.word),offset,D,False)))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 21 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B1,B0,B0,B1,B0,B1,B0,B0,B0,B0] :: 11 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 5 :: int)::ii) (( 0 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0] :: 6 Word.word))))))) then (let (rs :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in - (let (cb :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in (let (rd :: regno) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 6 :: int)::ii) :: 5 Word.word)) in + (let (cb :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in Some (CStore (rs,cb,(vec_of_bits [B0,B0,B0,B0,B0] :: 5 Word.word),rd,(vec_of_bits [B0,B0,B0,B0,B0, B0,B0,B0] :: 8 Word.word),B,True))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 21 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B1,B0,B0,B1,B0,B1,B0,B0,B0,B0] :: 11 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 5 :: int)::ii) (( 0 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B1] :: 6 Word.word))))))) then (let (rs :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in - (let (cb :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in (let (rd :: regno) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 6 :: int)::ii) :: 5 Word.word)) in + (let (cb :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in Some (CStore (rs,cb,(vec_of_bits [B0,B0,B0,B0,B0] :: 5 Word.word),rd,(vec_of_bits [B0,B0,B0,B0,B0, B0,B0,B0] :: 8 Word.word),H,True))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 21 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B1,B0,B0,B1,B0,B1,B0,B0,B0,B0] :: 11 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 5 :: int)::ii) (( 0 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B1,B0] :: 6 Word.word))))))) then (let (rs :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in - (let (cb :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in (let (rd :: regno) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 6 :: int)::ii) :: 5 Word.word)) in + (let (cb :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in Some (CStore (rs,cb,(vec_of_bits [B0,B0,B0,B0,B0] :: 5 Word.word),rd,(vec_of_bits [B0,B0,B0,B0,B0, B0,B0,B0] :: 8 Word.word),W,True))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 21 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B1,B0,B0,B1,B0,B1,B0,B0,B0,B0] :: 11 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 5 :: int)::ii) (( 0 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B1,B1] :: 6 Word.word))))))) then (let (rs :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in - (let (cb :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in (let (rd :: regno) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 6 :: int)::ii) :: 5 Word.word)) in + (let (cb :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in Some (CStore (rs,cb,(vec_of_bits [B0,B0,B0,B0,B0] :: 5 Word.word),rd,(vec_of_bits [B0,B0,B0,B0,B0, B0,B0,B0] :: 8 Word.word),D,True))))) else if (((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B1,B1,B1,B1,B1,B0] :: 6 Word.word)))) then - (let (cs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in - (let (cb :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in (let (offset :: 11 bits) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 0 :: int)::ii) :: 11 Word.word)) in + (let (cs :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in + (let (cb :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in Some (CSC (cs,cb,rt,(vec_of_bits [B0,B0,B0,B0,B0] :: 5 Word.word),offset,False)))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 21 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B1,B0,B0,B1,B0,B1,B0,B0,B0,B0] :: 11 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 5 :: int)::ii) (( 0 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B0,B0,B1,B1,B1] :: 6 Word.word))))))) then + (let (rd :: regno) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 6 :: int)::ii) :: 5 Word.word)) in (let (cs :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in (let (cb :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in - (let (rd :: regno) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 6 :: int)::ii) :: 5 Word.word)) in Some (CSC (cs,cb,(vec_of_bits [B0,B0,B0,B0,B0] :: 5 Word.word),rd,(vec_of_bits [B0,B0,B0,B0,B0,B0, B0,B0,B0,B0,B0] :: 11 Word.word),True))))) else if (((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B1,B1,B0,B1,B1,B0] :: 6 Word.word)))) then - (let (cd1 :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in - (let (cb :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in (let (rt :: regno) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 11 :: int)::ii) :: 5 Word.word)) in (let (offset :: 11 bits) = ((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 0 :: int)::ii) :: 11 Word.word)) in + (let (cd1 :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in + (let (cb :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in Some (CLC (cd1,cb,rt,(mips_sign_extend (( 16 :: int)::ii) offset :: 16 Word.word),False)))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 21 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B1,B0,B0,B1,B0,B1,B0,B0,B0,B0] :: 11 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 10 :: int)::ii) (( 0 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0,B0,B1,B1,B1,B1] :: 11 Word.word))))))) then (let (cd1 :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in @@ -5414,9 +5420,9 @@ definition decode :: "(32)Word.word \<Rightarrow>(ast)option " where B0,B0] :: 16 Word.word),True)))) else if (((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 26 :: int)::ii) :: 6 Word.word)) = (vec_of_bits [B0,B1,B1,B1,B0,B1] :: 6 Word.word)))) then + (let (offset :: 16 bits) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 0 :: int)::ii) :: 16 Word.word)) in (let (cd1 :: regno) = ((subrange_vec_dec v__0 (( 25 :: int)::ii) (( 21 :: int)::ii) :: 5 Word.word)) in (let (cb :: regno) = ((subrange_vec_dec v__0 (( 20 :: int)::ii) (( 16 :: int)::ii) :: 5 Word.word)) in - (let (offset :: 16 bits) = ((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 0 :: int)::ii) :: 16 Word.word)) in Some (CLC (cd1,cb,(vec_of_bits [B0,B0,B0,B0,B0] :: 5 Word.word),offset,False))))) else if ((((((((subrange_vec_dec v__0 (( 31 :: int)::ii) (( 21 :: int)::ii) :: 11 Word.word)) = (vec_of_bits [B0,B1,B0,B0,B1,B0,B0,B0,B1,B0,B0] :: 11 Word.word)))) \<and> (((((subrange_vec_dec v__0 (( 15 :: int)::ii) (( 0 :: int)::ii) :: 16 Word.word)) = (vec_of_bits [B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B1,B1,B0] :: 16 Word.word))))))) then @@ -5445,7 +5451,7 @@ definition execute_XOR :: "(5)Word.word \<Rightarrow>(5)Word.word \<Rightarrow> (*val execute_WAIT : unit -> M unit*) definition execute_WAIT :: " unit \<Rightarrow>((register_value),(unit),(exception))monad " where - " execute_WAIT g__19 = ( + " execute_WAIT _ = ( (read_reg PC_ref :: ( 64 Word.word) M) \<bind> (\<lambda> (w__0 :: 64 bits) . write_reg nextPC_ref w__0))" @@ -5474,23 +5480,23 @@ definition execute_TRAPIMM :: "(5)Word.word \<Rightarrow>(16)Word.word \<Righta (*val execute_TLBWR : unit -> M unit*) definition execute_TLBWR :: " unit \<Rightarrow>((register_value),(unit),(exception))monad " where - " execute_TLBWR g__23 = ( + " execute_TLBWR _ = ( (checkCP0Access () \<then> - (read_reg TLBRandom_ref :: ( 6 Word.word) M)) \<bind> (\<lambda> (w__0 :: 6 Word.word) . TLBWriteEntry w__0))" + (read_reg TLBRandom_ref :: ( 6 Word.word) M)) \<bind> (\<lambda> (w__0 :: TLBIndexT) . TLBWriteEntry w__0))" (*val execute_TLBWI : unit -> M unit*) definition execute_TLBWI :: " unit \<Rightarrow>((register_value),(unit),(exception))monad " where - " execute_TLBWI g__22 = ( + " execute_TLBWI _ = ( (checkCP0Access () \<then> - (read_reg TLBIndex_ref :: ( 6 Word.word) M)) \<bind> (\<lambda> (w__0 :: 6 Word.word) . TLBWriteEntry w__0))" + (read_reg TLBIndex_ref :: ( 6 Word.word) M)) \<bind> (\<lambda> (w__0 :: TLBIndexT) . TLBWriteEntry w__0))" (*val execute_TLBR : unit -> M unit*) definition execute_TLBR :: " unit \<Rightarrow>((register_value),(unit),(exception))monad " where - " execute_TLBR g__24 = ( + " execute_TLBR _ = ( (checkCP0Access () \<then> (read_reg TLBIndex_ref :: ( 6 Word.word) M)) \<bind> (\<lambda> (w__0 :: TLBIndexT) . (let i = (Word.uint w__0) in @@ -5518,7 +5524,7 @@ definition execute_TLBR :: " unit \<Rightarrow>((register_value),(unit),(except (*val execute_TLBP : unit -> M unit*) definition execute_TLBP :: " unit \<Rightarrow>((register_value),(unit),(exception))monad " where - " execute_TLBP g__25 = ( + " execute_TLBP _ = ( (checkCP0Access () \<then> read_reg TLBEntryHi_ref) \<bind> (\<lambda> (w__0 :: TLBEntryHiReg) . (tlbSearch ((get_TLBEntryHiReg_bits w__0 :: 64 Word.word)) :: ( ( 6 Word.word)option) M) \<bind> (\<lambda> result . @@ -5567,13 +5573,13 @@ definition execute_Store :: " WordType \<Rightarrow> bool \<Rightarrow>(5)Word. (*val execute_SYSCALL : unit -> M unit*) definition execute_SYSCALL :: " unit \<Rightarrow>((register_value),(unit),(exception))monad " where - " execute_SYSCALL g__17 = ( SignalException Sys )" + " execute_SYSCALL _ = ( SignalException Sys )" (*val execute_SYNC : unit -> M unit*) definition execute_SYNC :: " unit \<Rightarrow>((register_value),(unit),(exception))monad " where - " execute_SYNC g__20 = ( MEM_sync () )" + " execute_SYNC _ = ( MEM_sync () )" (*val execute_SWR : mword ty5 -> mword ty5 -> mword ty16 -> M unit*) @@ -5866,7 +5872,7 @@ definition execute_SDL :: "(5)Word.word \<Rightarrow>(5)Word.word \<Rightarrow> (*val execute_RI : unit -> M unit*) definition execute_RI :: " unit \<Rightarrow>((register_value),(unit),(exception))monad " where - " execute_RI g__28 = ( SignalException ResI )" + " execute_RI _ = ( SignalException ResI )" (*val execute_RDHWR : mword ty5 -> mword ty5 -> M unit*) @@ -5996,14 +6002,14 @@ definition execute_MUL :: "(5)Word.word \<Rightarrow>(5)Word.word \<Rightarrow> definition execute_MTLO :: "(5)Word.word \<Rightarrow>((register_value),(unit),(exception))monad " where " execute_MTLO rs = ( - (rGPR rs :: ( 64 Word.word) M) \<bind> (\<lambda> (w__0 :: 64 bits) . write_reg LO_ref w__0))" + (rGPR rs :: ( 64 Word.word) M) \<bind> (\<lambda> (w__0 :: 64 Word.word) . write_reg LO_ref w__0))" (*val execute_MTHI : mword ty5 -> M unit*) definition execute_MTHI :: "(5)Word.word \<Rightarrow>((register_value),(unit),(exception))monad " where " execute_MTHI rs = ( - (rGPR rs :: ( 64 Word.word) M) \<bind> (\<lambda> (w__0 :: 64 bits) . write_reg HI_ref w__0))" + (rGPR rs :: ( 64 Word.word) M) \<bind> (\<lambda> (w__0 :: 64 Word.word) . write_reg HI_ref w__0))" (*val execute_MTC0 : mword ty5 -> mword ty5 -> mword ty3 -> bool -> M unit*) @@ -6191,15 +6197,13 @@ definition execute_MOVN :: "(5)Word.word \<Rightarrow>(5)Word.word \<Rightarrow (*val execute_MFLO : mword ty5 -> M unit*) definition execute_MFLO :: "(5)Word.word \<Rightarrow>((register_value),(unit),(exception))monad " where - " execute_MFLO rd = ( - (read_reg LO_ref :: ( 64 Word.word) M) \<bind> (\<lambda> (w__0 :: 64 Word.word) . wGPR rd w__0))" + " execute_MFLO rd = ( (read_reg LO_ref :: ( 64 Word.word) M) \<bind> (\<lambda> (w__0 :: 64 bits) . wGPR rd w__0))" (*val execute_MFHI : mword ty5 -> M unit*) definition execute_MFHI :: "(5)Word.word \<Rightarrow>((register_value),(unit),(exception))monad " where - " execute_MFHI rd = ( - (read_reg HI_ref :: ( 64 Word.word) M) \<bind> (\<lambda> (w__0 :: 64 Word.word) . wGPR rd w__0))" + " execute_MFHI rd = ( (read_reg HI_ref :: ( 64 Word.word) M) \<bind> (\<lambda> (w__0 :: 64 bits) . wGPR rd w__0))" (*val execute_MFC0 : mword ty5 -> mword ty5 -> mword ty3 -> bool -> M unit*) @@ -6675,7 +6679,7 @@ definition execute_JALR :: "(5)Word.word \<Rightarrow>(5)Word.word \<Rightarrow " execute_JALR rs rd = ( (rGPR rs :: ( 64 Word.word) M) \<bind> (\<lambda> (w__0 :: 64 Word.word) . (execute_branch w__0 \<then> - (read_reg PC_ref :: ( 64 Word.word) M)) \<bind> (\<lambda> (w__1 :: 64 Word.word) . + (read_reg PC_ref :: ( 64 Word.word) M)) \<bind> (\<lambda> (w__1 :: 64 bits) . wGPR rd ((add_vec_int w__1 (( 8 :: int)::ii) :: 64 Word.word)))))" @@ -6689,7 +6693,7 @@ definition execute_JAL :: "(26)Word.word \<Rightarrow>((register_value),(unit), ((subrange_vec_dec ((add_vec_int w__0 (( 4 :: int)::ii) :: 64 Word.word)) (( 63 :: int)::ii) (( 28 :: int)::ii) :: 36 Word.word)) ((concat_vec offset (vec_of_bits [B0,B0] :: 2 Word.word) :: 28 Word.word)) :: 64 Word.word)) \<then> - (read_reg PC_ref :: ( 64 Word.word) M)) \<bind> (\<lambda> (w__1 :: 64 Word.word) . + (read_reg PC_ref :: ( 64 Word.word) M)) \<bind> (\<lambda> (w__1 :: 64 bits) . wGPR (vec_of_bits [B1,B1,B1,B1,B1] :: 5 Word.word) ((add_vec_int w__1 (( 8 :: int)::ii) :: 64 Word.word)))))" @@ -6708,13 +6712,13 @@ definition execute_J :: "(26)Word.word \<Rightarrow>((register_value),(unit),(e (*val execute_HCF : unit -> unit*) definition execute_HCF :: " unit \<Rightarrow> unit " where - " execute_HCF g__21 = ( () )" + " execute_HCF _ = ( () )" (*val execute_ERET : unit -> M unit*) definition execute_ERET :: " unit \<Rightarrow>((register_value),(unit),(exception))monad " where - " execute_ERET g__26 = ( + " execute_ERET _ = ( (((checkCP0Access () \<then> ERETHook () ) \<then> write_reg CP0LLBit_ref (vec_of_bits [B0] :: 1 Word.word)) \<then> @@ -6871,9 +6875,9 @@ definition execute_DIVU :: "(5)Word.word \<Rightarrow>(5)Word.word \<Rightarrow B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0] :: 64 Word.word)))))))))) then (undefined_bitvector - instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 32 :: int)::ii) :: ( 32 Word.word) M) \<bind> (\<lambda> (w__0 :: 32 bits) . + instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 32 :: int)::ii) :: ( 32 Word.word) M) \<bind> (\<lambda> (w__0 :: 32 Word.word) . (undefined_bitvector - instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 32 :: int)::ii) :: ( 32 Word.word) M) \<bind> (\<lambda> (w__1 :: 32 bits) . + instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 32 :: int)::ii) :: ( 32 Word.word) M) \<bind> (\<lambda> (w__1 :: 32 Word.word) . return (w__0, w__1))) else (let si = (Word.uint ((subrange_vec_dec rsVal (( 31 :: int)::ii) (( 0 :: int)::ii) :: 32 Word.word))) in @@ -6897,9 +6901,9 @@ definition execute_DIV :: "(5)Word.word \<Rightarrow>(5)Word.word \<Rightarrow> B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0,B0] :: 64 Word.word)))))))))) then (undefined_bitvector - instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 32 :: int)::ii) :: ( 32 Word.word) M) \<bind> (\<lambda> (w__0 :: 32 bits) . + instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 32 :: int)::ii) :: ( 32 Word.word) M) \<bind> (\<lambda> (w__0 :: 32 Word.word) . (undefined_bitvector - instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 32 :: int)::ii) :: ( 32 Word.word) M) \<bind> (\<lambda> (w__1 :: 32 bits) . + instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 32 :: int)::ii) :: ( 32 Word.word) M) \<bind> (\<lambda> (w__1 :: 32 Word.word) . return (w__0, w__1))) else (let si = (Word.sint ((subrange_vec_dec rsVal (( 31 :: int)::ii) (( 0 :: int)::ii) :: 32 Word.word))) in @@ -6922,9 +6926,9 @@ definition execute_DDIVU :: "(5)Word.word \<Rightarrow>(5)Word.word \<Rightarro (let rtVal = (Word.uint w__1) in (if (((rtVal = (( 0 :: int)::ii)))) then (undefined_bitvector - instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 64 :: int)::ii) :: ( 64 Word.word) M) \<bind> (\<lambda> (w__2 :: 64 bits) . + instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 64 :: int)::ii) :: ( 64 Word.word) M) \<bind> (\<lambda> (w__2 :: 64 Word.word) . (undefined_bitvector - instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 64 :: int)::ii) :: ( 64 Word.word) M) \<bind> (\<lambda> (w__3 :: 64 bits) . + instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 64 :: int)::ii) :: ( 64 Word.word) M) \<bind> (\<lambda> (w__3 :: 64 Word.word) . return (w__2, w__3))) else (let qi = (hardware_quot rsVal rtVal) in @@ -6944,9 +6948,9 @@ definition execute_DDIV :: "(5)Word.word \<Rightarrow>(5)Word.word \<Rightarrow (let rtVal = (Word.sint w__1) in (if (((rtVal = (( 0 :: int)::ii)))) then (undefined_bitvector - instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 64 :: int)::ii) :: ( 64 Word.word) M) \<bind> (\<lambda> (w__2 :: 64 bits) . + instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 64 :: int)::ii) :: ( 64 Word.word) M) \<bind> (\<lambda> (w__2 :: 64 Word.word) . (undefined_bitvector - instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 64 :: int)::ii) :: ( 64 Word.word) M) \<bind> (\<lambda> (w__3 :: 64 bits) . + instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 64 :: int)::ii) :: ( 64 Word.word) M) \<bind> (\<lambda> (w__3 :: 64 Word.word) . return (w__2, w__3))) else (let qi = (hardware_quot rsVal rtVal) in @@ -7469,7 +7473,7 @@ definition execute_CSC :: "(5)Word.word \<Rightarrow>(5)Word.word \<Rightarrow> (*val execute_CReturn : unit -> M unit*) definition execute_CReturn :: " unit \<Rightarrow>((register_value),(unit),(exception))monad " where - " execute_CReturn g__27 = ( checkCP2usable () \<then> raise_c2_exception_noreg CapEx_ReturnTrap )" + " execute_CReturn _ = ( checkCP2usable () \<then> raise_c2_exception_noreg CapEx_ReturnTrap )" (*val execute_CReadHwr : mword ty5 -> mword ty5 -> M unit*) @@ -7502,28 +7506,28 @@ definition execute_CReadHwr :: "(5)Word.word \<Rightarrow>(5)Word.word \<Righta else (let p00 = (Word.uint sel) in (if (((p00 = (( 0 :: int)::ii)))) then - (read_reg DDC_ref :: ( 257 Word.word) M) \<bind> (\<lambda> (w__13 :: 257 Word.word) . + (read_reg DDC_ref :: ( 257 Word.word) M) \<bind> (\<lambda> (w__13 :: CapReg) . return ((capRegToCapStruct w__13))) else if (((p00 = (( 1 :: int)::ii)))) then - (read_reg CTLSU_ref :: ( 257 Word.word) M) \<bind> (\<lambda> (w__14 :: 257 Word.word) . + (read_reg CTLSU_ref :: ( 257 Word.word) M) \<bind> (\<lambda> (w__14 :: CapReg) . return ((capRegToCapStruct w__14))) else if (((p00 = (( 8 :: int)::ii)))) then - (read_reg CTLSP_ref :: ( 257 Word.word) M) \<bind> (\<lambda> (w__15 :: 257 Word.word) . + (read_reg CTLSP_ref :: ( 257 Word.word) M) \<bind> (\<lambda> (w__15 :: CapReg) . return ((capRegToCapStruct w__15))) else if (((p00 = (( 22 :: int)::ii)))) then - (read_reg KR1C_ref :: ( 257 Word.word) M) \<bind> (\<lambda> (w__16 :: 257 Word.word) . + (read_reg KR1C_ref :: ( 257 Word.word) M) \<bind> (\<lambda> (w__16 :: CapReg) . return ((capRegToCapStruct w__16))) else if (((p00 = (( 23 :: int)::ii)))) then - (read_reg KR2C_ref :: ( 257 Word.word) M) \<bind> (\<lambda> (w__17 :: 257 Word.word) . + (read_reg KR2C_ref :: ( 257 Word.word) M) \<bind> (\<lambda> (w__17 :: CapReg) . return ((capRegToCapStruct w__17))) else if (((p00 = (( 29 :: int)::ii)))) then - (read_reg KCC_ref :: ( 257 Word.word) M) \<bind> (\<lambda> (w__18 :: 257 Word.word) . + (read_reg KCC_ref :: ( 257 Word.word) M) \<bind> (\<lambda> (w__18 :: CapReg) . return ((capRegToCapStruct w__18))) else if (((p00 = (( 30 :: int)::ii)))) then - (read_reg KDC_ref :: ( 257 Word.word) M) \<bind> (\<lambda> (w__19 :: 257 Word.word) . + (read_reg KDC_ref :: ( 257 Word.word) M) \<bind> (\<lambda> (w__19 :: CapReg) . return ((capRegToCapStruct w__19))) else if (((p00 = (( 31 :: int)::ii)))) then - (read_reg EPCC_ref :: ( 257 Word.word) M) \<bind> (\<lambda> (w__20 :: 257 Word.word) . + (read_reg EPCC_ref :: ( 257 Word.word) M) \<bind> (\<lambda> (w__20 :: CapReg) . return ((capRegToCapStruct w__20))) else assert_exp False (''should be unreachable code'') \<then> undefined_CapStruct () ) \<bind> (\<lambda> (capVal :: CapStruct) . @@ -7810,9 +7814,9 @@ definition execute_CJALR :: "(5)Word.word \<Rightarrow>(5)Word.word \<Rightarro else if (((((cb_ptr mod (( 4 :: int)::ii))) \<noteq> (( 0 :: int)::ii)))) then SignalException AdEL else (if link then - (read_reg PCC_ref :: ( 257 Word.word) M) \<bind> (\<lambda> (w__3 :: 257 Word.word) . + (read_reg PCC_ref :: ( 257 Word.word) M) \<bind> (\<lambda> (w__3 :: CapReg) . (let pcc = (capRegToCapStruct w__3) in - (read_reg PC_ref :: ( 64 Word.word) M) \<bind> (\<lambda> (w__4 :: 64 Word.word) . + (read_reg PC_ref :: ( 64 Word.word) M) \<bind> (\<lambda> (w__4 :: 64 bits) . (let (success, linkCap) = (setCapOffset pcc ((add_vec_int w__4 (( 8 :: int)::ii) :: 64 Word.word))) in if success then writeCapReg cd1 linkCap else assert_exp False (''''))))) @@ -7938,7 +7942,7 @@ definition execute_CGetPCCSetOffset :: "(5)Word.word \<Rightarrow>(5)Word.word register_inaccessible cd1) \<bind> (\<lambda> (w__0 :: bool) . if w__0 then raise_c2_exception CapEx_AccessSystemRegsViolation cd1 else - (read_reg PCC_ref :: ( 257 Word.word) M) \<bind> (\<lambda> (w__1 :: 257 Word.word) . + (read_reg PCC_ref :: ( 257 Word.word) M) \<bind> (\<lambda> (w__1 :: CapReg) . (let pcc = (capRegToCapStruct w__1) in (rGPR rs :: ( 64 Word.word) M) \<bind> (\<lambda> rs_val . (let (success, newPCC) = (setCapOffset pcc rs_val) in @@ -7954,9 +7958,9 @@ definition execute_CGetPCC :: "(5)Word.word \<Rightarrow>((register_value),(uni register_inaccessible cd1) \<bind> (\<lambda> (w__0 :: bool) . if w__0 then raise_c2_exception CapEx_AccessSystemRegsViolation cd1 else - (read_reg PCC_ref :: ( 257 Word.word) M) \<bind> (\<lambda> (w__1 :: 257 Word.word) . + (read_reg PCC_ref :: ( 257 Word.word) M) \<bind> (\<lambda> (w__1 :: CapReg) . (let pcc = (capRegToCapStruct w__1) in - (read_reg PC_ref :: ( 64 Word.word) M) \<bind> (\<lambda> (w__2 :: 64 Word.word) . + (read_reg PC_ref :: ( 64 Word.word) M) \<bind> (\<lambda> (w__2 :: 64 bits) . (let (success, pcc2) = (setCapOffset pcc w__2) in assert_exp success ('''') \<then> writeCapReg cd1 pcc2))))))" @@ -8312,7 +8316,7 @@ definition execute_CBZ :: "(5)Word.word \<Rightarrow>(16)Word.word \<Rightarrow ((concat_vec imm (vec_of_bits [B0,B0] :: 2 Word.word) :: 18 Word.word)) :: 64 Word.word)) (( 4 :: int)::ii) :: 64 Word.word)) in - (read_reg PC_ref :: ( 64 Word.word) M) \<bind> (\<lambda> (w__2 :: 64 Word.word) . + (read_reg PC_ref :: ( 64 Word.word) M) \<bind> (\<lambda> (w__2 :: 64 bits) . execute_branch ((add_vec w__2 offset :: 64 Word.word)))) else return () )))" @@ -8336,7 +8340,7 @@ definition execute_CBX :: "(5)Word.word \<Rightarrow>(16)Word.word \<Rightarrow ((concat_vec imm (vec_of_bits [B0,B0] :: 2 Word.word) :: 18 Word.word)) :: 64 Word.word)) (( 4 :: int)::ii) :: 64 Word.word)) in - (read_reg PC_ref :: ( 64 Word.word) M) \<bind> (\<lambda> (w__2 :: 64 Word.word) . + (read_reg PC_ref :: ( 64 Word.word) M) \<bind> (\<lambda> (w__2 :: 64 bits) . execute_branch ((add_vec w__2 offset :: 64 Word.word)))) else return () )))" @@ -8378,7 +8382,7 @@ definition execute_C2Dump :: "(5)Word.word \<Rightarrow> unit " where (*val execute_BREAK : unit -> M unit*) definition execute_BREAK :: " unit \<Rightarrow>((register_value),(unit),(exception))monad " where - " execute_BREAK g__18 = ( SignalException Bp )" + " execute_BREAK _ = ( SignalException Bp )" (*val execute_BEQ : mword ty5 -> mword ty5 -> mword ty16 -> bool -> bool -> M unit*) @@ -8397,10 +8401,10 @@ definition execute_BEQ :: "(5)Word.word \<Rightarrow>(5)Word.word \<Rightarrow> ((concat_vec imm (vec_of_bits [B0,B0] :: 2 Word.word) :: 18 Word.word)) :: 64 Word.word)) (( 4 :: int)::ii) :: 64 Word.word)) in - (read_reg PC_ref :: ( 64 Word.word) M) \<bind> (\<lambda> (w__2 :: 64 Word.word) . + (read_reg PC_ref :: ( 64 Word.word) M) \<bind> (\<lambda> (w__2 :: 64 bits) . execute_branch ((add_vec w__2 offset :: 64 Word.word)))) else if likely then - (read_reg PC_ref :: ( 64 Word.word) M) \<bind> (\<lambda> (w__3 :: 64 Word.word) . + (read_reg PC_ref :: ( 64 Word.word) M) \<bind> (\<lambda> (w__3 :: 64 bits) . write_reg nextPC_ref ((add_vec_int w__3 (( 8 :: int)::ii) :: 64 Word.word))) else return () )))" @@ -8421,10 +8425,10 @@ definition execute_BCMPZ :: "(5)Word.word \<Rightarrow>(16)Word.word \<Rightarr ((concat_vec imm (vec_of_bits [B0,B0] :: 2 Word.word) :: 18 Word.word)) :: 64 Word.word)) (( 4 :: int)::ii) :: 64 Word.word)) in - (read_reg PC_ref :: ( 64 Word.word) M) \<bind> (\<lambda> (w__1 :: 64 Word.word) . + (read_reg PC_ref :: ( 64 Word.word) M) \<bind> (\<lambda> (w__1 :: 64 bits) . execute_branch ((add_vec w__1 offset :: 64 Word.word)))) else if likely then - (read_reg PC_ref :: ( 64 Word.word) M) \<bind> (\<lambda> (w__2 :: 64 Word.word) . + (read_reg PC_ref :: ( 64 Word.word) M) \<bind> (\<lambda> (w__2 :: 64 bits) . write_reg nextPC_ref ((add_vec_int w__2 (( 8 :: int)::ii) :: 64 Word.word))) else return () ) \<then> (if link then wGPR (vec_of_bits [B1,B1,B1,B1,B1] :: 5 Word.word) linkVal @@ -8597,9 +8601,9 @@ fun execute :: " ast \<Rightarrow>((register_value),(unit),(exception))monad " |" execute (JALR (rs,rd)) = ( execute_JALR rs rd )" |" execute (BEQ (rs,rd,imm,ne,likely)) = ( execute_BEQ rs rd imm ne likely )" |" execute (BCMPZ (rs,imm,cmp,link,likely)) = ( execute_BCMPZ rs imm cmp link likely )" -|" execute (SYSCALL (g__17)) = ( execute_SYSCALL g__17 )" -|" execute (BREAK (g__18)) = ( execute_BREAK g__18 )" -|" execute (WAIT (g__19)) = ( execute_WAIT g__19 )" +|" execute (SYSCALL (arg0)) = ( execute_SYSCALL arg0 )" +|" execute (BREAK (arg0)) = ( execute_BREAK arg0 )" +|" execute (WAIT (arg0)) = ( execute_WAIT arg0 )" |" execute (TRAPREG (rs,rt,cmp)) = ( execute_TRAPREG rs rt cmp )" |" execute (TRAPIMM (rs,imm,cmp)) = ( execute_TRAPIMM rs imm cmp )" |" execute (Load (width,sign,linked,base,rt,offset)) = ( execute_Load width sign linked base rt offset )" @@ -8613,16 +8617,16 @@ fun execute :: " ast \<Rightarrow>((register_value),(unit),(exception))monad " |" execute (SDL (base,rt,offset)) = ( execute_SDL base rt offset )" |" execute (SDR (base,rt,offset)) = ( execute_SDR base rt offset )" |" execute (CACHE (base,op1,imm)) = ( execute_CACHE base op1 imm )" -|" execute (SYNC (g__20)) = ( execute_SYNC g__20 )" +|" execute (SYNC (arg0)) = ( execute_SYNC arg0 )" |" execute (MFC0 (rt,rd,sel,double)) = ( execute_MFC0 rt rd sel double )" -|" execute (HCF (g__21)) = ( return ((execute_HCF g__21)))" +|" execute (HCF (arg0)) = ( return ((execute_HCF arg0)))" |" execute (MTC0 (rt,rd,sel,double)) = ( execute_MTC0 rt rd sel double )" -|" execute (TLBWI (g__22)) = ( execute_TLBWI g__22 )" -|" execute (TLBWR (g__23)) = ( execute_TLBWR g__23 )" -|" execute (TLBR (g__24)) = ( execute_TLBR g__24 )" -|" execute (TLBP (g__25)) = ( execute_TLBP g__25 )" +|" execute (TLBWI (arg0)) = ( execute_TLBWI arg0 )" +|" execute (TLBWR (arg0)) = ( execute_TLBWR arg0 )" +|" execute (TLBR (arg0)) = ( execute_TLBR arg0 )" +|" execute (TLBP (arg0)) = ( execute_TLBP arg0 )" |" execute (RDHWR (rt,rd)) = ( execute_RDHWR rt rd )" -|" execute (ERET (g__26)) = ( execute_ERET g__26 )" +|" execute (ERET (arg0)) = ( execute_ERET arg0 )" |" execute (CGetPerm (rd,cb)) = ( execute_CGetPerm rd cb )" |" execute (CGetType (rd,cb)) = ( execute_CGetType rd cb )" |" execute (CGetBase (rd,cb)) = ( execute_CGetBase rd cb )" @@ -8660,7 +8664,7 @@ fun execute :: " ast \<Rightarrow>((register_value),(unit),(exception))monad " |" execute (CCSeal (cd1,cs,ct)) = ( execute_CCSeal cd1 cs ct )" |" execute (CUnseal (cd1,cs,ct)) = ( execute_CUnseal cd1 cs ct )" |" execute (CCall (cs,cb,b__151)) = ( execute_CCall cs cb b__151 )" -|" execute (CReturn (g__27)) = ( execute_CReturn g__27 )" +|" execute (CReturn (arg0)) = ( execute_CReturn arg0 )" |" execute (CBX (cb,imm,notset)) = ( execute_CBX cb imm notset )" |" execute (CBZ (cb,imm,notzero)) = ( execute_CBZ cb imm notzero )" |" execute (CJALR (cd1,cb,link)) = ( execute_CJALR cd1 cb link )" @@ -8671,7 +8675,7 @@ fun execute :: " ast \<Rightarrow>((register_value),(unit),(exception))monad " |" execute (CSC (cs,cb,rt,rd,offset,conditional)) = ( execute_CSC cs cb rt rd offset conditional )" |" execute (CLC (cd1,cb,rt,offset,linked)) = ( execute_CLC cd1 cb rt offset linked )" |" execute (C2Dump (rt)) = ( return ((execute_C2Dump rt)))" -|" execute (RI (g__28)) = ( execute_RI g__28 )" +|" execute (RI (arg0)) = ( execute_RI arg0 )" (*val supported_instructions : ast -> maybe ast*) @@ -8695,16 +8699,16 @@ definition fetch_and_execute :: " unit \<Rightarrow>((register_value),(bool),(e (read_reg branchPending_ref :: ( 1 Word.word) M)) \<bind> (\<lambda> (w__1 :: 1 bits) . ((write_reg inBranchDelay_ref w__1 \<then> write_reg branchPending_ref (vec_of_bits [B0] :: 1 Word.word)) \<then> - (read_reg inBranchDelay_ref :: ( 1 Word.word) M)) \<bind> (\<lambda> (w__2 :: 1 Word.word) . + (read_reg inBranchDelay_ref :: ( 1 Word.word) M)) \<bind> (\<lambda> (w__2 :: 1 bits) . (if ((bits_to_bool w__2)) then (read_reg delayedPC_ref :: ( 64 Word.word) M) else - (read_reg PC_ref :: ( 64 Word.word) M) \<bind> (\<lambda> (w__4 :: 64 Word.word) . + (read_reg PC_ref :: ( 64 Word.word) M) \<bind> (\<lambda> (w__4 :: 64 bits) . return ((add_vec_int w__4 (( 4 :: int)::ii) :: 64 Word.word)))) \<bind> (\<lambda> (w__5 :: 64 Word.word) . ((write_reg nextPC_ref w__5 \<then> cp2_next_pc () ) \<then> read_reg instCount_ref) \<bind> (\<lambda> (w__6 :: ii) . (write_reg instCount_ref ((w__6 + (( 1 :: int)::ii))) \<then> - (read_reg UART_WRITTEN_ref :: ( 1 Word.word) M)) \<bind> (\<lambda> (w__7 :: 1 Word.word) . + (read_reg UART_WRITTEN_ref :: ( 1 Word.word) M)) \<bind> (\<lambda> (w__7 :: 1 bits) . (((if ((bits_to_bool w__7)) then (read_reg UART_WDATA_ref :: ( 8 Word.word) M) \<bind> (\<lambda> (w__8 :: 8 bits) . (let (_ :: unit) = (putchar ((Word.uint w__8))) in @@ -8713,7 +8717,7 @@ definition fetch_and_execute :: " unit \<Rightarrow>((register_value),(bool),(e skip () ) \<then> skip () ) \<then> ((let loop_again = True in - try_catch ((read_reg PC_ref :: ( 64 Word.word) M) \<bind> (\<lambda> (w__9 :: 64 Word.word) . + try_catch ((read_reg PC_ref :: ( 64 Word.word) M) \<bind> (\<lambda> (w__9 :: 64 bits) . (TranslatePC w__9 :: ( 64 Word.word) M) \<bind> (\<lambda> pc_pa . (MEMr_wrapper (( 32 :: int)::ii) pc_pa (( 4 :: int)::ii) :: ( 32 Word.word) M) \<bind> (\<lambda> instr . (let instr_ast = (decode instr) in @@ -8750,9 +8754,9 @@ definition dump_mips_state :: " unit \<Rightarrow>((register_value),(unit),(exc 64 Word.word) . return ((let _ = (print_endline - (((op@) (''DEBUG MIPS REG '') - (((op@) ((string_of_int - instance_Show_Show_Num_integer_dict idx)) (((op@) ('' '') ((string_of_bits w__1))))))))) in + (((@) (''DEBUG MIPS REG '') + (((@) ((string_of_int + instance_Show_Show_Num_integer_dict idx)) (((@) ('' '') ((string_of_bits w__1))))))))) in () ))))))))" @@ -8782,19 +8786,19 @@ definition main :: " unit \<Rightarrow>((register_value),(unit),(exception))mon definition initialize_registers :: " unit \<Rightarrow>((register_value),(unit),(exception))monad " where " initialize_registers _ = ( (undefined_bitvector - instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 64 :: int)::ii) :: ( 64 Word.word) M) \<bind> (\<lambda> (w__0 :: 64 bits) . + instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 64 :: int)::ii) :: ( 64 Word.word) M) \<bind> (\<lambda> (w__0 :: 64 Word.word) . (write_reg PC_ref w__0 \<then> (undefined_bitvector - instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 64 :: int)::ii) :: ( 64 Word.word) M)) \<bind> (\<lambda> (w__1 :: 64 bits) . + instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 64 :: int)::ii) :: ( 64 Word.word) M)) \<bind> (\<lambda> (w__1 :: 64 Word.word) . (write_reg nextPC_ref w__1 \<then> (undefined_bitvector - instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 1 :: int)::ii) :: ( 1 Word.word) M)) \<bind> (\<lambda> (w__2 :: 1 bits) . + instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 1 :: int)::ii) :: ( 1 Word.word) M)) \<bind> (\<lambda> (w__2 :: 1 Word.word) . (write_reg TLBProbe_ref w__2 \<then> (undefined_bitvector - instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 6 :: int)::ii) :: ( 6 Word.word) M)) \<bind> (\<lambda> (w__3 :: TLBIndexT) . + instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 6 :: int)::ii) :: ( 6 Word.word) M)) \<bind> (\<lambda> (w__3 :: 6 Word.word) . (write_reg TLBIndex_ref w__3 \<then> (undefined_bitvector - instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 6 :: int)::ii) :: ( 6 Word.word) M)) \<bind> (\<lambda> (w__4 :: TLBIndexT) . + instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 6 :: int)::ii) :: ( 6 Word.word) M)) \<bind> (\<lambda> (w__4 :: 6 Word.word) . (write_reg TLBRandom_ref w__4 \<then> undefined_TLBEntryLoReg () ) \<bind> (\<lambda> (w__5 :: TLBEntryLoReg) . (write_reg TLBEntryLo0_ref w__5 \<then> @@ -8803,10 +8807,10 @@ definition initialize_registers :: " unit \<Rightarrow>((register_value),(unit) undefined_ContextReg () ) \<bind> (\<lambda> (w__7 :: ContextReg) . (write_reg TLBContext_ref w__7 \<then> (undefined_bitvector - instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 16 :: int)::ii) :: ( 16 Word.word) M)) \<bind> (\<lambda> (w__8 :: 16 bits) . + instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 16 :: int)::ii) :: ( 16 Word.word) M)) \<bind> (\<lambda> (w__8 :: 16 Word.word) . (write_reg TLBPageMask_ref w__8 \<then> (undefined_bitvector - instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 6 :: int)::ii) :: ( 6 Word.word) M)) \<bind> (\<lambda> (w__9 :: TLBIndexT) . + instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 6 :: int)::ii) :: ( 6 Word.word) M)) \<bind> (\<lambda> (w__9 :: 6 Word.word) . (write_reg TLBWired_ref w__9 \<then> undefined_TLBEntryHiReg () ) \<bind> (\<lambda> (w__10 :: TLBEntryHiReg) . (write_reg TLBEntryHi_ref w__10 \<then> @@ -8941,198 +8945,198 @@ definition initialize_registers :: " unit \<Rightarrow>((register_value),(unit) undefined_TLBEntry () ) \<bind> (\<lambda> (w__75 :: TLBEntry) . (write_reg TLBEntry63_ref w__75 \<then> (undefined_bitvector - instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 32 :: int)::ii) :: ( 32 Word.word) M)) \<bind> (\<lambda> (w__76 :: 32 bits) . + instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 32 :: int)::ii) :: ( 32 Word.word) M)) \<bind> (\<lambda> (w__76 :: 32 Word.word) . (write_reg CP0Compare_ref w__76 \<then> undefined_CauseReg () ) \<bind> (\<lambda> (w__77 :: CauseReg) . (write_reg CP0Cause_ref w__77 \<then> (undefined_bitvector - instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 64 :: int)::ii) :: ( 64 Word.word) M)) \<bind> (\<lambda> (w__78 :: 64 bits) . + instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 64 :: int)::ii) :: ( 64 Word.word) M)) \<bind> (\<lambda> (w__78 :: 64 Word.word) . (write_reg CP0EPC_ref w__78 \<then> (undefined_bitvector - instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 64 :: int)::ii) :: ( 64 Word.word) M)) \<bind> (\<lambda> (w__79 :: 64 bits) . + instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 64 :: int)::ii) :: ( 64 Word.word) M)) \<bind> (\<lambda> (w__79 :: 64 Word.word) . (write_reg CP0ErrorEPC_ref w__79 \<then> (undefined_bitvector - instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 1 :: int)::ii) :: ( 1 Word.word) M)) \<bind> (\<lambda> (w__80 :: 1 bits) . + instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 1 :: int)::ii) :: ( 1 Word.word) M)) \<bind> (\<lambda> (w__80 :: 1 Word.word) . (write_reg CP0LLBit_ref w__80 \<then> (undefined_bitvector - instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 64 :: int)::ii) :: ( 64 Word.word) M)) \<bind> (\<lambda> (w__81 :: 64 bits) . + instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 64 :: int)::ii) :: ( 64 Word.word) M)) \<bind> (\<lambda> (w__81 :: 64 Word.word) . (write_reg CP0LLAddr_ref w__81 \<then> (undefined_bitvector - instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 64 :: int)::ii) :: ( 64 Word.word) M)) \<bind> (\<lambda> (w__82 :: 64 bits) . + instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 64 :: int)::ii) :: ( 64 Word.word) M)) \<bind> (\<lambda> (w__82 :: 64 Word.word) . (write_reg CP0BadVAddr_ref w__82 \<then> (undefined_bitvector - instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 32 :: int)::ii) :: ( 32 Word.word) M)) \<bind> (\<lambda> (w__83 :: 32 bits) . + instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 32 :: int)::ii) :: ( 32 Word.word) M)) \<bind> (\<lambda> (w__83 :: 32 Word.word) . (write_reg CP0Count_ref w__83 \<then> (undefined_bitvector - instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 32 :: int)::ii) :: ( 32 Word.word) M)) \<bind> (\<lambda> (w__84 :: 32 bits) . + instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 32 :: int)::ii) :: ( 32 Word.word) M)) \<bind> (\<lambda> (w__84 :: 32 Word.word) . (write_reg CP0HWREna_ref w__84 \<then> (undefined_bitvector - instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 64 :: int)::ii) :: ( 64 Word.word) M)) \<bind> (\<lambda> (w__85 :: 64 bits) . + instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 64 :: int)::ii) :: ( 64 Word.word) M)) \<bind> (\<lambda> (w__85 :: 64 Word.word) . (write_reg CP0UserLocal_ref w__85 \<then> (undefined_bitvector - instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 3 :: int)::ii) :: ( 3 Word.word) M)) \<bind> (\<lambda> (w__86 :: 3 bits) . + instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 3 :: int)::ii) :: ( 3 Word.word) M)) \<bind> (\<lambda> (w__86 :: 3 Word.word) . (write_reg CP0ConfigK0_ref w__86 \<then> undefined_StatusReg () ) \<bind> (\<lambda> (w__87 :: StatusReg) . (write_reg CP0Status_ref w__87 \<then> (undefined_bitvector - instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 1 :: int)::ii) :: ( 1 Word.word) M)) \<bind> (\<lambda> (w__88 :: 1 bits) . + instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 1 :: int)::ii) :: ( 1 Word.word) M)) \<bind> (\<lambda> (w__88 :: 1 Word.word) . (write_reg branchPending_ref w__88 \<then> (undefined_bitvector - instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 1 :: int)::ii) :: ( 1 Word.word) M)) \<bind> (\<lambda> (w__89 :: 1 bits) . + instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 1 :: int)::ii) :: ( 1 Word.word) M)) \<bind> (\<lambda> (w__89 :: 1 Word.word) . (write_reg inBranchDelay_ref w__89 \<then> (undefined_bitvector - instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 64 :: int)::ii) :: ( 64 Word.word) M)) \<bind> (\<lambda> (w__90 :: 64 bits) . + instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 64 :: int)::ii) :: ( 64 Word.word) M)) \<bind> (\<lambda> (w__90 :: 64 Word.word) . (write_reg delayedPC_ref w__90 \<then> (undefined_bitvector - instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 64 :: int)::ii) :: ( 64 Word.word) M)) \<bind> (\<lambda> (w__91 :: 64 bits) . + instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 64 :: int)::ii) :: ( 64 Word.word) M)) \<bind> (\<lambda> (w__91 :: 64 Word.word) . (write_reg HI_ref w__91 \<then> (undefined_bitvector - instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 64 :: int)::ii) :: ( 64 Word.word) M)) \<bind> (\<lambda> (w__92 :: 64 bits) . + instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 64 :: int)::ii) :: ( 64 Word.word) M)) \<bind> (\<lambda> (w__92 :: 64 Word.word) . (write_reg LO_ref w__92 \<then> (undefined_bitvector instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 64 :: int)::ii) :: ( 64 Word.word) M)) \<bind> (\<lambda> (w__93 :: 64 Word.word) . - (undefined_vector (( 32 :: int)::ii) w__93 :: ( ( 64 Word.word)list) M) \<bind> (\<lambda> (w__94 :: ( 64 bits) list) . + (undefined_vector (( 32 :: int)::ii) w__93 :: ( ( 64 Word.word)list) M) \<bind> (\<lambda> (w__94 :: ( 64 Word.word) list) . (write_reg GPR_ref w__94 \<then> (undefined_bitvector - instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 8 :: int)::ii) :: ( 8 Word.word) M)) \<bind> (\<lambda> (w__95 :: 8 bits) . + instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 8 :: int)::ii) :: ( 8 Word.word) M)) \<bind> (\<lambda> (w__95 :: 8 Word.word) . (write_reg UART_WDATA_ref w__95 \<then> (undefined_bitvector - instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 1 :: int)::ii) :: ( 1 Word.word) M)) \<bind> (\<lambda> (w__96 :: 1 bits) . + instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 1 :: int)::ii) :: ( 1 Word.word) M)) \<bind> (\<lambda> (w__96 :: 1 Word.word) . (write_reg UART_WRITTEN_ref w__96 \<then> (undefined_bitvector - instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 8 :: int)::ii) :: ( 8 Word.word) M)) \<bind> (\<lambda> (w__97 :: 8 bits) . + instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 8 :: int)::ii) :: ( 8 Word.word) M)) \<bind> (\<lambda> (w__97 :: 8 Word.word) . (write_reg UART_RDATA_ref w__97 \<then> (undefined_bitvector - instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 1 :: int)::ii) :: ( 1 Word.word) M)) \<bind> (\<lambda> (w__98 :: 1 bits) . + instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 1 :: int)::ii) :: ( 1 Word.word) M)) \<bind> (\<lambda> (w__98 :: 1 Word.word) . (write_reg UART_RVALID_ref w__98 \<then> (undefined_bitvector - instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 257 :: int)::ii) :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__99 :: CapReg) . + instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 257 :: int)::ii) :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__99 :: 257 Word.word) . (write_reg PCC_ref w__99 \<then> (undefined_bitvector - instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 257 :: int)::ii) :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__100 :: CapReg) . + instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 257 :: int)::ii) :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__100 :: 257 Word.word) . (write_reg nextPCC_ref w__100 \<then> (undefined_bitvector - instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 257 :: int)::ii) :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__101 :: CapReg) . + instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 257 :: int)::ii) :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__101 :: 257 Word.word) . (write_reg delayedPCC_ref w__101 \<then> (undefined_bitvector - instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 1 :: int)::ii) :: ( 1 Word.word) M)) \<bind> (\<lambda> (w__102 :: 1 bits) . + instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 1 :: int)::ii) :: ( 1 Word.word) M)) \<bind> (\<lambda> (w__102 :: 1 Word.word) . (write_reg inCCallDelay_ref w__102 \<then> (undefined_bitvector - instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 257 :: int)::ii) :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__103 :: CapReg) . + instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 257 :: int)::ii) :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__103 :: 257 Word.word) . (write_reg DDC_ref w__103 \<then> (undefined_bitvector - instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 257 :: int)::ii) :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__104 :: CapReg) . + instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 257 :: int)::ii) :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__104 :: 257 Word.word) . (write_reg C01_ref w__104 \<then> (undefined_bitvector - instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 257 :: int)::ii) :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__105 :: CapReg) . + instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 257 :: int)::ii) :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__105 :: 257 Word.word) . (write_reg C02_ref w__105 \<then> (undefined_bitvector - instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 257 :: int)::ii) :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__106 :: CapReg) . + instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 257 :: int)::ii) :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__106 :: 257 Word.word) . (write_reg C03_ref w__106 \<then> (undefined_bitvector - instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 257 :: int)::ii) :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__107 :: CapReg) . + instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 257 :: int)::ii) :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__107 :: 257 Word.word) . (write_reg C04_ref w__107 \<then> (undefined_bitvector - instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 257 :: int)::ii) :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__108 :: CapReg) . + instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 257 :: int)::ii) :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__108 :: 257 Word.word) . (write_reg C05_ref w__108 \<then> (undefined_bitvector - instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 257 :: int)::ii) :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__109 :: CapReg) . + instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 257 :: int)::ii) :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__109 :: 257 Word.word) . (write_reg C06_ref w__109 \<then> (undefined_bitvector - instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 257 :: int)::ii) :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__110 :: CapReg) . + instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 257 :: int)::ii) :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__110 :: 257 Word.word) . (write_reg C07_ref w__110 \<then> (undefined_bitvector - instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 257 :: int)::ii) :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__111 :: CapReg) . + instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 257 :: int)::ii) :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__111 :: 257 Word.word) . (write_reg C08_ref w__111 \<then> (undefined_bitvector - instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 257 :: int)::ii) :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__112 :: CapReg) . + instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 257 :: int)::ii) :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__112 :: 257 Word.word) . (write_reg C09_ref w__112 \<then> (undefined_bitvector - instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 257 :: int)::ii) :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__113 :: CapReg) . + instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 257 :: int)::ii) :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__113 :: 257 Word.word) . (write_reg C10_ref w__113 \<then> (undefined_bitvector - instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 257 :: int)::ii) :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__114 :: CapReg) . + instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 257 :: int)::ii) :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__114 :: 257 Word.word) . (write_reg C11_ref w__114 \<then> (undefined_bitvector - instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 257 :: int)::ii) :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__115 :: CapReg) . + instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 257 :: int)::ii) :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__115 :: 257 Word.word) . (write_reg C12_ref w__115 \<then> (undefined_bitvector - instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 257 :: int)::ii) :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__116 :: CapReg) . + instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 257 :: int)::ii) :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__116 :: 257 Word.word) . (write_reg C13_ref w__116 \<then> (undefined_bitvector - instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 257 :: int)::ii) :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__117 :: CapReg) . + instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 257 :: int)::ii) :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__117 :: 257 Word.word) . (write_reg C14_ref w__117 \<then> (undefined_bitvector - instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 257 :: int)::ii) :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__118 :: CapReg) . + instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 257 :: int)::ii) :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__118 :: 257 Word.word) . (write_reg C15_ref w__118 \<then> (undefined_bitvector - instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 257 :: int)::ii) :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__119 :: CapReg) . + instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 257 :: int)::ii) :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__119 :: 257 Word.word) . (write_reg C16_ref w__119 \<then> (undefined_bitvector - instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 257 :: int)::ii) :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__120 :: CapReg) . + instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 257 :: int)::ii) :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__120 :: 257 Word.word) . (write_reg C17_ref w__120 \<then> (undefined_bitvector - instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 257 :: int)::ii) :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__121 :: CapReg) . + instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 257 :: int)::ii) :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__121 :: 257 Word.word) . (write_reg C18_ref w__121 \<then> (undefined_bitvector - instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 257 :: int)::ii) :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__122 :: CapReg) . + instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 257 :: int)::ii) :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__122 :: 257 Word.word) . (write_reg C19_ref w__122 \<then> (undefined_bitvector - instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 257 :: int)::ii) :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__123 :: CapReg) . + instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 257 :: int)::ii) :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__123 :: 257 Word.word) . (write_reg C20_ref w__123 \<then> (undefined_bitvector - instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 257 :: int)::ii) :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__124 :: CapReg) . + instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 257 :: int)::ii) :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__124 :: 257 Word.word) . (write_reg C21_ref w__124 \<then> (undefined_bitvector - instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 257 :: int)::ii) :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__125 :: CapReg) . + instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 257 :: int)::ii) :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__125 :: 257 Word.word) . (write_reg C22_ref w__125 \<then> (undefined_bitvector - instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 257 :: int)::ii) :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__126 :: CapReg) . + instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 257 :: int)::ii) :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__126 :: 257 Word.word) . (write_reg C23_ref w__126 \<then> (undefined_bitvector - instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 257 :: int)::ii) :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__127 :: CapReg) . + instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 257 :: int)::ii) :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__127 :: 257 Word.word) . (write_reg C24_ref w__127 \<then> (undefined_bitvector - instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 257 :: int)::ii) :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__128 :: CapReg) . + instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 257 :: int)::ii) :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__128 :: 257 Word.word) . (write_reg C25_ref w__128 \<then> (undefined_bitvector - instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 257 :: int)::ii) :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__129 :: CapReg) . + instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 257 :: int)::ii) :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__129 :: 257 Word.word) . (write_reg C26_ref w__129 \<then> (undefined_bitvector - instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 257 :: int)::ii) :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__130 :: CapReg) . + instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 257 :: int)::ii) :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__130 :: 257 Word.word) . (write_reg C27_ref w__130 \<then> (undefined_bitvector - instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 257 :: int)::ii) :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__131 :: CapReg) . + instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 257 :: int)::ii) :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__131 :: 257 Word.word) . (write_reg C28_ref w__131 \<then> (undefined_bitvector - instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 257 :: int)::ii) :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__132 :: CapReg) . + instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 257 :: int)::ii) :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__132 :: 257 Word.word) . (write_reg C29_ref w__132 \<then> (undefined_bitvector - instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 257 :: int)::ii) :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__133 :: CapReg) . + instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 257 :: int)::ii) :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__133 :: 257 Word.word) . (write_reg C30_ref w__133 \<then> (undefined_bitvector - instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 257 :: int)::ii) :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__134 :: CapReg) . + instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 257 :: int)::ii) :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__134 :: 257 Word.word) . (write_reg C31_ref w__134 \<then> (undefined_bitvector - instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 257 :: int)::ii) :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__135 :: CapReg) . + instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 257 :: int)::ii) :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__135 :: 257 Word.word) . (write_reg CTLSU_ref w__135 \<then> (undefined_bitvector - instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 257 :: int)::ii) :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__136 :: CapReg) . + instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 257 :: int)::ii) :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__136 :: 257 Word.word) . (write_reg CTLSP_ref w__136 \<then> (undefined_bitvector - instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 257 :: int)::ii) :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__137 :: CapReg) . + instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 257 :: int)::ii) :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__137 :: 257 Word.word) . (write_reg KR1C_ref w__137 \<then> (undefined_bitvector - instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 257 :: int)::ii) :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__138 :: CapReg) . + instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 257 :: int)::ii) :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__138 :: 257 Word.word) . (write_reg KR2C_ref w__138 \<then> (undefined_bitvector - instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 257 :: int)::ii) :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__139 :: CapReg) . + instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 257 :: int)::ii) :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__139 :: 257 Word.word) . (write_reg KCC_ref w__139 \<then> (undefined_bitvector - instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 257 :: int)::ii) :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__140 :: CapReg) . + instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 257 :: int)::ii) :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__140 :: 257 Word.word) . (write_reg KDC_ref w__140 \<then> (undefined_bitvector - instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 257 :: int)::ii) :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__141 :: CapReg) . + instance_Sail2_values_Bitvector_Machine_word_mword_dict (( 257 :: int)::ii) :: ( 257 Word.word) M)) \<bind> (\<lambda> (w__141 :: 257 Word.word) . (write_reg EPCC_ref w__141 \<then> undefined_CapCauseReg () ) \<bind> (\<lambda> (w__142 :: CapCauseReg) . (write_reg CapCause_ref w__142 \<then> |