Update README.md

README.md

@@ -26,9 +26,11 @@ and then `make` in [coq/ra](coq/ra).
 
 ### Structure
 
-* The language is in `lang.v`. The operational semantics is in `machine.v`.
+* The operational semantics is in `machine.v`. The language is in `lang.v`.
 * The base logic is in the `base` folder. The model is in `base/ghosts.v`.
+  Each base rule is proven in a separate file.
 * iRSL's main rules are in `rsl_instances.v`. The model is in `rsl.v`.
 * Non-atomic rules are in `na.v`.
 * iGPS's rules are in the `gps` folder. The model is in `gps/shared.v`
-* Examples are in the `examples` folder.
\ No newline at end of file
+* Examples are in the `examples` folder.
+* `tests/message_passing.v` contains a closed proof of MP without Iris statements.
\ No newline at end of file