Rule : At Least One Input

See Midgard Spec Section 5.1.3

Property

MinimumFee
= ∀ t ∈ Ledger:
    min_fee(t) <= tx_fee(t)

The spec claims that it is enough to check that:

MinFee-Violation
= ∃ t ∈ txs :
  tx_fee(t) < min_fee(t)

Logic Consistency

Placeholder section.

TODO: Check rule consistency.

inductive MinimumFee.FraudProof.MinimumFeeScript : Type

• MinFee (t : FlattenTransaction) : MinimumFeeScript

inductive MinimumFee.FraudProof.MinimumFee (b : FPData) : MinimumFeeScript → Prop