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

Disallow side effects in contract expressions #3213

Open
pi314mm opened this issue May 30, 2024 · 3 comments
Open

Disallow side effects in contract expressions #3213

pi314mm opened this issue May 30, 2024 · 3 comments
Assignees
Labels
[C] Feature / Enhancement A new feature request or enhancement to an existing feature. Z-Contracts Issue related to code contracts

Comments

@pi314mm
Copy link
Contributor

pi314mm commented May 30, 2024

Currently, function contracts allow for arbitrary expressions, including ones that allow for potential side effects.
This could result in a statement that modifies the input arguments to a function before running the function on those arguments, or modifying the result or input arguments after the computation has passed.

This is likely related to #2909. This showcases an infinite loop as a side effect resulting in a contract being vacuously true.

The problem with side effects within the function contracts is that it blurs the abstraction of the contract macros, as it requires the user to reason about the kani::assert statements that the contract macros compile to. The arguments are no longer being directly fed in and out of the function, but rather there are precomputations and postcomputations which could have side effects. To truly maintain the proper abstraction of these macros, the pre and post computations must be pure.

@pi314mm pi314mm added the [C] Feature / Enhancement A new feature request or enhancement to an existing feature. label May 30, 2024
@jsalzbergedu
Copy link
Contributor

jsalzbergedu commented May 30, 2024

I think only allowing const fn in the function contracts would be a good fit. const fn disallows arbitrary looping and disallows side effects that cannot be evaluated at compile time.

EDIT: const fn allows while true. We would need to do both this and some looping restriction.

@feliperodri feliperodri added this to the Function Contracts MVP milestone Jun 5, 2024
@feliperodri feliperodri self-assigned this Jun 6, 2024
@celinval
Copy link
Contributor

I think only allowing const fn in the function contracts would be a good fit. const fn disallows arbitrary looping and disallows side effects that cannot be evaluated at compile time.

EDIT: const fn allows while true. We would need to do both this and some looping restriction.

That's a great idea. I worry that this might be too restrictive though.

@celinval
Copy link
Contributor

I wonder if we can at least wrap everything into an Fn closure like the one being added in #3307. That will ensure that the contract expressions cannot mutably capture their environment.

@tautschnig tautschnig added the Z-Contracts Issue related to code contracts label Aug 1, 2024
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
[C] Feature / Enhancement A new feature request or enhancement to an existing feature. Z-Contracts Issue related to code contracts
Projects
None yet
Development

No branches or pull requests

5 participants