Rule : At Least One Input

See Midgard Spec Section 5.1.3

Property

AtLeastOneInput
= ∀ t ∈ Ledger:
    0 < |spend_inputs(t)|

The spec claims that it is enough to check that:

ZeroInput
= ∃ t ∈ txs :
  |spend_inputs(t)| = 0

There is a technical detail missing stating that the transaction (or transactions) belong to block b.

Invalid-Range
= ∃ b ∈ ledger, t ∈ b.txs :
  |spend_inputs(t)| = 0

Logic Consistency

Placeholder section.

TODO: Check rule consistency.

inductive AtLeastOneInput.FraudProof.AtLeastOneInputScript : Type

• InvalidRange (t : FlattenTransaction) : AtLeastOneInputScript

inductive AtLeastOneInput.FraudProof.AtLeastOneInput (b : FPData) : AtLeastOneInputScript → Prop

• InvalidRange {b : FPData} (t : FlattenTransaction) : b.txs.contains (TransactionHash.flat_tx_hash t) = true → t.inputs.length = 0 → AtLeastOneInput b (AtLeastOneInputScript.InvalidRange t)