Users Should Have the Option to Opt-out of Inductive Function Contract Verification #2823
Assignees
Labels
[E] User Experience
An UX enhancement for an existing feature. Including deprecation of an existing one.
Milestone
Comments
JustusAdam
added
the
[E] User Experience
JustusAdam
changed the title
JustusAdam
added a commit
that referenced
this issue
Oct 17, 2023
…2809) This adds support for verifying the contracts of recursive functions inductively. The idea is quite simple. We use a global variable to track whether we're reentering a function and depending on that value we either continue with checking the contract or assume the hypothesis by using its replacement. The precise mechanism that I implemented is explained in the documentation [here](https://github.com/JustusAdam/kani/blob/a31176c79098205ca0b2c2b199cdf06653754551/library/kani_macros/src/sysroot/contracts.rs#L126) Resolves #2724 **Open Question:** to facilitate induction the return type of the function must implement `kani::Arbitrary`. Since we can't discriminate between recursive and non-recursive functions in the proc-macro this means that this applies to all functions with contracts, not just recursive ones. This may be an unacceptable restriction. We could consider making inductive verification explicit with an annotation like `#[kani::inductive]` or conversely make inductive the default and let users opt-out with `#[kani::no_inductive]`. This is now tracked in #2823 I had to remove the names of the functions in which the messages occur in the test cases, since they are now generated, hard to read names By submitting this pull request, I confirm that my contribution is made under the terms of the Apache 2.0 and MIT licenses. --------- Co-authored-by: Zyad Hassan <88045115+zhassan-aws@users.noreply.github.com>
|
Hey @feliperodri, I was wondering if this will affect #2997? |
Sign up for free
to join this conversation on GitHub.
Already have an account?
Sign in to comment
Inductive verification for function contracts as conceived by #2809 places a
kani::Arbitrarybound on all check functions which means that contracts for functions with return types that do not implementkani:Arbitrarycan no longer be#[kani::proof_for_contract(...)]checked.Previously a
kani::Arbitrarybound was only required if the contract was to be used as a verified stub#[kani::stub_verified(...)]. This would allow a user to check contracts for functions that return types for which nokani::Arbitraryimplementation exists, for instance if the returned type was third-party. Inductive verification uses of a verified stub on recursive re-entry, entailing thekani::Arbitraryconstraint on checks also and disallowing this use case.The additional constraint applies to both recursive and non-recursive functions, because the procedural macro responsible for generating the check and replace functions cannot know whether a function is recursive. Mutually recursive functions have the recursive call in a nested function call whereas a procedural macro can only inspect the contents of its own body and thus not discover nested recursive calls.
To allow this use case Kani should allow users to opt-out of inductive verification on a per-function basis. For instance via a
#[kani::no_induction]macro. This could potentially make verification of such functions more expensive if they use recursion, a risk the user would be explicitly opting-in to.Alternatively inductive verification could be opt-in or it could be heuristically enabled if a non-mutual recursive call is detected and users could also opt-in explicitly for mutually recursive functions.
The text was updated successfully, but these errors were encountered: