xref: /seL4-l4v-10.1.1/HOL4/examples/l3-machine-code/arm/model/arm.sig

(* arm - generated by L3 - Wed Jan 31 15:06:54 2018 *)

signature arm =
sig

structure Map : Map

(* -------------------------------------------------------------------------
   Types
   ------------------------------------------------------------------------- *)

datatype Architecture
  = ARMv4 | ARMv4T | ARMv5T | ARMv5TE | ARMv6 | ARMv6K | ARMv6T2 | ARMv7_A
  | ARMv7_R

datatype Extensions
  = Extension_ThumbEE | Extension_Security | Extension_Multiprocessing
  | Extension_Virtualization | Extension_AdvanvedSIMD

type PSR =
  { A: bool, C: bool, E: bool, F: bool, GE: BitsN.nbit, I: bool,
    IT: BitsN.nbit, J: bool, M: BitsN.nbit, N: bool, Q: bool, T: bool,
    V: bool, Z: bool, psr'rst: BitsN.nbit }

type CP14 = { TEEHBR: BitsN.nbit }

type SCTLR =
  { A: bool, B: bool, BR: bool, C: bool, DZ: bool, EE: bool, FI: bool,
    I: bool, IE: bool, M: bool, NMFI: bool, RR: bool, SW: bool, TE: bool,
    U: bool, V: bool, VE: bool, Z: bool, sctlr'rst: BitsN.nbit }

type HSCTLR =
  { A: bool, C: bool, CP15BEN: bool, EE: bool, FI: bool, I: bool, M: bool,
    TE: bool, WXN: bool, hsctlr'rst: BitsN.nbit }

type HSR = { EC: BitsN.nbit, IL: bool, ISS: BitsN.nbit }

type SCR =
  { AW: bool, EA: bool, FIQ: bool, FW: bool, HCE: bool, IRQ: bool,
    NS: bool, SCD: bool, SIF: bool, nET: bool, scr'rst: BitsN.nbit }

type NSACR =
  { NSASEDIS: bool, NSD32DIS: bool, NSTRCDIS: bool, RFR: bool,
    cp: BitsN.nbit, nsacr'rst: BitsN.nbit }

type HCR =
  { AMO: bool, BSU: BitsN.nbit, DC: bool, FB: bool, FMO: bool, IMO: bool,
    PTW: bool, SWIO: bool, TAC: bool, TGE: bool, TID: BitsN.nbit,
    TIDCP: bool, TPC: bool, TPU: bool, TSC: bool, TSW: bool, TTLB: bool,
    TVM: bool, TWE: bool, TWI: bool, VA: bool, VF: bool, VI: bool,
    VM: bool, hcr'rst: BitsN.nbit }

type CP15 =
  { HCR: HCR, HSCTLR: HSCTLR, HSR: HSR, MVBAR: BitsN.nbit, NSACR: NSACR,
    SCR: SCR, SCTLR: SCTLR, VBAR: BitsN.nbit }

datatype InstrSet
  = InstrSet_ARM | InstrSet_Thumb | InstrSet_Jazelle | InstrSet_ThumbEE

datatype Encoding = Encoding_Thumb | Encoding_Thumb2 | Encoding_ARM

datatype RName
  = RName_0usr | RName_1usr | RName_2usr | RName_3usr | RName_4usr
  | RName_5usr | RName_6usr | RName_7usr | RName_8usr | RName_8fiq
  | RName_9usr | RName_9fiq | RName_10usr | RName_10fiq | RName_11usr
  | RName_11fiq | RName_12usr | RName_12fiq | RName_SPusr | RName_SPfiq
  | RName_SPirq | RName_SPsvc | RName_SPabt | RName_SPund | RName_SPmon
  | RName_SPhyp | RName_LRusr | RName_LRfiq | RName_LRirq | RName_LRsvc
  | RName_LRabt | RName_LRund | RName_LRmon | RName_PC

datatype SRType
  = SRType_LSL | SRType_LSR | SRType_ASR | SRType_ROR | SRType_RRX

datatype offset1
  = immediate_form1 of BitsN.nbit
  | register_form1 of BitsN.nbit * (SRType * Nat.nat)

datatype offset2
  = immediate_form2 of BitsN.nbit | register_form2 of BitsN.nbit

datatype VFPExtension = NoVFP | VFPv2 | VFPv3 | VFPv4

type FPSCR =
  { AHP: bool, C: bool, DN: bool, DZC: bool, DZE: bool, FZ: bool,
    IDC: bool, IDE: bool, IOC: bool, IOE: bool, IXC: bool, IXE: bool,
    N: bool, OFC: bool, OFE: bool, QC: bool, RMode: BitsN.nbit, UFC: bool,
    UFE: bool, V: bool, Z: bool, fpscr'rst: BitsN.nbit }

type FP = { FPSCR: FPSCR, REG: BitsN.nbit Map.map }

datatype VFPNegMul = VFPNegMul_VNMLA | VFPNegMul_VNMLS | VFPNegMul_VNMUL

datatype VFP
  = vabs of bool * (BitsN.nbit * BitsN.nbit)
  | vadd of bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))
  | vcmp of bool * (BitsN.nbit * (BitsN.nbit option))
  | vcvt_float of bool * (BitsN.nbit * BitsN.nbit)
  | vcvt_from_integer of bool * (bool * (BitsN.nbit * BitsN.nbit))
  | vcvt_to_integer of bool * (bool * (bool * (BitsN.nbit * BitsN.nbit)))
  | vdiv of bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))
  | vfma_vfms of bool * (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))
  | vfnma_vfnms of
      bool * (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))
  | vldm of
      bool * (bool * (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))))
  | vldr of bool * (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))
  | vmla_vmls of bool * (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))
  | vmov of bool * (BitsN.nbit * BitsN.nbit)
  | vmov_double of bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))
  | vmov_imm of bool * (BitsN.nbit * BitsN.nbit)
  | vmov_single of bool * (BitsN.nbit * BitsN.nbit)
  | vmov_two_singles of bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))
  | vmrs of BitsN.nbit
  | vmsr of BitsN.nbit
  | vmul of bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))
  | vneg of bool * (BitsN.nbit * BitsN.nbit)
  | vneg_mul of
      bool * (VFPNegMul * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))
  | vsqrt of bool * (BitsN.nbit * BitsN.nbit)
  | vstm of
      bool * (bool * (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))))
  | vstr of bool * (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))
  | vsub of bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))

datatype Hint
  = Breakpoint of BitsN.nbit
  | DataMemoryBarrier of BitsN.nbit
  | DataSynchronizationBarrier of BitsN.nbit
  | Debug of BitsN.nbit
  | InstructionSynchronizationBarrier of BitsN.nbit
  | PreloadData of bool * (bool * (BitsN.nbit * offset1))
  | PreloadDataLiteral of bool * BitsN.nbit
  | PreloadInstruction of bool * (BitsN.nbit * offset1)
  | SendEvent
  | WaitForEvent
  | WaitForInterrupt
  | Yield

datatype System
  = ChangeProcessorState of
      bool * (bool * (bool * (bool * (bool * (BitsN.nbit option)))))
  | EnterxLeavex of bool
  | ExceptionReturn
  | HypervisorCall of BitsN.nbit
  | MoveToBankedOrSpecialRegister of bool * (BitsN.nbit * BitsN.nbit)
  | MoveToRegisterFromBankedOrSpecial of bool * (BitsN.nbit * BitsN.nbit)
  | MoveToRegisterFromSpecial of bool * BitsN.nbit
  | MoveToSpecialFromImmediate of bool * (BitsN.nbit * BitsN.nbit)
  | MoveToSpecialFromRegister of bool * (BitsN.nbit * BitsN.nbit)
  | ReturnFromException of bool * (bool * (bool * BitsN.nbit))
  | SecureMonitorCall of BitsN.nbit
  | Setend of bool
  | StoreReturnState of bool * (bool * (bool * BitsN.nbit))
  | SupervisorCall of BitsN.nbit

datatype Store
  = StoreByte of
      bool * (bool * (bool * (BitsN.nbit * (BitsN.nbit * offset1))))
  | StoreByteUnprivileged of
      bool * (bool * (BitsN.nbit * (BitsN.nbit * offset1)))
  | StoreDual of
      bool *
      (bool *
       (bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * offset2)))))
  | StoreExclusive of
      BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))
  | StoreExclusiveByte of BitsN.nbit * (BitsN.nbit * BitsN.nbit)
  | StoreExclusiveDoubleword of
      BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))
  | StoreExclusiveHalf of BitsN.nbit * (BitsN.nbit * BitsN.nbit)
  | StoreHalf of
      bool * (bool * (bool * (BitsN.nbit * (BitsN.nbit * offset1))))
  | StoreHalfUnprivileged of
      bool * (bool * (BitsN.nbit * (BitsN.nbit * offset2)))
  | StoreMultiple of bool * (bool * (bool * (BitsN.nbit * BitsN.nbit)))
  | StoreMultipleUserRegisters of
      bool * (bool * (BitsN.nbit * BitsN.nbit))
  | StoreUnprivileged of
      bool * (bool * (BitsN.nbit * (BitsN.nbit * offset1)))
  | StoreWord of
      bool * (bool * (bool * (BitsN.nbit * (BitsN.nbit * offset1))))

datatype Load
  = LoadByte of
      bool *
      (bool * (bool * (bool * (BitsN.nbit * (BitsN.nbit * offset1)))))
  | LoadByteLiteral of bool * (bool * (BitsN.nbit * BitsN.nbit))
  | LoadByteUnprivileged of
      bool * (bool * (BitsN.nbit * (BitsN.nbit * offset1)))
  | LoadDual of
      bool *
      (bool *
       (bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * offset2)))))
  | LoadDualLiteral of bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))
  | LoadExclusive of BitsN.nbit * (BitsN.nbit * BitsN.nbit)
  | LoadExclusiveByte of BitsN.nbit * BitsN.nbit
  | LoadExclusiveDoubleword of BitsN.nbit * (BitsN.nbit * BitsN.nbit)
  | LoadExclusiveHalf of BitsN.nbit * BitsN.nbit
  | LoadHalf of
      bool *
      (bool * (bool * (bool * (BitsN.nbit * (BitsN.nbit * offset1)))))
  | LoadHalfLiteral of bool * (bool * (BitsN.nbit * BitsN.nbit))
  | LoadHalfUnprivileged of
      bool * (bool * (bool * (BitsN.nbit * (BitsN.nbit * offset2))))
  | LoadLiteral of bool * (BitsN.nbit * BitsN.nbit)
  | LoadMultiple of bool * (bool * (bool * (BitsN.nbit * BitsN.nbit)))
  | LoadMultipleExceptionReturn of
      bool * (bool * (bool * (BitsN.nbit * BitsN.nbit)))
  | LoadMultipleUserRegisters of bool * (bool * (BitsN.nbit * BitsN.nbit))
  | LoadSignedByteUnprivileged of
      bool * (bool * (BitsN.nbit * (BitsN.nbit * offset2)))
  | LoadUnprivileged of
      bool * (bool * (BitsN.nbit * (BitsN.nbit * offset1)))
  | LoadWord of
      bool * (bool * (bool * (BitsN.nbit * (BitsN.nbit * offset1))))

datatype Media
  = BitFieldClearOrInsert of
      BitsN.nbit * (BitsN.nbit * (Nat.nat * Nat.nat))
  | BitFieldExtract of
      bool * (BitsN.nbit * (BitsN.nbit * (Nat.nat * Nat.nat)))
  | ByteReverse of BitsN.nbit * BitsN.nbit
  | ByteReversePackedHalfword of BitsN.nbit * BitsN.nbit
  | ByteReverseSignedHalfword of BitsN.nbit * BitsN.nbit
  | ExtendByte of
      bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * Nat.nat)))
  | ExtendByte16 of
      bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * Nat.nat)))
  | ExtendHalfword of
      bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * Nat.nat)))
  | PackHalfword of
      SRType *
      (Nat.nat * (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))))
  | ReverseBits of BitsN.nbit * BitsN.nbit
  | Saturate of
      SRType * (Nat.nat * (Nat.nat * (bool * (BitsN.nbit * BitsN.nbit))))
  | Saturate16 of Nat.nat * (bool * (BitsN.nbit * BitsN.nbit))
  | SaturatingAddSubtract of
      BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))
  | SelectBytes of BitsN.nbit * (BitsN.nbit * BitsN.nbit)

datatype SIMD
  = SignedAddSub16 of
      BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))
  | SignedAddSub8 of bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))
  | SignedHalvingAddSub16 of
      BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))
  | SignedHalvingAddSub8 of
      bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))
  | SignedSaturatingAddSub16 of
      BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))
  | SignedSaturatingAddSub8 of
      bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))
  | UnsignedAddSub16 of
      BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))
  | UnsignedAddSub8 of bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))
  | UnsignedHalvingAddSub16 of
      BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))
  | UnsignedHalvingAddSub8 of
      bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))
  | UnsignedSaturatingAddSub16 of
      BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))
  | UnsignedSaturatingAddSub8 of
      bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))
  | UnsignedSumAbsoluteDifferences of
      BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))

datatype Multiply
  = Multiply32 of bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))
  | MultiplyAccumulate of
      bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))
  | MultiplyAccumulateAccumulate of
      BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))
  | MultiplyLong of
      bool *
      (bool *
       (bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))))
  | MultiplySubtract of
      BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))
  | Signed16Multiply32Accumulate of
      bool *
      (bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))))
  | Signed16Multiply32Result of
      bool * (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))
  | Signed16Multiply64Accumulate of
      bool *
      (bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))))
  | Signed16x32Multiply32Accumulate of
      bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))
  | Signed16x32Multiply32Result of
      bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))
  | SignedMostSignificantMultiply of
      bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))
  | SignedMostSignificantMultiplySubtract of
      bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))
  | SignedMultiplyDual of
      bool *
      (bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))))
  | SignedMultiplyLongDual of
      bool *
      (bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))))

datatype Data
  = AddSub of bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))
  | ArithLogicImmediate of
      BitsN.nbit * (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))
  | CountLeadingZeroes of BitsN.nbit * BitsN.nbit
  | Move of bool * (bool * (BitsN.nbit * BitsN.nbit))
  | MoveHalfword of bool * (BitsN.nbit * BitsN.nbit)
  | Register of
      BitsN.nbit *
      (bool *
       (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (SRType * Nat.nat)))))
  | RegisterShiftedRegister of
      BitsN.nbit *
      (bool *
       (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (SRType * BitsN.nbit)))))
  | ShiftImmediate of
      bool * (bool * (BitsN.nbit * (BitsN.nbit * (SRType * Nat.nat))))
  | ShiftRegister of
      bool * (bool * (BitsN.nbit * (BitsN.nbit * (SRType * BitsN.nbit))))
  | TestCompareImmediate of BitsN.nbit * (BitsN.nbit * BitsN.nbit)
  | TestCompareRegister of
      BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (SRType * Nat.nat)))

datatype Branch
  = BranchExchange of BitsN.nbit
  | BranchLinkExchangeImmediate of InstrSet * BitsN.nbit
  | BranchLinkExchangeRegister of BitsN.nbit
  | BranchTarget of BitsN.nbit
  | CheckArray of BitsN.nbit * BitsN.nbit
  | CompareBranch of bool * (BitsN.nbit * BitsN.nbit)
  | HandlerBranchLink of bool * BitsN.nbit
  | HandlerBranchLinkParameter of BitsN.nbit * BitsN.nbit
  | HandlerBranchParameter of BitsN.nbit * BitsN.nbit
  | TableBranchByte of bool * (BitsN.nbit * BitsN.nbit)

datatype instruction
  = Branch of Branch
  | ClearExclusive
  | Data of Data
  | Divide of bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))
  | Hint of Hint
  | IfThen of BitsN.nbit * BitsN.nbit
  | Load of Load
  | Media of Media
  | Multiply of Multiply
  | NoOperation
  | SIMD of SIMD
  | Store of Store
  | Swap of bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))
  | System of System
  | Undefined of BitsN.nbit
  | VFP of VFP

datatype MachineCode
  = ARM of BitsN.nbit
  | BadCode of string
  | Thumb of BitsN.nbit
  | Thumb2 of BitsN.nbit * BitsN.nbit
  | ThumbEE of BitsN.nbit

datatype enc = Enc_ARM | Enc_Thumb | Enc_Narrow | Enc_Wide

datatype maybe_instruction
  = FAIL of string
  | OK of (BitsN.nbit * string) * instruction
  | PENDING of string * ((BitsN.nbit * string) * instruction)
  | WORD of BitsN.nbit

datatype nat_or_reg = NAT of Nat.nat | REGISTER of BitsN.nbit

(* -------------------------------------------------------------------------
   Exceptions
   ------------------------------------------------------------------------- *)

exception ASSERT of string

exception AlignmentFault of BitsN.nbit

exception IMPLEMENTATION_DEFINED of string

exception UNPREDICTABLE of string

exception VFP_EXCEPTION of string

(* -------------------------------------------------------------------------
   Functions
   ------------------------------------------------------------------------- *)

structure Cast:
sig

val natToArchitecture: Nat.nat -> Architecture
val ArchitectureToNat: Architecture -> Nat.nat
val stringToArchitecture: string -> Architecture
val ArchitectureToString: Architecture -> string
val natToExtensions: Nat.nat -> Extensions
val ExtensionsToNat: Extensions -> Nat.nat
val stringToExtensions: string -> Extensions
val ExtensionsToString: Extensions -> string
val natToInstrSet: Nat.nat -> InstrSet
val InstrSetToNat: InstrSet -> Nat.nat
val stringToInstrSet: string -> InstrSet
val InstrSetToString: InstrSet -> string
val natToEncoding: Nat.nat -> Encoding
val EncodingToNat: Encoding -> Nat.nat
val stringToEncoding: string -> Encoding
val EncodingToString: Encoding -> string
val natToRName: Nat.nat -> RName
val RNameToNat: RName -> Nat.nat
val stringToRName: string -> RName
val RNameToString: RName -> string
val natToSRType: Nat.nat -> SRType
val SRTypeToNat: SRType -> Nat.nat
val stringToSRType: string -> SRType
val SRTypeToString: SRType -> string
val natToVFPExtension: Nat.nat -> VFPExtension
val VFPExtensionToNat: VFPExtension -> Nat.nat
val stringToVFPExtension: string -> VFPExtension
val VFPExtensionToString: VFPExtension -> string
val natToVFPNegMul: Nat.nat -> VFPNegMul
val VFPNegMulToNat: VFPNegMul -> Nat.nat
val stringToVFPNegMul: string -> VFPNegMul
val VFPNegMulToString: VFPNegMul -> string
val natToenc: Nat.nat -> enc
val encToNat: enc -> Nat.nat
val stringToenc: string -> enc
val encToString: enc -> string

end

val Architecture: Architecture ref
val CP14: CP14 ref
val CP15: CP15 ref
val CPSR: PSR ref
val CurrentCondition: BitsN.nbit ref
val ELR_hyp: BitsN.nbit ref
val Encoding: Encoding ref
val Extensions: (Extensions list) ref
val FP: FP ref
val MEM: (BitsN.nbit Map.map) ref
val REG: (BitsN.nbit Map.map) ref
val SPSR_abt: PSR ref
val SPSR_fiq: PSR ref
val SPSR_hyp: PSR ref
val SPSR_irq: PSR ref
val SPSR_mon: PSR ref
val SPSR_svc: PSR ref
val SPSR_und: PSR ref
val VFPExtension: VFPExtension ref
val undefined: bool ref
val PSR_A_rupd: PSR * bool -> PSR
val PSR_C_rupd: PSR * bool -> PSR
val PSR_E_rupd: PSR * bool -> PSR
val PSR_F_rupd: PSR * bool -> PSR
val PSR_GE_rupd: PSR * BitsN.nbit -> PSR
val PSR_I_rupd: PSR * bool -> PSR
val PSR_IT_rupd: PSR * BitsN.nbit -> PSR
val PSR_J_rupd: PSR * bool -> PSR
val PSR_M_rupd: PSR * BitsN.nbit -> PSR
val PSR_N_rupd: PSR * bool -> PSR
val PSR_Q_rupd: PSR * bool -> PSR
val PSR_T_rupd: PSR * bool -> PSR
val PSR_V_rupd: PSR * bool -> PSR
val PSR_Z_rupd: PSR * bool -> PSR
val PSR_psr'rst_rupd: PSR * BitsN.nbit -> PSR
val CP14_TEEHBR_rupd: CP14 * BitsN.nbit -> CP14
val SCTLR_A_rupd: SCTLR * bool -> SCTLR
val SCTLR_B_rupd: SCTLR * bool -> SCTLR
val SCTLR_BR_rupd: SCTLR * bool -> SCTLR
val SCTLR_C_rupd: SCTLR * bool -> SCTLR
val SCTLR_DZ_rupd: SCTLR * bool -> SCTLR
val SCTLR_EE_rupd: SCTLR * bool -> SCTLR
val SCTLR_FI_rupd: SCTLR * bool -> SCTLR
val SCTLR_I_rupd: SCTLR * bool -> SCTLR
val SCTLR_IE_rupd: SCTLR * bool -> SCTLR
val SCTLR_M_rupd: SCTLR * bool -> SCTLR
val SCTLR_NMFI_rupd: SCTLR * bool -> SCTLR
val SCTLR_RR_rupd: SCTLR * bool -> SCTLR
val SCTLR_SW_rupd: SCTLR * bool -> SCTLR
val SCTLR_TE_rupd: SCTLR * bool -> SCTLR
val SCTLR_U_rupd: SCTLR * bool -> SCTLR
val SCTLR_V_rupd: SCTLR * bool -> SCTLR
val SCTLR_VE_rupd: SCTLR * bool -> SCTLR
val SCTLR_Z_rupd: SCTLR * bool -> SCTLR
val SCTLR_sctlr'rst_rupd: SCTLR * BitsN.nbit -> SCTLR
val HSCTLR_A_rupd: HSCTLR * bool -> HSCTLR
val HSCTLR_C_rupd: HSCTLR * bool -> HSCTLR
val HSCTLR_CP15BEN_rupd: HSCTLR * bool -> HSCTLR
val HSCTLR_EE_rupd: HSCTLR * bool -> HSCTLR
val HSCTLR_FI_rupd: HSCTLR * bool -> HSCTLR
val HSCTLR_I_rupd: HSCTLR * bool -> HSCTLR
val HSCTLR_M_rupd: HSCTLR * bool -> HSCTLR
val HSCTLR_TE_rupd: HSCTLR * bool -> HSCTLR
val HSCTLR_WXN_rupd: HSCTLR * bool -> HSCTLR
val HSCTLR_hsctlr'rst_rupd: HSCTLR * BitsN.nbit -> HSCTLR
val HSR_EC_rupd: HSR * BitsN.nbit -> HSR
val HSR_IL_rupd: HSR * bool -> HSR
val HSR_ISS_rupd: HSR * BitsN.nbit -> HSR
val SCR_AW_rupd: SCR * bool -> SCR
val SCR_EA_rupd: SCR * bool -> SCR
val SCR_FIQ_rupd: SCR * bool -> SCR
val SCR_FW_rupd: SCR * bool -> SCR
val SCR_HCE_rupd: SCR * bool -> SCR
val SCR_IRQ_rupd: SCR * bool -> SCR
val SCR_NS_rupd: SCR * bool -> SCR
val SCR_SCD_rupd: SCR * bool -> SCR
val SCR_SIF_rupd: SCR * bool -> SCR
val SCR_nET_rupd: SCR * bool -> SCR
val SCR_scr'rst_rupd: SCR * BitsN.nbit -> SCR
val NSACR_NSASEDIS_rupd: NSACR * bool -> NSACR
val NSACR_NSD32DIS_rupd: NSACR * bool -> NSACR
val NSACR_NSTRCDIS_rupd: NSACR * bool -> NSACR
val NSACR_RFR_rupd: NSACR * bool -> NSACR
val NSACR_cp_rupd: NSACR * BitsN.nbit -> NSACR
val NSACR_nsacr'rst_rupd: NSACR * BitsN.nbit -> NSACR
val HCR_AMO_rupd: HCR * bool -> HCR
val HCR_BSU_rupd: HCR * BitsN.nbit -> HCR
val HCR_DC_rupd: HCR * bool -> HCR
val HCR_FB_rupd: HCR * bool -> HCR
val HCR_FMO_rupd: HCR * bool -> HCR
val HCR_IMO_rupd: HCR * bool -> HCR
val HCR_PTW_rupd: HCR * bool -> HCR
val HCR_SWIO_rupd: HCR * bool -> HCR
val HCR_TAC_rupd: HCR * bool -> HCR
val HCR_TGE_rupd: HCR * bool -> HCR
val HCR_TID_rupd: HCR * BitsN.nbit -> HCR
val HCR_TIDCP_rupd: HCR * bool -> HCR
val HCR_TPC_rupd: HCR * bool -> HCR
val HCR_TPU_rupd: HCR * bool -> HCR
val HCR_TSC_rupd: HCR * bool -> HCR
val HCR_TSW_rupd: HCR * bool -> HCR
val HCR_TTLB_rupd: HCR * bool -> HCR
val HCR_TVM_rupd: HCR * bool -> HCR
val HCR_TWE_rupd: HCR * bool -> HCR
val HCR_TWI_rupd: HCR * bool -> HCR
val HCR_VA_rupd: HCR * bool -> HCR
val HCR_VF_rupd: HCR * bool -> HCR
val HCR_VI_rupd: HCR * bool -> HCR
val HCR_VM_rupd: HCR * bool -> HCR
val HCR_hcr'rst_rupd: HCR * BitsN.nbit -> HCR
val CP15_HCR_rupd: CP15 * HCR -> CP15
val CP15_HSCTLR_rupd: CP15 * HSCTLR -> CP15
val CP15_HSR_rupd: CP15 * HSR -> CP15
val CP15_MVBAR_rupd: CP15 * BitsN.nbit -> CP15
val CP15_NSACR_rupd: CP15 * NSACR -> CP15
val CP15_SCR_rupd: CP15 * SCR -> CP15
val CP15_SCTLR_rupd: CP15 * SCTLR -> CP15
val CP15_VBAR_rupd: CP15 * BitsN.nbit -> CP15
val FPSCR_AHP_rupd: FPSCR * bool -> FPSCR
val FPSCR_C_rupd: FPSCR * bool -> FPSCR
val FPSCR_DN_rupd: FPSCR * bool -> FPSCR
val FPSCR_DZC_rupd: FPSCR * bool -> FPSCR
val FPSCR_DZE_rupd: FPSCR * bool -> FPSCR
val FPSCR_FZ_rupd: FPSCR * bool -> FPSCR
val FPSCR_IDC_rupd: FPSCR * bool -> FPSCR
val FPSCR_IDE_rupd: FPSCR * bool -> FPSCR
val FPSCR_IOC_rupd: FPSCR * bool -> FPSCR
val FPSCR_IOE_rupd: FPSCR * bool -> FPSCR
val FPSCR_IXC_rupd: FPSCR * bool -> FPSCR
val FPSCR_IXE_rupd: FPSCR * bool -> FPSCR
val FPSCR_N_rupd: FPSCR * bool -> FPSCR
val FPSCR_OFC_rupd: FPSCR * bool -> FPSCR
val FPSCR_OFE_rupd: FPSCR * bool -> FPSCR
val FPSCR_QC_rupd: FPSCR * bool -> FPSCR
val FPSCR_RMode_rupd: FPSCR * BitsN.nbit -> FPSCR
val FPSCR_UFC_rupd: FPSCR * bool -> FPSCR
val FPSCR_UFE_rupd: FPSCR * bool -> FPSCR
val FPSCR_V_rupd: FPSCR * bool -> FPSCR
val FPSCR_Z_rupd: FPSCR * bool -> FPSCR
val FPSCR_fpscr'rst_rupd: FPSCR * BitsN.nbit -> FPSCR
val FP_FPSCR_rupd: FP * FPSCR -> FP
val FP_REG_rupd: FP * (BitsN.nbit Map.map) -> FP
val boolify'5: BitsN.nbit -> bool * (bool * (bool * (bool * bool)))
val boolify'16:
  BitsN.nbit ->
  bool *
  (bool *
   (bool *
    (bool *
     (bool *
      (bool *
       (bool *
        (bool *
         (bool *
          (bool * (bool * (bool * (bool * (bool * (bool * bool))))))))))))))
val boolify'4: BitsN.nbit -> bool * (bool * (bool * bool))
val boolify'28:
  BitsN.nbit ->
  bool *
  (bool *
   (bool *
    (bool *
     (bool *
      (bool *
       (bool *
        (bool *
         (bool *
          (bool *
           (bool *
            (bool *
             (bool *
              (bool *
               (bool *
                (bool *
                 (bool *
                  (bool *
                   (bool *
                    (bool *
                     (bool *
                      (bool *
                       (bool * (bool * (bool * (bool * (bool * bool))))))))))))))))))))))))))
val boolify'3: BitsN.nbit -> bool * (bool * bool)
val boolify'8:
  BitsN.nbit ->
  bool * (bool * (bool * (bool * (bool * (bool * (bool * bool))))))
val ArchVersion: unit -> Nat.nat
val HaveDSPSupport: unit -> bool
val HaveThumb2: unit -> bool
val HaveThumbEE: unit -> bool
val HaveMPExt: unit -> bool
val HaveSecurityExt: unit -> bool
val HaveVirtExt: unit -> bool
val rec'PSR: BitsN.nbit -> PSR
val reg'PSR: PSR -> BitsN.nbit
val write'rec'PSR: (BitsN.nbit * PSR) -> BitsN.nbit
val write'reg'PSR: (PSR * BitsN.nbit) -> PSR
val rec'SCTLR: BitsN.nbit -> SCTLR
val reg'SCTLR: SCTLR -> BitsN.nbit
val write'rec'SCTLR: (BitsN.nbit * SCTLR) -> BitsN.nbit
val write'reg'SCTLR: (SCTLR * BitsN.nbit) -> SCTLR
val rec'HSCTLR: BitsN.nbit -> HSCTLR
val reg'HSCTLR: HSCTLR -> BitsN.nbit
val write'rec'HSCTLR: (BitsN.nbit * HSCTLR) -> BitsN.nbit
val write'reg'HSCTLR: (HSCTLR * BitsN.nbit) -> HSCTLR
val rec'HSR: BitsN.nbit -> HSR
val reg'HSR: HSR -> BitsN.nbit
val write'rec'HSR: (BitsN.nbit * HSR) -> BitsN.nbit
val write'reg'HSR: (HSR * BitsN.nbit) -> HSR
val rec'SCR: BitsN.nbit -> SCR
val reg'SCR: SCR -> BitsN.nbit
val write'rec'SCR: (BitsN.nbit * SCR) -> BitsN.nbit
val write'reg'SCR: (SCR * BitsN.nbit) -> SCR
val rec'NSACR: BitsN.nbit -> NSACR
val reg'NSACR: NSACR -> BitsN.nbit
val write'rec'NSACR: (BitsN.nbit * NSACR) -> BitsN.nbit
val write'reg'NSACR: (NSACR * BitsN.nbit) -> NSACR
val rec'HCR: BitsN.nbit -> HCR
val reg'HCR: HCR -> BitsN.nbit
val write'rec'HCR: (BitsN.nbit * HCR) -> BitsN.nbit
val write'reg'HCR: (HCR * BitsN.nbit) -> HCR
val ProcessorID: unit -> IntInf.int
val IsExternalAbort: unit -> bool
val IsSecure: unit -> bool
val UnalignedSupport: unit -> bool
val BadMode: BitsN.nbit -> bool
val CurrentModeIsNotUser: unit -> bool
val CurrentModeIsUserOrSystem: unit -> bool
val CurrentModeIsHyp: unit -> bool
val IntegerZeroDivideTrappingEnabled: unit -> bool
val ISETSTATE: unit -> BitsN.nbit
val write'ISETSTATE: BitsN.nbit -> unit
val CurrentInstrSet: unit -> InstrSet
val SelectInstrSet: InstrSet -> unit
val ITSTATE: unit -> BitsN.nbit
val write'ITSTATE: BitsN.nbit -> unit
val ITAdvance: unit -> unit
val InITBlock: unit -> bool
val LastInITBlock: unit -> bool
val ThumbCondition: unit -> BitsN.nbit
val BigEndian: unit -> bool
val SetExclusiveMonitors: (BitsN.nbit * Nat.nat) -> unit
val ExclusiveMonitorsPass: (BitsN.nbit * Nat.nat) -> bool
val ClearExclusiveLocal: IntInf.int -> unit
val CurrentCond: unit -> BitsN.nbit
val ConditionPassed: unit -> bool
val SPSR: unit -> PSR
val write'SPSR: PSR -> unit
val CPSRWriteByInstr: (BitsN.nbit * (BitsN.nbit * bool)) -> unit
val SPSRWriteByInstr: (BitsN.nbit * BitsN.nbit) -> unit
val RBankSelect:
  (BitsN.nbit *
   (RName *
    (RName * (RName * (RName * (RName * (RName * (RName * RName)))))))) ->
  RName
val RfiqBankSelect: (BitsN.nbit * (RName * RName)) -> RName
val LookUpRName: (BitsN.nbit * BitsN.nbit) -> RName
val Rmode: (BitsN.nbit * BitsN.nbit) -> BitsN.nbit
val write'Rmode: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit
val R: BitsN.nbit -> BitsN.nbit
val write'R: (BitsN.nbit * BitsN.nbit) -> unit
val SP: unit -> BitsN.nbit
val write'SP: BitsN.nbit -> unit
val LR: unit -> BitsN.nbit
val write'LR: BitsN.nbit -> unit
val PC: unit -> BitsN.nbit
val BranchTo: BitsN.nbit -> unit
val PCStoreValue: unit -> BitsN.nbit
val BranchWritePC: BitsN.nbit -> unit
val BXWritePC: BitsN.nbit -> unit
val LoadWritePC: BitsN.nbit -> unit
val ALUWritePC: BitsN.nbit -> unit
val ThisInstrLength: unit -> Nat.nat
val IncPC: unit -> unit
val mem1: BitsN.nbit -> (bool list)
val mem: (BitsN.nbit * Nat.nat) -> (bool list)
val write'mem: ((bool list) * (BitsN.nbit * Nat.nat)) -> unit
val BigEndianReverse: ((bool list) * Nat.nat) -> (bool list)
val Align: Nat.nat -> (BitsN.nbit * Nat.nat) -> BitsN.nbit
val Aligned: Nat.nat -> (BitsN.nbit * Nat.nat) -> bool
val MemA_with_priv: Nat.nat ->
  (BitsN.nbit * (Nat.nat * bool)) -> BitsN.nbit
val write'MemA_with_priv: Nat.nat ->
  (BitsN.nbit * (BitsN.nbit * (Nat.nat * bool))) -> unit
val MemA_unpriv: Nat.nat -> (BitsN.nbit * Nat.nat) -> BitsN.nbit
val write'MemA_unpriv: Nat.nat ->
  (BitsN.nbit * (BitsN.nbit * Nat.nat)) -> unit
val MemA: Nat.nat -> (BitsN.nbit * Nat.nat) -> BitsN.nbit
val write'MemA: Nat.nat -> (BitsN.nbit * (BitsN.nbit * Nat.nat)) -> unit
val MemU_with_priv: Nat.nat ->
  (BitsN.nbit * (Nat.nat * bool)) -> BitsN.nbit
val write'MemU_with_priv: Nat.nat ->
  (BitsN.nbit * (BitsN.nbit * (Nat.nat * bool))) -> unit
val MemU_unpriv: Nat.nat -> (BitsN.nbit * Nat.nat) -> BitsN.nbit
val write'MemU_unpriv: Nat.nat ->
  (BitsN.nbit * (BitsN.nbit * Nat.nat)) -> unit
val MemU: Nat.nat -> (BitsN.nbit * Nat.nat) -> BitsN.nbit
val write'MemU: Nat.nat -> (BitsN.nbit * (BitsN.nbit * Nat.nat)) -> unit
val NullCheckIfThumbEE: BitsN.nbit -> bool
val HighestSetBit: Nat.nat -> BitsN.nbit -> IntInf.int
val CountLeadingZeroBits: Nat.nat -> BitsN.nbit -> Nat.nat
val LowestSetBit: Nat.nat -> BitsN.nbit -> Nat.nat
val BitCount: Nat.nat -> BitsN.nbit -> Nat.nat
val SignExtendFrom: Nat.nat -> (BitsN.nbit * Nat.nat) -> BitsN.nbit
val Extend: Nat.nat * Nat.nat -> (bool * BitsN.nbit) -> BitsN.nbit
val UInt: Nat.nat -> BitsN.nbit -> IntInf.int
val SignedSatQ: Nat.nat -> (IntInf.int * Nat.nat) -> (BitsN.nbit * bool)
val UnsignedSatQ: Nat.nat -> (IntInf.int * Nat.nat) -> (BitsN.nbit * bool)
val SatQ: Nat.nat ->
  (IntInf.int * (Nat.nat * bool)) -> (BitsN.nbit * bool)
val SignedSat: Nat.nat -> (IntInf.int * Nat.nat) -> BitsN.nbit
val UnsignedSat: Nat.nat -> (IntInf.int * Nat.nat) -> BitsN.nbit
val LSL_C: Nat.nat -> (BitsN.nbit * Nat.nat) -> (BitsN.nbit * bool)
val LSL: Nat.nat -> (BitsN.nbit * Nat.nat) -> BitsN.nbit
val LSR_C: Nat.nat -> (BitsN.nbit * Nat.nat) -> (BitsN.nbit * bool)
val LSR: Nat.nat -> (BitsN.nbit * Nat.nat) -> BitsN.nbit
val ASR_C: Nat.nat -> (BitsN.nbit * Nat.nat) -> (BitsN.nbit * bool)
val ASR: Nat.nat -> (BitsN.nbit * Nat.nat) -> BitsN.nbit
val ROR_C: Nat.nat -> (BitsN.nbit * Nat.nat) -> (BitsN.nbit * bool)
val ROR: Nat.nat -> (BitsN.nbit * Nat.nat) -> BitsN.nbit
val RRX_C: Nat.nat -> (BitsN.nbit * bool) -> (BitsN.nbit * bool)
val RRX: Nat.nat -> (BitsN.nbit * bool) -> BitsN.nbit
val DecodeImmShift: (BitsN.nbit * BitsN.nbit) -> (SRType * Nat.nat)
val DecodeRegShift: BitsN.nbit -> SRType
val Shift_C: Nat.nat ->
  (BitsN.nbit * (SRType * (Nat.nat * bool))) -> (BitsN.nbit * bool)
val Shift: Nat.nat ->
  (BitsN.nbit * (SRType * (Nat.nat * bool))) -> BitsN.nbit
val ARMExpandImm_C: (BitsN.nbit * bool) -> (BitsN.nbit * bool)
val ARMExpandImm: BitsN.nbit -> BitsN.nbit
val ThumbExpandImm_C: (BitsN.nbit * bool) -> (BitsN.nbit * bool)
val ExpandImm_C: (BitsN.nbit * bool) -> (BitsN.nbit * bool)
val AddWithCarry: Nat.nat ->
  (BitsN.nbit * (BitsN.nbit * bool)) -> (BitsN.nbit * (bool * bool))
val DataProcessingALU:
  (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * bool))) ->
  (BitsN.nbit * (bool * bool))
val ArithmeticOpcode: BitsN.nbit -> bool
val ExcVectorBase: unit -> BitsN.nbit
val EnterMonitorMode: (PSR * (BitsN.nbit * BitsN.nbit)) -> unit
val EnterHypMode: (PSR * (BitsN.nbit * BitsN.nbit)) -> unit
val TakeReset: unit -> unit
val TakeUndefInstrException: unit -> unit
val TakeSVCException: unit -> unit
val TakeSMCException: unit -> unit
val TakeHVCException: unit -> unit
val TakeDataAbortException: unit -> unit
val TakePrefetchAbortException: unit -> unit
val TakePhysicalIRQException: unit -> unit
val TakeVirtualIRQException: unit -> unit
val TakePhysicalFIQException: unit -> unit
val TakeVirtualFIQException: unit -> unit
val TakeHypTrapException: unit -> unit
val WriteHSR: (BitsN.nbit * BitsN.nbit) -> unit
val CallSupervisor: BitsN.nbit -> unit
val CallHypervisor: BitsN.nbit -> unit
val BankedRegisterAccessValid: (BitsN.nbit * BitsN.nbit) -> unit
val SPSRAccessValid: (BitsN.nbit * BitsN.nbit) -> unit
val dfn'BranchTarget: BitsN.nbit -> unit
val dfn'BranchExchange: BitsN.nbit -> unit
val dfn'BranchLinkExchangeImmediate: (InstrSet * BitsN.nbit) -> unit
val dfn'BranchLinkExchangeRegister: BitsN.nbit -> unit
val dfn'CompareBranch: (bool * (BitsN.nbit * BitsN.nbit)) -> unit
val dfn'TableBranchByte: (bool * (BitsN.nbit * BitsN.nbit)) -> unit
val dfn'CheckArray: (BitsN.nbit * BitsN.nbit) -> unit
val dfn'HandlerBranchLink: (bool * BitsN.nbit) -> unit
val dfn'HandlerBranchLinkParameter: (BitsN.nbit * BitsN.nbit) -> unit
val dfn'HandlerBranchParameter: (BitsN.nbit * BitsN.nbit) -> unit
val dfn'EnterxLeavex: bool -> unit
val dfn'IfThen: (BitsN.nbit * BitsN.nbit) -> unit
val dfn'CountLeadingZeroes: (BitsN.nbit * BitsN.nbit) -> unit
val dfn'MoveHalfword: (bool * (BitsN.nbit * BitsN.nbit)) -> unit
val DataProcessing:
  (BitsN.nbit * (bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * bool))))) ->
  unit
val DataProcessingPC:
  (BitsN.nbit * (bool * (BitsN.nbit * BitsN.nbit))) -> unit
val dfn'Move: (bool * (bool * (BitsN.nbit * BitsN.nbit))) -> unit
val dfn'TestCompareImmediate:
  (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit
val dfn'ArithLogicImmediate:
  (BitsN.nbit * (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))) -> unit
val doRegister:
  (BitsN.nbit *
   (bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (SRType * Nat.nat)))))) ->
  unit
val dfn'Register:
  (BitsN.nbit *
   (bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (SRType * Nat.nat)))))) ->
  unit
val dfn'TestCompareRegister:
  (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (SRType * Nat.nat)))) -> unit
val dfn'ShiftImmediate:
  (bool * (bool * (BitsN.nbit * (BitsN.nbit * (SRType * Nat.nat))))) ->
  unit
val doRegisterShiftedRegister:
  (BitsN.nbit *
   (bool *
    (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (SRType * BitsN.nbit)))))) ->
  unit
val dfn'RegisterShiftedRegister:
  (BitsN.nbit *
   (bool *
    (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (SRType * BitsN.nbit)))))) ->
  unit
val dfn'ShiftRegister:
  (bool * (bool * (BitsN.nbit * (BitsN.nbit * (SRType * BitsN.nbit))))) ->
  unit
val dfn'AddSub: (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> unit
val dfn'SaturatingAddSubtract:
  (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> unit
val dfn'Multiply32:
  (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> unit
val dfn'MultiplyAccumulate:
  (bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))) -> unit
val dfn'MultiplyLong:
  (bool *
   (bool *
    (bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))))) ->
  unit
val dfn'MultiplyAccumulateAccumulate:
  (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> unit
val dfn'MultiplySubtract:
  (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> unit
val dfn'Signed16Multiply32Accumulate:
  (bool * (bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))))) ->
  unit
val dfn'Signed16Multiply32Result:
  (bool * (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))) -> unit
val dfn'Signed16x32Multiply32Accumulate:
  (bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))) -> unit
val dfn'Signed16x32Multiply32Result:
  (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> unit
val dfn'Signed16Multiply64Accumulate:
  (bool * (bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))))) ->
  unit
val dfn'SignedMultiplyDual:
  (bool * (bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))))) ->
  unit
val dfn'SignedMultiplyLongDual:
  (bool * (bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))))) ->
  unit
val dfn'SignedMostSignificantMultiply:
  (bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))) -> unit
val dfn'SignedMostSignificantMultiplySubtract:
  (bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))) -> unit
val SignedParallelAddSub16:
  (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> (IntInf.int * IntInf.int)
val dfn'SignedAddSub16:
  (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> unit
val dfn'SignedSaturatingAddSub16:
  (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> unit
val dfn'SignedHalvingAddSub16:
  (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> unit
val SignedParallelAddSub8:
  (bool * (BitsN.nbit * BitsN.nbit)) ->
  (IntInf.int * (IntInf.int * (IntInf.int * IntInf.int)))
val dfn'SignedAddSub8:
  (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> unit
val dfn'SignedSaturatingAddSub8:
  (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> unit
val dfn'SignedHalvingAddSub8:
  (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> unit
val UnsignedParallelAddSub16:
  (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> (IntInf.int * IntInf.int)
val dfn'UnsignedAddSub16:
  (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> unit
val dfn'UnsignedSaturatingAddSub16:
  (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> unit
val dfn'UnsignedHalvingAddSub16:
  (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> unit
val UnsignedParallelAddSub8:
  (bool * (BitsN.nbit * BitsN.nbit)) ->
  (IntInf.int * (IntInf.int * (IntInf.int * IntInf.int)))
val dfn'UnsignedAddSub8:
  (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> unit
val dfn'UnsignedSaturatingAddSub8:
  (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> unit
val dfn'UnsignedHalvingAddSub8:
  (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> unit
val dfn'UnsignedSumAbsoluteDifferences:
  (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> unit
val GenerateIntegerZeroDivide: unit -> unit
val dfn'Divide: (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> unit
val dfn'PackHalfword:
  (SRType * (Nat.nat * (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))))) ->
  unit
val dfn'Saturate:
  (SRType * (Nat.nat * (Nat.nat * (bool * (BitsN.nbit * BitsN.nbit))))) ->
  unit
val dfn'Saturate16: (Nat.nat * (bool * (BitsN.nbit * BitsN.nbit))) -> unit
val dfn'ExtendByte:
  (bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * Nat.nat)))) -> unit
val dfn'ExtendByte16:
  (bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * Nat.nat)))) -> unit
val dfn'ExtendHalfword:
  (bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * Nat.nat)))) -> unit
val dfn'SelectBytes: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit
val dfn'ByteReverse: (BitsN.nbit * BitsN.nbit) -> unit
val dfn'ByteReversePackedHalfword: (BitsN.nbit * BitsN.nbit) -> unit
val dfn'ByteReverseSignedHalfword: (BitsN.nbit * BitsN.nbit) -> unit
val dfn'ReverseBits: (BitsN.nbit * BitsN.nbit) -> unit
val dfn'BitFieldExtract:
  (bool * (BitsN.nbit * (BitsN.nbit * (Nat.nat * Nat.nat)))) -> unit
val dfn'BitFieldClearOrInsert:
  (BitsN.nbit * (BitsN.nbit * (Nat.nat * Nat.nat))) -> unit
val dfn'LoadWord:
  (bool * (bool * (bool * (BitsN.nbit * (BitsN.nbit * offset1))))) -> unit
val dfn'LoadLiteral: (bool * (BitsN.nbit * BitsN.nbit)) -> unit
val dfn'LoadUnprivileged:
  (bool * (bool * (BitsN.nbit * (BitsN.nbit * offset1)))) -> unit
val dfn'LoadByte:
  (bool * (bool * (bool * (bool * (BitsN.nbit * (BitsN.nbit * offset1)))))) ->
  unit
val dfn'LoadByteLiteral:
  (bool * (bool * (BitsN.nbit * BitsN.nbit))) -> unit
val dfn'LoadByteUnprivileged:
  (bool * (bool * (BitsN.nbit * (BitsN.nbit * offset1)))) -> unit
val dfn'LoadSignedByteUnprivileged:
  (bool * (bool * (BitsN.nbit * (BitsN.nbit * offset2)))) -> unit
val dfn'LoadHalf:
  (bool * (bool * (bool * (bool * (BitsN.nbit * (BitsN.nbit * offset1)))))) ->
  unit
val dfn'LoadHalfLiteral:
  (bool * (bool * (BitsN.nbit * BitsN.nbit))) -> unit
val dfn'LoadHalfUnprivileged:
  (bool * (bool * (bool * (BitsN.nbit * (BitsN.nbit * offset2))))) -> unit
val dfn'LoadMultiple:
  (bool * (bool * (bool * (BitsN.nbit * BitsN.nbit)))) -> unit
val dfn'LoadMultipleExceptionReturn:
  (bool * (bool * (bool * (BitsN.nbit * BitsN.nbit)))) -> unit
val dfn'LoadMultipleUserRegisters:
  (bool * (bool * (BitsN.nbit * BitsN.nbit))) -> unit
val dfn'LoadDual:
  (bool *
   (bool * (bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * offset2)))))) ->
  unit
val dfn'LoadDualLiteral:
  (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> unit
val dfn'LoadExclusive: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit
val dfn'LoadExclusiveByte: (BitsN.nbit * BitsN.nbit) -> unit
val dfn'LoadExclusiveHalf: (BitsN.nbit * BitsN.nbit) -> unit
val dfn'LoadExclusiveDoubleword:
  (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit
val dfn'StoreWord:
  (bool * (bool * (bool * (BitsN.nbit * (BitsN.nbit * offset1))))) -> unit
val dfn'StoreUnprivileged:
  (bool * (bool * (BitsN.nbit * (BitsN.nbit * offset1)))) -> unit
val dfn'StoreByte:
  (bool * (bool * (bool * (BitsN.nbit * (BitsN.nbit * offset1))))) -> unit
val dfn'StoreByteUnprivileged:
  (bool * (bool * (BitsN.nbit * (BitsN.nbit * offset1)))) -> unit
val dfn'StoreHalf:
  (bool * (bool * (bool * (BitsN.nbit * (BitsN.nbit * offset1))))) -> unit
val dfn'StoreHalfUnprivileged:
  (bool * (bool * (BitsN.nbit * (BitsN.nbit * offset2)))) -> unit
val dfn'StoreMultiple:
  (bool * (bool * (bool * (BitsN.nbit * BitsN.nbit)))) -> unit
val dfn'StoreMultipleUserRegisters:
  (bool * (bool * (BitsN.nbit * BitsN.nbit))) -> unit
val dfn'StoreDual:
  (bool *
   (bool * (bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * offset2)))))) ->
  unit
val dfn'StoreExclusive:
  (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> unit
val dfn'StoreExclusiveByte:
  (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit
val dfn'StoreExclusiveHalf:
  (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> unit
val dfn'StoreExclusiveDoubleword:
  (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> unit
val dfn'ClearExclusive: unit -> unit
val dfn'Swap: (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> unit
val dfn'ChangeProcessorState:
  (bool * (bool * (bool * (bool * (bool * (BitsN.nbit option)))))) -> unit
val dfn'ExceptionReturn: unit -> unit
val dfn'HypervisorCall: BitsN.nbit -> unit
val dfn'MoveToRegisterFromSpecial: (bool * BitsN.nbit) -> unit
val dfn'MoveToRegisterFromBankedOrSpecial:
  (bool * (BitsN.nbit * BitsN.nbit)) -> unit
val dfn'MoveToSpecialFromImmediate:
  (bool * (BitsN.nbit * BitsN.nbit)) -> unit
val dfn'MoveToSpecialFromRegister:
  (bool * (BitsN.nbit * BitsN.nbit)) -> unit
val dfn'MoveToBankedOrSpecialRegister:
  (bool * (BitsN.nbit * BitsN.nbit)) -> unit
val dfn'ReturnFromException: (bool * (bool * (bool * BitsN.nbit))) -> unit
val dfn'SecureMonitorCall: BitsN.nbit -> unit
val dfn'SupervisorCall: BitsN.nbit -> unit
val dfn'StoreReturnState: (bool * (bool * (bool * BitsN.nbit))) -> unit
val dfn'Setend: bool -> unit
val dfn'Undefined: BitsN.nbit -> unit
val dfn'NoOperation: unit -> unit
val dfn'Breakpoint: BitsN.nbit -> unit
val dfn'Debug: BitsN.nbit -> unit
val dfn'DataMemoryBarrier: BitsN.nbit -> unit
val dfn'DataSynchronizationBarrier: BitsN.nbit -> unit
val dfn'InstructionSynchronizationBarrier: BitsN.nbit -> unit
val dfn'PreloadData: (bool * (bool * (BitsN.nbit * offset1))) -> unit
val dfn'PreloadDataLiteral: (bool * BitsN.nbit) -> unit
val dfn'PreloadInstruction: (bool * (BitsN.nbit * offset1)) -> unit
val dfn'SendEvent: unit -> unit
val dfn'WaitForEvent: unit -> unit
val dfn'WaitForInterrupt: unit -> unit
val dfn'Yield: unit -> unit
val rec'FPSCR: BitsN.nbit -> FPSCR
val reg'FPSCR: FPSCR -> BitsN.nbit
val write'rec'FPSCR: (BitsN.nbit * FPSCR) -> BitsN.nbit
val write'reg'FPSCR: (FPSCR * BitsN.nbit) -> FPSCR
val RoundingMode: unit -> IEEEReal.rounding_mode
val FPAdd32: (BitsN.nbit * BitsN.nbit) -> BitsN.nbit
val FPSub32: (BitsN.nbit * BitsN.nbit) -> BitsN.nbit
val FPMul32: (BitsN.nbit * BitsN.nbit) -> BitsN.nbit
val FPAdd64: (BitsN.nbit * BitsN.nbit) -> BitsN.nbit
val FPSub64: (BitsN.nbit * BitsN.nbit) -> BitsN.nbit
val FPMul64: (BitsN.nbit * BitsN.nbit) -> BitsN.nbit
val FPToFixed32: (BitsN.nbit * (bool * bool)) -> BitsN.nbit
val FPToFixed64: (BitsN.nbit * (bool * bool)) -> BitsN.nbit
val FixedToFP32: (BitsN.nbit * (bool * bool)) -> BitsN.nbit
val FixedToFP64: (BitsN.nbit * (bool * bool)) -> BitsN.nbit
val D: BitsN.nbit -> BitsN.nbit
val write'D: (BitsN.nbit * BitsN.nbit) -> unit
val S: BitsN.nbit -> BitsN.nbit
val write'S: (BitsN.nbit * BitsN.nbit) -> unit
val VFPExpandImm: (BitsN.nbit * bool) -> BitsN.nbit
val FPCompare32: (BitsN.nbit * BitsN.nbit) -> BitsN.nbit
val FPCompare64: (BitsN.nbit * BitsN.nbit) -> BitsN.nbit
val FPZero32: BitsN.nbit -> BitsN.nbit
val FPZero64: BitsN.nbit -> BitsN.nbit
val dfn'vmov_imm: (bool * (BitsN.nbit * BitsN.nbit)) -> unit
val dfn'vmov: (bool * (BitsN.nbit * BitsN.nbit)) -> unit
val dfn'vmov_single: (bool * (BitsN.nbit * BitsN.nbit)) -> unit
val dfn'vmov_two_singles:
  (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> unit
val dfn'vmov_double:
  (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> unit
val dfn'vabs: (bool * (BitsN.nbit * BitsN.nbit)) -> unit
val dfn'vneg: (bool * (BitsN.nbit * BitsN.nbit)) -> unit
val dfn'vsqrt: (bool * (BitsN.nbit * BitsN.nbit)) -> unit
val dfn'vcvt_float: (bool * (BitsN.nbit * BitsN.nbit)) -> unit
val dfn'vcvt_to_integer:
  (bool * (bool * (bool * (BitsN.nbit * BitsN.nbit)))) -> unit
val dfn'vcvt_from_integer:
  (bool * (bool * (BitsN.nbit * BitsN.nbit))) -> unit
val dfn'vcmp: (bool * (BitsN.nbit * (BitsN.nbit option))) -> unit
val dfn'vmsr: BitsN.nbit -> unit
val dfn'vmrs: BitsN.nbit -> unit
val dfn'vadd: (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> unit
val dfn'vsub: (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> unit
val dfn'vmul: (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> unit
val dfn'vdiv: (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> unit
val dfn'vmla_vmls:
  (bool * (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))) -> unit
val dfn'vfma_vfms:
  (bool * (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))) -> unit
val dfn'vfnma_vfnms:
  (bool * (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))) -> unit
val dfn'vneg_mul:
  (bool * (VFPNegMul * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))) -> unit
val dfn'vldr:
  (bool * (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))) -> unit
val dfn'vstr:
  (bool * (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit)))) -> unit
val dfn'vldm:
  (bool * (bool * (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))))) ->
  unit
val dfn'vstm:
  (bool * (bool * (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))))) ->
  unit
val Run: instruction -> unit
val Fetch: unit -> MachineCode
val Do: (BitsN.nbit * bool) -> bool
val Skip: unit -> instruction
val UndefinedARM: BitsN.nbit -> instruction
val UndefinedThumb: unit -> instruction
val DECODE_UNPREDICTABLE: (MachineCode * string) -> unit
val DecodeHint: (BitsN.nbit * BitsN.nbit) -> instruction
val DecodeParallelAdditionSubtraction:
  (BitsN.nbit *
   (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))))) ->
  instruction
val DecodeVFP: BitsN.nbit -> (bool * (string * instruction))
val DecodeARM: BitsN.nbit -> instruction
val DecodeThumb: BitsN.nbit -> instruction
val DecodeThumbEE: BitsN.nbit -> instruction
val DecodeThumb2: (BitsN.nbit * BitsN.nbit) -> instruction
val Decode: MachineCode -> instruction
val Next: unit -> unit
val EncodeThumbImmediate: BitsN.nbit -> (BitsN.nbit option)
val EncodeARMImmediate_aux:
  (BitsN.nbit * BitsN.nbit) -> (BitsN.nbit option)
val EncodeARMImmediate: BitsN.nbit -> (BitsN.nbit option)
val EncodeImmShift: (SRType * Nat.nat) -> (BitsN.nbit * BitsN.nbit)
val EncodeRegShift: SRType -> BitsN.nbit
val EncodeAddSubOpc: BitsN.nbit -> BitsN.nbit
val EncodeVFPImmediate: (BitsN.nbit * bool) -> (BitsN.nbit option)
val EncodeVFPReg: (BitsN.nbit * bool) -> (BitsN.nbit * BitsN.nbit)
val e_branch: (BitsN.nbit * (Branch * enc)) -> MachineCode
val e_vfp: (BitsN.nbit * (VFP * enc)) -> MachineCode
val e_data: (BitsN.nbit * (Data * enc)) -> MachineCode
val e_media: (BitsN.nbit * (Media * enc)) -> MachineCode
val e_hint: (BitsN.nbit * (Hint * enc)) -> MachineCode
val e_system: (BitsN.nbit * (System * enc)) -> MachineCode
val e_multiply: (BitsN.nbit * (Multiply * enc)) -> MachineCode
val e_simd: (BitsN.nbit * (SIMD * enc)) -> MachineCode
val e_load: (BitsN.nbit * (Load * enc)) -> MachineCode
val e_store: (BitsN.nbit * (Store * enc)) -> MachineCode
val instructionEncode: (BitsN.nbit * (instruction * enc)) -> MachineCode
val SetPassCondition: BitsN.nbit -> unit
val Encode: (BitsN.nbit * (instruction * enc)) -> MachineCode
val al: BitsN.nbit * string
val stripSpaces: string -> string
val p_number: string -> (Nat.nat option)
val p_signed_number: (bool * string) -> ((bool * Nat.nat) option)
val p_encode_immediate: Nat.nat -> string -> ((bool * BitsN.nbit) option)
val p_encode_signed_immediate: Nat.nat ->
  (bool * string) -> ((bool * (bool * BitsN.nbit)) option)
val p_encode_signed_immediate_offset: Nat.nat ->
  (bool * string) -> ((bool * (bool * BitsN.nbit)) option)
val p_encode_signed_offset: Nat.nat ->
  (bool * string) -> ((bool * BitsN.nbit) option)
val p_unbounded_immediate: string -> (Nat.nat option)
val p_immediate: Nat.nat -> string -> ((bool * BitsN.nbit) option)
val p_immediate_number: Nat.nat -> string -> ((bool * BitsN.nbit) option)
val p_signed_immediate: Nat.nat ->
  string -> ((bool * (bool * BitsN.nbit)) option)
val p_signed_offset: Nat.nat ->
  string -> ((bool * (bool * BitsN.nbit)) option)
val p_offset: Nat.nat -> string -> ((bool * BitsN.nbit) option)
val p_arm_immediate: string -> ((string * BitsN.nbit) option)
val p_arm_fp_immediate: (bool * string) -> ((string * BitsN.nbit) option)
val p_range_imm: (Nat.nat * (Nat.nat * string)) -> (string * Nat.nat)
val p_label: string -> (string option)
val p_cond: string -> (BitsN.nbit option)
val p_suffix: string -> ((BitsN.nbit * string) option)
val p_suffix2: string -> ((BitsN.nbit * (string * string)) option)
val p_register: string -> (BitsN.nbit option)
val p_register1: (string list) -> (BitsN.nbit option)
val p_register2: (string list) -> ((BitsN.nbit * BitsN.nbit) option)
val p_register3:
  (string list) -> ((BitsN.nbit * (BitsN.nbit * BitsN.nbit)) option)
val p_register4:
  (string list) ->
  ((BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) option)
val p_reg_offset: (bool * string) -> ((bool * BitsN.nbit) option)
val p_register_offset: string -> ((bool * BitsN.nbit) option)
val p_fp_register: (bool * string) -> (BitsN.nbit option)
val p_any_fp_register: (string * string) -> ((bool * BitsN.nbit) option)
val p_fp_register3:
  (bool * (string list)) ->
  ((BitsN.nbit * (BitsN.nbit * BitsN.nbit)) option)
val closingRegList: string -> ((bool * string) option)
val p_reg_list: (BitsN.nbit * string) -> (BitsN.nbit option)
val p_registers_loop:
  (BitsN.nbit * (string list)) -> ((bool * BitsN.nbit) option)
val p_registers: (string list) -> ((bool * BitsN.nbit) option)
val p_fp_reg_list: (bool * (BitsN.nbit * string)) -> (BitsN.nbit option)
val p_fp_registers_loop:
  (bool * (BitsN.nbit * (string list))) -> (BitsN.nbit option)
val fp_reg_list:
  (bool * BitsN.nbit) -> ((bool * (BitsN.nbit * BitsN.nbit)) option)
val p_fp_registers:
  (string list) -> ((bool * (BitsN.nbit * BitsN.nbit)) option)
val p_shift_amount:
  (SRType * (char * string)) -> (string * (SRType * nat_or_reg))
val p_shift_imm_or_reg: string -> (string * (SRType * nat_or_reg))
val p_rotation: string -> (string * Nat.nat)
val p_arith_logic_full:
  (string * (BitsN.nbit * (bool * (string list)))) -> maybe_instruction
val p_arith_logic:
  (string * (BitsN.nbit * (bool * (string list)))) -> maybe_instruction
val p_test_compare:
  (string * (BitsN.nbit * (string list))) -> maybe_instruction
val p_mov_mvn:
  (string * (bool * (bool * (string list)))) -> maybe_instruction
val p_shift_full:
  (string * (SRType * (bool * (string list)))) -> maybe_instruction
val p_shift:
  (string * (SRType * (bool * (string list)))) -> maybe_instruction
val p_rrx: (string * (bool * (string list))) -> maybe_instruction
val p_adr: (string * (string list)) -> maybe_instruction
val p_bx: (string * (string list)) -> maybe_instruction
val p_bl: (string * (string list)) -> maybe_instruction
val p_b: (string * (string list)) -> maybe_instruction
val p_blx: (string * (string list)) -> maybe_instruction
val p_clz: (string * (string list)) -> maybe_instruction
val p_movt_movw: (string * (bool * (string list))) -> maybe_instruction
val p_addw_subw: (string * (bool * (string list))) -> maybe_instruction
val p_mul: (string * (bool * (string list))) -> maybe_instruction
val p_mla: (string * (bool * (string list))) -> maybe_instruction
val p_umull_etc:
  (string * (bool * (bool * (bool * (string list))))) -> maybe_instruction
val p_umaal: (string * (string list)) -> maybe_instruction
val p_mls: (string * (string list)) -> maybe_instruction
val p_smla:
  (string * (bool * (bool * (string list)))) -> maybe_instruction
val p_smul:
  (string * (bool * (bool * (string list)))) -> maybe_instruction
val p_smlaw: (string * (bool * (string list))) -> maybe_instruction
val p_smulw: (string * (bool * (string list))) -> maybe_instruction
val p_smlal:
  (string * (bool * (bool * (string list)))) -> maybe_instruction
val p_smuad_smusd:
  (string * (bool * (bool * (string list)))) -> maybe_instruction
val p_smlad_smlsd:
  (string * (bool * (bool * (string list)))) -> maybe_instruction
val p_smlald_smlsld:
  (string * (bool * (bool * (string list)))) -> maybe_instruction
val p_smmul: (string * (bool * (string list))) -> maybe_instruction
val p_smmla: (string * (bool * (string list))) -> maybe_instruction
val p_smmls: (string * (bool * (string list))) -> maybe_instruction
val p_qadd_etc:
  (string * (BitsN.nbit * (string list))) -> maybe_instruction
val p_sadd16_etc:
  (string * (BitsN.nbit * (string list))) -> maybe_instruction
val p_qadd16_etc:
  (string * (BitsN.nbit * (string list))) -> maybe_instruction
val p_shadd16_etc:
  (string * (BitsN.nbit * (string list))) -> maybe_instruction
val p_sadd8_etc: (string * (bool * (string list))) -> maybe_instruction
val p_qadd8_etc: (string * (bool * (string list))) -> maybe_instruction
val p_shadd8_etc: (string * (bool * (string list))) -> maybe_instruction
val p_uadd16_etc:
  (string * (BitsN.nbit * (string list))) -> maybe_instruction
val p_uqadd16_etc:
  (string * (BitsN.nbit * (string list))) -> maybe_instruction
val p_uhadd16_etc:
  (string * (BitsN.nbit * (string list))) -> maybe_instruction
val p_uadd8_etc: (string * (bool * (string list))) -> maybe_instruction
val p_uqadd8_etc: (string * (bool * (string list))) -> maybe_instruction
val p_uhadd8_etc: (string * (bool * (string list))) -> maybe_instruction
val p_usad8: (string * (string list)) -> maybe_instruction
val p_usada8: (string * (string list)) -> maybe_instruction
val p_pkhbt_pkhtb: (string * (bool * (string list))) -> maybe_instruction
val p_sat: (string * (bool * (string list))) -> maybe_instruction
val p_sat16: (string * (bool * (string list))) -> maybe_instruction
val pick_sxtb:
  (Nat.nat * (bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * Nat.nat))))) ->
  instruction
val p_sxtb_etc:
  (string * (Nat.nat * (bool * (string list)))) -> maybe_instruction
val p_sxtab_etc:
  (string * (Nat.nat * (bool * (string list)))) -> maybe_instruction
val p_sel: (string * (string list)) -> maybe_instruction
val p_rev: (string * (string list)) -> maybe_instruction
val p_rev16: (string * (string list)) -> maybe_instruction
val p_revsh: (string * (string list)) -> maybe_instruction
val p_rbit: (string * (string list)) -> maybe_instruction
val p_sbfx_ubfx: (string * (bool * (string list))) -> maybe_instruction
val p_bfc: (string * (string list)) -> maybe_instruction
val p_bfi: (string * (string list)) -> maybe_instruction
val closingAddress: string -> ((bool * string) option)
val p_address_mode1:
  (string list) ->
  (string * ((bool * (bool * (bool * (BitsN.nbit * offset1)))) option))
val p_address_mode2:
  (string list) ->
  (string * ((bool * (bool * (bool * (BitsN.nbit * offset2)))) option))
val p_address_mode3:
  (string list) -> (string * ((BitsN.nbit * (BitsN.nbit option)) option))
val pick_ldr_str:
  (Nat.nat *
   (bool * (bool * (bool * (BitsN.nbit * (BitsN.nbit * offset1)))))) ->
  instruction
val p_ldr_str: (string * (Nat.nat * (string list))) -> maybe_instruction
val pick_ldrb_ldrh:
  (bool *
   (bool *
    (bool * (bool * (bool * (BitsN.nbit * (BitsN.nbit * offset1))))))) ->
  instruction
val p_ldrb_ldrh:
  (string * (bool * (bool * (string list)))) -> maybe_instruction
val pick_ldrd_strd:
  (bool *
   (bool *
    (bool * (bool * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * offset2))))))) ->
  instruction
val p_ldrd_strd: (string * (bool * (string list))) -> maybe_instruction
val p_ldrt_strt1:
  (string * (Nat.nat * (string list))) -> maybe_instruction
val p_ldrt_strt2:
  (string * (Nat.nat * (string list))) -> maybe_instruction
val p_pld: (string * (bool * (string list))) -> maybe_instruction
val p_pli: (string * (string list)) -> maybe_instruction
val p_ldrex: (string * (string list)) -> maybe_instruction
val p_ldrexb_ldrexh:
  (string * (bool * (string list))) -> maybe_instruction
val p_ldrexd: (string * (string list)) -> maybe_instruction
val p_strex: (string * (string list)) -> maybe_instruction
val p_strexb_strexh:
  (string * (bool * (string list))) -> maybe_instruction
val p_strexd: (string * (string list)) -> maybe_instruction
val p_swp: (string * (bool * (string list))) -> maybe_instruction
val p_pop_push: (string * (bool * (string list))) -> maybe_instruction
val p_vpop_vpush: (string * (bool * (string list))) -> maybe_instruction
val p_ldm_stm:
  (string * (bool * (bool * (bool * (string list))))) -> maybe_instruction
val p_vldm_vstm:
  (string * (bool * (bool * (string list)))) -> maybe_instruction
val p_setend: (string list) -> maybe_instruction
val p_aif:
  (bool * (bool * (bool * string))) -> ((bool * (bool * bool)) option)
val p_cps: (bool * (bool * (string list))) -> maybe_instruction
val p_mode: string -> (BitsN.nbit option)
val banked_register: (BitsN.nbit * string) -> (BitsN.nbit option)
val p_banked_register: string -> (BitsN.nbit option)
val p_mrs: (string * (string list)) -> maybe_instruction
val p_cxsf: (BitsN.nbit * string) -> (BitsN.nbit option)
val p_spec_reg: string -> ((bool * BitsN.nbit) option)
val p_msr: (string * (string list)) -> maybe_instruction
val p_rfe: (string * (bool * (bool * (string list)))) -> maybe_instruction
val p_srs: (string * (bool * (bool * (string list)))) -> maybe_instruction
val p_call: (string * (Nat.nat * (string list))) -> maybe_instruction
val p_barrier_option: (string list) -> (BitsN.nbit option)
val p_dmb_dsb: (string * (bool * (string list))) -> maybe_instruction
val p_isb: (string * (string list)) -> maybe_instruction
val p_vcmpe: (string * (string list)) -> maybe_instruction
val p_vmrs_register: string -> (BitsN.nbit option)
val p_vmrs: (string * (string list)) -> maybe_instruction
val p_vmsr: (string * (string list)) -> maybe_instruction
val p_vcvt: (string * (bool * (string list))) -> maybe_instruction
val p_fp2: (string * (Nat.nat * (string list))) -> maybe_instruction
val p_fp3: (string * (Nat.nat * (string list))) -> maybe_instruction
val p_vldr_vstr: (string * (bool * (string list))) -> maybe_instruction
val p_noarg: (string * instruction) -> maybe_instruction
val p_tokens: string -> (string list)
val instructionFromString: string -> maybe_instruction
val s_cond: BitsN.nbit -> string
val s_reg: BitsN.nbit -> string
val s_reg2: (BitsN.nbit * BitsN.nbit) -> string
val s_reg3: (BitsN.nbit * (BitsN.nbit * BitsN.nbit)) -> string
val s_reg4:
  (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))) -> string
val s_vfp_reg: (bool * BitsN.nbit) -> string
val s_any_reg: ((bool option) * Nat.nat) -> string
val contiguous:
  (((Nat.nat * Nat.nat) list) * (Nat.nat * (bool list))) ->
  ((Nat.nat * Nat.nat) list)
val s_registers_from_contiguous:
  ((bool option) * (string * ((Nat.nat * Nat.nat) list))) -> string
val s_registers: Nat.nat -> ((bool option) * BitsN.nbit) -> string
val s_arm_registers: Nat.nat -> BitsN.nbit -> string
val s_fp_registers: Nat.nat -> (bool * BitsN.nbit) -> string
val s_hex: Nat.nat -> BitsN.nbit -> string
val s_offset: BitsN.nbit -> string
val s_add_sub_offset: (bool * BitsN.nbit) -> string
val s_branch: (BitsN.nbit * Branch) -> (string * string)
val s_vfp_suffix: (BitsN.nbit * bool) -> string
val s_vfp: (BitsN.nbit * VFP) -> (string * string)
val s_test_compare: BitsN.nbit -> string
val s_arith_logic: BitsN.nbit -> string
val s_shift: SRType -> string
val s_shift_n: (SRType * Nat.nat) -> string
val s_shift_r: (bool * (BitsN.nbit * (SRType * Nat.nat))) -> string
val s_expand_imm: BitsN.nbit -> string
val s_data: (BitsN.nbit * Data) -> (string * string)
val s_multiply: (BitsN.nbit * Multiply) -> (string * string)
val s_imm_form:
  (bool * (bool * (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))))) ->
  string
val s_reg_form:
  (bool *
   (bool *
    (bool *
     (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (SRType * Nat.nat))))))) ->
  string
val s_stack: (bool * bool) -> string
val s_load: (BitsN.nbit * Load) -> (string * string)
val s_store: (BitsN.nbit * Store) -> (string * string)
val s_barrier_option: BitsN.nbit -> string
val s_hint: (BitsN.nbit * Hint) -> (string * string)
val s_add_sub16:
  (string *
   (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))))) ->
  (string * string)
val s_add_sub8:
  (string *
   (BitsN.nbit * (bool * (BitsN.nbit * (BitsN.nbit * BitsN.nbit))))) ->
  (string * string)
val s_simd: (BitsN.nbit * SIMD) -> (string * string)
val s_xt_rotation:
  (BitsN.nbit * (BitsN.nbit * (BitsN.nbit * Nat.nat))) -> string
val s_media: (BitsN.nbit * Media) -> (string * string)
val s_psr: (bool * BitsN.nbit) -> string
val s_special: (bool * BitsN.nbit) -> string
val s_system: (BitsN.nbit * System) -> (string * string)
val s_it_mask: (bool * BitsN.nbit) -> string
val instructionToString: (BitsN.nbit * instruction) -> (string * string)

end