[vcgen] Some `Seq` tests

theories/vcgen/tests/test.v

@@ -9,6 +9,16 @@ Section tests_vcg.
   Context `{amonadG Σ}.
 
   Lemma test_seq (s l : loc) :
+    s ↦C[ULvl] #0 -∗ l ↦C[ULvl] #1 -∗
+    awp (a_bin_op PlusOp ((a_store (a_ret #l) (a_ret #2));;;;
+                           (a_bin_op PlusOp (a_ret #1) (a_store (a_ret #l) (a_ret #1))))
+                         (a_store (a_ret #s) (a_ret #4))) True (λ v, ⌜v = #6⌝ ∧ s ↦C[LLvl] #4 ∗ l ↦C[LLvl] #1).
+  Proof.
+    iIntros "Hs Hl".
+    vcg_solver. iModIntro. eauto with iFrame.
+  Qed.
+
+  Lemma test_seq2 (s l : loc) :
     s ↦C[ULvl] #0 -∗ l ↦C[ULvl] #1 -∗
     awp (a_bin_op PlusOp ((a_store (a_ret #l) (a_ret #2));;;;a_load (a_ret #l))
                          (a_store (a_ret #s) (a_ret #4))) True (λ v, ⌜v = #6⌝ ∧ s ↦C[LLvl] #4 ∗ l ↦C #2).
@@ -18,6 +28,15 @@ Section tests_vcg.
     rewrite Qp_half_half. eauto with iFrame.
   Qed.
 
+  Lemma test_seq3 (l : loc) :
+    l ↦C #0 -∗
+    awp ((a_store (a_ret #l) (a_ret #2));;;;
+                           (a_bin_op PlusOp (a_ret #1) (a_store (a_ret #l) (a_ret #1)))) True
+    (λ v, l ↦C[LLvl] #1).
+  Proof.
+    iIntros "Hl". vcg_solver. iModIntro. eauto with iFrame.
+  Qed.
+
   Lemma store_load (s l : loc) R :
     s ↦C #0 -∗ l ↦C #1 -∗
     awp (a_store (a_ret #s) (a_load (a_ret #l))) R (λ _, s ↦C[LLvl] #1 ∗ l ↦C #1).