diff --git a/src/SUMMARY.md b/src/SUMMARY.md
index 981eb22c9..486d2be9c 100644
--- a/src/SUMMARY.md
+++ b/src/SUMMARY.md
@@ -22,5 +22,8 @@
     - [MIR construction](./mir-construction.md)
     - [MIR borrowck](./mir-borrowck.md)
     - [MIR optimizations](./mir-optimizations.md)
+- [Constant evaluation](./const-eval.md)
+    - [miri const evaluator](./miri.md)
+- [Parameter Environments](./param_env.md)
 - [Generating LLVM IR](./trans.md)
 - [Glossary](./glossary.md)
diff --git a/src/const-eval.md b/src/const-eval.md
new file mode 100644
index 000000000..3fb65216a
--- /dev/null
+++ b/src/const-eval.md
@@ -0,0 +1,37 @@
+# Constant Evaluation
+
+Constant evaluation is the process of computing values at compile time. For a
+specific item (constant/static/array length) this happens after the MIR for the
+item is borrow-checked and optimized. In many cases trying to const evaluate an
+item will trigger the computation of its MIR for the first time.
+
+Prominent examples are
+
+* The initializer of a `static`
+* Array length
+    * needs to be known to reserve stack or heap space
+* Enum variant discriminants
+    * needs to be known to prevent two variants from having the same discriminant
+* Patterns
+    * need to be known to check for overlapping patterns
+
+Additionally constant evaluation can be used to reduce the workload or binary
+size at runtime by precomputing complex operations at compiletime and only
+storing the result.
+
+Constant evaluation can be done by calling the `const_eval` query of `TyCtxt`.
+
+The `const_eval` query takes a [`ParamEnv`](./param_env.html) of environment in
+which the constant is evaluated (e.g. the function within which the constant is
+used) and a `GlobalId`. The `GlobalId` is made up of an
+`Instance` referring to a constant or static or of an
+`Instance` of a function and an index into the function's `Promoted` table.
+
+Constant evaluation returns a `Result` with either the error, or the simplest
+representation of the constant. "simplest" meaning if it is representable as an
+integer or fat pointer, it will directly yield the value (via `Value::ByVal` or
+`Value::ByValPair`), instead of referring to the [`miri`](./miri.html) virtual
+memory allocation (via `Value::ByRef`). This means that the `const_eval`
+function cannot be used to create miri-pointers to the evaluated constant or
+static. If you need that, you need to directly work with the functions in
+[src/librustc_mir/interpret/const_eval.rs](https://github.com/rust-lang/rust/blob/master/src/librustc_mir/interpret/const_eval.rs).
diff --git a/src/glossary.md b/src/glossary.md
index a22c49632..34b4bd446 100644
--- a/src/glossary.md
+++ b/src/glossary.md
@@ -18,6 +18,9 @@ generics                |  the set of generic type parameters defined on a type
 ICE                     |  internal compiler error. When the compiler crashes.
 ICH                     |  incremental compilation hash. ICHs are used as fingerprints for things such as HIR and crate metadata, to check if changes have been made. This is useful in incremental compilation to see if part of a crate has changed and should be recompiled.
 infcx                   |  the inference context (see `librustc/infer`)
+MIR                     |  the Mid-level IR that is created after type-checking for use by borrowck and trans ([see more](./mir.html))
+miri                    |  an interpreter for MIR used for constant evaluation ([see more](./miri.html))
+obligation              |  something that must be proven by the trait system ([see more](trait-resolution.html))
 local crate             |  the crate currently being compiled.
 MIR                     |  the Mid-level IR that is created after type-checking for use by borrowck and trans ([see more](./mir.html))
 node-id or NodeId       |  an index identifying a particular node in the AST or HIR; gradually being phased out and replaced with `HirId`.
diff --git a/src/miri.md b/src/miri.md
new file mode 100644
index 000000000..4b0a600be
--- /dev/null
+++ b/src/miri.md
@@ -0,0 +1,142 @@
+# Miri
+
+Miri (**MIR** **I**nterpreter) is a virtual machine for executing MIR without
+compiling to machine code. It is usually invoked via `tcx.const_eval`.
+
+If you start out with a constant
+
+```rust
+const FOO: usize = 1 << 12;
+```
+
+rustc doesn't actually invoke anything until the constant is either used or
+placed into metadata.
+
+Once you have a use-site like
+
+```rust
+type Foo = [u8; FOO - 42];
+```
+
+The compiler needs to figure out the length of the array before being able to
+create items that use the type (locals, constants, function arguments, ...).
+
+To obtain the (in this case empty) parameter environment, one can call
+`let param_env = tcx.param_env(length_def_id);`. The `GlobalId` needed is
+
+```rust
+let gid = GlobalId {
+    promoted: None,
+    instance: Instance::mono(length_def_id),
+};
+```
+
+Invoking `tcx.const_eval(param_env.and(gid))` will now trigger the creation of
+the MIR of the array length expression. The MIR will look something like this:
+
+```mir
+const Foo::{{initializer}}: usize = {
+    let mut _0: usize;                   // return pointer
+    let mut _1: (usize, bool);
+
+    bb0: {
+        _1 = CheckedSub(const Unevaluated(FOO, Slice([])), const 42usize);
+        assert(!(_1.1: bool), "attempt to subtract with overflow") -> bb1;
+    }
+
+    bb1: {
+        _0 = (_1.0: usize);
+        return;
+    }
+}
+```
+
+Before the evaluation, a virtual memory location (in this case essentially a
+`vec![u8; 4]` or `vec![u8; 8]`) is created for storing the evaluation result.
+
+At the start of the evaluation, `_0` and `_1` are
+`Value::ByVal(PrimVal::Undef)`. When the initialization of `_1` is invoked, the
+value of the `FOO` constant is required, and triggers another call to
+`tcx.const_eval`, which will not be shown here. If the evaluation of FOO is
+successful, 42 will be subtracted by its value `4096` and the result stored in
+`_1` as `Value::ByValPair(PrimVal::Bytes(4054), PrimVal::Bytes(0))`. The first
+part of the pair is the computed value, the second part is a bool that's true if
+an overflow happened.
+
+The next statement asserts that said boolean is `0`. In case the assertion
+fails, its error message is used for reporting a compile-time error.
+
+Since it does not fail, `Value::ByVal(PrimVal::Bytes(4054))` is stored in the
+virtual memory was allocated before the evaluation. `_0` always refers to that
+location directly.
+
+After the evaluation is done, the virtual memory allocation is interned into the
+`TyCtxt`. Future evaluations of the same constants will not actually invoke
+miri, but just extract the value from the interned allocation.
+
+The `tcx.const_eval` function has one additional feature: it will not return a
+`ByRef(interned_allocation_id)`, but a `ByVal(computed_value)` if possible. This
+makes using the result much more convenient, as no further queries need to be
+executed in order to get at something as simple as a `usize`.
+
+## Datastructures
+
+Miri's core datastructures can be found in
+[librustc/mir/interpret](https://github.com/rust-lang/rust/blob/master/src/librustc/mir/interpret).
+This is mainly the error enum and the `Value` and `PrimVal` types. A `Value` can
+be either `ByVal` (a single `PrimVal`), `ByValPair` (two `PrimVal`s, usually fat
+pointers or two element tuples) or `ByRef`, which is used for anything else and
+refers to a virtual allocation. These allocations can be accessed via the
+methods on `tcx.interpret_interner`.
+
+If you are expecting a numeric result, you can use `unwrap_u64` (panics on
+anything that can't be representad as a `u64`) or `to_raw_bits` which results
+in an `Option<u128>` yielding the `ByVal` if possible.
+
+## Allocations
+
+A miri allocation is either a byte sequence of the memory or an `Instance` in
+the case of function pointers. Byte sequences can additionally contain
+relocations that mark a group of bytes as a pointer to another allocation. The
+actual bytes at the relocation refer to the offset inside the other allocation.
+
+These allocations exist so that references and raw pointers have something to
+point to. There is no global linear heap in which things are allocated, but each
+allocation (be it for a local variable, a static or a (future) heap allocation)
+gets its own little memory with exactly the required size. So if you have a
+pointer to an allocation for a local variable `a`, there is no possible (no
+matter how unsafe) operation that you can do that would ever change said pointer
+to a pointer to `b`.
+
+## Interpretation
+
+Although the main entry point to constant evaluation is the `tcx.const_eval`
+query, there are additional functions in
+[librustc_mir/interpret/const_eval.rs](https://github.com/rust-lang/rust/blob/master/src/librustc_mir/interpret/const_eval.rs)
+that allow accessing the fields of a `Value` (`ByRef` or otherwise). You should
+never have to access an `Allocation` directly except for translating it to the
+compilation target (at the moment just LLVM).
+
+Miri starts by creating a virtual stack frame for the current constant that is
+being evaluated. There's essentially no difference between a constant and a
+function with no arguments, except that constants do not allow local (named)
+variables at the time of writing this guide.
+
+A stack frame is defined by the `Frame` type in
+[librustc_mir/interpret/eval_context.rs](https://github.com/rust-lang/rust/blob/master/src/librustc_mir/interpret/eval_context.rs)
+and contains all the local
+variables memory (`None` at the start of evaluation). Each frame refers to the
+evaluation of either the root constant or subsequent calls to `const fn`. The
+evaluation of another constant simply calls `tcx.const_eval`, which produces an
+entirely new and independent stack frame.
+
+The frames are just a `Vec<Frame>`, there's no way to actually refer to a
+`Frame`'s memory even if horrible shenigans are done via unsafe code. The only
+memory that can be referred to are `Allocation`s.
+
+Miri now calls the `step` method (in
+[librustc_mir/interpret/step.rs](https://github.com/rust-lang/rust/blob/master/src/librustc_mir/interpret/step.rs)
+) until it either returns an error or has no further statements to execute. Each
+statement will now initialize or modify the locals or the virtual memory
+referred to by a local. This might require evaluating other constants or
+statics, which just recursively invokes `tcx.const_eval`.
diff --git a/src/param_env.md b/src/param_env.md
new file mode 100644
index 000000000..2474886ef
--- /dev/null
+++ b/src/param_env.md
@@ -0,0 +1,30 @@
+# Parameter Environment
+
+When working with associated and/or or generic items (types, constants,
+functions/methods) it is often relevant to have more information about the
+`Self` or generic parameters. Trait bounds and similar information is encoded in
+the `ParamEnv`. Often this is not enough information to obtain things like the
+type's `Layout`, but you can do all kinds of other checks on it (e.g. whether a
+type implements `Copy`) or you can evaluate an associated constant whose value
+does not depend on anything from the parameter environment.
+
+For example if you have a function
+
+```rust
+fn foo<T: Copy>(t: T) {
+}
+```
+
+the parameter environment for that function is `[T: Copy]`. This means any
+evaluation within this function will, when accessing the type `T`, know about
+its `Copy` bound via the parameter environment.
+
+Although you can obtain a valid `ParamEnv` for any item via
+`tcx.param_env(def_id)`, this `ParamEnv` can be too generic for your use case.
+Using the `ParamEnv` from the surrounding context can allow you to evaluate more
+things.
+
+Another great thing about `ParamEnv` is that you can use it to bundle the thing
+depending on generic parameters (e.g. a `Ty`) by calling `param_env.and(ty)`.
+This will produce a `ParamEnvAnd<Ty>`, making clear that you should probably not
+be using the inner value without taking care to also use the `ParamEnv`.
diff --git a/src/trait-resolution.md b/src/trait-resolution.md
index f12ce3b4b..10a5539e4 100644
--- a/src/trait-resolution.md
+++ b/src/trait-resolution.md
@@ -433,7 +433,7 @@ before, and hence the cache lookup would succeed, yielding
 One subtle interaction is that the results of trait lookup will vary
 depending on what where clauses are in scope. Therefore, we actually
 have *two* caches, a local and a global cache. The local cache is
-attached to the `ParamEnv` and the global cache attached to the
+attached to the [`ParamEnv`](./param_env.html) and the global cache attached to the
 `tcx`. We use the local cache whenever the result might depend on the
 where clauses that are in scope. The determination of which cache to
 use is done by the method `pick_candidate_cache` in `select.rs`. At