Merge specs from the cardano-chain repo #234
Merged
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
* Implementation of abstract ledger spec using Backpack. How does this work? We parametrise over a signature `UTxO`, which currenly encompasses the types `Hash`, `Coin` and `Addr`. We can specify explicitly our constraints on these types. We then define an abstract ledger in `Ledger.Abstract` which depends on these types, but knows nothing of their concrete representation. In `simple/UTxO` we instantiate these parameters as in Jared's original spec. There's a bit of a wart at the moment in that I don't think I can have the `HasHash` class being part of the signature. So this is defined in `Ledger.Abstract` and we then need to define the `simple/Ledger` module to contain these. * Define transitions for a simple ledger system. * Change copyright, maintainer etc.
The rules so far model: - utxo - witnesses - ledger I incorporated the feedback I received from @nc6, @JaredCorduan, Bruno, and @coot.
* rename Coin to Value * unicode union and domain exclusion * add ghci to the makefile (and remove old ghcid-test) * Change foldr->foldl' for non-lazy fold.
* Organise 'Ledger.Abstract' module. * Create simple and witnessed ledgers. The composition here is not especially nice - I suspect I am pushing at the boundaries of what backpack can nicely do. But at least for the moment I couldn't see a nicer way. Suggestions welcome! * Fix 'InsufficientWitnesses' predicate.
Add the preliminary version of the chain extension rules.
The rules here were taken directly from Duncan's delegation spec.
Improves delegation and adds more precise types
- Add delegation witnesses - Add a proposal for interaction between blockchain and ledger layer
this will allow us to reuse parts of this spec
* Connects the delegate function to other delegation constructs
* Adds aliases for partial and total function notation
* Rename figure labels consistently. [skip ci] * Fix condition on UTxO rule. [skip ci] * Restrict the delegation epochs to the next epoch. [skip ci] * Declare `dbody` and `dwit` as total functions. [skip ci] * Fix the reference to the union-override operator. [skip ci] * Define variable `cepoch` in the blockchain rules. [skip ci]
adding latex where command
* Adds a description of the delegation interface in English
…o dnadales/CDEC-625-add-voting-and-update-validation
* Start writing a document outlining the semantics we use. * Note about transition systems. * Add two things: - Explanation of composition of transition systems. - Properties of serialisation functions. * Update specs/semantics/latex/small-step-semantics.tex Co-Authored-By: nc6 <nick@topos.org.uk> * Update specs/semantics/latex/small-step-semantics.tex Co-Authored-By: nc6 <nick@topos.org.uk> * Update following comments. * Add motivation for distributivity over injective functions. * Section on notation. * Minor update.
…heck to the spec.[skip ci]
- Epoch length is now a protocol parameter. - Ledger maintains a map of epoch to epoch length both to slot/epoch calculations, and for the database layer.
…o mdimjasevic/288-data-queue
This commit introduces the `HasTypeReps` type class, which contains the `abstractSize` function.
287: Add a abstractSize function to compute the abstract size of values r=dnadales a=dnadales This PR defines a function: ```haskell abstractSize :: HasTypeReps a => AccountingMap -> a -> Size ``` where ```haskell type Size = Int type AccountingMap = Map TypeRep Size ``` By providing the size associated to different `TypeRep`s we can compute the total size of a value. The typeclass `HasTypeReps` ensures that we can extract the list of all `TypeReps` found inside a given value. Close #278. 290: Add: Explicit epoch/slot calculations. r=nc6 a=nc6 Built atop #283 - Epoch length is now a protocol parameter. - Ledger maintains a map of epoch to epoch length both to slot/epoch calculations, and for the database layer. Addresses #255 Co-authored-by: Damian Nadales <damian.nadales@iohk.io> Co-authored-by: Nicholas Clarke <nick@topos.org.uk>
…o mdimjasevic/288-data-queue
- Adds the CHAIN systems. - Adds a basic block type with delegation payload. - Adds generators for the chain types.
…rsement per-genesis key. - Adopt a new protocol version only if it has received enough endorsements at least `2k` slots ago.
This is not ready for merging, since it needs references added, but should serve to start guiding the implementation at the Haskell level.
Also address review comments.
nc6
approved these changes
Feb 12, 2019
nc6
pushed a commit
that referenced
this pull request
May 19, 2020
237: Add ledger utxo properties and incorporate feedback r=dnadales a=dnadales - Add two ledger UTxO properties: no double spending and utxo is outputs minus inputs. - Incorporate feedback received from @dcoutts and @jcmincke, and part of the feedback received during the Berlin workshop. - Add injectivity constraint to `txid`. - Replace `N` by `Z` as an alias for `Lovelace` and remove `Lovelace` cap and explicit fees. - Make protocol parameters consistent with Shelley spec. - Add author field, list of contributors, and git revision. Close #219, close #233, close #234, close #232, close #231. Co-authored-by: Damian Nadales <damian.nadales@iohk.io>
teodanciu
pushed a commit
to bienpulenta/cardano-ledger
that referenced
this pull request
Apr 19, 2023
…sh-algo-constraint remove HashAlgorithm constraint from Show Hash
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.
No description provided.