update README

README.md

@@ -163,6 +163,30 @@ lifetime logic is in [lifetime_sig.v](theories/lifetime/lifetime_sig.v).
 | LftL-fract-shorten         | frac_borrow.v        | frac_bor_shorten      |
 | LftL-fract-iff             | frac_borrow.v        | frac_bor_iff          |
 
+### Verification of Full Arc
+We do not have the **Core Arc** example (Section 3.3 of the RBrlx paper) in Coq.
+Instead, we have the **Full Arc** example (Section 5.3 of the RBrlx paper, also
+Section 6 of its technical appendix).
+
+The verification of Full Arc is split into 2 parts:
+
+1. Verifying Full Arc with respect to some abstract specification. This is done
+  in [lang/arc.v](theories/lang/arc.v), with the help of a CMRA (PCM) defined in
+  [lang/arc_cmra.v](theories/lang/arc_cmra.v).
+  The specification is proven in the `*_spec` lemmas.
+  More comments can be found in the aforementioned files.
+2. Verifying that the abstract specification implies the semantics
+  interpretation of the type of Arc and Weak. This can be found in
+  [typing/lib/arc.v](theories/typing/lib/arc.v).
+  In this file,
+    * the `Program Definition arc (ty : type)` and `Program Definition
+      weak (ty : type)` are the interpretations of the `Arc<ty>` and `Weak<ty>`
+      types, respectively.
+    * `arc_send`, `arc_sync`, `weak_send`, `weak_sync` prove that both `Arc<ty>`
+      and `Weak<ty>` correctly implement the `Send` and `Sync` traits.
+    * The `*_type` lemmas prove that each function semantically satisfies its
+      syntactic type.
+
 ## For Developers: How to update the GPFSL dependency
 
 * Do the change in [GPFSL], push it.