Remove the layout argument of [free_block].

This information is already contained in the allocation map. Removing
makes it easier to relate to the Cerberus memory model interface.

theories/lang/ghost_state.v

@@ -837,7 +837,7 @@ Section free_blocks.
   Lemma heap_free_block_upd σ1 l ly:
     l ↦|ly| -∗
     freeable l (ly_size ly) -∗
-    heap_state_ctx σ1 ==∗ ∃ σ2, ⌜free_block σ1 l ly σ2⌝ ∗ heap_state_ctx σ2.
+    heap_state_ctx σ1 ==∗ ∃ σ2, ⌜free_block σ1 l σ2⌝ ∗ heap_state_ctx σ2.
   Proof.
     iIntros "Hl Hfree (Hinv&Hhctx&Hrctx&Hsctx)". iDestruct "Hinv" as %Hinv.
     rewrite freeable_eq. iDestruct "Hfree" as (aid Haid) "[#Hrange Hkill]".
@@ -845,20 +845,22 @@ Section free_blocks.
     iDestruct (alloc_alive_lookup with "Hsctx Hkill") as %[[???] [??]].
     iDestruct (alloc_range_lookup with "Hrctx Hrange") as %[al'' [?[??]]]. simplify_eq/=.
     iDestruct (heap_mapsto_lookup_1 (λ st : lock_state, st = RSt 0) with "Hhctx Hl") as %? => //.
-    iExists _. iSplitR. { iPureIntro. by econstructor. }
+    iExists _. iSplitR. { iPureIntro. constructor => //. by rewrite Hv. }
     iMod (heap_free_free with "Hhctx Hl") as "Hhctx". rewrite Hv. iFrame => /=.
     iMod (alloc_alive_kill _ _ ({| al_start := l.2; al_len := ly_size ly; al_alive := true |}) with "Hsctx Hkill") as "[$ Hd]".
     erewrite alloc_range_ctx_same_range; [iFrame |done..].
-    iPureIntro. eapply free_block_invariant => //. by eapply FreeBlock.
+    iPureIntro. eapply free_block_invariant => //.
+    assert (ly_size ly = length v) as -> by done. eapply FreeBlock => //.
+    by rewrite Hv.
   Qed.
 
   Lemma heap_free_blocks_upd ls σ1:
-    ([∗ list] l ∈ ls, l.1 ↦|l.2| ∗ freeable l.1 (ly_size l.2)) -∗
+    ([∗ list] l ∈ ls, ∃ ly, l ↦|ly| ∗ freeable l (ly_size ly)) -∗
     heap_state_ctx σ1 ==∗ ∃ σ2, ⌜free_blocks σ1 ls σ2⌝ ∗ heap_state_ctx σ2.
   Proof.
-    iInduction ls as [|[l ly] ls] "IH" forall (σ1).
+    iInduction ls as [|l ls] "IH" forall (σ1).
     { iIntros "_ ? !>". iExists σ1. iFrame. iPureIntro. by constructor. }
-    iIntros "[[Hl Hf] Hls] Hσ" => /=.
+    iIntros "[(%ly&Hl&Hf) Hls] Hσ" => /=.
     iMod (heap_free_block_upd with "Hl Hf Hσ") as (σ2 Hfree) "Hσ".
     iMod ("IH" with "Hls Hσ") as (??) "Hσ".
     iExists _. iFrame. iPureIntro. by econstructor.

theories/lang/heap.v

@@ -269,37 +269,40 @@ Inductive alloc_new_blocks : heap_state → list loc → list val → heap_state
     alloc_new_blocks σ' ls vs σ'' →
     alloc_new_blocks σ (l :: ls) (v :: vs) σ''.
 
-Inductive free_block : heap_state → loc → layout → heap_state → Prop :=
-| FreeBlock σ l aid ly v:
-    let al_alive := Allocation l.2 ly.(ly_size) true  in
-    let al_dead  := Allocation l.2 ly.(ly_size) false in
+Inductive free_block : heap_state → loc → heap_state → Prop :=
+| FreeBlock σ l aid v:
     l.1 = Some aid →
-    σ.(hs_allocs) !! aid = Some al_alive →
-    length v = ly.(ly_size) →
+    σ.(hs_allocs) !! aid = Some (Allocation l.2 (length v) true) →
     heap_lookup_loc l v (λ st, st = RSt 0%nat) σ.(hs_heap) →
-    free_block σ l ly {|
-      hs_heap   := heap_free l.2 ly.(ly_size) σ.(hs_heap);
-      hs_allocs := <[aid := al_dead]> σ.(hs_allocs);
+    free_block σ l {|
+      hs_heap   := heap_free l.2 (length v) σ.(hs_heap);
+      hs_allocs := <[aid := Allocation l.2 (length v) false]> σ.(hs_allocs);
     |}.
 
-Inductive free_blocks : heap_state → list (loc * layout) → heap_state → Prop :=
+Inductive free_blocks : heap_state → list loc → heap_state → Prop :=
 | FreeBlocks_nil σ :
     free_blocks σ [] σ
-| FreeBlocks_cons σ σ' σ'' l ly ls :
-    free_block σ l ly σ' →
+| FreeBlocks_cons σ σ' σ'' l ls :
+    free_block σ l σ' →
     free_blocks σ' ls σ'' →
-    free_blocks σ ((l, ly) :: ls) σ''.
+    free_blocks σ (l :: ls) σ''.
 
-Lemma free_block_inj hs l ly hs1 hs2:
-  free_block hs l ly hs1 → free_block hs l ly hs2 → hs1 = hs2.
-Proof. inversion 1; simplify_eq. by inversion 1; simplify_eq. Qed.
+Lemma free_block_inj hs l hs1 hs2:
+  free_block hs l hs1 → free_block hs l hs2 → hs1 = hs2.
+Proof.
+  inversion 1; inversion 1.
+  revert select (_.1 = Some _).
+  revert select (_.1 = Some _).
+  move => -> ?. simplify_eq.
+  revert select (length _ = length _) => <-. done.
+Qed.
 
 Lemma free_blocks_inj hs1 hs2 hs ls:
   free_blocks hs ls hs1 → free_blocks hs ls hs2 → hs1 = hs2.
 Proof.
   move Heq: {1}(hs) => hs' Hb.
   elim: Hb hs Heq. { move => ?? ->. by inversion 1. }
-  move => ?????? Hb1 ? IH ??.
+  move => ????? Hb1 ? IH ??.
   inversion 1; simplify_eq. apply: IH; [|done].
   by apply: free_block_inj.
 Qed.
@@ -434,13 +437,13 @@ Proof.
   apply IH. by eapply alloc_new_block_invariant.
 Qed.
 
-Lemma free_block_invariant σ1 σ2 l ly:
-  free_block σ1 l ly σ2 →
+Lemma free_block_invariant σ1 σ2 l:
+  free_block σ1 l σ2 →
   heap_state_invariant σ1 →
   heap_state_invariant σ2.
 Proof.
   move => []; clear.
-  move => σ l aid ly v al_a al_d Haid Hal_a Hlen Hlookup H.
+  move => σ l aid v Haid Hal Hlookup H.
   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.
@@ -457,22 +460,22 @@ Proof.
     destruct (Hi2 _ _ Hhc) as [al [??]]. exists al.
     rewrite lookup_insert_ne; first done.
     move => Heq. destruct (Hi1 _ _ Hhc) as [?[?[??]]].
-    subst al_a. simplify_eq. unfold al_end in *. simpl in *. lia.
+    simplify_eq. unfold al_end in *. simpl in *. lia.
   - move => id al /=. destruct (decide (id = aid)) as [->|].
     + rewrite lookup_insert. move => [?]. subst al.
-      assert (allocation_in_range al_a); last done.
+      assert (allocation_in_range (Allocation l.2 (length v) true)); last done.
       by eapply Hi3.
     + rewrite lookup_insert_ne; last done. naive_solver.
   - move => id1 id2 al1 al2 Hne /= Hid1 Hid2 Hal1 Hal2.
     destruct (decide (id1 = aid)) as [->|];
     last (destruct (decide (id2 = aid)) as [->|]).
     + rewrite lookup_insert in Hid1. rewrite lookup_insert_ne // in Hid2.
-      simplify_eq. assert (al_a ## al2); last done.
-      eapply (Hi4 _ _ _ _ Hne Hal_a Hid2); first by eexists.
+      simplify_eq. assert (Allocation l.2 (length v) true ## al2); last done.
+      eapply (Hi4 _ _ _ _ Hne Hal Hid2); first by eexists.
       move: Hal2 => [?[/=]]. rewrite lookup_insert_ne //. by eexists.
     + rewrite lookup_insert in Hid2. rewrite lookup_insert_ne // in Hid1.
-      simplify_eq. assert (al1 ## al_a); last done.
-      eapply (Hi4 _ _ _ _ Hne Hid1 Hal_a); last by eexists.
+      simplify_eq. assert (al1 ## Allocation l.2 (length v) true); last done.
+      eapply (Hi4 _ _ _ _ Hne Hid1 Hal); last by eexists.
       move: Hal1 => [?[/=]]. rewrite lookup_insert_ne //. by eexists.
     + destruct Hal1 as [a1 [Ha1 ?]]. destruct Hal2 as [a2 [Ha2 ?]].
       rewrite !lookup_insert_ne // in Hid1, Hid2, Ha1, Ha2.
@@ -482,8 +485,8 @@ Proof.
     rewrite lookup_insert_ne // in Hid, Hal1. simplify_eq.
     rewrite heap_free_lookup_not_in_range;
     first (eapply Hi5 => //; by eexists). move => ?.
-    assert (al ## al_a) as Hdisj.
-    { apply (Hi4 _ _ _ _ H Hid Hal_a); by eexists. }
+    assert (al ## Allocation l.2 (length v) true) as Hdisj.
+    { apply (Hi4 _ _ _ _ H Hid Hal); by eexists. }
     erewrite elem_of_disjoint in Hdisj. by eapply Hdisj.
 Qed.
 
@@ -492,7 +495,7 @@ Lemma free_blocks_invariant σ1 σ2 ls:
   heap_state_invariant σ1 →
   heap_state_invariant σ2.
 Proof.
-  elim => [] // ?????? Hb Hbs IH H.
+  elim => [] // ????? Hb Hbs IH H.
   apply IH. by eapply free_block_invariant.
 Qed.
 

theories/lang/lang.v

@@ -108,7 +108,7 @@ Record runtime_function := {
   rf_fn : function;
   (* locations in the stack frame (locations of arguments and local
   vars allocated on Call, need to be freed by Return) *)
-  rf_locs: list (loc * layout);
+  rf_locs: list loc;
 }.
 
 Inductive runtime_expr :=
@@ -418,7 +418,7 @@ comparing pointers? (see lambda rust) *)
     (* initialize the arguments with the supplied values *)
     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; |} →
+    rf = {| rf_fn := fn'; rf_locs := lsa ++ lsv; |} →
     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 →

theories/lang/lifting.v

@@ -692,18 +692,21 @@ Proof.
   iIntros (v) "Hv". iDestruct ("HΨ'" with "Hv") as "(Ha & Hv & Hs)".
   iApply wp_lift_stmt_step => //.
   iIntros (σ3) "(Hctx&?)".
-  iMod (heap_free_blocks_upd (zip lsa (f_args fn).*2 ++ zip lsv (f_local_vars fn).*2) with "[Ha Hfree_a Hv Hfree_v] Hctx") as (σ2 Hfree) "Hctx". {
-    rewrite big_sepL_app !big_sepL_sep !big_sepL2_alt.
-    iDestruct "Ha" as "[% Ha]". iDestruct "Hv" as "[% Hv]".
-    iDestruct "Hfree_a" as "[% Hfree_a]". iDestruct "Hfree_v" as "[% Hfree_v]".
-    rewrite !zip_fmap_r !big_sepL_fmap/=. iFrame.
-    setoid_rewrite replicate_length. iFrame.
-    iApply (big_sepL_impl' with "Hfree_a").
-    { rewrite !zip_with_length !min_l ?fmap_length //; lia. }
-    iIntros (??? [?[v0[?[??]]]]%lookup_zip_with_Some [?[ly0[?[??]]]]%lookup_zip_with_Some) "!> H2"; simplify_eq/=.
-    have -> : v0 `has_layout_val` ly0.2; last done.
-    eapply Forall2_lookup_lr; [done..|].
-    rewrite list_lookup_fmap fmap_Some. naive_solver.
+  iMod (heap_free_blocks_upd (lsa ++ lsv) with "[Ha Hfree_a Hv Hfree_v] Hctx") as (σ2 Hfree) "Hctx". {
+    rewrite big_sepL_app. iSplitL "Ha Hfree_a".
+    - revert Hly. generalize (f_args fn). clear. move => args Hargs.
+      iInduction lsa as [|l lsa] "IH" forall (vl args Hargs); first done. simpl.
+      destruct args; first done. destruct vl; first done.
+      iDestruct "Ha" as "[Hl1 Ha]". iDestruct "Hfree_a" as "[Hl2 Hfree_a]".
+      rewrite fmap_cons in Hargs. apply Forall2_cons_inv in Hargs as [Hly Hargs].
+      iSplitL "Hl1 Hl2". { iExists _. iFrame. by rewrite Hly. }
+      iApply ("IH" $! vl args Hargs with "Ha Hfree_a").
+    - generalize (f_local_vars fn). clear. move => vars.
+      iInduction lsv as [|l lsv] "IH" forall (vars); first done. simpl.
+      destruct vars; first done.
+      iDestruct "Hv" as "[Hl1 Hv]". iDestruct "Hfree_v" as "[Hl2 Hfree_v]".
+      iSplitL "Hl1 Hl2". { iExists _. iFrame. by rewrite replicate_length. }
+      iApply ("IH" $! vars with "Hv Hfree_v").
   }
   iModIntro.
   iSplit; first by eauto 8 using ReturnS.