Draft of initial RMC documentation (rust-lang#471)

* Draft of initial RMC documentation

* revisions in response to feedback

Author: tedinski

rmc-docs/book.toml

@@ -11,5 +11,4 @@ multilingual = false
 [output.html]
 site-url = "/rmc/"
 git-repository-url = "https://github.com/model-checking/rmc"
-# If we get a stable default branch, we can use this feature, but HEAD doesn't work
-#edit-url-template = "https://github.com/model-checking/rmc/edit/HEAD/rmc-docs/{path}"
+edit-url-template = "https://github.com/model-checking/rmc/edit/main/rmc-docs/{path}"

rmc-docs/src/SUMMARY.md

@@ -1,12 +1,12 @@
 # The Rust Model Checker
 
 - [Getting started with RMC](./getting-started.md)
-  - [Installation]()
-  - [Comparison with other tools]()
+  - [Installation](./install-guide.md)
+  - [Comparison with other tools](./tool-comparison.md)
   - [RMC on a single file]()
   - [RMC on a crate]()
   - [Debugging failures]()
 
-- [RMC tutorial]()
+- [RMC tutorial](./rmc-tutorial.md)
 
 - [RMC developer documentation]()

rmc-docs/src/getting-started.md

@@ -1,9 +1,18 @@
 # Getting started with RMC
 
-Hello, World!
+RMC is a Rust verification tool based on _model checking_.
+With RMC, you can ensure that broad classes of problems are absent from your Rust code by writing _proof harnesses_, which are broadly similar to tests (especially property tests.)
+RMC is especially useful for verifying unsafe code in Rust, where many of the language's usual guarantees can no longer be checked by the compiler.
+But RMC is also useful for finding panics in safe Rust, and it can check user-defined assertions.
 
-```rust
-fn main() {
-    assert!(1 == 1);
-}
-```
+## Project Status
+
+RMC is currently in the initial development phase, and has not yet made an official release.
+It is under active development, but it does not yet support all Rust language features.
+If you encounter issues when using RMC we encourage you to [report them to us](https://github.com/model-checking/rmc/issues/new/choose).
+
+## Getting started
+
+1. [Begin with the RMC installation guide.](./install-guide.md) Currently, this means checking out and building RMC.
+2. [Understand how RMC compares to other potential tools for verifying Rust code.](./tool-comparison.md)
+3. [Try following the RMC tutorial to get a feel for how RMC can be applied.](./rmc-tutorial.md)

rmc-docs/src/install-guide.md

@@ -0,0 +1,108 @@
+# RMC Installation Guide
+
+RMC must currently be built from source.
+
+In general, the following dependencies are required:
+
+1. The dependencies needed to built `rustc`. RMC is a fork of the Rust compiler, and so we have the same minimum requirements.
+2. [CBMC](https://github.com/diffblue/cbmc) (>= 5.30.1)
+3. [CBMC Viewer](https://github.com/awslabs/aws-viewer-for-cbmc) (>= 2.6)
+
+## Installing on Ubuntu 20.04
+
+The simplest way to install (especially if you're using a fresh VM) is following our CI scripts:
+
+```
+# git clone [email protected]:model-checking/rmc.git
+git clone https://github.com/model-checking/rmc.git
+cd rmc
+git submodule update --init
+./scripts/setup/ubuntu-20.04/install_deps.sh
+./scripts/setup/ubuntu-20.04/install_cbmc.sh
+./scripts/setup/install_viewer.sh 2.6
+./scripts/setup/install_rustup.sh
+```
+
+## Installing on Mac OS
+
+You need to have [Homebrew](https://brew.sh/) installed already.
+
+```
+# git clone [email protected]:model-checking/rmc.git
+git clone https://github.com/model-checking/rmc.git
+cd rmc
+git submodule update --init
+./scripts/setup/macos-10.15/install_deps.sh
+./scripts/setup/macos-10.15/install_cbmc.sh
+./scripts/setup/install_viewer.sh 2.6
+./scripts/setup/install_rustup.sh
+```
+
+## Building and testing RMC
+
+Perform one-time build configuration:
+
+```
+./configure \
+    --enable-debug \
+    --set=llvm.download-ci-llvm=true \
+    --set=rust.debug-assertions-std=false \
+    --set=rust.deny-warnings=false
+```
+
+**NOTE: If you skip the above (`llvm.download-ci-llvm=true` specifically), builds may take a long time as all of LLVM would need to be built from scratch.**
+
+Then build RMC:
+
+```
+./x.py build -i --stage 1 library/std
+```
+
+Then, optionally, run the regression tests:
+
+```
+./scripts/rmc-regression.sh
+```
+
+This script has a lot of noisy output, but on a successful run you will see:
+
+```
+All RMC regression tests completed successfully.
+```
+
+## Try running RMC
+
+Get the RMC script in your path:
+
+```bash
+export PATH=$(pwd)/scripts:$PATH
+```
+
+Create a test file:
+
+```rust
+// File: test.rs
+fn main() {
+    assert!(1 == 2);
+}
+```
+
+Run RMC on the single file:
+
+```
+rmc test.rs
+```
+
+You should get a result like this one:
+
+```
+[snipped output]
+** Results:
+test.rs function main
+[main.assertion.1] line 2 assertion failed: 1 == 2: FAILURE
+
+** 1 of 1 failed (2 iterations)
+VERIFICATION FAILED
+```
+
+Fix the test and you should see `rmc` succeed.

rmc-docs/src/rmc-tutorial.md

@@ -0,0 +1,21 @@
+# RMC tutorial
+
+If you're interested in applying RMC, then you're probably in this situation:
+
+1. You're working on a moderately important project in Rust.
+2. You've already invested heavily in testing to ensure correctness, and possibly fuzzing to ensure the absence of shallow security issues.
+3. You want to invest further, to gain a much higher degree of assurance.
+
+> If you haven't already, we recommend techniques like property testing (e.g. with [`proptest`](https://github.com/AltSysrq/proptest)) before attempting model checking.
+> These yield good results, are very cheap to apply, and are often easier to adopt and debug.
+> Refactoring work to make your code more property-testable will generally also make the code more model-checkable as well.
+> RMC is a next step: a tool that can be applied once cheaper tactics are no longer yielding results, or once the easier to detect issues have already been dealt with.
+
+This tutorial will step you through a progression from simple to moderately complex tasks with RMC.
+It's meant to ensure you can get started, and see at least some simple examples of how typical proofs are structured.
+It will also teach you the basics of "debugging" proof harnesses, which mainly consists of diagnosing and resolving non-termination issues with the solver.
+
+1. [Begin with RMC installation.](./install-guide.md) This will take through to running `rmc` on your first Rust program.
+2. Consider reading our [tool comparison](./tool-comparison.md) to understand what RMC is.
+3. Coming soon: the tutorial.
+4. Consider returning to the [tool comparison](./tool-comparison.md) after trying the tutorial to see if any of the abstract ideas have become more concrete.

rmc-docs/src/tool-comparison.md

@@ -0,0 +1,22 @@
+# Comparison with other tools
+
+**Fuzzing** (for example, with [`cargo-fuzz`](https://github.com/rust-fuzz/cargo-fuzz)) is a unguided approach to random testing.
+A fuzzer generally provides an input of random bytes, and then examines fairly generic properties ("doesn't crash or commit undefined behavior") about the behavior of the resulting program.
+Fuzzers generally get their power through a kind of evolutionary algorithm that rewards new mutant inputs that "discover" new branches of the program under test.
+Fuzzers are excellent for testing security boundaries, precisely because they make no validity assumptions (hence "unguided") when generating the input.
+
+**Property testing** (for example, with [`proptest`](https://github.com/AltSysrq/proptest)) is a guided approach to random testing.
+"Guided" in the sense that the test generally provides a strategy (for generating random values) that constrains their range.
+The purpose of this is to either focus on interesting values, or because the assertions in the test will only hold for a constrained set of inputs.
+This generator is sampled several times, and the test's assertions are checked for each sample.
+Tests in this style do actually state properties: "forall inputs (of some constrained kind), this condition should hold."
+Property testing is often quite effective, but the engine can't fully prove the property, it can only sample randomly a few of those values to test (though property testing libraries frequently give interesting "edge cases" higher probability, making them more effective at bug-finding).
+
+**Model checking** is similar to these techniques in how you use them, but model checking is non-random and exhaustive (though often only up to some bound on input or problem size).
+Thus, properties checked with a model checker are effectively proofs.
+Instead of naively trying all possible _concrete_ inputs (which could be infeasible and blow up exponentially), model checkers like RMC will cleverly encode program traces as _symbolic_ "[SAT](https://en.wikipedia.org/wiki/Boolean_satisfiability_problem)/[SMT](https://en.wikipedia.org/wiki/Satisfiability_modulo_theories)" problems, and hand them off to SAT/SMT solvers.
+Again, SAT/SMT solving is an [NP-complete](https://en.wikipedia.org/wiki/NP-completeness) problem, but most practical programs can be model checked within milliseconds to seconds (with notable exceptions: you can easily try to reverse a cryptographic hash with a model checker, but good luck getting it to terminate!)
+
+Model checking allows you to prove non-trivial properties about programs, and check those proofs in roughly the same amount of time as a traditional test suite would take to run.
+The downside is many types of properties can quickly become "too large" to practically model check, and so writing "proof harnesses" (very similar to property tests and fuzzer harnesses) requires some skill to understand why the solver is not terminating and fix the structure of the problem you're giving it so that it does.
+This process basically boils down to "debugging" the proof.

scripts/rmc-regression.sh

@@ -40,3 +40,7 @@ $SCRIPT_DIR/codegen-firecracker.sh
 #        \           / v0.1.1
 #         dependency2
 ./src/test/rmc-dependency-test/diamond-dependency/run-dependency-test.sh
+
+echo
+echo "All RMC regression tests completed successfully."
+echo