Fix compass readme to support review

README-COMPASS.md

 # Compass Coq Development
 
-# Build
+# Getting Started
+
+To evaluate this artifact, which is a Coq development of mechnanized proofs, the
+reviewer can
+1. use the provided prebuilt VM, or
+2. build the proofs with the help of `opam` to deal with dependencies, or
+3. build the proofs after manually installing the dependencies.
+
+## Use the VM
+The VM has been tested to run on VirtualBox 6.?.?, with ?? GB RAM, and takes ??
+GB of memory. The username/password is `???/???`.
+
+The VM comes with Coq 8.13.2, and dependencies for Compass pre-installed.
+The editors CoqIDE and vscode (with vscoq) are also pre-installed.
+The Compass development is in `???`.
+
+The proofs have also been pre-built. To rebuild the proofs, please use
+
+    $ make clean && make -jN
+
+where `N` is the number of cores to use.
 
 ## Build with opam
 Opam version ≥ 2 is required.
@@ -8,11 +28,11 @@ Please see the install instructions at [opam homepage](https://opam.ocaml.org/do
 For example, in ubuntu 20.04, the following command installs opam and system
 dependencies.
 
-    sudo apt install opam libgmp-dev
+    $ sudo apt install opam libgmp-dev
 
 After installing opam, please run the following command to initialize opam.
 
-    opam init
+    $ opam init
 
 (The above command may fail if you run it in an unprivileged container.
 In that case, please run `opam init --disable-sandboxing`.)
@@ -20,28 +40,44 @@ In that case, please run `opam init --disable-sandboxing`.)
 Once opam is set up, please run the following command to install the
 dependencies and build the Compass Coq development.
 
-    ./build.sh
+    $ ./build.sh
 
 ## Build manually
 The following dependencies are needed:
-- Coq 8.13.2
+- Coq 8.13.2 or above
 - Development versions of [Iris] and [ORC11], see [coq-gpfsl.opam](coq-gpfsl.opam)
   for the exact versions.
 
 With the dependencies installed, run the following command to build the Compass
 Coq development, where `N` is the number of cores to use.
 
-    make -jN
+    $ make -jN
+
+# Step-by-Step Instructions
+
+In the following, we point out the contributions of this artifact, which support
+all claims in the paper.
+1. the extensions to the original [iRC11] logic made by our Compass framework
+2. the Compass framework and our specifications for various data structures
+3. the verifications of libraries and clients
 
-# Structure
+The reviewer can check that there is no admit in the proofs, and that the
+statements do not have spurious assumptions, and that they follow the statements
+given in the paper closely.
+For each component, we mark the corresponding sections and figures from the paper.
 
 ## Extensions to iRC11
+
 The Compass framework is built on top of the [iRC11] separation logic, which is
 sound for the [ORC11] memory model, an operational variant of [RC11] that has
 non-atomic, release-acquire, and relaxed accesses, and fences, and forbids
 *load buffering* behaviors, i.e. po ∪ rf is acyclic.
 
 Our verifications depend on the following new additions to [iRC11].
+These were not discussed at all in the submitted draft, due to space restriction.
+We will extend the paper in the camera-ready version to include more explanation
+about them.
+
 * The *view at* modality `@{V} P` ([`base_logic/vprop.v`](theories/base_logic/vprop.v))
   makes explicit the view of an assertion `P` in the logic.
   This logical construct is already available in [iRC11] and is similar to
@@ -49,21 +85,33 @@ Our verifications depend on the following new additions to [iRC11].
 * General *objective invariants* ([`logic/invariants.v`](theories/logic/invariants.v))
   allow arbitrary objective resources to be shared.
   Objective resources include unsynchronized ghost state and view-at assertions
-  `@{V} P`. General invariants lift the *single-location* restriction of [iRC11]'s invariants, and thus can be used to compose multiple data structures,
-  something that is useful for logical atomicity.
+  `@{V} P`. General invariants lift the *single-location* restriction of
+  [iRC11]'s GPS protocols, and thus can be used to compose ownership of multiple
+  locations and multiple data structures. This allows combining general
+  invariants with logical atomicity in almost the same way as in a SC logic.
+  The only difference is the extra side condition of objective resources
 * *Atomic points-to* ([`logic/atomic_ops.v`](theories/logic/atomic_ops.v))
   expose the middle-level rules, between the base logic's histories and
   the surface logic's [iRC11] protocols, for handling atomic locations directly
   with histories and views, but more abstractly than in the base logic.
+  The rules for atomic operations (atomic reads, writes, or CASes) only the
+  atomic points-to of the accessed location only under a view-at modality.
+  Therefore, atomic points-to can be easily put inside general invariants.
 
   | Paper     | Coq definition                |
   |-----------|-------------------------------|
   | Rel-Write | `AtomicSWriter_release_write` |
   | Acq-Read  | `AtomicSeen_acquire_read`     |
 
-* Logical atomic triples (LATs): [`logic/logatom.v`](theories/logic/logatom.v).
+* Logical atomic triples (LATs) [`logic/logatom.v`](theories/logic/logatom.v)
+  are directly reused from Iris, without change, in the same way as Cosmo.
+  This is because Iris support for LATs (through the concept *atomic updates*)
+  is quite general, and the relaxed memory effects can be handled orthogonally
+  through the use of the view-at modality and general invariants.
+  The proofs in [`logic/logatom.v`](theories/logic/logatom.v) simply show that
+  LATs imply iRC11 Hoare triples, as a sanity check.
 
-## Compass Framework
+## Compass Framework (§3)
 * [`event/`](theories/examples/event)
   * [`event.v`](theories/examples/event/event.v): the event type, and
     the physical interpretation of logical view (`seen_logview`).
@@ -93,7 +141,7 @@ Our verifications depend on the following new additions to [iRC11].
 
 ## Library Specifications and Proofs
 
-### [Queue](theories/examples/queue)
+### [Queue](theories/examples/queue) (§3.1-§3.2)
 * implementations
   * [`code_ms.v`](theories/examples/queue/code_ms.v): Michael-Scott queue.
   * [`code_hw.v`](theories/examples/queue/code_hw.v): Herlihy-Wing queue.
@@ -163,7 +211,7 @@ Our verifications depend on the following new additions to [iRC11].
     spec. (§3.2)
 
 
-### [Stack](theories/examples/stack)
+### [Stack](theories/examples/stack) (§3.3-§4.1)
 * implementations
   * [`code_treiber.v`](theories/examples/stack/code_treiber.v): Treiber stack
   * [`code_elim.v`](theories/examples/stack/code_elim.v): elimination stack that
@@ -207,10 +255,10 @@ Our verifications depend on the following new additions to [iRC11].
   * [`proof_treiber_graph.v`](theories/examples/stack/proof_treiber_graph.v):
     Treiber stack satisfies LAT<sub>hb</sub> spec.
   * [`proof_treiber_history.v`](theories/examples/stack/proof_treiber_history.v):
-    Treiber stack satisfies LAT<sup>hist</sup><sub>hb</sub> spec.
+    Treiber stack satisfies LAT<sup>hist</sup><sub>hb</sub> spec (§3.3).
   * [`proof_elim_graph.v`](theories/examples/stack/proof_elim_graph.v):
     Elimination stack satisfies LAT<sub>hb</sub> (assuming LAT<sub>hb</sub>
-    specs of stack and exchanger).
+    specs of stack and exchanger) (§4.1).
 * relations of specs
   * [`proof_history_abs.v`](theories/examples/stack/proof_history_abs.v):
     LAT<sup>hist</sup><sub>hb</sub> spec implies LAT<sup>abs</sup><sub>so</sub> spec.
@@ -222,7 +270,7 @@ Our verifications depend on the following new additions to [iRC11].
     The same client as above, but using LAT<sup>hist</sup><sub>hb</sub>.
 
 
-### [Exchanger](theories/examples/exchanger)
+### [Exchanger](theories/examples/exchanger) (§4.2)
 * implementation
   * [`code.v`](theories/examples/exchanger/code.v): A simple elimination-based exchanger
 * specs