add wp_load_shared for HeapLang

Author: tjhance

.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: |

_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

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.