Proof Protocol

Proof protocol is simply a mechanism converting /Successful Fraud Proof Computations/ into /Fraud Proof Tokens/ checking names and policies to guarantee that computations belong to the same Midgard instance.

We simplified the model a bit. Although Computations were implemented, we preferred to implement the logic first and then the interactions between the different models..

I added information to the FraudProof Tokens that are not in the spec.

In the spec, the Midgard protocol checks the computation hashes to get the correct block, here we use block identifiers. The main reason is that hash functions are not implemented.

structure FraudProofTokens.State.FPData : Type

FPData are simply block ids replacing the hash checking mechanism in the Midgard protocol.

• block_id : Tokens.Elem.TId

@[reducible, inline]

abbrev FraudProofTokens.State.FraudProofTokens : Type

FPTokens are tokens carrying this information.

Equations

• FraudProofTokens.State.FraudProofTokens = Tokens.State.Tokens FraudProofTokens.State.FPData

def FraudProofTokens.State.init : FraudProofTokens

Equations

• FraudProofTokens.State.init = Tokens.State.Tokens.init

def FraudProofTokens.Operations.get_block_id (bId : Tokens.Elem.TId) (fp : State.FraudProofTokens) : Option Tokens.Elem.TId

Equations

• FraudProofTokens.Operations.get_block_id bId fp = Tokens.State.Tokens.get_proj bId (fun (x : FraudProofTokens.State.FPData) => x.block_id) fp

Computation Thread Simulation

To generate tokens, we should go through the process of generating a computation thread token, splitting the fraudproof computation into several steps, and if the computation ends properly, then we can generate a FraudProof Token.

Since we value more checking the logic of FraudProofs than the interaction with the computation threads, we simplified the computation threads and implemented the FP logics directly in Lean.

@[reducible, inline]

abbrev FraudProofTokens.ComputationSim.SimDatum : Type

Equations

• FraudProofTokens.ComputationSim.SimDatum = ComputationThreads.Datum.StepDatum ProofProtocol.Catalogue.Script

@[reducible, inline]

abbrev FraudProofTokens.ComputationSim.SimThreads : Type

Equations

• FraudProofTokens.ComputationSim.SimThreads = Tokens.State.Tokens FraudProofTokens.ComputationSim.SimDatum

We simplify the implementation by using inductive types. These steps need to be implemented using computation threads splitting big computations. In this model, we skip the computation splitting and define them straight in the logic of the protocol.

Actions

We only have one action which is to mint a new token. We need to provide a valid computation_thread (something we check in the relation.)

inductive FraudProofTokens.Computation.Actions : Type

• Mint : ComputationThreads.Datum.StepDatum ProofProtocol.Catalogue.Script → Actions

Relation

inductive FraudProofTokens.Computation.Relation (s : State.FraudProofTokens) : Actions → State.FraudProofTokens → Prop

• Mint {s : State.FraudProofTokens} (cs_thread : ComputationThreads.Datum.StepDatum ProofProtocol.Catalogue.Script) (s' : State.FraudProofTokens) : Tokens.State.Tokens.mint cs_thread.name { block_id := cs_thread.block_id } s = s' → Relation s (Actions.Mint cs_thread) s'

Computation

StepMachine

Product Relation

I define the following machine trying to keep the other two as clean as possible.

inductive FraudProofTokens.Computation.Prod (s : State.FraudProofTokens) (st_q : StateQueue.State.StateQueue) (da : DataLayer.DA) (fproof : ComputationThreads.Datum.StepDatum ProofProtocol.Catalogue.Script) : State.FraudProofTokens → Prop

• Step {s : State.FraudProofTokens} {st_q : StateQueue.State.StateQueue} {da : DataLayer.DA} {fproof : ComputationThreads.Datum.StepDatum ProofProtocol.Catalogue.Script} (s' : State.FraudProofTokens) (prevblock hashblock : StateQueue.State.HashHeader) (fpdata : FPData) : MUList.State.ListST.get_data fproof.block_id id st_q = some (Sum.inr hashblock) → MUList.State.ListST.get_data hashblock.header.prev_header_hash id st_q = some (Sum.inr prevblock) → buildFPData da prevblock.header hashblock.header = some fpdata → ProofProtocol.Catalogue.FraudProof fpdata fproof.data → Relation s (Actions.Mint fproof) s' → Prod s st_q da fproof s'

structure FraudProofTokens.Computation.Params : Type

• da : DataLayer.DA
• stq : StateQueue.State.StateQueue

def FraudProofTokens.Computation.FraudProofMachine : StepMachines.StepMachine Params (ComputationThreads.Datum.StepDatum ProofProtocol.Catalogue.Script) State.FraudProofTokens

Equations

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