refactor and use ghost map

theories/lang/heap.v

@@ -75,12 +75,6 @@ Fixpoint heap_free (a : addr) (n : nat) (h : heap) : heap :=
   | S n => delete a (heap_free (Z.succ a) n h)
   end.
 
-Fixpoint heap_free_list (ls : list (loc * layout)) (h : heap) : heap :=
-  match ls with
-  | []           => h
-  | (l,ly) :: ls => heap_free l.2 ly.(ly_size) (heap_free_list ls h)
-  end.
-
 (** ** Lemmas about the heap and related operations. *)
 
 Lemma heap_lookup_inj_val a h v1 v2 Paid1 Paid2 Plk1 Plk2:
@@ -92,6 +86,16 @@ Proof.
   f_equal. by apply: IH.
 Qed.
 
+Lemma heap_lookup_is_Some a p v Paid Plk h:
+  heap_lookup a v Paid Plk h →
+  a ≤ p < a + length v →
+  is_Some (h !! p).
+Proof.
+  elim: v a => /=; first lia. move => b v IH a [[aid [lk [Ha _]]] H] Hp.
+  destruct (decide (p = a)) as [->|]; first naive_solver.
+  apply (IH (Z.succ a)) => //. lia.
+Qed.
+
 Lemma heap_update_ext h a v faid1 faid2 flk1 flk2:
   (∀ x, faid1 x = faid2 x) → (∀ x, flk1 x = flk2 x) →
   heap_update a v faid1 flk1 h = heap_update a v faid2 flk2 h.
@@ -100,14 +104,6 @@ Proof.
   apply: partial_alter_ext => ??. by rewrite Hext1 Hext2.
 Qed.
 
-Lemma heap_update_lookup_lt a1 a2 v faid flk h:
-  a1 < a2 →
-  heap_update a2 v faid flk h !! a1 = h !! a1.
-Proof.
-  elim: v a1 a2 => // ?? IH ???.
-  rewrite lookup_partial_alter_ne; last lia. apply IH. lia.
-Qed.
-
 Lemma heap_update_lookup_not_in_range a1 a2 v faid flk h:
   a1 < a2 ∨ a2 + length v ≤ a1 →
   heap_update a2 v faid flk h !! a1 = h !! a1.
@@ -128,7 +124,7 @@ Proof.
   - move => /= a1 a2 [??]. exfalso. lia.
   - move => ?? IH a1 a2 [H1 H2]. destruct (decide (a1 = a2)) as [->|Hne].
     + rewrite lookup_partial_alter -/heap_update Z.sub_diag /=.
-      rewrite heap_update_lookup_lt; [done | lia].
+      rewrite heap_update_lookup_not_in_range; [done | lia].
     + rewrite lookup_partial_alter_ne // -/heap_update /= IH; last first.
       { rewrite /= in H2. lia. } do 3 f_equal.
       rewrite lookup_cons_ne_0; last lia. f_equal. lia.
@@ -138,10 +134,6 @@ Lemma heap_free_delete h a1 a2 n :
   delete a1 (heap_free a2 n h) = heap_free a2 n (delete a1 h).
 Proof. elim: n a2 => //= ? IH ?. by rewrite delete_commute IH. Qed.
 
-Lemma heap_free_list_app ls1 ls2 h :
-  heap_free_list (ls1 ++ ls2) h = heap_free_list ls1 (heap_free_list ls2 h).
-Proof. by elim: ls1 => //= [[??]] ? ->. Qed.
-
 Lemma heap_upd_ext h l v f1 f2:
   (∀ x, f1 x = f2 x) → heap_upd l v f1 h = heap_upd l v f2 h.
 Proof. by apply heap_update_ext. Qed.
@@ -172,14 +164,14 @@ Proof.
   by rewrite H Hlookup H1 /=.
 Qed.
 
-Lemma heap_free_lookup_None a p (n : nat) h:
+Lemma heap_free_lookup_in_range a p (n : nat) h:
   a ≤ p < a + n →
   heap_free a n h !! p = None.
 Proof.
   elim: n a; first lia. move => n IH a [H1 H2] /=.
-  destruct (decide (a = p)) as [->|].
-  - by rewrite lookup_delete.
-  - rewrite lookup_delete_ne; last done. apply IH. lia.
+  rewrite lookup_delete_None.
+  destruct (decide (a = p)) as [->|]; [by left|right].
+  apply: IH. lia.
 Qed.
 
 Lemma heap_free_lookup_not_in_range a p (n : nat) h:
@@ -452,7 +444,7 @@ Proof.
   destruct H as (Hi1&Hi2&Hi3&Hi4&Hi5). split_and!.
   - move => a hc /= Hhc.
     assert (¬ (l.2 ≤ a < l.2 + length v)) as Hnot_in.
-    { move => ?. rewrite heap_free_lookup_None // in Hhc; lia. }
+    { move => ?. rewrite heap_free_lookup_in_range // in Hhc; lia. }
     rewrite heap_free_lookup_not_in_range in Hhc; last lia.
     destruct (Hi1 _ _ Hhc) as [al [?[??]]]. exists al. split; last done.
     rewrite /= lookup_insert_ne; first done.
@@ -460,7 +452,7 @@ Proof.
     unfold al_end in *. simpl in *. lia.
   - move => a hc /= Hhc.
     assert (¬ (l.2 ≤ a < l.2 + length v)) as Hnot_in.
-    { move => ?. rewrite heap_free_lookup_None // in Hhc; lia. }
+    { move => ?. rewrite heap_free_lookup_in_range // in Hhc; lia. }
     rewrite heap_free_lookup_not_in_range in Hhc; last lia.
     destruct (Hi2 _ _ Hhc) as [al [??]]. exists al.
     rewrite lookup_insert_ne; first done.
@@ -519,7 +511,7 @@ Proof.
   move: Hcontains => [[id[?[Heq [??]]]] Hcontains].
   destruct (decide (a1 = a2)) as [->|Hne].
   - rewrite lookup_partial_alter -/heap_update in H. simplify_eq => /=.
-    rewrite heap_update_lookup_lt; last lia. rewrite Heq /= Hfaid.
+    rewrite heap_update_lookup_not_in_range; last lia. rewrite Heq /= Hfaid.
     apply (Hσ a2 _ Heq).
   - rewrite lookup_partial_alter_ne // -/heap_update in H.
     by unshelve eapply (IH _ _ Hσ _ Hfaid Hlen a2 hc) => //.
@@ -540,22 +532,12 @@ Proof.
   move: Hcontains => [[id[?[Heq [??]]]] Hcontains].
   destruct (decide (a1 = a2)) as [->|Hne].
   - rewrite lookup_partial_alter -/heap_update in H. simplify_eq => /=.
-    rewrite heap_update_lookup_lt; last lia. rewrite Heq /= Hfaid.
+    rewrite heap_update_lookup_not_in_range; last lia. rewrite Heq /= Hfaid.
     apply (Hσ a2 _ Heq).
   - rewrite lookup_partial_alter_ne // -/heap_update in H.
     by unshelve eapply (IH _ _ Hσ _ Hfaid Hlen a2 hc) => //.
 Qed.
 
-Lemma heap_lookup_is_Some a p v Paid Plk h:
-  heap_lookup a v Paid Plk h →
-  a ≤ p < a + length v →
-  is_Some (h !! p).
-Proof.
-  elim: v a => /=; first lia. move => b v IH a [[aid [lk [Ha _]]] H] Hp.
-  destruct (decide (p = a)) as [->|]; first naive_solver.
-  apply (IH (Z.succ a)) => //. lia.
-Qed.
-
 Lemma heap_update_alloc_alive_in_heap σ a v1 v2 Paid Plk faid flk:
   heap_state_alloc_alive_in_heap σ →
   heap_lookup a v1 Paid Plk σ.(hs_heap) →

theories/lang/lang.v

@@ -349,9 +349,6 @@ Inductive eval_un_op : un_op → op_type → state → val → val → Prop :=
 
 (*** Evaluation of Expressions *)
 
-Definition state_alloc_new_blocks (σ1 : state) (ls : list loc) (vs : list val) (σ2 : state) : Prop :=
-  alloc_new_blocks σ1.(st_heap) ls vs σ2.(st_heap) ∧ σ1.(st_fntbl) = σ2.(st_fntbl).
-
 Inductive expr_step : expr → state → list Empty_set → runtime_expr → state → list runtime_expr → Prop :=
 | SkipES v σ:
     expr_step (SkipE (Val v)) σ [] (Val v) σ []
@@ -402,7 +399,7 @@ comparing pointers? (see lambda rust) *)
     z1 = z2 →
     expr_step (CAS (IntOp it) (Val v1) (Val v2) (Val v3)) σ []
               (Val (val_of_bool true)) (heap_fmap (heap_upd l1 v3 (λ _, RSt 0%nat)) σ) []
-| CallS lsa lsv σ σ' σ'' vf vs f rf fn fn' :
+| CallS lsa lsv σ hs' hs'' vf vs f rf fn fn' :
     val_to_loc vf = Some f →
     σ.(st_fntbl) !! f = Some fn →
     length lsa = length fn.(f_args) →
@@ -415,12 +412,12 @@ comparing pointers? (see lambda rust) *)
     Forall2 has_layout_loc lsa fn.(f_args).*2 →
     Forall2 has_layout_loc lsv fn.(f_local_vars).*2 →
     (* initialize the local vars to poison *)
-    state_alloc_new_blocks σ lsv ((λ p, replicate p.2.(ly_size) MPoison) <$> fn.(f_local_vars)) σ' →
+    alloc_new_blocks σ.(st_heap) lsv ((λ p, replicate p.2.(ly_size) MPoison) <$> fn.(f_local_vars)) hs' →
     (* initialize the arguments with the supplied values *)
-    state_alloc_new_blocks σ' lsa vs σ'' →
+    alloc_new_blocks hs' lsa vs hs'' →
     (* add used blocks allocations  *)
     rf = {| rf_fn := fn'; rf_locs := zip lsa fn.(f_args).*2 ++ zip lsv fn.(f_local_vars).*2; |} →
-    expr_step (Call (Val vf) (Val <$> vs)) σ [] (to_rtstmt rf (Goto fn'.(f_init))) σ'' []
+    expr_step (Call (Val vf) (Val <$> vs)) σ [] (to_rtstmt rf (Goto fn'.(f_init))) {| st_heap := hs''; st_fntbl := σ.(st_fntbl)|} []
 | CallFailS σ vf vs f fn:
     val_to_loc vf = Some f →
     σ.(st_fntbl) !! f = Some fn →
@@ -487,7 +484,6 @@ Proof.
   all: repeat select (heap_at _ _ _ _ _) ltac:(fun H => destruct H as [?[?[??]]]).
   all: try (rewrite /heap_fmap/=; eapply heap_update_heap_state_invariant => //).
   all: try (unfold has_layout_val in *; by etransitivity).
-  repeat match goal with H : state_alloc_new_blocks _ _ _ _ |- _ => destruct H as [??] end.
   repeat eapply alloc_new_blocks_invariant => //.
 Qed.
 
@@ -500,7 +496,7 @@ Proof.
   - move => o *.
     revert select (heap_at _ _ _ _ _) => -[?[?[??]]].
     rewrite /heap_fmap/=. eapply heap_update_heap_state_invariant => //.
-    match goal with H : _ `has_layout_val` _ |- _ => try rewrite H // end.
+    match goal with H : _ `has_layout_val` _ |- _ => rewrite H end.
     by destruct o.
   - move => ??? _ Hfree Hinv. by eapply free_blocks_invariant.
 Qed.

theories/lang/lifting.v

@@ -400,11 +400,11 @@ Proof.
   iIntros (Hv1 Hv2 Hop) "#Hl1 #Hl2 HΦ".
   iApply wp_binop. iIntros (σ) "Hσ".
   iAssert ⌜valid_ptr l1 σ.(st_heap)⌝%I as %?. {
-    iApply (alloc_alive_to_valid_ptr with "Hl1 [HΦ] Hσ").
+    iApply (alloc_alive_loc_to_valid_ptr with "Hl1 [HΦ] Hσ").
     by iDestruct "HΦ" as "[$ _]".
   }
   iAssert ⌜valid_ptr l2 σ.(st_heap)⌝%I as %?. {
-    iApply (alloc_alive_to_valid_ptr with "Hl2 [HΦ] Hσ").
+    iApply (alloc_alive_loc_to_valid_ptr with "Hl2 [HΦ] Hσ").
     by iDestruct "HΦ" as "[_ [$ _]]".
   }
   iSplit; first by iPureIntro; eexists _; econstructor.
@@ -655,7 +655,6 @@ Proof.
     iModIntro. iSplit; first done. rewrite /state_ctx. iFrame. iSplit; first done.
     iApply wp_alloc_failed.
   }
-  repeat match goal with H : state_alloc_new_blocks _ _ _ _ |- _ => destruct H as [??] end.
   iMod (heap_alloc_new_blocks_upd with "[$Hhctx $Hbctx]") as "[Hctx Hlv]" => //.
   rewrite big_sepL2_sep. iDestruct "Hlv" as "[Hlv Hfree_v]".
   iMod (heap_alloc_new_blocks_upd with "Hctx") as "[Hctx Hla]" => //.
@@ -667,8 +666,7 @@ Proof.
     iIntros "?". iExists _. iFrame. iPureIntro. split; first by apply replicate_length.
     apply: Forall2_lookup_lr. 2: done. done. rewrite list_lookup_fmap. apply fmap_Some. naive_solver.
   }
-  iFrame. rewrite /=. rewrite H3 H1 /=. iFrame.
-  rewrite stmt_wp_eq. iApply "HQinit" => //.
+  iFrame. rewrite stmt_wp_eq. iApply "HQinit" => //.
 
   (** prove Return *)
   iIntros (v) "Hv". iDestruct ("HΨ'" with "Hv") as "(Ha & Hv & Hs)".

theories/typing/adequacy.v

 From iris.program_logic Require Export adequacy weakestpre.
 From iris.algebra Require Import csum excl auth cmra_big_op gmap.
+From iris.base_logic.lib Require Import ghost_map.
 From refinedc.typing Require Export type.
 From refinedc.typing Require Import programs function bytes globals int fixpoint.
 From refinedc.lang Require Import ghost_state.
@@ -9,17 +10,17 @@ Set Default Proof Using "Type".
 Class typePreG Σ := PreTypeG {
   type_invG                      :> invPreG Σ;
   type_heap_heap_inG             :> inG Σ (authR heapUR);
-  type_heap_alloc_range_map_inG  :> inG Σ (authR alloc_range_mapUR);
-  type_heap_alloc_status_map_inG :> inG Σ (authR alloc_status_mapUR);
-  type_heap_fntbl_inG            :> inG Σ (authR fntblUR);
+  type_heap_alloc_range_map_inG  :> ghost_mapG Σ alloc_id (Z * nat);
+  type_heap_alloc_alive_map_inG  :> ghost_mapG Σ alloc_id bool;
+  type_heap_fntbl_inG            :> ghost_mapG Σ loc function;
 }.
 
 Definition typeΣ : gFunctors :=
   #[invΣ;
-    GFunctor (constRF (authR heapUR));
-    GFunctor (constRF (authR alloc_range_mapUR));
-    GFunctor (constRF (authR alloc_status_mapUR));
-    GFunctor (constRF (authR fntblUR))].
+   GFunctor (constRF (authR heapUR));
+   ghost_mapΣ alloc_id (Z * nat);
+   ghost_mapΣ alloc_id bool;
+   ghost_mapΣ loc function].
 Instance subG_typePreG {Σ} : subG typeΣ Σ → typePreG Σ.
 Proof. solve_inG. Qed.
 
@@ -51,32 +52,26 @@ Proof.
   set h := to_heapUR ∅.
   iMod (own_alloc (● h ⋅ ◯ h)) as (γh) "[Hh _]" => //.
   { apply auth_both_valid_discrete. split => //. }
-  set f := to_fntblUR fns.
-  iMod (own_alloc (● f ⋅ ◯ f)) as (γf) "[Hf Hfm]" => //.
-  { apply auth_both_valid_discrete. split => //. eauto using to_fntbl_valid. }
-  set r := to_alloc_range_mapUR ∅.
-  iMod (own_alloc (● r ⋅ ◯ r)) as (γr) "[Hr _]" => //.
-  { apply auth_both_valid_discrete. split => //. }
-  set s := to_alloc_status_mapUR ∅.
-  iMod (own_alloc (● s ⋅ ◯ s)) as (γs) "[Hs _]" => //.
-  { apply auth_both_valid_discrete. split => //. }
-
+  iMod (ghost_map_alloc fns) as (γf) "[Hf Hfm]".
+  iMod (ghost_map_alloc_empty (V:=(Z * nat))) as (γr) "Hr".
+  iMod (ghost_map_alloc_empty (V:=bool)) as (γs) "Hs".
   set (HheapG := HeapG _ _ γh _ γr _ γs _ γf).
   set (HrefinedCG := RefinedCG _ _ HheapG).
   set (HtypeG := TypeG _ HrefinedCG).
   move: (Hwp HtypeG) => {Hwp} [gl [gt]].
   set (Hglobals := {| global_locs := gl; global_initialized_types := gt; |}).
   move => Hwp.
-  iMod (heap_alloc_new_blocks_upd with "[Hh Hr Hs]") as "[Hctx Hmt]" => //. { by iFrame. }
+  iMod (heap_alloc_new_blocks_upd with "[Hh Hr Hs]") as "[Hctx Hmt]" => //. {
+    rewrite /heap_state_ctx /alloc_range_ctx /to_alloc_range_map /alloc_alive_ctx /to_alloc_alive_map !fmap_empty.
+    by iFrame.
+  }
   rewrite big_sepL2_sep. iDestruct "Hmt" as "[Hmt Hfree]".
-  iMod (Hwp with "Hmt [Hfm]") as "Hmains". {
-    rewrite /f => {f Hwp Hnew}.
-    iInduction (fns) as [] "IH" using map_ind => //.
-    iApply big_sepM_insert => //. rewrite to_fntbl_insert.
-    rewrite (insert_singleton_op); last by apply lookup_to_fntbl_None.
-    rewrite fntbl_entry_eq. iDestruct "Hfm" as "[$ Hfm]".
-    by iApply "IH".
+  iAssert (|==> [∗ map] k↦qs ∈ fns, fntbl_entry k qs)%I with "[Hfm]" as ">Hfm". {
+    iApply big_sepM_bupd. iApply (big_sepM_impl with "Hfm").
+    iIntros "!>" (???) "Hm". rewrite fntbl_entry_eq.
+    by iApply ghost_map_elem_persist.
   }
+  iMod (Hwp with "Hmt Hfm") as "Hmains".
 
   iModIntro. iExists NotStuck, _, (replicate (length thread_mains) (λ _, True%I)), _, _.
   iSplitL "Hctx Hf"; last first. 1: iSplitL "Hmains".