Merge branch 'master' of gitlab.mpi-sws.org:FP/iris-examples

.gitignore

 *.vo
 *.vio
 *.v.d
+.coqdeps.d
 *.glob
 *.cache
 *.aux

.gitlab-ci.yml

 image: ralfjung/opam-ci:latest
 
+stages:
+  - build
+
 variables:
-  CPU_CORES: "9"
+  CPU_CORES: "10"
 
 .template: &template
+  stage: build
   tags:
-  - fp-timing
+  - fp
   script:
   # prepare
   - . build/opam-ci.sh $OPAM_PINS
@@ -14,7 +18,8 @@ variables:
   - 'time make -k -j$CPU_CORES TIMED=y 2>&1 | tee build-log.txt'
   - 'if fgrep Axiom build-log.txt >/dev/null; then exit 1; fi'
   - 'cat build-log.txt | egrep "[a-zA-Z0-9_/-]+ \((real|user): [0-9]" | tee build-time.txt'
-  - 'if test -n "$VALIDATE" && (( RANDOM % 10 == 0 )); then make validate; fi'
+  # maybe validate
+  - 'if [[ -n "$VALIDATE" ]]; then make validate; fi'
   cache:
     key: "$CI_JOB_NAME"
     paths:
@@ -22,29 +27,33 @@ variables:
   only:
   - master
   - /^ci/
-
-build-coq.8.7.0:
-  <<: *template
-  variables:
-    OPAM_PINS: "coq version 8.7.0   coq-mathcomp-ssreflect version 1.6.2"
   except:
   - triggers
+  - schedules
 
-build-coq.8.6.1:
+## Build jobs
+
+build-coq.8.7.1:
   <<: *template
   variables:
-    OPAM_PINS: "coq version 8.6.1   coq-mathcomp-ssreflect version 1.6.2"
-    VALIDATE: "1"
+    OPAM_PINS: "coq version 8.7.1   coq-mathcomp-ssreflect version 1.6.4"
+  tags:
+  - fp-timing
   artifacts:
     paths:
     - build-time.txt
     - build-env.txt
-  except:
-  - triggers
+
+build-coq.8.6.1:
+  <<: *template
+  variables:
+    OPAM_PINS: "coq version 8.6.1   coq-mathcomp-ssreflect version 1.6.4"
 
 build-iris.dev:
   <<: *template
   variables:
-    OPAM_PINS: "coq version 8.6.1   coq-mathcomp-ssreflect version 1.6.2   coq-iris.dev git https://gitlab.mpi-sws.org/FP/iris-coq.git#$IRIS_REV"
+    OPAM_PINS: "coq version 8.7.1   coq-mathcomp-ssreflect version 1.6.4   coq-iris.dev git https://gitlab.mpi-sws.org/FP/iris-coq.git#$IRIS_REV"
+  except:
   only:
   - triggers
+  - schedules

Makefile

@@ -15,7 +15,7 @@ clean: Makefile.coq
 # Create Coq Makefile. POSIX awk can't do in-place editing, but coq_makefile wants the real
 # filename, so we do some file gymnastics.
 Makefile.coq: _CoqProject Makefile awk.Makefile
-	coq_makefile -f _CoqProject -o Makefile.coq
+	"$(COQBIN)coq_makefile" -f _CoqProject -o Makefile.coq
 	mv Makefile.coq Makefile.coq.tmp && awk -f awk.Makefile Makefile.coq.tmp > Makefile.coq && rm Makefile.coq.tmp
 
 # Install build-dependencies

Makefile.coq.local

+# Per-project targets
+include Makefile.coq.conf
+VOFILES=$(COQMF_VFILES:.v=.vo)
+
+barrier: $(filter theories/barrier/%,$(VOFILES))
+.PHONY: barrier
+
+lecture_notes: $(filter theories/barrier/%,$(VOFILES))
+.PHONY: lecture_notes
+
+spanning_tree: $(filter theories/spanning_tree/%,$(VOFILES))
+.PHONY: spanning_tree
+
+concurrent_stacks: $(filter theories/concurrent_stacks/%,$(VOFILES))
+.PHONY: concurrent_stacks
+
+logrel: $(filter theories/logrel/%,$(VOFILES))
+.PHONY: logrel

README.md

@@ -6,26 +6,64 @@ Some example verification demonstrating the use of Iris.
 
 This version is known to compile with:
 
- - Coq 8.6.1 / 8.7.0
- - Ssreflect 1.6.2
+ - Coq 8.6.1 / 8.7.1
+ - Ssreflect 1.6.4
  - A development version of [Iris](https://gitlab.mpi-sws.org/FP/iris-coq/)
+ - The coq86-devel branch of [Autosubst](https://github.com/uds-psl/autosubst)
 
-The easiest way to install the correct versions of the dependencies is through
-opam.  Once you got opam set up, just run `make build-dep` to install the right
-versions of the dependencies.  When the dependencies change (e.g., a newer
-version of Iris is needed), just run `make build-dep` again.
+## Building from source
 
-Alternatively, you can manually determine the required Iris commit by consulting
-the `opam.pins` file.
+When building from source, we recommend to use opam (1.2.2 or newer) for
+installing the dependencies.  This requires the following two repositories:
 
-## Building Instructions
+    opam repo add coq-released https://coq.inria.fr/opam/released
+    opam repo add iris-dev https://gitlab.mpi-sws.org/FP/opam-dev.git
 
-Run `make` to build the full development.
+Once you got opam set up, run `make build-dep` to install the right versions
+of the dependencies.
+
+Run `make -jN` to build the full development, where `N` is the number of your
+CPU cores.
+
+To update, do `git pull`.  After an update, the development may fail to compile
+because of outdated dependencies.  To fix that, please run `opam update`
+followed by `make build-dep`.
+
+## Case Studies
+
+This repository contains the following case studies:
+
+* [barrier](theories/barrier): Implementation and proof of a barrier as
+  described in ["Higher-Order Ghost State"](http://doi.acm.org/10.1145/2818638).
+* [logrel](theories/logrel): Logical relations from the
+  [IPM paper](http://doi.acm.org/10.1145/3093333.3009855):
+  - STLC
+      - Unary logical relations proving type safety
+  - F_mu (System F with recursive types)
+      - Unary logical relations proving type safety
+  - F_mu_ref (System F with recursive types and references)
+      - Unary logical relations proving type safety
+      - Binary logical relations for proving contextual refinements
+  - F_mu_ref_conc (System F with recursive types, references and concurrency)
+      - Unary logical relations proving type safety
+      - Binary logical relations for proving contextual refinements
+          - Proof of refinement for a pair of fine-grained/coarse-grained
+            concurrent counter implementations
+          - Proof of refinement for a pair of fine-grained/coarse-grained
+            concurrent stack implementations
+* [spanning-tree](theories/spanning_tree): Proof of a concurrent spanning tree
+  algorithm.
+* [concurrent-stacks](theories/concurrent_stacks): Proof of an implementation of
+  concurrent stacks with helping, as described in the [report](http://iris-project.org/pdfs/2017-case-study-concurrent-stacks-with-helping.pdf).
+* [lecture-notes](theories/lecture_notes): Coq examples for the
+  [Iris lecture notes](http://iris-project.org/tutorial-material.html).
 
 ## For Developers: How to update the Iris dependency
 
-- Do the change in Iris, push it.
-- In iris-atomic, change opam.pins to point to the new commit.
-- Run "make build-dep" (in iris-example) to install the new version of Iris.
-- You may have to do "make clean" as Coq will likely complain about .vo file
+* Do the change in Iris, push it.
+* Wait for CI to publish a new Iris version on the opam archive, then run
+  `opam update iris-dev`.
+* In iris-examples, change the `opam` file to depend on the new version.
+* Run `make build-dep` (in iris-examples) to install the new version of Iris.
+  You may have to do `make clean` as Coq will likely complain about .vo file
   mismatches.

_CoqProject

@@ -6,3 +6,57 @@ theories/barrier/barrier.v
 theories/barrier/protocol.v
 theories/barrier/example_client.v
 theories/barrier/example_joining_existentials.v
+
+theories/lecture_notes/coq_intro_example_1.v
+
+theories/spanning_tree/graph.v
+theories/spanning_tree/mon.v
+theories/spanning_tree/spanning.v
+theories/spanning_tree/proof.v
+
+theories/concurrent_stacks/concurrent_stack1.v
+theories/concurrent_stacks/concurrent_stack2.v
+theories/concurrent_stacks/concurrent_stack3.v
+theories/concurrent_stacks/concurrent_stack4.v
+
+theories/logrel/prelude/base.v
+theories/logrel/stlc/lang.v
+theories/logrel/stlc/typing.v
+theories/logrel/stlc/rules.v
+theories/logrel/stlc/logrel.v
+theories/logrel/stlc/fundamental.v
+theories/logrel/stlc/soundness.v
+theories/logrel/F_mu/lang.v
+theories/logrel/F_mu/typing.v
+theories/logrel/F_mu/rules.v
+theories/logrel/F_mu/logrel.v
+theories/logrel/F_mu/fundamental.v
+theories/logrel/F_mu/soundness.v
+theories/logrel/F_mu_ref/lang.v
+theories/logrel/F_mu_ref/typing.v
+theories/logrel/F_mu_ref/rules.v
+theories/logrel/F_mu_ref/rules_binary.v
+theories/logrel/F_mu_ref/logrel.v
+theories/logrel/F_mu_ref/logrel_binary.v
+theories/logrel/F_mu_ref/fundamental.v
+theories/logrel/F_mu_ref/fundamental_binary.v
+theories/logrel/F_mu_ref/soundness.v
+theories/logrel/F_mu_ref/context_refinement.v
+theories/logrel/F_mu_ref/soundness_binary.v
+theories/logrel/F_mu_ref_conc/lang.v
+theories/logrel/F_mu_ref_conc/rules.v
+theories/logrel/F_mu_ref_conc/typing.v
+theories/logrel/F_mu_ref_conc/logrel_unary.v
+theories/logrel/F_mu_ref_conc/fundamental_unary.v
+theories/logrel/F_mu_ref_conc/rules_binary.v
+theories/logrel/F_mu_ref_conc/logrel_binary.v
+theories/logrel/F_mu_ref_conc/fundamental_binary.v
+theories/logrel/F_mu_ref_conc/soundness_unary.v
+theories/logrel/F_mu_ref_conc/context_refinement.v
+theories/logrel/F_mu_ref_conc/soundness_binary.v
+theories/logrel/F_mu_ref_conc/examples/lock.v
+theories/logrel/F_mu_ref_conc/examples/counter.v
+theories/logrel/F_mu_ref_conc/examples/stack/stack_rules.v
+theories/logrel/F_mu_ref_conc/examples/stack/CG_stack.v
+theories/logrel/F_mu_ref_conc/examples/stack/FG_stack.v
+theories/logrel/F_mu_ref_conc/examples/stack/refinement.v

build/opam-ci.sh

@@ -55,7 +55,7 @@ done
 # Upgrade cached things.
 echo
 echo "[opam-ci] Upgrading opam"
-opam upgrade -y --fixup
+opam upgrade -y --fixup && opam upgrade -y
 
 # Install build-dependencies.
 echo
@@ -63,5 +63,6 @@ echo "[opam-ci] Installing build-dependencies"
 make build-dep OPAMFLAGS=-y
 
 # done
+set +x
 echo
 coqc -v

opam

@@ -10,4 +10,5 @@ install: [make "install"]
 remove: ["rm" "-rf" "%{lib}%/coq/user-contrib/iris_examples"]
 depends: [
   "coq-iris" { (= "dev.2018-02-21.1") | (= "dev") }
+  "coq-autosubst" { = "dev.coq86" }
 ]

theories/concurrent_stacks/concurrent_stack1.v

+From iris.base_logic Require Import base_logic.
+From iris.proofmode Require Import tactics.
+From iris.base_logic.lib Require Import invariants.
+From iris.program_logic Require Export weakestpre hoare.
+From iris.heap_lang Require Export lang.
+From iris.algebra Require Import agree list.
+From iris.heap_lang Require Import assert proofmode notation.
+Set Default Proof Using "Type".
+
+(** Stack 1: No helping, bag spec. *)
+
+Definition mk_stack : val :=
+  λ: "_",
+  let: "r" := ref NONEV in
+  (rec: "pop" "n" :=
+     match: !"r" with
+       NONE => #-1
+     | SOME "hd" =>
+       if: CAS "r" (SOME "hd") (Snd "hd")
+       then Fst "hd"
+       else "pop" "n"
+     end,
+    rec: "push" "n" :=
+       let: "r'" := !"r" in
+       let: "r''" := SOME ("n", "r'") in
+       if: CAS "r" "r'" "r''"
+       then #()
+       else "push" "n").
+
+Section stacks.
+  Context `{!heapG Σ}.
+  Implicit Types l : loc.
+
+  Definition is_stack_pre (P : val → iProp Σ) (F : val -c> iProp Σ) :
+     val -c> iProp Σ := λ v,
+    (v ≡ NONEV ∨ ∃ (h t : val), v ≡ SOMEV (h, t)%V ∗ P h ∗ ▷ F t)%I.
+
+  Local Instance is_stack_contr (P : val → iProp Σ): Contractive (is_stack_pre P).
+  Proof.
+    rewrite /is_stack_pre => n f f' Hf v.
+    repeat (f_contractive || f_equiv).
+    apply Hf.
+  Qed.
+
+  Definition is_stack_def (P : val -> iProp Σ) := fixpoint (is_stack_pre P).
+  Definition is_stack_aux P : seal (@is_stack_def P). by eexists. Qed.
+  Definition is_stack P := unseal (is_stack_aux P).
+  Definition is_stack_eq P : @is_stack P = @is_stack_def P := seal_eq (is_stack_aux P).
+
+  Definition stack_inv P v :=
+    (∃ l v', ⌜v = #l⌝ ∗ l ↦ v' ∗ is_stack P v')%I.
+
+
+  Lemma is_stack_unfold (P : val → iProp Σ) v :
+      is_stack P v ⊣⊢ is_stack_pre P (is_stack P) v.
+  Proof.
+    rewrite is_stack_eq. apply (fixpoint_unfold (is_stack_pre P)).
+  Qed.
+
+  Lemma is_stack_disj (P : val → iProp Σ) v :
+      is_stack P v -∗ is_stack P v ∗ (v ≡ NONEV ∨ ∃ (h t : val), v ≡ SOMEV (h, t)%V).
+  Proof.
+    iIntros "Hstack".
+    iDestruct (is_stack_unfold with "Hstack") as "[#Hstack|Hstack]".
+    - iSplit; try iApply is_stack_unfold; iLeft; auto.
+    - iDestruct "Hstack" as (h t) "[#Heq rest]".
+      iSplitL; try iApply is_stack_unfold; iRight; auto.
+  Qed.
+
+  (* Per-element invariant (i.e., bag spec). *)
+  Theorem stack_works P Φ :
+    (∀ (f₁ f₂ : val),
+            (∀ (v : val), □ WP f₁ #() {{ v, P v  ∨ v ≡ #-1 }})
+         -∗ (∀ (v : val), □ (P v -∗ WP f₂ v {{ v, True }}))
+         -∗ Φ (f₁, f₂)%V)%I
+    -∗ WP mk_stack #()  {{ Φ }}.
+  Proof.
+    iIntros "HΦ".
+    wp_lam.
+    wp_alloc l as "Hl".
+    pose proof (nroot .@ "N") as N.
+    rewrite -wp_fupd.
+    iMod (inv_alloc N _ (stack_inv P #l) with "[Hl]") as "#Hisstack".
+    iExists l, NONEV; iSplit; iFrame; auto.
+    { iApply is_stack_unfold. iLeft; auto. }
+    wp_let.
+    iModIntro.
+    iApply "HΦ".
+    - iIntros (v) "!#".
+      iLöb as "IH".
+      wp_rec.
+      wp_bind (! #l)%E.
+      iInv N as "Hstack" "Hclose".
+      iDestruct "Hstack" as (l' v') "[>% [Hl' Hstack]]".
+      injection H; intros; subst.
+      wp_load.
+      iDestruct (is_stack_disj with "Hstack") as "[Hstack #Heq]".
+      iMod ("Hclose" with "[Hl' Hstack]").
+      iExists l', v'; iFrame; auto.
+      iModIntro.
+      iDestruct "Heq" as "[H | H]".
+      + iRewrite "H".
+        wp_match.
+        iRight; auto.
+      + iDestruct "H" as (h t) "H".
+        iRewrite "H".
+        assert (to_val (h, t)%V = Some (h, t)%V) by apply to_of_val.
+        assert (is_Some (to_val (h, t)%V)) by (exists (h, t)%V; auto).
+        wp_match. fold of_val.
+        unfold subst; simpl; fold subst.
+        wp_bind (CAS _ _ _).
+        wp_proj.
+        iInv N as "Hstack" "Hclose".
+        iDestruct "Hstack" as (l'' v'') "[>% [Hl'' Hstack]]".
+        injection H2; intros; subst.
+        assert (Decision (v'' = InjRV (h, t)%V)) as Heq by apply val_eq_dec.
+        destruct Heq.
+        * wp_cas_suc.
+          iDestruct (is_stack_unfold with "Hstack") as "[Hstack | Hstack]".
+          subst.
+          iDestruct "Hstack" as "%"; discriminate.
+          iDestruct "Hstack" as (h' t') "[% [HP Hstack]]".
+          subst.
+          injection H3.
+          intros.
+          subst.
+          iMod ("Hclose" with "[Hl'' Hstack]").
+          iExists l'', t'; iFrame; auto.
+          iModIntro.
+          wp_if.
+          wp_proj.
+          iLeft; auto.
+        * wp_cas_fail.
+          iMod ("Hclose" with "[Hl'' Hstack]").
+          iExists l'', v''; iFrame; auto.
+          iModIntro.
+          wp_if.
+          iApply "IH".
+    - iIntros (v) "!# HP".
+      iLöb as "IH".
+      wp_rec.
+      wp_bind (! _)%E.
+      iInv N as "Hstack" "Hclose".
+      iDestruct "Hstack" as (l' v') "[>% [Hl' Hstack]]".
+      injection H; intros; subst.
+      wp_load.
+      iMod ("Hclose" with "[Hl' Hstack]").
+      by (iExists l', v'; iFrame).
+      iModIntro.
+      wp_let.
+      wp_let.
+      wp_bind (CAS _ _ _).
+      iInv N as "Hstack" "Hclose".
+      iDestruct "Hstack" as (l'' v'') "[>% [Hl'' Hstack]]".
+      injection H0; intros; subst.
+      assert (Decision (v'' = v'%V)) as Heq by apply val_eq_dec.
+      destruct Heq.
+      + wp_cas_suc.
+        iMod ("Hclose" with "[Hl'' HP Hstack]").
+        iExists l'', (InjRV (v, v')%V).
+        iFrame; auto.
+        iSplit; auto.
+        iApply is_stack_unfold.
+        iRight.
+        iExists v, v'.
+        iSplit; auto.
+        subst; iFrame.
+        iModIntro.
+        wp_if.
+        done.
+      + wp_cas_fail.
+        iMod ("Hclose" with "[Hl'' Hstack]").
+        iExists l'', v''; iFrame; auto.
+        iModIntro.
+        wp_if.
+        iApply "IH".
+        done.
+  Qed.
+End stacks.

theories/concurrent_stacks/concurrent_stack3.v

+From iris.program_logic Require Export weakestpre hoare.
+From iris.heap_lang Require Export lang proofmode notation.
+From iris.algebra Require Import excl.
+Set Default Proof Using "Type".
+
+(** Stack 3: No helping, view-shift spec. *)
+
+Definition mk_stack : val :=
+  λ: "_",
+  let: "r" := ref NONEV in
+  (rec: "pop" "n" :=
+       (match: !"r" with
+          NONE => NONE
+        | SOME "hd" =>
+          if: CAS "r" (SOME "hd") (Snd "hd")
+          then SOME (Fst "hd")
+          else "pop" "n"
+        end),
+    rec: "push" "n" :=
+        let: "r'" := !"r" in
+        let: "r''" := SOME ("n", "r'") in
+        if: CAS "r" "r'" "r''"
+        then #()
+        else "push" "n").
+
+Section stack_works.
+  Context `{!heapG Σ}.
+  Implicit Types l : loc.
+
+  Fixpoint is_stack xs v : iProp Σ :=
+    (match xs with
+     | [] => ⌜v = NONEV⌝
+     | x :: xs => ∃ (t : val), ⌜v = SOMEV (x, t)%V⌝ ∗ is_stack xs t
+     end)%I.
+
+  Definition stack_inv P v :=
+    (∃ l v' xs, ⌜v = #l⌝ ∗ l ↦ v' ∗ is_stack xs v' ∗ P xs)%I.
+
+  Lemma is_stack_disj xs v :
+      is_stack xs v -∗ is_stack xs v ∗ (⌜v = NONEV⌝ ∨ ∃ (h t : val), ⌜v = SOMEV (h, t)%V⌝).
+  Proof.
+    iIntros "Hstack".
+    destruct xs.
+    - iSplit; try iLeft; auto.
+    - iSplit; auto; iRight; iDestruct "Hstack" as (t) "[% Hstack]";
+      iExists v0, t; auto.
+  Qed.
+
+  Lemma is_stack_uniq : ∀ xs ys v,
+      is_stack xs v ∗ is_stack ys v -∗ ⌜xs = ys⌝.
+  Proof.
+    induction xs, ys; iIntros (v') "[Hstack1 Hstack2]"; auto.
+    - iDestruct "Hstack1" as "%".
+      iDestruct "Hstack2" as (t) "[% Hstack2]".
+      subst.
+      discriminate.
+    - iDestruct "Hstack2" as "%".
+      iDestruct "Hstack1" as (t) "[% Hstack1]".
+      subst.
+      discriminate.
+    - iDestruct "Hstack1" as (t) "[% Hstack1]".
+      iDestruct "Hstack2" as (t') "[% Hstack2]".
+      subst; injection H0; intros; subst.
+      iDestruct (IHxs with "[Hstack1 Hstack2]") as "%".
+        by iSplitL "Hstack1".
+      subst; auto.
+  Qed.
+
+  Lemma is_stack_empty : ∀ xs,
+      is_stack xs (InjLV #()) -∗ ⌜xs = []⌝.
+  Proof.
+    iIntros (xs) "Hstack".
+    destruct xs; auto.
+    iDestruct "Hstack" as (t) "[% rest]".
+    discriminate.
+  Qed.
+  Lemma is_stack_cons : ∀ xs h t,
+      is_stack xs (InjRV (h, t)%V) -∗
+               is_stack xs (InjRV (h, t)%V) ∗ ∃ ys, ⌜xs = h :: ys⌝.
+  Proof.
+    destruct xs; iIntros (h t) "Hstack".
+    - iDestruct "Hstack" as "%"; discriminate.
+    - iSplit; [auto | iExists xs].
+      iDestruct "Hstack" as (t') "[% Hstack]".
+      injection H; intros; subst; auto.
+  Qed.
+
+  (* Whole-stack invariant (P). However:
+     - The resources for the successful and failing pop must be disjoint.
+       Instead, there should be a normal conjunction between them.
+     Open question: How does this relate to a logically atomic spec? *)
+  Theorem stack_works P Q Q' Q'' Φ :
+    (∀ (f₁ f₂ : val) ι,
+        (□((∀ v vs, P (v :: vs) ={⊤∖↑ι}=∗ Q v ∗ P vs) -∗ (* pop *)
+            (P [] ={⊤∖↑ι}=∗ Q' ∗ P []) -∗
+            WP f₁ #() {{ v, (∃ (v' : val), v ≡ SOMEV v' ∗ Q v') ∨ (v ≡ NONEV ∗ Q')}}))
+         -∗ (∀ (v : val), (* push *)
+               □ ((∀ vs, P vs ={⊤∖↑ι}=∗ P (v :: vs) ∗ Q'') -∗
+                  WP f₂ v {{ v, Q'' }}))
+         -∗ Φ (f₁, f₂)%V)%I
+    -∗ P []
+    -∗ WP mk_stack #()  {{ Φ }}.
+  Proof.
+    iIntros "HΦ HP".
+    pose proof (nroot .@ "N") as N.
+    wp_let.
+    wp_alloc l as "Hl".
+    iMod (inv_alloc N _ (stack_inv P #l) with "[Hl HP]") as "#Istack".
+    { iNext; iExists l, (InjLV #()), []; iSplit; iFrame; auto. }
+    wp_let.
+    iApply "HΦ".
+    - iIntros "!# Hsucc Hfail".
+      iLöb as "IH".
+      wp_rec.
+      wp_bind (! _)%E.
+      iInv N as "Hstack" "Hclose".
+      iDestruct "Hstack" as (l' v' xs) "[>% [Hl' [Hstack HP]]]".
+      injection H; intros; subst.
+      wp_load.
+      iDestruct (is_stack_disj with "[Hstack]") as "[Hstack H]"; auto.
+      iDestruct "H" as "[% | H]".
+      * subst.
+        iDestruct (is_stack_empty with "Hstack") as "%".
+        subst.
+        iMod ("Hfail" with "HP") as "[HQ' HP]".
+        iMod ("Hclose" with "[Hl' Hstack HP]").
+        { iExists l', (InjLV #()), []; iSplit; iFrame; auto. }
+        iModIntro.
+        wp_match.
+        iRight; auto.
+      * iDestruct "H" as (h t) "%".
+        subst.
+        iMod ("Hclose" with "[Hl' Hstack HP]").
+        { iExists l', (InjRV (h, t)), xs; iSplit; iFrame; auto. }
+        iModIntro.
+
+        assert (to_val (h, t)%V = Some (h, t)%V) by apply to_of_val.
+        assert (is_Some (to_val (h, t)%V)) by (exists (h, t)%V; auto).
+        wp_match.
+        unfold subst; simpl; fold of_val.
+
+        wp_proj.
+        wp_bind (CAS _ _ _).
+        iInv N as "Hstack" "Hclose".
+        iDestruct "Hstack" as (l'' v' ys) "[>% [Hl'' [Hstack HP]]]".
+        injection H2; intros; subst.
+        assert (Decision (v' = InjRV (h, t)%V)) as Heq by apply val_eq_dec.
+        destruct Heq.
+      + wp_cas_suc.
+        subst.
+        iDestruct (is_stack_cons with "Hstack") as "[Hstack H]".
+        iDestruct "H" as (ys') "%"; subst.
+        iDestruct "Hstack" as (t') "[% Hstack]".
+        injection H3; intros; subst.
+        iDestruct ("Hsucc" with "[HP]") as "> [HQ HP]"; auto.
+        iMod ("Hclose" with "[Hl'' Hstack HP]").
+        { iExists l'', t', ys'; iSplit; iFrame; auto. }
+        iModIntro.
+        wp_if.
+        wp_proj.
+        iLeft; iExists h; auto.
+      + wp_cas_fail.
+        iMod ("Hclose" with "[Hl'' Hstack HP]").
+        { iExists l'', v', ys; iSplit; iFrame; auto. }
+        iModIntro.
+        wp_if.
+        iApply ("IH" with "Hsucc Hfail").
+    - iIntros (v) "!# Hpush".
+      iLöb as "IH".
+      wp_rec.
+      wp_bind (! _)%E.
+      iInv N as "Hstack" "Hclose".
+      iDestruct "Hstack" as (l' v' ys) "[>% [Hl' [Hstack HP]]]".
+      injection H; intros; subst.
+      wp_load.
+      iMod ("Hclose" with "[Hl' Hstack HP]").
+      { iExists l', v', ys; iSplit; iFrame; auto. }
+      iModIntro.
+      wp_let.
+      wp_let.
+      wp_bind (CAS _ _ _).
+      iInv N as "Hstack" "Hclose".
+      iDestruct "Hstack" as (l'' v'' xs) "[>% [Hl'' [Hstack HP]]]".
+      injection H0; intros; subst.
+      assert (Decision (v' = v''%V)) as Heq by apply val_eq_dec.
+      destruct Heq.
+      + wp_cas_suc.
+        iDestruct ("Hpush" with "[HP]") as "> [HP HQ]"; auto.
+        iMod ("Hclose" with "[Hl'' Hstack HP]").
+        { iExists l'', (InjRV (v, v')), (v :: xs); iSplit; iFrame; auto.
+          iExists v'; iSplit; subst; auto. }
+        iModIntro.
+        wp_if.
+        done.
+      + wp_cas_fail.
+        iMod ("Hclose" with "[Hl'' Hstack HP]").
+        { iExists l'', v'', xs; iSplit; iFrame; auto. }
+        iModIntro.
+        wp_if.
+        iApply ("IH" with "Hpush").
+  Qed.