---
title: "a-mir-formality"
tags: T-types, 2023-meetup-BRU, minutes
date: 2023-10-10
url: https://hackmd.io/A37wKGqoQ0OmyT8x5tROCA
---

# a-mir-formality

Plan: nikomatsakis to prepare covering core design ideas, expected scope over time, a roadmap for 2023/2024, what work is needed and in particular which parts require novelty and may diverge from rustc, and which are porting over same concepts.

## Expected outcomes

* Greater familiarity with the design of a-mir-formality
* Agreement on scope and roadmap
* Plan for how to make it less of a nikomatsakis pet project

## Background

### Core design ideas and goals

The idea is for a-mir-formality to serve as a specification of sorts for Rust. Rules are given in a very high-level fashion. Rules are executable, but clarity and correctness is top priority; completeness is second priority, and efficiency tertiary. a-mir-formality isn't expected to scale beyond simple tests, but that would include much of the compiler test suite. The hope is that a-mir-formality can cover the "ideal model" that we have in our heads, the one that the compiler is the full-fledged implementation of.

What can we use it for?

* Modeling things before stabilization and testing them against small examples
* Fuzzing and looking to see whether desired behaviors and properties are upheld
* Comparing against the real compiler
* The real compiler is much more optimized and much more complicated. Is that truly equivalent to the simpler version we are aiming for?
* We can also assess 'high-level optimizations' and behavior

This is version 3 of a-mir-formality. Version 1 was written in PLT Redex. Version 2 was a Rust rewrite, but nikomatsakis didn't like the style of it. It felt too much like the compiler. Version 3 is a much more high-level rewrite that feels much better.

### How complete can we get?

The hope is that we can model **ALL** of Rust eventually -- well, almost. Much like miri covers all of mir, and yet only gets so precise when it comes to unsafe code, there is no intention to model all the intricacies of specific platform details. For example, it would never cover the contents of an inline assembly block. But it should cover the complete picture when it comes to the type checker, trait checker, borrow checker, and the like.

The project was named a-mir-formality because the pun was too good to give up (for those who don't get the pun (like oli): "a mere formality"). And for now, it only aims to cover the MIR type system, which means it doesn't include the HIR type checker and all the interesting details about implicit coercions, autoref, method dispatch, and the like. It also excludes the Rust grammar. I do consider that stuff to be a possible future extension, or perhaps a related project, but for now it seems like it would just make the project impossible. There's plenty to cover just looking at MIR and the borrow checker.

### Roadmap and scope

Key:

* :x: never expect to model this
* :crystal_ball: some day, sure, but it would require extending to new parts of the compiler
* :hourglass: could do this in current framework, but not in the initial feature set
* :heavy_check_mark: in scope
* :heavy_minus_sign: *what does this mean?*

| Phase | Modeled? | How? |
| --- | --- | --- |
| Parsing | :crystal_ball:
| Macro expansion | :crystal_ball:
| Name resolution | :crystal_ball:
| Lifetime elision rules | :crystal_ball:
| Associated type trait selection | :crystal_ball: | e.g. `T::Item` becoming `<T as Iterator>::Item`
| Variance inference | :hourglass: | we will take variance as "input" to the declarations for now, but this seems not too hard |
| Coherence overlap / orphan | :heavy_check_mark: | The decl layer's OK check |
| HIR type checker's WF checks | :heavy_check_mark: | The decl layer's OK check |
| Dyn safety rules | :hourglass: |
| Impl matches trait? | :heavy_check_mark: | Decl layer's OK check|
| Const promotion | :hourglass: | decided by MIR building in rustc
| HIR type checking of fn bodies | :crystal_ball: | we take MIR as input |
| Method resolution | :crystal_ball: | decided by HIR type checker, embedded in MIR |
| Closure capture inference | :crystal_ball: | decided by HIR type checker, embedded in MIR |
| Closure mode (fn, fnmut) and signature inference | :crystal_ball: | decided by HIR type checker, embedded in MIR |
| Coercion insertion | :crystal_ball: | decided by HIR type checker, embedded in MIR |
| Drop/StorageDead placement | :crystal_ball: | decided by MIR building in rustc |
| Patterns/exhaustiveness | :crystal_ball: | decided by MIR building in rustc |
| Unsafe checking | :heavy_minus_sign: | Part of "type checking" on MIR |
| MIR type check | :heavy_check_mark: | mir layer generates goals
| Borrow checking | :heavy_check_mark: | mir layer polonius-style check |
| Rust subtyping | :heavy_check_mark: | modeled by the ty layer and also decl |
| Operational semantics | :x: | leave that to [MiniRust], but maybe we can bridge them |
| Transmute rules | :crystal_ball: | sure, why not?
| Layout | :crystal_ball: | we would do some subset, and we may have to, if it gets reflected in trait system |

[MiniRust]: https://github.com/RalfJung/minirust

## The 'formality' system

This section covers the core formality system, independent from Rust semantics (note that, at present, this is not cleanly divided from the Rust-specific stuff; I'd like to do that, so that I could use it for other modeling projects, but there's a little work required).

### The `term` macro

There are two or three key things to understand. The first is the [`#[term]`][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...

[term]: https://github.com/rust-lang/a-mir-formality/blob/bca36ecd069d6bdff77bffbb628ae3b2ef4f8ef7/crates/formality-macros/src/term.rs#L14-L36

* 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:

#[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. This also accepts some internal annotations:

* `#[cast]` can be applied on an enum variant with a single argument. It says that we should generate upcast/downcast impls to allow conversion. In this case, between a `Variable` and an `Expr`. This would 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`.
* `#[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

#[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

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`:

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

### Judgment functions

The next thing is the `judgement_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.

[`prove_wc`]: https://github.com/rust-lang/a-mir-formality/blob/bca36ecd069d6bdff77bffbb628ae3b2ef4f8ef7/crates/formality-prove/src/prove/prove_wc.rs#L21-L125

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:

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:

pub fn has_type(arg0: impl Upcast<Env>, arg1: impl Upcast<Expr>) -> Set<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 `Set`. 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. 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):

pub fn has_type(arg0: impl Upcast<Env>, arg1: impl Upcast<Expr>) -> Set<Type> {
    let arg0: Env = arg0.upcast();
    let arg1: Expr = arg1.upcast();
    
    let mut results = set![]; // we define this macro

    if /* inference rule 1 matches */ {
        results.push(/* result from inference rule 1 */);
    }
    
    if /* inference rule 2 matches */ {
        results.push(/* result from inference rule 1 */);
    }
    
    // ... 
    
    if /* inference rule N matches */ {
        results.push(/* result from inference rule N */);
    }
    
    results
}

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:

(
    (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...

// 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...

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:

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...

// 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`].

[`prove_wc`]: https://github.com/rust-lang/a-mir-formality/blob/bca36ecd069d6bdff77bffbb628ae3b2ef4f8ef7/crates/formality-prove/src/prove/prove_wc.rs#L21-L125

### 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.

## Modeling Rust

We model Rust as follows. First, there are two layers:

* The "Rust" layer takes as input something more-or-less resembling Rust surface syntax (modulo function bodies, which are MIR).
* The "desugared layer" defines types / where-clauses / declarations in a more primitive form.

### Rust layer

The rust layer is defined in the `formality-rust` crate. Here is the root type for a `Program`, which is a list of crates:

#[term($crates)]
pub struct Program {
    /// List of all crates.
    /// The last crate in the list is the current crate.
    pub crates: Vec<Crate>,
}

Each crate has a unique name and a list of items:

#[term(crate $id { $*items })]
pub struct Crate {
    pub id: CrateId,
    pub items: Vec<CrateItem>,
}

A crate item can be something like:

#[term]
pub enum CrateItem {
    #[cast]
    Struct(Struct),
    #[cast]
    Enum(Enum),
    #[cast]
    Trait(Trait),
    #[cast]
    TraitImpl(TraitImpl),
    #[cast]
    NegTraitImpl(NegTraitImpl),
    #[cast]
    Fn(Fn),
}

### Desugared layer

This gets "desugared" into a [set of "declarations"](https://github.com/rust-lang/a-mir-formality/blob/bca36ecd069d6bdff77bffbb628ae3b2ef4f8ef7/crates/formality-prove/src/decls.rs#L12-L24)

#[term]
pub struct Decls {
    pub max_size: usize,

    /// Each trait in the program
    pub trait_decls: Vec<TraitDecl>,
    pub impl_decls: Vec<ImplDecl>,
    pub neg_impl_decls: Vec<NegImplDecl>,
    pub alias_eq_decls: Vec<AliasEqDecl>,
    pub alias_bound_decls: Vec<AliasBoundDecl>,
    pub local_trait_ids: Set<TraitId>,
    pub local_adt_ids: Set<AdtId>,
}

A given piece of Rust syntax expands into multiple declarations. For example, a trait includes a [`TraitDecl`](https://github.com/rust-lang/a-mir-formality/blob/bca36ecd069d6bdff77bffbb628ae3b2ef4f8ef7/crates/formality-prove/src/decls.rs#L133-L144):

/// A "trait declaration" declares a trait that exists, its generics, and its where-clauses.
/// It doesn't capture the trait items, which will be transformed into other sorts of rules.
///
/// In Rust syntax, it covers the `trait Foo: Bar` part of the declaration, but not what appears in the `{...}`.
#[term(trait $id $binder)]
pub struct TraitDecl {
    /// The name of the trait
    pub id: TraitId,

    /// The binder here captures the generics of the trait; it always begins with a `Self` type.
    pub binder: Binder<TraitDeclBoundData>,
}

/// The "bound data" for a [`TraitDecl`][] -- i.e., what is covered by the forall.
#[term(where $where_clause)]
pub struct TraitDeclBoundData {
    /// The where-clauses declared on the trait
    pub where_clause: Wcs,
}

which defines the "header" of the trait, like its name, its generics (encapsulated in the `Binders`), and the where-clauses. It doesn't define the *members* of the trait, those would be defined elsewhere.

## Where-clauses

The [`Wc`](https://github.com/rust-lang/a-mir-formality/blob/main/crates/formality-types/src/grammar/wc.rs#L116-L119) struct defines *where-clauses*, or predicates:

#[term($data)]
pub struct Wc {
    data: Arc<WcData>,
}

it just contains a [`WcData`](https://github.com/rust-lang/a-mir-formality/blob/main/crates/formality-types/src/grammar/wc.rs#L131-L141):

#[term]
pub enum WcData {
    #[cast]
    PR(PR),

    #[grammar(for $v0)]
    ForAll(Binder<Wc>),

    #[grammar(if $v0 $v1)]
    Implies(Wcs, Wc),
}

/// "PR" == Predicate or Relation
///
/// We need a better name for this lol.
#[term]
pub enum PR {
    #[cast]
    Predicate(Predicate),
    #[cast]
    Relation(Relation),
}

/// Atomic predicates are the base goals we can try to prove; the rules for proving them
/// are derived (at least in part) based on the Rust source declarations.
#[term]
pub enum Predicate {
    /// True if a trait is fully implemented (along with all its where clauses).
    #[cast]
    IsImplemented(TraitRef),

    #[grammar(!$v0)]
    NotImplemented(TraitRef),

    #[grammar(@WellFormedTraitRef($v0))]
    WellFormedTraitRef(TraitRef),

    #[grammar(@IsLocal($v0))]
    IsLocal(TraitRef),

    #[grammar(@ConstHasType($v0, $v1))]
    ConstHasType(Const, Ty),
}

/// Relations are built-in goals which are implemented in custom Rust logic.
#[term]
pub enum Relation {
    #[grammar($v0 = $v1)]
    Equals(Parameter, Parameter),

    #[grammar($v0 <: $v1)]
    Sub(Parameter, Parameter),

    #[grammar($v0 : $v1)]
    Outlives(Parameter, Parameter),

    #[grammar(@wf($v0))]
    WellFormed(Parameter),
}

## The complete check

## The proves relation

To prove where-clauses

/// Top-level entry point for proving things; other rules recurse to this one.
pub fn prove(
    decls: impl Upcast<Decls>,
    env: impl Upcast<Env>,
    assumptions: impl Upcast<Wcs>,
    goal: impl Upcast<Wcs>,
) -> Set<Constraints> {

https://github.com/rust-lang/a-mir-formality/blob/bca36ecd069d6bdff77bffbb628ae3b2ef4f8ef7/crates/formality-prove/src/prove.rs#L23-L29

* How we do type unification
* How we check for all
* Michael's question

## Key questions for discussion

### Roadmap and initial spikes

### How to encourage contribution

## Notes from the meetup itself