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.
grammar/grammar.ebnf in the mvl-spec repo is the single source of truth. The block below is embedded from it verbatim by tools/gen_grammar_page.py, and this site's build fails if the two disagree — so what you read here is what the spec says.
The Rust parser, the tree-sitter grammar, and the MVL-in-MVL parser must all match it. make validate-keywords and make test-grammar-coverage in the compiler repo verify that, and tools/generators/check-drift.sh in mvl-spec regenerates every downstream keyword table from this grammar on each PR.
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
(* ======================================================================== *)
(* DO NOT EDIT. Embedded verbatim from mvl-spec grammar/grammar.ebnf *)
(* Version: spec-v0.1.7 *)
(* Edit the grammar in mvl-spec, then run: python3 tools/gen_grammar_page.py *)
(* ======================================================================== *)
(* MVL — Minimum Verification Language — Formal Grammar *)
(* Notation: ISO 14977 Extended BNF *)
(* rule = body ; production *)
(* [ x ] optional *)
(* { x } zero or more *)
(* ( a | b ) alternation *)
(* "lit" terminal string *)
(* UPPER terminal token (defined in === Lexical === section) *)
(* (* comment *) EBNF comment *)
(* *)
(* The grammar is LL(1) — see ADR-0005. *)
(* The tree-sitter grammar lives in its own repository (mvl-lang/tree-sitter-mvl,*)
(* grammar.js at the root, per Zed's extension requirements) and is hand- *)
(* translated from this file. Run `make test-grammar-coverage` to verify *)
(* coverage. *)
(* === 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 (* #1915 — bounded universal quantifier *)
| exists_expr (* #1915 — bounded existential quantifier *)
| "(" ref_expr ")" | "!" ref_atom
| ref_atom ( "+" | "-" | "*" | "/" | "%" ) ref_atom ;
forall_expr = "forall" IDENT "in" "[" INTEGER ".." INTEGER "]" "." ref_expr ; (* #1915 — integer bounds only; unbounded `forall x: T,` is rejected by parser *)
exists_expr = "exists" IDENT "in" "[" INTEGER ".." INTEGER "]" "." ref_expr ; (* #1915 — integer bounds only; unbounded `exists x: T,` is rejected by parser *)
(* === 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` below) 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 "{" [ field_init { "," field_init } [ "," ] ] "}" ;
field_init = 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 === *)
(* `ctor_path` allows a single `::` segment in constructor / struct-pattern *)
(* heads so enum variants can be matched by their qualified name — e.g. *)
(* `match r { UpdateResult::Applied(t) => …, RejectReason::NotAuthorised => …} *)
(* Nested constructor patterns (e.g. `Rejected(RejectReason::Foo)`) work by *)
(* recursion: each argument is itself a `pattern`. *)
pattern = base_pattern { "|" base_pattern } ;
base_pattern = "_" | IDENT | literal
| ctor_path "(" [ pattern_list ] ")"
| ctor_path "{" [ field_pattern { "," field_pattern } [ "," ] ] [ ".." ] "}"
| ctor_path (* bare variant, no payload *)
| "(" pattern "," pattern_list ")"
| "Some" "(" pattern ")" | "None"
| "Ok" "(" pattern ")" | "Err" "(" pattern ")" ;
ctor_path = IDENT [ "::" IDENT ] ;
field_pattern = IDENT ":" base_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 requires ensures invariant with decreases *)
(* forall exists *)
(* Pattern: Some None Ok Err *)
(* === Contextual Keywords === *)
(* Special in ONE syntactic position and ordinary identifiers everywhere else. *)
(* The lexer does NOT reserve these — it emits IDENT and the parser disambiguates *)
(* by position. Verified empirically: `let end: Int = 1;` compiles clean, and the *)
(* same holds for each word below, whereas `let fn = 1;` is rejected. *)
(* *)
(* Consumers must anchor on the enclosing production, never match the bare word. *)
(* A flat keyword list highlights `let end = 5` as a keyword. *)
(* *)
(* Contextual: self old end timeout audit *)
(* *)
(* Where each is valid: *)
(* self refinement predicates — the value being refined. NOTE: appears in *)
(* no production; it is named only in the prose above. *)
(* old `ensures` only — see ref_atom, entry-time value *)
(* end session types only — see session_op *)
(* timeout `select` arms only — see select_arm *)
(* audit trailing marker on relabel_decl / relabel_expr. NOTE: `audit` is *)
(* also a stdlib module name (std/audit.mvl); the two do not collide *)
(* because neither is reserved. *)
(* *)
(* NOT a keyword of any kind: `len`. It appears as a quoted terminal in ref_atom *)
(* because the refinement sub-grammar admits no arbitrary calls and must therefore *)
(* enumerate the forms it allows. In ordinary code `len` is a compiler-known *)
(* method (`x.len()`, resolved in src/mvl/checker/method_types.rs); the *)
(* free-function form `len(x)` exists only inside a predicate. `let len = 5;` is *)
(* legal, so it is not reserved and not contextual. *)
(* === Builtin Types === *)
(* Reserved by convention only — the lexer does not protect them. Users should *)
(* not shadow them. `Option` and `Result` additionally appear as quoted terminals *)
(* in option_type / result_type productions. *)
(* *)
(* Builtin types: Int Int8 Int16 Int32 Int64 UInt8 UInt16 UInt32 *)
(* UInt64 Float Float32 Float64 Bool Char Byte String *)
(* Unit Option Result List Array Map Set *)
(* === Stdlib IFC Labels === *)
(* Ordinary identifiers, NOT reserved. Pre-seeded into the parser's known-label *)
(* set so `Tainted[T]` parses as a labeled_type without an explicit `label` *)
(* declaration. User code extends the set with `label Foo;`. *)
(* *)
(* There is NO `Public` label — an unlabeled type is public by absence (see *)
(* labeled_type above). There is no `Clean` label either. *)
(* *)
(* Stdlib labels: Tainted Secret ConfigPath DbUrl ApiEndpoint AuditTarget *)
(* === Lexical === *)
IDENT = ALPHA { ALPHA | DIGIT | "_" } ;
(* Digit-group separator `_` (mvl-lang/mvl-spec#38): permitted between digits
in every numeric literal form below, ignored in the literal's value. A
leading `_` is unreachable — the lexer dispatches on is_ascii_digit first
(or on the base-prefix branch, which itself requires at least one real
digit: `0x_` alone is an error, not a valid zero). A trailing `_` (e.g.
`1_`) is NOT rejected by the current implementation — this is a known gap,
not a deliberate design choice; see src/mvl/parser/lexer/numbers.rs. *)
INTEGER = DIGIT { DIGIT | "_" }
| "0" ( "x" | "X" ) HEX_DIGIT { HEX_DIGIT | "_" }
| "0" ( "b" | "B" ) BIN_DIGIT { BIN_DIGIT | "_" }
| "0" ( "o" | "O" ) OCT_DIGIT { OCT_DIGIT | "_" } ;
(* A float either has a fractional part (exponent optional) or has no
fractional part but does have an exponent — `1e10` is a float with no
`.` at all. Digits-only with neither is INTEGER, not FLOAT. *)
FLOAT = DIGIT { DIGIT | "_" } "." DIGIT { DIGIT | "_" } [ EXPONENT ]
| DIGIT { DIGIT | "_" } EXPONENT ;
EXPONENT = ( "e" | "E" ) [ "+" | "-" ] 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" ;
HEX_DIGIT = DIGIT | "a"..."f" | "A"..."F" ;
BIN_DIGIT = "0" | "1" ;
OCT_DIGIT = "0"..."7" ;
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 — its own repository since spec 0.1.3; keyword tables generated from this EBNF