Intro

a-mir-formality is an early-stage experimental project maintained by the Rust types team. Its goal is to be a complete, authoritative formal model of the Rust MIR and type system. If successful, the intention is to bring this model into Rust as an RFC and develop it as an official part of the language definition.

Workspace structure

The project is a Cargo workspace with three main crates, organized in layers:

• formality-macros — Procedural macros that generate boilerplate for formality terms. The #[term] macro auto-derives Parse, Debug, Fold, and Visit traits.
• formality-core — Language-independent foundation for formal semantics: variable binding, the judgment/proof system, fixed-point computation, and collections. Reusable for modeling any language, not just Rust.
• formality-rust — The Rust-specific model, containing three subsystems:
  • grammar/ — AST definitions for types, traits, impls, functions, ADTs, and a MIR subset
  • check/ — Semantic checking (entry point: check_all_crates())
  • prove/ — Trait solving and type normalization

The root a-mir-formality binary parses a Rust program file and runs check_all_crates().

Data flow

Program text
    → try_term()       (parse)
    → Program AST
    → check_all_crates()
    → per-crate checking
    → trait proving / normalization
    → ProofTree result

Running tests

# Run the full test suite (what CI runs)
cargo test --all

# Run all targets including doc tests
cargo test --all-targets

# Run a single integration test by name
cargo test -p a-mir-formality -- test_name

# Run tests in a specific crate
cargo test -p formality-rust
cargo test -p formality-core

To see tracing output from a test, set the RUST_LOG environment variable:

RUST_LOG=debug cargo test -p a-mir-formality -- test_name

Test macros

Integration tests use two snapshot-testing macros (powered by expect-test):

• assert_ok!([ ... ]) — asserts that a program type-checks successfully
• assert_err!([ ... ] expect![[...]]) — asserts that a program fails with a specific error message

formality_core: the Formality system

a-mir-formality is build on the formality core system, defined by the formality_core crate. Formality core is a mildly opnionated series of macros, derives, and types that let you write high-level Rust code in a way that resembles standard type theory notation. Its primary purpose is to be used by a-mir-formality but it can be used for other projects.

Defining your language

The very first thing you do to define your own language is to use the formality_core::declare_language! macro. You use it like so:

#![allow(unused)]
fn main() {
formality_core::declare_language! {
    pub mod rust {
        const NAME = "Rust";
        type Kind = crate::grammar::ParameterKind;
        type Parameter = crate::grammar::Parameter;
        const BINDING_OPEN = '<';
        const BINDING_CLOSE = '>';
        const KEYWORDS = [
            "mut",
            "struct",
            "enum",
            "union",
            "const",
            "true",
            "false",
            "static",
            "let",
            "in",
            "loop",
            "break",
            "continue",
            "return",

            "fn_id",
            "exists",
            "call",
            "print",
        ];
    }
}
}

The declare_language macro will create a module with the name you specify (here, rust). You have to tell it a few things:

• The NAME of your language, a string for debugging.
• An enum defining the kinds of variables in your language; see the variables chapter for more information. For Rust, the kinds are types, lifetimes, and constants.
• An enum defining a parameter, which is the terms that can be used to represent the value of a variable; see the variables chapter for more information.
• Two characters BINDER_OPEN and BINDER_CLOSED defining the opening and closing characters for binders, e.g., < and >, to use when parsing.

Contents of the language module

The language module you create has various items in it:

• A struct FormalityLang that defines your language. Some of the contains of formality_core (notably the traits that involve bound variables) are

Specifying the language for a crate

That module will contain a language struct named FormalityLang. Other parts of the formality system (e.g., autoderives and the like) will need to know the current language you are defining, and they expect to find it at crate::FormalityLang. Best practice is to add a use at the top of your crate defining your language. For example, the formality_rust crate has:

#![allow(unused)]
fn main() {
/// Declare the language that we will use in `#[term]` macros.
pub use rust::FormalityLang;
}

Defining terms with the term macro

There are two or three key things to understand. The first is the #[term] macro. This is a procedural macro that you can attach to a struct or enum declaration that represents a piece of Rust syntax or part of the trait checking rules. It auto-derives a bunch of traits and functionality…

• rules for parsing from a string
• a Debug impl to serialize back out
• folding and substitution
• upcasting and downcasting impls for convenient type conversion

For some types, we opt not to use #[term], and instead implement the traits by hand. There are also derives so you can derive some of the traits but not all.

Using #[term]

Let’s do a simple example. If we had a really simple language, we might define expressions like this:

#![allow(unused)]
fn main() {
#[term]
enum Expr {
    #[cast]
    Variable(Variable),
    
    #[grammar($v0 + $v1)]
    Add(Box<Expr>, Box<Expr>),
}

#[term($name)]
struct Variable {
    name: String
}
}

The #[term] macro says that these are terms and we should generate all the boilerplate automatically. Note that it will generate code that references crate::FormalityLang so be sure to define your language appropriately.

The #[term] also accepts some internal annotations:

• #[cast] can be applied on an enum variant with a single argument. It says that this variant represents an “is-a” relationship and hence we should generate upcast/downcast impls to allow conversion. In this case, a variable is a kind of expression – i.e,. wrapping a variable up into an expression doesn’t carry any semantic meaning – so we want variables to be upcastable to expressions (and expressions to be downcast to variables). The #[cast] attribute will therefore generate an impl Variable: Upcast<Expr> that lets you convert a variable to an expression, and a downcast impl Expr: Downcast<Variable> that lets you try to convert from an expression to a variable. Downcasting is fallible, which means that the downcast will only succeed if this is an Expr::Variable. If this is a Expr::Add, the downcast would return None.
  • There is a special case version of #[cast] called #[variable]. It indicates that the variant represents a (type) variable – we are not using it here because this an expression variable. Variables are rather specially in folding/parsing to allow for substitution, binders, etc.
• #[grammar] tells the parser and pretty printer how to parse this variant. The $v0 and $v1 mean “recursively parse the first and second arguments”. This will parse a Box<Expr>, which of course is implemented to just parse an Expr.

If you are annotating a struct, the #[term] just accepts the grammar directly, so #[term($name)] struct Variable means “to parse a variable, just parse the name field (a string)”.

We could also define types and an environment, perhaps something like

#![allow(unused)]
fn main() {
#[term]
enum Type {
    Integer, // Default grammar is just the word `integer`
    String // Default grammar is just the word `string`
}

#[term] // Default grammar is just `env($bindings)`
struct Env {
    bindings: Set<(Variable, Type)>
}
}

You can see that the #[term] macro will generate some default parsing rules if you don’t say anything.

We can then write code like

#![allow(unused)]
fn main() {
let env: Env = term("env({(x, integer)})");
}

This will parse the string, panicking if either the string cannot be parsed or or if it is ambiguous (can be parsing in mutiple ways). This is super useful in tests.

These terms are just Rust types, so you can define methods in the usual way, e.g. this Env::get method will search for a variable named v:

#![allow(unused)]
fn main() {
impl Env {
    pub fn get(&self, v: &Variable) -> Option<&Type> {
        self.bindings.iter()
            .filter(|b| &b.0 == v)
            .map(|b| &b.1)
            .next()
    }
}
}

Parsing

Formality’s #[term] and #[grammar] attributes let you specify a grammar for your structs and enums, and the parser will automatically parse strings into those types. Here is a simple example:

#![allow(unused)]
fn main() {
#[term]
pub enum Expr {
    #[grammar($v0)]
    LocalVariable(Id),

    #[grammar($v0 $(v1))]
    FnCall(Id, Vec<Id>),
}

formality_core::id!(Id);
}

This defines an Expr that is either a local variable (a single identifier like x) or a function call (like f(x, y)). The #[grammar] attribute on each variant describes how to parse it: $v0 means “parse the first field” and $(v1) means “parse a parenthesized, comma-separated list for the second field.” For structs, the grammar goes directly on #[term]:

#![allow(unused)]
fn main() {
#[term($name : $ty)]
pub struct TypedBinding {
    name: Id,
    ty: Ty,
}
}

This parses strings like x : i32.

Symbols

A grammar consists of a series of symbols. Each symbol matches some text in the input string. Symbols come in two varieties:

• Most things are terminals or tokens: this means they just match themselves:
  • For example, the * in #[grammar($v0 * $v1)] is a terminal, and it means to parse a * from the input.
  • Delimiters are accepted but must be matched, e.g., ( /* tokens */ ) or [ /* tokens */ ].
• The $ character is used to introduce special matches. Generally these are nonterminals, which means they parse the contents of a field, where the grammar for a field is determined by its type.
  • If fields have names, then $field should name the field.
  • For positional fields (e.g., the T and U in Mul(Expr, Expr)), use $v0, $v1, etc.
• Valid uses of $ are as follows:
  • $field – just parse the field’s type
  • $*field – the field must be a collection of T (e.g., Vec<T>, Set<T>) – parse any number of T instances. Something like [ $*field ] would parse [f1 f2 f3], assuming f1, f2, and f3 are valid values for field.
  • $,field – similar to the above, but uses a comma separated list (with optional trailing comma). So [ $,field ] will parse something like [f1, f2, f3].
  • $?field – will parse field and use Default::default() value if not present.
  • $<field> – parse <E1, E2, E3>, where field is a collection of E
  • $<?field> – parse <E1, E2, E3>, where field is a collection of E, but accept empty string as empty vector
  • $(field) – parse (E1, E2, E3), where field is a collection of E
  • $(?field) – parse (E1, E2, E3), where field is a collection of E, but accept empty string as empty vector
  • $[field] – parse [E1, E2, E3], where field is a collection of E
  • $[?field] – parse [E1, E2, E3], where field is a collection of E, but accept empty string as empty vector
  • ${field} – parse {E1, E2, E3}, where field is a collection of E
  • ${?field} – parse {E1, E2, E3}, where field is a collection of E, but accept empty string as empty vector
  • $:guard <nonterminal> – parses <nonterminal> but only if the keyword guard is present. For example, $:where $,where_clauses would parse where WhereClause1, WhereClause2, WhereClause3 but would also accept nothing (in which case, you would get an empty vector).
  • $! – marks a commit point, see the section on commit points below
  • $$ – parse the terminal $

Default grammar

If no grammar is supplied, the default grammar is determined as follows:

• If a #[cast] or #[variable] annotation is present, then the default grammar is just $v0.
• Otherwise, the default grammar is the name of the type (for structs) or variant (for enums), followed by (), with the values for the fields in order. So Mul(Expr, Expr) would have a default grammar mul($v0, $v1).

Ambiguity: parse all possibilities, disambiguate at the top

The parser takes a parse-all-possibilities approach. When parsing an enum, all variants are attempted, and all successful parses are returned — not just the “best” one. Ambiguity in a child nonterminal propagates upward through the parse tree, producing a cross-product of possibilities. For example, if a struct has two fields and each field’s nonterminal is 2-ways ambiguous, the struct produces 2 × 2 = 4 successful parses.

Consider this example, which parses either a single identifier (e.g., x) or a “call” (e.g., x(y, z)):

#![allow(unused)]
fn main() {
#[term]
pub enum Expr {
    #[grammar($v0)]
    LocalVariable(Id),

    #[grammar($v0 $(v1))]
    FnCall(Id, Vec<Id>),
}
}

Given an input like x(y, z), the result is actually ambiguous. It could be that you parsed as an expression x with remaining text (y, z) or as a call expression; therefore, the parser returns both.

Disambiguation happens once, at the top level (when you call term("...") or core_term_with). Here we would filter out the parse as x because it failed to consume all the input. That leaves exactly one parse, and so term succeeds. If multiple distinct parses remain, the result is an ambiguity panic — this means your grammar genuinely has an unresolvable ambiguity for that input. You can resolve these with #[precedence] for intra-type ambiguity (like expression operator precedence) or #[reject] for cross-type ambiguity (like boundary ambiguity between two types).

Sometimes disambiguation happens during parsing. For example, if we add another layer the example, like Sum:

#![allow(unused)]
fn main() {
#[term]
pub enum Expr {
    #[grammar($v0)]
    LocalVariable(Id),

    #[grammar($v0 $(v1))]
    FnCall(Id, Vec<Id>),
}

#[term]
pub enum Sum {
    #[grammar($v0 + $v1)]
    Add(Expr, Expr),
}
}

Now when parsing x(y) + z as a Sum, we would recursively parse it as an Expr and encounter the same two results:

• parsed x as a Expr::LocalVariable, remaining text (y) + z
• parsed x(y) as a Expr::FnCall, remaining text + z

However, only the second one can be parsed as a Sum, because the Sum requires the next character to be +.

Failure, almost succeeding, and commit points

When parsing fails, we distinguish two cases:

• Failure — the input clearly didn’t match. Usually this means the first token wasn’t a valid start for the nonterminal. You’ll get an error like “expected an Expr”.
• Almost succeeded — we got part-way through parsing, consuming some tokens, but then hit an error. For example, parsing "1 / / 3" as an Expr might give “expected an Expr, found /”.

The distinction matters when parsing optional ($?field) or repeated ($*field) nonterminals. If parsing field outright fails, we treat the field as absent and continue with its Default::default() value. If parsing field almost succeeds, we assume it was present but malformed, and report a syntax error.

The default rule is that parsing “almost” succeeds if it consumes at least one token. For example:

#![allow(unused)]
fn main() {
#[term]
enum Projection {
  #[grammar(. $v0)]
  Field(Id),
}
}

Parsing ".#" as a Projection would “almost” succeed — it consumes the . but then fails to find an identifier.

Sometimes this default is too aggressive. Consider Projection embedded in another type:

#![allow(unused)]
fn main() {
#[term($*projections . #)]
struct ProjectionsThenHash {
  projections: Vec<Projection>,
}
}

We’d like ".#" to be a valid ProjectionsThenHash — zero projections followed by .#. But the parser sees the . as an “almost success” of a Projection, so it reports a syntax error instead of treating the projections list as empty.

Commit points

You can control this with $!, which marks a commit point. With $!, a parse is only considered to have “almost succeeded” if it reached the commit point. Before the commit point, failure is just failure (the variant wasn’t present).

Adding $! after the identifier in Projection fixes the problem:

#![allow(unused)]
fn main() {
#[term]
enum Projection {
  #[grammar(. $v0 $!)]
  Field(Id),
}
}

Now .# fails outright (the commit point after $v0 was never reached), so ProjectionsThenHash correctly treats the projections list as empty and parses .# as the trailing literal tokens.

See the parser_torture_tests::commit_points code for a working example.

Variables and scope

Most compilers parse source text into an ambiguous syntax tree first, then apply name resolution and semantics to figure out what things mean. Formality aims to parse more directly into a semantically meaningful representation — for example, distinguishing variables from identifiers during parsing rather than in a later pass.

Today this shows up in one place: variable scope. When you write <X> X, the binder <X> introduces X into scope, and the body X is parsed as a variable reference rather than an identifier. This is the one piece of context the parser carries, but we may expand context-sensitive parsing in the future.

How variable/identifier disambiguation works

The problem: when an enum has both a #[variable] variant and fields that use id! types, the same text could parse as either a variable or an identifier. Without disambiguation, this produces an ambiguity panic.

The solution: when the parser begins parsing an enum that has a #[variable] variant, it runs an upfront probe — “can this text be parsed as any in-scope variable?” If yes, it sets a flag on the parser stack. All id! types check this flag before accepting an identifier and reject the text if the flag is set.

To see how this works, consider a type system with types and permissions, where types can be variables, named types, or a permission applied to a type:

#![allow(unused)]
fn main() {
#[term]
pub enum Ty {
    #[variable(Kind::Ty)]
    Variable(Variable),

    #[cast]
    Id(Id),

    #[grammar($v0 $v1)]
    Apply(Perm, Arc<Ty>),

    #[grammar($v0 :: $v1)]
    Assoc(Arc<Ty>, AssocId),
}

#[term]
pub enum Perm {
    #[variable(Kind::Perm)]
    Variable(Variable),
}

formality_core::id!(Id);
formality_core::id!(AssocId);
}

Same-type disambiguation. With type variable T in scope, parse T as a Ty. Because Ty has a #[variable] variant, the parser probes: “can T be parsed as any in-scope variable?” Yes — T is a type variable. The flag is set. Now when the Id variant tries to parse T, Id (an id! type) checks the flag, sees it’s set, and rejects. Only Variable(T) succeeds. Without the flag, both Variable(T) and Id(T) would succeed — ambiguity panic.

Cross-type disambiguation. With perm variable P in scope, parse P i32 as a Ty. The parser begins parsing Ty at P and runs the probe. The probe asks “can P be parsed as any in-scope variable?” — and it can, because P is a perm variable. The probe checks for variables of any kind, not just the kind associated with this type’s #[variable] variant. So the flag is set. Id rejects P. But Perm’s #[variable] variant does match P, so the Apply variant succeeds: Apply(Variable(P), Id(i32)).

This cross-kind behavior is what makes the mechanism work across type boundaries. Ty’s probe finds the perm variable P even though Ty’s own #[variable] variant only accepts type variables. This prevents Id from claiming a name that belongs to a sibling type’s variable namespace.

Positional scoping. Parse i32::T as a Ty, with type variable T in scope. The outer Ty parse starts at i32::T. The probe asks “can i32::T be parsed as a variable?” No — i32 isn’t a variable name, so no flag is set. The Assoc variant parses i32 as a Ty, consumes ::, then parses T as an AssocId. At that text position, no type with a #[variable] variant is being parsed (only AssocId, an id! type, is being parsed here), so no probe has run. AssocId accepts T as a plain identifier. This is the right behavior — T after :: is an associated item name, not a variable reference.

See tests/parser_var_id_ambiguity.rs for working tests of all three scenarios.

Left-recursive grammars

We support left-recursive grammars. A grammar is left-recursive when one of its variants starts by parsing itself. For example, a path like a.b[c.d].e is naturally left-recursive:

#![allow(unused)]
fn main() {
#[term]
pub enum Path {
    #[cast]
    Id(Id),

    #[grammar($v0 . $v1)]
    Field(Arc<Path>, Id),

    #[grammar($v0 [ $v1 ])]
    Index(Arc<Path>, Arc<Path>),
}

formality_core::id!(Id);
}

This works because the parser handles left-recursion with a fixed-point loop: it first parses the base cases (just an Id), then repeatedly tries to extend those results with the left-recursive variants (Field, Index), accumulating all successful parses until no new ones are found. In this grammar there’s no ambiguity because . and [ are unambiguous delimiters between the parts.

Precedence

Often left-recursive grammars are ambiguous. For example, arithmetic expressions:

#![allow(unused)]
fn main() {
#[term]
pub enum Expr {
    #[cast]
    Id(Id),

    #[grammar($v0 + $v1)]
    #[precedence(1)]
    Add(Arc<Expr>, Arc<Expr>),

    #[grammar($v0 * $v1)]
    #[precedence(2)]
    Mul(Arc<Expr>, Arc<Expr>),
}

formality_core::id!(Id);
}

Without the #[precedence] annotations, a + b * c would have two parses: (a + b) * c and a + (b * c). The precedence annotations resolve this. Higher numbers bind tighter, so * (level 2) binds tighter than + (level 1), giving a + (b * c).

The default associativity is left, which can be written explicitly as #[precedence(L, left)]. You can also specify right-associativity (#[precedence(L, right)]) or non-associativity (#[precedence(L, none)]). This affects how things of the same level are parsed:

• a + b + c when left-associative is (a + b) + c
• a + b + c when right-associative is a + (b + c)
• a + b + c when none-associative is an error.

Explicit parenthesization

One thing precedence doesn’t give you is user-controlled grouping. In a real expression grammar you’d want to write (a + b) * c to override the default precedence. Formality doesn’t currently handle this automatically. You have to add an explicit Parens variant to your grammar:

#![allow(unused)]
fn main() {
#[term]
pub enum PlaceExpr {
    /// `x`
    ///
    /// A variable reference. Whether this is a place (lvalue) or
    /// value (rvalue) depends on context: place on the left of `=`
    /// or as operand of `&`, value everywhere else.
    #[cast]
    Var(ValueId),

    /// `* expr`
    ///
    /// Dereference. Like `Var`, place vs value depends on context.
    #[grammar(* $prefix)]
    Deref { prefix: Arc<PlaceExpr> },

    /// `( expr )`
    ///
    /// Parenthesized expression, needed so users can write `(*x).field`.
    #[grammar(($v0))]
    Parens(Arc<PlaceExpr>),

    /// `expr . field`
    ///
    /// Field projection. Like `Var`, place vs value depends on context.
    #[grammar($prefix . $field_name)]
    #[reject(PlaceExpr::Deref { .. }, _)]
    Field {
        prefix: Arc<PlaceExpr>,
        field_name: FieldName,
    },
}
}

Here PlaceExpr has a prefix operator (* expr) and a postfix operator (expr . field). Without the Parens variant, there’s no way to distinguish *(x.field) from (*x).field. Adding #[grammar(($v0))] Parens(PlaceExpr) lets the user write (*x).field to make the grouping explicit.

This is admittedly a bit awkward. Formality’s design goal is that the type structure matches what you’d find in a paper, and Parens nodes are parser machinery, not semantics. We may improve this in the future.

Cross-type ambiguity and #[reject]

Precedence handles ambiguity within a single recursive type, but sometimes the ambiguity is between two types. Consider a grammar where a Perm can be composed by juxtaposition (Perm Perm) and a Ty can apply a perm to a type (also by juxtaposition):

#![allow(unused)]
fn main() {
#[term]
pub enum Perm {
    #[grammar(leaf)]
    Leaf,

    #[grammar(given)]
    Given,

    #[cast]
    Id(PermId),

    #[grammar($v0 $v1)]
    Apply(Arc<Perm>, Arc<Perm>),
}

formality_core::id!(PermId);

#[term]
pub enum Ty {
    #[grammar($v0)]
    Named(TyId),

    #[grammar($v0 $v1)]
    #[reject(Perm::Apply(..), _)]
    ApplyPerm(Perm, Arc<Ty>),
}

formality_core::id!(TyId);
}

Parsing leaf x Data as a Ty is ambiguous. The parser doesn’t know where Perm ends and Ty begins:

• Perm = leaf, Ty = ApplyPerm(Id(x), Named(Data)) … i.e., the perm is just leaf
• Perm = Apply(Leaf, Id(x)), Ty = Named(Data) … i.e., the perm is leaf x

Both consume all the input, so the normal disambiguation (longest match) doesn’t help. You could restructure the grammar, but in formality the grammar is the type, and you likely don’t want to extract a different type just to control parsing.

The #[reject] attribute solves this at the use site. In the example above, #[reject(Perm::Apply(..), _)] on Ty::ApplyPerm says “reject any parse where the first field is a compound perm.” The second interpretation is silently dropped, leaving just one unambiguous parse.

The syntax: each position in #[reject] corresponds to a field of the variant. Use _ to skip a field (no constraint). Non-wildcard positions use Rust patterns and are checked with matches! under the hood. All fields must be listed explicitly, or you can use trailing .. to skip remaining fields (e.g., #[reject(Perm::Apply(..), ..)]). Omitting fields without .. is a compile error. Multiple #[reject] attributes on the same variant are OR’d (any match rejects). Within a single #[reject], non-wildcard fields are AND’d.

For named fields (on structs), use name: pattern syntax:

#![allow(unused)]
fn main() {
#[term($perm $ty)]
#[reject(perm: Perm::Apply(..), ty: _)]
pub struct ApplyPerm {
    perm: Perm,
    ty: Arc<Ty>,
}
}

See tests/parser-torture-tests/reject.rs for the full set of examples.

Customizing the parse

If you prefer, you can customize the parse by annotating your term with #[customize(parse)]. In the Rust case, for example, the parsing of RigidTy is customized (as is the debug impl):

#![allow(unused)]
fn main() {
#[term((rigid $name $*parameters))]
#[customize(parse, debug)]
pub struct RigidTy {
    pub name: RigidName,
    pub parameters: Parameters,
}
}

You must then supply an impl of CoreParse<L> for your language type L. Inside the impl you will want to instantiate a Parser and then invoke parse_variant for every variant. The key methods on ActiveVariant are:

• each_nonterminal(|value: T, p| { ... }) — the primary way to parse a child nonterminal. Instead of returning a single result, it calls the continuation for each successful parse of T, passing a forked ActiveVariant positioned at that parse’s remaining text. This is how ambiguity propagates: if T has 2 parses, the continuation runs twice, and the results are collected.
• each_comma_nonterminal(|items: Vec<T>, p| { ... }) — parse a comma-separated list, then run the continuation with the result.
• each_opt_nonterminal(|opt: Option<T>, p| { ... }) — parse an optional nonterminal.
• each_many_nonterminal(|items: Vec<T>, p| { ... }) — parse zero or more nonterminals.
• each_delimited_nonterminal(open, optional, close, |items: Vec<T>, p| { ... }) — parse a delimited comma-separated list (e.g., <T1, T2>).
• p.ok(value) — wrap a value into a successful parse result. Use this instead of Ok(value) at the end of variant closures.
• expect_char(c), expect_keyword(kw) — consume expected tokens.
• reject_nonterminal::<T>() — fail if the input starts with a T (useful for disambiguation).

The continuation-passing style means nonterminal parsing is always nested: you parse the first field, then in its continuation parse the second field, and so on. Each each_* call forks for each ambiguous child result, so you get the cross-product automatically.

In the Rust code, the impl for RigidTy looks as follows:

#![allow(unused)]
fn main() {
// Implement custom parsing for rigid types.
impl CoreParse<Rust> for RigidTy {
    fn parse<'t>(scope: &Scope<Rust>, text: &'t str) -> ParseResult<'t, Self> {
        Parser::multi_variant(scope, text, "RigidTy", |parser| {
            // Parse a `ScalarId` (and upcast it to `RigidTy`) with the highest
            // precedence. If someone writes `u8`, we always interpret it as a
            // scalar-id.
            parser.parse_variant_cast::<ScalarId>(Precedence::default());

            // Parse something like `Id<...>` as an ADT.
            parser.parse_variant("Adt", Precedence::default(), |p| {
                // Don't accept scalar-ids as Adt names.
                p.reject_nonterminal::<ScalarId>()?;

                p.each_nonterminal(|name: AdtId, p| {
                    each_parse_parameters(p, |parameters, p| {
                        p.ok(RigidTy {
                            name: name.clone().upcast(),
                            parameters,
                        })
                    })
                })
            });

            // Parse `&`
            parser.parse_variant("Ref", Precedence::default(), |p| {
                p.expect_char('&')?;
                p.each_nonterminal(|lt: Lt, p| {
                    p.each_nonterminal(|ty: Ty, p| {
                        p.ok(RigidTy {
                            name: RigidName::Ref(RefKind::Shared),
                            parameters: seq![lt.clone().upcast(), ty.upcast()],
                        })
                    })
                })
            });

            parser.parse_variant("RefMut", Precedence::default(), |p| {
                p.expect_char('&')?;
                p.each_nonterminal(|lt: Lt, p| {
                    p.expect_keyword("mut")?;
                    p.each_nonterminal(|ty: Ty, p| {
                        p.ok(RigidTy {
                            name: RigidName::Ref(RefKind::Mut),
                            parameters: seq![lt.clone().upcast(), ty.upcast()],
                        })
                    })
                })
            });

            parser.parse_variant("RawConst", Precedence::default(), |p| {
                p.expect_char('*')?;
                p.expect_keyword("const")?;
                p.each_nonterminal(|ty: Ty, p| {
                    p.ok(RigidTy {
                        name: RigidName::Raw(PtrKind::Const),
                        parameters: seq![ty.upcast()],
                    })
                })
            });

            parser.parse_variant("RawMut", Precedence::default(), |p| {
                p.expect_char('*')?;
                p.expect_keyword("mut")?;
                p.each_nonterminal(|ty: Ty, p| {
                    p.ok(RigidTy {
                        name: RigidName::Raw(PtrKind::Mut),
                        parameters: seq![ty.upcast()],
                    })
                })
            });

            parser.parse_variant("Tuple", Precedence::default(), |p| {
                p.expect_char('(')?;
                p.reject_custom_keywords(&["alias", "rigid", "predicate"])?;
                p.each_comma_nonterminal(|types: Vec<Ty>, p| {
                    p.expect_char(')')?;
                    let name = RigidName::Tuple(types.len());
                    p.ok(RigidTy {
                        name,
                        parameters: types.upcast(),
                    })
                })
            });
        })
    }
}
}

Customizing the debug

By default, the #[term] macro will generate a Debug impl that is guided by the #[grammar] attributes on your type (see the parsing section for more details). But sometimes you want to generate custom logic. You can include a #[customize(debug)] declaration to allow that. Most of the type, when you do this, you will also want to customize parsing, as the RigidTy does:

#![allow(unused)]
fn main() {
#[term((rigid $name $*parameters))]
#[customize(parse, debug)]
pub struct RigidTy {
    pub name: RigidName,
    pub parameters: Parameters,
}
}

Now you must simply implement Debug in the usual way. Here is the RigidTy declaration:

#![allow(unused)]
fn main() {
impl Debug for RigidTy {
    fn fmt(&self, f: &mut std::fmt::Formatter<'_>) -> std::fmt::Result {
        let RigidTy { name, parameters } = self;
        match name {
            RigidName::AdtId(name) => {
                write!(
                    f,
                    "{:?}{:?}",
                    name,
                    PrettyParameters::new("<", ">", parameters)
                )
            }
            RigidName::ScalarId(s) if parameters.is_empty() => {
                write!(f, "{:?}", s)
            }
            RigidName::Ref(RefKind::Shared) if parameters.len() == 2 => {
                write!(f, "&{:?} {:?}", parameters[0], parameters[1])
            }
            RigidName::Ref(RefKind::Mut) if parameters.len() == 2 => {
                write!(f, "&{:?} mut {:?}", parameters[0], parameters[1])
            }
            RigidName::Raw(PtrKind::Const) if parameters.len() == 1 => {
                write!(f, "*const {:?}", parameters[0])
            }
            RigidName::Raw(PtrKind::Mut) if parameters.len() == 1 => {
                write!(f, "*mut {:?}", parameters[0])
            }
            RigidName::Tuple(arity) if parameters.len() == *arity => {
                if *arity != 0 {
                    write!(f, "{:?}", PrettyParameters::new("(", ")", parameters))
                } else {
                    // PrettyParameters would skip the separators
                    // for 0 arity
                    write!(f, "()")
                }
            }
            _ => {
                write!(f, "{:?}{:?}", name, PrettyParameters::angle(parameters))
            }
        }
    }
}
}

Constructors

Unless you include #[customize(constructors)], the #[term] macro automatically creates constructors as follows:

• For a struct, defines a new method that takes an impl Upcast<T> for each of your fields.
• For an enum, defines a method per variant that has fields (converted to snake-case).
  • If the name of the variant is a Rust keyword like Struct, the method will be called struct_.
  • We do not generate constructors for variants with no arguments.

Variables

As in Defining your lang, declare_language! implements Language by setting the associated types Kind and Parameter. They must satisfy the bounds on that trait (including HasKind for Parameter); in formality_rust both are enums:

• Kind — the sorts of parameter (type, lifetime, const, …). Classifies variables and binders.
• Parameter — the values a parameter can be instantiated to.

The generated language module also defines pub type aliases in grammar (Variable, Binder, Substitution, …) that specialize the formality_core types to FormalityLang.

Internally, variables use CoreVariable<L>:

• UniversalVariables — treated as an unknown assumed in the environment.
• ExistentialVariables — a metavariable the rules will eventually constrain or solve.
• BoundVariables — tied to an enclosing binder (de Bruijn level and slot index). Binder::open introduces fresh bound variables with debruijn: None (see CoreBoundVar::fresh) Binder::new closes the binder again.

CoreVariable::is_free: universals and existentials are always free. A bound variable is free iff debruijn is None (including after Binder::open).

In #[term] definitions, use #[variable] on variable variants so folding applies substitutions and parsing resolves names against in-scope bindings (see Defining terms with the term macro).

Collections

When using formality, it’s best to use the following collection types:

• for sequences, use the standard Vec type
• formality_core::Set<T> – equivalent to BTreeSet but shorter. We use a BTreeSet because it has deterministic ordering for all operations.
• formality_core::Map<K, V> – equivalent to BTreeMap but shorter. We use a BTreeMap because it has deterministic ordering for all operations.

Macros

We also define macros:

• seq![...] – equivalent to vec![] but permits flattening with .. notation, as described below
• set![...] – like seq!, but produces a Set

In these macros you can “flatten” things that support IntoIterator, so set![..a, ..b] will effectively perform a set union of a and b.

Casting between collections and tuples

It is possible to upcast from variable tuple types to produce collections:

• A Vec<E1> can be upcast to a Vec<E2> if E1: Upcast<E2>.
• A Set<E1> can be upcast to a Set<E2> if E1: Upcast<E2>.
• Tuples of elements (e.g., (E1, E2) or (E1, E2, E3)) can be upcast to sets up to a fixed arity.
• Sets and vectors can be downcast to () and (E, C), where () succeeds only for empty collections, and (E, C) extracts the first element E and a collection C with all remaining elements (note that elements in sets are always ordered, so the first element is well defined there). This is useful when writing judgment rules that operate over sequences and sets.

Judgment functions and inference rules

The next thing is the judgment_fn! macro. This lets you write a judgment using inference rules. A “judgment” just means some kind of predicate that the computer can judge to hold or not hold. Inference rules are those rules you may have seen in papers and things:

premise1
premise2
premise3
------------------
conclusion

i.e., the conclusion is judged to be true if all the premises are true.

Judgments in type system papers can look all kinds of ways. For example, a common type system judgment would be the following:

Γ ⊢ E : T

This can be read as, in the environment Γ, the expression E has type T. You might have rule like these:

Γ[X] = ty                   // lookup variable in the environment
--------------- "variable"
Γ ⊢ X : ty

Γ ⊢ E1 : T                  // must have the same type
Γ ⊢ E2 : T
--------------- "add"
Γ ⊢ E1 + E2 : T

In a-mir-formality, you might write those rules like so:

#![allow(unused)]
fn main() {
judgment_fn! {
    pub fn has_type(
        env: Env,
        expr: Expr,
    ) => Type {
        (
            (env.get(&name) => ty)
            ---------------
            (has_type(env, name: Variable) => ty)
        )
        
        (
            (has_type(env, left) => ty_left)
            (has_type(env, right) => ty_right)
            (if ty_left == ty_right)
            ---------------
            (has_type(env, Expr::Add(left, right)) => ty_left)
        )
    }
}
}

Unlike mathematical papers, where judgments can look like whatever you want, judgments in a-mir-formality always have a fixed form that distinguish inputs and outputs:

judgment_name(input1, input2, input3) => output

In this case, has_type(env, expr) => ty is the equivalent of Γ ⊢ E : T. Note that, by convention, we tend to use more English style names, so env and not Γ, and expr and not E. Of course nothing is stop you from using single letters, it’s just a bit harder to read.

When we write the judgement_fn, it is going to desugar into an actual Rust function that looks like this:

#![allow(unused)]
fn main() {
pub fn has_type(arg0: impl Upcast<Env>, arg1: impl Upcast<Expr>) -> ProvenSet<Type> {
    let arg0: Env = arg0.upcast();
    let arg1: Expr = arg1.upcast();
    
    ...
}
}

Some things to note. First, the function arguments (arg0, arg1) implicitly accept anything that “upcasts” (infallibly converts) into the desired types. Upcast is a trait defined within a-mir-formality and implemented by the #[term] macro automatically.

Second, the function always returns a ProvenSet. This is because there can be more rules, and they may match in any ways. The generated code is going to exhaustively search to find all the ways that the rules could match. Unlike a plain Set, a ProvenSet also preserves proof trees for successful results and structured failure information when no rule applies. At a high-level the code looks like this (at least if we ignore the possibility of cycles; we’ll come back to that later):

#![allow(unused)]
fn main() {
pub fn has_type(arg0: impl Upcast<Env>, arg1: impl Upcast<Expr>) -> ProvenSet<Type> {
    let arg0: Env = arg0.upcast();
    let arg1: Expr = arg1.upcast();
    
    let mut results = Map::new();

    if /* inference rule 1 matches */ {
        results.insert(/* result from inference rule 1 */, /* proof tree */);
    }
    
    if /* inference rule 2 matches */ {
        results.insert(/* result from inference rule 2 */, /* proof tree */);
    }
    
    // ... 
    
    if /* inference rule N matches */ {
        results.insert(/* result from inference rule N */, /* proof tree */);
    }
    
    if !results.is_empty() {
        ProvenSet::proven(results)
    } else {
        ProvenSet::failed_rules(/* judgment */, /* location */, /* failed rules */)
    }
}
}

So how do we test if a particular inference rule matches? Let’s look more closely at the code we would generate for this inference rule:

#![allow(unused)]
fn main() {
(
    (env.get(name) => ty)
    ---------------
    (has_type(env, name: Variable) => ty)
)
}

The first part of the final line, has_type(env, name: Variable), defines patterns that are matched against the arguments. These are matched against the arguments (arg0, arg1) from the judgment. Patterns can either be trivial bindings (like env) or more complex (like name: Variable or Expr::Add(left, right)). In the latter case, they don’t have to match the type of the argument precisely. Instead, we use the Downcast trait combined with pattern matching. So this inference rule would compile to something like…

#![allow(unused)]
fn main() {
// Simple variable bindings just clone...
let env = arg0.clone();

// More complex patterns are downcasted and testing...
if let Some(name) = arg1.downcast::<Variable>() {
    ... // rule successfully matched! See below.
}
}

Once we’ve matched the arguments, we start trying to execute the inference rule conditions. We have one, env.get(&name) => ty. What does that do? A condition written like $expr => $pat basically becomes a for loop, so you get…

#![allow(unused)]
fn main() {
let env = arg0.clone();
if let Some(name) = arg1.downcast::<Variable>() {
    for ty in env.get(&name) {
        ... // other conditions, if any
    }
}
}

Once we run out of conditions, we can generate the final result, which comes from the => $expr in the conclusion of the rule. In this case, something like this:

#![allow(unused)]
fn main() {
let env = arg0.clone();
if let Some(name) = arg1.downcast::<Variable>() {
    for ty in env.get(&name) {
        result.push(ty);
    }
}
}

Thus each inference rule is converted into a little block of code that may push results onto the final set.

The second inference rule (for addition) looks like…

#![allow(unused)]
fn main() {
// given this...
// (
//     (has_type(env, left) => ty_left)
//     (has_type(env, right) => ty_right)
//     (if ty_left == ty_right)
//     ---------------
//     (has_type(env, Expr::Add(left, right)) => ty_left)
// )
// we generate this...
let env = arg0.clone();
if let Some(Expr::Add(left, right)) = arg1.downcast() {
    for ty_left in has_type(env, left) {
        for ty_right in has_type(env, right) {
            if ty_left == ty_right {
                result.push(ty_left);
            }
        }
    }
}
}

If you want to see a real judgement, take a look at the one for proving where clauses:

prove_wc(_decls: Program, env: Env, assumptions: Wcs, goal: Wc,) => Constraints

Handling cycles

Judgment functions must be inductive, which means that cycles are considered failures. We have a tabling implementation, which means we detect cycles and try to handle them intelligently. Basically we track a stack and, if a cycle is detected, we return an empty set of results. But we remember that the cycle happened. Then, once we are done, we’ll have computed some intermediate set of results R[0], and we execute again. This time, when we get the cycle, we return R[0] instead of an empty set. This will compute some new set of results, R[1]. So then we try again. We keep doing this until the new set of results R[i] is equal to the previous set of results R[i-1]. At that point, we have reached a fixed point, so we stop. Of course, it could be that you get an infinitely growing set of results, and execution never terminates. This means your rules are broken. Don’t do that.

FAQ and troubleshooting

Why am I getting errors about undefined references to crate::FormalityLang?

The various derive macros need to know what language you are working in. To figure this out, they reference crate::FormalityLang, which you must define. See the chapter on defining your language for more details.

formality_rust: the Rust model

formality_rust is the Rust-specific layer of a-mir-formality. It is organized into three main subsystems:

• grammar/ defines Rust-specific terms
• check/ runs semantic checking
• prove/ discharges logical obligations

grammar/

The grammar module defines the Rust terms used by the model: crates, items, types, where-clauses, trait references, and the MIR-like expression language used in function bodies.

check/

The main checking entry point is check_all_crates:

check_all_crates(crates: Crates,) => ()

It inserts an empty core crate if the first crate is not core, then checks every prefix of the crate list (treating the last crate in each prefix as the current crate).

Within a crate, checking rejects duplicate item names, checks each crate item, and then runs coherence checking:

check_crate(program: Program, c: Crate,) => ()

The different kinds of crate items are dispatched by check_crate_item:

check_crate_item(program: Program, c: CrateItem, crate_id: CrateId,) => ()

prove/

The prove module answers Rust-specific goals such as where-clauses, equality, subtyping, and outlives. Checking code calls into prove whenever it needs to establish those facts. The main entry point is prove_wc:

prove_wc(_decls: Program, env: Env, assumptions: Wcs, goal: Wc,) => Constraints

Pipeline

At a high level, checking a Rust program looks like this:

Crates
  -> check_all_crates
  -> item checking / borrow checking
  -> prove obligations as needed

Borrow checking

Borrow checking lives under check/borrow_check/. Its top-level judgment is borrow_check, which checks that the loans issued while executing a basic block are respected.

borrow_check

borrow_check(env: TypeckEnv, assumptions: Wcs, state: FlowState, block: Block,) => ()

At the top level, borrow checking works over a TypeckEnv, a set of assumptions, a FlowState, and a Block. It delegates to borrow_check_block, which walks the block and updates the flow state statement by statement:

borrow_check_block(env: TypeckEnv, assumptions: Wcs, state: FlowState, block: Block, places_live_on_exit: LivePlaces,) => FlowState

Statements

borrow_check_statement handles each kind of statement. Here are some representative rules:

let bindings

(prove_ty_is_wf(env, assumptions, state, ty) => state)
(for_all(init in init.into_iter()) with (state) // FIXME: should make syntax for this
    (let Init { expr } = init)
    (borrow_check_expr_has_ty(env,
        assumptions,
        state,
        expr,
        ty,
        LiveBefore::live_before(&Assignment(id), env, &state, &places_live_on_exit),
    ) => state))

(let state = state.with_local_in_scope(&env.env, label, id, ty)?)
(let state = if init.is_none() { state.with_uninit(&PlaceExpr::Var(id.clone())) } else { state.with_initialized(&PlaceExpr::Var(id.clone())) })
------------------------------------------------------------ ("let")
(borrow_check_statement(env, assumptions, state, Stmt::Let { label, id, ty, init }, places_live_on_exit) => (env, state))

if expressions

(borrow_check_expr_has_ty(
    env,
    assumptions,
    state,
    condition,
    Ty::bool(),
    Either(then_block, &else_block.block).live_before(env, &state, places_live_on_exit),
) => state)

(borrow_check_block(env, assumptions, state, then_block, places_live_on_exit) => then_state)
(borrow_check_block(env, assumptions, state, &else_block.block, places_live_on_exit) => else_state)

(let state: FlowState = Union((then_state, else_state)).upcast())
------------------------------------------------------------ ("if")
(borrow_check_statement(env, assumptions, state, Stmt::If { condition, then_block, else_block }, places_live_on_exit) => (env, state))

loop

(let continue_live = Stmt::loop_(label, body).live_before(&env, &state, places_live_on_exit))
(let state = state.push_continue_scope(&env.env, label, places_live_on_exit, continue_live)?)
(borrow_check_loop(env, assumptions, state, body, places_live_on_exit) => state)
(let state = state.pop_scope(label))
------------------------------------------------------------ ("loop")
(borrow_check_statement(env, assumptions, state, Stmt::Loop { label, body }, places_live_on_exit) => (env, state))

break and continue

(if state.scope_has_label(label))!
(let locals_to_drop = state.locals_dropped_to_label(label))
(drop_places(env, assumptions, state, locals_to_drop, places_live_on_exit) => state)
(let state = state.with_break(label))
(let state = state.diverges())
------------------------------------------------------------ ("break")
(borrow_check_statement(env, assumptions, state, Stmt::Break { label }, places_live_on_exit) => (env, state))

(if state.scope_has_label(label))!
(if let Some(places_live_on_continue) = state.live_after_continue(label))
(let locals_to_drop = state.locals_dropped_to_label(label))
(drop_places(env, assumptions, state, locals_to_drop, places_live_on_continue) => state)
(let state = state.with_continue(label))
(let state = state.diverges())
------------------------------------------------------------ ("continue")
(borrow_check_statement(env, assumptions, state, Stmt::Continue { label }, places_live_on_exit) => (env, state))

return

(borrow_check_expr(env, assumptions, state, expr, LivePlaces::default()) => (expr_ty, state))
(if let Some(output_ty) = &env.output_ty)
(prove_assignable(env, assumptions, state, expr_ty, output_ty) => state)
(let state = state.diverges())
------------------------------------------------------------ ("return")
(borrow_check_statement(env, assumptions, state, Stmt::Return { expr }, _places_live_on_exit) => (env, state))

Expressions

Borrow checking of value expressions is handled by borrow_check_expr:

borrow_check_expr(env: TypeckEnv, assumptions: Wcs, state: FlowState, expr: Expr, places_live_on_exit: LivePlaces,) => (Ty, FlowState)

Outlives

Borrow checking also accumulates pending outlives constraints. The outlives.rs code verifies these constraints:

verify_universal_outlives(env: TypeckEnv, assumptions: Wcs, outlives: Set<PendingOutlives>,) => ()

Existential variables succeed trivially; universal variables must be justified by the assumptions:

only_assumed_outlives(env: TypeckEnv, assumptions: Wcs, outlives: Set<PendingOutlives>, v: Variable,) => ()

Coherence checking

Coherence checking lives in check/coherence.rs and runs as part of crate checking.

check_coherence

check_coherence(program: Program, current_crate: Crate) => ()

At a high level, check_coherence:

• rejects duplicate impls in the current crate
• checks the current crate’s impls for overlap against all impls in the program
• runs orphan checking for positive impls in the current crate
• runs orphan checking for negative impls in the current crate

Orphan checking

orphan_check(program: Program, impl_a: TraitImpl) => ()

orphan_check instantiates the impl binder universally and proves that the trait reference is local under the impl’s where-clauses.

Negative impls have the same structure:

orphan_check_neg(program: Program, impl_a: NegTraitImpl) => ()

Overlap checking

overlap_check_impl compares two impls of the same trait. It first skips identical impls and impls for different traits. For matching trait ids, it tries to prove that the impls cannot both apply. If that fails, it reports the impls as overlapping.

Proving locality

The is_local module determines whether a trait reference could have been defined locally, which is the key predicate for orphan checking:

is_local_trait_ref(_decls: Program, env: Env, assumptions: Wcs, goal: TraitRef,) => Constraints

A parameter is considered local if it is a local type or a fundamental rigid type wrapping a local parameter:

is_local_parameter(_decls: Program, env: Env, assumptions: Wcs, goal: Parameter,) => Constraints

The complement — determining whether a trait reference may come from a remote crate — is used in coherence mode:

may_be_remote(_decls: Program, env: Env, assumptions: Wcs, goal: TraitRef,) => Constraints

Code generation

The codegen module translates the high-level expression grammar into MiniRust basic blocks. Its entry point is codegen_function, which takes a function body (a Block) and produces a lang::Function containing a map of basic blocks, local variables, and an entry point.

CodeBlock: the control-flow builder

The core abstraction is CodeBlock — a single-entry, multi-exit control-flow code block that is incrementally constructed. It is an enum with three variants representing the builder’s state:

/// A single-entry, multi-exit control flow code.
#[derive(Clone, PartialEq, Eq, PartialOrd, Ord, Hash, Debug)]
pub enum CodeBlock {
    /// Anonymous open block being constructed. Has no name yet — a name is
    /// allocated lazily when the block is terminated or needs to be referenced.
    ///
    /// Suppose you have `let x = 22;` this would create a set of statements like
    ///
    /// ```text
    /// stmts: [
    ///   let tmp1;
    ///   tmp1 = 22;
    ///   let x;
    ///   x = tmp;
    /// ]
    /// ```
    ///
    /// and then you have `let y = 33;`
    ///
    /// ```text
    /// stmts: [
    ///   let tmp2;
    ///   tmp2 = 33;
    ///   let y;
    ///   y = tmp2;
    /// ]
    /// ```
    ///
    /// and then you append those two so you get
    ///
    /// ```text
    /// stmts = [... /* as above, concatenated */]
    /// ```
    Block { stmts: Vec<lang::Statement> },

    /// Finalized blocks plus one open fallthrough block.
    ///
    /// For something like this `if foo { 22 } else { 33 }; ...``
    ///
    /// ```text
    /// blocks:
    ///   a {
    ///     if foo goto b else c
    ///   }
    ///   b {
    ///      tmp = 22
    ///      goto d
    ///   }
    ///   c {
    ///     tmp = 33
    ///     goto d
    ///   }
    /// entry: a
    /// fallthrough: d
    /// fallthrough_stmts: [...] // from the `...` above
    /// }}
    /// ```
    Open {
        /// Blocks that have a terminator and thus are "done".
        /// They may branch to each other or to the (incomplete) fallthrough block, as shown above.
        blocks: Map<lang::BbName, lang::BasicBlock>,

        /// The entry block in the list above or the fallthrough.
        entry: lang::BbName,

        /// The name of the not-yet-compelted fallthrough block, which may be referenced above.
        fallthrough: lang::BbName,

        /// The statements in the fallthrough block so far.
        fallthrough_stmts: Vec<lang::Statement>,
    },

    /// Finalized blocks (i.e., blocks with terminators) only. No successors.
    Closed {
        /// Blocks that have a terminator and thus are "done".
        blocks: Map<lang::BbName, lang::BasicBlock>,

        /// The entry block in the list above or the fallthrough.
        entry: lang::BbName,
    },
}

Lifecycle

A code block starts as an anonymous Block (just accumulating statements) and transitions to named states (Open / Closed) once it needs basic-block structure:

flowchart LR
    start(( )) -->|"new()"| Block
    start -->|"named(bb)"| Open
    Block -->|"terminate(_, None)"| Closed
    Block -->|"terminate(_, Some(bb))"| Open
    Closed -->|"terminate(_, Some(bb))"| Open
    Open -->|"terminate(_, None)"| Closed
    Open -->|"terminate(_, Some(bb))"| Open

    Block["
        Block

        Anonymous — just a list of statements with no name yet. A name is allocated lazily when the block is terminated.
    "]

    Closed["
        Closed

        All blocks are finalized. No fallthrough.
    "]
    
    Open["
        Open

        Finalized blocks plus one open fallthrough block (named, accepting statements).
    "]

Block is the starting state for simple expressions — statements accumulate without allocating any basic-block names. Most expressions stay in Block and get inlined into their parent via append. Once a terminator is needed (a call, branch, or explicit control flow), terminate names the block and transitions to Closed or Open.

Open is the state for regions that already have named blocks. Statements accumulate into the named fallthrough block. terminate finalizes the fallthrough and either closes the code block or opens a new fallthrough.

Once a code block is Closed, mutations (with_stmt, terminate) are no-ops. This naturally handles dead code after return or break. However, terminate with Some(next_bb) on a Closed code block will re-open it — this is used for blocks reachable via break that aren’t continuations of the previous terminator.

Core operations

The append operation

append is how sequential composition works. Its behavior depends on whether other is anonymous or named:

The key invariant: once a block is named, it is never destroyed. When appending a named code block (Open or Closed), its entry block is preserved as a jump target — append emits a Goto to it rather than inlining it. This ensures that blocks referenced by jumps (loop headers, break targets) always survive in the final map.

Compound helpers

These methods on CodegenFn combine terminate with block allocation:

Judgments

codegen_block

The top-level block codegen creates a fresh code block, then appends each statement’s code block in sequence:

codegen_block(global: CodegenGlobal, cfn: CodegenFn, scope: CodegenScope, block: Block,) => (CodeBlock, CodegenGlobal, CodegenFn)

codegen_stmt

Each statement produces a CodeBlock that gets appended to the enclosing block’s code block:

codegen_stmt(global: CodegenGlobal, cfn: CodegenFn, scope: CodegenScope, stmt: Stmt,) => (CodeBlock, CodegenScope, CodegenGlobal, CodegenFn)

codegen_expr_into

Expressions are compiled into a target local. Each rule returns a CodeBlock:

codegen_expr_into(global: CodegenGlobal, cfn: CodegenFn, scope: CodegenScope, target: MiniRustLocal, expr: Expr,) => (CodeBlock, CodegenGlobal, CodegenFn)

Walkthrough: literal expression

The simplest case — a literal like 42_u32:

(let code = cfn.fresh_code_block())
---- ("literal")
(codegen_expr_into(global, cfn, scope, target, Literal { value, ty }) => (
    code.assign(target, constant(value, ty)),
    global,
    cfn,
))

1. fresh_code_block() creates a CodeBlock::Block { stmts: [] } (anonymous)
2. .assign(target, constant(42, u32)) pushes one Assign statement → still Block { stmts: [assign] }

The caller appends this single-block code block into its own code block. Since it’s just a Block, append concatenates the statements directly — no basic-block names are allocated.

graph LR
    subgraph "returned CodeBlock (Block)"
        anon["(anonymous): target = const 42_u32"]
    end

Walkthrough: function call

A function call like foo(a, b) is more interesting:

(type_expr(cfn, scope, callee) => callee_ty)
(resolve_rigid(cfn, scope, callee_ty) => RigidTy { name: RigidName::FnDef(fn_id), parameters })
(let (fn_name, global) = global.ensure_fn(MonoKey::new(fn_id, parameters)))
(let (callee_temp, cfn) = cfn.alloc_temp(&callee_ty)?)
(codegen_expr_into(global, cfn, scope, callee_temp, callee) => (code, global, cfn))
(let (temps, cfn) = alloc_temps_for_args(cfn, scope, args)?)
(for_all(i in 0..args.len()) with(code, global, cfn)
    (codegen_expr_into(global, cfn, scope, &temps[i], &args[i]) => (arg_code, global, cfn))
    (let (code, cfn) = cfn.append_from(code, arg_code)))
(let (code, cfn) = cfn.call(code, fn_name, temps, target)?)
---- ("call")
(codegen_expr_into(global, cfn, scope, target, Expr::Call { callee, args }) => (code, global, cfn))

1. Fresh code block starts as Block { stmts: [] }
2. For each argument, codegen_expr_into returns a Block, and append concatenates its statements
3. .call(...) allocates next_bb, terminates with Call { next_block: next_bb } → Open with next_bb as fallthrough

graph LR
    subgraph "returned CodeBlock (Open)"
        bb0["bb0: arg stmts... → Call foo"]
        bb1["bb1: (open, empty)"]
        bb0 --> bb1
    end

The caller can now append more work into bb1.

Walkthrough: if/else

An if b { ... } else { ... } statement:

(let (ct, cfn) = cfn.alloc_local(bool_ty()))
(codegen_expr_into(global, cfn, scope, ct, condition) => (cond_code, global, cfn))
(codegen_block(global, cfn, scope, then_block) => (then_code, global, cfn))
(codegen_block(global, cfn, scope, &else_block.block) => (else_code, global, cfn))
(let (code, cfn) = cfn.branch_on_bool_from(cond_code, ct, then_code, else_code))
---- ("if")
(codegen_stmt(global, cfn, scope, Stmt::If { condition, then_block, else_block }) => (code, scope, global, cfn))

1. Codegen the condition into a temp (cond_region — typically a Block)
2. Codegen both branches independently (each returns its own CodeBlock)
3. branch_on_bool_from terminates cond_region with a Switch, absorbs both branches, and opens a join block

graph TD
    subgraph "returned CodeBlock"
        cond["bb0: eval condition → Switch"]
        then_bb["bb1: then branch"]
        else_bb["bb2: else branch"]
        join["bb3: (open, join point)"]
        cond -->|"true"| then_bb
        cond -->|"false"| else_bb
        then_bb -->|Goto| join
        else_bb -->|Goto| join
    end

If both branches diverge (e.g., both return), there is no join block — the result is Closed.

Walkthrough: loop

A 'label: loop { body }:

(let label = require_label(label)?)
(let (loop_start, cfn) = cfn.fresh_bb())
(let (exit_block, cfn) = cfn.fresh_bb())
(let scope = scope.with_label(&label.id, Some(loop_start), exit_block))
(codegen_block(global, cfn, scope, body) => (body_code, global, cfn))
(let (code, cfn) = build_loop(cfn, loop_start, exit_block, body_code)?)
---- ("loop")
(codegen_stmt(global, cfn, scope, Stmt::Loop { label, body }) => (code, scope, global, cfn))

The build_loop helper constructs:

1. CodeBlock::named(loop_start) — starts in Open state at loop_start
2. Append the body code block (emits Goto from parent fallthrough into loop_start)
3. If body has fallthrough, terminate with Goto(loop_start) back-edge and open exit
4. If body diverges, open exit anyway (reachable via break)

graph TD
    subgraph "returned CodeBlock (Open)"
        loop_start["loop_start: body stmts... → Goto loop_start"]
        exit["exit: (open, fallthrough)"]
        loop_start -->|"back-edge"| loop_start
        loop_start -.->|"break"| exit
    end

A break 'label compiles to terminate(Goto(exit_block)), directing control to the exit.

When this loop code block is appended into the parent, the parent’s fallthrough block gets a Goto to loop_start — since loop_start is a named block, append preserves it as a jump target rather than inlining it.

Putting it all together

The final step is build_function, which:

1. If the body code block still has fallthrough, appends a unit assignment + Return terminator
2. Extracts the entry block name
3. Calls into_blocks() to get the final Map<BbName, BasicBlock>
4. Prepends StorageLive statements to the entry block for all non-argument locals
5. Returns a lang::Function ready for MiniRust interpretation

Coverage report

Judgment fmt at crates/formality-core/src/judgment.rs:24

Signature:

fmt(&self, fmt: &mut std::fmt::Formatter<'_>) -> std::fmt::Result { let mut f = fmt.debug_struct(stringify!($name)); let __JudgmentStruct($($input_name),*) = self; $( f.field(stringify!($debug_input_name), $debug_input_name); )* f.finish() } } $(let $input_name: $input_ty = $crate::Upcast::upcast($input_name);)* // Assertions are preconditions. We shadow each input as a reference // so the assert expression borrows rather than consuming the variables. // // NB: we can't use `$crate` in this expression because of the `respan!` call, // which messes up `$crate` resolution. But we need the respan call for track_caller to properly // assign the span of the panic to the assertion expression and not the invocation of the judgment_fn // macro. Annoying! But our proc macros already reference `formality_core` so that seems ok. { $( #[allow(unused_variables)] let $input_name = &$input_name; )* $( $crate::respan!( $assert_expr ( formality_core::judgment::JudgmentAssertion::assert($assert_expr, stringify!($assert_expr)); ) ); )* } $( // Trivial cases are an (important) optimization that lets // you cut out all the normal rules. if $trivial_expr { let trivial_result = $trivial_result; let (file, line, column) = $crate::respan!( $trivial_expr ((file!(), line!(), column!())) ); let proof_tree = $crate::judgment::ProofTree::with_all( format!("trivial, as {} is true: {trivial_result:?}", stringify!($trivial_expr)), Default::default(), None, file, line, column, Default::default(), ); return $crate::ProvenSet::singleton((trivial_result, proof_tree)); } )* let mut failed_rules = $crate::set![]; let input = __JudgmentStruct($($input_name),*); let output = $crate::fixed_point::fixed_point::< __JudgmentStruct, $crate::Map<$output, $crate::judgment::ProofTree>, >( // Tracing span: |input| { let __JudgmentStruct($($input_name),*) = input; tracing::debug_span!( stringify!($name), $(?$debug_input_name),* ) }, // Stack: { thread_local! { static R: $crate::judgment::JudgmentStack<__JudgmentStruct, $output> = Default::default() } &R }, // Input: input.clone(), // Default value: |_| Default::default(), // Next value: |input: __JudgmentStruct| { let mut output: $crate::Map<$output, $crate::judgment::ProofTree> = $crate::Map::new(); failed_rules.clear(); #[allow(unused)] let input_string = format!("{:?}", input); $crate::push_rules!( $name, &input, output, failed_rules, &input_string, ($($input_name),*) => $output,
                        $(($($rule)*))*
                    );

                    output
                },
            );

            if !output.is_empty()

No rules discovered.

Judgment all_even at crates/formality-core/src/judgment/test_for_all.rs:19

Signature:

all_even(nums: Vec<Num>,) => ()

The number on each rule’s conclusion is positive coverage; the number on each premise is negative coverage. Click a number to browse the tests.

Positive coverage: all_even / all_even

2 tests exercised this rule:

Source location: crates/formality-core/src/judgment/test_for_all.rs:37 (all coverage from this test)

#[test]
fn test_for_all_success() {
    let nums = vec![Num(2), Num(4), Num(6)];
    all_even(nums).assert_ok(expect_test::expect!["{()}"]);
}

Source location: crates/formality-core/src/judgment/test_for_all.rs:51 (all coverage from this test)

#[test]
fn test_for_all_empty() {
    let nums: Vec<Num> = vec![];
    all_even(nums).assert_ok(expect_test::expect!["{()}"]);
}

Judgment sum_all at crates/formality-core/src/judgment/test_for_all.rs:55

Signature:

sum_all(nums: Vec<Num>,) => Num

The number on each rule’s conclusion is positive coverage; the number on each premise is negative coverage. Click a number to browse the tests.

Positive coverage: sum_all / sum

2 tests exercised this rule:

Source location: crates/formality-core/src/judgment/test_for_all.rs:74 (all coverage from this test)

#[test]
fn test_for_all_with_accumulator() {
    let nums = vec![Num(1), Num(2), Num(3)];
    sum_all(nums).assert_ok(expect_test::expect!["{Num(6)}"]);
}

Source location: crates/formality-core/src/judgment/test_for_all.rs:80 (all coverage from this test)

#[test]
fn test_for_all_with_accumulator_empty() {
    let nums: Vec<Num> = vec![];
    sum_all(nums).assert_ok(expect_test::expect!["{Num(0)}"]);
}

Judgment transitive_reachable at crates/formality-core/src/judgment/test_reachable.rs:23

Signature:

transitive_reachable(graph: Arc<Graph>, from: u32,) => u32

The number on each rule’s conclusion is positive coverage; the number on each premise is negative coverage. Click a number to browse the tests.

Positive coverage: transitive_reachable / base

2 tests exercised this rule:

Source location: crates/formality-core/src/judgment/test_filtered.rs:55 (all coverage from this test)

#[test]
fn judgment() {
    let graph = Arc::new(Graph {
        edges: vec![(0, 1), (1, 2), (2, 4), (2, 3), (3, 6), (4, 8), (8, 10)],
    });

    transitive_reachable(&graph, 0).assert_err(expect_test::expect![[r#"
        the rule "base" at (test_filtered.rs) failed because
          condition evaluated to false: `b % 2 == 0`"#]]);

    transitive_reachable(&graph, 2).assert_ok(expect_test::expect!["{4, 8, 10}"]);
}

Source location: crates/formality-core/src/judgment/test_reachable.rs:51 (all coverage from this test)

#[test]
fn judgment() {
    let graph = Arc::new(Graph {
        edges: vec![(0, 1), (1, 2), (2, 0), (2, 3)],
    });

    transitive_reachable(graph, 0).assert_ok(expect_test::expect!["{0, 1, 2, 3}"]);
}

Positive coverage: transitive_reachable / transitive

2 tests exercised this rule:

Source location: crates/formality-core/src/judgment/test_filtered.rs:55 (all coverage from this test)

#[test]
fn judgment() {
    let graph = Arc::new(Graph {
        edges: vec![(0, 1), (1, 2), (2, 4), (2, 3), (3, 6), (4, 8), (8, 10)],
    });

    transitive_reachable(&graph, 0).assert_err(expect_test::expect![[r#"
        the rule "base" at (test_filtered.rs) failed because
          condition evaluated to false: `b % 2 == 0`"#]]);

    transitive_reachable(&graph, 2).assert_ok(expect_test::expect!["{4, 8, 10}"]);
}

Source location: crates/formality-core/src/judgment/test_reachable.rs:51 (all coverage from this test)

#[test]
fn judgment() {
    let graph = Arc::new(Graph {
        edges: vec![(0, 1), (1, 2), (2, 0), (2, 3)],
    });

    transitive_reachable(graph, 0).assert_ok(expect_test::expect!["{0, 1, 2, 3}"]);
}

Judgment is_zero at crates/formality-core/tests/coverage.rs:40

Signature:

is_zero(n: Num) => ()

The number on each rule’s conclusion is positive coverage; the number on each premise is negative coverage. Click a number to browse the tests.

Judgment is_one at crates/formality-core/tests/coverage.rs:52

Signature:

is_one(n: Num) => ()

The number on each rule’s conclusion is positive coverage; the number on each premise is negative coverage. Click a number to browse the tests.

Judgment prove_thing at crates/formality-coverage/tests/scrape.rs:37

Signature:

prove_thing(x: u32) => ()

The number on each rule’s conclusion is positive coverage; the number on each premise is negative coverage. Click a number to browse the tests.

Judgment only_one at crates/formality-coverage/tests/scrape.rs:56

Signature:

only_one(x: u32) => ()

The number on each rule’s conclusion is positive coverage; the number on each premise is negative coverage. Click a number to browse the tests.

Judgment mixed at crates/formality-coverage/tests/scrape.rs:115

Signature:

mixed(x: u32) => ()

The number on each rule’s conclusion is positive coverage; the number on each premise is negative coverage. Click a number to browse the tests.

Judgment move_place at crates/formality-mdbook/src/lib.rs:565

Signature:

move_place(env: Env, live_after: LivePlaces, place: Place, ty: Ty,) => Env

The number on each rule’s conclusion is positive coverage; the number on each premise is negative coverage. Click a number to browse the tests.

Judgment check_adt at crates/formality-rust/src/check/adts.rs:11

Signature:

check_adt(program: Program, adt: Adt,) => ()

The number on each rule’s conclusion is positive coverage; the number on each premise is negative coverage. Click a number to browse the tests.

Positive coverage: check_adt / check adt

63 tests exercised this rule:

Source location: tests/basic_tests.rs:209 (all coverage from this test)

#[test]
fn non_lifetime_binder_in_enum_where_clause_pass() {
    FormalityTest::new(crates![crate core {
        #![feature(non_lifetime_binders)]
        trait A<T> where T: B { }

        trait B { }

        enum E where for<U> u32: A<U> { }

        impl <T> B for T {}
    }])
    .skip_execute()
    .ok()
}

Source location: tests/basic_tests.rs:239 (all coverage from this test)

#[test]
fn non_lifetime_binder_in_struct_where_clause_pass() {
    FormalityTest::new(crates![crate core {
        #![feature(non_lifetime_binders)]
        trait A<T> where T: B { }

        trait B { }

        struct S<T> where for<U> u32: A<U> { }

        impl <T> B for T {}
    }])
    .skip_execute()
    .ok()
}

Source location: tests/basic_tests.rs:426 (all coverage from this test)

Source location: tests/borrowck.rs:128 (all coverage from this test)

fn foo() -> Datum {
    let x: Datum = Datum { value: 0_u32 };
    let y: Datum = x;
    x = Datum { value: 1_u32 };
    let z: Datum = x;
    return z;
}