Update VIR representation of open/closed/opaque

[tjhance]

Making the 'open' qualifier more configurable in its visibility scope is a desirable feature (#1451).

This PR is a step towards implementing something like open(crate).

Presently, VIR represents visibility, open/closed, and opaque/opaque_outside_module via these fields:

pub struct FunctionX {
    /* ... */
    pub visibility: Visibility,
    pub publish: Option<bool>,
    pub fuel: u32,
    /* ... */
}

This PR replaces both 'publish' and 'fuel' fields with arbitrary visibility qualifiers:

#[derive(Debug, Serialize, Deserialize, Clone, ToDebugSNode)]
pub enum FuelOpaqueness {
    /// Opaque everywhere
    Opaque,
    /// Revealed insided the range given by 'visibility', opaque elsewhere.
    /// When revealed, it has the given fuel.
    /// (For non-recursive functions, fuel should be 1.)
    Revealed { visibility: Visibility, fuel: u32 },
}

pub struct FunctionX {
    /* ... */
    pub visibility: Visibility,
    pub body_visibility: Visibility,
    pub fuel_opaqueness: FuelOpaqueness,
    /* ... */
}

with the enforced property fuel_opaqueness.visibility ⊆ body_visibility ⊆ visibility.

Thus body_visibility is used to handle open/closed, while fuel_opaqueness can handle both opaque and opaque_outside_module.

This PR doesn't implement any new features, but it should make it easy to extend these features in the future to support arbitrary visibility qualifiers.

[utaal]

This looks like a nice overall improvement, also in clarity of what's visible where (in VIR). And I like the side-benefit that we no longer need open/closed qualifiers on uninterpreted functions.

[utaal]

Should this be a panic instead? (Given that this should be "true by construction")

[tjhance]

Well an error with a span is always better than a panic, but maybe it should say "Verus internal error" or something.

[utaal]

Agreed. Don't we have something like that? (maybe we should make a variant of one of the macros in https://github.com/verus-lang/verus/blob/main/source/rust_verify/src/util.rs for this purpose.)

[utaal]

This may be helpful: #1453
If it looks good, we can replace it after merging.

[tjhance]

And I like the side-benefit that we no longer need open/closed qualifiers on uninterpreted functions.

This has never been needed, but it has been allowed, which was possibly a mistake. My first draft of this PR added an error for this, but it caused a lot of failures, so I backed out that particular change. (I did, however, fix vstd and all the tests to remove open/closed from uninterpreted functions.)

[utaal]

Right, thanks for clarifying. Shall we add a deprecation warning?

[utaal]

We've discussed this at the verus meeting. There's a language design question to resolve here before we introduce the deprecation warning: #1457 but I don't think we should hold up merging this before that's resolved.

[tjhance]

BTW, I think I'm going to change the representation slightly ... I will probably remove the 'fuel' field from the FuelOpaqueness struct because right now, it's always set to 1. Maybe at some point there'll be a way to set it to non-1 values for recursive functions, but even if we did, it should probably be a separate field anyway.