Sepviz Tutorial (Part 2): Animations and Extensions

Welcome to Part 2 of the Sepviz tutorial! See how animation makes changes between heap-memory diagrams easy to follow in interactive proofs, explore Sepviz’s integration options, and learn how to extend Sepviz.

Display all goals and responses

Interactive Proofs and Animations

Diagrams made the previous proof easier to follow than purely algebraic notations, but we can do even better by smoothly animating the transitions between diagrams across proof steps, so that changes are obvious. This works best when interactively stepping through a proof rather than just reading it, so we will use a few more Alectryon features:

Ctrl + ↓, or ⌘ + ↓ on macOS, navigates to the next proof step.
Ctrl + ↑, or ⌘ + ↑ on macOS, navigates to the previous proof step.
Ctrl + Click, or ⌘ + Click on macOS, navigates to the proof step under the pointer.

Try it below! And watch the Rocq goal state shown in the output.

Theorem transitive: forall (a b c : nat), a = b -> b = c -> a = c.forall a b c : nat, a = b -> b = c -> a = c
Proof.forall a b c : nat, a = b -> b = c -> a = c
  intros.a, b, c: nat
H: a = b
H0: b = c
a = c
  subst.c: nat
c = c
  reflexivity.
Qed.

Now try stepping through the same proof as before.

 Lemma transfer_spec (L1 L2 : list val) (p1 p2 : loc) :
   {{{ isQueue p1 L1 ∗ isQueue p2 L2 }}}
     transfer #p1 #p2
   {{{ RET #(); isQueue p1 (L1 ++ L2) ∗ isQueue p2 [] }}}.Σ: gFunctors
heapGS0: heapGS Σ
L1, L2: list val
p1, p2: loc
⟬* PRE @ ⟬ Star ┆ ⟬ PointsTo┆p1┆⟦isQueue┆L1⟧ ⟭
           ┆ ⟬ PointsTo┆p2┆⟦isQueue┆L2⟧ ⟭
         ⟭ *⟭
transfer ⟦ $LitV ┆ p1 ⟧ ⟦ $LitV ┆ p2 ⟧
RET ⟦ $LitV ┆ () ⟧;
⟬* POST @ ⟬ Star ┆ ⟬ PointsTo┆p1┆⟦isQueue┆L1 ++ L2⟧ ⟭
            ┆ ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧ ⟭
          ⟭ *⟭
 Proof.Σ: gFunctors
heapGS0: heapGS Σ
L1, L2: list val
p1, p2: loc
⟬* PRE @ ⟬ Star ┆ ⟬ PointsTo┆p1┆⟦isQueue┆L1⟧ ⟭
           ┆ ⟬ PointsTo┆p2┆⟦isQueue┆L2⟧ ⟭
         ⟭ *⟭
transfer ⟦ $LitV ┆ p1 ⟧ ⟦ $LitV ┆ p2 ⟧
RET ⟦ $LitV ┆ () ⟧;
⟬* POST @ ⟬ Star ┆ ⟬ PointsTo┆p1┆⟦isQueue┆L1 ++ L2⟧ ⟭
            ┆ ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧ ⟭
          ⟭ *⟭
   iIntros "%Φ [HQ1 HQ2] HΦ".Σ: gFunctors
heapGS0: heapGS Σ
L1, L2: list val
p1, p2: loc
Φ: val → iPropI Σ
⟬* PRE @ "HQ1" : ⟬ PointsTo┆p1┆⟦isQueue┆L1⟧ ⟭ *⟭
⟬* PRE @ "HQ2" : ⟬ PointsTo┆p2┆⟦isQueue┆L2⟧ ⟭ *⟭
⟬* PRE @ "HΦ" : ⟬ Modality ┆ ▷ ┆ ⟬ Wand ┆ 
                                   ⟬ 
                                   Star ┆ 
                                   ⟬ PointsTo┆p1┆⟦isQueue┆
                                   L1 ++ L2⟧ ⟭
                                   ┆ 
                                   ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧
                                   ⟭ ⟭
                                   ┆ 
                                   Φ ⟦ $LitV ┆ ()%V ⟧
                                 ⟭
                ⟭ *⟭
--------------------------------------∗
WP transfer ⟦ $LitV ┆ p1 ⟧ ⟦ $LitV ┆ p2 ⟧ {{ v, Φ v }}
   rewrite /transfer.Σ: gFunctors
heapGS0: heapGS Σ
L1, L2: list val
p1, p2: loc
Φ: val → iPropI Σ
⟬* PRE @ "HQ1" : ⟬ PointsTo┆p1┆⟦isQueue┆L1⟧ ⟭ *⟭
⟬* PRE @ "HQ2" : ⟬ PointsTo┆p2┆⟦isQueue┆L2⟧ ⟭ *⟭
⟬* PRE @ "HΦ" : ⟬ Modality ┆ ▷ ┆ ⟬ Wand ┆ 
                                   ⟬ 
                                   Star ┆ 
                                   ⟬ PointsTo┆p1┆⟦isQueue┆
                                   L1 ++ L2⟧ ⟭
                                   ┆ 
                                   ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧
                                   ⟭ ⟭
                                   ┆ 
                                   Φ ⟦ $LitV ┆ ()%V ⟧
                                 ⟭
                ⟭ *⟭
--------------------------------------∗
WP (λ: "p1" "p2",
      if: ~ is_empty "p2"
      then let: "b1" := Snd ! "p1" in
           let: "f2" := Fst ! "p2" in
           let: "d" := Fst ! "b1" in
           "b1" <- (Fst ! "f2", Snd ! "f2");; 
           "p1" <- (Fst ! "p1", Snd ! "p2");; 
           "f2" <- ("d", NONEV);; 
           "p2" <- (Fst ! "p2", "f2")
      else ⟦ $LitV ┆ () ⟧)%V
     ⟦ $LitV ┆ p1 ⟧ ⟦ $LitV ┆ p2 ⟧
{{ v, Φ v }}
   wp_pures.Σ: gFunctors
heapGS0: heapGS Σ
L1, L2: list val
p1, p2: loc
Φ: val → iPropI Σ
⟬* PRE @ "HQ1" : ⟬ PointsTo┆p1┆⟦isQueue┆L1⟧ ⟭ *⟭
⟬* PRE @ "HQ2" : ⟬ PointsTo┆p2┆⟦isQueue┆L2⟧ ⟭ *⟭
⟬* PRE @ "HΦ" : ⟬ Wand ┆ ⟬ Star ┆ ⟬ PointsTo┆p1┆⟦isQueue┆
                                  L1 ++ L2⟧ ⟭
                           ┆ ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧
                             ⟭
                         ⟭
                  ┆ Φ ⟦ $LitV ┆ ()%V ⟧
                ⟭ *⟭
--------------------------------------∗
WP if: ~ is_empty ⟦ $LitV ┆ p2 ⟧
   then let: "b1" := Snd ! ⟦ $LitV ┆ p1 ⟧ in
        let: "f2" := Fst ! ⟦ $LitV ┆ p2 ⟧ in
        let: "d" := Fst ! "b1" in
        "b1" <- (Fst ! "f2", Snd ! "f2");; 
        ⟦ $LitV ┆ p1 ⟧ <-
        (Fst ! ⟦ $LitV ┆ p1 ⟧, Snd ! ⟦ $LitV ┆ p2 ⟧);; 
        "f2" <- ("d", NONEV);; 
        ⟦ $LitV ┆ p2 ⟧ <- (Fst ! ⟦ $LitV ┆ p2 ⟧, "f2")
   else ⟦ $LitV ┆ ()%V ⟧
{{ v, Φ v }}
   wp_apply (is_empty_spec with "HQ2").Σ: gFunctors
heapGS0: heapGS Σ
L1, L2: list val
p1, p2: loc
Φ: val → iPropI Σ
⟬* PRE @ "HQ1" : ⟬ PointsTo┆p1┆⟦isQueue┆L1⟧ ⟭ *⟭
⟬* PRE @ "HΦ" : ⟬ Wand ┆ ⟬ Star ┆ ⟬ PointsTo┆p1┆⟦isQueue┆
                                  L1 ++ L2⟧ ⟭
                           ┆ ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧
                             ⟭
                         ⟭
                  ┆ Φ ⟦ $LitV ┆ ()%V ⟧
                ⟭ *⟭
--------------------------------------∗
⟬ Wand ┆ ⟬ PointsTo┆p2┆⟦isQueue┆L2⟧ ⟭
  ┆ WP if: ~ ⟦ $LitV ┆ bool_decide (L2 = []) ⟧
       then let: "b1" := Snd ! ⟦ $LitV ┆ p1 ⟧ in
            let: "f2" := Fst ! ⟦ $LitV ┆ p2 ⟧ in
            let: "d" := Fst ! "b1" in
            "b1" <- (Fst ! "f2", Snd ! "f2");; 
            ⟦ $LitV ┆ p1 ⟧ <-
            (Fst ! ⟦ $LitV ┆ p1 ⟧,
             Snd ! ⟦ $LitV ┆ p2 ⟧);; 
            "f2" <- ("d", NONEV);; 
            ⟦ $LitV ┆ p2 ⟧ <-
            (Fst ! ⟦ $LitV ┆ p2 ⟧, "f2")
       else ⟦ $LitV ┆ ()%V ⟧
    {{ v, Φ v }}
⟭ iIntros "HQ2".Σ: gFunctors
heapGS0: heapGS Σ
L1, L2: list val
p1, p2: loc
Φ: val → iPropI Σ
⟬* PRE @ "HQ1" : ⟬ PointsTo┆p1┆⟦isQueue┆L1⟧ ⟭ *⟭
⟬* PRE @ "HΦ" : ⟬ Wand ┆ ⟬ Star ┆ ⟬ PointsTo┆p1┆⟦isQueue┆
                                  L1 ++ L2⟧ ⟭
                           ┆ ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧
                             ⟭
                         ⟭
                  ┆ Φ ⟦ $LitV ┆ ()%V ⟧
                ⟭ *⟭
⟬* PRE @ "HQ2" : ⟬ PointsTo┆p2┆⟦isQueue┆L2⟧ ⟭ *⟭
--------------------------------------∗
WP if: ~ ⟦ $LitV ┆ bool_decide (L2 = []) ⟧
   then let: "b1" := Snd ! ⟦ $LitV ┆ p1 ⟧ in
        let: "f2" := Fst ! ⟦ $LitV ┆ p2 ⟧ in
        let: "d" := Fst ! "b1" in
        "b1" <- (Fst ! "f2", Snd ! "f2");; 
        ⟦ $LitV ┆ p1 ⟧ <-
        (Fst ! ⟦ $LitV ┆ p1 ⟧, Snd ! ⟦ $LitV ┆ p2 ⟧);; 
        "f2" <- ("d", NONEV);; 
        ⟦ $LitV ┆ p2 ⟧ <- (Fst ! ⟦ $LitV ┆ p2 ⟧, "f2")
   else ⟦ $LitV ┆ ()%V ⟧
{{ v, Φ v }}

transfer has two branches depending on whether the second queue is empty or not. The proof thus has the same two cases. If it isn’t empty, we can destruct L2 as x :: L2'.

   destruct L2 as [ | x L2'].Σ: gFunctors
heapGS0: heapGS Σ
L1: list val
p1, p2: loc
Φ: val → iPropI Σ
⟬* PRE @ "HQ1" : ⟬ PointsTo┆p1┆⟦isQueue┆L1⟧ ⟭ *⟭
⟬* PRE @ "HΦ" : ⟬ Wand ┆ ⟬ Star ┆ ⟬ PointsTo┆p1┆⟦isQueue┆
                                  L1 ++ []⟧ ⟭
                           ┆ ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧
                             ⟭
                         ⟭
                  ┆ Φ ⟦ $LitV ┆ ()%V ⟧
                ⟭ *⟭
⟬* PRE @ "HQ2" : ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧ ⟭ *⟭
--------------------------------------∗
WP if: ~ ⟦ $LitV ┆ bool_decide ([] = []) ⟧
   then let: "b1" := Snd ! ⟦ $LitV ┆ p1 ⟧ in
        let: "f2" := Fst ! ⟦ $LitV ┆ p2 ⟧ in
        let: "d" := Fst ! "b1" in
        "b1" <- (Fst ! "f2", Snd ! "f2");; 
        ⟦ $LitV ┆ p1 ⟧ <-
        (Fst ! ⟦ $LitV ┆ p1 ⟧, Snd ! ⟦ $LitV ┆ p2 ⟧);; 
        "f2" <- ("d", NONEV);; 
        ⟦ $LitV ┆ p2 ⟧ <- (Fst ! ⟦ $LitV ┆ p2 ⟧, "f2")
   else ⟦ $LitV ┆ ()%V ⟧
{{ v, Φ v }}
Σ: gFunctors
heapGS0: heapGS Σ
L1: list val
x: val
L2': list val
p1, p2: loc
Φ: val → iPropI Σ
⟬* PRE @ "HQ1" : ⟬ PointsTo┆p1┆⟦isQueue┆L1⟧ ⟭ *⟭
⟬* PRE @ "HΦ" : ⟬ Wand ┆ ⟬ Star ┆ ⟬ PointsTo┆p1┆⟦isQueue┆
                                  L1 ++ 
                                  x :: L2'⟧ ⟭
                           ┆ ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧
                             ⟭
                         ⟭
                  ┆ Φ ⟦ $LitV ┆ ()%V ⟧
                ⟭ *⟭
⟬* PRE @ "HQ2" : ⟬ PointsTo┆p2┆⟦isQueue┆x :: L2'⟧ ⟭ *⟭
--------------------------------------∗
WP if: ~ ⟦ $LitV ┆ bool_decide (x :: L2' = []) ⟧
   then let: "b1" := Snd ! ⟦ $LitV ┆ p1 ⟧ in
        let: "f2" := Fst ! ⟦ $LitV ┆ p2 ⟧ in
        let: "d" := Fst ! "b1" in
        "b1" <- (Fst ! "f2", Snd ! "f2");; 
        ⟦ $LitV ┆ p1 ⟧ <-
        (Fst ! ⟦ $LitV ┆ p1 ⟧, Snd ! ⟦ $LitV ┆ p2 ⟧);; 
        "f2" <- ("d", NONEV);; 
        ⟦ $LitV ┆ p2 ⟧ <- (Fst ! ⟦ $LitV ┆ p2 ⟧, "f2")
   else ⟦ $LitV ┆ ()%V ⟧
{{ v, Φ v }}
   -Σ: gFunctors
heapGS0: heapGS Σ
L1: list val
p1, p2: loc
Φ: val → iPropI Σ
⟬* PRE @ "HQ1" : ⟬ PointsTo┆p1┆⟦isQueue┆L1⟧ ⟭ *⟭
⟬* PRE @ "HΦ" : ⟬ Wand ┆ ⟬ Star ┆ ⟬ PointsTo┆p1┆⟦isQueue┆
                                  L1 ++ []⟧ ⟭
                           ┆ ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧
                             ⟭
                         ⟭
                  ┆ Φ ⟦ $LitV ┆ ()%V ⟧
                ⟭ *⟭
⟬* PRE @ "HQ2" : ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧ ⟭ *⟭
--------------------------------------∗
WP if: ~ ⟦ $LitV ┆ bool_decide ([] = []) ⟧
   then let: "b1" := Snd ! ⟦ $LitV ┆ p1 ⟧ in
        let: "f2" := Fst ! ⟦ $LitV ┆ p2 ⟧ in
        let: "d" := Fst ! "b1" in
        "b1" <- (Fst ! "f2", Snd ! "f2");; 
        ⟦ $LitV ┆ p1 ⟧ <-
        (Fst ! ⟦ $LitV ┆ p1 ⟧, Snd ! ⟦ $LitV ┆ p2 ⟧);; 
        "f2" <- ("d", NONEV);; 
        ⟦ $LitV ┆ p2 ⟧ <- (Fst ! ⟦ $LitV ┆ p2 ⟧, "f2")
   else ⟦ $LitV ┆ ()%V ⟧
{{ v, Φ v }} wp_pures.Σ: gFunctors
heapGS0: heapGS Σ
L1: list val
p1, p2: loc
Φ: val → iPropI Σ
⟬* PRE @ "HQ1" : ⟬ PointsTo┆p1┆⟦isQueue┆L1⟧ ⟭ *⟭
⟬* PRE @ "HΦ" : ⟬ Wand ┆ ⟬ Star ┆ ⟬ PointsTo┆p1┆⟦isQueue┆
                                  L1 ++ []⟧ ⟭
                           ┆ ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧
                             ⟭
                         ⟭
                  ┆ Φ ⟦ $LitV ┆ ()%V ⟧
                ⟭ *⟭
⟬* PRE @ "HQ2" : ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧ ⟭ *⟭
--------------------------------------∗
|={⊤}=> Φ ⟦ $LitV ┆ ()%V ⟧ iApply "HΦ".Σ: gFunctors
heapGS0: heapGS Σ
L1: list val
p1, p2: loc
Φ: val → iPropI Σ
⟬* PRE @ "HQ1" : ⟬ PointsTo┆p1┆⟦isQueue┆L1⟧ ⟭ *⟭
⟬* PRE @ "HQ2" : ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧ ⟭ *⟭
--------------------------------------∗
|={⊤}=>
  ⟬ Star ┆ ⟬ PointsTo┆p1┆⟦isQueue┆L1 ++ []⟧ ⟭
    ┆ ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧ ⟭
  ⟭ rewrite app_nil_r.Σ: gFunctors
heapGS0: heapGS Σ
L1: list val
p1, p2: loc
Φ: val → iPropI Σ
⟬* PRE @ "HQ1" : ⟬ PointsTo┆p1┆⟦isQueue┆L1⟧ ⟭ *⟭
⟬* PRE @ "HQ2" : ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧ ⟭ *⟭
--------------------------------------∗
|={⊤}=>
  ⟬ Star ┆ ⟬ PointsTo┆p1┆⟦isQueue┆L1⟧ ⟭
    ┆ ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧ ⟭
  ⟭ iModIntro.Σ: gFunctors
heapGS0: heapGS Σ
L1: list val
p1, p2: loc
Φ: val → iPropI Σ
⟬* PRE @ "HQ1" : ⟬ PointsTo┆p1┆⟦isQueue┆L1⟧ ⟭ *⟭
⟬* PRE @ "HQ2" : ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧ ⟭ *⟭
--------------------------------------∗
⟬ Star ┆ ⟬ PointsTo┆p1┆⟦isQueue┆L1⟧ ⟭
  ┆ ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧ ⟭
⟭ by iFrame.
   -Σ: gFunctors
heapGS0: heapGS Σ
L1: list val
x: val
L2': list val
p1, p2: loc
Φ: val → iPropI Σ
⟬* PRE @ "HQ1" : ⟬ PointsTo┆p1┆⟦isQueue┆L1⟧ ⟭ *⟭
⟬* PRE @ "HΦ" : ⟬ Wand ┆ ⟬ Star ┆ ⟬ PointsTo┆p1┆⟦isQueue┆
                                  L1 ++ 
                                  x :: L2'⟧ ⟭
                           ┆ ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧
                             ⟭
                         ⟭
                  ┆ Φ ⟦ $LitV ┆ ()%V ⟧
                ⟭ *⟭
⟬* PRE @ "HQ2" : ⟬ PointsTo┆p2┆⟦isQueue┆x :: L2'⟧ ⟭ *⟭
--------------------------------------∗
WP if: ~ ⟦ $LitV ┆ bool_decide (x :: L2' = []) ⟧
   then let: "b1" := Snd ! ⟦ $LitV ┆ p1 ⟧ in
        let: "f2" := Fst ! ⟦ $LitV ┆ p2 ⟧ in
        let: "d" := Fst ! "b1" in
        "b1" <- (Fst ! "f2", Snd ! "f2");; 
        ⟦ $LitV ┆ p1 ⟧ <-
        (Fst ! ⟦ $LitV ┆ p1 ⟧, Snd ! ⟦ $LitV ┆ p2 ⟧);; 
        "f2" <- ("d", NONEV);; 
        ⟦ $LitV ┆ p2 ⟧ <- (Fst ! ⟦ $LitV ┆ p2 ⟧, "f2")
   else ⟦ $LitV ┆ ()%V ⟧
{{ v, Φ v }} wp_pures.Σ: gFunctors
heapGS0: heapGS Σ
L1: list val
x: val
L2': list val
p1, p2: loc
Φ: val → iPropI Σ
⟬* PRE @ "HQ1" : ⟬ PointsTo┆p1┆⟦isQueue┆L1⟧ ⟭ *⟭
⟬* PRE @ "HΦ" : ⟬ Wand ┆ ⟬ Star ┆ ⟬ PointsTo┆p1┆⟦isQueue┆
                                  L1 ++ 
                                  x :: L2'⟧ ⟭
                           ┆ ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧
                             ⟭
                         ⟭
                  ┆ Φ ⟦ $LitV ┆ ()%V ⟧
                ⟭ *⟭
⟬* PRE @ "HQ2" : ⟬ PointsTo┆p2┆⟦isQueue┆x :: L2'⟧ ⟭ *⟭
--------------------------------------∗
WP let: "b1" := Snd ! ⟦ $LitV ┆ p1 ⟧ in
   let: "f2" := Fst ! ⟦ $LitV ┆ p2 ⟧ in
   let: "d" := Fst ! "b1" in
   "b1" <- (Fst ! "f2", Snd ! "f2");; 
   ⟦ $LitV ┆ p1 ⟧ <-
   (Fst ! ⟦ $LitV ┆ p1 ⟧, Snd ! ⟦ $LitV ┆ p2 ⟧);; 
   "f2" <- ("d", NONEV);; 
   ⟦ $LitV ┆ p2 ⟧ <- (Fst ! ⟦ $LitV ┆ p2 ⟧, "f2")
{{ v, Φ v }}

Then, symbolically executing the code, we read some values…

     iDestruct "HQ1" as (f1 b1 d1) "(Hp1 & HL1 & Hb1)".Σ: gFunctors
heapGS0: heapGS Σ
L1: list val
x: val
L2': list val
p1, p2: loc
Φ: val → iPropI Σ
f1, b1: loc
d1: val
⟬* PRE @ "Hp1" : ⟬ PointsTo ┆ p1 ┆ ⟦ $Pair
                   ┆ ⟦ $LitV ┆ f1 ⟧ ┆ 
                   ⟦ $LitV ┆ b1 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HL1" : ⟬ PointsTo┆f1┆⟦isListSeg┆L1┆b1⟧ ⟭ *⟭
⟬* PRE @ "Hb1" : ⟬ PointsTo ┆ b1 ┆ ⟦ $Pair ┆ d1
                   ┆ NONEV ⟧ ┆ DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HΦ" : ⟬ Wand ┆ ⟬ Star ┆ ⟬ PointsTo┆p1┆⟦isQueue┆
                                  L1 ++ 
                                  x :: L2'⟧ ⟭
                           ┆ ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧
                             ⟭
                         ⟭
                  ┆ Φ ⟦ $LitV ┆ ()%V ⟧
                ⟭ *⟭
⟬* PRE @ "HQ2" : ⟬ PointsTo┆p2┆⟦isQueue┆x :: L2'⟧ ⟭ *⟭
--------------------------------------∗
WP let: "b1" := Snd ! ⟦ $LitV ┆ p1 ⟧ in
   let: "f2" := Fst ! ⟦ $LitV ┆ p2 ⟧ in
   let: "d" := Fst ! "b1" in
   "b1" <- (Fst ! "f2", Snd ! "f2");; 
   ⟦ $LitV ┆ p1 ⟧ <-
   (Fst ! ⟦ $LitV ┆ p1 ⟧, Snd ! ⟦ $LitV ┆ p2 ⟧);; 
   "f2" <- ("d", NONEV);; 
   ⟦ $LitV ┆ p2 ⟧ <- (Fst ! ⟦ $LitV ┆ p2 ⟧, "f2")
{{ v, Φ v }}
     wp_load.Σ: gFunctors
heapGS0: heapGS Σ
L1: list val
x: val
L2': list val
p1, p2: loc
Φ: val → iPropI Σ
f1, b1: loc
d1: val
⟬* PRE @ "Hp1" : ⟬ PointsTo ┆ p1 ┆ ⟦ $Pair
                   ┆ ⟦ $LitV ┆ f1 ⟧ ┆ 
                   ⟦ $LitV ┆ b1 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HL1" : ⟬ PointsTo┆f1┆⟦isListSeg┆L1┆b1⟧ ⟭ *⟭
⟬* PRE @ "Hb1" : ⟬ PointsTo ┆ b1 ┆ ⟦ $Pair ┆ d1
                   ┆ NONEV ⟧ ┆ DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HΦ" : ⟬ Wand ┆ ⟬ Star ┆ ⟬ PointsTo┆p1┆⟦isQueue┆
                                  L1 ++ 
                                  x :: L2'⟧ ⟭
                           ┆ ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧
                             ⟭
                         ⟭
                  ┆ Φ ⟦ $LitV ┆ ()%V ⟧
                ⟭ *⟭
⟬* PRE @ "HQ2" : ⟬ PointsTo┆p2┆⟦isQueue┆x :: L2'⟧ ⟭ *⟭
--------------------------------------∗
WP let: "b1" := Snd (⟦ $LitV ┆ f1 ⟧, ⟦ $LitV ┆ b1 ⟧)%V in
   let: "f2" := Fst ! ⟦ $LitV ┆ p2 ⟧ in
   let: "d" := Fst ! "b1" in
   "b1" <- (Fst ! "f2", Snd ! "f2");; 
   ⟦ $LitV ┆ p1 ⟧ <-
   (Fst ! ⟦ $LitV ┆ p1 ⟧, Snd ! ⟦ $LitV ┆ p2 ⟧);; 
   "f2" <- ("d", NONEV);; 
   ⟦ $LitV ┆ p2 ⟧ <- (Fst ! ⟦ $LitV ┆ p2 ⟧, "f2")
{{ v, Φ v }} wp_pures.Σ: gFunctors
heapGS0: heapGS Σ
L1: list val
x: val
L2': list val
p1, p2: loc
Φ: val → iPropI Σ
f1, b1: loc
d1: val
⟬* PRE @ "Hp1" : ⟬ PointsTo ┆ p1 ┆ ⟦ $Pair
                   ┆ ⟦ $LitV ┆ f1 ⟧ ┆ 
                   ⟦ $LitV ┆ b1 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HL1" : ⟬ PointsTo┆f1┆⟦isListSeg┆L1┆b1⟧ ⟭ *⟭
⟬* PRE @ "Hb1" : ⟬ PointsTo ┆ b1 ┆ ⟦ $Pair ┆ d1
                   ┆ NONEV ⟧ ┆ DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HΦ" : ⟬ Wand ┆ ⟬ Star ┆ ⟬ PointsTo┆p1┆⟦isQueue┆
                                  L1 ++ 
                                  x :: L2'⟧ ⟭
                           ┆ ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧
                             ⟭
                         ⟭
                  ┆ Φ ⟦ $LitV ┆ ()%V ⟧
                ⟭ *⟭
⟬* PRE @ "HQ2" : ⟬ PointsTo┆p2┆⟦isQueue┆x :: L2'⟧ ⟭ *⟭
--------------------------------------∗
WP let: "f2" := Fst ! ⟦ $LitV ┆ p2 ⟧ in
   let: "d" := Fst ! ⟦ $LitV ┆ b1 ⟧ in
   ⟦ $LitV ┆ b1 ⟧ <- (Fst ! "f2", Snd ! "f2");; 
   ⟦ $LitV ┆ p1 ⟧ <-
   (Fst ! ⟦ $LitV ┆ p1 ⟧, Snd ! ⟦ $LitV ┆ p2 ⟧);; 
   "f2" <- ("d", NONEV);; 
   ⟦ $LitV ┆ p2 ⟧ <- (Fst ! ⟦ $LitV ┆ p2 ⟧, "f2")
{{ v, Φ v }}
     iDestruct "HQ2" as (f2 b2 d2) "(Hp2 & HL2 & Hb2)".Σ: gFunctors
heapGS0: heapGS Σ
L1: list val
x: val
L2': list val
p1, p2: loc
Φ: val → iPropI Σ
f1, b1: loc
d1: val
f2, b2: loc
d2: val
⟬* PRE @ "Hp1" : ⟬ PointsTo ┆ p1 ┆ ⟦ $Pair
                   ┆ ⟦ $LitV ┆ f1 ⟧ ┆ 
                   ⟦ $LitV ┆ b1 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HL1" : ⟬ PointsTo┆f1┆⟦isListSeg┆L1┆b1⟧ ⟭ *⟭
⟬* PRE @ "Hb1" : ⟬ PointsTo ┆ b1 ┆ ⟦ $Pair ┆ d1
                   ┆ NONEV ⟧ ┆ DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HΦ" : ⟬ Wand ┆ ⟬ Star ┆ ⟬ PointsTo┆p1┆⟦isQueue┆
                                  L1 ++ 
                                  x :: L2'⟧ ⟭
                           ┆ ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧
                             ⟭
                         ⟭
                  ┆ Φ ⟦ $LitV ┆ ()%V ⟧
                ⟭ *⟭
⟬* PRE @ "Hp2" : ⟬ PointsTo ┆ p2 ┆ ⟦ $Pair
                   ┆ ⟦ $LitV ┆ f2 ⟧ ┆ 
                   ⟦ $LitV ┆ b2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HL2" : ⟬ PointsTo┆f2┆⟦isListSeg┆
                 x :: L2'┆b2⟧ ⟭ *⟭
⟬* PRE @ "Hb2" : ⟬ PointsTo ┆ b2 ┆ ⟦ $Pair ┆ d2
                   ┆ NONEV ⟧ ┆ DfracOwn 1
                 ⟭ *⟭
--------------------------------------∗
WP let: "f2" := Fst ! ⟦ $LitV ┆ p2 ⟧ in
   let: "d" := Fst ! ⟦ $LitV ┆ b1 ⟧ in
   ⟦ $LitV ┆ b1 ⟧ <- (Fst ! "f2", Snd ! "f2");; 
   ⟦ $LitV ┆ p1 ⟧ <-
   (Fst ! ⟦ $LitV ┆ p1 ⟧, Snd ! ⟦ $LitV ┆ p2 ⟧);; 
   "f2" <- ("d", NONEV);; 
   ⟦ $LitV ┆ p2 ⟧ <- (Fst ! ⟦ $LitV ┆ p2 ⟧, "f2")
{{ v, Φ v }}
     wp_load.Σ: gFunctors
heapGS0: heapGS Σ
L1: list val
x: val
L2': list val
p1, p2: loc
Φ: val → iPropI Σ
f1, b1: loc
d1: val
f2, b2: loc
d2: val
⟬* PRE @ "Hp1" : ⟬ PointsTo ┆ p1 ┆ ⟦ $Pair
                   ┆ ⟦ $LitV ┆ f1 ⟧ ┆ 
                   ⟦ $LitV ┆ b1 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HL1" : ⟬ PointsTo┆f1┆⟦isListSeg┆L1┆b1⟧ ⟭ *⟭
⟬* PRE @ "Hb1" : ⟬ PointsTo ┆ b1 ┆ ⟦ $Pair ┆ d1
                   ┆ NONEV ⟧ ┆ DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HΦ" : ⟬ Wand ┆ ⟬ Star ┆ ⟬ PointsTo┆p1┆⟦isQueue┆
                                  L1 ++ 
                                  x :: L2'⟧ ⟭
                           ┆ ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧
                             ⟭
                         ⟭
                  ┆ Φ ⟦ $LitV ┆ ()%V ⟧
                ⟭ *⟭
⟬* PRE @ "Hp2" : ⟬ PointsTo ┆ p2 ┆ ⟦ $Pair
                   ┆ ⟦ $LitV ┆ f2 ⟧ ┆ 
                   ⟦ $LitV ┆ b2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HL2" : ⟬ PointsTo┆f2┆⟦isListSeg┆
                 x :: L2'┆b2⟧ ⟭ *⟭
⟬* PRE @ "Hb2" : ⟬ PointsTo ┆ b2 ┆ ⟦ $Pair ┆ d2
                   ┆ NONEV ⟧ ┆ DfracOwn 1
                 ⟭ *⟭
--------------------------------------∗
WP let: "f2" := Fst (⟦ $LitV ┆ f2 ⟧, ⟦ $LitV ┆ b2 ⟧)%V in
   let: "d" := Fst ! ⟦ $LitV ┆ b1 ⟧ in
   ⟦ $LitV ┆ b1 ⟧ <- (Fst ! "f2", Snd ! "f2");; 
   ⟦ $LitV ┆ p1 ⟧ <-
   (Fst ! ⟦ $LitV ┆ p1 ⟧, Snd ! ⟦ $LitV ┆ p2 ⟧);; 
   "f2" <- ("d", NONEV);; 
   ⟦ $LitV ┆ p2 ⟧ <- (Fst ! ⟦ $LitV ┆ p2 ⟧, "f2")
{{ v, Φ v }} wp_load.Σ: gFunctors
heapGS0: heapGS Σ
L1: list val
x: val
L2': list val
p1, p2: loc
Φ: val → iPropI Σ
f1, b1: loc
d1: val
f2, b2: loc
d2: val
⟬* PRE @ "Hp1" : ⟬ PointsTo ┆ p1 ┆ ⟦ $Pair
                   ┆ ⟦ $LitV ┆ f1 ⟧ ┆ 
                   ⟦ $LitV ┆ b1 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HL1" : ⟬ PointsTo┆f1┆⟦isListSeg┆L1┆b1⟧ ⟭ *⟭
⟬* PRE @ "Hb1" : ⟬ PointsTo ┆ b1 ┆ ⟦ $Pair ┆ d1
                   ┆ NONEV ⟧ ┆ DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HΦ" : ⟬ Wand ┆ ⟬ Star ┆ ⟬ PointsTo┆p1┆⟦isQueue┆
                                  L1 ++ 
                                  x :: L2'⟧ ⟭
                           ┆ ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧
                             ⟭
                         ⟭
                  ┆ Φ ⟦ $LitV ┆ ()%V ⟧
                ⟭ *⟭
⟬* PRE @ "Hp2" : ⟬ PointsTo ┆ p2 ┆ ⟦ $Pair
                   ┆ ⟦ $LitV ┆ f2 ⟧ ┆ 
                   ⟦ $LitV ┆ b2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HL2" : ⟬ PointsTo┆f2┆⟦isListSeg┆
                 x :: L2'┆b2⟧ ⟭ *⟭
⟬* PRE @ "Hb2" : ⟬ PointsTo ┆ b2 ┆ ⟦ $Pair ┆ d2
                   ┆ NONEV ⟧ ┆ DfracOwn 1
                 ⟭ *⟭
--------------------------------------∗
WP let: "d" := Fst (d1, NONEV)%V in
   ⟦ $LitV ┆ b1 ⟧ <-
   (Fst ! ⟦ $LitV ┆ f2 ⟧, Snd ! ⟦ $LitV ┆ f2 ⟧);; 
   ⟦ $LitV ┆ p1 ⟧ <-
   (Fst ! ⟦ $LitV ┆ p1 ⟧, Snd ! ⟦ $LitV ┆ p2 ⟧);; 
   ⟦ $LitV ┆ f2 ⟧ <- ("d", NONEV);; 
   ⟦ $LitV ┆ p2 ⟧ <-
   (Fst ! ⟦ $LitV ┆ p2 ⟧, ⟦ $LitV ┆ f2 ⟧)
{{ v, Φ v }} wp_pures.Σ: gFunctors
heapGS0: heapGS Σ
L1: list val
x: val
L2': list val
p1, p2: loc
Φ: val → iPropI Σ
f1, b1: loc
d1: val
f2, b2: loc
d2: val
⟬* PRE @ "Hp1" : ⟬ PointsTo ┆ p1 ┆ ⟦ $Pair
                   ┆ ⟦ $LitV ┆ f1 ⟧ ┆ 
                   ⟦ $LitV ┆ b1 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HL1" : ⟬ PointsTo┆f1┆⟦isListSeg┆L1┆b1⟧ ⟭ *⟭
⟬* PRE @ "Hb1" : ⟬ PointsTo ┆ b1 ┆ ⟦ $Pair ┆ d1
                   ┆ NONEV ⟧ ┆ DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HΦ" : ⟬ Wand ┆ ⟬ Star ┆ ⟬ PointsTo┆p1┆⟦isQueue┆
                                  L1 ++ 
                                  x :: L2'⟧ ⟭
                           ┆ ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧
                             ⟭
                         ⟭
                  ┆ Φ ⟦ $LitV ┆ ()%V ⟧
                ⟭ *⟭
⟬* PRE @ "Hp2" : ⟬ PointsTo ┆ p2 ┆ ⟦ $Pair
                   ┆ ⟦ $LitV ┆ f2 ⟧ ┆ 
                   ⟦ $LitV ┆ b2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HL2" : ⟬ PointsTo┆f2┆⟦isListSeg┆
                 x :: L2'┆b2⟧ ⟭ *⟭
⟬* PRE @ "Hb2" : ⟬ PointsTo ┆ b2 ┆ ⟦ $Pair ┆ d2
                   ┆ NONEV ⟧ ┆ DfracOwn 1
                 ⟭ *⟭
--------------------------------------∗
WP ⟦ $LitV ┆ b1 ⟧ <-
   (Fst ! ⟦ $LitV ┆ f2 ⟧, Snd ! ⟦ $LitV ┆ f2 ⟧);; 
   ⟦ $LitV ┆ p1 ⟧ <-
   (Fst ! ⟦ $LitV ┆ p1 ⟧, Snd ! ⟦ $LitV ┆ p2 ⟧);; 
   ⟦ $LitV ┆ f2 ⟧ <- (d1, NONEV);; 
   ⟦ $LitV ┆ p2 ⟧ <-
   (Fst ! ⟦ $LitV ┆ p2 ⟧, ⟦ $LitV ┆ f2 ⟧)
{{ v, Φ v }}
     iDestruct (isListSeg_cons_inv with "HL2") as (c2) "[Hf2 HL2']".Σ: gFunctors
heapGS0: heapGS Σ
L1: list val
x: val
L2': list val
p1, p2: loc
Φ: val → iPropI Σ
f1, b1: loc
d1: val
f2, b2: loc
d2: val
c2: loc
⟬* PRE @ "Hp1" : ⟬ PointsTo ┆ p1 ┆ ⟦ $Pair
                   ┆ ⟦ $LitV ┆ f1 ⟧ ┆ 
                   ⟦ $LitV ┆ b1 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HL1" : ⟬ PointsTo┆f1┆⟦isListSeg┆L1┆b1⟧ ⟭ *⟭
⟬* PRE @ "Hb1" : ⟬ PointsTo ┆ b1 ┆ ⟦ $Pair ┆ d1
                   ┆ NONEV ⟧ ┆ DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HΦ" : ⟬ Wand ┆ ⟬ Star ┆ ⟬ PointsTo┆p1┆⟦isQueue┆
                                  L1 ++ 
                                  x :: L2'⟧ ⟭
                           ┆ ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧
                             ⟭
                         ⟭
                  ┆ Φ ⟦ $LitV ┆ ()%V ⟧
                ⟭ *⟭
⟬* PRE @ "Hp2" : ⟬ PointsTo ┆ p2 ┆ ⟦ $Pair
                   ┆ ⟦ $LitV ┆ f2 ⟧ ┆ 
                   ⟦ $LitV ┆ b2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "Hb2" : ⟬ PointsTo ┆ b2 ┆ ⟦ $Pair ┆ d2
                   ┆ NONEV ⟧ ┆ DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "Hf2" : ⟬ PointsTo ┆ f2 ┆ ⟦ $Pair ┆ x
                   ┆ ⟦ $LitV ┆ c2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HL2'" : ⟬ PointsTo┆c2┆⟦isListSeg┆L2'┆b2⟧ ⟭ *⟭
--------------------------------------∗
WP ⟦ $LitV ┆ b1 ⟧ <-
   (Fst ! ⟦ $LitV ┆ f2 ⟧, Snd ! ⟦ $LitV ┆ f2 ⟧);; 
   ⟦ $LitV ┆ p1 ⟧ <-
   (Fst ! ⟦ $LitV ┆ p1 ⟧, Snd ! ⟦ $LitV ┆ p2 ⟧);; 
   ⟦ $LitV ┆ f2 ⟧ <- (d1, NONEV);; 
   ⟦ $LitV ┆ p2 ⟧ <-
   (Fst ! ⟦ $LitV ┆ p2 ⟧, ⟦ $LitV ┆ f2 ⟧)
{{ v, Φ v }}
     wp_load.Σ: gFunctors
heapGS0: heapGS Σ
L1: list val
x: val
L2': list val
p1, p2: loc
Φ: val → iPropI Σ
f1, b1: loc
d1: val
f2, b2: loc
d2: val
c2: loc
⟬* PRE @ "Hp1" : ⟬ PointsTo ┆ p1 ┆ ⟦ $Pair
                   ┆ ⟦ $LitV ┆ f1 ⟧ ┆ 
                   ⟦ $LitV ┆ b1 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HL1" : ⟬ PointsTo┆f1┆⟦isListSeg┆L1┆b1⟧ ⟭ *⟭
⟬* PRE @ "Hb1" : ⟬ PointsTo ┆ b1 ┆ ⟦ $Pair ┆ d1
                   ┆ NONEV ⟧ ┆ DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HΦ" : ⟬ Wand ┆ ⟬ Star ┆ ⟬ PointsTo┆p1┆⟦isQueue┆
                                  L1 ++ 
                                  x :: L2'⟧ ⟭
                           ┆ ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧
                             ⟭
                         ⟭
                  ┆ Φ ⟦ $LitV ┆ ()%V ⟧
                ⟭ *⟭
⟬* PRE @ "Hp2" : ⟬ PointsTo ┆ p2 ┆ ⟦ $Pair
                   ┆ ⟦ $LitV ┆ f2 ⟧ ┆ 
                   ⟦ $LitV ┆ b2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "Hb2" : ⟬ PointsTo ┆ b2 ┆ ⟦ $Pair ┆ d2
                   ┆ NONEV ⟧ ┆ DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "Hf2" : ⟬ PointsTo ┆ f2 ┆ ⟦ $Pair ┆ x
                   ┆ ⟦ $LitV ┆ c2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HL2'" : ⟬ PointsTo┆c2┆⟦isListSeg┆L2'┆b2⟧ ⟭ *⟭
--------------------------------------∗
WP ⟦ $LitV ┆ b1 ⟧ <-
   (Fst ! ⟦ $LitV ┆ f2 ⟧, Snd (x, ⟦ $LitV ┆ c2 ⟧)%V);; 
   ⟦ $LitV ┆ p1 ⟧ <-
   (Fst ! ⟦ $LitV ┆ p1 ⟧, Snd ! ⟦ $LitV ┆ p2 ⟧);; 
   ⟦ $LitV ┆ f2 ⟧ <- (d1, NONEV);; 
   ⟦ $LitV ┆ p2 ⟧ <-
   (Fst ! ⟦ $LitV ┆ p2 ⟧, ⟦ $LitV ┆ f2 ⟧)
{{ v, Φ v }} wp_load.Σ: gFunctors
heapGS0: heapGS Σ
L1: list val
x: val
L2': list val
p1, p2: loc
Φ: val → iPropI Σ
f1, b1: loc
d1: val
f2, b2: loc
d2: val
c2: loc
⟬* PRE @ "Hp1" : ⟬ PointsTo ┆ p1 ┆ ⟦ $Pair
                   ┆ ⟦ $LitV ┆ f1 ⟧ ┆ 
                   ⟦ $LitV ┆ b1 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HL1" : ⟬ PointsTo┆f1┆⟦isListSeg┆L1┆b1⟧ ⟭ *⟭
⟬* PRE @ "Hb1" : ⟬ PointsTo ┆ b1 ┆ ⟦ $Pair ┆ d1
                   ┆ NONEV ⟧ ┆ DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HΦ" : ⟬ Wand ┆ ⟬ Star ┆ ⟬ PointsTo┆p1┆⟦isQueue┆
                                  L1 ++ 
                                  x :: L2'⟧ ⟭
                           ┆ ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧
                             ⟭
                         ⟭
                  ┆ Φ ⟦ $LitV ┆ ()%V ⟧
                ⟭ *⟭
⟬* PRE @ "Hp2" : ⟬ PointsTo ┆ p2 ┆ ⟦ $Pair
                   ┆ ⟦ $LitV ┆ f2 ⟧ ┆ 
                   ⟦ $LitV ┆ b2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "Hb2" : ⟬ PointsTo ┆ b2 ┆ ⟦ $Pair ┆ d2
                   ┆ NONEV ⟧ ┆ DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "Hf2" : ⟬ PointsTo ┆ f2 ┆ ⟦ $Pair ┆ x
                   ┆ ⟦ $LitV ┆ c2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HL2'" : ⟬ PointsTo┆c2┆⟦isListSeg┆L2'┆b2⟧ ⟭ *⟭
--------------------------------------∗
WP ⟦ $LitV ┆ b1 ⟧ <-
   (Fst (x, ⟦ $LitV ┆ c2 ⟧)%V, ⟦ $LitV ┆ c2 ⟧);; 
   ⟦ $LitV ┆ p1 ⟧ <-
   (Fst ! ⟦ $LitV ┆ p1 ⟧, Snd ! ⟦ $LitV ┆ p2 ⟧);; 
   ⟦ $LitV ┆ f2 ⟧ <- (d1, NONEV);; 
   ⟦ $LitV ┆ p2 ⟧ <-
   (Fst ! ⟦ $LitV ┆ p2 ⟧, ⟦ $LitV ┆ f2 ⟧)
{{ v, Φ v }}

… and set Fst b1 (the queue-ending dummy element d1) to the value x, the first element of L2; set Snd b1 (originally the null pointer) to #c2, the front pointer of list segment L2'.

     wp_store.Σ: gFunctors
heapGS0: heapGS Σ
L1: list val
x: val
L2': list val
p1, p2: loc
Φ: val → iPropI Σ
f1, b1: loc
d1: val
f2, b2: loc
d2: val
c2: loc
⟬* PRE @ "Hp1" : ⟬ PointsTo ┆ p1 ┆ ⟦ $Pair
                   ┆ ⟦ $LitV ┆ f1 ⟧ ┆ 
                   ⟦ $LitV ┆ b1 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HL1" : ⟬ PointsTo┆f1┆⟦isListSeg┆L1┆b1⟧ ⟭ *⟭
⟬* PRE @ "Hb1" : ⟬ PointsTo ┆ b1 ┆ ⟦ $Pair ┆ x
                   ┆ ⟦ $LitV ┆ c2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HΦ" : ⟬ Wand ┆ ⟬ Star ┆ ⟬ PointsTo┆p1┆⟦isQueue┆
                                  L1 ++ 
                                  x :: L2'⟧ ⟭
                           ┆ ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧
                             ⟭
                         ⟭
                  ┆ Φ ⟦ $LitV ┆ ()%V ⟧
                ⟭ *⟭
⟬* PRE @ "Hp2" : ⟬ PointsTo ┆ p2 ┆ ⟦ $Pair
                   ┆ ⟦ $LitV ┆ f2 ⟧ ┆ 
                   ⟦ $LitV ┆ b2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "Hb2" : ⟬ PointsTo ┆ b2 ┆ ⟦ $Pair ┆ d2
                   ┆ NONEV ⟧ ┆ DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "Hf2" : ⟬ PointsTo ┆ f2 ┆ ⟦ $Pair ┆ x
                   ┆ ⟦ $LitV ┆ c2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HL2'" : ⟬ PointsTo┆c2┆⟦isListSeg┆L2'┆b2⟧ ⟭ *⟭
--------------------------------------∗
WP ⟦ $LitV ┆ p1 ⟧ <-
   (Fst ! ⟦ $LitV ┆ p1 ⟧, Snd ! ⟦ $LitV ┆ p2 ⟧);; 
   ⟦ $LitV ┆ f2 ⟧ <- (d1, NONEV);; 
   ⟦ $LitV ┆ p2 ⟧ <-
   (Fst ! ⟦ $LitV ┆ p2 ⟧, ⟦ $LitV ┆ f2 ⟧)
{{ v, Φ v }}

Next, we update the back pointer of the first queue to point to the original ending pair of the second queue.

     wp_load.Σ: gFunctors
heapGS0: heapGS Σ
L1: list val
x: val
L2': list val
p1, p2: loc
Φ: val → iPropI Σ
f1, b1: loc
d1: val
f2, b2: loc
d2: val
c2: loc
⟬* PRE @ "Hp1" : ⟬ PointsTo ┆ p1 ┆ ⟦ $Pair
                   ┆ ⟦ $LitV ┆ f1 ⟧ ┆ 
                   ⟦ $LitV ┆ b1 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HL1" : ⟬ PointsTo┆f1┆⟦isListSeg┆L1┆b1⟧ ⟭ *⟭
⟬* PRE @ "Hb1" : ⟬ PointsTo ┆ b1 ┆ ⟦ $Pair ┆ x
                   ┆ ⟦ $LitV ┆ c2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HΦ" : ⟬ Wand ┆ ⟬ Star ┆ ⟬ PointsTo┆p1┆⟦isQueue┆
                                  L1 ++ 
                                  x :: L2'⟧ ⟭
                           ┆ ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧
                             ⟭
                         ⟭
                  ┆ Φ ⟦ $LitV ┆ ()%V ⟧
                ⟭ *⟭
⟬* PRE @ "Hp2" : ⟬ PointsTo ┆ p2 ┆ ⟦ $Pair
                   ┆ ⟦ $LitV ┆ f2 ⟧ ┆ 
                   ⟦ $LitV ┆ b2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "Hb2" : ⟬ PointsTo ┆ b2 ┆ ⟦ $Pair ┆ d2
                   ┆ NONEV ⟧ ┆ DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "Hf2" : ⟬ PointsTo ┆ f2 ┆ ⟦ $Pair ┆ x
                   ┆ ⟦ $LitV ┆ c2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HL2'" : ⟬ PointsTo┆c2┆⟦isListSeg┆L2'┆b2⟧ ⟭ *⟭
--------------------------------------∗
WP ⟦ $LitV ┆ p1 ⟧ <-
   (Fst ! ⟦ $LitV ┆ p1 ⟧,
    Snd (⟦ $LitV ┆ f2 ⟧, ⟦ $LitV ┆ b2 ⟧)%V);; 
   ⟦ $LitV ┆ f2 ⟧ <- (d1, NONEV);; 
   ⟦ $LitV ┆ p2 ⟧ <-
   (Fst ! ⟦ $LitV ┆ p2 ⟧, ⟦ $LitV ┆ f2 ⟧)
{{ v, Φ v }} wp_load.Σ: gFunctors
heapGS0: heapGS Σ
L1: list val
x: val
L2': list val
p1, p2: loc
Φ: val → iPropI Σ
f1, b1: loc
d1: val
f2, b2: loc
d2: val
c2: loc
⟬* PRE @ "Hp1" : ⟬ PointsTo ┆ p1 ┆ ⟦ $Pair
                   ┆ ⟦ $LitV ┆ f1 ⟧ ┆ 
                   ⟦ $LitV ┆ b1 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HL1" : ⟬ PointsTo┆f1┆⟦isListSeg┆L1┆b1⟧ ⟭ *⟭
⟬* PRE @ "Hb1" : ⟬ PointsTo ┆ b1 ┆ ⟦ $Pair ┆ x
                   ┆ ⟦ $LitV ┆ c2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HΦ" : ⟬ Wand ┆ ⟬ Star ┆ ⟬ PointsTo┆p1┆⟦isQueue┆
                                  L1 ++ 
                                  x :: L2'⟧ ⟭
                           ┆ ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧
                             ⟭
                         ⟭
                  ┆ Φ ⟦ $LitV ┆ ()%V ⟧
                ⟭ *⟭
⟬* PRE @ "Hp2" : ⟬ PointsTo ┆ p2 ┆ ⟦ $Pair
                   ┆ ⟦ $LitV ┆ f2 ⟧ ┆ 
                   ⟦ $LitV ┆ b2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "Hb2" : ⟬ PointsTo ┆ b2 ┆ ⟦ $Pair ┆ d2
                   ┆ NONEV ⟧ ┆ DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "Hf2" : ⟬ PointsTo ┆ f2 ┆ ⟦ $Pair ┆ x
                   ┆ ⟦ $LitV ┆ c2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HL2'" : ⟬ PointsTo┆c2┆⟦isListSeg┆L2'┆b2⟧ ⟭ *⟭
--------------------------------------∗
WP ⟦ $LitV ┆ p1 ⟧ <-
   (Fst (⟦ $LitV ┆ f1 ⟧, ⟦ $LitV ┆ b1 ⟧)%V,
    ⟦ $LitV ┆ b2 ⟧);; 
   ⟦ $LitV ┆ f2 ⟧ <- (d1, NONEV);; 
   ⟦ $LitV ┆ p2 ⟧ <-
   (Fst ! ⟦ $LitV ┆ p2 ⟧, ⟦ $LitV ┆ f2 ⟧)
{{ v, Φ v }} wp_store.Σ: gFunctors
heapGS0: heapGS Σ
L1: list val
x: val
L2': list val
p1, p2: loc
Φ: val → iPropI Σ
f1, b1: loc
d1: val
f2, b2: loc
d2: val
c2: loc
⟬* PRE @ "Hp1" : ⟬ PointsTo ┆ p1 ┆ ⟦ $Pair
                   ┆ ⟦ $LitV ┆ f1 ⟧ ┆ 
                   ⟦ $LitV ┆ b2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HL1" : ⟬ PointsTo┆f1┆⟦isListSeg┆L1┆b1⟧ ⟭ *⟭
⟬* PRE @ "Hb1" : ⟬ PointsTo ┆ b1 ┆ ⟦ $Pair ┆ x
                   ┆ ⟦ $LitV ┆ c2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HΦ" : ⟬ Wand ┆ ⟬ Star ┆ ⟬ PointsTo┆p1┆⟦isQueue┆
                                  L1 ++ 
                                  x :: L2'⟧ ⟭
                           ┆ ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧
                             ⟭
                         ⟭
                  ┆ Φ ⟦ $LitV ┆ ()%V ⟧
                ⟭ *⟭
⟬* PRE @ "Hp2" : ⟬ PointsTo ┆ p2 ┆ ⟦ $Pair
                   ┆ ⟦ $LitV ┆ f2 ⟧ ┆ 
                   ⟦ $LitV ┆ b2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "Hb2" : ⟬ PointsTo ┆ b2 ┆ ⟦ $Pair ┆ d2
                   ┆ NONEV ⟧ ┆ DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "Hf2" : ⟬ PointsTo ┆ f2 ┆ ⟦ $Pair ┆ x
                   ┆ ⟦ $LitV ┆ c2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HL2'" : ⟬ PointsTo┆c2┆⟦isListSeg┆L2'┆b2⟧ ⟭ *⟭
--------------------------------------∗
WP ⟦ $LitV ┆ f2 ⟧ <- (d1, NONEV);; 
   ⟦ $LitV ┆ p2 ⟧ <-
   (Fst ! ⟦ $LitV ┆ p2 ⟧, ⟦ $LitV ┆ f2 ⟧)
{{ v, Φ v }}

We set the pair pointed-to by the second queue's front pointer f2 to (d1, NONEV) (the first queue's original queue-ending element and the null pointer). After that, we update this queue's back pointer to f2 as well.

     wp_store.Σ: gFunctors
heapGS0: heapGS Σ
L1: list val
x: val
L2': list val
p1, p2: loc
Φ: val → iPropI Σ
f1, b1: loc
d1: val
f2, b2: loc
d2: val
c2: loc
⟬* PRE @ "Hp1" : ⟬ PointsTo ┆ p1 ┆ ⟦ $Pair
                   ┆ ⟦ $LitV ┆ f1 ⟧ ┆ 
                   ⟦ $LitV ┆ b2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HL1" : ⟬ PointsTo┆f1┆⟦isListSeg┆L1┆b1⟧ ⟭ *⟭
⟬* PRE @ "Hb1" : ⟬ PointsTo ┆ b1 ┆ ⟦ $Pair ┆ x
                   ┆ ⟦ $LitV ┆ c2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HΦ" : ⟬ Wand ┆ ⟬ Star ┆ ⟬ PointsTo┆p1┆⟦isQueue┆
                                  L1 ++ 
                                  x :: L2'⟧ ⟭
                           ┆ ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧
                             ⟭
                         ⟭
                  ┆ Φ ⟦ $LitV ┆ ()%V ⟧
                ⟭ *⟭
⟬* PRE @ "Hp2" : ⟬ PointsTo ┆ p2 ┆ ⟦ $Pair
                   ┆ ⟦ $LitV ┆ f2 ⟧ ┆ 
                   ⟦ $LitV ┆ b2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "Hb2" : ⟬ PointsTo ┆ b2 ┆ ⟦ $Pair ┆ d2
                   ┆ NONEV ⟧ ┆ DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "Hf2" : ⟬ PointsTo ┆ f2 ┆ ⟦ $Pair ┆ d1
                   ┆ NONEV ⟧ ┆ DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HL2'" : ⟬ PointsTo┆c2┆⟦isListSeg┆L2'┆b2⟧ ⟭ *⟭
--------------------------------------∗
WP ⟦ $LitV ┆ p2 ⟧ <-
   (Fst ! ⟦ $LitV ┆ p2 ⟧, ⟦ $LitV ┆ f2 ⟧)
{{ v, Φ v }} wp_load.Σ: gFunctors
heapGS0: heapGS Σ
L1: list val
x: val
L2': list val
p1, p2: loc
Φ: val → iPropI Σ
f1, b1: loc
d1: val
f2, b2: loc
d2: val
c2: loc
⟬* PRE @ "Hp1" : ⟬ PointsTo ┆ p1 ┆ ⟦ $Pair
                   ┆ ⟦ $LitV ┆ f1 ⟧ ┆ 
                   ⟦ $LitV ┆ b2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HL1" : ⟬ PointsTo┆f1┆⟦isListSeg┆L1┆b1⟧ ⟭ *⟭
⟬* PRE @ "Hb1" : ⟬ PointsTo ┆ b1 ┆ ⟦ $Pair ┆ x
                   ┆ ⟦ $LitV ┆ c2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HΦ" : ⟬ Wand ┆ ⟬ Star ┆ ⟬ PointsTo┆p1┆⟦isQueue┆
                                  L1 ++ 
                                  x :: L2'⟧ ⟭
                           ┆ ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧
                             ⟭
                         ⟭
                  ┆ Φ ⟦ $LitV ┆ ()%V ⟧
                ⟭ *⟭
⟬* PRE @ "Hp2" : ⟬ PointsTo ┆ p2 ┆ ⟦ $Pair
                   ┆ ⟦ $LitV ┆ f2 ⟧ ┆ 
                   ⟦ $LitV ┆ b2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "Hb2" : ⟬ PointsTo ┆ b2 ┆ ⟦ $Pair ┆ d2
                   ┆ NONEV ⟧ ┆ DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "Hf2" : ⟬ PointsTo ┆ f2 ┆ ⟦ $Pair ┆ d1
                   ┆ NONEV ⟧ ┆ DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HL2'" : ⟬ PointsTo┆c2┆⟦isListSeg┆L2'┆b2⟧ ⟭ *⟭
--------------------------------------∗
WP ⟦ $LitV ┆ p2 ⟧ <-
   (Fst (⟦ $LitV ┆ f2 ⟧, ⟦ $LitV ┆ b2 ⟧)%V,
    ⟦ $LitV ┆ f2 ⟧)
{{ v, Φ v }} wp_store.Σ: gFunctors
heapGS0: heapGS Σ
L1: list val
x: val
L2': list val
p1, p2: loc
Φ: val → iPropI Σ
f1, b1: loc
d1: val
f2, b2: loc
d2: val
c2: loc
⟬* PRE @ "Hp1" : ⟬ PointsTo ┆ p1 ┆ ⟦ $Pair
                   ┆ ⟦ $LitV ┆ f1 ⟧ ┆ 
                   ⟦ $LitV ┆ b2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HL1" : ⟬ PointsTo┆f1┆⟦isListSeg┆L1┆b1⟧ ⟭ *⟭
⟬* PRE @ "Hb1" : ⟬ PointsTo ┆ b1 ┆ ⟦ $Pair ┆ x
                   ┆ ⟦ $LitV ┆ c2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HΦ" : ⟬ Wand ┆ ⟬ Star ┆ ⟬ PointsTo┆p1┆⟦isQueue┆
                                  L1 ++ 
                                  x :: L2'⟧ ⟭
                           ┆ ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧
                             ⟭
                         ⟭
                  ┆ Φ ⟦ $LitV ┆ ()%V ⟧
                ⟭ *⟭
⟬* PRE @ "Hp2" : ⟬ PointsTo ┆ p2 ┆ ⟦ $Pair
                   ┆ ⟦ $LitV ┆ f2 ⟧ ┆ 
                   ⟦ $LitV ┆ f2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "Hb2" : ⟬ PointsTo ┆ b2 ┆ ⟦ $Pair ┆ d2
                   ┆ NONEV ⟧ ┆ DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "Hf2" : ⟬ PointsTo ┆ f2 ┆ ⟦ $Pair ┆ d1
                   ┆ NONEV ⟧ ┆ DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HL2'" : ⟬ PointsTo┆c2┆⟦isListSeg┆L2'┆b2⟧ ⟭ *⟭
--------------------------------------∗
|={⊤}=> Φ ⟦ $LitV ┆ ()%V ⟧

Having moved all the elements of the queue at p2 to p1, we apply some lemmas to fold back and unify the representations of the queues between the pre- and postconditions.

     iApply "HΦ"; iModIntro.Σ: gFunctors
heapGS0: heapGS Σ
L1: list val
x: val
L2': list val
p1, p2: loc
Φ: val → iPropI Σ
f1, b1: loc
d1: val
f2, b2: loc
d2: val
c2: loc
⟬* PRE @ "Hp1" : ⟬ PointsTo ┆ p1 ┆ ⟦ $Pair
                   ┆ ⟦ $LitV ┆ f1 ⟧ ┆ 
                   ⟦ $LitV ┆ b2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HL1" : ⟬ PointsTo┆f1┆⟦isListSeg┆L1┆b1⟧ ⟭ *⟭
⟬* PRE @ "Hb1" : ⟬ PointsTo ┆ b1 ┆ ⟦ $Pair ┆ x
                   ┆ ⟦ $LitV ┆ c2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "Hp2" : ⟬ PointsTo ┆ p2 ┆ ⟦ $Pair
                   ┆ ⟦ $LitV ┆ f2 ⟧ ┆ 
                   ⟦ $LitV ┆ f2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "Hb2" : ⟬ PointsTo ┆ b2 ┆ ⟦ $Pair ┆ d2
                   ┆ NONEV ⟧ ┆ DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "Hf2" : ⟬ PointsTo ┆ f2 ┆ ⟦ $Pair ┆ d1
                   ┆ NONEV ⟧ ┆ DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HL2'" : ⟬ PointsTo┆c2┆⟦isListSeg┆L2'┆b2⟧ ⟭ *⟭
--------------------------------------∗
⟬ Star ┆ ⟬ PointsTo┆p1┆⟦isQueue┆L1 ++ x :: L2'⟧ ⟭
  ┆ ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧ ⟭
⟭
     iPoseProof (isQueue_fold_empty with "[$Hp2 $Hf2]") as "HQ2".Σ: gFunctors
heapGS0: heapGS Σ
L1: list val
x: val
L2': list val
p1, p2: loc
Φ: val → iPropI Σ
f1, b1: loc
d1: val
f2, b2: loc
d2: val
c2: loc
⟬* PRE @ "Hp1" : ⟬ PointsTo ┆ p1 ┆ ⟦ $Pair
                   ┆ ⟦ $LitV ┆ f1 ⟧ ┆ 
                   ⟦ $LitV ┆ b2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HL1" : ⟬ PointsTo┆f1┆⟦isListSeg┆L1┆b1⟧ ⟭ *⟭
⟬* PRE @ "Hb1" : ⟬ PointsTo ┆ b1 ┆ ⟦ $Pair ┆ x
                   ┆ ⟦ $LitV ┆ c2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "Hb2" : ⟬ PointsTo ┆ b2 ┆ ⟦ $Pair ┆ d2
                   ┆ NONEV ⟧ ┆ DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HL2'" : ⟬ PointsTo┆c2┆⟦isListSeg┆L2'┆b2⟧ ⟭ *⟭
⟬* PRE @ "HQ2" : ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧ ⟭ *⟭
--------------------------------------∗
⟬ Star ┆ ⟬ PointsTo┆p1┆⟦isQueue┆L1 ++ x :: L2'⟧ ⟭
  ┆ ⟬ PointsTo┆p2┆⟦isQueue┆[]⟧ ⟭
⟭
     iFrame "HQ2".Σ: gFunctors
heapGS0: heapGS Σ
L1: list val
x: val
L2': list val
p1, p2: loc
Φ: val → iPropI Σ
f1, b1: loc
d1: val
f2, b2: loc
d2: val
c2: loc
⟬* PRE @ "Hp1" : ⟬ PointsTo ┆ p1 ┆ ⟦ $Pair
                   ┆ ⟦ $LitV ┆ f1 ⟧ ┆ 
                   ⟦ $LitV ┆ b2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HL1" : ⟬ PointsTo┆f1┆⟦isListSeg┆L1┆b1⟧ ⟭ *⟭
⟬* PRE @ "Hb1" : ⟬ PointsTo ┆ b1 ┆ ⟦ $Pair ┆ x
                   ┆ ⟦ $LitV ┆ c2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "Hb2" : ⟬ PointsTo ┆ b2 ┆ ⟦ $Pair ┆ d2
                   ┆ NONEV ⟧ ┆ DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HL2'" : ⟬ PointsTo┆c2┆⟦isListSeg┆L2'┆b2⟧ ⟭ *⟭
--------------------------------------∗
⟬ PointsTo┆p1┆⟦isQueue┆L1 ++ x :: L2'⟧ ⟭
     iPoseProof (isListSeg_cons_app with "[$Hb1 $HL2']") as "HL2".Σ: gFunctors
heapGS0: heapGS Σ
L1: list val
x: val
L2': list val
p1, p2: loc
Φ: val → iPropI Σ
f1, b1: loc
d1: val
f2, b2: loc
d2: val
c2: loc
⟬* PRE @ "Hp1" : ⟬ PointsTo ┆ p1 ┆ ⟦ $Pair
                   ┆ ⟦ $LitV ┆ f1 ⟧ ┆ 
                   ⟦ $LitV ┆ b2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HL1" : ⟬ PointsTo┆f1┆⟦isListSeg┆L1┆b1⟧ ⟭ *⟭
⟬* PRE @ "Hb2" : ⟬ PointsTo ┆ b2 ┆ ⟦ $Pair ┆ d2
                   ┆ NONEV ⟧ ┆ DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HL2" : ⟬ PointsTo┆b1┆⟦isListSeg┆
                 x :: L2'┆b2⟧ ⟭ *⟭
--------------------------------------∗
⟬ PointsTo┆p1┆⟦isQueue┆L1 ++ x :: L2'⟧ ⟭
     iPoseProof (isListSeg_concat with "[$HL1 $HL2]") as "HL".Σ: gFunctors
heapGS0: heapGS Σ
L1: list val
x: val
L2': list val
p1, p2: loc
Φ: val → iPropI Σ
f1, b1: loc
d1: val
f2, b2: loc
d2: val
c2: loc
⟬* PRE @ "Hp1" : ⟬ PointsTo ┆ p1 ┆ ⟦ $Pair
                   ┆ ⟦ $LitV ┆ f1 ⟧ ┆ 
                   ⟦ $LitV ┆ b2 ⟧ ⟧ ┆ 
                   DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "Hb2" : ⟬ PointsTo ┆ b2 ┆ ⟦ $Pair ┆ d2
                   ┆ NONEV ⟧ ┆ DfracOwn 1
                 ⟭ *⟭
⟬* PRE @ "HL" : ⟬ PointsTo┆f1┆⟦isListSeg┆
                L1 ++ x :: L2'┆b2⟧ ⟭ *⟭
--------------------------------------∗
⟬ PointsTo┆p1┆⟦isQueue┆L1 ++ x :: L2'⟧ ⟭
     iPoseProof (isQueue_fold with "[$Hp1 $HL $Hb2]") as "HQ1".Σ: gFunctors
heapGS0: heapGS Σ
L1: list val
x: val
L2': list val
p1, p2: loc
Φ: val → iPropI Σ
f1, b1: loc
d1: val
f2, b2: loc
d2: val
c2: loc
⟬* PRE @ "HQ1" : ⟬ PointsTo┆p1┆⟦isQueue┆
                 L1 ++ x :: L2'⟧ ⟭ *⟭
--------------------------------------∗
⟬ PointsTo┆p1┆⟦isQueue┆L1 ++ x :: L2'⟧ ⟭
     by iFrame.
 Qed.

Integration with VsRocq

As we mentioned before, this webpage was generated using our integration with Alectryon, a tool primarily meant for presenting Rocq proofs in a literate style. We were able to freely intersperse prose explanations with Rocq code above and hide irrelevant parts of the code or output.

Meanwhile, our tool also integrates with VsRocq, a VS Code extension for editing Rocq proofs. You can find the extension here!

Extensions and Reusability

Adding a new operator

Adding support for a new operator is simply a matter of adding a new notation to translate the surface syntax of the separation logic framework into the more abstract syntax expected by our visualizer. We demonstrate this below for the big-∧ operator (iterated conjunction). The first Check command shows the default output from Rocq/Iris…

 Check (([∧ list] x ∈ xs, P x)%I).([∧ list] x ∈ xs, P x)%I
     : iPropI Σ

Then, we translate it to a BigOp term with the operator symbol, iteration label, and body predicate as arguments…

 Notation "'BigOp' ┆ ∧  ┆ x ∈ l ┆ P" :=
   (big_opL bi_and (λ _ x, P%I) l)
     (in custom sep at level 200,
     x constr, l constr, P constr at level 200): sepviz_scope.

… so that the visualizer supports the operator, as in the output of the command below.

 Check (([∧ list] x ∈ xs, P x)%I).⟬ BigOp ┆ ∧ ┆ x ∈ xs ┆ P x ⟭
     : iPropI Σ

If you want to try your own operators, copying and modifying notations from our existing sets of notations is a good place to start.

Supporting a new framework

Separation Logic Foundations is Volume 6 of the Software Foundations textbooks in Rocq. It comes with its own mechanization of separation logic based on CFML. We invite the reader to browse the file SLFExample.v in VS Code with our VsRocq integration. In that file, we have set up notations similar to the previous examples for the representation predicates defined in that file (linked lists and stacks), which enable visualizations.

Adding a new representation predicate

Scroll to line 825 in SLFExample.v. This is a logical, inductive definition of a tree as either an empty Leaf or a Node with a value and two subtrees.

A few lines below, the representation predicate MTree states that the structure at location p is a logical tree T: either an empty Leaf, in which case p = null (a pure predicate), or a Node, in which case p points to a record with a value and two subtrees where MTree recursively holds.

Adding visualization support is straightforward. We already have notations for records and the required separation logic operators. We just need to add a notation to print MTree terms in the syntax our tool expects. Copy and paste the following definition into the marked section of the file (in VS Code):

Notation "'PointsTo' ┆ p ┆ ⟦ '$MTree' ┆ x ⟧" :=
  (MTree x p)
    (in custom sep at level 200,
     p constr, x constr at level 200): sepviz_scope.

Then, we need to specify how to notate this structure. It should receive the label “MTree”, and its single argument apart from the location (above, x) should be shown as a row in a table. (This is only when the argument is not destructed further and MTree is not expanded into its definition.) Copy and paste the following definition at the end of the sepviz.yaml file (in VS Code):

'$MTree':
  label: 'MTree'
  args:
    0:
      inTable: true

(Make sure the indentation matches the entry right above it!) Now, back in SLFExample.v, step through the next few sections of the file to see visualizations of theorems with trees.

Conclusion

This concludes our tutorial! Sepviz is free and open source and available under an MIT license. The CAV paper (open access) documents its architecture and usage, and the repository documents how to set up the necessary dependencies and environment.