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.

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

Add many new features to the Constrained modues in cardano-ledger-test #3709

Merged
merged 1 commit into from
Sep 13, 2023

Conversation

TimSheard
Copy link
Contributor

@TimSheard TimSheard commented Sep 5, 2023

The goal of this PR was to add Traces of simple transactions, and shrinking to tests generated from constraints.
In order to do this we had to add many new features. Here is a summary

Added module Test.Cardano.Ledger.Constrained.Trace.TraceMonad. A monad for generating traces
Includes an example of making a simple Tx's with 1 input and output.
Added 'actions' that update the Env in the TraceM monad for inputs, outputs and fees.
Added Tests that such Tx's pass the applySTS and that the 'actions' compute the same state.
Added Tests that traces of length 100, are real traces and lead to valid states.
Added Stage.hs, to break up large constraint lists into reusable pieces
Added Two experiments to make Targets invertible.
Added Profile improvements, use HashSet(Name era) rather than Set(Name era)
Parameterized the Preds directory files by UnivSize, so on can control the size of the universes.
Added the Gadt Rule, and sts :: Proof era -> Rule tag -> ...
Replaced Target with RootTarget, added some examples in Vars.hs
Added all the Constrained sub directory tests to the Tests in cardano-ledger-test

Description

Checklist

  • Commit sequence broadly makes sense and commits have useful messages
  • New tests are added if needed and existing tests are updated
  • 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)
  • 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)
  • 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

@TimSheard TimSheard requested review from a team as code owners September 5, 2023 21:25
@MaximilianAlgehed
Copy link
Collaborator

MaximilianAlgehed commented Sep 6, 2023

@TimSheard it would be great if these two tests from Test.Cardano.Ledger.Constrained.Examples could be included in CI:

  testSpec "Constraint soundness" $ pure $ property prop_soundness
  testSpec "Shrinking soundness" $ pure $ withMaxSuccess 20 $ property prop_shrinking

They are now  -- Tim

@TimSheard TimSheard force-pushed the ts-constrained-trace branch 3 times, most recently from 74f0fe5 to d4b750e Compare September 6, 2023 21:45
@TimSheard TimSheard changed the title WIP Add many new features to the Constrained modues in cardano-ledger-test Add many new features to the Constrained modues in cardano-ledger-test Sep 7, 2023
Copy link
Contributor

@lehins lehins left a comment

Choose a reason for hiding this comment

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

Could use a little cleanup, otherwise looks good.

Includes an example of making a simple Tx's with 1 input and output.
Added 'actions' that update the Env in the TraceM monad for inputs, outputs and fees.
Added Tests that such Tx's pass the applySTS and that the 'actions' compute the same state.
Added Tests that traces of length 100, are real traces and lead to valid states.
Added Stage.hs, to break up large constraint lists into reusable pieces
Added RootTarget, extends Target to make some Targets invertable. RootTargets for NewEpochState and down.
Added Profile improvements, use HashSet(Name era) rather than Set(Name era)
Parameterized the Preds directory files by UnivSize, so on can control the size of the universes.
Added the Gadt Rule, and sts :: Proof era -> Rule tag -> ...
Added all the Constrained sub directory tests to the Tests in cardano-ledger-test
@TimSheard TimSheard merged commit 46be183 into master Sep 13, 2023
12 checks passed
@iohk-bors iohk-bors bot deleted the ts-constrained-trace branch September 13, 2023 12:14
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

3 participants