call_requires/call_ensures don't have expected behavior for "normal" function calls

[tjhance]

This fails verification in the annotated locations:

// normal versions

fn caller1(u: u64) -> u64 { 3 }

fn test1(x: u64) {
    let y = caller1(x);
    assert(call_ensures(caller1, (x,), y)); // fails
}

fn caller2(u: u64) -> u64
    requires false
{
    3
}

fn test2(x: u64) {
    assume(call_requires(caller2, (x,)));
    caller2(x); // fails (precondition)
}


// trait versions

trait Tr : Sized {
    fn f(self) -> Self;
}

fn test_ensures<T: Tr>(a: T) {
    let b = a.f();
    assert(call_ensures(T::f, (a,), b)); // fails
}

trait Tr2 : Sized {
    fn g(self) -> Self
        requires false;
}

fn test_requires<T: Tr2>(a: T) {
    assume(call_requires(T::g, (a,)));
    let b = a.g(); // fails (precondition)
}

Note that it's possible to workaround this by assigning the functions to variables and then calling them. This works because it forces Verus to invoke the more flexible function trait based encoding machinery.

That is, everything below succeeds:

// normal versions

fn caller1(u: u64) -> u64 { 3 }

fn test1(x: u64) {
    let f = caller1;
    let y = f(x);
    assert(call_ensures(caller1, (x,), y));
}

fn caller2(u: u64) -> u64
    requires false
{
    3
}

fn test2(x: u64) {
    assume(call_requires(caller2, (x,)));
    let f = caller2;
    f(x);
}


// trait versions

trait Tr : Sized {
    fn f(self) -> Self;
}

fn test_ensures<T: Tr>(a: T) {
    let f = T::f;
    let b = f(a);
    assert(call_ensures(T::f, (a,), b));
}

trait Tr2 : Sized {
    fn g(self) -> Self
        requires false;
}

fn test_requires<T: Tr2>(a: T) {
    assume(call_requires(T::g, (a,)));
    let g = T::g;
    let b = g(a);
}