Use separate inductives for allocation (refactoring).

theories/lang/base.v

@@ -62,6 +62,14 @@ Proof. by intros ?? ->%leibniz_equiv. Qed.
 Lemma zip_fmap_r {A B C} (l1 : list A) (l2 : list B) (f : B → C) :
   zip l1 (f <$> l2) = (λ x, (x.1, f x.2)) <$>  zip l1 l2.
 Proof. rewrite zip_with_fmap_r zip_with_zip. by apply: list_fmap_ext => // [[]]. Qed.
+
+Lemma zip_with_nil_inv' {A B C : Type} (f : A → B → C) (l1 : list A) (l2 : list B) :
+  length l1 = length l2 → zip_with f l1 l2 = [] → l1 = [] ∧ l2 = [].
+Proof.
+  move => Hlen /zip_with_nil_inv [] H; rewrite H /= in Hlen;
+  split => //; by apply nil_length_inv.
+Qed.
+
 Lemma entails_eq {PROP : bi} (P1 P2 : PROP) :
   P1 = P2 → P1 -∗ P2.
 Proof. move => ->. reflexivity. Qed.

theories/lang/heap.v

@@ -210,6 +210,16 @@ Section blocks_used_agree.
     assert (l.1 ∉ dom (gset alloc_id) ub); last by set_solver.
     by rewrite elem_of_dom Hl.
   Qed.
+
+  Lemma blocks_used_agree_update l v h flk allocs:
+    blocks_used_agree h allocs →
+    allocs !! l.1 = None →
+    heap_block_free h l →
+    blocks_used_agree (heap_upd l v flk h) (<[l.1:=to_allocation l.2 (length v)]> allocs).
+  Proof.
+    move => Hagree Hnone Hfree l' /lookup_insert_None[??] ?.
+    rewrite heap_upd_lookup_ne //. by apply: Hagree.
+  Qed.
 End blocks_used_agree.
 
 Section allocs.
@@ -636,3 +646,36 @@ Section heap.
     by iApply (heap_free_free with "Hown").
   Qed.
 End heap.
+
+Section alloc_new_blocks.
+  Context `{!heapG Σ}.
+
+  Lemma heap_alloc_new_block_upd σ1 l v σ2:
+    alloc_new_block σ1 l v σ2 →
+    state_ctx σ1 ==∗
+      state_ctx σ2 ∗
+      allocs_entry l.1 (to_allocation l.2 (length v)) ∗
+      l ↦ v.
+  Proof.
+    iIntros (Halloc) "Hctx". iDestruct "Hctx" as (Hagree) "(Hhctx&Hbctx&Hfctx)".
+    inversion_clear Halloc.
+    iMod (allocs_alloc (st_allocs σ1) l.1 (to_allocation l.2 (length v))
+            with "Hbctx") as "[Hbctx Hb]"; first done.
+    iDestruct (allocs_entry_to_loc_in_bounds l (length v)
+                 with "Hb") as "#Hinb"; first by naive_solver.
+    iMod (heap_alloc l (st_heap σ1) v with "[Hhctx $Hinb]") as "[Hhctx Hv]" => //.
+    iModIntro. iFrame. iPureIntro => /=. by apply blocks_used_agree_update.
+  Qed.
+
+  Lemma heap_alloc_new_blocks_upd σ1 ls vs σ2:
+    alloc_new_blocks σ1 ls vs σ2 →
+    state_ctx σ1 ==∗
+      state_ctx σ2 ∗
+      ([∗ list] l; v ∈ ls; vs, allocs_entry l.1 (to_allocation l.2 (length v))) ∗
+      ([∗ list] l; v ∈ ls; vs, l ↦ v).
+  Proof.
+    move => H. iInduction H as [] "IH"; first by iIntros "$ !>" => //=.
+    iIntros "H". iMod (heap_alloc_new_block_upd with "H") as "(H&Ha&Hl)" => //.
+    iFrame. by iApply "IH".
+  Qed.
+End alloc_new_blocks.

theories/lang/lang.v

@@ -209,8 +209,9 @@ Delimit Scope loc_scope with L.
 Open Scope loc_scope.
 
 Definition alloc_id := Z.
+Definition addr := Z.
 
-Definition loc : Set := alloc_id * Z.
+Definition loc : Set := alloc_id * addr.
 Bind Scope loc_scope with loc.
 
 Inductive mbyte : Set :=
@@ -1010,6 +1011,24 @@ Definition subst_function (xs : list var_name) (vs : list val) (f : function) :
 Definition to_allocation (off : Z) (len : nat) : allocation :=
   Allocation off (off + len).
 
+Inductive alloc_new_block : state → loc → val → state → Prop :=
+| AllocNewBlock σ l v:
+    σ.(st_allocs) !! l.1 = None →
+    heap_block_free σ.(st_heap) l →
+    alloc_new_block σ l v {|
+      st_heap   := heap_upd l v (λ _, RSt 0%nat) σ.(st_heap);
+      st_allocs := <[l.1 := to_allocation l.2 (length v)]> σ.(st_allocs);
+      st_fntbl  := σ.(st_fntbl); st_alloc_failure := σ.(st_alloc_failure);
+    |}.
+
+Inductive alloc_new_blocks : state → list loc → list val → state → Prop :=
+| AllocNewBlock_nil σ :
+    alloc_new_blocks σ [] [] σ
+| AllocNewBlock_cons σ σ' σ'' l v ls vs :
+    alloc_new_block σ l v σ' →
+    alloc_new_blocks σ' ls vs σ'' →
+    alloc_new_blocks σ (l :: ls) (v :: vs) σ''.
+
 (*** Evaluation of statements *)
 Inductive simple_stmt_step : thread_state → state → list Empty_set → thread_state → state → list thread_state → Prop :=
 | StmtExprS ts σ σ' Ks e e' os efs:
@@ -1043,7 +1062,7 @@ Inductive simple_stmt_step : thread_state → state → list Empty_set → threa
      (update_stmt {| ts_conts := cs; ts_rfn := co.(c_rfn); ts_alloc_failure := false; |} (subst_stmt [co.(c_rvar)] [v] co.(c_rfn).(rf_stmt)))
      (* deallocate the stack *)
      (heap_fmap (heap_free_list ts.(ts_rfn).(rf_locs)) σ) []
-| CallS lsa lsv ts σ vf vs s co f rf fn fn' h' h'' ret ub':
+| CallS lsa lsv ts σ σ' σ'' vf vs s co f rf fn fn' ret :
     ts.(ts_rfn).(rf_stmt) = Call ret (Val vf) (Val <$> vs) s →
     val_to_loc vf = Some f →
     σ.(st_fntbl) !! f = Some fn →
@@ -1053,28 +1072,19 @@ Inductive simple_stmt_step : thread_state → state → list Empty_set → threa
     fn' = subst_function (fn.(f_args).*1 ++ fn.(f_local_vars).*1) (val_of_loc <$> (lsa ++ lsv)) fn →
     (* check the layout of the arguments *)
     Forall2 has_layout_val vs fn.(f_args).*2 →
-    (* ensure that ls points to free blocks *)
-    Forall (heap_block_free σ.(st_heap)) lsa →
-    Forall (heap_block_free σ.(st_heap)) lsv →
-    (* ensure that ls blocks are unused *)
-    Forall (λ l, σ.(st_allocs) !! l.1 = None) lsa →
-    Forall (λ l, σ.(st_allocs) !! l.1 = None) lsv →
     (* ensure that locations are aligned *)
     Forall2 has_layout_loc lsa fn.(f_args).*2 →
     Forall2 has_layout_loc lsv fn.(f_local_vars).*2 →
-    (* ensure that the blocks in ls are disjoint *)
-    NoDup (lsa ++ lsv).*1 →
     (* initialize the local vars to poison *)
-    heap_upd_list lsv ((λ p, replicate p.2.(ly_size) MPoison) <$> fn.(f_local_vars)) (λ _, RSt 0%nat) σ.(st_heap) = h' →
+    alloc_new_blocks σ lsv ((λ p, replicate p.2.(ly_size) MPoison) <$> fn.(f_local_vars)) σ' →
     (* initialize the arguments with the supplied values *)
-    heap_upd_list lsa vs (λ _, RSt 0%nat) h' = h'' →
+    alloc_new_blocks σ' lsa vs σ'' →
     (* add used blocks allocations  *)
-    list_to_map (zip (lsa.*1 ++ lsv.*1) (zip_with to_allocation (lsa.*2 ++ lsv.*2) (ly_size <$> (fn.(f_args).*2 ++ fn.(f_local_vars).*2)))) ∪ σ.(st_allocs) = ub' →
-    rf = {| rf_fn := fn'; rf_locs := zip lsa fn.(f_args).*2 ++ zip lsv fn.(f_local_vars).*2; rf_stmt := Goto fn'.(f_init); |} →
+    rf = {| rf_fn := fn'; rf_locs := zip lsa fn.(f_args).*2 ++ zip lsv fn.(f_local_vars).*2;
+            rf_stmt := Goto fn'.(f_init); |} →
     co = {| c_rfn := (update_stmt ts s).(ts_rfn); c_rvar := ret |} →
     simple_stmt_step ts σ []
-      {| ts_conts := co::ts.(ts_conts); ts_rfn := rf; ts_alloc_failure := ts.(ts_alloc_failure); |}
-      {| st_heap:= h''; st_fntbl := σ.(st_fntbl); st_allocs := ub'; st_alloc_failure := σ.(st_alloc_failure); |} []
+      {| ts_conts := co::ts.(ts_conts); ts_rfn := rf; ts_alloc_failure := ts.(ts_alloc_failure); |} σ'' []
 | CallFailS ts σ vf vs s f fn ret:
     ts.(ts_rfn).(rf_stmt) = Call ret (Val vf) (Val <$> vs) s →
     val_to_loc vf = Some f →

theories/lang/lifting.v

@@ -531,82 +531,23 @@ Proof.
     iIntros "!> !>". iMod "HE" as "_". iIntros "!>". iSplit; first done.
     rewrite /state_ctx. iFrame. iSplit; first done. iIntros (?). done.
   }
-  match goal with | H : NoDup _ |- _ => rewrite ->fmap_app, NoDup_app in H; revert H end.
-  move => [? [? ?]].
-  repeat match goal with | H : Forall (fun l => _ !! _ = None) _ |- _ => move/Forall_forall in H end.
-  revert select (length lsa = _) => Hlena.
-  revert select (length lsv = _) => Hlenv.
-
-  (* Allocate new allocation blocks for the local variables. *)
-  iMod (allocs_alloc_list lsv (((λ p, replicate (ly_size p.2) ☠%V) <$> f_local_vars fn))
-          with "Hbctx") as "[Hbctx Hblsv]" => //.
-  { apply elem_of_disjoint => id Hdom Hin. move: Hdom. apply/not_elem_of_dom. set_solver. }
-  { by rewrite fmap_length. }
-
-  (* Allocate heap segments for the local variables. *)
-  iMod (heap_alloc_list lsv (((λ p, replicate (ly_size p.2) ☠%V) <$> f_local_vars fn))
-          with "[Hhctx $Hblsv]") as "[Hhctx Hv]" => //.
-  { by rewrite fmap_length. }
-
-  (* Allocate new allocation blocks for the function arguments. *)
-  iMod (allocs_alloc_list lsa vs with "Hbctx") as "[Hbctx Hblsa]" => //.
-  { apply elem_of_disjoint => id. rewrite dom_union => Hid1 /elem_of_list_to_set Hlsa. move: Hid1.
-    apply/not_elem_of_union. split; [ | apply/not_elem_of_dom; set_solver].
-    rewrite dom_list_to_map_L fst_zip. { apply/elem_of_list_to_set. naive_solver. }
-    rewrite zip_with_length !fmap_length Hlenv. lia. }
-  { by etrans. }
-
-  (* Allocate heap segments for the function arguments. *)
-  iMod (heap_alloc_list lsa vs with "[Hhctx $Hblsa]") as "[$ Ha]" => //.
-  { apply Forall_forall => [[??]] Hin. apply heap_block_free_upd_list.
-    by eapply (Forall_forall _ lsa). set_solver. }
-  { by etrans. }
-
-  rewrite /= [in list_to_map _ ∪ (list_to_map _ ∪ _)]assoc -list_to_map_app.
-  rewrite -zip_with_app.
-  2: { rewrite zip_with_length !fmap_length Min.min_l //. by rewrite Hlena Hlen_vs. }
-  rewrite -zip_with_app; last by rewrite !fmap_length Hlena Hlen_vs.
-
-  have -> : (length <$> vs) = ly_size <$> (f_args fn).*2. {
-    move: Hly. clear. move: (f_args fn).*2 => f. elim => //. by csimpl => ???? -> ? ->.
-  }
-  have -> : (length <$> ((λ p, replicate (ly_size p.2) ☠%V) <$> f_local_vars fn)) =
-            ly_size <$> (f_local_vars fn).*2. {
-    rewrite -!list_fmap_compose. apply list_fmap_ext => // -[??] /=. by rewrite replicate_length.
-  }
-  rewrite -(fmap_app ly_size).
-
+  iMod (heap_alloc_new_blocks_upd with "[$Hhctx $Hbctx $Hfctx]") as "[Hctx [Hv' Hv]]" => //.
+  iMod (heap_alloc_new_blocks_upd with "Hctx") as "[Hctx [Ha' Ha]]" => //.
   iModIntro. iNext.
   iDestruct ("HWP" $! lsa lsv with "[//] Ha [Hv]") as (Ψ') "(HQinit & HΨ')". {
     rewrite big_sepL2_fmap_r. iApply (big_sepL2_mono with "Hv") => ??? ?? /=.
     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.
   }
-  iMod "HE" as "_". iModIntro. iSplit; first done. iFrame.
-  rewrite -(update_stmt_id {| ts_rfn := _; ts_conts := _|}) /=.
-  iSplit. {
-    iPureIntro => /=.
-    apply: blocks_used_agree_heap_upd_list_in.
-    { rewrite dom_union dom_list_to_map fst_zip; first by set_solver.
-      rewrite zip_with_length !app_length !fmap_length Min.min_l //.
-      rewrite !app_length !fmap_length Hlena Hlenv. done. }
-    apply: blocks_used_agree_heap_upd_list_in.
-    { rewrite dom_union dom_list_to_map fst_zip; first by set_solver.
-      rewrite zip_with_length !app_length !fmap_length Min.min_l //.
-      rewrite !app_length !fmap_length Hlena Hlenv. done. }
-    move => l' Hl'. apply Hub. by apply lookup_union_None in Hl' as [??].
-  }
-  iIntros (_).
+  iMod "HE" as "_". iModIntro. iSplit; first done. iFrame. iIntros (_).
   iApply (wps_wand with "HQinit").
-
   (** prove Return *)
   iIntros (v) "Hv HWP". iDestruct ("HΨ'" with "Hv") as "(Ha & Hv & Hs)".
-  rewrite update_stmt_update.
   iApply wp_lift_stmt_step => //; first by right.
   iIntros (σ3) "(%&Hhctx&Hfctx)".
   iMod (fupd_intro_mask' _ ∅) as "HE"; first set_solver. iModIntro.
   iSplit; first by eauto 8 using ReturnS.
-  iIntros (os ts3 σ2 ? Hst). inv_stmt_step. iIntros "!> !>".
+  iIntros (os ts3 σ2' ? Hst). inv_stmt_step. iIntros "!> !>".
   iMod "HE" as "$". iFrame. rewrite /heap_fmap/= heap_free_list_app /=.
   rewrite -!(big_sepL2_fmap_r snd (λ _ l ly, l↦|ly|)%I).
   iMod (heap_free_list_free with "Hhctx Hv") as "Hhctx".