# 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