Abstract Idea of Merkle Trees

We provide minimal structure to model Merkle Trees specific to the proof protocol.

For a more complete definition check DataStructures.MerkleTree.Definitions.

inductive MerkleAxioms.MerkleTree : Type

axiom MerkleAxioms.value_tree {α : Type} : α → MerkleTree

axiom MerkleAxioms.list_tree {α : Type} : List α → MerkleTree

axiom MerkleAxioms.same_tree {α : Type} (ls rs : List α) : list_tree ls = list_tree rs → ls = rs

inductive MerkleAxioms.SidedPath : Type

• Left : MerkleTree → SidedPath
• Right : MerkleTree → SidedPath

@[reducible, inline]

abbrev MerkleAxioms.Path : Type

Equations

• MerkleAxioms.Path = List MerkleAxioms.SidedPath

axiom MerkleAxioms.is_valid_path {α : Type} (v : α) (path : Path) (m : MerkleTree) : Bool

axiom MerkleAxioms.pathMem {α : Type} (v : α) (ls : List α) (p : Path) : is_valid_path v p (list_tree ls) = true → v ∈ ls

inductive FullDataTree.BinHTree (α : Type) : Type

• Node {α : Type} : α → BinHTree α → BinHTree α → BinHTree α
• Leaf {α : Type} : α → BinHTree α

inductive ListSimulation.Path : Type

• Here : Path
• There : Path → Path

instance ListSimulation.instDecidableEqPath : DecidableEq Path

Equations

• ListSimulation.instDecidableEqPath = ListSimulation.instDecidableEqPath.decEq

def ListSimulation.instDecidableEqPath.decEq (x✝ x✝¹ : Path) : Decidable (x✝ = x✝¹)

Equations

• ListSimulation.instDecidableEqPath.decEq ListSimulation.Path.Here ListSimulation.Path.Here = isTrue ⋯
• ListSimulation.instDecidableEqPath.decEq ListSimulation.Path.Here a.There = isFalse ⋯
• ListSimulation.instDecidableEqPath.decEq a.There ListSimulation.Path.Here = isFalse ⋯
• ListSimulation.instDecidableEqPath.decEq a.There b.There = if h : a = b then h ▸ have inst := ListSimulation.instDecidableEqPath.decEq a a; isTrue ⋯ else isFalse ⋯

def ListSimulation.Path.add (n : ℕ) (p : Path) : Path

Equations

• ListSimulation.Path.add Nat.zero p = p
• ListSimulation.Path.add pn.succ p = ListSimulation.Path.add pn p.There

theorem ListSimulation.path_add_there {n : ℕ} {p : Path} : Path.add n p.There = Path.add n.succ p

theorem ListSimulation.path_add_there' {n : ℕ} {p : Path} : Path.add n p.There = (Path.add n p).There

def ListSimulation.path_minus (p q : Path) : Path

Equations

• ListSimulation.path_minus p'.There q'.There = ListSimulation.path_minus p' q'
• ListSimulation.path_minus ListSimulation.Path.Here q = ListSimulation.Path.Here
• ListSimulation.path_minus p ListSimulation.Path.Here = p

theorem ListSimulation.path_minus_self {p : Path} : path_minus p p = Path.Here

theorem ListSimulation.path_minus_zero {p : Path} : path_minus p Path.Here = p

theorem ListSimulation.path_minus_there_there {p q : Path} : path_minus p q = path_minus p.There q.There

theorem ListSimulation.path_minus_self_there {p : Path} : path_minus p.There p = Path.Here.There

theorem ListSimulation.path_add_minus_self {p : Path} {n : ℕ} : path_minus (Path.add n p) p = Path.add n Path.Here

def ListSimulation.pathToIdx (p : Path) : ℕ

Equations

• ListSimulation.pathToIdx pn.There = (ListSimulation.pathToIdx pn).succ
• ListSimulation.pathToIdx ListSimulation.Path.Here = 0

def ListSimulation.check_valid_path {α : Type} [DecidableEq α] (v : α) (p : Path) (ls : List α) : Bool

Equations

• ListSimulation.check_valid_path v ListSimulation.Path.Here (l :: _ls) = decide (v = l)
• ListSimulation.check_valid_path v rs.There (head :: ls_2) = ListSimulation.check_valid_path v rs ls_2
• ListSimulation.check_valid_path v p ls = false

theorem ListSimulation.validProof {α : Type} [DecidableEq α] (v : α) (p : Path) (ls : List α) : (check_valid_path v p ls == true) = true → v ∈ ls

theorem ListSimulation.validProof' {α : Type} [DecidableEq α] {v : α} {ls : List α} (vin : v ∈ ls) : ∃ (p : Path), (check_valid_path v p ls == true) = true

def ListSimulation.less_than (l r : Path) : Prop

Equations

• ListSimulation.less_than ListSimulation.Path.Here r = True
• ListSimulation.less_than ls.There rs.There = ListSimulation.less_than ls rs
• ListSimulation.less_than l r = False

def ListSimulation.next_in_path (l r : Path) : Prop

Equations

• ListSimulation.next_in_path l r = (r = l.There)

def ListSimulation.is_next (l r : Path) : Bool

Equations

• ListSimulation.is_next l r = (r == l.There)

def ListSimulation.first_in_path (p : Path) : Prop

Equations

• ListSimulation.first_in_path p = (p = ListSimulation.Path.Here)

def ListSimulation.check_last_in_path {α : Type} (p : Path) (ls : List α) : Bool

Equations

• ListSimulation.check_last_in_path p'.There (head :: ls') = ListSimulation.check_last_in_path p' ls'
• ListSimulation.check_last_in_path ListSimulation.Path.Here [head] = true
• ListSimulation.check_last_in_path p ls = false

def ListSimulation.last_path_in_list {α : Type} (l : List α) : Path

Equations

• ListSimulation.last_path_in_list l = List.foldl (fun (p : ListSimulation.Path) (x : α) => p.There) ListSimulation.Path.Here l

inductive ListSimulation.NonMemProof (α : Type) : Type

• NonMemFirst {α : Type} : α → Path → NonMemProof α
• NonMemLast {α : Type} : α → Path → NonMemProof α
• NonBetween {α : Type} : α → Path → α → Path → NonMemProof α

def ListSimulation.minus_path_non_mem {α : Type} (p : Path) (nm : NonMemProof α) : NonMemProof α

Equations

• ListSimulation.minus_path_non_mem p (ListSimulation.NonMemProof.NonMemFirst a p') = ListSimulation.NonMemProof.NonMemFirst a (ListSimulation.path_minus p' p)
• ListSimulation.minus_path_non_mem p (ListSimulation.NonMemProof.NonMemLast a p') = ListSimulation.NonMemProof.NonMemLast a (ListSimulation.path_minus p' p)
• ListSimulation.minus_path_non_mem p (ListSimulation.NonMemProof.NonBetween a ap b bp) = ListSimulation.NonMemProof.NonBetween a (ListSimulation.path_minus ap p) b (ListSimulation.path_minus bp p)

theorem ListSimulation.minus_path_non_mem_here {α : Type} {wit : NonMemProof α} : minus_path_non_mem Path.Here wit = wit

def ListSimulation.check_non_membership {α : Type} [LinearOrder α] (wit : NonMemProof α) (elem : α) (ls : List α) (_ls_non_empty : ¬ls = []) : Bool

Equations

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

axiom ListSimulation.validProofNonMem {α : Type} [LinearOrder α] {wit : NonMemProof α} {e : α} {ls : List α} (ls_nempty : ¬ls = []) (lsS : List.Sorted (fun (x1 x2 : α) => x1 < x2) ls) (mem : (check_non_membership wit e ls ls_nempty == true) = true) : e ∉ ls

axiom ListSimulation.validProofNonMem' {α : Type} [t : LinearOrder α] {e : α} {ls : List α} (ls_nempty : ¬ls = []) (lsS : List.Sorted (fun (x1 x2 : α) => x1 < x2) ls) (ein : e ∉ ls) : ∃ (wit : NonMemProof α), (check_non_membership wit e ls ls_nempty == true) = true

def SparseTrees.SPTree (α : Type) : Type

Equations

• SparseTrees.SPTree α = (α → Bool)