Network.TLS.Wrapper

(source)

Definitions

record Wrapper : Nat -> Type

Totality: total
Visibility: public export
Constructor:

MkWrapper : List Bits8 -> Vect mac_size Bits8 -> Wrapper mac_size

Projections:

.auth_tag : Wrapper mac_size -> Vect mac_size Bits8
.encrypted_data : Wrapper mac_size -> List Bits8

.encrypted_data : Wrapper mac_size -> List Bits8

Visibility: public export

encrypted_data : Wrapper mac_size -> List Bits8

Visibility: public export

.auth_tag : Wrapper mac_size -> Vect mac_size Bits8

Visibility: public export

auth_tag : Wrapper mac_size -> Vect mac_size Bits8

Visibility: public export

to_application_data : Wrapper mac_size -> List Bits8

Visibility: public export

from_application_data : List Bits8 -> Maybe (Wrapper mac_size)

Visibility: public export

record Wrapper2 : Nat -> Nat -> Type

Totality: total
Visibility: public export
Constructor:

MkWrapper2 : Vect iv_size Bits8 -> List Bits8 -> Vect mac_size Bits8 -> Wrapper2 iv_size mac_size

Projections:

.auth_tag : Wrapper2 iv_size mac_size -> Vect mac_size Bits8
.encrypted_data : Wrapper2 iv_size mac_size -> List Bits8
.iv_data : Wrapper2 iv_size mac_size -> Vect iv_size Bits8

.iv_data : Wrapper2 iv_size mac_size -> Vect iv_size Bits8

Visibility: public export

iv_data : Wrapper2 iv_size mac_size -> Vect iv_size Bits8

Visibility: public export

.encrypted_data : Wrapper2 iv_size mac_size -> List Bits8

Visibility: public export

encrypted_data : Wrapper2 iv_size mac_size -> List Bits8

Visibility: public export

.auth_tag : Wrapper2 iv_size mac_size -> Vect mac_size Bits8

Visibility: public export

auth_tag : Wrapper2 iv_size mac_size -> Vect mac_size Bits8

Visibility: public export

to_application_data2 : Wrapper2 iv_size mac_size -> List Bits8

Visibility: public export

from_application_data2 : List Bits8 -> Maybe (Wrapper2 iv_size mac_size)

Visibility: public export

record WrappedRecord : Type

Totality: total
Visibility: public export
Constructor:

MkWrappedRecord : RecordType -> List Bits8 -> WrappedRecord

Projections:

.record_type : WrappedRecord -> RecordType
.wrapped_data : WrappedRecord -> List Bits8

.record_type : WrappedRecord -> RecordType

Visibility: public export

record_type : WrappedRecord -> RecordType

Visibility: public export

.wrapped_data : WrappedRecord -> List Bits8

Visibility: public export

wrapped_data : WrappedRecord -> List Bits8

Visibility: public export

to_application_data : WrappedRecord -> List Bits8

Visibility: public export