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 (23)

Authors

  1. J
    Jasmin authors and contributors

Maintainers

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

Sources

jasmin-compiler-v2026.09.0.tar.bz2
sha256=11fec571efb9f7b3a47fea324b4e2a68289e0b73b2248d237eccf139b5218190

doc/jasmin.jasmin/Jasmin/Armv8a_decl/index.html

Module Jasmin.Armv8a_decl

type __ = Obj.t
val armv8a_reg_size : Wsize.wsize
val armv8a_xreg_size : Wsize.wsize
type register =
  1. | R0
  2. | R1
  3. | R2
  4. | R3
  5. | R4
  6. | R5
  7. | R6
  8. | R7
  9. | R8
  10. | R9
  11. | R10
  12. | R11
  13. | R12
  14. | R13
  15. | R14
  16. | R15
  17. | R16
  18. | R17
  19. | R19
  20. | R20
  21. | R21
  22. | R22
  23. | R23
  24. | R24
  25. | R25
  26. | R26
  27. | R27
  28. | R28
  29. | R29
  30. | R30
  31. | RSP
val register_rect : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> '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 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> register -> 'a1
type is_register =
  1. | Coq_is_R0
  2. | Coq_is_R1
  3. | Coq_is_R2
  4. | Coq_is_R3
  5. | Coq_is_R4
  6. | Coq_is_R5
  7. | Coq_is_R6
  8. | Coq_is_R7
  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
  17. | Coq_is_R16
  18. | Coq_is_R17
  19. | Coq_is_R19
  20. | Coq_is_R20
  21. | Coq_is_R21
  22. | Coq_is_R22
  23. | Coq_is_R23
  24. | Coq_is_R24
  25. | Coq_is_R25
  26. | Coq_is_R26
  27. | Coq_is_R27
  28. | Coq_is_R28
  29. | Coq_is_R29
  30. | Coq_is_R30
  31. | Coq_is_RSP
val is_register_rect : 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> '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 -> '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_R0 =
  1. | Box_register_R0
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 -> '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 -> Datatypes.reflect
val register_eqb_OK_sumbool : register -> register -> bool
val eqTC_register : register Utils0.eqTypeC
val armv8a_register_eqType : Eqtype.Equality.coq_type
val registers : register list
val finTC_register : register Utils0.finTypeC
val register_finType : Fintype.Finite.coq_type
val register_to_string : register -> string
val shift_kind_eqType : Eqtype.Equality.coq_type
val shift_kinds : Shift_kind.shift_kind list
val string_of_shift_kind : Shift_kind.shift_kind -> string
val check_shift_amount : Wsize.wsize -> BinNums.coq_Z -> bool
val shift_of_sop2 : Wsize.wsize -> Operators.sop2 -> Shift_kind.shift_kind option
val is_arith_imm : BinNums.coq_Z -> bool
val is_ones_run : BinNums.coq_Z -> BinNums.coq_Z -> bool
val is_bitmask_imm : Wsize.wsize -> BinNums.coq_Z -> bool
val is_wide_imm : Wsize.wsize -> BinNums.coq_Z -> bool
val is_mov_imm : Wsize.wsize -> BinNums.coq_Z -> bool
type armv8a_caimm_cond =
  1. | CAimmC_armv8a_shift_amount of Wsize.wsize
  2. | CAimmC_armv8a_halfword_shift of Wsize.wsize
  3. | CAimmC_armv8a_arith_imm
  4. | CAimmC_armv8a_bitmask_imm
  5. | CAimmC_armv8a_mov_imm
val armv8a_caimm_cond_rect : (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> armv8a_caimm_cond -> 'a1
val armv8a_caimm_cond_rec : (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> armv8a_caimm_cond -> 'a1
type is_armv8a_caimm_cond =
  1. | Coq_is_CAimmC_armv8a_shift_amount of Wsize.wsize * Wsize.is_wsize
  2. | Coq_is_CAimmC_armv8a_halfword_shift of Wsize.wsize * Wsize.is_wsize
  3. | Coq_is_CAimmC_armv8a_arith_imm
  4. | Coq_is_CAimmC_armv8a_bitmask_imm
  5. | Coq_is_CAimmC_armv8a_mov_imm
val is_armv8a_caimm_cond_rect : (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> armv8a_caimm_cond -> is_armv8a_caimm_cond -> 'a1
val is_armv8a_caimm_cond_rec : (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> armv8a_caimm_cond -> is_armv8a_caimm_cond -> 'a1
val armv8a_caimm_cond_tag : armv8a_caimm_cond -> BinNums.positive
val is_armv8a_caimm_cond_inhab : armv8a_caimm_cond -> is_armv8a_caimm_cond
val is_armv8a_caimm_cond_functor : armv8a_caimm_cond -> is_armv8a_caimm_cond -> is_armv8a_caimm_cond
type box_armv8a_caimm_cond_CAimmC_armv8a_shift_amount = Wsize.wsize
val coq_Box_armv8a_caimm_cond_CAimmC_armv8a_shift_amount_0 : box_armv8a_caimm_cond_CAimmC_armv8a_shift_amount -> Wsize.wsize
type box_armv8a_caimm_cond_CAimmC_armv8a_arith_imm =
  1. | Box_armv8a_caimm_cond_CAimmC_armv8a_arith_imm
type armv8a_caimm_cond_fields_t = __
val armv8a_caimm_cond_fields : armv8a_caimm_cond -> armv8a_caimm_cond_fields_t
val armv8a_caimm_cond_construct : BinNums.positive -> armv8a_caimm_cond_fields_t -> armv8a_caimm_cond option
val armv8a_caimm_cond_induction : (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> armv8a_caimm_cond -> is_armv8a_caimm_cond -> 'a1
val armv8a_caimm_cond_eqb_fields : (armv8a_caimm_cond -> armv8a_caimm_cond -> bool) -> BinNums.positive -> armv8a_caimm_cond_fields_t -> armv8a_caimm_cond_fields_t -> bool
val armv8a_caimm_cond_eqb : armv8a_caimm_cond -> armv8a_caimm_cond -> bool
val armv8a_caimm_cond_eqb_OK : armv8a_caimm_cond -> armv8a_caimm_cond -> Datatypes.reflect
val armv8a_caimm_cond_eqb_OK_sumbool : armv8a_caimm_cond -> armv8a_caimm_cond -> bool
val eqTC_armv8a_caimm_cond : armv8a_caimm_cond Utils0.eqTypeC
val armv8a_check_CAimm : armv8a_caimm_cond -> Wsize.wsize -> Word0.word -> bool
val armv8a_caimm_cond_pp : armv8a_caimm_cond -> string