package jasmin
Compiler for High-Assurance and High-Speed Cryptography
Install
dune-project
Dependency
Authors
Maintainers
Sources
jasmin-compiler-v2026.09.0.tar.bz2
sha256=11fec571efb9f7b3a47fea324b4e2a68289e0b73b2248d237eccf139b5218190
doc/jasmin.jasmin/Jasmin/Armv8a_stack_zeroization/index.html
Module Jasmin.Armv8a_stack_zeroization
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 listval 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 listval 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 listval 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 listval 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 listval 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 listval 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.lcmdval 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_rval 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.lcmdval 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 listval 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.lcmdval 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.tval 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.lcmdval 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.lcmdval 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.tval 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