@[instance_reducible]

instance Cryptlib.Data.MerkleHashTree.instBEqByteArray_cryptlib : BEq ByteArray

Equations

• Cryptlib.Data.MerkleHashTree.instBEqByteArray_cryptlib = { beq := fun (a b : ByteArray) => decide (a.data = b.data) }

@[instance_reducible]

instance Cryptlib.Data.MerkleHashTree.instHashableByteArray_cryptlib : Hashable ByteArray

Equations

• Cryptlib.Data.MerkleHashTree.instHashableByteArray_cryptlib = { hash := fun (a : ByteArray) => hash a.data }

Settings for Merkle Hash Trees.

structure Cryptlib.Data.MerkleHashTree.Settings (α : Type) [Hashable α] : Type

• hash0 : ByteArray
• hash1 : α → ByteArray
• hash2 : ByteArray → ByteArray → ByteArray

def Cryptlib.Data.MerkleHashTree.sha256HashByteArraySettings : Settings ByteArray

Equations

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

inductive Cryptlib.Data.MerkleHashTree.HashTree (α : Type) : Type

• empty {α : Type} (hash : ByteArray) : HashTree α
• leaf {α : Type} (hash : ByteArray) (index : ℕ) (value : α) : HashTree α
• node {α : Type} (hash : ByteArray) (leftIndex rightIndex : ℕ) (leftTree rightTree : HashTree α) : HashTree α

def Cryptlib.Data.MerkleHashTree.instBEqHashTree.beq {α✝ : Type} [BEq α✝] : HashTree α✝ → HashTree α✝ → Bool

Equations

• One or more equations did not get rendered due to their size.
• Cryptlib.Data.MerkleHashTree.instBEqHashTree.beq (Cryptlib.Data.MerkleHashTree.HashTree.empty a) (Cryptlib.Data.MerkleHashTree.HashTree.empty b) = (a == b)
• Cryptlib.Data.MerkleHashTree.instBEqHashTree.beq x✝¹ x✝ = false

@[instance_reducible]

instance Cryptlib.Data.MerkleHashTree.instBEqHashTree {α✝ : Type} [BEq α✝] : BEq (HashTree α✝)

Equations

• Cryptlib.Data.MerkleHashTree.instBEqHashTree = { beq := Cryptlib.Data.MerkleHashTree.instBEqHashTree.beq }

def Cryptlib.Data.MerkleHashTree.reprHashTree {α : Type} [Repr α] (tree : HashTree α) (indent : String) (last : Bool) : String

Equations

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

@[instance_reducible]

instance Cryptlib.Data.MerkleHashTree.instInhabitedHashTree {α : Type} : Inhabited (HashTree α)

Equations

• Cryptlib.Data.MerkleHashTree.instInhabitedHashTree = { default := Cryptlib.Data.MerkleHashTree.HashTree.empty { data := #[] } }

structure Cryptlib.Data.MerkleHashTree.MerkleHashTrees (α : Type) [Hashable α] : Type

• settings : Settings α
• size : ℕ
• hashtrees : Std.HashMap ℕ (HashTree α)
• indices : Std.HashMap ByteArray ℕ

The current Merkle tree head.

def Cryptlib.Data.MerkleHashTree.currentHead (α : Type) [Hashable α] (tree : MerkleHashTrees α) : HashTree α

Equations

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

def Cryptlib.Data.MerkleHashTree.printHashTree {α : Type} [Repr α] (tree : HashTree α) : IO Unit

Equations

• Cryptlib.Data.MerkleHashTree.printHashTree tree = IO.println (toString "hashTree\n" ++ toString (Cryptlib.Data.MerkleHashTree.reprHashTree tree " " false))

def Cryptlib.Data.MerkleHashTree.printMerkleHashTrees {α : Type} [Repr α] [Hashable α] (mht : MerkleHashTrees α) : IO Unit

Equations

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

The current Merkle tree hash.

def Cryptlib.Data.MerkleHashTree.digest (α : Type) [Hashable α] (treeSize : ℕ) (tree : MerkleHashTrees α) : ByteArray

Equations

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

def Cryptlib.Data.MerkleHashTree.index (α : Type) [Hashable α] (tree : MerkleHashTrees α) (hash : ByteArray) : ℕ

Equations

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

The current size and Merkle tree hash.

def Cryptlib.Data.MerkleHashTree.info (α : Type) [Hashable α] (tree : MerkleHashTrees α) : ℕ × ByteArray

Equations

• Cryptlib.Data.MerkleHashTree.info α tree = (tree.size, Cryptlib.Data.MerkleHashTree.digest α tree.size tree)

An empty tree.

def Cryptlib.Data.MerkleHashTree.empty (α : Type) [Hashable α] (settings : Settings α) : MerkleHashTrees α

Equations

• Cryptlib.Data.MerkleHashTree.empty α settings = { settings := settings, size := 0, hashtrees := ∅.insert 0 (Cryptlib.Data.MerkleHashTree.HashTree.empty settings.hash0), indices := ∅ }

The hash value of a HashTree.

def Cryptlib.Data.MerkleHashTree.hashValue (α : Type) [Hashable α] (tree : HashTree α) : ByteArray

Equations

• Cryptlib.Data.MerkleHashTree.hashValue α (Cryptlib.Data.MerkleHashTree.HashTree.empty hash) = hash
• Cryptlib.Data.MerkleHashTree.hashValue α (Cryptlib.Data.MerkleHashTree.HashTree.leaf hash index value) = hash
• Cryptlib.Data.MerkleHashTree.hashValue α (Cryptlib.Data.MerkleHashTree.HashTree.node hash leftIndex rightIndex leftTree rightTree) = hash

def Cryptlib.Data.MerkleHashTree.rIndex (α : Type) (tree : HashTree α) : ℕ

Equations

• One or more equations did not get rendered due to their size.
• Cryptlib.Data.MerkleHashTree.rIndex α (Cryptlib.Data.MerkleHashTree.HashTree.leaf hash index value) = index
• Cryptlib.Data.MerkleHashTree.rIndex α (Cryptlib.Data.MerkleHashTree.HashTree.node hash leftIndex rightIndex leftTree rightTree) = rightIndex

def Cryptlib.Data.MerkleHashTree.lIndex (α : Type) (tree : HashTree α) : ℕ

Equations

• One or more equations did not get rendered due to their size.
• Cryptlib.Data.MerkleHashTree.lIndex α (Cryptlib.Data.MerkleHashTree.HashTree.leaf hash index value) = index
• Cryptlib.Data.MerkleHashTree.lIndex α (Cryptlib.Data.MerkleHashTree.HashTree.node hash leftIndex rightIndex leftTree rightTree) = leftIndex

def Cryptlib.Data.MerkleHashTree.isPowerOf2 (n : ℕ) : Bool

Equations

• Cryptlib.Data.MerkleHashTree.isPowerOf2 n = (n &&& n - 1 == 0)

Adds an input to the tree.

def Cryptlib.Data.MerkleHashTree.add (α : Type) [Hashable α] (inp : α) (tree : MerkleHashTrees α) : MerkleHashTrees α

Equations

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

def Cryptlib.Data.MerkleHashTree.add.insert (α : Type) [Hashable α] (inp : α) (tree : MerkleHashTrees α) (ht : HashTree α) : HashTree α

Equations

• One or more equations did not get rendered due to their size.
• Cryptlib.Data.MerkleHashTree.add.insert α inp tree (Cryptlib.Data.MerkleHashTree.HashTree.empty hash) = Cryptlib.Data.MerkleHashTree.HashTree.leaf (tree.settings.hash1 inp) tree.size inp

Adds a list of inputs to the tree.

def Cryptlib.Data.MerkleHashTree.fromList (α : Type) [Hashable α] (settings : Settings α) (xs : List α) : MerkleHashTrees α

Equations

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

structure Cryptlib.Data.MerkleHashTree.InclusionProof : Type

• index : ℕ
• treeSize : ℕ
• proof : List ByteArray

@[instance_reducible]

instance Cryptlib.Data.MerkleHashTree.instBEqInclusionProof : BEq InclusionProof

Equations

• Cryptlib.Data.MerkleHashTree.instBEqInclusionProof = { beq := Cryptlib.Data.MerkleHashTree.instBEqInclusionProof.beq }

def Cryptlib.Data.MerkleHashTree.instBEqInclusionProof.beq : InclusionProof → InclusionProof → Bool

Equations

• Cryptlib.Data.MerkleHashTree.instBEqInclusionProof.beq { index := a, treeSize := a_1, proof := a_2 } { index := b, treeSize := b_1, proof := b_2 } = (a == b && (a_1 == b_1 && a_2 == b_2))
• Cryptlib.Data.MerkleHashTree.instBEqInclusionProof.beq x✝¹ x✝ = false

@[instance_reducible]

instance Cryptlib.Data.MerkleHashTree.instToStringInclusionProof : ToString InclusionProof

Equations

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

@[instance_reducible]

instance Cryptlib.Data.MerkleHashTree.instInhabitedInclusionProof : Inhabited InclusionProof

Equations

• Cryptlib.Data.MerkleHashTree.instInhabitedInclusionProof = { default := { treeSize := 0 } }

def Cryptlib.Data.MerkleHashTree.sizeTree (α : Type) [Hashable α] (tree : MerkleHashTrees α) (treeSize : ℕ) : HashTree α

Equations

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

def Cryptlib.Data.MerkleHashTree.generateInclusionProof (α : Type) [Hashable α] (targetHash : ByteArray) (treeSize : ℕ) (tree : MerkleHashTrees α) : Option InclusionProof

Equations

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

def Cryptlib.Data.MerkleHashTree.generateInclusionProof.path (α : Type) [Hashable α] (index : ℕ) (tree : HashTree α) : List ByteArray

Equations

• One or more equations did not get rendered due to their size.
• Cryptlib.Data.MerkleHashTree.generateInclusionProof.path α index (Cryptlib.Data.MerkleHashTree.HashTree.empty hash) = []
• Cryptlib.Data.MerkleHashTree.generateInclusionProof.path α index (Cryptlib.Data.MerkleHashTree.HashTree.leaf hash index_1 value) = []

def Cryptlib.Data.MerkleHashTree.shiftR1 (p : ℕ × ℕ) : ℕ × ℕ

Equations

• Cryptlib.Data.MerkleHashTree.shiftR1 p = (p.1 >>> 1, p.2 >>> 1)

@[irreducible]

def Cryptlib.Data.MerkleHashTree.untilSet (fst snd : ℕ) : ℕ × ℕ

Equations

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

def Cryptlib.Data.MerkleHashTree.verifyInclusionProof (α : Type) [Hashable α] (settings : Settings α) (leafHash rootHash : ByteArray) (proof : InclusionProof) : Bool

Equations

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

def Cryptlib.Data.MerkleHashTree.verifyInclusionProof.verify (α : Type) [Hashable α] (settings : Settings α) (rootHash : ByteArray) (index treeSize : ℕ) (currentHash : ByteArray) (proof' : List ByteArray) : Bool

Equations

• One or more equations did not get rendered due to their size.
• Cryptlib.Data.MerkleHashTree.verifyInclusionProof.verify α settings rootHash index treeSize currentHash [] = (treeSize == 0 && currentHash == rootHash)
• Cryptlib.Data.MerkleHashTree.verifyInclusionProof.verify α settings rootHash index 0 currentHash proof' = false