Improve --verify-function and --verify-module

[utaal]

Some ideas from @achreto, @tjhance, @utaal:

• Support a wildcard for "a module and its submodules" for --verify-module, maybe --verify_module some_module::*.
• Support --verify module::function (instead of separate module/function flags).

[utaal]

@jonhnet: #596 (comment)

I've been using --verify-module to focus verus' attention on one file (module) at a time. That file contains state machines, which create submodules, and --verify-module ignores those submodules. So my verification has been surprisingly ignoring a big chunk of my file. That's certainly not what this user expected; I doubt it's what other users will expect.

[utaal]

@jaybosamiya: #596 (comment)

Fwiw, I've hit upon the same issue in the past, thus verus-mode.el has an explicit check for this situation where it will disable its "only run on the current module" behavior and starts running on the whole module.

I had tried implementing a "module and its submodules" wildcard but had hit some weird condition that caused me to abandon the approach I was taking; not sure what it was and I can't seem to find my notes on it; anyways relevant bit of Verus to update to support wildcard modules would be around here. I don't see anything that should prevent a "module and its submodules" implementation by just updating this to also handle a wildcard case, so am not sure why I had abandoned the approach I was taking back then. Could potentially have just been that I thought a nicer front-end interface might be possible or something, but yeah, I think this is feasible to implement with the wildcard thing, and I think (even if we don't yet have a better CLI option for it); at minimum we need something that tells us what is happening.

[jonhnet]

@jialin-li just wasted twenty minutes being fooled by this UI failure. She was using --verify-module X, where X contained a state_machine!, which implied a submodule X::Y. Verus was happily saying everything verifies, but nothing in Y was being checked.

I think --verify-module X should mean "verify X and all of its submodules." We could add --verify-module-exclusive for people who really only want X and none of its submodules. My argument for transitive closure being the default is this: --verify-module is used to improve response time by excluding most of a project. I have yet to encounter a case where including X's submodules adds enough time to verifying X that I'd be annoyed at having transitivity be the default. I'd be delighted to have to ask explicitly to exclude them.

[utaal]

@marshtompsxd asked (#1077):

Hi Verus team, I am trying to find an easy way to verify all the submodules recursively inside one module (like using a wildcard?). Concretely, I was looking for something like --verify-module foo::bar::*, and then Verus will verify module foo::bar and all the submodules inside foo::bar recursively. However, for now the only way to do it is to specify all the submodules one by one to Verus.