---
# System prepended metadata

title: Stable-MIR Meetings

---

# Stable-MIR Meetings

## 2022-05-24: development

### Goals

* aligned on problem that we solving (15min)

* aligned on development plan

### Problem we are solving

* draft/skeletal charter: https://hackmd.io/DE2nBWNeRreyGfhPFoIG6w

* potentially distinct phases

    * pre- and post-drop elaboration.
    * instead of having pre and post drop-elab MIR, have a single MIR that represents both, by injecting boolean flags (so drop elaboration becomes just something that figures out constant booleans where there were runtime booleans before).

* user stories are good. Could add more
* there is tension between desire for low-level information about implementation details versus high-level information about the big-picture relationships in the program itself.
    * should figure out what parts of each of those we want in an MVP (minimum viable product)
* which tool(s) should be part of the initial users for MVP
    * MIRI is one choice
    * it would be good to have at least one high-level alternative tool
    * prusti? creusot?
    * prusti need to run post elaborated-drops, but also needs borrow-checking (one obvious answer would be to adopt the `drop-if` operations suggested by niko)
    * creusot doesn't need drop-elaboration or borrow-checker information; just need to know that the borrow-checker has run.
        * but it does need all the type-substitutions and DefId's in the MIR
        * so SMIR would need to be very transparent in its wrapping around MIR to acquire the secondary information that creusot needs.
        * this is a worry to Xavier: To get the benefits of SMIR, need to isolate the compiler APIs, but hard to get there without re-implementing the entire compiler
        * starting transparent is an approach; we'll talk about that more as part of dev-plan discussion.
* two initial customers, one high-level and one low-level
    * MIRI operates on a very late MIR with most everything it needs encoded in the MIR itself.
    * Kani is similar; e.g. has to replicate transmute's behavior.
    * creusot and prusti both need a significant amount of the compiler API

# Dev Plan Discussion

* start transparent, slow migration to increasing opaque is fast path to iteration.

* Xavier made [sketch tool-lib](https://github.com/xldenis/tool-lib/blob/b39e76a452b4bac9aaee9d0f4736581b1a56e97b/src/lib.rs)
  * this served for creusot
  * but note two things:
      1. uses of `::*`
      2. comments of form "// TODO: Remove", which represent modules that still need specific lists of items elaborated.

* would be good to do same exercise for MIRI.

* Session: used by creusot to report error messages
    * but used by other tools, e.g. Kani, for backend stuff

* HIR (?): used by creusot because that's where DefId's are defined
    * and the HirMap is used to do some lookups
    * HirVisitor used to check for certain patterns to improve creusot's error diagnostics.
    * Prusti uses HIR visitor to collect specification closures.

* attributes are used by many tools

* rustc offers various utilities, and it would be *nice* to factor them out into things that are shareable, but we need to take care not to distract ourselves from main goal

* Ghost MIR initiative
    * would be nice to embed loop invariants/contracts into the MIR, so that tools can see these user-injected things

* general pattern we expect: take something like rustc_middle::ty, and migrate it to point at chalk-ty instead.
    * repeat that across other large dependencies within the compiler
    * but note that until the opaque layer actually provides *everything* that tools need, tools will need to fall back on DefId's and lookups against the original compiler internals

* metadata
    * (felix missed this)
    * whatever was said, Oli ended with "that's a no brainer, just open an MCP with compiler-team"

* (de)coupling
    * make a new driver? Run the compiler as a service?
    * celina: thinking that we can serialize the data, either to the file or to a socket
    * xavier: until there's a fully opaque barrier, not much advantage of running two separate processes
        * TyContext exposes every single query
    * xavier: imagined a blessed library distributed through rustup that exposes a selected set of curated APIs
    * xavier: running on stable is not our near-term objective (Vytautas agrees)


* architecture:
    * (Celina) a server sits in between server, ingests MIR and exposes SMIR to users
        * (Xavier) how to handle secondary apis? 
    * (Vytautas): Prusti dream: RustAnalyzer/Salsa style architecture. (Xavier agrees)

* Miri migration:
    * All work would happen in the compiler by migrating MIR interpreter to depend on SMIR.
    * Expose a stand-alone `const-eval` crate which doesn't depend on `tcx` 
    * 
* needs: 
    * trait resolution
    * MIRI needs access to all MIR, including all dependencies
