From f873eae1b26a193e7b53c4db610357f0f8d807bc Mon Sep 17 00:00:00 2001
From: Travis Hance <tjhance7@gmail.com>
Date: Sun, 15 Sep 2024 17:14:11 -0400
Subject: [PATCH] add wp_load_shared for HeapLang

---
 .github/workflows/ci.yml                |  1 +
 _CoqProject                             |  1 +
 src/examples/heap_lang_wp_load_shared.v | 25 +++++++++++++++++++++++++
 3 files changed, 27 insertions(+)
 create mode 100644 src/examples/heap_lang_wp_load_shared.v

diff --git a/.github/workflows/ci.yml b/.github/workflows/ci.yml
index 275819b..d3b823c 100644
--- a/.github/workflows/ci.yml
+++ b/.github/workflows/ci.yml
@@ -22,6 +22,7 @@ jobs:
         opam update
         opam pin coq 8.19.1 --confirm-level=yes
         opam pin coq-iris 4.2.0 --confirm-level=yes
+        opam pin coq-iris-heap-lang 4.2.0 --confirm-level=yes
 
     - name: Run check
       run: |
diff --git a/_CoqProject b/_CoqProject
index b74b689..6440467 100644
--- a/_CoqProject
+++ b/_CoqProject
@@ -45,6 +45,7 @@ src/examples/seqs.v
 src/examples/main.v
 src/examples/fractional.v
 src/examples/counting.v
+src/examples/heap_lang_wp_load_shared.v
 
 -arg -w -arg -argument-scope-delimiter
 -arg -w -arg -notation-overridden
diff --git a/src/examples/heap_lang_wp_load_shared.v b/src/examples/heap_lang_wp_load_shared.v
new file mode 100644
index 0000000..7c05b2d
--- /dev/null
+++ b/src/examples/heap_lang_wp_load_shared.v
@@ -0,0 +1,25 @@
+From iris.prelude Require Import options.
+From iris.program_logic Require Export weakestpre.
+From iris.heap_lang Require Export lang proofmode notation.
+
+Require Import guarding.guard.
+Require Import guarding.tactics.
+
+(* Derivation for Heap-Read-Shared law for HeapLang. *)
+
+Section HeapLangWpLoadShared.
+
+  Context `{!heapGS Σ}.
+
+  Lemma wp_load_shared s E F l dq v G : (F ⊆ E) →
+    {{{ G ∗ (G &&{F}&&> l ↦{dq} v) }}} Load (Val $ LitV $ LitLoc l) @ s; E {{{ RET v; G }}}.
+  Proof.
+    intros Hfe.
+    iIntros (Φ) "[G #g] HΦ".
+    leaf_open "g" with "G" as "[Hpt Hback]". { set_solver. }
+    wp_load.
+    iMod ("Hback" with "Hpt") as "G".
+    iModIntro. iApply "HΦ". iFrame "G".
+  Qed.
+
+End HeapLangWpLoadShared.