Arm_stack_zeroization (p.jasmin.2025.06.2.doc.jasmin.jasmin.Jasmin.Arm_stack

val sz_init : 
  (Arm_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_decl.rflag,
    Arm_decl.condt)
    Arch_extra.arch_toIdent ->
  Expr.var_i ->
  Wsize.wsize ->
  BinNums.coq_Z ->
  (Arm_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_decl.rflag,
    Arm_decl.condt,
    Arm_instr_decl.arm_op,
    Arm_extra.arm_extra_op)
    Arch_extra.extended_op
    Linear.lcmd

val store_zero : 
  (Arm_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_decl.rflag,
    Arm_decl.condt)
    Arch_extra.arch_toIdent ->
  Expr.var_i ->
  Wsize.wsize ->
  Fexpr.fexpr ->
  (Arm_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_decl.rflag,
    Arm_decl.condt,
    Arm_instr_decl.arm_op,
    Arm_extra.arm_extra_op)
    Arch_extra.extended_op
    Linear.linstr_r

val sz_loop : 
  (Arm_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_decl.rflag,
    Arm_decl.condt)
    Arch_extra.arch_toIdent ->
  Expr.var_i ->
  Label.label ->
  Wsize.wsize ->
  (Arm_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_decl.rflag,
    Arm_decl.condt,
    Arm_instr_decl.arm_op,
    Arm_extra.arm_extra_op)
    Arch_extra.extended_op
    Linear.lcmd

val restore_sp : 
  (Arm_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_decl.rflag,
    Arm_decl.condt)
    Arch_extra.arch_toIdent ->
  Expr.var_i ->
  Arm_extra.arm_extended_op Linear.linstr list

val stack_zero_loop : 
  (Arm_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_decl.rflag,
    Arm_decl.condt)
    Arch_extra.arch_toIdent ->
  Expr.var_i ->
  Label.label ->
  Wsize.wsize ->
  Wsize.wsize ->
  BinNums.coq_Z ->
  (Arm_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_decl.rflag,
    Arm_decl.condt,
    Arm_instr_decl.arm_op,
    Arm_extra.arm_extra_op)
    Arch_extra.extended_op
    Linear.lcmd

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

val sz_unrolled : 
  (Arm_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_decl.rflag,
    Arm_decl.condt)
    Arch_extra.arch_toIdent ->
  Expr.var_i ->
  Wsize.wsize ->
  BinNums.coq_Z ->
  (Arm_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_decl.rflag,
    Arm_decl.condt,
    Arm_instr_decl.arm_op,
    Arm_extra.arm_extra_op)
    Arch_extra.extended_op
    Linear.lcmd

val stack_zero_unrolled : 
  (Arm_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_decl.rflag,
    Arm_decl.condt)
    Arch_extra.arch_toIdent ->
  Expr.var_i ->
  Wsize.wsize ->
  Wsize.wsize ->
  BinNums.coq_Z ->
  (Arm_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_decl.rflag,
    Arm_decl.condt,
    Arm_instr_decl.arm_op,
    Arm_extra.arm_extra_op)
    Arch_extra.extended_op
    Linear.lcmd

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

val stack_zeroization_cmd : 
  (Arm_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arm_decl.rflag,
    Arm_decl.condt)
    Arch_extra.arch_toIdent ->
  Stack_zero_strategy.stack_zero_strategy ->
  Ident.Ident.ident ->
  Label.label ->
  Wsize.wsize ->
  Wsize.wsize ->
  BinNums.coq_Z ->
  ((Arm_decl.register,
     Arch_utils.empty,
     Arch_utils.empty,
     Arm_decl.rflag,
     Arm_decl.condt,
     Arm_instr_decl.arm_op,
     Arm_extra.arm_extra_op)
     Arch_extra.extended_op
     Linear.lcmd
   * Var0.SvExtra.Sv.t)
    Compiler_util.cexec