Fix README

README.md

@@ -46,13 +46,13 @@ CPU cores.
   * The subfolder [model](theories/lifetime/model) proves the core rules, which
     are then sealed behind a module signature in
     [lifetime.v](theories/lifetime/lifetime.v).
-* The folder [logic](theories/logic) proves the surface-level rules of [GPFSL].
-  These rules are the combined version of [GPFSL]'s raw rules with the lifetime
-  logic or the view-dependent invariants.
+* The folder [logic](theories/logic) proves the surface-level rules of [GPFSL]
+  *atomic-borrows-based* protocols. These rules combine [GPFSL]'s raw rules with
+  the lifetime logic rules for atomic borrows.
 * The folder [typing](theories/typing) defines the domain of semantic types,
   interpretations of all the judgments, as well as proofs of all typing rules.
   * [type.v](theories/typing/type.v) contains the definition of a semantic type.
-  * [programs.v](theories/typing/programs.v) defines the typing judgements for
+  * [programs.v](theories/typing/programs.v) defines the typing judgments for
     instructions and function bodies.
   * [soundness.v](theories/typing/soundness.v) contains the main soundness
     theorem of the type system.