Add thread ids

theories/simplang/examples/heap_test.v

@@ -17,23 +17,23 @@ Instance : sheapInv Σ := {|
 
 Definition val_rel (v1 v2 : val) : iProp Σ := (⌜v1 = v2⌝)%I.
 
-Lemma test_load l l2 :
+Lemma test_load l l2 π :
   l ↦t #4 -∗ l2 ↦s #4 -∗
-  ((! #l)%E ⪯{val_rel} ! #l2 {{ val_rel }}).
+  ((! #l)%E ⪯{π, val_rel} ! #l2 {{ val_rel }}).
 Proof.
   iIntros "H H1". target_load. source_load. sim_val. eauto.
 Qed.
 
-Lemma test_store l l2 :
+Lemma test_store l l2 π :
   l ↦t #4 -∗ l2 ↦s #4 -∗
-  ((#l <- #42)%E ⪯{val_rel} #l2 <- #1337 {{ val_rel }}).
+  ((#l <- #42)%E ⪯{π, val_rel} #l2 <- #1337 {{ val_rel }}).
 Proof.
   iIntros "H H1". target_store. source_store. sim_val. eauto.
 Qed.
 
 (* FIXME: fix precedences for ⪯ to make the parantheses unnecessary *)
-Lemma test_alloc :
-  ⊢ (Alloc #2 ;; #()) ⪯{val_rel} (Alloc #4;;#()) {{ val_rel }}.
+Lemma test_alloc π :
+  ⊢ (Alloc #2 ;; #()) ⪯{π, val_rel} (Alloc #4;;#()) {{ val_rel }}.
 Proof.
   target_alloc l1 as "H" "_".
   source_alloc l2 as "H2" "_".
@@ -43,18 +43,18 @@ Proof.
   eauto.
 Qed.
 
-Lemma test_free l l2 :
+Lemma test_free l l2 π :
   l ↦t #42 -∗ l2 ↦s #1337 -∗ l ==>t 1 -∗ l2 ==>s 1 -∗
-  Free #l ⪯{val_rel} Free #l2 {{ val_rel }}.
+  Free #l ⪯{π, val_rel} Free #l2 {{ val_rel }}.
 Proof.
   iIntros "H1 H2 H3 H4".
   target_free. source_free. sim_val. eauto.
 Qed.
 
 (* FIXME: if we remove the parantheses around the first element, parsing is broken *)
-Lemma test_freeN l l2 :
+Lemma test_freeN l l2 π :
   l ↦t∗ [(#42); #99] -∗ l2 ↦s∗ [(#1337); #420; #666] -∗ l ==>t 2 -∗ l2 ==>s 3 -∗
-  FreeN #2 #l ⪯{val_rel} FreeN #3 #l2 {{ val_rel }}.
+  FreeN #2 #l ⪯{π, val_rel} FreeN #3 #l2 {{ val_rel }}.
 Proof.
   iIntros "H1 H2 H3 H4".
   target_free; first done. source_free; first done. sim_val. eauto.
@@ -66,46 +66,46 @@ Module bij_test.
   Import heap_bij.
   Context `{sbijG Σ}.
 
-  Lemma test_load l l2 :
+  Lemma test_load l l2 π:
     l ↦t #4 -∗ l2 ↦s #4 -∗
-    ((! #l)%E ⪯{val_rel} ! #l2 {{ val_rel }}).
+    ((! #l)%E ⪯{π, val_rel} ! #l2 {{ val_rel }}).
   Proof.
     iIntros "H H1". target_load. source_load. sim_val. eauto.
   Qed.
 
-  Lemma test_store l l2 :
+  Lemma test_store l l2 π:
     l ↦t #4 -∗ l2 ↦s #4 -∗
-    ((#l <- #42)%E ⪯{val_rel} #l2 <- #1337 {{ val_rel }}).
+    ((#l <- #42)%E ⪯{π, val_rel} #l2 <- #1337 {{ val_rel }}).
   Proof.
     iIntros "H H1". target_store. source_store. sim_val. eauto.
   Qed.
 
-  Lemma test_insert l l2 :
+  Lemma test_insert l l2 π:
     l ↦t #4 -∗ l2 ↦s #4 -∗ l ==>t 1 -∗ l2 ==>s 1 -∗
-    ((#l <- #42)%E ⪯{val_rel} #l2 <- #42 {{ val_rel }}).
+    ((#l <- #42)%E ⪯{π, val_rel} #l2 <- #42 {{ val_rel }}).
   Proof.
     iIntros "H H1 H2 H3".
-    iApply (sim_bij_insert _ l l2 with "H2 H3 H H1 "); first done; iIntros "Hb".
+    iApply (sim_bij_insert _ _ l l2 with "H2 H3 H H1 "); first done; iIntros "Hb".
     iApply (sim_bij_store with "Hb []"); first done. by sim_val.
   Qed.
 
-  Lemma test_bij_store (l_t l_s : loc) :
+  Lemma test_bij_store (l_t l_s : loc) π :
     l_t ↔h l_s -∗
-    (#l_t <- #42)%E ⪯{val_rel} (#l_s <- #42)%E {{ val_rel }}.
+    (#l_t <- #42)%E ⪯{π, val_rel} (#l_s <- #42)%E {{ val_rel }}.
   Proof.
     iIntros "H". sim_store; first done. by sim_val.
   Qed.
 
-  Lemma test_bij_load (l_t l_s : loc) :
+  Lemma test_bij_load (l_t l_s : loc) π:
     l_t ↔h l_s -∗
-    ! #l_t ⪯{val_rel} ! #l_s {{ val_rel }}.
+    ! #l_t ⪯{π, val_rel} ! #l_s {{ val_rel }}.
   Proof.
     iIntros "H". sim_load v_t v_s as "Ha"; sim_val. done.
   Qed.
 
-  Lemma test_bij_free (l_t l_s : loc) :
+  Lemma test_bij_free (l_t l_s : loc) π:
     l_t ↔h l_s -∗
-    Free #l_t ⪯{val_rel} Free #l_s {{ val_rel }}.
+    Free #l_t ⪯{π, val_rel} Free #l_s {{ val_rel }}.
   Proof.
     iIntros "#H". sim_free; sim_val. done.
   Qed.