Review the Conway diff spec

[WhatisRT]

Here are some things I've spotted in a quick first pass. I had hoped for this to be a short list, but it didn't really turn out that way.

To make progress on these items, it's probably best to tackle the items starting with the easiest and least controversial ones. What's left can then become its own issue, which may or may not be fixed before we tag a release version.

• Protocol Parameters:
  • Would be good to cite CIP-1694 for the groups more clearly
  • PParams should have its own figure
  • positivePParams has too long lines
• Fee calculation
  • with shouldn't show up in figures, can it be replaced by case?
  • Something isn't syntactically correct. Is there a where keyword missing?
  • A whole bunch of proof bits of the well-founded recursion are visible
• Transactions
  • The declaration of TransactionStructure is visible
• UTxO
  • Something needs to be done about ValidCertDeposits. It either needs to be properly explained or its definition visible. The latter is probably a bad idea because it uses indices IIRC.
  • The explanation for _≡?_ would probably be better in the Notation section.
  • Figure 16:
    • I think we can remove the universally quantified names at the beginning of the rules again, since MAlonzo bug: unreachable code reached agda/agda#7380 was fixed as part of Agda 2.7. It should be confirmed that this does not break conformance testing.
    • Lot's of open going on. Γ and s can probably be 'pattern-mached' at the bottom of the rule instead of using open on them. The open statements for tx and txb can probably just be hidden (we do that elsewhere too).
    • The only thing that actually changed here is the handling of the donations field, it would be good to highlight or mention that.
  • Figure 17 also has the same issue with open, but here we can't 'pattern-match'. At least we can hide the ones for tx and txb, the other two could be done by actual pattern-matching in the let-binding (see Fig. 20).
  • Figure 20 has broken alignment and is missing the actual let syntax
• Governance
  • Figure 21 has a broken caption
  • Relation _≈ᵍ_ should be explained better. Two actions relate with it if they modify the same piece of EnactState, which also means they can depend on each other (see hasParent). _≈ᵍ_ is called _≈_ in the prose.
  • Figure 22 doesn't need the 'Functions used in the GOV rules' label at the top, we never do that elsewhere
  • It was suggested on discord to rename GOV to GOVS and GOV' to GOV for consistency
  • Figure 26:
    • Pattern-matching on the records (i.e. vote and prop) would probably look cleaner if it was an actual pattern-match, i.e. flipping the sides. Then vote and prop would be the universally quantified variables instead. This probably also lets us get rid of the explicit quantification of x (the anchor).
    • The definition of GOV has a manually passed hidden argument
    • Again some open going on that could be removed for a pattern-match
• Certificates
  • Figure 30 has manually passed hidden arguments
  • Figure 31 has odd-looking line breaks.
  • A DELEG-reg rule seems to be missing
  • Figure 32, GOVCERT-regdrep has a visible open and quantified pp
• Ledger State Transition
  • What's up with that inconsistent section name?
  • It was suggested we rename _|ᵒ_. Maybe we can name it removeOrphanDRepVotes and stick that function that's currently named like that into a where block, giving it some simpler name? Does that helper function even need to exist?
  • Figure 35: lots of open going in that could be changed into real or fake pattern-matching
  • Should make a note that LEDGER-I did not change
• Ratification
  • Lots of question marks showing up in Figure 41. Can we get rid of those?
  • Figure 42 has a _<$>_. Is there a good way to get rid of it so we don't have to explain it? Otherwise it needs to be explained in the Notation section. Refactor accepted predicate in Ratify #702
  • acceptConds in Figure 43 looks broken
  • Figure 44: lots of quantification and opening going on, also a manually passed hidden argument at the bottom
  • Rename RATIFY' to RATIFY and RATIFY to RATIFIES
• Epoch boundary
  • Not the first time this comes up, but Figure 47 is still somewhat messy. Are there some good helper functions that could be defined to clean it up? Constructing big records could also become cleaner with vertical vectors maybe?

[williamdemeo]

Regarding the hiding (or not) the use of open, I wanted to preserve the comments @WhatisRT made about this from an old closed PR:

"open can't just be hidden from view, since it carries a lot of meaning. For example, in EPOCH it does some of the actual work. Rather, we should use techniques that avoid using open in the code, like for example pattern-matching on a state/environment when defining rules, instead of binding it to a single name and then writing open State s. Another option would be to use some kind of deep accessors to avoid nested opens and then applying those deep accessors to our variables. What's right needs to be decided on a case-by-case basis."

[carlostome]

≈ᵍ should be explained better. Two actions relate with it if they modify the same piece of EnactState, which also means they can depend on each other (see hasParent). ≈ᵍ is called ≈ in the prose.

It seems to me that maybe this should be called something self-explanatory, like SameKind, instead of yet another made up "equality" symbol.

Moreover, maybe it should be defined primitively instead of relying on govActionPriority

[WhatisRT]

Both of these suggestions seem good to me! Though I feel like SameKind sounds a bit too generic, maybe ModifySameState? OTOH I don't really like these long names...

[carlostome]

SameGAKind, (I like that it includes the word "kind" since it is what the text uses:

... used for determining whether two actions are of the same “kind” ...

That said, we can change both the name and the text explanation and get rid of the concept of "kind". WDYT?

For define in it primitively I'll open a different issue.

[WhatisRT]

Ah, that makes sense then! Maybe it makes sense to define this properly in the prose: 'we say that two GAs are of the same kind if they modify the same piece of EnactState'. Maybe a different word than 'kind' would fit this better, but nothing comes to mind right now. Or I don't mind getting rid of all of that entirely, if you have a good idea for that!

[carlostome]

For consistency with

It was suggested on discord to rename GOV to GOVS and GOV' to GOV for consistency

shall we also rename RATIFY' to RATIFY and RATIFY to RATIFYS (or RATIFIES)?

[WhatisRT]

Sounds good!

[carlostome]

Both of these suggestions seem good to me! Though I feel like SameKind sounds a bit too generic, maybe ModifySameState? OTOH I don't really like these long names...

What about "overlap" as a concept. Two governance actions overlap iff they modify the same piece of state.

[WhatisRT]

I really like that name!