Module Hax_engine.Concrete_ident_generated

type t =
  1. | Hax_lib__int__Impl_5___unsafe_from_str
  2. | Alloc__slice__Impl__T
  3. | Core__ops__arith__Sub__Output
  4. | Core__ptr__const_ptr__Impl
  5. | Core__borrow__Impl_2__'_
  6. | Core__panicking__assert_failed__'_
  7. | Core__array__iter__Impl__T
  8. | Core__marker__Copy
  9. | Rust_primitives__hax__array_of_list
  10. | Hax_lib_protocol__crypto__hash__'_
  11. | Rust_primitives__dummy_hax_concrete_ident_wrapper____1
  12. | Core__ops__range__RangeFrom
  13. | Core__iter__traits__iterator__Iterator__enumerate
  14. | Core__slice__Impl__len__'_
  15. | Core__ops__index__IndexMut__index_mut
  16. | Rust_primitives__hax__control_flow_monad__ControlFlowMonad
  17. | Hax_lib__Refinement__get
  18. | Hax_lib_protocol__crypto__Impl
  19. | Rust_primitives__dummy_hax_concrete_ident_wrapper____1__f
  20. | Rust_primitives__unsize
  21. | Hax_lib_protocol__crypto__aead_encrypt__'__1
  22. | Hax_lib_protocol__crypto__AEADTag
  23. | Hax_lib_protocol__crypto__Impl_4__from_bytes
  24. | Core__iter__traits__iterator__Iterator
  25. | Rust_primitives__dummy_hax_concrete_ident_wrapper_____arith__X
  26. | Core__result__Result
  27. | Core__ops__index__Index__index
  28. | Rust_primitives__crypto_abstractions__Use
  29. | Core__option__Impl__is_some__'_
  30. | Hax_lib_protocol__crypto__Impl_1__from_bytes__'_
  31. | Hax_lib_protocol__crypto__DHScalar
  32. | Core__ops__try_trait__Try__branch
  33. | Rust_primitives__crypto_abstractions
  34. | Rust_primitives__dummy_hax_concrete_ident_wrapper__refinements__U
  35. | Core__ops__arith__Mul__mul
  36. | Rust_primitives__hax__Failure
  37. | Rust_primitives__dummy_hax_concrete_ident_wrapper____1__f__T
  38. | Std__
  39. | Hax_lib_protocol__crypto__Impl_1__from_bytes
  40. | Hax_lib__int__Impl_29
  41. | Rust_primitives__u128__eq
  42. | Core__ops__try_trait__Try__Output
  43. | Core__cmp__PartialOrd__gt__'__1
  44. | Rust_primitives__hax__control_flow_monad
  45. | Hax_lib_protocol__crypto__Impl_4
  46. | Rust_primitives__hax__folds__fold_enumerated_slice
  47. | Rust_primitives__hax__never_to_any
  48. | Hax_lib_protocol__crypto__Impl__from_bytes__'_
  49. | Core__array__iter__Impl
  50. | Core__ops__range__RangeFrom__start
  51. | Core__num__Impl_9__to_le_bytes
  52. | Core__option__Impl
  53. | Alloc__vec__Impl_11__A
  54. | Core__result__Impl_27__E
  55. | Hax_lib_protocol__crypto__AEADKey
  56. | Rust_primitives__u128__sub
  57. | Hax_lib_protocol__crypto__Impl_9
  58. | Alloc__string__String
  59. | Core__ops__arith__Rem
  60. | Core__ops__bit__Shl__Output
  61. | Core__ops
  62. | Core__ops__arith__Mul
  63. | Rust_primitives__u128__shr
  64. | Core__macros__builtin__assert
  65. | Rust_primitives__hax__monomorphized_update_at
  66. | Core__result__Impl__E
  67. | Core__result__Impl_26__E
  68. | Core__ops__range__Range__start
  69. | Alloc__slice__Impl__to_vec
  70. | Hax_lib__int__Impl_7
  71. | Hax_lib__Refinement
  72. | Rust_primitives__hax__monomorphized_update_at__update_at_usize
  73. | Hax_lib__Refinement__InnerType
  74. | Core__ops__bit__Shr__Output
  75. | Hax_lib__
  76. | Rust_primitives__u128__shl
  77. | Rust_primitives__hax__int__div
  78. | Core__marker__Sized
  79. | Hax_lib__Refinement__get_mut
  80. | Rust_primitives__hax__folds__fold_range
  81. | Core__ops__arith__Div
  82. | Core__ops__arith__Neg__Output
  83. | Rust_primitives__hax__while_loop
  84. | Core__slice__index__Impl_2
  85. | Alloc__vec__from_elem
  86. | Core__slice__Impl
  87. | Core__ops__bit__Shr__shr
  88. | Core__num__Impl_9
  89. | Core__ops__control_flow__ControlFlow__Continue__0
  90. | Core__result__Impl__T
  91. | Alloc__vec__Impl_14__T
  92. | Hax_lib_protocol__crypto__dh_scalar_multiply
  93. | Core__iter__adapters__step_by__StepBy
  94. | Std__prelude__rust_2021
  95. | Core__ops__control_flow__ControlFlow__Break__0
  96. | Alloc__vec__Impl_1__A
  97. | Core__result__Impl_26__T
  98. | Core__str__Impl__as_ptr__'_
  99. | Core__cmp__PartialOrd__le__'_
  100. | Core__ops__bit__BitAnd__bitand
  101. | Core__ops__arith__Neg__neg
  102. | Core__ops__bit__BitXor__bitxor
  103. | Rust_primitives__dummy_hax_concrete_ident_wrapper__question_mark_result__A
  104. | Core__cmp__PartialOrd
  105. | Alloc__vec__Impl_2__extend_from_slice__'__1
  106. | Rust_primitives__hax__box_new
  107. | Core__ops__control_flow__ControlFlow__Break
  108. | Core__ops__bit__BitXor
  109. | Core__ops__bit__BitXor__Output
  110. | Core__ops__bit__BitOr__Output
  111. | Core__ops__deref__DerefMut
  112. | Hax_lib_protocol__crypto__hmac
  113. | Hax_lib_protocol__crypto__Impl_5__from_bytes
  114. | Rust_primitives__hax__int__mul
  115. | Hax_lib_protocol__crypto__dh_scalar_multiply_base
  116. | Rust_primitives__hax__int__ne
  117. | Rust_primitives__hax__control_flow_monad__ControlFlowMonad__lift
  118. | Hax_lib__int__Impl_5__pow2
  119. | Core__slice__Impl__chunks_exact
  120. | Rust_primitives__u128__div
  121. | Core__convert__Impl_3__U
  122. | Rust_primitives__offset
  123. | Core__convert__From__from
  124. | Core__ops__range__RangeTo
  125. | Core__clone__Clone
  126. | Rust_primitives__hax__dropped_body
  127. | Hax_lib__inline
  128. | Rust_primitives__dummy_hax_concrete_ident_wrapper__refinements__T
  129. | Hax_lib_protocol__crypto__Impl_6
  130. | Rust_primitives__dummy_hax_concrete_ident_wrapper_____arith
  131. | Rust_primitives__u128__add
  132. | Rust_primitives__dummy_hax_concrete_ident_wrapper___
  133. | Alloc__alloc__Impl_3
  134. | Core__option__Impl__is_some
  135. | Hax_lib__int__Impl_5___unsafe_from_str__'_
  136. | Core__ops__arith__Mul__Output
  137. | Hax_lib__int__Impl_5
  138. | Alloc__vec__Impl_1__truncate
  139. | Rust_primitives__dummy_hax_concrete_ident_wrapper__I
  140. | Rust_primitives__u128__mul
  141. | Core__slice__Impl__iter__'_
  142. | Core__ops__arith__Neg
  143. | Hax_lib_protocol__
  144. | Core__cmp__PartialOrd__lt__'__1
  145. | Rust_primitives__dummy_hax_concrete_ident_wrapper_____Use
  146. | Core__ops__arith__Div__div
  147. | Core__ops__range__RangeTo__end
  148. | Alloc__vec__Impl_13__T
  149. | Hax_lib__inline_unsafe
  150. | Std__prelude
  151. | Core__convert__From
  152. | Rust_primitives__hax__int__eq
  153. | Rust_primitives__hax__int__ge
  154. | Rust_primitives__dummy_hax_concrete_ident_wrapper__Use
  155. | Rust_primitives__alloc
  156. | Rust_primitives__dummy_hax_concrete_ident_wrapper__Use_3
  157. | Core__ops__arith__Sub__sub
  158. | Core__iter__traits__collect__IntoIterator
  159. | Hax_lib__RefineAs__into_checked
  160. | Rust_primitives__u128__bit_and
  161. | Core__fmt__Debug
  162. | Core__ops__deref__DerefMut__deref_mut__'_
  163. | Core__ops__try_trait__Try
  164. | Rust_primitives__hax__int__from_machine
  165. | Alloc__vec__Impl_11
  166. | Rust_primitives__dummy_hax_concrete_ident_wrapper_____Use_2
  167. | Hax_lib_protocol__crypto__hmac__'__1
  168. | Core__ops__index__Index__index__'_
  169. | Core__ops__index__Index__Output
  170. | Rust_primitives__dummy_hax_concrete_ident_wrapper____1__Use
  171. | Core__option__Option__Some
  172. | Rust_primitives__dummy_hax_concrete_ident_wrapper__refinements
  173. | Core__cmp__PartialOrd__le__'__1
  174. | Core__alloc__Allocator
  175. | Rust_primitives__dummy_hax_concrete_ident_wrapper__dummy
  176. | Rust_primitives__hax__folds__fold_enumerated_chunked_slice
  177. | Core__iter__traits__iterator__Iterator__step_by
  178. | Core__result__Impl_27__F
  179. | Core__convert__Impl_3
  180. | Alloc__vec__Impl_2__extend_from_slice__'_
  181. | Rust_primitives__u128__gt
  182. | Core__borrow__Impl_2
  183. | Core__cmp__PartialEq
  184. | Alloc__vec__Impl_8
  185. | Core__result__Result__Err__0
  186. | Rust_primitives__hax__repeat
  187. | Rust_primitives__dummy_hax_concrete_ident_wrapper__question_mark_result
  188. | Hax_lib_protocol__crypto__Impl_4__from_bytes__'_
  189. | Core__iter__traits__iterator__Iterator__fold
  190. | Core__iter__traits__iterator__Iterator__next__'_
  191. | Hax_lib__RefineAs
  192. | Alloc__slice__Impl_2
  193. | Rust_primitives__dummy_hax_concrete_ident_wrapper__Use_2
  194. | Hax_lib__Refinement__get_mut__'_
  195. | Core__fmt__num__Impl_80
  196. | Core__ops__deref__Deref__deref
  197. | Core__result__Result__Ok__0
  198. | Core__option__Option__None
  199. | Rust_primitives__dummy_hax_concrete_ident_wrapper__question_mark_result__B
  200. | Rust_primitives__hax__failure
  201. | Core__cmp
  202. | Core__cmp__PartialOrd__ge__'_
  203. | Rust_primitives__u128
  204. | Core__array__iter__Impl__N
  205. | Core__slice__iter__ChunksExact
  206. | Rust_primitives__hax__int__rem
  207. | Alloc__slice__Concat__Output
  208. | Core__panicking__AssertKind
  209. | Alloc__vec__Impl_13
  210. | Core__
  211. | Rust_primitives__hax__Never
  212. | Rust_primitives__u128__ge
  213. | Core__slice__index__Impl_2__T
  214. | Rust_primitives__u128__le
  215. | Alloc__slice__Impl__concat
  216. | Alloc__vec__Impl_1
  217. | Core__borrow__Impl_2__T
  218. | Rust_primitives__u128__bit_or
  219. | Core__result__Impl__map_err
  220. | Hax_lib__Refinement__new
  221. | Hax_lib_protocol__crypto__aead_encrypt__'_
  222. | Core__ops__index__Index
  223. | Core__cmp__PartialEq__ne__'__1
  224. | Core__convert__Impl_3__T
  225. | Core__clone__Clone__clone
  226. | Hax_lib__assert
  227. | Core__cmp__PartialOrd__lt__'_
  228. | Rust_primitives__hax
  229. | Hax_lib_protocol__crypto__aead_encrypt
  230. | Core__ops__control_flow__ControlFlow__Continue
  231. | Rust_primitives__hax__int__le
  232. | Core__iter__traits__collect__IntoIterator__into_iter
  233. | Core__slice__Impl__iter
  234. | Core__result__Impl_26
  235. | Alloc__vec__Impl_2__T
  236. | Core__convert__num__Impl_64
  237. | Core__cmp__PartialOrd__gt__'_
  238. | Core__option__Option
  239. | Core__ops__bit__Not__Output
  240. | Rust_primitives__u128__bit_xor
  241. | Alloc__vec__Impl_1__T
  242. | Alloc__boxed__Box
  243. | Core__cmp__PartialOrd__le
  244. | Rust_primitives__dummy_hax_concrete_ident_wrapper__iterator_functions
  245. | Core__slice__index__Impl_4__T
  246. | Core__ops__function__FnMut
  247. | Rust_primitives__hax__int__lt
  248. | Core__panicking__panic
  249. | Hax_lib_protocol__crypto__Impl_5__from_bytes__'_
  250. | Hax_lib__int__Concretization
  251. | Core__slice__Impl__chunks_exact__'_
  252. | Alloc__vec__Vec
  253. | Core__ops__range__Range
  254. | Core__result__Impl
  255. | Alloc__slice__Impl__concat__'_
  256. | Hax_lib__int
  257. | Core__cmp__PartialOrd__lt
  258. | Core__cmp__PartialOrd__ge__'__1
  259. | Rust_primitives__Use
  260. | Alloc__slice__Concat
  261. | Rust_primitives__dummy_hax_concrete_ident_wrapper__Use_4
  262. | Core__ops__deref__Deref__Target
  263. | Hax_lib_protocol__crypto__HMACAlgorithm
  264. | Core__ops__deref__DerefMut__deref_mut
  265. | Core__ops__arith__Rem__rem
  266. | Rust_primitives__dummy_hax_concrete_ident_wrapper
  267. | Rust_primitives__dummy_hax_concrete_ident_wrapper__iterator_functions__It
  268. | Rust_primitives__u128__lt
  269. | Core__slice__Impl__T
  270. | Alloc__alloc__Impl_1
  271. | Core__ops__arith__Add__add
  272. | Hax_lib___internal_loop_invariant
  273. | Core__slice__iter__Iter
  274. | Core__iter__traits__iterator__Iterator__next
  275. | Hax_lib_protocol__crypto
  276. | Rust_primitives__hax__control_flow_monad__mresult__run
  277. | Alloc__vec__Impl_11__T
  278. | Core__fmt__Arguments
  279. | Hax_lib_protocol__crypto__AEADAlgorithm
  280. | Hax_lib_protocol__crypto__hmac__'_
  281. | Hax_lib__int__Int
  282. | Core__convert__Into__into
  283. | Alloc__slice__Impl__into_vec
  284. | Hax_lib__int__Concretization__concretize
  285. | Core__iter__traits__iterator__Iterator__Item
  286. | Hax_lib__inline__'_
  287. | Core__ops__arith__Rem__Output
  288. | Alloc__vec__Impl_14__I
  289. | Core__ops__deref__Deref
  290. | Hax_lib_protocol__crypto__Impl_6__from_bytes
  291. | Core__ptr__const_ptr__Impl__T
  292. | Core__array__iter__IntoIter
  293. | Rust_primitives__hax__control_flow_monad__moption__run
  294. | Hax_lib__inline_unsafe__'_
  295. | Core__slice__Impl__len
  296. | Core__ops__arith__Sub
  297. | Core__macros__assert_eq
  298. | Rust_primitives__impl_arith
  299. | Core__panicking__AssertKind__Eq
  300. | Rust_primitives__u128__ne
  301. | Alloc__vec__Impl_1__truncate__'_
  302. | Core__ops__try_trait__FromResidual__from_residual
  303. | Hax_lib_protocol__crypto__hash
  304. | Core__convert__Infallible
  305. | Alloc__boxed__Impl__new
  306. | Hax_lib_protocol__crypto__Impl__from_bytes
  307. | Core__cmp__PartialEq__ne__'_
  308. | Core__iter__traits__collect__IntoIterator__IntoIter
  309. | Alloc__boxed__Impl__T
  310. | Hax_lib__int__Abstraction__AbstractType
  311. | Hax_lib_protocol__ProtocolError
  312. | Rust_primitives__hax__Failure__Ctor
  313. | Rust_primitives__hax__monomorphized_update_at__update_at_range_from
  314. | Core__clone__Clone__clone__'_
  315. | Core__ops__bit__Not
  316. | Core__borrow__Borrow
  317. | Hax_lib_protocol__crypto__HashAlgorithm__Sha256
  318. | Core__ops__bit__BitOr__bitor
  319. | Alloc__vec__Impl_8__T
  320. | Hax_lib__int__Abstraction
  321. | Alloc__macros__vec
  322. | Core__convert__Into
  323. | Core__panicking__assert_failed__'__1
  324. | Core__cmp__PartialEq__eq
  325. | Core__slice__index__Impl_4
  326. | Core__ops__bit__Shl
  327. | Rust_primitives__u128__rem
  328. | Alloc__vec__Impl_14
  329. | Hax_lib_protocol__crypto__Impl_6__from_bytes__'_
  330. | Rust_primitives__hax__int__add
  331. | Core__ops__bit__Shr
  332. | Rust_primitives__hax__int__into_machine
  333. | Core__cmp__PartialEq__ne
  334. | Rust_primitives__dummy_hax_concrete_ident_wrapper__dummy__T
  335. | Alloc__vec__Impl_8__A
  336. | Rust_primitives__hax__folds__fold_range_step_by
  337. | Core__ops__function__FnOnce
  338. | Alloc__vec__Impl_14__A
  339. | Core__ops__arith__Add
  340. | Core__slice__index__SliceIndex
  341. | Rust_primitives__hax__int__gt
  342. | Core__result__Impl_27
  343. | Hax_lib_protocol__crypto__aead_decrypt
  344. | Core__option__Option__Some__0
  345. | Hax_lib__int__Impl_13
  346. | Core__ops__bit__BitOr
  347. | Hax_lib_protocol__crypto__DHGroup
  348. | Core__ops__bit__Not__not
  349. | Core__ops__index__IndexMut
  350. | Core__panicking__assert_failed
  351. | Core__ops__try_trait__Try__from_output
  352. | Core__ops__index__IndexMut__index_mut__'_
  353. | Hax_lib_protocol__crypto__aead_decrypt__'__1
  354. | Rust_primitives__hax__monomorphized_update_at__update_at_range_full
  355. | Core__ops__bit__Shl__shl
  356. | Core__result__Result__Err
  357. | Core__ops__arith__Add__Output
  358. | Rust_primitives__hax__folds
  359. | Alloc__vec__Impl_13__I
  360. | Rust_primitives__std
  361. | Core__iter__adapters__enumerate__Enumerate
  362. | Core__cmp__PartialEq__eq__'__1
  363. | Alloc__vec__Impl_2__A
  364. | Alloc__vec__Impl_13__A
  365. | Alloc__boxed__Impl
  366. | Core__ops__try_trait__Try__Residual
  367. | Core__str__Impl__as_ptr
  368. | Core__cmp__PartialOrd__ge
  369. | Alloc__alloc__Global
  370. | Alloc__vec__Impl_2
  371. | Rust_primitives__hax__control_flow_monad__moption
  372. | Core__ops__control_flow__ControlFlow
  373. | Core__ops__arith__Div__Output
  374. | Rust_primitives__crypto_abstractions__crypto_abstractions
  375. | Hax_lib_protocol__crypto__DHGroup__X25519
  376. | Hax_lib_protocol__crypto__DHElement
  377. | Rust_primitives__
  378. | Hax_lib_protocol__crypto__Impl_1
  379. | Hax_lib_protocol__crypto__Impl_5
  380. | Core__ops__deref__Deref__deref__'_
  381. | Alloc__vec__Impl_2__extend_from_slice
  382. | Core__option__Impl__T
  383. | Hax_lib__int__Abstraction__lift
  384. | Core__str__Impl
  385. | Rust_primitives__dummy_hax_concrete_ident_wrapper__Use_1
  386. | Alloc__slice__Impl_2__V
  387. | Rust_primitives__hax__control_flow_monad__mexception
  388. | Core__ops__range__RangeFull
  389. | Hax_lib_protocol__crypto__HMACAlgorithm__Sha256
  390. | Core__ptr__const_ptr__Impl__offset
  391. | Rust_primitives__hax__monomorphized_update_at__update_at_range_to
  392. | Rust_primitives__hax__update_at
  393. | Alloc__slice__Impl_2__T
  394. | Rust_primitives__hax__monomorphized_update_at__update_at_range
  395. | Core__clone__impls__Impl_6
  396. | Core__ops__range__Range__end
  397. | Rust_primitives__hax__control_flow_monad__mexception__run
  398. | Core__convert__num__Impl_88
  399. | Core__ops__bit__BitAnd
  400. | Core__result__Impl_27__T
  401. | Rust_primitives__dummy_hax_concrete_ident_wrapper_____Use_1
  402. | Hax_lib_protocol__crypto__AEADAlgorithm__Chacha20Poly1305
  403. | Core__ops__try_trait__FromResidual
  404. | Core__cmp__PartialOrd__gt
  405. | Rust_primitives__hax__MutRef
  406. | Hax_lib_protocol__crypto__aead_decrypt__'_
  407. | Rust_primitives__hax__int__sub
  408. | Core__panicking__assert_failed__'__2
  409. | Hax_lib_protocol__crypto__HashAlgorithm
  410. | Hax_lib_protocol__crypto__AEADIV
  411. | Core__result__Result__Ok
  412. | Core__cmp__PartialEq__eq__'_
  413. | Rust_primitives__hax__int
  414. | Alloc__slice__Impl__to_vec__'_
  415. | Rust_primitives__hax__control_flow_monad__mresult
  416. | Alloc__slice__Impl
  417. | Core__ops__bit__BitAnd__Output
val pp : Ppx_deriving_runtime.Format.formatter -> t -> Ppx_deriving_runtime.unit
val show : t -> Ppx_deriving_runtime.string
val equal : t -> t -> Ppx_deriving_runtime.bool
val t_of_yojson : Ppx_yojson_conv_lib.Yojson.Safe.t -> t
val yojson_of_t : t -> Ppx_yojson_conv_lib.Yojson.Safe.t
val compare : t -> t -> int
val t_of_sexp : Sexplib0.Sexp.t -> t
val sexp_of_t : t -> Sexplib0.Sexp.t
val hash_fold_t : Ppx_hash_lib.Std.Hash.state -> t -> Ppx_hash_lib.Std.Hash.state
val hash : t -> Ppx_hash_lib.Std.Hash.hash_value
include sig ... end
type comparable_t = t
type comparator_witness
val comparator : (comparable_t, comparator_witness) Base__Comparator.comparator
module Values : sig ... end
val def_id_of : t -> Types.def_id
val impl_infos_json_list : Yojson.Safe.t list
val impl_infos : (Types.def_id * Types.impl_infos) Base.List.t