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

Sync executable with formal spec - PPUP STS #729

Closed
uroboros opened this issue Aug 8, 2019 · 0 comments · Fixed by #763
Closed

Sync executable with formal spec - PPUP STS #729

uroboros opened this issue Aug 8, 2019 · 0 comments · Fixed by #763
Assignees
@uroboros
Labels
⚙️ executable-model

Comments

@uroboros
Copy link
Contributor

uroboros commented Aug 8, 2019

Screenshot_FIG9

The exec. spec is missing 2 predicates in the formal spec for the PPUP STS:

pup /= Empty
ppv -> v elem pup ==> pvCanFollow (ppv pup_s) v
@uroboros uroboros mentioned this issue Aug 8, 2019
Closed
@uroboros uroboros self-assigned this Aug 13, 2019
JaredCorduan added a commit that referenced this issue Aug 14, 2019
@JaredCorduan
Issue #729 Sync executable with formal spec - PPUP
19af2e8
@JaredCorduan JaredCorduan mentioned this issue Aug 14, 2019
Merged
JaredCorduan added a commit that referenced this issue Aug 14, 2019
@JaredCorduan
Issue #729 Sync executable with formal spec - PPUP
4b18a75
kevinhammond pushed a commit that referenced this issue Oct 28, 2019
@JaredCorduan
Issue #729 Sync executable with formal spec - PPUP
c036069
nc6 pushed a commit that referenced this issue May 19, 2020
@iohk-bors @coot
Merge #729
e2240cc 
729: Estimations of encoded sizes of headers r=coot a=coot

The PR includes tests which serve two purposes:

* there are no thunks in size expressions
* generated data satisfy the size limits

Co-authored-by: Marcin Szamotulski <[email protected]>
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@uroboros uroboros

Labels
⚙️ executable-model
Projects
None yet
Milestone
No milestone
Development

Successfully merging a pull request may close this issue.

Sync executable with formal spec - PPUP IntersectMBO/cardano-ledger
1 participant
@uroboros