Armv8a_extra (p.jasmin.2026.09.0.doc.jasmin.jasmin.Jasmin.Armv8a

type __ = Obj.t

type armv8a_extra_op =

| Oarmv8a_swap of Wsize.wsize
| Oarmv8a_add_large_imm
| Oarmv8a_smart_li of Wsize.wsize

val armv8a_extra_op_rect : 
  (Wsize.wsize -> 'a1) ->
  'a1 ->
  (Wsize.wsize -> 'a1) ->
  armv8a_extra_op ->
  'a1

val armv8a_extra_op_rec : 
  (Wsize.wsize -> 'a1) ->
  'a1 ->
  (Wsize.wsize -> 'a1) ->
  armv8a_extra_op ->
  'a1

type is_armv8a_extra_op =

| Coq_is_Oarmv8a_swap of Wsize.wsize * Wsize.is_wsize
| Coq_is_Oarmv8a_add_large_imm
| Coq_is_Oarmv8a_smart_li of Wsize.wsize * Wsize.is_wsize

val is_armv8a_extra_op_rect : 
  (Wsize.wsize -> Wsize.is_wsize -> 'a1) ->
  'a1 ->
  (Wsize.wsize -> Wsize.is_wsize -> 'a1) ->
  armv8a_extra_op ->
  is_armv8a_extra_op ->
  'a1

val is_armv8a_extra_op_rec : 
  (Wsize.wsize -> Wsize.is_wsize -> 'a1) ->
  'a1 ->
  (Wsize.wsize -> Wsize.is_wsize -> 'a1) ->
  armv8a_extra_op ->
  is_armv8a_extra_op ->
  'a1

val armv8a_extra_op_tag : armv8a_extra_op -> BinNums.positive

val is_armv8a_extra_op_inhab : armv8a_extra_op -> is_armv8a_extra_op

val is_armv8a_extra_op_functor : 
  armv8a_extra_op ->
  is_armv8a_extra_op ->
  is_armv8a_extra_op

type box_armv8a_extra_op_Oarmv8a_swap = Wsize.wsize

val coq_Box_armv8a_extra_op_Oarmv8a_swap_0 : 
  box_armv8a_extra_op_Oarmv8a_swap ->
  Wsize.wsize

type box_armv8a_extra_op_Oarmv8a_add_large_imm =

| Box_armv8a_extra_op_Oarmv8a_add_large_imm

type armv8a_extra_op_fields_t = __

val armv8a_extra_op_fields : armv8a_extra_op -> armv8a_extra_op_fields_t

val armv8a_extra_op_construct : 
  BinNums.positive ->
  armv8a_extra_op_fields_t ->
  armv8a_extra_op option

val armv8a_extra_op_induction : 
  (Wsize.wsize -> Wsize.is_wsize -> 'a1) ->
  'a1 ->
  (Wsize.wsize -> Wsize.is_wsize -> 'a1) ->
  armv8a_extra_op ->
  is_armv8a_extra_op ->
  'a1

val armv8a_extra_op_eqb_fields : 
  (armv8a_extra_op -> armv8a_extra_op -> bool) ->
  BinNums.positive ->
  armv8a_extra_op_fields_t ->
  armv8a_extra_op_fields_t ->
  bool

val armv8a_extra_op_eqb : armv8a_extra_op -> armv8a_extra_op -> bool

val armv8a_extra_op_eqb_OK : 
  armv8a_extra_op ->
  armv8a_extra_op ->
  Datatypes.reflect

val armv8a_extra_op_eqb_OK_sumbool : armv8a_extra_op -> armv8a_extra_op -> bool

val coq_HB_unnamed_factory_1 : armv8a_extra_op Eqtype.Coq_hasDecEq.axioms_

val armv8a_extra_armv8a_extra_op__canonical__eqtype_Equality : 
  Eqtype.Equality.coq_type

val eqTC_armv8a_extra_op : armv8a_extra_op Utils0.eqTypeC

val coq_Oarmv8a_add_large_imm_instr : Sopn.instruction_desc

val smart_li_instr : Wsize.wsize -> Sopn.instruction_desc

val get_instr_desc : armv8a_extra_op -> Sopn.instruction_desc

val armv8a_extra_op_decl : armv8a_extra_op Sopn.asmOp

module E : sig ... end

val asm_args_of_opn_args : 
  Armv8a_params_core.ARMv8AFopn_core.opn_args list ->
  (((Armv8a_decl.register,
      Arch_utils.empty,
      Arch_utils.empty,
      Arm_common.rflag,
      Arm_common.condt,
      Armv8a_instr_decl.armv8a_asm_op)
      Arch_decl.asm_op_msb_t
    * Fexpr.lexpr list)
   * Fexpr.rexpr list)
    list

val uncons_LLvar : 
  Expr.instr_info ->
  Fexpr.lexpr list ->
  (Expr.var_i * Fexpr.lexpr list) Compiler_util.cexec

val uncons_wconst : 
  Expr.instr_info ->
  Fexpr.rexpr list ->
  (BinNums.coq_Z * Fexpr.rexpr list) Compiler_util.cexec

val smart_li_args : 
  Expr.instr_info ->
  Eqtype.Equality.sort ->
  Fexpr.lexpr list ->
  Fexpr.rexpr list ->
  (Compiler_util.pp_error_loc, (Expr.var_i * BinNums.coq_Z) * Fexpr.rexpr list)
    Utils0.result

val assemble_smart_li : 
  Expr.instr_info ->
  Wsize.wsize ->
  Fexpr.lexpr list ->
  Fexpr.rexpr list ->
  (Compiler_util.pp_error_loc,
    (((Armv8a_decl.register,
        Arch_utils.empty,
        Arch_utils.empty,
        Arm_common.rflag,
        Arm_common.condt,
        Armv8a_instr_decl.armv8a_asm_op)
        Arch_decl.asm_op_msb_t
      * Fexpr.lexpr list)
     * Fexpr.rexpr list)
      list)
    Utils0.result

val assemble_extra : 
  Expr.instr_info ->
  armv8a_extra_op ->
  Fexpr.lexpr list ->
  Fexpr.rexpr list ->
  (((Armv8a_decl.register,
      Arch_utils.empty,
      Arch_utils.empty,
      Arm_common.rflag,
      Arm_common.condt,
      Armv8a_instr_decl.armv8a_asm_op)
      Arch_decl.asm_op_msb_t
    * Fexpr.lexpr list)
   * Fexpr.rexpr list)
    list
    Compiler_util.cexec

val armv8a_extra : 
  (Armv8a_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_common.rflag,
    Arm_common.condt)
    Arch_extra.arch_toIdent ->
  (Armv8a_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_common.rflag,
    Arm_common.condt,
    Armv8a_instr_decl.armv8a_asm_op,
    armv8a_extra_op)
    Arch_extra.asm_extra

type armv8a_extended_op =
  (Armv8a_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_common.rflag,
    Arm_common.condt,
    Armv8a_instr_decl.armv8a_asm_op,
    armv8a_extra_op)
    Arch_extra.extended_op

val coq_Oarmv8a : 
  (Armv8a_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_common.rflag,
    Arm_common.condt)
    Arch_extra.arch_toIdent ->
  (Armv8a_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_common.rflag,
    Arm_common.condt,
    Armv8a_instr_decl.armv8a_asm_op)
    Arch_decl.asm_op_t' ->
  armv8a_extended_op Sopn.sopn