Crypto.ChaCha

Definitions

Key : Type

Visibility: public export

ChaChaState : Type

Visibility: public export

constants : Vect 4 Bits32

Visibility: public export

quarter_rotate : Fin 16 -> Fin 16 -> Fin 16 -> Fin 16 -> State ChaChaState ()

Visibility: public export

double_rotate : State ChaChaState ()

Visibility: public export

run2x : Nat -> ChaChaState -> ChaChaState

Visibility: public export

chacha_rfc8439_block : Nat -> Bits32 -> Key -> Vect 3 Bits32 -> Vect 64 Bits8

  ChaCha construction with 4 octets counter and 12 octets nonce as per RFC8439

Visibility: public export

chacha_original_block : Nat -> Bits64 -> Key -> Vect 2 Bits32 -> Vect 64 Bits8

  ChaCha construction with 8 octets counter and 8 octets nonce as per the original ChaCha specification

Visibility: public export