No-cheating mode

[utaal]

Suggested by @parno.

As discussed in the Verus meeting on October 1st 2024 with @parno, @Chris-Hawblitzel, @jonhnet, @tjhance, @utaal, @jaybosamiya.

Chris suggests that a flag --no-cheating should be command line, not an attribute like #[deny(cheating)].
@utaal, @Chris-Hawblitzel, @jaybosamiya: for crafting a specific policy for #[verifier::external_body] we may want rust-alike forbid, deny, allow.

@jonhnet, @parno: consider adding a list of files that allow #[allow(cheating)]. Tool enforces that are transitively closed.

[achreto]

With regards to unsafe usages in Rust, there are some tools that provides a nice audit list.
For example: https://github.com/geiger-rs/cargo-geiger

When building a verified application, then I would like to know whether some of my dependencies are using assumes/external body. Having a tool like cargo-geiger for "cheats" that produces a report or so that shows 1) what is trusted and 2) the usages of assumes/external_body

[utaal]

@Chris-Hawblitzel: on a list of modules at the root of the crate, you can forbid(external_body) on each module, except those that are trusted.
@utaal: in fact that may be the way to provide the list of trusted modules: those that do not have forbid(external_body).
@jaybosamiya: let's not use filenames.

@Chris-Hawblitzel, @utaal: instead let's have a crate-root-level mechanism to mark allowed external_body:
#![forbid_all(external_body)] at the root of the crate;
#[unforbid(external_body)] on the mod name; lines in the crate root.

@Chris-Hawblitzel: Verus can enforce a policy that unforbid-en modules are constrained to e.g. which file name to use.

[parno]

To expand on (my interpretation of) Chris's suggestion: We can use familiar-looking Rust syntax (e.g., the various lint levels) to make the notation accessible, but Verus can impose additional policy on top of this when run with --no-cheating. The policy can, for example, enforce:

1. The crate root must start with #![deny(verus::assumptions)].
2. The #[allow(verus::assumptions)] annotation can only appear in the crate root, and only on the mod name lines.
3. An #[allow(verus::assumptions)] module must correspond to a file-level module (to satisfy Jon's easy-to-audit criteria)
4. Modules on the allow list must be transitively closed; they can't use any non-allow modules

[parno]

Note that we also discussed connecting --no-cheating to exec-mode termination checking.

There's also some older but possibly relevant discussion w.r.t. trusted/untrusted splits.