Improve notations parsing/printing, tweak some tests.

7eafceed · Robbert Krebbers · 4ac784a4 · 7eafceed · 7eafceed · 7eafceed
Commit 7eafceed authored Nov 13, 2018 by Robbert Krebbers
11 changed files
--- a/theories/c_translation/translation.v
+++ b/theories/c_translation/translation.v
@@ -13,7 +13,8 @@ Definition a_alloc : val := λ: "x1" "x2",
  let: "v" := Snd "vv" in
  assert: (#0 < "n");;
  a_atomic_env (λ: <>, SOME (ref (SOME (#true, lreplicate "n" "v")), #0)).
-Notation "'allocᶜ' ( e1 , e2 )" := (a_alloc e1%E e2%E) (at level 80) : expr_scope.
+Notation "'allocᶜ' ( e1 , e2 )" :=
+  (a_alloc e1%E e2%E) (at level 10, e1, e2 at level 99) : expr_scope.

 Definition a_free_check : val :=
  rec: "go" "env" "l" "n" :=
@@ -46,7 +47,8 @@ Definition a_free : val := λ: "x",
       end
    end
  ).
-Notation "'freeᶜ' ( e )" := (a_free e%E) (at level 80) : expr_scope.
+Notation "'freeᶜ' ( e )" :=
+  (a_free e%E) (at level 10, e at level 99) : expr_scope.

 Definition a_store : val := λ: "x1" "x2",
  "vv" ←ᶜ "x1" |||ᶜ "x2" ;;ᶜ
@@ -91,12 +93,13 @@ Definition a_seq_bind : val := λ: "x" "f",
  a_atomic_env (λ: "env", mset_clear "env") ;;ᶜ
  "f" "a".
 Notation "x ←ᶜ e1 ;ᶜ e2" :=
-  (a_seq_bind e1 (λ: x, e2))%E
-  (at level 100, e1 at next level, e2 at level 200, right associativity) : expr_scope.
+  (a_seq_bind e1%E (λ: x, e2)%E)%E
+  (at level 100, e1 at next level, e2 at level 200, right associativity,
+   format "'[' x  ←ᶜ  '[' e1 ']' ;ᶜ  '/' e2 ']'") : expr_scope.
 Notation "e1 ;ᶜ e2" :=
-  (a_seq_bind e1 (λ: <>, e2))%E
+  (a_seq_bind e1%E (λ: <>, e2)%E)%E
  (at level 100, e2 at level 200,
-   format "'[' '[hv' '[' e1 ']'  ;ᶜ  ']' '/' e2 ']'") : expr_scope.
+   format "'[' '[hv' '[' e1 ']'  ;ᶜ ']'  '/' e2 ']'") : expr_scope.

 Definition a_mut_bind : val := λ: "x" "f",
  "v" ←ᶜ "x" ;ᶜ
@@ -106,7 +109,8 @@ Definition a_mut_bind : val := λ: "x" "f",
  a_ret "b".
 Notation "x ←mutᶜ e1 ;ᶜ e2" :=
  (a_mut_bind e1 (λ: x, e2))%E
-  (at level 100, e1 at next level, e2 at level 200, right associativity) : expr_scope.
+  (at level 100, e1 at next level, e2 at level 200, right associativity,
+   format "'[' x  ←mutᶜ  '[' e1 ']' ;ᶜ  '/' e2 ']'") : expr_scope.

 Definition a_if : val := λ: "cnd" "e1" "e2",
  (* sequenced binds needed here; there should be sequence point after the conditional *)
@@ -114,27 +118,28 @@ Definition a_if : val := λ: "cnd" "e1" "e2",
  if: "c" then "e1" #() else "e2" #().
 Notation "'ifᶜ' ( cnd ) { e1 } 'elseᶜ' { e2 }" :=
  (a_if cnd%E (λ: <>, e1)%E (λ: <>, e2)%E)
-  (at level 200, cnd, e1, e2 at level 200,
-   format "'ifᶜ'  ( cnd )  {  e1  }  'elseᶜ'  {  e2  }") : expr_scope.
+  (at level 10, cnd, e1, e2 at level 99,
+   format "'[v' 'ifᶜ'  ( cnd )  {  '/  ' '[' e1 ']'  '/' }  'elseᶜ'  {  '/  ' '[' e2 ']'  '/' } ']'") : expr_scope.

 Definition a_while: val :=
  rec: "while" "cnd" "bdy" :=
    ifᶜ ("cnd" #()) { "bdy" #() ;ᶜ "while" "cnd" "bdy" }
    elseᶜ { skipᶜ }.
-Notation "'whileᶜ' ( e1 ) { e2 }" := (a_while (λ: <>, e1)%E (λ: <>, e2)%E)
-  (at level 200, e1, e2 at level 200,
-   format "'whileᶜ'  ( e1 )  {  e2  }") : expr_scope.
+Notation "'whileᶜ' ( cnd ) { e }" := (a_while (λ: <>, cnd)%E (λ: <>, e)%E)
+  (at level 10, cnd, e at level 99,
+   format "'[v' 'whileᶜ'  ( cnd )  {  '/  ' '[' e ']'  '/' } ']'") : expr_scope.
+
 (* A version of while with value lambdas, this is an artifact because of the way
 heap_lang works in Coq *)
-Notation "'whileVᶜ' ( e1 ) { e2 }" := (a_while (LamV <> e1)%V (LamV <> e2)%V)
-  (at level 200, e1, e2 at level 200,
-   format "'whileVᶜ'  ( e1 )  {  e2  }") : expr_scope.
+Notation "'whileVᶜ' ( cnd ) { e }" := (a_while (LamV <> cnd) (LamV <> e))
+  (at level 10, cnd, e at level 99,
+   format "'[v' 'whileVᶜ'  ( cnd )  {  '/  ' '[' e ']' '/'  } ']'") : expr_scope.

 Definition a_call: val := λ: "f" "arg",
  "a" ←ᶜ "arg" ;ᶜ a_atomic (λ: <>, "f" "a").
 Notation "'callᶜ' ( f , a )" :=
  (a_call f a)%E
-  (at level 100, a at level 200,
+  (at level 10, f, a at level 99,
   format "'callᶜ'  ( f ,  a )") : expr_scope.

 Definition a_un_op (op : un_op) : val := λ: "x",

--- a/theories/tests/basics.v
+++ b/theories/tests/basics.v
@@ -7,33 +7,33 @@ Section test.
  (** dereferencing *)
  Lemma test1 cl v :
    cl ↦C v -∗ AWP ∗ᶜ ♯ₗcl {{ w, ⌜w = v⌝ ∗ cl ↦C v }}.
-  Proof. iIntros "**". vcg. auto. Qed.
+  Proof. iIntros. vcg. auto. Qed.

  (** double dereferencing *)
  Lemma test2 cl1 cl2 v :
    cl1 ↦C cloc_to_val cl2 -∗ cl2 ↦C v -∗
    AWP ∗ᶜ ∗ᶜ ♯ₗcl1 {{ v, ⌜v = #1⌝ ∗ cl1 ↦C cloc_to_val cl2 -∗ cl2 ↦C v }}.
-  Proof. iIntros "**". vcg. auto. Qed.
+  Proof. iIntros. vcg. auto. Qed.

  (** sequence points *)
  Lemma test3 cl v :
    cl ↦C v -∗ AWP ∗ᶜ ♯ₗcl ;ᶜ ∗ᶜ ♯ₗcl {{ w, ⌜w = v⌝ ∗ cl ↦C v }}.
-  Proof. iIntros "**". vcg. auto. Qed.
+  Proof. iIntros. vcg. auto. Qed.

  (** assignments *)
  Lemma test4 (l : cloc) (v1 v2: val) :
    l ↦C v1 -∗ AWP ♯ₗl =ᶜ a_ret v2 {{ v, ⌜v = v2⌝ ∗ l ↦C[LLvl] v2 }}.
-  Proof. iIntros "**". vcg. auto. Qed.
+  Proof. iIntros. vcg. auto. Qed.

  Lemma store_load s l R :
    s ↦C #0 -∗ l ↦C #1 -∗
    AWP ♯ₗs =ᶜ ∗ᶜ ♯ₗl @ R {{ _, s ↦C[LLvl] #1 ∗ l ↦C #1 }}.
-  Proof. iIntros "**". vcg. auto with iFrame. Qed.
+  Proof. iIntros. vcg. auto with iFrame. Qed.

  Lemma store_load_load s1 s2 l R :
    s1 ↦C #0 -∗ l ↦C #1 -∗ s2 ↦C #0 -∗
    AWP ♯ₗs1 =ᶜ ∗ᶜ ♯ₗl ;ᶜ ∗ᶜ ♯ₗs1 +ᶜ ♯42 @ R {{ _, s1 ↦C #1 ∗ l ↦C #1 }}.
-  Proof. iIntros "**". vcg. auto with iFrame. Qed.
+  Proof. iIntros. vcg. auto with iFrame. Qed.

  (** double dereferencing & modification *)
  Lemma test5 (l1 l2 r1 r2 : cloc) (v1 v2: val) :
@@ -42,57 +42,57 @@ Section test.
    AWP ♯ₗl1 =ᶜ ♯ₗr1 ;ᶜ ∗ᶜ ∗ᶜ ♯ₗl1
    {{ w, ⌜w = v2⌝ ∗
      l1 ↦C cloc_to_val r2 ∗ l2 ↦C v1 ∗ r1 ↦C cloc_to_val r2 -∗ r2 ↦C v2 }}.
-  Proof. iIntros "**". vcg. auto with iFrame. Qed.
+  Proof. iIntros. vcg. auto with iFrame. Qed.

  (** par *)
  Lemma test_par_1 (l1 l2 : cloc) (v1 v2: val) :
    l1 ↦C v1 -∗ l2 ↦C v2 -∗
    AWP ∗ᶜ ♯ₗl1 |||ᶜ  ∗ᶜ ♯ₗl2
    {{ w, ⌜w = (v1, v2)%V⌝ ∗ l1 ↦C v1 ∗ l2 ↦C v2 }}.
-  Proof. iIntros "**". vcg. auto with iFrame. Qed.
+  Proof. iIntros. vcg. auto with iFrame. Qed.

  Lemma test_par_2 (l1 l2 : cloc) (v1 v2: val) :
    l1 ↦C v1 -∗ l2 ↦C v2 -∗
    AWP (♯ₗl1 =ᶜ a_ret v2) |||ᶜ  (♯ₗl2 =ᶜ a_ret v1)
    {{ w, ⌜w = (v2, v1)%V⌝ ∗ l1 ↦C[LLvl] v2 ∗ l2 ↦C[LLvl] v1 }}.
-  Proof. iIntros "**". vcg. auto with iFrame. Qed.
+  Proof. iIntros. vcg. auto with iFrame. Qed.

  (** pre bin op *)
  Lemma test6 (l : cloc) (z0 : Z) R:
    l ↦C #z0 -∗
    AWP ♯ₗl +=ᶜ ♯1 @ R {{ v, ⌜v = #z0⌝ ∧ l ↦C[LLvl] #(1 + z0) }}.
-  Proof. iIntros "**". vcg. eauto with iFrame. Qed.
+  Proof. iIntros. vcg. eauto with iFrame. Qed.

  Lemma test7 (l k : cloc) (z0 z1 : Z) R:
    l ↦C #z0 -∗
    k ↦C #z1 -∗
    AWP (♯ₗl +=ᶜ ♯1) +ᶜ (∗ᶜ♯ₗk) @ R
      {{ v, ⌜v = #(z0+z1)⌝ ∧ l ↦C[LLvl] #(1 + z0) ∗ k ↦C #z1 }}.
-  Proof. iIntros "**". vcg. eauto with iFrame. Qed.
+  Proof. iIntros. vcg. eauto with iFrame. Qed.

  (** more sequences *)
  Lemma test_seq s l :
    s ↦C[ULvl] #0 -∗ l ↦C[ULvl] #1 -∗
    AWP (♯ₗl =ᶜ ♯2 ;ᶜ ♯1 +ᶜ (♯ₗ l =ᶜ ♯1)) +ᶜ (♯ₗ s =ᶜ ♯4)
      {{ v, ⌜v = #6⌝ ∧ s ↦C[LLvl] #4 ∗ l ↦C[LLvl] #1 }}.
-  Proof. iIntros "**". vcg. eauto with iFrame. Qed.
+  Proof. iIntros. vcg. eauto with iFrame. Qed.

  Lemma test_seq2 s l :
    s ↦C[ULvl] #0 -∗ l ↦C[ULvl] #1 -∗
    AWP (♯ₗl =ᶜ ♯2 ;ᶜ ∗ᶜ ♯ₗl) +ᶜ (♯ₗs =ᶜ ♯4) {{ v, ⌜v = #6⌝ ∧ s ↦C[LLvl] #4 ∗ l ↦C #2 }}.
-  Proof. iIntros "**". vcg. eauto with iFrame. Qed.
+  Proof. iIntros. vcg. eauto with iFrame. Qed.

  Lemma test_seq3 l :
    l ↦C #0 -∗
    AWP ♯ₗl =ᶜ ♯2 ;ᶜ ♯1 +ᶜ (♯ₗl =ᶜ ♯1) {{ _, l ↦C[LLvl] #1 }}.
-  Proof. iIntros "**". vcg. eauto with iFrame. Qed.
+  Proof. iIntros. vcg. eauto with iFrame. Qed.

  Lemma test_seq4 l k :
    l ↦C #0 -∗
    k ↦C #0 -∗
    AWP (♯ₗl =ᶜ ♯2 ;ᶜ ♯1 +ᶜ (♯ₗl =ᶜ ♯1)) +ᶜ (♯ₗk =ᶜ ♯2 ;ᶜ ♯1 +ᶜ (♯ₗk =ᶜ ♯1))
      {{ v, ⌜v = #4⌝ ∧ l ↦C[LLvl] #1 ∗ k ↦C[LLvl] #1 }}.
-  Proof. iIntros "**". vcg. eauto with iFrame. Qed.
+  Proof. iIntros. vcg. eauto with iFrame. Qed.

  Definition stupid (l : cloc) : expr :=
    a_store (♯ₗ l) (♯ 1);ᶜ a_ret #0.
@@ -100,32 +100,32 @@ Section test.
  Lemma test_seq_fail l :
    l ↦C[ULvl] #0 -∗
    AWP ((stupid l) +ᶜ (stupid l)) +ᶜ (a_ret #0) {{ v, l ↦C #1 }}.
-  Proof. iIntros "**". vcg. Fail by eauto with iFrame. Abort.
+  Proof. iIntros. vcg. Fail by eauto with iFrame. Abort.

  Lemma test_seq5 l k :
    l ↦C #0 -∗
    k ↦C #0 -∗
    AWP ♯0 +ᶜ (♯ₗl =ᶜ ♯1 ;ᶜ ♯ₗk =ᶜ ♯2 ;ᶜ ♯0) {{ v, ⌜v = #0⌝ ∗ l ↦C #1 ∗ k ↦C #2 }}.
-  Proof. iIntros "**". vcg. eauto with iFrame. Qed.
+  Proof. iIntros. vcg. eauto with iFrame. Qed.

  Lemma test_seq6 l k :
    l ↦C #0 -∗
    k ↦C #0 -∗
    AWP ♯1 +ᶜ (♯ₗl =ᶜ ♯1 ;ᶜ (♯ₗk =ᶜ ♯2) +ᶜ ∗ᶜ ♯ₗl ;ᶜ ∗ᶜ ♯ₗk +ᶜ (♯ₗl =ᶜ ♯2))
      {{ v, ⌜v = #5⌝ ∗ l ↦C[LLvl] #2 ∗ k ↦C #2 }}.
-  Proof. iIntros "**". vcg. eauto with iFrame. Qed.
+  Proof. iIntros. vcg. eauto with iFrame. Qed.

  Lemma test_seq7 l :
    l ↦C #0 -∗
    AWP ♯1 +ᶜ (♯ₗl =ᶜ ♯1 ;ᶜ ∗ᶜ ♯ₗl +ᶜ ∗ᶜ ♯ₗl ;ᶜ ♯ₗl =ᶜ ♯2) {{ v, ⌜v = #3⌝ ∗ l ↦C[LLvl] #2 }}.
-  Proof. iIntros "**". vcg. eauto with iFrame. Qed.
+  Proof. iIntros. vcg. eauto with iFrame. Qed.

  (** while *)
  Lemma test_while l R :
    l ↦C #1 -∗
    AWP whileᶜ (∗ᶜ ♯ₗl <ᶜ ♯2) { ♯ₗl =ᶜ ♯1 } @ R {{ _, True }}.
  Proof.
-    iIntros "**". vcg. iIntros "**". iLöb as "IH".
+    iIntros. vcg. iIntros. iLöb as "IH".
    iApply a_whileV_spec; iNext.
    vcg. iIntros "Hl".
    iLeft. iSplitR; eauto. iModIntro.

--- a/theories/tests/binop.v
+++ b/theories/tests/binop.v
@@ -7,6 +7,6 @@ Section test.
    Φ (cloc_to_val (cloc_plus p n)) -∗
    p ↦C v1 -∗
    q ↦C cloc_to_val p -∗
-    AWP (∗ᶜ♯ₗq +∗ᶜ ♯n) @ R {{ v, Φ v ∗ p ↦C v1 ∗ q ↦C cloc_to_val p }}.
-  Proof. iIntros "**". vcg. eauto with iFrame. Qed.
+    AWP ∗ᶜ♯ₗq +∗ᶜ ♯n @ R {{ v, Φ v ∗ p ↦C v1 ∗ q ↦C cloc_to_val p }}.
+  Proof. iIntros. vcg. eauto with iFrame. Qed.
 End test.
--- a/theories/tests/fact.v
+++ b/theories/tests/fact.v
 From iris_c.vcgen Require Import proofmode.
-Local Open Scope Z_scope.

 Definition incr : val := λ: "l",
-  (a_ret "l") =ᶜ (∗ᶜ (a_ret "l") +ᶜ ♯1).
-
-Definition factorial_body : val := λ: "n" "c" "r",
-  whileᶜ (∗ᶜ (a_ret "c") <ᶜ (a_ret "n"))
-         { (callᶜ (incr, a_ret "c")) ;ᶜ
-           a_ret "r" =ᶜ ((∗ᶜ (a_ret "r")) *ᶜ (∗ᶜ (a_ret "c"))) }.
+  (a_ret "l") =ᶜ ∗ᶜ (a_ret "l") +ᶜ ♯1 ;ᶜ
+  ♯().

 Definition factorial : val := λ: "n",
-  "r" ←ᶜ a_alloc ♯1 ♯1;ᶜ
-  "k" ←ᶜ a_alloc ♯1 ♯0;ᶜ
-  factorial_body "n" "k" "r" ;ᶜ
+  "r" ←mutᶜ ♯1;ᶜ
+  "c" ←mutᶜ ♯0;ᶜ
+  whileᶜ (∗ᶜ (a_ret "c") <ᶜ a_ret "n") {
+    callᶜ (incr, a_ret "c");ᶜ
+    a_ret "r" =ᶜ ∗ᶜ (a_ret "r") *ᶜ ∗ᶜ (a_ret "c")
+  };ᶜ
  ∗ᶜ(a_ret "r").

 Section factorial_spec.
  Context `{amonadG Σ}.

-  Lemma incr_spec (l : cloc) (n : Z) R Φ :
-    l ↦C #n -∗ (l ↦C[LLvl] #(n+1) -∗ Φ #(n+1)) -∗
+  Lemma incr_spec l (n : Z) R Φ :
+    l ↦C #n -∗ (l ↦C #(1 + n) -∗ Φ #()) -∗
    AWP incr (cloc_to_val l) @ R {{ Φ }}.
-  Proof.
-    iIntros "Hl HΦ". awp_lam. vcg.
-    rewrite !Z.add_0_l Z.add_comm. eauto.
-  Qed.
-
-  Lemma factorial_body_spec (n k : nat) (c r: cloc) R :
-    (⌜k ≤ n⌝ ∧ c ↦C[ULvl] #k ∗ r ↦C #(fact k)) -∗
-    AWP factorial_body #n (cloc_to_val c) (cloc_to_val r) @ R
-        {{ _, c ↦C #n ∗ r ↦C #(fact n) }}.
-  Proof.
-    iIntros "(Hk & Hc & Hr)". awp_lam. awp_pures.
-    iLöb as "IH" forall (n k) "Hk Hc Hr". iApply a_whileV_spec. iNext.
-    vcg. iIntros "Hr Hc".
-    case_bool_decide.
-    + iLeft. iSplit; eauto.
-      iModIntro. vcg.
-      iIntros "Hc Hr". iIntros "!> HR". iExists R. iFrame.
-      iApply (incr_spec with "Hc"). iIntros "Hc $".
-      vcg_continue. iIntros "Hc Hr".
-      iModIntro.
-      assert ((fact k) * (S k) = fact (S k)) as ->.
-      { rewrite /fact. lia. }
-      iApply ("IH" $! n (S k) with "[] Hc Hr").
-      { iPureIntro. lia. }
-    + iRight. iSplit; eauto.  iModIntro.
-      iDestruct "Hk" as %Hk.
-      assert (k = n) as -> by lia. by iFrame.
-  Qed.
+  Proof. iIntros "**". awp_lam. vcg. eauto. Qed.

  Lemma factorial_spec (n: nat) R :
    AWP factorial #n @ R {{ v, ⌜v = #(fact n)⌝ }}%I.
  Proof.
-    awp_lam. vcg.
-    iIntros (r) "? ?".
-    iIntros (c) "? ?".
-    iIntros "Hr Hc".
-    iApply (awp_wand _ (λ _, c ↦C #n ∗ r ↦C #(fact n))%I with "[Hr Hc]").
-    - iApply ((factorial_body_spec n 0 c r) with "[$Hr $Hc]"); eauto with lia.
-    - iIntros (?) "[Hc Hr]". vcg_continue. eauto with iFrame.
+    awp_lam. vcg. iIntros (r c) "**".
+    iApply (awp_wand _ (λ _, c ↦C #n ∗ r ↦C #(fact n))%I with "[-]"); last first.
+    { iIntros (?) "[Hc Hr]". vcg_continue. eauto with iFrame. }
+    iAssert (∃ k : nat, ⌜k ≤ n⌝ ∧ c ↦C #k ∗ r ↦C #(fact k))%I with "[-]" as (k Hk) "[??]".
+    { iExists 0%nat. eauto with lia iFrame. }
+    iLöb as "IH" forall (n k Hk). iApply a_whileV_spec; iNext.
+    vcg. iIntros "**". case_bool_decide.
+    + iLeft. iSplit; eauto. iModIntro. vcg.
+      iIntros "Hc Hr !> HR". iExists R. iFrame "HR".
+      iApply (incr_spec with "Hc"); iIntros "Hc $".
+      vcg_continue. iIntros "Hc Hr !>".
+      assert (fact k * S k = fact (S k)) as -> by (simpl; lia).
+      iApply ("IH" $! n (S k) with "[%] Hc Hr"). lia.
+    + iRight. iSplit; eauto. iModIntro.
+      assert (k = n) as -> by lia. by iFrame.
  Qed.
-
 End factorial_spec.
--- a/theories/tests/gcd.v
+++ b/theories/tests/gcd.v
 From iris_c.vcgen Require Import proofmode.
-Local Open Scope Z_scope.

-(* TODO: Notation, get rid of parenthesis around the while loop *)
 Definition gcd : val := λ: "x",
-   "a" ←ᶜ a_ret (Fst "x");ᶜ
-   "b" ←ᶜ a_ret (Snd "x");ᶜ
-   (whileᶜ (∗ᶜ(a_ret "a") !=ᶜ ∗ᶜ(a_ret "b")) {
-     ifᶜ (∗ᶜ(a_ret "a") <ᶜ ∗ᶜ(a_ret "b")) {
-       (a_ret "b") =ᶜ ∗ᶜ(a_ret "b") -ᶜ ∗ᶜ(a_ret "a")
-     } elseᶜ {
-       (a_ret "a") =ᶜ ∗ᶜ(a_ret "a") -ᶜ ∗ᶜ(a_ret "b")
-     }
-   }) ;ᶜ
-   ∗ᶜ(a_ret "a").
+  "a" ←ᶜ a_ret (Fst "x");ᶜ
+  "b" ←ᶜ a_ret (Snd "x");ᶜ
+  whileᶜ(∗ᶜ(a_ret "a") !=ᶜ ∗ᶜ(a_ret "b")) {
+    ifᶜ (∗ᶜ(a_ret "a") <ᶜ ∗ᶜ(a_ret "b")) {
+      (a_ret "b") =ᶜ ∗ᶜ(a_ret "b") -ᶜ ∗ᶜ(a_ret "a")
+    } elseᶜ {
+      (a_ret "a") =ᶜ ∗ᶜ(a_ret "a") -ᶜ ∗ᶜ(a_ret "b")
+    }
+  };ᶜ ∗ᶜ(a_ret "a").

 Section gcd_spec.
  Context `{amonadG Σ}.

-  Lemma gcd_spec (a b : Z) (l r: cloc) R :
+  Lemma gcd_spec l r a b R :
    0 ≤ a → 0 ≤ b →
    l ↦C #a -∗ r ↦C #b -∗
-    awp (gcd (cloc_to_val l, cloc_to_val r)%V) R (λ v, ⌜v = #(Z.gcd a b)⌝).
+    AWP gcd (cloc_to_val l, cloc_to_val r)%V @ R {{ v, ⌜v = #(Z.gcd a b)⌝ }}.
  Proof.
-    iIntros (??) "Hl Hr". unfold gcd.  awp_lam.
-    vcg. iIntros "Hl Hr".
+    iIntros (??) "**". awp_lam. vcg; iIntros.
    iApply (a_whileV_inv_spec (∃ x y : Z,
-      ⌜0 ≤ x ∧ 0 ≤ y ∧ Z.gcd x y = Z.gcd a b⌝ ∧ l ↦C #x ∗ r ↦C #y)%I with "[Hl Hr]").
-    - iExists a, b. eauto with iFrame.
-    - iModIntro.  iDestruct 1 as (x y (?&?&Hgcd)) "[Hl Hr]".
-      vcg.
-      iIntros "Hr Hl /=".
+      ⌜0 ≤ x ∧ 0 ≤ y ∧ Z.gcd x y = Z.gcd a b⌝ ∧ l ↦C #x ∗ r ↦C #y)%I with "[-]").
+    { iExists a, b. eauto with iFrame. }
+    iModIntro. iDestruct 1 as (x y (?&?&Hgcd)) "[??]". vcg. iIntros "** /=".
+    case_bool_decide; simpl; [iLeft | iRight]; iSplit; eauto.
+    + repeat iModIntro. vcg_continue. simplify_eq/=.
+      rewrite -Hgcd Z.gcd_diag Z.abs_eq; eauto with iFrame.
+    + iModIntro. iApply a_if_spec. vcg. iIntros "** /=".
      case_bool_decide; simpl; [ iLeft | iRight ];
-        iSplit; eauto.
-      + repeat iModIntro. vcg_continue. simplify_eq/=.
-        rewrite -Hgcd Z.gcd_diag Z.abs_eq; eauto with iFrame.
-      + iModIntro.
-        iApply a_if_spec. vcg.
-        iIntros "Hl Hr /=".
-        case_bool_decide; simpl; [ iLeft | iRight ];
-          (iSplit; first done); iModIntro.
-        * vcg. iIntros "Hl Hr". iModIntro. iExists x, (y - x); iFrame.
-          iPureIntro. rewrite Z.gcd_sub_diag_r. lia.
-        * vcg. iIntros "Hl Hr". iModIntro. iExists (x-y), y; iFrame.
-          iPureIntro. rewrite Z.gcd_comm Z.gcd_sub_diag_r Z.gcd_comm. lia.
+        (iSplit; first done); iModIntro.
+      * vcg. iIntros "** !>". iExists x, (y - x); iFrame.
+        iPureIntro. rewrite Z.gcd_sub_diag_r. lia.
+      * vcg. iIntros "** !>". iExists (x-y), y; iFrame.
+        iPureIntro. rewrite Z.gcd_comm Z.gcd_sub_diag_r Z.gcd_comm. lia.
  Qed.
 End gcd_spec.
--- a/theories/tests/invoke.v
+++ b/theories/tests/invoke.v
@@ -4,39 +4,34 @@ From iris_c.vcgen Require Import proofmode.
 Section tests_vcg.
  Context `{amonadG Σ}.

-  Definition c_id : val := λ: "v", a_ret ("v").
+  Definition c_id : val := λ: "v", a_ret "v".

  Lemma test_invoke_1 (l: cloc)  R :
    l ↦C #42 -∗
      AWP callᶜ (c_id, ∗ᶜ ♯ₗl) @ R {{ v, ⌜v = #42⌝ ∗  l ↦C #42 }}%I.
  Proof.
-    iIntros "Hl". vcg.
-    iIntros "Hl". iModIntro. iIntros "HR". iExists R. iFrame.
-    awp_lam. vcg. iIntros "Hl $".
-    vcg_continue. eauto.
+    iIntros "Hl". vcg. iIntros "Hl !> HR". iExists R. iFrame.
+    awp_lam. vcg. iIntros "Hl $". vcg_continue. eauto.
  Qed.

  Definition plus_pair : val := λ: "vv",
-    let: "v1" := Fst "vv" in
-    let: "v2" := Snd "vv" in
+    "v1" ←ᶜ a_ret (Fst "vv");ᶜ
+    "v2" ←ᶜ a_ret (Snd "vv");ᶜ
    (a_ret "v1") +ᶜ (a_ret "v2").

  Lemma test_invoke_2 R :
    AWP callᶜ (plus_pair, ♯21 |||ᶜ ♯21) @ R {{ v, ⌜v = #42⌝ }}%I.
  Proof.
-    iIntros. vcg. iModIntro. iIntros "HR". iExists R. iFrame.
-    awp_lam. awp_pures. vcg.
-    iIntros "$". vcg_continue. done.
+    iIntros. vcg. iIntros "!> HR". iExists R. iFrame. awp_lam. vcg.
+    iIntros "$". by vcg_continue.
  Qed.

  Lemma test_invoke_3 (l : cloc) R :
    l ↦C #21 -∗
-      AWP callᶜ (plus_pair, (∗ᶜ ♯ₗl |||ᶜ ∗ᶜ ♯ₗl)) @ R
-        {{ v, ⌜v = #42⌝ ∗  l ↦C #21 }}%I.
+    AWP callᶜ (plus_pair, (∗ᶜ ♯ₗl |||ᶜ ∗ᶜ ♯ₗl)) @ R
+      {{ v, ⌜v = #42⌝ ∗  l ↦C #21 }}%I.
  Proof.
-    iIntros. vcg. iIntros "Hl".
-    iModIntro. iIntros "HR". iExists R. iFrame.
-    awp_lam. awp_pures. vcg.
-    iIntros "Hl $". vcg_continue. eauto.
+    iIntros. vcg. iIntros "Hl !> HR". iExists R. iFrame. awp_lam. vcg.
+    iIntros "Hl $". vcg_continue; eauto.
  Qed.
 End tests_vcg.
--- a/theories/tests/lists.v
+++ b/theories/tests/lists.v
+(** TODO: this file should be updated to not break the C-language abstraction *)
 From iris_c.vcgen Require Import proofmode.

 Definition a_list_nil : val := λ:<>, a_ret NONEV.

--- a/theories/tests/memcpy.v
+++ b/theories/tests/memcpy.v
@@ -14,13 +14,13 @@ Lemma memcpy_spec `{amonadG Σ} lxs lys xs ys n R :
  lxs ↦C∗ xs -∗ lys ↦C∗ ys -∗
  AWP memcpy (cloc_to_val lxs, (cloc_to_val lys, #n))%V @ R {{ _, lxs ↦C∗ ys ∗ lys ↦C∗ ys }}.
 Proof.
-  iIntros (Hlen <-) "Hxs Hys". awp_lam. vcg. iIntros (p q) "Hp Hq".
+  iIntros (Hlen <-) "**". awp_lam. vcg. iIntros (p q) "**".
  iApply (awp_wand _ (λ _, ∃ p' q', p ↦C p' ∗ q ↦C q' ∗
    lxs ↦C∗ ys ∗ lys ↦C∗ ys)%I with "[-]"); last first.
  { iIntros (v). iDestruct 1 as (p' q') "[??]". by vcg_continue. }
  iInduction xs as [|x xs] "IH" forall (lxs lys ys Hlen);
    destruct ys as [|y ys]; simplify_eq/=; first by vcg; eauto 10 with iFrame.
-  vcg; iIntros "!> !> !> Hx Hy Hp Hq".
+  vcg; iIntros "!> !> !> **".
  iSpecialize ("IH" $! (lxs +∗ 1) (lys +∗ 1) with "[//] [$] [$] [$] [$]").
  rewrite !cloc_plus_plus -(Nat2Z.inj_add 1).
  iApply (awp_wand with "IH").

--- a/theories/tests/swap.v
+++ b/theories/tests/swap.v
@@ -14,13 +14,9 @@ Section tests_vcg.

  Lemma swap_spec (l1 l2 r : cloc) (v1 v2: val) R :
    r ↦C #0 -∗ l1 ↦C v1 ∗ l2 ↦C v2 -∗
-    AWP swap (cloc_to_val l1, (cloc_to_val l2, cloc_to_val r)) @ R
+    AWP swap (cloc_to_val l1, (cloc_to_val l2, cloc_to_val r))%V @ R
      {{ _, l2 ↦C v1 ∗ l1 ↦C v2 }}.
-  Proof.
-    iIntros "Hr [Hl1 Hl2]".
-    awp_pures. awp_lam.
-    vcg. eauto with iFrame.
-  Qed.
+  Proof. iIntros. awp_lam. vcg. eauto with iFrame. Qed.

  Definition swap_with_alloc : val := λ: "a",
    "l1" ←ᶜ a_ret (Fst "a");ᶜ
@@ -31,13 +27,8 @@ Section tests_vcg.
    (a_ret "l2") =ᶜ ∗ᶜ (a_ret "r") ;ᶜ
    ♯().

-  Lemma swap_with_alloc_spec (l1 l2 : cloc) (v1 v2: val) R :
+  Lemma swap_with_alloc_spec l1 l2 v1 v2 R :
    l1 ↦C v1 -∗ l2 ↦C v2 -∗
-    AWP swap_with_alloc (cloc_to_val l1, cloc_to_val l2) @ R {{ _, l1 ↦C v2 ∗ l2 ↦C v1 }}.
-  Proof.
-    iIntros "Hl1 Hl2".
-    awp_pures. awp_lam. vcg.
-    iIntros (l3) "? l1 l2 l3". eauto with iFrame.
-  Qed.
+    AWP swap_with_alloc (cloc_to_val l1, cloc_to_val l2)%V @ R {{ _, l1 ↦C v2 ∗ l2 ↦C v1 }}.
+  Proof. iIntros. awp_lam. vcg. eauto with iFrame. Qed.
 End tests_vcg.
-
--- a/theories/tests/unknowns.v
+++ b/theories/tests/unknowns.v
 (** Testing vcgen on expressions contaning unknown subexpressions *)
 From iris_c.vcgen Require Import proofmode.
-Local Open Scope Z_scope.

 Section tests_vcg.
  Context `{amonadG Σ}.

-  Lemma test1 (l k : cloc) (e: expr) :
+  Lemma test1 l k e :
    □ (∀ Φ v, k ↦C v -∗ (k ↦C #12 -∗ Φ v) -∗ awp e True Φ) -∗
    l ↦C #1 -∗
    k ↦C #10 -∗
-    AWP
-    ♯ₗl =ᶜ ♯2 +ᶜ e ;ᶜ
-    ♯ₗl =ᶜ e
-    {{ _, True }}.
+    AWP ♯ₗl =ᶜ ♯2 +ᶜ e ;ᶜ ♯ₗl =ᶜ e {{ _, True }}.
  Proof.
    iIntros "#He Hl Hk". vcg.
    iIntros "Hl Hk".
@@ -35,29 +31,27 @@ Section tests_vcg.
     implementation-defined behaviour *)
  Lemma test3 (n : nat) (m : Z) :
    1 ≤ n →
-    (AWP ∗ᶜ(allocᶜ (♯n,♯m)) {{ v, ⌜v = #m⌝ }})%I.
+    AWP ∗ᶜ(allocᶜ (♯n,♯m)) {{ v, ⌜v = #m⌝ }}%I.
  Proof.
-    intros ?. iStartProof.
-    vcg. iExists (n). repeat iSplit; eauto.
+    intros. vcg. iExists (n). repeat iSplit; eauto.
    { iPureIntro. lia. }
    iIntros (l) "? Hl". assert (∃ m, n = S m) as [k ->]. exists (pred n). lia.
    iDestruct "Hl" as "[Hl Hls]". (* TODO: this looks ridiculous *)
    vcg_continue. eauto 42 with iFrame.
  Qed.

-  Lemma test3_NOMATCH (n : Z) (m : Z) :
+  Lemma test3_NOMATCH (n m : Z) :
    1 ≤ n →
-    (AWP ∗ᶜ(allocᶜ (♯n,♯m)) {{ v, ⌜v = #m⌝ }})%I.
+    AWP ∗ᶜ(allocᶜ (♯n,♯m)) {{ v, ⌜v = #m⌝ }}%I.
  Proof.
-    intros ?. iStartProof.
-    vcg.
+    intros. vcg.
    match goal with
    | [ |- environments.envs_entails _
      (∃ n0 : nat, _)%I] => idtac
    end.
  Abort.

-  Lemma test6 (l k : cloc) (e1 e2 : expr) :
+  Lemma test6 l k e1 e2 :
    (∀ Φ, Φ #11 -∗ awp e1 True Φ) -∗
    (∀ Φ, Φ #12 -∗ awp e2 True Φ) -∗
    l ↦C #1 -∗

--- a/theories/vcgen/proofmode.v
+++ b/theories/vcgen/proofmode.v
@@ -112,12 +112,14 @@ End tactics.
 Arguments vcg_wp_continuation {_ _ _ _}.