From 84873d184b4e5da53e5b9b1bc4d6c0e91a24823b Mon Sep 17 00:00:00 2001 From: Alix Trieu Date: Mon, 3 Jan 2022 18:35:04 +0100 Subject: [PATCH] Rename Monotone into Directed --- README.md | 3 +- .../confidentiality_adequacy.v | 2 +- .../examples_binary/push_pop_binary.v | 6 +- .../ftlr_binary/AddSubLt_binary.v | 4 +- .../binary_model/ftlr_binary/Load_binary.v | 2 +- .../ftlr_binary/Restrict_binary.v | 2 +- .../binary_model/ftlr_binary/StoreU_binary.v | 2 +- .../binary_model/ftlr_binary/Store_binary.v | 2 +- .../ftlr_binary/ftlr_base_binary.v | 4 +- .../ftlr_binary/interp_weakening_binary.v | 14 +- theories/binary_model/fundamental_binary.v | 6 +- theories/binary_model/logrel_binary.v | 40 +++--- theories/binary_model/monotone_binary.v | 18 +-- theories/cap_lang.v | 2 +- theories/examples/addr_reg_sample.v | 2 +- theories/examples/awkward_example_adequacy.v | 2 +- theories/examples/awkward_example_u.v | 6 +- theories/examples/downwards_lse_adequacy.v | 2 +- theories/examples/macros/push_pop.v | 38 +++--- theories/examples/macros/scall_u.v | 10 +- theories/examples/stack_object.v | 8 +- theories/examples/stack_object_adequacy.v | 2 +- theories/examples/stack_object_helpers.v | 4 +- theories/ftlr/AddSubLt.v | 4 +- theories/ftlr/Restrict.v | 2 +- theories/ftlr/Store.v | 2 +- theories/ftlr/StoreU.v | 2 +- theories/ftlr/ftlr_base.v | 4 +- theories/ftlr/interp_weakening.v | 14 +- theories/fundamental.v | 6 +- theories/logrel.v | 40 +++--- theories/machine_base.v | 16 +-- theories/monotone.v | 18 +-- theories/overlay/call.v | 2 +- theories/overlay/lang.v | 18 +-- theories/overlay_cap_lang_sim.v | 128 +++++++++--------- 36 files changed, 218 insertions(+), 219 deletions(-) diff --git a/README.md b/README.md index 29f5620..33d7938 100644 --- a/README.md +++ b/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* diff --git a/theories/binary_model/examples_binary/confidentiality_adequacy.v b/theories/binary_model/examples_binary/confidentiality_adequacy.v index e08969f..d67b523 100644 --- a/theories/binary_model/examples_binary/confidentiality_adequacy.v +++ b/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 := diff --git a/theories/binary_model/examples_binary/push_pop_binary.v b/theories/binary_model/examples_binary/push_pop_binary.v index 8eb6b4b..5169b8a 100644 --- a/theories/binary_model/examples_binary/push_pop_binary.v +++ b/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')". diff --git a/theories/binary_model/ftlr_binary/AddSubLt_binary.v b/theories/binary_model/ftlr_binary/AddSubLt_binary.v index c2fda67..934747c 100644 --- a/theories/binary_model/ftlr_binary/AddSubLt_binary.v +++ b/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)) diff --git a/theories/binary_model/ftlr_binary/Load_binary.v b/theories/binary_model/ftlr_binary/Load_binary.v index 702a266..1d68526 100644 --- a/theories/binary_model/ftlr_binary/Load_binary.v +++ b/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. } diff --git a/theories/binary_model/ftlr_binary/Restrict_binary.v b/theories/binary_model/ftlr_binary/Restrict_binary.v index 2e86d9a..c371693 100644 --- a/theories/binary_model/ftlr_binary/Restrict_binary.v +++ b/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. diff --git a/theories/binary_model/ftlr_binary/StoreU_binary.v b/theories/binary_model/ftlr_binary/StoreU_binary.v index a4facf6..04e1728 100644 --- a/theories/binary_model/ftlr_binary/StoreU_binary.v +++ b/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. diff --git a/theories/binary_model/ftlr_binary/Store_binary.v b/theories/binary_model/ftlr_binary/Store_binary.v index 32f8fa9..f6f4115 100644 --- a/theories/binary_model/ftlr_binary/Store_binary.v +++ b/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". diff --git a/theories/binary_model/ftlr_binary/ftlr_base_binary.v b/theories/binary_model/ftlr_binary/ftlr_base_binary.v index a87bd34..b0f65cf 100644 --- a/theories/binary_model/ftlr_binary/ftlr_base_binary.v +++ b/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)) diff --git a/theories/binary_model/ftlr_binary/interp_weakening_binary.v b/theories/binary_model/ftlr_binary/interp_weakening_binary.v index f1cb82f..fca92e2 100644 --- a/theories/binary_model/ftlr_binary/interp_weakening_binary.v +++ b/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. diff --git a/theories/binary_model/fundamental_binary.v b/theories/binary_model/fundamental_binary.v index 26c92ef..fe52ece 100644 --- a/theories/binary_model/fundamental_binary.v +++ b/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. diff --git a/theories/binary_model/logrel_binary.v b/theories/binary_model/logrel_binary.v index 6ebdbcc..0083e6c 100644 --- a/theories/binary_model/logrel_binary.v +++ b/theories/binary_model/logrel_binary.v @@ -120,7 +120,7 @@ Section logrel. (match g with (* | Local => ⌜related_sts_pub_plus_world W W'⌝ *) | Local | Global => ⌜related_sts_priv_world W W'⌝ - | Monotone => ⌜related_sts_a_world W W' l⌝ + | Directed => ⌜related_sts_a_world W W' l⌝ end)%I. Global Instance future_world_persistent g l W W': Persistent (future_world g l W W'). @@ -158,7 +158,7 @@ Section logrel. | | nwl | pwl | | | - < a | a ≤ - | - < a | a ≤ - | ------------------------------------------------------------- - | Monotone | {M,P} | {M,P,U} | {M} | {M,U} | + | Directed | {M,P} | {M,P,U} | {M} | {M,U} | |-----------------------------------------------------------| | Local | {P} | N/A | |-----------------------------------------------------------| @@ -177,7 +177,7 @@ Section logrel. match l with | Local => (std W) !! a = Some Permanent | Global => (std W) !! a = Some Permanent - | Monotone => (std W) !! a = Some Monotemporary + | Directed => (std W) !! a = Some Monotemporary ∨ (std W) !! a = Some Permanent end. @@ -223,7 +223,7 @@ Section logrel. Program Definition interp_cap_RWL (interp : D) : D := λne W w, (match w with - | (inr ((RWL,Monotone),b,e,a), inr (RWL,Monotone,b',e',a')) => + | (inr ((RWL,Directed),b,e,a), inr (RWL,Directed,b',e',a')) => ⌜b = b' ∧ e = e' ∧ a = a'⌝ ∗ [∗ list] a ∈ (region_addrs b e), (read_write_cond a interp) ∧ ⌜region_state_pwl_mono W a⌝ (* | inr ((RWL,Local),b,e,a) => *) @@ -261,7 +261,7 @@ Section logrel. Program Definition interp_cap_RWLX (interp : D) : D := λne W w, (match w with - | (inr ((RWLX,Monotone),b,e,a),inr (RWLX,Monotone,b',e',a')) => + | (inr ((RWLX,Directed),b,e,a),inr (RWLX,Directed,b',e',a')) => ⌜b = b' ∧ e = e' ∧ a = a'⌝ ∗ ([∗ list] a ∈ (region_addrs b e), (read_write_cond a interp) ∧ ⌜region_state_pwl_mono W a⌝) @@ -273,10 +273,10 @@ Section logrel. Program Definition interp_cap_URW (interp : D) : D := λne W w, (match w with - | (inr ((URW,Monotone),b,e,a), inr (URW,Monotone,b',e',a')) => + | (inr ((URW,Directed),b,e,a), inr (URW,Directed,b',e',a')) => ⌜b = b' ∧ e = e' ∧ a = a'⌝ ∗ ([∗ list] a' ∈ (region_addrs b (addr_reg.min a e)), (read_write_cond a' interp) - ∧ ⌜region_state_nwl W a' Monotone⌝) ∗ + ∧ ⌜region_state_nwl W a' Directed⌝) ∗ ([∗ list] a' ∈ (region_addrs (addr_reg.max b a) e), (read_write_cond a' interp) ∧ ⌜region_state_U_mono W a'⌝) | (inr ((URW,Local),b,e,a), inr (URW,Local,b',e',a')) => ⌜b = b' ∧ e = e' ∧ a = a'⌝ ∗ @@ -292,7 +292,7 @@ Section logrel. Program Definition interp_cap_URWL (interp : D) : D := λne W w, (match w with - | (inr ((URWL,Monotone),b,e,a), inr (URWL,Monotone,b',e',a')) => + | (inr ((URWL,Directed),b,e,a), inr (URWL,Directed,b',e',a')) => ⌜b = b' ∧ e = e' ∧ a = a'⌝ ∗ ([∗ list] a' ∈ (region_addrs b (addr_reg.min a e)), (read_write_cond a' interp) ∧ ⌜region_state_pwl_mono W a'⌝) ∗ @@ -309,10 +309,10 @@ Section logrel. Program Definition interp_cap_URWX (interp : D) : D := λne W w, (match w with - | (inr ((URWX,Monotone),b,e,a), inr (URWX,Monotone,b',e',a')) => + | (inr ((URWX,Directed),b,e,a), inr (URWX,Directed,b',e',a')) => ⌜b = b' ∧ e = e' ∧ a = a'⌝ ∗ ([∗ list] a' ∈ (region_addrs b (addr_reg.min a e)), (read_write_cond a' interp) - ∧ ⌜region_state_nwl W a' Monotone⌝) + ∧ ⌜region_state_nwl W a' Directed⌝) ∗ ([∗ list] a' ∈ (region_addrs (addr_reg.max b a) e), (read_write_cond a' interp) ∧ ⌜region_state_U_mono W a'⌝) | (inr ((URWX,Local),b,e,a), inr (URWX,Local,b',e',a')) => @@ -330,7 +330,7 @@ Section logrel. Program Definition interp_cap_URWLX (interp : D) : D := λne W w, (match w with - | (inr ((URWLX,Monotone),b,e,a), inr (URWLX,Monotone,b',e',a')) => + | (inr ((URWLX,Directed),b,e,a), inr (URWLX,Directed,b',e',a')) => ⌜b = b' ∧ e = e' ∧ a = a'⌝ ∗ ([∗ list] a' ∈ (region_addrs b (addr_reg.min a e)), (read_write_cond a' interp) ∧ ⌜region_state_pwl_mono W a'⌝) @@ -658,15 +658,15 @@ Section logrel. [|eauto];solve_addr]). Qed. - Definition isMonotone l := + Definition isDirected l := match l with - | Monotone => true + | Directed => true | _ => false end. Lemma writeLocalAllowed_implies_local W (p : Perm) (l : Locality) (b e a : Addr) (w : Word): machine_base.pwl p = true -> - interp W (inr ((p, l), b, e, a),w) -∗ ⌜isMonotone l = true⌝. + interp W (inr ((p, l), b, e, a),w) -∗ ⌜isDirected l = true⌝. Proof. intros. iIntros "Hvalid". unfold interp; rewrite fixpoint_interp1_eq /=. @@ -677,7 +677,7 @@ Section logrel. Lemma writeLocalAllowedU_implies_local W p l b e a (w : Word): pwlU p = true -> - interp W (inr (p, l, b, e, a),w) -∗ ⌜isMonotone l = true⌝. + interp W (inr (p, l, b, e, a),w) -∗ ⌜isDirected l = true⌝. Proof. intros. iIntros "Hvalid". unfold interp; rewrite fixpoint_interp1_eq /=. @@ -952,7 +952,7 @@ Section logrel. Proof. intros Hp Hb. iIntros "Hvalid". iDestruct (interp_eq with "Hvalid") as %<-. - iAssert (⌜isMonotone l = true⌝)%I as "%". by iApply writeLocalAllowed_implies_local. + iAssert (⌜isDirected l = true⌝)%I as "%". by iApply writeLocalAllowed_implies_local. eapply withinBounds_le_addr in Hb. unfold interp; rewrite fixpoint_interp1_eq /=. destruct p; simpl in Hp; try congruence; destruct l;try done. @@ -968,7 +968,7 @@ Section logrel. Proof. intros Hp Hb. iIntros "Hvalid". iDestruct (interp_eq with "Hvalid") as %<-. - iAssert (⌜isMonotone l = true⌝)%I as "%". by iApply writeLocalAllowedU_implies_local. + iAssert (⌜isDirected l = true⌝)%I as "%". by iApply writeLocalAllowedU_implies_local. eapply withinBounds_le_addr in Hb. unfold interp; rewrite fixpoint_interp1_eq /=. destruct p; simpl in Hp; try congruence; destruct l;try done; @@ -991,7 +991,7 @@ Section logrel. ⌜std W !! a' = Some Monotemporary⌝. Proof. intros Hp Hlt Hb. iIntros "Hvalid". - iAssert (⌜isMonotone l = true⌝)%I as "%". by iApply writeLocalAllowedU_implies_local. + iAssert (⌜isDirected l = true⌝)%I as "%". by iApply writeLocalAllowedU_implies_local. eapply withinBounds_le_addr in Hlt. iDestruct (interp_eq with "Hvalid") as %<-. unfold interp; rewrite fixpoint_interp1_eq /=. @@ -1013,13 +1013,13 @@ Section logrel. ([∗ list] a ∈ region_addrs b (if isU p && isLocal l then (addr_reg.min a e) else e), (if writeAllowed p || readAllowedU p then read_write_cond a interp else (∃ (P:D), ⌜(∀ Wv, Persistent (P Wv.1 Wv.2))⌝ ∧ read_cond a P interp)) ∧ ⌜if pwlU p then region_state_pwl_mono W a else region_state_nwl W a l⌝) ∗ - (⌜if pwlU p then isMonotone l else True⌝) ∗ + (⌜if pwlU p then isDirected l else True⌝) ∗ (if isU p && isLocal l then [∗ list] a ∈ region_addrs (addr_reg.max b a) e, read_write_cond a interp ∧ ⌜if pwlU p then region_state_U_pwl_mono W a else (match l with - | Monotone => region_state_U_mono W a + | Directed => region_state_U_mono W a | _ => region_state_U W a end)⌝ else emp%I))%I). Proof. diff --git a/theories/binary_model/monotone_binary.v b/theories/binary_model/monotone_binary.v index 5c7e574..db06f29 100644 --- a/theories/binary_model/monotone_binary.v +++ b/theories/binary_model/monotone_binary.v @@ -300,7 +300,7 @@ Section monotone. iSpecialize ("Hw" $! r W'' with "Hrelated"). iApply "Hw". + iIntros (Hrelated'). - iAssert (future_world Monotone a0 W W'')%I as "Hrelated". + iAssert (future_world Directed a0 W W'')%I as "Hrelated". { iPureIntro. apply related_sts_pub_a_trans_world with W'; auto. } iSpecialize ("Hw" $! r W'' with "Hrelated"). iApply "Hw". @@ -349,7 +349,7 @@ Section monotone. iDestruct "Hw" as "#[Hrw Hst ]". iSplit;eauto. iFrame "#". iDestruct "Hst" as %Hstd. - iPureIntro. eapply (region_state_nwl_monotone W W' _ Monotone); auto. + iPureIntro. eapply (region_state_nwl_monotone W W' _ Directed); auto. * iApply (big_sepL_mono with "Hw2"). iIntros (n y Hsome) "Hw". iDestruct "Hw" as "#[Hrw Hst ]". @@ -405,7 +405,7 @@ Section monotone. iDestruct "Hw" as "#[Hrw Hst ]". iSplit;eauto. iFrame "#". iDestruct "Hst" as %Hstd. - iPureIntro. eapply (region_state_nwl_monotone W W' _ Monotone); auto. + iPureIntro. eapply (region_state_nwl_monotone W W' _ Directed); auto. * iApply (big_sepL_mono with "Hw2"). iIntros (n y Hsome) "Hw". iDestruct "Hw" as "#[Hrw Hst ]". @@ -501,7 +501,7 @@ Section monotone. iSpecialize ("Hw" $! r W'' with "Hrelated"). iApply "Hw". + iIntros (Hrelated'). - iAssert (future_world Monotone a0 W W'')%I as "Hrelated". + iAssert (future_world Directed a0 W W'')%I as "Hrelated". { iPureIntro. apply related_sts_a_trans_world with W';auto. } iSpecialize ("Hw" $! r W'' with "Hrelated"). iApply "Hw". @@ -552,7 +552,7 @@ Section monotone. iDestruct "Hw" as "#[Hrw Hst ]". iSplit;eauto. iFrame "#". iDestruct "Hst" as %Hstd. - iPureIntro. eapply (region_state_nwl_monotone_a W W' _ (addr_reg.min a a0) Monotone); auto. + iPureIntro. eapply (region_state_nwl_monotone_a W W' _ (addr_reg.min a a0) Directed); auto. eapply region_addrs_lookup_le;eauto. apply related_sts_a_weak_world with a;auto. solve_addr. * iApply (big_sepL_mono with "Hw2"). iIntros (n y Hsome) "Hw". @@ -615,7 +615,7 @@ Section monotone. iDestruct "Hw" as "#[Hrw Hst ]". iSplit;eauto. iFrame "#". iDestruct "Hst" as %Hstd. - iPureIntro. eapply (region_state_nwl_monotone_a W W' _ (addr_reg.min a a0) Monotone); auto. + iPureIntro. eapply (region_state_nwl_monotone_a W W' _ (addr_reg.min a a0) Directed); auto. eapply region_addrs_lookup_le;eauto. apply related_sts_a_weak_world with a;auto. solve_addr. * iApply (big_sepL_mono with "Hw2"). iIntros (n y Hsome) "Hw". @@ -645,14 +645,14 @@ Section monotone. iPureIntro. apply region_state_U_pwl_monotone_mono_a with W a;auto. } Qed. - Definition isMonotoneWord (w : Word) := + Definition isDirectedWord (w : Word) := match w with | inl _ => false - | inr (_,l,_,_,_) => isMonotone l + | inr (_,l,_,_,_) => isDirected l end. Lemma interp_monotone_nm W W' w : - ⌜related_sts_priv_world W W'⌝ -∗ ⌜isMonotoneWord w.1 = false⌝ -∗ + ⌜related_sts_priv_world W W'⌝ -∗ ⌜isDirectedWord w.1 = false⌝ -∗ interp W w -∗ interp W' w. Proof. iIntros (Hrelated Hnl) "#Hw". diff --git a/theories/cap_lang.v b/theories/cap_lang.v index d830fc5..37213a5 100644 --- a/theories/cap_lang.v +++ b/theories/cap_lang.v @@ -772,7 +772,7 @@ Definition machine_component: Type := component nat _ _ Word. Definition initial_state `{MachineParameters} (r_stk: RegName) (b_stk e_stk: Addr) (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)) + | 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)) end. Definition can_address_only (w: Word) (addrs: gset Addr): Prop := diff --git a/theories/examples/addr_reg_sample.v b/theories/examples/addr_reg_sample.v index c4a3cc3..e94fd16 100644 --- a/theories/examples/addr_reg_sample.v +++ b/theories/examples/addr_reg_sample.v @@ -106,7 +106,7 @@ Section instr_encodings. (* encodings of enter capability permission pair *) Definition global_e := encodePermPair (E, Global). (* encodings of enter capability permission pair *) - Definition monotone_e := encodePermPair (E, Monotone). + Definition monotone_e := encodePermPair (E, Directed). End instr_encodings. Lemma all_registers_NoDup : diff --git a/theories/examples/awkward_example_adequacy.v b/theories/examples/awkward_example_adequacy.v index eac9aaa..d31a870 100644 --- a/theories/examples/awkward_example_adequacy.v +++ b/theories/examples/awkward_example_adequacy.v @@ -163,7 +163,7 @@ Definition is_initial_memory `{memory_layout} (m: gmap Addr Word) := Definition is_initial_registers `{memory_layout} (reg: gmap RegName Word) := reg !! PC = Some (inr (RX, Global, awk_region_start, awk_region_end, awk_preamble_start)) ∧ - reg !! r_stk = Some (inr (URWLX, Monotone, stack_start, stack_end, stack_start)) ∧ + reg !! r_stk = Some (inr (URWLX, Directed, stack_start, stack_end, stack_start)) ∧ reg !! r_t0 = Some (inr (RWX, Global, adv_start, adv_end, adv_start)) ∧ (∀ (r: RegName), r ∉ ({[ PC; r_stk; r_t0 ]} : gset RegName) → ∃ (w:Word), reg !! r = Some w ∧ is_cap w = false). diff --git a/theories/examples/awkward_example_u.v b/theories/examples/awkward_example_u.v index 729ad96..99a023c 100644 --- a/theories/examples/awkward_example_u.v +++ b/theories/examples/awkward_example_u.v @@ -89,7 +89,7 @@ Section awkward_example. (a_link + f_a)%a = Some a_entry -> (* the monotonicity of the PC is not monotone *) - isMonotone pc_g = false → + isDirected pc_g = false → (* malloc'ed memory assumption *) (d + 1)%a = Some d' -> @@ -516,7 +516,7 @@ Section awkward_example. { iNext. iSplit;done. } (* the adversary stack is valid in W2 *) - iAssert (interp W2 (inr (URWLX, Monotone, a_act_end, estk, frame_end))) as "#Hadv_stack_val". + iAssert (interp W2 (inr (URWLX, Directed, a_act_end, estk, frame_end))) as "#Hadv_stack_val". { iClear "∗". iApply fixpoint_interp1_eq. iSimpl. assert (addr_reg.min frame_end estk = frame_end) as ->. @@ -1080,7 +1080,7 @@ Section awkward_example. { iNext. iDestruct "Hprog_done" as "($&$&$&$&$&$)". iSplit;done. } (* the adversary stack is valid in W2 *) - iAssert (interp W5 (inr (URWLX, Monotone, a_act_final, estk, a_act_end))) as "#Hadv_stack_val_2". + iAssert (interp W5 (inr (URWLX, Directed, a_act_final, estk, a_act_end))) as "#Hadv_stack_val_2". { iClear "∗". iApply fixpoint_interp1_eq. iSimpl. assert (addr_reg.min a_act_end estk = a_act_end) as ->. diff --git a/theories/examples/downwards_lse_adequacy.v b/theories/examples/downwards_lse_adequacy.v index 9380f0f..7c92940 100644 --- a/theories/examples/downwards_lse_adequacy.v +++ b/theories/examples/downwards_lse_adequacy.v @@ -163,7 +163,7 @@ Definition is_initial_memory `{memory_layout} (m: gmap Addr Word) := Definition is_initial_registers `{memory_layout} (reg: gmap RegName Word) := reg !! PC = Some (inr (RX, Global, lse_region_start, lse_region_end, lse_preamble_start)) ∧ - reg !! r_stk = Some (inr (URWLX, Monotone, stack_start, stack_end, stack_start)) ∧ + reg !! r_stk = Some (inr (URWLX, Directed, stack_start, stack_end, stack_start)) ∧ reg !! r_t0 = Some (inr (RWX, Global, adv_start, adv_end, adv_start)) ∧ (∀ (r: RegName), r ∉ ({[ PC; r_stk; r_t0 ]} : gset RegName) → ∃ (w:Word), reg !! r = Some w ∧ is_cap w = false). diff --git a/theories/examples/macros/push_pop.v b/theories/examples/macros/push_pop.v index 5e2999f..0d9d333 100644 --- a/theories/examples/macros/push_pop.v +++ b/theories/examples/macros/push_pop.v @@ -14,29 +14,29 @@ Section stack_macros. Definition pushU_r a1 r_stk r : iProp Σ := (a1 ↦ₐ pushU_r_instr r_stk r)%I. - Definition isMonotone_word (w:Word) := + Definition isDirected_word (w:Word) := match w with | inl _ => false | inr (_,l,_,_,_) => match l with - | Monotone => true + | Directed => true | _ => false end end. Lemma pushU_r_spec a1 a2 w w' r 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' → - (isMonotone_word w' = true → (canReadUpTo w' <=? stk_a)%a = true) → + (isDirected_word w' = true → (canReadUpTo w' <=? stk_a)%a = true) → ▷ pushU_r a1 r_stk r ∗ ▷ 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) ∗ ▷ r ↦ᵣ w' ∗ ▷ stk_a ↦ₐ w ∗ ▷ (PC ↦ᵣ inr ((p,g),b,e,a2) ∗ pushU_r a1 r_stk r ∗ - r_stk ↦ᵣ inr ((URWLX,Monotone),stk_b,stk_e,stk_a') ∗ r ↦ᵣ w' ∗ stk_a ↦ₐ w' + r_stk ↦ᵣ inr ((URWLX,Directed),stk_b,stk_e,stk_a') ∗ r ↦ᵣ w' ∗ stk_a ↦ₐ w' -∗ WP Seq (Instr Executable) {{ φ }}) ⊢ WP Seq (Instr Executable) {{ φ }}. @@ -56,19 +56,19 @@ Section stack_macros. the monotone requirements *) Lemma pushU_r_or_fail_spec a1 a2 w w' r 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' → ▷ pushU_r a1 r_stk r ∗ ▷ 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) ∗ ▷ r ↦ᵣ w' ∗ ▷ stk_a ↦ₐ w ∗ ▷ (φ FailedV) - ∗ ▷ (⌜isMonotone_word w' = true → (canReadUpTo w' <=? stk_a)%a = true⌝ + ∗ ▷ (⌜isDirected_word w' = true → (canReadUpTo w' <=? stk_a)%a = true⌝ ∗ PC ↦ᵣ inr ((p,g),b,e,a2) ∗ pushU_r a1 r_stk r ∗ - r_stk ↦ᵣ inr ((URWLX,Monotone),stk_b,stk_e,stk_a') ∗ r ↦ᵣ w' ∗ stk_a ↦ₐ w' + r_stk ↦ᵣ inr ((URWLX,Directed),stk_b,stk_e,stk_a') ∗ r ↦ᵣ w' ∗ stk_a ↦ₐ w' -∗ WP Seq (Instr Executable) {{ φ }}) ⊢ WP Seq (Instr Executable) {{ φ }}. @@ -89,16 +89,16 @@ Section stack_macros. Lemma pushU_r_spec_same a1 a2 w 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' → ▷ pushU_r a1 r_stk r_stk ∗ ▷ 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 ∗ ▷ (PC ↦ᵣ inr ((p,g),b,e,a2) ∗ pushU_r a1 r_stk r_stk ∗ - r_stk ↦ᵣ inr ((URWLX,Monotone),stk_b,stk_e,stk_a') ∗ stk_a ↦ₐ inr ((URWLX,Monotone),stk_b,stk_e,stk_a) + r_stk ↦ᵣ inr ((URWLX,Directed),stk_b,stk_e,stk_a') ∗ stk_a ↦ₐ inr ((URWLX,Directed),stk_b,stk_e,stk_a) -∗ WP Seq (Instr Executable) {{ φ }}) ⊢ WP Seq (Instr Executable) {{ φ }}. @@ -119,16 +119,16 @@ Section stack_macros. Lemma pushU_z_spec 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' → ▷ pushU_z 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 ∗ ▷ (PC ↦ᵣ inr ((p,g),b,e,a2) ∗ pushU_z 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 -∗ WP Seq (Instr Executable) {{ φ }}) ⊢ WP Seq (Instr Executable) {{ φ }}. @@ -153,7 +153,7 @@ Section stack_macros. Lemma popU_spec a1 a2 a3 a4 r w w' wt1 p g b e stk_b stk_e stk_a stk_a' φ : isCorrectPC (inr ((p,g),b,e,a1)) ∧ isCorrectPC (inr ((p,g),b,e,a2)) ∧ isCorrectPC (inr ((p,g),b,e,a3)) → - withinBounds ((URWLX,Monotone),stk_b,stk_e,stk_a') = true → + withinBounds ((URWLX,Directed),stk_b,stk_e,stk_a') = true → r ≠ PC → (a1 + 1)%a = Some a2 → (a2 + 1)%a = Some a3 → @@ -162,7 +162,7 @@ Section stack_macros. ▷ popU a1 a2 a3 r_stk r ∗ ▷ 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 ∗ ▷ r_t1 ↦ᵣ wt1 ∗ ▷ r ↦ᵣ w' @@ -170,7 +170,7 @@ Section stack_macros. ∗ popU a1 a2 a3 r_stk r ∗ r ↦ᵣ w ∗ stk_a' ↦ₐ w - ∗ r_stk ↦ᵣ inr ((URWLX,Monotone),stk_b,stk_e,stk_a') + ∗ r_stk ↦ᵣ inr ((URWLX,Directed),stk_b,stk_e,stk_a') ∗ r_t1 ↦ᵣ (inl (-1)%Z) -∗ WP Seq (Instr Executable) {{ φ }}) ⊢ diff --git a/theories/examples/macros/scall_u.v b/theories/examples/macros/scall_u.v index 203a9e6..866e536 100644 --- a/theories/examples/macros/scall_u.v +++ b/theories/examples/macros/scall_u.v @@ -105,7 +105,7 @@ Section scall. withinBounds ((URWLX, Local), b_r, e_r, a_r) = true -> withinBounds ((URWLX, Local), b_r, e_r, b_r_adv) = true → contiguous_between a a_first a_cont → - isMonotone g = false → + isDirected g = false → r1 ∉ [PC;r_stk;r_t0;r_t1;r_t2;r_t3;r_t4;r_t5;r_t6] → (* the jump destination will not be overwritten/cleared *) params ## [PC;r_stk;r_t0;r_t1; r_t2; r_t3; r_t4; r_t5; r_t6] → (* the parameters will not be overwritten/cleared *) dom (gset RegName) rmap = all_registers_s ∖ {[ PC; r_stk; r1; r_t0]} ∖ (list_to_set params) → @@ -116,15 +116,15 @@ Section scall. (▷ scallU_prologue a r1 params ∗ ▷ PC ↦ᵣ inr ((p,g),b,e,a_first) - ∗ ▷ r_stk ↦ᵣ inr ((URWLX,Monotone),b_r,e_r,a_r) + ∗ ▷ r_stk ↦ᵣ inr ((URWLX,Directed),b_r,e_r,a_r) ∗ ▷ (∃ w, r_t0 ↦ᵣ w) ∗ ▷ ([∗ map] r_i↦w_i ∈ rmap, r_i ↦ᵣ w_i) ∗ ▷ ([[a_r, b_r_adv]]↦ₐ[[ws_own]]) (* local stack - note that the perm here is NOT unitialized, as the definition of interp1 has a promote_permission in there *) (* No ownership of adversarial stack here; no clearing required *) ∗ ▷ (PC ↦ᵣ inr (p,g,b,e,a_cont) - ∗ r_stk ↦ᵣ inr ((URWLX,Monotone),b_r_adv,e_r,b_r_adv) - ∗ r_t0 ↦ᵣ inr ((E,Monotone),b_r,b_r_adv,a_r) (* Note that this capbility does not grant permissions up to the end of the stack anymore *) + ∗ r_stk ↦ᵣ inr ((URWLX,Directed),b_r_adv,e_r,b_r_adv) + ∗ r_t0 ↦ᵣ inr ((E,Directed),b_r,b_r_adv,a_r) (* Note that this capbility does not grant permissions up to the end of the stack anymore *) ∗ (∃ rmap', ⌜dom (gset RegName) rmap = dom (gset RegName) rmap' ∧ ∀ r w, rmap' !! r = Some w → w = inl 0%Z⌝ ∗ [∗ map] r_i↦w_i ∈ rmap', r_i ↦ᵣ w_i) ∗ [[ a_r, b_r_adv ]]↦ₐ[[ [inl w_1; @@ -133,7 +133,7 @@ Section scall. inl w_4a; inl w_4b_U; inr (p,g,b,e,a_next); - inr (URWLX,Monotone,b_r,e_r,a_r_adv)] ]] (* local stack *) + inr (URWLX,Directed,b_r,e_r,a_r_adv)] ]] (* local stack *) ∗ scallU_prologue a r1 params -∗ WP Seq (Instr Executable) {{ φ }}) ⊢ WP Seq (Instr Executable) {{ φ }})%I. diff --git a/theories/examples/stack_object.v b/theories/examples/stack_object.v index 1e7abd6..628b33e 100644 --- a/theories/examples/stack_object.v +++ b/theories/examples/stack_object.v @@ -87,7 +87,7 @@ Section stack_object. (a_link + f_a)%a = Some a_entry -> (* the monotonicity of the PC is not monotone *) - isMonotone pc_g = false → + isDirected pc_g = false → (* footprint of the register map *) dom (gset RegName) rmap = all_registers_s ∖ {[PC;r_stk;r_adv]} → @@ -453,7 +453,7 @@ Section stack_object. set rmap3 := <[PC:=updatePcPerm (inr (g, Global, b, e, a'))]> (<[PC:=inl 0%Z]> - (<[r_stk:=inr (URWLX, Monotone, b_r_adv, estk, frame_end)]> + (<[r_stk:=inr (URWLX, Directed, b_r_adv, estk, frame_end)]> (<[r_adv:=inr (g, Global, b, e, a')]> rmap2))). match goal with |- context [ [[af3,b_r_adv]]↦ₐ[[?act]]%I ] => set actw := act @@ -534,7 +534,7 @@ Section stack_object. rewrite -(region_addrs_single a_param af2)//. apply region_addrs_disjoint_skip_middle. auto. clear -Hb_r_adv. solve_addr. } (* we are ready to close the parts of the world that must stay valid: the two stack objects *) - iAssert (⌜if pwl l then p = Monotone else True⌝)%I as %Hmono. + iAssert (⌜if pwl l then p = Directed else True⌝)%I as %Hmono. { destruct (pwl l) eqn:Hpwl. iDestruct (writeLocalAllowed_implies_local with "Hwsecret_valid") as %HH;auto. iPureIntro. destruct p;inversion HH;auto. auto. } iMod (close_stack_object with "Hsecret_cond Hsec_res Hsts Hr") as "(Hsts & Hr & #Hvalid)"; @@ -642,7 +642,7 @@ Section stack_object. where the parameter is not yet monotemporary, this is fine in this case since we do not care about it anymore *) - iSimpl. rewrite (fixpoint_interp1_eq _ (inr (E, Monotone, bstk, b_r_adv, af3))). iModIntro. + iSimpl. rewrite (fixpoint_interp1_eq _ (inr (E, Directed, bstk, b_r_adv, af3))). iModIntro. iIntros (r' W' Hrelated). iNext. iIntros "(#[Hall Hregs_valid] & Hregs & Hr & Hsts & Hown)". iSplit;auto. iDestruct "Hall" as %Hr_all. iClear "Hall". diff --git a/theories/examples/stack_object_adequacy.v b/theories/examples/stack_object_adequacy.v index e392048..ed52466 100644 --- a/theories/examples/stack_object_adequacy.v +++ b/theories/examples/stack_object_adequacy.v @@ -163,7 +163,7 @@ Definition is_initial_memory `{memory_layout} (m: gmap Addr Word) := Definition is_initial_registers `{memory_layout} (reg: gmap RegName Word) := reg !! PC = Some (inr (RX, Global, obj_region_start, obj_region_end, obj_preamble_start)) ∧ - reg !! r_stk = Some (inr (URWLX, Monotone, stack_start, stack_end, stack_start)) ∧ + reg !! r_stk = Some (inr (URWLX, Directed, stack_start, stack_end, stack_start)) ∧ reg !! r_t0 = Some (inr (RWX, Global, adv_start, adv_end, adv_start)) ∧ (∀ (r: RegName), r ∉ ({[ PC; r_stk; r_t0 ]} : gset RegName) → ∃ (w:Word), reg !! r = Some w ∧ is_cap w = false). diff --git a/theories/examples/stack_object_helpers.v b/theories/examples/stack_object_helpers.v index 04029ea..7ac90ec 100644 --- a/theories/examples/stack_object_helpers.v +++ b/theories/examples/stack_object_helpers.v @@ -385,7 +385,7 @@ Section stack_object. (W1)))) W' b_r_adv → - interp W (inr (URWLX, Monotone, bstk, estk, astk)) -∗ + interp W (inr (URWLX, Directed, bstk, estk, astk)) -∗ □ ([∗ map] a16↦w7 ∈ m, □ ∃ (φ0 : WORLD * Word → iPropI Σ), ⌜∀ Wv : WORLD * Word, Persistent (φ0 Wv)⌝ @@ -635,7 +635,7 @@ Section stack_object. Qed. Lemma close_stack_object W E m la1 la2 ρ wps l p bsec esec asec : - (if pwl l then p = Monotone else True) → + (if pwl l then p = Directed else True) → readAllowed l → length (region_addrs bsec esec) = length wps → Forall (λ w : (Z + Cap), ∃ z : Z, w = inl z) wps → diff --git a/theories/ftlr/AddSubLt.v b/theories/ftlr/AddSubLt.v index b633530..99e1490 100644 --- a/theories/ftlr/AddSubLt.v +++ b/theories/ftlr/AddSubLt.v @@ -24,7 +24,7 @@ Section fundamental. Lemma add_sub_lt_case (W : WORLD) (r : leibnizO Reg) (p : Perm) (g : Locality) (b e a : Addr) (w : Word) (ρ : region_type) (dst : RegName) (r1 r2: Z + RegName) (P:D): - p = RX ∨ p = RWX ∨ (p = RWLX /\ g = Monotone) + p = RX ∨ p = RWX ∨ (p = RWLX /\ g = Directed) → (∀ x : RegName, is_Some (r !! x)) → isCorrectPC (inr (p, g, b, e, a)) → (b <= a)%a ∧ (a < e)%a @@ -44,7 +44,7 @@ Section fundamental. -∗ region a0 -∗ sts_full_world a0 -∗ na_own logrel_nais ⊤ - -∗ ⌜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 !r! r1)) diff --git a/theories/ftlr/Restrict.v b/theories/ftlr/Restrict.v index 5c36f27..75c2930 100644 --- a/theories/ftlr/Restrict.v +++ b/theories/ftlr/Restrict.v @@ -88,7 +88,7 @@ Section fundamental. rewrite H5 in H3. iDestruct (region_close with "[$Hstate $Hr $Ha $Hmono Hw]") as "Hr"; eauto. { destruct ρ;auto;[|specialize (Hnotmonostatic g)|specialize (Hnotuninitialized w0)];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. diff --git a/theories/ftlr/Store.v b/theories/ftlr/Store.v index 2e15002..42f9b65 100644 --- a/theories/ftlr/Store.v +++ b/theories/ftlr/Store.v @@ -24,7 +24,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)). Proof. iIntros (Hp) "#HR". diff --git a/theories/ftlr/StoreU.v b/theories/ftlr/StoreU.v index fadf5f7..5c787bc 100644 --- a/theories/ftlr/StoreU.v +++ b/theories/ftlr/StoreU.v @@ -129,7 +129,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)). Proof. diff --git a/theories/ftlr/ftlr_base.v b/theories/ftlr/ftlr_base.v index 0073fb3..a06062b 100644 --- a/theories/ftlr/ftlr_base.v +++ b/theories/ftlr/ftlr_base.v @@ -22,7 +22,7 @@ Section fundamental. Definition ftlr_instr (W : WORLD) (r : leibnizO Reg) (p : Perm) (g : Locality) (b e a : Addr) (w : Word) (i: instr) (ρ : region_type) (P : D) := - p = RX ∨ p = RWX ∨ (p = RWLX /\ g = Monotone) + p = RX ∨ p = RWX ∨ (p = RWLX /\ g = Directed) → (∀ x : RegName, is_Some (r !! x)) → isCorrectPC (inr (p, g, b, e, a)) → (b <= a)%a ∧ (a < e)%a @@ -40,7 +40,7 @@ Section fundamental. -∗ region a0 -∗ sts_full_world a0 -∗ na_own logrel_nais ⊤ - -∗ ⌜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 !r! r1)) diff --git a/theories/ftlr/interp_weakening.v b/theories/ftlr/interp_weakening.v index 041b8ba..0aedf3a 100644 --- a/theories/ftlr/interp_weakening.v +++ b/theories/ftlr/interp_weakening.v @@ -29,14 +29,14 @@ Section fundamental. -∗ region a0 -∗ sts_full_world a0 -∗ na_own logrel_nais ⊤ - -∗ ⌜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'⌝. @@ -71,7 +71,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'⌝. @@ -233,7 +233,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. @@ -272,7 +272,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. @@ -293,7 +293,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. @@ -351,7 +351,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. diff --git a/theories/fundamental.v b/theories/fundamental.v index 87aa523..4d88e9f 100644 --- a/theories/fundamental.v +++ b/theories/fundamental.v @@ -54,7 +54,7 @@ Section fundamental. Proof. intros. case_decide;apply _. Qed. Theorem fundamental W r p g b e (a : Addr) : - ⊢ ((⌜p = RX⌝ ∨ ⌜p = RWX⌝ ∨ ⌜p = RWLX ∧ g = Monotone⌝) → + ⊢ ((⌜p = RX⌝ ∨ ⌜p = RWX⌝ ∨ ⌜p = RWLX ∧ g = Directed⌝) → region_conditions W p g b e → interp_expression r W (inr ((p,g),b,e,a))). Proof. @@ -202,7 +202,7 @@ Section fundamental. Qed. Lemma fundamental_from_interp_correctPC W p g b e a r : - p = RX ∨ p = RWX ∨ (p = RWLX ∧ g = Monotone) → + p = RX ∨ p = RWX ∨ (p = RWLX ∧ g = Directed) → ⊢ interp W (inr (p, g, b, e, a)) → interp_expression r W (inr (p,g,b,e,a)). Proof. @@ -234,7 +234,7 @@ Section fundamental. iIntros "Hinterp". 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_from_interp_correctPC with "Hinterp"). destruct Hp as [-> | [-> | ->] ];auto. diff --git a/theories/logrel.v b/theories/logrel.v index fe17ee8..f7d877a 100644 --- a/theories/logrel.v +++ b/theories/logrel.v @@ -112,7 +112,7 @@ Section logrel. (match g with (* | Local => ⌜related_sts_pub_plus_world W W'⌝ *) | Local | Global => ⌜related_sts_priv_world W W'⌝ - | Monotone => ⌜related_sts_a_world W W' l⌝ + | Directed => ⌜related_sts_a_world W W' l⌝ end)%I. Global Instance future_world_persistent g l W W': Persistent (future_world g l W W'). @@ -145,7 +145,7 @@ Section logrel. | | nwl | pwl | | | - < a | a ≤ - | - < a | a ≤ - | ------------------------------------------------------------- - | Monotone | {M,P} | {M,P,U} | {M} | {M,U} | + | Directed | {M,P} | {M,P,U} | {M} | {M,U} | |-----------------------------------------------------------| | Local | {P} | N/A | |-----------------------------------------------------------| @@ -164,7 +164,7 @@ Section logrel. match l with | Local => (std W) !! a = Some Permanent | Global => (std W) !! a = Some Permanent - | Monotone => (std W) !! a = Some Monotemporary + | Directed => (std W) !! a = Some Monotemporary ∨ (std W) !! a = Some Permanent end. @@ -208,7 +208,7 @@ Section logrel. Program Definition interp_cap_RWL (interp : D) : D := λne W w, (match w with - | inr ((RWL,Monotone),b,e,a) => + | inr ((RWL,Directed),b,e,a) => [∗ list] a ∈ (region_addrs b e), (read_write_cond a interp) ∧ ⌜region_state_pwl_mono W a⌝ (* | inr ((RWL,Local),b,e,a) => *) (* [∗ list] a ∈ (region_addrs b e), ∃ p, ⌜PermFlows RWL p⌝ ∗ (read_write_cond a p interp) ∧ ⌜region_state_pwl W a⌝ *) @@ -242,7 +242,7 @@ Section logrel. Program Definition interp_cap_RWLX (interp : D) : D := λne W w, (match w with - | inr ((RWLX,Monotone),b,e,a) => + | inr ((RWLX,Directed),b,e,a) => ([∗ list] a ∈ (region_addrs b e), (read_write_cond a interp) ∧ ⌜region_state_pwl_mono W a⌝) (* | inr ((RWLX,Local),b,e,a) => *) @@ -253,9 +253,9 @@ Section logrel. Program Definition interp_cap_URW (interp : D) : D := λne W w, (match w with - | inr ((URW,Monotone),b,e,a) => + | inr ((URW,Directed),b,e,a) => ([∗ list] a' ∈ (region_addrs b (addr_reg.min a e)), (read_write_cond a' interp) - ∧ ⌜region_state_nwl W a' Monotone⌝) ∗ + ∧ ⌜region_state_nwl W a' Directed⌝) ∗ ([∗ list] a' ∈ (region_addrs (addr_reg.max b a) e), (read_write_cond a' interp) ∧ ⌜region_state_U_mono W a'⌝) | inr ((URW,Local),b,e,a) => ([∗ list] a' ∈ (region_addrs b (addr_reg.min a e)), (read_write_cond a' interp) @@ -269,7 +269,7 @@ Section logrel. Program Definition interp_cap_URWL (interp : D) : D := λne W w, (match w with - | inr ((URWL,Monotone),b,e,a) => + | inr ((URWL,Directed),b,e,a) => ([∗ list] a' ∈ (region_addrs b (addr_reg.min a e)), (read_write_cond a' interp) ∧ ⌜region_state_pwl_mono W a'⌝) ∗ ([∗ list] a' ∈ (region_addrs (addr_reg.max b a) e), (read_write_cond a' interp) ∧ @@ -285,9 +285,9 @@ Section logrel. Program Definition interp_cap_URWX (interp : D) : D := λne W w, (match w with - | inr ((URWX,Monotone),b,e,a) => + | inr ((URWX,Directed),b,e,a) => ([∗ list] a' ∈ (region_addrs b (addr_reg.min a e)), (read_write_cond a' interp) - ∧ ⌜region_state_nwl W a' Monotone⌝) + ∧ ⌜region_state_nwl W a' Directed⌝) ∗ ([∗ list] a' ∈ (region_addrs (addr_reg.max b a) e), (read_write_cond a' interp) ∧ ⌜region_state_U_mono W a'⌝) | inr ((URWX,Local),b,e,a) => @@ -303,7 +303,7 @@ Section logrel. Program Definition interp_cap_URWLX (interp : D) : D := λne W w, (match w with - | inr ((URWLX,Monotone),b,e,a) => + | inr ((URWLX,Directed),b,e,a) => ([∗ list] a' ∈ (region_addrs b (addr_reg.min a e)), (read_write_cond a' interp) ∧ ⌜region_state_pwl_mono W a'⌝) ∗ ([∗ list] a' ∈ (region_addrs (addr_reg.max b a) e), (read_write_cond a' interp) ∧ @@ -603,15 +603,15 @@ Section logrel. [|eauto];solve_addr]). Qed. - Definition isMonotone l := + Definition isDirected l := match l with - | Monotone => true + | Directed => true | _ => false end. Lemma writeLocalAllowed_implies_local W p l b e a: pwl p = true -> - interp W (inr (p, l, b, e, a)) -∗ ⌜isMonotone l = true⌝. + interp W (inr (p, l, b, e, a)) -∗ ⌜isDirected l = true⌝. Proof. intros. iIntros "Hvalid". unfold interp; rewrite fixpoint_interp1_eq /=. @@ -620,7 +620,7 @@ Section logrel. Lemma writeLocalAllowedU_implies_local W p l b e a: pwlU p = true -> - interp W (inr (p, l, b, e, a)) -∗ ⌜isMonotone l = true⌝. + interp W (inr (p, l, b, e, a)) -∗ ⌜isDirected l = true⌝. Proof. intros. iIntros "Hvalid". unfold interp; rewrite fixpoint_interp1_eq /=. @@ -841,7 +841,7 @@ Section logrel. ⌜std W !! a = Some Monotemporary⌝. Proof. intros Hp Hb. iIntros "Hvalid". - iAssert (⌜isMonotone l = true⌝)%I as "%". by iApply writeLocalAllowed_implies_local. + iAssert (⌜isDirected l = true⌝)%I as "%". by iApply writeLocalAllowed_implies_local. eapply withinBounds_le_addr in Hb. unfold interp; rewrite fixpoint_interp1_eq /=. destruct p; simpl in Hp; try congruence; destruct l;try done. @@ -856,7 +856,7 @@ Section logrel. ⌜std W !! a = Some Monotemporary ∨ ∃ w, std W !! a = Some (Uninitialized w)⌝. Proof. intros Hp Hb. iIntros "Hvalid". - iAssert (⌜isMonotone l = true⌝)%I as "%". by iApply writeLocalAllowedU_implies_local. + iAssert (⌜isDirected l = true⌝)%I as "%". by iApply writeLocalAllowedU_implies_local. eapply withinBounds_le_addr in Hb. unfold interp; rewrite fixpoint_interp1_eq /=. destruct p; simpl in Hp; try congruence; destruct l;try done; @@ -878,7 +878,7 @@ Section logrel. ⌜std W !! a' = Some Monotemporary⌝. Proof. intros Hp Hlt Hb. iIntros "Hvalid". - iAssert (⌜isMonotone l = true⌝)%I as "%". by iApply writeLocalAllowedU_implies_local. + iAssert (⌜isDirected l = true⌝)%I as "%". by iApply writeLocalAllowedU_implies_local. eapply withinBounds_le_addr in Hlt. unfold interp; rewrite fixpoint_interp1_eq /=. destruct p; simpl in Hp; try congruence; destruct l;try done; @@ -898,13 +898,13 @@ Section logrel. ([∗ list] a ∈ region_addrs b (if isU p && isLocal l then (addr_reg.min a e) else e), (if writeAllowed p || readAllowedU p then read_write_cond a interp else (∃ (P:D), ⌜(∀ Wv, Persistent (P Wv.1 Wv.2))⌝ ∧ read_cond a P interp)) ∧ ⌜if pwlU p then region_state_pwl_mono W a else region_state_nwl W a l⌝) ∗ - (⌜if pwlU p then isMonotone l else True⌝) ∗ + (⌜if pwlU p then isDirected l else True⌝) ∗ (if isU p && isLocal l then [∗ list] a ∈ region_addrs (addr_reg.max b a) e, read_write_cond a interp ∧ ⌜if pwlU p then region_state_U_pwl_mono W a else (match l with - | Monotone => region_state_U_mono W a + | Directed => region_state_U_mono W a | _ => region_state_U W a end)⌝ else emp%I))%I). Proof. diff --git a/theories/machine_base.v b/theories/machine_base.v index 8f23e16..2f3f185 100644 --- a/theories/machine_base.v +++ b/theories/machine_base.v @@ -21,7 +21,7 @@ Inductive Perm: Type := Inductive Locality: Type := | Global | Local -| Monotone. +| Directed. Definition Cap: Type := (Perm * Locality) * Addr * Addr * Addr. @@ -64,7 +64,7 @@ Notation Mem := (gmap Addr Word). Definition isLocal (l: Locality): bool := match l with - | Local | Monotone => true + | Local | Directed => true | _ => false end. @@ -194,7 +194,7 @@ Definition canStore (p: Perm) (a: Addr) (w: Word): bool := | inr ((_, g), _, _, _) => match g with | Global => true | Local => pwl p - | Monotone => pwl p && leb_addr (canReadUpTo w) a + | Directed => pwl p && leb_addr (canReadUpTo w) a end end. @@ -204,7 +204,7 @@ Definition canStoreU (p: Perm) (a: Addr) (w: Word): bool := | inr ((_, g), _, _, _) => match g with | Global => true | Local => pwlU p - | Monotone => pwlU p && leb_addr (canReadUpTo w) a + | Directed => pwlU p && leb_addr (canReadUpTo w) a end end. @@ -237,9 +237,9 @@ Qed. Definition LocalityFlowsTo (l1 l2: Locality): bool := match l1 with - | Monotone => true + | Directed => true | Local => match l2 with - | Monotone => false + | Directed => false | _ => true end | Global => match l2 with @@ -622,12 +622,12 @@ Proof. set encode := fun l => match l with | Local => 1 | Global => 2 - | Monotone => 3 + | Directed => 3 end%positive. set decode := fun n => match n with | 1 => Some Local | 2 => Some Global - | 3 => Some Monotone + | 3 => Some Directed | _ => None end%positive. eapply (Build_Countable _ _ encode decode). diff --git a/theories/monotone.v b/theories/monotone.v index d7c9832..00ea201 100644 --- a/theories/monotone.v +++ b/theories/monotone.v @@ -295,7 +295,7 @@ Section monotone. iSpecialize ("Hw" $! r W'' with "Hrelated"). iApply "Hw". + iIntros (Hrelated'). - iAssert (future_world Monotone a0 W W'')%I as "Hrelated". + iAssert (future_world Directed a0 W W'')%I as "Hrelated". { iPureIntro. apply related_sts_pub_a_trans_world with W'; auto. } iSpecialize ("Hw" $! r W'' with "Hrelated"). iApply "Hw". @@ -342,7 +342,7 @@ Section monotone. iDestruct "Hw" as "#[Hrw Hst ]". iSplit;eauto. iFrame "#". iDestruct "Hst" as %Hstd. - iPureIntro. eapply (region_state_nwl_monotone W W' _ Monotone); auto. + iPureIntro. eapply (region_state_nwl_monotone W W' _ Directed); auto. * iApply (big_sepL_mono with "Hw2"). iIntros (n y Hsome) "Hw". iDestruct "Hw" as "#[Hrw Hst ]". @@ -396,7 +396,7 @@ Section monotone. iDestruct "Hw" as "#[Hrw Hst ]". iSplit;eauto. iFrame "#". iDestruct "Hst" as %Hstd. - iPureIntro. eapply (region_state_nwl_monotone W W' _ Monotone); auto. + iPureIntro. eapply (region_state_nwl_monotone W W' _ Directed); auto. * iApply (big_sepL_mono with "Hw2"). iIntros (n y Hsome) "Hw". iDestruct "Hw" as "#[Hrw Hst ]". @@ -487,7 +487,7 @@ Section monotone. iSpecialize ("Hw" $! r W'' with "Hrelated"). iApply "Hw". + iIntros (Hrelated'). - iAssert (future_world Monotone a0 W W'')%I as "Hrelated". + iAssert (future_world Directed a0 W W'')%I as "Hrelated". { iPureIntro. apply related_sts_a_trans_world with W';auto. } iSpecialize ("Hw" $! r W'' with "Hrelated"). iApply "Hw". @@ -536,7 +536,7 @@ Section monotone. iDestruct "Hw" as "#[Hrw Hst ]". iSplit;eauto. iFrame "#". iDestruct "Hst" as %Hstd. - iPureIntro. eapply (region_state_nwl_monotone_a W W' _ (addr_reg.min a a0) Monotone); auto. + iPureIntro. eapply (region_state_nwl_monotone_a W W' _ (addr_reg.min a a0) Directed); auto. eapply region_addrs_lookup_le;eauto. apply related_sts_a_weak_world with a;auto. solve_addr. * iApply (big_sepL_mono with "Hw2"). iIntros (n y Hsome) "Hw". @@ -597,7 +597,7 @@ Section monotone. iDestruct "Hw" as "#[Hrw Hst ]". iSplit;eauto. iFrame "#". iDestruct "Hst" as %Hstd. - iPureIntro. eapply (region_state_nwl_monotone_a W W' _ (addr_reg.min a a0) Monotone); auto. + iPureIntro. eapply (region_state_nwl_monotone_a W W' _ (addr_reg.min a a0) Directed); auto. eapply region_addrs_lookup_le;eauto. apply related_sts_a_weak_world with a;auto. solve_addr. * iApply (big_sepL_mono with "Hw2"). iIntros (n y Hsome) "Hw". @@ -626,14 +626,14 @@ Section monotone. iPureIntro. apply region_state_U_pwl_monotone_mono_a with W a;auto. } Qed. - Definition isMonotoneWord (w : Word) := + Definition isDirectedWord (w : Word) := match w with | inl _ => false - | inr (_,l,_,_,_) => isMonotone l + | inr (_,l,_,_,_) => isDirected l end. Lemma interp_monotone_nm W W' w : - ⌜related_sts_priv_world W W'⌝ -∗ ⌜isMonotoneWord w = false⌝ -∗ + ⌜related_sts_priv_world W W'⌝ -∗ ⌜isDirectedWord w = false⌝ -∗ interp W w -∗ interp W' w. Proof. iIntros (Hrelated Hnl) "#Hw". diff --git a/theories/overlay/call.v b/theories/overlay/call.v index 94bbb8c..f5de11e 100644 --- a/theories/overlay/call.v +++ b/theories/overlay/call.v @@ -98,7 +98,7 @@ Section call. ++ [ inl (encodeInstr (Mov (R 0 eq_refl) (inr r_stk))) ; inl (encodeInstr (PromoteU (R 0 eq_refl))) ; inl (encodeInstr (Lea (R 0 eq_refl) (inl (-66)%Z))) - ; inl (encodeInstr (Restrict (R 0 eq_refl) (inl (encodePermPair (E, Monotone))))) + ; inl (encodeInstr (Restrict (R 0 eq_refl) (inl (encodePermPair (E, Directed))))) ] (* Prepare new stack capability for callee *) ++ [inl (encodeInstr (GetA (R 1 eq_refl) r_stk)); diff --git a/theories/overlay/lang.v b/theories/overlay/lang.v index afbd417..71805b9 100644 --- a/theories/overlay/lang.v +++ b/theories/overlay/lang.v @@ -78,7 +78,7 @@ Definition canStore (p: Perm) (a: Addr) (w: base.Word): bool := | inr (Regular ((_, g), _, _, _)) => match g with | Global => true | Local => pwl p - | Monotone => pwl p && leb_addr (canReadUpTo w) a + | Directed => pwl p && leb_addr (canReadUpTo w) a end | inr (Stk _ _ _ _ _) | inr (Ret _ _ _) => pwl p && leb_addr (canReadUpTo w) a end. @@ -89,7 +89,7 @@ Definition canStoreU (p: Perm) (a: Addr) (w: base.Word): bool := | inr (Regular ((_, g), _, _, _)) => match g with | Global => true | Local => pwlU p - | Monotone => pwlU p && leb_addr (canReadUpTo w) a + | Directed => pwlU p && leb_addr (canReadUpTo w) a end | inr (Stk _ _ _ _ _) | inr (Ret _ _ _) => pwlU p && leb_addr (canReadUpTo w) a end. @@ -217,7 +217,7 @@ Section opsem. else (Failed, φ) | inr (Ret b e a) => (Failed, φ) | inr (Stk d p b e a) => - if readAllowed p && withinBounds ((p, Monotone), b, e, a) then + if readAllowed p && withinBounds ((p, Directed), b, e, a) then match stack d ((reg φ, stk φ)::(callstack φ)) with | None => (Failed, φ) | Some m => updatePC (update_reg φ dst (MemLocate m a)) @@ -234,7 +234,7 @@ Section opsem. else (Failed, φ) | inr (Ret b e a) => (Failed, φ) | inr (Stk d p b e a) => - if writeAllowed p && withinBounds ((p, Monotone), b, e, a) && canStore p a (RegLocate (reg φ) src) then + if writeAllowed p && withinBounds ((p, Directed), b, e, a) && canStore p a (RegLocate (reg φ) src) then if nat_eq_dec d (length (callstack φ)) then updatePC (update_stk φ a (RegLocate (reg φ) src)) else match update_stack φ d a (RegLocate (reg φ) src) with @@ -251,7 +251,7 @@ Section opsem. if writeAllowed p && withinBounds ((p, g), b, e, a) then updatePC (update_mem φ a (inl n)) else (Failed, φ) | inr (Ret b e a) => (Failed, φ) | inr (Stk d p b e a) => - if writeAllowed p && withinBounds ((p, Monotone), b, e, a) then + if writeAllowed p && withinBounds ((p, Directed), b, e, a) then if nat_eq_dec d (length (callstack φ)) then updatePC (update_stk φ a (inl n)) else match update_stack φ d a (inl n) with @@ -366,7 +366,7 @@ Section opsem. | inr (Stk d p b e a) => match p with | E => (Failed, φ) - | _ => if PermPairFlowsTo (decodePermPair n) (p, Monotone) then + | _ => if PermPairFlowsTo (decodePermPair n) (p, Directed) then updatePC (update_reg φ dst (inr (Stk d (fst (decodePermPair n)) b e a))) else (Failed, φ) end @@ -392,7 +392,7 @@ Section opsem. | inl n => match p with | E => (Failed, φ) - | _ => if PermPairFlowsTo (decodePermPair n) (p, Monotone) then + | _ => if PermPairFlowsTo (decodePermPair n) (p, Directed) then updatePC (update_reg φ dst (inr (Stk d (fst (decodePermPair n)) b e a))) else (Failed, φ) end @@ -645,7 +645,7 @@ Section opsem. | inr (Regular ((_, g), _, _, _)) => updatePC (update_reg φ dst (inl (encodeLoc g))) | inr (Stk _ _ _ _ _) | inr (Ret _ _ _) => - updatePC (update_reg φ dst (inl (encodeLoc Monotone))) + updatePC (update_reg φ dst (inl (encodeLoc Directed))) end | IsPtr dst r => match RegLocate (reg φ) r with @@ -1041,7 +1041,7 @@ Section opsem. Definition exec_call (φ: ExecConf) (rf: RegName) (rargs: list RegName) pcp pcg (pcb pce pca: Addr): Conf := match pcg with - | Monotone => (Failed, φ) (* Can't store PC if it's monotone because we currently assume heap is above stack *) + | Directed => (Failed, φ) (* Can't store PC if it's monotone because we currently assume heap is above stack *) | _ => match (reg φ) !r! r_stk with | inr (Stk d URWLX b e a) => diff --git a/theories/overlay_cap_lang_sim.v b/theories/overlay_cap_lang_sim.v index 73fc534..1dec7d2 100644 --- a/theories/overlay_cap_lang_sim.v +++ b/theories/overlay_cap_lang_sim.v @@ -52,8 +52,8 @@ Section overlay_to_cap_lang. | inl n => inl n | inr c => match c with | Regular c => inr c - | Stk d p b e a => inr (p, Monotone, b, e, a) - | Ret b e a => inr (E, Monotone, b, e, a) + | Stk d p b e a => inr (p, Directed, b, e, a) + | Ret b e a => inr (E, Directed, b, e, a) end end. @@ -749,7 +749,7 @@ Section overlay_to_cap_lang. end else c1 = lang.Failed /\ c2 = Failed | Some (inr (Stk dd pp bb ee aa)) => - if (readAllowed pp) && (withinBounds (pp, Monotone, bb, ee, aa)) then + if (readAllowed pp) && (withinBounds (pp, Directed, bb, ee, aa)) then exists xstk, stack dd ((reg1, stk)::cs) = Some xstk /\ exists wsrc, xstk !! aa = Some wsrc /\ interp wsrc h stk cs /\ match incrementPC (<[dst:=wsrc]> reg1) with | Some reg1'' => c1 = lang.NextI /\ c2 = NextI /\ reg1'' = reg1' /\ h' = h /\ stk' = stk /\ cs' = cs /\ incrementPC' (<[dst:=translate_word wsrc]> reg2) = Some reg2' /\ mem2' = mem2 @@ -913,7 +913,7 @@ Section overlay_to_cap_lang. destruct (reg_eq_dec dst rr); [subst rr; rewrite lookup_insert; eauto| rewrite lookup_insert_ne; auto]. * intros rr. destruct (reg_eq_dec PC rr); [subst rr; rewrite !lookup_insert; inversion 1; auto| rewrite !(lookup_insert_ne _ PC); auto]. destruct (reg_eq_dec dst rr); [subst rr; rewrite !lookup_insert; inversion 1; auto| rewrite !lookup_insert_ne; auto]. } - { destruct (readAllowed p0 && withinBounds (p0, Monotone, a0, a1, a2)) eqn:Hconds; cycle 1. + { destruct (readAllowed p0 && withinBounds (p0, Directed, a0, a1, a2)) eqn:Hconds; cycle 1. { destruct AA as [-> ->]. econstructor. * eapply sim_expr_exec_inv in Hsexpr. subst K. simpl. repeat econstructor. @@ -1599,12 +1599,12 @@ Section overlay_to_cap_lang. | None => c1 = lang.Failed /\ c2 = Failed | Some aa' => if isU pp then if Addr_le_dec aa' aa then match incrementPC (<[dst:=inr (Stk dd pp bb ee aa')]> reg1) - with Some reg1'' => c1 = lang.NextI /\ c2 = NextI /\ reg1'' = reg1' /\ h' = h /\ stk' = stk /\ cs' = cs /\ incrementPC' (<[dst:=inr (pp, Monotone, bb, ee, aa')]> reg2) = Some reg2' /\ mem2' = mem2 + with Some reg1'' => c1 = lang.NextI /\ c2 = NextI /\ reg1'' = reg1' /\ h' = h /\ stk' = stk /\ cs' = cs /\ incrementPC' (<[dst:=inr (pp, Directed, bb, ee, aa')]> reg2) = Some reg2' /\ mem2' = mem2 | _ => c1 = lang.Failed /\ c2 = Failed end else c1 = lang.Failed /\ c2 = Failed else match incrementPC (<[dst:=inr (Stk dd pp bb ee aa')]> reg1) - with Some reg1'' => c1 = lang.NextI /\ c2 = NextI /\ reg1'' = reg1' /\ h' = h /\ stk' = stk /\ cs' = cs /\ incrementPC' (<[dst:=inr (pp, Monotone, bb, ee, aa')]> reg2) = Some reg2' /\ mem2' = mem2 + with Some reg1'' => c1 = lang.NextI /\ c2 = NextI /\ reg1'' = reg1' /\ h' = h /\ stk' = stk /\ cs' = cs /\ incrementPC' (<[dst:=inr (pp, Directed, bb, ee, aa')]> reg2) = Some reg2' /\ mem2' = mem2 | _ => c1 = lang.Failed /\ c2 = Failed end end @@ -1701,7 +1701,7 @@ Section overlay_to_cap_lang. { destruct p0; inv X1; inv X2; auto. } destruct (isU p0) eqn:HisU. { destruct (Addr_le_dec aa' a2). - - assert (exists w, (<[dst:=inr (Stk n p0 a0 a1 aa')]> reg1) !! PC = Some w /\ (<[dst:=inr (p0, Monotone, a0, a1, aa')]> reg2) !! PC = Some (translate_word w)) as [wpc [HY HZ] ]. + - assert (exists w, (<[dst:=inr (Stk n p0 a0 a1 aa')]> reg1) !! PC = Some w /\ (<[dst:=inr (p0, Directed, a0, a1, aa')]> reg2) !! PC = Some (translate_word w)) as [wpc [HY HZ] ]. { destruct (reg_eq_dec dst PC); [subst dst; rewrite !lookup_insert; eauto|]. rewrite !lookup_insert_ne //. eauto. } destruct (incrementPC (<[dst:=inr (Stk n p0 a0 a1 aa')]> reg1)) as [reg1''|] eqn:Hincrement1; cycle 1. @@ -1720,7 +1720,7 @@ Section overlay_to_cap_lang. instantiate (1 := mem2) in Z3. rewrite Z3 -Z4 in X2. destruct p0; try congruence; inv X1; inv X2; repeat split; auto. - destruct p0; simpl in HisU; try congruence; inv X1; inv X2; auto. } - assert (exists w, (<[dst:=inr (Stk n p0 a0 a1 aa')]> reg1) !! PC = Some w /\ (<[dst:=inr (p0, Monotone, a0, a1, aa')]> reg2) !! PC = Some (translate_word w)) as [wpc [HY HZ] ]. + assert (exists w, (<[dst:=inr (Stk n p0 a0 a1 aa')]> reg1) !! PC = Some w /\ (<[dst:=inr (p0, Directed, a0, a1, aa')]> reg2) !! PC = Some (translate_word w)) as [wpc [HY HZ] ]. { destruct (reg_eq_dec dst PC); [subst dst; rewrite !lookup_insert; eauto|]. rewrite !lookup_insert_ne //. eauto. } rewrite /base.update_reg /= in X1. rewrite /update_reg /= in X2. @@ -1973,7 +1973,7 @@ Section overlay_to_cap_lang. | Some (inr (Stk dd pp bb ee aa)) => if perm_eq_dec pp E then c1 = lang.Failed /\ c2 = Failed else match lang.z_of_argument reg1 r with - | Some nn => if PermPairFlowsTo (decodePermPair nn) (pp, Monotone) then + | Some nn => if PermPairFlowsTo (decodePermPair nn) (pp, Directed) then match incrementPC (<[dst:=inr (Stk dd (decodePermPair nn).1 bb ee aa)]> reg1) with | Some reg1'' => c1 = lang.NextI /\ c2 = NextI /\ reg1'' = reg1' /\ h' = h /\ stk' = stk /\ cs' = cs /\ incrementPC' (<[dst:=inr ((decodePermPair nn), bb, ee, aa)]> reg2) = Some reg2' /\ mem2' = mem2 | None => c1 = lang.Failed /\ c2 = Failed @@ -2046,7 +2046,7 @@ Section overlay_to_cap_lang. rewrite Hc' in Hwr'. rewrite Hwr in H1. rewrite Hwr' in H2. inv H1; inv H2; auto. + simpl in H1, H2; rewrite /base.RegLocate Hwdst in H1; rewrite /RegLocate Hwdst' /= in H2. - assert ((if PermPairFlowsTo (decodePermPair nn) (p0, Monotone) then lang.updatePC (base.update_reg (reg1, h, stk, cs) dst (inr (Stk n (decodePermPair nn).1 a0 a1 a2))) else (lang.Failed, (reg1, h, stk, cs))) = (c1, (reg1', h', stk', cs')) /\ (if PermPairFlowsTo (decodePermPair nn) (p0, Monotone) then updatePC (update_reg (reg2, mem2) dst (inr (decodePermPair nn, a0, a1, a2))) else (Failed, (reg2, mem2))) = (c2, (reg2', mem2'))) as [X1 X2]. + assert ((if PermPairFlowsTo (decodePermPair nn) (p0, Directed) then lang.updatePC (base.update_reg (reg1, h, stk, cs) dst (inr (Stk n (decodePermPair nn).1 a0 a1 a2))) else (lang.Failed, (reg1, h, stk, cs))) = (c1, (reg1', h', stk', cs')) /\ (if PermPairFlowsTo (decodePermPair nn) (p0, Directed) then updatePC (update_reg (reg2, mem2) dst (inr (decodePermPair nn, a0, a1, a2))) else (Failed, (reg2, mem2))) = (c2, (reg2', mem2'))) as [X1 X2]. { destruct r; [inv Hnn; destruct p0; try congruence; auto|]. destruct (Hregsdef r) as [wr [Hwr _] ]. rewrite /= Hwr in Hnn. destruct wr; inv Hnn. @@ -2054,9 +2054,9 @@ Section overlay_to_cap_lang. rewrite Hwr /= in H1. rewrite Hwr' /= in H2. destruct p0; try congruence; auto. } clear H1 H2. - destruct (PermPairFlowsTo (decodePermPair nn) (p0, Monotone)) eqn:Hflowsto; cycle 1. + destruct (PermPairFlowsTo (decodePermPair nn) (p0, Directed)) eqn:Hflowsto; cycle 1. * inv X1; inv X2; auto. - * assert (decodePermPair nn = ((decodePermPair nn).1, Monotone)) as XYZ. + * assert (decodePermPair nn = ((decodePermPair nn).1, Directed)) as XYZ. { rewrite /PermPairFlowsTo /= in Hflowsto. destruct (decodePermPair nn) as [x y]. simpl; f_equal. simpl in Hflowsto. @@ -2178,7 +2178,7 @@ Section overlay_to_cap_lang. - eapply sim_expr_exec_inv in Hsexpr. subst K. repeat econstructor. - rewrite can_step_fill /can_step /=. intros [A | A]; discriminate. } - destruct (PermPairFlowsTo (decodePermPair nn) (p0, Monotone)) eqn:Hflowsto; cycle 1. + destruct (PermPairFlowsTo (decodePermPair nn) (p0, Directed)) eqn:Hflowsto; cycle 1. { destruct AA as [-> ->]. econstructor. - eapply sim_expr_exec_inv in Hsexpr. subst K. repeat econstructor. @@ -2245,7 +2245,7 @@ Section overlay_to_cap_lang. | Some aa2 => if isWithin aa1 aa2 bb ee then match incrementPC (<[dst:=inr (Stk dd pp aa1 aa2 aa)]> reg1) with - | Some reg1'' => c1 = lang.NextI /\ c2 = NextI /\ reg1'' = reg1' /\ h' = h /\ stk' = stk /\ cs' = cs /\ incrementPC' (<[dst:=inr (pp, Monotone, aa1, aa2, aa)]> reg2) = Some reg2' /\ mem2' = mem2 + | Some reg1'' => c1 = lang.NextI /\ c2 = NextI /\ reg1'' = reg1' /\ h' = h /\ stk' = stk /\ cs' = cs /\ incrementPC' (<[dst:=inr (pp, Directed, aa1, aa2, aa)]> reg2) = Some reg2' /\ mem2' = mem2 | _ => c1 = lang.Failed /\ c2 = Failed end else c1 = lang.Failed /\ c2 = Failed @@ -2375,7 +2375,7 @@ Section overlay_to_cap_lang. * destruct (perm_eq_dec p0 E); [inv X1; inv X2; auto|]. replace lang.isWithin with isWithin in X1 by reflexivity. destruct (isWithin aa1 aa2 a0 a1) eqn:HisWithin; [|inv X1; inv X2; auto]. - assert (exists w, (<[dst:=inr (Stk n p0 aa1 aa2 a2)]> reg1) !! PC = Some w /\ (<[dst:=inr (p0, Monotone, aa1, aa2, a2)]> reg2) !! PC = Some (translate_word w)) as [wpc [HY HZ] ]. + assert (exists w, (<[dst:=inr (Stk n p0 aa1 aa2 a2)]> reg1) !! PC = Some w /\ (<[dst:=inr (p0, Directed, aa1, aa2, a2)]> reg2) !! PC = Some (translate_word w)) as [wpc [HY HZ] ]. { destruct (reg_eq_dec dst PC); [subst dst; rewrite !lookup_insert; eauto|]. rewrite !lookup_insert_ne //. eauto. } destruct (incrementPC (<[dst:=inr (Stk n p0 aa1 aa2 a2)]> reg1)) as [reg1''|] eqn:Hincrement1; cycle 1. @@ -2615,7 +2615,7 @@ Section overlay_to_cap_lang. rewrite /RegLocate (Hsregs _ _ Hwr) in H2. destruct wr; [inv H1; inv H2; auto|]. destruct (translate_word_cap c) as [c' Hc']. - rewrite Hc' in H2. set (nn := match c with Ret _ _ _ | Stk _ _ _ _ _ => encodeLoc Monotone | Regular (_, l, _, _, _) => encodeLoc l end). + rewrite Hc' in H2. set (nn := match c with Ret _ _ _ | Stk _ _ _ _ _ => encodeLoc Directed | Regular (_, l, _, _, _) => encodeLoc l end). exists nn. assert (X1: lang.updatePC (<[dst:=inl nn]> reg1, h, stk, cs) = (c1, (reg1', h', stk', cs'))). { rewrite -H1 /base.update_reg /=. subst nn; destruct c; auto. @@ -3322,7 +3322,7 @@ Section overlay_to_cap_lang. if addr_eq_dec aa aa' then exists aa'', (aa + 1)%a = Some aa'' /\ match incrementPC (<[dst:=inr (Stk dd pp bb ee aa'')]> reg1) with - | Some reg1'' => c1 = lang.NextI /\ c2 = NextI /\ reg1'' = reg1' /\ h' = h /\ stk' = (<[aa':=wsrc]> stk) /\ cs' = cs /\ incrementPC' (<[dst:=inr (pp, Monotone, bb, ee, aa'')]> reg2) = Some reg2' /\ mem2' = (<[aa':=translate_word wsrc]> mem2) + | Some reg1'' => c1 = lang.NextI /\ c2 = NextI /\ reg1'' = reg1' /\ h' = h /\ stk' = (<[aa':=wsrc]> stk) /\ cs' = cs /\ incrementPC' (<[dst:=inr (pp, Directed, bb, ee, aa'')]> reg2) = Some reg2' /\ mem2' = (<[aa':=translate_word wsrc]> mem2) | _ => c1 = lang.Failed /\ c2 = Failed end else @@ -3430,7 +3430,7 @@ Section overlay_to_cap_lang. replace (a2 + 1)%a with (Some ^(a2 + 1)%a) in H2 by (clear -Hconds4; solve_addr). rewrite /base.update_reg /base.update_mem /= in H1. rewrite /update_reg /update_mem /= in H2. - assert (exists w, (<[dst:=inr (Stk n p0 a0 a1 ^(a2 + 1)%a)]> reg1) !! PC = Some w /\ (<[dst:=inr (p0, Monotone, a0, a1, ^(a2 + 1)%a)]> reg2) !! PC = Some (translate_word w)) as [wpc [HY HZ] ]. + assert (exists w, (<[dst:=inr (Stk n p0 a0 a1 ^(a2 + 1)%a)]> reg1) !! PC = Some w /\ (<[dst:=inr (p0, Directed, a0, a1, ^(a2 + 1)%a)]> reg2) !! PC = Some (translate_word w)) as [wpc [HY HZ] ]. { destruct (reg_eq_dec dst PC); [subst dst; rewrite !lookup_insert; eauto|]. rewrite !lookup_insert_ne //. eauto. } unfold Stackframe in *. destruct (nat_eq_dec n (length cs)) as [_|KK]; [|elim KK; destruct Hinterpdst; auto]. @@ -3830,7 +3830,7 @@ Section overlay_to_cap_lang. | Some (inr (Stk dd pp bb ee aa)) => if perm_eq_dec pp E then c1 = lang.Failed /\ c2 = Failed else match incrementPC (<[dst:=inr (Stk dd (promote_perm pp) bb (addr_reg.min aa ee) aa)]> reg1) with - | Some reg1'' => c1 = lang.NextI /\ c2 = NextI /\ reg1'' = reg1' /\ h' = h /\ stk' = stk /\ cs' = cs /\ incrementPC' (<[dst:=inr (promote_perm pp, Monotone, bb, addr_reg.min aa ee, aa)]> reg2) = Some reg2' /\ mem2' = mem2 + | Some reg1'' => c1 = lang.NextI /\ c2 = NextI /\ reg1'' = reg1' /\ h' = h /\ stk' = stk /\ cs' = cs /\ incrementPC' (<[dst:=inr (promote_perm pp, Directed, bb, addr_reg.min aa ee, aa)]> reg2) = Some reg2' /\ mem2' = mem2 | None => c1 = lang.Failed /\ c2 = Failed end | _ => c1 = lang.Failed /\ c2 = Failed @@ -3864,7 +3864,7 @@ Section overlay_to_cap_lang. - destruct (perm_eq_dec p0 E); [inv H1; inv H2; auto|]. rewrite /base.update_reg /= in H1. rewrite /update_reg /= in H2. - assert (exists w, (<[dst:=inr (Stk n (promote_perm p0) a0 (addr_reg.min a2 a1) a2)]> reg1) !! PC = Some w /\ (<[dst:=inr (promote_perm p0, Monotone, a0, addr_reg.min a2 a1, a2)]> reg2) !! PC = Some (translate_word w)) as [wpc [HY HZ] ]. + assert (exists w, (<[dst:=inr (Stk n (promote_perm p0) a0 (addr_reg.min a2 a1) a2)]> reg1) !! PC = Some w /\ (<[dst:=inr (promote_perm p0, Directed, a0, addr_reg.min a2 a1, a2)]> reg2) !! PC = Some (translate_word w)) as [wpc [HY HZ] ]. { destruct (reg_eq_dec dst PC); [subst dst; rewrite !lookup_insert; eauto|]. rewrite !lookup_insert_ne //. eauto. } destruct (incrementPC (<[dst:=inr (Stk n (promote_perm p0) a0 (addr_reg.min a2 a1) a2)]> reg1)) as [reg1''|] eqn:Hincrement1; cycle 1. @@ -4050,8 +4050,8 @@ Section overlay_to_cap_lang. exists rwi, mem !! ai = Some (translate_word rwi) /\ reg' !! r = Some rwi), rtc erased_step - ([Seq (Instr Executable)], (<[PC:=inr (RX, Monotone, br, er, ar)]> (<[call.r_stk:=inr (URWLX, Monotone, bstk, estk, astk)]> reg), mem)) - ([Seq (Instr Executable)], (<[PC:=inr (RX, Monotone, br, er, ar_final)]> (<[call.r_stk:=inr (URWLX, Monotone, bstk, estk, astk_final)]> (foldr (fun r reg => <[r:= translate_word (base.RegLocate reg' r)]> reg) reg rlist)), mem)). + ([Seq (Instr Executable)], (<[PC:=inr (RX, Directed, br, er, ar)]> (<[call.r_stk:=inr (URWLX, Directed, bstk, estk, astk)]> reg), mem)) + ([Seq (Instr Executable)], (<[PC:=inr (RX, Directed, br, er, ar_final)]> (<[call.r_stk:=inr (URWLX, Directed, bstk, estk, astk_final)]> (foldr (fun r reg => <[r:= translate_word (base.RegLocate reg' r)]> reg) reg rlist)), mem)). Proof. induction rlist; intros. - simpl. simpl in Hstkfinal. assert (astk = astk_final) as <- by (clear -Hstkfinal; solve_addr). @@ -4223,8 +4223,8 @@ Section overlay_to_cap_lang. (Hcanstore: forall i wi, wlist !! i = Some wi -> lang.canStoreU URWLX (^(astk + Z.of_nat i)%a) (word_of_argument reg1 wi) = true) (Hnotin: inr PC ∉ wlist /\ inr call.r_stk ∉ wlist), rtc erased_step - ([Seq (Instr Executable)], (<[PC:=inr (pr, gr, br, er, ar)]> (<[call.r_stk:=inr (URWLX, Monotone, bstk, estk, astk)]> reg), mem)) - ([Seq (Instr Executable)], (<[PC:=inr (pr, gr, br, er, ar_final)]> (<[call.r_stk:=inr (URWLX, Monotone, bstk, estk, astk_final)]> reg), (push_words_no_check mem astk (map (fun w => translate_word (word_of_argument reg1 w)) wlist)).2)). + ([Seq (Instr Executable)], (<[PC:=inr (pr, gr, br, er, ar)]> (<[call.r_stk:=inr (URWLX, Directed, bstk, estk, astk)]> reg), mem)) + ([Seq (Instr Executable)], (<[PC:=inr (pr, gr, br, er, ar_final)]> (<[call.r_stk:=inr (URWLX, Directed, bstk, estk, astk_final)]> reg), (push_words_no_check mem astk (map (fun w => translate_word (word_of_argument reg1 w)) wlist)).2)). Proof. induction wlist; intros. - simpl. simpl in Hstkfinal, Harfinal. @@ -4232,7 +4232,7 @@ Section overlay_to_cap_lang. replace ar_final with ar by (clear -Harfinal; solve_addr). eapply rtc_refl. - simpl map. rewrite push_words_no_check_cons. - eapply rtc_transitive with (y := ([Seq (Instr Executable)], (<[PC:=inr (pr, gr, br, er, ^(ar + 1)%a)]> (<[call.r_stk:=inr (URWLX, Monotone, bstk, estk, ^(astk + 1)%a)]> reg), <[astk:=translate_word (word_of_argument reg1 a)]> mem))). + eapply rtc_transitive with (y := ([Seq (Instr Executable)], (<[PC:=inr (pr, gr, br, er, ^(ar + 1)%a)]> (<[call.r_stk:=inr (URWLX, Directed, bstk, estk, ^(astk + 1)%a)]> reg), <[astk:=translate_word (word_of_argument reg1 a)]> mem))). + eapply rtc_l. * econstructor. econstructor; eauto. { instantiate (2 := []). instantiate (3 := []). reflexivity. } @@ -4254,7 +4254,7 @@ Section overlay_to_cap_lang. rewrite /update_reg /update_mem /=. generalize (Hcanstore 0 a eq_refl). intros Hacanstore. replace (^(astk + 0%nat)%a) with astk in Hacanstore by (clear; solve_addr). rewrite canStoreU_translate_word in Hacanstore. - assert (match a with | inl n => inl n | inr rsrc => match <[PC:=inr (pr, gr, br, er, ar)]> (<[call.r_stk:=inr (URWLX, Monotone, bstk, estk, astk)]> reg) !! rsrc with | Some w => w | None => inl 0%Z end end = (translate_word (word_of_argument reg1 a))) as ->. + assert (match a with | inl n => inl n | inr rsrc => match <[PC:=inr (pr, gr, br, er, ar)]> (<[call.r_stk:=inr (URWLX, Directed, bstk, estk, astk)]> reg) !! rsrc with | Some w => w | None => inl 0%Z end end = (translate_word (word_of_argument reg1 a))) as ->. { destruct a; [reflexivity|]. destruct Hnotin as [Hnotin1 Hnotin2]. eapply not_elem_of_cons in Hnotin1. destruct Hnotin1 as [Hnotin1 Hnotin1']. @@ -4450,7 +4450,7 @@ Section overlay_to_cap_lang. end else c1 = lang.Failed /\ c2 = Failed | Some (inr (Stk dd pp bb ee aa)) => - if (readAllowed pp) && (withinBounds (pp, Monotone, bb, ee, aa)) then + if (readAllowed pp) && (withinBounds (pp, Directed, bb, ee, aa)) then exists xstk, stack dd ((reg1, stk)::cs) = Some xstk /\ exists wsrc, xstk !! aa = Some wsrc /\ interp wsrc h stk cs /\ match incrementPC (<[dst:=wsrc]> reg1) with | Some reg1'' => c1 = lang.NextI /\ c2 = NextI /\ reg1'' = reg1' /\ h' = h /\ stk' = stk /\ cs' = cs /\ incrementPC' (<[dst:=translate_word wsrc]> reg2) = Some reg2' /\ mem2' = mem2 @@ -4613,7 +4613,7 @@ Section overlay_to_cap_lang. destruct (reg_eq_dec dst rr); [subst rr; rewrite lookup_insert; eauto| rewrite lookup_insert_ne; auto]. * intros rr. destruct (reg_eq_dec PC rr); [subst rr; rewrite !lookup_insert; inversion 1; auto| rewrite !(lookup_insert_ne _ PC); auto]. destruct (reg_eq_dec dst rr); [subst rr; rewrite !lookup_insert; inversion 1; auto| rewrite !lookup_insert_ne; auto]. } - { destruct (readAllowed p0 && withinBounds (p0, Monotone, a0, a1, a2)) eqn:Hconds; cycle 1. + { destruct (readAllowed p0 && withinBounds (p0, Directed, a0, a1, a2)) eqn:Hconds; cycle 1. { destruct AA as [-> ->]. econstructor. * eapply sim_expr_exec_inv in Hsexpr. subst K. simpl. repeat econstructor. @@ -5293,12 +5293,12 @@ Section overlay_to_cap_lang. | None => c1 = lang.Failed /\ c2 = Failed | Some aa' => if isU pp then if Addr_le_dec aa' aa then match incrementPC (<[dst:=inr (Stk dd pp bb ee aa')]> reg1) - with Some reg1'' => c1 = lang.NextI /\ c2 = NextI /\ reg1'' = reg1' /\ h' = h /\ stk' = stk /\ cs' = cs /\ incrementPC' (<[dst:=inr (pp, Monotone, bb, ee, aa')]> reg2) = Some reg2' /\ mem2' = mem2 + with Some reg1'' => c1 = lang.NextI /\ c2 = NextI /\ reg1'' = reg1' /\ h' = h /\ stk' = stk /\ cs' = cs /\ incrementPC' (<[dst:=inr (pp, Directed, bb, ee, aa')]> reg2) = Some reg2' /\ mem2' = mem2 | _ => c1 = lang.Failed /\ c2 = Failed end else c1 = lang.Failed /\ c2 = Failed else match incrementPC (<[dst:=inr (Stk dd pp bb ee aa')]> reg1) - with Some reg1'' => c1 = lang.NextI /\ c2 = NextI /\ reg1'' = reg1' /\ h' = h /\ stk' = stk /\ cs' = cs /\ incrementPC' (<[dst:=inr (pp, Monotone, bb, ee, aa')]> reg2) = Some reg2' /\ mem2' = mem2 + with Some reg1'' => c1 = lang.NextI /\ c2 = NextI /\ reg1'' = reg1' /\ h' = h /\ stk' = stk /\ cs' = cs /\ incrementPC' (<[dst:=inr (pp, Directed, bb, ee, aa')]> reg2) = Some reg2' /\ mem2' = mem2 | _ => c1 = lang.Failed /\ c2 = Failed end end @@ -5395,7 +5395,7 @@ Section overlay_to_cap_lang. { destruct p0; inv X1; inv X2; auto. } destruct (isU p0) eqn:HisU. { destruct (Addr_le_dec aa' a2). - - assert (exists w, (<[dst:=inr (Stk n p0 a0 a1 aa')]> reg1) !! PC = Some w /\ (<[dst:=inr (p0, Monotone, a0, a1, aa')]> reg2) !! PC = Some (translate_word w)) as [wpc [HY HZ] ]. + - assert (exists w, (<[dst:=inr (Stk n p0 a0 a1 aa')]> reg1) !! PC = Some w /\ (<[dst:=inr (p0, Directed, a0, a1, aa')]> reg2) !! PC = Some (translate_word w)) as [wpc [HY HZ] ]. { destruct (reg_eq_dec dst PC); [subst dst; rewrite !lookup_insert; eauto|]. rewrite !lookup_insert_ne //. eauto. } destruct (incrementPC (<[dst:=inr (Stk n p0 a0 a1 aa')]> reg1)) as [reg1''|] eqn:Hincrement1; cycle 1. @@ -5414,7 +5414,7 @@ Section overlay_to_cap_lang. instantiate (1 := mem2) in Z3. rewrite Z3 -Z4 in X2. destruct p0; try congruence; inv X1; inv X2; repeat split; auto. - destruct p0; simpl in HisU; try congruence; inv X1; inv X2; auto. } - assert (exists w, (<[dst:=inr (Stk n p0 a0 a1 aa')]> reg1) !! PC = Some w /\ (<[dst:=inr (p0, Monotone, a0, a1, aa')]> reg2) !! PC = Some (translate_word w)) as [wpc [HY HZ] ]. + assert (exists w, (<[dst:=inr (Stk n p0 a0 a1 aa')]> reg1) !! PC = Some w /\ (<[dst:=inr (p0, Directed, a0, a1, aa')]> reg2) !! PC = Some (translate_word w)) as [wpc [HY HZ] ]. { destruct (reg_eq_dec dst PC); [subst dst; rewrite !lookup_insert; eauto|]. rewrite !lookup_insert_ne //. eauto. } rewrite /base.update_reg /= in X1. rewrite /update_reg /= in X2. @@ -5656,7 +5656,7 @@ Section overlay_to_cap_lang. | Some (inr (Stk dd pp bb ee aa)) => if perm_eq_dec pp E then c1 = lang.Failed /\ c2 = Failed else match lang.z_of_argument reg1 r with - | Some nn => if PermPairFlowsTo (decodePermPair nn) (pp, Monotone) then + | Some nn => if PermPairFlowsTo (decodePermPair nn) (pp, Directed) then match incrementPC (<[dst:=inr (Stk dd (decodePermPair nn).1 bb ee aa)]> reg1) with | Some reg1'' => c1 = lang.NextI /\ c2 = NextI /\ reg1'' = reg1' /\ h' = h /\ stk' = stk /\ cs' = cs /\ incrementPC' (<[dst:=inr ((decodePermPair nn), bb, ee, aa)]> reg2) = Some reg2' /\ mem2' = mem2 | None => c1 = lang.Failed /\ c2 = Failed @@ -5729,7 +5729,7 @@ Section overlay_to_cap_lang. rewrite Hc' in Hwr'. rewrite Hwr in H1. rewrite Hwr' in H2. inv H1; inv H2; auto. + simpl in H1, H2; rewrite /base.RegLocate Hwdst in H1; rewrite /RegLocate Hwdst' /= in H2. - assert ((if PermPairFlowsTo (decodePermPair nn) (p0, Monotone) then lang.updatePC (base.update_reg (reg1, h, stk, cs) dst (inr (Stk n (decodePermPair nn).1 a0 a1 a2))) else (lang.Failed, (reg1, h, stk, cs))) = (c1, (reg1', h', stk', cs')) /\ (if PermPairFlowsTo (decodePermPair nn) (p0, Monotone) then updatePC (update_reg (reg2, mem2) dst (inr (decodePermPair nn, a0, a1, a2))) else (Failed, (reg2, mem2))) = (c2, (reg2', mem2'))) as [X1 X2]. + assert ((if PermPairFlowsTo (decodePermPair nn) (p0, Directed) then lang.updatePC (base.update_reg (reg1, h, stk, cs) dst (inr (Stk n (decodePermPair nn).1 a0 a1 a2))) else (lang.Failed, (reg1, h, stk, cs))) = (c1, (reg1', h', stk', cs')) /\ (if PermPairFlowsTo (decodePermPair nn) (p0, Directed) then updatePC (update_reg (reg2, mem2) dst (inr (decodePermPair nn, a0, a1, a2))) else (Failed, (reg2, mem2))) = (c2, (reg2', mem2'))) as [X1 X2]. { destruct r; [inv Hnn; destruct p0; try congruence; auto|]. destruct (Hregsdef r) as [wr [Hwr _] ]. rewrite /= Hwr in Hnn. destruct wr; inv Hnn. @@ -5737,9 +5737,9 @@ Section overlay_to_cap_lang. rewrite Hwr /= in H1. rewrite Hwr' /= in H2. destruct p0; try congruence; auto. } clear H1 H2. - destruct (PermPairFlowsTo (decodePermPair nn) (p0, Monotone)) eqn:Hflowsto; cycle 1. + destruct (PermPairFlowsTo (decodePermPair nn) (p0, Directed)) eqn:Hflowsto; cycle 1. * inv X1; inv X2; auto. - * assert (decodePermPair nn = ((decodePermPair nn).1, Monotone)) as XYZ. + * assert (decodePermPair nn = ((decodePermPair nn).1, Directed)) as XYZ. { rewrite /PermPairFlowsTo /= in Hflowsto. destruct (decodePermPair nn) as [x y]. simpl; f_equal. simpl in Hflowsto. @@ -5852,7 +5852,7 @@ Section overlay_to_cap_lang. - eapply sim_expr_exec_inv in Hsexpr. subst K. repeat econstructor. - rewrite can_step_fill /can_step /=. intros [A | A]; discriminate. } - destruct (PermPairFlowsTo (decodePermPair nn) (p0, Monotone)) eqn:Hflowsto; cycle 1. + destruct (PermPairFlowsTo (decodePermPair nn) (p0, Directed)) eqn:Hflowsto; cycle 1. { destruct AA as [-> ->]. econstructor. - eapply sim_expr_exec_inv in Hsexpr. subst K. repeat econstructor. @@ -5943,7 +5943,7 @@ Section overlay_to_cap_lang. | Some aa2 => if isWithin aa1 aa2 bb ee then match incrementPC (<[dst:=inr (Stk dd pp aa1 aa2 aa)]> reg1) with - | Some reg1'' => c1 = lang.NextI /\ c2 = NextI /\ reg1'' = reg1' /\ h' = h /\ stk' = stk /\ cs' = cs /\ incrementPC' (<[dst:=inr (pp, Monotone, aa1, aa2, aa)]> reg2) = Some reg2' /\ mem2' = mem2 + | Some reg1'' => c1 = lang.NextI /\ c2 = NextI /\ reg1'' = reg1' /\ h' = h /\ stk' = stk /\ cs' = cs /\ incrementPC' (<[dst:=inr (pp, Directed, aa1, aa2, aa)]> reg2) = Some reg2' /\ mem2' = mem2 | _ => c1 = lang.Failed /\ c2 = Failed end else c1 = lang.Failed /\ c2 = Failed @@ -6073,7 +6073,7 @@ Section overlay_to_cap_lang. * destruct (perm_eq_dec p0 E); [inv X1; inv X2; auto|]. replace lang.isWithin with isWithin in X1 by reflexivity. destruct (isWithin aa1 aa2 a0 a1) eqn:HisWithin; [|inv X1; inv X2; auto]. - assert (exists w, (<[dst:=inr (Stk n p0 aa1 aa2 a2)]> reg1) !! PC = Some w /\ (<[dst:=inr (p0, Monotone, aa1, aa2, a2)]> reg2) !! PC = Some (translate_word w)) as [wpc [HY HZ] ]. + assert (exists w, (<[dst:=inr (Stk n p0 aa1 aa2 a2)]> reg1) !! PC = Some w /\ (<[dst:=inr (p0, Directed, aa1, aa2, a2)]> reg2) !! PC = Some (translate_word w)) as [wpc [HY HZ] ]. { destruct (reg_eq_dec dst PC); [subst dst; rewrite !lookup_insert; eauto|]. rewrite !lookup_insert_ne //. eauto. } destruct (incrementPC (<[dst:=inr (Stk n p0 aa1 aa2 a2)]> reg1)) as [reg1''|] eqn:Hincrement1; cycle 1. @@ -6313,7 +6313,7 @@ Section overlay_to_cap_lang. rewrite /RegLocate (Hsregs _ _ Hwr) in H2. destruct wr; [inv H1; inv H2; auto|]. destruct (translate_word_cap c) as [c' Hc']. - rewrite Hc' in H2. set (nn := match c with Ret _ _ _ | Stk _ _ _ _ _ => encodeLoc Monotone | Regular (_, l, _, _, _) => encodeLoc l end). + rewrite Hc' in H2. set (nn := match c with Ret _ _ _ | Stk _ _ _ _ _ => encodeLoc Directed | Regular (_, l, _, _, _) => encodeLoc l end). exists nn. assert (X1: lang.updatePC (<[dst:=inl nn]> reg1, h, stk, cs) = (c1, (reg1', h', stk', cs'))). { rewrite -H1 /base.update_reg /=. subst nn; destruct c; auto. @@ -7018,7 +7018,7 @@ Section overlay_to_cap_lang. if addr_eq_dec aa aa' then exists aa'', (aa + 1)%a = Some aa'' /\ match incrementPC (<[dst:=inr (Stk dd pp bb ee aa'')]> reg1) with - | Some reg1'' => c1 = lang.NextI /\ c2 = NextI /\ reg1'' = reg1' /\ h' = h /\ stk' = (<[aa':=wsrc]> stk) /\ cs' = cs /\ incrementPC' (<[dst:=inr (pp, Monotone, bb, ee, aa'')]> reg2) = Some reg2' /\ mem2' = (<[aa':=translate_word wsrc]> mem2) + | Some reg1'' => c1 = lang.NextI /\ c2 = NextI /\ reg1'' = reg1' /\ h' = h /\ stk' = (<[aa':=wsrc]> stk) /\ cs' = cs /\ incrementPC' (<[dst:=inr (pp, Directed, bb, ee, aa'')]> reg2) = Some reg2' /\ mem2' = (<[aa':=translate_word wsrc]> mem2) | _ => c1 = lang.Failed /\ c2 = Failed end else @@ -7126,7 +7126,7 @@ Section overlay_to_cap_lang. replace (a2 + 1)%a with (Some ^(a2 + 1)%a) in H2 by (clear -Hconds4; solve_addr). rewrite /base.update_reg /base.update_mem /= in H1. rewrite /update_reg /update_mem /= in H2. - assert (exists w, (<[dst:=inr (Stk n p0 a0 a1 ^(a2 + 1)%a)]> reg1) !! PC = Some w /\ (<[dst:=inr (p0, Monotone, a0, a1, ^(a2 + 1)%a)]> reg2) !! PC = Some (translate_word w)) as [wpc [HY HZ] ]. + assert (exists w, (<[dst:=inr (Stk n p0 a0 a1 ^(a2 + 1)%a)]> reg1) !! PC = Some w /\ (<[dst:=inr (p0, Directed, a0, a1, ^(a2 + 1)%a)]> reg2) !! PC = Some (translate_word w)) as [wpc [HY HZ] ]. { destruct (reg_eq_dec dst PC); [subst dst; rewrite !lookup_insert; eauto|]. rewrite !lookup_insert_ne //. eauto. } unfold Stackframe in *. destruct (nat_eq_dec n (length cs)) as [_|KK]; [|elim KK; destruct Hinterpdst; auto]. @@ -7532,7 +7532,7 @@ Section overlay_to_cap_lang. | Some (inr (Stk dd pp bb ee aa)) => if perm_eq_dec pp E then c1 = lang.Failed /\ c2 = Failed else match incrementPC (<[dst:=inr (Stk dd (promote_perm pp) bb (addr_reg.min aa ee) aa)]> reg1) with - | Some reg1'' => c1 = lang.NextI /\ c2 = NextI /\ reg1'' = reg1' /\ h' = h /\ stk' = stk /\ cs' = cs /\ incrementPC' (<[dst:=inr (promote_perm pp, Monotone, bb, addr_reg.min aa ee, aa)]> reg2) = Some reg2' /\ mem2' = mem2 + | Some reg1'' => c1 = lang.NextI /\ c2 = NextI /\ reg1'' = reg1' /\ h' = h /\ stk' = stk /\ cs' = cs /\ incrementPC' (<[dst:=inr (promote_perm pp, Directed, bb, addr_reg.min aa ee, aa)]> reg2) = Some reg2' /\ mem2' = mem2 | None => c1 = lang.Failed /\ c2 = Failed end | _ => c1 = lang.Failed /\ c2 = Failed @@ -7566,7 +7566,7 @@ Section overlay_to_cap_lang. - destruct (perm_eq_dec p0 E); [inv H1; inv H2; auto|]. rewrite /base.update_reg /= in H1. rewrite /update_reg /= in H2. - assert (exists w, (<[dst:=inr (Stk n (promote_perm p0) a0 (addr_reg.min a2 a1) a2)]> reg1) !! PC = Some w /\ (<[dst:=inr (promote_perm p0, Monotone, a0, addr_reg.min a2 a1, a2)]> reg2) !! PC = Some (translate_word w)) as [wpc [HY HZ] ]. + assert (exists w, (<[dst:=inr (Stk n (promote_perm p0) a0 (addr_reg.min a2 a1) a2)]> reg1) !! PC = Some w /\ (<[dst:=inr (promote_perm p0, Directed, a0, addr_reg.min a2 a1, a2)]> reg2) !! PC = Some (translate_word w)) as [wpc [HY HZ] ]. { destruct (reg_eq_dec dst PC); [subst dst; rewrite !lookup_insert; eauto|]. rewrite !lookup_insert_ne //. eauto. } destruct (incrementPC (<[dst:=inr (Stk n (promote_perm p0) a0 (addr_reg.min a2 a1) a2)]> reg1)) as [reg1''|] eqn:Hincrement1; cycle 1. @@ -7994,7 +7994,7 @@ Section overlay_to_cap_lang. rewrite HPC in H5; inv H5. generalize (Hsregs _ _ HPC). intros HPC'. rewrite /base.RegLocate HPC in H6. - assert (Hgnotmono: g <> Monotone). + assert (Hgnotmono: g <> Directed). { intro X; rewrite /exec_call X in H9. inv H9. } rewrite /exec_call /base.RegLocate Hwstk in H9. assert (Hstkrange1: (a0 < a2)%a). @@ -8029,9 +8029,9 @@ Section overlay_to_cap_lang. reg1), clear_stk saved_stk ^(a2 + 99)%a) :: cs)) = (lang.NextI, σ2)) by (destruct g; try congruence; auto). clear H9. revert H1; intro H9. simpl. destruct (push_words_no_check (<[a2:=inl 0%Z]> mem2) ^(a2 + 1)%a (map (λ w : Z + RegName, translate_word (word_of_argument reg1 w)) (map inr (list_difference all_registers [PC; call.r_stk])))) as [aa mem2'] eqn:Hpush1. - destruct ((push_words_no_check (<[^(a2 + 32)%a:=inr (URWLX, Monotone, a0, a1, ^(a2 + 32)%a)]> mem2') ^(a2 + 33)%a (map (λ w : Z + RegName, translate_word (word_of_argument reg1 w)) ([inl (encodeInstr (Mov (R 1 eq_refl) (inr PC))); inl (encodeInstr (Lea (R 1 eq_refl) (inl (-1)%Z))); inl (encodeInstr (Load call.r_stk (R 1 eq_refl)))] ++ map inl call.pop_env_instrs ++ [inl (encodeInstr (LoadU PC call.r_stk (inl (-1)%Z)))])))) as [ab mem2''] eqn:Hpush2. - destruct (push_words_no_check (<[^(a2 + 99)%a:=inr (E, Monotone, a0, ^(a2 + 99)%a, ^(a2 + 33)%a)]> (<[a2:=inr (p, g, b, e, ^(a + (140 + length rargs))%a)]> mem2'')) ^(a2 + 100)%a (map (λ r : RegName, translate_word (base.RegLocate reg1 r)) rargs)) as [ac mem2'''] eqn:Hpush3. - set (final_state := ([Seq (Instr NextI)], (<[PC:=updatePcPerm (translate_word wrf)]> (<[call.r_stk:=inr (URWLX, Monotone, ^(a2 + 99)%a, a1, ^(Some astkend)%a)]> (<[rf:=translate_word wrf]> (gset_to_gmap (inl 0%Z) (list_to_set all_registers)))), mem2'''))). + destruct ((push_words_no_check (<[^(a2 + 32)%a:=inr (URWLX, Directed, a0, a1, ^(a2 + 32)%a)]> mem2') ^(a2 + 33)%a (map (λ w : Z + RegName, translate_word (word_of_argument reg1 w)) ([inl (encodeInstr (Mov (R 1 eq_refl) (inr PC))); inl (encodeInstr (Lea (R 1 eq_refl) (inl (-1)%Z))); inl (encodeInstr (Load call.r_stk (R 1 eq_refl)))] ++ map inl call.pop_env_instrs ++ [inl (encodeInstr (LoadU PC call.r_stk (inl (-1)%Z)))])))) as [ab mem2''] eqn:Hpush2. + destruct (push_words_no_check (<[^(a2 + 99)%a:=inr (E, Directed, a0, ^(a2 + 99)%a, ^(a2 + 33)%a)]> (<[a2:=inr (p, g, b, e, ^(a + (140 + length rargs))%a)]> mem2'')) ^(a2 + 100)%a (map (λ r : RegName, translate_word (base.RegLocate reg1 r)) rargs)) as [ac mem2'''] eqn:Hpush3. + set (final_state := ([Seq (Instr NextI)], (<[PC:=updatePcPerm (translate_word wrf)]> (<[call.r_stk:=inr (URWLX, Directed, ^(a2 + 99)%a, a1, ^(Some astkend)%a)]> (<[rf:=translate_word wrf]> (gset_to_gmap (inl 0%Z) (list_to_set all_registers)))), mem2'''))). exists final_state. split. { eapply tc_rtc_r. - eapply tc_once. econstructor. econstructor. @@ -8378,7 +8378,7 @@ Section overlay_to_cap_lang. + econstructor; eauto. * instantiate (2 := []). reflexivity. * econstructor. } - simpl. assert (Hcode2: forall i, i < 39 + length rargs -> mem2'' !! (^(a + (102 + i))%a) = translate_word <$> ([inl (encodeInstr (Mov (R 0 eq_refl) (inr call.r_stk))); inl (encodeInstr (PromoteU (R 0 eq_refl))); inl (encodeInstr (Lea (R 0 eq_refl) (inl (-66)%Z))); inl (encodeInstr (Restrict (R 0 eq_refl) (inl (encodePermPair (E, Monotone)))))] ++ [inl (encodeInstr (GetA (R 1 eq_refl) call.r_stk)); inl (encodeInstr (GetE (R 2 eq_refl) call.r_stk)); inl (encodeInstr (Subseg call.r_stk (inr (R 1 eq_refl)) (inr (R 2 eq_refl))))] ++ call.push_instrs [inr (R 0 eq_refl)] ++ call.push_instrs (map inr rargs) ++ call.rclear_instrs (list_difference all_registers [PC; rf; call.r_stk]) ++ [inl (encodeInstr (Jmp rf))]) !! i). + simpl. assert (Hcode2: forall i, i < 39 + length rargs -> mem2'' !! (^(a + (102 + i))%a) = translate_word <$> ([inl (encodeInstr (Mov (R 0 eq_refl) (inr call.r_stk))); inl (encodeInstr (PromoteU (R 0 eq_refl))); inl (encodeInstr (Lea (R 0 eq_refl) (inl (-66)%Z))); inl (encodeInstr (Restrict (R 0 eq_refl) (inl (encodePermPair (E, Directed)))))] ++ [inl (encodeInstr (GetA (R 1 eq_refl) call.r_stk)); inl (encodeInstr (GetE (R 2 eq_refl) call.r_stk)); inl (encodeInstr (Subseg call.r_stk (inr (R 1 eq_refl)) (inr (R 2 eq_refl))))] ++ call.push_instrs [inr (R 0 eq_refl)] ++ call.push_instrs (map inr rargs) ++ call.rclear_instrs (list_difference all_registers [PC; rf; call.r_stk]) ++ [inl (encodeInstr (Jmp rf))]) !! i). { intros. erewrite Hmem2''. - generalize (Hcode (102 + i) ltac:(lia)). intros [ai [Hai Hinstri] ]. @@ -8755,7 +8755,7 @@ Section overlay_to_cap_lang. rewrite insert_insert /snd. rewrite (Hsregs _ _ Hwrf). auto. } } simpl app. rewrite Hpush3 /snd /final_state. - assert (<[PC:=updatePcPerm (translate_word wrf)]> (<[call.r_stk:=inr (URWLX, Monotone, ^(a2 + 99)%a, a1, ^(a2 + (100 + length rargs))%a)]> (foldl (λ (reg : Reg) (r : RegName), <[r:=inl 0%Z]> reg) reg2 (list_difference all_registers [PC; rf; call.r_stk]))) = <[PC:=updatePcPerm (translate_word wrf)]> (<[call.r_stk:=inr (URWLX, Monotone, ^(a2 + 99)%a, a1, ^(Some astkend)%a)]> (<[rf:=translate_word wrf]> (gset_to_gmap (inl 0%Z) (list_to_set all_registers))))) as YZ. + assert (<[PC:=updatePcPerm (translate_word wrf)]> (<[call.r_stk:=inr (URWLX, Directed, ^(a2 + 99)%a, a1, ^(a2 + (100 + length rargs))%a)]> (foldl (λ (reg : Reg) (r : RegName), <[r:=inl 0%Z]> reg) reg2 (list_difference all_registers [PC; rf; call.r_stk]))) = <[PC:=updatePcPerm (translate_word wrf)]> (<[call.r_stk:=inr (URWLX, Directed, ^(a2 + 99)%a, a1, ^(Some astkend)%a)]> (<[rf:=translate_word wrf]> (gset_to_gmap (inl 0%Z) (list_to_set all_registers))))) as YZ. { eapply map_eq; intros r. destruct (reg_eq_dec r PC); [subst r; rewrite !lookup_insert //|rewrite !(lookup_insert_ne _ PC r); auto]. destruct (reg_eq_dec r call.r_stk); [subst r; rewrite !lookup_insert Hastkend //|]. @@ -9628,7 +9628,7 @@ Local Transparent all_registers. rewrite /update_reg /cap_lang.mem /reg /MemLocate. generalize (Hstksim0 _ _ HnewPC'). intros [AA [AB AC] ]. rewrite AA. - assert (ZZ: (foldr (λ (r : RegName) (reg : Reg), <[r:=translate_word (base.RegLocate nregs r)]> reg) (<[R 1 eq_refl:=inr (RX, Monotone, br, er, ^(na_stk + 32)%a)]> reg2) rlist) = <[PC := reg2 !r! PC]> (<[call.r_stk := reg2 !r! call.r_stk]> (translate_word <$> nregs))). + assert (ZZ: (foldr (λ (r : RegName) (reg : Reg), <[r:=translate_word (base.RegLocate nregs r)]> reg) (<[R 1 eq_refl:=inr (RX, Directed, br, er, ^(na_stk + 32)%a)]> reg2) rlist) = <[PC := reg2 !r! PC]> (<[call.r_stk := reg2 !r! call.r_stk]> (translate_word <$> nregs))). { eapply map_eq. intros. assert (Hdup: NoDup rlist). { subst rlist. apply NoDup_list_difference. @@ -9658,12 +9658,12 @@ Local Transparent all_registers. rewrite ZZ. rewrite insert_insert. rewrite (insert_commute _ call.r_stk PC) //. rewrite !insert_insert /=. - assert (YY: updatePC (<[PC:=inr (pcp, pcg, pcb, pce, pcam1)]> (<[call.r_stk:=inr (URWLX, Monotone, br, ne_stk, ^(na_stk + 1)%a)]> (translate_word <$> nregs)), mem2) = (NextI, update_reg (<[PC:=inr (pcp, pcg, pcb, pce, pcam1)]> (<[call.r_stk:=inr (URWLX, Monotone, br, ne_stk, ^(na_stk + 1)%a)]> (translate_word <$> nregs)), mem2) PC (inr (pcp, pcg, pcb, pce, pca)))). + assert (YY: updatePC (<[PC:=inr (pcp, pcg, pcb, pce, pcam1)]> (<[call.r_stk:=inr (URWLX, Directed, br, ne_stk, ^(na_stk + 1)%a)]> (translate_word <$> nregs)), mem2) = (NextI, update_reg (<[PC:=inr (pcp, pcg, pcb, pce, pcam1)]> (<[call.r_stk:=inr (URWLX, Directed, br, ne_stk, ^(na_stk + 1)%a)]> (translate_word <$> nregs)), mem2) PC (inr (pcp, pcg, pcb, pce, pca)))). { rewrite /updatePC /RegLocate lookup_insert /= Hpcam1eq. destruct Hcanexec as [-> | [-> | ->] ]; auto. } rewrite YY /update_reg /=. rewrite insert_insert. - assert (XX: <[PC:=inr (pcp, pcg, pcb, pce, pca)]> (<[call.r_stk:=inr (URWLX, Monotone, br, ne_stk, ^(na_stk + 1)%a)]> (translate_word <$> nregs)) = translate_word <$> nregs). + assert (XX: <[PC:=inr (pcp, pcg, pcb, pce, pca)]> (<[call.r_stk:=inr (URWLX, Directed, br, ne_stk, ^(na_stk + 1)%a)]> (translate_word <$> nregs)) = translate_word <$> nregs). { eapply map_eq. intros. destruct (reg_eq_dec i PC); [subst i|]. - rewrite lookup_insert lookup_fmap HnewPC /= //. @@ -10034,7 +10034,7 @@ Local Transparent all_registers. rewrite /update_reg /cap_lang.mem /reg /MemLocate. generalize (Hstksim0 _ _ HnewPC'). intros [AA [AB AC] ]. rewrite AA. - assert (ZZ: (foldr (λ (r : RegName) (reg : Reg), <[r:=translate_word (base.RegLocate nregs r)]> reg) (<[R 1 eq_refl:=inr (RX, Monotone, br, er, ^(na_stk + 32)%a)]> reg2) rlist) = <[PC := reg2 !r! PC]> (<[call.r_stk := reg2 !r! call.r_stk]> (translate_word <$> nregs))). + assert (ZZ: (foldr (λ (r : RegName) (reg : Reg), <[r:=translate_word (base.RegLocate nregs r)]> reg) (<[R 1 eq_refl:=inr (RX, Directed, br, er, ^(na_stk + 32)%a)]> reg2) rlist) = <[PC := reg2 !r! PC]> (<[call.r_stk := reg2 !r! call.r_stk]> (translate_word <$> nregs))). { eapply map_eq. intros. assert (Hdup: NoDup rlist). { subst rlist. apply NoDup_list_difference. @@ -10064,12 +10064,12 @@ Local Transparent all_registers. rewrite ZZ. rewrite insert_insert. rewrite (insert_commute _ call.r_stk PC) //. rewrite !insert_insert /=. - assert (YY: updatePC (<[PC:=inr (pcp, pcg, pcb, pce, pcam1)]> (<[call.r_stk:=inr (URWLX, Monotone, br, ne_stk, ^(na_stk + 1)%a)]> (translate_word <$> nregs)), mem2) = (NextI, update_reg (<[PC:=inr (pcp, pcg, pcb, pce, pcam1)]> (<[call.r_stk:=inr (URWLX, Monotone, br, ne_stk, ^(na_stk + 1)%a)]> (translate_word <$> nregs)), mem2) PC (inr (pcp, pcg, pcb, pce, pca)))). + assert (YY: updatePC (<[PC:=inr (pcp, pcg, pcb, pce, pcam1)]> (<[call.r_stk:=inr (URWLX, Directed, br, ne_stk, ^(na_stk + 1)%a)]> (translate_word <$> nregs)), mem2) = (NextI, update_reg (<[PC:=inr (pcp, pcg, pcb, pce, pcam1)]> (<[call.r_stk:=inr (URWLX, Directed, br, ne_stk, ^(na_stk + 1)%a)]> (translate_word <$> nregs)), mem2) PC (inr (pcp, pcg, pcb, pce, pca)))). { rewrite /updatePC /RegLocate lookup_insert /= Hpcam1eq. destruct Hcanexec as [-> | [-> | ->] ]; auto. } rewrite YY /update_reg /=. rewrite insert_insert. - assert (XX: <[PC:=inr (pcp, pcg, pcb, pce, pca)]> (<[call.r_stk:=inr (URWLX, Monotone, br, ne_stk, ^(na_stk + 1)%a)]> (translate_word <$> nregs)) = translate_word <$> nregs). + assert (XX: <[PC:=inr (pcp, pcg, pcb, pce, pca)]> (<[call.r_stk:=inr (URWLX, Directed, br, ne_stk, ^(na_stk + 1)%a)]> (translate_word <$> nregs)) = translate_word <$> nregs). { eapply map_eq. intros. destruct (reg_eq_dec i PC); [subst i|]. - rewrite lookup_insert lookup_fmap HnewPC /= //. @@ -10413,7 +10413,7 @@ Local Transparent all_registers. rewrite /update_reg /cap_lang.mem /reg /MemLocate. generalize (Hstksim0 _ _ HnewPC'). intros [AA [AB AC] ]. rewrite AA. - assert (ZZ: (foldr (λ (r : RegName) (reg : Reg), <[r:=translate_word (base.RegLocate nregs r)]> reg) (<[R 1 eq_refl:=inr (RX, Monotone, br, er, ^(na_stk + 32)%a)]> reg2) rlist) = <[PC := reg2 !r! PC]> (<[call.r_stk := reg2 !r! call.r_stk]> (translate_word <$> nregs))). + assert (ZZ: (foldr (λ (r : RegName) (reg : Reg), <[r:=translate_word (base.RegLocate nregs r)]> reg) (<[R 1 eq_refl:=inr (RX, Directed, br, er, ^(na_stk + 32)%a)]> reg2) rlist) = <[PC := reg2 !r! PC]> (<[call.r_stk := reg2 !r! call.r_stk]> (translate_word <$> nregs))). { eapply map_eq. intros. assert (Hdup: NoDup rlist). { subst rlist. apply NoDup_list_difference. @@ -10443,12 +10443,12 @@ Local Transparent all_registers. rewrite ZZ. rewrite insert_insert. rewrite (insert_commute _ call.r_stk PC) //. rewrite !insert_insert /=. - assert (YY: updatePC (<[PC:=inr (pcp, pcg, pcb, pce, pcam1)]> (<[call.r_stk:=inr (URWLX, Monotone, br, ne_stk, ^(na_stk + 1)%a)]> (translate_word <$> nregs)), mem2) = (NextI, update_reg (<[PC:=inr (pcp, pcg, pcb, pce, pcam1)]> (<[call.r_stk:=inr (URWLX, Monotone, br, ne_stk, ^(na_stk + 1)%a)]> (translate_word <$> nregs)), mem2) PC (inr (pcp, pcg, pcb, pce, pca)))). + assert (YY: updatePC (<[PC:=inr (pcp, pcg, pcb, pce, pcam1)]> (<[call.r_stk:=inr (URWLX, Directed, br, ne_stk, ^(na_stk + 1)%a)]> (translate_word <$> nregs)), mem2) = (NextI, update_reg (<[PC:=inr (pcp, pcg, pcb, pce, pcam1)]> (<[call.r_stk:=inr (URWLX, Directed, br, ne_stk, ^(na_stk + 1)%a)]> (translate_word <$> nregs)), mem2) PC (inr (pcp, pcg, pcb, pce, pca)))). { rewrite /updatePC /RegLocate lookup_insert /= Hpcam1eq. destruct Hcanexec as [-> | [-> | ->] ]; auto. } rewrite YY /update_reg /=. rewrite insert_insert. - assert (XX: <[PC:=inr (pcp, pcg, pcb, pce, pca)]> (<[call.r_stk:=inr (URWLX, Monotone, br, ne_stk, ^(na_stk + 1)%a)]> (translate_word <$> nregs)) = translate_word <$> nregs). + assert (XX: <[PC:=inr (pcp, pcg, pcb, pce, pca)]> (<[call.r_stk:=inr (URWLX, Directed, br, ne_stk, ^(na_stk + 1)%a)]> (translate_word <$> nregs)) = translate_word <$> nregs). { eapply map_eq. intros. destruct (reg_eq_dec i PC); [subst i|]. - rewrite lookup_insert lookup_fmap HnewPC /= //. @@ -10583,7 +10583,7 @@ Local Transparent all_registers. { assert (lang.updatePC (reg1, h, stk, cs) = (lang.NextI, (<[PC := inr (Stk d p b e a0)]>reg1, h, stk, cs))) as ->. { rewrite /lang.updatePC /= /base.RegLocate HPC /= Hap1 /=. inv H6; destruct p; simpl; naive_solver. } - assert (updatePC (reg2, mem2) = (NextI, (<[PC := inr (p, Monotone, b, e, a0)]> reg2, mem2))) as ->. + assert (updatePC (reg2, mem2) = (NextI, (<[PC := inr (p, Directed, b, e, a0)]> reg2, mem2))) as ->. { rewrite /updatePC /= /RegLocate HPC' /= Hap1 /=. inv H6; destruct p; simpl; naive_solver. } simpl. econstructor. @@ -10644,7 +10644,7 @@ Local Transparent all_registers. { assert (lang.updatePC (reg1, h, stk, cs) = (lang.NextI, (<[PC := inr (Stk d p b e a0)]>reg1, h, stk, cs))) as ->. { rewrite /lang.updatePC /= /base.RegLocate HPC /= Hap1 /=. inv H6; destruct p; simpl; naive_solver. } - assert (updatePC (reg2, mem2) = (NextI, (<[PC := inr (p, Monotone, b, e, a0)]> reg2, mem2))) as ->. + assert (updatePC (reg2, mem2) = (NextI, (<[PC := inr (p, Directed, b, e, a0)]> reg2, mem2))) as ->. { rewrite /updatePC /= /RegLocate HPC' /= Hap1 /=. inv H6; destruct p; simpl; naive_solver. } simpl. econstructor. @@ -10835,7 +10835,7 @@ Local Transparent all_registers. rewrite /update_reg /cap_lang.mem /reg /MemLocate. generalize (Hstksim0 _ _ HnewPC'). intros [AA [AB AC] ]. rewrite AA. - assert (ZZ: (foldr (λ (r : RegName) (reg : Reg), <[r:=translate_word (base.RegLocate nregs r)]> reg) (<[R 1 eq_refl:=inr (RX, Monotone, br, er, ^(na_stk + 32)%a)]> reg2) rlist) = <[PC := reg2 !r! PC]> (<[call.r_stk := reg2 !r! call.r_stk]> (translate_word <$> nregs))). + assert (ZZ: (foldr (λ (r : RegName) (reg : Reg), <[r:=translate_word (base.RegLocate nregs r)]> reg) (<[R 1 eq_refl:=inr (RX, Directed, br, er, ^(na_stk + 32)%a)]> reg2) rlist) = <[PC := reg2 !r! PC]> (<[call.r_stk := reg2 !r! call.r_stk]> (translate_word <$> nregs))). { eapply map_eq. intros. assert (Hdup: NoDup rlist). { subst rlist. apply NoDup_list_difference. @@ -10865,12 +10865,12 @@ Local Transparent all_registers. rewrite ZZ. rewrite insert_insert. rewrite (insert_commute _ call.r_stk PC) //. rewrite !insert_insert /=. - assert (YY: updatePC (<[PC:=inr (pcp, pcg, pcb, pce, pcam1)]> (<[call.r_stk:=inr (URWLX, Monotone, br, ne_stk, ^(na_stk + 1)%a)]> (translate_word <$> nregs)), mem2) = (NextI, update_reg (<[PC:=inr (pcp, pcg, pcb, pce, pcam1)]> (<[call.r_stk:=inr (URWLX, Monotone, br, ne_stk, ^(na_stk + 1)%a)]> (translate_word <$> nregs)), mem2) PC (inr (pcp, pcg, pcb, pce, pca)))). + assert (YY: updatePC (<[PC:=inr (pcp, pcg, pcb, pce, pcam1)]> (<[call.r_stk:=inr (URWLX, Directed, br, ne_stk, ^(na_stk + 1)%a)]> (translate_word <$> nregs)), mem2) = (NextI, update_reg (<[PC:=inr (pcp, pcg, pcb, pce, pcam1)]> (<[call.r_stk:=inr (URWLX, Directed, br, ne_stk, ^(na_stk + 1)%a)]> (translate_word <$> nregs)), mem2) PC (inr (pcp, pcg, pcb, pce, pca)))). { rewrite /updatePC /RegLocate lookup_insert /= Hpcam1eq. destruct Hcanexec as [-> | [-> | ->] ]; auto. } rewrite YY /update_reg /=. rewrite insert_insert. - assert (XX: <[PC:=inr (pcp, pcg, pcb, pce, pca)]> (<[call.r_stk:=inr (URWLX, Monotone, br, ne_stk, ^(na_stk + 1)%a)]> (translate_word <$> nregs)) = translate_word <$> nregs). + assert (XX: <[PC:=inr (pcp, pcg, pcb, pce, pca)]> (<[call.r_stk:=inr (URWLX, Directed, br, ne_stk, ^(na_stk + 1)%a)]> (translate_word <$> nregs)) = translate_word <$> nregs). { eapply map_eq. intros. destruct (reg_eq_dec i PC); [subst i|]. - rewrite lookup_insert lookup_fmap HnewPC /= //.