warn when using higher mode types in parameters (and return) with lower modes, #170

[utaal]

• temporarily based on the branch for preserve the type decoration in the type for Tracked<&mut T> params #746, which is a dependency

[Chris-Hawblitzel]

There's nothing inherently wrong with writing an exec function that takes an exec int parameter, but it's not really useful either, since you can't call it, since there are no exec int values. So I guess it's helpful to print out an error message to stop people from accidentally writing something useless and confusing. It probably improves diagnostics. But I'm wondering how far we intend to go with this feature. You can still write the following:

struct S<A>(A);

fn f(s: S<int>) {
    let x: int = s.0;
}

This is morally equivalent to fn f(x: int). Do we intend to disallow all possible exec usages of int and nat? Is it worth the effort? Or is this more like a linter that prints warnings in common cases?

[utaal]

I agree that this isn't a soundness issue.

In terms of treating this as an error (vs a lint), my main concern was erasure: making sure that we wouldn't allow exec-mode parameters with types that don't have a runtime representation, but I suppose doing codegen for them may not be a big deal, as they can never be called by verified code. When we allow unverified clients, though, it may be best if these functions aren't allowed (although an unverified client would also find it non-trivial -- although not impossible -- to call these functions).

[utaal]

Do we intend to disallow all possible exec usages of int and nat?

One thing that I forgot to point out is that the intent here is to disallow it only in parameters. Incorrect usage in e.g. variables would still be allowed.

---

The new commit should cover the case I missed and that you pointed out (thanks!), but there may be more that I missed. Do you think we should turn this into a warning? If we think this is fairly complete at this point, I'd argue we may want to have it be an error as (a) I don't see a use case where something that fails this check was intentional and (b) to protect against misuse by unverified clients in the future.

[tjhance]

What happens if the user writes Foo<int> where Foo is an exec type that uses its type parameter ghostily?

[utaal]

What happens if the user writes Foo<int> where Foo is an exec type that uses its type parameter ghostily?

Right. I see the problem now (brain is still a bit on vacation, I suspect). Thanks! I'll have another more careful look at this later.

[utaal]

Triaged in the Verus meeting; we want to lower to warning, and make the min_typ_mode function partial to be correct.