Constrained encoded with own_constrained + wand type for values.

Co-authored-by: Michael Sammler <msammler@mpi-sws.org>

examples/proofs/btree/btree_learn.v

@@ -11,7 +11,7 @@ Section learnable.
   }.
   Next Obligation.
     iIntros (r l β) "Hl". rewrite btree_t_unfold /ty_own /=.
-    iDestruct "Hl" as ([[[n ks] vs] cs]) "Hl". rewrite tyexists_eq /=.
+    iDestruct "Hl" as ([[[n ks] vs] cs]) "Hl". rewrite tyexists_eq /persistent_own_constraint /=.
     rewrite /ty_own /=. iDestruct "Hl" as "[_ %]". iPureIntro. naive_solver.
   Qed.
 End learnable.

theories/lithium/classes.v

@@ -100,6 +100,28 @@ Global Instance simplify_goal_id_inst {Σ} (P : iProp Σ):
   SimplifyGoal P None | 100 :=
   λ T, i2p (simplify_goal_id P T).
 
+(* TODO: Is the following useful? *)
+(* Lemma simplify_persistent_pure_goal {Σ} (Φ : Prop) T: *)
+(*   T ⌜Φ⌝ -∗ simplify_goal (Σ := Σ) (□ ⌜Φ⌝) T. *)
+(* Proof. iIntros "HT". iExists _. iFrame. by iIntros (?). Qed. *)
+(* Global Instance simplify_persistent_pure_goal_id {Σ} (Φ : Prop): *)
+(*   SimplifyGoal (Σ:=Σ) (□ ⌜Φ⌝) (Some 0%N) := *)
+(*   λ T, i2p (simplify_persistent_pure_goal Φ T). *)
+
+(* Lemma simplify_persistent_pure_hyp {Σ} (Φ : Prop) T: *)
+(*   (⌜Φ⌝ -∗ T) -∗ simplify_hyp (Σ := Σ) (□ ⌜Φ⌝) T. *)
+(* Proof. iIntros "HT" (?). by iApply "HT". Qed. *)
+(* Global Instance simplify_persistent_pure_hyp_inst {Σ} (Φ : Prop): *)
+(*   SimplifyHyp (Σ:=Σ) (□ ⌜Φ⌝) (Some 0%N) := *)
+(*   λ T, i2p (simplify_persistent_pure_hyp Φ T). *)
+
+(* Lemma simplify_persistent_sep_hyp {Σ} (P Q : iProp Σ) T: *)
+(*   (□ P -∗ □ Q -∗ T) -∗ simplify_hyp (Σ := Σ) (□ (P ∗ Q)) T. *)
+(* Proof. iIntros "HT [HP HQ]". iApply ("HT" with "HP HQ"). Qed. *)
+(* Global Instance simplify_persistent_sep_hyp_inst {Σ} (P Q : iProp Σ): *)
+(*   SimplifyHyp (Σ:=Σ) (□ (P ∗ Q)) (Some 0%N) := *)
+(*   λ T, i2p (simplify_persistent_sep_hyp P Q T). *)
+
 (** * Subsumption *)
 (** ** Definition *)
 Definition subsume {Σ} (P1 P2 T : iProp Σ) : iProp Σ :=

theories/typing/constrained.v

@@ -2,78 +2,6 @@ From refinedc.typing Require Export type.
 From refinedc.typing Require Import programs optional.
 Set Default Proof Using "Type".
 
-Section constrained.
-  Context `{!typeG Σ}.
-
-  Program Definition constrained (ty : type) (P : iProp Σ) : type := {|
-    ty_own β l := (l ◁ₗ{β} ty ∗ □ P)%I
-  |}.
-  Next Obligation. move => ty P ? l ?. iIntros "[H $]". by iApply ty_share. Qed.
-
-  Global Instance constrained_rty_ne n : Proper ((dist n) ==> (dist n) ==> (dist n)) constrained.
-  Proof. solve_type_proper. Qed.
-  Global Instance constrained_rty_proper : Proper ((≡) ==> (≡) ==> (≡)) constrained.
-  Proof. solve_type_proper. Qed.
-
-  Global Program Instance constrained_movable ty P `{!Movable ty} : Movable (constrained ty P) := {|
-     ty_layout := ty.(ty_layout);
-     ty_own_val v := (v ◁ᵥ ty ∗ □ P)%I;
-  |}.
-  Next Obligation. iIntros (????) "[? _]". by iApply ty_aligned. Qed.
-  Next Obligation. iIntros (????) "[? _]". by iApply ty_size_eq. Qed.
-  Next Obligation. iIntros (????) "[? $]". by iApply ty_deref. Qed.
-  Next Obligation. iIntros (??????) "Hl [? $]". by iApply (ty_ref with "[//] [Hl]"). Qed.
-
-  Global Instance constrained_loc_in_bounds ty β P `{!LocInBounds ty β} :
-    LocInBounds (constrained ty P) β.
-  Proof.
-    constructor. iIntros (l) "[Hl _]". by iApply loc_in_bounds_in_bounds.
-  Qed.
-
-  Lemma simplify_hyp_place_constrained P l β ty T `{!Persistent P}:
-    (P -∗ l ◁ₗ{β} ty -∗ T) -∗ simplify_hyp (l◁ₗ{β} constrained ty P) T.
-  Proof. iIntros "HT [Hl #?]". by iApply "HT". Qed.
-  Global Instance simplify_hyp_place_constrained_inst P l β ty `{!Persistent P}:
-    SimplifyHypPlace l β (constrained ty P)%I (Some 0%N) :=
-    λ T, i2p (simplify_hyp_place_constrained P l β ty T).
-
-  Lemma simplify_goal_place_constrained P l β ty T `{!Persistent P}:
-    T (l ◁ₗ{β} ty ∗ P) -∗ simplify_goal (l◁ₗ{β} constrained ty P) T.
-  Proof. iIntros "HT". iExists _. iFrame. iIntros "[$ #?]". by iModIntro. Qed.
-  Global Instance simplify_goal_place_constrained_inst P l β ty `{!Persistent P}:
-    SimplifyGoalPlace l β (constrained ty P)%I (Some 0%N) :=
-    λ T, i2p (simplify_goal_place_constrained P l β ty T).
-
-  Lemma simplify_hyp_val_constrained P v ty T `{!Movable ty}:
-    (P -∗ v ◁ᵥ ty -∗ T) -∗ simplify_hyp (v◁ᵥ constrained ty P) T.
-  Proof. iIntros "HT [Hl #?]". by iApply "HT". Qed.
-  Global Instance simplify_hyp_val_constrained_inst P v ty `{!Movable ty}:
-    SimplifyHypVal v (constrained ty P)%I (Some 0%N) :=
-    λ T, i2p (simplify_hyp_val_constrained P v ty T).
-
-  Lemma simplify_goal_val_constrained P v ty T `{!Movable ty} `{!Persistent P}:
-    T (v ◁ᵥ ty ∗ P) -∗ simplify_goal (v◁ᵥ constrained ty P) T.
-  Proof. iIntros "HT". iExists _. iFrame. iIntros "[$ #?]". by iModIntro. Qed.
-  Global Instance simplify_goal_val_constrained_inst P v ty `{!Movable ty} `{!Persistent P}:
-    SimplifyGoalVal v (constrained ty P)%I (Some 0%N) :=
-    λ T, i2p (simplify_goal_val_constrained P v ty T).
-
-  Global Program Instance constrained_optional ty P optty ot1 ot2 `{!Movable ty} `{!Movable optty} `{!Optionable ty optty ot1 ot2} : Optionable (constrained ty P) optty ot1 ot2 := {|
-    opt_pre v1 v2 := opt_pre ty v1 v2
-  |}.
-  Next Obligation. move => ???????? /=. apply opt_alt_sz. Qed.
-  Next Obligation.
-    iIntros (????????[]?????) "Hpre H1 H2". 1: iDestruct "H1" as "[H1 _]".
-    by iApply (opt_bin_op true with "Hpre H1 H2").
-    by iApply (opt_bin_op false with "Hpre H1 H2").
-  Qed.
-
-  Global Instance optionable_agree_constrained P (ty2 : type) `{!OptionableAgree ty1 ty2} : OptionableAgree (constrained ty1 P) ty2.
-  Proof. done. Qed.
-End constrained.
-Typeclasses Opaque constrained.
-
-
 Class OwnConstraint `{!typeG Σ} (P : own_state → iProp Σ) : Prop := {
   own_constraint_persistent : Persistent (P Shr);
   own_constraint_share E : ↑shrN ⊆ E → P Own ={E}=∗ P Shr;
@@ -83,7 +11,7 @@ Global Existing Instance own_constraint_persistent.
 Section own_constrained.
   Context `{!typeG Σ}.
 
-  Program Definition own_constrained (ty : type) (P : own_state → iProp Σ) `{!OwnConstraint P} : type := {|
+  Program Definition own_constrained (P : own_state → iProp Σ) `{!OwnConstraint P} (ty : type) : type := {|
     ty_own β l := (l ◁ₗ{β} ty ∗ P β)%I
   |}.
   Next Obligation.
@@ -92,7 +20,12 @@ Section own_constrained.
     by iApply own_constraint_share.
   Qed.
 
-  Global Program Instance own_constrained_movable ty P `{!Movable ty}  `{!OwnConstraint P} : Movable (own_constrained ty P) := {|
+  Global Instance own_constrained_rty_ne n P `{!OwnConstraint P} : Proper ((dist n) ==> (dist n)) (own_constrained P).
+  Proof. solve_type_proper. Qed.
+  Global Instance own_constrained_rty_proper P `{!OwnConstraint P} : Proper ((≡) ==> (≡)) (own_constrained P).
+  Proof. solve_type_proper. Qed.
+
+  Global Program Instance own_constrained_movable ty P `{!Movable ty} `{!OwnConstraint P} : Movable (own_constrained P ty) := {|
      ty_layout := ty.(ty_layout);
      ty_own_val v := (v ◁ᵥ ty ∗ P Own)%I;
   |}.
@@ -101,34 +34,53 @@ Section own_constrained.
   Next Obligation. iIntros (?????) "[? $]". by iApply ty_deref. Qed.
   Next Obligation. iIntros (???????) "Hl [? $]". by iApply (ty_ref with "[//] [Hl]"). Qed.
 
+  Global Instance own_constrained_loc_in_bounds ty β P `{!OwnConstraint P} `{!LocInBounds ty β} :
+    LocInBounds (own_constrained P ty) β.
+  Proof.
+    constructor. iIntros (l) "[Hl _]". by iApply loc_in_bounds_in_bounds.
+  Qed.
+
   Lemma simplify_hyp_place_own_constrained P l β ty T `{!OwnConstraint P}:
-    (P β -∗ l ◁ₗ{β} ty -∗ T) -∗ simplify_hyp (l◁ₗ{β} own_constrained ty P) T.
+    (P β -∗ l ◁ₗ{β} ty -∗ T) -∗ simplify_hyp (l◁ₗ{β} own_constrained P ty) T.
   Proof. iIntros "HT [Hl HP]". by iApply ("HT" with "HP"). Qed.
   Global Instance simplify_hyp_place_own_constrained_inst P l β ty `{!OwnConstraint P}:
-    SimplifyHypPlace l β (own_constrained ty P)%I (Some 0%N) :=
+    SimplifyHypPlace l β (own_constrained P ty)%I (Some 0%N) :=
     λ T, i2p (simplify_hyp_place_own_constrained P l β ty T).
 
   Lemma simplify_goal_place_own_constrained P l β ty T `{!OwnConstraint P}:
-    T (l ◁ₗ{β} ty ∗ P β) -∗ simplify_goal (l◁ₗ{β} own_constrained ty P) T.
+    T (l ◁ₗ{β} ty ∗ P β) -∗ simplify_goal (l◁ₗ{β} own_constrained P ty) T.
   Proof. iIntros "HT". iExists _. iFrame. iIntros "[$ $]". Qed.
   Global Instance simplify_goal_place_own_constrained_inst P l β ty `{!OwnConstraint P}:
-    SimplifyGoalPlace l β (own_constrained ty P)%I (Some 0%N) :=
+    SimplifyGoalPlace l β (own_constrained P ty)%I (Some 0%N) :=
     λ T, i2p (simplify_goal_place_own_constrained P l β ty T).
 
   Lemma simplify_hyp_val_own_constrained P v ty T `{!Movable ty} `{!OwnConstraint P}:
-    (P Own -∗ v ◁ᵥ ty -∗ T) -∗ simplify_hyp (v ◁ᵥ own_constrained ty P) T.
+    (P Own -∗ v ◁ᵥ ty -∗ T) -∗ simplify_hyp (v ◁ᵥ own_constrained P ty) T.
   Proof. iIntros "HT [Hl HP]". by iApply ("HT" with "HP"). Qed.
   Global Instance simplify_hyp_val_own_constrained_inst P v ty `{!Movable ty} `{!OwnConstraint P}:
-    SimplifyHypVal v (own_constrained ty P)%I (Some 0%N) :=
+    SimplifyHypVal v (own_constrained P ty)%I (Some 0%N) :=
     λ T, i2p (simplify_hyp_val_own_constrained P v ty T).
 
   Lemma simplify_goal_val_own_constrained P v ty T `{!Movable ty} `{!OwnConstraint P}:
-    T (v ◁ᵥ ty ∗ P Own) -∗ simplify_goal (v ◁ᵥ own_constrained ty P) T.
+    T (v ◁ᵥ ty ∗ P Own) -∗ simplify_goal (v ◁ᵥ own_constrained P ty) T.
   Proof. iIntros "HT". iExists _. iFrame. iIntros "[$ $]". Qed.
   Global Instance simplify_goal_val_own_constrained_inst P v ty `{!Movable ty} `{!OwnConstraint P}:
-    SimplifyGoalVal v (own_constrained ty P)%I (Some 0%N) :=
+    SimplifyGoalVal v (own_constrained P ty)%I (Some 0%N) :=
     λ T, i2p (simplify_goal_val_own_constrained P v ty T).
 
+  Global Program Instance own_constrained_optional ty P optty ot1 ot2 `{!Movable ty} `{!Movable optty} `{!OwnConstraint P} `{!Optionable ty optty ot1 ot2} : Optionable (own_constrained P ty) optty ot1 ot2 := {|
+    opt_pre v1 v2 := opt_pre ty v1 v2
+  |}.
+  Next Obligation. move => ????????? /=. apply opt_alt_sz. Qed.
+  Next Obligation.
+    iIntros (?????????[]?????) "Hpre H1 H2". 1: iDestruct "H1" as "[H1 _]".
+    by iApply (opt_bin_op true with "Hpre H1 H2").
+    by iApply (opt_bin_op false with "Hpre H1 H2").
+  Qed.
+
+  Global Instance optionable_agree_own_constrained P (ty2 : type) `{!OwnConstraint P} `{!OptionableAgree ty1 ty2} : OptionableAgree (own_constrained P ty1) ty2.
+  Proof. done. Qed.
+
 
   Definition tyown_constraint (l : loc) (ty : type) (β : own_state) : iProp Σ := l ◁ₗ{β} ty.
 
@@ -149,5 +101,62 @@ Section own_constrained.
     SimplifyGoal (tyown_constraint l ty β) (Some 0%N) :=
     λ T, i2p (simplify_goal_place_tyown_constrained l β ty T).
 End own_constrained.
+
 Typeclasses Opaque own_constrained tyown_constraint.
 Arguments tyown_constraint : simpl never.
+
+Section constrained.
+  Context `{!typeG Σ}.
+
+  Definition persistent_own_constraint (P : iProp Σ) (β : own_state) : iProp Σ := □ P.
+
+  Global Instance persistent_own_constraint_inst P: OwnConstraint (persistent_own_constraint P).
+  Proof. constructor; [by apply _ | by iIntros (??) "H !>"]. Qed.
+
+  Lemma simplify_hyp_place_persistent_constrained P β T:
+    (P -∗ T) -∗ simplify_hyp (persistent_own_constraint P β) T.
+  Proof. iIntros "HT #Hl". by iApply "HT". Qed.
+  Global Instance simplify_hyp_place_persistent_constrained_inst P β:
+    SimplifyHyp (persistent_own_constraint P β) (Some 0%N) :=
+    λ T, i2p (simplify_hyp_place_persistent_constrained P β T).
+
+  Lemma simplify_goal_place_persistent_constrained P `{!Persistent P} β T:
+    T P -∗ simplify_goal (persistent_own_constraint P β) T.
+  Proof. iIntros "HT". iExists _. iFrame. iIntros "#$". Qed.
+  Global Instance simplify_goal_place_persistent_constrained_inst P `{!Persistent P} β:
+    SimplifyGoal (persistent_own_constraint P β) (Some 0%N) :=
+    λ T, i2p (simplify_goal_place_persistent_constrained P β T).
+End constrained.
+
+Typeclasses Opaque persistent_own_constraint.
+Arguments persistent_own_constraint : simpl never.
+
+Notation constrained ty P := (own_constrained (persistent_own_constraint P) ty).
+
+Section nonshr_constrained.
+  Context `{!typeG Σ}.
+
+  Definition nonshr_constraint (P : iProp Σ) (β : own_state) : iProp Σ :=
+    match β with | Own => P | Shr => True end.
+
+  Global Program Instance nonshr_constraint_own_constraint P: OwnConstraint (nonshr_constraint P).
+  Next Obligation. iIntros (???) "?". done. Qed.
+
+  Lemma simplify_hyp_place_nonshr_constrained P T:
+    (P -∗ T) -∗ simplify_hyp (nonshr_constraint P Own) T.
+  Proof. iIntros "HT Hl". by iApply "HT". Qed.
+  Global Instance simplify_hyp_place_nonshr_constrained_inst P:
+    SimplifyHyp (nonshr_constraint P Own) (Some 0%N) :=
+    λ T, i2p (simplify_hyp_place_nonshr_constrained P T).
+
+  Lemma simplify_goal_place_nonshr_constrained P T:
+    T P -∗ simplify_goal (nonshr_constraint P Own) T.
+  Proof. iIntros "HT". iExists _. iFrame. iIntros "$". Qed.
+  Global Instance simplify_goal_place_nonshr_constrained_inst P:
+    SimplifyGoal (nonshr_constraint P Own) (Some 0%N) :=
+    λ T, i2p (simplify_goal_place_nonshr_constrained P T).
+
+End nonshr_constrained.
+
+Typeclasses Opaque nonshr_constraint.
+Arguments nonshr_constraint : simpl never.

theories/typing/singleton.v

@@ -38,6 +38,21 @@ Section singleton_val.
     SubsumeVal v ty (singleton_val ly v') :=
     λ T, i2p (singleton_val_subsume_goal v v' ly ty T).
 
+  Lemma singleton_val_subsume_goal_loc l v' ly ty `{!Movable ty} T:
+    (∀ v, v ◁ᵥ ty -∗ ⌜ty.(ty_layout) = ly⌝ ∗ ⌜v = v'⌝ ∗ T) -∗
+    subsume (l ◁ₗ ty) (l ◁ₗ singleton_val ly v') T.
+  Proof.
+    iIntros "HT Hty".
+    iDestruct (ty_aligned with "Hty") as %Hal.
+    iDestruct (ty_deref with "Hty") as (v) "[Hmt Hty]".
+    iDestruct (ty_size_eq with "Hty") as %Hly.
+    iDestruct ("HT" with "Hty") as (<- ->) "$".
+    by iFrame.
+  Qed.
+  Global Instance singleton_val_subsume_goal_loc_inst l v' ly ty `{!Movable ty}:
+    SubsumePlace l Own ty (singleton_val ly v') :=
+    λ T, i2p (singleton_val_subsume_goal_loc l v' ly ty T).
+
   Lemma singleton_val_merge v l ly T:
     (find_in_context (FindVal v) (λ ty:mtype, ⌜ty.(ty_layout) = ly⌝ ∗ (l ◁ₗ ty -∗ T))) -∗
       simplify_hyp (l ◁ₗ singleton_val ly v) T.

theories/typing/tyfold.v

@@ -24,12 +24,11 @@ Section tyfold.
     rty := tyfold_type tys base
   |}.
 
-  Typeclasses Transparent own_constrained constrained.
+  Typeclasses Transparent own_constrained persistent_own_constraint.
   Lemma simplify_hyp_place_tyfold_optional l β ls tys b T:
     (l ◁ₗ{β} (maybe2 cons tys) @ optionalO (λ '(ty, tys), tyexists (λ l2, tyexists (λ ls2,
        constrained (
-       own_constrained (ty (singleton_place l2))
-         (tyown_constraint l2 (ls2 @ tyfold tys b))) (⌜ls = l2::ls2⌝)))) b -∗ T) -∗
+       own_constrained (tyown_constraint l2 (ls2 @ tyfold tys b)) (ty (singleton_place l2))) (⌜ls = l2::ls2⌝)))) b -∗ T) -∗
     simplify_hyp (l◁ₗ{β} ls @ tyfold tys b) T.
   Proof.
     iIntros "HT Hl". iApply "HT". iDestruct "Hl" as (Hlen) "[Htys Hb]".

theories/typing/type.v

@@ -544,6 +544,10 @@ Ltac f_equiv' :=
      destruct H
   | |- _ = _ => reflexivity
 
+  | |- ?R (?f _) _ => simple apply (_ : Proper (R ==> R) f)
+  | |- ?R (?f _ _) _ => simple apply (_ : Proper (R ==> R ==> R) f)
+  | |- ?R (?f _ _ _) _ => simple apply (_ : Proper (R ==> R ==> R ==> R) f)
+  | |- ?R (?f _ _ _ _) _ => simple apply (_ : Proper (R ==> R ==> R ==> R ==> R) f)
   | |- ?R (?f _ _ _ _) _ => simple apply (_ : Proper (_ ==> _ ==> _ ==> _ ==> R) f)
   | |- ?R (?f _ _ _) _ => simple apply (_ : Proper (_ ==> _ ==> _ ==> R) f)
   | |- ?R (?f _ _) _ => simple apply (_ : Proper (_ ==> _ ==> R) f)

theories/typing/wand.v

@@ -5,15 +5,16 @@ Set Default Proof Using "Type".
 Section wand.
   Context `{!typeG Σ}.
 
-  Program Definition wand_ex {A} (P : A → iProp Σ) (ty : A → type) : type := {|
+  Context {A : Type}.
+  Implicit Types (P : A → iProp Σ).
+
+  Program Definition wand_ex P (ty : A → type) : type := {|
     ty_own β l := match β return _ with
                   | Own => ∀ x, P x -∗ l ◁ₗ (ty x)
                   | Shr => True
                   end
   |}%I.
-  Next Obligation. by iIntros (??????) "?". Qed.
-
-  Context {A : Type}. Implicit Types (P : A → iProp Σ).
+  Next Obligation. by iIntros (?????) "?". Qed.
 
   Lemma subsume_wand l P1 P2 ty1 ty2 T:
     (* The trick is that we prove the wand at the very end so it can
@@ -59,3 +60,89 @@ Section wand.
 
 End wand.
 Notation wand P ty := (wand_ex (A:=unit) (λ _, P) (λ _, ty)).
+
+Section wand_val.
+  Context `{!typeG Σ}.
+
+  Context {A : Type}.
+  Implicit Types (P : A → iProp Σ).
+
+  Program Definition wand_val_ex ly P (ty : A → type) `{!∀ x, Movable (ty x)} : type := {|
+    ty_own β l :=
+      ∃ v,  ⌜l `has_layout_loc` ly⌝ ∗ ⌜v `has_layout_val` ly⌝ ∗ l ↦[β] v ∗
+        match β return _ with
+        | Own => ∀ x, P x -∗ v ◁ᵥ (ty x)
+        | Shr => True
+        end
+  |}%I.
+  Next Obligation.
+    iIntros (???????) "H". iDestruct "H" as (v) "(Hly1&Hly2&Hl&_)".
+    iMod (heap_mapsto_own_state_share with "Hl") as "Hl". eauto with iFrame.
+  Qed.
+
+  Global Program Instance wand_val_movable P ly ty
+         `{!∀ x, Movable (ty x)} : Movable (wand_val_ex ly P ty) := {|
+     ty_layout := ly;
+     ty_own_val v := (⌜v `has_layout_val` ly⌝ ∗ ∀ x, P x -∗ v ◁ᵥ (ty x))%I;
+  |}.
+  Next Obligation. iIntros (?????) "Hl". iDestruct "Hl" as (?) "[$ _]". Qed.
+  Next Obligation. iIntros (?????) "[$ _]". Qed.
+  Next Obligation. iIntros (?????) "Hl". iDestruct "Hl" as (v) "(?&?&?&?)". eauto with iFrame. Qed.
+  Next Obligation. iIntros (????? v) "??[??]". iExists v. iFrame. Qed.
+
+  Global Instance wand_val_loc_in_bounds P ly (ty : A → type)
+         `{!∀ x, Movable (ty x)} `{!∀ x, LocInBounds (ty x) β}:
+    LocInBounds (wand_val_ex ly P ty) β.
+  Proof.
+    constructor. iIntros (l) "Hl". iDestruct "Hl" as (?) "(_&_&Hl&_)".
+    iDestruct (heap_mapsto_own_state_loc_in_bounds with "Hl") as "H".
+    iApply (loc_in_bounds_shorten with "H"). lia.
+  Qed.
+
+  Lemma subsume_wand_val v ly1 ly2 P1 P2 ty1 ty2 T `{!∀ x, Movable (ty1 x)} `{!∀ x, Movable (ty2 x)}:
+    (* The trick is that we prove the wand at the very end so it can
+    use all leftover resources. This only works if there is at most
+    one wand per block (but this is enough for iterating over linked
+    lists). *)
+    ⌜ly1 = ly2⌝ ∗ T ∗ (∀ x, P2 x -∗ ∃ y, P1 y ∗ (v ◁ᵥ ty1 y -∗ v ◁ᵥ ty2 x ∗ True)) -∗
+    subsume (v ◁ᵥ wand_val_ex ly1 P1 ty1) (v ◁ᵥ wand_val_ex ly2 P2 ty2) T.
+  Proof.
+    iIntros "(->&$&Hwand) ($&Hty1)" (x) "HP2".
+    iDestruct ("Hwand" with "HP2") as (y) "[HP1 Hwand]".
+    iDestruct ("Hty1" with "HP1") as "Hty1". iDestruct ("Hwand" with "Hty1") as "[$_]".
+  Qed.
+  Global Instance subsume_wand_val_inst v ly1 ly2 P1 P2 ty1 ty2 `{!∀ x, Movable (ty1 x)} `{!∀ x, Movable (ty2 x)}:
+    SubsumeVal v (wand_val_ex ly1 P1 ty1)%I (wand_val_ex ly2 P2 ty2)%I :=
+    λ T, i2p (subsume_wand_val v ly1 ly2 P1 P2 ty1 ty2 T).
+
+  Lemma simplify_hyp_resolve_wand_val v ly P ty T `{!∀ x, Movable (ty x)}:
+    (∃ x, P x ∗ (v ◁ᵥ ty x -∗ T)) -∗
+    simplify_hyp (v ◁ᵥ wand_val_ex ly P ty) T.
+  Proof.
+    iDestruct 1 as (x) "[HP HT]". iIntros "[_ Hwand]".
+    iApply "HT". by iApply "Hwand".
+  Qed.
+  (* must be before [simplify_goal_place_refine_r] *)
+  Global Instance simplify_hyp_resolve_wand_val_inst v ly P ty `{!∀ x, Movable (ty x)}:
+    SimplifyHypVal v (wand_val_ex ly P ty) (Some 9%N) :=
+    λ T, i2p (simplify_hyp_resolve_wand_val v ly P ty T).
+
+  Lemma simplify_goal_wand_val_eq v ly (ty : A → type) T `{!∀ x, Movable (ty x)}:
+    ⌜v `has_layout_val` ly⌝ ∗ T True -∗
+    simplify_goal (v ◁ᵥ wand_val_ex ly (λ x, v ◁ᵥ (ty x)) ty) T.
+  Proof. iIntros "[??]". iExists _. iFrame. by eauto. Qed.
+  Global Instance simplify_goal_wand_val_eq_inst v ly ty `{!∀ x, Movable (ty x)}:
+    SimplifyGoalVal v (wand_val_ex ly (λ x, v ◁ᵥ (ty x)) ty)%I (Some 0%N) :=
+    λ T, i2p (simplify_goal_wand_val_eq v ly ty T).
+
+  (* TODO: make this more general, maybe with a SimpleSubsume
+  judgement, which does not have a continutation?*)
+  Lemma simplify_goal_wand_val_eq_ref v ly ty (x1 x2 : A → _) T `{!RMovable ty}:
+    ⌜v `has_layout_val` ly⌝ ∗ T ⌜∀ x, x1 x = x2 x⌝ -∗
+    simplify_goal (v ◁ᵥ wand_val_ex ly (λ x, v ◁ᵥ (x1 x) @ ty) (λ x, (x2 x) @ ty)) T.
+  Proof. iIntros "[??]". iExists _. iFrame. iIntros (Heq x) "?". by rewrite Heq. Qed.
+  Global Instance simplify_goal_wand_val_eq_ref_inst v ly ty x1 x2 `{!RMovable ty}:
+    SimplifyGoalVal v (wand_val_ex ly (λ x, v ◁ᵥ (x1 x) @ ty) (λ x, (x2 x) @ ty))%I (Some 0%N) :=
+    λ T, i2p (simplify_goal_wand_val_eq_ref v ly ty x1 x2 T).
+End wand_val.
+Notation wand_val ly P ty := (wand_val_ex (A:=unit) ly (λ _, P) (λ _, ty)).

tutorial/proofs/t03_list/generated_proof_length_val.v

+From refinedc.typing Require Import typing.
+From refinedc.tutorial.t03_list Require Import generated_code.
+From refinedc.tutorial.t03_list Require Import generated_spec.
+Set Default Proof Using "Type".
+
+(* Generated from [tutorial/t03_list.c]. *)
+Section proof_length_val.
+  Context `{!typeG Σ} `{!globalG Σ}.
+
+  (* Typing proof for [length_val]. *)
+  Lemma type_length_val :
+    ⊢ typed_function impl_length_val type_of_length_val.
+  Proof.
+    start_function "length_val" ([v l]) => arg_p local_len.
+    split_blocks ((
+      <[ "#1" :=
+        ∃ v2 : val,
+        ∃ l1 : list type,
+        arg_p ◁ₗ (own_constrained (nonshr_constraint (v2 ◁ᵥ l1 @ list_t)) (singleton_val (LPtr) (v2))) ∗
+        local_len ◁ₗ ((length l - length l1) @ (int (size_t))) ∗
+        (v ◁ᵥ wand_val LPtr (v2 ◁ᵥ l1 @ list_t) (l @ list_t))
+    ]> $
+      ∅
+    )%I : gmap label (iProp Σ)) ((
+      ∅
+    )%I : gmap label (iProp Σ)).
+    - repeat liRStep; liShow.
+      all: print_typesystem_goal "length_val" "#0".
+    - repeat liRStep; liShow.
+      all: print_typesystem_goal "length_val" "#1".
+    Unshelve. all: sidecond_hook; prepare_sideconditions; normalize_and_simpl_goal; try solve_goal; unsolved_sidecond_hook.
+    all: print_sidecondition_goal "length_val".
+  Qed.
+End proof_length_val.

tutorial/proofs/t03_list/generated_spec.v

@@ -132,6 +132,11 @@ Section spec.
     fn(∀ (v, l) : val * (list type); (singleton_val (LPtr) (v)); (v ◁ᵥ l @ list_t) ∗ ⌜length l <= max_int size_t⌝)
       → ∃ () : (), ((length l) @ (int (size_t))); (v ◁ᵥ l @ list_t).
 
+  (* Specifications for function [length_val]. *)
+  Definition type_of_length_val :=
+    fn(∀ (v, l) : val * (list type); (singleton_val (LPtr) (v)); (v ◁ᵥ l @ list_t) ∗ ⌜length l <= max_int size_t⌝)
+      → ∃ () : (), ((length l) @ (int (size_t))); (v ◁ᵥ l @ list_t).
+
   (* Specifications for function [append]. *)
   Definition type_of_append :=
     fn(∀ (p, l1, l2) : loc * (list type) * (list type); (p @ (&own (l1 @ (list_t)))), (l2 @ (list_t)); True)

tutorial/proofs/t03_list/proof_files

@@ -6,6 +6,7 @@ generated_proof_free_array.v
 generated_proof_init.v
 generated_proof_is_empty.v
 generated_proof_length.v
+generated_proof_length_val.v
 generated_proof_length_val_rec.v
 generated_proof_member.v
 generated_proof_pop.v

tutorial/t03_list.c

@@ -110,6 +110,25 @@ size_t length_val_rec (list_t p) {
   return length_val_rec(p->tail) + 1;
 }
 
+[[rc::parameters("v : val", "l : {list type}")]]
+[[rc::args("singleton_val<LPtr, v>")]]
+[[rc::requires("[v ◁ᵥ l @ list_t]")]]
+[[rc::requires("{length l <= max_int size_t}")]]
+[[rc::returns("{length l} @ int<size_t>")]]
+[[rc::ensures("[v ◁ᵥ l @ list_t]")]]  // TODO: there should be nicer syntax for this
+size_t length_val (list_t p) {
+  size_t len = 0;
+  [[rc::exists("v2 : val", "l1 : {list type}")]]
+  [[rc::inv_vars("p : own_constrained<nonshr_constraint<{v2 ◁ᵥ l1 @ list_t}>, singleton_val<LPtr, v2>>",
+                 "len : {length l - length l1} @ int<size_t>")]]
+  [[rc::constraints("[v ◁ᵥ wand_val LPtr (v2 ◁ᵥ l1 @ list_t) (l @ list_t)]")]]
+  while (p != NULL) {
+    p = p->tail;
+    len += 1;
+  }
+  return len;
+}
+
 [[rc::parameters("p : loc", "l1 : {list type}", "l2 : {list type}")]]
 [[rc::args("p @ &own<l1 @ list_t>", "l2 @ list_t")]]
 [[rc::ensures("p @ &own<{l1 ++ l2} @ list_t>")]]