Mismatch between formal and executable UProp type and UPPVV rule

IntersectMBO / cardano-ledger

The ledger implementation and specifications of the Cardano blockchain.

Apache License 2.0

258 stars 158 forks source link

Mismatch between formal and executable UProp type and UPPVV rule #1024

Closed jmhrpr closed 2 years ago

jmhrpr commented 4 years ago

In the executable ledger spec the UProp type doesn’t seem to have a field for the update proposal size despite an abstract function “upSize” being defined in the formal ledger spec Chapter 6.1, p.20, Figure 20. Following this, in the formal ledger spec Chapter 6.2, p.23, Figure 25: Update proposals validity rules, the proposal size is checked against the maxProposalSize which is defined in the protocol parameters. This is not implemented in the executable spec.

JaredCorduan commented 2 years ago

Development of Byron code has been frozen and only potential security fixes will be applied in the future