Hax_engine.Concrete_ident_generated
type t =
| Core__ops__arith__Neg__neg
| Rust_primitives__hax__int__lt
| Core__alloc__Allocator
| Alloc__macros
| Hax_lib_protocol__crypto__Impl_5
| Core__cmp__PartialOrd__gt__'__1
| Alloc__alloc
| Hax_lib_protocol__crypto__Impl_1__from_bytes__'_
| Core__cmp__PartialOrd__lt__'__1
| Core__slice__Impl__iter
| Rust_primitives__u128__mul
| Rust_primitives__u128__sub
| Rust_primitives__hax__int__sub
| Hax_lib_protocol__crypto__HMACAlgorithm
| Core__ops__range__Range__start
| Rust_primitives__dummy_hax_concrete_ident_wrapper__Use
| Alloc__alloc__Impl_1
| Core__array__iter
| Hax_lib__Refinement__get
| Core__ops__arith__Rem__Output
| Hax_lib_protocol__crypto__HashAlgorithm__Sha256
| Rust_primitives
| Rust_primitives__u128__bit_or
| Rust_primitives__u128__lt
| Hax_lib__inline_unsafe__'_
| Rust_primitives__dummy_hax_concrete_ident_wrapper__question_mark_result__B
| Alloc__vec__Impl_13__T
| Alloc__slice__Impl_2__T
| Core__ops__deref__Deref__Target
| Rust_primitives__hax__folds__fold_range_step_by_cf
| Hax_lib
| Hax_lib_protocol__crypto__AEADTag
| Core__ops__try_trait__Try
| Hax_lib__Refinement__InnerType
| Rust_primitives__u128__bit_xor
| Alloc__vec__Impl_8
| Core__ops
| Rust_primitives__hax__folds__fold_range_cf
| Rust_primitives__hax__while_loop_return
| Core__convert__num
| Rust_primitives__unsize
| Core__ops__bit__Shl
| Hax_lib__int__Impl_5
| Rust_primitives__hax__folds__fold_return
| Core__ptr__const_ptr__Impl__offset
| Hax_lib_protocol__crypto__DHGroup
| Hax_lib_protocol__crypto__HashAlgorithm
| Core__ops__control_flow__ControlFlow__Continue
| Rust_primitives__dummy_hax_concrete_ident_wrapper__Use_4
| Rust_primitives__dummy_hax_concrete_ident_wrapper_____Use
| Core__ops__function
| Core__convert__Impl_3__T
| Core__option__Option__None
| Core__fmt__Debug
| Core__cmp__PartialOrd__ge
| Core__convert__Into__into
| Rust_primitives__hax__int__mul
| Alloc__slice__Concat__Output
| Alloc__vec__Impl_2
| Alloc__vec__Impl_1__truncate
| Core__convert__Into
| Core__clone__impls
| Core__ops__control_flow__ControlFlow
| Alloc__alloc__Impl_3
| Core__ops__bit__Not
| Core__slice__iter__Iter
| Alloc__vec__Impl_11__A
| Hax_lib__Refinement
| Core__iter__traits__iterator
| Alloc__slice__Impl
| Core__ptr
| Core__cmp__PartialEq__eq__'__1
| Alloc__vec__Impl_14
| Rust_primitives__hax__dropped_body
| Rust_primitives__hax__folds__fold_range_return
| Rust_primitives__hax__control_flow_monad__mexception__run
| Hax_lib__inline_unsafe
| Rust_primitives__hax__box_new
| Core__ops__arith__Mul__Output
| Core__ops__control_flow
| Core__macros__builtin
| Rust_primitives__std
| Core__str
| Core__result__Impl_27__F
| Rust_primitives__hax__int
| Hax_lib__int__Abstraction__lift
| Core__slice__Impl
| Alloc__vec__Impl_2__A
| Core__iter__adapters__enumerate__Enumerate
| Alloc__vec
| Core__iter__adapters__step_by__StepBy
| Alloc__vec__Vec
| Core__ops__bit__BitAnd__bitand
| Rust_primitives__dummy_hax_concrete_ident_wrapper__refinements
| Core__slice__Impl__chunks_exact
| Core__slice__index__Impl_2
| Rust_primitives__u128
| Rust_primitives__dummy_hax_concrete_ident_wrapper__iterator_functions
| Rust_primitives__crypto_abstractions
| Hax_lib_protocol__crypto
| Hax_lib_protocol__crypto__aead_decrypt__'_
| Rust_primitives__hax__while_loop
| Rust_primitives__hax__control_flow_monad__mresult__run
| Alloc__vec__Impl_2__extend_from_slice__'__1
| Core__ops__try_trait__Try__branch
| Core__clone__impls__Impl_6
| Core__ops__deref__Deref
| Rust_primitives__hax__folds__fold_enumerated_slice
| Core__result__Impl_26
| Core__ops__try_trait__Try__from_output
| Core__result__Result__Err__0
| Core__ops__arith__Sub__sub
| Rust_primitives__alloc
| Core__ops__arith__Mul
| Std__prelude__rust_2021
| Core__convert__From__from
| Core__ops__bit__BitAnd
| Core__result__Result__Err
| Rust_primitives__hax__monomorphized_update_at__update_at_range_to
| Core__ops__index__IndexMut__index_mut__'_
| Rust_primitives__hax__control_flow_monad__ControlFlowMonad
| Hax_lib_protocol__crypto__AEADAlgorithm__Chacha20Poly1305
| Hax_lib_protocol__crypto__Impl__from_bytes
| Core__borrow__Borrow
| Hax_lib_protocol__crypto__Impl_4
| Core__ops__bit__Not__not
| Core__ops__arith__Rem
| Hax_lib_protocol__crypto__aead_decrypt__'__1
| Rust_primitives__u128__ge
| Hax_lib_protocol__crypto__aead_encrypt__'__1
| Core__convert__num__Impl_88
| Hax_lib_protocol__crypto__Impl_4__from_bytes__'_
| Core__ops__deref__DerefMut
| Rust_primitives__hax__control_flow_monad__moption
| Core__panicking__assert_failed__'__1
| Rust_primitives__dummy_hax_concrete_ident_wrapper__question_mark_result
| Core__iter__traits__collect
| Rust_primitives__hax__int__le
| Core__ops__bit__Shl__Output
| Alloc__vec__Impl_13
| Hax_lib__int__Impl_5___unsafe_from_str
| Core__result__Impl_26__E
| Core__result__Impl
| Core__ops__control_flow__ControlFlow__Break__0
| Hax_lib__int__Impl_29
| Rust_primitives__dummy_hax_concrete_ident_wrapper_____Use_2
| Rust_primitives__dummy_hax_concrete_ident_wrapper_____arith__X
| Rust_primitives__dummy_hax_concrete_ident_wrapper___
| Rust_primitives__hax__repeat
| Rust_primitives__hax__folds__fold_range
| Rust_primitives__hax__Failure__Ctor
| Core__cmp__PartialOrd__lt
| Hax_lib_protocol__crypto__dh_scalar_multiply_base
| Alloc__vec__Impl_8__T
| Std__prelude
| Core__ops__bit__Not__Output
| Rust_primitives__dummy_hax_concrete_ident_wrapper____1
| Core__ops__index__Index
| Rust_primitives__hax__control_flow_monad__ControlFlowMonad__lift
| Core__slice__index__SliceIndex
| Alloc__slice__Concat
| Hax_lib_protocol__crypto__DHGroup__X25519
| Core__option__Option__Some
| Rust_primitives__u128__ne
| Rust_primitives__dummy_hax_concrete_ident_wrapper__refinements__U
| Core__slice__index
| Core__result__Impl__T
| Core__ops__arith__Div__div
| Core__result
| Rust_primitives__hax__folds__fold_enumerated_chunked_slice_return
| Core__result__Impl__map_err
| Rust_primitives__u128__gt
| Core__ptr__const_ptr__Impl__T
| Core__iter__traits__collect__IntoIterator__into_iter
| Alloc__string__String
| Alloc__string
| Core__clone__Clone
| Core__cmp__PartialOrd__ge__'__1
| Rust_primitives__hax__failure
| Core__ops__index__IndexMut__index_mut
| Core__iter__traits__iterator__Iterator__Item
| Core__ops__range__Range__end
| Rust_primitives__crypto_abstractions__Use
| Rust_primitives__dummy_hax_concrete_ident_wrapper__dummy
| Hax_lib__int__Impl_5__pow2
| Core__slice
| Rust_primitives__hax__folds__fold_cf
| Alloc__slice__Impl__concat
| Core__slice__Impl__iter__'_
| Alloc__vec__Impl_14__T
| Alloc__slice__Impl_2
| Core__marker__Sized
| Core__ops__try_trait__Try__Residual
| Core__ops__index__Index__index
| Hax_lib_protocol__crypto__hmac
| Hax_lib_protocol__crypto__hmac__'__1
| Alloc__vec__Impl_2__extend_from_slice__'_
| Core__panicking
| Std
| Rust_primitives__hax__int__from_machine
| Hax_lib_protocol__crypto__Impl_1__from_bytes
| Core__ops__arith__Add__add
| Core__borrow__Impl_2
| Hax_lib_protocol__crypto__DHScalar
| Hax_lib__Refinement__new
| Rust_primitives__dummy_hax_concrete_ident_wrapper__iterator_functions__It
| Alloc__boxed
| Core__result__Impl_27__T
| Hax_lib_protocol__crypto__hmac__'_
| Hax_lib_protocol__crypto__aead_encrypt
| Core__array
| Core__iter__adapters__enumerate
| Core__ops__index__Index__Output
| Core__cmp
| Core__ops__range
| Hax_lib__int
| Rust_primitives__hax__control_flow_monad__mexception
| Hax_lib__int__Concretization
| Core__str__Impl
| Hax_lib_protocol__crypto__AEADKey
| Hax_lib_protocol__crypto__Impl_1
| Core__str__Impl__as_ptr__'_
| Hax_lib__inline
| Alloc__boxed__Impl
| Alloc__vec__Impl_14__I
| Core__ops__bit__Shr__shr
| Core__ops__bit__Shl__shl
| Rust_primitives__hax__folds__fold_enumerated_chunked_slice
| Core__cmp__PartialOrd__le__'_
| Core__fmt__Arguments
| Core__cmp__PartialOrd__ge__'_
| Core__ops__arith
| Hax_lib__int__Impl_5___unsafe_from_str__'_
| Rust_primitives__hax__int__ne
| Rust_primitives__hax__Failure
| Core__fmt__num
| Rust_primitives__dummy_hax_concrete_ident_wrapper__Use_1
| Core__convert__From
| Core__ops__control_flow__ControlFlow__Break
| Hax_lib_protocol__crypto__AEADIV
| Alloc__vec__Impl_11
| Core__ops__arith__Sub__Output
| Rust_primitives__u128__add
| Core__iter__traits
| Rust_primitives__hax__update_at
| Core__panicking__AssertKind
| Rust_primitives__dummy_hax_concrete_ident_wrapper__Use_3
| Core__cmp__PartialOrd
| Core__iter__traits__iterator__Iterator__fold
| Hax_lib_protocol__crypto__Impl_9
| Core__macros
| Core__ops__bit__Shr
| Rust_primitives__dummy_hax_concrete_ident_wrapper_____Use_1
| Core__cmp__PartialOrd__le__'__1
| Alloc__vec__Impl_11__T
| Core__result__Result__Ok
| Alloc__vec__Impl_8__A
| Rust_primitives__hax__monomorphized_update_at__update_at_usize
| Rust_primitives__hax__monomorphized_update_at__update_at_range_from
| Alloc__slice__Impl__to_vec
| Rust_primitives__u128__bit_and
| Rust_primitives__hax__folds__fold_enumerated_slice_return
| Core__ops__range__RangeTo
| Rust_primitives__hax__monomorphized_update_at
| Core__ops__function__FnMut
| Hax_lib__int__Impl_13
| Core__slice__iter
| Hax_lib_protocol__crypto__Impl_5__from_bytes__'_
| Rust_primitives__dummy_hax_concrete_ident_wrapper__question_mark_result__A
| Core__convert
| Hax_lib__RefineAs__into_checked
| Alloc__vec__Impl_1__A
| Core__result__Impl_27__E
| Core__slice__Impl__len__'_
| Alloc__slice__Impl__into_vec
| Core__slice__iter__ChunksExact
| Core__ops__bit__BitXor__Output
| Rust_primitives__hax__MutRef
| Hax_lib__inline__'_
| Core__num__Impl_9__to_le_bytes
| Core__array__iter__Impl__T
| Rust_primitives__u128__shr
| Core__ops__bit__BitAnd__Output
| Hax_lib_protocol__crypto__dh_scalar_multiply
| Core
| Core__borrow
| Core__cmp__PartialOrd__gt__'_
| Core__clone__Clone__clone__'_
| Hax_lib_protocol__crypto__AEADAlgorithm
| Core__slice__Impl__T
| Rust_primitives__u128__le
| Core__slice__Impl__chunks_exact__'_
| Core__result__Impl__E
| Core__ops__try_trait__FromResidual
| Rust_primitives__dummy_hax_concrete_ident_wrapper____1__Use
| Core__str__Impl__as_ptr
| Hax_lib_protocol__crypto__aead_encrypt__'_
| Core__ops__bit
| Hax_lib__int__Impl_7
| Core__clone__Clone__clone
| Alloc__vec__from_elem
| Alloc__slice__Impl__concat__'_
| Core__ops__arith__Sub
| Hax_lib_protocol__crypto__Impl_6__from_bytes
| Rust_primitives__hax__folds
| Core__slice__index__Impl_2__T
| Core__cmp__PartialOrd__gt
| Core__ops__arith__Add
| Core__ops__arith__Mul__mul
| Hax_lib_protocol__crypto__hash__'_
| Alloc__slice
| Alloc
| Core__option__Option__Some__0
| Core__ops__arith__Neg__Output
| Core__convert__Impl_3
| Core__ops__control_flow__ControlFlow__Continue__0
| Alloc__boxed__Box
| Core__ops__bit__BitOr__Output
| Core__ops__range__Range
| Rust_primitives__hax__control_flow_monad__mresult
| Core__ops__index__Index__index__'_
| Core__marker__Copy
| Core__cmp__PartialEq__ne__'_
| Core__marker
| Alloc__alloc__Global
| Core__option__Impl__is_some
| Core__ops__bit__BitOr
| Hax_lib__Refinement__get_mut__'_
| Core__fmt__num__Impl_80
| Core__iter__traits__collect__IntoIterator__IntoIter
| Hax_lib_protocol__ProtocolError
| Core__iter__traits__iterator__Iterator__next__'_
| Core__iter__adapters__step_by
| Core__borrow__Impl_2__T
| Core__ops__index
| Hax_lib_protocol
| Hax_lib_protocol__crypto__aead_decrypt
| Rust_primitives__dummy_hax_concrete_ident_wrapper__I
| Alloc__vec__Impl_1__truncate__'_
| Hax_lib_protocol__crypto__hash
| Core__result__Result__Ok__0
| Hax_lib_protocol__crypto__Impl_4__from_bytes
| Core__panicking__assert_failed
| Core__iter
| Core__result__Impl_27
| Core__ops__function__FnOnce
| Rust_primitives__hax__monomorphized_update_at__update_at_range_full
| Core__panicking__assert_failed__'_
| Rust_primitives__dummy_hax_concrete_ident_wrapper____1__f__T
| Rust_primitives__hax__folds__fold_enumerated_chunked_slice_cf
| Hax_lib_protocol__crypto__DHElement
| Core__num
| Core__alloc
| Core__ops__deref__Deref__deref__'_
| Core__ops__range__RangeTo__end
| Core__iter__traits__iterator__Iterator__step_by
| Core__convert__Infallible
| Rust_primitives__crypto_abstractions__crypto_abstractions
| Core__panicking__assert_failed__'__2
| Core__option__Option
| Hax_lib__int__Abstraction__AbstractType
| Core__cmp__PartialEq__eq
| Core__iter__traits__collect__IntoIterator
| Rust_primitives__dummy_hax_concrete_ident_wrapper__dummy__T
| Rust_primitives__hax__int__into_machine
| Rust_primitives__hax__array_of_list
| Rust_primitives__dummy_hax_concrete_ident_wrapper_____arith
| Core__ops__arith__Div
| Core__ops__deref__DerefMut__deref_mut__'_
| Rust_primitives__hax__int__gt
| Core__option__Impl__is_some__'_
| Hax_lib_protocol__crypto__Impl
| Core__ops__arith__Add__Output
| Rust_primitives__hax__int__eq
| Core__result__Result
| Alloc__vec__Impl_2__T
| Core__ops__try_trait
| Alloc__slice__Impl__to_vec__'_
| Core__panicking__AssertKind__Eq
| Core__option__Impl__T
| Core__ops__try_trait__FromResidual__from_residual
| Core__cmp__PartialOrd__le
| Core__slice__index__Impl_4__T
| Rust_primitives__dummy_hax_concrete_ident_wrapper____1__f
| Alloc__slice__Impl__T
| Core__ops__bit__BitXor
| Hax_lib_protocol__crypto__Impl_6
| Core__ops__deref__Deref__deref
| Alloc__boxed__Impl__new
| Core__panicking__panic
| Core__num__Impl_9
| Alloc__boxed__Impl__T
| Core__ops__arith__Div__Output
| Core__option__Impl
| Core__fmt
| Core__cmp__PartialEq__ne
| Hax_lib_protocol__crypto__HMACAlgorithm__Sha256
| Rust_primitives__u128__eq
| Core__cmp__PartialOrd__lt__'_
| Rust_primitives__hax__int__div
| Core__ops__bit__Shr__Output
| Alloc__vec__Impl_1
| Core__convert__num__Impl_64
| Hax_lib_protocol__crypto__Impl_6__from_bytes__'_
| Rust_primitives__hax__folds__fold_range_step_by
| Rust_primitives__hax__int__add
| Core__result__Impl_26__T
| Rust_primitives__Use
| Rust_primitives__hax__folds__fold_range_step_by_return
| Core__ops__range__RangeFull
| Rust_primitives__hax__Never
| Rust_primitives__hax__int__ge
| Core__clone
| Hax_lib__assert
| Rust_primitives__hax__never_to_any
| Rust_primitives__hax__folds__fold_enumerated_slice_cf
| Core__iter__traits__iterator__Iterator__next
| Core__array__iter__Impl
| Rust_primitives__dummy_hax_concrete_ident_wrapper__Use_2
| Core__cmp__PartialEq__ne__'__1
| Hax_lib__int__Abstraction
| Core__iter__adapters
| Rust_primitives__hax__while_loop_cf
| Core__array__iter__Impl__N
| Alloc__vec__Impl_13__I
| Core__ops__deref
| Core__slice__Impl__len
| Core__option
| Alloc__vec__Impl_1__T
| Hax_lib_protocol__crypto__Impl__from_bytes__'_
| Core__cmp__PartialEq
| Rust_primitives__offset
| Rust_primitives__u128__rem
| Core__array__iter__IntoIter
| Core__ops__range__RangeFrom
| Core__iter__traits__iterator__Iterator
| Rust_primitives__dummy_hax_concrete_ident_wrapper__refinements__T
| Alloc__vec__Impl_2__extend_from_slice
| Rust_primitives__hax__control_flow_monad
| Core__slice__index__Impl_4
| Rust_primitives__hax__int__rem
| Core__ops__index__IndexMut
| Hax_lib__Refinement__get_mut
| Core__ops__arith__Rem__rem
| Hax_lib___internal_loop_invariant
| Alloc__vec__Impl_14__A
| Core__ops__bit__BitOr__bitor
| Rust_primitives__hax
| Hax_lib__int__Concretization__concretize
| Core__ptr__const_ptr__Impl
| Alloc__slice__Impl_2__V
| Core__ops__range__RangeFrom__start
| Core__cmp__PartialEq__eq__'_
| Hax_lib__int__Int
| Rust_primitives__u128__shl
| Rust_primitives__hax__monomorphized_update_at__update_at_range
| Core__ptr__const_ptr
| Rust_primitives__hax__control_flow_monad__moption__run
| Core__iter__traits__iterator__Iterator__enumerate
| Rust_primitives__dummy_hax_concrete_ident_wrapper
| Core__borrow__Impl_2__'_
| Hax_lib__RefineAs
| Rust_primitives__u128__div
| Core__convert__Impl_3__U
| Core__ops__bit__BitXor__bitxor
| Alloc__vec__Impl_13__A
| Core__ops__arith__Neg
| Core__ops__deref__DerefMut__deref_mut
| Hax_lib_protocol__crypto__Impl_5__from_bytes
| Core__ops__try_trait__Try__Output
val pp :
Ppx_deriving_runtime.Format.formatter ->
t ->
Ppx_deriving_runtime.unit
val show : t -> Ppx_deriving_runtime.string
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 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
val comparator : (comparable_t, comparator_witness) Base__Comparator.comparator
module Values : sig ... end
val def_id_of : t -> Types.def_id
val impl_infos : (Types.def_id * Types.impl_infos) Base.List.t