RefCell: add comments explaining the data layout

theories/typing/unsafe/refcell/ref.v

@@ -11,6 +11,14 @@ Definition refcell_refN := refcellN .@ "ref".
 Section ref.
   Context `{typeG Σ, refcellG Σ}.
 
+  (* The Rust type looks as follows (after some unfolding):
+
+     pub struct Ref<'b, T: ?Sized + 'b> {
+       value: &'b T,
+       borrow: &'b Cell<BorrowFlag>,
+     }
+  *)
+
   Program Definition ref (α : lft) (ty : type) :=
     {| ty_size := 2;
        ty_own tid vl :=

theories/typing/unsafe/refcell/refcell.v

@@ -83,6 +83,13 @@ End refcell_inv.
 Section refcell.
   Context `{typeG Σ, refcellG Σ}.
 
+  (* Original Rust type:
+     pub struct RefCell<T: ?Sized> {
+       borrow: Cell<BorrowFlag>,
+       value: UnsafeCell<T>,
+     }
+  *)
+
   Program Definition refcell (ty : type) :=
     {| ty_size := S ty.(ty_size);
        ty_own tid vl :=

theories/typing/unsafe/refcell/refmut.v

@@ -9,6 +9,16 @@ Set Default Proof Using "Type".
 Section refmut.
   Context `{typeG Σ, refcellG Σ}.
 
+  (* The Rust type looks as follows (after some unfolding):
+
+     pub struct RefMut<'b, T: ?Sized + 'b> {
+       value: &'b mut T,
+       borrow: &'b Cell<BorrowFlag>,
+     }
+
+     In other words, we have a pointer to the data, and a pointer
+     to the refcount field of the RefCell. *)
+
   Program Definition refmut (α : lft) (ty : type) :=
     {| ty_size := 2;
        ty_own tid vl :=

theories/typing/unsafe/refcell/refmut_code.v

@@ -173,7 +173,7 @@ Section refmut_functions.
   Lemma refmut_map_type ty1 ty2 envty E :
     typed_instruction_ty [] [] [] refmut_map
       (fn(∀ β, [☀β] ++ E; refmut β ty1,
-                          fn(∀ α, [☀α] ++ E; envty, &uniq{α}ty1) → &uniq{α}ty2,
+                          fn(∀ α, [☀α] ++ E; envty, &uniq{α} ty1) → &uniq{α} ty2,
                           envty)
        → refmut β ty2).
   Proof.