circular_doubly_linked_lists.v

(*
  Circular doubly-linked lists.
  Each list is accessed via a cursor that owns the whole structure.
  Operations: insert, delete, fold, cursor movement forward and backward.
*)

From iris.program_logic Require Export weakestpre.
From iris.proofmode Require Export proofmode.
From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import proofmode notation array.
From iris.prelude Require Import options.

(* Notations to pretend we have structs. *)
Definition offset_val: Z := 0.
Definition offset_next: Z := 1.
Definition offset_prev: Z := 2.

Local Notation "ptr .val" := (ptr +ₗ #offset_val)%E
  (at level 8, format "ptr .val") : expr_scope.
Local Notation "ptr .next" := (ptr +ₗ #offset_next)%E
  (at level 8, format "ptr .next") : expr_scope.
Local Notation "ptr .prev" := (ptr +ₗ #offset_prev)%E
  (at level 8, format "ptr .prev") : expr_scope.

Local Notation "ptr .val" := (Loc.add ptr offset_val)
  (at level 8, format "ptr .val"): stdpp_scope.
Local Notation "ptr .next" := (Loc.add ptr offset_next)
  (at level 8, format "ptr .next"): stdpp_scope.
Local Notation "ptr .prev" := (Loc.add ptr offset_prev)
  (at level 8, format "ptr .prev"): stdpp_scope.

(* Operations on circular doubly-linked lists in HeapLang. *)
Definition new_clist: val := λ: "_", ref NONE.

Definition insert: val := λ: "val" "clist",
  let: "new" := AllocN #3 "val" in
  let: "opt_curr" := !"clist" in
  "clist" <- SOME "new" ;;
  match: "opt_curr" with
    NONE =>
      "new".next <- "new" ;;
      "new".prev <- "new"
  | SOME "curr" =>
      let: "prev" := !"curr".prev in
      "prev".next <- "new" ;;
      "curr".prev <- "new" ;;
      "new".next <- "curr" ;;
      "new".prev <- "prev"
  end.

Definition delete: val := λ: "clist",
  match: !"clist" with
    NONE => NONE
  | SOME "curr" =>
      let: "val" := !"curr".val in
      let: "next" := !"curr".next in
      let: "prev" := !"curr".prev in
      array_free "curr" #3 ;;
      if: "next" = "curr"
      then ("clist" <- NONE ;; SOME "val")
      else (
        "clist" <- SOME "next" ;;
        "next".prev <- "prev" ;;
        "prev".next <- "next" ;;
        SOME "val"
      )
  end.

Definition append: val := λ: "clist_xs" "clist_ys",
  match: !"clist_ys" with
    NONE => #()
  | SOME "curr_ys" =>
    "clist_ys" <- NONE ;;
    match: !"clist_xs" with
      NONE => "clist_xs" <- SOME "curr_ys"
    | SOME "curr_xs" =>
      let: "prev_xs" := !"curr_xs".prev in
      let: "prev_ys" := !"curr_ys".prev in
      "prev_xs".next <- "curr_ys" ;;
      "curr_ys".prev <- "prev_xs" ;;
      "prev_ys".next <- "curr_xs" ;;
      "curr_xs".prev <- "prev_ys"
    end
  end.

Definition next: val := λ: "clist",
  match: !"clist" with
    NONE => #()
  | SOME "curr" => "clist" <- SOME (!"curr".next)
  end.

Definition prev: val := λ: "clist",
  match: !"clist" with
    NONE => #()
  | SOME "curr" => "clist" <- SOME (!"curr".prev)
  end.

Definition fold_aux: val :=
  rec: "fold" "f" "acc" "ptr" "stop" :=
    if: "ptr" = "stop"
    then "acc"
    else "fold" "f" ("f" "acc" (!"ptr".val)) (!"ptr".next) "stop".

Definition fold_clist: val := λ: "f" "acc" "clist",
  match: !"clist" with
    NONE => "acc"
  | SOME "h" => fold_aux "f" ("f" "acc" (!"h".val)) (!"h".next) "h"
  end.

Section clist_spec.
  Context `{!heapGS Σ}.

  (* Predicate describing a segment of a doubly-linked list. *)
  Fixpoint lseg (xs: list val) (h t: loc): iProp Σ :=
    match xs with
    | [] => ⌜h = t⌝
    | x::xs =>
      ∃ (n: loc),
      h.val ↦ x ∗
      h.next ↦ #n ∗
      n.prev ↦ #h ∗
      lseg xs n t
    end.

  (* Predicate describing a cursor into a circular doubly-linked list. *)
  Definition is_clist_aux (xs: list val) (opt_ptr: val): iProp Σ :=
    ⌜xs = []⌝ ∗ ⌜opt_ptr = NONEV⌝ ∨
    ⌜xs ≠ []⌝ ∗ ∃ (h: loc), ⌜opt_ptr = SOMEV #h⌝ ∗ lseg xs h h.

  Definition is_clist (xs: list val) (l: loc): iProp Σ :=
    ∃ opt_ptr, l ↦ opt_ptr ∗ is_clist_aux xs opt_ptr.

  (* Alternate segment predicate that: *)
  (* - fixes heap locations instead of values. *)
  (* - doesn't assert anything about values stored in the segment. *)
  Fixpoint lseg_locs (ls: list loc) (h t: loc): iProp Σ :=
    match ls with
    | [] => ⌜h = t⌝
    | l::ls =>
      ⌜h = l⌝ ∗
      ∃ (n: loc),
      h.next ↦ #n ∗
      n.prev ↦ #h ∗
      lseg_locs ls n t
    end.

  (* Separately specify values stored in a list of locations. *)
  Fixpoint lseg_values (ls: list loc) (xs: list val): iProp Σ :=
    match ls, xs with
    | l::ls, x::xs => l.val ↦ x ∗ lseg_values ls xs
    | [], [] => emp
    | _, _ => False
    end.

  (* Equivalence between the predicates. *)
  Lemma lseg_locs_equiv xs h t:
    lseg xs h t ⊣⊢ ∃ ls, lseg_locs ls h t ∗ lseg_values ls xs.
  Proof.
    revert h; induction xs as [|x xs]; intros h; apply bi.equiv_entails_2; simpl.
    - iIntros "->". by iExists [].
    - iIntros "(%&?&?)". by destruct ls.
    - iIntros "(%&?&?&?&Hseg)".
      iDestruct (IHxs with "Hseg") as "(%&?&?)".
      iExists (h::ls). by iFrame.
    - iIntros "(%&Hlocs&Hvals)".
      destruct ls as [|l ls]; try done; simpl.
      iDestruct "Hlocs" as "(<-&%&?&?&Hlocs)".
      iDestruct "Hvals" as "(?&Hvals)".
      iDestruct (IHxs with "[$Hlocs $Hvals]") as "Hseg".
      iFrame.
  Qed.

  (* Example circular doubly-linked lists. *)
  Example clist_empty clist:
    is_clist [] clist
    ⊣⊢
    clist ↦ NONEV.
  Proof.
    apply bi.equiv_entails_2.
    - iIntros "(%&?&[[_ ->]|(%&%&?)])"; by iFrame.
    - iIntros "?"; iFrame; by iLeft.
  Qed.

  Example clist_one x clist:
    is_clist [x] clist
    ⊣⊢
    ∃ (p: loc),
    clist ↦ SOMEV #p ∗
    p.val ↦ x ∗ p.next ↦ #p ∗ p.prev ↦ #p.
  Proof.
    apply bi.equiv_entails_2.
    - iIntros "(%&?&[[% _]|(_&%&->&%&?&?&?&->)])"; [done|iFrame].
    - iIntros "(%&?&?&?&?)". iFrame. iRight. by iFrame.
  Qed.

  Example clist_two x y clist:
    is_clist [x;y] clist
    ⊣⊢
    ∃ (p q: loc),
    clist ↦ SOMEV #p ∗
    p.val ↦ x ∗ p.next ↦ #q ∗ p.prev ↦ #q ∗
    q.val ↦ y ∗ q.next ↦ #p ∗ q.prev ↦ #p.
  Proof.
    apply bi.equiv_entails_2.
    - iIntros "(%&?&[[% _]|(_&%p&->&%q&?&?&?&%&?&?&?&->)])"; first done.
      iExists p, q; by iFrame.
    - iIntros "(%&%&?&?&?&?&?&?&?)". iFrame. iRight. iSplitR; first done.
      iExists p; by iFrame.
  Qed.

  Example clist_three x y z clist:
    is_clist [x;y;z] clist
    ⊣⊢
    ∃ (p q r: loc),
    clist ↦ SOMEV #p ∗
    p.val ↦ x ∗ p.next ↦ #q ∗ p.prev ↦ #r ∗
    q.val ↦ y ∗ q.next ↦ #r ∗ q.prev ↦ #p ∗
    r.val ↦ z ∗ r.next ↦ #p ∗ r.prev ↦ #q.
  Proof.
    apply bi.equiv_entails_2.
    - iIntros "(%&?&[[% _]|(_&%p&->&%q&?&?&?&%r&?&?&?&%&?&?&?&->)])"; first done.
      iExists p, q, r; by iFrame.
    - iIntros "(%&%&%&?&?&?&?&?&?&?&?&?&?)". iFrame. iRight. iSplitR; first done.
      iExists p. by iFrame.
  Qed.

  (* Miscellaneous lemmas. *)
  Lemma list_cons_eq_snoc:
    forall {T: Type} (x: T) (xs: list T), exists zs z, x :: xs = zs ++ [z].
  Proof.
    intros T x xs; generalize dependent x; induction xs as [|y xs]; intros x.
    - exists [], x; constructor.
    - destruct (IHxs y) as (zs' & z' & Heq).
      exists (x::zs'), z'. simpl. rewrite <- Heq. intuition.
  Qed.

  Lemma sep_emp (P: iProp Σ):
    P ∗ emp ⊣⊢ P.
  Proof.
    apply bi.equiv_entails_2.
    - iIntros "[? ?]"; iFrame.
    - iIntros; iFrame.
  Qed.

  Lemma maps_to_replicate_fields h v n p:
    h ↦∗ [v;n;p] ⊣⊢ h.val ↦ v ∗ h.next ↦ n ∗ h.prev ↦ p.
  Proof.
    rewrite ?array_cons ?array_nil ?sep_emp.
    replace (h ↦ v)%I with ((h.val) ↦ v)%I; [|by rewrite Loc.add_0];
    replace ((h +ₗ 1) ↦ n)%I with ((h.next) ↦ n)%I; [|done];
    replace ((h +ₗ 1 +ₗ 1) ↦ p)%I with ((h.prev) ↦ p)%I; [|by rewrite Loc.add_assoc].
    apply bi.equiv_entails_2; iIntros "(?&?&?)"; iFrame.
  Qed.

  (* We can split up segments of circular doubly-linked lists. *)
  Lemma lseg_app xs ys h t:
    lseg (xs ++ ys) h t ⊣⊢ ∃ (m: loc), lseg xs h m ∗ lseg ys m t.
  Proof.
    revert h; induction xs as [|x xs]; intros h; simpl; apply bi.equiv_entails_2.
    - iIntros; by iFrame.
    - iIntros "(%&<-&H)"; by iFrame.
    - iIntros "(%&?&?&?&Hseg)"; iDestruct (IHxs with "Hseg") as "(%&?&?)"; iFrame.
    - iIntros "(%&(%&?&?&?&Hxs)&Hys)"; iDestruct (IHxs with "[Hxs Hys]") as "?"; iFrame.
  Qed.

  Lemma lseg_locs_app ls ps h t:
    lseg_locs (ls ++ ps) h t ⊣⊢ ∃ (m: loc), lseg_locs ls h m ∗ lseg_locs ps m t.
  Proof.
    revert h; induction ls as [|l ls]; intros h; simpl; apply bi.equiv_entails_2.
    - iIntros; by iFrame.
    - iIntros "(%&<-&H)"; by iFrame.
    - iIntros "(<-&(%&?&?&Hseg))". iDestruct (IHls with "Hseg") as "(%&?&?)". by iFrame.
    - iIntros "(%&(<-&%&?&?&Hls)&Hps)". iDestruct (IHls with "[$Hls $Hps]") as "?". by iFrame.
  Qed.

  (* Get access to the last node in a segment. *)
  Lemma lseg_predecessor {xs} {h t: loc} (Hne: xs ≠ []):
    lseg xs h t
    ⊢
    ∃ ys z p, ⌜xs = ys ++ [z]⌝ ∗ lseg ys h p ∗ p.val ↦ z ∗ p.next ↦ #t ∗ t.prev ↦ #p.
  Proof.
    destruct xs as [|xₕ xs]; first done; clear Hne.
    rename xs into xs'; destruct (list_cons_eq_snoc xₕ xs') as (xs & xₜ & ->).
    iIntros "Hseg"; iDestruct (lseg_app with "Hseg") as "(%p&?&(%&?&?&?&->))"; by iFrame.
  Qed.

  (* Specifications for operations on circular doubly-linked lists. *)
  Lemma new_clist_spec:
    {{{ True }}}
      new_clist #()
    {{{ ptr, RET #ptr; is_clist [] ptr }}}.
  Proof.
    iIntros (φ) "_ Hcont".
    wp_rec. wp_alloc ptr as "Hptr".
    iApply "Hcont".
    iFrame. by iLeft.
  Qed.

  Lemma insert_spec (x: val) (xs: list val) (clist: loc):
    {{{ is_clist xs clist }}}
      insert x #clist
    {{{ RET #(); is_clist (x::xs) clist }}}.
  Proof.
    iIntros (φ) "(%&?&Hclist) Hcont".
    wp_rec; wp_alloc n as "Hn"; first done.
    iDestruct (maps_to_replicate_fields with "Hn") as "(?&?&?)".
    wp_load; wp_store.
    iDestruct "Hclist" as "[[-> ->]|(%Hxs &%&->& Hseg)]".
    - repeat wp_store. iApply "Hcont"; iModIntro. iFrame. iRight. by iFrame.
    - iDestruct (lseg_predecessor Hxs with "Hseg") as "(%&%&%&->&?&?&?&?)".
      wp_load. repeat wp_store. iApply "Hcont". iFrame. iRight; simpl. iFrame.
      iModIntro. repeat (iSplitR; try done).
      iApply lseg_app. by iFrame.
  Qed.

  Lemma append_spec (xs ys: list val) (clist_xs clist_ys: loc):
    {{{ is_clist xs clist_xs ∗ is_clist ys clist_ys }}}
      append #clist_xs #clist_ys
    {{{ RET #(); is_clist (xs ++ ys) clist_xs ∗ is_clist [] clist_ys }}}.
  Proof.
    iIntros (φ) "[(%opt_ptr_xs&Hclist_xs&Hxs) (%opt_ptr_ys&Hclist_ys&Hys)] Hcont".
    wp_rec; wp_load.
    iDestruct "Hys" as "[[-> ->]|(%Hys_ne&%h_ys&->&Hys)]".
    - wp_pures. iApply "Hcont"; iModIntro. rewrite app_nil_r. eauto with iFrame.
    - wp_store; iAssert (is_clist (xs ++ ys) clist_xs -∗ φ #())%I with "[Hcont Hclist_ys]" as "Hcont";
        first by iIntros "?"; iApply "Hcont"; eauto with iFrame.
      wp_load. iDestruct "Hxs" as "[[-> ->]|(%Hxs_ne&%h_xs&->&Hxs)]".
      + wp_store. iApply "Hcont"; iModIntro; iFrame; iRight; by iFrame.
      + rename xs into xs'; iDestruct (lseg_predecessor Hxs_ne with "Hxs")
          as "(%xs & %x & %p_xs & -> & Hxs & Hpv_xs & Hpn_xs & Hpp_xs)".
        rename ys into ys'; iDestruct (lseg_predecessor Hys_ne with "Hys")
          as "(%ys & %y & %p_ys & -> & Hys & Hpv_ys & Hpn_ys & Hpp_ys)".
        repeat wp_load; repeat wp_store.
        iApply "Hcont"; iModIntro; iFrame; iRight.
        rewrite ?app_nil; repeat setoid_rewrite lseg_app.
        iFrame. by iPureIntro; intuition.
  Qed.

  Lemma free_node (h n p: loc) v:
    {{{ h.val ↦ v ∗ h.next ↦ #n ∗ h.prev ↦ #p }}}
      array_free #h #3
    {{{ RET #(); True }}}.
  Proof.
    iIntros (φ) "(Hv&Hn&Hp) Hcont".
    iAssert (h ↦∗ [v;#n;#p])%I with "[Hv Hn Hp]" as "H".
    { iApply maps_to_replicate_fields; iFrame. }
    by iApply (wp_array_free with "H").
  Qed.

  Definition delete_result (r: val) (xs: list val) (clist: loc): iProp Σ :=
    match xs with
    | [] => ⌜r = NONEV⌝ ∗ is_clist [] clist
    | x::xs => ⌜r = SOMEV x⌝ ∗ is_clist xs clist
    end.

  Lemma delete_spec (xs: list val) (clist: loc):
    {{{ is_clist xs clist }}}
      delete #clist
    {{{ r, RET r; delete_result r xs clist }}}.
  Proof.
    iIntros (φ) "(%&Hclist&[[-> ->]|(%Hxs&%&->&Hseg)]) Hcont";
    wp_rec; wp_load; wp_pures.
    - (* Case: The list is already empty, so there is nothing to do. *)
      iApply "Hcont". iFrame. by iModIntro; iSplitR; [|iLeft].
    - (* Case: The list is non-empty. *)
      (* Extract the first node from the predicate so we can load from it. *)
      destruct xs as [|x₀ xs]; first done; clear Hxs; simpl.
      iDestruct "Hseg" as "(% & Hhv & Hhn & Hnp & Hseg)".
      (* We need to read h.prev, but we don't yet have evidence that we own it. *)
      (* There are two we can obtain this evidence, depending on whether xs is *)
      (* empty. These cases also correspond to the two branches in the code. *)
      destruct xs as [|x₁ xs].
      + (* Case: There is only one node. Use Hseg to establish that n = h, so we *)
        (*       can read h.prev under our current assumptions and take the first *)
        (*       branch. *)
        iDestruct "Hseg" as "->".
        repeat wp_load; wp_pures; wp_bind (array_free _ _).
        iApply (free_node with "[Hhv Hhn Hnp]"); first by iFrame.
        iNext; iIntros "_"; wp_pures.
        rewrite bool_decide_eq_true_2; try done.
        wp_store; wp_pures; iApply "Hcont"; iModIntro; iSplitR; try done.
        iFrame; by iLeft.
      + (* Case: There are two or more nodes. Use Hseg to extract the previous *)
        (*       node, which must be distinct from h, and also establish that *)
        (*       n ≠ h to take the second branch. *)
        iDestruct (lseg_predecessor with "Hseg")
          as "(%&%&%&->&Hseg&Hpv&Hpn&Hhp)"; first done.
        (* Record that next and current are distinct before we free current. *)
        destruct (decide (n = h)) as [->|Hne];
        first by iCombine "Hhp Hnp" gives "[% _]".
        (* Free the current node. *)
        repeat wp_load; wp_pures; wp_bind (array_free _ _).
        iApply (free_node with "[Hhv Hhn Hhp]"); first by iFrame.
        iNext; iIntros "_"; wp_pures.
        (* Now use the knowledge that n ≠ h to take the second branch. *)
        rewrite bool_decide_eq_false_2; [|intros [=]; done].
        (* Finish. *)
        repeat wp_store; wp_pures; iApply "Hcont"; iModIntro; iSplitR; try done.
        iFrame; iRight; iSplitR; first by destruct ys.
        iExists _; iSplitR; first done.
        rewrite lseg_app; by iFrame.
  Qed.

  Definition rotate {T} (xs: list T): list T :=
    match xs with
    | [] => []
    | x::xs => xs ++ [x]
    end.

  Lemma next_spec (xs: list val) (clist: loc):
    {{{ is_clist xs clist }}}
      next #clist
    {{{ RET #(); is_clist (rotate xs) clist }}}.
  Proof.
    iIntros (φ) "(%&Hclist&[[-> ->]|(%Hxs&%&->&Hseg)]) Hcont";
    wp_rec; wp_load; wp_pures.
    - iApply "Hcont"; iFrame; by iLeft.
    - destruct xs as [|x xs]; first done; clear Hxs; simpl.
      iDestruct "Hseg" as "(%&Hhv&Hhn&Hnp&Hseg)".
      wp_load; wp_store; iApply "Hcont"; iModIntro.
      iFrame; iRight; iSplitR; first by destruct xs.
      iExists _; iSplitR; first done.
      rewrite lseg_app; by iFrame.
  Qed.

  Lemma prev_spec (xs: list val) (clist: loc):
    {{{ is_clist xs clist }}}
      prev #clist
    {{{ RET #(); ∃ ys, ⌜xs = rotate ys⌝ ∗ is_clist ys clist }}}.
  Proof.
    iIntros (φ) "(%&Hclist&[[-> ->]|(%Hxs&%&->&Hseg)]) Hcont";
    wp_rec; wp_load; wp_pures.
    - iApply "Hcont"; iModIntro; iExists []; iSplitR; first done; iFrame; by iLeft.
    - iDestruct (lseg_predecessor Hxs with "Hseg") as "(%&%&%&->&Hseg&Hpv&Hpn&Hhp)".
      wp_load; wp_store; iApply "Hcont"; iModIntro.
      iExists (z::ys); iSplitR; first done; iFrame; iRight; iSplitR; first done.
      by iFrame.
  Qed.

  Lemma fold_aux_spec (ls: list loc) (i xs: list val) (f acc: val) (ptr stop: loc)
                      (P: val → iProp Σ) (I: val → list val → iProp Σ):
    {{{ lseg_locs ls ptr stop ∗
        ⌜stop ∉ ls⌝ ∗
        lseg_values ls xs ∗
        I acc i ∗
        ([∗ list] y ∈ xs, P y) ∗
        (∀ a y ys, {{{ I a ys ∗ P y }}} f a y {{{ r, RET r; I r (ys ++ [y]) }}})
    }}}
      fold_aux f acc #ptr #stop
    {{{ acc, RET acc;
        lseg_locs ls ptr stop ∗
        lseg_values ls xs ∗
        I acc (i ++ xs)
    }}}.
  Proof.
    iIntros (φ) "(Hlocs & %Hstop & Hvals & HI & HPxs & #Hf) Hcont".
    iInduction ls as [|l ls] "IH" forall (ptr acc xs i);
    destruct xs as [|x xs]; try done; simpl.
    - iDestruct "Hlocs" as "->".
      wp_rec. wp_pures.
      rewrite app_nil_r bool_decide_eq_true_2; [|done]; wp_pures.
      iApply "Hcont". by iFrame.
    - iDestruct "Hlocs" as "(->&%&Hln&Hnp&Hlocs)".
      iDestruct "Hvals" as "(Hlv&Hvals)".
      iDestruct "HPxs" as "(HPx&HPxs)".
      apply not_elem_of_cons in Hstop; destruct Hstop as [Hstop_l Hstop].
      wp_rec. wp_pures.
      rewrite bool_decide_eq_false_2; [|intros [=]; done]; wp_pures.
      wp_load. wp_load. wp_bind (f _ _).
      iApply ("Hf" with "[$HI $HPx]"); clear acc; iNext; iIntros "%acc HI".
      iApply ("IH" $! Hstop with "Hlocs Hvals HI HPxs"); clear acc.
      rewrite -app_assoc; simpl.
      iNext; iIntros "%acc (Hlocs&Hvals&Hi)".
      iApply "Hcont".
      by iFrame.
  Qed.

  Lemma fold_spec (xs: list val) (f acc: val) (clist: loc)
                  (P: val → iProp Σ) (I: val → list val → iProp Σ):
    {{{ is_clist xs clist ∗
        I acc [] ∗
        ([∗ list] y ∈ xs, P y) ∗
        (∀ a y ys, {{{ I a ys ∗ P y }}} f a y {{{ r, RET r; I r (ys ++ [y]) }}})
    }}}
      fold_clist f acc #clist
    {{{ acc, RET acc; is_clist xs clist ∗ I acc xs }}}.
  Proof.
    iIntros (φ) "((%&Hclist&[[-> ->]|(%Hxs&%&->&Hseg)]) & HI & HPxs & #Hf) Hcont";
    wp_rec; wp_load; wp_pures.
    - iApply "Hcont". iFrame. by iLeft.
    - destruct xs as [|x xs]; first done; clear Hxs; simpl.
      iDestruct "Hseg" as "(%&Hhv&Hhn&Hnp&Hseg)".
      iDestruct "HPxs" as "[HPx HPxs]".
      iDestruct (lseg_locs_equiv with "Hseg") as "(%&Hlocs&Hvals)".
      wp_load. wp_load. wp_bind (f _ _).
      iApply ("Hf" with "[$HI $HPx]"); clear acc; simpl.
      iNext; iIntros "%acc HI".
      destruct (decide (h ∈ ls)) as [Hls|Hls]. {
        apply elem_of_list_split in Hls; destruct Hls as (ls1 & ls2 & ->).
        iDestruct (lseg_locs_app with "Hlocs") as "(%&Hls1&Hls2)"; simpl.
        iDestruct "Hls2" as "(->&%p&Hhn_dup&Hpp&Hls2)".
        by iCombine "Hhn Hhn_dup" gives "[% _]".
      }
      iApply (fold_aux_spec ls [x] xs f _ _ _ P I with "[$Hlocs $Hvals $HI $HPxs]").
      { iSplitR; done. }
      clear acc; iNext; iIntros "%acc (Hlocs & Hvals & HI)"; simpl.
      iApply "Hcont". iFrame. iRight; iSplitR; first done. iExists _; iSplitR; first done.
      simpl; iFrame. iApply lseg_locs_equiv; iFrame.
  Qed.

End clist_spec.