Moved action specific predicates to actionWellFormed and fix a conformance failure

[Soupstraw]

Description

This PR moves the action-specific predicates in GOV-Propose to actionWellFormed and adds a check that makes sure all the receiving staking credentials of a TreasuryWithdrawal are registered when the proposal is made.

This probably requires some changes to the prose. It seemed like the prose about actionWellFormed was already outdated before these changes, because it only mentioned we check the parameter updates, but we also had some conditions about treasury withdrawals as well.

I also added two other predicate checks to the GOV rule which are present in the implementation:

• In GOV-Propose: the return address of a new proposal must be a registered staking credential
• In GOV-Vote: the proposal being voted for must not be expired

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

[WhatisRT]

Actually, now that I look at it I think it's better to move it into a separate helper function. The idea is that actionWellFormed follows this pattern: #31 And that's destroyed by adding these extra arguments.

[WhatisRT]

Looks pretty good, but actionValid and actionWellFormed are now in hidden code blocks, i.e. this removes actual logic from the PDF. I think just making the two functions but not the decision procedures visible is good enough right now, but it probably needs to be improved later.

Also, I'm not so sure about the usage of ∙ in the new functions. It makes sense, but it's not consistent with how we write non-STS predicates elsewhere. Maybe remove them for now and we can open a discussion about that in a new issue?

[williamdemeo]

Sorry @Soupstraw I didn't see this earlier. I'll review it today!

[williamdemeo]

I've moved actionValid and actionWellFormed out of the hidden code block and into a new figure. I also added prose near that figure to explain the logic, reduced the prose about this logic that was below the GOV rule figure (at the bottom of Gov.lagda), and replaced it with a reference to the new figure.

[williamdemeo]

I just pushed my suggested changes directly to your branch since they merely reorganize and document the code a bit. Otherwise, looks really nice. Good work!

[WhatisRT]

LGTM