Make STS rules above UTXO era-independent. #1922
Conversation
| @@ -108,9 +113,6 @@ applyTxs :: | |||
| forall era m. | |||
| ( STS (LEDGERS era), | |||
| BaseM (LEDGERS era) ~ ShelleyBase, | |||
There was a problem hiding this comment.
| BaseM (LEDGERS era) ~ ShelleyBase, |
We can remove the line above, it compiles for me without it.
Or am I missing something? 🤔
There was a problem hiding this comment.
Hmm, interesting. I wonder why I didn't see an "unneeded" warning.
| @@ -127,9 +126,6 @@ applyBlockTransition :: | |||
| forall era m. | |||
| ( STS (STS.BBODY era), | |||
| BaseM (STS.BBODY era) ~ ShelleyBase, | |||
| Environment (STS.BBODY era) ~ STS.BbodyEnv era, | ||
| State (STS.BBODY era) ~ STS.BbodyState era, | ||
| Signal (STS.BBODY era) ~ Block era | ||
| BaseM (STS.BBODY era) ~ ShelleyBase |
shelley/chain-and-ledger/executable-spec/src/Shelley/Spec/Ledger/STS/Utxow.hs
Outdated
Show resolved
Hide resolved
| @@ -310,9 +321,28 @@ utxoWitnessed = | |||
| TRC (UtxoEnv slot pp stakepools genDelegs, u, tx) | |||
|
|
|||
| instance | |||
There was a problem hiding this comment.
It seems that each constraint on the STS instance of UTXOW is needed here too. I haven't look at Embed closely, but it's kind of strange that we really need all of these constraints just to embed one error into another.
There was a problem hiding this comment.
Embed has a superclass constraint of STS
| DSignable c (Hash c EraIndependentTxBody), | ||
| ShelleyBased era, | ||
| DSignable c (Hash c EraIndependentTxBody), |
nc6
force-pushed
the
nc/era-indep
branch
2 times, most recently
from
2e15914
to
a33914f
Compare
nc6
force-pushed
the
nc/era-indep
branch
5 times, most recently
from
3c5dc4f
to
a02d163
Compare
Honestly it's embarassing that I failed to notice that this worked. We carry a few more constraints in the STS instances and Embed instances. But the payoff is that we only have to override the specific rules we want to change in each era, and not re-plumb everything. Obviously this means that, in the future, if we make a change in a different rule then we have to go back and turn the era-independent one into an era-dependent version (and add instances for all intermediate eras). But still, this feels like a definite improvement.
|
Huh, |
|
bors merge |
1922: Make STS rules above UTXO era-independent. r=mrBliss a=nc6 Honestly it's embarassing that I failed to notice that this worked. We carry a few more constraints in the STS instances and Embed instances. But the payoff is that we only have to override the specific rules we want to change in each era, and not re-plumb everything. Obviously this means that, in the future, if we make a change in a different rule then we have to go back and turn the era-independent one into an era-dependent version (and add instances for all intermediate eras). But still, this feels like a definite improvement. Co-authored-by: Nicholas Clarke <nicholas.clarke@iohk.io>
| DSignable c (Hash c EraIndependentTxBody) | ||
| ( Era era, | ||
| ShelleyBased era, | ||
| STS (UTXOW era), |
There was a problem hiding this comment.
I think this constraint is causing CI to time out in https://hydra.iohk.io/build/4513046/nixlog/1.
The test case in question:
testCase "don't spend from a bootstrap address" testBootstrapNotSpending
| STS (CHAIN era), | ||
| STS (BBODY era) | ||
| ) => | ||
| Embed (BBODY (ShelleyEra c)) (CHAIN (ShelleyEra c)) | ||
| Embed (BBODY era) (CHAIN era) |
There was a problem hiding this comment.
Is this right?
Note that the STS (CHAIN era) instance above has a Embed (BBODY era) (CHAIN era) constraint, i.e., this instance. Since this instance has a STS (CHAIN era) constraint, there is a cycle.
Embed (BBODY era) (CHAIN era),
| VRF.Signable (VRF c) Seed | ||
| ( Era era, | ||
| ShelleyBased era, | ||
| STS (CHAIN era) |
| VRF.Signable (VRF c) Seed | ||
| ( Era era, | ||
| ShelleyBased era, | ||
| STS (CHAIN era), |
| ( Era era, | ||
| c ~ Crypto era, | ||
| ShelleyBased era, | ||
| STS (CHAIN era), |
Hmm, I'm not sure whether these cycles are problematic. I'm just suspicious because of the tests timing out. |
`Embed sub super` has the `STS super` super-class constraint, but `Embed sub
super` is almost always used as a super-class constraint of `Embed sub super`
itself. This is a cycle. My hypothesis is that these cycles are fine, *until*
you start relying on constraints that are implied by them, because the
corresponding dictionaries will be recursive too. I believe this is what caused
some tests to hang.
To remedy this, remove the `STS super` super-class constraint from the `Embed`
class. Next, remove the new redundant constraints and add the constraints that
are now missing.
Finally, remove the cycle between each pair of `Embed` and `STS` instances. For
example:
```diff
instance
( ..
Embed (UTXO era) (UTXOW era),
..
) =>
STS (UTXOW era)
where
..
instance
( ..
- STS (UTXOW era),
..
) =>
Embed (UTXO era) (UTXOW era)
where
..
```
|
Canceled. |
|
I just pushed a commit removing – what I think – are cycles between |
|
bors merge |
2702: Update dependencies r=mrBliss a=mrBliss Highlights: * IntersectMBO/cardano-ledger#1915 * IntersectMBO/cardano-ledger#1922 * IntersectMBO/cardano-ledger#1902 * IntersectMBO/cardano-ledger#1923 * IntersectMBO/cardano-ledger#1927 * IntersectMBO/cardano-ledger#1929 Co-authored-by: Thomas Winant <thomas@well-typed.com>
Honestly it's embarassing that I failed to notice that this worked. We
carry a few more constraints in the STS instances and Embed instances.
But the payoff is that we only have to override the specific rules we
want to change in each era, and not re-plumb everything.
Obviously this means that, in the future, if we make a change in a
different rule then we have to go back and turn the era-independent one
into an era-dependent version (and add instances for all intermediate
eras). But still, this feels like a definite improvement.