formal-ledger-specifications icon indicating copy to clipboard operation
formal-ledger-specifications copied to clipboard

Published 20 hours ago • verified publisher icon IntersectMBO

Well-formedness properties

Open WhatisRT opened this issue 2 years ago • 2 comments

There are many properties that are currently part of the rules, which don't really fit into any particular rule thematically, and don't depend on anything but the signal. We could call these 'well-formedness properties', and bundle all of them into one place for them to be checked. This should improve consistency and readability of the STS rules.

Here are some:

  • Addresses
    • Byron: bootstrapAddrsSize <= 64
    • Maybe networkID = NetworkID, though this needs access to global constants
  • Transactions
    • txADhash ≡ map hash txAD
    • Maybe txins ≢ ∅
    • Maybe coin mint ≡ 0
  • PParams has paramsWellFormed
  • More for blocks (once we have those), maybe others

WhatisRT avatar Nov 23 '22 15:11 WhatisRT