Script Definition

Script here is a list of steps, stateful computations that may fail. Eventually, we also need them to signal when they've ended, so the Computation Thread knows when to end.

inductive ScriptsDefinition.Ended (α : Type) : Type

Script definition. Defines how computations threads are initialized and steps to proceed.

• Un {α : Type} : α → Ended α
• Err {α : Type} : Ended α
• Ed {α : Type} : Ended α

@[reducible, inline]

abbrev ScriptsDefinition.StepM (α β : Type) : Type

Equations

• ScriptsDefinition.StepM α β = (α → β → ScriptsDefinition.Ended α)

@[reducible, inline]

abbrev ScriptsDefinition.CompM (α β : Type) : Type

Equations

• ScriptsDefinition.CompM α β = List (ScriptsDefinition.StepM α β)

structure ScriptsDefinition.Script (κ α β : Type) : Type

• init : κ → α
• steps : CompM α β

def ScriptsDefinition.cond_lift {α β : Type} (f : α → β → Bool) : StepM α β

Equations

• ScriptsDefinition.cond_lift f st b = if f st b = true then ScriptsDefinition.Ended.Un st else ScriptsDefinition.Ended.Err

def ScriptsDefinition.last_step {α β : Type} : StepM α β

Equations

• ScriptsDefinition.last_step x✝¹ x✝ = ScriptsDefinition.Ended.Ed

def ScriptsDefinition.last_step_comb {α β : Type} (step : StepM α β) : StepM α β

Equations

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

def ScriptsDefinition.runCompM {α β : Type} (st : α) (steps : CompM α β) (ins : List β) : Ended (Option α)

Equations

• One or more equations did not get rendered due to their size.
• ScriptsDefinition.runCompM st [] [] = ScriptsDefinition.Ended.Un (some st)
• ScriptsDefinition.runCompM st steps ins = ScriptsDefinition.Ended.Un none

def ScriptsDefinition.Execution {κ α β : Type} (scr : Script κ α β) (init : κ) (ins : List β) : Ended (Option α)

Equations

• ScriptsDefinition.Execution scr init ins = ScriptsDefinition.runCompM (scr.init init) scr.steps ins

def ScriptsDefinition.SuccessfulEx {κ α β : Type} (scr : Script κ α β) (init : κ) (ins : List β) : Bool

Equations

• ScriptsDefinition.SuccessfulEx scr init ins = match ScriptsDefinition.Execution scr init ins with | ScriptsDefinition.Ended.Ed => true | x => false

inductive ScriptsDefinition.MPTOps (ε ℍ : Type) : Type

• Membership {ε ℍ : Type} : ε → ℍ → MPTOps ε ℍ
• NonMembership {ε ℍ : Type} : ε → ℍ → MPTOps ε ℍ

List Operations

Before implementing Merkle Trees, we can implement everthing using Lists.

The main difference is that when we search for elements, we need to provide a witness, i.e. a path, along with the corresponding element.

def ListWitness.listIndex {α : Type} (p : ListSimulation.Path) (ls : List α) : Option α

Equations

• ListWitness.listIndex ListSimulation.Path.Here (h :: tail) = some h
• ListWitness.listIndex p'.There (head :: l) = ListWitness.listIndex p' l
• ListWitness.listIndex p [] = none

theorem ListWitness.check_path_same_index {α : Type} [DecidableEq α] {v : α} {p : ListSimulation.Path} {ls : List α} : ListSimulation.check_valid_path v p ls = true ↔ listIndex p ls = some v

theorem ListWitness.check_path_same_index_other {α : Type} [DecidableEq α] {v v' : α} {p : ListSimulation.Path} {ls : List α} : ListSimulation.check_valid_path v p ls = false ↔ listIndex p ls = some v' ∧ ¬v = v'

theorem ListWitness.check_path_same_index' {α : Type} [DecidableEq α] {v : α} {p : ListSimulation.Path} {ls : List α} : ListSimulation.check_valid_path v p ls = false ↔ listIndex p ls = none

theorem ListWitness.listIndex_cons {α : Type} {ls : List α} {a : α} {p : ListSimulation.Path} (h : α) (H : listIndex p ls = some a) : listIndex p.There (h :: ls) = some a

theorem ListWitness.listIndex_path_minus {α : Type} {q : ListSimulation.Path} {ls : List α} {a : α} {n : ℕ} (h : α) (H : listIndex (ListSimulation.path_minus (ListSimulation.Path.add n q.There) q.There) ls = some a) : listIndex (ListSimulation.path_minus (ListSimulation.Path.add n q.There) q) (h :: ls) = some a

def ListWitness.findWitness?' {α β : Type} (f : α → Option β) (as : List α) (acc : ListSimulation.Path) : Option (β × ListSimulation.Path)

Equations

• ListWitness.findWitness?' f [] acc = none
• ListWitness.findWitness?' f (b :: bs) acc = match f b with | some v => some (v, acc) | none => ListWitness.findWitness?' f bs acc.There

theorem ListWitness.findWitness_path_add {α β : Type} {b : β} {f : α → Option β} {as : List α} {acc path : ListSimulation.Path} (H : findWitness?' f as acc = some (b, path)) : ∃ (n : ℕ), ListSimulation.Path.add n acc = path

@[reducible, inline]

abbrev ListWitness.findWitness? {α β : Type} (f : α → Option β) (as : List α) : Option (β × ListSimulation.Path)

Equations

• ListWitness.findWitness? f as = ListWitness.findWitness?' f as ListSimulation.Path.Here

def ListWitness.findWitnessB {α : Type} (f : α → Bool) : List α → Option (α × ListSimulation.Path)

Equations

• ListWitness.findWitnessB f = ListWitness.findWitness? fun (v : α) => if f v = true then some v else none

theorem ListWitness.correctWitId {α : Type} [DecidableEq α] {path acc : ListSimulation.Path} {a a' : α} {as : List α} (H : findWitness?' (fun (a' : α) => if (a' == a) = true then some a' else none) as acc = some (a', path)) : (a == a') = true ∧ listIndex (ListSimulation.path_minus path acc) as = some a

theorem ListWitness.correctWit {α β : Type} {b : β} {path acc : ListSimulation.Path} {f : α → Option β} {as : List α} (H : findWitness?' f as acc = some (b, path)) : ∃ (a : α), listIndex (ListSimulation.path_minus path acc) as = some a ∧ f a = some b

theorem ListWitness.findWitness_none {α β : Type} {acc : ListSimulation.Path} {f : α → Option β} {as : List α} (H : findWitness?' f as acc = none) (a : α) (aIn : a ∈ as) : f a = none

theorem ListWitness.witness_path_less_length {α β : Type} {b : β} {path : ListSimulation.Path} {f : α → Option β} {as : List α} (H : findWitness? f as = some (b, path)) : ListSimulation.pathToIdx path < as.length

theorem ListWitness.witness_valid_path {α : Type} [DecidableEq α] {b : α} {path : ListSimulation.Path} (v : α) {as : List α} (H : findWitness? (fun (v' : α) => if (v == v') = true then some v else none) as = some (b, path)) : ListSimulation.check_valid_path v path as = true

def ListWitness.findNMWitness?' {α : Type} [LinearOrder α] (v prev : α) (acc : ListSimulation.Path) (as : List α) : Option (ListSimulation.NonMemProof α)

Equations

• One or more equations did not get rendered due to their size.
• ListWitness.findNMWitness?' v prev acc [] = some (ListSimulation.NonMemProof.NonMemLast prev acc)

def ListWitness.findNMWitness? {α : Type} [LinearOrder α] (v a : α) (as : List α) : Option (ListSimulation.NonMemProof α)

Equations

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

theorem ListWitness.findmem_none_nonmem {α : Type} [LinearOrder α] {v hd : α} {as : List α} (asLT : List.Sorted (fun (x1 x2 : α) => x1 < x2) (hd :: as)) (H : findNMWitness? v hd as = none) : (findWitness? (fun (v' : α) => if (v == v') = true then some v else none) (hd :: as)).isSome = true

theorem ListWitness.findnon_mem_none_find {α : Type} [LinearOrder α] {v hd : α} {as : List α} (asLT : List.Sorted (fun (x1 x2 : α) => x1 < x2) (hd :: as)) (H : (findWitness? (fun (v' : α) => if (v == v') = true then some v else none) (hd :: as)).isSome = true) : (findNMWitness? v hd as).isNone = true

theorem ListWitness.nonmem_find'_notfirst {α : Type} [LinearOrder α] {v hd t : α} {patht acc : ListSimulation.Path} {as : List α} {res : ListSimulation.NonMemProof α} (H : findNMWitness?' v hd acc as = some res) (t✝ : α) (path : ListSimulation.Path) : ¬res = ListSimulation.NonMemProof.NonMemFirst t✝ path

theorem ListWitness.nonmem_find'_last_or_between {α : Type} [LinearOrder α] {v hd : α} {acc : ListSimulation.Path} {as : List α} {res : ListSimulation.NonMemProof α} (H : findNMWitness?' v hd acc as = some res) : (∃ (t : α) (n : ℕ), res = ListSimulation.NonMemProof.NonMemLast t (ListSimulation.Path.add n acc)) ∨ ∃ (tl : α) (tr : α) (n : ℕ), res = ListSimulation.NonMemProof.NonBetween tl (ListSimulation.Path.add n acc) tr (ListSimulation.Path.add n.succ acc)

theorem ListWitness.findnon_mem_first {α : Type} [LinearOrder α] {v hd t : α} {patht : ListSimulation.Path} {as : List α} (H : findNMWitness? v hd as = some (ListSimulation.NonMemProof.NonMemFirst t patht)) : hd = t ∧ patht = ListSimulation.Path.Here ∧ v < hd

theorem ListWitness.findnon_mem_correct' {α : Type} [LinearOrder α] {v hd : α} {wit : ListSimulation.NonMemProof α} {acc : ListSimulation.Path} {as : List α} (lt : hd < v) (sort : List.Sorted (fun (x1 x2 : α) => x1 < x2) (hd :: as)) (H : findNMWitness?' v hd acc as = some wit) : ListSimulation.check_non_membership (ListSimulation.minus_path_non_mem acc wit) v (hd :: as) ⋯ = true

theorem ListWitness.findnon_mem_correct {α : Type} [LinearOrder α] {v hd : α} {wit : ListSimulation.NonMemProof α} {as : List α} (sort : List.Sorted (fun (x1 x2 : α) => x1 < x2) (hd :: as)) (H : findNMWitness? v hd as = some wit) : ListSimulation.check_non_membership wit v (hd :: as) ⋯ = true

theorem ListWitness.non_mem_find {α : Type} [l : LinearOrder α] {v : α} {wit : ListSimulation.NonMemProof α} {as : List α} (ne : ¬as = []) (sort : List.Sorted (fun (x1 x2 : α) => x1 < x2) as) (H : ListSimulation.check_non_membership wit v as ne = true) : findNMWitness? v (as.head ne) as.tail = some wit

axiom ListWitness.forall_not_witness_eq_none {α : Type} [l : LinearOrder α] {ls : List α} {e hd : α} (lsSorted : List.Sorted (fun (x1 x2 : α) => x1 < x2) (hd :: ls)) (H : ∀ (wit : ListSimulation.NonMemProof α), ¬findNMWitness? e hd ls = some wit) : findNMWitness? e hd ls = none