Rule : Transaction Validity Range

See Midgard Spec Section 5.1.2

Property

TxValidityRange
= ∀ f ∈ Ledger:
  time_range(block(t)) ⊆ validity_interval(t)

The spec claims that it is enough to check that:

Invalid-Range
= ∃ t ∈ txs :
  time_range(b) ⊈ validity_interval(t)

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

Invalid-Range
= ∃ b ∈ ledger, t ∈ b.txs :
  time_range(b) ⊈ validity_interval(t)

Logic Consistency

Placeholder section.

TODO: Check rule consistency.

inductive TransactionValidityRange.FraudProof.ValidityRangeScript : Type

• InvalidRange (t : FlattenTransaction) : ValidityRangeScript

inductive TransactionValidityRange.FraudProof.ValidityRange (b : FPData) : ValidityRangeScript → Prop

• InvalidRange {b : FPData} (t : FlattenTransaction) : b.txs.contains (TransactionHash.flat_tx_hash t) = true → some b.start_time < t.validityInternal.lower ∨ t.validityInternal.upper < some b.end_time → ValidityRange b (ValidityRangeScript.InvalidRange t)