Armv8a_stack_zeroization (p.jasmin.2026.09.0.doc.jasmin.jasmin.Jasmin.Armv8a_stack

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 fopn_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 fopn_sub : 
  (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 ->
  Expr.var_i ->
  (Fexpr.lexpr list * Armv8a_extra.armv8a_extended_op Sopn.sopn)
  * Fexpr.rexpr list

val fopn_movi : 
  (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 ->
  (Fexpr.lexpr list * Armv8a_extra.armv8a_extended_op Sopn.sopn)
  * Fexpr.rexpr list

val fopn_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 fopn_li : 
  (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 ->
  (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

val sz_init : 
  (Armv8a_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_common.rflag,
    Arm_common.condt)
    Arch_extra.arch_toIdent ->
  Expr.var_i ->
  Wsize.wsize ->
  BinNums.coq_Z ->
  (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
    Linear.lcmd

val store_zero : 
  (Armv8a_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_common.rflag,
    Arm_common.condt)
    Arch_extra.arch_toIdent ->
  Expr.var_i ->
  Wsize.wsize ->
  Fexpr.fexpr ->
  (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
    Linear.linstr_r

val sz_loop : 
  (Armv8a_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_common.rflag,
    Arm_common.condt)
    Arch_extra.arch_toIdent ->
  Expr.var_i ->
  Label.label ->
  Wsize.wsize ->
  (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
    Linear.lcmd

val restore_sp : 
  (Armv8a_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_common.rflag,
    Arm_common.condt)
    Arch_extra.arch_toIdent ->
  Expr.var_i ->
  Armv8a_extra.armv8a_extended_op Linear.linstr list

val stack_zero_loop : 
  (Armv8a_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_common.rflag,
    Arm_common.condt)
    Arch_extra.arch_toIdent ->
  Expr.var_i ->
  Label.label ->
  Wsize.wsize ->
  Wsize.wsize ->
  BinNums.coq_Z ->
  (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
    Linear.lcmd

val stack_zero_loop_vars : 
  (Armv8a_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_common.rflag,
    Arm_common.condt)
    Arch_extra.arch_toIdent ->
  Var0.SvExtra.Sv.t

val sz_unrolled : 
  (Armv8a_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_common.rflag,
    Arm_common.condt)
    Arch_extra.arch_toIdent ->
  Expr.var_i ->
  Wsize.wsize ->
  BinNums.coq_Z ->
  (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
    Linear.lcmd

val stack_zero_unrolled : 
  (Armv8a_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_common.rflag,
    Arm_common.condt)
    Arch_extra.arch_toIdent ->
  Expr.var_i ->
  Wsize.wsize ->
  Wsize.wsize ->
  BinNums.coq_Z ->
  (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
    Linear.lcmd

val stack_zero_unrolled_vars : 
  (Armv8a_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_common.rflag,
    Arm_common.condt)
    Arch_extra.arch_toIdent ->
  Var0.SvExtra.Sv.t

val stack_zeroization_cmd : 
  (Armv8a_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_common.rflag,
    Arm_common.condt)
    Arch_extra.arch_toIdent ->
  Stack_zero_strategy.stack_zero_strategy ->
  Ident.Ident.ident ->
  Label.label ->
  Wsize.wsize ->
  Wsize.wsize ->
  BinNums.coq_Z ->
  ((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
     Linear.lcmd
   * Var0.SvExtra.Sv.t)
    Compiler_util.cexec