-
Notifications
You must be signed in to change notification settings - Fork 60
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
Can't write recursive spec functions on recursive enums containing Vec
s
#1195
Comments
Based on discussion with @Chris-Hawblitzel, I started working on a PR to add an axiom that solves this (here). However, this axiom (which is based on the analogous one for @jaybosamiya suggested that the issue might be to do with closures. So we tried a version with explicit recursion, eliminating the closures (playground link):
This still fails with the following error:
|
FWIW, you can eliminate the first error by changing the |
Oh, interesting, thanks for this! If I comment out
Should I file another issue for this panic? |
We've discussed this a bit on Zulip, but wanted to post an issue since it didn't seem like there was a straightforward resolution with Verus as it is right now.
Suppose I have
enum
s like this:I want to write an
impl DeepView
that mapsFoo
s toSpecFoo
s. I ran into a number of issues with respect to addingdecreases_by
lemmas to trait impls, but ignoring those, I have the following (playground link):But this fails to prove termination on the recursive call to
v[i].dview()
, despite the assertion inlemma_foo_decreases
passing.As another data point, I think it has something to do with Vec, because when I instead have a
Box<Foo>
orBox<SpecFoo>
in theenum
, the equivalent code verifies just fine (playground link):The text was updated successfully, but these errors were encountered: