Some comments in denv.v

theories/vcgen/denv.v

+(** * Reified environments *)
 From iris.proofmode Require Import environments coq_tactics.
 Import env_notations.
 From iris_c.vcgen Require Import dcexpr.
 From iris_c.c_translation Require Import monad.
 From iris.algebra Require Import frac.
 
+(** The reification process is done in two steps. First, we split the
+    main environment into a 'partial environment' (`penv`), that
+    contains propositions of the form `l ↦U v`, and the rest.
+
+    Using this partial environment we construct a set `E` of known
+    locations. Then, using this set we can construct a reified
+    environment (`denv`), where the locations are reified. *)
 Section denv.
   Definition is_dloc (E: known_locs) (dv: dval) : option nat :=
     match dv with
@@ -12,24 +20,30 @@ Section denv.
     end.
   Global Arguments is_dloc _ !_ /.
 
+  (** A 'partial environment': *)
   Record penv_item := PenvItem {
     penv_loc   : cloc;
     penv_level : lvl;
     penv_frac  : frac;
     penv_val   : val
   }.
+  Definition penv := list penv_item.
 
+  (** The reified environment. The `DenvItem` at index `i` in the list
+      denotes the value for the reified location under the index `i`. *)
   Record denv_item := DenvItem {
     denv_level : lvl;
     denv_frac  : frac;
     denv_dval  : dval
   }.
-
-  Definition penv := list penv_item.
   Definition denv := list (option denv_item).
 
+
   Definition penv_to_known_locs : penv → known_locs := fmap penv_loc.
 
+  (** A reified environment is well-formed if every item is well
+      formed and all the indices are contained in the set of known
+      locations. *)
   Fixpoint denv_wf_val (E: known_locs) (m: denv) : bool :=
     match m with
     | [] => true
@@ -44,16 +58,11 @@ Section denv.
     | [], _ => false
     end.
 
-  Lemma denv_wf_len_spec E m :
-    denv_wf_len E m <-> length E >= length m.
-  Proof.
-    revert m. induction E; destruct m; intros; try (simpl; lia).
-    simpl. specialize (IHE m). rewrite IHE. lia.
-  Qed.
-
   Definition denv_wf (E: known_locs) (m: denv) : bool :=
     denv_wf_val E m && denv_wf_len E m.
 
+
+  (** ** Merging of two reified environments *)
   Definition denv_item_opt_merge
       (dio1 dio2 : option denv_item) : option denv_item :=
     match dio1, dio2 with
@@ -74,6 +83,9 @@ Section denv.
   Definition denv_stack_merge (ms : list denv) : denv :=
     foldr denv_merge [] ms.
 
+
+  (** ** Operations on the reified environments.
+      Singleton, insertion, two types of deletion. *)
   Fixpoint denv_singleton (i : nat) (lv : lvl) (q : frac) (dv : dval) : denv :=
     match i with
     | O => [Some (DenvItem lv q dv)]
@@ -95,6 +107,9 @@ Section denv.
       end
     end.
 
+  (** Removing a permission for reading.
+      If `(dLoc i) ↦U{q} v` is present in the environment,
+      then remove half of it and return `(q,v)`. *)
   Fixpoint denv_delete_frac (i : nat) (m : denv) {struct m}
        : option (denv * frac * dval) :=
     match m with
@@ -153,13 +168,26 @@ Section denv.
     ''(m', q, dv) ← denv_delete_full_aux i m;
     Some (q, dv).
 
+  (** Removing a permission for writing.
+      If `(dLoc i) ↦U v` is present in the environment,
+      then remove it and return `v`. *)
   Definition denv_delete_full (i : nat) (m : denv) : option (denv * dval) :=
     ''(m', q, dv) ← denv_delete_full_aux i m;
     guard (q = 1)%Qp;
     Some (m', dv).
 
-  Definition denv_unlock (m: denv) : denv :=
-    map (λ dio, ''(DenvItem _ q dv) ← dio; Some (DenvItem ULvl q dv)) m.
+  (** Versions of `denv_delete_frac` and `denv_delete_full` for stacks
+  of environments. *)
+  Definition denv_delete_frac_2 (i : nat) (ms : list denv) (m : denv)
+       : option (list denv * denv * frac * dval) :=
+    match denv_delete_frac_stack i ms with
+    | Some (ms', q, dv) => Some (ms', m, q, dv)
+    | None =>
+      match denv_delete_frac i m with
+      | Some (m', q, dv) => Some (ms, m', q, dv)
+      | None => None
+      end
+    end.
 
   Definition denv_delete_full_2 (i : nat) (ms : list denv) (m : denv)
        : option (list denv * denv * dval) :=
@@ -171,35 +199,42 @@ Section denv.
     | _, _ => None
     end.
 
-  Definition denv_delete_frac_2 (i : nat) (ms : list denv) (m : denv)
-       : option (list denv * denv * frac * dval) :=
-    match denv_delete_frac_stack i ms with
-    | Some (ms', q, dv) => Some (ms', m, q, dv)
-    | None =>
-      match denv_delete_frac i m with
-      | Some (m', q, dv) => Some (ms, m', q, dv)
-      | None => None
-      end
-    end.
+  (** Turn all `(dLoc i) ↦L v` into `(dLoc i) ↦U v`. *)
+  Definition denv_unlock (m: denv) : denv :=
+    map (λ dio, ''(DenvItem _ q dv) ← dio; Some (DenvItem ULvl q dv)) m.
 End denv.
 
+(* Some basic properties and lemmas required further *)
 Lemma is_dloc_Some E dv i : is_dloc E dv = Some i → dv = dLocV (dLoc i 0).
 Proof. by destruct dv as [| |[? []|]|]; intros; simplify_eq /=. Qed.
 
 Lemma denv_merge_nil_r m : denv_merge m [] = m.
 Proof. induction m; simpl; eauto. Qed.
 
+Lemma denv_wf_len_spec E m :
+  denv_wf_len E m <-> length E >= length m.
+Proof.
+  revert m. induction E; destruct m; intros; try (simpl; lia).
+  simpl. specialize (IHE m). rewrite IHE. lia.
+Qed.
+
 Section denv_spec.
   Context `{amonadG Σ}.
 
   (** ** Interpretations *)
-  Definition denv_interp (L : known_locs) (m : denv) : iProp Σ :=
+  (** Interpreting a reified environment and a stack of environments *)
+  Definition denv_interp (E : known_locs) (m : denv) : iProp Σ :=
     ([∗ list] i ↦ dio ∈ m,
         from_option (λ '(DenvItem lv q dv),
-          dloc_interp L (dLoc i 0) ↦C[lv]{q} dval_interp L dv) True dio)%I.
-                           (*   ↑ FIX THAT *)
+          dloc_interp E (dLoc i 0) ↦C[lv]{q} dval_interp E dv) True dio)%I.
+                           (* RK: ↑ FIX THAT *)
+
+  (* DF: TODO: change the order of the arguments here *)
 
-  Fixpoint denv_stack_interp (ms1 ms2 : list denv) E (P : iProp Σ) :=
+  (** `denv_stack_interp ms1 ms2 E P`
+      ~ `(ms1.n -∗ ms2.n ∗ (.... ∗ (ms1.1 -∗ ms2.1 ∗ P)))`
+   *)
+  Fixpoint denv_stack_interp (ms1 ms2 : list denv) (E : known_locs) (P : iProp Σ) :=
     match ms1,ms2 with
     | m::ms,m'::ms' =>
       denv_stack_interp ms ms' E (denv_interp E m -∗ denv_interp E m' ∗ P)
@@ -207,16 +242,18 @@ Section denv_spec.
     | _, _ => False
     end%I.
 
+  (** Interpretation of partial environments, needed for `splitenv.v`. *)
   Definition penv_interp (m : penv) : iProp Σ :=
     ([∗ list] p ∈ m, penv_loc p ↦C[penv_level p]{penv_frac p} penv_val p)%I.
 
-  (** Auxiliary interpretation function *)
-  Definition denv_interp_aux (L : known_locs) (m : denv) (k : nat) : iProp Σ :=
+  (** Auxiliary interpretation function.
+      This is only used for doing proofs by induction. *)
+  Definition denv_interp_aux (E : known_locs) (m : denv) (k : nat) : iProp Σ :=
     ([∗ list] i ↦ dio ∈ m,
      from_option (λ '(DenvItem lv q dv),
-       dloc_interp L (dLoc (k+i) 0) ↦C[lv]{q} dval_interp L dv) True dio)%I.
+       dloc_interp E (dLoc (k+i) 0) ↦C[lv]{q} dval_interp E dv) True dio)%I.
 
-  (** ** Helper lemmas *)
+  (** *** Helper lemmas *)
   Lemma denv_interp_aux_0 L m :
     denv_interp_aux L m 0 ≡ denv_interp L m.
   Proof. reflexivity. Qed.