Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Check property: every valid protocol update allows to produce new blocks #287

Closed
dnadales opened this issue Mar 5, 2019 · 1 comment
Closed

Check property: every valid protocol update allows to produce new blocks #287

dnadales opened this issue Mar 5, 2019 · 1 comment
Labels
byron ⚙️ executable-model 📜 formal-spec wontfix This will not be worked on

Comments

@dnadales
Copy link
Member

dnadales commented Mar 5, 2019

We want to avoid a protocol update from stopping the production of new blocks, so we should check that every valid protocol update leaves the validation layer in a state where it is possible to produce new blocks, including all the data they carry such as delegation certificates, update proposals, votes, and transactions.
@dnadales dnadales mentioned this issue Mar 5, 2019
Closed
@dnadales
Copy link
Member Author

dnadales commented Aug 5, 2019

For Byron at least, we can't guarantee this (for instance, we don't have checks in place that assert that the minimum block size is high enough to allow the production of blocks). So a liveness property like the one required in this issue depends on having checks in place for the parameter values of an update proposal.

@dnadales dnadales added 📜 formal-spec wontfix This will not be worked on labels Aug 20, 2019
nc6 added a commit that referenced this issue May 19, 2020
@iohk-bors @dnadales @nc6
Merge #287 #290
730f529 
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>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
byron ⚙️ executable-model 📜 formal-spec wontfix This will not be worked on
Projects
None yet
Milestone
No milestone
Development

No branches or pull requests
1 participant
@dnadales