path: root/aarch64/duopod/aarch64_duopod.lem

(*Generated by Sail from aarch64_duopod.*)
open import Pervasives_extra
open import Sail_instr_kinds
open import Sail_values
open import Sail_operators_bitlists
open import Prompt_monad
open import Prompt
open import State
open import Aarch64_duopod_types
open import Aarch64_extras_embed_sequential



val vcons : forall  'a. 'a -> list 'a -> list 'a







val builtin_and_vec : forall 'n. bits 'n -> bits 'n -> bits 'n



val builtin_or_vec : forall 'n. bits 'n -> bits 'n -> bits 'n



val __raw_SetSlice_int : forall 'w. integer -> ii -> ii -> bits 'w -> ii

val __GetSlice_int : integer -> ii -> ii -> list bitU

let __GetSlice_int n m o = (get_slice_int n m o : list bitU)

val __raw_SetSlice_bits : forall 'n 'w. integer -> integer -> bits 'n -> ii -> bits 'w -> bits 'n

val __raw_GetSlice_bits : forall 'n 'w. integer -> integer -> bits 'n -> ii -> bits 'w

val cast_unit_vec : bitU -> list bitU

let cast_unit_vec b = match b with | B0 -> [B0] | B1 -> [B1] end

val DecStr : ii -> string

val HexStr : ii -> string

val __TraceMemoryWrite : forall 'int8_times_n 'm. integer -> bits 'm -> bits 'int8_times_n -> unit

val __InitRAM : integer -> ii -> list bitU -> list bitU -> unit

let __InitRAM g__289 g__290 g__291 g__292 = ()

val __TraceMemoryRead : forall 'int8_times_n 'm. integer -> bits 'm -> bits 'int8_times_n -> unit

val ex_nat : ii -> integer

let ex_nat n = n

val ex_int : ii -> integer

let ex_int n = n

val ex_range : integer -> integer

val coerce_int_nat : ii -> M ii

let coerce_int_nat x =
   assert_exp true "Cannot coerce int to nat" >>
   return x

val break : unit -> unit

let break () = ()

val undefined_exception : unit -> exception

let undefined_exception () =
   internal_pick
     [Error_Undefined;Error_See (undefined_string ());Error_Implementation_Defined (undefined_string
                                                                                      ());Error_ReservedEncoding]

val boolean_of_num : integer -> boolean

let boolean_of_num arg_ =
   let l__280 = arg_ in
   if (eq l__280 (0:ii))
   then FALSE
   else TRUE

val num_of_boolean : boolean -> integer

let num_of_boolean arg_ = match arg_ with | FALSE -> (0:ii) | TRUE -> (1:ii) end

val undefined_boolean : unit -> boolean

let undefined_boolean () = internal_pick [FALSE;TRUE]

val signal_of_num : integer -> signal

let signal_of_num arg_ =
   let l__279 = arg_ in
   if (eq l__279 (0:ii))
   then LOW
   else HIGH

val num_of_signal : signal -> integer

let num_of_signal arg_ = match arg_ with | LOW -> (0:ii) | HIGH -> (1:ii) end

val undefined_signal : unit -> signal

let undefined_signal () = internal_pick [LOW;HIGH]

val __RetCode_of_num : integer -> __RetCode

let __RetCode_of_num arg_ =
   let l__271 = arg_ in
   if (eq l__271 (0:ii))
   then __RC_OK
   else
   if (eq l__271 (1:ii))
   then __RC_UNDEFINED
   else
   if (eq l__271 (2:ii))
   then __RC_UNPREDICTABLE
   else
   if (eq l__271 (3:ii))
   then __RC_SEE
   else
   if (eq l__271 (4:ii))
   then __RC_IMPLEMENTATION_DEFINED
   else
   if (eq l__271 (5:ii))
   then __RC_SUBARCHITECTURE_DEFINED
   else
   if (eq l__271 (6:ii))
   then __RC_EXCEPTION_TAKEN
   else if (eq l__271 (7:ii)) then __RC_ASSERT_FAILED else __RC_UNMATCHED_CASE

val num_of___RetCode : __RetCode -> integer

let num_of___RetCode arg_ =
   match arg_ with
   | __RC_OK -> (0:ii)
   | __RC_UNDEFINED -> (1:ii)
   | __RC_UNPREDICTABLE -> (2:ii)
   | __RC_SEE -> (3:ii)
   | __RC_IMPLEMENTATION_DEFINED -> (4:ii)
   | __RC_SUBARCHITECTURE_DEFINED -> (5:ii)
   | __RC_EXCEPTION_TAKEN -> (6:ii)
   | __RC_ASSERT_FAILED -> (7:ii)
   | __RC_UNMATCHED_CASE -> (8:ii)
   end

val undefined___RetCode : unit -> __RetCode

let undefined___RetCode () =
   internal_pick
     [__RC_OK;__RC_UNDEFINED;__RC_UNPREDICTABLE;__RC_SEE;__RC_IMPLEMENTATION_DEFINED;__RC_SUBARCHITECTURE_DEFINED;__RC_EXCEPTION_TAKEN;__RC_ASSERT_FAILED;__RC_UNMATCHED_CASE]

val FPConvOp_of_num : integer -> FPConvOp

let FPConvOp_of_num arg_ =
   let l__267 = arg_ in
   if (eq l__267 (0:ii))
   then FPConvOp_CVT_FtoI
   else
   if (eq l__267 (1:ii))
   then FPConvOp_CVT_ItoF
   else
   if (eq l__267 (2:ii))
   then FPConvOp_MOV_FtoI
   else if (eq l__267 (3:ii)) then FPConvOp_MOV_ItoF else FPConvOp_CVT_FtoI_JS

val num_of_FPConvOp : FPConvOp -> integer

let num_of_FPConvOp arg_ =
   match arg_ with
   | FPConvOp_CVT_FtoI -> (0:ii)
   | FPConvOp_CVT_ItoF -> (1:ii)
   | FPConvOp_MOV_FtoI -> (2:ii)
   | FPConvOp_MOV_ItoF -> (3:ii)
   | FPConvOp_CVT_FtoI_JS -> (4:ii)
   end

val undefined_FPConvOp : unit -> FPConvOp

let undefined_FPConvOp () =
   internal_pick
     [FPConvOp_CVT_FtoI;FPConvOp_CVT_ItoF;FPConvOp_MOV_FtoI;FPConvOp_MOV_ItoF;FPConvOp_CVT_FtoI_JS]

val Exception_of_num : integer -> Exception

let Exception_of_num arg_ =
   let l__239 = arg_ in
   if (eq l__239 (0:ii))
   then Exception_Uncategorized
   else
   if (eq l__239 (1:ii))
   then Exception_WFxTrap
   else
   if (eq l__239 (2:ii))
   then Exception_CP15RTTrap
   else
   if (eq l__239 (3:ii))
   then Exception_CP15RRTTrap
   else
   if (eq l__239 (4:ii))
   then Exception_CP14RTTrap
   else
   if (eq l__239 (5:ii))
   then Exception_CP14DTTrap
   else
   if (eq l__239 (6:ii))
   then Exception_AdvSIMDFPAccessTrap
   else
   if (eq l__239 (7:ii))
   then Exception_FPIDTrap
   else
   if (eq l__239 (8:ii))
   then Exception_PACTrap
   else
   if (eq l__239 (9:ii))
   then Exception_CP14RRTTrap
   else
   if (eq l__239 (10:ii))
   then Exception_IllegalState
   else
   if (eq l__239 (11:ii))
   then Exception_SupervisorCall
   else
   if (eq l__239 (12:ii))
   then Exception_HypervisorCall
   else
   if (eq l__239 (13:ii))
   then Exception_MonitorCall
   else
   if (eq l__239 (14:ii))
   then Exception_SystemRegisterTrap
   else
   if (eq l__239 (15:ii))
   then Exception_ERetTrap
   else
   if (eq l__239 (16:ii))
   then Exception_InstructionAbort
   else
   if (eq l__239 (17:ii))
   then Exception_PCAlignment
   else
   if (eq l__239 (18:ii))
   then Exception_DataAbort
   else
   if (eq l__239 (19:ii))
   then Exception_SPAlignment
   else
   if (eq l__239 (20:ii))
   then Exception_FPTrappedException
   else
   if (eq l__239 (21:ii))
   then Exception_SError
   else
   if (eq l__239 (22:ii))
   then Exception_Breakpoint
   else
   if (eq l__239 (23:ii))
   then Exception_SoftwareStep
   else
   if (eq l__239 (24:ii))
   then Exception_Watchpoint
   else
   if (eq l__239 (25:ii))
   then Exception_SoftwareBreakpoint
   else
   if (eq l__239 (26:ii))
   then Exception_VectorCatch
   else if (eq l__239 (27:ii)) then Exception_IRQ else Exception_FIQ

val num_of_Exception : Exception -> integer

let num_of_Exception arg_ =
   match arg_ with
   | Exception_Uncategorized -> (0:ii)
   | Exception_WFxTrap -> (1:ii)
   | Exception_CP15RTTrap -> (2:ii)
   | Exception_CP15RRTTrap -> (3:ii)
   | Exception_CP14RTTrap -> (4:ii)
   | Exception_CP14DTTrap -> (5:ii)
   | Exception_AdvSIMDFPAccessTrap -> (6:ii)
   | Exception_FPIDTrap -> (7:ii)
   | Exception_PACTrap -> (8:ii)
   | Exception_CP14RRTTrap -> (9:ii)
   | Exception_IllegalState -> (10:ii)
   | Exception_SupervisorCall -> (11:ii)
   | Exception_HypervisorCall -> (12:ii)
   | Exception_MonitorCall -> (13:ii)
   | Exception_SystemRegisterTrap -> (14:ii)
   | Exception_ERetTrap -> (15:ii)
   | Exception_InstructionAbort -> (16:ii)
   | Exception_PCAlignment -> (17:ii)
   | Exception_DataAbort -> (18:ii)
   | Exception_SPAlignment -> (19:ii)
   | Exception_FPTrappedException -> (20:ii)
   | Exception_SError -> (21:ii)
   | Exception_Breakpoint -> (22:ii)
   | Exception_SoftwareStep -> (23:ii)
   | Exception_Watchpoint -> (24:ii)
   | Exception_SoftwareBreakpoint -> (25:ii)
   | Exception_VectorCatch -> (26:ii)
   | Exception_IRQ -> (27:ii)
   | Exception_FIQ -> (28:ii)
   end

val undefined_Exception : unit -> Exception

let undefined_Exception () =
   internal_pick
     [Exception_Uncategorized;Exception_WFxTrap;Exception_CP15RTTrap;Exception_CP15RRTTrap;Exception_CP14RTTrap;Exception_CP14DTTrap;Exception_AdvSIMDFPAccessTrap;Exception_FPIDTrap;Exception_PACTrap;Exception_CP14RRTTrap;Exception_IllegalState;Exception_SupervisorCall;Exception_HypervisorCall;Exception_MonitorCall;Exception_SystemRegisterTrap;Exception_ERetTrap;Exception_InstructionAbort;Exception_PCAlignment;Exception_DataAbort;Exception_SPAlignment;Exception_FPTrappedException;Exception_SError;Exception_Breakpoint;Exception_SoftwareStep;Exception_Watchpoint;Exception_SoftwareBreakpoint;Exception_VectorCatch;Exception_IRQ;Exception_FIQ]

val ArchVersion_of_num : integer -> ArchVersion

let ArchVersion_of_num arg_ =
   let l__236 = arg_ in
   if (eq l__236 (0:ii))
   then ARMv8p0
   else if (eq l__236 (1:ii)) then ARMv8p1 else if (eq l__236 (2:ii)) then ARMv8p2 else ARMv8p3

val num_of_ArchVersion : ArchVersion -> integer

let num_of_ArchVersion arg_ =
   match arg_ with
   | ARMv8p0 -> (0:ii)
   | ARMv8p1 -> (1:ii)
   | ARMv8p2 -> (2:ii)
   | ARMv8p3 -> (3:ii)
   end

val undefined_ArchVersion : unit -> ArchVersion

let undefined_ArchVersion () = internal_pick [ARMv8p0;ARMv8p1;ARMv8p2;ARMv8p3]

val Unpredictable_of_num : integer -> Unpredictable

let Unpredictable_of_num arg_ =
   let l__192 = arg_ in
   if (eq l__192 (0:ii))
   then Unpredictable_WBOVERLAPLD
   else
   if (eq l__192 (1:ii))
   then Unpredictable_WBOVERLAPST
   else
   if (eq l__192 (2:ii))
   then Unpredictable_LDPOVERLAP
   else
   if (eq l__192 (3:ii))
   then Unpredictable_BASEOVERLAP
   else
   if (eq l__192 (4:ii))
   then Unpredictable_DATAOVERLAP
   else
   if (eq l__192 (5:ii))
   then Unpredictable_DEVPAGE2
   else
   if (eq l__192 (6:ii))
   then Unpredictable_INSTRDEVICE
   else
   if (eq l__192 (7:ii))
   then Unpredictable_RESCPACR
   else
   if (eq l__192 (8:ii))
   then Unpredictable_RESMAIR
   else
   if (eq l__192 (9:ii))
   then Unpredictable_RESTEXCB
   else
   if (eq l__192 (10:ii))
   then Unpredictable_RESPRRR
   else
   if (eq l__192 (11:ii))
   then Unpredictable_RESDACR
   else
   if (eq l__192 (12:ii))
   then Unpredictable_RESVTCRS
   else
   if (eq l__192 (13:ii))
   then Unpredictable_RESTnSZ
   else
   if (eq l__192 (14:ii))
   then Unpredictable_OORTnSZ
   else
   if (eq l__192 (15:ii))
   then Unpredictable_LARGEIPA
   else
   if (eq l__192 (16:ii))
   then Unpredictable_ESRCONDPASS
   else
   if (eq l__192 (17:ii))
   then Unpredictable_ILZEROIT
   else
   if (eq l__192 (18:ii))
   then Unpredictable_ILZEROT
   else
   if (eq l__192 (19:ii))
   then Unpredictable_BPVECTORCATCHPRI
   else
   if (eq l__192 (20:ii))
   then Unpredictable_VCMATCHHALF
   else
   if (eq l__192 (21:ii))
   then Unpredictable_VCMATCHDAPA
   else
   if (eq l__192 (22:ii))
   then Unpredictable_WPMASKANDBAS
   else
   if (eq l__192 (23:ii))
   then Unpredictable_WPBASCONTIGUOUS
   else
   if (eq l__192 (24:ii))
   then Unpredictable_RESWPMASK
   else
   if (eq l__192 (25:ii))
   then Unpredictable_WPMASKEDBITS
   else
   if (eq l__192 (26:ii))
   then Unpredictable_RESBPWPCTRL
   else
   if (eq l__192 (27:ii))
   then Unpredictable_BPNOTIMPL
   else
   if (eq l__192 (28:ii))
   then Unpredictable_RESBPTYPE
   else
   if (eq l__192 (29:ii))
   then Unpredictable_BPNOTCTXCMP
   else
   if (eq l__192 (30:ii))
   then Unpredictable_BPMATCHHALF
   else
   if (eq l__192 (31:ii))
   then Unpredictable_BPMISMATCHHALF
   else
   if (eq l__192 (32:ii))
   then Unpredictable_RESTARTALIGNPC
   else
   if (eq l__192 (33:ii))
   then Unpredictable_RESTARTZEROUPPERPC
   else
   if (eq l__192 (34:ii))
   then Unpredictable_ZEROUPPER
   else
   if (eq l__192 (35:ii))
   then Unpredictable_ERETZEROUPPERPC
   else
   if (eq l__192 (36:ii))
   then Unpredictable_A32FORCEALIGNPC
   else
   if (eq l__192 (37:ii))
   then Unpredictable_SMD
   else
   if (eq l__192 (38:ii))
   then Unpredictable_AFUPDATE
   else
   if (eq l__192 (39:ii))
   then Unpredictable_IESBinDebug
   else
   if (eq l__192 (40:ii))
   then Unpredictable_ZEROPMSEVFR
   else
   if (eq l__192 (41:ii))
   then Unpredictable_NOOPTYPES
   else
   if (eq l__192 (42:ii))
   then Unpredictable_ZEROMINLATENCY
   else if (eq l__192 (43:ii)) then Unpredictable_CLEARERRITEZERO else Unpredictable_TBD

val num_of_Unpredictable : Unpredictable -> integer

let num_of_Unpredictable arg_ =
   match arg_ with
   | Unpredictable_WBOVERLAPLD -> (0:ii)
   | Unpredictable_WBOVERLAPST -> (1:ii)
   | Unpredictable_LDPOVERLAP -> (2:ii)
   | Unpredictable_BASEOVERLAP -> (3:ii)
   | Unpredictable_DATAOVERLAP -> (4:ii)
   | Unpredictable_DEVPAGE2 -> (5:ii)
   | Unpredictable_INSTRDEVICE -> (6:ii)
   | Unpredictable_RESCPACR -> (7:ii)
   | Unpredictable_RESMAIR -> (8:ii)
   | Unpredictable_RESTEXCB -> (9:ii)
   | Unpredictable_RESPRRR -> (10:ii)
   | Unpredictable_RESDACR -> (11:ii)
   | Unpredictable_RESVTCRS -> (12:ii)
   | Unpredictable_RESTnSZ -> (13:ii)
   | Unpredictable_OORTnSZ -> (14:ii)
   | Unpredictable_LARGEIPA -> (15:ii)
   | Unpredictable_ESRCONDPASS -> (16:ii)
   | Unpredictable_ILZEROIT -> (17:ii)
   | Unpredictable_ILZEROT -> (18:ii)
   | Unpredictable_BPVECTORCATCHPRI -> (19:ii)
   | Unpredictable_VCMATCHHALF -> (20:ii)
   | Unpredictable_VCMATCHDAPA -> (21:ii)
   | Unpredictable_WPMASKANDBAS -> (22:ii)
   | Unpredictable_WPBASCONTIGUOUS -> (23:ii)
   | Unpredictable_RESWPMASK -> (24:ii)
   | Unpredictable_WPMASKEDBITS -> (25:ii)
   | Unpredictable_RESBPWPCTRL -> (26:ii)
   | Unpredictable_BPNOTIMPL -> (27:ii)
   | Unpredictable_RESBPTYPE -> (28:ii)
   | Unpredictable_BPNOTCTXCMP -> (29:ii)
   | Unpredictable_BPMATCHHALF -> (30:ii)
   | Unpredictable_BPMISMATCHHALF -> (31:ii)
   | Unpredictable_RESTARTALIGNPC -> (32:ii)
   | Unpredictable_RESTARTZEROUPPERPC -> (33:ii)
   | Unpredictable_ZEROUPPER -> (34:ii)
   | Unpredictable_ERETZEROUPPERPC -> (35:ii)
   | Unpredictable_A32FORCEALIGNPC -> (36:ii)
   | Unpredictable_SMD -> (37:ii)
   | Unpredictable_AFUPDATE -> (38:ii)
   | Unpredictable_IESBinDebug -> (39:ii)
   | Unpredictable_ZEROPMSEVFR -> (40:ii)
   | Unpredictable_NOOPTYPES -> (41:ii)
   | Unpredictable_ZEROMINLATENCY -> (42:ii)
   | Unpredictable_CLEARERRITEZERO -> (43:ii)
   | Unpredictable_TBD -> (44:ii)
   end

val undefined_Unpredictable : unit -> Unpredictable

let undefined_Unpredictable () =
   internal_pick
     [Unpredictable_WBOVERLAPLD;Unpredictable_WBOVERLAPST;Unpredictable_LDPOVERLAP;Unpredictable_BASEOVERLAP;Unpredictable_DATAOVERLAP;Unpredictable_DEVPAGE2;Unpredictable_INSTRDEVICE;Unpredictable_RESCPACR;Unpredictable_RESMAIR;Unpredictable_RESTEXCB;Unpredictable_RESPRRR;Unpredictable_RESDACR;Unpredictable_RESVTCRS;Unpredictable_RESTnSZ;Unpredictable_OORTnSZ;Unpredictable_LARGEIPA;Unpredictable_ESRCONDPASS;Unpredictable_ILZEROIT;Unpredictable_ILZEROT;Unpredictable_BPVECTORCATCHPRI;Unpredictable_VCMATCHHALF;Unpredictable_VCMATCHDAPA;Unpredictable_WPMASKANDBAS;Unpredictable_WPBASCONTIGUOUS;Unpredictable_RESWPMASK;Unpredictable_WPMASKEDBITS;Unpredictable_RESBPWPCTRL;Unpredictable_BPNOTIMPL;Unpredictable_RESBPTYPE;Unpredictable_BPNOTCTXCMP;Unpredictable_BPMATCHHALF;Unpredictable_BPMISMATCHHALF;Unpredictable_RESTARTALIGNPC;Unpredictable_RESTARTZEROUPPERPC;Unpredictable_ZEROUPPER;Unpredictable_ERETZEROUPPERPC;Unpredictable_A32FORCEALIGNPC;Unpredictable_SMD;Unpredictable_AFUPDATE;Unpredictable_IESBinDebug;Unpredictable_ZEROPMSEVFR;Unpredictable_NOOPTYPES;Unpredictable_ZEROMINLATENCY;Unpredictable_CLEARERRITEZERO;Unpredictable_TBD]

val Constraint_of_num : integer -> Constraint

let Constraint_of_num arg_ =
   let l__178 = arg_ in
   if (eq l__178 (0:ii))
   then Constraint_NONE
   else
   if (eq l__178 (1:ii))
   then Constraint_UNKNOWN
   else
   if (eq l__178 (2:ii))
   then Constraint_UNDEF
   else
   if (eq l__178 (3:ii))
   then Constraint_UNDEFEL0
   else
   if (eq l__178 (4:ii))
   then Constraint_NOP
   else
   if (eq l__178 (5:ii))
   then Constraint_TRUE
   else
   if (eq l__178 (6:ii))
   then Constraint_FALSE
   else
   if (eq l__178 (7:ii))
   then Constraint_DISABLED
   else
   if (eq l__178 (8:ii))
   then Constraint_UNCOND
   else
   if (eq l__178 (9:ii))
   then Constraint_COND
   else
   if (eq l__178 (10:ii))
   then Constraint_ADDITIONAL_DECODE
   else
   if (eq l__178 (11:ii))
   then Constraint_WBSUPPRESS
   else
   if (eq l__178 (12:ii))
   then Constraint_FAULT
   else if (eq l__178 (13:ii)) then Constraint_FORCE else Constraint_FORCENOSLCHECK

val num_of_Constraint : Constraint -> integer

let num_of_Constraint arg_ =
   match arg_ with
   | Constraint_NONE -> (0:ii)
   | Constraint_UNKNOWN -> (1:ii)
   | Constraint_UNDEF -> (2:ii)
   | Constraint_UNDEFEL0 -> (3:ii)
   | Constraint_NOP -> (4:ii)
   | Constraint_TRUE -> (5:ii)
   | Constraint_FALSE -> (6:ii)
   | Constraint_DISABLED -> (7:ii)
   | Constraint_UNCOND -> (8:ii)
   | Constraint_COND -> (9:ii)
   | Constraint_ADDITIONAL_DECODE -> (10:ii)
   | Constraint_WBSUPPRESS -> (11:ii)
   | Constraint_FAULT -> (12:ii)
   | Constraint_FORCE -> (13:ii)
   | Constraint_FORCENOSLCHECK -> (14:ii)
   end

val undefined_Constraint : unit -> Constraint

let undefined_Constraint () =
   internal_pick
     [Constraint_NONE;Constraint_UNKNOWN;Constraint_UNDEF;Constraint_UNDEFEL0;Constraint_NOP;Constraint_TRUE;Constraint_FALSE;Constraint_DISABLED;Constraint_UNCOND;Constraint_COND;Constraint_ADDITIONAL_DECODE;Constraint_WBSUPPRESS;Constraint_FAULT;Constraint_FORCE;Constraint_FORCENOSLCHECK]

val InstrSet_of_num : integer -> InstrSet

let InstrSet_of_num arg_ =
   let l__176 = arg_ in
   if (eq l__176 (0:ii))
   then InstrSet_A64
   else if (eq l__176 (1:ii)) then InstrSet_A32 else InstrSet_T32

val num_of_InstrSet : InstrSet -> integer

let num_of_InstrSet arg_ =
   match arg_ with | InstrSet_A64 -> (0:ii) | InstrSet_A32 -> (1:ii) | InstrSet_T32 -> (2:ii) end

val undefined_InstrSet : unit -> InstrSet

let undefined_InstrSet () = internal_pick [InstrSet_A64;InstrSet_A32;InstrSet_T32]

val undefined_ProcState : unit -> ProcState

let undefined_ProcState () =
   <| ProcState_N = (undefined_vector (1:ii) (undefined_bit ()) : list bitU); 
      ProcState_Z = (undefined_vector (1:ii) (undefined_bit ()) : list bitU); 
      ProcState_C = (undefined_vector (1:ii) (undefined_bit ()) : list bitU); 
      ProcState_V = (undefined_vector (1:ii) (undefined_bit ()) : list bitU); 
      ProcState_D = (undefined_vector (1:ii) (undefined_bit ()) : list bitU); 
      ProcState_A = (undefined_vector (1:ii) (undefined_bit ()) : list bitU); 
      ProcState_I = (undefined_vector (1:ii) (undefined_bit ()) : list bitU); 
      ProcState_F = (undefined_vector (1:ii) (undefined_bit ()) : list bitU); 
      ProcState_PAN = (undefined_vector (1:ii) (undefined_bit ()) : list bitU); 
      ProcState_UAO = (undefined_vector (1:ii) (undefined_bit ()) : list bitU); 
      ProcState_SS = (undefined_vector (1:ii) (undefined_bit ()) : list bitU); 
      ProcState_IL = (undefined_vector (1:ii) (undefined_bit ()) : list bitU); 
      ProcState_EL = (undefined_vector (2:ii) (undefined_bit ()) : list bitU); 
      ProcState_nRW = (undefined_vector (1:ii) (undefined_bit ()) : list bitU); 
      ProcState_SP = (undefined_vector (1:ii) (undefined_bit ()) : list bitU); 
      ProcState_Q = (undefined_vector (1:ii) (undefined_bit ()) : list bitU); 
      ProcState_GE = (undefined_vector (4:ii) (undefined_bit ()) : list bitU); 
      ProcState_IT = (undefined_vector (8:ii) (undefined_bit ()) : list bitU); 
      ProcState_J = (undefined_vector (1:ii) (undefined_bit ()) : list bitU); 
      ProcState_T = (undefined_vector (1:ii) (undefined_bit ()) : list bitU); 
      ProcState_E = (undefined_vector (1:ii) (undefined_bit ()) : list bitU); 
      ProcState_M = (undefined_vector (5:ii) (undefined_bit ()) : list bitU) |>

val BranchType_of_num : integer -> BranchType

let BranchType_of_num arg_ =
   let l__170 = arg_ in
   if (eq l__170 (0:ii))
   then BranchType_CALL
   else
   if (eq l__170 (1:ii))
   then BranchType_ERET
   else
   if (eq l__170 (2:ii))
   then BranchType_DBGEXIT
   else
   if (eq l__170 (3:ii))
   then BranchType_RET
   else
   if (eq l__170 (4:ii))
   then BranchType_JMP
   else if (eq l__170 (5:ii)) then BranchType_EXCEPTION else BranchType_UNKNOWN

val num_of_BranchType : BranchType -> integer

let num_of_BranchType arg_ =
   match arg_ with
   | BranchType_CALL -> (0:ii)
   | BranchType_ERET -> (1:ii)
   | BranchType_DBGEXIT -> (2:ii)
   | BranchType_RET -> (3:ii)
   | BranchType_JMP -> (4:ii)
   | BranchType_EXCEPTION -> (5:ii)
   | BranchType_UNKNOWN -> (6:ii)
   end

val undefined_BranchType : unit -> BranchType

let undefined_BranchType () =
   internal_pick
     [BranchType_CALL;BranchType_ERET;BranchType_DBGEXIT;BranchType_RET;BranchType_JMP;BranchType_EXCEPTION;BranchType_UNKNOWN]

val undefined_ExceptionRecord : unit -> ExceptionRecord

let undefined_ExceptionRecord () =
   <| ExceptionRecord_typ = (undefined_Exception ()); 
      ExceptionRecord_syndrome = (undefined_vector (25:ii) (undefined_bit ()) : list bitU); 
      ExceptionRecord_vaddress = (undefined_vector (64:ii) (undefined_bit ()) : list bitU); 
      ExceptionRecord_ipavalid = (undefined_bool ()); 
      ExceptionRecord_ipaddress = (undefined_vector (52:ii) (undefined_bit ()) : list bitU) |>

val Fault_of_num : integer -> Fault

let Fault_of_num arg_ =
   let l__152 = arg_ in
   if (eq l__152 (0:ii))
   then Fault_None
   else
   if (eq l__152 (1:ii))
   then Fault_AccessFlag
   else
   if (eq l__152 (2:ii))
   then Fault_Alignment
   else
   if (eq l__152 (3:ii))
   then Fault_Background
   else
   if (eq l__152 (4:ii))
   then Fault_Domain
   else
   if (eq l__152 (5:ii))
   then Fault_Permission
   else
   if (eq l__152 (6:ii))
   then Fault_Translation
   else
   if (eq l__152 (7:ii))
   then Fault_AddressSize
   else
   if (eq l__152 (8:ii))
   then Fault_SyncExternal
   else
   if (eq l__152 (9:ii))
   then Fault_SyncExternalOnWalk
   else
   if (eq l__152 (10:ii))
   then Fault_SyncParity
   else
   if (eq l__152 (11:ii))
   then Fault_SyncParityOnWalk
   else
   if (eq l__152 (12:ii))
   then Fault_AsyncParity
   else
   if (eq l__152 (13:ii))
   then Fault_AsyncExternal
   else
   if (eq l__152 (14:ii))
   then Fault_Debug
   else
   if (eq l__152 (15:ii))
   then Fault_TLBConflict
   else
   if (eq l__152 (16:ii))
   then Fault_Lockdown
   else if (eq l__152 (17:ii)) then Fault_Exclusive else Fault_ICacheMaint

val num_of_Fault : Fault -> integer

let num_of_Fault arg_ =
   match arg_ with
   | Fault_None -> (0:ii)
   | Fault_AccessFlag -> (1:ii)
   | Fault_Alignment -> (2:ii)
   | Fault_Background -> (3:ii)
   | Fault_Domain -> (4:ii)
   | Fault_Permission -> (5:ii)
   | Fault_Translation -> (6:ii)
   | Fault_AddressSize -> (7:ii)
   | Fault_SyncExternal -> (8:ii)
   | Fault_SyncExternalOnWalk -> (9:ii)
   | Fault_SyncParity -> (10:ii)
   | Fault_SyncParityOnWalk -> (11:ii)
   | Fault_AsyncParity -> (12:ii)
   | Fault_AsyncExternal -> (13:ii)
   | Fault_Debug -> (14:ii)
   | Fault_TLBConflict -> (15:ii)
   | Fault_Lockdown -> (16:ii)
   | Fault_Exclusive -> (17:ii)
   | Fault_ICacheMaint -> (18:ii)
   end

val undefined_Fault : unit -> Fault

let undefined_Fault () =
   internal_pick
     [Fault_None;Fault_AccessFlag;Fault_Alignment;Fault_Background;Fault_Domain;Fault_Permission;Fault_Translation;Fault_AddressSize;Fault_SyncExternal;Fault_SyncExternalOnWalk;Fault_SyncParity;Fault_SyncParityOnWalk;Fault_AsyncParity;Fault_AsyncExternal;Fault_Debug;Fault_TLBConflict;Fault_Lockdown;Fault_Exclusive;Fault_ICacheMaint]

val AccType_of_num : integer -> AccType

let AccType_of_num arg_ =
   let l__137 = arg_ in
   if (eq l__137 (0:ii))
   then AccType_NORMAL
   else
   if (eq l__137 (1:ii))
   then AccType_VEC
   else
   if (eq l__137 (2:ii))
   then AccType_STREAM
   else
   if (eq l__137 (3:ii))
   then AccType_VECSTREAM
   else
   if (eq l__137 (4:ii))
   then AccType_ATOMIC
   else
   if (eq l__137 (5:ii))
   then AccType_ATOMICRW
   else
   if (eq l__137 (6:ii))
   then AccType_ORDERED
   else
   if (eq l__137 (7:ii))
   then AccType_ORDEREDRW
   else
   if (eq l__137 (8:ii))
   then AccType_LIMITEDORDERED
   else
   if (eq l__137 (9:ii))
   then AccType_UNPRIV
   else
   if (eq l__137 (10:ii))
   then AccType_IFETCH
   else
   if (eq l__137 (11:ii))
   then AccType_PTW
   else
   if (eq l__137 (12:ii))
   then AccType_DC
   else
   if (eq l__137 (13:ii))
   then AccType_IC
   else if (eq l__137 (14:ii)) then AccType_DCZVA else AccType_AT

val num_of_AccType : AccType -> integer

let num_of_AccType arg_ =
   match arg_ with
   | AccType_NORMAL -> (0:ii)
   | AccType_VEC -> (1:ii)
   | AccType_STREAM -> (2:ii)
   | AccType_VECSTREAM -> (3:ii)
   | AccType_ATOMIC -> (4:ii)
   | AccType_ATOMICRW -> (5:ii)
   | AccType_ORDERED -> (6:ii)
   | AccType_ORDEREDRW -> (7:ii)
   | AccType_LIMITEDORDERED -> (8:ii)
   | AccType_UNPRIV -> (9:ii)
   | AccType_IFETCH -> (10:ii)
   | AccType_PTW -> (11:ii)
   | AccType_DC -> (12:ii)
   | AccType_IC -> (13:ii)
   | AccType_DCZVA -> (14:ii)
   | AccType_AT -> (15:ii)
   end

val undefined_AccType : unit -> AccType

let undefined_AccType () =
   internal_pick
     [AccType_NORMAL;AccType_VEC;AccType_STREAM;AccType_VECSTREAM;AccType_ATOMIC;AccType_ATOMICRW;AccType_ORDERED;AccType_ORDEREDRW;AccType_LIMITEDORDERED;AccType_UNPRIV;AccType_IFETCH;AccType_PTW;AccType_DC;AccType_IC;AccType_DCZVA;AccType_AT]

val undefined_FaultRecord : unit -> FaultRecord

let undefined_FaultRecord () =
   <| FaultRecord_typ = (undefined_Fault ()); 
      FaultRecord_acctype = (undefined_AccType ()); 
      FaultRecord_ipaddress = (undefined_vector (52:ii) (undefined_bit ()) : list bitU); 
      FaultRecord_s2fs1walk = (undefined_bool ()); 
      FaultRecord_write = (undefined_bool ()); 
      FaultRecord_level = (undefined_int ()); 
      FaultRecord_extflag = (undefined_vector (1:ii) (undefined_bit ()) : list bitU); 
      FaultRecord_secondstage = (undefined_bool ()); 
      FaultRecord_domain = (undefined_vector (4:ii) (undefined_bit ()) : list bitU); 
      FaultRecord_errortype = (undefined_vector (2:ii) (undefined_bit ()) : list bitU); 
      FaultRecord_debugmoe = (undefined_vector (4:ii) (undefined_bit ()) : list bitU) |>

val MBReqDomain_of_num : integer -> MBReqDomain

let MBReqDomain_of_num arg_ =
   let l__134 = arg_ in
   if (eq l__134 (0:ii))
   then MBReqDomain_Nonshareable
   else
   if (eq l__134 (1:ii))
   then MBReqDomain_InnerShareable
   else if (eq l__134 (2:ii)) then MBReqDomain_OuterShareable else MBReqDomain_FullSystem

val num_of_MBReqDomain : MBReqDomain -> integer

let num_of_MBReqDomain arg_ =
   match arg_ with
   | MBReqDomain_Nonshareable -> (0:ii)
   | MBReqDomain_InnerShareable -> (1:ii)
   | MBReqDomain_OuterShareable -> (2:ii)
   | MBReqDomain_FullSystem -> (3:ii)
   end

val undefined_MBReqDomain : unit -> MBReqDomain

let undefined_MBReqDomain () =
   internal_pick
     [MBReqDomain_Nonshareable;MBReqDomain_InnerShareable;MBReqDomain_OuterShareable;MBReqDomain_FullSystem]

val MBReqTypes_of_num : integer -> MBReqTypes

let MBReqTypes_of_num arg_ =
   let l__132 = arg_ in
   if (eq l__132 (0:ii))
   then MBReqTypes_Reads
   else if (eq l__132 (1:ii)) then MBReqTypes_Writes else MBReqTypes_All

val num_of_MBReqTypes : MBReqTypes -> integer

let num_of_MBReqTypes arg_ =
   match arg_ with
   | MBReqTypes_Reads -> (0:ii)
   | MBReqTypes_Writes -> (1:ii)
   | MBReqTypes_All -> (2:ii)
   end

val undefined_MBReqTypes : unit -> MBReqTypes

let undefined_MBReqTypes () = internal_pick [MBReqTypes_Reads;MBReqTypes_Writes;MBReqTypes_All]

val MemType_of_num : integer -> MemType

let MemType_of_num arg_ =
   let l__131 = arg_ in
   if (eq l__131 (0:ii))
   then MemType_Normal
   else MemType_Device

val num_of_MemType : MemType -> integer

let num_of_MemType arg_ = match arg_ with | MemType_Normal -> (0:ii) | MemType_Device -> (1:ii) end

val undefined_MemType : unit -> MemType

let undefined_MemType () = internal_pick [MemType_Normal;MemType_Device]

val DeviceType_of_num : integer -> DeviceType

let DeviceType_of_num arg_ =
   let l__128 = arg_ in
   if (eq l__128 (0:ii))
   then DeviceType_GRE
   else
   if (eq l__128 (1:ii))
   then DeviceType_nGRE
   else if (eq l__128 (2:ii)) then DeviceType_nGnRE else DeviceType_nGnRnE

val num_of_DeviceType : DeviceType -> integer

let num_of_DeviceType arg_ =
   match arg_ with
   | DeviceType_GRE -> (0:ii)
   | DeviceType_nGRE -> (1:ii)
   | DeviceType_nGnRE -> (2:ii)
   | DeviceType_nGnRnE -> (3:ii)
   end

val undefined_DeviceType : unit -> DeviceType

let undefined_DeviceType () =
   internal_pick [DeviceType_GRE;DeviceType_nGRE;DeviceType_nGnRE;DeviceType_nGnRnE]

val undefined_MemAttrHints : unit -> MemAttrHints

let undefined_MemAttrHints () =
   <| MemAttrHints_attrs = (undefined_vector (2:ii) (undefined_bit ()) : list bitU); 
      MemAttrHints_hints = (undefined_vector (2:ii) (undefined_bit ()) : list bitU); 
      MemAttrHints_transient = (undefined_bool ()) |>

val undefined_MemoryAttributes : unit -> MemoryAttributes

let undefined_MemoryAttributes () =
   <| MemoryAttributes_typ = (undefined_MemType ()); 
      MemoryAttributes_device = (undefined_DeviceType ()); 
      MemoryAttributes_inner = (undefined_MemAttrHints ()); 
      MemoryAttributes_outer = (undefined_MemAttrHints ()); 
      MemoryAttributes_shareable = (undefined_bool ()); 
      MemoryAttributes_outershareable = (undefined_bool ()) |>

val undefined_FullAddress : unit -> FullAddress

let undefined_FullAddress () =
   <| FullAddress_physicaladdress = (undefined_vector (52:ii) (undefined_bit ()) : list bitU); 
      FullAddress_NS = (undefined_vector (1:ii) (undefined_bit ()) : list bitU) |>

val undefined_AddressDescriptor : unit -> AddressDescriptor

let undefined_AddressDescriptor () =
   <| AddressDescriptor_fault = (undefined_FaultRecord ()); 
      AddressDescriptor_memattrs = (undefined_MemoryAttributes ()); 
      AddressDescriptor_paddress = (undefined_FullAddress ()); 
      AddressDescriptor_vaddress = (undefined_vector (64:ii) (undefined_bit ()) : list bitU) |>

val undefined_DescriptorUpdate : unit -> DescriptorUpdate

let undefined_DescriptorUpdate () =
   <| DescriptorUpdate_AF = (undefined_bool ()); 
      DescriptorUpdate_AP = (undefined_bool ()); 
      DescriptorUpdate_descaddr = (undefined_AddressDescriptor ()) |>

val MemAtomicOp_of_num : integer -> MemAtomicOp

let MemAtomicOp_of_num arg_ =
   let l__120 = arg_ in
   if (eq l__120 (0:ii))
   then MemAtomicOp_ADD
   else
   if (eq l__120 (1:ii))
   then MemAtomicOp_BIC
   else
   if (eq l__120 (2:ii))
   then MemAtomicOp_EOR
   else
   if (eq l__120 (3:ii))
   then MemAtomicOp_ORR
   else
   if (eq l__120 (4:ii))
   then MemAtomicOp_SMAX
   else
   if (eq l__120 (5:ii))
   then MemAtomicOp_SMIN
   else
   if (eq l__120 (6:ii))
   then MemAtomicOp_UMAX
   else if (eq l__120 (7:ii)) then MemAtomicOp_UMIN else MemAtomicOp_SWP

val num_of_MemAtomicOp : MemAtomicOp -> integer

let num_of_MemAtomicOp arg_ =
   match arg_ with
   | MemAtomicOp_ADD -> (0:ii)
   | MemAtomicOp_BIC -> (1:ii)
   | MemAtomicOp_EOR -> (2:ii)
   | MemAtomicOp_ORR -> (3:ii)
   | MemAtomicOp_SMAX -> (4:ii)
   | MemAtomicOp_SMIN -> (5:ii)
   | MemAtomicOp_UMAX -> (6:ii)
   | MemAtomicOp_UMIN -> (7:ii)
   | MemAtomicOp_SWP -> (8:ii)
   end

val undefined_MemAtomicOp : unit -> MemAtomicOp

let undefined_MemAtomicOp () =
   internal_pick
     [MemAtomicOp_ADD;MemAtomicOp_BIC;MemAtomicOp_EOR;MemAtomicOp_ORR;MemAtomicOp_SMAX;MemAtomicOp_SMIN;MemAtomicOp_UMAX;MemAtomicOp_UMIN;MemAtomicOp_SWP]

val FPType_of_num : integer -> FPType

let FPType_of_num arg_ =
   let l__116 = arg_ in
   if (eq l__116 (0:ii))
   then FPType_Nonzero
   else
   if (eq l__116 (1:ii))
   then FPType_Zero
   else
   if (eq l__116 (2:ii))
   then FPType_Infinity
   else if (eq l__116 (3:ii)) then FPType_QNaN else FPType_SNaN

val num_of_FPType : FPType -> integer

let num_of_FPType arg_ =
   match arg_ with
   | FPType_Nonzero -> (0:ii)
   | FPType_Zero -> (1:ii)
   | FPType_Infinity -> (2:ii)
   | FPType_QNaN -> (3:ii)
   | FPType_SNaN -> (4:ii)
   end

val undefined_FPType : unit -> FPType

let undefined_FPType () =
   internal_pick [FPType_Nonzero;FPType_Zero;FPType_Infinity;FPType_QNaN;FPType_SNaN]

val FPExc_of_num : integer -> FPExc

let FPExc_of_num arg_ =
   let l__111 = arg_ in
   if (eq l__111 (0:ii))
   then FPExc_InvalidOp
   else
   if (eq l__111 (1:ii))
   then FPExc_DivideByZero
   else
   if (eq l__111 (2:ii))
   then FPExc_Overflow
   else
   if (eq l__111 (3:ii))
   then FPExc_Underflow
   else if (eq l__111 (4:ii)) then FPExc_Inexact else FPExc_InputDenorm

val num_of_FPExc : FPExc -> integer

let num_of_FPExc arg_ =
   match arg_ with
   | FPExc_InvalidOp -> (0:ii)
   | FPExc_DivideByZero -> (1:ii)
   | FPExc_Overflow -> (2:ii)
   | FPExc_Underflow -> (3:ii)
   | FPExc_Inexact -> (4:ii)
   | FPExc_InputDenorm -> (5:ii)
   end

val undefined_FPExc : unit -> FPExc

let undefined_FPExc () =
   internal_pick
     [FPExc_InvalidOp;FPExc_DivideByZero;FPExc_Overflow;FPExc_Underflow;FPExc_Inexact;FPExc_InputDenorm]

val FPRounding_of_num : integer -> FPRounding

let FPRounding_of_num arg_ =
   let l__106 = arg_ in
   if (eq l__106 (0:ii))
   then FPRounding_TIEEVEN
   else
   if (eq l__106 (1:ii))
   then FPRounding_POSINF
   else
   if (eq l__106 (2:ii))
   then FPRounding_NEGINF
   else
   if (eq l__106 (3:ii))
   then FPRounding_ZERO
   else if (eq l__106 (4:ii)) then FPRounding_TIEAWAY else FPRounding_ODD

val num_of_FPRounding : FPRounding -> integer

let num_of_FPRounding arg_ =
   match arg_ with
   | FPRounding_TIEEVEN -> (0:ii)
   | FPRounding_POSINF -> (1:ii)
   | FPRounding_NEGINF -> (2:ii)
   | FPRounding_ZERO -> (3:ii)
   | FPRounding_TIEAWAY -> (4:ii)
   | FPRounding_ODD -> (5:ii)
   end

val undefined_FPRounding : unit -> FPRounding

let undefined_FPRounding () =
   internal_pick
     [FPRounding_TIEEVEN;FPRounding_POSINF;FPRounding_NEGINF;FPRounding_ZERO;FPRounding_TIEAWAY;FPRounding_ODD]

val SysRegAccess_of_num : integer -> SysRegAccess

let SysRegAccess_of_num arg_ =
   let l__102 = arg_ in
   if (eq l__102 (0:ii))
   then SysRegAccess_OK
   else
   if (eq l__102 (1:ii))
   then SysRegAccess_UNDEFINED
   else
   if (eq l__102 (2:ii))
   then SysRegAccess_TrapToEL1
   else if (eq l__102 (3:ii)) then SysRegAccess_TrapToEL2 else SysRegAccess_TrapToEL3

val num_of_SysRegAccess : SysRegAccess -> integer

let num_of_SysRegAccess arg_ =
   match arg_ with
   | SysRegAccess_OK -> (0:ii)
   | SysRegAccess_UNDEFINED -> (1:ii)
   | SysRegAccess_TrapToEL1 -> (2:ii)
   | SysRegAccess_TrapToEL2 -> (3:ii)
   | SysRegAccess_TrapToEL3 -> (4:ii)
   end

val undefined_SysRegAccess : unit -> SysRegAccess

let undefined_SysRegAccess () =
   internal_pick
     [SysRegAccess_OK;SysRegAccess_UNDEFINED;SysRegAccess_TrapToEL1;SysRegAccess_TrapToEL2;SysRegAccess_TrapToEL3]

val SRType_of_num : integer -> SRType

let SRType_of_num arg_ =
   let l__98 = arg_ in
   if (eq l__98 (0:ii))
   then SRType_LSL
   else
   if (eq l__98 (1:ii))
   then SRType_LSR
   else
   if (eq l__98 (2:ii))
   then SRType_ASR
   else if (eq l__98 (3:ii)) then SRType_ROR else SRType_RRX

val num_of_SRType : SRType -> integer

let num_of_SRType arg_ =
   match arg_ with
   | SRType_LSL -> (0:ii)
   | SRType_LSR -> (1:ii)
   | SRType_ASR -> (2:ii)
   | SRType_ROR -> (3:ii)
   | SRType_RRX -> (4:ii)
   end

val undefined_SRType : unit -> SRType

let undefined_SRType () = internal_pick [SRType_LSL;SRType_LSR;SRType_ASR;SRType_ROR;SRType_RRX]

val ShiftType_of_num : integer -> ShiftType

let ShiftType_of_num arg_ =
   let l__95 = arg_ in
   if (eq l__95 (0:ii))
   then ShiftType_LSL
   else
   if (eq l__95 (1:ii))
   then ShiftType_LSR
   else if (eq l__95 (2:ii)) then ShiftType_ASR else ShiftType_ROR

val num_of_ShiftType : ShiftType -> integer

let num_of_ShiftType arg_ =
   match arg_ with
   | ShiftType_LSL -> (0:ii)
   | ShiftType_LSR -> (1:ii)
   | ShiftType_ASR -> (2:ii)
   | ShiftType_ROR -> (3:ii)
   end

val undefined_ShiftType : unit -> ShiftType

let undefined_ShiftType () = internal_pick [ShiftType_LSL;ShiftType_LSR;ShiftType_ASR;ShiftType_ROR]

val PrefetchHint_of_num : integer -> PrefetchHint

let PrefetchHint_of_num arg_ =
   let l__93 = arg_ in
   if (eq l__93 (0:ii))
   then Prefetch_READ
   else if (eq l__93 (1:ii)) then Prefetch_WRITE else Prefetch_EXEC

val num_of_PrefetchHint : PrefetchHint -> integer

let num_of_PrefetchHint arg_ =
   match arg_ with
   | Prefetch_READ -> (0:ii)
   | Prefetch_WRITE -> (1:ii)
   | Prefetch_EXEC -> (2:ii)
   end

val undefined_PrefetchHint : unit -> PrefetchHint

let undefined_PrefetchHint () = internal_pick [Prefetch_READ;Prefetch_WRITE;Prefetch_EXEC]

val InterruptID_of_num : integer -> InterruptID

let InterruptID_of_num arg_ =
   let l__89 = arg_ in
   if (eq l__89 (0:ii))
   then InterruptID_PMUIRQ
   else
   if (eq l__89 (1:ii))
   then InterruptID_COMMIRQ
   else
   if (eq l__89 (2:ii))
   then InterruptID_CTIIRQ
   else if (eq l__89 (3:ii)) then InterruptID_COMMRX else InterruptID_COMMTX

val num_of_InterruptID : InterruptID -> integer

let num_of_InterruptID arg_ =
   match arg_ with
   | InterruptID_PMUIRQ -> (0:ii)
   | InterruptID_COMMIRQ -> (1:ii)
   | InterruptID_CTIIRQ -> (2:ii)
   | InterruptID_COMMRX -> (3:ii)
   | InterruptID_COMMTX -> (4:ii)
   end

val undefined_InterruptID : unit -> InterruptID

let undefined_InterruptID () =
   internal_pick
     [InterruptID_PMUIRQ;InterruptID_COMMIRQ;InterruptID_CTIIRQ;InterruptID_COMMRX;InterruptID_COMMTX]

val CrossTriggerOut_of_num : integer -> CrossTriggerOut

let CrossTriggerOut_of_num arg_ =
   let l__82 = arg_ in
   if (eq l__82 (0:ii))
   then CrossTriggerOut_DebugRequest
   else
   if (eq l__82 (1:ii))
   then CrossTriggerOut_RestartRequest
   else
   if (eq l__82 (2:ii))
   then CrossTriggerOut_IRQ
   else
   if (eq l__82 (3:ii))
   then CrossTriggerOut_RSVD3
   else
   if (eq l__82 (4:ii))
   then CrossTriggerOut_TraceExtIn0
   else
   if (eq l__82 (5:ii))
   then CrossTriggerOut_TraceExtIn1
   else if (eq l__82 (6:ii)) then CrossTriggerOut_TraceExtIn2 else CrossTriggerOut_TraceExtIn3

val num_of_CrossTriggerOut : CrossTriggerOut -> integer

let num_of_CrossTriggerOut arg_ =
   match arg_ with
   | CrossTriggerOut_DebugRequest -> (0:ii)
   | CrossTriggerOut_RestartRequest -> (1:ii)
   | CrossTriggerOut_IRQ -> (2:ii)
   | CrossTriggerOut_RSVD3 -> (3:ii)
   | CrossTriggerOut_TraceExtIn0 -> (4:ii)
   | CrossTriggerOut_TraceExtIn1 -> (5:ii)
   | CrossTriggerOut_TraceExtIn2 -> (6:ii)
   | CrossTriggerOut_TraceExtIn3 -> (7:ii)
   end

val undefined_CrossTriggerOut : unit -> CrossTriggerOut

let undefined_CrossTriggerOut () =
   internal_pick
     [CrossTriggerOut_DebugRequest;CrossTriggerOut_RestartRequest;CrossTriggerOut_IRQ;CrossTriggerOut_RSVD3;CrossTriggerOut_TraceExtIn0;CrossTriggerOut_TraceExtIn1;CrossTriggerOut_TraceExtIn2;CrossTriggerOut_TraceExtIn3]

val CrossTriggerIn_of_num : integer -> CrossTriggerIn

let CrossTriggerIn_of_num arg_ =
   let l__75 = arg_ in
   if (eq l__75 (0:ii))
   then CrossTriggerIn_CrossHalt
   else
   if (eq l__75 (1:ii))
   then CrossTriggerIn_PMUOverflow
   else
   if (eq l__75 (2:ii))
   then CrossTriggerIn_RSVD2
   else
   if (eq l__75 (3:ii))
   then CrossTriggerIn_RSVD3
   else
   if (eq l__75 (4:ii))
   then CrossTriggerIn_TraceExtOut0
   else
   if (eq l__75 (5:ii))
   then CrossTriggerIn_TraceExtOut1
   else if (eq l__75 (6:ii)) then CrossTriggerIn_TraceExtOut2 else CrossTriggerIn_TraceExtOut3

val num_of_CrossTriggerIn : CrossTriggerIn -> integer

let num_of_CrossTriggerIn arg_ =
   match arg_ with
   | CrossTriggerIn_CrossHalt -> (0:ii)
   | CrossTriggerIn_PMUOverflow -> (1:ii)
   | CrossTriggerIn_RSVD2 -> (2:ii)
   | CrossTriggerIn_RSVD3 -> (3:ii)
   | CrossTriggerIn_TraceExtOut0 -> (4:ii)
   | CrossTriggerIn_TraceExtOut1 -> (5:ii)
   | CrossTriggerIn_TraceExtOut2 -> (6:ii)
   | CrossTriggerIn_TraceExtOut3 -> (7:ii)
   end

val undefined_CrossTriggerIn : unit -> CrossTriggerIn

let undefined_CrossTriggerIn () =
   internal_pick
     [CrossTriggerIn_CrossHalt;CrossTriggerIn_PMUOverflow;CrossTriggerIn_RSVD2;CrossTriggerIn_RSVD3;CrossTriggerIn_TraceExtOut0;CrossTriggerIn_TraceExtOut1;CrossTriggerIn_TraceExtOut2;CrossTriggerIn_TraceExtOut3]

val MemBarrierOp_of_num : integer -> MemBarrierOp

let MemBarrierOp_of_num arg_ =
   let l__73 = arg_ in
   if (eq l__73 (0:ii))
   then MemBarrierOp_DSB
   else if (eq l__73 (1:ii)) then MemBarrierOp_DMB else MemBarrierOp_ISB

val num_of_MemBarrierOp : MemBarrierOp -> integer

let num_of_MemBarrierOp arg_ =
   match arg_ with
   | MemBarrierOp_DSB -> (0:ii)
   | MemBarrierOp_DMB -> (1:ii)
   | MemBarrierOp_ISB -> (2:ii)
   end

val undefined_MemBarrierOp : unit -> MemBarrierOp

let undefined_MemBarrierOp () = internal_pick [MemBarrierOp_DSB;MemBarrierOp_DMB;MemBarrierOp_ISB]

val undefined_AccessDescriptor : unit -> AccessDescriptor

let undefined_AccessDescriptor () =
   <| AccessDescriptor_acctype = (undefined_AccType ()); 
      AccessDescriptor_page_table_walk = (undefined_bool ()); 
      AccessDescriptor_secondstage = (undefined_bool ()); 
      AccessDescriptor_s2fs1walk = (undefined_bool ()); 
      AccessDescriptor_level = (undefined_int ()) |>

val undefined_Permissions : unit -> Permissions

let undefined_Permissions () =
   <| Permissions_ap = (undefined_vector (3:ii) (undefined_bit ()) : list bitU); 
      Permissions_xn = (undefined_vector (1:ii) (undefined_bit ()) : list bitU); 
      Permissions_xxn = (undefined_vector (1:ii) (undefined_bit ()) : list bitU); 
      Permissions_pxn = (undefined_vector (1:ii) (undefined_bit ()) : list bitU) |>

val undefined_TLBRecord : unit -> TLBRecord

let undefined_TLBRecord () =
   <| TLBRecord_perms = (undefined_Permissions ()); 
      TLBRecord_nG = (undefined_vector (1:ii) (undefined_bit ()) : list bitU); 
      TLBRecord_domain = (undefined_vector (4:ii) (undefined_bit ()) : list bitU); 
      TLBRecord_contiguous = (undefined_bool ()); 
      TLBRecord_level = (undefined_int ()); 
      TLBRecord_blocksize = (undefined_int ()); 
      TLBRecord_descupdate = (undefined_DescriptorUpdate ()); 
      TLBRecord_CnP = (undefined_vector (1:ii) (undefined_bit ()) : list bitU); 
      TLBRecord_addrdesc = (undefined_AddressDescriptor ()) |>

val ImmediateOp_of_num : integer -> ImmediateOp

let ImmediateOp_of_num arg_ =
   let l__70 = arg_ in
   if (eq l__70 (0:ii))
   then ImmediateOp_MOVI
   else
   if (eq l__70 (1:ii))
   then ImmediateOp_MVNI
   else if (eq l__70 (2:ii)) then ImmediateOp_ORR else ImmediateOp_BIC

val num_of_ImmediateOp : ImmediateOp -> integer

let num_of_ImmediateOp arg_ =
   match arg_ with
   | ImmediateOp_MOVI -> (0:ii)
   | ImmediateOp_MVNI -> (1:ii)
   | ImmediateOp_ORR -> (2:ii)
   | ImmediateOp_BIC -> (3:ii)
   end

val undefined_ImmediateOp : unit -> ImmediateOp

let undefined_ImmediateOp () =
   internal_pick [ImmediateOp_MOVI;ImmediateOp_MVNI;ImmediateOp_ORR;ImmediateOp_BIC]

val MoveWideOp_of_num : integer -> MoveWideOp

let MoveWideOp_of_num arg_ =
   let l__68 = arg_ in
   if (eq l__68 (0:ii))
   then MoveWideOp_N
   else if (eq l__68 (1:ii)) then MoveWideOp_Z else MoveWideOp_K

val num_of_MoveWideOp : MoveWideOp -> integer

let num_of_MoveWideOp arg_ =
   match arg_ with | MoveWideOp_N -> (0:ii) | MoveWideOp_Z -> (1:ii) | MoveWideOp_K -> (2:ii) end

val undefined_MoveWideOp : unit -> MoveWideOp

let undefined_MoveWideOp () = internal_pick [MoveWideOp_N;MoveWideOp_Z;MoveWideOp_K]

val SystemAccessType_of_num : integer -> SystemAccessType

let SystemAccessType_of_num arg_ =
   let l__66 = arg_ in
   if (eq l__66 (0:ii))
   then SystemAccessType_RT
   else if (eq l__66 (1:ii)) then SystemAccessType_RRT else SystemAccessType_DT

val num_of_SystemAccessType : SystemAccessType -> integer

let num_of_SystemAccessType arg_ =
   match arg_ with
   | SystemAccessType_RT -> (0:ii)
   | SystemAccessType_RRT -> (1:ii)
   | SystemAccessType_DT -> (2:ii)
   end

val undefined_SystemAccessType : unit -> SystemAccessType

let undefined_SystemAccessType () =
   internal_pick [SystemAccessType_RT;SystemAccessType_RRT;SystemAccessType_DT]

val VBitOp_of_num : integer -> VBitOp

let VBitOp_of_num arg_ =
   let l__63 = arg_ in
   if (eq l__63 (0:ii))
   then VBitOp_VBIF
   else
   if (eq l__63 (1:ii))
   then VBitOp_VBIT
   else if (eq l__63 (2:ii)) then VBitOp_VBSL else VBitOp_VEOR

val num_of_VBitOp : VBitOp -> integer

let num_of_VBitOp arg_ =
   match arg_ with
   | VBitOp_VBIF -> (0:ii)
   | VBitOp_VBIT -> (1:ii)
   | VBitOp_VBSL -> (2:ii)
   | VBitOp_VEOR -> (3:ii)
   end

val undefined_VBitOp : unit -> VBitOp

let undefined_VBitOp () = internal_pick [VBitOp_VBIF;VBitOp_VBIT;VBitOp_VBSL;VBitOp_VEOR]

val TimeStamp_of_num : integer -> TimeStamp

let TimeStamp_of_num arg_ =
   let l__61 = arg_ in
   if (eq l__61 (0:ii))
   then TimeStamp_None
   else if (eq l__61 (1:ii)) then TimeStamp_Virtual else TimeStamp_Physical

val num_of_TimeStamp : TimeStamp -> integer

let num_of_TimeStamp arg_ =
   match arg_ with
   | TimeStamp_None -> (0:ii)
   | TimeStamp_Virtual -> (1:ii)
   | TimeStamp_Physical -> (2:ii)
   end

val undefined_TimeStamp : unit -> TimeStamp

let undefined_TimeStamp () = internal_pick [TimeStamp_None;TimeStamp_Virtual;TimeStamp_Physical]

val PrivilegeLevel_of_num : integer -> PrivilegeLevel

let PrivilegeLevel_of_num arg_ =
   let l__58 = arg_ in
   if (eq l__58 (0:ii))
   then PL3
   else if (eq l__58 (1:ii)) then PL2 else if (eq l__58 (2:ii)) then PL1 else PL0

val num_of_PrivilegeLevel : PrivilegeLevel -> integer

let num_of_PrivilegeLevel arg_ =
   match arg_ with | PL3 -> (0:ii) | PL2 -> (1:ii) | PL1 -> (2:ii) | PL0 -> (3:ii) end

val undefined_PrivilegeLevel : unit -> PrivilegeLevel

let undefined_PrivilegeLevel () = internal_pick [PL3;PL2;PL1;PL0]

val undefined_AArch32_SErrorSyndrome : unit -> AArch32_SErrorSyndrome

let undefined_AArch32_SErrorSyndrome () =
   <| AArch32_SErrorSyndrome_AET = (undefined_vector (2:ii) (undefined_bit ()) : list bitU); 
      AArch32_SErrorSyndrome_ExT = (undefined_vector (1:ii) (undefined_bit ()) : list bitU) |>

val SystemOp_of_num : integer -> SystemOp

let SystemOp_of_num arg_ =
   let l__54 = arg_ in
   if (eq l__54 (0:ii))
   then Sys_AT
   else
   if (eq l__54 (1:ii))
   then Sys_DC
   else if (eq l__54 (2:ii)) then Sys_IC else if (eq l__54 (3:ii)) then Sys_TLBI else Sys_SYS

val num_of_SystemOp : SystemOp -> integer

let num_of_SystemOp arg_ =
   match arg_ with
   | Sys_AT -> (0:ii)
   | Sys_DC -> (1:ii)
   | Sys_IC -> (2:ii)
   | Sys_TLBI -> (3:ii)
   | Sys_SYS -> (4:ii)
   end

val undefined_SystemOp : unit -> SystemOp

let undefined_SystemOp () = internal_pick [Sys_AT;Sys_DC;Sys_IC;Sys_TLBI;Sys_SYS]

val undefined_PCSample : unit -> PCSample

let undefined_PCSample () =
   <| PCSample_valid_name = (undefined_bool ()); 
      PCSample_pc = (undefined_vector (64:ii) (undefined_bit ()) : list bitU); 
      PCSample_el = (undefined_vector (2:ii) (undefined_bit ()) : list bitU); 
      PCSample_rw = (undefined_vector (1:ii) (undefined_bit ()) : list bitU); 
      PCSample_ns = (undefined_vector (1:ii) (undefined_bit ()) : list bitU); 
      PCSample_contextidr = (undefined_vector (32:ii) (undefined_bit ()) : list bitU); 
      PCSample_contextidr_el2 = (undefined_vector (32:ii) (undefined_bit ()) : list bitU); 
      PCSample_vmid = (undefined_vector (16:ii) (undefined_bit ()) : list bitU) |>

val ReduceOp_of_num : integer -> ReduceOp

let ReduceOp_of_num arg_ =
   let l__49 = arg_ in
   if (eq l__49 (0:ii))
   then ReduceOp_FMINNUM
   else
   if (eq l__49 (1:ii))
   then ReduceOp_FMAXNUM
   else
   if (eq l__49 (2:ii))
   then ReduceOp_FMIN
   else
   if (eq l__49 (3:ii))
   then ReduceOp_FMAX
   else if (eq l__49 (4:ii)) then ReduceOp_FADD else ReduceOp_ADD

val num_of_ReduceOp : ReduceOp -> integer

let num_of_ReduceOp arg_ =
   match arg_ with
   | ReduceOp_FMINNUM -> (0:ii)
   | ReduceOp_FMAXNUM -> (1:ii)
   | ReduceOp_FMIN -> (2:ii)
   | ReduceOp_FMAX -> (3:ii)
   | ReduceOp_FADD -> (4:ii)
   | ReduceOp_ADD -> (5:ii)
   end

val undefined_ReduceOp : unit -> ReduceOp

let undefined_ReduceOp () =
   internal_pick
     [ReduceOp_FMINNUM;ReduceOp_FMAXNUM;ReduceOp_FMIN;ReduceOp_FMAX;ReduceOp_FADD;ReduceOp_ADD]

val LogicalOp_of_num : integer -> LogicalOp

let LogicalOp_of_num arg_ =
   let l__47 = arg_ in
   if (eq l__47 (0:ii))
   then LogicalOp_AND
   else if (eq l__47 (1:ii)) then LogicalOp_EOR else LogicalOp_ORR

val num_of_LogicalOp : LogicalOp -> integer

let num_of_LogicalOp arg_ =
   match arg_ with | LogicalOp_AND -> (0:ii) | LogicalOp_EOR -> (1:ii) | LogicalOp_ORR -> (2:ii) end

val undefined_LogicalOp : unit -> LogicalOp

let undefined_LogicalOp () = internal_pick [LogicalOp_AND;LogicalOp_EOR;LogicalOp_ORR]

val ExtendType_of_num : integer -> ExtendType

let ExtendType_of_num arg_ =
   let l__40 = arg_ in
   if (eq l__40 (0:ii))
   then ExtendType_SXTB
   else
   if (eq l__40 (1:ii))
   then ExtendType_SXTH
   else
   if (eq l__40 (2:ii))
   then ExtendType_SXTW
   else
   if (eq l__40 (3:ii))
   then ExtendType_SXTX
   else
   if (eq l__40 (4:ii))
   then ExtendType_UXTB
   else
   if (eq l__40 (5:ii))
   then ExtendType_UXTH
   else if (eq l__40 (6:ii)) then ExtendType_UXTW else ExtendType_UXTX

val num_of_ExtendType : ExtendType -> integer

let num_of_ExtendType arg_ =
   match arg_ with
   | ExtendType_SXTB -> (0:ii)
   | ExtendType_SXTH -> (1:ii)
   | ExtendType_SXTW -> (2:ii)
   | ExtendType_SXTX -> (3:ii)
   | ExtendType_UXTB -> (4:ii)
   | ExtendType_UXTH -> (5:ii)
   | ExtendType_UXTW -> (6:ii)
   | ExtendType_UXTX -> (7:ii)
   end

val undefined_ExtendType : unit -> ExtendType

let undefined_ExtendType () =
   internal_pick
     [ExtendType_SXTB;ExtendType_SXTH;ExtendType_SXTW;ExtendType_SXTX;ExtendType_UXTB;ExtendType_UXTH;ExtendType_UXTW;ExtendType_UXTX]

val SystemHintOp_of_num : integer -> SystemHintOp

let SystemHintOp_of_num arg_ =
   let l__33 = arg_ in
   if (eq l__33 (0:ii))
   then SystemHintOp_NOP
   else
   if (eq l__33 (1:ii))
   then SystemHintOp_YIELD
   else
   if (eq l__33 (2:ii))
   then SystemHintOp_WFE
   else
   if (eq l__33 (3:ii))
   then SystemHintOp_WFI
   else
   if (eq l__33 (4:ii))
   then SystemHintOp_SEV
   else
   if (eq l__33 (5:ii))
   then SystemHintOp_SEVL
   else if (eq l__33 (6:ii)) then SystemHintOp_ESB else SystemHintOp_PSB

val num_of_SystemHintOp : SystemHintOp -> integer

let num_of_SystemHintOp arg_ =
   match arg_ with
   | SystemHintOp_NOP -> (0:ii)
   | SystemHintOp_YIELD -> (1:ii)
   | SystemHintOp_WFE -> (2:ii)
   | SystemHintOp_WFI -> (3:ii)
   | SystemHintOp_SEV -> (4:ii)
   | SystemHintOp_SEVL -> (5:ii)
   | SystemHintOp_ESB -> (6:ii)
   | SystemHintOp_PSB -> (7:ii)
   end

val undefined_SystemHintOp : unit -> SystemHintOp

let undefined_SystemHintOp () =
   internal_pick
     [SystemHintOp_NOP;SystemHintOp_YIELD;SystemHintOp_WFE;SystemHintOp_WFI;SystemHintOp_SEV;SystemHintOp_SEVL;SystemHintOp_ESB;SystemHintOp_PSB]

val MemOp_of_num : integer -> MemOp

let MemOp_of_num arg_ =
   let l__31 = arg_ in
   if (eq l__31 (0:ii))
   then MemOp_LOAD
   else if (eq l__31 (1:ii)) then MemOp_STORE else MemOp_PREFETCH

val num_of_MemOp : MemOp -> integer

let num_of_MemOp arg_ =
   match arg_ with | MemOp_LOAD -> (0:ii) | MemOp_STORE -> (1:ii) | MemOp_PREFETCH -> (2:ii) end

val undefined_MemOp : unit -> MemOp

let undefined_MemOp () = internal_pick [MemOp_LOAD;MemOp_STORE;MemOp_PREFETCH]

val OpType_of_num : integer -> OpType

let OpType_of_num arg_ =
   let l__27 = arg_ in
   if (eq l__27 (0:ii))
   then OpType_Load
   else
   if (eq l__27 (1:ii))
   then OpType_Store
   else
   if (eq l__27 (2:ii))
   then OpType_LoadAtomic
   else if (eq l__27 (3:ii)) then OpType_Branch else OpType_Other

val num_of_OpType : OpType -> integer

let num_of_OpType arg_ =
   match arg_ with
   | OpType_Load -> (0:ii)
   | OpType_Store -> (1:ii)
   | OpType_LoadAtomic -> (2:ii)
   | OpType_Branch -> (3:ii)
   | OpType_Other -> (4:ii)
   end

val undefined_OpType : unit -> OpType

let undefined_OpType () =
   internal_pick [OpType_Load;OpType_Store;OpType_LoadAtomic;OpType_Branch;OpType_Other]

val FPUnaryOp_of_num : integer -> FPUnaryOp

let FPUnaryOp_of_num arg_ =
   let l__24 = arg_ in
   if (eq l__24 (0:ii))
   then FPUnaryOp_ABS
   else
   if (eq l__24 (1:ii))
   then FPUnaryOp_MOV
   else if (eq l__24 (2:ii)) then FPUnaryOp_NEG else FPUnaryOp_SQRT

val num_of_FPUnaryOp : FPUnaryOp -> integer

let num_of_FPUnaryOp arg_ =
   match arg_ with
   | FPUnaryOp_ABS -> (0:ii)
   | FPUnaryOp_MOV -> (1:ii)
   | FPUnaryOp_NEG -> (2:ii)
   | FPUnaryOp_SQRT -> (3:ii)
   end

val undefined_FPUnaryOp : unit -> FPUnaryOp

let undefined_FPUnaryOp () =
   internal_pick [FPUnaryOp_ABS;FPUnaryOp_MOV;FPUnaryOp_NEG;FPUnaryOp_SQRT]

val CompareOp_of_num : integer -> CompareOp

let CompareOp_of_num arg_ =
   let l__20 = arg_ in
   if (eq l__20 (0:ii))
   then CompareOp_GT
   else
   if (eq l__20 (1:ii))
   then CompareOp_GE
   else
   if (eq l__20 (2:ii))
   then CompareOp_EQ
   else if (eq l__20 (3:ii)) then CompareOp_LE else CompareOp_LT

val num_of_CompareOp : CompareOp -> integer

let num_of_CompareOp arg_ =
   match arg_ with
   | CompareOp_GT -> (0:ii)
   | CompareOp_GE -> (1:ii)
   | CompareOp_EQ -> (2:ii)
   | CompareOp_LE -> (3:ii)
   | CompareOp_LT -> (4:ii)
   end

val undefined_CompareOp : unit -> CompareOp

let undefined_CompareOp () =
   internal_pick [CompareOp_GT;CompareOp_GE;CompareOp_EQ;CompareOp_LE;CompareOp_LT]

val PSTATEField_of_num : integer -> PSTATEField

let PSTATEField_of_num arg_ =
   let l__16 = arg_ in
   if (eq l__16 (0:ii))
   then PSTATEField_DAIFSet
   else
   if (eq l__16 (1:ii))
   then PSTATEField_DAIFClr
   else
   if (eq l__16 (2:ii))
   then PSTATEField_PAN
   else if (eq l__16 (3:ii)) then PSTATEField_UAO else PSTATEField_SP

val num_of_PSTATEField : PSTATEField -> integer

let num_of_PSTATEField arg_ =
   match arg_ with
   | PSTATEField_DAIFSet -> (0:ii)
   | PSTATEField_DAIFClr -> (1:ii)
   | PSTATEField_PAN -> (2:ii)
   | PSTATEField_UAO -> (3:ii)
   | PSTATEField_SP -> (4:ii)
   end

val undefined_PSTATEField : unit -> PSTATEField

let undefined_PSTATEField () =
   internal_pick
     [PSTATEField_DAIFSet;PSTATEField_DAIFClr;PSTATEField_PAN;PSTATEField_UAO;PSTATEField_SP]

val FPMaxMinOp_of_num : integer -> FPMaxMinOp

let FPMaxMinOp_of_num arg_ =
   let l__13 = arg_ in
   if (eq l__13 (0:ii))
   then FPMaxMinOp_MAX
   else
   if (eq l__13 (1:ii))
   then FPMaxMinOp_MIN
   else if (eq l__13 (2:ii)) then FPMaxMinOp_MAXNUM else FPMaxMinOp_MINNUM

val num_of_FPMaxMinOp : FPMaxMinOp -> integer

let num_of_FPMaxMinOp arg_ =
   match arg_ with
   | FPMaxMinOp_MAX -> (0:ii)
   | FPMaxMinOp_MIN -> (1:ii)
   | FPMaxMinOp_MAXNUM -> (2:ii)
   | FPMaxMinOp_MINNUM -> (3:ii)
   end

val undefined_FPMaxMinOp : unit -> FPMaxMinOp

let undefined_FPMaxMinOp () =
   internal_pick [FPMaxMinOp_MAX;FPMaxMinOp_MIN;FPMaxMinOp_MAXNUM;FPMaxMinOp_MINNUM]

val CountOp_of_num : integer -> CountOp

let CountOp_of_num arg_ =
   let l__11 = arg_ in
   if (eq l__11 (0:ii))
   then CountOp_CLZ
   else if (eq l__11 (1:ii)) then CountOp_CLS else CountOp_CNT

val num_of_CountOp : CountOp -> integer

let num_of_CountOp arg_ =
   match arg_ with | CountOp_CLZ -> (0:ii) | CountOp_CLS -> (1:ii) | CountOp_CNT -> (2:ii) end

val undefined_CountOp : unit -> CountOp

let undefined_CountOp () = internal_pick [CountOp_CLZ;CountOp_CLS;CountOp_CNT]

val VFPNegMul_of_num : integer -> VFPNegMul

let VFPNegMul_of_num arg_ =
   let l__9 = arg_ in
   if (eq l__9 (0:ii))
   then VFPNegMul_VNMLA
   else if (eq l__9 (1:ii)) then VFPNegMul_VNMLS else VFPNegMul_VNMUL

val num_of_VFPNegMul : VFPNegMul -> integer

let num_of_VFPNegMul arg_ =
   match arg_ with
   | VFPNegMul_VNMLA -> (0:ii)
   | VFPNegMul_VNMLS -> (1:ii)
   | VFPNegMul_VNMUL -> (2:ii)
   end

val undefined_VFPNegMul : unit -> VFPNegMul

let undefined_VFPNegMul () = internal_pick [VFPNegMul_VNMLA;VFPNegMul_VNMLS;VFPNegMul_VNMUL]

val VBitOps_of_num : integer -> VBitOps

let VBitOps_of_num arg_ =
   let l__7 = arg_ in
   if (eq l__7 (0:ii))
   then VBitOps_VBIF
   else if (eq l__7 (1:ii)) then VBitOps_VBIT else VBitOps_VBSL

val num_of_VBitOps : VBitOps -> integer

let num_of_VBitOps arg_ =
   match arg_ with | VBitOps_VBIF -> (0:ii) | VBitOps_VBIT -> (1:ii) | VBitOps_VBSL -> (2:ii) end

val undefined_VBitOps : unit -> VBitOps

let undefined_VBitOps () = internal_pick [VBitOps_VBIF;VBitOps_VBIT;VBitOps_VBSL]

val VCGEtype_of_num : integer -> VCGEtype

let VCGEtype_of_num arg_ =
   let l__5 = arg_ in
   if (eq l__5 (0:ii))
   then VCGEtype_signed
   else if (eq l__5 (1:ii)) then VCGEtype_unsigned else VCGEtype_fp

val num_of_VCGEtype : VCGEtype -> integer

let num_of_VCGEtype arg_ =
   match arg_ with
   | VCGEtype_signed -> (0:ii)
   | VCGEtype_unsigned -> (1:ii)
   | VCGEtype_fp -> (2:ii)
   end

val undefined_VCGEtype : unit -> VCGEtype

let undefined_VCGEtype () = internal_pick [VCGEtype_signed;VCGEtype_unsigned;VCGEtype_fp]

val VCGTtype_of_num : integer -> VCGTtype

let VCGTtype_of_num arg_ =
   let l__3 = arg_ in
   if (eq l__3 (0:ii))
   then VCGTtype_signed
   else if (eq l__3 (1:ii)) then VCGTtype_unsigned else VCGTtype_fp

val num_of_VCGTtype : VCGTtype -> integer

let num_of_VCGTtype arg_ =
   match arg_ with
   | VCGTtype_signed -> (0:ii)
   | VCGTtype_unsigned -> (1:ii)
   | VCGTtype_fp -> (2:ii)
   end

val undefined_VCGTtype : unit -> VCGTtype

let undefined_VCGTtype () = internal_pick [VCGTtype_signed;VCGTtype_unsigned;VCGTtype_fp]

val __InstrEnc_of_num : integer -> __InstrEnc

let __InstrEnc_of_num arg_ =
   let l__0 = arg_ in
   if (eq l__0 (0:ii))
   then __A64
   else if (eq l__0 (1:ii)) then __A32 else if (eq l__0 (2:ii)) then __T16 else __T32

val num_of___InstrEnc : __InstrEnc -> integer

let num_of___InstrEnc arg_ =
   match arg_ with | __A64 -> (0:ii) | __A32 -> (1:ii) | __T16 -> (2:ii) | __T32 -> (3:ii) end

val undefined___InstrEnc : unit -> __InstrEnc

let undefined___InstrEnc () = internal_pick [__A64;__A32;__T16;__T32]

val __UNKNOWN_integer : unit -> ii

let __UNKNOWN_integer () = (0:ii)

val ThisInstrAddr : integer -> unit -> M (list bitU)

let ThisInstrAddr (N__tv : integer) () =
   (read_reg _PC_ref : M (list bitU)) >>= fun (w__0 : bits ty64) ->
   return (slice w__0 (0:ii) N__tv : list bitU)

val ThisInstr : unit -> M (list bitU)

let ThisInstr () = (read_reg __ThisInstr_ref : M (list bitU))

val SynchronizeContext : unit -> unit

let SynchronizeContext () = ()

val ProcessorID : unit -> ii

let ProcessorID () = (0:ii)

val __UNKNOWN_PrefetchHint : unit -> PrefetchHint

let __UNKNOWN_PrefetchHint () = Prefetch_READ

val __UNKNOWN_MemType : unit -> MemType

let __UNKNOWN_MemType () = MemType_Normal

val __UNKNOWN_MemOp : unit -> MemOp

let __UNKNOWN_MemOp () = MemOp_LOAD

let (M32_User : list bitU) = [B1;B0;B0;B0;B0]

let (M32_Undef : list bitU) = [B1;B1;B0;B1;B1]

let (M32_System : list bitU) = [B1;B1;B1;B1;B1]

let (M32_Svc : list bitU) = [B1;B0;B0;B1;B1]

let (M32_Monitor : list bitU) = [B1;B0;B1;B1;B0]

let (M32_IRQ : list bitU) = [B1;B0;B0;B1;B0]

let (M32_Hyp : list bitU) = [B1;B1;B0;B1;B0]

let (M32_FIQ : list bitU) = [B1;B0;B0;B0;B1]

let (M32_Abort : list bitU) = [B1;B0;B1;B1;B1]

val __UNKNOWN_InstrSet : unit -> InstrSet

let __UNKNOWN_InstrSet () = InstrSet_A64

val Hint_Prefetch : list bitU -> PrefetchHint -> ii -> bool -> unit

let Hint_Prefetch address hint target stream = ()

val Hint_Branch : BranchType -> unit

let Hint_Branch hint = ()

val HaveAnyAArch32 : unit -> bool

let HaveAnyAArch32 () = false

val __UNKNOWN_Fault : unit -> Fault

let __UNKNOWN_Fault () = Fault_None

val __UNKNOWN_boolean : unit -> bool

let __UNKNOWN_boolean () = false

val Unreachable : unit -> M unit

let Unreachable () = assert_exp false "FALSE"

val RBankSelect : list bitU -> ii -> ii -> ii -> ii -> ii -> ii -> ii -> M ii

let RBankSelect mode usr fiq irq svc abt und hyp =
   let (result : ii) = undefined_int () in
   let _pat_ = mode in
   (if (eq_vec _pat_ M32_User)
    then
      let (result : ii) = usr in
      return result
    else
      (if (eq_vec _pat_ M32_FIQ)
       then
         let (result : ii) = fiq in
         return result
       else
         (if (eq_vec _pat_ M32_IRQ)
          then
            let (result : ii) = irq in
            return result
          else
            (if (eq_vec _pat_ M32_Svc)
             then
               let (result : ii) = svc in
               return result
             else
               (if (eq_vec _pat_ M32_Abort)
                then
                  let (result : ii) = abt in
                  return result
                else
                  (if (eq_vec _pat_ M32_Hyp)
                   then
                     let (result : ii) = hyp in
                     return result
                   else
                     (if (eq_vec _pat_ M32_Undef)
                      then
                        let (result : ii) = und in
                        return result
                      else
                        (if (eq_vec _pat_ M32_System)
                         then
                           let (result : ii) = usr in
                           return result
                         else
                           Unreachable () >>
                           return result) >>= fun (result : ii) ->
                        return result) >>= fun (result : ii) ->
                     return result) >>= fun (result : ii) ->
                  return result) >>= fun (result : ii) ->
               return result) >>= fun (result : ii) ->
            return result) >>= fun (result : ii) ->
         return result) >>= fun (result : ii) ->
      return result) >>= fun (result : ii) ->
   return result

val TakeUnmaskedPhysicalSErrorInterrupts : bool -> M unit

let TakeUnmaskedPhysicalSErrorInterrupts iesb_req = assert_exp false "FALSE"

val __UNKNOWN_Exception : unit -> Exception

let __UNKNOWN_Exception () = Exception_Uncategorized

val ErrorSynchronizationBarrier : MBReqDomain -> MBReqTypes -> unit

let ErrorSynchronizationBarrier domain types = ()

val EndOfInstruction : unit -> unit

let EndOfInstruction () = ()

let (EL3 : list bitU) = [B1;B1]

let (EL2 : list bitU) = [B1;B0]

let (EL1 : list bitU) = [B0;B1]

let (EL0 : list bitU) = [B0;B0]

val __UNKNOWN_DeviceType : unit -> DeviceType

let __UNKNOWN_DeviceType () = DeviceType_GRE

let (DebugException_VectorCatch : list bitU) = [B0;B1;B0;B1]

val __UNKNOWN_Constraint : unit -> Constraint

let __UNKNOWN_Constraint () = Constraint_NONE

val ConstrainUnpredictable : Unpredictable -> Constraint

let ConstrainUnpredictable which =
   match which with
   | Unpredictable_WBOVERLAPLD -> Constraint_WBSUPPRESS
   | Unpredictable_WBOVERLAPST -> Constraint_NONE
   | Unpredictable_LDPOVERLAP -> Constraint_UNDEF
   | Unpredictable_BASEOVERLAP -> Constraint_NONE
   | Unpredictable_DATAOVERLAP -> Constraint_NONE
   | Unpredictable_DEVPAGE2 -> Constraint_FAULT
   | Unpredictable_INSTRDEVICE -> Constraint_NONE
   | Unpredictable_RESCPACR -> Constraint_UNKNOWN
   | Unpredictable_RESMAIR -> Constraint_UNKNOWN
   | Unpredictable_RESTEXCB -> Constraint_UNKNOWN
   | Unpredictable_RESDACR -> Constraint_UNKNOWN
   | Unpredictable_RESPRRR -> Constraint_UNKNOWN
   | Unpredictable_RESVTCRS -> Constraint_UNKNOWN
   | Unpredictable_RESTnSZ -> Constraint_FORCE
   | Unpredictable_OORTnSZ -> Constraint_FORCE
   | Unpredictable_LARGEIPA -> Constraint_FORCE
   | Unpredictable_ESRCONDPASS -> Constraint_FALSE
   | Unpredictable_ILZEROIT -> Constraint_FALSE
   | Unpredictable_ILZEROT -> Constraint_FALSE
   | Unpredictable_BPVECTORCATCHPRI -> Constraint_TRUE
   | Unpredictable_VCMATCHHALF -> Constraint_FALSE
   | Unpredictable_VCMATCHDAPA -> Constraint_FALSE
   | Unpredictable_WPMASKANDBAS -> Constraint_FALSE
   | Unpredictable_WPBASCONTIGUOUS -> Constraint_FALSE
   | Unpredictable_RESWPMASK -> Constraint_DISABLED
   | Unpredictable_WPMASKEDBITS -> Constraint_FALSE
   | Unpredictable_RESBPWPCTRL -> Constraint_DISABLED
   | Unpredictable_BPNOTIMPL -> Constraint_DISABLED
   | Unpredictable_RESBPTYPE -> Constraint_DISABLED
   | Unpredictable_BPNOTCTXCMP -> Constraint_DISABLED
   | Unpredictable_BPMATCHHALF -> Constraint_FALSE
   | Unpredictable_BPMISMATCHHALF -> Constraint_FALSE
   | Unpredictable_RESTARTALIGNPC -> Constraint_FALSE
   | Unpredictable_RESTARTZEROUPPERPC -> Constraint_TRUE
   | Unpredictable_ZEROUPPER -> Constraint_TRUE
   | Unpredictable_ERETZEROUPPERPC -> Constraint_TRUE
   | Unpredictable_A32FORCEALIGNPC -> Constraint_FALSE
   | Unpredictable_SMD -> Constraint_UNDEF
   | Unpredictable_AFUPDATE -> Constraint_TRUE
   | Unpredictable_IESBinDebug -> Constraint_TRUE
   | Unpredictable_CLEARERRITEZERO -> Constraint_FALSE
   end

val ClearExclusiveByAddress : FullAddress -> ii -> ii -> unit

let ClearExclusiveByAddress paddress processorid size = ()

val __UNKNOWN_AccType : unit -> AccType

let __UNKNOWN_AccType () = AccType_NORMAL

val CreateAccessDescriptor : AccType -> AccessDescriptor

let CreateAccessDescriptor acctype =
   let (accdesc : AccessDescriptor) = undefined_AccessDescriptor () in
   let (accdesc : AccessDescriptor) = <|accdesc with AccessDescriptor_acctype = acctype|> in
   let (accdesc : AccessDescriptor) = <|accdesc with AccessDescriptor_page_table_walk = false|> in
   accdesc

val AArch64_CreateFaultRecord : Fault -> list bitU -> ii -> AccType -> bool -> list bitU -> list bitU -> bool -> bool -> FaultRecord

let AArch64_CreateFaultRecord typ ipaddress level acctype write extflag errortype secondstage s2fs1walk =
   let (fault : FaultRecord) = undefined_FaultRecord () in
   let (fault : FaultRecord) = <|fault with FaultRecord_typ = typ|> in
   let (fault : FaultRecord) =
     <|fault with FaultRecord_domain = (undefined_vector (4:ii) (undefined_bit ()) : list bitU)|> in
   let (fault : FaultRecord) =
     <|fault with FaultRecord_debugmoe = (undefined_vector (4:ii) (undefined_bit ()) : list bitU)|> in
   let (fault : FaultRecord) = <|fault with FaultRecord_errortype = errortype|> in
   let (fault : FaultRecord) = <|fault with FaultRecord_ipaddress = ipaddress|> in
   let (fault : FaultRecord) = <|fault with FaultRecord_level = level|> in
   let (fault : FaultRecord) = <|fault with FaultRecord_acctype = acctype|> in
   let (fault : FaultRecord) = <|fault with FaultRecord_write = write|> in
   let (fault : FaultRecord) = <|fault with FaultRecord_extflag = extflag|> in
   let (fault : FaultRecord) = <|fault with FaultRecord_secondstage = secondstage|> in
   let (fault : FaultRecord) = <|fault with FaultRecord_s2fs1walk = s2fs1walk|> in
   fault

val AArch64_AlignmentFault : AccType -> bool -> bool -> FaultRecord

let AArch64_AlignmentFault acctype iswrite secondstage =
   let (ipaddress : bits ty52) = (undefined_vector (52:ii) (undefined_bit ()) : list bitU) in
   let (level : ii) = undefined_int () in
   let (extflag : bits ty1) = (undefined_vector (1:ii) (undefined_bit ()) : list bitU) in
   let (errortype : bits ty2) = (undefined_vector (2:ii) (undefined_bit ()) : list bitU) in
   let (s2fs1walk : bool) = undefined_bool () in
   AArch64_CreateFaultRecord
     Fault_Alignment
     ipaddress
     level
     acctype
     iswrite
     extflag
     errortype
     secondstage
     s2fs1walk

val aget_SP : integer -> unit -> M (list bitU)

let aget_SP (width__tv : integer) () =
   assert_exp (or_bool
                 (eq width__tv (8:ii))
                 (or_bool
                    (eq width__tv (16:ii))
                    (or_bool (eq width__tv (32:ii)) (eq width__tv (64:ii))))) "((width == 8) || ((width == 16) || ((width == 32) || (width == 64))))" >>
   read_reg PSTATE_ref >>= fun (w__0 : ProcState) ->
   if (eq_vec w__0.ProcState_SP ([B0]))
   then
     (read_reg SP_EL0_ref : M (list bitU)) >>= fun (w__1 : bits ty64) ->
     return (slice w__1 (0:ii) width__tv : list bitU)
   else
     read_reg PSTATE_ref >>= fun (w__2 : ProcState) ->
     let p__288 = w__2.ProcState_EL in
     let _pat_ = p__288 in
     if (eq_vec _pat_ EL0)
     then
       (read_reg SP_EL0_ref : M (list bitU)) >>= fun (w__3 : bits ty64) ->
       return (slice w__3 (0:ii) width__tv : list bitU)
     else
       if (eq_vec _pat_ EL1)
       then
         (read_reg SP_EL1_ref : M (list bitU)) >>= fun (w__4 : bits ty64) ->
         return (slice w__4 (0:ii) width__tv : list bitU)
       else
         if (eq_vec _pat_ EL2)
         then
           (read_reg SP_EL2_ref : M (list bitU)) >>= fun (w__5 : bits ty64) ->
           return (slice w__5 (0:ii) width__tv : list bitU)
         else
           (read_reg SP_EL3_ref : M (list bitU)) >>= fun (w__6 : bits ty64) ->
           return (slice w__6 (0:ii) width__tv : list bitU)

val __IMPDEF_boolean : string -> bool

let __IMPDEF_boolean x =
   if (eq x "Condition valid for trapped T32")
   then true
   else
   if (eq x "Has Dot Product extension")
   then true
   else
   if (eq x "Has RAS extension")
   then true
   else
   if (eq x "Has SHA512 and SHA3 Crypto instructions")
   then true
   else
   if (eq x "Has SM3 and SM4 Crypto instructions")
   then true
   else
   if (eq x "Has basic Crypto instructions")
   then true
   else
   if (eq x "Have CRC extension")
   then true
   else
   if (eq x "Report I-cache maintenance fault in IFSR")
   then true
   else
   if (eq x "Reserved Control Space EL0 Trapped")
   then true
   else
   if (eq x "Translation fault on misprogrammed contiguous bit")
   then true
   else
   if (eq x "UNDEF unallocated CP15 access at NS EL0")
   then true
   else if (eq x "UNDEF unallocated CP15 access at NS EL0") then true else false

val ThisInstrLength : unit -> M ii

let ThisInstrLength () =
   read_reg __ThisInstrEnc_ref >>= fun (w__0 : __InstrEnc) ->
   return (if (eq w__0 __T16)
           then (16:ii)
           else (32:ii))

val HaveEL : list bitU -> bool

let HaveEL el = if (or_bool (eq_vec el EL1) (eq_vec el EL0)) then true else true

val HighestEL : unit -> list bitU

let HighestEL () = if (HaveEL EL3) then EL3 else if (HaveEL EL2) then EL2 else EL1

val HasArchVersion : ArchVersion -> bool

let HasArchVersion version =
   or_bool
     (eq version ARMv8p0)
     (or_bool (eq version ARMv8p1) (or_bool (eq version ARMv8p2) (eq version ARMv8p3)))

val HaveVirtHostExt : unit -> bool

let HaveVirtHostExt () = HasArchVersion ARMv8p1

val HaveUAOExt : unit -> bool

let HaveUAOExt () = HasArchVersion ARMv8p2

val HaveRASExt : unit -> bool

let HaveRASExt () = or_bool (HasArchVersion ARMv8p2) (__IMPDEF_boolean "Has RAS extension")

val HavePANExt : unit -> bool

let HavePANExt () = HasArchVersion ARMv8p1

val HavePACExt : unit -> bool

let HavePACExt () = HasArchVersion ARMv8p3

val ConstrainUnpredictableBool : Unpredictable -> M bool

let ConstrainUnpredictableBool which =
   let (c : Constraint) = ConstrainUnpredictable which in
   assert_exp (or_bool (eq c Constraint_TRUE) (eq c Constraint_FALSE)) "((c == Constraint_TRUE) || (c == Constraint_FALSE))" >>
   return (eq c Constraint_TRUE)

val LookUpRIndex : ii -> list bitU -> M ii

let LookUpRIndex n mode =
   assert_exp (and_bool (gteq n (0:ii)) (lteq n (14:ii))) "((n >= 0) && (n <= 14))" >>
   let (result : ii) = undefined_int () in
   let v_0 = n in
   (if (eq v_0 (8:ii))
    then
      RBankSelect mode (8:ii) (24:ii) (8:ii) (8:ii) (8:ii) (8:ii) (8:ii) >>= fun (w__0 : ii) ->
      let (result : ii) = w__0 in
      return result
    else
      (if (eq v_0 (9:ii))
       then
         RBankSelect mode (9:ii) (25:ii) (9:ii) (9:ii) (9:ii) (9:ii) (9:ii) >>= fun (w__1 : ii) ->
         let (result : ii) = w__1 in
         return result
       else
         (if (eq v_0 (10:ii))
          then
            RBankSelect mode (10:ii) (26:ii) (10:ii) (10:ii) (10:ii) (10:ii) (10:ii) >>= fun (w__2 :
              ii) ->
            let (result : ii) = w__2 in
            return result
          else
            (if (eq v_0 (11:ii))
             then
               RBankSelect mode (11:ii) (27:ii) (11:ii) (11:ii) (11:ii) (11:ii) (11:ii) >>= fun (w__3 :
                 ii) ->
               let (result : ii) = w__3 in
               return result
             else
               (if (eq v_0 (12:ii))
                then
                  RBankSelect mode (12:ii) (28:ii) (12:ii) (12:ii) (12:ii) (12:ii) (12:ii) >>= fun (w__4 :
                    ii) ->
                  let (result : ii) = w__4 in
                  return result
                else
                  (if (eq v_0 (13:ii))
                   then
                     RBankSelect mode (13:ii) (29:ii) (17:ii) (19:ii) (21:ii) (23:ii) (15:ii) >>= fun (w__5 :
                       ii) ->
                     let (result : ii) = w__5 in
                     return result
                   else
                     (if (eq v_0 (14:ii))
                      then
                        RBankSelect mode (14:ii) (30:ii) (16:ii) (18:ii) (20:ii) (22:ii) (14:ii) >>= fun (w__6 :
                          ii) ->
                        let (result : ii) = w__6 in
                        return result
                      else
                        let (result : ii) = n in
                        return result) >>= fun (result : ii) ->
                     return result) >>= fun (result : ii) ->
                  return result) >>= fun (result : ii) ->
               return result) >>= fun (result : ii) ->
            return result) >>= fun (result : ii) ->
         return result) >>= fun (result : ii) ->
      return result) >>= fun (result : ii) ->
   return result

val AArch32_ExceptionClass : Exception -> M (ii * list bitU)

let AArch32_ExceptionClass typ =
   ThisInstrLength () >>= fun (w__0 : ii) ->
   let (il : bits ty1) = if (eq (ex_int w__0) (32:ii)) then [B1] else [B0] in
   let (ec : ii) = undefined_int () in
   match typ with
   | Exception_Uncategorized ->
      let (ec : ii) = (0:ii) in
      let (il : bits ty1) = [B1] in
      return (ec,il)
   | Exception_WFxTrap ->
      let (ec : ii) = (1:ii) in
      return (ec,il)
   | Exception_CP15RTTrap ->
      let (ec : ii) = (3:ii) in
      return (ec,il)
   | Exception_CP15RRTTrap ->
      let (ec : ii) = (4:ii) in
      return (ec,il)
   | Exception_CP14RTTrap ->
      let (ec : ii) = (5:ii) in
      return (ec,il)
   | Exception_CP14DTTrap ->
      let (ec : ii) = (6:ii) in
      return (ec,il)
   | Exception_AdvSIMDFPAccessTrap ->
      let (ec : ii) = (7:ii) in
      return (ec,il)
   | Exception_FPIDTrap ->
      let (ec : ii) = (8:ii) in
      return (ec,il)
   | Exception_CP14RRTTrap ->
      let (ec : ii) = (12:ii) in
      return (ec,il)
   | Exception_IllegalState ->
      let (ec : ii) = (14:ii) in
      let (il : bits ty1) = [B1] in
      return (ec,il)
   | Exception_SupervisorCall ->
      let (ec : ii) = (17:ii) in
      return (ec,il)
   | Exception_HypervisorCall ->
      let (ec : ii) = (18:ii) in
      return (ec,il)
   | Exception_MonitorCall ->
      let (ec : ii) = (19:ii) in
      return (ec,il)
   | Exception_InstructionAbort ->
      let (ec : ii) = (32:ii) in
      let (il : bits ty1) = [B1] in
      return (ec,il)
   | Exception_PCAlignment ->
      let (ec : ii) = (34:ii) in
      let (il : bits ty1) = [B1] in
      return (ec,il)
   | Exception_DataAbort ->
      let (ec : ii) = (36:ii) in
      return (ec,il)
   | Exception_FPTrappedException ->
      let (ec : ii) = (40:ii) in
      return (ec,il)
   | _ ->
      Unreachable () >>
      return (ec,il)
   end >>= fun ((ec : ii), (il : bits ty1)) ->
   read_reg PSTATE_ref >>= fun (w__1 : ProcState) ->
   let (ec : ii) =
     if (and_bool
           (or_bool (eq (ex_int ec) (32:ii)) (eq (ex_int ec) (36:ii)))
           (eq_vec w__1.ProcState_EL EL2))
     then
       let (ec : ii) = integerAdd (ex_int ec) (1:ii) in
       ec
     else ec in
   return (ec,il)

val EncodeLDFSC : Fault -> ii -> M (list bitU)

let EncodeLDFSC typ level =
   let (result : bits ty6) = (undefined_vector (6:ii) (undefined_bit ()) : list bitU) in
   match typ with
   | Fault_AddressSize ->
      let result =
        (concat_vec ([B0;B0;B0;B0]) (__GetSlice_int (2:ii) level (0:ii) : list bitU) : list bitU) in
      assert_exp (or_bool
                    (eq level (0:ii))
                    (or_bool (eq level (1:ii)) (or_bool (eq level (2:ii)) (eq level (3:ii))))) "((level == 0) || ((level == 1) || ((level == 2) || (level == 3))))" >>
      return result
   | Fault_AccessFlag ->
      let result =
        (concat_vec ([B0;B0;B1;B0]) (__GetSlice_int (2:ii) level (0:ii) : list bitU) : list bitU) in
      assert_exp (or_bool (eq level (1:ii)) (or_bool (eq level (2:ii)) (eq level (3:ii)))) "((level == 1) || ((level == 2) || (level == 3)))" >>
      return result
   | Fault_Permission ->
      let result =
        (concat_vec ([B0;B0;B1;B1]) (__GetSlice_int (2:ii) level (0:ii) : list bitU) : list bitU) in
      assert_exp (or_bool (eq level (1:ii)) (or_bool (eq level (2:ii)) (eq level (3:ii)))) "((level == 1) || ((level == 2) || (level == 3)))" >>
      return result
   | Fault_Translation ->
      let result =
        (concat_vec ([B0;B0;B0;B1]) (__GetSlice_int (2:ii) level (0:ii) : list bitU) : list bitU) in
      assert_exp (or_bool
                    (eq level (0:ii))
                    (or_bool (eq level (1:ii)) (or_bool (eq level (2:ii)) (eq level (3:ii))))) "((level == 0) || ((level == 1) || ((level == 2) || (level == 3))))" >>
      return result
   | Fault_SyncExternal ->
      let (result : bits ty6) = [B0;B1;B0;B0;B0;B0] in
      return result
   | Fault_SyncExternalOnWalk ->
      let result =
        (concat_vec ([B0;B1;B0;B1]) (__GetSlice_int (2:ii) level (0:ii) : list bitU) : list bitU) in
      assert_exp (or_bool
                    (eq level (0:ii))
                    (or_bool (eq level (1:ii)) (or_bool (eq level (2:ii)) (eq level (3:ii))))) "((level == 0) || ((level == 1) || ((level == 2) || (level == 3))))" >>
      return result
   | Fault_SyncParity ->
      let (result : bits ty6) = [B0;B1;B1;B0;B0;B0] in
      return result
   | Fault_SyncParityOnWalk ->
      let result =
        (concat_vec ([B0;B1;B1;B1]) (__GetSlice_int (2:ii) level (0:ii) : list bitU) : list bitU) in
      assert_exp (or_bool
                    (eq level (0:ii))
                    (or_bool (eq level (1:ii)) (or_bool (eq level (2:ii)) (eq level (3:ii))))) "((level == 0) || ((level == 1) || ((level == 2) || (level == 3))))" >>
      return result
   | Fault_AsyncParity ->
      let (result : bits ty6) = [B0;B1;B1;B0;B0;B1] in
      return result
   | Fault_AsyncExternal ->
      let (result : bits ty6) = [B0;B1;B0;B0;B0;B1] in
      return result
   | Fault_Alignment ->
      let (result : bits ty6) = [B1;B0;B0;B0;B0;B1] in
      return result
   | Fault_Debug ->
      let (result : bits ty6) = [B1;B0;B0;B0;B1;B0] in
      return result
   | Fault_TLBConflict ->
      let (result : bits ty6) = [B1;B1;B0;B0;B0;B0] in
      return result
   | Fault_Lockdown ->
      let (result : bits ty6) = [B1;B1;B0;B1;B0;B0] in
      return result
   | Fault_Exclusive ->
      let (result : bits ty6) = [B1;B1;B0;B1;B0;B1] in
      return result
   | _ ->
      Unreachable () >>
      return result
   end >>= fun (result : bits ty6) ->
   return result

val BigEndianReverse : list bitU -> M (list bitU)

let rec BigEndianReverse value_name =
   assert_exp (or_bool
                 (eq (length value_name) (8:ii))
                 (or_bool
                    (eq (length value_name) (16:ii))
                    (or_bool
                       (eq (length value_name) (32:ii))
                       (or_bool (eq (length value_name) (64:ii)) (eq (length value_name) (128:ii)))))) "" >>
   let half = integerDiv (length value_name) (2:ii) in
   assert_exp true "" >>
   if (eq (length value_name) (8:ii))
   then return value_name
   else
     (BigEndianReverse (slice value_name (0:ii) half : list bitU) : M (list bitU)) >>= fun (w__0 :
       list bitU) ->
     (BigEndianReverse (slice value_name half (integerMinus (length value_name) half) : list bitU) : M (list bitU)) >>= fun (w__1 :
       list bitU) ->
     return (concat_vec w__0 w__1 : list bitU)

val AArch32_ReportHypEntry : ExceptionRecord -> M unit

let AArch32_ReportHypEntry exception =
   let (typ : Exception) = exception.ExceptionRecord_typ in
   let (il : bits ty1) = (undefined_vector (1:ii) (undefined_bit ()) : list bitU) in
   let (ec : ii) = undefined_int () in
   (AArch32_ExceptionClass typ : M ((ii * list bitU))) >>= fun (tup__0, tup__1) ->
   let ec = tup__0 in
   let il = tup__1 in
   let (iss : bits ty25) = exception.ExceptionRecord_syndrome in
   let (il : bits ty1) =
     if (and_bool
           (or_bool (eq (ex_int ec) (36:ii)) (eq (ex_int ec) (37:ii)))
           (eq_vec ([access_vec_dec iss (24:ii)]) ([B0])))
     then
       let (il : bits ty1) = [B1] in
       il
     else il in
   write_reg
     HSR_ref
     (concat_vec (concat_vec (__GetSlice_int (6:ii) ec (0:ii) : list bitU) il : list bitU) iss : list bitU) >>
   (if (or_bool (eq typ Exception_InstructionAbort) (eq typ Exception_PCAlignment))
    then
      write_reg HIFAR_ref (slice exception.ExceptionRecord_vaddress (0:ii) (32:ii) : list bitU) >>
      write_reg HDFAR_ref (undefined_vector (32:ii) (undefined_bit ()) : list bitU)
    else
      if (eq typ Exception_DataAbort)
      then
        write_reg HIFAR_ref (undefined_vector (32:ii) (undefined_bit ()) : list bitU) >>
        write_reg HDFAR_ref (slice exception.ExceptionRecord_vaddress (0:ii) (32:ii) : list bitU)
      else return ()) >>
   if exception.ExceptionRecord_ipavalid
   then
     (read_reg HPFAR_ref : M (list bitU)) >>= fun (w__0 : list bitU) ->
     write_reg
       HPFAR_ref
       (set_slice
          (32:ii)
          (28:ii)
          w__0
          (4:ii)
          (slice exception.ExceptionRecord_ipaddress (12:ii) (28:ii) : list bitU) : list bitU)
   else
     (read_reg HPFAR_ref : M (list bitU)) >>= fun (w__1 : list bitU) ->
     write_reg
       HPFAR_ref
       (set_slice
          (32:ii)
          (28:ii)
          w__1
          (4:ii)
          (undefined_vector (28:ii) (undefined_bit ()) : list bitU) : list bitU)

val Replicate : integer -> list bitU -> M (list bitU)

let Replicate (N__tv : integer) x =
   assert_exp (eq (ex_int (hardware_mod N__tv (length x))) (0:ii)) "((N MOD M) == 0)" >>
   let p = ex_int (integerDiv N__tv (length x)) in
   assert_exp true "" >>
   return (replicate_bits x p : list bitU)

val Zeros__0 : integer -> list bitU

val Zeros__1 : integer -> unit -> list bitU

let Zeros__0 N = (replicate_bits ([B0]) N : list bitU)

let Zeros__1 (N__tv : integer) () = (Zeros__0 N__tv : list bitU)

val ZeroExtend__0 : list bitU -> integer -> M (list bitU)

val ZeroExtend__1 : integer -> list bitU -> M (list bitU)

let ZeroExtend__0 x N =
   assert_exp (gteq N (length x)) "" >>
   return (concat_vec (Zeros__0 (integerMinus N (length x)) : list bitU) x : list bitU)

let ZeroExtend__1 (N__tv : integer) x = (ZeroExtend__0 x N__tv : M (list bitU))

val aset_SP : list bitU -> M unit

let aset_SP value_name =
   assert_exp (or_bool (eq (length value_name) (32:ii)) (eq (length value_name) (64:ii))) "((width == 32) || (width == 64))" >>
   read_reg PSTATE_ref >>= fun (w__0 : ProcState) ->
   if (eq_vec w__0.ProcState_SP ([B0]))
   then
     (ZeroExtend__1 (64:ii) value_name : M (list bitU)) >>= fun (w__1 : bits ty64) ->
     write_reg SP_EL0_ref w__1
   else
     read_reg PSTATE_ref >>= fun (w__2 : ProcState) ->
     let p__287 = w__2.ProcState_EL in
     let _pat_ = p__287 in
     if (eq_vec _pat_ EL0)
     then
       (ZeroExtend__1 (64:ii) value_name : M (list bitU)) >>= fun (w__3 : bits ty64) ->
       write_reg SP_EL0_ref w__3
     else
       if (eq_vec _pat_ EL1)
       then
         (ZeroExtend__1 (64:ii) value_name : M (list bitU)) >>= fun (w__4 : bits ty64) ->
         write_reg SP_EL1_ref w__4
       else
         if (eq_vec _pat_ EL2)
         then
           (ZeroExtend__1 (64:ii) value_name : M (list bitU)) >>= fun (w__5 : bits ty64) ->
           write_reg SP_EL2_ref w__5
         else
           (ZeroExtend__1 (64:ii) value_name : M (list bitU)) >>= fun (w__6 : bits ty64) ->
           write_reg SP_EL3_ref w__6

val LSL_C : list bitU -> ii -> M (list bitU * list bitU)

let LSL_C x shift =
   assert_exp (gt shift (0:ii)) "(shift > 0)" >>
   let extended_x = (concat_vec x (Zeros__0 shift : list bitU) : list bitU) in
   let result = (slice extended_x (0:ii) (length x) : list bitU) in
   let (carry_out : bits ty1) = [access_vec_dec extended_x (length result)] in
   return (result,carry_out)

val LSL : list bitU -> ii -> M (list bitU)

let LSL x shift =
   assert_exp (gteq shift (0:ii)) "(shift >= 0)" >>
   let (__anon1 : bits ty1) = (undefined_vector (1:ii) (undefined_bit ()) : list bitU) in
   let result = (undefined_vector (length x) (undefined_bit ()) : list bitU) in
   (if (eq shift (0:ii))
    then
      let result = x in
      return (__anon1,result)
    else
      (LSL_C x shift : M ((list bitU * list bitU))) >>= fun (tup__0, tup__1) ->
      let result = tup__0 in
      let (__anon1 : bits ty1) = tup__1 in
      return (__anon1,result)) >>= fun ((__anon1 : bits ty1), result) ->
   return result

val LSInstructionSyndrome : unit -> M (list bitU)

let LSInstructionSyndrome () =
   assert_exp false "FALSE" >>
   return (Zeros__0 (11:ii) : list bitU)

val IsZero : list bitU -> bool

let IsZero x = eq_vec x (Zeros__0 (length x) : list bitU)

val AddWithCarry : list bitU -> list bitU -> list bitU -> (list bitU * list bitU)

let AddWithCarry x y carry_in =
   let (unsigned_sum : ii) = integerAdd (integerAdd (uint x) (uint y)) (uint carry_in) in
   let (signed_sum : ii) = integerAdd (integerAdd (sint x) (sint y)) (uint carry_in) in
   let result = (__GetSlice_int (length x) unsigned_sum (0:ii) : list bitU) in
   let (n : bits ty1) = [access_vec_dec result (integerMinus (length result) (1:ii))] in
   let (z : bits ty1) = if (IsZero result) then [B1] else [B0] in
   let (c : bits ty1) = if (eq (uint result) (ex_int unsigned_sum)) then [B0] else [B1] in
   let (v : bits ty1) = if (eq (sint result) (ex_int signed_sum)) then [B0] else [B1] in
   (result,(concat_vec (concat_vec (concat_vec n z : list bitU) c : list bitU) v : list bitU))

val GetPSRFromPSTATE : unit -> M (list bitU)

let GetPSRFromPSTATE () =
   let (spsr : bits ty32) = (Zeros__1 (32:ii) () : list bitU) in
   read_reg PSTATE_ref >>= fun (w__0 : ProcState) ->
   let spsr = (update_subrange_vec_dec spsr (31:ii) (31:ii) w__0.ProcState_N : list bitU) in
   read_reg PSTATE_ref >>= fun (w__1 : ProcState) ->
   let spsr = (update_subrange_vec_dec spsr (30:ii) (30:ii) w__1.ProcState_Z : list bitU) in
   read_reg PSTATE_ref >>= fun (w__2 : ProcState) ->
   let spsr = (update_subrange_vec_dec spsr (29:ii) (29:ii) w__2.ProcState_C : list bitU) in
   read_reg PSTATE_ref >>= fun (w__3 : ProcState) ->
   let spsr = (update_subrange_vec_dec spsr (28:ii) (28:ii) w__3.ProcState_V : list bitU) in
   read_reg PSTATE_ref >>= fun (w__4 : ProcState) ->
   let spsr = (update_subrange_vec_dec spsr (21:ii) (21:ii) w__4.ProcState_SS : list bitU) in
   read_reg PSTATE_ref >>= fun (w__5 : ProcState) ->
   let spsr = (update_subrange_vec_dec spsr (20:ii) (20:ii) w__5.ProcState_IL : list bitU) in
   read_reg PSTATE_ref >>= fun (w__6 : ProcState) ->
   (if (eq_vec w__6.ProcState_nRW ([B1]))
    then
      read_reg PSTATE_ref >>= fun (w__7 : ProcState) ->
      let spsr = (update_subrange_vec_dec spsr (27:ii) (27:ii) w__7.ProcState_Q : list bitU) in
      read_reg PSTATE_ref >>= fun (w__8 : ProcState) ->
      let spsr =
        (update_subrange_vec_dec
           spsr
           (26:ii)
           (25:ii)
           (subrange_vec_dec w__8.ProcState_IT (1:ii) (0:ii) : list bitU) : list bitU) in
      read_reg PSTATE_ref >>= fun (w__9 : ProcState) ->
      let spsr = (update_subrange_vec_dec spsr (19:ii) (16:ii) w__9.ProcState_GE : list bitU) in
      read_reg PSTATE_ref >>= fun (w__10 : ProcState) ->
      let spsr =
        (update_subrange_vec_dec
           spsr
           (15:ii)
           (10:ii)
           (subrange_vec_dec w__10.ProcState_IT (7:ii) (2:ii) : list bitU) : list bitU) in
      read_reg PSTATE_ref >>= fun (w__11 : ProcState) ->
      let spsr = (update_subrange_vec_dec spsr (9:ii) (9:ii) w__11.ProcState_E : list bitU) in
      read_reg PSTATE_ref >>= fun (w__12 : ProcState) ->
      let spsr = (update_subrange_vec_dec spsr (8:ii) (8:ii) w__12.ProcState_A : list bitU) in
      read_reg PSTATE_ref >>= fun (w__13 : ProcState) ->
      let spsr = (update_subrange_vec_dec spsr (7:ii) (7:ii) w__13.ProcState_I : list bitU) in
      read_reg PSTATE_ref >>= fun (w__14 : ProcState) ->
      let spsr = (update_subrange_vec_dec spsr (6:ii) (6:ii) w__14.ProcState_F : list bitU) in
      read_reg PSTATE_ref >>= fun (w__15 : ProcState) ->
      let spsr = (update_subrange_vec_dec spsr (5:ii) (5:ii) w__15.ProcState_T : list bitU) in
      read_reg PSTATE_ref >>= fun (w__16 : ProcState) ->
      read_reg PSTATE_ref >>= fun (w__17 : ProcState) ->
      assert_exp (eq_vec ([access_vec_dec w__16.ProcState_M (4:ii)]) w__17.ProcState_nRW) "(((PSTATE).M)<4> == (PSTATE).nRW)" >>
      read_reg PSTATE_ref >>= fun (w__18 : ProcState) ->
      let (spsr : bits ty32) =
        (update_subrange_vec_dec spsr (4:ii) (0:ii) w__18.ProcState_M : list bitU) in
      return spsr
    else
      read_reg PSTATE_ref >>= fun (w__19 : ProcState) ->
      let spsr = (update_subrange_vec_dec spsr (9:ii) (9:ii) w__19.ProcState_D : list bitU) in
      read_reg PSTATE_ref >>= fun (w__20 : ProcState) ->
      let spsr = (update_subrange_vec_dec spsr (8:ii) (8:ii) w__20.ProcState_A : list bitU) in
      read_reg PSTATE_ref >>= fun (w__21 : ProcState) ->
      let spsr = (update_subrange_vec_dec spsr (7:ii) (7:ii) w__21.ProcState_I : list bitU) in
      read_reg PSTATE_ref >>= fun (w__22 : ProcState) ->
      let spsr = (update_subrange_vec_dec spsr (6:ii) (6:ii) w__22.ProcState_F : list bitU) in
      read_reg PSTATE_ref >>= fun (w__23 : ProcState) ->
      let spsr = (update_subrange_vec_dec spsr (4:ii) (4:ii) w__23.ProcState_nRW : list bitU) in
      read_reg PSTATE_ref >>= fun (w__24 : ProcState) ->
      let spsr = (update_subrange_vec_dec spsr (3:ii) (2:ii) w__24.ProcState_EL : list bitU) in
      read_reg PSTATE_ref >>= fun (w__25 : ProcState) ->
      let (spsr : bits ty32) =
        (update_subrange_vec_dec spsr (0:ii) (0:ii) w__25.ProcState_SP : list bitU) in
      return spsr) >>= fun (spsr : bits ty32) ->
   return spsr

val ExceptionSyndrome : Exception -> ExceptionRecord

let ExceptionSyndrome typ =
   let (r : ExceptionRecord) = undefined_ExceptionRecord () in
   let (r : ExceptionRecord) = <|r with ExceptionRecord_typ = typ|> in
   let (r : ExceptionRecord) =
     <|r with ExceptionRecord_syndrome = (Zeros__1 (25:ii) () : list bitU)|> in
   let (r : ExceptionRecord) =
     <|r with ExceptionRecord_vaddress = (Zeros__1 (64:ii) () : list bitU)|> in
   let (r : ExceptionRecord) = <|r with ExceptionRecord_ipavalid = false|> in
   let (r : ExceptionRecord) =
     <|r with ExceptionRecord_ipaddress = (Zeros__1 (52:ii) () : list bitU)|> in
   r

val SignExtend__0 : list bitU -> integer -> M (list bitU)

val SignExtend__1 : integer -> list bitU -> M (list bitU)

let SignExtend__0 x N =
   assert_exp (gteq N (length x)) "" >>
   return (concat_vec
             (replicate_bits
                ([access_vec_dec x (integerMinus (length x) (1:ii))])
                (integerMinus N (length x)) : list bitU)
             x : list bitU)

let SignExtend__1 (N__tv : integer) x = (SignExtend__0 x N__tv : M (list bitU))

val Ones__0 : integer -> list bitU

val Ones__1 : integer -> unit -> list bitU

let Ones__0 N = (replicate_bits ([B1]) N : list bitU)

let Ones__1 (N__tv : integer) () = (Ones__0 N__tv : list bitU)

val ExcVectorBase : unit -> M (list bitU)

let ExcVectorBase () =
   (read_reg SCTLR_ref : M (list bitU)) >>= fun (w__0 : bits ty32) ->
   if (eq_vec ([access_vec_dec w__0 (13:ii)]) ([B1]))
   then return (concat_vec (Ones__0 (16:ii) : list bitU) (Zeros__0 (16:ii) : list bitU) : list bitU)
   else
     (read_reg VBAR_ref : M (list bitU)) >>= fun (w__1 : bits ty32) ->
     return (concat_vec (slice w__1 (5:ii) (27:ii) : list bitU) (Zeros__0 (5:ii) : list bitU) : list bitU)

val Align__0 : ii -> ii -> ii

val Align__1 : list bitU -> ii -> list bitU

let Align__0 x y = integerDiv (integerMult y x) y

let Align__1 x y = (__GetSlice_int (length x) (Align__0 (uint x) y) (0:ii) : list bitU)

val aset__Mem : AddressDescriptor -> integer -> AccessDescriptor -> list bitU -> M unit

let aset__Mem desc size accdesc value_name =
   assert_exp (or_bool
                 (eq size (1:ii))
                 (or_bool
                    (eq size (2:ii))
                    (or_bool (eq size (4:ii)) (or_bool (eq size (8:ii)) (eq size (16:ii)))))) "((size == 1) || ((size == 2) || ((size == 4) || ((size == 8) || (size == 16)))))" >>
   let (address : bits ty52) = desc.AddressDescriptor_paddress.FullAddress_physicaladdress in
   assert_exp (eq_vec address (Align__1 address size : list bitU)) "(address == Align(address, size))" >>
   if (eq_vec address (hex_slice "0x13000000" (52:ii) (0:ii) : list bitU))
   then
     if (eq (uint value_name) (4:ii))
     then
       let (_ : unit) = prerr_endline "Program exited by writing ^D to TUBE
" in
       exit ()
     else return (putchar (uint (slice value_name (0:ii) (8:ii) : list bitU)))
   else
     (read_reg __Memory_ref : M (list bitU)) >>= fun (w__0 : list bitU) ->
     write_ram (52:ii) size w__0 address value_name

val aget__Mem : AddressDescriptor -> integer -> AccessDescriptor -> M (list bitU)

let aget__Mem desc size accdesc =
   assert_exp (or_bool
                 (eq size (1:ii))
                 (or_bool
                    (eq size (2:ii))
                    (or_bool (eq size (4:ii)) (or_bool (eq size (8:ii)) (eq size (16:ii)))))) "((size == 1) || ((size == 2) || ((size == 4) || ((size == 8) || (size == 16)))))" >>
   let (address : bits ty52) = desc.AddressDescriptor_paddress.FullAddress_physicaladdress in
   assert_exp (eq_vec address (Align__1 address size : list bitU)) "(address == Align(address, size))" >>
   (read_reg __Memory_ref : M (list bitU)) >>= fun (w__0 : list bitU) ->
   (read_ram (52:ii) size w__0 address : M (list bitU))

val aset_X : ii -> list bitU -> M unit

let aset_X n value_name =
   assert_exp (and_bool (gteq (ex_int n) (0:ii)) (lteq (ex_int n) (31:ii))) "((n >= 0) && (n <= 31))" >>
   assert_exp (or_bool (eq (length value_name) (32:ii)) (eq (length value_name) (64:ii))) "((width == 32) || (width == 64))" >>
   if (neq (ex_int n) (31:ii))
   then
     read_reg _R_ref >>= fun (w__0 : list (list bitU)) ->
     (ZeroExtend__0 value_name (64:ii) : M (list bitU)) >>= fun (w__1 : list bitU) ->
     write_reg _R_ref (update_list_dec w__0 n w__1 : list (list bitU))
   else return ()

val aset_ELR__0 : list bitU -> list bitU -> M unit

val aset_ELR__1 : list bitU -> M unit

let aset_ELR__0 el value_name =
   let (r : bits ty64) = value_name in
   let _pat_ = el in
   if (eq_vec _pat_ EL1)
   then write_reg ELR_EL1_ref r
   else
     if (eq_vec _pat_ EL2)
     then write_reg ELR_EL2_ref r
     else if (eq_vec _pat_ EL3) then write_reg ELR_EL3_ref r else Unreachable ()

let aset_ELR__1 value_name =
   read_reg PSTATE_ref >>= fun (w__0 : ProcState) ->
   assert_exp (neq_vec w__0.ProcState_EL EL0) "" >>
   read_reg PSTATE_ref >>= fun (w__1 : ProcState) ->
   aset_ELR__0 w__1.ProcState_EL value_name

val aget_X : integer -> ii -> M (list bitU)

let aget_X (width__tv : integer) n =
   assert_exp (and_bool (gteq n (0:ii)) (lteq n (31:ii))) "((n >= 0) && (n <= 31))" >>
   assert_exp (or_bool
                 (eq width__tv (8:ii))
                 (or_bool
                    (eq width__tv (16:ii))
                    (or_bool (eq width__tv (32:ii)) (eq width__tv (64:ii))))) "((width == 8) || ((width == 16) || ((width == 32) || (width == 64))))" >>
   if (neq n (31:ii))
   then
     read_reg _R_ref >>= fun (w__0 : list (bits ty64)) ->
     return (slice (access_list_dec w__0 n : list bitU) (0:ii) width__tv : list bitU)
   else return (Zeros__0 width__tv : list bitU)

val Prefetch : list bitU -> list bitU -> unit

let Prefetch address prfop =
   let (hint : PrefetchHint) = undefined_PrefetchHint () in
   let (target : ii) = undefined_int () in
   let (stream : bool) = undefined_bool () in
   let b__0 = (slice prfop (3:ii) (2:ii) : list bitU) in
   let (hint : PrefetchHint) =
     if (eq_vec b__0 ([B0;B0]))
     then
       let (hint : PrefetchHint) = Prefetch_READ in
       hint
     else
       let (hint : PrefetchHint) =
         if (eq_vec b__0 ([B0;B1]))
         then
           let (hint : PrefetchHint) = Prefetch_EXEC in
           hint
         else
           let (hint : PrefetchHint) =
             if (eq_vec b__0 ([B1;B0]))
             then
               let (hint : PrefetchHint) = Prefetch_WRITE in
               hint
             else hint in
           hint in
       hint in
   let (target : ii) = uint (slice prfop (1:ii) (2:ii) : list bitU) in
   let (stream : bool) = neq_vec ([access_vec_dec prfop (0:ii)]) ([B0]) in
   let (_ : unit) = Hint_Prefetch address hint target stream in
   ()

val IsSecondStage : FaultRecord -> M bool

let IsSecondStage fault =
   assert_exp (neq fault.FaultRecord_typ Fault_None) "((fault).type != Fault_None)" >>
   return fault.FaultRecord_secondstage

val IsFault : AddressDescriptor -> bool

let IsFault addrdesc = neq addrdesc.AddressDescriptor_fault.FaultRecord_typ Fault_None

val IsExternalSyncAbort__0 : Fault -> M bool

val IsExternalSyncAbort__1 : FaultRecord -> M bool

let IsExternalSyncAbort__0 typ =
   assert_exp (neq typ Fault_None) "" >>
   return (or_bool
             (eq typ Fault_SyncExternal)
             (or_bool
                (eq typ Fault_SyncParity)
                (or_bool (eq typ Fault_SyncExternalOnWalk) (eq typ Fault_SyncParityOnWalk))))

let IsExternalSyncAbort__1 fault = IsExternalSyncAbort__0 fault.FaultRecord_typ

val IsExternalAbort__0 : Fault -> M bool

val IsExternalAbort__1 : FaultRecord -> M bool

let IsExternalAbort__0 typ =
   assert_exp (neq typ Fault_None) "" >>
   return (or_bool
             (eq typ Fault_SyncExternal)
             (or_bool
                (eq typ Fault_SyncParity)
                (or_bool
                   (eq typ Fault_SyncExternalOnWalk)
                   (or_bool
                      (eq typ Fault_SyncParityOnWalk)
                      (or_bool (eq typ Fault_AsyncExternal) (eq typ Fault_AsyncParity))))))

let IsExternalAbort__1 fault = IsExternalAbort__0 fault.FaultRecord_typ

val IsDebugException : FaultRecord -> M bool

let IsDebugException fault =
   assert_exp (neq fault.FaultRecord_typ Fault_None) "((fault).type != Fault_None)" >>
   return (eq fault.FaultRecord_typ Fault_Debug)

val IPAValid : FaultRecord -> M bool

let IPAValid fault =
   assert_exp (neq fault.FaultRecord_typ Fault_None) "((fault).type != Fault_None)" >>
   return (if fault.FaultRecord_s2fs1walk
           then
             or_bool
               (eq fault.FaultRecord_typ Fault_AccessFlag)
               (or_bool
                  (eq fault.FaultRecord_typ Fault_Permission)
                  (or_bool
                     (eq fault.FaultRecord_typ Fault_Translation)
                     (eq fault.FaultRecord_typ Fault_AddressSize)))
           else
           if fault.FaultRecord_secondstage
           then
             or_bool
               (eq fault.FaultRecord_typ Fault_AccessFlag)
               (or_bool
                  (eq fault.FaultRecord_typ Fault_Translation)
                  (eq fault.FaultRecord_typ Fault_AddressSize))
           else false)

val aarch64_integer_arithmetic_addsub_immediate : ii -> integer -> list bitU -> ii -> bool -> bool -> M unit

let aarch64_integer_arithmetic_addsub_immediate d datasize imm n setflags sub_op =
   let dbytes = ex_int (integerDiv datasize (8:ii)) in
   assert_exp true "datasize constraint" >>
   assert_exp true "dbytes constraint" >>
   let result = (undefined_vector datasize (undefined_bit ()) : list bitU) in
   (if (eq n (31:ii))
    then (aget_SP datasize () : M (list bitU))
    else (aget_X datasize n : M (list bitU))) >>= fun operand1 ->
   let operand2 = imm in
   let (nzcv : bits ty4) = (undefined_vector (4:ii) (undefined_bit ()) : list bitU) in
   let (carry_in : bits ty1) = (undefined_vector (1:ii) (undefined_bit ()) : list bitU) in
   let ((carry_in : bits ty1), operand2) =
     if sub_op
     then
       let operand2 = (not_vec operand2 : list bitU) in
       let (carry_in : bits ty1) = [B1] in
       (carry_in,operand2)
     else
       let (carry_in : bits ty1) = [B0] in
       (carry_in,operand2) in
   let (tup__0, tup__1) = (AddWithCarry operand1 operand2 carry_in : (list bitU * list bitU)) in
   let result = tup__0 in
   let nzcv = tup__1 in
   (if setflags
    then
      let (tup__0, tup__1, tup__2, tup__3) =
        ((subrange_vec_dec nzcv (3:ii) (3:ii) : list bitU),(subrange_vec_dec nzcv (2:ii) (2:ii) : list bitU),(subrange_vec_dec
                                                                                                                nzcv
                                                                                                                (1:ii)
                                                                                                                (1:ii) : list bitU),(subrange_vec_dec
                                                                                                                                       nzcv
                                                                                                                                       (0:ii)
                                                                                                                                       (0:ii) : list bitU)) in
      read_reg PSTATE_ref >>= fun (w__2 : ProcState) ->
      write_reg PSTATE_ref <|w__2 with ProcState_N = tup__0|> >>
      read_reg PSTATE_ref >>= fun (w__3 : ProcState) ->
      write_reg PSTATE_ref <|w__3 with ProcState_Z = tup__1|> >>
      read_reg PSTATE_ref >>= fun (w__4 : ProcState) ->
      write_reg PSTATE_ref <|w__4 with ProcState_C = tup__2|> >>
      read_reg PSTATE_ref >>= fun (w__5 : ProcState) ->
      write_reg PSTATE_ref <|w__5 with ProcState_V = tup__3|>
    else return ()) >>
   if (and_bool (eq d (31:ii)) (not setflags))
   then aset_SP result
   else aset_X d result

val HighestELUsingAArch32 : unit -> bool

let HighestELUsingAArch32 () = if (not (HaveAnyAArch32 ())) then false else false

val aget_SCR_GEN : unit -> M (list bitU)

let aget_SCR_GEN () =
   assert_exp (HaveEL EL3) "HaveEL(EL3)" >>
   let (r : bits ty32) = (undefined_vector (32:ii) (undefined_bit ()) : list bitU) in
   (if (HighestELUsingAArch32 ())
    then
      (read_reg SCR_ref : M (list bitU)) >>= fun (w__0 : bits ty32) ->
      let (r : bits ty32) = w__0 in
      return r
    else
      (read_reg SCR_EL3_ref : M (list bitU)) >>= fun (w__1 : bits ty32) ->
      let (r : bits ty32) = w__1 in
      return r) >>= fun (r : bits ty32) ->
   return r

val IsSecureBelowEL3 : unit -> M bool

let IsSecureBelowEL3 () =
   if (HaveEL EL3)
   then
     (aget_SCR_GEN () : M (list bitU)) >>= fun (w__0 : list bitU) ->
     return (eq_vec ([access_vec_dec w__0 (0:ii)]) ([B0]))
   else return (if (HaveEL EL2) then false else false)

val UsingAArch32 : unit -> M bool

let UsingAArch32 () =
   read_reg PSTATE_ref >>= fun (w__0 : ProcState) ->
   let (aarch32 : bool) = eq_vec w__0.ProcState_nRW ([B1]) in
   (if (not (HaveAnyAArch32 ()))
    then assert_exp (not aarch32) "!(aarch32)"
    else return ()) >>
   (if (HighestELUsingAArch32 ())
    then assert_exp aarch32 "aarch32"
    else return ()) >>
   return aarch32

val aset_SPSR : list bitU -> M unit

let aset_SPSR value_name =
   UsingAArch32 () >>= fun (w__0 : bool) ->
   if w__0
   then
     read_reg PSTATE_ref >>= fun (w__1 : ProcState) ->
     let p__286 = w__1.ProcState_M in
     let _pat_ = p__286 in
     if (eq_vec _pat_ M32_FIQ)
     then write_reg SPSR_fiq_ref value_name
     else
       if (eq_vec _pat_ M32_IRQ)
       then write_reg SPSR_irq_ref value_name
       else
         if (eq_vec _pat_ M32_Svc)
         then write_reg SPSR_svc_ref value_name
         else
           if (eq_vec _pat_ M32_Monitor)
           then write_reg SPSR_mon_ref value_name
           else
             if (eq_vec _pat_ M32_Abort)
             then write_reg SPSR_abt_ref value_name
             else
               if (eq_vec _pat_ M32_Hyp)
               then write_reg SPSR_hyp_ref value_name
               else
                 if (eq_vec _pat_ M32_Undef)
                 then write_reg SPSR_und_ref value_name
                 else Unreachable ()
   else
     read_reg PSTATE_ref >>= fun (w__2 : ProcState) ->
     let p__285 = w__2.ProcState_EL in
     let _pat_ = p__285 in
     if (eq_vec _pat_ EL1)
     then write_reg SPSR_EL1_ref value_name
     else
       if (eq_vec _pat_ EL2)
       then write_reg SPSR_EL2_ref value_name
       else if (eq_vec _pat_ EL3) then write_reg SPSR_EL3_ref value_name else Unreachable ()

val IsSecure : unit -> M bool

let IsSecure () =
   UsingAArch32 () >>= fun (w__0 : bool) ->
   read_reg PSTATE_ref >>= fun (w__1 : ProcState) ->
   if (and_bool (and_bool (HaveEL EL3) (not w__0)) (eq_vec w__1.ProcState_EL EL3))
   then return true
   else
     UsingAArch32 () >>= fun (w__2 : bool) ->
     read_reg PSTATE_ref >>= fun (w__3 : ProcState) ->
     if (and_bool (and_bool (HaveEL EL3) w__2) (eq_vec w__3.ProcState_M M32_Monitor))
     then return true
     else IsSecureBelowEL3 ()

val CurrentInstrSet : unit -> M InstrSet

let CurrentInstrSet () =
   let (result : InstrSet) = undefined_InstrSet () in
   UsingAArch32 () >>= fun (w__0 : bool) ->
   (if w__0
    then
      read_reg PSTATE_ref >>= fun (w__1 : ProcState) ->
      let (result : InstrSet) =
        if (eq_vec w__1.ProcState_T ([B0]))
        then InstrSet_A32
        else InstrSet_T32 in
      return result
    else
      let (result : InstrSet) = InstrSet_A64 in
      return result) >>= fun (result : InstrSet) ->
   return result

val AArch32_ExecutingCP10or11Instr : unit -> M bool

let AArch32_ExecutingCP10or11Instr () =
   (ThisInstr () : M (list bitU)) >>= fun (instr : bits ty32) ->
   CurrentInstrSet () >>= fun (instr_set : InstrSet) ->
   assert_exp (or_bool (eq instr_set InstrSet_A32) (eq instr_set InstrSet_T32)) "((instr_set == InstrSet_A32) || (instr_set == InstrSet_T32))" >>
   return (if (eq instr_set InstrSet_A32)
           then
             and_bool
               (or_bool
                  (eq_vec (slice instr (24:ii) (4:ii) : list bitU) ([B1;B1;B1;B0]))
                  (eq_vec (slice instr (25:ii) (3:ii) : list bitU) ([B1;B1;B0])))
               (eq_vec
                  (and_vec (slice instr (8:ii) (4:ii) : list bitU) ([B1;B1;B1;B0]) : list bitU)
                  ([B1;B0;B1;B0]))
           else
             and_bool
               (and_bool
                  (eq_vec
                     (and_vec (slice instr (28:ii) (4:ii) : list bitU) ([B1;B1;B1;B0]) : list bitU)
                     ([B1;B1;B1;B0]))
                  (or_bool
                     (eq_vec (slice instr (24:ii) (4:ii) : list bitU) ([B1;B1;B1;B0]))
                     (eq_vec (slice instr (25:ii) (3:ii) : list bitU) ([B1;B1;B0]))))
               (eq_vec
                  (and_vec (slice instr (8:ii) (4:ii) : list bitU) ([B1;B1;B1;B0]) : list bitU)
                  ([B1;B0;B1;B0])))

val HaveAArch32EL : list bitU -> bool

let HaveAArch32EL el =
   if (not (HaveEL el))
   then false
   else
   if (not (HaveAnyAArch32 ()))
   then false
   else
   if (HighestELUsingAArch32 ())
   then true
   else
   if (eq_vec el (HighestEL () : list bitU))
   then false
   else if (eq_vec el EL0) then true else true

val ELStateUsingAArch32K : list bitU -> bool -> M (bool * bool)

let ELStateUsingAArch32K el secure =
   let (aarch32 : bool) = undefined_bool () in
   let (known : bool) = true in
   let (aarch32_at_el1 : bool) = undefined_bool () in
   let (aarch32_below_el3 : bool) = undefined_bool () in
   (if (not (HaveAArch32EL el))
    then
      let (aarch32 : bool) = false in
      return (aarch32,aarch32_at_el1,aarch32_below_el3,known)
    else
      (if (HighestELUsingAArch32 ())
       then
         let (aarch32 : bool) = true in
         return (aarch32,aarch32_at_el1,aarch32_below_el3,known)
       else
         (read_reg SCR_EL3_ref : M (list bitU)) >>= fun (w__0 : bits ty32) ->
         let aarch32_below_el3 =
           and_bool (HaveEL EL3) (eq_vec ([access_vec_dec w__0 (10:ii)]) ([B0])) in
         (read_reg HCR_EL2_ref : M (list bitU)) >>= fun (w__1 : bits ty64) ->
         (read_reg HCR_EL2_ref : M (list bitU)) >>= fun (w__2 : bits ty64) ->
         (read_reg HCR_EL2_ref : M (list bitU)) >>= fun (w__3 : bits ty64) ->
         let aarch32_at_el1 =
           or_bool
             aarch32_below_el3
             (and_bool
                (and_bool
                   (and_bool (HaveEL EL2) (not secure))
                   (eq_vec ([access_vec_dec w__1 (31:ii)]) ([B0])))
                (not
                   (and_bool
                      (and_bool
                         (eq_vec ([access_vec_dec w__2 (34:ii)]) ([B1]))
                         (eq_vec ([access_vec_dec w__3 (27:ii)]) ([B1])))
                      (HaveVirtHostExt ())))) in
         (if (and_bool (eq_vec el EL0) (not aarch32_at_el1))
          then
            read_reg PSTATE_ref >>= fun (w__4 : ProcState) ->
            (if (eq_vec w__4.ProcState_EL EL0)
             then
               read_reg PSTATE_ref >>= fun (w__5 : ProcState) ->
               let (aarch32 : bool) = eq_vec w__5.ProcState_nRW ([B1]) in
               return (aarch32,known)
             else
               let (known : bool) = false in
               return (aarch32,known)) >>= fun ((aarch32 : bool), (known : bool)) ->
            return (aarch32,known)
          else
            let (aarch32 : bool) =
              or_bool
                (and_bool aarch32_below_el3 (neq_vec el EL3))
                (and_bool aarch32_at_el1 (or_bool (eq_vec el EL1) (eq_vec el EL0))) in
            return (aarch32,known)) >>= fun ((aarch32 : bool), (known : bool)) ->
         return (aarch32,aarch32_at_el1,aarch32_below_el3,known)) >>= fun ((aarch32 : bool), (aarch32_at_el1 :
        bool), (aarch32_below_el3 : bool), (known : bool)) ->
      return (aarch32,aarch32_at_el1,aarch32_below_el3,known)) >>= fun ((aarch32 : bool), (aarch32_at_el1 :
     bool), (aarch32_below_el3 : bool), (known : bool)) ->
   let (aarch32 : bool) =
     if (not known)
     then
       let (aarch32 : bool) = undefined_bool () in
       aarch32
     else aarch32 in
   return (known,aarch32)

val ELStateUsingAArch32 : list bitU -> bool -> M bool

let ELStateUsingAArch32 el secure =
   let (aarch32 : bool) = undefined_bool () in
   let (known : bool) = undefined_bool () in
   ELStateUsingAArch32K el secure >>= fun (tup__0, tup__1) ->
   let known = tup__0 in
   let aarch32 = tup__1 in
   assert_exp known "known" >>
   return aarch32

val ELUsingAArch32 : list bitU -> M bool

let ELUsingAArch32 el =
   IsSecureBelowEL3 () >>= fun (w__0 : bool) ->
   ELStateUsingAArch32 el w__0

val ELIsInHost : list bitU -> M bool

let ELIsInHost el =
   IsSecureBelowEL3 () >>= fun (w__0 : bool) ->
   ELUsingAArch32 EL2 >>= fun (w__1 : bool) ->
   (read_reg HCR_EL2_ref : M (list bitU)) >>= fun (w__2 : bits ty64) ->
   (read_reg HCR_EL2_ref : M (list bitU)) >>= fun (w__3 : bits ty64) ->
   return (and_bool
             (and_bool
                (and_bool (and_bool (not w__0) (HaveVirtHostExt ())) (not w__1))
                (eq_vec ([access_vec_dec w__2 (34:ii)]) ([B1])))
             (or_bool
                (eq_vec el EL2)
                (and_bool (eq_vec el EL0) (eq_vec ([access_vec_dec w__3 (27:ii)]) ([B1])))))

val S1TranslationRegime__0 : list bitU -> M (list bitU)

val S1TranslationRegime__1 : unit -> M (list bitU)

let S1TranslationRegime__0 el =
   if (neq_vec el EL0)
   then return el
   else
     ELUsingAArch32 EL3 >>= fun (w__0 : bool) ->
     (read_reg SCR_ref : M (list bitU)) >>= fun (w__1 : bits ty32) ->
     if (and_bool (and_bool (HaveEL EL3) w__0) (eq_vec ([access_vec_dec w__1 (0:ii)]) ([B0])))
     then return EL3
     else
       ELIsInHost el >>= fun (w__2 : bool) ->
       return (if (and_bool (HaveVirtHostExt ()) w__2)
               then EL2
               else EL1)

let S1TranslationRegime__1 () =
   read_reg PSTATE_ref >>= fun (w__0 : ProcState) ->
   (S1TranslationRegime__0 w__0.ProcState_EL : M (list bitU))

val aset_FAR__0 : list bitU -> list bitU -> M unit

val aset_FAR__1 : list bitU -> M unit

let aset_FAR__0 regime value_name =
   let (r : bits ty64) = value_name in
   let _pat_ = regime in
   if (eq_vec _pat_ EL1)
   then write_reg FAR_EL1_ref r
   else
     if (eq_vec _pat_ EL2)
     then write_reg FAR_EL2_ref r
     else if (eq_vec _pat_ EL3) then write_reg FAR_EL3_ref r else Unreachable ()

let aset_FAR__1 value_name =
   (S1TranslationRegime__1 () : M (list bitU)) >>= fun (w__0 : list bitU) ->
   aset_FAR__0 w__0 value_name

val aset_ESR__0 : list bitU -> list bitU -> M unit

val aset_ESR__1 : list bitU -> M unit

let aset_ESR__0 regime value_name =
   let (r : bits ty32) = value_name in
   let _pat_ = regime in
   if (eq_vec _pat_ EL1)
   then write_reg ESR_EL1_ref r
   else
     if (eq_vec _pat_ EL2)
     then write_reg ESR_EL2_ref r
     else if (eq_vec _pat_ EL3) then write_reg ESR_EL3_ref r else Unreachable ()

let aset_ESR__1 value_name =
   (S1TranslationRegime__1 () : M (list bitU)) >>= fun (w__0 : list bitU) ->
   aset_ESR__0 w__0 value_name

val aget_VBAR__0 : list bitU -> M (list bitU)

val aget_VBAR__1 : unit -> M (list bitU)

let aget_VBAR__0 regime =
   let (r : bits ty64) = (undefined_vector (64:ii) (undefined_bit ()) : list bitU) in
   let _pat_ = regime in
   (if (eq_vec _pat_ EL1)
    then
      (read_reg VBAR_EL1_ref : M (list bitU)) >>= fun (w__0 : bits ty64) ->
      let (r : bits ty64) = w__0 in
      return r
    else
      (if (eq_vec _pat_ EL2)
       then
         (read_reg VBAR_EL2_ref : M (list bitU)) >>= fun (w__1 : bits ty64) ->
         let (r : bits ty64) = w__1 in
         return r
       else
         (if (eq_vec _pat_ EL3)
          then
            (read_reg VBAR_EL3_ref : M (list bitU)) >>= fun (w__2 : bits ty64) ->
            let (r : bits ty64) = w__2 in
            return r
          else
            Unreachable () >>
            return r) >>= fun (r : bits ty64) ->
         return r) >>= fun (r : bits ty64) ->
      return r) >>= fun (r : bits ty64) ->
   return r

let aget_VBAR__1 () =
   (S1TranslationRegime__1 () : M (list bitU)) >>= fun (w__0 : list bitU) ->
   (aget_VBAR__0 w__0 : M (list bitU))

val aget_SCTLR__0 : list bitU -> M (list bitU)

val aget_SCTLR__1 : unit -> M (list bitU)

let aget_SCTLR__0 regime =
   let (r : bits ty32) = (undefined_vector (32:ii) (undefined_bit ()) : list bitU) in
   let _pat_ = regime in
   (if (eq_vec _pat_ EL1)
    then
      (read_reg SCTLR_EL1_ref : M (list bitU)) >>= fun (w__0 : bits ty32) ->
      let (r : bits ty32) = w__0 in
      return r
    else
      (if (eq_vec _pat_ EL2)
       then
         (read_reg SCTLR_EL2_ref : M (list bitU)) >>= fun (w__1 : bits ty32) ->
         let (r : bits ty32) = w__1 in
         return r
       else
         (if (eq_vec _pat_ EL3)
          then
            (read_reg SCTLR_EL3_ref : M (list bitU)) >>= fun (w__2 : bits ty32) ->
            let (r : bits ty32) = w__2 in
            return r
          else
            Unreachable () >>
            return r) >>= fun (r : bits ty32) ->
         return r) >>= fun (r : bits ty32) ->
      return r) >>= fun (r : bits ty32) ->
   return r

let aget_SCTLR__1 () =
   (S1TranslationRegime__1 () : M (list bitU)) >>= fun (w__0 : list bitU) ->
   (aget_SCTLR__0 w__0 : M (list bitU))

val BigEndian : unit -> M bool

let BigEndian () =
   let (bigend : bool) = undefined_bool () in
   UsingAArch32 () >>= fun (w__0 : bool) ->
   (if w__0
    then
      read_reg PSTATE_ref >>= fun (w__1 : ProcState) ->
      let (bigend : bool) = neq_vec w__1.ProcState_E ([B0]) in
      return bigend
    else
      read_reg PSTATE_ref >>= fun (w__2 : ProcState) ->
      (if (eq_vec w__2.ProcState_EL EL0)
       then
         (aget_SCTLR__1 () : M (list bitU)) >>= fun (w__3 : list bitU) ->
         let (bigend : bool) = neq_vec ([access_vec_dec w__3 (24:ii)]) ([B0]) in
         return bigend
       else
         (aget_SCTLR__1 () : M (list bitU)) >>= fun (w__4 : list bitU) ->
         let (bigend : bool) = neq_vec ([access_vec_dec w__4 (25:ii)]) ([B0]) in
         return bigend) >>= fun (bigend : bool) ->
      return bigend) >>= fun (bigend : bool) ->
   return bigend

val IsInHost : unit -> M bool

let IsInHost () =
   read_reg PSTATE_ref >>= fun (w__0 : ProcState) ->
   ELIsInHost w__0.ProcState_EL

val BadMode : list bitU -> bool

let BadMode mode =
   let (valid_name : bool) = undefined_bool () in
   let _pat_ = mode in
   let (valid_name : bool) =
     if (eq_vec _pat_ M32_Monitor)
     then
       let (valid_name : bool) = HaveAArch32EL EL3 in
       valid_name
     else
       let (valid_name : bool) =
         if (eq_vec _pat_ M32_Hyp)
         then
           let (valid_name : bool) = HaveAArch32EL EL2 in
           valid_name
         else
           let (valid_name : bool) =
             if (eq_vec _pat_ M32_FIQ)
             then
               let (valid_name : bool) = HaveAArch32EL EL1 in
               valid_name
             else
               let (valid_name : bool) =
                 if (eq_vec _pat_ M32_IRQ)
                 then
                   let (valid_name : bool) = HaveAArch32EL EL1 in
                   valid_name
                 else
                   let (valid_name : bool) =
                     if (eq_vec _pat_ M32_Svc)
                     then
                       let (valid_name : bool) = HaveAArch32EL EL1 in
                       valid_name
                     else
                       let (valid_name : bool) =
                         if (eq_vec _pat_ M32_Abort)
                         then
                           let (valid_name : bool) = HaveAArch32EL EL1 in
                           valid_name
                         else
                           let (valid_name : bool) =
                             if (eq_vec _pat_ M32_Undef)
                             then
                               let (valid_name : bool) = HaveAArch32EL EL1 in
                               valid_name
                             else
                               let (valid_name : bool) =
                                 if (eq_vec _pat_ M32_System)
                                 then
                                   let (valid_name : bool) = HaveAArch32EL EL1 in
                                   valid_name
                                 else
                                   let (valid_name : bool) =
                                     if (eq_vec _pat_ M32_User)
                                     then
                                       let (valid_name : bool) = HaveAArch32EL EL0 in
                                       valid_name
                                     else
                                       let (valid_name : bool) = false in
                                       valid_name in
                                   valid_name in
                               valid_name in
                           valid_name in
                       valid_name in
                   valid_name in
               valid_name in
           valid_name in
       valid_name in
   not valid_name

val aset_Rmode : ii -> list bitU -> list bitU -> M unit

let aset_Rmode n mode value_name =
   assert_exp (and_bool (gteq (ex_int n) (0:ii)) (lteq (ex_int n) (14:ii))) "((n >= 0) && (n <= 14))" >>
   IsSecure () >>= fun (w__0 : bool) ->
   (if (not w__0)
    then assert_exp (neq_vec mode M32_Monitor) "(mode != M32_Monitor)"
    else return ()) >>
   assert_exp (not (BadMode mode)) "!(BadMode(mode))" >>
   if (eq_vec mode M32_Monitor)
   then
     if (eq (ex_int n) (13:ii))
     then write_reg SP_mon_ref value_name
     else
       if (eq (ex_int n) (14:ii))
       then write_reg LR_mon_ref value_name
       else
         read_reg _R_ref >>= fun (w__1 : list (bits ty64)) ->
         let (__tmp_1 : bits ty64) = (access_list_dec w__1 n : list bitU) in
         let __tmp_1 = (update_subrange_vec_dec __tmp_1 (31:ii) (0:ii) value_name : list bitU) in
         read_reg _R_ref >>= fun (w__2 : list (list bitU)) ->
         write_reg _R_ref (update_list_dec w__2 n __tmp_1 : list (list bitU))
   else
     ConstrainUnpredictableBool Unpredictable_ZEROUPPER >>= fun (w__3 : bool) ->
     if (and_bool (not (HighestELUsingAArch32 ())) w__3)
     then
       read_reg _R_ref >>= fun (w__4 : list (list bitU)) ->
       LookUpRIndex n mode >>= fun (w__5 : ii) ->
       (ZeroExtend__0 value_name (64:ii) : M (list bitU)) >>= fun (w__6 : list bitU) ->
       write_reg _R_ref (update_list_dec w__4 w__5 w__6 : list (list bitU))
     else
       read_reg _R_ref >>= fun (w__7 : list (bits ty64)) ->
       LookUpRIndex n mode >>= fun (w__8 : ii) ->
       let (__tmp_2 : bits ty64) = (access_list_dec w__7 w__8 : list bitU) in
       let __tmp_2 = (update_subrange_vec_dec __tmp_2 (31:ii) (0:ii) value_name : list bitU) in
       read_reg _R_ref >>= fun (w__9 : list (list bitU)) ->
       LookUpRIndex n mode >>= fun (w__10 : ii) ->
       write_reg _R_ref (update_list_dec w__9 w__10 __tmp_2 : list (list bitU))

val aset_R : ii -> list bitU -> M unit

let aset_R n value_name =
   read_reg PSTATE_ref >>= fun (w__0 : ProcState) ->
   aset_Rmode n w__0.ProcState_M value_name

val ELFromM32 : list bitU -> M (bool * list bitU)

let ELFromM32 mode =
   let (el : bits ty2) = (undefined_vector (2:ii) (undefined_bit ()) : list bitU) in
   let (valid_name : bool) = not (BadMode mode) in
   let _pat_ = mode in
   (if (eq_vec _pat_ M32_Monitor)
    then
      let (el : bits ty2) = EL3 in
      return (el,valid_name)
    else
      (if (eq_vec _pat_ M32_Hyp)
       then
         let el = EL2 in
         (aget_SCR_GEN () : M (list bitU)) >>= fun (w__0 : list bitU) ->
         let (valid_name : bool) =
           and_bool
             valid_name
             (or_bool (not (HaveEL EL3)) (eq_vec ([access_vec_dec w__0 (0:ii)]) ([B1]))) in
         return (el,valid_name)
       else
         (if (eq_vec _pat_ M32_FIQ)
          then
            (read_reg SCR_ref : M (list bitU)) >>= fun (w__1 : bits ty32) ->
            let (el : bits ty2) =
              if (and_bool
                    (and_bool (HaveEL EL3) (HighestELUsingAArch32 ()))
                    (eq_vec ([access_vec_dec w__1 (0:ii)]) ([B0])))
              then EL3
              else EL1 in
            return (el,valid_name)
          else
            (if (eq_vec _pat_ M32_IRQ)
             then
               (read_reg SCR_ref : M (list bitU)) >>= fun (w__2 : bits ty32) ->
               let (el : bits ty2) =
                 if (and_bool
                       (and_bool (HaveEL EL3) (HighestELUsingAArch32 ()))
                       (eq_vec ([access_vec_dec w__2 (0:ii)]) ([B0])))
                 then EL3
                 else EL1 in
               return (el,valid_name)
             else
               (if (eq_vec _pat_ M32_Svc)
                then
                  (read_reg SCR_ref : M (list bitU)) >>= fun (w__3 : bits ty32) ->
                  let (el : bits ty2) =
                    if (and_bool
                          (and_bool (HaveEL EL3) (HighestELUsingAArch32 ()))
                          (eq_vec ([access_vec_dec w__3 (0:ii)]) ([B0])))
                    then EL3
                    else EL1 in
                  return (el,valid_name)
                else
                  (if (eq_vec _pat_ M32_Abort)
                   then
                     (read_reg SCR_ref : M (list bitU)) >>= fun (w__4 : bits ty32) ->
                     let (el : bits ty2) =
                       if (and_bool
                             (and_bool (HaveEL EL3) (HighestELUsingAArch32 ()))
                             (eq_vec ([access_vec_dec w__4 (0:ii)]) ([B0])))
                       then EL3
                       else EL1 in
                     return (el,valid_name)
                   else
                     (if (eq_vec _pat_ M32_Undef)
                      then
                        (read_reg SCR_ref : M (list bitU)) >>= fun (w__5 : bits ty32) ->
                        let (el : bits ty2) =
                          if (and_bool
                                (and_bool (HaveEL EL3) (HighestELUsingAArch32 ()))
                                (eq_vec ([access_vec_dec w__5 (0:ii)]) ([B0])))
                          then EL3
                          else EL1 in
                        return (el,valid_name)
                      else
                        (if (eq_vec _pat_ M32_System)
                         then
                           (read_reg SCR_ref : M (list bitU)) >>= fun (w__6 : bits ty32) ->
                           let (el : bits ty2) =
                             if (and_bool
                                   (and_bool (HaveEL EL3) (HighestELUsingAArch32 ()))
                                   (eq_vec ([access_vec_dec w__6 (0:ii)]) ([B0])))
                             then EL3
                             else EL1 in
                           return (el,valid_name)
                         else
                           let ((el : bits ty2), (valid_name : bool)) =
                             if (eq_vec _pat_ M32_User)
                             then
                               let (el : bits ty2) = EL0 in
                               (el,valid_name)
                             else
                               let (valid_name : bool) = false in
                               (el,valid_name) in
                           return (el,valid_name)) >>= fun ((el : bits ty2), (valid_name : bool)) ->
                        return (el,valid_name)) >>= fun ((el : bits ty2), (valid_name : bool)) ->
                     return (el,valid_name)) >>= fun ((el : bits ty2), (valid_name : bool)) ->
                  return (el,valid_name)) >>= fun ((el : bits ty2), (valid_name : bool)) ->
               return (el,valid_name)) >>= fun ((el : bits ty2), (valid_name : bool)) ->
            return (el,valid_name)) >>= fun ((el : bits ty2), (valid_name : bool)) ->
         return (el,valid_name)) >>= fun ((el : bits ty2), (valid_name : bool)) ->
      return (el,valid_name)) >>= fun ((el : bits ty2), (valid_name : bool)) ->
   let (el : bits ty2) =
     if (not valid_name)
     then
       let (el : bits ty2) = (undefined_vector (2:ii) (undefined_bit ()) : list bitU) in
       el
     else el in
   return (valid_name,el)

val AArch32_WriteMode : list bitU -> M unit

let AArch32_WriteMode mode =
   let (el : bits ty2) = (undefined_vector (2:ii) (undefined_bit ()) : list bitU) in
   let (valid_name : bool) = undefined_bool () in
   (ELFromM32 mode : M ((bool * list bitU))) >>= fun (tup__0, tup__1) ->
   let valid_name = tup__0 in
   let el = tup__1 in
   assert_exp valid_name "valid" >>
   read_reg PSTATE_ref >>= fun (w__0 : ProcState) ->
   write_reg PSTATE_ref <|w__0 with ProcState_M = mode|> >>
   read_reg PSTATE_ref >>= fun (w__1 : ProcState) ->
   write_reg PSTATE_ref <|w__1 with ProcState_EL = el|> >>
   read_reg PSTATE_ref >>= fun (w__2 : ProcState) ->
   write_reg PSTATE_ref <|w__2 with ProcState_nRW = ([B1])|> >>
   read_reg PSTATE_ref >>= fun (w__3 : ProcState) ->
   write_reg
     PSTATE_ref
     <|w__3 with
       ProcState_SP =
         (if (or_bool (eq_vec mode M32_User) (eq_vec mode M32_System))
          then [B0]
          else [B1])|>

val AddrTop : list bitU -> bool -> list bitU -> M ii

let AddrTop address IsInstr el =
   assert_exp (HaveEL el) "HaveEL(el)" >>
   (S1TranslationRegime__0 el : M (list bitU)) >>= fun (regime : bits ty2) ->
   let (tbid : bits ty1) = (undefined_vector (1:ii) (undefined_bit ()) : list bitU) in
   let (tbi : bits ty1) = (undefined_vector (1:ii) (undefined_bit ()) : list bitU) in
   ELUsingAArch32 regime >>= fun (w__0 : bool) ->
   (if w__0
    then return ((31:ii),tbi,tbid)
    else
      let _pat_ = regime in
      (if (eq_vec _pat_ EL1)
       then
         (if (eq_vec ([access_vec_dec address (55:ii)]) ([B1]))
          then
            (read_reg TCR_EL1_ref : M (list bitU)) >>= fun (w__1 : bits ty64) ->
            return ([access_vec_dec w__1 (38:ii)])
          else
            (read_reg TCR_EL1_ref : M (list bitU)) >>= fun (w__2 : bits ty64) ->
            return ([access_vec_dec w__2 (37:ii)])) >>= fun (w__3 : list bitU) ->
         let tbi = w__3 in
         (if (HavePACExt ())
          then
            (if (eq_vec ([access_vec_dec address (55:ii)]) ([B1]))
             then
               (read_reg TCR_EL1_ref : M (list bitU)) >>= fun (w__4 : bits ty64) ->
               return ([access_vec_dec w__4 (52:ii)])
             else
               (read_reg TCR_EL1_ref : M (list bitU)) >>= fun (w__5 : bits ty64) ->
               return ([access_vec_dec w__5 (51:ii)])) >>= fun (w__6 : list bitU) ->
            let (tbid : bits ty1) = w__6 in
            return tbid
          else return tbid) >>= fun (tbid : bits ty1) ->
         return (tbi,tbid)
       else
         (if (eq_vec _pat_ EL2)
          then
            ELIsInHost el >>= fun (w__7 : bool) ->
            (if (and_bool (HaveVirtHostExt ()) w__7)
             then
               (if (eq_vec ([access_vec_dec address (55:ii)]) ([B1]))
                then
                  (read_reg TCR_EL2_ref : M (list bitU)) >>= fun (w__8 : bits ty64) ->
                  return ([access_vec_dec w__8 (38:ii)])
                else
                  (read_reg TCR_EL2_ref : M (list bitU)) >>= fun (w__9 : bits ty64) ->
                  return ([access_vec_dec w__9 (37:ii)])) >>= fun (w__10 : list bitU) ->
               let tbi = w__10 in
               (if (HavePACExt ())
                then
                  (if (eq_vec ([access_vec_dec address (55:ii)]) ([B1]))
                   then
                     (read_reg TCR_EL2_ref : M (list bitU)) >>= fun (w__11 : bits ty64) ->
                     return ([access_vec_dec w__11 (52:ii)])
                   else
                     (read_reg TCR_EL2_ref : M (list bitU)) >>= fun (w__12 : bits ty64) ->
                     return ([access_vec_dec w__12 (51:ii)])) >>= fun (w__13 : list bitU) ->
                  let (tbid : bits ty1) = w__13 in
                  return tbid
                else return tbid) >>= fun (tbid : bits ty1) ->
               return (tbi,tbid)
             else
               (read_reg TCR_EL2_ref : M (list bitU)) >>= fun (w__14 : bits ty64) ->
               let tbi = [access_vec_dec w__14 (20:ii)] in
               (if (HavePACExt ())
                then
                  (read_reg TCR_EL2_ref : M (list bitU)) >>= fun (w__15 : bits ty64) ->
                  let (tbid : bits ty1) = [access_vec_dec w__15 (29:ii)] in
                  return tbid
                else return tbid) >>= fun (tbid : bits ty1) ->
               return (tbi,tbid)) >>= fun ((tbi : bits ty1), (tbid : bits ty1)) ->
            return (tbi,tbid)
          else
            (read_reg TCR_EL3_ref : M (list bitU)) >>= fun (w__16 : bits ty32) ->
            let tbi = [access_vec_dec w__16 (20:ii)] in
            (if (HavePACExt ())
             then
               (read_reg TCR_EL3_ref : M (list bitU)) >>= fun (w__17 : bits ty32) ->
               let (tbid : bits ty1) = [access_vec_dec w__17 (29:ii)] in
               return tbid
             else return tbid) >>= fun (tbid : bits ty1) ->
            return (tbi,tbid)) >>= fun ((tbi : bits ty1), (tbid : bits ty1)) ->
         return (tbi,tbid)) >>= fun ((tbi : bits ty1), (tbid : bits ty1)) ->
      return (if (and_bool
                    (eq_vec tbi ([B1]))
                    (or_bool (or_bool (not (HavePACExt ())) (eq_vec tbid ([B0]))) (not IsInstr)))
      then (55:ii)
      else (63:ii),tbi,tbid)) >>= fun ((w__18 : ii), (tbi : bits ty1), (tbid : bits ty1)) ->
   return w__18

val AArch64_TranslateAddress : list bitU -> AccType -> bool -> bool -> ii -> M AddressDescriptor

val AArch64_NoFault : unit -> FaultRecord

let AArch64_NoFault () =
   let (ipaddress : bits ty52) = (undefined_vector (52:ii) (undefined_bit ()) : list bitU) in
   let (level : ii) = undefined_int () in
   let (acctype : AccType) = AccType_NORMAL in
   let (iswrite : bool) = undefined_bool () in
   let (extflag : bits ty1) = (undefined_vector (1:ii) (undefined_bit ()) : list bitU) in
   let (errortype : bits ty2) = (undefined_vector (2:ii) (undefined_bit ()) : list bitU) in
   let (secondstage : bool) = false in
   let (s2fs1walk : bool) = false in
   AArch64_CreateFaultRecord
     Fault_None
     ipaddress
     level
     acctype
     iswrite
     extflag
     errortype
     secondstage
     s2fs1walk

let AArch64_TranslateAddress vaddress acctype iswrite wasaligned size =
   (ZeroExtend__1 (64:ii) vaddress : M (list bitU)) >>= fun (w__0 : bits ty64) ->
   return (<| AddressDescriptor_fault = (AArch64_NoFault ()); 
              AddressDescriptor_memattrs =
                (<| MemoryAttributes_typ = MemType_Normal; 
                    MemoryAttributes_device = DeviceType_GRE; 
                    MemoryAttributes_inner =
                      (<| MemAttrHints_attrs = ([B0;B0]); 
                          MemAttrHints_hints = ([B0;B0]); 
                          MemAttrHints_transient = false |>); 
                    MemoryAttributes_outer =
                      (<| MemAttrHints_attrs = ([B0;B0]); 
                          MemAttrHints_hints = ([B0;B0]); 
                          MemAttrHints_transient = false |>); 
                    MemoryAttributes_shareable = true; 
                    MemoryAttributes_outershareable = true |>); 
              AddressDescriptor_paddress =
                (<| FullAddress_physicaladdress = (slice vaddress (0:ii) (52:ii) : list bitU) |>); 
              AddressDescriptor_vaddress = w__0 |>)

val AArch64_MaybeZeroRegisterUppers : unit -> M unit

let AArch64_MaybeZeroRegisterUppers () =
   UsingAArch32 () >>= fun (w__0 : bool) ->
   assert_exp w__0 "UsingAArch32()" >>
   let (include_R15_name : bool) = undefined_bool () in
   let (last : integer) = undefined_range (14:ii) (30:ii) in
   let (first : integer) = (0:ii) in
   read_reg PSTATE_ref >>= fun (w__1 : ProcState) ->
   ELUsingAArch32 EL1 >>= fun (w__2 : bool) ->
   (if (and_bool (eq_vec w__1.ProcState_EL EL0) (not w__2))
    then
      let (first : integer) = (0:ii) in
      let (last : integer) = (14:ii) in
      let (include_R15_name : bool) = false in
      return (first,include_R15_name,last)
    else
      read_reg PSTATE_ref >>= fun (w__3 : ProcState) ->
      read_reg PSTATE_ref >>= fun (w__4 : ProcState) ->
      IsSecure () >>= fun (w__5 : bool) ->
      ELUsingAArch32 EL2 >>= fun (w__6 : bool) ->
      let ((first : integer), (include_R15_name : bool), (last : integer)) =
        if (and_bool
              (and_bool
                 (and_bool
                    (or_bool (eq_vec w__3.ProcState_EL EL0) (eq_vec w__4.ProcState_EL EL1))
                    (HaveEL EL2))
                 (not w__5))
              (not w__6))
        then
          let (first : integer) = (0:ii) in
          let (last : integer) = (30:ii) in
          let (include_R15_name : bool) = false in
          (first,include_R15_name,last)
        else
          let (first : integer) = (0:ii) in
          let (last : integer) = (30:ii) in
          let (include_R15_name : bool) = true in
          (first,include_R15_name,last) in
      return (first,include_R15_name,last)) >>= fun ((first : integer), (include_R15_name : bool), (last :
     integer)) ->
   (foreachM (index_list first last (1:ii)) ()
     (fun n () ->
      ConstrainUnpredictableBool Unpredictable_ZEROUPPER >>= fun (w__7 : bool) ->
      if (and_bool (or_bool (neq (ex_int n) (ex_int (15:ii))) include_R15_name) w__7)
      then
        read_reg _R_ref >>= fun (w__8 : list (bits ty64)) ->
        let (__tmp_3 : bits ty64) = (access_list_dec w__8 n : list bitU) in
        let __tmp_3 =
          (update_subrange_vec_dec __tmp_3 (63:ii) (32:ii) (Zeros__0 (32:ii) : list bitU) : list bitU) in
        read_reg _R_ref >>= fun (w__9 : list (list bitU)) ->
        write_reg _R_ref (update_list_dec w__9 n __tmp_3 : list (list bitU))
      else return ()))

val AArch64_FaultSyndrome : bool -> FaultRecord -> M (list bitU)

let AArch64_FaultSyndrome d_side fault =
   assert_exp (neq fault.FaultRecord_typ Fault_None) "((fault).type != Fault_None)" >>
   let (iss : bits ty25) = (Zeros__1 (25:ii) () : list bitU) in
   IsExternalSyncAbort__1 fault >>= fun (w__0 : bool) ->
   let (iss : bits ty25) =
     if (and_bool (HaveRASExt ()) w__0)
     then
       let (iss : bits ty25) =
         (set_slice (25:ii) (2:ii) iss (11:ii) fault.FaultRecord_errortype : list bitU) in
       iss
     else iss in
   (if d_side
    then
      IsSecondStage fault >>= fun (w__1 : bool) ->
      (if (and_bool w__1 (not fault.FaultRecord_s2fs1walk))
       then
         (LSInstructionSyndrome () : M (list bitU)) >>= fun (w__2 : list bitU) ->
         let (iss : bits ty25) = (set_slice (25:ii) (11:ii) iss (14:ii) w__2 : list bitU) in
         return iss
       else return iss) >>= fun (iss : bits ty25) ->
      let (iss : bits ty25) =
        if (or_bool
              (eq fault.FaultRecord_acctype AccType_DC)
              (or_bool
                 (eq fault.FaultRecord_acctype AccType_IC)
                 (eq fault.FaultRecord_acctype AccType_AT)))
        then
          let (iss : bits ty25) = (set_slice (25:ii) (1:ii) iss (8:ii) ([B1]) : list bitU) in
          let (iss : bits ty25) = (set_slice (25:ii) (1:ii) iss (6:ii) ([B1]) : list bitU) in
          iss
        else
          let (iss : bits ty25) =
            (set_slice (25:ii) (1:ii) iss (6:ii) (if fault.FaultRecord_write then [B1] else [B0]) : list bitU) in
          iss in
      return iss
    else return iss) >>= fun (iss : bits ty25) ->
   IsExternalAbort__1 fault >>= fun (w__3 : bool) ->
   let (iss : bits ty25) =
     if w__3
     then
       let (iss : bits ty25) =
         (set_slice (25:ii) (1:ii) iss (9:ii) fault.FaultRecord_extflag : list bitU) in
       iss
     else iss in
   let iss =
     (set_slice (25:ii) (1:ii) iss (7:ii) (if fault.FaultRecord_s2fs1walk then [B1] else [B0]) : list bitU) in
   (EncodeLDFSC fault.FaultRecord_typ fault.FaultRecord_level : M (list bitU)) >>= fun (w__4 :
     list bitU) ->
   let (iss : bits ty25) = (set_slice (25:ii) (6:ii) iss (0:ii) w__4 : list bitU) in
   return iss

val AArch64_AbortSyndrome : Exception -> FaultRecord -> list bitU -> M ExceptionRecord

let AArch64_AbortSyndrome typ fault vaddress =
   let (exception : ExceptionRecord) = ExceptionSyndrome typ in
   let (d_side : bool) = or_bool (eq typ Exception_DataAbort) (eq typ Exception_Watchpoint) in
   (AArch64_FaultSyndrome d_side fault : M (list bitU)) >>= fun (w__0 : bits ty25) ->
   let exception = <|exception with ExceptionRecord_syndrome = w__0|> in
   (ZeroExtend__1 (64:ii) vaddress : M (list bitU)) >>= fun (w__1 : bits ty64) ->
   let exception = <|exception with ExceptionRecord_vaddress = w__1|> in
   IPAValid fault >>= fun (w__2 : bool) ->
   let (exception : ExceptionRecord) =
     if w__2
     then
       let (exception : ExceptionRecord) = <|exception with ExceptionRecord_ipavalid = true|> in
       let (exception : ExceptionRecord) =
         <|exception with ExceptionRecord_ipaddress = fault.FaultRecord_ipaddress|> in
       exception
     else
       let (exception : ExceptionRecord) = <|exception with ExceptionRecord_ipavalid = false|> in
       exception in
   return exception

val AArch64_ExceptionClass : Exception -> list bitU -> M (ii * list bitU)

let AArch64_ExceptionClass typ target_el =
   ThisInstrLength () >>= fun (w__0 : ii) ->
   let (il : bits ty1) = if (eq (ex_int w__0) (32:ii)) then [B1] else [B0] in
   UsingAArch32 () >>= fun (from_32 : bool) ->
   assert_exp (or_bool from_32 (eq_vec il ([B1]))) "(from_32 || (il == '1'))" >>
   let (ec : ii) = undefined_int () in
   match typ with
   | Exception_Uncategorized ->
      let (ec : ii) = (0:ii) in
      let (il : bits ty1) = [B1] in
      return (ec,il)
   | Exception_WFxTrap ->
      let (ec : ii) = (1:ii) in
      return (ec,il)
   | Exception_CP15RTTrap ->
      let ec = (3:ii) in
      assert_exp from_32 "from_32" >>
      return (ec,il)
   | Exception_CP15RRTTrap ->
      let ec = (4:ii) in
      assert_exp from_32 "from_32" >>
      return (ec,il)
   | Exception_CP14RTTrap ->
      let ec = (5:ii) in
      assert_exp from_32 "from_32" >>
      return (ec,il)
   | Exception_CP14DTTrap ->
      let ec = (6:ii) in
      assert_exp from_32 "from_32" >>
      return (ec,il)
   | Exception_AdvSIMDFPAccessTrap ->
      let (ec : ii) = (7:ii) in
      return (ec,il)
   | Exception_FPIDTrap ->
      let (ec : ii) = (8:ii) in
      return (ec,il)
   | Exception_CP14RRTTrap ->
      let ec = (12:ii) in
      assert_exp from_32 "from_32" >>
      return (ec,il)
   | Exception_IllegalState ->
      let (ec : ii) = (14:ii) in
      let (il : bits ty1) = [B1] in
      return (ec,il)
   | Exception_SupervisorCall ->
      let (ec : ii) = (17:ii) in
      return (ec,il)
   | Exception_HypervisorCall ->
      let (ec : ii) = (18:ii) in
      return (ec,il)
   | Exception_MonitorCall ->
      let (ec : ii) = (19:ii) in
      return (ec,il)
   | Exception_SystemRegisterTrap ->
      let ec = (24:ii) in
      assert_exp (not from_32) "!(from_32)" >>
      return (ec,il)
   | Exception_InstructionAbort ->
      let (ec : ii) = (32:ii) in
      let (il : bits ty1) = [B1] in
      return (ec,il)
   | Exception_PCAlignment ->
      let (ec : ii) = (34:ii) in
      let (il : bits ty1) = [B1] in
      return (ec,il)
   | Exception_DataAbort ->
      let (ec : ii) = (36:ii) in
      return (ec,il)
   | Exception_SPAlignment ->
      let ec = (38:ii) in
      let il = [B1] in
      assert_exp (not from_32) "!(from_32)" >>
      return (ec,il)
   | Exception_FPTrappedException ->
      let (ec : ii) = (40:ii) in
      return (ec,il)
   | Exception_SError ->
      let (ec : ii) = (47:ii) in
      let (il : bits ty1) = [B1] in
      return (ec,il)
   | Exception_Breakpoint ->
      let (ec : ii) = (48:ii) in
      let (il : bits ty1) = [B1] in
      return (ec,il)
   | Exception_SoftwareStep ->
      let (ec : ii) = (50:ii) in
      let (il : bits ty1) = [B1] in
      return (ec,il)
   | Exception_Watchpoint ->
      let (ec : ii) = (52:ii) in
      let (il : bits ty1) = [B1] in
      return (ec,il)
   | Exception_SoftwareBreakpoint ->
      let (ec : ii) = (56:ii) in
      return (ec,il)
   | Exception_VectorCatch ->
      let ec = (58:ii) in
      let il = [B1] in
      assert_exp from_32 "from_32" >>
      return (ec,il)
   | _ ->
      Unreachable () >>
      return (ec,il)
   end >>= fun ((ec : ii), (il : bits ty1)) ->
   read_reg PSTATE_ref >>= fun (w__1 : ProcState) ->
   let (ec : ii) =
     if (and_bool
           (or_bool
              (eq (ex_int ec) (32:ii))
              (or_bool
                 (eq (ex_int ec) (36:ii))
                 (or_bool
                    (eq (ex_int ec) (48:ii))
                    (or_bool (eq (ex_int ec) (50:ii)) (eq (ex_int ec) (52:ii))))))
           (eq_vec target_el w__1.ProcState_EL))
     then
       let (ec : ii) = integerAdd (ex_int ec) (1:ii) in
       ec
     else ec in
   let (ec : ii) =
     if (and_bool
           (or_bool
              (eq (ex_int ec) (17:ii))
              (or_bool
                 (eq (ex_int ec) (18:ii))
                 (or_bool
                    (eq (ex_int ec) (19:ii))
                    (or_bool (eq (ex_int ec) (40:ii)) (eq (ex_int ec) (56:ii))))))
           (not from_32))
     then
       let (ec : ii) = integerAdd (ex_int ec) (4:ii) in
       ec
     else ec in
   return (ec,il)

val AArch64_ReportException : ExceptionRecord -> list bitU -> M unit

let AArch64_ReportException exception target_el =
   let (typ : Exception) = exception.ExceptionRecord_typ in
   let (il : bits ty1) = (undefined_vector (1:ii) (undefined_bit ()) : list bitU) in
   let (ec : ii) = undefined_int () in
   (AArch64_ExceptionClass typ target_el : M ((ii * list bitU))) >>= fun (tup__0, tup__1) ->
   let ec = tup__0 in
   let il = tup__1 in
   let (iss : bits ty25) = exception.ExceptionRecord_syndrome in
   let (il : bits ty1) =
     if (and_bool
           (or_bool (eq (ex_int ec) (36:ii)) (eq (ex_int ec) (37:ii)))
           (eq_vec ([access_vec_dec iss (24:ii)]) ([B0])))
     then
       let (il : bits ty1) = [B1] in
       il
     else il in
   aset_ESR__0
     target_el
     (concat_vec (concat_vec (__GetSlice_int (6:ii) ec (0:ii) : list bitU) il : list bitU) iss : list bitU) >>
   (if (or_bool
          (eq typ Exception_InstructionAbort)
          (or_bool
             (eq typ Exception_PCAlignment)
             (or_bool (eq typ Exception_DataAbort) (eq typ Exception_Watchpoint))))
    then aset_FAR__0 target_el exception.ExceptionRecord_vaddress
    else aset_FAR__0 target_el (undefined_vector (64:ii) (undefined_bit ()) : list bitU)) >>
   if (eq_vec target_el EL2)
   then
     if exception.ExceptionRecord_ipavalid
     then
       (read_reg HPFAR_EL2_ref : M (list bitU)) >>= fun (w__0 : list bitU) ->
       write_reg
         HPFAR_EL2_ref
         (set_slice
            (64:ii)
            (40:ii)
            w__0
            (4:ii)
            (slice exception.ExceptionRecord_ipaddress (12:ii) (40:ii) : list bitU) : list bitU)
     else
       (read_reg HPFAR_EL2_ref : M (list bitU)) >>= fun (w__1 : list bitU) ->
       write_reg
         HPFAR_EL2_ref
         (set_slice
            (64:ii)
            (40:ii)
            w__1
            (4:ii)
            (undefined_vector (40:ii) (undefined_bit ()) : list bitU) : list bitU)
   else return ()

val AArch64_BranchAddr : list bitU -> M (list bitU)

let AArch64_BranchAddr vaddress =
   UsingAArch32 () >>= fun (w__0 : bool) ->
   assert_exp (not w__0) "!(UsingAArch32())" >>
   read_reg PSTATE_ref >>= fun (w__1 : ProcState) ->
   AddrTop vaddress true w__1.ProcState_EL >>= fun (w__2 : ii) ->
   coerce_int_nat w__2 >>= fun (msbit : ii) ->
   if (eq (ex_nat msbit) (63:ii))
   then return vaddress
   else
     read_reg PSTATE_ref >>= fun (w__3 : ProcState) ->
     read_reg PSTATE_ref >>= fun (w__4 : ProcState) ->
     IsInHost () >>= fun (w__5 : bool) ->
     if (and_bool
           (or_bool (or_bool (eq_vec w__3.ProcState_EL EL0) (eq_vec w__4.ProcState_EL EL1)) w__5)
           (eq_vec ([access_vec_dec vaddress msbit]) ([B1])))
     then
       (SignExtend__1
          (64:ii)
          (slice vaddress (0:ii) (integerAdd (ex_nat msbit) (1:ii)) : (list bitU)) : M (list bitU))
     else
       (ZeroExtend__1
          (64:ii)
          (slice vaddress (0:ii) (integerAdd (ex_nat msbit) (1:ii)) : (list bitU)) : M (list bitU))

val BranchTo : list bitU -> BranchType -> M unit

let BranchTo target branch_type =
   write_reg __BranchTaken_ref true >>
   let (_ : unit) = Hint_Branch branch_type in
   if (eq (length target) (32:ii))
   then
     UsingAArch32 () >>= fun (w__0 : bool) ->
     assert_exp w__0 "UsingAArch32()" >>
     (ZeroExtend__1 (64:ii) target : M (list bitU)) >>= fun (w__1 : bits ty64) ->
     write_reg _PC_ref w__1
   else
     UsingAArch32 () >>= fun (w__2 : bool) ->
     assert_exp (and_bool (eq (length target) (64:ii)) (not w__2)) "((N == 64) && !(UsingAArch32()))" >>
     (AArch64_BranchAddr (slice target (0:ii) (64:ii) : list bitU) : M (list bitU)) >>= fun (w__3 :
       bits ty64) ->
     write_reg _PC_ref w__3

val AArch64_TakeException : list bitU -> ExceptionRecord -> list bitU -> ii -> M unit

let AArch64_TakeException target_el exception preferred_exception_return vect_offset__arg =
   let vect_offset = vect_offset__arg in
   let (_ : unit) = SynchronizeContext () in
   ELUsingAArch32 target_el >>= fun (w__0 : bool) ->
   read_reg PSTATE_ref >>= fun (w__1 : ProcState) ->
   assert_exp (and_bool
                 (and_bool (HaveEL target_el) (not w__0))
                 (gteq (uint target_el) (uint w__1.ProcState_EL))) "((HaveEL(target_el) && !(ELUsingAArch32(target_el))) && (UInt(target_el) >= UInt((PSTATE).EL)))" >>
   UsingAArch32 () >>= fun (from_32 : bool) ->
   (if from_32
    then AArch64_MaybeZeroRegisterUppers ()
    else return ()) >>
   read_reg PSTATE_ref >>= fun (w__2 : ProcState) ->
   (if (gt (uint target_el) (uint w__2.ProcState_EL))
    then
      let (lower_32 : bool) = undefined_bool () in
      (if (eq_vec target_el EL3)
       then
         IsSecure () >>= fun (w__3 : bool) ->
         (if (and_bool (not w__3) (HaveEL EL2))
          then
            ELUsingAArch32 EL2 >>= fun (w__4 : bool) ->
            let (lower_32 : bool) = w__4 in
            return lower_32
          else
            ELUsingAArch32 EL1 >>= fun (w__5 : bool) ->
            let (lower_32 : bool) = w__5 in
            return lower_32) >>= fun (lower_32 : bool) ->
         return lower_32
       else
         IsInHost () >>= fun (w__6 : bool) ->
         read_reg PSTATE_ref >>= fun (w__7 : ProcState) ->
         (if (and_bool (and_bool w__6 (eq_vec w__7.ProcState_EL EL0)) (eq_vec target_el EL2))
          then
            ELUsingAArch32 EL0 >>= fun (w__8 : bool) ->
            let (lower_32 : bool) = w__8 in
            return lower_32
          else
            ELUsingAArch32 (sub_vec_int target_el (1:ii) : list bitU) >>= fun (w__9 : bool) ->
            let (lower_32 : bool) = w__9 in
            return lower_32) >>= fun (lower_32 : bool) ->
         return lower_32) >>= fun (lower_32 : bool) ->
      let (vect_offset : ii) = integerAdd vect_offset (if lower_32 then (1536:ii) else (1024:ii)) in
      return vect_offset
    else
      read_reg PSTATE_ref >>= fun (w__10 : ProcState) ->
      let (vect_offset : ii) =
        if (eq_vec w__10.ProcState_SP ([B1]))
        then
          let (vect_offset : ii) = integerAdd (ex_int vect_offset) (512:ii) in
          vect_offset
        else vect_offset in
      return vect_offset) >>= fun (vect_offset : ii) ->
   (GetPSRFromPSTATE () : M (list bitU)) >>= fun (spsr : bits ty32) ->
   (if (HaveUAOExt ())
    then
      read_reg PSTATE_ref >>= fun (w__11 : ProcState) ->
      write_reg PSTATE_ref <|w__11 with ProcState_UAO = ([B0])|>
    else return ()) >>
   (if (not
          (or_bool
             (eq exception.ExceptionRecord_typ Exception_IRQ)
             (eq exception.ExceptionRecord_typ Exception_FIQ)))
    then AArch64_ReportException exception target_el
    else return ()) >>
   read_reg PSTATE_ref >>= fun (w__12 : ProcState) ->
   write_reg PSTATE_ref <|w__12 with ProcState_EL = target_el|> >>
   read_reg PSTATE_ref >>= fun (w__13 : ProcState) ->
   write_reg PSTATE_ref <|w__13 with ProcState_nRW = ([B0])|> >>
   read_reg PSTATE_ref >>= fun (w__14 : ProcState) ->
   write_reg PSTATE_ref <|w__14 with ProcState_SP = ([B1])|> >>
   aset_SPSR spsr >>
   aset_ELR__1 preferred_exception_return >>
   read_reg PSTATE_ref >>= fun (w__15 : ProcState) ->
   write_reg PSTATE_ref <|w__15 with ProcState_SS = ([B0])|> >>
   let split_vec = [B1;B1;B1;B1] in
   let (tup__0, tup__1, tup__2, tup__3) =
     ((subrange_vec_dec split_vec (3:ii) (3:ii) : list bitU),(subrange_vec_dec
                                                                split_vec
                                                                (2:ii)
                                                                (2:ii) : list bitU),(subrange_vec_dec
                                                                                       split_vec
                                                                                       (1:ii)
                                                                                       (1:ii) : list bitU),(subrange_vec_dec
                                                                                                              split_vec
                                                                                                              (0:ii)
                                                                                                              (0:ii) : list bitU)) in
   read_reg PSTATE_ref >>= fun (w__16 : ProcState) ->
   write_reg PSTATE_ref <|w__16 with ProcState_D = tup__0|> >>
   read_reg PSTATE_ref >>= fun (w__17 : ProcState) ->
   write_reg PSTATE_ref <|w__17 with ProcState_A = tup__1|> >>
   read_reg PSTATE_ref >>= fun (w__18 : ProcState) ->
   write_reg PSTATE_ref <|w__18 with ProcState_I = tup__2|> >>
   read_reg PSTATE_ref >>= fun (w__19 : ProcState) ->
   write_reg PSTATE_ref <|w__19 with ProcState_F = tup__3|> >>
   read_reg PSTATE_ref >>= fun (w__20 : ProcState) ->
   write_reg PSTATE_ref <|w__20 with ProcState_IL = ([B0])|> >>
   (if from_32
    then
      read_reg PSTATE_ref >>= fun (w__21 : ProcState) ->
      write_reg PSTATE_ref <|w__21 with ProcState_IT = ([B0;B0;B0;B0;B0;B0;B0;B0])|> >>
      read_reg PSTATE_ref >>= fun (w__22 : ProcState) ->
      write_reg PSTATE_ref <|w__22 with ProcState_T = ([B0])|>
    else return ()) >>
   read_reg PSTATE_ref >>= fun (w__23 : ProcState) ->
   read_reg PSTATE_ref >>= fun (w__24 : ProcState) ->
   ELIsInHost EL0 >>= fun (w__25 : bool) ->
   (aget_SCTLR__1 () : M (list bitU)) >>= fun (w__26 : list bitU) ->
   (if (and_bool
          (and_bool
             (HavePANExt ())
             (or_bool
                (eq_vec w__23.ProcState_EL EL1)
                (and_bool (eq_vec w__24.ProcState_EL EL2) w__25)))
          (eq_vec ([access_vec_dec w__26 (23:ii)]) ([B0])))
    then
      read_reg PSTATE_ref >>= fun (w__27 : ProcState) ->
      write_reg PSTATE_ref <|w__27 with ProcState_PAN = ([B1])|>
    else return ()) >>
   (aget_VBAR__1 () : M (list bitU)) >>= fun (w__28 : list bitU) ->
   BranchTo
     (concat_vec
        (slice w__28 (11:ii) (53:ii) : list bitU)
        (__GetSlice_int (11:ii) vect_offset (0:ii) : list bitU) : list bitU)
     BranchType_EXCEPTION >>
   let (iesb_req : bool) = undefined_bool () in
   (aget_SCTLR__1 () : M (list bitU)) >>= fun (w__29 : list bitU) ->
   (if (and_bool (HaveRASExt ()) (eq_vec ([access_vec_dec w__29 (21:ii)]) ([B1])))
    then
      let (_ : unit) = ErrorSynchronizationBarrier MBReqDomain_FullSystem MBReqTypes_All in
      let iesb_req = true in
      TakeUnmaskedPhysicalSErrorInterrupts iesb_req >>
      return iesb_req
    else return iesb_req) >>= fun (iesb_req : bool) ->
   return (EndOfInstruction ())

val AArch64_WatchpointException : list bitU -> FaultRecord -> M unit

let AArch64_WatchpointException vaddress fault =
   read_reg PSTATE_ref >>= fun (w__0 : ProcState) ->
   assert_exp (neq_vec w__0.ProcState_EL EL3) "((PSTATE).EL != EL3)" >>
   IsSecure () >>= fun (w__1 : bool) ->
   read_reg PSTATE_ref >>= fun (w__2 : ProcState) ->
   read_reg PSTATE_ref >>= fun (w__3 : ProcState) ->
   (read_reg HCR_EL2_ref : M (list bitU)) >>= fun (w__4 : bits ty64) ->
   (read_reg MDCR_EL2_ref : M (list bitU)) >>= fun (w__5 : bits ty32) ->
   let (route_to_el2 : bool) =
     and_bool
       (and_bool
          (and_bool (HaveEL EL2) (not w__1))
          (or_bool (eq_vec w__2.ProcState_EL EL0) (eq_vec w__3.ProcState_EL EL1)))
       (or_bool
          (eq_vec ([access_vec_dec w__4 (27:ii)]) ([B1]))
          (eq_vec ([access_vec_dec w__5 (8:ii)]) ([B1]))) in
   (ThisInstrAddr (64:ii) () : M (list bitU)) >>= fun (preferred_exception_return : bits ty64) ->
   let (vect_offset : ii) = (0:ii) in
   AArch64_AbortSyndrome Exception_Watchpoint fault vaddress >>= fun (exception : ExceptionRecord) ->
   read_reg PSTATE_ref >>= fun (w__6 : ProcState) ->
   if (or_bool (eq_vec w__6.ProcState_EL EL2) route_to_el2)
   then AArch64_TakeException EL2 exception preferred_exception_return vect_offset
   else AArch64_TakeException EL1 exception preferred_exception_return vect_offset

val AArch64_VectorCatchException : FaultRecord -> M unit

let AArch64_VectorCatchException fault =
   read_reg PSTATE_ref >>= fun (w__0 : ProcState) ->
   assert_exp (neq_vec w__0.ProcState_EL EL2) "((PSTATE).EL != EL2)" >>
   IsSecure () >>= fun (w__1 : bool) ->
   (read_reg HCR_EL2_ref : M (list bitU)) >>= fun (w__2 : bits ty64) ->
   (read_reg MDCR_EL2_ref : M (list bitU)) >>= fun (w__3 : bits ty32) ->
   assert_exp (and_bool
                 (and_bool (HaveEL EL2) (not w__1))
                 (or_bool
                    (eq_vec ([access_vec_dec w__2 (27:ii)]) ([B1]))
                    (eq_vec ([access_vec_dec w__3 (8:ii)]) ([B1])))) "((HaveEL(EL2) && !(IsSecure())) && (((HCR_EL2).TGE == '1') || ((MDCR_EL2).TDE == '1')))" >>
   (ThisInstrAddr (64:ii) () : M (list bitU)) >>= fun (preferred_exception_return : bits ty64) ->
   let (vect_offset : ii) = (0:ii) in
   let (vaddress : bits ty64) = (undefined_vector (64:ii) (undefined_bit ()) : list bitU) in
   AArch64_AbortSyndrome Exception_VectorCatch fault vaddress >>= fun (exception : ExceptionRecord) ->
   AArch64_TakeException EL2 exception preferred_exception_return vect_offset

val AArch64_UndefinedFault : unit -> M unit

let AArch64_UndefinedFault () =
   IsSecure () >>= fun (w__0 : bool) ->
   read_reg PSTATE_ref >>= fun (w__1 : ProcState) ->
   (read_reg HCR_EL2_ref : M (list bitU)) >>= fun (w__2 : bits ty64) ->
   let (route_to_el2 : bool) =
     and_bool
       (and_bool (and_bool (HaveEL EL2) (not w__0)) (eq_vec w__1.ProcState_EL EL0))
       (eq_vec ([access_vec_dec w__2 (27:ii)]) ([B1])) in
   (ThisInstrAddr (64:ii) () : M (list bitU)) >>= fun (preferred_exception_return : bits ty64) ->
   let (vect_offset : ii) = (0:ii) in
   let (exception : ExceptionRecord) = ExceptionSyndrome Exception_Uncategorized in
   read_reg PSTATE_ref >>= fun (w__3 : ProcState) ->
   if (gt (uint w__3.ProcState_EL) (uint EL1))
   then
     read_reg PSTATE_ref >>= fun (w__4 : ProcState) ->
     AArch64_TakeException w__4.ProcState_EL exception preferred_exception_return vect_offset
   else
     if route_to_el2
     then AArch64_TakeException EL2 exception preferred_exception_return vect_offset
     else AArch64_TakeException EL1 exception preferred_exception_return vect_offset

val AArch64_SPAlignmentFault : unit -> M unit

let AArch64_SPAlignmentFault () =
   (ThisInstrAddr (64:ii) () : M (list bitU)) >>= fun (preferred_exception_return : bits ty64) ->
   let (vect_offset : ii) = (0:ii) in
   let (exception : ExceptionRecord) = ExceptionSyndrome Exception_SPAlignment in
   read_reg PSTATE_ref >>= fun (w__0 : ProcState) ->
   if (gt (uint w__0.ProcState_EL) (uint EL1))
   then
     read_reg PSTATE_ref >>= fun (w__1 : ProcState) ->
     AArch64_TakeException w__1.ProcState_EL exception preferred_exception_return vect_offset
   else
     IsSecure () >>= fun (w__2 : bool) ->
     (read_reg HCR_EL2_ref : M (list bitU)) >>= fun (w__3 : bits ty64) ->
     if (and_bool (and_bool (HaveEL EL2) (not w__2)) (eq_vec ([access_vec_dec w__3 (27:ii)]) ([B1])))
     then AArch64_TakeException EL2 exception preferred_exception_return vect_offset
     else AArch64_TakeException EL1 exception preferred_exception_return vect_offset

val CheckSPAlignment : unit -> M unit

let CheckSPAlignment () =
   (aget_SP (64:ii) () : M (list bitU)) >>= fun (sp : bits ty64) ->
   let (stack_align_check : bool) = undefined_bool () in
   read_reg PSTATE_ref >>= fun (w__0 : ProcState) ->
   (if (eq_vec w__0.ProcState_EL EL0)
    then
      (aget_SCTLR__1 () : M (list bitU)) >>= fun (w__1 : list bitU) ->
      let (stack_align_check : bool) = neq_vec ([access_vec_dec w__1 (4:ii)]) ([B0]) in
      return stack_align_check
    else
      (aget_SCTLR__1 () : M (list bitU)) >>= fun (w__2 : list bitU) ->
      let (stack_align_check : bool) = neq_vec ([access_vec_dec w__2 (3:ii)]) ([B0]) in
      return stack_align_check) >>= fun (stack_align_check : bool) ->
   if (and_bool stack_align_check (neq_vec sp (Align__1 sp (16:ii) : list bitU)))
   then AArch64_SPAlignmentFault ()
   else return ()

val AArch64_InstructionAbort : list bitU -> FaultRecord -> M unit

let AArch64_InstructionAbort vaddress fault =
   (read_reg SCR_EL3_ref : M (list bitU)) >>= fun (w__0 : bits ty32) ->
   IsExternalAbort__1 fault >>= fun (w__1 : bool) ->
   let (route_to_el3 : bool) =
     and_bool (and_bool (HaveEL EL3) (eq_vec ([access_vec_dec w__0 (3:ii)]) ([B1]))) w__1 in
   IsSecure () >>= fun (w__2 : bool) ->
   read_reg PSTATE_ref >>= fun (w__3 : ProcState) ->
   read_reg PSTATE_ref >>= fun (w__4 : ProcState) ->
   (read_reg HCR_EL2_ref : M (list bitU)) >>= fun (w__5 : bits ty64) ->
   IsSecondStage fault >>= fun (w__6 : bool) ->
   (read_reg HCR_EL2_ref : M (list bitU)) >>= fun (w__7 : bits ty64) ->
   IsExternalAbort__1 fault >>= fun (w__8 : bool) ->
   let (route_to_el2 : bool) =
     and_bool
       (and_bool
          (and_bool (HaveEL EL2) (not w__2))
          (or_bool (eq_vec w__3.ProcState_EL EL0) (eq_vec w__4.ProcState_EL EL1)))
       (or_bool
          (or_bool (eq_vec ([access_vec_dec w__5 (27:ii)]) ([B1])) w__6)
          (and_bool (and_bool (HaveRASExt ()) (eq_vec ([access_vec_dec w__7 (37:ii)]) ([B1]))) w__8)) in
   (ThisInstrAddr (64:ii) () : M (list bitU)) >>= fun (preferred_exception_return : bits ty64) ->
   let (vect_offset : ii) = (0:ii) in
   AArch64_AbortSyndrome Exception_InstructionAbort fault vaddress >>= fun (exception :
     ExceptionRecord) ->
   read_reg PSTATE_ref >>= fun (w__9 : ProcState) ->
   if (or_bool (eq_vec w__9.ProcState_EL EL3) route_to_el3)
   then AArch64_TakeException EL3 exception preferred_exception_return vect_offset
   else
     read_reg PSTATE_ref >>= fun (w__10 : ProcState) ->
     if (or_bool (eq_vec w__10.ProcState_EL EL2) route_to_el2)
     then AArch64_TakeException EL2 exception preferred_exception_return vect_offset
     else AArch64_TakeException EL1 exception preferred_exception_return vect_offset

val AArch64_DataAbort : list bitU -> FaultRecord -> M unit

let AArch64_DataAbort vaddress fault =
   (read_reg SCR_EL3_ref : M (list bitU)) >>= fun (w__0 : bits ty32) ->
   IsExternalAbort__1 fault >>= fun (w__1 : bool) ->
   let (route_to_el3 : bool) =
     and_bool (and_bool (HaveEL EL3) (eq_vec ([access_vec_dec w__0 (3:ii)]) ([B1]))) w__1 in
   IsSecure () >>= fun (w__2 : bool) ->
   read_reg PSTATE_ref >>= fun (w__3 : ProcState) ->
   read_reg PSTATE_ref >>= fun (w__4 : ProcState) ->
   (read_reg HCR_EL2_ref : M (list bitU)) >>= fun (w__5 : bits ty64) ->
   IsSecondStage fault >>= fun (w__6 : bool) ->
   (read_reg HCR_EL2_ref : M (list bitU)) >>= fun (w__7 : bits ty64) ->
   IsExternalAbort__1 fault >>= fun (w__8 : bool) ->
   let (route_to_el2 : bool) =
     and_bool
       (and_bool
          (and_bool (HaveEL EL2) (not w__2))
          (or_bool (eq_vec w__3.ProcState_EL EL0) (eq_vec w__4.ProcState_EL EL1)))
       (or_bool
          (or_bool (eq_vec ([access_vec_dec w__5 (27:ii)]) ([B1])) w__6)
          (and_bool (and_bool (HaveRASExt ()) (eq_vec ([access_vec_dec w__7 (37:ii)]) ([B1]))) w__8)) in
   (ThisInstrAddr (64:ii) () : M (list bitU)) >>= fun (preferred_exception_return : bits ty64) ->
   let (vect_offset : ii) = (0:ii) in
   AArch64_AbortSyndrome Exception_DataAbort fault vaddress >>= fun (exception : ExceptionRecord) ->
   read_reg PSTATE_ref >>= fun (w__9 : ProcState) ->
   if (or_bool (eq_vec w__9.ProcState_EL EL3) route_to_el3)
   then AArch64_TakeException EL3 exception preferred_exception_return vect_offset
   else
     read_reg PSTATE_ref >>= fun (w__10 : ProcState) ->
     if (or_bool (eq_vec w__10.ProcState_EL EL2) route_to_el2)
     then AArch64_TakeException EL2 exception preferred_exception_return vect_offset
     else AArch64_TakeException EL1 exception preferred_exception_return vect_offset

val AArch64_BreakpointException : FaultRecord -> M unit

let AArch64_BreakpointException fault =
   read_reg PSTATE_ref >>= fun (w__0 : ProcState) ->
   assert_exp (neq_vec w__0.ProcState_EL EL3) "((PSTATE).EL != EL3)" >>
   IsSecure () >>= fun (w__1 : bool) ->
   read_reg PSTATE_ref >>= fun (w__2 : ProcState) ->
   read_reg PSTATE_ref >>= fun (w__3 : ProcState) ->
   (read_reg HCR_EL2_ref : M (list bitU)) >>= fun (w__4 : bits ty64) ->
   (read_reg MDCR_EL2_ref : M (list bitU)) >>= fun (w__5 : bits ty32) ->
   let (route_to_el2 : bool) =
     and_bool
       (and_bool
          (and_bool (HaveEL EL2) (not w__1))
          (or_bool (eq_vec w__2.ProcState_EL EL0) (eq_vec w__3.ProcState_EL EL1)))
       (or_bool
          (eq_vec ([access_vec_dec w__4 (27:ii)]) ([B1]))
          (eq_vec ([access_vec_dec w__5 (8:ii)]) ([B1]))) in
   (ThisInstrAddr (64:ii) () : M (list bitU)) >>= fun (preferred_exception_return : bits ty64) ->
   let (vect_offset : ii) = (0:ii) in
   let (vaddress : bits ty64) = (undefined_vector (64:ii) (undefined_bit ()) : list bitU) in
   AArch64_AbortSyndrome Exception_Breakpoint fault vaddress >>= fun (exception : ExceptionRecord) ->
   read_reg PSTATE_ref >>= fun (w__6 : ProcState) ->
   if (or_bool (eq_vec w__6.ProcState_EL EL2) route_to_el2)
   then AArch64_TakeException EL2 exception preferred_exception_return vect_offset
   else AArch64_TakeException EL1 exception preferred_exception_return vect_offset

val AArch64_Abort : list bitU -> FaultRecord -> M unit

let AArch64_Abort vaddress fault =
   IsDebugException fault >>= fun (w__0 : bool) ->
   if w__0
   then
     if (eq fault.FaultRecord_acctype AccType_IFETCH)
     then
       UsingAArch32 () >>= fun (w__1 : bool) ->
       if (and_bool w__1 (eq_vec fault.FaultRecord_debugmoe DebugException_VectorCatch))
       then AArch64_VectorCatchException fault
       else AArch64_BreakpointException fault
     else AArch64_WatchpointException vaddress fault
   else
     if (eq fault.FaultRecord_acctype AccType_IFETCH)
     then AArch64_InstructionAbort vaddress fault
     else AArch64_DataAbort vaddress fault

val AArch64_aset_MemSingle : list bitU -> integer -> AccType -> bool -> list bitU -> M unit

let AArch64_aset_MemSingle address size acctype wasaligned value_name =
   assert_exp (or_bool
                 (eq size (1:ii))
                 (or_bool
                    (eq size (2:ii))
                    (or_bool (eq size (4:ii)) (or_bool (eq size (8:ii)) (eq size (16:ii)))))) "((size == 1) || ((size == 2) || ((size == 4) || ((size == 8) || (size == 16)))))" >>
   assert_exp (eq_vec address (Align__1 address size : list bitU)) "(address == Align(address, size))" >>
   let (memaddrdesc : AddressDescriptor) = undefined_AddressDescriptor () in
   let (iswrite : bool) = true in
   AArch64_TranslateAddress address acctype iswrite wasaligned size >>= fun (w__0 :
     AddressDescriptor) ->
   let memaddrdesc = w__0 in
   (if (IsFault memaddrdesc)
    then AArch64_Abort address memaddrdesc.AddressDescriptor_fault
    else return ()) >>
   let (_ : unit) =
     if memaddrdesc.AddressDescriptor_memattrs.MemoryAttributes_shareable
     then ClearExclusiveByAddress memaddrdesc.AddressDescriptor_paddress (ProcessorID ()) size
     else () in
   let (accdesc : AccessDescriptor) = CreateAccessDescriptor acctype in
   aset__Mem memaddrdesc size accdesc value_name

val AArch64_aget_MemSingle : list bitU -> integer -> AccType -> bool -> M (list bitU)

let AArch64_aget_MemSingle address size acctype wasaligned =
   assert_exp (or_bool
                 (eq size (1:ii))
                 (or_bool
                    (eq size (2:ii))
                    (or_bool (eq size (4:ii)) (or_bool (eq size (8:ii)) (eq size (16:ii)))))) "((size == 1) || ((size == 2) || ((size == 4) || ((size == 8) || (size == 16)))))" >>
   assert_exp (eq_vec address (Align__1 address size : list bitU)) "(address == Align(address, size))" >>
   let (memaddrdesc : AddressDescriptor) = undefined_AddressDescriptor () in
   let value_name = (undefined_vector (integerMult (8:ii) size) (undefined_bit ()) : list bitU) in
   let (iswrite : bool) = false in
   AArch64_TranslateAddress address acctype iswrite wasaligned size >>= fun (w__0 :
     AddressDescriptor) ->
   let memaddrdesc = w__0 in
   (if (IsFault memaddrdesc)
    then AArch64_Abort address memaddrdesc.AddressDescriptor_fault
    else return ()) >>
   let (accdesc : AccessDescriptor) = CreateAccessDescriptor acctype in
   (aget__Mem memaddrdesc size accdesc : M (list bitU)) >>= fun w__1 ->
   let value_name = w__1 in
   return value_name

val AArch64_CheckAlignment : list bitU -> ii -> AccType -> bool -> M bool

let AArch64_CheckAlignment address alignment acctype iswrite =
   let (aligned : bool) = eq_vec address (Align__1 address alignment : list bitU) in
   let (atomic : bool) = or_bool (eq acctype AccType_ATOMIC) (eq acctype AccType_ATOMICRW) in
   let (ordered : bool) =
     or_bool
       (eq acctype AccType_ORDERED)
       (or_bool (eq acctype AccType_ORDEREDRW) (eq acctype AccType_LIMITEDORDERED)) in
   let (vector_name : bool) = eq acctype AccType_VEC in
   (aget_SCTLR__1 () : M (list bitU)) >>= fun (w__0 : list bitU) ->
   let (check' : bool) =
     or_bool (or_bool atomic ordered) (eq_vec ([access_vec_dec w__0 (1:ii)]) ([B1])) in
   let (secondstage : bool) = undefined_bool () in
   (if (and_bool check' (not aligned))
    then
      let secondstage = false in
      AArch64_Abort address (AArch64_AlignmentFault acctype iswrite secondstage) >>
      return secondstage
    else return secondstage) >>= fun (secondstage : bool) ->
   return aligned

val aset_Mem : list bitU -> integer -> AccType -> list bitU -> M unit

let aset_Mem address size acctype value_name__arg =
   let value_name = value_name__arg in
   let (i : ii) = undefined_int () in
   let (iswrite : bool) = true in
   BigEndian () >>= fun (w__0 : bool) ->
   (if w__0
    then
      (BigEndianReverse value_name : M (list bitU)) >>= fun (w__1 : list bitU) ->
      let (value_name : list bitU) = w__1 in
      return value_name
    else return value_name) >>= fun (value_name : list bitU) ->
   AArch64_CheckAlignment address size acctype iswrite >>= fun (aligned : bool) ->
   let (atomic : bool) = undefined_bool () in
   let (atomic : bool) =
     if (or_bool
           (neq size (16:ii))
           (not (or_bool (eq acctype AccType_VEC) (eq acctype AccType_VECSTREAM))))
     then
       let (atomic : bool) = aligned in
       atomic
     else
       let (atomic : bool) = eq_vec address (Align__1 address (8:ii) : list bitU) in
       atomic in
   let (c : Constraint) = undefined_Constraint () in
   (if (not atomic)
    then
      assert_exp (gt size (1:ii)) "(size > 1)" >>
      AArch64_aset_MemSingle
        address
        (1:ii)
        acctype
        aligned
        (slice value_name (0:ii) (8:ii) : list bitU) >>
      (if (not aligned)
       then
         let c = ConstrainUnpredictable Unpredictable_DEVPAGE2 in
         assert_exp (or_bool (eq c Constraint_FAULT) (eq c Constraint_NONE)) "((c == Constraint_FAULT) || (c == Constraint_NONE))" >>
         let (aligned : bool) =
           if (eq c Constraint_NONE)
           then
             let (aligned : bool) = true in
             aligned
           else aligned in
         return (aligned,c)
       else return (aligned,c)) >>= fun ((aligned : bool), (c : Constraint)) ->
      (foreachM (index_list (1:ii) (integerMinus size (1:ii)) (1:ii)) ()
        (fun i () ->
         AArch64_aset_MemSingle
           (add_vec_int address i : list bitU)
           (1:ii)
           acctype
           aligned
           (slice value_name (integerMult (8:ii) i) (8:ii) : list bitU))) >>
      return (aligned,c)
    else
      (if (and_bool
             (eq size (16:ii))
             (or_bool (eq acctype AccType_VEC) (eq acctype AccType_VECSTREAM)))
       then
         AArch64_aset_MemSingle
           address
           (8:ii)
           acctype
           aligned
           (slice value_name (0:ii) (64:ii) : list bitU) >>
         AArch64_aset_MemSingle
           (add_vec_int address (8:ii) : list bitU)
           (8:ii)
           acctype
           aligned
           (slice value_name (64:ii) (64:ii) : list bitU)
       else AArch64_aset_MemSingle address size acctype aligned value_name) >>
      return (aligned,c)) >>= fun ((aligned : bool), (c : Constraint)) ->
   return ()

val aget_Mem : list bitU -> integer -> AccType -> M (list bitU)

let aget_Mem address size acctype =
   assert_exp (or_bool
                 (eq size (1:ii))
                 (or_bool
                    (eq size (2:ii))
                    (or_bool (eq size (4:ii)) (or_bool (eq size (8:ii)) (eq size (16:ii)))))) "((size == 1) || ((size == 2) || ((size == 4) || ((size == 8) || (size == 16)))))" >>
   let value_name = (undefined_vector (integerMult (8:ii) size) (undefined_bit ()) : list bitU) in
   let (i : ii) = undefined_int () in
   let (iswrite : bool) = false in
   AArch64_CheckAlignment address size acctype iswrite >>= fun (aligned : bool) ->
   let (atomic : bool) = undefined_bool () in
   let (atomic : bool) =
     if (or_bool
           (neq size (16:ii))
           (not (or_bool (eq acctype AccType_VEC) (eq acctype AccType_VECSTREAM))))
     then
       let (atomic : bool) = aligned in
       atomic
     else
       let (atomic : bool) = eq_vec address (Align__1 address (8:ii) : list bitU) in
       atomic in
   let (c : Constraint) = undefined_Constraint () in
   (if (not atomic)
    then
      assert_exp (gt size (1:ii)) "(size > 1)" >>
      (AArch64_aget_MemSingle address (1:ii) acctype aligned : M (list bitU)) >>= fun (w__0 :
        list bitU) ->
      let value_name =
        (set_slice (integerMult (8:ii) size) (8:ii) value_name (0:ii) w__0 : list bitU) in
      (if (not aligned)
       then
         let c = ConstrainUnpredictable Unpredictable_DEVPAGE2 in
         assert_exp (or_bool (eq c Constraint_FAULT) (eq c Constraint_NONE)) "((c == Constraint_FAULT) || (c == Constraint_NONE))" >>
         let (aligned : bool) =
           if (eq c Constraint_NONE)
           then
             let (aligned : bool) = true in
             aligned
           else aligned in
         return (aligned,c)
       else return (aligned,c)) >>= fun ((aligned : bool), (c : Constraint)) ->
      (foreachM (index_list (1:ii) (integerMinus size (1:ii)) (1:ii)) value_name
        (fun i value_name ->
         (AArch64_aget_MemSingle (add_vec_int address i : list bitU) (1:ii) acctype aligned : M (list bitU)) >>= fun (w__1 :
           list bitU) ->
         let value_name =
           (set_slice (integerMult (8:ii) size) (8:ii) value_name (integerMult (8:ii) i) w__1 : list bitU) in
         return value_name)) >>= fun value_name ->
      return (aligned,c,value_name)
    else
      (if (and_bool
             (eq size (16:ii))
             (or_bool (eq acctype AccType_VEC) (eq acctype AccType_VECSTREAM)))
       then
         (AArch64_aget_MemSingle address (8:ii) acctype aligned : M (list bitU)) >>= fun (w__2 :
           list bitU) ->
         let value_name =
           (set_slice (integerMult (8:ii) size) (64:ii) value_name (0:ii) w__2 : list bitU) in
         (AArch64_aget_MemSingle (add_vec_int address (8:ii) : list bitU) (8:ii) acctype aligned : M (list bitU)) >>= fun (w__3 :
           list bitU) ->
         let value_name =
           (set_slice (integerMult (8:ii) size) (64:ii) value_name (64:ii) w__3 : list bitU) in
         return value_name
       else
         (AArch64_aget_MemSingle address size acctype aligned : M (list bitU)) >>= fun w__4 ->
         let value_name = w__4 in
         return value_name) >>= fun value_name ->
      return (aligned,c,value_name)) >>= fun ((aligned : bool), (c : Constraint), value_name) ->
   BigEndian () >>= fun (w__5 : bool) ->
   (if w__5
    then
      (BigEndianReverse value_name : M (list bitU)) >>= fun w__6 ->
      let value_name = w__6 in
      return value_name
    else return value_name) >>= fun value_name ->
   return value_name

val AArch32_EnterMode : list bitU -> list bitU -> ii -> ii -> M unit

let AArch32_EnterMode target_mode preferred_exception_return lr_offset vect_offset =
   let (_ : unit) = SynchronizeContext () in
   ELUsingAArch32 EL1 >>= fun (w__0 : bool) ->
   read_reg PSTATE_ref >>= fun (w__1 : ProcState) ->
   assert_exp (and_bool w__0 (neq_vec w__1.ProcState_EL EL2)) "(ELUsingAArch32(EL1) && ((PSTATE).EL != EL2))" >>
   (GetPSRFromPSTATE () : M (list bitU)) >>= fun (spsr : bits ty32) ->
   read_reg PSTATE_ref >>= fun (w__2 : ProcState) ->
   (if (eq_vec w__2.ProcState_M M32_Monitor)
    then
      (read_reg SCR_ref : M (list bitU)) >>= fun (w__3 : list bitU) ->
      write_reg SCR_ref (set_slice (32:ii) (1:ii) w__3 (0:ii) ([B0]) : list bitU)
    else return ()) >>
   AArch32_WriteMode target_mode >>
   aset_SPSR spsr >>
   aset_R (14:ii) (add_vec_int preferred_exception_return lr_offset : list bitU) >>
   read_reg PSTATE_ref >>= fun (w__4 : ProcState) ->
   (read_reg SCTLR_ref : M (list bitU)) >>= fun (w__5 : bits ty32) ->
   write_reg PSTATE_ref <|w__4 with ProcState_T = ([access_vec_dec w__5 (30:ii)])|> >>
   read_reg PSTATE_ref >>= fun (w__6 : ProcState) ->
   write_reg PSTATE_ref <|w__6 with ProcState_SS = ([B0])|> >>
   (if (eq_vec target_mode M32_FIQ)
    then
      let split_vec = [B1;B1;B1] in
      let (tup__0, tup__1, tup__2) =
        ((subrange_vec_dec split_vec (2:ii) (2:ii) : list bitU),(subrange_vec_dec
                                                                   split_vec
                                                                   (1:ii)
                                                                   (1:ii) : list bitU),(subrange_vec_dec
                                                                                          split_vec
                                                                                          (0:ii)
                                                                                          (0:ii) : list bitU)) in
      read_reg PSTATE_ref >>= fun (w__7 : ProcState) ->
      write_reg PSTATE_ref <|w__7 with ProcState_A = tup__0|> >>
      read_reg PSTATE_ref >>= fun (w__8 : ProcState) ->
      write_reg PSTATE_ref <|w__8 with ProcState_I = tup__1|> >>
      read_reg PSTATE_ref >>= fun (w__9 : ProcState) ->
      write_reg PSTATE_ref <|w__9 with ProcState_F = tup__2|>
    else
      if (or_bool (eq_vec target_mode M32_Abort) (eq_vec target_mode M32_IRQ))
      then
        let split_vec = [B1;B1] in
        let (tup__0, tup__1) =
          ((subrange_vec_dec split_vec (1:ii) (1:ii) : list bitU),(subrange_vec_dec
                                                                     split_vec
                                                                     (0:ii)
                                                                     (0:ii) : list bitU)) in
        read_reg PSTATE_ref >>= fun (w__10 : ProcState) ->
        write_reg PSTATE_ref <|w__10 with ProcState_A = tup__0|> >>
        read_reg PSTATE_ref >>= fun (w__11 : ProcState) ->
        write_reg PSTATE_ref <|w__11 with ProcState_I = tup__1|>
      else
        read_reg PSTATE_ref >>= fun (w__12 : ProcState) ->
        write_reg PSTATE_ref <|w__12 with ProcState_I = ([B1])|>) >>
   read_reg PSTATE_ref >>= fun (w__13 : ProcState) ->
   (read_reg SCTLR_ref : M (list bitU)) >>= fun (w__14 : bits ty32) ->
   write_reg PSTATE_ref <|w__13 with ProcState_E = ([access_vec_dec w__14 (25:ii)])|> >>
   read_reg PSTATE_ref >>= fun (w__15 : ProcState) ->
   write_reg PSTATE_ref <|w__15 with ProcState_IL = ([B0])|> >>
   read_reg PSTATE_ref >>= fun (w__16 : ProcState) ->
   write_reg PSTATE_ref <|w__16 with ProcState_IT = ([B0;B0;B0;B0;B0;B0;B0;B0])|> >>
   (read_reg SCTLR_ref : M (list bitU)) >>= fun (w__17 : bits ty32) ->
   (if (and_bool (HavePANExt ()) (eq_vec ([access_vec_dec w__17 (23:ii)]) ([B0])))
    then
      read_reg PSTATE_ref >>= fun (w__18 : ProcState) ->
      write_reg PSTATE_ref <|w__18 with ProcState_PAN = ([B1])|>
    else return ()) >>
   (ExcVectorBase () : M (list bitU)) >>= fun (w__19 : list bitU) ->
   BranchTo
     (concat_vec
        (slice w__19 (5:ii) (27:ii) : list bitU)
        (__GetSlice_int (5:ii) vect_offset (0:ii) : list bitU) : list bitU)
     BranchType_UNKNOWN >>
   return (EndOfInstruction ())

val AArch32_GeneralExceptionsToAArch64 : unit -> M bool

let AArch32_GeneralExceptionsToAArch64 () =
   read_reg PSTATE_ref >>= fun (w__0 : ProcState) ->
   ELUsingAArch32 EL1 >>= fun (w__1 : bool) ->
   IsSecure () >>= fun (w__2 : bool) ->
   ELUsingAArch32 EL2 >>= fun (w__3 : bool) ->
   (read_reg HCR_EL2_ref : M (list bitU)) >>= fun (w__4 : bits ty64) ->
   return (or_bool
             (and_bool (eq_vec w__0.ProcState_EL EL0) (not w__1))
             (and_bool
                (and_bool (and_bool (HaveEL EL2) (not w__2)) (not w__3))
                (eq_vec ([access_vec_dec w__4 (27:ii)]) ([B1]))))

val AArch32_EnterHypMode : ExceptionRecord -> list bitU -> ii -> M unit

let AArch32_EnterHypMode exception preferred_exception_return vect_offset =
   let (_ : unit) = SynchronizeContext () in
   IsSecure () >>= fun (w__0 : bool) ->
   ELUsingAArch32 EL2 >>= fun (w__1 : bool) ->
   assert_exp (and_bool (and_bool (HaveEL EL2) (not w__0)) w__1) "((HaveEL(EL2) && !(IsSecure())) && ELUsingAArch32(EL2))" >>
   (GetPSRFromPSTATE () : M (list bitU)) >>= fun (spsr : bits ty32) ->
   (if (not
          (or_bool
             (eq exception.ExceptionRecord_typ Exception_IRQ)
             (eq exception.ExceptionRecord_typ Exception_FIQ)))
    then AArch32_ReportHypEntry exception
    else return ()) >>
   AArch32_WriteMode M32_Hyp >>
   aset_SPSR spsr >>
   write_reg ELR_hyp_ref preferred_exception_return >>
   read_reg PSTATE_ref >>= fun (w__2 : ProcState) ->
   (read_reg HSCTLR_ref : M (list bitU)) >>= fun (w__3 : bits ty32) ->
   write_reg PSTATE_ref <|w__2 with ProcState_T = ([access_vec_dec w__3 (30:ii)])|> >>
   read_reg PSTATE_ref >>= fun (w__4 : ProcState) ->
   write_reg PSTATE_ref <|w__4 with ProcState_SS = ([B0])|> >>
   (aget_SCR_GEN () : M (list bitU)) >>= fun (w__5 : list bitU) ->
   (if (or_bool (not (HaveEL EL3)) (eq_vec ([access_vec_dec w__5 (3:ii)]) ([B0])))
    then
      read_reg PSTATE_ref >>= fun (w__6 : ProcState) ->
      write_reg PSTATE_ref <|w__6 with ProcState_A = ([B1])|>
    else return ()) >>
   (aget_SCR_GEN () : M (list bitU)) >>= fun (w__7 : list bitU) ->
   (if (or_bool (not (HaveEL EL3)) (eq_vec ([access_vec_dec w__7 (1:ii)]) ([B0])))
    then
      read_reg PSTATE_ref >>= fun (w__8 : ProcState) ->
      write_reg PSTATE_ref <|w__8 with ProcState_I = ([B1])|>
    else return ()) >>
   (aget_SCR_GEN () : M (list bitU)) >>= fun (w__9 : list bitU) ->
   (if (or_bool (not (HaveEL EL3)) (eq_vec ([access_vec_dec w__9 (2:ii)]) ([B0])))
    then
      read_reg PSTATE_ref >>= fun (w__10 : ProcState) ->
      write_reg PSTATE_ref <|w__10 with ProcState_F = ([B1])|>
    else return ()) >>
   read_reg PSTATE_ref >>= fun (w__11 : ProcState) ->
   (read_reg HSCTLR_ref : M (list bitU)) >>= fun (w__12 : bits ty32) ->
   write_reg PSTATE_ref <|w__11 with ProcState_E = ([access_vec_dec w__12 (25:ii)])|> >>
   read_reg PSTATE_ref >>= fun (w__13 : ProcState) ->
   write_reg PSTATE_ref <|w__13 with ProcState_IL = ([B0])|> >>
   read_reg PSTATE_ref >>= fun (w__14 : ProcState) ->
   write_reg PSTATE_ref <|w__14 with ProcState_IT = ([B0;B0;B0;B0;B0;B0;B0;B0])|> >>
   (read_reg HVBAR_ref : M (list bitU)) >>= fun (w__15 : bits ty32) ->
   BranchTo
     (concat_vec
        (slice w__15 (5:ii) (27:ii) : list bitU)
        (__GetSlice_int (5:ii) vect_offset (0:ii) : list bitU) : list bitU)
     BranchType_UNKNOWN >>
   return (EndOfInstruction ())

val AArch32_TakeUndefInstrException__0 : unit -> M unit

val AArch32_TakeUndefInstrException__1 : ExceptionRecord -> M unit

let AArch32_TakeUndefInstrException__1 exception =
   IsSecure () >>= fun (w__0 : bool) ->
   read_reg PSTATE_ref >>= fun (w__1 : ProcState) ->
   (read_reg HCR_ref : M (list bitU)) >>= fun (w__2 : bits ty32) ->
   let (route_to_hyp : bool) =
     and_bool
       (and_bool (and_bool (HaveEL EL2) (not w__0)) (eq_vec w__1.ProcState_EL EL0))
       (eq_vec ([access_vec_dec w__2 (27:ii)]) ([B1])) in
   (ThisInstrAddr (32:ii) () : M (list bitU)) >>= fun (preferred_exception_return : bits ty32) ->
   let (vect_offset : ii) = (4:ii) in
   CurrentInstrSet () >>= fun (w__3 : InstrSet) ->
   let (lr_offset : ii) = if (eq w__3 InstrSet_A32) then (4:ii) else (2:ii) in
   read_reg PSTATE_ref >>= fun (w__4 : ProcState) ->
   if (eq_vec w__4.ProcState_EL EL2)
   then AArch32_EnterHypMode exception preferred_exception_return vect_offset
   else
     if route_to_hyp
     then AArch32_EnterHypMode exception preferred_exception_return (20:ii)
     else AArch32_EnterMode M32_Undef preferred_exception_return lr_offset vect_offset

let AArch32_TakeUndefInstrException__0 () =
   let (exception : ExceptionRecord) = ExceptionSyndrome Exception_Uncategorized in
   AArch32_TakeUndefInstrException__1 exception

val UnallocatedEncoding : unit -> M unit

let UnallocatedEncoding () =
   UsingAArch32 () >>= fun (w__0 : bool) ->
   AArch32_ExecutingCP10or11Instr () >>= fun (w__1 : bool) ->
   (if (and_bool w__0 w__1)
    then
      (read_reg FPEXC_ref : M (list bitU)) >>= fun (w__2 : list bitU) ->
      write_reg FPEXC_ref (set_slice (32:ii) (1:ii) w__2 (29:ii) ([B0]) : list bitU)
    else return ()) >>
   UsingAArch32 () >>= fun (w__3 : bool) ->
   AArch32_GeneralExceptionsToAArch64 () >>= fun (w__4 : bool) ->
   if (and_bool w__3 (not w__4))
   then AArch32_TakeUndefInstrException__0 ()
   else AArch64_UndefinedFault ()

val aarch64_memory_single_general_immediate_unsigned : AccType -> integer -> MemOp -> ii -> list bitU -> bool -> integer -> bool -> ii -> bool -> M unit

let aarch64_memory_single_general_immediate_unsigned acctype datasize memop n offset postindex regsize signed t wback__arg =
   assert_exp true "destsize constraint" >>
   let dbytes = ex_int (integerDiv datasize (8:ii)) in
   assert_exp true "datasize constraint" >>
   assert_exp true "dbytes constraint" >>
   let wback = wback__arg in
   let (address : bits ty64) = (undefined_vector (64:ii) (undefined_bit ()) : list bitU) in
   let data = (undefined_vector datasize (undefined_bit ()) : list bitU) in
   let (wb_unknown : bool) = false in
   let (rt_unknown : bool) = false in
   let (c : Constraint) = undefined_Constraint () in
   (if (and_bool
          (and_bool (and_bool (eq memop MemOp_LOAD) wback) (eq (ex_int n) (ex_int t)))
          (neq (ex_int n) (31:ii)))
    then
      let c = ConstrainUnpredictable Unpredictable_WBOVERLAPLD in
      assert_exp (or_bool
                    (eq c Constraint_WBSUPPRESS)
                    (or_bool
                       (eq c Constraint_UNKNOWN)
                       (or_bool (eq c Constraint_UNDEF) (eq c Constraint_NOP)))) "((c == Constraint_WBSUPPRESS) || ((c == Constraint_UNKNOWN) || ((c == Constraint_UNDEF) || (c == Constraint_NOP))))" >>
      match c with
      | Constraint_WBSUPPRESS ->
         let (wback : bool) = false in
         return (wb_unknown,wback)
      | Constraint_UNKNOWN ->
         let (wb_unknown : bool) = true in
         return (wb_unknown,wback)
      | Constraint_UNDEF ->
         UnallocatedEncoding () >>
         return (wb_unknown,wback)
      | Constraint_NOP -> return (wb_unknown,wback)
      end >>= fun ((wb_unknown : bool), (wback : bool)) ->
      return (c,wb_unknown,wback)
    else return (c,wb_unknown,wback)) >>= fun ((c : Constraint), (wb_unknown : bool), (wback : bool)) ->
   (if (and_bool
          (and_bool (and_bool (eq memop MemOp_STORE) wback) (eq (ex_int n) (ex_int t)))
          (neq (ex_int n) (31:ii)))
    then
      let c = ConstrainUnpredictable Unpredictable_WBOVERLAPST in
      assert_exp (or_bool
                    (eq c Constraint_NONE)
                    (or_bool
                       (eq c Constraint_UNKNOWN)
                       (or_bool (eq c Constraint_UNDEF) (eq c Constraint_NOP)))) "((c == Constraint_NONE) || ((c == Constraint_UNKNOWN) || ((c == Constraint_UNDEF) || (c == Constraint_NOP))))" >>
      match c with
      | Constraint_NONE ->
         let (rt_unknown : bool) = false in
         return rt_unknown
      | Constraint_UNKNOWN ->
         let (rt_unknown : bool) = true in
         return rt_unknown
      | Constraint_UNDEF ->
         UnallocatedEncoding () >>
         return rt_unknown
      | Constraint_NOP -> return rt_unknown
      end >>= fun (rt_unknown : bool) ->
      return (c,rt_unknown)
    else return (c,rt_unknown)) >>= fun ((c : Constraint), (rt_unknown : bool)) ->
   (if (eq (ex_int n) (31:ii))
    then
      (if (neq memop MemOp_PREFETCH)
       then CheckSPAlignment ()
       else return ()) >>
      (aget_SP (64:ii) () : M (list bitU)) >>= fun (w__0 : bits ty64) ->
      let (address : bits ty64) = w__0 in
      return address
    else
      (aget_X (64:ii) n : M (list bitU)) >>= fun (w__1 : bits ty64) ->
      let (address : bits ty64) = w__1 in
      return address) >>= fun (address : bits ty64) ->
   let (address : bits ty64) =
     if (not postindex)
     then
       let (address : bits ty64) = (add_vec address offset : list bitU) in
       address
     else address in
   match memop with
   | MemOp_STORE ->
      (if rt_unknown
       then
         let data = (undefined_vector (length data) (undefined_bit ()) : list bitU) in
         return data
       else
         (aget_X (length data) t : M (list bitU)) >>= fun w__2 ->
         let data = w__2 in
         return data) >>= fun data ->
      aset_Mem address dbytes acctype data >>
      return data
   | MemOp_LOAD ->
      (aget_Mem address dbytes acctype : M (list bitU)) >>= fun w__3 ->
      let data = w__3 in
      (if signed
       then
         (SignExtend__0 data regsize : M (list bitU)) >>= fun (w__4 : list bitU) ->
         aset_X t w__4
       else
         (ZeroExtend__0 data regsize : M (list bitU)) >>= fun (w__5 : list bitU) ->
         aset_X t w__5) >>
      return data
   | MemOp_PREFETCH -> return data
   end >>= fun data ->
   (if wback
    then
      let (address : bits ty64) =
        if wb_unknown
        then
          let (address : bits ty64) = (undefined_vector (64:ii) (undefined_bit ()) : list bitU) in
          address
        else
          let (address : bits ty64) =
            if postindex
            then
              let (address : bits ty64) = (add_vec address offset : list bitU) in
              address
            else address in
          address in
      (if (eq (ex_int n) (31:ii))
       then aset_SP address
       else aset_X n address) >>
      return address
    else return address) >>= fun (address : bits ty64) ->
   return ()

val aarch64_memory_single_general_immediate_signed_postidx : AccType -> integer -> MemOp -> ii -> list bitU -> bool -> integer -> bool -> ii -> bool -> M unit

let aarch64_memory_single_general_immediate_signed_postidx acctype datasize memop n offset postindex regsize signed t wback__arg =
   assert_exp true "destsize constraint" >>
   let dbytes = ex_int (integerDiv datasize (8:ii)) in
   assert_exp true "datasize constraint" >>
   assert_exp true "dbytes constraint" >>
   let wback = wback__arg in
   let (address : bits ty64) = (undefined_vector (64:ii) (undefined_bit ()) : list bitU) in
   let data = (undefined_vector datasize (undefined_bit ()) : list bitU) in
   let (wb_unknown : bool) = false in
   let (rt_unknown : bool) = false in
   let (c : Constraint) = undefined_Constraint () in
   (if (and_bool
          (and_bool (and_bool (eq memop MemOp_LOAD) wback) (eq (ex_int n) (ex_int t)))
          (neq (ex_int n) (31:ii)))
    then
      let c = ConstrainUnpredictable Unpredictable_WBOVERLAPLD in
      assert_exp (or_bool
                    (eq c Constraint_WBSUPPRESS)
                    (or_bool
                       (eq c Constraint_UNKNOWN)
                       (or_bool (eq c Constraint_UNDEF) (eq c Constraint_NOP)))) "((c == Constraint_WBSUPPRESS) || ((c == Constraint_UNKNOWN) || ((c == Constraint_UNDEF) || (c == Constraint_NOP))))" >>
      match c with
      | Constraint_WBSUPPRESS ->
         let (wback : bool) = false in
         return (wb_unknown,wback)
      | Constraint_UNKNOWN ->
         let (wb_unknown : bool) = true in
         return (wb_unknown,wback)
      | Constraint_UNDEF ->
         UnallocatedEncoding () >>
         return (wb_unknown,wback)
      | Constraint_NOP -> return (wb_unknown,wback)
      end >>= fun ((wb_unknown : bool), (wback : bool)) ->
      return (c,wb_unknown,wback)
    else return (c,wb_unknown,wback)) >>= fun ((c : Constraint), (wb_unknown : bool), (wback : bool)) ->
   (if (and_bool
          (and_bool (and_bool (eq memop MemOp_STORE) wback) (eq (ex_int n) (ex_int t)))
          (neq (ex_int n) (31:ii)))
    then
      let c = ConstrainUnpredictable Unpredictable_WBOVERLAPST in
      assert_exp (or_bool
                    (eq c Constraint_NONE)
                    (or_bool
                       (eq c Constraint_UNKNOWN)
                       (or_bool (eq c Constraint_UNDEF) (eq c Constraint_NOP)))) "((c == Constraint_NONE) || ((c == Constraint_UNKNOWN) || ((c == Constraint_UNDEF) || (c == Constraint_NOP))))" >>
      match c with
      | Constraint_NONE ->
         let (rt_unknown : bool) = false in
         return rt_unknown
      | Constraint_UNKNOWN ->
         let (rt_unknown : bool) = true in
         return rt_unknown
      | Constraint_UNDEF ->
         UnallocatedEncoding () >>
         return rt_unknown
      | Constraint_NOP -> return rt_unknown
      end >>= fun (rt_unknown : bool) ->
      return (c,rt_unknown)
    else return (c,rt_unknown)) >>= fun ((c : Constraint), (rt_unknown : bool)) ->
   (if (eq (ex_int n) (31:ii))
    then
      (if (neq memop MemOp_PREFETCH)
       then CheckSPAlignment ()
       else return ()) >>
      (aget_SP (64:ii) () : M (list bitU)) >>= fun (w__0 : bits ty64) ->
      let (address : bits ty64) = w__0 in
      return address
    else
      (aget_X (64:ii) n : M (list bitU)) >>= fun (w__1 : bits ty64) ->
      let (address : bits ty64) = w__1 in
      return address) >>= fun (address : bits ty64) ->
   let (address : bits ty64) =
     if (not postindex)
     then
       let (address : bits ty64) = (add_vec address offset : list bitU) in
       address
     else address in
   match memop with
   | MemOp_STORE ->
      (if rt_unknown
       then
         let data = (undefined_vector (length data) (undefined_bit ()) : list bitU) in
         return data
       else
         (aget_X (length data) t : M (list bitU)) >>= fun w__2 ->
         let data = w__2 in
         return data) >>= fun data ->
      aset_Mem address dbytes acctype data >>
      return data
   | MemOp_LOAD ->
      (aget_Mem address dbytes acctype : M (list bitU)) >>= fun w__3 ->
      let data = w__3 in
      (if signed
       then
         (SignExtend__0 data regsize : M (list bitU)) >>= fun (w__4 : list bitU) ->
         aset_X t w__4
       else
         (ZeroExtend__0 data regsize : M (list bitU)) >>= fun (w__5 : list bitU) ->
         aset_X t w__5) >>
      return data
   | MemOp_PREFETCH -> return data
   end >>= fun data ->
   (if wback
    then
      let (address : bits ty64) =
        if wb_unknown
        then
          let (address : bits ty64) = (undefined_vector (64:ii) (undefined_bit ()) : list bitU) in
          address
        else
          let (address : bits ty64) =
            if postindex
            then
              let (address : bits ty64) = (add_vec address offset : list bitU) in
              address
            else address in
          address in
      (if (eq (ex_int n) (31:ii))
       then aset_SP address
       else aset_X n address) >>
      return address
    else return address) >>= fun (address : bits ty64) ->
   return ()

val memory_single_general_immediate_unsigned_aarch64_memory_single_general_immediate_unsigned__decode : list bitU -> list bitU -> list bitU -> list bitU -> list bitU -> list bitU -> M unit

let memory_single_general_immediate_unsigned_aarch64_memory_single_general_immediate_unsigned__decode size V opc imm12 Rn Rt =
   write_reg __unconditional_ref true >>
   let (wback : bool) = false in
   let (postindex : bool) = false in
   let (scale : ii) = uint size in
   (ZeroExtend__0 imm12 (64:ii) : M (list bitU)) >>= fun (w__0 : list bitU) ->
   (LSL w__0 scale : M (list bitU)) >>= fun (offset : bits ty64) ->
   let (n : ii) = uint Rn in
   let (t : ii) = uint Rt in
   let (acctype : AccType) = AccType_NORMAL in
   let (memop : MemOp) = undefined_MemOp () in
   let (signed : bool) = undefined_bool () in
   let (regsize : ii) = undefined_int () in
   (if (eq_vec ([access_vec_dec opc (1:ii)]) ([B0]))
    then
      let (memop : MemOp) =
        if (eq_vec ([access_vec_dec opc (0:ii)]) ([B1]))
        then MemOp_LOAD
        else MemOp_STORE in
      let (regsize : ii) = if (eq_vec size ([B1;B1])) then (64:ii) else (32:ii) in
      let (signed : bool) = false in
      return (memop,regsize,signed)
    else
      (if (eq_vec size ([B1;B1]))
       then
         let memop = MemOp_PREFETCH in
         (if (eq_vec ([access_vec_dec opc (0:ii)]) ([B1]))
          then UnallocatedEncoding ()
          else return ()) >>
         return (memop,regsize,signed)
       else
         let memop = MemOp_LOAD in
         (if (and_bool (eq_vec size ([B1;B0])) (eq_vec ([access_vec_dec opc (0:ii)]) ([B1])))
          then UnallocatedEncoding ()
          else return ()) >>
         let (regsize : ii) =
           if (eq_vec ([access_vec_dec opc (0:ii)]) ([B1]))
           then (32:ii)
           else (64:ii) in
         let (signed : bool) = true in
         return (memop,regsize,signed)) >>= fun ((memop : MemOp), (regsize : ii), (signed : bool)) ->
      return (memop,regsize,signed)) >>= fun ((memop : MemOp), (regsize : ii), (signed : bool)) ->
   let (datasize : ii) = shl_int (8:ii) scale in
   aarch64_memory_single_general_immediate_unsigned
     acctype
     (ex_int datasize)
     memop
     n
     offset
     postindex
     (ex_int regsize)
     signed
     t
     wback

val memory_single_general_immediate_unsigned_aarch64_memory_single_general_immediate_signed_postidx__decode : list bitU -> list bitU -> list bitU -> list bitU -> list bitU -> list bitU -> M unit

let memory_single_general_immediate_unsigned_aarch64_memory_single_general_immediate_signed_postidx__decode size V opc imm12 Rn Rt =
   write_reg __unconditional_ref true >>
   let (wback : bool) = false in
   let (postindex : bool) = false in
   let (scale : ii) = uint size in
   (ZeroExtend__0 imm12 (64:ii) : M (list bitU)) >>= fun (w__0 : list bitU) ->
   (LSL w__0 scale : M (list bitU)) >>= fun (offset : bits ty64) ->
   let (n : ii) = uint Rn in
   let (t : ii) = uint Rt in
   let (acctype : AccType) = AccType_NORMAL in
   let (memop : MemOp) = undefined_MemOp () in
   let (signed : bool) = undefined_bool () in
   let (regsize : ii) = undefined_int () in
   (if (eq_vec ([access_vec_dec opc (1:ii)]) ([B0]))
    then
      let (memop : MemOp) =
        if (eq_vec ([access_vec_dec opc (0:ii)]) ([B1]))
        then MemOp_LOAD
        else MemOp_STORE in
      let (regsize : ii) = if (eq_vec size ([B1;B1])) then (64:ii) else (32:ii) in
      let (signed : bool) = false in
      return (memop,regsize,signed)
    else
      (if (eq_vec size ([B1;B1]))
       then
         UnallocatedEncoding () >>
         return (memop,regsize,signed)
       else
         let memop = MemOp_LOAD in
         (if (and_bool (eq_vec size ([B1;B0])) (eq_vec ([access_vec_dec opc (0:ii)]) ([B1])))
          then UnallocatedEncoding ()
          else return ()) >>
         let (regsize : ii) =
           if (eq_vec ([access_vec_dec opc (0:ii)]) ([B1]))
           then (32:ii)
           else (64:ii) in
         let (signed : bool) = true in
         return (memop,regsize,signed)) >>= fun ((memop : MemOp), (regsize : ii), (signed : bool)) ->
      return (memop,regsize,signed)) >>= fun ((memop : MemOp), (regsize : ii), (signed : bool)) ->
   let (datasize : ii) = shl_int (8:ii) scale in
   aarch64_memory_single_general_immediate_signed_postidx
     acctype
     (ex_int datasize)
     memop
     n
     offset
     postindex
     (ex_int regsize)
     signed
     t
     wback

val memory_single_general_immediate_signed_preidx_aarch64_memory_single_general_immediate_signed_postidx__decode : list bitU -> list bitU -> list bitU -> list bitU -> list bitU -> list bitU -> M unit

let memory_single_general_immediate_signed_preidx_aarch64_memory_single_general_immediate_signed_postidx__decode size V opc imm9 Rn Rt =
   write_reg __unconditional_ref true >>
   let (wback : bool) = true in
   let (postindex : bool) = false in
   let (scale : ii) = uint size in
   (SignExtend__0 imm9 (64:ii) : M (list bitU)) >>= fun (offset : bits ty64) ->
   let (n : ii) = uint Rn in
   let (t : ii) = uint Rt in
   let (acctype : AccType) = AccType_NORMAL in
   let (memop : MemOp) = undefined_MemOp () in
   let (signed : bool) = undefined_bool () in
   let (regsize : ii) = undefined_int () in
   (if (eq_vec ([access_vec_dec opc (1:ii)]) ([B0]))
    then
      let (memop : MemOp) =
        if (eq_vec ([access_vec_dec opc (0:ii)]) ([B1]))
        then MemOp_LOAD
        else MemOp_STORE in
      let (regsize : ii) = if (eq_vec size ([B1;B1])) then (64:ii) else (32:ii) in
      let (signed : bool) = false in
      return (memop,regsize,signed)
    else
      (if (eq_vec size ([B1;B1]))
       then
         UnallocatedEncoding () >>
         return (memop,regsize,signed)
       else
         let memop = MemOp_LOAD in
         (if (and_bool (eq_vec size ([B1;B0])) (eq_vec ([access_vec_dec opc (0:ii)]) ([B1])))
          then UnallocatedEncoding ()
          else return ()) >>
         let (regsize : ii) =
           if (eq_vec ([access_vec_dec opc (0:ii)]) ([B1]))
           then (32:ii)
           else (64:ii) in
         let (signed : bool) = true in
         return (memop,regsize,signed)) >>= fun ((memop : MemOp), (regsize : ii), (signed : bool)) ->
      return (memop,regsize,signed)) >>= fun ((memop : MemOp), (regsize : ii), (signed : bool)) ->
   let (datasize : ii) = shl_int (8:ii) scale in
   aarch64_memory_single_general_immediate_signed_postidx
     acctype
     (ex_int datasize)
     memop
     n
     offset
     postindex
     (ex_int regsize)
     signed
     t
     wback

val memory_single_general_immediate_signed_postidx_aarch64_memory_single_general_immediate_signed_postidx__decode : list bitU -> list bitU -> list bitU -> list bitU -> list bitU -> list bitU -> M unit

let memory_single_general_immediate_signed_postidx_aarch64_memory_single_general_immediate_signed_postidx__decode size V opc imm9 Rn Rt =
   write_reg __unconditional_ref true >>
   let (wback : bool) = true in
   let (postindex : bool) = true in
   let (scale : ii) = uint size in
   (SignExtend__0 imm9 (64:ii) : M (list bitU)) >>= fun (offset : bits ty64) ->
   let (n : ii) = uint Rn in
   let (t : ii) = uint Rt in
   let (acctype : AccType) = AccType_NORMAL in
   let (memop : MemOp) = undefined_MemOp () in
   let (signed : bool) = undefined_bool () in
   let (regsize : ii) = undefined_int () in
   (if (eq_vec ([access_vec_dec opc (1:ii)]) ([B0]))
    then
      let (memop : MemOp) =
        if (eq_vec ([access_vec_dec opc (0:ii)]) ([B1]))
        then MemOp_LOAD
        else MemOp_STORE in
      let (regsize : ii) = if (eq_vec size ([B1;B1])) then (64:ii) else (32:ii) in
      let (signed : bool) = false in
      return (memop,regsize,signed)
    else
      (if (eq_vec size ([B1;B1]))
       then
         UnallocatedEncoding () >>
         return (memop,regsize,signed)
       else
         let memop = MemOp_LOAD in
         (if (and_bool (eq_vec size ([B1;B0])) (eq_vec ([access_vec_dec opc (0:ii)]) ([B1])))
          then UnallocatedEncoding ()
          else return ()) >>
         let (regsize : ii) =
           if (eq_vec ([access_vec_dec opc (0:ii)]) ([B1]))
           then (32:ii)
           else (64:ii) in
         let (signed : bool) = true in
         return (memop,regsize,signed)) >>= fun ((memop : MemOp), (regsize : ii), (signed : bool)) ->
      return (memop,regsize,signed)) >>= fun ((memop : MemOp), (regsize : ii), (signed : bool)) ->
   let (datasize : ii) = shl_int (8:ii) scale in
   aarch64_memory_single_general_immediate_signed_postidx
     acctype
     (ex_int datasize)
     memop
     n
     offset
     postindex
     (ex_int regsize)
     signed
     t
     wback

val ReservedValue : unit -> M unit

let ReservedValue () =
   UsingAArch32 () >>= fun (w__0 : bool) ->
   AArch32_GeneralExceptionsToAArch64 () >>= fun (w__1 : bool) ->
   if (and_bool w__0 (not w__1))
   then AArch32_TakeUndefInstrException__0 ()
   else AArch64_UndefinedFault ()

val integer_arithmetic_addsub_immediate_decode : list bitU -> list bitU -> list bitU -> list bitU -> list bitU -> list bitU -> list bitU -> M unit

let integer_arithmetic_addsub_immediate_decode sf op S shift imm12 Rn Rd =
   write_reg __unconditional_ref true >>
   let (d : ii) = uint Rd in
   let (n : ii) = uint Rn in
   let (datasize : integer) = if (eq_vec sf ([B1])) then (64:ii) else (32:ii) in
   let (sub_op : bool) = eq_vec op ([B1]) in
   let (setflags : bool) = eq_vec S ([B1]) in
   let imm = (undefined_vector datasize (undefined_bit ()) : list bitU) in
   let b__0 = shift in
   (if (eq_vec b__0 ([B0;B0]))
    then
      (ZeroExtend__0 imm12 datasize : M (list bitU)) >>= fun w__0 ->
      let imm = w__0 in
      return imm
    else
      (if (eq_vec b__0 ([B0;B1]))
       then
         (ZeroExtend__0 (concat_vec imm12 (Zeros__0 (12:ii) : list bitU) : list bitU) datasize : M (list bitU)) >>= fun w__1 ->
         let imm = w__1 in
         return imm
       else
         ReservedValue () >>
         return imm) >>= fun imm ->
      return imm) >>= fun imm ->
   aarch64_integer_arithmetic_addsub_immediate d datasize imm n setflags sub_op

val decode : list bitU -> M unit

let decode op_code =
   if (eq_vec (subrange_vec_dec op_code (29:ii) (24:ii) : list bitU) ([B1;B1;B1;B0;B0;B1]))
   then
     let (size : bits ty2) = (subrange_vec_dec op_code (31:ii) (30:ii) : list bitU) in
     let (V : bits ty1) = [access_vec_dec op_code (26:ii)] in
     let (opc : bits ty2) = (subrange_vec_dec op_code (23:ii) (22:ii) : list bitU) in
     let (imm12 : bits ty12) = (subrange_vec_dec op_code (21:ii) (10:ii) : list bitU) in
     let (Rn : bits ty5) = (subrange_vec_dec op_code (9:ii) (5:ii) : list bitU) in
     let (Rt : bits ty5) = (subrange_vec_dec op_code (4:ii) (0:ii) : list bitU) in
     memory_single_general_immediate_unsigned_aarch64_memory_single_general_immediate_unsigned__decode
       size
       V
       opc
       imm12
       Rn
       Rt
   else
     if (and_bool
           (eq_vec (subrange_vec_dec op_code (29:ii) (24:ii) : list bitU) ([B1;B1;B1;B0;B0;B0]))
           (and_bool
              (eq_vec (subrange_vec_dec op_code (21:ii) (21:ii) : list bitU) ([B0]))
              (eq_vec (subrange_vec_dec op_code (11:ii) (10:ii) : list bitU) ([B0;B1]))))
     then
       let (size : bits ty2) = (subrange_vec_dec op_code (31:ii) (30:ii) : list bitU) in
       let (V : bits ty1) = [access_vec_dec op_code (26:ii)] in
       let (opc : bits ty2) = (subrange_vec_dec op_code (23:ii) (22:ii) : list bitU) in
       let (imm9 : bits ty9) = (subrange_vec_dec op_code (20:ii) (12:ii) : list bitU) in
       let (Rn : bits ty5) = (subrange_vec_dec op_code (9:ii) (5:ii) : list bitU) in
       let (Rt : bits ty5) = (subrange_vec_dec op_code (4:ii) (0:ii) : list bitU) in
       memory_single_general_immediate_signed_postidx_aarch64_memory_single_general_immediate_signed_postidx__decode
         size
         V
         opc
         imm9
         Rn
         Rt
     else
       if (and_bool
             (eq_vec (subrange_vec_dec op_code (29:ii) (24:ii) : list bitU) ([B1;B1;B1;B0;B0;B0]))
             (and_bool
                (eq_vec (subrange_vec_dec op_code (21:ii) (21:ii) : list bitU) ([B0]))
                (eq_vec (subrange_vec_dec op_code (11:ii) (10:ii) : list bitU) ([B1;B1]))))
       then
         let (size : bits ty2) = (subrange_vec_dec op_code (31:ii) (30:ii) : list bitU) in
         let (V : bits ty1) = [access_vec_dec op_code (26:ii)] in
         let (opc : bits ty2) = (subrange_vec_dec op_code (23:ii) (22:ii) : list bitU) in
         let (imm9 : bits ty9) = (subrange_vec_dec op_code (20:ii) (12:ii) : list bitU) in
         let (Rn : bits ty5) = (subrange_vec_dec op_code (9:ii) (5:ii) : list bitU) in
         let (Rt : bits ty5) = (subrange_vec_dec op_code (4:ii) (0:ii) : list bitU) in
         memory_single_general_immediate_signed_preidx_aarch64_memory_single_general_immediate_signed_postidx__decode
           size
           V
           opc
           imm9
           Rn
           Rt
       else
         if (eq_vec (subrange_vec_dec op_code (29:ii) (24:ii) : list bitU) ([B1;B1;B1;B0;B0;B1]))
         then
           let (size : bits ty2) = (subrange_vec_dec op_code (31:ii) (30:ii) : list bitU) in
           let (V : bits ty1) = [access_vec_dec op_code (26:ii)] in
           let (opc : bits ty2) = (subrange_vec_dec op_code (23:ii) (22:ii) : list bitU) in
           let (imm12 : bits ty12) = (subrange_vec_dec op_code (21:ii) (10:ii) : list bitU) in
           let (Rn : bits ty5) = (subrange_vec_dec op_code (9:ii) (5:ii) : list bitU) in
           let (Rt : bits ty5) = (subrange_vec_dec op_code (4:ii) (0:ii) : list bitU) in
           memory_single_general_immediate_unsigned_aarch64_memory_single_general_immediate_signed_postidx__decode
             size
             V
             opc
             imm12
             Rn
             Rt
         else
           let (sf : bits ty1) = [access_vec_dec op_code (31:ii)] in
           let (op : bits ty1) = [access_vec_dec op_code (30:ii)] in
           let (S : bits ty1) = [access_vec_dec op_code (29:ii)] in
           let (shift : bits ty2) = (subrange_vec_dec op_code (23:ii) (22:ii) : list bitU) in
           let (imm12 : bits ty12) = (subrange_vec_dec op_code (21:ii) (10:ii) : list bitU) in
           let (Rn : bits ty5) = (subrange_vec_dec op_code (9:ii) (5:ii) : list bitU) in
           let (Rd : bits ty5) = (subrange_vec_dec op_code (4:ii) (0:ii) : list bitU) in
           integer_arithmetic_addsub_immediate_decode sf op S shift imm12 Rn Rd

val initialize_registers : unit -> M unit

let initialize_registers () =
   write_reg __unconditional_ref (undefined_bool ()) >>
   write_reg __ThisInstrEnc_ref (undefined___InstrEnc ()) >>
   write_reg __ThisInstr_ref (undefined_vector (32:ii) (undefined_bit ()) : list bitU) >>
   write_reg __Memory_ref (undefined_vector (52:ii) (undefined_bit ()) : list bitU) >>
   write_reg __BranchTaken_ref (undefined_bool ()) >>
   write_reg
     _R_ref
     (undefined_vector (31:ii) (undefined_vector (64:ii) (undefined_bit ()) : list bitU) : list (list bitU)) >>
   write_reg _PC_ref (undefined_vector (64:ii) (undefined_bit ()) : list bitU) >>
   write_reg VBAR_EL3_ref (undefined_vector (64:ii) (undefined_bit ()) : list bitU) >>
   write_reg VBAR_EL2_ref (undefined_vector (64:ii) (undefined_bit ()) : list bitU) >>
   write_reg VBAR_EL1_ref (undefined_vector (64:ii) (undefined_bit ()) : list bitU) >>
   write_reg VBAR_ref (undefined_vector (32:ii) (undefined_bit ()) : list bitU) >>
   write_reg TCR_EL3_ref (undefined_vector (32:ii) (undefined_bit ()) : list bitU) >>
   write_reg TCR_EL2_ref (undefined_vector (64:ii) (undefined_bit ()) : list bitU) >>
   write_reg TCR_EL1_ref (undefined_vector (64:ii) (undefined_bit ()) : list bitU) >>
   write_reg SP_mon_ref (undefined_vector (32:ii) (undefined_bit ()) : list bitU) >>
   write_reg SP_EL3_ref (undefined_vector (64:ii) (undefined_bit ()) : list bitU) >>
   write_reg SP_EL2_ref (undefined_vector (64:ii) (undefined_bit ()) : list bitU) >>
   write_reg SP_EL1_ref (undefined_vector (64:ii) (undefined_bit ()) : list bitU) >>
   write_reg SP_EL0_ref (undefined_vector (64:ii) (undefined_bit ()) : list bitU) >>
   write_reg SPSR_und_ref (undefined_vector (32:ii) (undefined_bit ()) : list bitU) >>
   write_reg SPSR_svc_ref (undefined_vector (32:ii) (undefined_bit ()) : list bitU) >>
   write_reg SPSR_mon_ref (undefined_vector (32:ii) (undefined_bit ()) : list bitU) >>
   write_reg SPSR_irq_ref (undefined_vector (32:ii) (undefined_bit ()) : list bitU) >>
   write_reg SPSR_hyp_ref (undefined_vector (32:ii) (undefined_bit ()) : list bitU) >>
   write_reg SPSR_fiq_ref (undefined_vector (32:ii) (undefined_bit ()) : list bitU) >>
   write_reg SPSR_abt_ref (undefined_vector (32:ii) (undefined_bit ()) : list bitU) >>
   write_reg SPSR_EL3_ref (undefined_vector (32:ii) (undefined_bit ()) : list bitU) >>
   write_reg SPSR_EL2_ref (undefined_vector (32:ii) (undefined_bit ()) : list bitU) >>
   write_reg SPSR_EL1_ref (undefined_vector (32:ii) (undefined_bit ()) : list bitU) >>
   write_reg SCTLR_EL3_ref (undefined_vector (32:ii) (undefined_bit ()) : list bitU) >>
   write_reg SCTLR_EL2_ref (undefined_vector (32:ii) (undefined_bit ()) : list bitU) >>
   write_reg SCTLR_EL1_ref (undefined_vector (32:ii) (undefined_bit ()) : list bitU) >>
   write_reg SCTLR_ref (undefined_vector (32:ii) (undefined_bit ()) : list bitU) >>
   write_reg SCR_EL3_ref (undefined_vector (32:ii) (undefined_bit ()) : list bitU) >>
   write_reg SCR_ref (undefined_vector (32:ii) (undefined_bit ()) : list bitU) >>
   write_reg PSTATE_ref (undefined_ProcState ()) >>
   write_reg MDCR_EL2_ref (undefined_vector (32:ii) (undefined_bit ()) : list bitU) >>
   write_reg LR_mon_ref (undefined_vector (32:ii) (undefined_bit ()) : list bitU) >>
   write_reg HVBAR_ref (undefined_vector (32:ii) (undefined_bit ()) : list bitU) >>
   write_reg HSR_ref (undefined_vector (32:ii) (undefined_bit ()) : list bitU) >>
   write_reg HSCTLR_ref (undefined_vector (32:ii) (undefined_bit ()) : list bitU) >>
   write_reg HPFAR_EL2_ref (undefined_vector (64:ii) (undefined_bit ()) : list bitU) >>
   write_reg HPFAR_ref (undefined_vector (32:ii) (undefined_bit ()) : list bitU) >>
   write_reg HIFAR_ref (undefined_vector (32:ii) (undefined_bit ()) : list bitU) >>
   write_reg HDFAR_ref (undefined_vector (32:ii) (undefined_bit ()) : list bitU) >>
   write_reg HCR_EL2_ref (undefined_vector (64:ii) (undefined_bit ()) : list bitU) >>
   write_reg HCR_ref (undefined_vector (32:ii) (undefined_bit ()) : list bitU) >>
   write_reg FPEXC_ref (undefined_vector (32:ii) (undefined_bit ()) : list bitU) >>
   write_reg FAR_EL3_ref (undefined_vector (64:ii) (undefined_bit ()) : list bitU) >>
   write_reg FAR_EL2_ref (undefined_vector (64:ii) (undefined_bit ()) : list bitU) >>
   write_reg FAR_EL1_ref (undefined_vector (64:ii) (undefined_bit ()) : list bitU) >>
   write_reg ESR_EL3_ref (undefined_vector (32:ii) (undefined_bit ()) : list bitU) >>
   write_reg ESR_EL2_ref (undefined_vector (32:ii) (undefined_bit ()) : list bitU) >>
   write_reg ESR_EL1_ref (undefined_vector (32:ii) (undefined_bit ()) : list bitU) >>
   write_reg ELR_hyp_ref (undefined_vector (32:ii) (undefined_bit ()) : list bitU) >>
   write_reg ELR_EL3_ref (undefined_vector (64:ii) (undefined_bit ()) : list bitU) >>
   write_reg ELR_EL2_ref (undefined_vector (64:ii) (undefined_bit ()) : list bitU) >>
   write_reg ELR_EL1_ref (undefined_vector (64:ii) (undefined_bit ()) : list bitU)