working on better vcgen...

_CoqProject

@@ -10,6 +10,7 @@ theories/c_translation/proofmode.v
 theories/c_translation/translation.v
 theories/c_translation/derived.v
 theories/heap_lang_vcgen/naive.v
+theories/heap_lang_vcgen/naive_opt.v
 theories/tests/test1.v
 theories/tests/test2.v
 theories/tests/fact.v

theories/heap_lang_vcgen/naive_opt.v

+From iris.heap_lang Require Export proofmode notation.
+From iris.bi Require Import big_op.
+From iris.proofmode Require Import coq_tactics.
+
+Section vcg.
+  Context `{heapG Σ}.
+
+  Inductive dloc :=
+    | dLoc : nat → dloc
+    | dLocUnknown : loc → dloc.
+
+  Global Instance dloc_decision : EqDecision dloc.
+  Proof. solve_decision. Defined.
+
+  Inductive dbase_lit : Type :=
+    | dLitInt : Z → dbase_lit
+    | dLitBool : bool → dbase_lit
+    | dLitUnit : dbase_lit
+    | dLitLoc : dloc → dbase_lit
+    | dLitUnknown : base_lit → dbase_lit.
+
+  Global Instance dlit_decision : EqDecision dbase_lit.
+  Proof. solve_decision. Defined.
+
+  Inductive dval : Type :=
+    | dLitV : dbase_lit → dval
+    | dValUnknown : val → dval.
+
+  Inductive doption (A : Type) : Type :=
+    | dNone : doption A
+    | dSome : A → doption A
+    | dUnknown : option A → doption A.
+
+  Arguments dNone {_}.
+  Arguments dSome {_} _.
+  Arguments dUnknown {_} _.
+
+  Global Instance doption_fmap : FMap doption := λ A B f m,
+    match m with
+    | dNone => dNone
+    | dSome x => dSome (f x)
+    | dUnknown o => dUnknown (f <$> o)
+    end.
+
+  Inductive wp_expr :=
+    | Base : iProp Σ → wp_expr
+    | Inhale : dloc → (dval → wp_expr) → wp_expr
+    | Exhale : dloc → dval → wp_expr → wp_expr
+    | IsSome {A} : doption A → (A → wp_expr) → wp_expr
+    | IsLoc : dval → (dloc → wp_expr) → wp_expr.
+  Arguments Base _%I.
+
+  Definition dloc_interp (E : list loc) (dl : dloc) : loc :=
+    match dl with
+    | dLoc i => from_option id inhabitant (E !! i)
+    | dLocUnknown l => l
+    end.
+
+  Definition dbase_lit_interp (E : list loc) (l : dbase_lit) : base_lit :=
+    match l with
+    | dLitInt x => LitInt x
+    | dLitBool b => LitBool b
+    | dLitUnit => LitUnit
+    | dLitLoc dl => LitLoc (dloc_interp E dl)
+    | dLitUnknown l => l
+    end.
+
+  Definition dval_interp (E : list loc) (v : dval) : val :=
+    match v with
+    | dLitV l => LitV (dbase_lit_interp E l)
+    | dValUnknown v => v
+    end.
+
+  Fixpoint doption_interp {A} (mx : doption A) : option A :=
+    match mx with
+    | dNone => None
+    | dSome x => Some x
+    | dUnknown mx => mx
+    end.
+
+  Definition dbin_op_eval_int (op : bin_op) (n1 n2 : Z) : dbase_lit :=
+    match op with
+    | PlusOp => dLitInt (n1 + n2)
+    | MinusOp => dLitInt (n1 - n2)
+    | MultOp => dLitInt (n1 * n2)
+    | QuotOp => dLitInt (n1 `quot` n2)
+    | RemOp => dLitInt (n1 `rem` n2)
+    | AndOp => dLitInt (Z.land n1 n2)
+    | OrOp => dLitInt (Z.lor n1 n2)
+    | XorOp => dLitInt (Z.lxor n1 n2)
+    | ShiftLOp => dLitInt (n1 ≪ n2)
+    | ShiftROp => dLitInt (n1 ≫ n2)
+    | LeOp => dLitBool (bool_decide (n1 ≤ n2))
+    | LtOp => dLitBool (bool_decide (n1 < n2))
+    | EqOp => dLitBool (bool_decide (n1 = n2))
+    end.
+
+  Lemma dbin_op_eval_int_correct E op n1 n2 :
+    bin_op_eval_int op n1 n2 = dbase_lit_interp E (dbin_op_eval_int op n1 n2).
+  Proof. by destruct op. Qed.
+
+  Definition dbin_op_eval_bool (op : bin_op) (b1 b2 : bool) : doption dbase_lit :=
+    match op with
+    | PlusOp | MinusOp | MultOp | QuotOp | RemOp => dNone (* Arithmetic *)
+    | AndOp => dSome (dLitBool (b1 && b2))
+    | OrOp => dSome (dLitBool (b1 || b2))
+    | XorOp => dSome (dLitBool (xorb b1 b2))
+    | ShiftLOp | ShiftROp => dNone (* Shifts *)
+    | LeOp | LtOp => dNone (* InEquality *)
+    | EqOp => dSome (dLitBool (bool_decide (b1 = b2)))
+    end.
+
+  Lemma dbin_op_eval_bool_correct E op b1 b2 w :
+    dbin_op_eval_bool op b1 b2 = dSome w →
+    bin_op_eval_bool op b1 b2 = Some (dbase_lit_interp E w).
+  Proof. destruct op; simpl; try by inversion 1. Qed.
+
+  Definition dbin_op_eval (E : list loc) (op : bin_op) (dv1 dv2 : dval) : doption dval :=
+    match dv1,dv2 with
+    | dValUnknown _, _ | _,dValUnknown _ =>
+      dUnknown (dValUnknown <$> bin_op_eval op (dval_interp E dv1) (dval_interp E dv2))
+    | dLitV l1, dLitV l2 =>
+      if decide (op = EqOp)
+      then dSome $ dLitV $ dLitBool
+                 $ bool_decide (dbase_lit_interp E l1 = dbase_lit_interp E l2)
+      else match l1, l2 with
+           | (dLitInt n1), (dLitInt n2) =>
+             dSome $ dLitV $ dbin_op_eval_int op n1 n2
+           | (dLitBool b1), (dLitBool b2) =>
+             dLitV <$> dbin_op_eval_bool op b1 b2
+           | dLitUnknown _, _ | _, dLitUnknown _ =>
+             dUnknown (dValUnknown <$> bin_op_eval op (dval_interp E dv1) (dval_interp E dv2))
+           | _, _ => dNone
+           end
+    end.
+
+  Lemma dbin_op_eval_correct E op dv1 dv2 w :
+    doption_interp (dbin_op_eval E op dv1 dv2) = Some w →
+    bin_op_eval op (dval_interp E dv1) (dval_interp E dv2) = Some (dval_interp E w).
+  Proof.
+    destruct dv1 as [dl1 | v1].
+    - destruct dv2 as [dl2 | v2].
+      + unfold bin_op_eval. simpl. case_decide; simplify_eq/=.
+        { inversion 1. rewrite /bin_op_eval /=.  f_equal. simplify_eq /=.
+           do 2 case_bool_decide; simplify_eq /=; eauto. destruct H1. done. }
+        { rewrite /bin_op_eval; intros; destruct dl1, dl2;
+            rewrite /bin_op_eval_int /bin_op_eval_bool; simplify_eq /=; f_equal;
+              try (destruct op; done); simpl.
+          -  rewrite /bin_op_eval in H1; case_decide; first done.
+             destruct b; simplify_eq /=; f_equal.
+          - destruct op; simplify_eq /=; try done.
+          -  case_decide; first done. destruct b0; simplify_eq /=; f_equal.
+             destruct op; simplify_eq /=; try done.
+          -  case_decide; first done. destruct b; simplify_eq /=; f_equal.
+          -  case_decide; first done; destruct b; simplify_eq /=; f_equal;
+              destruct op; simplify_eq /=; try done.
+          -  case_decide; first done; destruct b; simplify_eq /=; f_equal.
+          -  case_decide; first done; destruct b; simplify_eq /=; f_equal.
+          -  case_decide; first done; destruct b,b0; simplify_eq /=; f_equal.
+             destruct op; simplify_eq /=; try done. }
+      + simpl; destruct (bin_op_eval op #(dbase_lit_interp E dl1) v2); try by inversion 1.
+    - simpl; destruct (bin_op_eval op v1 (dval_interp E dv2)); try by inversion 1.
+  Qed.
+
+  Fixpoint wp_interp (E : list loc) (a : wp_expr) : iProp Σ :=
+    match a with
+    | Base Φ => Φ
+    | Inhale dl Φ =>
+      ∃ dv, dloc_interp E dl ↦ dval_interp E dv ∗ wp_interp E (Φ dv)
+    | Exhale dl dv Φ =>
+      dloc_interp E dl ↦ dval_interp E dv -∗ wp_interp E Φ
+    | IsSome dmx Φ  => ∃ x, ⌜doption_interp dmx = Some x⌝ ∧ wp_interp E (Φ x)
+    | IsLoc dv Φ =>
+      ∃ dl : dloc, ⌜dval_interp E dv = #(dloc_interp E dl)⌝ ∧ wp_interp E (Φ dl)
+    end%I.
+
+  Fixpoint wp_interp_sane (E : list loc) (a : wp_expr) : iProp Σ :=
+    match a with
+    | Base Φ => Φ
+    | Inhale dl Φ =>
+      ∃ v, dloc_interp E dl ↦ v ∗ wp_interp_sane E (Φ (dValUnknown v))
+    | Exhale dl dv Φ =>
+      dloc_interp E dl ↦ dval_interp E dv -∗ wp_interp_sane E Φ
+    | IsSome dmx Φ  =>
+      ∃ x, ⌜doption_interp dmx = Some x⌝ ∧ wp_interp_sane E (Φ x)
+    | IsLoc dv Φ =>
+      ∃ l : loc, ⌜dval_interp E dv = #l⌝ ∧ wp_interp_sane E (Φ (dLocUnknown l))
+    end%I.
+
+  Lemma wp_interp_sane_sound E a : wp_interp_sane E a ⊢ wp_interp E a.
+  Proof.
+    generalize dependent E.
+    induction a.
+    - done.
+    - simpl. iIntros (E) "He". iDestruct "He" as (v) "[H1 H2]".
+      iExists (dValUnknown v). simpl. iFrame. by iApply H0.
+    - simpl. iIntros (E) "He H". iApply IHa. by iApply "He".
+    - simpl. iIntros (E) "He". iDestruct "He" as (v) "[H1 H2]".
+      iExists v. iFrame. by iApply H0.
+    - simpl. iIntros (E) "He". iDestruct "He" as (l) "[H1 H2]".
+      iExists (dLocUnknown l). simpl. iFrame. by iApply H0.
+  Qed.
+
+  Class WpQuote (E : list loc) (e : expr) (Φ : dval → wp_expr) (t : wp_expr) :=
+    wp_quote :
+      wp_interp E t ⊢
+      WP e {{ v, ∃ dv, ⌜ dval_interp E dv = v ⌝ ∧ wp_interp E (Φ dv) }}.
+
+  Global Instance wp_quote_default E e Φ :
+    WpQuote E e Φ (Base (WP e {{ v, wp_interp E (Φ (dValUnknown v)) }})) | 1000.
+  Proof.
+    rewrite /WpQuote /=. apply wp_mono=> v.
+    iIntros "H". iExists (dValUnknown v); auto.
+  Qed.
+
+  Class LocLookup (E : list loc) (l : loc) (i : nat) :=
+    loc_lookup : E !! i = Some l.
+
+  Global Instance loc_lookup_here l E : LocLookup (l :: E) l 0.
+  Proof. done. Qed.
+
+  Global Instance loc_lookup_there l l' E i :
+    LocLookup E l i → LocLookup (l' :: E) l (S i).
+  Proof. done. Qed.
+
+  Class BaseLitQuote (E : list loc) (l : base_lit) (dl : dbase_lit) :=
+    base_lit_quote : l = dbase_lit_interp E dl.
+
+  (** BaseLitQuote for locs *)
+  Global Instance base_lit_quote_loc E l i :
+    LocLookup E l i → BaseLitQuote E (LitLoc l) (dLitLoc (dLoc i)) | 1.
+  Proof. by rewrite /LocLookup /BaseLitQuote /= => ->. Qed.
+
+  Global Instance base_lit_quote_loc_unknown E l :
+    BaseLitQuote E (LitLoc l) (dLitLoc (dLocUnknown l)) | 10.
+  Proof. done. Qed.
+
+  (** BaseLitQuote for constants *)
+  Global Instance base_lit_quote_int E i :
+    BaseLitQuote E (LitInt i) (dLitInt i).
+  Proof. by rewrite /BaseLitQuote /=. Qed.
+
+  Global Instance base_lit_quote_default E l :
+    BaseLitQuote E l (dLitUnknown l) | 1000.
+  Proof. done. Qed.
+
+  Class IntoDVal (E : list loc) (e : expr) (dv : dval) :=
+    into_dval : e = of_val (dval_interp E dv).
+
+  Global Instance into_dval_loc E l dl :
+    BaseLitQuote E l dl → IntoDVal E (Lit l) (dLitV dl).
+  Proof. by rewrite /BaseLitQuote /IntoDVal=> ->. Qed.
+
+  Global Instance into_dval_default E e v :
+    IntoVal e v → IntoDVal E e (dValUnknown v) | 1000.
+  Proof. by rewrite /IntoVal /IntoDVal=> /of_to_val ->. Qed.
+
+  Instance wp_quote_value E e dv Φ :
+    IntoDVal E e dv → WpQuote E e Φ (Φ dv).
+  Proof. rewrite /WpQuote. iIntros (->) "H". iApply wp_value. eauto. Qed.
+
+  Global Instance wp_quote_load E e Φ t :
+    WpQuote E e (λ dv, IsLoc dv (λ l, Inhale l (λ w, Exhale l w (Φ w)))) t →
+    WpQuote E (Load e) Φ t.
+  Proof.
+    rewrite /WpQuote /= => ->. iIntros "H". wp_apply (wp_wand with "H").
+    iIntros (?). iDestruct 1 as (dv <- l -> w) "[Hl H]".
+    wp_load. iExists w; iSplit; first done. by iApply "H".
+  Qed.
+
+  Global Instance wp_quote_bin_op E op e1 e2 Φ Ψ t :
+    (∀ dv1, WpQuote E e2
+              (λ dv2, IsSome (dbin_op_eval E op dv1 dv2) Φ) (Ψ dv1)) →
+    (* IsSome (dUnknown (bin_op_eval op (dval_interp E dv1) (dval_interp E dv2))) *)
+    (*        (λ v, Φ (dValUnknown v))) (Ψ dv1)) → *)
+
+    WpQuote E e1 Ψ t →
+    WpQuote E (BinOp op e1 e2) Φ t.
+  Proof.
+    rewrite /WpQuote /= => He2 ->. iIntros "H".
+    wp_apply (wp_wand with "H"); iIntros (v1).
+    iDestruct 1 as (dv <-) "H". rewrite He2.
+    wp_apply (wp_wand with "H"); iIntros (v2).
+    iDestruct 1 as (dv' <- w ?) "H".
+    wp_op.
+    - by apply dbin_op_eval_correct.
+    - iExists w. auto.
+  Qed.
+
+  Global Instance wp_quote_store E e1 e2 Φ Ψ t :
+    (∀ l, WpQuote E e2 (λ v2,
+            Inhale l (λ _, Exhale l v2 (Φ (dLitV dLitUnit)))) (Ψ l)) →
+    WpQuote E e1 (λ w, IsLoc w Ψ) t →
+    WpQuote E (Store e1 e2) Φ t.
+  Proof.
+    rewrite /WpQuote /= => He2 ->. iIntros "H".
+    wp_apply (wp_wand with "H"); iIntros (v1).
+    iDestruct 1 as (dl <- l ->) "H".
+    rewrite He2. wp_apply (wp_wand with "H"); iIntros (v2).
+    iDestruct 1 as (dv <- w) "[Hl H]". wp_store.
+    iExists (dLitV dLitUnit). iSplit; first done. by iApply "H".
+  Qed.
+
+  Fixpoint optimize (s : option (nat * dval)) (Φ : wp_expr) : wp_expr :=
+    match Φ with
+    | Base Φ1 =>
+       match s with
+       | None => Base Φ1
+       | Some (i,w) => Exhale (dLoc i) w (Base Φ1)
+       end
+    | Inhale dl Φ1 =>
+       match s with
+       | None => Inhale dl (λ v, optimize None (Φ1 v))
+       | Some (i,w) =>
+          if bool_decide (dl = dLoc i) then optimize None (Φ1 w)
+          else Inhale dl (λ v, optimize s (Φ1 v))
+       end
+    | Exhale (dLoc i) w Φ =>
+       match s with
+       | None => optimize (Some (i,w)) Φ
+       | Some (i',w') => Exhale (dLoc i') w' (optimize (Some (i,w)) Φ)
+       end
+    | Exhale (dLocUnknown l) w Φ => Exhale (dLocUnknown l) w (optimize s Φ)
+    | IsSome dmx Φ1 =>
+       match dmx with
+       | dNone => Base False
+       | dSome x => optimize s (Φ1 x)
+       | _ => IsSome dmx (λ v, optimize s (Φ1 v))
+       end
+    | IsLoc dv Φ1 =>
+       match dv with
+       | dLitV (dLitLoc l) => optimize s (Φ1 l)
+       | dLitV (dLitUnknown _) | dValUnknown _ =>
+             IsLoc dv (λ v, optimize s (Φ1 v))
+       | _ => Base False
+       end
+    end.
+
+  Definition exhale_
+      (E : list loc) (s : option (nat * dval)) (P : iProp Σ) : iProp Σ :=
+    match s with
+    | Some (i, v) => dloc_interp E (dLoc i) ↦ dval_interp E v -∗ P
+    | None => P
+    end%I.
+
+  Global Instance exhale_mono' E s : Proper ((⊢) ==> (⊢)) (exhale_ E s).
+  Proof. destruct s; solve_proper. Qed.
+
+
+ Lemma vcg_opt_sound' E s t :
+    wp_interp E (optimize s t) -∗ exhale_ E s (wp_interp E t).
+  Proof.
+    generalize dependent s.
+    induction t; simpl.
+    - intros [[l v]|]; simpl; eauto.
+    - intros [[l' v']|]; simpl.
+      + case_bool_decide; simplify_eq/=.
+        * iIntros "Hwv' H".
+          rewrite H0 /=. eauto 10 with iFrame.
+        * iIntros "H1 H2".
+          iDestruct "H1" as (dv) "[Hd H]".
+          iExists dv.  iFrame; simpl. setoid_rewrite H0. rewrite /exhale_.
+          by iSpecialize ("H" with "H2").
+      + iDestruct 1 as (v) "[Hl H]". iExists v. rewrite H0. iFrame.
+    - intros [[l' v']|]; simpl.
+      + iIntros "H1 H2 H3". destruct d; simpl;
+        rewrite IHt; by iApply ("H1" with "[$]").
+      + iIntros "H1 H2".
+        destruct d; simpl; rewrite IHt; by iApply ("H1" with "[$]").
+    - intros s. destruct d; simpl.
+      + iIntros "[]".
+      + rewrite H0. simpl. f_equiv. iIntros "H". iExists a; auto.
+      + setoid_rewrite H0. iDestruct 1 as (x ->) "H".
+        iApply (exhale_mono' with "H"). iIntros "H". iExists x; auto.
+    - intros s. destruct d; simpl; try by iIntros "[]".
+      + destruct d; simpl; try by iIntros "[]".
+        * rewrite H0. f_equiv. iIntros "H". iExists d; auto.
+        * iIntros "H". iDestruct "H" as (dl) "[% H2]". simplify_eq.
+          rewrite H0. iApply (exhale_mono' with "H2").
+          iIntros "H". iExists dl; auto.
+      +  iIntros "H". iDestruct "H" as (dl) "[% H2]". simplify_eq.
+         rewrite H0. iApply (exhale_mono' with "H2").
+         iIntros "H". iExists dl; auto.
+  Qed.
+
+  Lemma vcg_opt_sound E t :
+    wp_interp E (optimize None t) -∗ wp_interp E t.
+  Proof. by rewrite vcg_opt_sound'. Qed.
+
+  Lemma tac_vcg_opt_sound Δ e Φ E t :
+    WpQuote E e (λ dv, Base (Φ (dval_interp E dv))) t →
+    envs_entails Δ (wp_interp_sane E (optimize None t)) →
+    envs_entails Δ (WP e {{ Φ }}).
+  Proof.
+    rewrite /WpQuote /= envs_entails_eq=> Hquote ->.
+    rewrite wp_interp_sane_sound vcg_opt_sound Hquote. apply wp_mono=> v.
+    by iDestruct 1 as (dv ->) "?".
+  Qed.
+
+  Fixpoint exhale_list (s : list (nat * dval)) (Φ : wp_expr) : wp_expr :=
+    match s with
+    | (i, v) :: s' => Exhale (dLoc i) v (exhale_list s' Φ)
+    | [] => Φ
+    end.
+
+  Definition exhale_list_interp
+             (E : list loc) (pl : list (nat * dval)) (P : iProp Σ) : iProp Σ :=
+    match pl with
+    | [] => P
+    | _  => (([∗ list] lw ∈ pl, dloc_interp E (dLoc lw.1) ↦ dval_interp E lw.2) -∗ P)
+    end%I.
+
+  (*Fixpoint exhale_list_interp'
+           (E : list loc) (s : list (nat * dval)) (P : iProp Σ) : iProp Σ :=
+    match s with
+    | (i, v) :: s' =>
+      dloc_interp E (dLoc i) ↦ dval_interp E v -∗ exhale_list_interp E s' P
+    | [] => P
+    end%I.*)
+
+  Global Instance exhale_list_interp_mono' E s :
+    Proper ((⊢) ==> (⊢)) (exhale_list_interp E s).
+  Proof. induction s; solve_proper. Qed.
+
+  Lemma vcg_exhale_list_sound' E s t :
+    wp_interp E (exhale_list s t) -∗ exhale_list_interp E s (wp_interp E t).
+  Proof.
+    unfold exhale_list_interp.
+    induction s as [| [i w] s']; simpl.
+    - iIntros "$".
+    - iIntros "H". iIntros "[Hl H2]".
+      iSpecialize ("H" with "Hl").
+      rewrite IHs'. destruct s'; by iApply "H".
+  Qed.
+
+  Fixpoint find_and_remove (pl : list (nat * dval)) (dl: dloc) :
+    (list (nat * dval) * option dval) :=
+    match pl with
+    | [] => ([], None)
+    | (i,v) :: pl' =>
+      if (bool_decide (dl = dLoc i)) then (pl', Some v)
+      else match find_and_remove pl' dl with
+           | (r, None)   => ((i,v) :: r, None)
+           | (r, Some w) => (r, Some w)
+           end
+    end.
+
+  Lemma find_and_remove_dLocUnknown pl l :
+    find_and_remove pl (dLocUnknown l) = (pl, None).
+  Proof. induction pl as [|[? ?] ?]; eauto; simpl; by rewrite IHpl. Qed.
+
+  (* Lemma find_and_remove_dLocKnown pl pl' d w' : *)
+  (*   find_and_remove pl d = (pl', Some w') → ∃ i, d = dLoc i. *)
+  (* Proof. *)
+  (*   case d; eauto; intros ?; rewrite find_and_remove_dLocUnknown; inversion 1. *)
+  (* Qed. *)
+
+  Lemma find_and_remove_dLocKnown pl pl' i w :
+    find_and_remove pl (dLoc i) = (pl', Some w) →
+    ∃ pre, pl = pre ++ [(i,w)] ++ pl'.
+  Proof.
+    induction pl; intros Hfind.
+    - inversion Hfind.
+    - destruct a as (j,w'); simpl in Hfind; case_bool_decide; simplify_eq.
+      + by exists [].
+      + assert (find_and_remove pl (dLoc i) = (pl', Some w)).
+        destruct (find_and_remove pl (dLoc i)), o; done.
+        specialize (IHpl H1).
+        destruct IHpl as [pre Hpl]; subst.
+        by exists ((j, w') :: pre).
+  Qed.
+
+  Lemma find_and_remove_none pl pl' d :
+    find_and_remove pl d = (pl', None) → pl = pl'.
+  Proof.
+    case d; eauto; intros ?.
+    - generalize dependent pl'.
+      induction pl as [| [? ?] ?]; intros ? ?; simplify_eq /=; eauto.
+      case_bool_decide; simplify_eq.
+      destruct (find_and_remove pl (dLoc n)), o; simplify_eq; eauto.
+      f_equal. by apply IHpl.
+    - rewrite find_and_remove_dLocUnknown. by intros ?; simplify_eq /=.
+  Qed.
+
+  Lemma find_and_remove_noDup pl pl' d o:
+    NoDup pl.*1 → find_and_remove pl d = (pl', o) → NoDup pl'.*1.
+  Proof.
+    intros.
+    destruct d.
+    - destruct o. apply find_and_remove_dLocKnown in H1.
+      destruct H1 as [pre H1]. subst.
+      rewrite fmap_app in H0. simpl in H0.
+      apply NoDup_app in H0 as [_ [_ H3]].
+      apply NoDup_cons in H3 as [_ H3].
+      done. apply find_and_remove_none in H1; by simplify_eq /=.
+    - rewrite find_and_remove_dLocUnknown in H1; by simplify_eq /=.
+  Qed.
+
+  Lemma find_and_remove_big_sepL pl i pl' w' (Φ : nat * dval → iProp Σ) :
+    find_and_remove pl (dLoc i) = (pl', Some w') →
+    ([∗ list] lw ∈ pl, Φ lw)%I ⊣⊢ (([∗ list] lw ∈ pl', Φ lw) ∗ Φ (i, w'))%I.
+  Proof.
+    (* iIntros "%". iInduction s as [|(j, w) tl] "IH" forall (s' H0);
+     simpl; iSplit; try (done || simpl in H0; case_bool_decide;
+     simplify_eq /=; iIntros "[H1 H2]"; iFrame).
+    - destruct (find_and_remove tl (dLoc i)); simplify_eq /=.
+      iFrame. iApply "IH"; destruct o; done.
+    - destruct (find_and_remove tl (dLoc i)); simplify_eq /=.
+      destruct o; simplify_eq. *)
+  Admitted.
+
+  Fixpoint mem (s : list (nat * dval)) (i: nat) : bool :=
+    match s with
+    | [] => false
+    | (j, _) :: s' => if (bool_decide (i = j)) then true else mem s' i
+    end.
+
+  Lemma mem_no_dup s i : false = mem s i → i ∉ s.*1.
+  Proof.
+    induction s; intros Hf.
+    - by apply not_elem_of_nil.
+    -  apply not_elem_of_cons. simpl in Hf. destruct a as [i' ?].
+       case_bool_decide; first done. naive_solver.
+  Qed.
+
+
+  Fixpoint optimize_list (s : list (nat * dval)) (Φ : wp_expr) : wp_expr :=
+    match Φ with
+    | Base Φ1 => exhale_list s Φ
+    | Inhale dl Φ1 =>
+      match find_and_remove s dl with
+      | (s', None)   => Inhale dl (λ v, optimize_list s (Φ1 v))
+      | (s', Some w) => optimize_list s' (Φ1 w)
+      end
+    | Exhale (dLoc i) w Φ =>
+      if mem s i then Base False
+      else optimize_list ((i,w) :: s) Φ
+    | Exhale (dLocUnknown l) w Φ => Exhale (dLocUnknown l) w (optimize_list s Φ)
+    | IsSome dmx Φ1 =>
+      match dmx with
+      | dNone => Base False
+      | dSome x => optimize_list s (Φ1 x)
+      | _ => IsSome dmx (λ v, optimize_list s (Φ1 v))
+      end
+    | IsLoc dv Φ1 =>
+      match dv with
+      | dLitV (dLitLoc l) => optimize_list s (Φ1 l)
+      | dLitV (dLitUnknown _) | dValUnknown _ =>