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

Symbolic testing #887

Draft
wants to merge 10 commits into
base: master
Choose a base branch
from
Draft

Symbolic testing #887

wants to merge 10 commits into from

Conversation

g-r-a-n-t
Copy link
Member

@g-r-a-n-t g-r-a-n-t commented May 24, 2023

This PR includes the following:

  • basic groundwork for invariant support
  • invariants that verify the std::lib

Invariants in Fe are similar to tests. The difference being that invaraints are executed symbolically instead of concretely.

example:

#invariant
fn de_morgan_true(a: bool, b: bool) {
    spec::given_true(a and b)
    spec::assert_true(not ((not a) or (not b)))
}

#invariant
fn de_morgan_false(a: bool, b: bool) {
    spec::given_false(a and b)
    spec::assert_false(not ((not a) or (not b)))
}

In the example given above, we provide the invariants with two arguments: a and b. These variables do not have concrete values, so we need to evaluate the invariant symbolically. This is done using kevm.

@g-r-a-n-t g-r-a-n-t marked this pull request as draft May 24, 2023 00:31
This was referenced May 24, 2023
@g-r-a-n-t g-r-a-n-t force-pushed the invariants branch 2 times, most recently from 43d9de4 to 9a2ad56 Compare May 30, 2023 17:24
@g-r-a-n-t g-r-a-n-t force-pushed the invariants branch 2 times, most recently from 9b727f4 to c179559 Compare June 16, 2023 22:54
Grant Wuerker added 2 commits June 16, 2023 17:01
@g-r-a-n-t g-r-a-n-t changed the title Invariants Symbolic testing Jul 20, 2023
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.

1 participant