Rule : All Referenece Inputs Must be Valid.

See Midgard Spec Section 5.1.3

Property

AllReferenceInputsValid
= ∀ t ∈ Ledger, ∀ r ∈ reference_inputs(t)
  : (∃ t_1 ∈ Ledger, t_1 ≼ t ∧ r ∈ outputs(t_1))
  ∧ (∄ t_2 ∈ Ledger, t_2 ≺ t ∧ r ∈ spent_inputs(t_2))

The spec claims that it is enough to check that:

NO-Reference-Input
= 

REFERENCE-INPUT-NO-IDX
= 

Logic Consistency

Placeholder section.

TODO: Check rule consistency.

inductive AllReferenceInputsValid.FraudProof.AllReferenceInputsValidScript : Type

• NoReferenceInput (t : FlattenTransaction) (i : OutputRef) : AllReferenceInputsValidScript
• ReferenceInputNoIdx (t : FlattenTransaction) (i : OutputRef) (t1 : FlattenTransaction) : AllReferenceInputsValidScript

inductive AllReferenceInputsValid.FraudProof.AllReferenceInputsValid (b : FPData) : AllReferenceInputsValidScript → Prop

• NoReferenceInput {b : FPData} {x✝ : AllReferenceInputsValidScript} : AllReferenceInputsValid b x✝
• ReferenceInputNoIdx {b : FPData} {x✝ : AllReferenceInputsValidScript} : AllReferenceInputsValid b x✝