ANNOTATIONS.md

RefinedC type system annotation syntax

The RefinedC type system interfaces to the C language using:

• C2X attributes of the form [[rc::<ident>(<string>, ... ,<string>)]],
• macros defined in refinedc.h that are provided as a shortcut for using certain specific attributes in the body of functions,
• special comments of the form //rc::<ident> <payload>?.

Contents

• RefinedC type system annotation syntax
• Contents
• Valid attributes
• Placement of attributes
• Description of the attributes
  • rc::annot_args (for advanced users)
  • rc::annot (for advanced users)
  • rc::args
  • rc::constraints
  • rc::ensures
  • rc::exists
  • rc::let
  • rc::field
  • rc::global
  • rc::immovable (does not work yet in ail_to_coq it seems)
  • rc::inv_vars
  • rc::lemmas
  • rc::manual_proof
  • rc::parameters
  • rc::ptr_type
  • rc::refined_by
  • rc::requires
  • rc::returns
  • rc::size
  • rc::skip
  • rc::tactics
  • rc::tagged_union
  • rc::trust_me
  • rc::union_tag
• Grammar for annotations
  • Basic tokens
  • Embedded Coq syntax
  • Type expressions
    • Type constuctor application
    • Refinements
    • Existential types
    • Constrained types
    • Other constructors
  • Constraints
• Special support
• Annotations using macros
• Annotations using comments
  • Importing dependencies
  • Context directive
  • Inlined Coq code
  • Type definition

Valid attributes

RefinedC attributes of the form [[rc::<ident>(<string>, ... ,<string>)]] can be placed on certain C constructs (e.g., on functions or on loops). Attributes of several kinds can be specified, they are distinguished using the identifier that they carry. Each specific kind of attribute is constrained as to where it may appear in the source code. For instance, postcondition attributes may only appear on a function definition or a function declaration. The following table gives information about every available kind of attributes, including how many arguments (i.e., strings) it may have, and what syntactic constructs it can be attached to.

Identifier	Arguments	Allowed on	Syntax for the arguments
annot_args	One or more	Functions	<integer> ":" <integer> <coq_expr>
annot	Exactly one	Expressions	Arbitrary Coq syntax
args	One or more	Functions	<type_expr>
constraints	One or more	Structures, Loops	<constr>
ensures	One or more	Functions	<constr>
exists	One or more	Functions, Loops	<ident> ":" <coq_expr>
let	One or more	Structures	<ident> {":" <coq_expr>} "=" <coq_expr>
field	Exactly one	Structure members	<type_expr>
global	Exactly one	Global variables	<type_expr>
immovable	None	Structures	N/A
inv_vars	One or more	Loops	<ident> ":" <type_expr>
lemmas	One or more	Functions	Argument for the Coq apply: tactic
manual_proof	Exactly one	Functions	<import_path> ":" <ident> "," <ident>
parameters	One or more	Functions, Structures	<ident> ":" <coq_expr>
ptr_type	Exactly one	Structures	<ident> ":" <type_expr>
refined_by	One or more	Structures	<ident> ":" <coq_expr>
requires	One or more	Functions	<constr>
returns	Exactly one	Functions	<type_expr>
size	Exactly one	Structures	<coq_expr>
skip	None	Functions	N/A
tactics	One or more	Functions	Arbitrary Ltac tactic
tagged_union	Exactly one	Structures	<coq_expr>
trust_me	None	Functions	N/A
union_tag	Exactly one	Union members	<ident> {"(" <ident> ":" <coq_expr> ")}*

Note that only the attributes requiring one or more arguments may be used more than once in the annotations for a particular C construct.

Remark: the ordering of attributes does not matter except between those of the same kind. Having several attributes of a repeatable kind is equivalent to having a single one carrying all the combined arguments (in attributes order). As an example, the annotations on the following functions are equivalent.

[[rc::parameters("i : Z")]]
[[rc::args("int<i32>", "i @ int<i32>")]] // Spec for the two arguments.
[[rc::returns("i @ int<32>")]]
int snd_0(int x, int y){
  return x;
}

[[rc::parameters("i : Z")]]
[[rc::args("int<i32>")]] // Spec for the first argument.
[[rc::args("i @ int<i32>")]] // Spec for the second argument.
[[rc::returns("i @ int<32>")]]
int snd_1(int x, int y){
  return x;
}

[[rc::args("int<i32>")]] // Spec for the first argument.
[[rc::parameters("i : Z")]]
[[rc::args("i @ int<i32>")]] // Spec for the second argument.
[[rc::returns("i @ int<32>")]]
int snd_2(int x, int y){
  return x;
}

Remark: attributes on functions may be placed either on its declaration or on its definition (or a combination of both).

Placement of attributes

As show in the above examples, annotations on functions are placed immediately before their definitions and/or declarations. And things go similarly for most of the annotations, including those on loops, structure or union members. Note that in all these cases, there should be no blank line interleaved between the annotations themselves, or between the annotations and the element of C syntax to which they will be attached.

In fact, there is only one kind of annotation for which the annotation must be given in a somewhat unexpected place: structures. On a structure attributes do not precede the declaration, they are placed right after the struct keyword. An example of this is given below.

struct
[[rc::refined_by("r : nat", "g : nat", "b : nat")]]
color {
  [[rc::field("r @ int<u8>")]]
  uint8_t r;

  [[rc::field("g @ int<u8>")]]
  uint8_t g;

  [[rc::field("b @ int<u8>")]]
  uint8_t b;
};

Description of the attributes

In the following we describe the syntax and semantics for the arguments of the supported attributes. The syntax will be described using a BNF-like format. We will rely on the grammar defined in the following section.

rc::annot_args (for advanced users)

This annotation appears on functions only and has at least one argument. Every argument is of the following form.