cleaned up some files we do not need (yet), updated coqfile to compil…

…e only the finished part of ftlr (store + storeU), simplified the model, updated all state modification files, and added some lemmas for manipulating static to uninitialized states

.gitignore

@@ -1,3 +1,4 @@
+_opam
 *.glob
 *.v.d
 *.vo

_CoqProject

@@ -17,9 +17,8 @@ theories/multiple_updates.v
 theories/region_invariants.v
 theories/region_invariants_transitions.v
 theories/region_invariants_revocation.v
+theories/region_invariants_batch_uninitialized.v
 theories/region_invariants_static.v
-theories/region_invariants_uninitialized.v
-theories/region_invariants_allocation.v
 theories/rules/rules_base.v
 theories/rules/rules_Get.v
 theories/rules/rules_Load.v
@@ -42,21 +41,9 @@ theories/rules/rules.v
 theories/logrel.v
 theories/monotone.v
 theories/ftlr/ftlr_base.v
-theories/ftlr/interp_weakening.v
-theories/ftlr/Get.v
-theories/ftlr/Load.v
-theories/ftlr/Store.v
-theories/ftlr/AddSubLt.v
-theories/ftlr/Lea.v
-theories/ftlr/Mov.v
-theories/ftlr/Restrict.v
-theories/ftlr/IsPtr.v
 theories/ftlr/Jmp.v
-theories/ftlr/Jnz.v
-theories/ftlr/Subseg.v
-theories/ftlr/LoadU.v
+theories/ftlr/Store.v
 theories/ftlr/StoreU.v
-theories/ftlr/PromoteU.v
 theories/fundamental.v
 theories/examples/addr_reg_sample.v
 theories/examples/disjoint_regions_tactics.v
@@ -66,5 +53,10 @@ theories/examples/stack_macros_helpers.v
 theories/examples/macros/malloc.v
 theories/examples/macros/req.v
 theories/examples/macros/push_pop.v
+theories/examples/macros/rclear.v
 theories/examples/macros/prepstack.v
+theories/examples/macros/checkbelow.v
+theories/examples/macros/fetch.v
+theories/examples/macros/assert.v
 theories/examples/macros/macros.v
+theories/examples/downwards_lse.v

theories/examples/disjoint_regions_tactics.v

@@ -30,7 +30,7 @@ Proof.
   intros a ?%elem_of_region_addrs. solve_addr.
 Qed.
 Hint Resolve AddrRegionRange_region_addrs : disj_regions.
-0
+
 Definition AddrRegionsRange (ll: list (list Addr)) (b e: Addr) :=
   ∀ l a, l ∈ ll → a ∈ l → (b <= a)%a ∧ (a < e)%a.
 

theories/examples/downwards_lse.v

@@ -227,7 +227,7 @@ Section lse.
     { destruct (decide (p = E)).
       - subst. iClear "Hwstk_valid Hwret_valid". rewrite fixpoint_interp1_eq. iSimpl in "Hwret_valid'".
         rewrite /enter_cond. iApply "Hwret_valid'". destruct g;iPureIntro.
-        apply related_sts_priv_refl_world. apply related_sts_pub_plus_refl_world. apply related_sts_a_refl_world.
+        apply related_sts_priv_refl_world. apply related_sts_priv_refl_world. apply related_sts_a_refl_world.
       - iDestruct (fundamental_from_interp (<[PC:=inl 0%Z]> (<[r_t0:=inr (p,g,b,e,a')]> rmap')) with "Hwret_valid'") as "Hcont". iNext.
         rewrite updatePcPerm_cap_non_E//. }
 

theories/examples/macros/malloc.v

@@ -1,6 +1,6 @@
 From iris.algebra Require Import frac.
 From iris.proofmode Require Import tactics.
-From cap_machine Require Import rules logrel addr_reg_sample fundamental multiple_updates.
+From cap_machine Require Import rules logrel addr_reg_sample fundamental multiple_updates region_invariants_static.
 From cap_machine.examples Require Import contiguous stack_macros_helpers.
 From iris.base_logic Require Export na_invariants.
 
@@ -577,8 +577,8 @@ Section SimpleMalloc.
     iDestruct ("Hmono" $! _ _ Hrelated' with "Hφ") as "Hφ'".
     assert (is_Some (M !! l)) as [x Hsome].
     { apply elem_of_gmap_dom. rewrite -Hdom. apply elem_of_gmap_dom. eauto. }
-    iDestruct (region_map_delete_nonstatic with "Hr") as "Hr"; [intros m;split;intros Hcontr;congruence|].
-    iDestruct (region_map_insert_nonstatic Permanent with "Hr") as "Hr";auto.
+    iDestruct (region_map_delete_nonstatic with "Hr") as "Hr"; [intros m;intros Hcontr;congruence|].
+    iDestruct (region_map_insert_nonmonostatic Permanent with "Hr") as "Hr";auto.
     iDestruct (big_sepM_delete _ _ l _ Hsome with "[Hl Hstate $Hr]") as "Hr".
     { iExists Permanent. iFrame. iSplitR;[iPureIntro;apply lookup_insert|].
       iExists γ, p, φ. rewrite HMeq lookup_insert in Hsome.
@@ -682,19 +682,11 @@ Section SimpleMalloc.
       iDestruct (big_sepL2_extract_l with "Hbe") as "[_ Hb]";[eauto|].
       iDestruct "Hb" as (w') "Hw'".
       destruct ρ;auto. (* all the following will lead to duplicate resources for x *)
-      - iDestruct (region_open_temp_nwl with "[$Hrel $Hr $Hsts]") as (v) "(_ & _ & _ & Hw & _)";[eauto|auto|..].
-        iDestruct (cap_duplicate_false with "[$Hw' $Hw]") as "?";auto.
       - iDestruct (region_open_monotemp_nwl with "[$Hrel $Hr $Hsts]") as (v) "(_ & _ & _ & Hw & _)";[eauto|auto|..].
         iDestruct (cap_duplicate_false with "[$Hw' $Hw]") as "?";auto.
       - iDestruct (region_open_perm with "[$Hrel $Hr $Hsts]") as (v) "(_ & _ & _ & Hw & _)";[eauto|auto|..].
         iDestruct (cap_duplicate_false with "[$Hw' $Hw]") as "?";auto.
-      - iMod (region_invariants_static.region_open_static with "[$Hr $Hsts]") as "(_ & _ & ? & H & %)";[apply Hρ|..].
-        rewrite /region_invariants_static.static_resources.
-        apply elem_of_gmap_dom in H2 as [? Hx].
-        iDestruct (big_sepM_delete with "H") as "[H ?]";[apply Hx|].
-        iDestruct "H" as (? ?) "[HH Hw]". iDestruct (rel_agree _ H2 with "[$Hrel $HH]") as "(% & _)";subst. 
-        iDestruct (cap_duplicate_false with "[$Hw' $Hw]") as "?";auto.
-      - iMod (region_invariants_static.region_open_monostatic with "[$Hr $Hsts]") as "(_ & _ & ? & H & %)";[apply Hρ|..].
+      - iMod (region_open_monostatic with "[$Hr $Hsts]") as "(_ & _ & ? & H & %)";[apply Hρ|..].
         rewrite /region_invariants_static.static_resources.
         apply elem_of_gmap_dom in H2 as [? Hx].
         iDestruct (big_sepM_delete with "H") as "[H ?]";[apply Hx|].
@@ -728,8 +720,7 @@ Section SimpleMalloc.
     set regs := <[PC:=updatePcPerm (inr (p, g, b', e', a))]>
                             (<[r_t0:=inr (p, g, b', e', a)]> (<[r_t1:=inr (RWX, Global, ba, ea, ba)]> (<[r_t2:=inl 0%Z]> (<[r_t3:=inl 0%Z]> (<[r_t4:=inl 0%Z]> r))))).
     iDestruct ("Hcont'" $! regs with "[] [$Hown Hregs $Hr $Hsts]") as "[_ Hcont'']".
-    { destruct g; iPureIntro;[apply related_sts_pub_priv_world|
-                              apply related_sts_pub_pub_plus_world|
+    { destruct g; iPureIntro;[apply related_sts_pub_priv_world..|
                               apply related_sts_pub_a_world]; try apply related_sts_pub_update_multiple_perm;auto. }
     { rewrite /regs. iSplitR "Hregs".
       - iSplit.

theories/examples/region_macros.v

@@ -2,8 +2,7 @@ From iris.algebra Require Import frac.
 From iris.proofmode Require Import tactics.
 Require Import Eqdep_dec List.
 From cap_machine Require Import rules logrel.
-From cap_machine Require Export addr_reg_sample region_invariants_revocation
-     region_invariants_allocation multiple_updates.
+From cap_machine Require Export addr_reg_sample region_invariants_revocation multiple_updates.
 From cap_machine Require Export iris_extra.
 
 Section region_macros.
@@ -31,116 +30,116 @@ Section region_macros.
 
    (* -------------------- ALLOCATING A NEW REGION OF ZEROES ------------------ *)
 
-   Lemma region_addrs_zeroes_alloc_aux E a W p (n : nat) :
-     p ≠ O → is_Some (a + (Z.of_nat n))%a →
-     Forall (λ a, a ∉ dom (gset Addr) (std W)) (region_addrs_aux a n) →
-     ([∗ list] a0 ∈ region_addrs_aux a n, a0 ↦ₐ[p] inl 0%Z)
-       -∗ region W
-       -∗ sts_full_world W
-     ={E}=∗ ([∗ list] x ∈ region_addrs_aux a n, read_write_cond x p interp)
-         ∗ region (std_update_temp_multiple W (region_addrs_aux a n))
-         ∗ sts_full_world (std_update_temp_multiple W (region_addrs_aux a n)).
-   Proof.
-     iInduction (n) as [| n] "IHn" forall (a W).
-     - simpl. iIntros (_ _ _) "_ Hr Hsts". iFrame. done.
-     - iIntros (Hne Hnext Hforall) "Hlist Hr Hsts".
-       iDestruct "Hlist" as "[Ha Hlist]".
-       simpl in Hforall.
-       apply list.Forall_cons in Hforall as [ Hasta Hforall].
-       destruct (pwl p) eqn:Hpwl.
-       + iAssert (∀ W, interp W (inl 0%Z))%I as "#Hav".
-         { iIntros (W'). rewrite fixpoint_interp1_eq. eauto. }
-         (* if n is 0 we do not need to use IH *)
-         destruct n.
-         { simpl. iFrame.
-           iMod (extend_region_temp_pwl E _ a p (inl 0%Z) (λ Wv, interp Wv.1 Wv.2)
-                 with "[] Hsts Hr Ha Hav") as "(Hr & Ha & Hsts)"; auto.
-           { iModIntro. iIntros (W1 W2 Hrelated) "Hv /=". do 2 (rewrite fixpoint_interp1_eq /=). done. }
-           iFrame. done.
-         }
-         iMod ("IHn" with "[] [] [] Hlist Hr Hsts") as "(Hlist & Hr & Hsts)"; auto.
-         { iPureIntro. destruct Hnext as [? ?]. zify_addr; solve [ eauto | lia ]. }
-         iFrame. destruct Hnext as [e He]. assert (a ≠ addr_reg.top) by (intros ->; solve_addr).
-         iMod (extend_region_temp_pwl E _ a p (inl 0%Z) (λ Wv, interp Wv.1 Wv.2)
-                 with "[] Hsts Hr Ha Hav") as "(Hr & Ha & Hsts)"; auto.
-         { apply (std_update_multiple_dom_sta_i _ (S n) _ _ 1); auto; lia. }
-         { iModIntro. iIntros (W1 W2 Hrelated) "Hv /=". do 2 (rewrite fixpoint_interp1_eq /=). done. }
-         iFrame. done.
-       + iAssert (∀ W, interp W (inl 0%Z))%I as "#Hav".
-         { iIntros (W'). rewrite fixpoint_interp1_eq. eauto. }
-         (* if n is 0 we do not need to use IH *)
-         destruct n.
-         { simpl. iFrame.
-           iMod (extend_region_temp_nwl E _ a p (inl 0%Z) (λ Wv, interp Wv.1 Wv.2)
-                 with "[] Hsts Hr Ha Hav") as "(Hr & Ha & Hsts)"; auto.
-           { iModIntro. iIntros (W1 W2 Hrelated) "Hv /=". do 2 (rewrite fixpoint_interp1_eq /=). done. }
-           iFrame. done.
-         }
-         iMod ("IHn" with "[] [] [] Hlist Hr Hsts") as "(Hlist & Hr & Hsts)"; auto.
-         { iPureIntro. destruct Hnext as [? ?]. zify_addr; solve [ eauto | lia ]. }
-         iFrame. destruct Hnext as [e He]. assert (a ≠ addr_reg.top) by (intros ->; solve_addr).
-         iMod (extend_region_temp_nwl E _ a p (inl 0%Z) (λ Wv, interp Wv.1 Wv.2)
-                 with "[] Hsts Hr Ha Hav") as "(Hr & Ha & Hsts)"; auto.
-         { apply (std_update_multiple_dom_sta_i _ (S n) _ _ 1); auto; lia. }
-         { iModIntro. iIntros (W1 W2 Hrelated) "Hv /=". do 2 (rewrite fixpoint_interp1_eq /=). done. }
-         iFrame. done.
-   Qed.
-
-   Lemma region_addrs_zeroes_valid_aux n W :
-     ⊢ ([∗ list] y ∈ replicate n (inl 0%Z), ▷ (fixpoint interp1) W y).
-   Proof.
-     iInduction (n) as [| n] "IHn".
-     - done.
-     - simpl. iSplit; last iFrame "#".
-       rewrite fixpoint_interp1_eq. iNext.
-       eauto.
-   Qed.
-
-   Lemma region_addrs_zeroes_valid (a b : Addr) W :
-     ⊢ ([∗ list] _;y2 ∈ region_addrs a b; region_addrs_zeroes a b,
-                                        ▷ (fixpoint interp1) W y2).
-   Proof.
-     rewrite /region_addrs /region_addrs_zeroes.
-     iApply (big_sepL2_to_big_sepL_r _ _ (region_addrs_zeroes a b)).
-     - rewrite region_addrs_aux_length replicate_length //.
-     - iApply region_addrs_zeroes_valid_aux.
-   Qed.
-
-   Lemma region_addrs_zeroes_trans_aux (a b : Addr) p n :
-     ([∗ list] y1;y2 ∈ region_addrs_aux a n;replicate n (inl 0%Z), y1 ↦ₐ[p] y2)
-       -∗ [∗ list] y1 ∈ region_addrs_aux a n, y1 ↦ₐ[p] inl 0%Z.
-   Proof.
-     iInduction (n) as [| n] "IHn" forall (a); first auto.
-     iIntros "Hlist".
-     iDestruct "Hlist" as "[Ha Hlist]".
-     iFrame.
-     iApply "IHn". iFrame.
-   Qed.
-
-   Lemma region_addrs_zeroes_trans (a b : Addr) p :
-     ([∗ list] y1;y2 ∈ region_addrs a b;region_addrs_zeroes a b, y1 ↦ₐ[p] y2)
-       -∗ [∗ list] a0 ∈ region_addrs a b, a0 ↦ₐ[p] (inl 0%Z).
-   Proof.
-     iIntros "Hlist".
-     rewrite /region_addrs /region_addrs_zeroes.
-     iApply region_addrs_zeroes_trans_aux; auto.
-   Qed.
-
-   Lemma region_addrs_zeroes_alloc E W (a b : Addr) p :
-     p ≠ O →
-     Forall (λ a0 : Addr, (a0 ∉ dom (gset Addr) (std W))) (region_addrs a b) →
-     ([∗ list] y1;y2 ∈ region_addrs a b;region_addrs_zeroes a b, y1 ↦ₐ[p] y2)
-       ∗ region W ∗ sts_full_world W
-     ={E}=∗ ([∗ list] a0 ∈ region_addrs a b, read_write_cond a0 p interp)
-         ∗ region (std_update_temp_multiple W (region_addrs a b))
-         ∗ sts_full_world (std_update_temp_multiple W (region_addrs a b)).
-   Proof.
-     iIntros (Hne Hforall) "[Hlist [Hr Hsts] ]".
-     iDestruct (region_addrs_zeroes_trans with "Hlist") as "Hlist".
-     rewrite /region_addrs. rewrite /region_addrs in Hforall.
-     iMod (region_addrs_zeroes_alloc_aux with "[$Hlist] [$Hr] [$Hsts]") as "H"; auto.
-     rewrite /region_size. zify_addr; eauto; lia.
-   Qed.
+   (* Lemma region_addrs_zeroes_alloc_aux E a W p (n : nat) : *)
+   (*   p ≠ O → is_Some (a + (Z.of_nat n))%a → *)
+   (*   Forall (λ a, a ∉ dom (gset Addr) (std W)) (region_addrs_aux a n) → *)
+   (*   ([∗ list] a0 ∈ region_addrs_aux a n, a0 ↦ₐ[p] inl 0%Z) *)
+   (*     -∗ region W *)
+   (*     -∗ sts_full_world W *)
+   (*   ={E}=∗ ([∗ list] x ∈ region_addrs_aux a n, read_write_cond x p interp) *)
+   (*       ∗ region (std_update_temp_multiple W (region_addrs_aux a n)) *)
+   (*       ∗ sts_full_world (std_update_temp_multiple W (region_addrs_aux a n)). *)
+   (* Proof. *)
+   (*   iInduction (n) as [| n] "IHn" forall (a W). *)
+   (*   - simpl. iIntros (_ _ _) "_ Hr Hsts". iFrame. done. *)
+   (*   - iIntros (Hne Hnext Hforall) "Hlist Hr Hsts". *)
+   (*     iDestruct "Hlist" as "[Ha Hlist]". *)
+   (*     simpl in Hforall. *)
+   (*     apply list.Forall_cons in Hforall as [ Hasta Hforall]. *)
+   (*     destruct (pwl p) eqn:Hpwl. *)
+   (*     + iAssert (∀ W, interp W (inl 0%Z))%I as "#Hav". *)
+   (*       { iIntros (W'). rewrite fixpoint_interp1_eq. eauto. } *)
+   (*       (* if n is 0 we do not need to use IH *) *)
+   (*       destruct n. *)
+   (*       { simpl. iFrame. *)
+   (*         iMod (extend_region_temp_pwl E _ a p (inl 0%Z) (λ Wv, interp Wv.1 Wv.2) *)
+   (*               with "[] Hsts Hr Ha Hav") as "(Hr & Ha & Hsts)"; auto. *)
+   (*         { iModIntro. iIntros (W1 W2 Hrelated) "Hv /=". do 2 (rewrite fixpoint_interp1_eq /=). done. } *)
+   (*         iFrame. done. *)
+   (*       } *)
+   (*       iMod ("IHn" with "[] [] [] Hlist Hr Hsts") as "(Hlist & Hr & Hsts)"; auto. *)
+   (*       { iPureIntro. destruct Hnext as [? ?]. zify_addr; solve [ eauto | lia ]. } *)
+   (*       iFrame. destruct Hnext as [e He]. assert (a ≠ addr_reg.top) by (intros ->; solve_addr). *)
+   (*       iMod (extend_region_temp_pwl E _ a p (inl 0%Z) (λ Wv, interp Wv.1 Wv.2) *)
+   (*               with "[] Hsts Hr Ha Hav") as "(Hr & Ha & Hsts)"; auto. *)
+   (*       { apply (std_update_multiple_dom_sta_i _ (S n) _ _ 1); auto; lia. } *)
+   (*       { iModIntro. iIntros (W1 W2 Hrelated) "Hv /=". do 2 (rewrite fixpoint_interp1_eq /=). done. } *)
+   (*       iFrame. done. *)
+   (*     + iAssert (∀ W, interp W (inl 0%Z))%I as "#Hav". *)
+   (*       { iIntros (W'). rewrite fixpoint_interp1_eq. eauto. } *)
+   (*       (* if n is 0 we do not need to use IH *) *)
+   (*       destruct n. *)
+   (*       { simpl. iFrame. *)
+   (*         iMod (extend_region_temp_nwl E _ a p (inl 0%Z) (λ Wv, interp Wv.1 Wv.2) *)
+   (*               with "[] Hsts Hr Ha Hav") as "(Hr & Ha & Hsts)"; auto. *)
+   (*         { iModIntro. iIntros (W1 W2 Hrelated) "Hv /=". do 2 (rewrite fixpoint_interp1_eq /=). done. } *)
+   (*         iFrame. done. *)
+   (*       } *)
+   (*       iMod ("IHn" with "[] [] [] Hlist Hr Hsts") as "(Hlist & Hr & Hsts)"; auto. *)
+   (*       { iPureIntro. destruct Hnext as [? ?]. zify_addr; solve [ eauto | lia ]. } *)
+   (*       iFrame. destruct Hnext as [e He]. assert (a ≠ addr_reg.top) by (intros ->; solve_addr). *)
+   (*       iMod (extend_region_temp_nwl E _ a p (inl 0%Z) (λ Wv, interp Wv.1 Wv.2) *)
+   (*               with "[] Hsts Hr Ha Hav") as "(Hr & Ha & Hsts)"; auto. *)
+   (*       { apply (std_update_multiple_dom_sta_i _ (S n) _ _ 1); auto; lia. } *)
+   (*       { iModIntro. iIntros (W1 W2 Hrelated) "Hv /=". do 2 (rewrite fixpoint_interp1_eq /=). done. } *)
+   (*       iFrame. done. *)
+   (* Qed. *)
+
+   (* Lemma region_addrs_zeroes_valid_aux n W : *)
+   (*   ⊢ ([∗ list] y ∈ replicate n (inl 0%Z), ▷ (fixpoint interp1) W y). *)
+   (* Proof. *)
+   (*   iInduction (n) as [| n] "IHn". *)
+   (*   - done. *)
+   (*   - simpl. iSplit; last iFrame "#". *)
+   (*     rewrite fixpoint_interp1_eq. iNext. *)
+   (*     eauto. *)
+   (* Qed. *)
+
+   (* Lemma region_addrs_zeroes_valid (a b : Addr) W : *)
+   (*   ⊢ ([∗ list] _;y2 ∈ region_addrs a b; region_addrs_zeroes a b, *)
+   (*                                      ▷ (fixpoint interp1) W y2). *)
+   (* Proof. *)
+   (*   rewrite /region_addrs /region_addrs_zeroes. *)
+   (*   iApply (big_sepL2_to_big_sepL_r _ _ (region_addrs_zeroes a b)). *)
+   (*   - rewrite region_addrs_aux_length replicate_length //. *)
+   (*   - iApply region_addrs_zeroes_valid_aux. *)
+   (* Qed. *)
+
+   (* Lemma region_addrs_zeroes_trans_aux (a b : Addr) p n : *)
+   (*   ([∗ list] y1;y2 ∈ region_addrs_aux a n;replicate n (inl 0%Z), y1 ↦ₐ[p] y2) *)
+   (*     -∗ [∗ list] y1 ∈ region_addrs_aux a n, y1 ↦ₐ[p] inl 0%Z. *)
+   (* Proof. *)
+   (*   iInduction (n) as [| n] "IHn" forall (a); first auto. *)
+   (*   iIntros "Hlist". *)
+   (*   iDestruct "Hlist" as "[Ha Hlist]". *)
+   (*   iFrame. *)
+   (*   iApply "IHn". iFrame. *)
+   (* Qed. *)
+
+   (* Lemma region_addrs_zeroes_trans (a b : Addr) p : *)
+   (*   ([∗ list] y1;y2 ∈ region_addrs a b;region_addrs_zeroes a b, y1 ↦ₐ[p] y2) *)
+   (*     -∗ [∗ list] a0 ∈ region_addrs a b, a0 ↦ₐ[p] (inl 0%Z). *)
+   (* Proof. *)
+   (*   iIntros "Hlist". *)
+   (*   rewrite /region_addrs /region_addrs_zeroes. *)
+   (*   iApply region_addrs_zeroes_trans_aux; auto. *)
+   (* Qed. *)
+
+   (* Lemma region_addrs_zeroes_alloc E W (a b : Addr) p : *)
+   (*   p ≠ O → *)
+   (*   Forall (λ a0 : Addr, (a0 ∉ dom (gset Addr) (std W))) (region_addrs a b) → *)
+   (*   ([∗ list] y1;y2 ∈ region_addrs a b;region_addrs_zeroes a b, y1 ↦ₐ[p] y2) *)
+   (*     ∗ region W ∗ sts_full_world W *)
+   (*   ={E}=∗ ([∗ list] a0 ∈ region_addrs a b, read_write_cond a0 p interp) *)
+   (*       ∗ region (std_update_temp_multiple W (region_addrs a b)) *)
+   (*       ∗ sts_full_world (std_update_temp_multiple W (region_addrs a b)). *)
+   (* Proof. *)
+   (*   iIntros (Hne Hforall) "[Hlist [Hr Hsts] ]". *)
+   (*   iDestruct (region_addrs_zeroes_trans with "Hlist") as "Hlist". *)
+   (*   rewrite /region_addrs. rewrite /region_addrs in Hforall. *)
+   (*   iMod (region_addrs_zeroes_alloc_aux with "[$Hlist] [$Hr] [$Hsts]") as "H"; auto. *)
+   (*   rewrite /region_size. zify_addr; eauto; lia. *)
+   (* Qed. *)
 
 
    (* ------------------------------ OPENING A REGION ----------------------------------- *)