At-attributes - new language feature

[MikaelMayer]

Summary

We plan on adding two new attributes in the language to have type-safe user-defined attributes.

• A special (invisible) attribute {:attribute} in front of a datatype to mark it as a potential attribute for the rest of the code.
• A special (invisible) attribute {:@ X} which takes a constructor of a datatype marked as {:attribute}

To simplify the use of user-defined attributes and ensure they are typed appropriately, we introduce a special syntax @X or @X(...) in places where attributes are accepted and more, as a shortcut for {:@ X(....)}

This is related to #3149

Background and Motivation

Attributes in Dafny tweak verification strategy (e.g. split_here, isolate_assertions, only, autocontracts, disable_nonlinear_arithmetic, fuel...), or compilation strategy (e.g. extern, nativeType, compile, synthesize, ...). Recently, with the Yucca project and now the Daffodyl project, We have seen Dafny users starting using custom attributes for their own projects as well.

Unfortunately, attributes do not have a strong resolution phase. Thus, if an attribute is misspelled, Dafny won’t generate any issue. This can create confusion in some code until the typo is spotted. Moreover, contrary to built-in attributes, user-defined attributes arguments are not checked against certain types, so this makes user codebase with attributes prone to errors or maintenance issues.

However, we can’t just type-check all attributes, as we expect that users will have to define their own attributes for more reasons, e.g. tweaking more the compiler (e.g. in Rust, see below), or the verification strategy (possibly an ITP in the future)

Here are a few other motivations about why attributes matter in the future.

Motivation 1. Lots of attributes to expect for Dafny-to-Rust

For the new Dafny-to-Rust code generator, I expect that there will need to be a lot more attributes to let our customers compile to more performant code. For example, to fine-tune how memory locations will encode types, that introduces 3 if not 4 new attributes. There are reason to believe more attributes will be necessary in the future, e.g. to model lifetimes, or to have different encoding of a type parameter as a generic or as a type member for interoperability.

Motivation 2. User-defined attributes

Besides these built-in attributes, there will also be necessary to provide support for user-defined attributes on which Rust heavily relies on. For example, there are many JSON serialization library, all of which define attributes to put on structures.
#[derive(Serialize)] and #[derive(Deserialize)] . Yet, we don’t have a reliable mechanism to identify what could serve as a custom attribute or not in Dafny.

Motivation 3: More precise assertion scoping.

Assertions in expressions currently leak outside of their scope, similar to assertion in statement blocks. However, there are cases when we want to ensure they are local, accessible or not to inner blocks, or exported only for example. Fine-tuning this aspect of assertions could be done via attributes. However, this also means adding a lot of new attributes, and I've seen that attributes are a barrier to adopting such behaviors partly because of their syntax (see next paragraph)

Motivation 4: Escape the maze of curly braces.

Attributes trigger a maze of curly braces that I think are hard to read. However. It’s not only that. Braces are used for heterogeneous language constructs already. If you see a curly brace in Dafny, what can it contains? It depends both on the external context and on the internal value:

• If the context is a module: Curly braces contain declarations
• If the context is a class-like definition: Curly braces contain member definitions
• If the context is a code block: Curly braces contain statements (method block, loops, if-statements, proof blocks)
• If the context is a function block: Curly braces contain a single expression (function body)
• If the context is an expression: Curly braces contain multiple expressions separated by a comma (sets, multiset)
• If the context is an if or a match or a while loop: Curly braces contain cases
• If the context is a calc: Curly braces contain expressions ending with semicolon and separated by optional operators
• If the inside starts with a colon: It contains then a name, a potential space and comma-separated arguments (attribute)

Of all of these, the last usage of curly brace is the only one that is not determined by the context but what it starts with. This inconsistency, although minor, is just an hint than maybe we could think of a different way to represent attributes to not overload the already crowded space of curly brace semantics.

Moreover, defining attributes with arguments separated by commas while not being enclosed with parentheses is pretty non-standard. In LISP, or bash, parentheses are also outside of the expression but arguments are space-separated, not comma-separated. In languages where arguments are separated by comma, they are regrouped as a tuple using parentheses after the function name. So that’s for my argument that our attribute syntax is a bit peculiar and not familiar for new users.

Proposed Feature

With everything in place, users would be able to define and use typed attributes like this:

# Rust Library
@attribute
datatype derive<T extends Derivable> = derive(t: T)

trait Derivable {}
datatype Serialize extends Derivable = Serialize
datatype Deserialize extends Derivable = Deserialize

Now, in remaining Dafny code, users can use the constructor of this datatype as an attribute, like this:

@derive(Serialize)
datatype MyStruct = ...

Note that such typed attributes can be placed between the datatype keyword and name, as for regular attributes, but we will probably deprecate that in the future for readability.

This would be the same for other declarations, methods, assertions, etc.

Existing attributes will have a typed attribute version available if one is using the standard library, so that one would be able to write

@IsolateAssertions
@ExternModule("OtherModule", "ExternMethodName")
method complicatedMethod() {
  ...
  @only assert x == 2;
  @split_here assert y == 5;
}

@fuel(1, 2)
function restrictedFuel() { ... }

and even get suggestions if an attribute is mistyped.

Alternatives

Because the new type system is not yet compatible with the entire Dafny test suite, we will have only one kind of attribute. In the future, we might want to ensure attributes must extend some traits so that we can't use assertion attributes for methods.

[MikaelMayer]

After discussions with the team, here are a few more precisions on the implementation of this feature.

• We won't parse old attributes in the position where new @-attributes are expected
• We won't parse new @-attributes in the position where old attributes are expected unless it's the same position
• We will change the case for new attributes to PascalCase and keep most names, but rename a few which were misnamed:
• To disambiguate between @-calls like f@label(value) and potential @-attributes, we will require that there is no space between f and @ for it to be an at-call. If there is a space, it starts an attribute. The space between the @ and the label is still optional.
• To disambiguate @Attribute(a+b)[i].f := 2, where (a+b) is part of the assignment, similarly, we will require that there is no space between an attribute name and its opening parenthesis. so the above will mean an attribute with an argument, whereas @Attribute (a+b)[i].f := 2 will mean an attribute with zero argument.
• We will aim that every visible node in the AST can have its own new @-attribute, placed before the node. For expressions, the attribute will always attach to the outermost expression. To attach an attribute to an innermost expression like x in @attribute x / y), one will have to wrap it with parentheses (@Attribute x) / y`