Ledger Rule - All inputs must be Valid

See MidgardSpec -- Section 5.1.1.

This section is a proof-of-concept trying to verify the logic behind fraudproofs and their descomposition.

The Valid Inputs Property

The property we are checking in this file is:

ValidInput
= ∀ t ∈ Ledger, ∀ i ∈ spend_inputs(t)
  : (∃ t_1 ∈ Ledger, t ≠ t_1 ∧ i ∈ outputs(t_1))
  ∧ (∄ t_2 ∈ Ledger, t ≠ t_2 ∧ i ∈ spend_inputs(t_2))

Claim of the spec:

ValidInput ↔
            ( NOInput
            ∧ InputNoIdx
            ∧ WithdrawnInput
            ∧ DoubleSpend
            ∧ DoubleWithdraw
            )

To prove the above claim, we need to have a definition of the Ledger, i.e. a Ledger Spec. However, once we have the spec implemented, we can prove the above statement in isolation.

What we can try is to modify the ValidInput statement so we only use local data: e.g. each transaction consumes utxos and produce new ones. So we do not need to look at the whole Ledger.

Let's propose the following valid input statement: Let's txs be the current list of transactions forming a block and utxo_prev the current set of utxos alive.

ValidInput
= ∀ t ∈ txs, ∀ i ∈ spend_inputs(t)
  : i ∈ utxo_prev
  ∧ (∄ t_2 ∈ txs, t ≠ t_2 ∧ i ∈ spend_inputs(t_2))

In words, inputs exist before spending them and only one transaction gets to spend them.

Simple Translation into Lean

This is how we would write it in lean. In the spec there is no clear definition of what they consider a /Ledger/, I assume it is just a list of blocks.

In the spec, it is not clear how the different components are composed to /verify/ the All Valid Property.

def AllInputsValid.AllValid.AllValidProp (ledger : List BlockBody) : Prop

Equations

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

All valid Property from the spec. There are no mention of withdrawals here, maybe we should add something so it matches the other properties.

def AllInputsValid.AllValid.AllValidPropLocal (txs : List FlattenTransaction) (utxo_prev : List OutputRef) : Prop

Equations

• AllInputsValid.AllValid.AllValidPropLocal txs utxo_prev = ∀ t ∈ txs, ∀ i ∈ t.inputs, i ∈ utxo_prev ∧ ∀ t' ∈ txs, ¬t' = t → ¬t'.inputs.contains i = true

def AllInputsValid.AllValid.AllValidPropLocalBool (txs : List FlattenTransaction) (utxo_prev : List OutputRef) : Bool

Equations

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

Methodology

In this first PoC, I assume I have access to all the required data. Lateron, we will replace:

• List membership by MPT membership.
• List non-membership by MPT (Sorted Lists or Tries) non-membership.

Data retieval may be a bit different. We get some hashes from the State Queue, or recieve external data and verify it correct using hashes.

When it comes to the logic of /Optimistic properties/, we follow the same ideas stated in the Operators Directory module. We define a way to observe the property, to create a witness, and then, a way to /correct/ the state. Technically, we are not in a bad (/bad/ in the old ways) state, we allow such states to be reached, but we penalize the agents generating it.

NoInput Violation

There is a non-membership proof that may involve several others.

Definition

Spec:

   ∃ t ∈ txs, ∃ i ∈ spend_inputs(t)
    : (i ∉ utxos_prev)
    ∧ (∄ t_1 ∈ txs, t ≠ t_1 → tx_hash(t_1) = tx_hash(i))

Replaced by

   ∃ t ∈ txs, ∃ i ∈ spend_inputs(t)
    : (i ∉ utxos_prev)
    ∧ (hash(i) ∉ txs)

def AllInputsValid.NoInputViolation.NoInputProp (txs : List FlattenTransaction) (utxos_prev : List OutputRef) : Prop

Equations

• AllInputsValid.NoInputViolation.NoInputProp txs utxos_prev = ∃ t ∈ txs, ∃ i ∈ t.inputs, i ∉ utxos_prev ∧ ¬∃ t' ∈ txs, ¬t = t' ∧ TransactionHash.flat_tx_hash t' = i.id

noncomputable def AllInputsValid.NoInputViolation.NoInputPropBool (txs : List FlattenTransaction) (utxos_prev : List OutputRef) : Bool

The following property is noncomputable because flat_tx_hash is not computable.

Equations

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

Computation

Computation Finds a Witness

Computation finding one violation. Hashing is axiomatized, so we cannot run it.

TODO: Missing witnesses. We need to reconstruct the path so we can build the fraudproof. See findWitness?

noncomputable def AllInputsValid.NoInputViolation.Computation (prev : List TxId) (prev_ne : ¬prev = []) (txs : List FlattenTransaction) (txs_ne : ¬txs = []) : Option ((((OutputRef × ListSimulation.NonMemProof TxId × ListSimulation.NonMemProof Hash_64) × FlattenTransaction) × ListSimulation.Path) × ListSimulation.Path)

Equations

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

theorem AllInputsValid.NoInputViolation.Computation_correct {prev : List TxId} {txs : List FlattenTransaction} {i : OutputRef} {t : FlattenTransaction} {pi pt : ListSimulation.Path} {noi : ListSimulation.NonMemProof TxId} {not : ListSimulation.NonMemProof Hash_64} (prev_ne : ¬prev = []) (prev_sorted : List.Sorted (fun (x1 x2 : TxId) => x1 < x2) prev) (txs_ne : ¬txs = []) (txs_sorted : List.Sorted (fun (x1 x2 : Hash_64) => x1 < x2) (List.map TransactionHash.flat_tx_hash txs)) (H : Computation prev prev_ne txs txs_ne = some ((((i, noi, not), t), pi), pt)) : ListWitness.listIndex pt txs = some t ∧ ListWitness.listIndex pi t.inputs = some i ∧ ListSimulation.check_non_membership noi i.id prev prev_ne = true ∧ ListSimulation.check_non_membership not i.id (List.map TransactionHash.flat_tx_hash txs) ⋯ = true

Computation Returns None

If Computation returns none, it means we cannot build valid witnesses. If we cannot build a valid witness, it should mean the transaction is valid.

Therefore, all inputs are correct? Since i ∈ t.inputs, hash t cannot be the same as hash i.

theorem AllInputsValid.NoInputViolation.Computation_empty [LawfulBEq FlattenTransaction] {prev : List TxId} {txs : List FlattenTransaction} (assump : ∀ (tx : FlattenTransaction), ∀ i ∈ tx.inputs, ¬TransactionHash.flat_tx_hash tx = i.id) (prev_ne : ¬prev = []) (prev_sorted : List.Sorted (fun (x1 x2 : TxId) => x1 < x2) prev) (txs_ne : ¬txs = []) (txs_sorted : List.Sorted (fun (x1 x2 : Hash_64) => x1 < x2) (List.map TransactionHash.flat_tx_hash txs)) (H : Computation prev prev_ne txs txs_ne = none) (t : FlattenTransaction) : t ∈ txs → ∀ i ∈ t.inputs, (∃ t' ∈ txs, (!t == t' && decide (TransactionHash.flat_tx_hash t' = i.id)) = true) ∨ i.id ∈ prev

Computation Thread

structure AllInputsValid.NoInputViolation.State : Type

• t : FlattenTransaction
• spend_inputs : List OutputRef
• i : OutputRef
• txs : List FlattenTransaction
• txs_sorted : List.Sorted (fun (x1 x2 : Hash_64) => x1 < x2) (List.map TransactionHash.flat_tx_hash self.txs)
• txs_ne : ¬self.txs = []
• utxo_prev : List TxId
• utxo_prev_sorted : List.Sorted (fun (x1 x2 : TxId) => x1 < x2) self.utxo_prev
• utxo_prev_ne : ¬self.utxo_prev = []

inductive AllInputsValid.NoInputViolation.Input : Type

• Mem : ListSimulation.Path → Input
• NonMem : ListSimulation.NonMemProof TxId → Input
• Skip : Input

noncomputable def AllInputsValid.NoInputViolation.NoInputSteps [DecidableEq FlattenTransaction] : List (ScriptsDefinition.StepM State Input)

Equations

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

structure AllInputsValid.NoInputViolation.SortedBlockBody : Type

• block : BlockBody
• txs_ne : ¬self.block.transactions = []
• txs_sorted : List.Sorted (fun (x1 x2 : Hash_64) => x1 < x2) (List.map (fun (x : TxOrderId × MidgardTx) => TransactionHash.flat_tx_hash x.2) self.block.transactions)
• utxo_ne : ¬self.block.utxos = []
• utxo_sorted : List.Sorted (fun (x1 x2 : Hash_64) => x1 < x2) (List.map (fun (x : OutputRef × Output) => TransactionHash.output_hash x.2) self.block.utxos)

noncomputable def AllInputsValid.NoInputViolation.noinput_script [DecidableEq FlattenTransaction] (t : FlattenTransaction) (i : OutputRef) : ScriptsDefinition.Script SortedBlockBody State Input

Equations

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

def AllInputsValid.NoInputViolation.noinput_execution [DecidableEq FlattenTransaction] {st : SortedBlockBody} {noi : ListSimulation.NonMemProof TxId} {not : ListSimulation.NonMemProof Hash_64} {pi pt : ListSimulation.Path} {t : FlattenTransaction} {i : OutputRef} (H : Computation (List.map (fun (x : OutputRef × Output) => TransactionHash.output_hash x.2) st.block.utxos) ⋯ (List.map (fun (x : TxOrderId × MidgardTx) => x.2) st.block.transactions) ⋯ = some ((((i, noi, not), t), pi), pt)) : ScriptsDefinition.Execution (noinput_script t i) st [Input.Mem pt, Input.Mem pi, Input.NonMem noi, Input.NonMem not] = ScriptsDefinition.Ended.Ed

Equations

• ⋯ = ⋯

def AllInputsValid.NoInputViolation.noinput_execution_none [LawfulBEq FlattenTransaction] [DecidableEq FlattenTransaction] {st : SortedBlockBody} {noi not : ListSimulation.NonMemProof TxId} {pi pt : ListSimulation.Path} {t : FlattenTransaction} {i : OutputRef} (H : Computation (List.map (fun (x : OutputRef × Output) => TransactionHash.output_hash x.2) st.block.utxos) ⋯ (List.map (fun (x : TxOrderId × MidgardTx) => x.2) st.block.transactions) ⋯ = none) : ScriptsDefinition.Execution (noinput_script t i) st [Input.Mem pt, Input.Mem pi, Input.NonMem noi, Input.NonMem not] = ScriptsDefinition.Ended.Err

Equations

• ⋯ = ⋯

No Input IDX Violation

Definition

∃ t ∈ txs, ∃ i ∈ spend_inputs(t), ∃ t_1 ∈ txs
    : tx_hash(t_1) = tx_hash(i)
    ∧ i ∉ outputs(t_1)

def AllInputsValid.InputNOIDXViolation.InputNoIdxProp (txs : List FlattenTransaction) : Prop

Equations

• AllInputsValid.InputNOIDXViolation.InputNoIdxProp txs = ∃ t ∈ txs, ∃ i ∈ t.inputs, ∃ t' ∈ txs, TransactionHash.flat_tx_hash t' = i.id ∧ t'.outputs.length < i.index

noncomputable def AllInputsValid.InputNOIDXViolation.InputNoIdxPropBool (txs : List FlattenTransaction) : Bool

Equations

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

Computation

noncomputable def AllInputsValid.InputNOIDXViolation.Computation (txs acc : List FlattenTransaction) : Option FlattenTransaction

Equations

• One or more equations did not get rendered due to their size.
• AllInputsValid.InputNOIDXViolation.Computation [] acc = none

Computation Thread

structure AllInputsValid.InputNOIDXViolation.State : Type

• t : Transaction
• i : Transaction
• t1 : Transaction
• spend_inputs : List Transaction
• txs : List Transaction
• output_t1 : List Transaction
• i_idx : ℕ

inductive AllInputsValid.InputNOIDXViolation.Input : Type

• Mem : ListSimulation.Path → Input

noncomputable def AllInputsValid.InputNOIDXViolation.Steps [DecidableEq Transaction] : List (ScriptsDefinition.StepM State Input)

Equations

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

WithdrawnInput Violation

 ∃ t ∈ txs,
 ∃ i ∈ spend_inputs(t),
 ∃ w ∈ wtxs,
 i = l2_outref(w)

def AllInputsValid.WithdrawnInputViolation.WithdrawnInputProp (txs : List FlattenTransaction) (withdrawals : Withdrawals) : Prop

Equations

• AllInputsValid.WithdrawnInputViolation.WithdrawnInputProp txs withdrawals = ∃ t ∈ txs, ∃ i ∈ t.inputs, ∃ w ∈ withdrawals, i = w.2.l2_outref

def AllInputsValid.WithdrawnInputViolation.WithdrawnInputPropBool (txs : List FlattenTransaction) (withdrawals : Withdrawals) : Bool

Equations

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

Lean Computation function.

def AllInputsValid.WithdrawnInputViolation.Computation (txs : List FlattenTransaction) (withdrawals : Withdrawals) : Option (FlattenTransaction × OutputRef × OutputRef)

Equations

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

theorem AllInputsValid.WithdrawnInputViolation.Computation_correct {txs : List FlattenTransaction} {withdrawals : Withdrawals} {t : FlattenTransaction} {i w : OutputRef} (H : Computation txs withdrawals = some (t, i, w)) : t ∈ txs ∧ i ∈ t.inputs ∧ ∃ withdrawal ∈ withdrawals, withdrawal.1 = w ∧ withdrawal.2.l2_outref = i

theorem AllInputsValid.WithdrawnInputViolation.Computation_none {txs : List FlattenTransaction} {withdrawals : Withdrawals} (H : Computation txs withdrawals = none) (t : FlattenTransaction) : t ∈ txs → ∀ i ∈ t.inputs, ∀ w ∈ withdrawals, ¬w.2.l2_outref = i

Computation Thread

structure AllInputsValid.WithdrawnInputViolation.State : Type

• t : FlattenTransaction
• i : OutputRef
• w : OutputRef
• txs : List FlattenTransaction
• wtxs : Withdrawals

inductive AllInputsValid.WithdrawnInputViolation.Input : Type

• Mem : ListSimulation.Path → Input

def AllInputsValid.WithdrawnInputViolation.Steps [DecidableEq FlattenTransaction] : List (ScriptsDefinition.StepM State Input)

Equations

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

DoubleSpend Violation

Property:

∃ t ∈ txs,
∃ i ∈ spend_inputs(t),
∃ t_1 ∈ txs
 : ¬ t = t_1
 ∧ i ∈ spend_inputs(t_1)

def AllInputsValid.DoubleSpendViolation.DoubleSpendProp (txs : List FlattenTransaction) : Prop

Equations

• AllInputsValid.DoubleSpendViolation.DoubleSpendProp txs = ∃ t ∈ txs, ∃ i ∈ t.inputs, ∃ t' ∈ txs, ¬t = t' ∧ t'.inputs.contains i = true

def AllInputsValid.DoubleSpendViolation.DoubleSpendPropBool (txs : List FlattenTransaction) : Bool

Equations

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

Computation

def AllInputsValid.DoubleSpendViolation.Computation (txs : List FlattenTransaction) : Option (FlattenTransaction × OutputRef × FlattenTransaction)

Equations

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

theorem AllInputsValid.DoubleSpendViolation.Computation_correct {txs : List FlattenTransaction} {t : FlattenTransaction} {i : OutputRef} {t' : FlattenTransaction} (H : Computation txs = some (t, i, t')) : t ∈ txs ∧ t' ∈ txs ∧ ¬t = t' ∧ i ∈ t.inputs ∧ i ∈ t'.inputs

theorem AllInputsValid.DoubleSpendViolation.Computation_none {txs : List FlattenTransaction} (H : Computation txs = none) (t : FlattenTransaction) : t ∈ txs → ∀ i ∈ t.inputs, ∀ t' ∈ txs, ¬t = t' → i ∉ t'.inputs

Computation Thread

structure AllInputsValid.DoubleSpendViolation.State : Type

• t : FlattenTransaction
• i : OutputRef
• t' : FlattenTransaction
• txs : List FlattenTransaction

inductive AllInputsValid.DoubleSpendViolation.Input : Type

• Mem : ListSimulation.Path → Input

def AllInputsValid.DoubleSpendViolation.Steps [DecidableEq FlattenTransaction] : List (ScriptsDefinition.StepM State Input)

Equations

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

DoubleWithdraw Violation

Property:

 ∃ w, w_1 ∈ withdrawals
 : ¬ w = w_1
 ∧ l2_outref(w) = l2_outref(w_1)

def AllInputsValid.DoubleWithdrawViolation.DoubleWithdrawProp (wts : Withdrawals) : Prop

Equations

• AllInputsValid.DoubleWithdrawViolation.DoubleWithdrawProp wts = ∃ w ∈ wts, ∃ w' ∈ wts, ¬w.1 = w'.1 ∧ w.2.l2_outref = w'.2.l2_outref

def AllInputsValid.DoubleWithdrawViolation.DoubleWithdrawPropBool (wts : Withdrawals) : Bool

Equations

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

Computation

def AllInputsValid.DoubleWithdrawViolation.Computation (wts : Withdrawals) : Option (WithdrawalId × WithdrawalId)

Equations

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

theorem AllInputsValid.DoubleWithdrawViolation.Computation_correct {wts : Withdrawals} {w w' : WithdrawalId} (H : Computation wts = some (w, w')) : ∃ (wb : WithdrawalInfo) (wb' : WithdrawalInfo), (w, wb) ∈ wts ∧ (w', wb') ∈ wts ∧ ¬w = w' ∧ wb.l2_outref = wb'.l2_outref

theorem AllInputsValid.DoubleWithdrawViolation.Computation_none {wts : Withdrawals} (H : Computation wts = none) (w : Withdrawal) : w ∈ wts → ∀ w' ∈ wts, ¬w.1 = w'.1 → ¬w.2.l2_outref = w'.2.l2_outref

Computation Thread

structure AllInputsValid.DoubleWithdrawViolation.State : Type

• w : Withdrawal
• w' : Withdrawal
• wts : Withdrawals

inductive AllInputsValid.DoubleWithdrawViolation.Input : Type

• Mem : ListSimulation.Path → Input

def AllInputsValid.DoubleWithdrawViolation.Steps : List (ScriptsDefinition.StepM State Input)

Equations

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

Lemmas

We need to prove that our Computation Threads are checking the property we want.

Verification

We define a property AllValidProp and we claim that we can split it into different fraudproofs:

• NoInputProp
• InputNoIdxProp
• WithdrawnProp
• DoubleSpendProp
• DoubleWithdrawProp

However, these props are at different levels.

The main prop AllValidProp is at the ledger level and the other ones are at the block level.

theorem AllInputsValid.Complete.allinputs_complete (txs : List FlattenTransaction) (utxo_prev : List OutputRef) (withdrawals : Withdrawals) : AllValid.AllValidPropLocalBool txs utxo_prev = true ↔ (!NoInputViolation.NoInputPropBool txs utxo_prev && !InputNOIDXViolation.InputNoIdxPropBool txs && !WithdrawnInputViolation.WithdrawnInputPropBool txs withdrawals && !DoubleSpendViolation.DoubleSpendPropBool txs && !DoubleWithdrawViolation.DoubleWithdrawPropBool withdrawals) = true

Fraud Proof

In this section, we define the scripts and the fraudproofs as inductive types. We are forgetting about the different scripts steps and if they are proving the original statement or not.

In other words, this is a quick fix to have a mechanized implementation of the FraudProof mechanisim.

inductive AllInputsValid.FraudProof.AllInputsScript : Type

Scripts interface.

• NoInput (t : FlattenTransaction) (i : OutputRef) : AllInputsScript
• InputNoIdx : FlattenTransaction → OutputRef → FlattenTransaction → AllInputsScript
• WithdrawnInput : FlattenTransaction → OutputRef → Withdrawal → AllInputsScript
• DoubleWithdraw : Withdrawal → Withdrawal → AllInputsScript

inductive AllInputsValid.FraudProof.AllInputs (data : FPData) : AllInputsScript → Prop

• NoInputs {data : FPData} (t : FlattenTransaction) (i : OutputRef) : data.txs.contains (TransactionHash.flat_tx_hash t) = true → t.inputs.contains i = true → data.utxos_prev.contains i = false → data.txs.contains i.id = false → AllInputs data (AllInputsScript.NoInput t i)
• InpudNoIdx {data : FPData} (t : FlattenTransaction) (i : OutputRef) (t' : FlattenTransaction) : data.txs.contains (TransactionHash.flat_tx_hash t) = true → t.inputs.contains i = true → data.txs.contains (TransactionHash.flat_tx_hash t') = true → (TransactionHash.flat_tx_hash t' == i.id) = true → t'.outputs.length < i.index → AllInputs data (AllInputsScript.InputNoIdx t i t')
• Withdrawn {data : FPData} (t : FlattenTransaction) (i : OutputRef) (w : Withdrawal) : data.txs.contains (TransactionHash.flat_tx_hash t) = true → t.inputs.contains i = true → (List.contains data.wts w = true → (w.2.l2_outref == i) = true) = (true = true) → AllInputs data (AllInputsScript.WithdrawnInput t i w)
• DoubleWithdraw {data : FPData} (w w' : Withdrawal) : List.contains data.wts w = true → List.contains data.wts w' = true → ((!decide ((w == w') = true)) = true → (w.2.l2_outref == w'.2.l2_outref) = true) = (true = true) → AllInputs data (AllInputsScript.DoubleWithdraw w w')