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

Module Jasmin.X86_instr_decl

type __ = Obj.t
type x86_op =
  1. | MOV of Wsize.wsize
  2. | MOVSX of Wsize.wsize * Wsize.wsize
  3. | MOVZX of Wsize.wsize * Wsize.wsize
  4. | CMOVcc of Wsize.wsize
  5. | XCHG of Wsize.wsize
  6. | ADD of Wsize.wsize
  7. | SUB of Wsize.wsize
  8. | MUL of Wsize.wsize
  9. | IMUL of Wsize.wsize
  10. | IMULr of Wsize.wsize
  11. | IMULri of Wsize.wsize
  12. | DIV of Wsize.wsize
  13. | IDIV of Wsize.wsize
  14. | CQO of Wsize.wsize
  15. | ADC of Wsize.wsize
  16. | SBB of Wsize.wsize
  17. | NEG of Wsize.wsize
  18. | INC of Wsize.wsize
  19. | DEC of Wsize.wsize
  20. | LZCNT of Wsize.wsize
  21. | TZCNT of Wsize.wsize
  22. | BSR of Wsize.wsize
  23. | SETcc
  24. | BT of Wsize.wsize
  25. | CLC
  26. | STC
  27. | LEA of Wsize.wsize
  28. | TEST of Wsize.wsize
  29. | CMP of Wsize.wsize
  30. | AND of Wsize.wsize
  31. | ANDN of Wsize.wsize
  32. | OR of Wsize.wsize
  33. | XOR of Wsize.wsize
  34. | NOT of Wsize.wsize
  35. | ROR of Wsize.wsize
  36. | ROL of Wsize.wsize
  37. | RCR of Wsize.wsize
  38. | RCL of Wsize.wsize
  39. | SHL of Wsize.wsize
  40. | SHR of Wsize.wsize
  41. | SAL of Wsize.wsize
  42. | SAR of Wsize.wsize
  43. | SHLD of Wsize.wsize
  44. | SHRD of Wsize.wsize
  45. | RORX of Wsize.wsize
  46. | SARX of Wsize.wsize
  47. | SHRX of Wsize.wsize
  48. | SHLX of Wsize.wsize
  49. | MULX_lo_hi of Wsize.wsize
  50. | ADCX of Wsize.wsize
  51. | ADOX of Wsize.wsize
  52. | BSWAP of Wsize.wsize
  53. | POPCNT of Wsize.wsize
  54. | BTR of Wsize.wsize
  55. | BTS of Wsize.wsize
  56. | PEXT of Wsize.wsize
  57. | PDEP of Wsize.wsize
  58. | MOVX of Wsize.wsize
  59. | POR
  60. | PADD of Wsize.velem * Wsize.wsize
  61. | MOVD of Wsize.wsize
  62. | MOVV of Wsize.wsize
  63. | VMOV of Wsize.wsize
  64. | VMOVDQA of Wsize.wsize
  65. | VMOVDQU of Wsize.wsize
  66. | VPMOVSX of Wsize.velem * Wsize.wsize * Wsize.velem * Wsize.wsize
  67. | VPMOVZX of Wsize.velem * Wsize.wsize * Wsize.velem * Wsize.wsize
  68. | VPAND of Wsize.wsize
  69. | VPANDN of Wsize.wsize
  70. | VPOR of Wsize.wsize
  71. | VPXOR of Wsize.wsize
  72. | VPADD of Wsize.velem * Wsize.wsize
  73. | VPSUB of Wsize.velem * Wsize.wsize
  74. | VPAVG of Wsize.velem * Wsize.wsize
  75. | VPMULL of Wsize.velem * Wsize.wsize
  76. | VPMULH of Wsize.wsize
  77. | VPMULHU of Wsize.wsize
  78. | VPMULHRS of Wsize.wsize
  79. | VPMUL of Wsize.wsize
  80. | VPMULU of Wsize.wsize
  81. | VPEXTR of Wsize.wsize
  82. | VPINSR of Wsize.velem
  83. | VPSLL of Wsize.velem * Wsize.wsize
  84. | VPSRL of Wsize.velem * Wsize.wsize
  85. | VPSRA of Wsize.velem * Wsize.wsize
  86. | VPSLLV of Wsize.velem * Wsize.wsize
  87. | VPSRLV of Wsize.velem * Wsize.wsize
  88. | VPSLLDQ of Wsize.wsize
  89. | VPSRLDQ of Wsize.wsize
  90. | VPSHUFB of Wsize.wsize
  91. | VPSHUFD of Wsize.wsize
  92. | VPSHUFHW of Wsize.wsize
  93. | VPSHUFLW of Wsize.wsize
  94. | VPBLEND of Wsize.velem * Wsize.wsize
  95. | BLENDV of Wsize.velem * Wsize.wsize
  96. | VPACKUS of Wsize.velem * Wsize.wsize
  97. | VPACKSS of Wsize.velem * Wsize.wsize
  98. | VSHUFPS of Wsize.wsize
  99. | VPBROADCAST of Wsize.velem * Wsize.wsize
  100. | VMOVSHDUP of Wsize.wsize
  101. | VMOVSLDUP of Wsize.wsize
  102. | VPALIGNR of Wsize.wsize
  103. | VBROADCASTI128
  104. | VPUNPCKH of Wsize.velem * Wsize.wsize
  105. | VPUNPCKL of Wsize.velem * Wsize.wsize
  106. | VEXTRACTI128
  107. | VINSERTI128
  108. | VPERM2I128
  109. | VPERMD
  110. | VPERMQ
  111. | VPMOVMSKB of Wsize.wsize * Wsize.wsize
  112. | MOVEMASK of Wsize.velem * Wsize.wsize
  113. | VPCMPEQ of Wsize.velem * Wsize.wsize
  114. | VPCMPGT of Wsize.velem * Wsize.wsize
  115. | VPSIGN of Wsize.velem * Wsize.wsize
  116. | VPMADDUBSW of Wsize.wsize
  117. | VPMADDWD of Wsize.wsize
  118. | VMOVLPD
  119. | VMOVHPD
  120. | VPMINU of Wsize.velem * Wsize.wsize
  121. | VPMINS of Wsize.velem * Wsize.wsize
  122. | VPMAXU of Wsize.velem * Wsize.wsize
  123. | VPMAXS of Wsize.velem * Wsize.wsize
  124. | VPABS of Wsize.velem * Wsize.wsize
  125. | VPTEST of Wsize.wsize
  126. | CLFLUSH
  127. | PREFETCHT0
  128. | PREFETCHT1
  129. | PREFETCHT2
  130. | PREFETCHNTA
  131. | LFENCE
  132. | MFENCE
  133. | SFENCE
  134. | RDTSC of Wsize.wsize
  135. | RDTSCP of Wsize.wsize
  136. | AESDEC
  137. | VAESDEC of Wsize.wsize
  138. | AESDECLAST
  139. | VAESDECLAST of Wsize.wsize
  140. | AESENC
  141. | VAESENC of Wsize.wsize
  142. | AESENCLAST
  143. | VAESENCLAST of Wsize.wsize
  144. | AESIMC
  145. | VAESIMC
  146. | AESKEYGENASSIST
  147. | VAESKEYGENASSIST
  148. | PCLMULQDQ
  149. | VPCLMULQDQ of Wsize.wsize
  150. | SHA256RNDS2
  151. | SHA256MSG1
  152. | SHA256MSG2
val x86_op_rect : (Wsize.wsize -> 'a1) -> (Wsize.wsize -> Wsize.wsize -> 'a1) -> (Wsize.wsize -> Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> 'a1 -> (Wsize.wsize -> 'a1) -> 'a1 -> 'a1 -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> 'a1 -> (Wsize.velem -> Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.velem -> Wsize.wsize -> Wsize.velem -> Wsize.wsize -> 'a1) -> (Wsize.velem -> Wsize.wsize -> Wsize.velem -> Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.velem -> Wsize.wsize -> 'a1) -> (Wsize.velem -> Wsize.wsize -> 'a1) -> (Wsize.velem -> Wsize.wsize -> 'a1) -> (Wsize.velem -> Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.velem -> 'a1) -> (Wsize.velem -> Wsize.wsize -> 'a1) -> (Wsize.velem -> Wsize.wsize -> 'a1) -> (Wsize.velem -> Wsize.wsize -> 'a1) -> (Wsize.velem -> Wsize.wsize -> 'a1) -> (Wsize.velem -> Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.velem -> Wsize.wsize -> 'a1) -> (Wsize.velem -> Wsize.wsize -> 'a1) -> (Wsize.velem -> Wsize.wsize -> 'a1) -> (Wsize.velem -> Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.velem -> Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> 'a1 -> (Wsize.velem -> Wsize.wsize -> 'a1) -> (Wsize.velem -> Wsize.wsize -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> (Wsize.wsize -> Wsize.wsize -> 'a1) -> (Wsize.velem -> Wsize.wsize -> 'a1) -> (Wsize.velem -> Wsize.wsize -> 'a1) -> (Wsize.velem -> Wsize.wsize -> 'a1) -> (Wsize.velem -> Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> 'a1 -> 'a1 -> (Wsize.velem -> Wsize.wsize -> 'a1) -> (Wsize.velem -> Wsize.wsize -> 'a1) -> (Wsize.velem -> Wsize.wsize -> 'a1) -> (Wsize.velem -> Wsize.wsize -> 'a1) -> (Wsize.velem -> Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> 'a1 -> (Wsize.wsize -> 'a1) -> 'a1 -> (Wsize.wsize -> 'a1) -> 'a1 -> (Wsize.wsize -> 'a1) -> 'a1 -> (Wsize.wsize -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> (Wsize.wsize -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> x86_op -> 'a1
val x86_op_rec : (Wsize.wsize -> 'a1) -> (Wsize.wsize -> Wsize.wsize -> 'a1) -> (Wsize.wsize -> Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> 'a1 -> (Wsize.wsize -> 'a1) -> 'a1 -> 'a1 -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> 'a1 -> (Wsize.velem -> Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.velem -> Wsize.wsize -> Wsize.velem -> Wsize.wsize -> 'a1) -> (Wsize.velem -> Wsize.wsize -> Wsize.velem -> Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.velem -> Wsize.wsize -> 'a1) -> (Wsize.velem -> Wsize.wsize -> 'a1) -> (Wsize.velem -> Wsize.wsize -> 'a1) -> (Wsize.velem -> Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.velem -> 'a1) -> (Wsize.velem -> Wsize.wsize -> 'a1) -> (Wsize.velem -> Wsize.wsize -> 'a1) -> (Wsize.velem -> Wsize.wsize -> 'a1) -> (Wsize.velem -> Wsize.wsize -> 'a1) -> (Wsize.velem -> Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.velem -> Wsize.wsize -> 'a1) -> (Wsize.velem -> Wsize.wsize -> 'a1) -> (Wsize.velem -> Wsize.wsize -> 'a1) -> (Wsize.velem -> Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.velem -> Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> 'a1 -> (Wsize.velem -> Wsize.wsize -> 'a1) -> (Wsize.velem -> Wsize.wsize -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> (Wsize.wsize -> Wsize.wsize -> 'a1) -> (Wsize.velem -> Wsize.wsize -> 'a1) -> (Wsize.velem -> Wsize.wsize -> 'a1) -> (Wsize.velem -> Wsize.wsize -> 'a1) -> (Wsize.velem -> Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> 'a1 -> 'a1 -> (Wsize.velem -> Wsize.wsize -> 'a1) -> (Wsize.velem -> Wsize.wsize -> 'a1) -> (Wsize.velem -> Wsize.wsize -> 'a1) -> (Wsize.velem -> Wsize.wsize -> 'a1) -> (Wsize.velem -> Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> (Wsize.wsize -> 'a1) -> (Wsize.wsize -> 'a1) -> 'a1 -> (Wsize.wsize -> 'a1) -> 'a1 -> (Wsize.wsize -> 'a1) -> 'a1 -> (Wsize.wsize -> 'a1) -> 'a1 -> (Wsize.wsize -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> (Wsize.wsize -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> x86_op -> 'a1
type is_x86_op =
  1. | Coq_is_MOV of Wsize.wsize * Wsize.is_wsize
  2. | Coq_is_MOVSX of Wsize.wsize * Wsize.is_wsize * Wsize.wsize * Wsize.is_wsize
  3. | Coq_is_MOVZX of Wsize.wsize * Wsize.is_wsize * Wsize.wsize * Wsize.is_wsize
  4. | Coq_is_CMOVcc of Wsize.wsize * Wsize.is_wsize
  5. | Coq_is_XCHG of Wsize.wsize * Wsize.is_wsize
  6. | Coq_is_ADD of Wsize.wsize * Wsize.is_wsize
  7. | Coq_is_SUB of Wsize.wsize * Wsize.is_wsize
  8. | Coq_is_MUL of Wsize.wsize * Wsize.is_wsize
  9. | Coq_is_IMUL of Wsize.wsize * Wsize.is_wsize
  10. | Coq_is_IMULr of Wsize.wsize * Wsize.is_wsize
  11. | Coq_is_IMULri of Wsize.wsize * Wsize.is_wsize
  12. | Coq_is_DIV of Wsize.wsize * Wsize.is_wsize
  13. | Coq_is_IDIV of Wsize.wsize * Wsize.is_wsize
  14. | Coq_is_CQO of Wsize.wsize * Wsize.is_wsize
  15. | Coq_is_ADC of Wsize.wsize * Wsize.is_wsize
  16. | Coq_is_SBB of Wsize.wsize * Wsize.is_wsize
  17. | Coq_is_NEG of Wsize.wsize * Wsize.is_wsize
  18. | Coq_is_INC of Wsize.wsize * Wsize.is_wsize
  19. | Coq_is_DEC of Wsize.wsize * Wsize.is_wsize
  20. | Coq_is_LZCNT of Wsize.wsize * Wsize.is_wsize
  21. | Coq_is_TZCNT of Wsize.wsize * Wsize.is_wsize
  22. | Coq_is_BSR of Wsize.wsize * Wsize.is_wsize
  23. | Coq_is_SETcc
  24. | Coq_is_BT of Wsize.wsize * Wsize.is_wsize
  25. | Coq_is_CLC
  26. | Coq_is_STC
  27. | Coq_is_LEA of Wsize.wsize * Wsize.is_wsize
  28. | Coq_is_TEST of Wsize.wsize * Wsize.is_wsize
  29. | Coq_is_CMP of Wsize.wsize * Wsize.is_wsize
  30. | Coq_is_AND of Wsize.wsize * Wsize.is_wsize
  31. | Coq_is_ANDN of Wsize.wsize * Wsize.is_wsize
  32. | Coq_is_OR of Wsize.wsize * Wsize.is_wsize
  33. | Coq_is_XOR of Wsize.wsize * Wsize.is_wsize
  34. | Coq_is_NOT of Wsize.wsize * Wsize.is_wsize
  35. | Coq_is_ROR of Wsize.wsize * Wsize.is_wsize
  36. | Coq_is_ROL of Wsize.wsize * Wsize.is_wsize
  37. | Coq_is_RCR of Wsize.wsize * Wsize.is_wsize
  38. | Coq_is_RCL of Wsize.wsize * Wsize.is_wsize
  39. | Coq_is_SHL of Wsize.wsize * Wsize.is_wsize
  40. | Coq_is_SHR of Wsize.wsize * Wsize.is_wsize
  41. | Coq_is_SAL of Wsize.wsize * Wsize.is_wsize
  42. | Coq_is_SAR of Wsize.wsize * Wsize.is_wsize
  43. | Coq_is_SHLD of Wsize.wsize * Wsize.is_wsize
  44. | Coq_is_SHRD of Wsize.wsize * Wsize.is_wsize
  45. | Coq_is_RORX of Wsize.wsize * Wsize.is_wsize
  46. | Coq_is_SARX of Wsize.wsize * Wsize.is_wsize
  47. | Coq_is_SHRX of Wsize.wsize * Wsize.is_wsize
  48. | Coq_is_SHLX of Wsize.wsize * Wsize.is_wsize
  49. | Coq_is_MULX_lo_hi of Wsize.wsize * Wsize.is_wsize
  50. | Coq_is_ADCX of Wsize.wsize * Wsize.is_wsize
  51. | Coq_is_ADOX of Wsize.wsize * Wsize.is_wsize
  52. | Coq_is_BSWAP of Wsize.wsize * Wsize.is_wsize
  53. | Coq_is_POPCNT of Wsize.wsize * Wsize.is_wsize
  54. | Coq_is_BTR of Wsize.wsize * Wsize.is_wsize
  55. | Coq_is_BTS of Wsize.wsize * Wsize.is_wsize
  56. | Coq_is_PEXT of Wsize.wsize * Wsize.is_wsize
  57. | Coq_is_PDEP of Wsize.wsize * Wsize.is_wsize
  58. | Coq_is_MOVX of Wsize.wsize * Wsize.is_wsize
  59. | Coq_is_POR
  60. | Coq_is_PADD of Wsize.velem * Wsize.is_velem * Wsize.wsize * Wsize.is_wsize
  61. | Coq_is_MOVD of Wsize.wsize * Wsize.is_wsize
  62. | Coq_is_MOVV of Wsize.wsize * Wsize.is_wsize
  63. | Coq_is_VMOV of Wsize.wsize * Wsize.is_wsize
  64. | Coq_is_VMOVDQA of Wsize.wsize * Wsize.is_wsize
  65. | Coq_is_VMOVDQU of Wsize.wsize * Wsize.is_wsize
  66. | Coq_is_VPMOVSX of Wsize.velem * Wsize.is_velem * Wsize.wsize * Wsize.is_wsize * Wsize.velem * Wsize.is_velem * Wsize.wsize * Wsize.is_wsize
  67. | Coq_is_VPMOVZX of Wsize.velem * Wsize.is_velem * Wsize.wsize * Wsize.is_wsize * Wsize.velem * Wsize.is_velem * Wsize.wsize * Wsize.is_wsize
  68. | Coq_is_VPAND of Wsize.wsize * Wsize.is_wsize
  69. | Coq_is_VPANDN of Wsize.wsize * Wsize.is_wsize
  70. | Coq_is_VPOR of Wsize.wsize * Wsize.is_wsize
  71. | Coq_is_VPXOR of Wsize.wsize * Wsize.is_wsize
  72. | Coq_is_VPADD of Wsize.velem * Wsize.is_velem * Wsize.wsize * Wsize.is_wsize
  73. | Coq_is_VPSUB of Wsize.velem * Wsize.is_velem * Wsize.wsize * Wsize.is_wsize
  74. | Coq_is_VPAVG of Wsize.velem * Wsize.is_velem * Wsize.wsize * Wsize.is_wsize
  75. | Coq_is_VPMULL of Wsize.velem * Wsize.is_velem * Wsize.wsize * Wsize.is_wsize
  76. | Coq_is_VPMULH of Wsize.wsize * Wsize.is_wsize
  77. | Coq_is_VPMULHU of Wsize.wsize * Wsize.is_wsize
  78. | Coq_is_VPMULHRS of Wsize.wsize * Wsize.is_wsize
  79. | Coq_is_VPMUL of Wsize.wsize * Wsize.is_wsize
  80. | Coq_is_VPMULU of Wsize.wsize * Wsize.is_wsize
  81. | Coq_is_VPEXTR of Wsize.wsize * Wsize.is_wsize
  82. | Coq_is_VPINSR of Wsize.velem * Wsize.is_velem
  83. | Coq_is_VPSLL of Wsize.velem * Wsize.is_velem * Wsize.wsize * Wsize.is_wsize
  84. | Coq_is_VPSRL of Wsize.velem * Wsize.is_velem * Wsize.wsize * Wsize.is_wsize
  85. | Coq_is_VPSRA of Wsize.velem * Wsize.is_velem * Wsize.wsize * Wsize.is_wsize
  86. | Coq_is_VPSLLV of Wsize.velem * Wsize.is_velem * Wsize.wsize * Wsize.is_wsize
  87. | Coq_is_VPSRLV of Wsize.velem * Wsize.is_velem * Wsize.wsize * Wsize.is_wsize
  88. | Coq_is_VPSLLDQ of Wsize.wsize * Wsize.is_wsize
  89. | Coq_is_VPSRLDQ of Wsize.wsize * Wsize.is_wsize
  90. | Coq_is_VPSHUFB of Wsize.wsize * Wsize.is_wsize
  91. | Coq_is_VPSHUFD of Wsize.wsize * Wsize.is_wsize
  92. | Coq_is_VPSHUFHW of Wsize.wsize * Wsize.is_wsize
  93. | Coq_is_VPSHUFLW of Wsize.wsize * Wsize.is_wsize
  94. | Coq_is_VPBLEND of Wsize.velem * Wsize.is_velem * Wsize.wsize * Wsize.is_wsize
  95. | Coq_is_BLENDV of Wsize.velem * Wsize.is_velem * Wsize.wsize * Wsize.is_wsize
  96. | Coq_is_VPACKUS of Wsize.velem * Wsize.is_velem * Wsize.wsize * Wsize.is_wsize
  97. | Coq_is_VPACKSS of Wsize.velem * Wsize.is_velem * Wsize.wsize * Wsize.is_wsize
  98. | Coq_is_VSHUFPS of Wsize.wsize * Wsize.is_wsize
  99. | Coq_is_VPBROADCAST of Wsize.velem * Wsize.is_velem * Wsize.wsize * Wsize.is_wsize
  100. | Coq_is_VMOVSHDUP of Wsize.wsize * Wsize.is_wsize
  101. | Coq_is_VMOVSLDUP of Wsize.wsize * Wsize.is_wsize
  102. | Coq_is_VPALIGNR of Wsize.wsize * Wsize.is_wsize
  103. | Coq_is_VBROADCASTI128
  104. | Coq_is_VPUNPCKH of Wsize.velem * Wsize.is_velem * Wsize.wsize * Wsize.is_wsize
  105. | Coq_is_VPUNPCKL of Wsize.velem * Wsize.is_velem * Wsize.wsize * Wsize.is_wsize
  106. | Coq_is_VEXTRACTI128
  107. | Coq_is_VINSERTI128
  108. | Coq_is_VPERM2I128
  109. | Coq_is_VPERMD
  110. | Coq_is_VPERMQ
  111. | Coq_is_VPMOVMSKB of Wsize.wsize * Wsize.is_wsize * Wsize.wsize * Wsize.is_wsize
  112. | Coq_is_MOVEMASK of Wsize.velem * Wsize.is_velem * Wsize.wsize * Wsize.is_wsize
  113. | Coq_is_VPCMPEQ of Wsize.velem * Wsize.is_velem * Wsize.wsize * Wsize.is_wsize
  114. | Coq_is_VPCMPGT of Wsize.velem * Wsize.is_velem * Wsize.wsize * Wsize.is_wsize
  115. | Coq_is_VPSIGN of Wsize.velem * Wsize.is_velem * Wsize.wsize * Wsize.is_wsize
  116. | Coq_is_VPMADDUBSW of Wsize.wsize * Wsize.is_wsize
  117. | Coq_is_VPMADDWD of Wsize.wsize * Wsize.is_wsize
  118. | Coq_is_VMOVLPD
  119. | Coq_is_VMOVHPD
  120. | Coq_is_VPMINU of Wsize.velem * Wsize.is_velem * Wsize.wsize * Wsize.is_wsize
  121. | Coq_is_VPMINS of Wsize.velem * Wsize.is_velem * Wsize.wsize * Wsize.is_wsize
  122. | Coq_is_VPMAXU of Wsize.velem * Wsize.is_velem * Wsize.wsize * Wsize.is_wsize
  123. | Coq_is_VPMAXS of Wsize.velem * Wsize.is_velem * Wsize.wsize * Wsize.is_wsize
  124. | Coq_is_VPABS of Wsize.velem * Wsize.is_velem * Wsize.wsize * Wsize.is_wsize
  125. | Coq_is_VPTEST of Wsize.wsize * Wsize.is_wsize
  126. | Coq_is_CLFLUSH
  127. | Coq_is_PREFETCHT0
  128. | Coq_is_PREFETCHT1
  129. | Coq_is_PREFETCHT2
  130. | Coq_is_PREFETCHNTA
  131. | Coq_is_LFENCE
  132. | Coq_is_MFENCE
  133. | Coq_is_SFENCE
  134. | Coq_is_RDTSC of Wsize.wsize * Wsize.is_wsize
  135. | Coq_is_RDTSCP of Wsize.wsize * Wsize.is_wsize
  136. | Coq_is_AESDEC
  137. | Coq_is_VAESDEC of Wsize.wsize * Wsize.is_wsize
  138. | Coq_is_AESDECLAST
  139. | Coq_is_VAESDECLAST of Wsize.wsize * Wsize.is_wsize
  140. | Coq_is_AESENC
  141. | Coq_is_VAESENC of Wsize.wsize * Wsize.is_wsize
  142. | Coq_is_AESENCLAST
  143. | Coq_is_VAESENCLAST of Wsize.wsize * Wsize.is_wsize
  144. | Coq_is_AESIMC
  145. | Coq_is_VAESIMC
  146. | Coq_is_AESKEYGENASSIST
  147. | Coq_is_VAESKEYGENASSIST
  148. | Coq_is_PCLMULQDQ
  149. | Coq_is_VPCLMULQDQ of Wsize.wsize * Wsize.is_wsize
  150. | Coq_is_SHA256RNDS2
  151. | Coq_is_SHA256MSG1
  152. | Coq_is_SHA256MSG2
val is_x86_op_rect : (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> 'a1 -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> 'a1 -> 'a1 -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> 'a1 -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.velem -> Wsize.is_velem -> 'a1) -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> 'a1 -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> (Wsize.wsize -> Wsize.is_wsize -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> 'a1 -> 'a1 -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> 'a1 -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> 'a1 -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> 'a1 -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> 'a1 -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> x86_op -> is_x86_op -> 'a1
val is_x86_op_rec : (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> 'a1 -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> 'a1 -> 'a1 -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> 'a1 -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.velem -> Wsize.is_velem -> 'a1) -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> 'a1 -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> (Wsize.wsize -> Wsize.is_wsize -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> 'a1 -> 'a1 -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> 'a1 -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> 'a1 -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> 'a1 -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> 'a1 -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> x86_op -> is_x86_op -> 'a1
val x86_op_tag : x86_op -> BinNums.positive
val is_x86_op_inhab : x86_op -> is_x86_op
val is_x86_op_functor : x86_op -> is_x86_op -> is_x86_op
type box_x86_op_MOV = Wsize.wsize
val coq_Box_x86_op_MOV_0 : box_x86_op_MOV -> Wsize.wsize
type box_x86_op_MOVSX = {
  1. coq_Box_x86_op_MOVSX_0 : Wsize.wsize;
  2. coq_Box_x86_op_MOVSX_1 : Wsize.wsize;
}
val coq_Box_x86_op_MOVSX_0 : box_x86_op_MOVSX -> Wsize.wsize
val coq_Box_x86_op_MOVSX_1 : box_x86_op_MOVSX -> Wsize.wsize
type box_x86_op_SETcc =
  1. | Box_x86_op_SETcc
type box_x86_op_PADD = {
  1. coq_Box_x86_op_PADD_0 : Wsize.velem;
  2. coq_Box_x86_op_PADD_1 : Wsize.wsize;
}
val coq_Box_x86_op_PADD_0 : box_x86_op_PADD -> Wsize.velem
val coq_Box_x86_op_PADD_1 : box_x86_op_PADD -> Wsize.wsize
type box_x86_op_VPMOVSX = {
  1. coq_Box_x86_op_VPMOVSX_0 : Wsize.velem;
  2. coq_Box_x86_op_VPMOVSX_1 : Wsize.wsize;
  3. coq_Box_x86_op_VPMOVSX_2 : Wsize.velem;
  4. coq_Box_x86_op_VPMOVSX_3 : Wsize.wsize;
}
val coq_Box_x86_op_VPMOVSX_0 : box_x86_op_VPMOVSX -> Wsize.velem
val coq_Box_x86_op_VPMOVSX_1 : box_x86_op_VPMOVSX -> Wsize.wsize
val coq_Box_x86_op_VPMOVSX_2 : box_x86_op_VPMOVSX -> Wsize.velem
val coq_Box_x86_op_VPMOVSX_3 : box_x86_op_VPMOVSX -> Wsize.wsize
type box_x86_op_VPINSR = Wsize.velem
val coq_Box_x86_op_VPINSR_0 : box_x86_op_VPINSR -> Wsize.velem
type x86_op_fields_t = __
val x86_op_fields : x86_op -> x86_op_fields_t
val x86_op_construct : BinNums.positive -> x86_op_fields_t -> x86_op option
val x86_op_induction : (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> 'a1 -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> 'a1 -> 'a1 -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> 'a1 -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.velem -> Wsize.is_velem -> 'a1) -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> 'a1 -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> (Wsize.wsize -> Wsize.is_wsize -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> 'a1 -> 'a1 -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.velem -> Wsize.is_velem -> Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> 'a1 -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> 'a1 -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> 'a1 -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> 'a1 -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> 'a1 -> (Wsize.wsize -> Wsize.is_wsize -> 'a1) -> 'a1 -> 'a1 -> 'a1 -> x86_op -> is_x86_op -> 'a1
val x86_op_eqb_fields : (x86_op -> x86_op -> bool) -> BinNums.positive -> x86_op_fields_t -> x86_op_fields_t -> bool
val x86_op_eqb : x86_op -> x86_op -> bool
val x86_op_eqb_OK : x86_op -> x86_op -> Bool.reflect
val x86_op_eqb_OK_sumbool : x86_op -> x86_op -> bool
val coq_HB_unnamed_factory_1 : x86_op Eqtype.Coq_hasDecEq.axioms_
val x86_instr_decl_x86_op__canonical__eqtype_Equality : Eqtype.Equality.coq_type
val b_ty : Type.stype list
val b4_ty : Type.stype list
val b5_ty : Type.stype list
val bw_ty : Wsize.wsize -> Type.stype list
val bw2_ty : Wsize.wsize -> Type.stype list
val b2w_ty : Wsize.wsize -> Type.stype list
val b4w_ty : Wsize.wsize -> Type.stype list
val b5w_ty : Wsize.wsize -> Type.stype list
val b5w2_ty : Wsize.wsize -> Type.stype list
val w_ty : Wsize.wsize -> Type.stype list
val w2_ty : Wsize.wsize -> Wsize.wsize -> Type.stype list
val w3_ty : Wsize.wsize -> Type.stype list
val w8_ty : Type.stype list
val w128_ty : Type.stype list
val w256_ty : Type.stype list
val w2b_ty : Wsize.wsize -> Wsize.wsize -> Type.stype list
val ww8_ty : Wsize.wsize -> Type.stype list
val ww8b_ty : Wsize.wsize -> Type.stype list
val w2w8_ty : Wsize.wsize -> Type.stype list
val w128w8_ty : Type.stype list
val w128ww8_ty : Wsize.wsize -> Type.stype list
val w256w8_ty : Type.stype list
val w256w128w8_ty : Type.stype list
val w256x2w8_ty : Type.stype list
val coq_SF_of_word : Wsize.wsize -> Ssralg.GRing.ComRing.sort -> bool
val coq_PF_of_word : Wsize.wsize -> Ssralg.GRing.ComRing.sort -> bool
val coq_ZF_of_word : Wsize.wsize -> Ssralg.GRing.ComRing.sort -> bool
val rflags_of_mul : bool -> Sem_type.sem_tuple
val rflags_of_div : Sem_type.sem_tuple
val prim_8_64 : (Wsize.wsize -> 'a1) -> 'a1 Sopn.prim_constructor
val prim_16_64 : (Wsize.wsize -> 'a1) -> 'a1 Sopn.prim_constructor
val prim_32_64 : (Wsize.wsize -> 'a1) -> 'a1 Sopn.prim_constructor
val prim_128_256 : (Wsize.wsize -> 'a1) -> 'a1 Sopn.prim_constructor
val reg_msb_flag : Wsize.wsize -> Arch_decl.msb_flag
val max_32 : Wsize.wsize -> Wsize.wsize
val c : Arch_decl.arg_kind list
val r : Arch_decl.arg_kind list
val rx : Arch_decl.arg_kind list
val m : bool -> Arch_decl.arg_kind list
val rm : bool -> Arch_decl.arg_kind list
val rxm : bool -> Arch_decl.arg_kind list
val m_r : Arch_decl.arg_kind list list
val r_rm_false : Arch_decl.arg_kind list list
val r_rm : Arch_decl.arg_kind list list
val r_rmi : Wsize.wsize -> Arch_decl.arg_kind list list
val m_ri : Wsize.wsize -> Arch_decl.arg_kind list list
val xmm : Arch_decl.arg_kind list
val xmmm : bool -> Arch_decl.arg_kind list
val xmmmi : Wsize.wsize -> Arch_decl.arg_kind list
val xmm_xmmm : Arch_decl.arg_kind list list
val xmmm_xmm : Arch_decl.arg_kind list list
val xmm_xmm_xmmm : Arch_decl.arg_kind list list
val xmm_xmm_xmmmi : Wsize.wsize -> Arch_decl.arg_kind list list
val check_mov : Wsize.wsize -> Arch_decl.arg_kind list list list
val check_movx : Wsize.wsize -> Arch_decl.arg_kind list list list
val check_por : Arch_decl.i_args_kinds
val check_padd : Arch_decl.i_args_kinds
val check_movsx : Wsize.wsize -> Wsize.wsize -> Arch_decl.arg_kind list list list
val size_MOVSX : Wsize.wsize -> Wsize.wsize -> bool
val size_MOVZX : Wsize.wsize -> Wsize.wsize -> bool
val check_xchg : Arch_decl.arg_kind list list list
val c_r_rm : Arch_decl.arg_kind list list
val check_add : Wsize.wsize -> Arch_decl.arg_kind list list list
val check_mul : Wsize.wsize -> Arch_decl.arg_kind list list list
val check_adcx : Wsize.wsize -> Arch_decl.arg_kind list list list
val check_mulx : Arch_decl.arg_kind list list list
val check_neg : Wsize.wsize -> Arch_decl.arg_kind list list list
val check_setcc : Arch_decl.arg_kind list list list
val x86_SETcc : bool -> Sem_type.sem_tuple
val check_bt : Wsize.wsize -> Arch_decl.arg_kind list list list
val x86_CLC : Sem_type.sem_tuple
val x86_STC : Sem_type.sem_tuple
val check_lea : Wsize.wsize -> Arch_decl.arg_kind list list list
val check_test : Wsize.wsize -> Arch_decl.arg_kind list list list
val check_cmp : Wsize.wsize -> Arch_decl.arg_kind list list list
val check_andn : Wsize.wsize -> Arch_decl.arg_kind list list list
val check_ror : Wsize.wsize -> Arch_decl.arg_kind list list list
val x86_shift_mask : Wsize.wsize -> Ssralg.GRing.ComRing.sort
val check_shld : Wsize.wsize -> Arch_decl.arg_kind list list list
val safe_shxd : Wsize.wsize -> Wsize.safe_cond list
val check_rorx : Wsize.wsize -> Arch_decl.arg_kind list list list
val check_sarx : Wsize.wsize -> Arch_decl.arg_kind list list list
val check_movd : Wsize.wsize -> Arch_decl.arg_kind list list list
val check_vmovdq : Wsize.wsize -> Arch_decl.arg_kind list list list
val vector_size : Wsize.velem -> Wsize.wsize -> BinNums.coq_Z option
val check_vector_length : Wsize.velem -> Wsize.wsize -> Wsize.velem -> Wsize.wsize -> bool
val check_xmm_xmm_xmmm : Wsize.wsize -> Arch_decl.arg_kind list list list
val check_vpextr : Wsize.wsize -> Arch_decl.arg_kind list list list
val check_vpinsr : Wsize.wsize -> Arch_decl.arg_kind list list list
val check_xmm_xmm_imm8 : Wsize.wsize -> Arch_decl.arg_kind list list list
val check_xmm_xmm_xmmmi : Wsize.wsize -> Arch_decl.arg_kind list list list
val check_xmm_xmmm_imm8 : Wsize.wsize -> Arch_decl.arg_kind list list list
val check_xmm_xmm_xmmm_imm8 : Wsize.wsize -> Arch_decl.arg_kind list list list
val check_xmm_xmm_xmmm_xmm : Wsize.wsize -> Arch_decl.arg_kind list list list
val coq_SaturatedSignedToUnsigned : Wsize.wsize -> Wsize.wsize -> Ssralg.GRing.ComRing.sort -> Ssralg.GRing.ComRing.sort
val check_xmm_xmmm : Wsize.wsize -> Arch_decl.arg_kind list list list
val check_xmmm_xmm_imm8 : Wsize.wsize -> Arch_decl.arg_kind list list list
val check_movpd : Arch_decl.arg_kind list list list
val check_vptest : Wsize.wsize -> Arch_decl.arg_kind list list list
val x86_prim_string : (string * x86_op Sopn.prim_constructor) list
val eqC_x86_op : x86_op Utils0.eqTypeC