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.

Sign up for GitHub

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

Jump to bottom

Quantifiers for function contracts #2546

Open
JustusAdam opened this issue Jun 20, 2023 · 1 comment · May be fixed by #3737
Open

Quantifiers for function contracts #2546

JustusAdam opened this issue Jun 20, 2023 · 1 comment · May be fixed by #3737
Assignees
@feliperodri @JustusAdam
Labels
[C] Feature / Enhancement A new feature request or enhancement to an existing feature.
Milestone
Function Contracts

Comments

@JustusAdam
Copy link
Contributor

JustusAdam commented Jun 20, 2023 •
edited
Loading

A rudimentary implementation for forall and exists for kani function contracts. They are implemented as higher-order builtins, which compile to __CPROVER_forall and __CPROVER_exists respectively.
@JustusAdam JustusAdam converted this from a draft issue Jun 20, 2023
@JustusAdam JustusAdam self-assigned this Jun 20, 2023
@JustusAdam JustusAdam moved this to In Progress in Kani 2023-07-10 Jun 20, 2023
@JustusAdam JustusAdam mentioned this issue Jun 20, 2023
Closed
6 tasks
@JustusAdam JustusAdam changed the title Quantifiers Quantifiers for function contracts Jun 20, 2023
@JustusAdam JustusAdam mentioned this issue Jun 20, 2023
Open
@JustusAdam JustusAdam added this to the Function Contracts MVP milestone Jun 20, 2023
@celinval celinval removed the status in Kani 2023-07-10 Jul 10, 2023
@tautschnig tautschnig added the [C] Feature / Enhancement A new feature request or enhancement to an existing feature. label Sep 22, 2023
@JustusAdam JustusAdam mentioned this issue Sep 22, 2023
Closed
@feliperodri feliperodri self-assigned this Feb 8, 2024
@d0nutptr
Copy link

Hello! I was curious if there was a sense of when this functionality might be available?

I was trying to create a function contract to express the hashing property:

kani::ensures(result != hash(kani::any_where(|x| *x != input)))

but I believe I need quantifiers for this to actually work. Thank you!

@feliperodri feliperodri linked a pull request Nov 25, 2024 that will close this issue
Draft
5 tasks
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees

@feliperodri feliperodri

@JustusAdam JustusAdam

Labels
[C] Feature / Enhancement A new feature request or enhancement to an existing feature.
Projects
No open projects
Kani 2023-07-10
Status: No status
Milestone
Function Contracts
Development

Successfully merging a pull request may close this issue.

Add support for quantifiers feliperodri/kani
4 participants
@tautschnig @d0nutptr @feliperodri @JustusAdam