641-incorporate-feedback-from-the-second-audit

[carlostome]

Addresses #641

TODO (partial):

• Combine sections 1 and 2 (Combine Sections 1 and 2 #686)
• Rename security group's threshold parameter from Q5e to Q5 (Sec. 3, pp. 8-9)
• Add security-relevant parameters to Fig 3 (Sec. 3, pp. 9) (related to Added some protocol parameters to the security group #660)
• Explain UpdateT and how its used to check wellformedness (Sec. 3, pp. 8)
• Add explanation of actionWellFormed for the case of TreasuryWdrl, and address the question: should the parameter x : RwdAddr ⇀ Coin be also wellformed? (Sec. 4, pp. 11-12) (yes, solved by Moved action specific predicates to actionWellFormed and fix a conformance failure #673)
• Add description of refInputs (Sec. 5, pp 15) (not needed)
• Clarify the purpose of curTreasury and txdonation (Sec. 5, pp. 15)
• Highlight txid (Sec. 5, pp. 15)
• the type synonym Deposits is used in Sec. 6 (Figs. 12 and 13) but introduced in Sec. 8, Fig. 23
• Clarify the motivation for allowing anyone to vote for any role even if the vote is invalid (during ratification).* (Sec. 7, pp. 21)
• Suggestion to put back definition of cwitness (Sec. 8) (not needed)
• Explain if making deposits explicit (Sec. 8.2) prevents issues if deposit amounts could be changed. (Sec.8 pp. 23) (see comment)
• Combine sections 8.1 to 8.3 as features of delegation in Conway. Emphasize 8.3 more. (Sec.8, pp. 23-24)
• Add English text explanation for Figs. 30 and 31 (Sec. 9, pp 33-34) (outdated)
• Rename Enact-NewComm to Enact-UpdComm (Sec. 10, pp. 31)
• In Sec. 11.1, clarify whether threshold x is meant as a fraction to the total stake of all votes, and how is the total stake counted for the purpose of counting if an action passes. (Sec. 11.1, pp. 39)
• Should NewEpochState be part of Conway? if so add it to Fig. 41. (Sec. 12, pp. 46) (not needed)
• Add English text explanation of Fig. 42. (Sec. 12, pp. 46) (outdated)
• Add explanation why fees is not used when computing treasury in Fig. 43. (Sec. 12, pp. 48) (outdated)
• In sentence "To form an EnactState, some governance action IDs need to be provided." Is the reason some governance action IDs need to be provided because of prevAction needing an ID to hash? (see comment)
• Possible issue/clarification question. In bootstrapping the governance system (App C), who will be part of the constitution committee, if only TriggerHF, ChangeParams, and Info are allowed (and UpdateCommittee is not allowed)? It seems that unless there is already a CC, this might be a problem since TriggerHF and ChangeParams both need the CC to approve. Suggestion. Describe where the initial CC comes from in App C. (see comment)

Checklist

• Commit sequence broadly makes sense and commits have useful messages
• Any semantic changes to the specifications are documented in CHANGELOG.md
• Code is formatted according to CONTRIBUTING.md
• Self-reviewed the diff

[carlostome]

• the type synonym Deposits is used in Sec. 6 (Figs. 12 and 13) but introduced in Sec. 8, Fig. 23

module UTxO imports Certs but appears before in the PDF. Either we rearrange the order of imports or inline the definition.

WDYT? @WhatisRT @williamdemeo

[williamdemeo]

• the type synonym Deposits is used in Sec. 6 (Figs. 12 and 13) but introduced in Sec. 8, Fig. 23

module UTxO imports Certs but appears before in the PDF. Either we rearrange the order of imports or inline the definition.

WDYT? @WhatisRT @williamdemeo

I think the simplest thing to do would be to leave the ordering as it is and in the first place where Deposits is used we note that it is defined later, in Sec 8, Fig 23, with a reference/link to that section.

[WhatisRT]

Here are some answers to the open items. If you have further questions let me know!

Clarify the motivation for allowing anyone to vote for any role even if the vote is invalid (during ratification).* (Sec. 7, pp. 21)

I assume that's still in the prose, but we aren't actually doing this anymore because there was a memory attack if it was allowed. You could spam votes on irrelevant things, and it would fill up the state faster & cheaper than we want to allow. We now have things like canVote and isRegistered to prevent this. But generally the idea was that we don't care if you cast invalid votes, they don't affect the results and get garbage collected eventually anyway. The issue was that they first stay around for a month or so, which was long enough to enable the attack.

Suggestion to put back definition of cwitness (Sec. 8)

It's a Shelley-era thing that hasn't meaningfully changed since then, and the reviewed spec just shows changes. So it makes sense to be hidden here but it should be visible in the full spec.

Explain if making deposits explicit (Sec. 8.2) prevents issues if deposit amounts could be changed. (Sec.8 pp. 23)

I'm not sure where an issue would arise, this is just giving an extra annotation that is being checked for correctness. Previously the ledger would compute deposits for you, so when making a transaction with certificates it was harder to know if it balances properly because you'd have to mimic the calculations the ledger does. Now you just add up all the numbers in there, and if the transaction is valid this sum is guaranteed to be what you pay/receive.

In Sec. 11.1, clarify whether threshold x is meant as a fraction to the total stake of all votes, and how is the total stake counted for the purpose of counting if an action passes. (Sec. 11.1, pp. 39)

This is explained by acceptedStakeRatio and acceptedBy in Fig. 38. We compare the stake of yes votes with the stake of yes and no votes to the threshold, and if it's greater or equal it's accepted. Note that these don't need to be 'physical' votes, there are plenty of ways in which we default or discard votes in certain scenarios. See actualVotes for that. We use use the map of votes produced by actualVotes for all vote counting.

Should NewEpochState be part of Conway? if so add it to Fig. 41. (Sec. 12, pp. 46)

No, it didn't change.

Add explanation why fees is not used when computing treasury in Fig. 43. (Sec. 12, pp. 48)

I think this question is because in the first audit it was. However, that was just a shortcut I took early in writing the Conway spec and was completely incorrect. The mechanism that moves and distributes transaction fees is applyRUpd.

In sentence "To form an EnactState, some governance action IDs need to be provided." Is the reason some governance action IDs need to be provided because of prevAction needing an ID to hash?

Yes.

Possible issue/clarification question. In bootstrapping the governance system (App C), who will be part of the constitution committee, if only TriggerHF, ChangeParams, and Info are allowed (and UpdateCommittee is not allowed)? It seems that unless there is already a CC, this might be a problem since TriggerHF and ChangeParams both need the CC to approve. Suggestion. Describe where the initial CC comes from in App C.

Yes, bootstrapping was done with an interim CC. I'm not sure how exactly the members were selected, but it's not really in scope of the spec anyway. We can just say that it's required to supply a sensible initial value.

[WhatisRT]

The PDF has an error when building, but the diff looks good so far. I'll approve it when the error is fixed and I've had a look at the PDF.

[carlostome]

The PDF has an error when building, but the diff looks good so far

I can't reproduce the build error locally. nix-build -A ledger.docs runs successfully on my machine. Any ideas @WhatisRT?

[WhatisRT]

I didn't run it myself, I just looked at the CI output: https://github.com/IntersectMBO/formal-ledger-specifications/actions/runs/13304598502/job/37331617849#step:4:6165

I'm surprised there would be different behaviour on different systems with an error like this. Maybe you had some uncommitted changes?

[WhatisRT]

LGTM