package jasmin

  1. Overview
  2. Docs
Compiler for High-Assurance and High-Speed Cryptography

Install 

dune-project
 Dependency

github.com Readme Edit opam file Versions (17)

Authors

  1. J
    Jasmin authors and contributors

Maintainers

  1. J
    Jean-Christophe Léchenet <jean-christophe.lechenet@inria.fr>

Sources

jasmin-compiler-v2025.06.1.tar.bz2
sha256=e92b42fa69da7c730b0c26dacf842a72b4febcaf4f2157a1dc18b3cce1f859fa

doc/jasmin.jasmin/Jasmin/Arch_extra/index.html

Module Jasmin.Arch_extra

type 't coq_ToIdent = {
  1. to_ident : 't -> Ident.Ident.ident;
  2. of_ident : Ident.Ident.ident -> 't option;
}
val to_ident : Type.stype -> 'a1 Arch_decl.coq_ToString -> 'a1 coq_ToIdent -> 'a1 -> Ident.Ident.ident
val of_ident : Type.stype -> 'a1 Arch_decl.coq_ToString -> 'a1 coq_ToIdent -> Ident.Ident.ident -> 'a1 option
val to_var : Type.stype -> 'a1 Arch_decl.coq_ToString -> 'a1 coq_ToIdent -> 'a1 -> Var0.Var.var
val of_var : Type.stype -> 'a1 Arch_decl.coq_ToString -> 'a1 coq_ToIdent -> Var0.Var.var -> 'a1 option
module type MkToIdent_T = sig ... end
type ('reg, 'regx, 'xreg, 'rflag, 'cond) arch_toIdent = {
  1. toI_r : 'reg coq_ToIdent;
  2. toI_rx : 'regx coq_ToIdent;
  3. toI_x : 'xreg coq_ToIdent;
  4. toI_f : 'rflag coq_ToIdent;
}
val toI_r : ('a1, 'a2, 'a3, 'a4, 'a5) Arch_decl.arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5) arch_toIdent -> 'a1 coq_ToIdent
val toI_rx : ('a1, 'a2, 'a3, 'a4, 'a5) Arch_decl.arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5) arch_toIdent -> 'a2 coq_ToIdent
val toI_x : ('a1, 'a2, 'a3, 'a4, 'a5) Arch_decl.arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5) arch_toIdent -> 'a3 coq_ToIdent
val toI_f : ('a1, 'a2, 'a3, 'a4, 'a5) Arch_decl.arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5) arch_toIdent -> 'a4 coq_ToIdent
module type AToIdent_T = sig ... end
val var_of_implicit_arg : ('a1, 'a2, 'a3, 'a4, 'a5) Arch_decl.arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5) arch_toIdent -> ('a1, 'a2, 'a3, 'a4, 'a5) Arch_decl.implicit_arg -> Var0.Var.var
val sopn_constrained_register : ('a1, 'a2, 'a3, 'a4, 'a5) Arch_decl.arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5) arch_toIdent -> ('a1, 'a2, 'a3, 'a4, 'a5) Arch_decl.arg_constrained_register -> Sopn.arg_constrained_register
val sopn_arg_desc : ('a1, 'a2, 'a3, 'a4, 'a5) Arch_decl.arch_decl -> ('a1, 'a2, 'a3, 'a4, 'a5) arch_toIdent -> ('a1, 'a2, 'a3, 'a4, 'a5) Arch_decl.arg_desc -> Sopn.arg_desc
type ('reg, 'regx, 'xreg, 'rflag, 'cond, 'asm_op, 'extra_op) asm_extra = {
  1. _asm : ('reg, 'regx, 'xreg, 'rflag, 'cond, 'asm_op) Arch_decl.asm;
  2. _atoI : ('reg, 'regx, 'xreg, 'rflag, 'cond) arch_toIdent;
  3. _extra : 'extra_op Sopn.asmOp;
  4. to_asm : Expr.instr_info -> 'extra_op -> Fexpr.lexpr list -> Fexpr.rexpr list -> ((('reg, 'regx, 'xreg, 'rflag, 'cond, 'asm_op) Arch_decl.asm_op_msb_t * Fexpr.lexpr list) * Fexpr.rexpr list) list Compiler_util.cexec;
}
val _asm : ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) asm_extra -> ('a1, 'a2, 'a3, 'a4, 'a5, 'a6) Arch_decl.asm
val _atoI : ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) asm_extra -> ('a1, 'a2, 'a3, 'a4, 'a5) arch_toIdent
val _extra : ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) asm_extra -> 'a7 Sopn.asmOp
val to_asm : ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) asm_extra -> Expr.instr_info -> 'a7 -> Fexpr.lexpr list -> Fexpr.rexpr list -> ((('a1, 'a2, 'a3, 'a4, 'a5, 'a6) Arch_decl.asm_op_msb_t * Fexpr.lexpr list) * Fexpr.rexpr list) list Compiler_util.cexec
type ('reg, 'regx, 'xreg, 'rflag, 'cond, 'asm_op, 'extra_op) extra_op_t = 'extra_op
type ('reg, 'regx, 'xreg, 'rflag, 'cond, 'asm_op, 'extra_op) extended_op =
  1. | BaseOp of ('reg, 'regx, 'xreg, 'rflag, 'cond, 'asm_op) Arch_decl.asm_op_msb_t
  2. | ExtOp of ('reg, 'regx, 'xreg, 'rflag, 'cond, 'asm_op, 'extra_op) extra_op_t
val extended_op_beq : ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) asm_extra -> ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) extended_op -> ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) extended_op -> bool
val extended_op_eq_axiom : ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) asm_extra -> ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) extended_op Eqtype.eq_axiom
val coq_HB_unnamed_factory_1 : ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) asm_extra -> ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) extended_op Eqtype.Coq_hasDecEq.axioms_
val arch_extra_extended_op__canonical__eqtype_Equality : ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) asm_extra -> Eqtype.Equality.coq_type
val get_instr_desc : ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) asm_extra -> ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) extended_op -> Sopn.instruction_desc
val sopn_prim_string_base : ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) asm_extra -> (string * 'a6 Sopn.prim_constructor) list -> (string * ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) extended_op Sopn.prim_constructor) list
val sopn_prim_string_extra : ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) asm_extra -> (string * 'a7 Sopn.prim_constructor) list -> (string * ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) extended_op Sopn.prim_constructor) list
val get_prime_op : ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) asm_extra -> (string * ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) extended_op Sopn.prim_constructor) list
val eqTC_extended_op : ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) asm_extra -> ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) extended_op Utils0.eqTypeC
val asm_opI : ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) asm_extra -> ('a1, 'a2, 'a3, 'a4, 'a5, 'a6, 'a7) extended_op Sopn.asmOp