Can't write recursive spec functions on recursive enums containing Vecs

[pratapsingh1729]

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 enums like this:

pub enum Foo {
    Bar(Vec<Foo>),
}

pub enum SpecFoo {
    Bar(Seq<SpecFoo>),
}

I want to write an impl DeepView that maps Foos to SpecFoos. I ran into a number of issues with respect to adding decreases_by lemmas to trait impls, but ignoring those, I have the following (playground link):

impl Foo {
    #[via_fn]
    pub proof fn lemma_foo_decreases(&self) 
    {
        match self {
            Foo::Bar(v) => {
                assert forall |i| (0 < i < v.len() ==> decreases_to!(self => v[i])) by {};
            }
        }
    }
    
    pub open spec fn dview(&self) -> SpecFoo 
        decreases self via Foo::lemma_foo_decreases
    {
        match self {
            Foo::Bar(v) => {
                SpecFoo::Bar(Seq::new(v.len() as nat, |i| v[i].dview()))
            }
        }
    }
}

But this fails to prove termination on the recursive call to v[i].dview(), despite the assertion in lemma_foo_decreases passing.

As another data point, I think it has something to do with Vec, because when I instead have a Box<Foo> or Box<SpecFoo> in the enum, the equivalent code verifies just fine (playground link):

pub enum Foo {
    Blah,
    Bar(Box<Foo>),
}

pub enum SpecFoo {
    Blah,
    Bar(Box<SpecFoo>),
}


impl Foo {
    #[via_fn]
    pub proof fn lemma_foo_decreases(&self) 
    {
        match self {
            Foo::Blah => {}
            Foo::Bar(f) => {
                assert (decreases_to!(self => f)) by {};
            }
        }
    }
    
    pub open spec fn dview(&self) -> SpecFoo 
        decreases self via Foo::lemma_foo_decreases
    {
        match self {
            Foo::Blah => SpecFoo::Blah,
            Foo::Bar(f) => {
                SpecFoo::Bar(Box::new(f.dview()))
            }
        }
    }
}

[pratapsingh1729]

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

[parno]

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.

[pratapsingh1729]

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?