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

Detect and report vacuous properties #627

Merged
merged 3 commits into from
Sep 11, 2019
Merged

Detect and report vacuous properties #627

merged 3 commits into from
Sep 11, 2019

Conversation

bts
Copy link
Contributor

@bts bts commented Aug 28, 2019

This is important for minimizing user confusion and surprise. Because
property assumes transaction success, when a function cannot
successfully run to completion, it is possible to "validate" any
property in this setting.

Consider some logical formula that corresponds to the Pact expression
(property some_property), where some_property can be anything:

tx_success => some_property

This is equivalent to:

¬tx_success Λ some_property

If tx_success is always false, then this expression is always true, no
matter the value of some_property.

We now detect such a condition where it is not possible for this
function to succeed (if called as a top-level function), and we produce
an error notifying the user that the property is moot:

Vacuous property encountered! There is no way for a transaction to succeed if it is calls this function from the top-level. Because all property expressions in Pact assume transaction success, in this case it would be possible to validate any property, even e.g. false.

Closes #623.

/cc @ggobugi27

This is important for minimizing user confusion and surprise. Because
`property` assumes transaction success, when a function cannot
successfully run to completion, it is possible to "validate" any
`property` in this setting.

Consider some logical formula that corresponds to the Pact expression
`(property some_property)`, where `some_property` can be anything:

    tx_success => some_property

This is equivalent to:

    ¬tx_success Λ some_property

If `tx_success` is always false, then this expression is *always* true, no
matter the value of `some_property`.

We now detect such a condition where it is not possible for this
function to succeed (if called as a top-level function), and we produce
an error notifying the user that the property is moot.
@bts bts added the FV Formal verification label Aug 28, 2019
@bts bts requested a review from emilypi August 28, 2019 21:00
src/Pact/Analyze/Check.hs Outdated Show resolved Hide resolved
@bts bts requested a review from emilypi September 9, 2019 19:12
@bts bts merged commit d8a4d0e into master Sep 11, 2019
@bts bts deleted the vacuous-property-check branch September 11, 2019 13:47
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
FV Formal verification
Projects
None yet
Development

Successfully merging this pull request may close these issues.

Issue warning if a property passes vacuously
2 participants