Arranger Block Validity Fraud Proofs

We explore a simple protocol with two kind of players: One proposing blocks and the other just challenging.

The main goal is to prove that when we have an honest challenger challenging only /good/ blocks are accepted: See honest_chooser_valid

Player One (Proposer)

Player one, the player proposing elements, actions are to propose a new block da : BTree α × ℍ. Since we do not have IO, upon propsing a new block, they player also provides all possible strategies for all elements.

structure P1_Actions (α ℍ : Type) : Type

• da : BTree α × ℍ
• dac_str : ABTree (Option α) (Option (ℍ × ℍ))
• gen_elem_str {n : ℕ} : ISkeleton n → Sequence n (Option (ℍ × ℍ)) × Option α

Local Validity

We define a local valid block Local_valid to a block that hashes to a given hash, holds only valid elements and has no duplicates.

structure Local_valid {α ℍ : Type} [DecidableEq α] [Hash α ℍ] [HashMagma ℍ] (data : BTree α) (mk : ℍ) (val_fun : α → Bool) : Prop

• MkTree : data.hash_BTree = mk
• ValidElems : BTree.fold val_fun and data = true
• NoDup : data.toList.Nodup

Helper function building a complete tree from a sequence of 2^lgn elements.

def Valid_Seq {α ℍ : Type} {lgn : ℕ} [DecidableEq α] [Hash α ℍ] [HashMagma ℍ] (data : Sequence (2 ^ lgn) α) (merkle_tree : ℍ) (P : α → Bool) : Prop

Equations

• Valid_Seq data merkle_tree P = Local_valid (perfectSeqLeaves data) merkle_tree P

Same as Local_valid but instead of having a struct, we just have a Prop.

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

Equations

• local_valid da val_fun = (da.1.hash_BTree = da.2 ∧ BTree.fold val_fun and da.1 = true ∧ da.1.toList.Nodup)

theorem struct_and_iff_valid {α ℍ : Type} [DecidableEq α] [Hash α ℍ] [HashMagma ℍ] (data : BTree α) (mk : ℍ) (val_fun : α → Bool) : Local_valid data mk val_fun ↔ local_valid (data, mk) val_fun

PLayer 2 (Challenger)

The second player, bsaed on what the player one (proposer) proposes, can perform one of the following actions:

1. DAC challenge
2. Element invalid challenge
3. Duplicate elements challenge
4. accept the block as valid

inductive P2_Actions (α ℍ : Type) : Type

• DAC {α ℍ : Type} (str : ABTree Unit (ℍ × ℍ × ℍ → Option ChooserMoves)) : P2_Actions α ℍ
• Invalid {α ℍ : Type} {n : ℕ} (p : α) (seq : ISkeleton n) (str : Sequence n (ℍ × ℍ × ℍ → Option ChooserSmp)) : P2_Actions α ℍ
• Duplicate {α ℍ : Type} (n m : ℕ) (path_p : ISkeleton n) (path_q : ISkeleton m) (str_p : Sequence n (ℍ × ℍ × ℍ → Option ChooserSmp)) (str_q : Sequence m (ℍ × ℍ × ℍ → Option ChooserSmp)) : P2_Actions α ℍ
• Ok {α ℍ : Type} : P2_Actions α ℍ

L2 Local Linear Protocol

Simple linear protocol: no optimizations as logarithmic search. There is no time involved: we assume players have all the time in the world to play and there is no rush. We assume players play to win, and we do not reason about the incentives they have to beahve like that. If plaer two wins, the proposed block is discarded and nothing else happens. In the real protocol, we player one should be penalized.

Helper function defining actions taken after player one moved.

def inner_l2_actions {α ℍ : Type} [BEq α] [BEq ℍ] [o : Hash α ℍ] [HashMagma ℍ] (val_fun : α → Bool) (playerOne : P1_Actions α ℍ) (playerTwo : P2_Actions α ℍ) : Bool

Equations

• One or more equations did not get rendered due to their size.
• inner_l2_actions val_fun playerOne P2_Actions.Ok = true

Definition of L2 protocol playing linear games.

def linear_l2_protocol {α ℍ : Type} [BEq α] [BEq ℍ] [o : Hash α ℍ] [HashMagma ℍ] (val_fun : α → Bool) (playerOne : P1_Actions α ℍ) (playerTwo : BTree α × ℍ → P2_Actions α ℍ) : Bool

Equations

• linear_l2_protocol val_fun playerOne playerTwo = inner_l2_actions val_fun playerOne (playerTwo playerOne.da)

Crafting Honest Players.

Witness Finding.

structure IH (ℍ : Type) : Type

• side : SkElem
• spine : ℍ
• sib : ℍ

structure Witness (α ℍ : Type) : Type

• length : ℕ
• pathInfo : Sequence self.length (IH ℍ)
• src : α
• dst : ℍ

Find leftest invalid value

def find_left_invalid_path {α ℍ : Type} [o : Hash α ℍ] [m : HashMagma ℍ] (val : α → Bool) : BTree α → Option (Witness α ℍ)

Equations

• One or more equations did not get rendered due to their size.
• find_left_invalid_path val (ABTree.leaf a) = if val a = true then none else some { length := 0, pathInfo := Sequence.nil, src := a, dst := o.mhash a }

theorem find_valid_nothing {α ℍ : Type} [o : Hash α ℍ] [m : HashMagma ℍ] (val : α → Bool) (t : BTree α) (valid : BTree.fold val and t = true) : find_left_invalid_path val t = none

theorem find_nothing_is_valid {α ℍ : Type} [o : Hash α ℍ] [m : HashMagma ℍ] (val : α → Bool) (t : BTree α) : find_left_invalid_path val t = none → BTree.fold val and t = true

theorem find_invalid_path_accessed {α ℍ : Type} [o : Hash α ℍ] [m : HashMagma ℍ] (val : α → Bool) (t : BTree α) (wit : Witness α ℍ) : find_left_invalid_path val t = some wit → ABTree.iaccess t (Sequence.map (fun (f : IH ℍ) => f.side) wit.pathInfo) = some (Sum.inl wit.src) ∧ val wit.src = false

def generate_merkle_tree {α ℍ : Type} [o : Hash α ℍ] [m : HashMagma ℍ] (data : BTree α) : ABTree α ℍ

Equations

• One or more equations did not get rendered due to their size.
• generate_merkle_tree (ABTree.leaf a) = ABTree.leaf a

def gen_chooser_opt' {ℍ : Type} [BEq ℍ] (data : ℍ × ℍ) (proposed : ℍ × ℍ × ℍ) : Option ChooserMoves

Equations

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

Honest player two. Check each condition and if the proposed block violates one, it generates a witness and challenges the validity of such block.

def honest_chooser {α ℍ : Type} [DecidableEq α] [BEq ℍ] [Hash α ℍ] [m : HashMagma ℍ] (val_fun : α → Bool) (public_data : BTree α) (da_mtree : ℍ) : P2_Actions α ℍ

Equations

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

theorem const_comp {α β γ : Type} (f : α → β) (g : γ) : (fun (x : β) => g) ∘ f = fun (x : α) => g

theorem gen_chooser_opt_some {ℍ : Type} [BEq ℍ] : ((fun (fhs : ℍ × ℍ × ℍ → Option ChooserMoves) (x : ℍ × ℍ × ℍ) => fhs x) ∘ gen_chooser_opt) ∘ some = (fun (fhs : ℍ × ℍ × ℍ → Option ChooserMoves) (x : ℍ × ℍ × ℍ) => fhs x) ∘ gen_chooser_opt'

theorem fold_getI_hash {α ℍ : Type} [o : Hash α ℍ] [m : HashMagma ℍ] (b : ABTree α Unit) : ABTree.fold o.mhash (fun (x : Unit) => m.comb) b = ABTree.getI' o.mhash (fun (x : ℍ × ℍ) => m.comb x.1 x.2) b.hash_SubTree

Honest chooser finds correct witnesses, and thus, it always wins the challenging games (if played.)

theorem honest_chooser_wins {α ℍ : Type} [BEq ℍ] [LawfulBEq ℍ] [o : Hash α ℍ] [m : HashMagma ℍ] (da : BTree α) : winning_condition_player (fun (hc : ℍ) (a : α) (h : ℍ) => dac_leaf_winning_condition hc a h = true) (fun (_x : Unit) (x : ℍ × ℍ) (res : ℍ) => dac_node_winning_condition res x.1 x.2 = true) (fun (_x : ℍ) => id) { data := ABTree.map o.mhash id da, res := ABTree.fold o.mhash (fun (_x : Unit) => m.comb) da } (ABTree.map some some (ABTree.hash_SubTree da))

Honest player do not challenge valid blocks

theorem honest_chooser_accepts_valid {α ℍ : Type} [DecidableEq α] [BEq ℍ] [LawfulBEq ℍ] [o : Hash α ℍ] [m : HashMagma ℍ] (val_fun : α → Bool) (data : BTree α) (mk : ℍ) (da_valid : Local_valid data mk val_fun) : honest_chooser val_fun data mk = P2_Actions.Ok

L2 Protocol and Honest player

theorem inner_honest_valid_dac_wrong {α ℍ : Type} [DecidableEq α] [BEq ℍ] [LawfulBEq ℍ] [o : Hash α ℍ] [m : HashMagma ℍ] [InjectiveHash α ℍ] [InjectiveMagma ℍ] (val_fun : α → Bool) (da : BTree α × ℍ) (dac_str : ABTree (Option α) (Option (ℍ × ℍ))) (gen_elem_str : {n : ℕ} → ISkeleton n → Sequence n (Option (ℍ × ℍ)) × Option α) (Hm : (da.2 == ABTree.fold o.mhash (fun (x : Unit) => m.comb) da.1) = false) : (linear_l2_protocol val_fun { da := da, dac_str := dac_str, gen_elem_str := gen_elem_str } fun (x : BTree α × ℍ) => honest_chooser val_fun x.1 x.2) = false

Helper lemma, if a block is accepted by linear_l2_protocol, then that block is valid.

theorem inner_honest_valid {α ℍ : Type} [DecidableEq α] [BEq ℍ] [LawfulBEq ℍ] [o : Hash α ℍ] [m : HashMagma ℍ] [InjectiveHash α ℍ] [InjectiveMagma ℍ] (val_fun : α → Bool) (da : BTree α × ℍ) (dac_str : ABTree (Option α) (Option (ℍ × ℍ))) (gen_elem_str : {n : ℕ} → ISkeleton n → Sequence n (Option (ℍ × ℍ)) × Option α) : (linear_l2_protocol val_fun { da := da, dac_str := dac_str, gen_elem_str := gen_elem_str } fun (x : BTree α × ℍ) => honest_chooser val_fun x.1 x.2) = true → local_valid da val_fun

Valid blocks are accepted by the linear_l2_protocol .

theorem honest_chooser_valid_local_valid {α ℍ : Type} [BEq ℍ] [LawfulBEq ℍ] [DecidableEq α] [o : Hash α ℍ] [m : HashMagma ℍ] [InjectiveHash α ℍ] [InjectiveMagma ℍ] (val_fun : α → Bool) (p1 : P1_Actions α ℍ) : local_valid p1.da val_fun → (linear_l2_protocol val_fun p1 fun (x : BTree α × ℍ) => match x with | (t, mt) => honest_chooser val_fun t mt) = true

Main theorem, the L2 Protocol linear_l2_protocol accepts valid blocks and every block accepted by the protocol is valid, when equipped with the honest player two.

theorem honest_chooser_valid {α ℍ : Type} [BEq ℍ] [LawfulBEq ℍ] [DecidableEq α] [o : Hash α ℍ] [m : HashMagma ℍ] [InjectiveHash α ℍ] [InjectiveMagma ℍ] (val_fun : α → Bool) (p1 : P1_Actions α ℍ) : (linear_l2_protocol val_fun p1 fun (x : BTree α × ℍ) => match x with | (t, mt) => honest_chooser val_fun t mt) = true ↔ local_valid p1.da val_fun