Riscv_stack_zeroization (p.jasmin.2025.06.1.doc.jasmin.jasmin.Jasmin.Riscv_stack

val sz_init : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_extra.arch_toIdent ->
  Expr.var_i ->
  Wsize.wsize ->
  BinNums.coq_Z ->
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt,
    Riscv_instr_decl.riscv_op,
    Riscv_extra.riscv_extra_op)
    Arch_extra.extended_op
    Linear.lcmd

val store_zero : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_extra.arch_toIdent ->
  Wsize.wsize ->
  Expr.var_i ->
  BinNums.coq_Z ->
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt,
    Riscv_instr_decl.riscv_op,
    Riscv_extra.riscv_extra_op)
    Arch_extra.extended_op
    Linear.linstr_r

val sz_loop : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_extra.arch_toIdent ->
  Expr.var_i ->
  Label.label ->
  Wsize.wsize ->
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt,
    Riscv_instr_decl.riscv_op,
    Riscv_extra.riscv_extra_op)
    Arch_extra.extended_op
    Linear.lcmd

val restore_sp : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_extra.arch_toIdent ->
  Expr.var_i ->
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt,
    Riscv_instr_decl.riscv_op,
    Riscv_extra.riscv_extra_op)
    Arch_extra.extended_op
    Linear.linstr
    list

val stack_zero_loop : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_extra.arch_toIdent ->
  Expr.var_i ->
  Label.label ->
  Wsize.wsize ->
  Wsize.wsize ->
  BinNums.coq_Z ->
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt,
    Riscv_instr_decl.riscv_op,
    Riscv_extra.riscv_extra_op)
    Arch_extra.extended_op
    Linear.lcmd

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

val sz_unrolled : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_extra.arch_toIdent ->
  Expr.var_i ->
  Wsize.wsize ->
  BinNums.coq_Z ->
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt,
    Riscv_instr_decl.riscv_op,
    Riscv_extra.riscv_extra_op)
    Arch_extra.extended_op
    Linear.lcmd

val stack_zero_unrolled : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_extra.arch_toIdent ->
  Expr.var_i ->
  Wsize.wsize ->
  Wsize.wsize ->
  BinNums.coq_Z ->
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt,
    Riscv_instr_decl.riscv_op,
    Riscv_extra.riscv_extra_op)
    Arch_extra.extended_op
    Linear.lcmd

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

val stack_zeroization_cmd : 
  (Riscv_decl.register,
    Arch_utils.empty,
    Arch_utils.empty,
    Arch_utils.empty,
    Riscv_decl.condt)
    Arch_extra.arch_toIdent ->
  Stack_zero_strategy.stack_zero_strategy ->
  Ident.Ident.ident ->
  Label.label ->
  Wsize.wsize ->
  Wsize.wsize ->
  BinNums.coq_Z ->
  ((Riscv_decl.register,
     Arch_utils.empty,
     Arch_utils.empty,
     Arch_utils.empty,
     Riscv_decl.condt,
     Riscv_instr_decl.riscv_op,
     Riscv_extra.riscv_extra_op)
     Arch_extra.extended_op
     Linear.lcmd
   * Var0.SvExtra.Sv.t)
    Compiler_util.cexec