Hash Definition Module

class MixableHash (α : Type u) (ℍ : Type v) : Type (max u v)

• hash : α → ℍ
• mix : ℍ → ℍ → ℍ

def hash_32 (α : Type u) : Type u

Equations

• hash_32 α = (α → Hash_32)

def HashMix_32 : Type

Equations

• HashMix_32 = (Hash_32 → Hash_32 → Hash_32)

def hash_64 (α : Type u) : Type u

Equations

• hash_64 α = (α → Hash_64)

def hashmix_64 : Type

Equations

• hashmix_64 = (Hash_64 → Hash_64 → Hash_64)

axiom blake2b_512 : ByteArray → Hash_64

axiom blake2b_256 : ByteArray → Hash_32

axiom blake2b_224 : ByteArray → Hash_28

noncomputable instance instMixableHashHash_28OfSerializable {α : Type} [o : Serializable α] : MixableHash α Hash_28

Equations

• instMixableHashHash_28OfSerializable = { hash := blake2b_224 ∘ Serializable.serialize, mix := fun (a b : Hash_28) => blake2b_224 { data := (Vector.append a b).toArray } }

noncomputable instance instMixableHashHash_32OfSerializable {α : Type} [o : Serializable α] : MixableHash α Hash_32

Equations

• instMixableHashHash_32OfSerializable = { hash := blake2b_256 ∘ Serializable.serialize, mix := fun (a b : Hash_32) => blake2b_256 { data := (Vector.append a b).toArray } }

@[reducible, inline]

abbrev NHash : Type

Equations

• NHash = Nat