package jasmin
Compiler for High-Assurance and High-Speed Cryptography
Install
dune-project
Dependency
Authors
Maintainers
Sources
jasmin-compiler-v2025.06.1.tar.bz2
sha256=e92b42fa69da7c730b0c26dacf842a72b4febcaf4f2157a1dc18b3cce1f859fa
doc/jasmin.jasmin/Jasmin/Riscv_extra/index.html
Module Jasmin.Riscv_extra
type __ = Obj.tval riscv_extra_op_rect : (Wsize.wsize -> 'a1) -> 'a1 -> riscv_extra_op -> 'a1val riscv_extra_op_rec : (Wsize.wsize -> 'a1) -> 'a1 -> riscv_extra_op -> 'a1val is_riscv_extra_op_rect :
(Wsize.wsize -> Wsize.is_wsize -> 'a1) ->
'a1 ->
riscv_extra_op ->
is_riscv_extra_op ->
'a1val is_riscv_extra_op_rec :
(Wsize.wsize -> Wsize.is_wsize -> 'a1) ->
'a1 ->
riscv_extra_op ->
is_riscv_extra_op ->
'a1val riscv_extra_op_tag : riscv_extra_op -> BinNums.positiveval is_riscv_extra_op_inhab : riscv_extra_op -> is_riscv_extra_opval is_riscv_extra_op_functor :
riscv_extra_op ->
is_riscv_extra_op ->
is_riscv_extra_optype box_riscv_extra_op_SWAP = Wsize.wsizeval coq_Box_riscv_extra_op_SWAP_0 : box_riscv_extra_op_SWAP -> Wsize.wsizetype riscv_extra_op_fields_t = __val riscv_extra_op_fields : riscv_extra_op -> riscv_extra_op_fields_tval riscv_extra_op_construct :
BinNums.positive ->
riscv_extra_op_fields_t ->
riscv_extra_op optionval riscv_extra_op_induction :
(Wsize.wsize -> Wsize.is_wsize -> 'a1) ->
'a1 ->
riscv_extra_op ->
is_riscv_extra_op ->
'a1val riscv_extra_op_eqb_fields :
(riscv_extra_op -> riscv_extra_op -> bool) ->
BinNums.positive ->
riscv_extra_op_fields_t ->
riscv_extra_op_fields_t ->
boolval riscv_extra_op_eqb : riscv_extra_op -> riscv_extra_op -> boolval riscv_extra_op_eqb_OK : riscv_extra_op -> riscv_extra_op -> Bool.reflectval riscv_extra_op_eqb_OK_sumbool : riscv_extra_op -> riscv_extra_op -> boolval coq_HB_unnamed_factory_1 : riscv_extra_op Eqtype.Coq_hasDecEq.axioms_val riscv_extra_riscv_extra_op__canonical__eqtype_Equality :
Eqtype.Equality.coq_typeval eqTC_riscv_extra_op : riscv_extra_op Utils0.eqTypeCval coq_Oriscv_add_large_imm_instr : Sopn.instruction_descval get_instr_desc : riscv_extra_op -> Sopn.instruction_descval riscv_extra_op_decl : riscv_extra_op Sopn.asmOpmodule E : sig ... endval asm_args_of_opn_args :
Riscv_params_core.RISCVFopn_core.opn_args list ->
(((Riscv_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arch_utils.empty,
Riscv_decl.condt,
Riscv_instr_decl.riscv_op)
Arch_decl.asm_op_msb_t
* Fexpr.lexpr list)
* Fexpr.rexpr list)
listval assemble_extra :
Expr.instr_info ->
riscv_extra_op ->
Fexpr.lexpr list ->
Fexpr.rexpr list ->
(((Riscv_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arch_utils.empty,
Riscv_decl.condt,
Riscv_instr_decl.riscv_op)
Arch_decl.asm_op_msb_t
* Fexpr.lexpr list)
* Fexpr.rexpr list)
list
Compiler_util.cexectype riscv_extended_op =
(Riscv_decl.register,
Arch_utils.empty,
Arch_utils.empty,
Arch_utils.empty,
Riscv_decl.condt,
Riscv_instr_decl.riscv_op,
riscv_extra_op)
Arch_extra.extended_op