Skip to content

Latest commit

 

History

History
123 lines (92 loc) · 5.8 KB

2022-05-27-mir-formality-roadmap.md

File metadata and controls

123 lines (92 loc) · 5.8 KB
Raw

Formality roadmap

Zulip discussion link: https://rust-lang.zulipchat.com/#narrow/stream/326132-t-types.2Fmeetings/topic/2022-05-27/near/284128865

Goals

  • Complete model of safe Rust including all static checks + operational semantics
  • Able to run against portions of standard Rust test suite to compare behavior

Current status of MIR formality

  • Subtyping algorithm modeled
  • Solver is "explore all routes", does not match recursive structure in chalk
  • Many gaps along the way:
    • ... (fill in)

Big picture tasks and layers

  • Checking a MIR program: The mir layer drives the process of checking that a program meets all of Rust rules. This relies on...
    • OK goals: the decl layer creates an "ok goal" for the various Rust declarations
    • Type checker: The mir layer
  • Solving goals: The logic layer is tasked with taking a goal and returning a answer scheme. This relies on...
    • Defining what is true: The decl layer is tasked with converting Rust declarations into clauses
    • Built-in Rust rules: The ty layer implements various built-in relations like subtyping

Spikes

The plan is to drive this development through spikes, meaning example tests that we can use to work out what parts of the sytem need to be implemented. nikomatsakis intends to have enough implemented by next Wednesday's formality meeting that folks can start filling in.

Spikes and why they were chosen:

Test driver

Filed under rust-lang/a-mir-formality#42

We should create a test harness / rustc driver formalityc that works as follows:

  • It parses an input rust crate and compiles it to MIR
  • It generates MIR formality files from the MIR and some portion of the interfaces of other crates
  • It writes those files to a test file and then invokes racket to run MIR formality against them
    • It reads some sort of special comments (e.g., // compile-fail) to determine what behavior is expected.

This can be used to extend our test suite with Rust test files rather than hand-coding things in Racket.

Eventually I expect the racket code to go away and be replaced with either Rust code or (my current preference) some Rust interpreter of our definition.

Implementation in rustc

Another angle is ongoing work to align the formality model with rustc implementations:

  • subtyping work

Discussion: Implementation in chalk

Another angle is ongoing work to align the formality model with chalk implementations:

  • Formality does not model the chalk recursive trait solver
  • Chalk needs to adopt Formality's overall goal structure
  • Chalk needs to adopt Formality's subtyping and type-relating goals
  • Chalk needs to adopt Formality's approach to associated types

Conclusion from discussion: probably we just want to restart chalk from scratch.

Discussion: Overview of rustc static checks

Key:

  • ❌ never expect to model this
  • ⌛ would like to model this, but not right now
  • ➖ not covered by the spikes above
  • ✔️ this is part of our first goal
Phase Modeled? How?
Parsing ❌
Macro expansion ⌛
Name resolution ⌛
Lifetime elision rules ⌛
Associated type trait selection ⌛ e.g. T::Item becoming <T as Iterator>::Item
Variance inference ⌛ we will take variance as "input" to the declarations
Coherence overlap / orphan ✔️ The decl layer's OK check
HIR type checker's WF checks ✔️ The decl layer's OK check
Dyn safety rules ➖
Impl matches trait? ✔️ Decl layer's OK check
Const promotion ⌛ decided by MIR building in rustc
HIR type checking of fn bodies ⌛ we take MIR as input
Method resolution ⌛ decided by HIR type checker, embedded in MIR
Closure capture inference ⌛ decided by HIR type checker, embedded in MIR
Closure mode (fn, fnmut) and signature inference ⌛ decided by HIR type checker, embedded in MIR
Coercion insertion ⌛ decided by HIR type checker, embedded in MIR
Drop/StorageDead placement ⌛ decided by MIR building in rustc
Patterns/exhaustiveness ⌛ decided by MIR building in rustc
Unsafe checking ➖ Part of "type checking" on MIR
MIR type check ✔️ mir layer generates goals
Borrow checking ✔️ mir layer polonius-style check
Rust subtyping ✔️ modeled by the ty layer and also decl
Operational semantics ⌛ basically what miri does
Transmute rules ⌛
Layout ⌛ input to operational semantics for now

Discussion: Const generics

Discussion around whether we want to model const generics and what would be required to do so.

Conclusion was that we needed deeper discussion, but some felt modeling const generics could be useful for resolving some of the questions around newer features; this would broaden scope to include

Questions for discussion

  • What about coherence rules?
  • What is needed to align chalk and formality?
  • Should we include operational semantics and -- if so -- how does that fit in?
    • conclusion from meeting seemed to be to keep it out of scope to start
  • What are all the static checks rustc does, and which are covered by the spikes above?
    • see table
  • Const generics?