An Overview of Chalk

Chalk is under heavy development, so if any of these links are broken or if any of the information is inconsistent with the code or outdated, please open an issue so we can fix it. If you are able to fix the issue yourself, we would love your contribution!

Chalk recasts Rust's trait system explicitly in terms of logic programming by "lowering" Rust code into a kind of logic program we can then execute queries against. (See Lowering to Logic and Lowering Rules) Its goal is to be an executable, highly readable specification of the Rust trait system.

There are many expected benefits from this work. It will consolidate our existing, somewhat ad-hoc implementation into something far more principled and expressive, which should behave better in corner cases, and be much easier to extend.

Chalk Structure

Chalk has two main "products". The first of these is the chalk_engine crate, which defines the core SLG solver. This is the part rustc uses.

The rest of chalk can be considered an elaborate testing harness. Chalk is capable of parsing Rust-like "programs", lowering them to logic, and performing queries on them.

Here's a sample session in the chalk repl, chalki. After feeding it our program, we perform some queries on it.

?- program
Enter a program; press Ctrl-D when finished
| struct Foo { }
| struct Bar { }
| struct Vec<T> { }
| trait Clone { }
| impl<T> Clone for Vec<T> where T: Clone { }
| impl Clone for Foo { }

?- Vec<Foo>: Clone
Unique; substitution [], lifetime constraints []

?- Vec<Bar>: Clone
No possible solution.

?- exists<T> { Vec<T>: Clone }
Ambiguous; no inference guidance

You can see more examples of programs and queries in the unit tests.

Next we'll go through each stage required to produce the output above.

Parsing (chalk_parse)

Chalk is designed to be incorporated with the Rust compiler, so the syntax and concepts it deals with heavily borrow from Rust. It is convenient for the sake of testing to be able to run chalk on its own, so chalk includes a parser for a Rust-like syntax. This syntax is orthogonal to the Rust AST and grammar. It is not intended to look exactly like it or support the exact same syntax.

The parser takes that syntax and produces an Abstract Syntax Tree (AST). You can find the complete definition of the AST in the source code.

The syntax contains things from Rust that we know and love, for example: traits, impls, and struct definitions. Parsing is often the first "phase" of transformation that a program goes through in order to become a format that chalk can understand.

Rust Intermediate Representation (chalk_rust_ir)

After getting the AST we convert it to a more convenient intermediate representation called chalk_rust_ir. This is sort of analogous to the HIR in Rust. The process of converting to IR is called lowering.

The chalk::program::Program struct contains some "rust things" but indexed and accessible in a different way. For example, if you have a type like Foo<Bar>, we would represent Foo as a string in the AST but in chalk::program::Program, we use numeric indices (ItemId).

The IR source code contains the complete definition.

Chalk Intermediate Representation (chalk_ir)

Once we have Rust IR it is time to convert it to "program clauses". A ProgramClause is essentially one of the following:

A clause of the form consequence :- conditions where :- is read as "if" and conditions = cond1 && cond2 && ...
A universally quantified clause of the form forall<T> { consequence :- conditions }
- forall<T> { ... } is used to represent universal quantification. See the section on Lowering to logic for more information.
- A key thing to note about forall is that we don't allow you to "quantify" over traits, only types and regions (lifetimes). That is, you can't make a rule like forall<Trait> { u32: Trait } which would say "u32 implements all traits". You can however say forall<T> { T: Trait } meaning "Trait is implemented by all types".
- forall<T> { ... } is represented in the code using the Binders<T> struct.

See also: Goals and Clauses

This is where we encode the rules of the trait system into logic. For example, if we have the following Rust:

impl<T: Clone> Clone for Vec<T> {}

We generate the following program clause:

forall<T> { (Vec<T>: Clone) :- (T: Clone) }

This rule dictates that Vec<T>: Clone is only satisfied if T: Clone is also satisfied (i.e. "provable").

Similar to chalk::program::Program which has "rust-like things", chalk_ir defines ProgramEnvironment which is "pure logic". The main field in that struct is program_clauses, which contains the ProgramClauses generated by the rules module.

Rules (chalk_solve)

The chalk_solve crate (source code) defines the logic rules we use for each item in the Rust IR. It works by iterating over every trait, impl, etc. and emitting the rules that come from each one.

See also: Lowering Rules

Well-formedness checks

As part of lowering to logic, we also do some "well formedness" checks. See the chalk_solve::wf source code for where those are done.

See also: Well-formedness checking

Coherence

The method CoherenceSolver::specialization_priorities in the coherence module (source code) checks "coherence", which means that it ensures that two impls of the same trait for the same type cannot exist.

Solver (chalk_solve)

Finally, when we've collected all the program clauses we care about, we want to perform queries on it. The component that finds the answer to these queries is called the solver.

See also: The SLG Solver

Crates

Chalk's functionality is broken up into the following crates:

chalk_engine: Defines the core SLG solver.
chalk_rust_ir, containing the "HIR-like" form of the AST
chalk_ir: Defines chalk's internal representation of types, lifetimes, and goals.
chalk_solve: Combines chalk_ir and chalk_engine, effectively, which implements logic rules converting chalk_rust_ir to chalk_ir
- Defines the coherence module, which implements coherence rules
- chalk_engine::context provides the necessary hooks.
chalk_parse: Defines the raw AST and a parser.
chalk: Brings everything together. Defines the following modules:
- chalk::lowering, which converts AST to chalk_rust_ir
- Also includes chalki, chalk's REPL.

Browse source code on GitHub

Testing

chalk has a test framework for lowering programs to logic, checking the lowered logic, and performing queries on it. This is how we test the implementation of chalk itself, and the viability of the lowering rules.

The main kind of tests in chalk are goal tests. They contain a program, which is expected to lower to logic successfully, and a set of queries (goals) along with the expected output. Here's an example. Since chalk's output can be quite long, goal tests support specifying only a prefix of the output.

Lowering tests check the stages that occur before we can issue queries to the solver: the lowering to chalk_rust_ir, and the well-formedness checks that occur after that.

Rustc 开发指南