All fixed

logsem · Jul 21, 2020 · 52e6c1c · 52e6c1c
1 parent 36486bc
commit 52e6c1c
Show file tree

Hide file tree

Showing 2 changed files with 21 additions and 20 deletions.
diff --git a/theories/examples/awkward_example_adequacy.v b/theories/examples/awkward_example_adequacy.v
@@ -239,6 +239,7 @@ Section Adequacy.
     pose proof (dom_mkregion_incl a e l) as HH.
     rewrite elem_of_subseteq in HH |- * => HH.
     specialize (HH _ H). eapply elem_of_list_to_set; eauto.
+    Unshelve. apply _.
   Qed.
 
   Lemma in_dom_mkregion' a e l k:
@@ -263,7 +264,7 @@ Section Adequacy.
     try match goal with |- _ ## dom _ (mkregion _ _ _) =>
       eapply disjoint_mono_r; [ apply dom_mkregion_incl |] end;
     rewrite -?list_to_set_app_L ?dom_list_to_map_singleton;
-    apply list_to_set_disj.
+    apply stdpp_extra.list_to_set_disj.
 
   Lemma mkregion_sepM_to_sepL2 (a e: Addr) l (φ: Addr → Word → iProp Σ) :
     (a + length l)%a = Some e →
@@ -369,22 +370,22 @@ Section Adequacy.
 
     (* Massage points-to into sepL2s with permission-pointsto *)
 
-    iDestruct (mkregion_prepare RO with "Hlink_table") as ">Hlink_table". by apply link_table_size.
-    iDestruct (mkregion_prepare RW with "Hfail") as ">Hfail". by apply fail_size.
-    iDestruct (mkregion_prepare RWX with "Hmalloc_mem") as ">Hmalloc_mem".
+    iDestruct (mkregion_prepare RO with "[$Hlink_table]") as ">Hlink_table". by apply link_table_size.
+    iDestruct (mkregion_prepare RW with "[$Hfail]") as ">Hfail". by apply fail_size.
+    iDestruct (mkregion_prepare RWX with "[$Hmalloc_mem]") as ">Hmalloc_mem".
     { rewrite replicate_length /region_size. clear.
       generalize malloc_mem_start malloc_end malloc_mem_size. solve_addr. }
-    iMod (MonRefAlloc _ _ RWX with "Hmalloc_memptr") as "Hmalloc_memptr".
-    iDestruct (mkregion_prepare RX with "Hmalloc_code") as ">Hmalloc_code".
+    iMod (MonRefAlloc _ _ RWX with "[$Hmalloc_memptr]") as "Hmalloc_memptr".
+    iDestruct (mkregion_prepare RX with "[$Hmalloc_code]") as ">Hmalloc_code".
       by apply malloc_code_size.
-    iDestruct (mkregion_prepare RWX with "Hadv") as ">Hadv". by apply adv_size.
+    iDestruct (mkregion_prepare RWX with "[$Hadv]") as ">Hadv". by apply adv_size.
     (* Keep the stack as a sepM, it'll be easier to allocate the corresponding
        uninitialized region later. *)
-    iDestruct (MonRefAlloc_sepM RWLX with "Hstack") as ">Hstack".
-    iDestruct (mkregion_prepare RWX with "Hawk_preamble") as ">Hawk_preamble".
+    iDestruct (MonRefAlloc_sepM RWLX with "[$Hstack]") as ">Hstack".
+    iDestruct (mkregion_prepare RWX with "[$Hawk_preamble]") as ">Hawk_preamble".
       by apply awk_preamble_size.
-    iDestruct (mkregion_prepare RWX with "Hawk_body") as ">Hawk_body". by apply awk_body_size.
-    iMod (MonRefAlloc _ _ RWX with "Hawk_link") as "Hawk_link".
+    iDestruct (mkregion_prepare RWX with "[$Hawk_body]") as ">Hawk_body". by apply awk_body_size.
+    iMod (MonRefAlloc _ _ RWX with "[$Hawk_link]") as "Hawk_link".
     rewrite -/(awkward_example _ _ _ _) -/(awkward_preamble _ _ _ _).
 
     (* Split the link table *)
@@ -536,9 +537,9 @@ Section Adequacy.
         (* Stack: trivially valid because fully uninitialized *)
         destruct (decide (r = r_stk)) as [ -> |].
         { rewrite /RegLocate Hstk fixpoint_interp1_eq /=.
-          rewrite (region_addrs_empty stack_start (min _ _)) /=.
+          rewrite (region_addrs_empty stack_start (addr_reg.min _ _)) /=.
           2: clear; solve_addr. iSplitR; [auto|].
-          rewrite (_: max stack_start stack_start = stack_start). 2: clear; solve_addr.
+          rewrite (_: addr_reg.max stack_start stack_start = stack_start). 2: clear; solve_addr.
           iApply (big_sepL_mono with "Hstack").
           iIntros (? ? Hk) "H". iDestruct "H" as (?) "?".
           rewrite /read_write_cond /region_state_U_pwl. iExists _. iFrame.

diff --git a/theories/examples/awkward_example_preamble.v b/theories/examples/awkward_example_preamble.v
@@ -93,7 +93,7 @@ Section awkward_example_preamble.
   Definition awk_invN : namespace := awkN .@ "inv".
   Definition awk_codeN : namespace := awkN .@ "code".
   Definition awk_clsN : namespace := awkN .@ "cls".
-  Definition awk_env : namespace := awkN .@ "env". 
+  Definition awk_env : namespace := awkN .@ "env".
 
   Lemma awkward_preamble_spec (f_m f_a offset_to_awkward: Z) (r: Reg) W pc_p pc_b pc_e
         ai pc_p' a_first a_end b_link e_link a_link a_entry a_entry'
@@ -273,7 +273,7 @@ Section awkward_example_preamble.
 
       rewrite /registers_mapsto.
       rewrite -insert_delete.
-      iDestruct (big_sepM_insert with "Hregs'") as "[HPC Hregs']". by apply lookup_delete. 
+      iDestruct (big_sepM_insert with "Hregs'") as "[HPC Hregs']". by apply lookup_delete.
       destruct (Hr'_full r_t1) as [r1v ?].
       iDestruct (big_sepM_delete _ _ r_t1 with "Hregs'") as "[Hr1 Hregs']".
         by rewrite lookup_delete_ne //.
@@ -318,7 +318,7 @@ Section awkward_example_preamble.
       { unshelve iSpecialize ("Hr'_valid" $! r_adv _); [done|].
         rewrite /(RegLocate r' r_adv) Hradvv. iApply "Hr'_valid". }
       unshelve iSpecialize ("Hr'_valid" $! r_t0 _); [done|].
-      rewrite /(RegLocate r' r_t0) Hr0v. iApply "Hr'_valid". 
+      rewrite /(RegLocate r' r_t0) Hr0v. iApply "Hr'_valid".
       { iNext. iIntros (?) "HH". iIntros (->). iApply "HH". eauto. }
     }
 
@@ -334,10 +334,10 @@ Section awkward_example_preamble.
 
     (* either we fail, or we use the continuation in rt0 *)
     iDestruct (jmp_or_fail_spec with "Hr0_valid2") as "Hcont".
-    destruct (decide (isCorrectPC (updatePcPerm r0))). 
+    destruct (decide (isCorrectPC (updatePcPerm r0))).
     2 : { iEpilogue "(HPC & Hi & Hr0)". iApply "Hcont". iFrame "HPC". iIntros (Hcontr);done. }
-    iDestruct "Hcont" as (p g b e a3 Heq) "#Hcont". 
-    simplify_eq. 
+    iDestruct "Hcont" as (p g b e a3 Heq) "#Hcont".
+    simplify_eq.
 
     iAssert (future_world g W2 W2) as "#Hfuture".
     { destruct g; iPureIntro. apply related_sts_priv_refl_world. apply related_sts_pub_refl_world. }
@@ -374,7 +374,7 @@ Section awkward_example_preamble.
     { apply related_sts_pub_world_fresh_loc; auto. }
     iSpecialize ("Hcont'" $! r'' with "[Hsts Hr Hregs HnaI]").
     { iFrame.
-      iDestruct (region_monotone with "[] [] Hr") as "$"; auto.
+      iDestruct (region_monotone with "Hr") as "$"; auto.
       rewrite /interp_reg. iSplit; [iPureIntro; apply Hr''_full|].
       iIntros (rr Hrr).
       assert (is_Some (r'' !! rr)) as [rrv Hrrv] by apply Hr''_full.