Verus panic when checking termination on a Seq of recursive enums

[pratapsingh1729]

Originally discovered in #1195.

As a minimal example, I want to write a recursive enum, like the following:

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

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

I then want to write a function (eventually an impl DeepView) to convert Foo to SpecFoo. I've tried various versions of this based on suggestions from @parno and @jaybosamiya, and the one that seems to work best uses two mutually recursive functions, as follows:

pub open spec fn blah(s: Seq<Foo>) -> Seq<SpecFoo> 
    decreases s.len()
{
    if s.len() == 0 {
        Seq::empty()
    } else {
        blah(s.drop_last()).push(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()))
        }
    }
}

Playground link here

However, this panics:

thread '<unnamed>' panicked at rust_verify/src/verifier.rs:780: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=3daf1740c8f7e4db77810e0c03b04b55#)
thread '<unnamed>' panicked at rust_verify/src/verifier.rs:2081:29:
worker thread panicked

Notably, if I make either of blah or recurse_foo a closed spec fn with no body, the panic goes away and it verifies. So I guess the error must be to do with the mutual recursion?

It turns out this is something of a blocker for our project, so it would be nice to know if this is just a bug that can be fixed, or if there's a fundamental issue with this kind of construction that would necessitate an alternative approach.

[Chris-Hawblitzel]

I can fix the mutual recursion issue so that the decreases check generates valid AIR for mixtures of datatypes and integers, like decreases_to! already does. Is there a repro example that I can use that would already work if we used assert(decreases_to!(...)); assume(false); as a stand-in for decreases checking? For example, something like the following, but that would pass the assertions?

pub open spec fn blah(s: Seq<Foo>) -> Seq<SpecFoo> 
    decreases s.len() via blah_check
{
    if s.len() == 0 {
        Seq::empty()
    } else {
        blah(s.drop_last()).push(recurse_foo(s.last()))
    }
}

pub open spec fn recurse_foo(f: Foo) -> SpecFoo 
    decreases 0int via recurse_foo_check
//    decreases f via recurse_foo_check
{
    match f {
        Foo::Bar(v) => {
            SpecFoo::Bar(blah(v.view()))
        }
    }
}

#[verifier::decreases_by]
proof fn blah_check(s: Seq<Foo>) {
    if s.len() != 0 {
        assert(decreases_to!(s.len() => s.last())); // FAILS
        assume(false);
    }
}

#[verifier::decreases_by]
proof fn recurse_foo_check(f: Foo) {
    match f {
        Foo::Bar(v) => {
            assert(decreases_to!(f => v.view().len())); // FAILS
            assume(false);
        }
    }
}

[pratapsingh1729]

Thanks very much for looking into this issue! Here is a version that verifies:

pub open spec fn blah(s: Seq<Foo>) -> Seq<SpecFoo> 
    decreases s.len() via blah_check
{
    if s.len() == 0 {
        Seq::empty()
    } else {
        blah(s.drop_last()).push(recurse_foo(s.last()))
    }
}

pub open spec fn recurse_foo(f: Foo) -> SpecFoo 
    decreases 0int via recurse_foo_check
//    decreases f via recurse_foo_check
{
    match f {
        Foo::Bar(v) => {
            SpecFoo::Bar(blah(v.view()))
        }
    }
}

#[verifier::decreases_by]
proof fn blah_check(s: Seq<Foo>) {
    if s.len() != 0 {
        assert(decreases_to!(s.len() => s.drop_last().len()));
        assume(false);
    }
}

#[verifier::decreases_by]
proof fn recurse_foo_check(f: Foo) {
    match f {
        Foo::Bar(v) => {
            assert(decreases_to!(f => v));
            assume(false);
        }
    }
}

I'm not sure if this is what you meant, but it seems to me that the decreases_to! assertions in these versions should be sufficient to prove termination in this case.