wp_alloc provides a vector of allocated values

theories/lang/lifting.v

@@ -40,16 +40,19 @@ Lemma wp_bindi {E e} Ki Φ :
      WP fill_item Ki e @ E {{ Φ }}.
 Proof. exact: weakestpre.wp_bind. Qed.
 
-Lemma wp_alloc E n:
+Lemma wp_alloc E (n : Z) :
   0 < n →
   {{{ True }}} Alloc (Lit $ LitInt n) @ E
-  {{{ l vl, RET LitV $ LitLoc l; ⌜n = length vl⌝ ∗ †l…(Z.to_nat n) ∗ l ↦∗ vl }}}.
+  {{{ l sz (vl : vec val sz), RET LitV $ LitLoc l; ⌜n = sz⌝ ∗ †l…(Z.to_nat n) ∗ l ↦∗ vl }}}.
 Proof.
   iIntros (? Φ) "HΦ". iApply wp_lift_atomic_head_step_no_fork; auto.
   iIntros (σ1) "Hσ !>"; iSplit; first by auto.
   iNext; iIntros (v2 σ2 efs Hstep); inv_head_step.
   iMod (heap_alloc with "Hσ") as "[Hσ Hl]"; [done..|].
-  iModIntro; iSplit=> //. iFrame. iApply "HΦ"; auto.
+  iModIntro; iSplit=> //. iFrame.
+  (* FIXME: Merging these two into one "iApply" doesn't work. *)
+  iSpecialize ("HΦ" $! _ (length init)). iApply ("HΦ" $! (list_to_vec init)).
+  rewrite vec_to_list_of_list. auto.
 Qed.
 
 Lemma wp_free E (n:Z) l vl :

theories/lang/new_delete.v

@@ -25,7 +25,10 @@ Section specs.
     iIntros (? Φ) "HΦ". wp_lam. wp_op; intros ?.
     - wp_if. assert (n = 0) as -> by lia. iApply ("HΦ" $! _ []).
       rewrite heap_mapsto_vec_nil. auto.
-    - wp_if. wp_alloc l vl as "H↦" "H†". iApply  "HΦ". iFrame. auto.
+    - wp_if. wp_alloc l vl as "H↦" "H†".
+      (* FIXME: I have to state the coercion vec_to_list explicitly here. *)
+      iApply ("HΦ" $! _ (vec_to_list vl)).
+      rewrite vec_to_list_length -{2}Hsz Z2Nat.id //. iFrame. auto.
   Qed.
 
   Lemma wp_delete E (n:Z) l vl :

theories/lang/proofmode.v

@@ -146,7 +146,7 @@ Implicit Types Δ : envs (iResUR Σ).
 Lemma tac_wp_alloc Δ Δ' E j1 j2 n Φ :
   0 < n →
   IntoLaterNEnvs 1 Δ Δ' →
-  (∀ l vl, n = length vl → ∃ Δ'',
+  (∀ l sz (vl : vec val sz), n = sz → ∃ Δ'',
     envs_app false (Esnoc (Esnoc Enil j1 (l ↦∗ vl)) j2 (†l…(Z.to_nat n))) Δ'
       = Some Δ'' ∧
     (Δ'' ⊢ Φ (LitV $ LitLoc l))) →
@@ -154,10 +154,10 @@ Lemma tac_wp_alloc Δ Δ' E j1 j2 n Φ :
 Proof.
   intros ?? HΔ. rewrite -wp_fupd. eapply wand_apply; first exact:wp_alloc.
   rewrite -always_and_sep_l. apply and_intro; first done.
-  rewrite into_laterN_env_sound; apply later_mono, forall_intro=> l;
-  apply forall_intro=> vl. apply wand_intro_l. rewrite -assoc.
+  rewrite into_laterN_env_sound; apply later_mono, forall_intro=> l.
+  apply forall_intro=>sz. apply forall_intro=> vl. apply wand_intro_l. rewrite -assoc.
   apply pure_elim_sep_l=> Hn. apply wand_elim_r'.
-  destruct (HΔ l vl) as (Δ''&?&HΔ'). done.
+  destruct (HΔ l _ vl) as (Δ''&?&HΔ'); first done.
   rewrite envs_app_sound //; simpl. by rewrite right_id HΔ' -fupd_intro.
 Qed.
 
@@ -233,7 +233,16 @@ Tactic Notation "wp_alloc" ident(l) ident(vl) "as" constr(H) constr(Hf) :=
     eapply tac_wp_alloc with _ H Hf;
       [try fast_done
       |apply _
-      |first [intros l vl ? | fail 1 "wp_alloc:" l "or" vl "not fresh"];
+      |let sz := fresh "sz" in let Hsz := fresh "Hsz" in
+       first [intros l sz vl Hsz | fail 1 "wp_alloc:" l "or" vl "not fresh"];
+       (* If Hsz is "constant Z = nat", change that to an equation on nat and
+          potentially substitute away the sz. *)
+       try (match goal with Hsz : ?x = _ |- _ => rewrite <-(Z2Nat.id x) in Hsz; last done end;
+            apply Nat2Z.inj in Hsz;
+            try (cbv [Z.to_nat Pos.to_nat] in Hsz;
+                 simpl in Hsz;
+                 (* Substitute only if we have a literal nat. *)
+                 match goal with Hsz : S _ = _ |- _ => subst sz end));
         eexists; split;
           [env_cbv; reflexivity || fail "wp_alloc:" H "or" Hf "not fresh"
           |wp_finish]]

theories/lang/spawn.v

@@ -67,14 +67,9 @@ Lemma spawn_spec (Ψ : val → iProp Σ) e (f : val) :
     spawn [e] {{{ c, RET #c; join_handle c Ψ }}}.
 Proof.
   iIntros (<-%of_to_val Φ) "Hf HΦ". rewrite /spawn /=.
-  wp_let. wp_alloc l vl as "Hl" "H†". wp_let.
+  wp_let. wp_alloc l vl as "Hl" "H†". wp_let. inv_vec vl=>v0 v1.
   iMod (own_alloc (Excl ())) as (γf) "Hγf"; first done.
   iMod (own_alloc (Excl ())) as (γj) "Hγj"; first done.
-  (* TODO: maybe we should get vl as a vector here instead of a separate hypothesis for the length? *)
-  assert (2 = length vl)%nat as Hvl.
-  { apply Nat2Z.inj. done. }
-  destruct vl as [|v0 vl]; first done. destruct vl as [|v1 vl]; first done.
-  destruct vl; last done. clear H Hvl.
   rewrite heap_mapsto_vec_cons heap_mapsto_vec_singleton.
   iDestruct "Hl" as "[Hc Hd]". wp_write. clear v0.
   iMod (inv_alloc N _ (spawn_inv γf γj l Ψ) with "[Hc]") as "#?".