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/X86_decl/index.html

Module Jasmin.X86_decl

type __ = Obj.t
val x86_reg_size : Wsize.wsize
val x86_xreg_size : Wsize.wsize
type register =
  1. | RAX
  2. | RCX
  3. | RDX
  4. | RBX
  5. | RSP
  6. | RBP
  7. | RSI
  8. | RDI
  9. | R8
  10. | R9
  11. | R10
  12. | R11
  13. | R12
  14. | R13
  15. | R14
  16. | R15
val register_rect : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> register -> 'a1
val register_rec : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> register -> 'a1
type is_register =
  1. | Coq_is_RAX
  2. | Coq_is_RCX
  3. | Coq_is_RDX
  4. | Coq_is_RBX
  5. | Coq_is_RSP
  6. | Coq_is_RBP
  7. | Coq_is_RSI
  8. | Coq_is_RDI
  9. | Coq_is_R8
  10. | Coq_is_R9
  11. | Coq_is_R10
  12. | Coq_is_R11
  13. | Coq_is_R12
  14. | Coq_is_R13
  15. | Coq_is_R14
  16. | Coq_is_R15
val is_register_rect : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> register -> is_register -> 'a1
val is_register_rec : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> register -> is_register -> 'a1
val register_tag : register -> BinNums.positive
val is_register_inhab : register -> is_register
val is_register_functor : register -> is_register -> is_register
type box_register_RAX =
  1. | Box_register_RAX
type register_fields_t = __
val register_fields : register -> register_fields_t
val register_construct : BinNums.positive -> register_fields_t -> register option
val register_induction : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> register -> is_register -> 'a1
val register_eqb_fields : (register -> register -> bool) -> BinNums.positive -> register_fields_t -> register_fields_t -> bool
val register_eqb : register -> register -> bool
val register_eqb_OK : register -> register -> Bool.reflect
val register_eqb_OK_sumbool : register -> register -> bool
type register_ext =
  1. | MM0
  2. | MM1
  3. | MM2
  4. | MM3
  5. | MM4
  6. | MM5
  7. | MM6
  8. | MM7
val register_ext_rect : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> register_ext -> 'a1
val register_ext_rec : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> register_ext -> 'a1
type is_register_ext =
  1. | Coq_is_MM0
  2. | Coq_is_MM1
  3. | Coq_is_MM2
  4. | Coq_is_MM3
  5. | Coq_is_MM4
  6. | Coq_is_MM5
  7. | Coq_is_MM6
  8. | Coq_is_MM7
val is_register_ext_rect : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> register_ext -> is_register_ext -> 'a1
val is_register_ext_rec : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> register_ext -> is_register_ext -> 'a1
val register_ext_tag : register_ext -> BinNums.positive
val is_register_ext_inhab : register_ext -> is_register_ext
val is_register_ext_functor : register_ext -> is_register_ext -> is_register_ext
type box_register_ext_MM0 =
  1. | Box_register_ext_MM0
type register_ext_fields_t = __
val register_ext_fields : register_ext -> register_ext_fields_t
val register_ext_construct : BinNums.positive -> register_ext_fields_t -> register_ext option
val register_ext_induction : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> register_ext -> is_register_ext -> 'a1
val register_ext_eqb_fields : (register_ext -> register_ext -> bool) -> BinNums.positive -> register_ext_fields_t -> register_ext_fields_t -> bool
val register_ext_eqb : register_ext -> register_ext -> bool
val register_ext_eqb_OK : register_ext -> register_ext -> Bool.reflect
val register_ext_eqb_OK_sumbool : register_ext -> register_ext -> bool
type xmm_register =
  1. | XMM0
  2. | XMM1
  3. | XMM2
  4. | XMM3
  5. | XMM4
  6. | XMM5
  7. | XMM6
  8. | XMM7
  9. | XMM8
  10. | XMM9
  11. | XMM10
  12. | XMM11
  13. | XMM12
  14. | XMM13
  15. | XMM14
  16. | XMM15
val xmm_register_rect : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> xmm_register -> 'a1
val xmm_register_rec : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> xmm_register -> 'a1
type is_xmm_register =
  1. | Coq_is_XMM0
  2. | Coq_is_XMM1
  3. | Coq_is_XMM2
  4. | Coq_is_XMM3
  5. | Coq_is_XMM4
  6. | Coq_is_XMM5
  7. | Coq_is_XMM6
  8. | Coq_is_XMM7
  9. | Coq_is_XMM8
  10. | Coq_is_XMM9
  11. | Coq_is_XMM10
  12. | Coq_is_XMM11
  13. | Coq_is_XMM12
  14. | Coq_is_XMM13
  15. | Coq_is_XMM14
  16. | Coq_is_XMM15
val is_xmm_register_rect : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> xmm_register -> is_xmm_register -> 'a1
val is_xmm_register_rec : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> xmm_register -> is_xmm_register -> 'a1
val xmm_register_tag : xmm_register -> BinNums.positive
val is_xmm_register_inhab : xmm_register -> is_xmm_register
val is_xmm_register_functor : xmm_register -> is_xmm_register -> is_xmm_register
type box_xmm_register_XMM0 =
  1. | Box_xmm_register_XMM0
type xmm_register_fields_t = __
val xmm_register_fields : xmm_register -> xmm_register_fields_t
val xmm_register_construct : BinNums.positive -> xmm_register_fields_t -> xmm_register option
val xmm_register_induction : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> xmm_register -> is_xmm_register -> 'a1
val xmm_register_eqb_fields : (xmm_register -> xmm_register -> bool) -> BinNums.positive -> xmm_register_fields_t -> xmm_register_fields_t -> bool
val xmm_register_eqb : xmm_register -> xmm_register -> bool
val xmm_register_eqb_OK : xmm_register -> xmm_register -> Bool.reflect
val xmm_register_eqb_OK_sumbool : xmm_register -> xmm_register -> bool
type rflag =
  1. | CF
  2. | PF
  3. | ZF
  4. | SF
  5. | OF
val rflag_rect : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> rflag -> 'a1
val rflag_rec : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> rflag -> 'a1
type is_rflag =
  1. | Coq_is_CF
  2. | Coq_is_PF
  3. | Coq_is_ZF
  4. | Coq_is_SF
  5. | Coq_is_OF
val is_rflag_rect : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> rflag -> is_rflag -> 'a1
val is_rflag_rec : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> rflag -> is_rflag -> 'a1
val rflag_tag : rflag -> BinNums.positive
val is_rflag_inhab : rflag -> is_rflag
val is_rflag_functor : rflag -> is_rflag -> is_rflag
type box_rflag_CF =
  1. | Box_rflag_CF
type rflag_fields_t = __
val rflag_fields : rflag -> rflag_fields_t
val rflag_construct : BinNums.positive -> rflag_fields_t -> rflag option
val rflag_induction : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> rflag -> is_rflag -> 'a1
val rflag_eqb_fields : (rflag -> rflag -> bool) -> BinNums.positive -> rflag_fields_t -> rflag_fields_t -> bool
val rflag_eqb : rflag -> rflag -> bool
val rflag_eqb_OK : rflag -> rflag -> Bool.reflect
val rflag_eqb_OK_sumbool : rflag -> rflag -> bool
type condt =
  1. | O_ct
  2. | NO_ct
  3. | B_ct
  4. | NB_ct
  5. | E_ct
  6. | NE_ct
  7. | BE_ct
  8. | NBE_ct
  9. | S_ct
  10. | NS_ct
  11. | P_ct
  12. | NP_ct
  13. | L_ct
  14. | NL_ct
  15. | LE_ct
  16. | NLE_ct
val condt_rect : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> condt -> 'a1
val condt_rec : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> condt -> 'a1
type is_condt =
  1. | Coq_is_O_ct
  2. | Coq_is_NO_ct
  3. | Coq_is_B_ct
  4. | Coq_is_NB_ct
  5. | Coq_is_E_ct
  6. | Coq_is_NE_ct
  7. | Coq_is_BE_ct
  8. | Coq_is_NBE_ct
  9. | Coq_is_S_ct
  10. | Coq_is_NS_ct
  11. | Coq_is_P_ct
  12. | Coq_is_NP_ct
  13. | Coq_is_L_ct
  14. | Coq_is_NL_ct
  15. | Coq_is_LE_ct
  16. | Coq_is_NLE_ct
val is_condt_rect : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> condt -> is_condt -> 'a1
val is_condt_rec : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> condt -> is_condt -> 'a1
val condt_tag : condt -> BinNums.positive
val is_condt_inhab : condt -> is_condt
val is_condt_functor : condt -> is_condt -> is_condt
type box_condt_O_ct =
  1. | Box_condt_O_ct
type condt_fields_t = __
val condt_fields : condt -> condt_fields_t
val condt_construct : BinNums.positive -> condt_fields_t -> condt option
val condt_induction : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> condt -> is_condt -> 'a1
val condt_eqb_fields : (condt -> condt -> bool) -> BinNums.positive -> condt_fields_t -> condt_fields_t -> bool
val condt_eqb : condt -> condt -> bool
val condt_eqb_OK : condt -> condt -> Bool.reflect
val condt_eqb_OK_sumbool : condt -> condt -> bool
val coq_HB_unnamed_factory_1 : register Eqtype.Coq_hasDecEq.axioms_
val x86_decl_register__canonical__eqtype_Equality : Eqtype.Equality.coq_type
val coq_HB_unnamed_factory_3 : register_ext Eqtype.Coq_hasDecEq.axioms_
val x86_decl_register_ext__canonical__eqtype_Equality : Eqtype.Equality.coq_type
val coq_HB_unnamed_factory_5 : xmm_register Eqtype.Coq_hasDecEq.axioms_
val x86_decl_xmm_register__canonical__eqtype_Equality : Eqtype.Equality.coq_type
val coq_HB_unnamed_factory_7 : rflag Eqtype.Coq_hasDecEq.axioms_
val x86_decl_rflag__canonical__eqtype_Equality : Eqtype.Equality.coq_type
val coq_HB_unnamed_factory_9 : condt Eqtype.Coq_hasDecEq.axioms_
val x86_decl_condt__canonical__eqtype_Equality : Eqtype.Equality.coq_type
val registers : register list
val coq_HB_unnamed_factory_11 : register Choice.Countable.axioms_
val choice_Countable__to__choice_hasChoice : register Choice.Coq_hasChoice.axioms_
val choice_Countable__to__choice_Choice_isCountable : register Choice.Choice_isCountable.axioms_
val coq_HB_unnamed_mixin_15 : register Choice.Coq_hasChoice.axioms_
val x86_decl_register__canonical__choice_Choice : Choice.Choice.coq_type
val coq_HB_unnamed_mixin_16 : register Choice.Choice_isCountable.axioms_
val x86_decl_register__canonical__choice_Countable : Choice.Countable.coq_type
val coq_HB_unnamed_factory_17 : register Fintype.Coq_isFinite.axioms_
val x86_decl_register__canonical__fintype_Finite : Fintype.Finite.coq_type
val regxs : register_ext list
val coq_HB_unnamed_factory_19 : register_ext Choice.Countable.axioms_
val choice_Countable__to__choice_hasChoice__21 : register_ext Choice.Coq_hasChoice.axioms_
val choice_Countable__to__choice_Choice_isCountable__24 : register_ext Choice.Choice_isCountable.axioms_
val coq_HB_unnamed_mixin_25 : register_ext Choice.Coq_hasChoice.axioms_
val x86_decl_register_ext__canonical__choice_Choice : Choice.Choice.coq_type
val coq_HB_unnamed_mixin_26 : register_ext Choice.Choice_isCountable.axioms_
val x86_decl_register_ext__canonical__choice_Countable : Choice.Countable.coq_type
val coq_HB_unnamed_factory_27 : register_ext Fintype.Coq_isFinite.axioms_
val x86_decl_register_ext__canonical__fintype_Finite : Fintype.Finite.coq_type
val xmm_registers : xmm_register list
val coq_HB_unnamed_factory_29 : xmm_register Choice.Countable.axioms_
val choice_Countable__to__choice_hasChoice__31 : xmm_register Choice.Coq_hasChoice.axioms_
val choice_Countable__to__choice_Choice_isCountable__34 : xmm_register Choice.Choice_isCountable.axioms_
val coq_HB_unnamed_mixin_35 : xmm_register Choice.Coq_hasChoice.axioms_
val x86_decl_xmm_register__canonical__choice_Choice : Choice.Choice.coq_type
val coq_HB_unnamed_mixin_36 : xmm_register Choice.Choice_isCountable.axioms_
val x86_decl_xmm_register__canonical__choice_Countable : Choice.Countable.coq_type
val coq_HB_unnamed_factory_37 : xmm_register Fintype.Coq_isFinite.axioms_
val x86_decl_xmm_register__canonical__fintype_Finite : Fintype.Finite.coq_type
val rflags : rflag list
val coq_HB_unnamed_factory_39 : rflag Choice.Countable.axioms_
val choice_Countable__to__choice_hasChoice__41 : rflag Choice.Coq_hasChoice.axioms_
val choice_Countable__to__choice_Choice_isCountable__44 : rflag Choice.Choice_isCountable.axioms_
val coq_HB_unnamed_mixin_45 : rflag Choice.Coq_hasChoice.axioms_
val x86_decl_rflag__canonical__choice_Choice : Choice.Choice.coq_type
val coq_HB_unnamed_mixin_46 : rflag Choice.Choice_isCountable.axioms_
val x86_decl_rflag__canonical__choice_Countable : Choice.Countable.coq_type
val coq_HB_unnamed_factory_47 : rflag Fintype.Coq_isFinite.axioms_
val x86_decl_rflag__canonical__fintype_Finite : Fintype.Finite.coq_type
val eqTC_register : register Utils0.eqTypeC
val finC_register : register Utils0.finTypeC
val register_to_string : register -> string
val regx_to_string : register_ext -> string
val eqTC_xmm_register : xmm_register Utils0.eqTypeC
val finC_xmm_register : xmm_register Utils0.finTypeC
val xreg_to_string : xmm_register -> string
val eqTC_rflag : rflag Utils0.eqTypeC
val finC_rflag : rflag Utils0.finTypeC
val rflag_to_string : rflag -> string
val x86_rflag_toS : rflag Arch_decl.coq_ToString
val eqC_condt : condt Utils0.eqTypeC