Clickable Documentation

CCS’25

Main artifact proofs are in L2 .

Zenode badge:

Main proof is honest_chooser_valid proving our main validity claim.

theorem honest_chooser_valid {α ℍ}
   [BEq ℍ][LawfulBEq ℍ][DecidableEq α]
   [o : Hash α ℍ][m : HashMagma ℍ][InjectiveHash α ℍ][InjectiveMagma ℍ]
   (val_fun : α -> Bool)
   (p1 : P1_Actions α ℍ)
   : linear_l2_protocol val_fun p1 ( fun (t, mt) => honest_chooser val_fun t mt)
     ↔ local_valid p1.da val_fun

Players

Player One, proposing DAs, is defined as a new batch with all possible moves in all possible games.

structure P1_Actions (α ℍ : Type) : Type
 where
 da : BTree α × ℍ
 dac_str : ABTree (Option α) (Option (ℍ × ℍ))
 gen_elem_str : {n : Nat} -> ISkeleton n -> (Sequence n (Option (ℍ × ℍ)) × Option α)

Player Two, the one (possibly) challenging, is defined as

inductive P2_Actions (α ℍ : Type)  : Type
  where
   | DAC (str : ABTree Unit ((ℍ × ℍ × ℍ) -> Option ChooserMoves))
   | Invalid {n : Nat} (p : α) (seq : ISkeleton n) (str : Sequence n ((ℍ × ℍ × ℍ) -> Option ChooserSmp))
   | Duplicate (n m : Nat)
      -- There are two paths
      (path_p : ISkeleton n) (path_q : ISkeleton m)
      -- Strategies to force proposer to show elements.
      (str_p : Sequence n ((ℍ × ℍ × ℍ) -> Option ChooserSmp))
      (str_q : Sequence m ((ℍ × ℍ × ℍ) -> Option ChooserSmp))
   | Ok

Validity of Batches.

Notion of (local) batch validity is defined exactly as the article says:

def local_valid {α ℍ : Type} [DecidableEq α][Hash α ℍ][HashMagma ℍ]
  (da : BTree α × ℍ)(val_fun : α -> Bool) : Prop
 -- Merkle Tree is correct
 := da.fst.hash_BTree = da.snd
 -- All elements are |val_fun| valid
 ∧ (da.fst.fold val_fun and)
 -- There are no duplicated elements.
 ∧ List.Nodup da.fst.toList

Winning Lemmas

To see how we prove that honest players win games see file ElementInTree .

• Lemma elem_back_rev_honest_two stating that knowing the data, honest choosers lead proposers either to quit or to prove that an element is in a tree.
• We define the notion of winning conditions in file GenericTree and prove that proposers win winning_proposer_wins.

Adding History.

To complete the CSS’25 article proofs, we needed to check that there are no duplicates elements across history. Local validity is local to each block, but history non-duplicity is contextual and depends on the previous elements added. It is effectful in a way.

We defined a new protocol in History L2 on top of the previous one ( L2 ). The new protocol has a history of added blocks and checks that all blocks are local valid plus they do not duplicate elements.

def historical_valid
  {α ℍ : Type} [DecidableEq α][Hash α ℍ][HashMagma ℍ]
  -- History of commited blocks and their hashes.
  (Hist : List (BTree α × ℍ))
  -- Validity Function
  (val_fun : α -> Bool)
  : Prop
  :=
  -- Each epoch is `local_valid`
  (∀ e ∈ Hist, local_valid e val_fun)
  ∧ -- Plus there are no duplicated elements. This one subsumes nodup in local_valid.
  (List.Nodup (Hist.map (BTree.toList $ ·.fst)).flatten)

We add a new move for player two, now the player two (the chooser) can detect duplicate elements across history and build witnesses and fraudproofs accordingly. Player one (the proposer), now has to provide strategies defending their claim for all elements across history too. Since we do not have IO.

Same as before, our main theorem is that the protocol equipped with an honest player only accepts valid blocks.

theorem HistoryProtocol {α ℍ}
   [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 (t, mt) => historical_honest_algorith val_fun h t mt)
    ∧
      historical_valid hist val_fun)
   ↔ historical_valid (hist ++ [p1.local_str.da]) val_fun

Compilation

Lake Compilation (Lean native)

Get lean first, https://leanprover-community.github.io/get_started.html .

To build the whole project should suffice with a simple lake build command

lake update
lake build

Follow Makefile:

make help

Nix Compilation

Get Nix, follow make file.

make help

Compile Documentation

See Makefile help.

Added Pages

Project Structure:

Data Structures

Here I programmed useful data structures:

BTree

Binary Trees

Hash

Hash stuff, classes defining hash function from one type to another. Collision Free notions.

MTree

Merkle Trees. (BTree + Hashes).

Sequences

Fin lists (Sequences,Arrays?,n-Tuples), in Lean

def Sequence (a : Type) (n : Nat) := { t : List a // t.lenght = n }
    

SeqBTree

Sequences to BTrees. Balance Complete Trees, so we can show log search of fraud-proofs.

TreeAccess

Main star when formalizing L2 (Arranger) games. Main lesson here, we need to characterize the algorithm in a complete way. We need errors and enough information to build fraudproofs. This reminds me a lot of ‘Z’ charts characterizing good and bad behaviours.

• Find invalid elements returning extra metadata when an invalid element is found and proof-carrying data when no element is found. We need extra data to build strategies and to eventually prove that correct agents always win.
• Find duplicated elements. Find_inv ; Find_inv when invalid is membership? Several proofs are needed here.

Extras

Don’t really remember here, files here may be obsolete.

Games

ElemInTree

Arbitration games proving element membership in merkle trees.

FMBC

Fmbc stuff. I did it to guide reviewrs, idk.

FromBtoMTree

DAC game, merkle tree is correctly built arbitration game.

GameDef

definitions of games.

GenericTree

Generic Games played on top of Binary Trees arenas.

LogProof

logarithmic games are logarithmic.

PathToTreeGames

similar to ElemInTree?

ReverseLinearGames

linear games can be played bottom-up ant top-down.

Simultaneous

Arbitration Games where both players provide their strategies before playing. It is not their complete strategies but a commitment element. The Merkle Tree root of their strategies.

Proofs

Again, not so sure.

L2.Lean

Root file implementing Arranger games and strategies. Using everything we defined, we prove that honest players always win.

HistoryL2.Lean

Root file implementing Arrangers with History. Using everything we defined, we prove that honest players always win and they accept honest claims.

FraudProof

Here we aim to implement and formalize FraudProof ideas placed in L2 Setchain.

Implementation List

Basic Data Structures

Binary Tree

Small binary tree implementation plus some important definitions:

Sibilings path from an element to the root.

abbrev TreePath (α : Type ):= List (Sum (BTree α) (BTree α))

When an element is in a tree, and moreover, we can compute its proof. In this case, a path from the element (value) to the root.

def valueIn [BEq α] (v : α) ( bt : BTree α ) : Bool
def valueInProof [BEq α](v : α) (bt : BTree α) : Option ( TreePath α )

Value

Opaque type representing values in our data structure.

Requisites: an equilvalence relation.

Hash

Hash are strings (maybe we can change that, there is a hash notion already in Lean)

It defines a hash function H : Value -> Hash and an operator \oplus: Hash -> Hash -> Hash.

Moreover, we assume perfect hashing (no collisions).

axiom hash_prop (v1 v2 : Value) : v1 ≠ v2 → H v1 ≠ H v2

Merkle Tree simple data structure MTree Implementation

Merkle Trees are nothing but the hash of the root of the markle tree they represent.

Here we define important notions as hash paths. For example, a Hash is in a Merkle tree, if we provide the evidence, a list of hashes and positions, leading to the root.

def nodeIn (h : Hash) (path : Path) (t : MTree) : Bool
:= match t with
| MTree.node hT => listPathHashes h path == hT

Games data structures

Games

There is only one game: membership game. Given a value (or a hash), it is an element in a given Merkle Tree.

General Game Definitions – GameDefs

Who wins. Maybe as we define more adv games we may have more stuff here?

One Step Game – OneStepGame

One step game are games over a path of length 1. That is we have two hashes hb ht : Hash and proposers win if they can produce a valid sibling hash hb' : Hash, that is opHash hb hb' = ht.

Other games eventually lead to this game.

Linear Game – LinearGame

Linear games consist on one player proposing hashes along the one, one at a time, and the chooser deciding if a hash is incorrect, challenging that claim.

The chooser either chooses between ‘this hash is incorrect’ or ‘continue with the next’. If the chooser challenges a correct hash, the chooser loses.

It can be player from the root to the leaf or the other way around.

Log Game – LogGame

Similar to the Linear one but instead of going through the list offering one by one, the Proposer produces the hash in the middle of the path between the leaf and the root. The chooser then chooses on which half the game should continue to.

It is called Log Game since it halves the path at every instance. Leading to a one step game.

Players – Players

Here we define two players.

Proposer

Proposers propose hashes along the way. Since eventually they need to provide siblings too, proposer strategies are compose of two arrays of hashes:

structure HC (n : Nat) where
  -- Hashes along the way
  pathNode : Fin ( n + 1 ) -> Hash
  -- Path elem knows how to hash.
  pathSib : Fin n -> PathElem

Proposers are indexed on the length of the path.

Plus some operations over proposers.

IDEA Maybe. Min Proposer

I guess we can implement a minimal proposer using just an array of hashes as long as the path itself. It is just taking pathSib and computing pathNode. But that only works for the correct player.

Chooser

Choosers are somewhat simpler, but I haven’t proved anything on them yet. They take three hashes and choose which side (Left or Right) they want to continue playing in.

Winning Players – WinningDefinitions

The goal here was to prove that good proposers always win. That is that a player with some information, in particular, the original binary tree, can compute a winning strategy.

Two main concepts:

• What’s the definition of a winning strategy?
• How to build a winning strategy from the information honest player have?

Winning Proposer

Winning proposers are path of a given length connecting two hashes. By connecting, I mean that the proposer propose hashes (nodes and siblings) that hash correct from one hsah to the other. We can see it better in this three props:

@[simp]
def GoodInit (h : Hash) := Player.pathNode 0 = h

@[simp]
def GoodRoot (h : Hash ) := Player.pathNode ⟨ n , by simp ⟩ = h

@[simp]
def GoodMid  :=
    forall (m : Nat) (mLtn : m < n ),
    Player.pathNode ⟨ (m + 1) , by apply Nat.succ_lt_succ;assumption⟩ =
    opHash ( Player.pathNode ⟨ m , by apply Nat.lt_add_one_of_lt; assumption ⟩) ( Player.pathSib ⟨ m , mLtn ⟩ )

We also lift operations from strategies to winning proposers (we’ll need them when proving.)

Fraud Proof Games – FraudProofs

Main file proving that:

Winning Proposers win Linear Game

Winning Proposers win Log Game

Chooser Guarantees

If someone wrongly challenges a posted Merkle Tree, we can defend it and win. It is a similar theorem to winning strategies when challenged. But on the other side.

Main Idea: Path Skeletons

We need path skeletons to prove that choosers have winning strategies. Theorem is like:

Following the same path provided by proposers, correct choosers know the how to fill the same path with corrects hashes. Knowing that something is wrong, i.e. the last hash proposed is wrong but the first is right (it is the hash of the root assumed correct.), choosers can choose wisely when to challenge.

Linear games

Found a bug here. My bad when defining hash props. Fixed, but I made a bug in proof evident.

Log Games

Multicut games

Model Merkle Tree chain?

Should we model the idea of posting Merkle Trees and the possibility of challenges.

Computing Hashes?

python3 -m venv venv
source ./venv/bin/activate.fish

python3 -m pip install web3

Delegating this to Python.

from web3 import web3 # hashfunctions.

print(web3.solidity_keccak(['string'],['testing']))

Removing opaque types.

See ‘Hash Classes’

Validity Proofs

Hash Classes

-- Hash function
@[class] structure Hash (α ℍ : Type) where
  mhash : α -> ℍ
-- Hash comb function
@[class] structure HashMagma (ℍ : Type) where
  comb : ℍ -> ℍ -> ℍ

-- Laws
-- Collision resistant?
@[class] structure CollResistant (α ℍ : Type)[op : Hash α ℍ] where
  -- Collision resistant? It should be hard to find these guys.
  noCollisions : forall (a b : α), a ≠ b -> op.mhash a ≠ op.mhash b

-- Similar but for magma op.
@[class] structure SLawFulHash (ℍ : Type)[m : HashMagma ℍ] where
  -- Combine diff hashes are diff.
  neqLeft : forall (a1 a2 b1 b2 : ℍ), a1 ≠ a2 -> m.comb a1 b1 ≠ m.comb a2 b2
  neqRight : forall (a1 a2 b1 b2 : ℍ), b1 ≠ b2 -> m.comb a1 b1 ≠ m.comb a2 b2

Hash Injective

Injective prop is stronger than collision resistant and lawful.

IO Interactions

From Opaque to Classes

Keccak256 is a valid IO Hash?

IO Merkle Tree generation.

A bit more general games

DAs

DAs are weird computational data. \(\{ a : α , b : β \}\) and a process \(f\) such that \( f(a) = b\).

Skeletons in BTree/Tree computations.

Implementation of winning Defensive strategy and challenging strategies.

Proving the above?

DA : BTree -> Merkle Tree

DA : (BTree -> MTree) and Valid

Depending on what the DA is, we may need different stuff.

1. DA : \(\langle e , path , ha \rangle\) – Tree is implicit and hashes to \(ha\)
2. DA : \(\langle h(e) , path , ha \rangle\) – Tree is implicit and hashes to \(ha\)
3. DA : \(\langle tree , _ , path , ha \rangle\) – Tree is |tree| and hashes to \(ha\)

Elements are f-Valid

No repeated elements

Sequences to Vectors: Move on from Fin to Finite list

Good things, we will not need \(funext\).

def Sequence (n : Nat) (a : Type) := { ls : [ a ] // ls.length = n } -- Vector n a

Linear to Log using Generic Trees

Define Game transformations

Sequence Linear to Tree Linear

Sequence Linear to Log Tree Linear

I have been fighting with this one. I fall into the first model I actually proved correct. Tried to define some wierd transformations, nothing worked but I have an idea.

Same as before, I have two ways of seeing the sequence of hashes I have, as a sequence of siblings plus side or just computing each hash. I tried the sibling path, but it gets a bit fuzzy and it is not exactly what I need when going though the logarithmic game. The logarithmic game is played only observing the resulting intermediary hashes. Next step is to try to program that. I took the first path because it was an easy transformation, forming a tree game arena with exactly what I had while computing intermediary hashes along the way. But it turned out to be a bit complex, maybe I can come back to this idea after gaining some intuition about this.

Hash Function

Implicit assumptions.

Hash functions are:

• Collision resistants (from RDoC)

I did not require it to prove strategies are correct when proving Merkle trees are correct.

Chooser Strategy.

When an invalid hash tree is detected, we can invoke a choosers strategy to debunk the block. The strategy operates under the assumption the top hash is wrong, otherwise there is no way to know if the agent proposing the block is wrong. For example, the agent can front-run another and post what it seems to be a valid block without knowing the tree.

Optimization: We can build players choosing shorters paths when possible.

We know the whole tree and it is not complete.

Chooser generation stategy game.

We can define a game using generation strategies. If choosers provide inside knowledge of how they created their strategies, we can perform useful transformation. Honest choosers know the data and thus, are part of this family.

Simultaneous games

Since we have data behind Choosers now (and we generate functions based on that), we can play a simultaneous game. At each step, both players reveal information and based on that the game progresses. I think they are equivalent, but I am leaving the proof of that to after FMBC.

Simulatneous games – Always sectioning games

The BoLD paper describes an optimization over the k-sectioning arbitration game. It says that when the player choosing a side on a k-sectioning, it also provides the ranges and the next sectioning, and roles are swapped. I do not fully understand how it works, but the idea is that sectioning happens at each move. The only similar game I have is what I call simultaneous games, but I am not sure what they do yet.

Ask Marga what’s her take

To build the whole project

lake build

L2Setchain FraudProofs

Data = batch tag , \(\langle id , h , σ \rangle \) implicitly assigned to \(b\) where:

• symbol \(σ\) seems to be a structure containing at least \(f + 1\) signatures
• symbol \( h \) is a hash??
• symbol \( id\) is an identification tag
• symbol \( b \) is a batch defined as a list/sequence of transactions?

Batch tags are valid iff they hold 4 props (additional to the above) over the same ‘da’?

DA: This is the next valid batch tag corresponding to batch \(b\): \(\langle id, h , σ \rangle\)

Data availability Challenge

Data is unknown to a part of the network. It is not challenging the validity of the DA. This challenge challenges missing data? and it makes sense because of economic rules.

Challenge is over a specific node, notation here is very high level.

It is more on the lines of information retrieval than challenging results. The way I was thinking about DAs was \( data_rep , res \) with two implicit computations \( F(data) = data_rep ∧ C(data) = res\). Here the first part is the missing one, \(F(data) = data_rep\).

After posting the tag, another agent ask for data indicating a node

pathToN : Skeleton

The original proposer then provides the information

data ! pathToN = info

And then there is a challenge game to play. The DA the proposer just did is the following Data hashes to \(h\) (already proposed) and such path goes to \(info\).

(data ! pathToN = info) \and C(data) = h

If information provided by the proposer, the challenger can challenge the whole subtree. In Lean, we have a game just for that.

Signature Challenge is just invoking a checker, one shoot game.

Validity Challenge

Challenger knows there is an invalid transaction \(e\) in batch \(t\). Game consists then on showing that \(e ∈ t\) assuming \(t\) is the batch corresponding to current batch tag \(C(t) = h\). One player plays to prove \(e ∈ t\), the other to prove the opposite.

Integrity Challenge 1

Two paths leading to the same element. similar to the above but with one extra step, the defender should choose a path (the one that it thinks is wrong) and play the ElementInTree game.

Integrity Challenge 2

Element \(e\) appears in two batches. Same as before but involving one paths in each batch.