Module Hax_engine.Concrete_ident_generated

type t =
  1. | Core__ops__range__RangeTo
  2. | Rust_primitives__isize__ne
  3. | Rust_primitives__hax__int__into_machine
  4. | Rust_primitives__isize__bit_and
  5. | Rust_primitives__u128__mul
  6. | Core__result__Result__Err
  7. | Core__ops__function
  8. | Hax_lib__prop__ToProp
  9. | Alloc__alloc__Impl_1
  10. | Core__ops__bit__BitOr__bitor
  11. | Rust_primitives__u32__ge
  12. | Core__ops__deref__DerefMut__deref_mut__'_
  13. | Rust_primitives__i8__eq
  14. | Rust_primitives__i16__mul
  15. | Alloc__vec__Impl_11__T
  16. | Core__ops__arith__Mul__Output
  17. | Rust_primitives__u16__shl
  18. | Rust_primitives__u32__bit_xor
  19. | Core__slice__Impl__T
  20. | Rust_primitives__i128__eq
  21. | Rust_primitives__u8__le
  22. | Rust_primitives__hax__monomorphized_update_at
  23. | Rust_primitives__hax__folds__fold_enumerated_slice_cf
  24. | Rust_primitives__hax__dropped_body
  25. | Alloc__slice__Impl__T
  26. | Core__array__iter__Impl__T
  27. | Hax_lib__abstraction
  28. | Hax_lib_protocol__crypto__HMACAlgorithm__Sha256
  29. | Core__cmp__PartialEq__eq
  30. | Rust_primitives__u8__add
  31. | Rust_primitives__i128__neg
  32. | Rust_primitives__hax__int__gt
  33. | Rust_primitives__hax__box_new
  34. | Hax_lib_protocol__crypto__DHScalar
  35. | Rust_primitives__i128__shl
  36. | Hax_lib__prop__forall
  37. | Core__slice__Impl__iter
  38. | Rust_primitives__dummy_hax_concrete_ident_wrapper__refinements
  39. | Rust_primitives__isize__eq
  40. | Rust_primitives__hax__int__lt
  41. | Core__alloc
  42. | Hax_lib_protocol
  43. | Hax_lib_protocol__crypto__HashAlgorithm__Sha256
  44. | Core__option__Option
  45. | Alloc__string
  46. | Hax_lib__prop__constructors__and
  47. | Rust_primitives__u64__le
  48. | Rust_primitives__u64__ge
  49. | Alloc__slice__Impl__concat__'_
  50. | Alloc__slice__Impl_2__T
  51. | Alloc__vec__Impl_14__A
  52. | Rust_primitives__dummy_hax_concrete_ident_wrapper__Use
  53. | Rust_primitives__dummy_hax_concrete_ident_wrapper__props
  54. | Rust_primitives__u8__bit_xor
  55. | Core__ptr__const_ptr__Impl
  56. | Core__ops__bit__BitXor__Output
  57. | Rust_primitives__hax__folds__fold_cf
  58. | Hax_lib_protocol__crypto__Impl_5__from_bytes__'_
  59. | Rust_primitives__i32__rem
  60. | Rust_primitives__isize__neg
  61. | Rust_primitives__hax__control_flow_monad__moption
  62. | Rust_primitives__isize__bit_xor
  63. | Hax_lib_protocol__crypto__hmac
  64. | Hax_lib__prop__constructors__ne
  65. | Rust_primitives__u128__ne
  66. | Rust_primitives__u64__shl
  67. | Core__result__Impl_28__F
  68. | Hax_lib_protocol__crypto__Impl_5__from_bytes
  69. | Hax_lib_protocol__crypto__Impl_6__from_bytes__'_
  70. | Rust_primitives__hax__folds__fold_enumerated_chunked_slice_cf
  71. | Core__result__Impl_27__T
  72. | Hax_lib_protocol__crypto__Impl_9
  73. | Hax_lib__prop__constructors__not
  74. | Rust_primitives__hax__machine_int__add
  75. | Hax_lib_protocol__crypto__aead_encrypt
  76. | Rust_primitives__dummy_hax_concrete_ident_wrapper_____Use_2
  77. | Rust_primitives__u32__le
  78. | Rust_primitives__u128__add
  79. | Rust_primitives__hax__int__ne
  80. | Core__iter__traits__iterator
  81. | Hax_lib__prop__constructors__or
  82. | Rust_primitives__usize__ne
  83. | Alloc__slice__Concat
  84. | Rust_primitives__hax__machine_int__le
  85. | Alloc__slice__Impl_2
  86. | Rust_primitives__i32__eq
  87. | Rust_primitives__i64__neg
  88. | Hax_lib__any_to_unit
  89. | Rust_primitives__hax__folds__fold_range
  90. | Core__convert__Into__into
  91. | Rust_primitives__i8__shr
  92. | Core__ops__control_flow__ControlFlow__Continue__0
  93. | Rust_primitives__u64
  94. | Alloc__boxed__Impl
  95. | Rust_primitives__isize__le
  96. | Core
  97. | Rust_primitives__i8__lt
  98. | Rust_primitives__i128__mul
  99. | Rust_primitives__hax__int__eq
  100. | Core__cmp__PartialEq__ne
  101. | Rust_primitives__u128__shl
  102. | Hax_lib__prop__exists
  103. | Hax_lib__RefineAs__into_checked
  104. | Rust_primitives__hax__machine_int__ge
  105. | Rust_primitives__i32__div
  106. | Alloc__slice__Impl
  107. | Core__slice__index__Impl_2
  108. | Core__ops__bit__BitXor__bitxor
  109. | Rust_primitives__i16__div
  110. | Core__ops__arith__Div__div
  111. | Rust_primitives__usize__bit_and
  112. | Hax_lib_protocol__crypto__Impl_4
  113. | Core__ops__control_flow__ControlFlow
  114. | Rust_primitives__u64__div
  115. | Core__slice__Impl__len
  116. | Hax_lib__abstraction__Concretization
  117. | Rust_primitives__usize__shl
  118. | Rust_primitives__i8__ne
  119. | Rust_primitives__hax__int
  120. | Rust_primitives__dummy_hax_concrete_ident_wrapper__props__Use
  121. | Rust_primitives__hax__control_flow_monad__moption__run
  122. | Rust_primitives__u16__ne
  123. | Core__clone__Clone__clone__'_
  124. | Alloc__vec__Impl_14
  125. | Core__slice__index
  126. | Hax_lib__prop__Impl_2
  127. | Core__ops__range__Range__end
  128. | Core__panicking__panic
  129. | Rust_primitives__i64__div
  130. | Core__cmp__PartialOrd__lt
  131. | Core__ops__range__RangeTo__end
  132. | Rust_primitives__u32__neg
  133. | Rust_primitives__i8__rem
  134. | Rust_primitives__i64__bit_or
  135. | Rust_primitives__i32__ne
  136. | Core__ops__try_trait__Try__Output
  137. | Core__ops__function__FnMut
  138. | Rust_primitives__u16__bit_and
  139. | Rust_primitives__hax__folds__fold_enumerated_slice
  140. | Rust_primitives__hax__folds__fold_enumerated_slice_return
  141. | Rust_primitives__u32
  142. | Core__ops__try_trait
  143. | Core__ptr__const_ptr__Impl__offset
  144. | Rust_primitives__dummy_hax_concrete_ident_wrapper__props__Closure_2
  145. | Rust_primitives__i16__ne
  146. | Core__str__Impl__as_ptr__'_
  147. | Rust_primitives__u64__eq
  148. | Core__ops__arith__Add__add
  149. | Rust_primitives__hax__monomorphized_update_at__update_at_range_to
  150. | Rust_primitives__hax__machine_int__mul
  151. | Hax_lib_protocol__crypto__DHElement
  152. | Core__fmt
  153. | Rust_primitives__hax__while_loop_return
  154. | Core__array__iter__Impl__N
  155. | Rust_primitives__i128__le
  156. | Rust_primitives__dummy_hax_concrete_ident_wrapper__props__Closure_3
  157. | Core__result__Impl_27__E
  158. | Core__ops__try_trait__FromResidual
  159. | Core__panicking__assert_failed__'__2
  160. | Core__borrow__Impl_2__T
  161. | Core__cmp
  162. | Core__cmp__PartialOrd__gt
  163. | Core__ops__range__RangeFrom
  164. | Core__ops__arith__Rem__rem
  165. | Rust_primitives__u128__bit_and
  166. | Rust_primitives__u128__bit_or
  167. | Rust_primitives__hax__monomorphized_update_at__update_at_range_from
  168. | Rust_primitives__hax__folds__fold_enumerated_chunked_slice
  169. | Rust_primitives__isize__ge
  170. | Core__ops__bit__BitOr
  171. | Alloc__slice__Concat__Output
  172. | Alloc__vec__Impl_2__T
  173. | Rust_primitives__alloc
  174. | Rust_primitives__u16__neg
  175. | Hax_lib_protocol__crypto__Impl_4__from_bytes__'_
  176. | Rust_primitives__u128__bit_xor
  177. | Rust_primitives__isize__rem
  178. | Core__result__Result__Err__0
  179. | Rust_primitives__u32__gt
  180. | Core__convert__From
  181. | Hax_lib_protocol__ProtocolError
  182. | Hax_lib__int__Impl_7
  183. | Core__ops__try_trait__Try__branch
  184. | Hax_lib__inline_unsafe__'_
  185. | Rust_primitives__u8__rem
  186. | Rust_primitives__i64
  187. | Rust_primitives__i64__add
  188. | Alloc__vec__Impl_13__I
  189. | Rust_primitives__i64__bit_xor
  190. | Core__ops__bit__BitAnd__Output
  191. | Rust_primitives__u32__eq
  192. | Alloc__vec__Impl_1__truncate
  193. | Hax_lib_protocol__crypto
  194. | Rust_primitives__u128__div
  195. | Rust_primitives__i32__neg
  196. | Rust_primitives__isize__shl
  197. | Rust_primitives__i16__bit_and
  198. | Core__cmp__PartialOrd__le__'__1
  199. | Rust_primitives__isize__bit_or
  200. | Rust_primitives__usize__gt
  201. | Rust_primitives__u128__neg
  202. | Core__ops__bit__Not
  203. | Hax_lib_protocol__crypto__aead_decrypt__'__1
  204. | Core__panicking__assert_failed__'_
  205. | Core__option__Impl__is_some
  206. | Core__ops__arith__Neg__neg
  207. | Rust_primitives__usize__ge
  208. | Rust_primitives__hax__array_of_list
  209. | Rust_primitives__hax__MutRef
  210. | Core__fmt__num
  211. | Core__ops__try_trait__FromResidual__from_residual
  212. | Rust_primitives__i128__bit_or
  213. | Rust_primitives__usize__bit_or
  214. | Core__iter__traits__collect__IntoIterator__into_iter
  215. | Rust_primitives__std
  216. | Rust_primitives__i8__bit_or
  217. | Alloc__vec__from_elem
  218. | Core__ops__deref__DerefMut
  219. | Rust_primitives__hax__Failure
  220. | Core__array__iter
  221. | Rust_primitives__i64__gt
  222. | Rust_primitives__hax__int__add
  223. | Rust_primitives__hax__int__ge
  224. | Core__marker__Copy
  225. | Rust_primitives__usize__le
  226. | Rust_primitives__i16__ge
  227. | Rust_primitives__hax__never_to_any
  228. | Rust_primitives__hax__while_loop
  229. | Alloc__alloc__Global
  230. | Hax_lib_protocol__crypto__HMACAlgorithm
  231. | Rust_primitives__crypto_abstractions
  232. | Rust_primitives__u16__rem
  233. | Core__slice__index__Impl_4__T
  234. | Core__result__Impl_27
  235. | Core__result__Impl__map_err
  236. | Rust_primitives__u8__bit_or
  237. | Hax_lib__int__Int
  238. | Rust_primitives__u128__le
  239. | Rust_primitives__i64__shr
  240. | Rust_primitives__hax__int__le
  241. | Core__slice__index__Impl_4
  242. | Core__ops__try_trait__Try
  243. | Rust_primitives__u16__bit_xor
  244. | Core__ops__function__FnOnce__Output
  245. | Core__ops__bit
  246. | Rust_primitives__u16__lt
  247. | Rust_primitives__hax__machine_int__eq
  248. | Hax_lib_protocol__crypto__AEADAlgorithm
  249. | Core__ops__index__IndexMut__index_mut__'_
  250. | Core__convert__From__from
  251. | Rust_primitives__usize__neg
  252. | Core__array
  253. | Core__iter__adapters__step_by__StepBy
  254. | Alloc__vec__Impl_13__T
  255. | Hax_lib___internal_loop_decreases
  256. | Hax_lib_protocol__crypto__DHGroup
  257. | Hax_lib__prop__Impl__eq
  258. | Hax_lib__RefineAs
  259. | Core__ops__arith__Div
  260. | Hax_lib__prop__constructors
  261. | Rust_primitives__i32__sub
  262. | Rust_primitives__hax__folds__fold_range_step_by_return
  263. | Rust_primitives__hax__folds__fold_enumerated_chunked_slice_return
  264. | Rust_primitives__u128__gt
  265. | Core__ops__bit__BitAnd
  266. | Core__ops__arith__Mul
  267. | Alloc__string__String
  268. | Core__ops
  269. | Hax_lib__inline
  270. | Alloc__vec__Impl_8__A
  271. | Core__ops__range
  272. | Rust_primitives__u64__add
  273. | Core__iter__traits__iterator__Iterator__next
  274. | Core__result__Impl_28__T
  275. | Core__iter__adapters__enumerate
  276. | Rust_primitives__dummy_hax_concrete_ident_wrapper__Closure
  277. | Rust_primitives__dummy_hax_concrete_ident_wrapper_____Use_1
  278. | Rust_primitives__u16__add
  279. | Core__clone__impls__Impl_6
  280. | Core__ops__index__Index__Output
  281. | Rust_primitives__dummy_hax_concrete_ident_wrapper__Use_1
  282. | Core__ops__deref
  283. | Core__ops__deref__Deref__deref__'_
  284. | Core__ops__arith__Sub__sub
  285. | Rust_primitives__u16
  286. | Core__option__Impl
  287. | Core__convert__num__Impl_64
  288. | Rust_primitives__hax
  289. | Rust_primitives__u16__sub
  290. | Rust_primitives__crypto_abstractions__Use
  291. | Hax_lib__prop__constructors__forall
  292. | Rust_primitives__hax__int__from_machine
  293. | Rust_primitives__hax__machine_int__bitand
  294. | Hax_lib_protocol__crypto__dh_scalar_multiply_base
  295. | Core__convert__Impl_3
  296. | Rust_primitives__isize
  297. | Hax_lib_protocol__crypto__AEADKey
  298. | Core__ops__range__RangeFrom__start
  299. | Rust_primitives__usize__sub
  300. | Rust_primitives__i8__le
  301. | Hax_lib_protocol__crypto__Impl_4__from_bytes
  302. | Core__ops__bit__Shr__Output
  303. | Rust_primitives__i32__lt
  304. | Rust_primitives__hax__int__neg
  305. | Rust_primitives__hax__machine_int__shr
  306. | Alloc__slice__Impl_2__V
  307. | Rust_primitives__dummy_hax_concrete_ident_wrapper____1__Use
  308. | Core__borrow
  309. | Core__ops__index__IndexMut__index_mut
  310. | Core__borrow__Impl_2__'_
  311. | Rust_primitives__i16__eq
  312. | Core__panicking__AssertKind
  313. | Rust_primitives__hax__machine_int__rem
  314. | Rust_primitives__u16__eq
  315. | Rust_primitives__i8__ge
  316. | Rust_primitives__i128__bit_xor
  317. | Rust_primitives__usize__div
  318. | Core__ops__arith__Add
  319. | Rust_primitives__usize__bit_xor
  320. | Hax_lib___internal_while_loop_invariant
  321. | Rust_primitives__usize__eq
  322. | Core__convert
  323. | Rust_primitives__dummy_hax_concrete_ident_wrapper__Closure_1
  324. | Rust_primitives__i16__sub
  325. | Rust_primitives__unsize
  326. | Alloc__slice__Impl__concat
  327. | Hax_lib_protocol__crypto__Impl_6__from_bytes
  328. | Rust_primitives__hax__folds__fold_chunked_slice_return
  329. | Core__ops__bit__Shl__Output
  330. | Core__slice__iter__ChunksExact
  331. | Rust_primitives__u8__lt
  332. | Rust_primitives__hax__machine_int__lt
  333. | Core__ops__bit__Shr
  334. | Core__iter__traits__collect
  335. | Rust_primitives__u16__shr
  336. | Rust_primitives__i16__bit_or
  337. | Core__ptr
  338. | Rust_primitives__dummy_hax_concrete_ident_wrapper__Use_4
  339. | Core__ops__deref__Deref
  340. | Rust_primitives__u32__rem
  341. | Core__result__Impl
  342. | Hax_lib___internal_loop_invariant
  343. | Core__str
  344. | Core__cmp__PartialOrd__gt__'__1
  345. | Rust_primitives__i8__div
  346. | Rust_primitives__i16__gt
  347. | Rust_primitives__u16__le
  348. | Core__clone__impls
  349. | Alloc__vec__Impl_2__extend_from_slice
  350. | Rust_primitives__usize__rem
  351. | Rust_primitives__isize__add
  352. | Core__ptr__const_ptr__Impl__T
  353. | Rust_primitives__u64__rem
  354. | Alloc__boxed__Impl__T
  355. | Rust_primitives__dummy_hax_concrete_ident_wrapper
  356. | Rust_primitives__u8__ne
  357. | Core__num__Impl_9
  358. | Rust_primitives__offset
  359. | Rust_primitives__hax__machine_int__sub
  360. | Core__ops__index
  361. | Hax_lib__abstraction__Abstraction__lift
  362. | Core__iter__traits__iterator__Iterator__enumerate
  363. | Hax_lib__abstraction__Abstraction
  364. | Core__clone
  365. | Core__slice__index__Impl_2__T
  366. | Core__clone__Clone__clone
  367. | Hax_lib_protocol__crypto__Impl_1
  368. | Core__iter__traits__iterator__Iterator__Item
  369. | Core__ops__try_trait__Try__Residual
  370. | Hax_lib__int__Impl_7___unsafe_from_str
  371. | Core__num
  372. | Core__ops__function__Fn
  373. | Rust_primitives__u8__shl
  374. | Rust_primitives__usize__add
  375. | Rust_primitives__i8__add
  376. | Std
  377. | Core__result__Impl_28
  378. | Core__fmt__Debug
  379. | Hax_lib__prop__Impl__not
  380. | Alloc__vec__Impl_14__I
  381. | Core__slice
  382. | Hax_lib__Refinement__get_mut__'_
  383. | Rust_primitives__u128__rem
  384. | Core__iter__traits__iterator__Iterator__fold
  385. | Alloc__vec__Impl_1__T
  386. | Alloc__vec__Impl_2__extend_from_slice__'_
  387. | Rust_primitives__i32__mul
  388. | Core__ops__function__FnOnce
  389. | Core__array__iter__IntoIter
  390. | Rust_primitives__dummy_hax_concrete_ident_wrapper__Use_3
  391. | Rust_primitives__u128__eq
  392. | Rust_primitives__i32__bit_and
  393. | Core__convert__Infallible
  394. | Rust_primitives__hax__repeat
  395. | Core__ops__deref__DerefMut__deref_mut
  396. | Std__prelude
  397. | Rust_primitives__u8
  398. | Alloc__slice__Impl__to_vec__'_
  399. | Rust_primitives__i8__shl
  400. | Hax_lib_protocol__crypto__Impl_6
  401. | Core__panicking__assert_failed
  402. | Rust_primitives__dummy_hax_concrete_ident_wrapper__iterator_functions__It
  403. | Alloc__vec__Impl_1__A
  404. | Rust_primitives__i64__bit_and
  405. | Core__ops__control_flow
  406. | Rust_primitives__hax__machine_int__bitor
  407. | Core__ops__bit__Not__not
  408. | Rust_primitives__dummy_hax_concrete_ident_wrapper____1__f__T
  409. | Rust_primitives__dummy_hax_concrete_ident_wrapper__props__Closure
  410. | Core__ops__control_flow__ControlFlow__Continue
  411. | Core__result__Result
  412. | Rust_primitives__i64__shl
  413. | Rust_primitives__hax__folds__fold_chunked_slice_cf
  414. | Hax_lib__prop__constructors__eq
  415. | Core__ops__index__Index
  416. | Rust_primitives__hax__monomorphized_update_at__update_at_range_full
  417. | Core__borrow__Borrow
  418. | Rust_primitives__dummy_hax_concrete_ident_wrapper_____arith
  419. | Rust_primitives__usize
  420. | Rust_primitives__u32__add
  421. | Rust_primitives__u64__mul
  422. | Alloc__vec__Impl_1__truncate__'_
  423. | Rust_primitives__i8__bit_and
  424. | Rust_primitives__i64__mul
  425. | Core__slice__iter
  426. | Core__cmp__PartialOrd__ge__'__1
  427. | Rust_primitives__i128__bit_and
  428. | Rust_primitives__i128
  429. | Rust_primitives__hax__folds
  430. | Hax_lib__int__Impl_44
  431. | Rust_primitives__hax__folds__fold_range_step_by_cf
  432. | Rust_primitives__i64__ge
  433. | Rust_primitives__hax__control_flow_monad__mexception__run
  434. | Core__iter__traits__iterator__Iterator
  435. | Rust_primitives__dummy_hax_concrete_ident_wrapper__I
  436. | Hax_lib_protocol__crypto__Impl__from_bytes__'_
  437. | Hax_lib_protocol__crypto__aead_decrypt
  438. | Rust_primitives__hax__machine_int__div
  439. | Core__convert__Into
  440. | Core__ops__bit__Not__Output
  441. | Core__cmp__PartialOrd__ge__'_
  442. | Rust_primitives__Use
  443. | Rust_primitives__hax__failure
  444. | Core__cmp__PartialEq__ne__'__1
  445. | Rust_primitives__hax__folds__fold_return
  446. | Core__ops__arith__Rem__Output
  447. | Rust_primitives__u128__shr
  448. | Hax_lib__Refinement__get_mut
  449. | Core__cmp__PartialEq__ne__'_
  450. | Rust_primitives__u8__mul
  451. | Rust_primitives__i128__add
  452. | Rust_primitives__hax__Never
  453. | Rust_primitives__hax__folds__fold_range_cf
  454. | Core__iter__traits__iterator__Iterator__next__'_
  455. | Hax_lib_protocol__crypto__Impl__from_bytes
  456. | Core__convert__num
  457. | Hax_lib__int__ToInt
  458. | Core__cmp__PartialOrd__lt__'__1
  459. | Rust_primitives__u16__gt
  460. | Core__slice__Impl
  461. | Core__convert__num__Impl_88
  462. | Core__ops__arith__Mul__mul
  463. | Rust_primitives__i64__rem
  464. | Rust_primitives__hax__int__div
  465. | Alloc__boxed__Box
  466. | Rust_primitives__hax__machine_int
  467. | Rust_primitives__i128__gt
  468. | Rust_primitives__i8__bit_xor
  469. | Rust_primitives__i32__bit_xor
  470. | Rust_primitives__i8__neg
  471. | Rust_primitives__i16__bit_xor
  472. | Rust_primitives__i16__rem
  473. | Core__ops__arith__Add__Output
  474. | Core__option__Option__None
  475. | Rust_primitives__i32__shr
  476. | Rust_primitives__u16__bit_or
  477. | Alloc__vec__Impl_8
  478. | Core__ptr__const_ptr
  479. | Core__slice__Impl__chunks_exact
  480. | Alloc__slice__Impl__into_vec
  481. | Rust_primitives__dummy_hax_concrete_ident_wrapper___
  482. | Rust_primitives__u32__mul
  483. | Rust_primitives__u32__div
  484. | Rust_primitives__hax__folds__fold_range_return
  485. | Rust_primitives__hax__int__sub
  486. | Rust_primitives__i16__add
  487. | Core__option__Impl__is_some__'_
  488. | Rust_primitives__u32__bit_or
  489. | Rust_primitives
  490. | Rust_primitives__hax__Failure__Ctor
  491. | Rust_primitives__hax__control_flow_monad__ControlFlowMonad
  492. | Core__slice__Impl__chunks_exact__'_
  493. | Rust_primitives__hax__machine_int__ne
  494. | Alloc__vec__Impl_11__A
  495. | Core__cmp__PartialOrd__ge
  496. | Rust_primitives__hax__int__mul
  497. | Core__panicking__AssertKind__Eq
  498. | Core__result
  499. | Hax_lib__int__Impl_17
  500. | Hax_lib__prop
  501. | Core__ops__range__Range
  502. | Rust_primitives__i16__shr
  503. | Rust_primitives__isize__lt
  504. | Core__num__Impl_9__to_le_bytes
  505. | Rust_primitives__i16__shl
  506. | Rust_primitives__i128__rem
  507. | Rust_primitives__u16__ge
  508. | Core__result__Impl__E
  509. | Core__cmp__PartialEq__eq__'__1
  510. | Rust_primitives__i32__gt
  511. | Rust_primitives__hax__control_flow_monad__mexception
  512. | Core__slice__index__SliceIndex
  513. | Hax_lib_protocol__crypto__hash__'_
  514. | Core__ops__try_trait__Try__from_output
  515. | Core__iter__traits__iterator__Iterator__step_by
  516. | Core__ops__index__Index__index
  517. | Hax_lib_protocol__crypto__hash
  518. | Rust_primitives__i32__shl
  519. | Core__ops__bit__BitAnd__bitand
  520. | Rust_primitives__i64__ne
  521. | Core__ops__arith__Neg__Output
  522. | Rust_primitives__dummy_hax_concrete_ident_wrapper__dummy
  523. | Rust_primitives__u32__shr
  524. | Rust_primitives__u128
  525. | Rust_primitives__hax__monomorphized_update_at__update_at_range
  526. | Core__ops__control_flow__ControlFlow__Break__0
  527. | Alloc__vec__Impl_8__T
  528. | Core__array__iter__Impl
  529. | Rust_primitives__i128__shr
  530. | Rust_primitives__i128__sub
  531. | Hax_lib_protocol__crypto__Impl_5
  532. | Hax_lib__Refinement__get
  533. | Core__ops__control_flow__ControlFlow__Break
  534. | Core__cmp__PartialOrd__lt__'_
  535. | Core__panicking__assert_failed__'__1
  536. | Rust_primitives__crypto_abstractions__crypto_abstractions
  537. | Core__ops__deref__Deref__deref
  538. | Hax_lib__prop__constructors__implies
  539. | Hax_lib__prop__Impl__ne
  540. | Core__ops__arith
  541. | Rust_primitives__u8__sub
  542. | Core__cmp__PartialOrd__le
  543. | Rust_primitives__u32__ne
  544. | Core__ops__index__IndexMut
  545. | Rust_primitives__dummy_hax_concrete_ident_wrapper__question_mark_result__B
  546. | Rust_primitives__usize__mul
  547. | Rust_primitives__i16__le
  548. | Rust_primitives__isize__div
  549. | Rust_primitives__hax__control_flow_monad__ControlFlowMonad__lift
  550. | Alloc__vec__Impl_13__A
  551. | Core__iter__traits__collect__IntoIterator
  552. | Rust_primitives__i16__neg
  553. | Core__ops__bit__BitXor
  554. | Hax_lib_protocol__crypto__aead_encrypt__'_
  555. | Hax_lib__abstraction__Abstraction__AbstractType
  556. | Rust_primitives__dummy_hax_concrete_ident_wrapper__props__Closure_1
  557. | Core__ops__arith__Sub
  558. | Rust_primitives__hax__control_flow_monad__mresult__run
  559. | Core__alloc__Allocator
  560. | Core__marker
  561. | Core__result__Impl__T
  562. | Hax_lib__abstraction__Concretization__concretize
  563. | Hax_lib_protocol__crypto__aead_decrypt__'_
  564. | Rust_primitives__u64__ne
  565. | Rust_primitives__i128__ne
  566. | Core__option__Option__Some
  567. | Hax_lib__int__Impl_9
  568. | Rust_primitives__dummy_hax_concrete_ident_wrapper__iterator_functions
  569. | Hax_lib__prop__Impl_3
  570. | Rust_primitives__dummy_hax_concrete_ident_wrapper____1__f
  571. | Hax_lib__prop__Prop
  572. | Alloc__vec__Impl_2__extend_from_slice__'__1
  573. | Hax_lib__int
  574. | Alloc__vec__Impl_11
  575. | Core__result__Result__Ok
  576. | Hax_lib__Refinement__InnerType
  577. | Core__fmt__Arguments
  578. | Rust_primitives__i8__mul
  579. | Core__slice__Impl__len__'_
  580. | Rust_primitives__u32__lt
  581. | Alloc__vec__Impl_2__A
  582. | Core__option__Option__Some__0
  583. | Hax_lib_protocol__crypto__dh_scalar_multiply
  584. | Hax_lib__int__Impl_7___unsafe_from_str__'_
  585. | Core__ops__bit__BitOr__Output
  586. | Rust_primitives__u32__sub
  587. | Rust_primitives__i8
  588. | Core__clone__Clone
  589. | Rust_primitives__u8__shr
  590. | Hax_lib__prop__Impl__and
  591. | Hax_lib__assert
  592. | Hax_lib__int__ToInt__to_int
  593. | Rust_primitives__u64__bit_and
  594. | Rust_primitives__u64__bit_or
  595. | Rust_primitives__u64__lt
  596. | Core__result__Impl_28__E
  597. | Hax_lib_protocol__crypto__hmac__'_
  598. | Rust_primitives__u128__sub
  599. | Rust_primitives__usize__shr
  600. | Rust_primitives__i64__le
  601. | Hax_lib_protocol__crypto__AEADTag
  602. | Core__iter__traits
  603. | Rust_primitives__hax__folds__fold_chunked_slice
  604. | Rust_primitives__u32__shl
  605. | Rust_primitives__i16
  606. | Rust_primitives__u16__mul
  607. | Hax_lib_protocol__crypto__AEADIV
  608. | Rust_primitives__u8__eq
  609. | Rust_primitives__u8__ge
  610. | Hax_lib_protocol__crypto__Impl
  611. | Rust_primitives__isize__mul
  612. | Hax_lib__prop__constructors__exists
  613. | Hax_lib__inline_unsafe
  614. | Core__ops__index__Index__index__'_
  615. | Core__marker__Tuple
  616. | Core__ops__deref__Deref__Target
  617. | Hax_lib__prop__Impl__or
  618. | Core__iter__adapters
  619. | Rust_primitives__dummy_hax_concrete_ident_wrapper__dummy__T
  620. | Rust_primitives__u128__lt
  621. | Rust_primitives__i64__lt
  622. | Core__ops__range__RangeFull
  623. | Core__slice__Impl__iter__'_
  624. | Rust_primitives__hax__machine_int__gt
  625. | Alloc
  626. | Core__str__Impl__as_ptr
  627. | Hax_lib__Refinement
  628. | Alloc__vec__Vec
  629. | Alloc__slice__Impl__to_vec
  630. | Rust_primitives__u8__neg
  631. | Core__option
  632. | Core__cmp__PartialOrd__le__'_
  633. | Hax_lib__Refinement__new
  634. | Core__fmt__num__Impl_80
  635. | Rust_primitives__dummy_hax_concrete_ident_wrapper__Use_2
  636. | Hax_lib__prop__Impl__from_bool
  637. | Rust_primitives__i32__le
  638. | Hax_lib__inline__'_
  639. | Rust_primitives__dummy_hax_concrete_ident_wrapper__refinements__T
  640. | Alloc__alloc
  641. | Rust_primitives__isize__gt
  642. | Rust_primitives__u64__neg
  643. | Rust_primitives__u32__bit_and
  644. | Rust_primitives__hax__folds__fold_range_step_by
  645. | Hax_lib__int__Impl_16
  646. | Core__ops__range__Range__start
  647. | Core__ops__arith__Sub__Output
  648. | Core__ops__bit__Shl__shl
  649. | Core__marker__Sized
  650. | Rust_primitives__hax__machine_int__shl
  651. | Alloc__boxed
  652. | Hax_lib_protocol__crypto__HashAlgorithm
  653. | Rust_primitives__hax__control_flow_monad
  654. | Hax_lib__prop__implies
  655. | Rust_primitives__dummy_hax_concrete_ident_wrapper_____arith__X
  656. | Rust_primitives__i32__ge
  657. | Core__iter__adapters__enumerate__Enumerate
  658. | Alloc__vec__Impl_2
  659. | Rust_primitives__isize__sub
  660. | Rust_primitives__u64__shr
  661. | Alloc__vec__Impl_1
  662. | Rust_primitives__i128__ge
  663. | Hax_lib_protocol__crypto__AEADAlgorithm__Chacha20Poly1305
  664. | Alloc__vec__Impl_14__T
  665. | Hax_lib__prop__constructors__from_bool
  666. | Core__iter__adapters__step_by
  667. | Hax_lib_protocol__crypto__Impl_1__from_bytes__'_
  668. | Alloc__alloc__Impl_3
  669. | Core__result__Result__Ok__0
  670. | Core__cmp__PartialOrd
  671. | Rust_primitives__i8__sub
  672. | Core__panicking
  673. | Rust_primitives__hax__while_loop_cf
  674. | Rust_primitives__dummy_hax_concrete_ident_wrapper__refinements__U
  675. | Rust_primitives__dummy_hax_concrete_ident_wrapper_____Use
  676. | Core__ops__arith__Div__Output
  677. | Core__convert__Impl_4__T
  678. | Rust_primitives__u8__div
  679. | Rust_primitives__i8__gt
  680. | Rust_primitives__isize__shr
  681. | Rust_primitives__u128__ge
  682. | Core__option__Impl__T
  683. | Rust_primitives__i16__lt
  684. | Alloc__vec__Impl_13
  685. | Core__borrow__Impl_2
  686. | Core__iter__traits__collect__IntoIterator__IntoIter
  687. | Rust_primitives__i128__div
  688. | Core__str__Impl
  689. | Hax_lib__prop__Impl
  690. | Rust_primitives__u8__bit_and
  691. | Core__cmp__PartialEq__eq__'_
  692. | Hax_lib_protocol__crypto__hmac__'__1
  693. | Rust_primitives__i64__eq
  694. | Rust_primitives__u64__gt
  695. | Rust_primitives__dummy_hax_concrete_ident_wrapper__question_mark_result__A
  696. | Std__prelude__rust_2021
  697. | Alloc__boxed__Impl__new
  698. | Core__ops__arith__Neg
  699. | Rust_primitives__u64__bit_xor
  700. | Core__convert__Impl_3__U
  701. | Hax_lib__int__Impl_7__pow2
  702. | Core__convert__Impl_3__T
  703. | Core__cmp__PartialEq
  704. | Core__ops__bit__Shr__shr
  705. | Rust_primitives__hax__update_at
  706. | Rust_primitives__hax__machine_int__not
  707. | Hax_lib_protocol__crypto__DHGroup__X25519
  708. | Rust_primitives__hax__int__rem
  709. | Rust_primitives__hax__monomorphized_update_at__update_at_usize
  710. | Hax_lib__prop__ToProp__to_prop
  711. | Hax_lib_protocol__crypto__aead_encrypt__'__1
  712. | Hax_lib_protocol__crypto__Impl_1__from_bytes
  713. | Hax_lib__prop__Impl__implies
  714. | Alloc__slice
  715. | Core__slice__iter__Iter
  716. | Hax_lib
  717. | Rust_primitives__i32__add
  718. | Rust_primitives__i64__sub
  719. | Rust_primitives__hax__control_flow_monad__mresult
  720. | Rust_primitives__dummy_hax_concrete_ident_wrapper__question_mark_result
  721. | Core__ops__bit__Shl
  722. | Rust_primitives__u16__div
  723. | Rust_primitives__i32
  724. | Core__ops__arith__Rem
  725. | Rust_primitives__hax__machine_int__bitxor
  726. | Rust_primitives__dummy_hax_concrete_ident_wrapper____1
  727. | Rust_primitives__u64__sub
  728. | Core__cmp__PartialOrd__gt__'_
  729. | Core__iter
  730. | Core__convert__Impl_4
  731. | Rust_primitives__u8__gt
  732. | Rust_primitives__usize__lt
  733. | Rust_primitives__i128__lt
  734. | Rust_primitives__i32__bit_or
  735. | Alloc__vec
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