Rename Monotone into Directed

README.md

@@ -254,8 +254,7 @@ In the `overlay` folder:
 
 # Differences with the paper
 
-Some definitions have different names from the paper. In particular, _directed
-capabilities_ are called _monotone capabilities_ in the Coq development.
+Some definitions have different names from the paper.  
 
 *name in paper => name in mechanization*
 

theories/binary_model/examples_binary/confidentiality_adequacy.v

@@ -38,7 +38,7 @@ Class memory_layout `{MachineParameters} := {
 Definition initial_state_stk `{MachineParameters} (b_stk e_stk: Addr) (stack_init : list Word) (c: machine_component): cfg cap_lang :=
   match c with
   | Lib _ _ _ _ pre_comp => ([Seq (Instr Executable)], (∅, ∅)) (* dummy value *)
-  | Main _ _ _ _ (ms, _, _) c_main => ([Seq (Instr Executable)], (<[r_stk := inr (URWLX, Monotone, b_stk, e_stk, b_stk)]> (<[PC := c_main]> (gset_to_gmap (inl 0%Z) (list_to_set all_registers))), (ms : Mem) ∪ (mkregion b_stk e_stk stack_init)))
+  | Main _ _ _ _ (ms, _, _) c_main => ([Seq (Instr Executable)], (<[r_stk := inr (URWLX, Directed, b_stk, e_stk, b_stk)]> (<[PC := c_main]> (gset_to_gmap (inl 0%Z) (list_to_set all_registers))), (ms : Mem) ∪ (mkregion b_stk e_stk stack_init)))
   end.
 
 Definition comp1 `{memory_layout} : machine_component :=

theories/binary_model/examples_binary/push_pop_binary.v

@@ -31,7 +31,7 @@ Section macros.
 
   Lemma pushU_z_spec E a1 a2 w z p g b e stk_b stk_e stk_a stk_a' :
     isCorrectPC (inr ((p,g),b,e,a1)) →
-    withinBounds ((URWLX,Monotone),stk_b,stk_e,stk_a) = true →
+    withinBounds ((URWLX,Directed),stk_b,stk_e,stk_a) = true →
     (a1 + 1)%a = Some a2 →
     (stk_a + 1)%a = Some stk_a' →
     nclose specN ⊆ E →
@@ -40,11 +40,11 @@ Section macros.
     ∗ ⤇ Seq (Instr Executable)
     ∗ ▷ pushU_z_s a1 r_stk z
     ∗ ▷ PC ↣ᵣ inr ((p,g),b,e,a1)
-    ∗ ▷ r_stk ↣ᵣ inr ((URWLX,Monotone),stk_b,stk_e,stk_a)
+    ∗ ▷ r_stk ↣ᵣ inr ((URWLX,Directed),stk_b,stk_e,stk_a)
     ∗ ▷ stk_a ↣ₐ w
     ={E}=∗ ⤇ Seq (Instr Executable)
          ∗ PC ↣ᵣ inr ((p,g),b,e,a2) ∗ pushU_z_s a1 r_stk z ∗
-         r_stk ↣ᵣ inr ((URWLX,Monotone),stk_b,stk_e,stk_a') ∗ stk_a ↣ₐ inl z.
+         r_stk ↣ᵣ inr ((URWLX,Directed),stk_b,stk_e,stk_a') ∗ stk_a ↣ₐ inl z.
   Proof.
     iIntros (Hvpc1 Hwb Hsuc Hstk Hnclose)
             "(#Hspec & Hj & Ha1 & HPC & Hr_stk & Hstk_a')".

theories/binary_model/ftlr_binary/AddSubLt_binary.v

@@ -38,7 +38,7 @@ Section fundamental.
   Lemma add_sub_lt_case (W : WORLD) (r : prodO (leibnizO Reg) (leibnizO Reg)) (p : Perm)
         (g : Locality) (b e a : Addr) (w : Word) (ρ : region_type) (dst : RegName) (r1 r2: Z + RegName) (P:D):
     (∀ w : Word, <[PC:=w]> r.1 = <[PC:=w]> r.2)
-    → p = RX ∨ p = RWX ∨ (p = RWLX /\ g = Monotone)
+    → p = RX ∨ p = RWX ∨ (p = RWLX /\ g = Directed)
     → (∀ x : RegName, is_Some (r.1 !! x) ∧ is_Some (r.2 !! x))
     → isCorrectPC (inr (p, g, b, e, a))
     → (b <= a)%a ∧ (a < e)%a
@@ -60,7 +60,7 @@ Section fundamental.
                        -∗ sts_full_world a0
                           -∗ na_own logrel_nais ⊤
                              -∗ ⤇ Seq (Instr Executable)
-                                -∗ ⌜a2 = RX ∨ a2 = RWX ∨ a2 = RWLX ∧ a3 = Monotone⌝
+                                -∗ ⌜a2 = RX ∨ a2 = RWX ∨ a2 = RWLX ∧ a3 = Directed⌝
                                    → □ region_conditions a0 a2 a3 a4 a5 -∗ interp_conf a0)
     -∗ region_conditions W p g b e
     -∗ (∀ r1 : RegName, ⌜r1 ≠ PC⌝ → fixpoint interp1 W (r.1 !r! r1, r.2 !r! r1))

theories/binary_model/ftlr_binary/Load_binary.v

@@ -382,7 +382,7 @@ Section fundamental.
         - destruct o as [HRX | [HRWX | HRWLX] ]; auto.
           subst; simplify_map_eq.
           iDestruct (writeLocalAllowed_implies_local _ RWLX with "[HLVInterp]") as "%"; auto.
-          destruct x0; unfold isMonotone in *. all: inversion H4.
+          destruct x0; unfold isDirected in *. all: inversion H4.
           iPureIntro; do 2 right; auto.
         - simplify_map_eq. iPureIntro. naive_solver.
       }

theories/binary_model/ftlr_binary/Restrict_binary.v

@@ -113,7 +113,7 @@ Section fundamental.
         rewrite H5 in H3. iDestruct (region_close with "[$Hstate $Hr $Ha $Ha' $Hmono Hw]") as "Hr"; eauto.
         { destruct ρ;auto;[|specialize (Hnotmonostatic g)|specialize (Hnotuninitialized p)];contradiction. }
         destruct (PermFlowsTo RX p'') eqn:Hpft.
-        { assert (Hpg: p'' = RX ∨ p'' = RWX ∨ p'' = RWLX ∧ g'' = Monotone).
+        { assert (Hpg: p'' = RX ∨ p'' = RWX ∨ p'' = RWLX ∧ g'' = Directed).
           { destruct p''; simpl in Hpft; eauto; try discriminate.
             destruct (andb_true_eq _ _ ltac:(naive_solver)).
             simpl in H3, H4. destruct p0; simpl in H3; try discriminate.

theories/binary_model/ftlr_binary/StoreU_binary.v

@@ -207,7 +207,7 @@ Section fundamental.
   Qed.
 
   Lemma execcPC_implies_interp W p g b e a0 :
-    p = RX ∨ p = RWX ∨ p = RWLX ∧ g = Monotone →
+    p = RX ∨ p = RWX ∨ p = RWLX ∧ g = Directed →
     region_conditions W p g b e  -∗
       ((fixpoint interp1) W) (inr (p, g, b, e, a0),inr (p,g,b,e,a0)).
   Proof.

theories/binary_model/ftlr_binary/Store_binary.v

@@ -25,7 +25,7 @@ Section fundamental.
   Implicit Types interp : (D).
 
   Lemma execcPC_implies_interp W p g b e a0:
-    p = RX ∨ p = RWX ∨ p = RWLX ∧ g = Monotone →
+    p = RX ∨ p = RWX ∨ p = RWLX ∧ g = Directed →
     region_conditions W p g b e -∗ ((fixpoint interp1) W) (inr (p, g, b, e, a0),inr (p, g, b, e, a0)).
   Proof.
     iIntros (Hp) "#HR".

theories/binary_model/ftlr_binary/ftlr_base_binary.v

@@ -23,7 +23,7 @@ Section fundamental.
   Definition ftlr_instr (W : WORLD) (r : prodO (leibnizO Reg) (leibnizO Reg)) (p : Perm)
              (g : Locality) (b e a : Addr) (w1 : Word) (i: instr) (ρ : region_type) (P : D) :=
     (∀ w : Word, <[PC:=w]> r.1 = <[PC:=w]> r.2)
-    → p = RX ∨ p = RWX ∨ (p = RWLX /\ g = Monotone)
+    → p = RX ∨ p = RWX ∨ (p = RWLX /\ g = Directed)
     → (∀ x : RegName, is_Some (r.1 !! x) ∧ is_Some (r.2 !! x))
     → isCorrectPC (inr (p, g, b, e, a))
     → (b <= a)%a ∧ (a < e)%a
@@ -43,7 +43,7 @@ Section fundamental.
                        -∗ sts_full_world a0
                           -∗ na_own logrel_nais ⊤
                              -∗ ⤇ Seq (Instr Executable)
-                                -∗ ⌜a2 = RX ∨ a2 = RWX ∨ a2 = RWLX ∧ a3 = Monotone⌝
+                                -∗ ⌜a2 = RX ∨ a2 = RWX ∨ a2 = RWLX ∧ a3 = Directed⌝
                                    → □ region_conditions a0 a2 a3 a4 a5 -∗ interp_conf a0)
     -∗ region_conditions W p g b e
     -∗ (∀ r1 : RegName, ⌜r1 ≠ PC⌝ → fixpoint interp1 W (r.1 !r! r1, r.2 !r! r1))

theories/binary_model/ftlr_binary/interp_weakening_binary.v

@@ -31,14 +31,14 @@ Section fundamental.
                        -∗ sts_full_world a0
                           -∗ na_own logrel_nais ⊤
                              -∗ ⤇ Seq (Instr Executable)
-                                -∗ ⌜a2 = RX ∨ a2 = RWX ∨ a2 = RWLX ∧ a3 = Monotone⌝
+                                -∗ ⌜a2 = RX ∨ a2 = RWX ∨ a2 = RWLX ∧ a3 = Directed⌝
                                    → □ region_conditions a0 a2 a3 a4 a5 -∗ interp_conf a0))%I.
 
   (* TODO: Move in monotone ? *)
   Lemma region_state_nwl_future W W' l l' p a a':
     (a < a')%a →
     LocalityFlowsTo l' l ->
-    (if pwlU p then l = Monotone else True) ->
+    (if pwlU p then l = Directed else True) ->
     (@future_world Σ l' a' W W') -∗
     ⌜if pwlU p then region_state_pwl_mono W a else region_state_nwl W a l⌝ -∗
     ⌜region_state_nwl W' a l'⌝.
@@ -73,7 +73,7 @@ Section fundamental.
     (a < a')%a →
     PermFlowsTo p' p ->
     LocalityFlowsTo l' l ->
-    (if pwlU p then l = Monotone else True) ->
+    (if pwlU p then l = Directed else True) ->
     (@future_world Σ l' a' W W') -∗
     ⌜if pwlU p then region_state_pwl_mono W a else region_state_nwl W a l⌝ -∗
     ⌜if pwlU p' then region_state_pwl_mono W' a else region_state_nwl W' a l'⌝.
@@ -235,7 +235,7 @@ Section fundamental.
               case_eq (pwlU p'); intros.
               * assert (pwlU p = true) as HP by (destruct p, p'; naive_solver).
                 rewrite HP in H1. iPureIntro. auto.
-              * iApply (region_state_nwl_future W W Global Monotone _ _ (min a' e')); eauto.
+              * iApply (region_state_nwl_future W W Global Directed _ _ (min a' e')); eauto.
                 assert (x ∈ region_addrs b' (min a' e')) as [_ Hin]%elem_of_region_addrs;
                   [apply elem_of_list_lookup;eauto|];auto.
                 destruct (pwlU p);inversion H0;auto.
@@ -274,7 +274,7 @@ Section fundamental.
               case_eq (pwlU p'); intros.
               * assert (pwlU p = true) as HP by (destruct p, p'; naive_solver).
                 rewrite HP in H1. iPureIntro. auto.
-              * iApply (region_state_nwl_future W W Local Monotone _ _ (min a' e')); eauto.
+              * iApply (region_state_nwl_future W W Local Directed _ _ (min a' e')); eauto.
                 assert (x ∈ region_addrs b' (min a' e')) as [_ Hin]%elem_of_region_addrs;
                   [apply elem_of_list_lookup;eauto|];auto.
                 destruct (pwlU p);inversion H0;auto.
@@ -295,7 +295,7 @@ Section fundamental.
               case_eq (pwlU p'); intros.
               * assert (pwlU p = true) as HP by (destruct p, p'; naive_solver).
                 rewrite HP in H1. iPureIntro. auto.
-              * iApply (region_state_nwl_future W W Monotone Monotone _ _ (min a' e')); eauto.
+              * iApply (region_state_nwl_future W W Directed Directed _ _ (min a' e')); eauto.
                 assert (x ∈ region_addrs b' (min a' e')) as [_ Hin]%elem_of_region_addrs;
                   [apply elem_of_list_lookup;eauto|];auto.
                 destruct (pwlU p);inversion H0;auto.
@@ -353,7 +353,7 @@ Section fundamental.
               case_eq (pwlU p'); intros.
               * assert (pwlU p = true) as HP by (destruct p, p'; naive_solver).
                 rewrite HP in H1. iPureIntro. auto.
-              * iApply (region_state_nwl_future W W l Monotone _ _ (min a' e')); eauto.
+              * iApply (region_state_nwl_future W W l Directed _ _ (min a' e')); eauto.
                 assert (x ∈ region_addrs b' (min a' e')) as [_ Hin]%elem_of_region_addrs;
                   [apply elem_of_list_lookup;eauto|];auto.
                 destruct (pwlU p);auto. destruct l;auto;inversion H0.

theories/binary_model/fundamental_binary.v

@@ -76,7 +76,7 @@ Section fundamental.
   Proof. intros. case_decide;apply _. Qed.
 
   Theorem fundamental_binary W r p g b e (a : Addr) :
-    ⊢ ((⌜p = RX⌝ ∨ ⌜p = RWX⌝ ∨ ⌜p = RWLX ∧ g = Monotone⌝) →
+    ⊢ ((⌜p = RX⌝ ∨ ⌜p = RWX⌝ ∨ ⌜p = RWLX ∧ g = Directed⌝) →
        spec_ctx →
        region_conditions W p g b e →
        interp_expression r W (inr ((p,g),b,e,a),inr ((p,g),b,e,a))).
@@ -237,7 +237,7 @@ Section fundamental.
   Qed.
 
   Lemma fundamental_binary_from_interp_correctPC W p g b e a r (w:Word) :
-    p = RX ∨ p = RWX ∨ (p = RWLX ∧ g = Monotone) →
+    p = RX ∨ p = RWX ∨ (p = RWLX ∧ g = Directed) →
     ⊢ spec_ctx -∗ interp W (inr (p, g, b, e, a),w) -∗
       interp_expression r W (inr (p,g,b,e,a),w).
   Proof.
@@ -272,7 +272,7 @@ Section fundamental.
     iDestruct (interp_eq with "Hinterp") as %<-.
     destruct (decide (isCorrectPC (inr ((p,g),b,e,a)))).
     - assert (p = RX ∨ p = RWX ∨ p = RWLX) as Hp;[inversion i;auto|].
-      iAssert (⌜p = RWLX → g = Monotone⌝)%I as %Hmono.
+      iAssert (⌜p = RWLX → g = Directed⌝)%I as %Hmono.
       { iIntros (->). iDestruct (writeLocalAllowed_implies_local with "Hinterp") as %Hmono;[auto|destruct g;auto]. }
       iApply (fundamental_binary_from_interp_correctPC with "Hspec Hinterp").
       destruct Hp as [-> | [-> | ->] ];auto.