#[is-variant]

[utaal]

I've implemented an equivalent to Dafny’s adt.Variant? and (limited support) for variant accessors:

#[is-variant]
enum Result<T, E> {
  Ok(T),
  Err(E),
}

#[is-variant] is an attribute macro that makes some #[spec] methods available for Result:

• r.is_Ok() and r.is_Err(), similar to Dafny’s r.Ok? and r.Err?
• r.get_Ok_0() and r.get_Err_0() (in general r.get_VariantName_FieldIndex()) to access the field(s)
  Sample usage:

fn foo(r: Result<u64, String>) {
  requires(r.is_Ok() && r.get_Ok_0() >= 30)
  match {
    Result::Ok(v) => assert(v >= 20),
    Result::Err(_) => unreached::<()>(),
  }
}

There are some more examples of how to use these in the tests for the feature https://github.com/secure-foundations/verus/blob/d2e8869aa85bde74dfbce9c55cb86fec7b90f589/source/rust_verify/tests/adts.rs#L233-L349

This scheme, we believe, has the cleanest encoding. It can directly leverage the SMT field accessors and (is-Variant) primitive.

The naming scheme also remains consistent if and when, in the future, we add support for enum variants with named fields, e.g.

#[is-variant]
enum Result<T> {
  Ok(T),
  Err { message: String }
}

where r.get_Err_message() will encode the message field.

It is however a departure from Dafny's .field accessors (in the previous example, one could have done r.message if they had the fact that r.Err?). This seems necessary to avoid an artificial restriction on Rust's rules or typechecking issues, as Rust (contrary do Dafny) allows fields with the same name but different types:

#[is-variant]
enum E<T, U> {
  A { v: T },
  B { v: U, j: usize }, 
}

[tjhance]

thoughts on doing r.get_Ok() instead r.get_Ok_0() (in the specific case that there is only one argument)?

I do realize it's a little inconsistent, which is a minus.

[utaal]

Yea, I'm not opposed, but I think I'd be leaning on the side of consistency over saving the two characters. Also, I have a bit of a preference for keeping these code paths as simple as possible in the verifier, as they're easier to maintain (this is a secondary concern, though).

[Chris-Hawblitzel]

We could always add additional, shorter, accessor function names in the future (i.e. have both r.get_Ok() and r.get_Ok_0() or both r.get_Err_message() and r.get_message() or r.message().)

[jonhnet]

The _0 syntax is a bit hideous, but I understand that's a hackaround for the world in which we can't change Rust to have named fields. From the discussion, it looks like there's a path to a prettier future.

Probably what we should really be doing is playing with richer examples:

#[is-variant] enum Node<K, V> { Nil, Index(pivots: Vec<K>, childPointers: Vec<Index>, Leaf(data: Vec<Pair<K, V>>) }

I'm using the Hypothetical Future Syntax. With Present Syntax, we'd have n.get_Index_0()[3], which is pretty nasty; I'd vastly rather read n.get_Index_pivots()[3]. (And as Chris points out, n.get_pivots()[3] would be even better.)

I'd most prefer n.pivots[3] -- treat 'pivots' as a field, as Dafny does. Is there a reason that's not rustacious?

I'm honestly a little surprised that Rust doesn't have a way to name struct fields? That can't be right! Positionally-identified arguments are reasonable for short argument lists to procedures, but pretty gross for datatypes.

[tjhance]

I think enums allow each constructor to have either ordered, unnamed arguments, or unordered named arguments.

[jonhnet]

OH! So we can have name arguments. I'm happy then.

[utaal]

As @tjhance is saying, you can already write (in vanilla Rust):

enum Node<K, V> {
  Nil,
  Index { pivots: Vec<K>, child_pointers: Vec<Index> },
  Leaf(Vec<Pair<K, V>>), // intentionally changed to positional for the sake of the example
}

you can freely mix the positional and named fields (for different variants). So for this #[is-variant] would generate

n.get_Index_pivots()
n.get_Index_child_pointers()
n.get_Leaf_0()

The reason for having get_Index_pivots and not just get_pivots is because Rust allows the following:

enum WeirdNode {
  IndexVals { pivots: Vec<V> },
  IndexKeys { pivots: Vec<K> }, // pivots has different types in the two variants
}

which would make the type of an hypothetical get_pivots() dependent on the current value (which I expect is messier to typecheck, Dafny doesn't have this kind of dependent typing either).
(I still need to implement support for named arguments, but) for your example, you'd get: n.get_Index_pivots()[3]

I'd most prefer n.pivots[3] -- treat 'pivots' as a field, as Dafny does. Is there a reason that's not rustacious?

This would require a significant change to the typechecker, so it would be for later. But strictly speaking it's not rustacious for the reason discussed above (its type can be ambiguous unless we outlaw fields with the same name but different types, which may work for named fields, but wouldn't for positional field).

[utaal]

Note that one of our goals is to, one day, support vanilla rust with specification in attributes (a-la-Prusti) for those who don't need/want to switch to our syntax, so it may be worthwhile not to depart from Rust rules unless we really need to. (We can still add some sugar to smooth out the annoying cases, of course.)