Stateful Protocol.

History Protocol takes into account the whole history of the L2 Protocol.

The main difference is that blocks are conditional valid depending on the elements that were added before the current block (the History.)

Main Definition is that valid now checks that elements do not occurr more than once across the whole history. Here we are a bit redundant, because historic non-duplication implies local non-duplication. However, we choosed to follow a compositional approach. Eventually, we may be interested in adding more properties and it is worth exploring such approach.

So historical_valid is local_valid plus no-duplicates accross history.

def historical_valid {α ℍ : Type} [DecidableEq α] [Hash α ℍ] [HashMagma ℍ] (Hist : List (BTree α × ℍ)) (val_fun : α → Bool) : Prop

Equations

• historical_valid Hist val_fun = ((∀ e ∈ Hist, local_valid e val_fun) ∧ (List.map (fun (x : BTree α × ℍ) => x.1.toList) Hist).flatten.Nodup)

Lemma historical_concat characterizes the evolution of the definition historical_valid everytime we add a new block. Since the protocol evolves linearly adding new blocks, this lemma simplifies the following proofs.

theorem historical_concat {α ℍ : Type} [DecidableEq α] [Hash α ℍ] [HashMagma ℍ] (hist : List (BTree α × ℍ)) (new : BTree α × ℍ) (val_fun : α → Bool) : historical_valid (hist ++ [new]) val_fun = (historical_valid hist val_fun ∧ ((List.map (fun (x : BTree α × ℍ) => x.1.toList) hist).flatten ++ new.1.toList).Nodup ∧ local_valid new val_fun)

Player two, the player acting as challenger, on top of the previous moves defined in L2.lean file, can also challenge new blocks of duplicating elements across history.

inductive P2_History_Actions (α ℍ : Type) : Type

• Local {α ℍ : Type} (ll : P2_Actions α ℍ) : P2_History_Actions α ℍ
• DupHistory_Actions {α ℍ : Type} (epoch n : ℕ) (en : α) (path_p : ISkeleton n) (str_p : Sequence n (ℍ × ℍ × ℍ → Option ChooserSmp)) (m : ℕ) (em : α) (path_q : ISkeleton m) (str_q : Sequence m (ℍ × ℍ × ℍ → Option ChooserSmp)) : P2_History_Actions α ℍ

Player one actions are defending the elements they present.

structure P1_History_Actions (α ℍ : Type) : Type

• local_str : P1_Actions α ℍ
• global_str : List (BTree α × ℍ) → ℕ → {n : ℕ} → ISkeleton n → Sequence n (Option (ℍ × ℍ)) × Option α

Duplicates in History

We define how we find elements and duplicates.

def find_first_dup_in_history {α ℍ : Type} [DecidableEq α] (elems : List (Skeleton × α)) (hist : List (BTree α × ℍ)) : Option ((List (BTree α × ℍ) × (BTree α × ℍ) × List (BTree α × ℍ)) × (List (Skeleton × α) × (Skeleton × α) × List (Skeleton × α)) × List (Skeleton × α) × (Skeleton × α) × List (Skeleton × α))

Equations

• find_first_dup_in_history elems hist = split_at_first_pred (fun (e : BTree α × ℍ) => find_intersect (fun (x : Skeleton × α) => x.2) e.1.toPaths_elems elems) hist

theorem no_dups_find_first_none {α ℍ : Type} [DecidableEq α] (elems : List (Skeleton × α)) (hist : List (BTree α × ℍ)) (HDis : (List.map (fun (x : BTree α × ℍ) => x.1.toList) hist).flatten.Disjoint (List.map (fun (x : Skeleton × α) => x.2) elems)) : find_first_dup_in_history elems hist = none

theorem find_first_dup_in_history_none {α ℍ : Type} [DecidableEq α] (elems : List (Skeleton × α)) (hist : List (BTree α × ℍ)) (HNoFind : find_first_dup_in_history elems hist = none) : (List.map (fun (x : BTree α × ℍ) => x.1.toList) hist).flatten.Disjoint (List.map (fun (x : Skeleton × α) => x.2) elems)

theorem find_first_dup_in_history_law {α ℍ : Type} [DecidableEq α] {t : BTree α} {hist pre post : List (BTree α × ℍ)} {oldDA : BTree α × ℍ} {oldE currE : Skeleton × α} {preOld posOld preCurr posCurr : List (Skeleton × α)} (H : find_first_dup_in_history t.toPaths_elems hist = some ((pre, oldDA, post), (preOld, oldE, posOld), preCurr, currE, posCurr)) : ABTree.access oldDA.1 oldE.1 = some (Sum.inl oldE.2) ∧ ABTree.access t currE.1 = some (Sum.inl currE.2) ∧ oldE.2 = currE.2 ∧ hist[pre.length]? = some oldDA

Honest PLayer

Honest players check new blocks to see if they check the required conditions and if not, they build a challengin move.

def historical_honest_algorith {α ℍ : Type} [DecidableEq α] [BEq ℍ] [Hash α ℍ] [m : HashMagma ℍ] (val_fun : α → Bool) (history : List (BTree α × ℍ)) (public_data : BTree α) (da_mtree : ℍ) : P2_History_Actions α ℍ

Equations

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

theorem List.Disjoin_iff_forall {α : Type} {l r : List α} [DecidableEq α] : l.Disjoint r ↔ ∀ i ∈ l, ∀ j ∈ r, (i != j) = true

theorem honest_chooser_history_accepts_valid {α ℍ : Type} [DecidableEq α] [BEq ℍ] [LawfulBEq ℍ] [o : Hash α ℍ] [m : HashMagma ℍ] {val_fun : α → Bool} {history : List (BTree α × ℍ)} {new : BTree α × ℍ} (da_valid : historical_valid (history ++ [new]) val_fun) : historical_honest_algorith val_fun history new.1 new.2 = P2_History_Actions.Local P2_Actions.Ok

theorem Nodups_no_dups_in_history {α ℍ : Type} [DecidableEq α] [BEq ℍ] [Hash α ℍ] [m : HashMagma ℍ] (val_fun : α → Bool) (history : List (BTree α × ℍ)) (public_data : BTree α) (da_mtree : ℍ) (HDis : (List.map (fun (x : BTree α × ℍ) => x.1.toList) history).flatten.Disjoint public_data.toList) : historical_honest_algorith val_fun history public_data da_mtree = P2_History_Actions.Local (honest_chooser val_fun public_data da_mtree)

L2 History Protocol

The protocol consists on a player providing information and another player challenging such information. Since we do not have IO here, all players must build and provide all strategies before hand.

def linear_l2_historical_protocol {α ℍ : Type} [BEq α] [BEq ℍ] [o : Hash α ℍ] [HashMagma ℍ] (val_fun : α → Bool) (hist : List (BTree α × ℍ)) (playerOne : P1_History_Actions α ℍ) (playerTwo : List (BTree α × ℍ) → BTree α × ℍ → P2_History_Actions α ℍ) : Bool

Equations

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

theorem history_honest_chooser_no_intersect_hist {α ℍ : Type} [BEq ℍ] [LawfulBEq ℍ] [DecidableEq α] [o : Hash α ℍ] [m : HashMagma ℍ] [InjectiveHash α ℍ] [InjectiveMagma ℍ] (val_fun : α → Bool) (p1 : P1_History_Actions α ℍ) (hist : List (BTree α × ℍ)) (histCorrect : ∀ e ∈ hist, e.1.hash_BTree = e.2) (HHist : (List.map (fun (x : BTree α × ℍ) => x.1.toList) hist).flatten.Nodup) : (linear_l2_historical_protocol val_fun hist p1 fun (h : List (BTree α × ℍ)) (x : BTree α × ℍ) => match x with | (t, mt) => historical_honest_algorith val_fun h t mt) = true → ((List.map (fun (x : BTree α × ℍ) => x.1.toList) hist).flatten ++ p1.local_str.da.1.toList).Nodup

theorem history_honest_chooser_local_valid {α ℍ : Type} [BEq ℍ] [LawfulBEq ℍ] [DecidableEq α] [o : Hash α ℍ] [m : HashMagma ℍ] [InjectiveHash α ℍ] [InjectiveMagma ℍ] (val_fun : α → Bool) (p1 : P1_History_Actions α ℍ) (hist : List (BTree α × ℍ)) (HNodups : ((List.map (fun (x : BTree α × ℍ) => x.1.toList) hist).flatten ++ p1.local_str.da.1.toList).Nodup) : (linear_l2_historical_protocol val_fun hist p1 fun (h : List (BTree α × ℍ)) (x : BTree α × ℍ) => match x with | (t, mt) => historical_honest_algorith val_fun h t mt) = true → local_valid p1.local_str.da val_fun

theorem history_honest_chooser_valid {α ℍ : Type} [BEq ℍ] [LawfulBEq ℍ] [DecidableEq α] [o : Hash α ℍ] [m : HashMagma ℍ] [InjectiveHash α ℍ] [InjectiveMagma ℍ] (val_fun : α → Bool) (p1 : P1_History_Actions α ℍ) (hist : List (BTree α × ℍ)) (hist_valid : historical_valid hist val_fun) : (linear_l2_historical_protocol val_fun hist p1 fun (h : List (BTree α × ℍ)) (x : BTree α × ℍ) => match x with | (t, mt) => historical_honest_algorith val_fun h t mt) = true → historical_valid (hist ++ [p1.local_str.da]) val_fun

theorem history_honest_chooser_valid' {α ℍ : Type} [BEq ℍ] [LawfulBEq ℍ] [DecidableEq α] [o : Hash α ℍ] [m : HashMagma ℍ] [InjectiveHash α ℍ] [InjectiveMagma ℍ] (val_fun : α → Bool) (p1 : P1_History_Actions α ℍ) (hist : List (BTree α × ℍ)) (AllValid : historical_valid (hist ++ [p1.local_str.da]) val_fun) : (linear_l2_historical_protocol val_fun hist p1 fun (h : List (BTree α × ℍ)) (x : BTree α × ℍ) => match x with | (t, mt) => historical_honest_algorith val_fun h t mt) = true

Theorem HistoryProtocol states that the history protocol when played with an honest player challenging proposed blocks only accepts correct blocks (->) and correct blocks are accepted by the protocol (<-).

theorem HistoryProtocol {α ℍ : Type} [BEq ℍ] [LawfulBEq ℍ] [DecidableEq α] [o : Hash α ℍ] [m : HashMagma ℍ] [InjectiveHash α ℍ] [InjectiveMagma ℍ] (val_fun : α → Bool) (p1 : P1_History_Actions α ℍ) (hist : List (BTree α × ℍ)) : (linear_l2_historical_protocol val_fun hist p1 fun (h : List (BTree α × ℍ)) (x : BTree α × ℍ) => match x with | (t, mt) => historical_honest_algorith val_fun h t mt) = true ∧ historical_valid hist val_fun ↔ historical_valid (hist ++ [p1.local_str.da]) val_fun