1.5. Octet Sequences🔗

Fixed-length byte strings Y_n are modeled as a ByteArray bundled with a size proof.

structure

OctetSeq (n : Nat) : Type
OctetSeq (n : Nat) : Type

𝔹_n : octet strings of exactly n bytes. GP §3.7.4.

Constructor

OctetSeq.mk

data : ByteArray

size_eq : self.data.size = n

The 256-bit hash type H is OctetSeq 32.

def

Hash : Type
Hash : Type

ℍ ≡ 𝔹_32 : 256-bit hash values. GP §3.8.1.

def

Hash.zero : Hash
Hash.zero : Hash

ℍ_0 : the zero hash, [0]_32. GP §3.8.1.