@[reducible, inline]

abbrev MTree (ℍ : Type) : Type

Equations

• MTree ℍ = ℍ

def comb_MTree {ℍ : Type} [m : HashMagma ℍ] : MTree ℍ → MTree ℍ → MTree ℍ

Equations

• comb_MTree = m.comb

def BTree.hash_BTree {α ℍ : Type} [o : Hash α ℍ] [HashMagma ℍ] : BTree α → MTree ℍ

Equations

• t.hash_BTree = BTree.fold o.mhash comb_MTree t

def ABTree.hash_Tree {α ℍ : Type} [o : Hash α ℍ] [m : HashMagma ℍ] : BTree α → ABTree α ℍ

Equations

• ABTree.hash_Tree = ABTree.fold ABTree.leaf fun (x : Unit) (sl sr : ABTree α ℍ) => ABTree.node (m.comb (ABTree.getI' o.mhash id sl) (ABTree.getI' o.mhash id sr)) sl sr

def ABTree.hash_SubTree {α ℍ : Type} [o : Hash α ℍ] [m : HashMagma ℍ] : BTree α → ABTree α (ℍ × ℍ)

Equations

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

structure MkData (ℍ : Type) : Type

• top : ℍ
• left : ℍ
• right : ℍ

def ABTree.merkle_root {α ℍ : Type} [o : Hash α ℍ] : ABTree α (MkData ℍ) → ℍ

Equations

• ABTree.merkle_root = ABTree.getI' o.mhash fun (x : MkData ℍ) => x.top

def ABTree.hash_MKSubts {α ℍ : Type} [Hash α ℍ] [m : HashMagma ℍ] : BTree α → ABTree α (MkData ℍ)

Equations

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

def hashM {α ℍ : Type} {m : Type → Type} [Monad m] (hL : α → m ℍ) (hC : ℍ → ℍ → m ℍ) (t : BTree α) : m (MTree ℍ)

Equations

• hashM hL hC (ABTree.leaf v) = hL v
• hashM hL hC (ABTree.node PUnit.unit nL nR) = do let l ← hashM hL hC nL let r ← hashM hL hC nR hC l r

inductive SkElem : Type

• Left : SkElem
• Right : SkElem

instance instBEqSkElem : BEq SkElem

Equations

• instBEqSkElem = { beq := fun (l r : SkElem) => match l, r with | SkElem.Left, SkElem.Left => true | SkElem.Right, SkElem.Right => true | x, x_1 => false }

instance instLawfulBEqSkElem : LawfulBEq SkElem

def SkElem.destruct {α : Type} (s : SkElem) (l r : α) : α

Equations

• SkElem.Left.destruct l r = l
• SkElem.Right.destruct l r = r

@[reducible, inline]

abbrev Skeleton : Type

Equations

• Skeleton = List SkElem

@[reducible, inline]

abbrev ISkeleton (n : ℕ) : Type

Equations

• ISkeleton n = Sequence n SkElem

def ABTree.find_left {α β : Type} (is : α → Bool) : ABTree α β → Option (List (SkElem × (α ⊕ β)))

Equations

• One or more equations did not get rendered due to their size.
• ABTree.find_left is (ABTree.leaf v) = if is v = true then some [] else none

def ABTree.gen_path_elem_forward {α β γ : Type} {n : ℕ} (t : ABTree α β) (ag : α → γ) (bg : β → γ) (p : Sequence n SkElem) : Option (α × Sequence n (γ × γ))

Equations

• One or more equations did not get rendered due to their size.
• (ABTree.leaf v).gen_path_elem_forward ag bg p_2 = some (v, Sequence.nil)
• t.gen_path_elem_forward ag bg p = none

def op_side {ℍ : Type} [mag : HashMagma ℍ] (side : SkElem) (a b : ℍ) : ℍ

Equations

• op_side SkElem.Left a b = mag.comb a b
• op_side SkElem.Right a b = mag.comb b a

theorem opHash_neqRight {ℍ : Type} [HashMagma ℍ] [lHStr : SLawFulHash ℍ] {hl hr pl pr : ℍ} : ¬hl = hr → ¬op_side SkElem.Right hl pl = op_side SkElem.Right hr pr

theorem opHash_neqLeft {ℍ : Type} [HashMagma ℍ] [lHStr : SLawFulHash ℍ] {hl hr pl pr : ℍ} : ¬hl = hr → ¬op_side SkElem.Left hl pl = op_side SkElem.Left hr pr

def listPathHashes {ℍ : Type} [HashMagma ℍ] (h : ℍ) (path : List (SkElem × ℍ)) : ℍ

Equations

• listPathHashes h path = List.foldl (fun (h : ℍ) (x : SkElem × ℍ) => match x with | (s, l) => op_side s h l) h path

def nodeIn {ℍ : Type} [BEq ℍ] [HashMagma ℍ] (h : ℍ) (path : List (SkElem × ℍ)) (t : MTree ℍ) : Bool

Equations

• nodeIn h path t = (listPathHashes h path == t)

def containCompute {α ℍ : Type} [BEq ℍ] [o : Hash α ℍ] [HashMagma ℍ] (v : α) (path : List (SkElem × ℍ)) (t : MTree ℍ) : Bool

Equations

• containCompute v path t = nodeIn (o.mhash v) path t

theorem leftChildContaintionN {α ℍ : Type} [BEq ℍ] [LawfulBEq ℍ] [Hash α ℍ] [HashMagma ℍ] (v : α) (h : ℍ) (btR broot : BTree α) : broot = (BTree.leaf v).node btR → h = btR.hash_BTree → containCompute v [(SkElem.Left, h)] broot.hash_BTree = true

theorem rightChildContaintionN {α ℍ : Type} [BEq ℍ] [LawfulBEq ℍ] [Hash α ℍ] [HashMagma ℍ] (v : α) (h : ℍ) (btL broot : BTree α) : broot = btL.node (BTree.leaf v) → h = btL.hash_BTree → containCompute v [(SkElem.Right, h)] broot.hash_BTree = true

theorem leafChildContaintionN {α ℍ : Type} [BEq ℍ] [LawfulBEq ℍ] [Hash α ℍ] [HashMagma ℍ] (v : α) (broot : BTree α) : broot = BTree.leaf v → containCompute v [] broot.hash_BTree = true