structure Cryptlib.Primitives.Hash.Sha2.Sha256.Digest : Type

• h0 : UInt32
• h1 : UInt32
• h2 : UInt32
• h3 : UInt32
• h4 : UInt32
• h5 : UInt32
• h6 : UInt32
• h7 : UInt32

@[instance_reducible]

instance Cryptlib.Primitives.Hash.Sha2.Sha256.instBEqDigest : BEq Digest

Equations

• Cryptlib.Primitives.Hash.Sha2.Sha256.instBEqDigest = { beq := Cryptlib.Primitives.Hash.Sha2.Sha256.instBEqDigest.beq }

def Cryptlib.Primitives.Hash.Sha2.Sha256.instBEqDigest.beq : Digest → Digest → Bool

Equations

• One or more equations did not get rendered due to their size.
• Cryptlib.Primitives.Hash.Sha2.Sha256.instBEqDigest.beq x✝¹ x✝ = false

def Cryptlib.Primitives.Hash.Sha2.Sha256.Digest.new (h0 h1 h2 h3 h4 h5 h6 h7 : UInt32) : Digest

Equations

• Cryptlib.Primitives.Hash.Sha2.Sha256.Digest.new h0 h1 h2 h3 h4 h5 h6 h7 = { h0 := h0, h1 := h1, h2 := h2, h3 := h3, h4 := h4, h5 := h5, h6 := h6, h7 := h7 }

@[instance_reducible]

instance Cryptlib.Primitives.Hash.Sha2.Sha256.instInhabitedDigest : Inhabited Digest

Equations

• Cryptlib.Primitives.Hash.Sha2.Sha256.instInhabitedDigest = { default := Cryptlib.Primitives.Hash.Sha2.Sha256.Digest.new 0 0 0 0 0 0 0 0 }

def Cryptlib.Primitives.Hash.Sha2.Sha256.Digest.add (d1 d2 : Digest) : Digest

Equations

• d1.add d2 = { h0 := d1.h0 + d2.h0, h1 := d1.h1 + d2.h1, h2 := d1.h2 + d2.h2, h3 := d1.h3 + d2.h3, h4 := d1.h4 + d2.h4, h5 := d1.h5 + d2.h5, h6 := d1.h6 + d2.h6, h7 := d1.h7 + d2.h7 }

def Cryptlib.Primitives.Hash.Sha2.Sha256.Digest.xor (d1 d2 : Digest) : Digest

Equations

• One or more equations did not get rendered due to their size.

def Cryptlib.Primitives.Hash.Sha2.Sha256.Digest.ofArray (d : Array UInt32) : Digest

Equations

• Cryptlib.Primitives.Hash.Sha2.Sha256.Digest.ofArray d = Cryptlib.Primitives.Hash.Sha2.Sha256.Digest.new d[0]! d[1]! d[2]! d[3]! d[4]! d[5]! d[6]! d[7]!

def Cryptlib.Primitives.Hash.Sha2.Sha256.Digest.ofSubarray (d : Subarray UInt32) : Digest

Equations

• Cryptlib.Primitives.Hash.Sha2.Sha256.Digest.ofSubarray d = Cryptlib.Primitives.Hash.Sha2.Sha256.Digest.new d[0]! d[1]! d[2]! d[3]! d[4]! d[5]! d[6]! d[7]!

def Cryptlib.Primitives.Hash.Sha2.Sha256.Digest.toArray (d : Digest) : Array UInt32

Equations

• d.toArray = #[d.h0, d.h1, d.h2, d.h3, d.h4, d.h5, d.h6, d.h7]

def Cryptlib.Primitives.Hash.Sha2.Sha256.Digest.toSubarray (d : Digest) : Subarray UInt32

Equations

• d.toSubarray = d.toArray.toSubarray

def Cryptlib.Primitives.Hash.Sha2.Sha256.Digest.toBytes (d : Digest) : ByteArray

Equations

• One or more equations did not get rendered due to their size.

def Cryptlib.Primitives.Hash.Sha2.Sha256.init_hash : Digest

Equations

• One or more equations did not get rendered due to their size.

def Cryptlib.Primitives.Hash.Sha2.Sha256.round_constants : Array UInt32

Equations

• One or more equations did not get rendered due to their size.

def Cryptlib.Primitives.Hash.Sha2.Sha256.Nat.to_be64 (x : Nat) : ByteArray

Equations

• One or more equations did not get rendered due to their size.

def Cryptlib.Primitives.Hash.Sha2.Sha256.prepare (msg : ByteArray) : Array UInt32

Equations

• One or more equations did not get rendered due to their size.

def Cryptlib.Primitives.Hash.Sha2.Sha256.to_chunks (msg : Array UInt32) : List (Array UInt32)

Equations

• One or more equations did not get rendered due to their size.

def Cryptlib.Primitives.Hash.Sha2.Sha256.schedule (message : Array UInt32) : Array UInt32

Equations

• One or more equations did not get rendered due to their size.

def Cryptlib.Primitives.Hash.Sha2.Sha256.compress_loop (chunk : Array UInt32) (state : Digest) : Digest

Equations

• One or more equations did not get rendered due to their size.

def Cryptlib.Primitives.Hash.Sha2.Sha256.compress (chunk : Array UInt32) (h : Digest) : Digest

Equations

• One or more equations did not get rendered due to their size.

def Cryptlib.Primitives.Hash.Sha2.Sha256.hash (msg : ByteArray) : { out : ByteArray // out.size = 32 }

Equations

• One or more equations did not get rendered due to their size.

def Cryptlib.Primitives.Hash.Sha2.Sha256.Scheme : Hash.Hash

SHA-256 as a Hash: accumulate the message, hash at finalize.

Equations

• One or more equations did not get rendered due to their size.