Rule : Required Signatures are Correct

See Midgard Spec Section 5.1.5

Property

RequiredSignatures
= ∀ t ∈ txd:
  required_signer_hashes(t)
    = { paymentHK(addr(u)) | (r,u) ∈ utxos ∧ r ∈ spend_inputs(t) ∧ addr(u) ∈ Addr^{vkey} }

The spec claims that it is enough to check that:

Missing-Req-Signer-TX
=

Missing-Req-Signer-UTXO
=

NON-Req-Signer
=
=

Logic Consistency

Placeholder section.

TODO: Check rule consistency.

inductive RequiredSignatures.FraudProof.RequiredSignaturesScript : Type

inductive RequiredSignatures.FraudProof.RequiredSignatures (b : FPData) : RequiredSignaturesScript → Prop