tweak type_new to get a nice natural number for the new size

00ee1d5e · Ralf Jung · d7d27fb7 · 00ee1d5e · 00ee1d5e · 00ee1d5e
Commit 00ee1d5e authored 8 years ago by Ralf Jung
--- a/theories/typing/examples/lazy_lft.v
+++ b/theories/typing/examples/lazy_lft.v
@@ -24,8 +24,8 @@ Section lazy_lft.
    iApply (type_newlft []). iIntros (α).
    iApply (type_new_subtype (Π[uninit 1;uninit 1])); [solve_typing..|].
      iIntros (t). simpl_subst.
-    iApply type_new; [solve_typing|]. iIntros (f). simpl_subst.
-    iApply type_new; [solve_typing|]. iIntros (g). simpl_subst.
+    iApply type_new; [solve_typing..|]. iIntros (f). simpl_subst.
+    iApply type_new; [solve_typing..|]. iIntros (g). simpl_subst.
    iApply type_int. iIntros (v42). simpl_subst.
    iApply type_assign; [solve_typing..|].
    iApply (type_assign _ (&shr{α}_)); [solve_typing..|].

--- a/theories/typing/lft_contexts.v
+++ b/theories/typing/lft_contexts.v
@@ -287,6 +287,7 @@ Lemma elctx_sat_submseteq `{invG Σ, lftG Σ} E E' L :
  E' ⊆+ E → elctx_sat E L E'.
 Proof. iIntros (HE' ?) "_ !# H". by iApply big_sepL_submseteq. Qed.

+(* TODO: This is not really the right file for stuff like this. *)
 Hint Constructors Forall Forall2 elem_of_list : lrust_typing.
 Hint Resolve of_val_unlock : lrust_typing.
 Hint Resolve
@@ -299,6 +300,9 @@ Hint Resolve

 Hint Resolve elctx_sat_submseteq | 100 : lrust_typing.

+Hint Extern 1 (@eq nat _ (Z.to_nat _)) => (etrans; [symmetry; exact: Nat2Z.id | reflexivity]) : lrust_typing.
+Hint Extern 1 (@eq nat (Z.to_nat _) _) => (etrans; [exact: Nat2Z.id | reflexivity]) : lrust_typing.
+
 (* FIXME : I would prefer using a [Hint Resolve <-] for this, but
   unfortunately, this is not preserved across modules. See:
     https://coq.inria.fr/bugs/show_bug.cgi?id=5189

--- a/theories/typing/lib/cell.v
+++ b/theories/typing/lib/cell.v
@@ -155,7 +155,7 @@ Section typing.
      iIntros (α ϝ ret arg). inv_vec arg=>c x. simpl_subst.
    iApply type_deref; [solve_typing..|].
    iIntros (c'); simpl_subst.
-    iApply type_new; [solve_typing..|]. iIntros (r); simpl_subst.
+    iApply type_new; [solve_typing..|]; iIntros (r); simpl_subst.
    (* Drop to Iris level. *)
    iIntros (tid) "#LFT #HE Htl HL HC".
    rewrite 3!tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
@@ -170,11 +170,11 @@ Section typing.
    iDestruct (ty_size_eq with "Hrown") as ">Heq". iDestruct "Heq" as %Heq.
    (* FIXME: Changing the order of $Hr↦ $Hc'↦ breaks applying...?? *)
    wp_apply (wp_memcpy with "[$Hr↦ $Hc'↦]").
-    { by rewrite Heq Nat2Z.id. }
+    { by rewrite Heq. }
    { f_equal. done. }
    iIntros "[Hr↦ Hc'↦]". wp_seq.
    iDestruct "Hx" as "[Hx↦ Hx†]". iDestruct "Hx↦" as (vx) "[Hx↦ Hxown]".
-    rewrite Nat2Z.id. iDestruct (ty_size_eq with "Hxown") as "#%".
+    iDestruct (ty_size_eq with "Hxown") as "#%".
    wp_apply (wp_memcpy with "[$Hc'↦ $Hx↦]"); try by f_equal.
    iIntros "[Hc'↦ Hx↦]". wp_seq.
    iMod ("Hclose2" with "[Hc'↦ Hxown] Htl") as "[Htok Htl]"; first by auto with iFrame.

--- a/theories/typing/lib/mutex/mutex.v
+++ b/theories/typing/lib/mutex/mutex.v
@@ -104,8 +104,9 @@ Section code.
  Proof.
    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
      iIntros (_ ϝ ret arg). inv_vec arg=>x. simpl_subst.
-    iApply type_new; [solve_typing..|]; iIntros (m); simpl_subst.
-    rewrite (Nat2Z.id (S ty.(ty_size))). (* FIXME: Having to do this after every type_new is rather annoying... *)
+    (* FIXME: It should be possible to infer the `S ty.(ty_size)` here.
+       This should be done in the @eq external hints added in lft_contexts.v. *)
+    iApply (type_new (S ty.(ty_size))); [solve_typing..|]; iIntros (m); simpl_subst.
    (* FIXME: The following should work.  We could then go into Iris later.
    iApply (type_memcpy ty); [solve_typing..|]. *)
    (* Switch to Iris. *)
@@ -145,8 +146,7 @@ Section code.
  Proof.
    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
      iIntros (_ ϝ ret arg). inv_vec arg=>m. simpl_subst.
-    iApply type_new; [solve_typing..|]; iIntros (x); simpl_subst.
-    rewrite (Nat2Z.id ty.(ty_size)).
+    iApply (type_new ty.(ty_size)); [solve_typing..|]; iIntros (x); simpl_subst.
    (* Switch to Iris. *)
    iIntros (tid) "#LFT #HE Hna HL Hk [Hx [Hm _]]".
    rewrite !tctx_hasty_val /=.

--- a/theories/typing/lib/mutex/mutexguard.v
+++ b/theories/typing/lib/mutex/mutexguard.v
@@ -112,8 +112,7 @@ Section code.
    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
      iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
    iApply type_deref; [solve_typing..|]; iIntros (m); simpl_subst.
-    iApply type_new; [solve_typing..|]; iIntros (g); simpl_subst.
-    rewrite (Nat2Z.id 1). (* Having to do this is rather annoying... *)
+    iApply (type_new 1); [solve_typing..|]; iIntros (g); simpl_subst.
    (* Switch to Iris. *)
    iIntros (tid) "#LFT #HE Hna HL Hk [Hg [Hx [Hm _]]]".
    rewrite !tctx_hasty_val [[x]]lock /=.

--- a/theories/typing/lib/rc/rc.v
+++ b/theories/typing/lib/rc/rc.v
@@ -359,10 +359,10 @@ Section code.
  Proof.
    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
      iIntros (_ ϝ ret arg). inv_vec arg=>x. simpl_subst.
-    iApply type_new; [solve_typing..|]; iIntros (rcbox); simpl_subst.
-    iApply type_new; [solve_typing..|]; iIntros (rc); simpl_subst.
+    iApply (type_new (2 + ty.(ty_size))); [solve_typing..|]; iIntros (rcbox); simpl_subst.
+    iApply (type_new 1); [solve_typing..|]; iIntros (rc); simpl_subst.
    iIntros (tid) "#LFT #HE Hna HL Hk [Hrc [Hrcbox [Hx _]]]".
-    rewrite (Nat2Z.id (2 + ty.(ty_size))) !tctx_hasty_val.
+    rewrite !tctx_hasty_val.
    iDestruct (ownptr_own with "Hx") as (lx vlx) "(% & Hx↦ & Hx & Hx†)". subst x.
    iDestruct (ownptr_uninit_own with "Hrcbox")
      as (lrcbox vlrcbox) "(% & Hrcbox↦ & Hrcbox†)". subst rcbox. inv_vec vlrcbox=>???.
@@ -402,8 +402,7 @@ Section code.
  Proof.
    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
      iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
-    iApply type_new; [solve_typing..|]; iIntros (r); simpl_subst.
-    rewrite (Nat2Z.id 1). (* Having to do this is rather annoying... *)
+    iApply (type_new 1); [solve_typing..|]; iIntros (r); simpl_subst.
    iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
    iIntros (tid) "#LFT #HE Hna HL Hk [Hx [Hrc' [Hr _]]]".
    rewrite !tctx_hasty_val [[x]]lock.
@@ -466,7 +465,7 @@ Section code.
  Proof.
    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
      iIntros (α ϝ ret arg). inv_vec arg=>rcx. simpl_subst.
-    iApply type_new; [solve_typing..|]; iIntros (x); simpl_subst. rewrite (Nat2Z.id 1).
+    iApply (type_new 1); [solve_typing..|]; iIntros (x); simpl_subst.
    iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
    iIntros (tid) "#LFT #HE Hna HL Hk [Hrcx [#Hrc' [Hx _]]]".
    rewrite !tctx_hasty_val [[rcx]]lock.
@@ -528,8 +527,7 @@ Section code.
    (* TODO: There is a *lot* of duplication between this proof and the one for drop. *)
    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
    iIntros (_ ϝ ret arg). inv_vec arg=>rcx. simpl_subst.
-    iApply type_new; [solve_typing..|]; iIntros (r); simpl_subst.
-    rewrite (Nat2Z.id (Σ[ ty; rc ty ]).(ty_size)).
+    iApply (type_new (Σ[ ty; rc ty ]).(ty_size)); [solve_typing..|]; iIntros (r); simpl_subst.
    iApply (type_cont [] [ϝ ⊑ₗ []]
                      (λ _, [rcx ◁ box (uninit 1); r ◁ box (Σ[ ty; rc ty ])])) ;
      [solve_typing..| |]; last first.
@@ -623,8 +621,7 @@ Section code.
  Proof.
    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
    iIntros (_ ϝ ret arg). inv_vec arg=>rcx. simpl_subst.
-    iApply type_new; [solve_typing..|]; iIntros (r); simpl_subst.
-    rewrite (Nat2Z.id (option ty).(ty_size)).
+    iApply (type_new (option ty).(ty_size)); [solve_typing..|]; iIntros (r); simpl_subst.
    iApply (type_cont [] [ϝ ⊑ₗ []]
                      (λ _, [rcx ◁ box (uninit 1); r ◁ box (option ty)]));
      [solve_typing..| |]; last first.
@@ -714,7 +711,7 @@ Section code.
  Proof.
    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
      iIntros (α ϝ ret arg). inv_vec arg=>rcx. simpl_subst.
-    iApply type_new; [solve_typing..|]; iIntros (r); simpl_subst. rewrite (Nat2Z.id 2%nat).
+    iApply (type_new 2); [solve_typing..|]; iIntros (r); simpl_subst.
    iApply (type_cont [] [ϝ ⊑ₗ []]
                      (λ _, [rcx ◁ box (uninit 1); r ◁ box (option $ &uniq{α} ty)]));
      [solve_typing..| |]; last first.
@@ -835,7 +832,7 @@ Section code.
  Proof.
    intros Hclone E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
      iIntros (α ϝ ret arg). inv_vec arg=>rcx. simpl_subst.
-    iApply type_new; [solve_typing..|]; iIntros (r); simpl_subst. rewrite (Nat2Z.id 1%nat).
+    iApply (type_new 1); [solve_typing..|]; iIntros (r); simpl_subst.
    iApply (type_cont [] [ϝ ⊑ₗ []]
                      (λ _, [rcx ◁ box (uninit 1); r ◁ box (&uniq{α} ty)]));
      [solve_typing..| |]; last first.

--- a/theories/typing/lib/rc/weak.v
+++ b/theories/typing/lib/rc/weak.v
@@ -129,8 +129,7 @@ Section code.
  Proof.
    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
      iIntros (α ϝ ret arg). inv_vec arg=>w. simpl_subst.
-    iApply type_new; [solve_typing..|]; iIntros (r); simpl_subst.
-    rewrite (Nat2Z.id 2). (* Having to do this is rather annoying... *)
+    iApply (type_new 2); [solve_typing..|]; iIntros (r); simpl_subst.
    iApply (type_cont [] [ϝ ⊑ₗ []]
                      (λ _, [w ◁ box (&shr{α} weak ty); r ◁ box (option (rc ty))])) ;
      [solve_typing..| |]; last first.
@@ -241,8 +240,7 @@ Section code.
    (* TODO : this is almost identical to rc_clone *)
    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
    iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
-    iApply type_new; [solve_typing..|]; iIntros (r); simpl_subst.
-    rewrite (Nat2Z.id 1). (* Having to do this is rather annoying... *)
+    iApply (type_new 1); [solve_typing..|]; iIntros (r); simpl_subst.
    iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
    iIntros (tid) "#LFT #HE Hna HL Hk [Hx [Hrc' [Hr _]]]".
    rewrite !tctx_hasty_val [[x]]lock.
@@ -304,8 +302,7 @@ Section code.
    (* TODO : this is almost identical to rc_clone *)
    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
    iIntros (α ϝ ret arg). inv_vec arg=>x. simpl_subst.
-    iApply type_new; [solve_typing..|]; iIntros (r); simpl_subst.
-    rewrite (Nat2Z.id 1). (* Having to do this is rather annoying... *)
+    iApply (type_new 1); [solve_typing..|]; iIntros (r); simpl_subst.
    iApply type_deref; [solve_typing..|]; iIntros (rc'); simpl_subst.
    iIntros (tid) "#LFT #HE Hna HL Hk [Hx [Hrc' [Hr _]]]".
    rewrite !tctx_hasty_val [[x]]lock.
@@ -456,10 +453,9 @@ Section code.
  Proof.
    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
      iIntros (_ ϝ ret arg). inv_vec arg. simpl_subst.
-    iApply type_new; [solve_typing..|]; iIntros (rcbox); simpl_subst.
-    iApply type_new; [solve_typing..|]; iIntros (w); simpl_subst.
-    iIntros (tid) "#LFT #HE Hna HL Hk [Hw [Hrcbox _]]".
-    rewrite (Nat2Z.id (2 + ty.(ty_size))) !tctx_hasty_val.
+    iApply (type_new (2 + ty.(ty_size))); [solve_typing..|]; iIntros (rcbox); simpl_subst.
+    iApply (type_new 1); [solve_typing..|]; iIntros (w); simpl_subst.
+    iIntros (tid) "#LFT #HE Hna HL Hk [Hw [Hrcbox _]]". rewrite !tctx_hasty_val.
    iDestruct (ownptr_uninit_own with "Hrcbox") as (lrcbox vlrcbox)
       "(% & Hrcbox↦ & Hrcbox†)". subst rcbox. inv_vec vlrcbox=>??? /=.
    iDestruct (heap_mapsto_vec_cons with "Hrcbox↦") as "[Hrcbox↦0 Hrcbox↦1]".

--- a/theories/typing/lib/refcell/refcell_code.v
+++ b/theories/typing/lib/refcell/refcell_code.v
@@ -24,10 +24,9 @@ Section refcell_functions.
  Proof.
    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
      iIntros (_ ϝ ret arg). inv_vec arg=>x. simpl_subst.
-    iApply type_new; [solve_typing..|].
+    iApply (type_new (S ty.(ty_size))); [solve_typing..|].
    iIntros (r tid) "#LFT #HE Hna HL Hk HT". simpl_subst.
-    rewrite (Nat2Z.id (S ty.(ty_size))) tctx_interp_cons
-            tctx_interp_singleton !tctx_hasty_val.
+    rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
    iDestruct "HT" as "[Hr Hx]".
    iDestruct (ownptr_own with "Hx") as (lx vlx) "(% & Hx↦ & Hx & Hx†)". subst x.
    iDestruct (ownptr_uninit_own with "Hr") as (lr vlr) "(% & Hr↦ & Hr†)". subst r.
@@ -59,10 +58,9 @@ Section refcell_functions.
  Proof.
    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
      iIntros (_ ϝ ret arg). inv_vec arg=>x. simpl_subst.
-    iApply type_new; [solve_typing..|].
+    iApply (type_new ty.(ty_size)); [solve_typing..|].
    iIntros (r tid) "#LFT #HE Hna HL Hk HT". simpl_subst.
-    rewrite (Nat2Z.id (ty.(ty_size))) tctx_interp_cons
-            tctx_interp_singleton !tctx_hasty_val.
+    rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
    iDestruct "HT" as "[Hr Hx]".
    iDestruct (ownptr_own with "Hx") as (lx vlx) "(% & >Hx↦ & Hx & Hx†)". subst x.
    inv_vec vlx=>-[[|?|?]|????] vl; try iDestruct "Hx" as ">[]". simpl vec_to_list.

--- a/theories/typing/lib/rwlock/rwlock_code.v
+++ b/theories/typing/lib/rwlock/rwlock_code.v
@@ -24,10 +24,9 @@ Section rwlock_functions.
  Proof.
    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
      iIntros (_ ret ϝ arg). inv_vec arg=>x. simpl_subst.
-    iApply type_new; [solve_typing..|].
+    iApply (type_new (S ty.(ty_size))); [solve_typing..|].
    iIntros (r tid) "#LFT HE Hna HL Hk HT". simpl_subst.
-    rewrite (Nat2Z.id (S ty.(ty_size))) tctx_interp_cons
-            tctx_interp_singleton !tctx_hasty_val.
+    rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
    iDestruct "HT" as "[Hr Hx]". destruct x as [[|lx|]|]; try done.
    iDestruct "Hx" as "[Hx Hx†]". iDestruct "Hx" as (vl) "[Hx↦ Hx]".
    destruct r as [[|lr|]|]; try done. iDestruct "Hr" as "[Hr Hr†]".
@@ -60,10 +59,9 @@ Section rwlock_functions.
  Proof.
    intros E L. iApply type_fn; [solve_typing..|]. iIntros "/= !#".
      iIntros (_ ret ϝ arg). inv_vec arg=>x. simpl_subst.
-    iApply type_new; [solve_typing..|].
+    iApply (type_new ty.(ty_size)); [solve_typing..|].
    iIntros (r tid) "#LFT HE Hna HL Hk HT". simpl_subst.
-    rewrite (Nat2Z.id (ty.(ty_size))) tctx_interp_cons
-            tctx_interp_singleton !tctx_hasty_val.
+    rewrite tctx_interp_cons tctx_interp_singleton !tctx_hasty_val.
    iDestruct "HT" as "[Hr Hx]". destruct x as [[|lx|]|]; try done.
    iDestruct "Hx" as "[Hx Hx†]".
    iDestruct "Hx" as ([|[[]|]vl]) "[Hx↦ Hx]"; try iDestruct "Hx" as ">[]".

--- a/theories/typing/own.v
+++ b/theories/typing/own.v
@@ -257,13 +257,14 @@ Section typing.
    iExists vl. iFrame. by rewrite Nat2Z.id uninit_own.
  Qed.

-  Lemma type_new E L C T x (n : Z) e :
+  Lemma type_new {E L C T} (n' : nat) x (n : Z) e :
    Closed (x :b: []) e →
    0 ≤ n →
-    (∀ (v : val) (n' := Z.to_nat n),
+    n' = Z.to_nat n →
+    (∀ (v : val),
        typed_body E L C ((v ◁ own_ptr n' (uninit n')) :: T) (subst' x v e)) -∗
    typed_body E L C T (let: x := new [ #n ] in e).
-  Proof. iIntros. iApply type_let; [by apply type_new_instr|solve_typing..]. Qed.
+  Proof. iIntros. subst. iApply type_let; [by apply type_new_instr|solve_typing..]. Qed.

  Lemma type_new_subtype ty E L C T x (n : Z) e :
    Closed (x :b: []) e →
@@ -309,17 +310,18 @@ Section typing.
    (∀ (v : val), typed_body E L C ((v ◁ own_ptr 1 ty)::T') (subst x v e)) -∗
    typed_body E L C T (letalloc: x <- p in e).
  Proof.
-    iIntros. iApply type_new.
+    iIntros (??? Hsz) "**". iApply type_new.
    - rewrite /Closed /=. rewrite !andb_True.
      eauto 10 using is_closed_weaken with set_solver.
    - done.
-    - iIntros (xv) "/=".
+    - solve_typing.
+    - iIntros (xv) "/=". rewrite -Hsz.
      assert (subst x xv (x <- p ;; e)%E = (xv <- p ;; subst x xv e)%E) as ->.
      { (* TODO : simpl_subst should be able to do this. *)
        unfold subst=>/=. repeat f_equal.
        - by rewrite bool_decide_true.
        - eapply is_closed_subst. done. set_solver. }
-      iApply type_assign; [|solve_typing|by eapply write_own|done].
+      iApply type_assign; [|solve_typing|by eapply write_own|solve_typing].
      apply subst_is_closed; last done. apply is_closed_of_val.
  Qed.

@@ -335,6 +337,7 @@ Section typing.
    - rewrite /Closed /=. rewrite !andb_True.
      eauto 10 using is_closed_of_val, is_closed_weaken with set_solver.
    - lia.
+    - done.
    - iIntros (xv) "/=".
      assert (subst x xv (x <-{ty.(ty_size)} !p ;; e)%E =
              (xv <-{ty.(ty_size)} !p ;; subst x xv e)%E) as ->.