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

Fix unexpected free variable in FV #1251

Merged
merged 5 commits into from
Jul 26, 2023
Merged

Conversation

rsoeldner
Copy link
Member

@rsoeldner rsoeldner commented Jul 14, 2023

Addresses #1250

This PR makes use of a stack of free variables to allow for nested application of higher-order functions such as fold or map.

PR checklist:

  • Test coverage for the proposed changes
  • PR description contains example output from repl interaction or a snippet from unit test output
  • Documentation has been updated if new natives or FV properties have been added. To generate new documentation, issue cabal run tests. If they pass locally, docs are generated.
  • Any changes that could be relevant to users have been recorded in the changelog
  • In case of changes to the Pact trace output (pact -t), make sure pact-lsp is in sync.

Additionally, please justify why you should or should not do the following:

  • Confirm replay/back compat
  • Benchmark regressions
  • (For Kadena engineers) Run integration-tests against a Chainweb built with this version of Pact

@rsoeldner rsoeldner added bug FV Formal verification labels Jul 14, 2023
@rsoeldner rsoeldner changed the title WIP: Fix unexpected free variable in bug WIP: Fix unexpected free variable in FV Jul 14, 2023
@@ -1938,6 +1922,7 @@ runTranslation modName funName info caps pactArgs body checkType = do
CheckDefconst
-> error "invariant violation: this cannot be a constant"
_ <- extendPath -- form final edge for any remaining events
expectNoFreeVars
Copy link
Member Author

Choose a reason for hiding this comment

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

final check that no free vars are dangling

@rsoeldner rsoeldner marked this pull request as ready for review July 23, 2023 13:29
@rsoeldner rsoeldner changed the title WIP: Fix unexpected free variable in FV Fix unexpected free variable in FV Jul 24, 2023
@jwiegley
Copy link
Contributor

@rsoeldner Where is the test to show what behavior this is actually impacting?

@rsoeldner
Copy link
Member Author

@jwiegley ... missed pushing them

(fold (child) true [[1]]))
|]

expectVerified [text|
Copy link
Contributor

Choose a reason for hiding this comment

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

Does this test need any properties? Or an assertion that (= (parent) [[false]]) or similar?

Copy link
Member Author

Choose a reason for hiding this comment

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

No, it would fail even without a property annotation

Copy link
Contributor

@imalsogreg imalsogreg left a comment

Choose a reason for hiding this comment

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

Looks great.

@rsoeldner rsoeldner merged commit 7f79433 into master Jul 26, 2023
5 checks passed
@rsoeldner rsoeldner deleted the rsoeldner/fv-higherorder branch July 26, 2023 19:11
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
bug FV Formal verification
Projects
None yet
Development

Successfully merging this pull request may close these issues.

3 participants