Allow legacy dereg certs

[Soupstraw]

Description

This PR changes the DELEG-dereg rule so that the deposit can be zero. In the implementation the deposit is optional and if it's not provided, we translate that to a deposit of zero. The implementation does that for backwards compatibility because the previous eras did not have a deposit field in the dereg cert.

closes #636

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]

I think it'd make more sense to change the type of the deposit so that we can check d ≡ nothing instead. I guess the idea here is that the deposit must be there because of the previous line, so we don't need to check that the credential appears in the deposits map. Still looks a bit weird though...

[williamdemeo]

@WhatisRT, just to be clear, are you suggesting line 133 should be

    ∙ d ≡ nothing ⊎ (CredentialDeposit c , d) ∈ dep

...and change the type of the deposit so the above type-checks?

I must admit, I don't fully understand this change (beyond maybe "that's what the implementation does"). @Soupstraw could you explain?

[Soupstraw]

I changed the type of the deposit field to Maybe Coin and then added an additional check that the declared deposit is eihter nothing or just d, where d is equal to the deposit in the deposits map for the credential c. The former case is the "legacy" certificate which will be phased out in a future era and the latter is the one we want people to be using from Conway onwards.

[Soupstraw]

But both certificates are accepted in Conway, so it makes sense to also talk about it in the spec, because people who implement smart contracts should be aware that the legacy certificates also exist.

[WhatisRT]

LGTM. I just merged another PR though, so this needs a rebase

[WhatisRT]

Ah, you already did that, nevermind