-
Notifications
You must be signed in to change notification settings - Fork 66
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
Invalid AIR generation when returning unit type #1108
Comments
<return value> == ()
panics the verifier
I'm adding other cases to this issue where using a unit return type can result in invalid AIR code. For example (from #1161 ):
|
Here's another one: trait Tr : Sized {
fn get() -> (r: Self)
ensures r == r;
}
impl Tr for () {
fn get() -> (r: Self)
{
}
} |
This still seems to be an issue at the latest version https://github.com/verus-lang/verus/tree/edeaa3660f1f6106aef5e469e01d2b5a4027352e
|
With PR #1280, all issues mentioned in this thread so far will be fixed, with the exception of:
This is a poly issue, so should be revisited after the upcoming poly refactor. |
The following code:
panics the verifier, as follows:
Minimal playground link with full backtrace
On the other hand, removing the
ensures res == ()
onowl_unit()
makes the panic go away (link).Thanks to parametricity, the
ensures res == ()
spec is not actually needed, but noting in case it points to a bigger bug.The text was updated successfully, but these errors were encountered: