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

Constrained generators for EPOCH rule #4740

Merged
merged 1 commit into from
Dec 17, 2024
Merged

Constrained generators for EPOCH rule #4740

merged 1 commit into from
Dec 17, 2024

Conversation

MaximilianAlgehed
Copy link
Collaborator

@MaximilianAlgehed MaximilianAlgehed commented Nov 6, 2024 •
edited by Soupstraw
Loading

Description

closes #4669

Checklist

  • Commit sequence broadly makes sense and commits have useful messages
  • New tests are added if needed and existing tests are updated
  • All visible changes are prepended to the latest section of a CHANGELOG.md for the affected packages.
    New section is never added with the code changes. (See RELEASING.md)
  • When applicable, versions are updated in .cabal and CHANGELOG.md files according to the
    versioning process.
  • The version bounds in .cabal files for all affected packages are updated.
    If you change the bounds in a cabal file, that package itself must have a version increase. (See RELEASING.md)
  • Code is formatted with fourmolu (use scripts/fourmolize.sh)
  • Cabal files are formatted (use scripts/cabal-format.sh)
  • hie.yaml has been updated (use scripts/gen-hie.sh)
  • Self-reviewed the diff

@MaximilianAlgehed
Copy link
Collaborator Author

@Soupstraw here is a WIP approach to getting prop_EPOCH passing - when we have that property passing we should also have a generator for the conformance test.

@MaximilianAlgehed MaximilianAlgehed force-pushed the epoch branch 2 times, most recently from bc129f0 to f27fa1a Compare November 9, 2024 11:10
@MaximilianAlgehed MaximilianAlgehed marked this pull request as ready for review November 28, 2024 12:47
@MaximilianAlgehed MaximilianAlgehed requested a review from a team as a code owner November 28, 2024 12:47
@MaximilianAlgehed
Copy link
Collaborator Author

@Soupstraw I would appreciate some eyes on this. There are still things to do here but the generators used in prop_EPOCH should be usable in their current limited format with the conformance tests while I work to improve them.

@MaximilianAlgehed
Copy link
Collaborator Author

@Soupstraw I don't get how this can compile on my machine? There is a function called Agda.epochStep that I don't seem to be able to grep for in the code base at all.

@Soupstraw
Copy link
Contributor

epochStep comes from the MAlonzo generated code from the executable spec. There's an SRP block in the cabal.project file that imports that code from the spec repo.

@MaximilianAlgehed
Copy link
Collaborator Author

@Soupstraw how do we turn on the EPOCH conformance test here?

TimSheard
TimSheard reviewed Dec 5, 2024
View reviewed changes
Copy link
Contributor

@TimSheard TimSheard left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Things look reasonable to me.

libs/cardano-ledger-test/cardano-ledger-test.cabal Outdated Show resolved Hide resolved
libs/cardano-ledger-test/src/Test/Cardano/Ledger/Constrained/Conway/Epoch.hs Outdated Show resolved Hide resolved
libs/constrained-generators/src/Constrained/Base.hs
Comment on lines +1284 to +1287
r <- genFromSpecT spec
unsafePerformIO $
r `seq`
pure (pure r) `catch` \(e :: SomeException) -> pure (fatalError (pure $ show e))
Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Is it just calls to error that we are trying to catch, or something else?

Copy link
Collaborator Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Calls to error yes

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

This is a horrible piece of code that is totally incorrect:

  1. It will catch all exceptions, including async exceptions. It should have been catching the ErrorCall exception instead of SomeException, if it needs to catch error calls.

  2. Moreover this code will not even catch error calls because seq happens outside of catch:

ghci> let x = undefined in x `seq` pure x `catch` \e -> putStrLn ("WTH " <> show (e :: SomeException))
*** Exception: Prelude.undefined
CallStack (from HasCallStack):
  undefined, called at <interactive>:8:9 in interactive:Ghci2
ghci> let x = undefined in (x `seq` pure x) `catch` \e -> putStrLn ("WTH ==============\n" <> show (e :: SomeException))
WTH ==============
Prelude.undefined
CallStack (from HasCallStack):
  undefined, called at <interactive>:10:9 in interactive:Ghci3
  1. Moreover, using unsafePerformIO to catch an exception will lead to non-deterministic execution, which can break referential transparency. In other words it is never safe to catch exceptions in pure code with unsafePerformIO

libs/constrained-generators/src/Constrained/Base.hs Show resolved Hide resolved
@MaximilianAlgehed MaximilianAlgehed force-pushed the epoch branch 5 times, most recently from e578934 to 6767b04 Compare December 11, 2024 12:35
TimSheard
TimSheard approved these changes Dec 11, 2024
View reviewed changes
Copy link
Contributor

@TimSheard TimSheard left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ok just a few comments about adding comments to make things clearer.

libs/cardano-ledger-conformance/src/Test/Cardano/Ledger/Conformance/ExecSpecRule/Conway/Base.hs Outdated Show resolved Hide resolved
libs/cardano-ledger-test/src/Test/Cardano/Ledger/STS.hs Outdated Show resolved Hide resolved
@MaximilianAlgehed MaximilianAlgehed enabled auto-merge (squash) December 12, 2024 14:23
@MaximilianAlgehed @Soupstraw
attempt to get epoch rule constraints running - encountering really
51f9cef 
weird problems

Make things compile

minor

Don't need a concrete CertState in proposalsSpec

Start on EPOCH state generator spec

Add variant of stsProperty where the spec for the post state can depend
on the signal

Start constraining DRepPulsingState in EpochState generator

Use conformsToSpecProp to get more feed back when sts property fails

try to just get the property passing

Add missing instance

fmt

WIP insanity

WIP approach to shrinking

wip

Make compile again

More constraints

comment

Get the epoch rule closer to being right

fmt

Fix build error

wip

Correct lens version

Fix

Fix build issue
@MaximilianAlgehed MaximilianAlgehed merged commit 1900f29 into master Dec 17, 2024
157 checks passed
@MaximilianAlgehed MaximilianAlgehed deleted the epoch branch December 17, 2024 18:55
@lehins lehins mentioned this pull request Dec 17, 2024
Closed
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Reviewers

@Soupstraw Soupstraw Soupstraw left review comments

@lehins lehins lehins left review comments

@TimSheard TimSheard TimSheard approved these changes

Assignees
No one assigned
Labels
None yet
Projects
None yet
Milestone
No milestone
Development

Successfully merging this pull request may close these issues.

EPOCH generators
4 participants
@MaximilianAlgehed @Soupstraw @lehins @TimSheard