Formal Grammar (EBNF)¶
The MVL grammar is LL(1) — every construct can be parsed with a single token of lookahead. This is a deliberate design choice (ADR-0005): the parser is hand-written recursive descent, no parser generator, no PEG, no macros. The whole grammar fits in ≈100 productions, small enough for a developer to hold in working memory.
The grammar below is the authoritative specification. The Rust parser, the tree-sitter grammar, and any future MVL-in-MVL parser must all match it. make test-grammar-coverage verifies coverage against the corpus.
Notation: ISO 14977 Extended BNF.
rule = body ;— production[ x ]— optional{ x }— zero or more( a | b )— alternation"lit"— terminal stringUPPER— terminal token (see the Lexical section at the end)(* comment *)— EBNF comment
Source of truth: grammar/grammar.ebnf in the mvl-spec repo.
(* === Top-level === *)
(* "pub" is factored out so each decl_body alternative starts with a *)
(* distinct keyword — this preserves the LL(1) property (ADR-0005). *)
(* Semantic constraint: "pub" is required before reexport_decl. *)
program = { use_decl } { declaration } ;
declaration = [ "pub" ] decl_body ;
decl_body = type_decl | fn_decl | const_decl | reexport_decl
| extern_decl | impl_decl | actor_decl | effect_decl
| label_decl | relabel_decl ;
(* === Modules and imports === *)
(* One file = one module. Module name = filename without extension. *)
(* Directories are module groups; foo.mvl is the entry (Rust 2018 style). *)
(* foo/mod.mvl is deprecated — accepted with a warning, prefer foo.mvl. *)
use_decl = "use" module_path [ ";" ] ;
reexport_decl = "use" module_path [ ";" ] ; (* "pub" required — enforced by type checker *)
module_path = IDENT { ( "." | "::" ) IDENT } [ "." "{" IDENT { "," IDENT } "}" ] ;
(* === Type declarations === *)
type_decl = "type" IDENT [ type_params ] "=" type_body ;
type_params = "[" type_param { "," type_param } "]" ;
(* Const generics (#928) — value-level parameters, e.g. `[T, const N: Int]`. *)
(* The const-param type must be a simple type identifier (no nested generics). *)
type_param = IDENT | "const" IDENT ":" IDENT ;
type_body = struct_body | enum_body | alias_type ;
struct_body = "struct" "{" { field_decl } "}" [ "with" "invariant" refinement ] ;
(* "with invariant" adds a cross-field predicate checked at construction and mutation — Phase 6, #654 *)
enum_body = "enum" "{" variant { "," variant } "}" ;
variant = IDENT [ "(" type_list ")" | "{" field_list "}" ] ;
field_decl = IDENT ":" type_expr [ "where" refinement ] ;
field_list = field_decl { "," field_decl } ;
alias_type = type_expr ;
(* === Function declarations === *)
(* `test` (#587) marks a unit-test entry point: `test fn name() -> Unit { … }`. *)
(* Orthogonal to totality; mutually exclusive with `builtin`; `pub` forbidden. *)
(* `fn_name` allows a receiver-type prefix (#928) for extension methods: *)
(* `fn List[T]::flatten(self)`, `fn Option[T]::is_some(self)`. *)
(* ADR-0053: the trailing `where` clause on fn signatures is REJECTED. *)
(* `where` in MVL is exclusively a solver-discharged refinement predicate *)
(* attached to a param/return/field/alias type (`n: Int where self > 0`), *)
(* never a trait-bound clause on a fn signature. MVL has no trait system. *)
fn_decl = [ "test" ] [ totality ] [ "builtin" ] "fn" fn_name [ type_params ]
"(" [ param_list ] ")" "->" return_type
[ "!" effect_list ]
{ fn_contract }
( block | (* empty — builtin only *) ) ;
fn_name = [ IDENT [ "[" type_list "]" ] "::" ] IDENT ;
fn_contract = ( "requires" | "ensures" ) refinement (* Phase 1, #621 *)
| "ghost" "let" IDENT "=" ref_expr ";" ; (* Phase 4, #627 — erased before codegen *)
(* tree-sitter splits fn_contract into two named rules: *)
contract_clause = ( "requires" | "ensures" ) ref_expr ; (* Phase 5, #628 — tree-sitter form of requires/ensures *)
ghost_let_stmt = "ghost" "let" pattern ":" type_expr "=" ref_expr ";" ; (* Phase 4, #627 — tree-sitter form *)
totality = "total" | "partial" ;
(* builtin fn: runtime-provided implementation; body is forbidden *)
(* Security is expressed via wrapper types on parameters/return (`Tainted[T]`, *)
(* `Secret[T]`) — see `labeled_type` below. There is no fn-level security *)
(* prefix; lowercase `public`/`tainted`/`secret` are NOT reserved words. *)
param_list = param { "," param } ;
param = [ capability ] IDENT ":" type_expr [ "where" refinement ] ;
capability = "iso" | "val" | "ref" | "tag" ;
return_type = type_expr [ "where" refinement ] ;
effect_list = effect { "+" effect } ;
effect = IDENT [ "(" STRING ")" ] ;
(* Parametrized effects restrict an effect to a specific resource. Examples:
! FileRead("/etc/app/") — read access limited to /etc/app/ and below
! Net("api.example.com") — network access limited to a specific host
! DB("SELECT") — read-only database access
A caller declaring ! FileRead("/etc/") satisfies a callee requiring
! FileRead("/etc/app/config.toml") via prefix matching (subsetting). *)
(* ADR-0053: `constraints` / `constraint` / `trait_bound` productions removed. *)
(* Reserved slot; parser emits a hard error diagnostic if encountered so *)
(* MVL never grows a Rust-style trait system by accident. *)
(* === Actor declarations (Phase 8, #63) === *)
(* `pub fn` = async behavior (message handler); parameters must be sendable. *)
(* `fn` = private synchronous helper; no sendability restriction. *)
(* Return type defaults to Unit when `->` is omitted on pub fn behaviors. *)
actor_decl = "actor" IDENT [ type_params ] "{" { actor_field } { actor_method } "}" ;
actor_field = field_decl [ "," ] ;
actor_method = [ "pub" ] "fn" IDENT "(" [ param_list ] ")" [ "->" return_type ]
[ "!" effect_list ] block ;
(* === Effect declarations === *)
(* `effect IO` — base effect; `effect FileIO > IO` — subsumes IO (#852). *)
(* No trailing semicolon — declarations are terminated by the next top-level keyword. *)
effect_decl = "effect" IDENT [ ">" IDENT { "+" IDENT } ] ;
(* === IFC label declarations (#894, #896) === *)
(* `label Tainted` — declares a user-defined security label for the module. *)
(* `relabel trust: Tainted -> _` — declares a label transition. *)
(* `relabel trust: Tainted -> _ audit` — all call sites emit audit events. *)
(* No trailing semicolon on either form. *)
label_decl = "label" IDENT ;
label_ref = IDENT | "_" ;
relabel_decl = [ "pub" ] "relabel" IDENT ":" label_ref "->" label_ref [ "audit" ] ;
(* `relabel trust(expr, "TAG")` — applies a transition (expression form). *)
(* `relabel trust(expr, "TAG") audit` — this call site emits an audit event. *)
relabel_expr = "relabel" IDENT "(" expr "," STRING ")" [ "audit" ] ;
(* === Extern blocks === *)
(* Declares foreign functions. "c" ABI: thin C-linkage declarations (linker provides body). *)
(* "rust" ABI: the compiler emits an IR bridge body (e.g. rand-based roll_dice). *)
extern_decl = "extern" STRING "{" { extern_fn_decl } "}" ;
extern_fn_decl = "fn" IDENT "(" [ param_list ] ")" "->" return_type
[ "!" effect_list ] ";" ;
(* === Impl blocks === *)
(* Provides method implementations for a trait on a named type. *)
impl_decl = "impl" IDENT [ "[" type_list "]" ] "for" IDENT "{" { fn_decl } "}" ;
(* === Type expressions === *)
(* MVL has no anonymous tuple types — use named structs instead (ADR-0002, #1380). *)
type_expr = base_type | option_type | result_type | ref_type
| labeled_type | refined_type | fn_type | session_type ;
base_type = IDENT [ "[" type_list "]" ] ;
option_type = "Option" "[" type_expr "]" ;
result_type = "Result" "[" type_expr "," type_expr "]" ;
ref_type = ( "val" | "ref" ) type_expr ;
(* Labeled type: syntactically identical to `base_type` (an IDENT with a *)
(* single type argument). The distinction is *semantic*: the leading IDENT *)
(* must be a declared IFC label — either a stdlib-preseeded label (`Tainted`, *)
(* `Secret`, `ConfigPath`, `DbUrl`, `ApiEndpoint`, `AuditTarget`) or one *)
(* declared via `label_decl` in the current module. There is no fixed set of *)
(* label names; `Public` is NOT a keyword or a stdlib label — it is spelled by *)
(* its *absence* (an unlabeled type is public by default). *)
labeled_type = IDENT "[" type_expr "]" ; (* IDENT ∈ declared-label set *)
refined_type = type_expr "where" refinement ;
fn_type = "fn" "(" type_list ")" "->" type_expr [ "!" effect_list ] ;
type_list = type_expr { "," type_expr } ;
(* === Session types (Honda 1993, spec 016) === *)
(* Type-level protocols. `!T. S` send, `?T. S` receive, `+{ l: S, … }` internal *)
(* choice (this side selects), `&{ l: S, … }` external choice (other side selects), *)
(* `end` protocol termination. The grammar is right-recursive to encode *)
(* left-to-right sequencing. `&T` (Rust-style borrow) is rejected with a hint *)
(* — see `ref T` / `val T` for borrows; the `&{` two-token lookahead disambiguates. *)
session_type = session_op ;
session_op = "!" type_expr "." session_op
| "?" type_expr "." session_op
| "+" "{" session_branches "}"
| "&" "{" session_branches "}"
| "end" ;
session_branches = IDENT ":" session_op { "," IDENT ":" session_op } ;
(* === Refinement predicates === *)
refinement = ref_expr ;
ref_expr = ref_term { ( "&&" | "||" ) ref_term } ;
ref_term = ref_atom [ ( "==" | "!=" | "<" | ">" | "<=" | ">=" ) ref_atom ] ;
ref_atom = IDENT { "." IDENT } (* field access for struct invariants, Phase 6, #654 *)
| INTEGER | FLOAT
| "len" "(" IDENT ")"
| "old" "(" ref_expr ")" (* Phase 4, #627 — entry-time value in ensures *)
| forall_expr (* Phase 5, #628 — universal quantifier *)
| exists_expr (* Phase 5, #628 — existential quantifier *)
| "(" ref_expr ")" | "!" ref_atom
| ref_atom ( "+" | "-" | "*" | "/" | "%" ) ref_atom ;
forall_expr = "forall" IDENT ":" type_expr "," ref_expr ; (* Phase 5, #628 *)
exists_expr = "exists" IDENT ":" type_expr "," ref_expr ; (* Phase 5, #628 *)
(* === Statements === *)
block = "{" { statement } "}" ;
statement = let_stmt | assign_stmt | return_stmt | if_stmt
| match_stmt | for_stmt | while_stmt | expr_stmt ;
let_stmt = "let" pattern ":" type_expr "=" expr ";" ;
assign_stmt = lvalue "=" expr ";" ;
return_stmt = "return" [ expr ] ";" ;
if_stmt = "if" expr block [ "else" ( if_stmt | block ) ]
| "if" "let" pattern "=" expr block [ "else" block ] ; (* desugars to match; see #704, #891 *)
match_stmt = "match" expr "{" { match_arm } "}" ;
match_arm = pattern [ "if" guard_expr ] "=>" ( expr | block ) [ "," ] ;
(* comma is a separator between arms; trailing comma is optional *)
guard_expr = ref_expr ; (* guard pattern — uses refinement expression language; see #938 *)
for_stmt = "for" pattern "in" expr block ;
while_stmt = "while" expr
{ "invariant" refinement } (* Phase 3, #621 — checked at entry and after each iteration *)
[ decreases_expr ] (* Phase 5, #628 — termination measure; required in total fns *)
block ;
decreases_expr = "decreases" ref_expr ; (* Phase 5, #628 — named form used in tree-sitter *)
expr_stmt = expr ";" ;
(* === Expressions === *)
(* `declassify(e)` and `sanitize(e)` were removed under #894 — use *)
(* `relabel name(e, "TAG")` (see `relabel_expr` above) with a declared *)
(* transition instead. *)
expr = literal | IDENT | field_access | fn_call | method_call
| unary_expr | binary_expr | borrow_expr | if_expr | match_expr
| lambda | block_expr | propagate | construct
| "consume" expr | as_expr
| actor_create_expr | select_expr | relabel_expr ;
as_expr = expr "as" type_expr ; (* checked coercion — runtime refinement check if unproven *)
(* Phase 8, #63: actor creation — `actor TypeName { field: expr, … }` — returns ActorRef *)
actor_create_expr = "actor" IDENT "{" [ actor_field_init { "," actor_field_init } ] "}" ;
actor_field_init = IDENT ":" expr ;
(* Phase 8, #69: select — waits on the first ready arm; at most one timeout arm allowed. *)
(* Note: `timeout` is a *contextual* identifier inside a select arm, NOT a reserved word. *)
select_expr = "select" "{" { select_arm } "}" ;
select_arm = [ IDENT "=" ] expr "=>" block (* regular arm; optional result binding *)
| "timeout" "(" expr ")" "=>" block ; (* timeout arm — fires after duration *)
unary_expr = unary_op expr ;
binary_expr = expr binary_op expr ;
unary_op = "-" | "!" | "~" | "*" ; (* neg, logical-not, bitwise-not, deref *)
binary_op = "+" | "-" | "*" | "/" | "%" (* arithmetic *)
| "==" | "!=" | "<" | ">" | "<=" | ">=" (* comparison *)
| "&&" | "||" (* logical *)
| "&" | "|" | "^" (* bitwise AND / OR / XOR *)
| "<<" | ">>" ; (* left / right shift *)
borrow_expr = ( "val" | "ref" ) expr ; (* take shared or mutable reference *)
propagate = expr "?" ; (* Result/Option propagation *)
fn_call = path_name [ "[" type_list "]" ] "(" [ arg_list ] ")" ;
path_name = IDENT [ "[" type_list "]" ] [ "::" IDENT ] ;
(* Examples: foo(x) first[T](xs) Enum::Variant(x) Map[K,V]::new() *)
method_call = expr "." IDENT "(" [ arg_list ] ")" ;
field_access = expr "." IDENT ;
arg_list = expr { "," expr } ;
lambda = "|" [ param_list ] "|" [ "->" type_expr ] expr ;
construct = IDENT "{" { IDENT ":" expr "," } "}" ;
if_expr = "if" expr block "else" block
| "if" "let" pattern "=" expr block "else" block ; (* desugars to match; see #891 *)
match_expr = "match" expr "{" { match_arm } "}" ;
block_expr = block ;
(* === Patterns === *)
pattern = base_pattern { "|" base_pattern } ;
base_pattern = "_" | IDENT | literal
| IDENT "(" [ pattern_list ] ")"
| IDENT "{" { IDENT ":" base_pattern "," } [ ".." ] "}"
| "(" pattern "," pattern_list ")"
| "Some" "(" pattern ")" | "None"
| "Ok" "(" pattern ")" | "Err" "(" pattern ")" ;
pattern_list = pattern { "," pattern } ;
(* === Literals === *)
literal = INTEGER | FLOAT | STRING | CHAR | "true" | "false"
| list_literal | map_literal | set_literal ;
list_literal = "[" [ expr { "," expr } ] "]" ;
map_literal = "{" expr ":" expr { "," expr ":" expr } "}" ;
set_literal = "{" expr { "," expr } "}" ;
(* Note: empty "{}" is ambiguous — use Map::new() or Map[K,V]::new() for empty maps.
Map[K,V]::new() is preferred when no surrounding type annotation is available. *)
(* === Constants === *)
const_decl = "const" IDENT ":" type_expr "=" expr ";" ;
(* === Comments === *)
COMMENT = "//" { ANY_CHAR } NEWLINE ; (* line comment only, no block comments *)
DOC_COMMENT = "///" { ANY_CHAR } NEWLINE ; (* doc comment — convention, not syntax *)
(* === Reserved Keywords === *)
(* All identifiers below are unconditionally reserved — they CANNOT be used as *)
(* variable names, function names, type names, or import aliases. *)
(* This is a deliberate design choice (ADR-0005, ADR-0025): hard reservation *)
(* keeps the grammar LL(1) without contextual disambiguation and makes it *)
(* immediately clear to readers that these are language constructs, not library *)
(* identifiers. User-defined names that conflict must be renamed. *)
(* *)
(* Declaration: fn type const use pub extern impl builtin *)
(* struct enum actor effect test *)
(* Totality: total partial *)
(* Cast: as *)
(* Control flow: if else for in while match return select *)
(* Let binding: let ghost *)
(* Ownership: iso val ref tag consume *)
(* IFC: label relabel *)
(* Boolean: true false *)
(* Refinements: where self old requires ensures invariant with *)
(* decreases forall exists *)
(* Pattern: Some None Ok Err *)
(* === Lexical === *)
IDENT = ALPHA { ALPHA | DIGIT | "_" } ;
INTEGER = DIGIT { DIGIT } ;
FLOAT = DIGIT { DIGIT } "." DIGIT { DIGIT } ;
STRING = '"' { CHAR_ELEM } '"' (* single-line with escape sequences *)
| '"""' { CHAR_ELEM | NEWLINE } '"""' (* multiline — literal newlines preserved *)
| 'r"' { ANY_CHAR_EXCEPT_DQUOTE } '"' (* raw — no escape processing *)
| 'r"""' { ANY_CHAR } '"""' ; (* raw multiline *)
CHAR = "'" CHAR_ELEM "'" ;
ALPHA = "a"..."z" | "A"..."Z" | "_" ;
DIGIT = "0"..."9" ;
See Also¶
- Design Principle #8 — why LL(1) and why hand-written
- Language Reference — informal prose reference
- ADR-0005 — the recursive descent decision
- ADR-0053 — why
whereis refinements-only, never trait bounds - tree-sitter grammar — hand-translated for editor tooling