Define a step function to run the EPOCH rule from the specification #925
Conversation
|
Enabling this shows a new error when reenabling the test Delegate, retire and re-register pool of #640. The error is explained in IntersectMBO/cardano-ledger#5306. |
| EpochStateToConf : EpochSpec.EpochState ⭆ EpochState | ||
| EpochStateToConf .convⁱ deposits epochSt = | ||
| let open EpochSpec.EpochState epochSt in | ||
| ⟦ acnt , ss , certDeposits ls ⊢conv ls , es , fut ⟧ᵉ' |
There was a problem hiding this comment.
Look here. I started imitating LStateToConf to define this. However, LStateToConf does not call to certDeposits. Is that a bug? AFAIU, the LState should have the deposits needed for the conversion to the conformance state.
There was a problem hiding this comment.
I think this is just a matter of preference. You can either get the deposits from LState, or you pass in a pair and then call certDeposits somewhere earlier. Maybe it was just more convenient like that because of module dependencies or something.
facundominguez
force-pushed
the
fd/spec-epoch-step
branch
from
5baa74e to
241c8f3
Compare
facundominguez
force-pushed
the
fd/spec-epoch-step
branch
from
241c8f3 to
a1282e6
Compare
|
Is the idea to extract better error messages to be able to narrow down conformance failures? If that's the case, it might be worth trying to invest a bit of time into thinking about more general solutions. Maybe there's a way to nicely augment the |
|
👋 The motivation for this PR is to avoid duplicating in the conformance model the logic of the specification model. I just added this to the description of the PR. |
|
Ah, I see. In this case just ignore my comment. |
2 participants
By running the rule from the specification, we can avoid duplicating in the conformance model the logic of the specification model.