Made CERTBASE get applied at the end of CERTS

[Soupstraw]

Description

Previously the CERTBASE rule was applied to the state before the CERT transitions happened, but this caused the DRep delegations not get removed when the DRep was removed with the deregdrep certificate.

I've modified CERTS so that CERTBASE now gets applied last, after all of the certificates have been applied. I also moved reward withdrawals from CERTS to LEDGER.

closes #635

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]

Good catch!

I see where the problem comes from:

ReflexiveTransitiveClosureᵇ' has nothing to do with a basecase (as the superscript seems to indicate) but about nonemptyness.

Maybe you can remove this definition (and _⊢_⇀⟦_⟧*'_ which doesn't seem to be used anywhere) as part of this PR? (if not please open an issue so we keep track of it)

[Soupstraw]

ReflexiveTransitiveClosureᵇ' just runs the base case as the first step and the one without tick runs the base case as the last step. I realized that this solution creates some new problems, because some conditions in CERTBASE actually need to be checked on the initial state.

[carlostome]

What conformance test issue does this address?

[Soupstraw]

@carlostome I added the issue number above

[williamdemeo]

@Soupstraw I'm going to see if I can modify your PR so that it addresses the conformance test issue (#635) while also preserving the changes I made a while back to resolve issue #545 (PR 604).

[williamdemeo]

@Soupstraw I see you moved these two premises to the LEDGER rule. Could you explain why they can't remain here? (I need them here for the proof of the CERTBASE-pov lemma, which is used in the proof of CERTS-pov.)

[Soupstraw]

The problem with the first premise is that in the implementation we check it in the LEDGER rule. I guess we could keep it in the same place in the spec and change the implementation instead. The important part is that it's still checked before the certs are applied, like it was before this PR.

The thing that was wrong was that validVoteDelegs was applied before the certificates had been applied. This caused DRep delegations to not get removed when the transaction had a unregdrep certificate, because the filter function used the old dReps map, where the DRep was still registered.

I think the second one could actually stay here as well if we call CERTBASE at the start, but I think it makes way more sense to do anything related to withdrawals in the LEDGER rule. The fact that we do the withrawals logic in CERTS is because that's how it was done in Shelley, before we had a dedicated CERTS rule. The withdrawals don't really have anything to do with certificates, so I don't think it makes sense to keep it here, and I've talked with @WhatisRT and @lehins about this and they both agreed. I've already moved that check to LEDGER in the implementation, so I think it'd be good to do it here also.

I think the best solution would be to have two base cases in the CERTS rule, one that gets applied at the start and then another that gets applied at the end. That way we can do the checks before we apply the certificates, and then update the voteDelegs only once we have applied all the certificates.

[williamdemeo]

Okay, I'll have to take a closer look at this to refresh my memory and really understand exactly what's going on. My impression was that the premises that were moved were required for the CERTS-pov proof... but it's possible the statement of that property turns out to be wrong and/or not actually what we want. I think you understand this issue better than anyone right now, so I trust your judgment on it, and would be grateful if you could take some time at the water cooler today to explain it. I will then help with this PR by fixing the CERTS-pov theorem statement and construct a new proof of it.

[williamdemeo]

It seems too much has changed here for me to be able to recover the proof of CERTBASE-pov and fix the type-checking errors in this PR. (@Soupstraw, does this type-check on your machine?)

I recommend either (a) revert some of the changes (and, if necessary, modify the Haskell implementation so conformance tests pass) OR (b) somehow find a new proof of pov for CERTS that doesn't use the preconditions that were moved from CERT-base to LEDGER.

Since I'm not sure (b) is possible, I vote for (a). Perhaps it's just a matter of moving the two premises back to CERT-base.

By the way, I was able to fix some of the type-checking errors by copying the changes you made to LEDGER-V in Conformance/Ledger.agda over to LEDGER-V in Ledger/Ledger.lagda. (I didn't push those changes because I don't want to contaminate your PR with another commit that doesn't type-check, and since I suspect that won't provide a path to a complete solution.)

[williamdemeo]

The PR doesn't type check right now. (Please see other comments.)

[Soupstraw]

@williamdemeo I thought that if nix-build -A ledger.hsSrc succeeds, then all of the files typecheck, but I guess it only needs the conformance spec to typecheck. I'll see if I can figure out the PoV proofs.

[williamdemeo]

@williamdemeo I thought that if nix-build -A ledger.hsSrc succeeds, then all of the files typecheck, but I guess it only needs the conformance spec to typecheck. I'll see if I can figure out the PoV proofs.

Sure, but I can also help with the pov proofs. As I mentioned above, it's possible we will need to adjust the statements of the properties we're proving.