STS Evolution #1804
Closed
STS Evolution #1804
Conversation
This file contains bidirectional Unicode text that may be interpreted or compiled differently than what appears below. To review, open the file in an editor that reveals hidden Unicode characters.
Learn more about bidirectional Unicode characters
nc6
requested review from
WhatisRT,
JaredCorduan,
TimSheard,
redxaxder and
polinavino
redxaxder
reviewed
Aug 24, 2020
|
|
||
| deriving stock instance Show (Base.AdminPredicateFailure Era_1) | ||
|
|
||
| instance STS ADMIN where |
There was a problem hiding this comment.
This looks like a case where the extension's ADMIN is just the base ADMIN with the era changed.
If type variable on the rule was brought back, would this instance be free?
There was a problem hiding this comment.
Not sure it would be free, but we might be able to derive it easily.
There was a problem hiding this comment.
Something like...
instance SomeConstraint e => STS (ADMIN e) where
type Environment (ADMIN e) = ()
type State (ADMIN e) = BT.Accounting e
type Signal (ADMIN e) = Base.Admin e
type PredicateFailure (ADMIN e) = Base.AdminPredicateFailure e
initialRules = []
transitionRules = [Base.processAdmin @(ADMIN e) @e]
dnadales
reviewed
Aug 24, 2020
| type instance BT.Op Era_0 = Op Era_0 | ||
|
|
||
| newtype Accounting e = Accounting | ||
| { unAccounting :: Map (BT.AccountName e) (BT.Account e) |
There was a problem hiding this comment.
Do the elements of the map also contain an AccountName? If so, is an invariant of this type that the account name of a key should be the same as the account name of the element at that key? Also if this is correct, why does Account need the account name as well?
There was a problem hiding this comment.
They do, it is, and because this ledger was only an example and I didn't stop to make it nice :-D
dnadales
reviewed
Aug 24, 2020
|
|
||
| data Block e = Block | ||
| { blockId :: BT.BlockId e, | ||
| blockOps :: [BT.Op e] |
There was a problem hiding this comment.
Are blockOps the block payload (transactions) or is this a different thing?
There was a problem hiding this comment.
Yep. I should probably have left it as Tx, but then I had used that for a more specific type and was lazy...
dnadales
reviewed
Aug 24, 2020
| extract tx | ||
| ) | ||
| ) | ||
| trans @ops (TRC (env, inject txs st, inject xs ops)) |
There was a problem hiding this comment.
Does the call to trans here means that trans @ops has to modify the entire State tx?
There was a problem hiding this comment.
Hmmm, no, since this is an ops transition rule trans @ops should modify State ops.
This demonstrates adding an extension module which introduces multi-currency.
This allows us to add extra fields.
nc6
force-pushed
the
nc/sts-evolution-2
branch
from
af5b08a
to
77622ef
Compare
|
Closing this PR now, since it was only up to showcase an idea. |
nc6
added a commit
that referenced
this pull request
Sep 9, 2020
This PR demonstrates a way to parametrise the ledger over value. It paves the way for overriding this type in subsequent eras, without making any semantic changes to the Shelley ledger. Functions in the ledger are now classfied into three groups: - Those that remain universally quantified over eras. - Those that have specific requirements on certain era-parametrised types to work (e.g. that they can be serialised), and - Those that are specific to Shelley. There are two examples of the latter: `consumed` and `produced`. The STS rules are likewise split in two: - Those that remain universally quantified over eras. - Those that are specific to Shelley. The intention is that many will transition to the third (missing) category, where the actual rules specify their exact requirements on the era (see #1804 for an example of how to do this). This was not done because I wanted to get this ready for the meeting and I didn't have time. This PR makes some very deliberate design choices: - The 'Value' type family and any constraints thereon are _not_ lifted into the 'Era' class. Such would imply universality over eras, which is too strong a constraint. They would prevent us, for example, from adding to the `Val` class in future eras, which seems quite plausible. Furthermore, having more explicit constraints at the use site helps our understanding of the code; it is much more obvious _when_ we are relying on certain things, which can be a tool to spot bugs. Note that these constraints do not propogate wildly, because in general they are dispatched through the instantiation of the type family to a specific type in a given era. - It deliberately removes some instances (`Eq` for example) where it seems there is no strong reason to have it. The presence of an `Eq` instance everywhere has bitten us in the past, where for example we have ended up calling `(==)` on a large part of state in the consensus integration, which is an expensive operation. Honestly, I suspect I'll have to add these back to get the tests working, since they rely on them, but I think there's a decent case for making these instances orphans in the testing code instead. This is a *draft* PR for discussion. It does not yet touch the testing code, and is inconsistent about various things (in particular, I stuck `era ~ Shelley c` in a lot of places in a hurry).
polinavino
pushed a commit
that referenced
this pull request
Sep 24, 2020
This PR demonstrates a way to parametrise the ledger over value. It paves the way for overriding this type in subsequent eras, without making any semantic changes to the Shelley ledger. Functions in the ledger are now classfied into three groups: - Those that remain universally quantified over eras. - Those that have specific requirements on certain era-parametrised types to work (e.g. that they can be serialised), and - Those that are specific to Shelley. There are two examples of the latter: `consumed` and `produced`. The STS rules are likewise split in two: - Those that remain universally quantified over eras. - Those that are specific to Shelley. The intention is that many will transition to the third (missing) category, where the actual rules specify their exact requirements on the era (see #1804 for an example of how to do this). This was not done because I wanted to get this ready for the meeting and I didn't have time. This PR makes some very deliberate design choices: - The 'Value' type family and any constraints thereon are _not_ lifted into the 'Era' class. Such would imply universality over eras, which is too strong a constraint. They would prevent us, for example, from adding to the `Val` class in future eras, which seems quite plausible. Furthermore, having more explicit constraints at the use site helps our understanding of the code; it is much more obvious _when_ we are relying on certain things, which can be a tool to spot bugs. Note that these constraints do not propogate wildly, because in general they are dispatched through the instantiation of the type family to a specific type in a given era. - It deliberately removes some instances (`Eq` for example) where it seems there is no strong reason to have it. The presence of an `Eq` instance everywhere has bitten us in the past, where for example we have ended up calling `(==)` on a large part of state in the consensus integration, which is an expensive operation. Honestly, I suspect I'll have to add these back to get the tests working, since they rely on them, but I think there's a decent case for making these instances orphans in the testing code instead. This is a *draft* PR for discussion. It does not yet touch the testing code, and is inconsistent about various things (in particular, I stuck `era ~ Shelley c` in a lot of places in a hurry).
redxaxder
pushed a commit
that referenced
this pull request
Sep 25, 2020
This PR demonstrates a way to parametrise the ledger over value. It paves the way for overriding this type in subsequent eras, without making any semantic changes to the Shelley ledger. Functions in the ledger are now classfied into three groups: - Those that remain universally quantified over eras. - Those that have specific requirements on certain era-parametrised types to work (e.g. that they can be serialised), and - Those that are specific to Shelley. There are two examples of the latter: `consumed` and `produced`. The STS rules are likewise split in two: - Those that remain universally quantified over eras. - Those that are specific to Shelley. The intention is that many will transition to the third (missing) category, where the actual rules specify their exact requirements on the era (see #1804 for an example of how to do this). This was not done because I wanted to get this ready for the meeting and I didn't have time. This PR makes some very deliberate design choices: - The 'Value' type family and any constraints thereon are _not_ lifted into the 'Era' class. Such would imply universality over eras, which is too strong a constraint. They would prevent us, for example, from adding to the `Val` class in future eras, which seems quite plausible. Furthermore, having more explicit constraints at the use site helps our understanding of the code; it is much more obvious _when_ we are relying on certain things, which can be a tool to spot bugs. Note that these constraints do not propogate wildly, because in general they are dispatched through the instantiation of the type family to a specific type in a given era. - It deliberately removes some instances (`Eq` for example) where it seems there is no strong reason to have it. The presence of an `Eq` instance everywhere has bitten us in the past, where for example we have ended up calling `(==)` on a large part of state in the consensus integration, which is an expensive operation. Honestly, I suspect I'll have to add these back to get the tests working, since they rely on them, but I think there's a decent case for making these instances orphans in the testing code instead. This is a *draft* PR for discussion. It does not yet touch the testing code, and is inconsistent about various things (in particular, I stuck `era ~ Shelley c` in a lot of places in a hurry).
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Add this suggestion to a batch that can be applied as a single commit.
This suggestion is invalid because no changes were made to the code.
Suggestions cannot be applied while the pull request is closed.
Suggestions cannot be applied while viewing a subset of changes.
Only one suggestion per line can be applied in a batch.
Add this suggestion to a batch that can be applied as a single commit.
Applying suggestions on deleted lines is not supported.
You must change the existing code in this line in order to create a valid suggestion.
Outdated suggestions cannot be applied.
This suggestion has been applied or marked resolved.
Suggestions cannot be applied from pending reviews.
Suggestions cannot be applied on multi-line comments.
Suggestions cannot be applied while the pull request is queued to merge.
Suggestion cannot be applied right now. Please check back later.
Draft PR for discussion.
This presents a straw man for a means to extend base Shelley system with additional modules providing other features. It introduces a basic account based blockchain model, and then a separate module which overrides this to support multi-currency.
This demonstrates the following features:
OPSandADMIN-ADMINfor example relies on the structure ofAccountingandAdminbut not their specific type:processOpsrelies on the structure ofOp, but is fully parametric over itsAccountingprovided that itstxandadminrules support it, since allprocessOpsdoes is pass this down to a lower layer.datatotypeforPredicateFailure.Downsides:
Thoughts:
Posting here for discussion; thoughts, ideas for how to make this better happily received, especially if they come with code!