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

val to_opn : 
  (Armv8a_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_common.rflag,
    Arm_common.condt)
    Arch_extra.arch_toIdent ->
  ((Fexpr.lexpr 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_t')
   * Fexpr.rexpr list) ->
  (Fexpr.lexpr list * Armv8a_extra.armv8a_extended_op Sopn.sopn)
  * Fexpr.rexpr list

val coq_ARMv8AFopn_mov : 
  (Armv8a_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_common.rflag,
    Arm_common.condt)
    Arch_extra.arch_toIdent ->
  Expr.var_i ->
  Expr.var_i ->
  (Fexpr.lexpr list * Armv8a_extra.armv8a_extended_op Sopn.sopn)
  * Fexpr.rexpr list

val coq_ARMv8AFopn_addi : 
  (Armv8a_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_common.rflag,
    Arm_common.condt)
    Arch_extra.arch_toIdent ->
  Expr.var_i ->
  Expr.var_i ->
  BinNums.coq_Z ->
  (Fexpr.lexpr list * Armv8a_extra.armv8a_extended_op Sopn.sopn)
  * Fexpr.rexpr list

val coq_ARMv8AFopn_subi : 
  (Armv8a_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_common.rflag,
    Arm_common.condt)
    Arch_extra.arch_toIdent ->
  Expr.var_i ->
  Expr.var_i ->
  BinNums.coq_Z ->
  (Fexpr.lexpr list * Armv8a_extra.armv8a_extended_op Sopn.sopn)
  * Fexpr.rexpr list

val coq_ARMv8AFopn_align : 
  (Armv8a_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_common.rflag,
    Arm_common.condt)
    Arch_extra.arch_toIdent ->
  Expr.var_i ->
  Expr.var_i ->
  Wsize.wsize ->
  (Fexpr.lexpr list * Armv8a_extra.armv8a_extended_op Sopn.sopn)
  * Fexpr.rexpr list

val coq_ARMv8AFopn_smart_addi : 
  (Armv8a_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_common.rflag,
    Arm_common.condt)
    Arch_extra.arch_toIdent ->
  Expr.var_i ->
  Expr.var_i ->
  BinNums.coq_Z ->
  ((Fexpr.lexpr list * Armv8a_extra.armv8a_extended_op Sopn.sopn)
   * Fexpr.rexpr list)
    list

val coq_ARMv8AFopn_smart_subi : 
  (Armv8a_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_common.rflag,
    Arm_common.condt)
    Arch_extra.arch_toIdent ->
  Expr.var_i ->
  Expr.var_i ->
  BinNums.coq_Z ->
  ((Fexpr.lexpr list * Armv8a_extra.armv8a_extended_op Sopn.sopn)
   * Fexpr.rexpr list)
    list

val coq_ARMv8AFopn_smart_addi_tmp : 
  (Armv8a_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_common.rflag,
    Arm_common.condt)
    Arch_extra.arch_toIdent ->
  Expr.var_i ->
  Expr.var_i ->
  BinNums.coq_Z ->
  ((Fexpr.lexpr list * Armv8a_extra.armv8a_extended_op Sopn.sopn)
   * Fexpr.rexpr list)
    list

val coq_ARMv8AFopn_smart_subi_tmp : 
  (Armv8a_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_common.rflag,
    Arm_common.condt)
    Arch_extra.arch_toIdent ->
  Expr.var_i ->
  Expr.var_i ->
  BinNums.coq_Z ->
  ((Fexpr.lexpr list * Armv8a_extra.armv8a_extended_op Sopn.sopn)
   * Fexpr.rexpr list)
    list

val armv8a_immediate : 
  (Armv8a_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_common.rflag,
    Arm_common.condt)
    Arch_extra.arch_toIdent ->
  Expr.var_i ->
  BinNums.coq_Z ->
  ((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_extra.armv8a_extra_op)
    Arch_extra.extended_op_gen
    Expr.instr_r

val armv8a_saparams : 
  (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.armv8a_extra_op)
    Arch_extra.extended_op
    Stack_alloc_params.stack_alloc_params

val armv8a_allocate_stack_frame : 
  (Armv8a_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_common.rflag,
    Arm_common.condt)
    Arch_extra.arch_toIdent ->
  Expr.var_i ->
  Expr.var_i option ->
  BinNums.coq_Z ->
  ((Fexpr.lexpr list * Armv8a_extra.armv8a_extended_op Sopn.sopn)
   * Fexpr.rexpr list)
    list

val armv8a_free_stack_frame : 
  (Armv8a_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_common.rflag,
    Arm_common.condt)
    Arch_extra.arch_toIdent ->
  Expr.var_i ->
  Expr.var_i option ->
  BinNums.coq_Z ->
  ((Fexpr.lexpr list * Armv8a_extra.armv8a_extended_op Sopn.sopn)
   * Fexpr.rexpr list)
    list

val armv8a_set_up_sp_register : 
  (Armv8a_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_common.rflag,
    Arm_common.condt)
    Arch_extra.arch_toIdent ->
  Expr.var_i ->
  BinNums.coq_Z ->
  Wsize.wsize ->
  Expr.var_i ->
  Expr.var_i ->
  ((Fexpr.lexpr list
    * (Armv8a_decl.register,
        Arch_utils.empty,
        Arch_utils.empty,
        Arm_common.rflag,
        Arm_common.condt,
        Armv8a_instr_decl.armv8a_asm_op,
        Armv8a_extra.armv8a_extra_op)
        Arch_extra.extended_op
        Sopn.sopn)
   * Fexpr.rexpr list)
    list

val armv8a_tmp : 
  (Armv8a_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_common.rflag,
    Arm_common.condt)
    Arch_extra.arch_toIdent ->
  Ident.Ident.ident

val armv8a_tmp2 : 
  (Armv8a_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_common.rflag,
    Arm_common.condt)
    Arch_extra.arch_toIdent ->
  Ident.Ident.ident

val armv8a_lmove : 
  (Armv8a_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_common.rflag,
    Arm_common.condt)
    Arch_extra.arch_toIdent ->
  Wsize.wsize ->
  Expr.var_i ->
  Expr.var_i ->
  (Fexpr.lexpr list * Armv8a_extra.armv8a_extended_op Sopn.sopn)
  * Fexpr.rexpr list

val armv8a_check_ws : Eqtype.Equality.sort -> bool

val armv8a_lstore : 
  (Armv8a_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_common.rflag,
    Arm_common.condt)
    Arch_extra.arch_toIdent ->
  Wsize.wsize ->
  Expr.var_i ->
  BinNums.coq_Z ->
  Expr.var_i ->
  (Fexpr.lexpr list * Armv8a_extra.armv8a_extended_op Sopn.sopn)
  * Fexpr.rexpr list

val armv8a_lload : 
  (Armv8a_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_common.rflag,
    Arm_common.condt)
    Arch_extra.arch_toIdent ->
  Wsize.wsize ->
  Expr.var_i ->
  Expr.var_i ->
  BinNums.coq_Z ->
  (Fexpr.lexpr list * Armv8a_extra.armv8a_extended_op Sopn.sopn)
  * Fexpr.rexpr list

val armv8a_lloads : 
  (Armv8a_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_common.rflag,
    Arm_common.condt)
    Arch_extra.arch_toIdent ->
  Expr.var_i ->
  (Var0.Var.var * BinNums.coq_Z) list ->
  BinNums.coq_Z ->
  ((Fexpr.lexpr list
    * (Armv8a_decl.register,
        Arch_utils.empty,
        Arch_utils.empty,
        Arm_common.rflag,
        Arm_common.condt,
        Armv8a_instr_decl.armv8a_asm_op,
        Armv8a_extra.armv8a_extra_op)
        Arch_extra.extended_op
        Sopn.sopn)
   * Fexpr.rexpr list)
    list

val armv8a_liparams : 
  (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.armv8a_extra_op)
    Arch_extra.extended_op
    Linearization.linearization_params

val armv8a_fvars_correct : 
  (Armv8a_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_common.rflag,
    Arm_common.condt)
    Arch_extra.arch_toIdent ->
  Lowering.fresh_vars ->
  Expr.progT ->
  (Armv8a_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_common.rflag,
    Arm_common.condt,
    Armv8a_instr_decl.armv8a_asm_op,
    Armv8a_extra.armv8a_extra_op)
    Arch_extra.extended_op
    Expr.fun_decl
    list ->
  bool

val armv8a_loparams : 
  (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.armv8a_extra_op)
    Arch_extra.extended_op
    Arch_params.lowering_params

val armv8a_shparams : 
  (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.armv8a_extra_op)
    Arch_extra.extended_op
    Slh_lowering.sh_params

val condt_of_rflag : Arm_common.rflag -> Arm_common.condt

val condt_not : Arm_common.condt -> Arm_common.condt

val condt_and : Arm_common.condt -> Arm_common.condt -> Arm_common.condt option

val condt_or : Arm_common.condt -> Arm_common.condt -> Arm_common.condt option

val is_rflags_GE : Arm_common.rflag -> Arm_common.rflag -> bool

val assemble_cond : 
  (Armv8a_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_common.rflag,
    Arm_common.condt)
    Arch_extra.arch_toIdent ->
  Expr.instr_info ->
  Fexpr.fexpr ->
  Arm_common.condt Compiler_util.cexec

val is_valid_address : 
  (Armv8a_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_common.rflag,
    Arm_common.condt)
    Arch_decl.reg_address ->
  bool

val armv8a_agparams : 
  (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.armv8a_extra_op)
    Asm_gen.asm_gen_params

val armv8a_szparams : 
  (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.armv8a_extra_op)
    Arch_extra.extended_op
    Stack_zeroization.stack_zeroization_params

val armv8a_is_move_op : 
  (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.armv8a_extra_op)
    Arch_extra.extended_op
    Sopn.asm_op_t ->
  bool

val armv8a_params : 
  (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.armv8a_extra_op)
    Arch_params.architecture_params