Const members of an enum

[pratapsingh1729]

I have the following code (playground link):

pub enum Mode {
    A,
    B,
    C
}

pub const MY_MODE: Mode = Mode::A;

This gives me the following error message:

error: expression has mode spec, expected mode exec
  --> /playground/src/main.rs:11:27
   |
11 | pub const MY_MODE: Mode = Mode::A;
   |                           ^^^^^^^

I am confused by this error message. Why is Mode::A inferred to have mode spec here? My understanding was that after #843, constant declarations should be dual-mode exec and spec.

(Not sure if this is an actual bug in Verus or there's just some syntax I am missing!)

[utaal]

Try pub exec const instead.

This may be a syntax inconsistency we may want to fix (in functions, exec is the default).

[pratapsingh1729]

Thank you! Yes, it works with a pub exec const. Ideally, however, I'd prefer to have the dual-mode functionality, since I use this constant in both spec contexts and in exec contexts. This works using just pub const when the const is a usize (link), but not when it is an enum member (link). Since I'm generating the code it's easier not to have to differentiate between whether the constant is being emitted for spec or exec contexts, if it's possible to do so in Verus.

[tjhance]

related (but slightly different) (but probably same root cause): https://github.com/verus-lang/verus/issues/861

[utaal]

Ah I see. Right, makes sense. This is indeed probably a bug (or a missing part of a feature). The bug @tjhance refers to is indeed likely another symptom of the same cause (thanks for looking it up!).

[pratapsingh1729]

A workaround for having the same const in spec and exec but not being able to declare it using the syntax above is to use when_used_as_spec, as follows:

pub spec const SPEC_FOO: Mode = Mode::A;

#[verifier::when_used_as_spec(SPEC_FOO)]
pub exec const FOO: Mode ensures FOO == SPEC_FOO { Mode::A }

...

Full playground link

Not sure if this is intended functionality, but it seems to work for me, in case it turns out that having the dual-mode functionality is unsound in some way.