Open pratapsingh1729 opened 1 week ago
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 Seq
) is insufficient to solve the problem.
@jaybosamiya suggested that the issue might be to do with closures. So we tried a version with explicit recursion, eliminating the closures (playground link):
pub enum Foo {
Bar(Vec<Foo>),
}
pub enum SpecFoo {
Bar(Seq<SpecFoo>),
}
pub open spec fn blah(s: Seq<Foo>) -> Seq<SpecFoo>
decreases s
{
if s.len() == 0 {
Seq::empty()
} else {
blah(s.drop_last()) + seq![recurse_foo(s.last())]
}
}
pub open spec fn recurse_foo(f: Foo) -> SpecFoo
decreases f
{
match f {
Foo::Bar(v) => {
SpecFoo::Bar(blah(v.view()))
}
}
}
This still fails with the following error:
error: could not prove termination
--> /playground/src/main.rs:20:9
|
20 | blah(s.drop_last()) + seq![recurse_foo(s.last())]
| ^^^^^^^^^^^^^^^^^^^
error: could not prove termination
--> /playground/src/main.rs:29:26
|
29 | SpecFoo::Bar(blah(v.view()))
| ^^^^^^^^^^^^^^
error: aborting due to 2 previous errors
FWIW, you can eliminate the first error by changing the decreases s
to decreases s.len()
. To observe that, you need to comment out the seq![recurse_foo(s.last())]
, since if you leave it in, it appears to cause a panic.
Oh, interesting, thanks for this! If I comment out seq![recurse_foo(s.last())]
, I get no verification failures and the proof goes through. When I add it back, or when I change it to use Seq::push
instead of +
and the seq!
macro, it does indeed panic, as follows (playground link):
thread '<unnamed>' panicked at rust_verify/src/verifier.rs:747:21:
internal error: generated ill-typed AIR code: error 'in call to check_decrease_int, argument #2 has type "Poly" when it should have type "Int"' in expression '(check_decrease_int (let
((s!$0 tmp%2))
(vstd!seq.Seq.len.? $ TYPE%main!Foo. s!$0)
) decrease%init0 false
)'
note: [run with `RUST_BACKTRACE=1` environment variable to display a backtrace](https://play.verus-lang.org/?version=stable&mode=basic&edition=2021&gist=6eeaff127a708d7d49efa8b2dc4cbf2a#)
thread '<unnamed>' panicked at rust_verify/src/verifier.rs:1976:29:
worker thread panicked
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):