Crypto.Hash.MerkleDamgard

(source)

Definitions

record MerkleDamgard : Nat -> (0 _ : Nat) -> (0 _ : Type) -> Type

Totality: total
Visibility: public export
Constructor:

MkMerkleDamgard : Vect internal_state_nbyte word_type -> (buffer_nbyte : Nat) -> LT buffer_nbyte block_nbyte -> Vect buffer_nbyte Bits8 -> Nat -> MerkleDamgard internal_state_nbyte block_nbyte word_type

Projections:

.buffer : ({rec:0} : MerkleDamgard internal_state_nbyte block_nbyte word_type) -> Vect (buffer_nbyte {rec:0}) Bits8
.buffer_nbyte : MerkleDamgard internal_state_nbyte block_nbyte word_type -> Nat
.buffer_nbyte_constraint : ({rec:0} : MerkleDamgard internal_state_nbyte block_nbyte word_type) -> LT (buffer_nbyte {rec:0}) block_nbyte
.hash_values : MerkleDamgard internal_state_nbyte block_nbyte word_type -> Vect internal_state_nbyte word_type
.npassed_blocks : MerkleDamgard internal_state_nbyte block_nbyte word_type -> Nat

.hash_values : MerkleDamgard internal_state_nbyte block_nbyte word_type -> Vect internal_state_nbyte word_type

Visibility: public export

hash_values : MerkleDamgard internal_state_nbyte block_nbyte word_type -> Vect internal_state_nbyte word_type

Visibility: public export

.buffer_nbyte : MerkleDamgard internal_state_nbyte block_nbyte word_type -> Nat

Visibility: public export

buffer_nbyte : MerkleDamgard internal_state_nbyte block_nbyte word_type -> Nat

Visibility: public export

.buffer_nbyte_constraint : ({rec:0} : MerkleDamgard internal_state_nbyte block_nbyte word_type) -> LT (buffer_nbyte {rec:0}) block_nbyte

Visibility: public export

buffer_nbyte_constraint : ({rec:0} : MerkleDamgard internal_state_nbyte block_nbyte word_type) -> LT (buffer_nbyte {rec:0}) block_nbyte

Visibility: public export

.buffer : ({rec:0} : MerkleDamgard internal_state_nbyte block_nbyte word_type) -> Vect (buffer_nbyte {rec:0}) Bits8

Visibility: public export

buffer : ({rec:0} : MerkleDamgard internal_state_nbyte block_nbyte word_type) -> Vect (buffer_nbyte {rec:0}) Bits8

Visibility: public export

.npassed_blocks : MerkleDamgard internal_state_nbyte block_nbyte word_type -> Nat

Visibility: public export

npassed_blocks : MerkleDamgard internal_state_nbyte block_nbyte word_type -> Nat

Visibility: public export

mk_merkle_damgard : Vect internal_state_nbyte word_type -> {auto 0 _ : LTE 1 block_nbyte} -> MerkleDamgard internal_state_nbyte block_nbyte word_type

Visibility: export

pad_lemma : LTE 1 block_nbyte -> (residue_max_nbyte + 1) + length_nbyte = block_nbyte -> LTE residue_nbyte residue_max_nbyte -> plus residue_nbyte (S (plus (minus residue_max_nbyte residue_nbyte) length_nbyte)) = block_nbyte

Visibility: public export

pad_over_lemma : (residue_max_nbyte + 1) + length_nbyte = block_nbyte -> LT residue_nbyte block_nbyte -> plus residue_nbyte (S (plus (plus (minus block_nbyte residue_nbyte) residue_max_nbyte) length_nbyte)) = plus block_nbyte (plus block_nbyte 0)

Visibility: public export

pad_residue : (0 _ : LTE 1 block_nbyte) -> (0 _ : (residue_max_nbyte + 1) + length_nbyte = block_nbyte) -> (0 _ : LTE residue_nbyte residue_max_nbyte) -> Vect residue_nbyte Bits8 -> Vect length_nbyte Bits8 -> Vect block_nbyte Bits8

Visibility: public export

pad_over_residue : (0 _ : LTE 1 block_nbyte) -> (0 _ : (residue_max_nbyte + 1) + length_nbyte = block_nbyte) -> (0 _ : LT residue_max_nbyte residue_nbyte) -> (0 _ : LT residue_nbyte block_nbyte) -> Vect residue_nbyte Bits8 -> Vect length_nbyte Bits8 -> Vect (2 * block_nbyte) Bits8

Visibility: public export

pad_theorem : (0 _ : LTE 1 block_nbyte) -> (0 _ : (residue_max_nbyte + 1) + length_nbyte = block_nbyte) -> (0 _ : LT residue_nbyte block_nbyte) -> Vect residue_nbyte Bits8 -> Vect length_nbyte Bits8 -> Either (Vect block_nbyte Bits8) (Vect (block_nbyte + block_nbyte) Bits8)

Visibility: public export