Improve notations.

_CoqProject

@@ -8,7 +8,6 @@ theories/lib/U.v
 theories/c_translation/monad.v
 theories/c_translation/proofmode.v
 theories/c_translation/translation.v
-theories/c_translation/notation.v
 theories/c_translation/derived.v
 theories/vcgen/dcexpr.v
 theories/vcgen/denv.v

theories/c_translation/monad.v

@@ -13,7 +13,11 @@ Definition a_bind : val := λ: "f" "x" "env" "l",
   let: "a" := "x" "env" "l" in
   "f" "a" "env" "l".
 
-Notation "a ;;; b" := (a_bind (λ: <>, b) a)%E (at level 80, right associativity).
+Notation "x ←ᶜ y ;;ᶜ z" :=
+  (a_bind (λ: x, z) y)%E
+  (at level 100, y at next level, z at level 200, right associativity) : expr_scope.
+Notation "x ;;ᶜ z" := (a_bind (λ: <>, z) x)%E
+  (at level 100, z at level 200, right associativity) : expr_scope.
 
 (* M A → A *)
 Definition a_run : val := λ: "x",
@@ -39,6 +43,7 @@ Definition a_atomic_env : val := λ: "f" "env" "l",
 (* M A → M B → M (A * B) *)
 Definition a_par : val := λ: "x" "y" "env" "l",
   "x" "env" "l" ||| "y" "env" "l".
+Notation "e1 |||ᶜ e2" := (a_par e1 e2)%E (at level 50) : expr_scope.
 
 Definition amonadN := nroot .@ "amonad".
 
@@ -82,15 +87,15 @@ Section a_wp.
   Qed.
 End a_wp.
 
-Notation "'AWP' e @ R {{ Φ } }" := (awp e%E R Φ)
+Notation "'AWP' e @ R {{ Φ } }" := (awp e%E R%I Φ)
   (at level 20, e, Φ at level 200, only parsing) : bi_scope.
-Notation "'AWP' e {{ Φ } }" := (awp e%E True Φ)
+Notation "'AWP' e {{ Φ } }" := (awp e%E True%I Φ)
   (at level 20, e, Φ at level 200, only parsing) : bi_scope.
 
-Notation "'AWP' e @ R {{ v , Q } }" := (awp e%E R (λ v, Q))
+Notation "'AWP' e @ R {{ v , Q } }" := (awp e%E R%I (λ v, Q))
   (at level 20, e, Q at level 200,
    format "'[' 'AWP'  e  '/' '[          ' @  R  {{  v ,  Q  } } ']' ']'") : bi_scope.
-Notation "'AWP' e {{ v , Q } }" := (awp e%E True (λ v, Q))
+Notation "'AWP' e {{ v , Q } }" := (awp e%E True%I (λ v, Q))
   (at level 20, e, Q at level 200,
    format "'[' 'AWP'  e  '/' '[   ' {{  v ,  Q  } } ']' ']'") : bi_scope.
 

theories/c_translation/notation.v

-From iris.program_logic Require Import language.
-From iris.heap_lang Require Export lang notation.
-From iris_c.c_translation Require Import monad translation.
-Set Default Proof Using "Type".
-
-Definition ret (v: val) : expr := a_ret v.
-
-Notation "♯ l" := (a_ret (LitV l%Z%V)) (at level 8, format "♯ l").
-Notation "♯ l" := (a_ret (Lit l%Z%V)) (at level 8, format "♯ l") : expr_scope.
-
-Notation "∗ᶜ e" :=
-  (a_load e%E) (at level 9, right associativity) : expr_scope.
-
-Notation "e1 ;ᶜ e2" := (e1%E ;;;; e2%E)
-  (at level 100, e2 at level 200,
-   format "'[' '[hv' '[' e1 ']'  ;ᶜ  ']' '/' e2 ']'") : expr_scope.
-
-
-Notation "e1 +ᶜ e2" := (a_bin_op PlusOp e1%E e2%E) (at level 80) : expr_scope.
-Notation "e1 -ᶜ e2" := (a_bin_op MinusOp e1%E e2%E) (at level 80) : expr_scope.
-Notation "e1 *ᶜ e2" := (a_bin_op MultOp e1%E e2%E) (at level 80) : expr_scope.
-Notation "e1 ≤ᶜ e2" := (a_bin_op LeOp e1%E e2%E) (at level 80) : expr_scope.
-Notation "e1 <ᶜ e2" := (a_bin_op LtOp e1%E e2%E) (at level 80) : expr_scope.
-Notation "e1 ==ᶜ e2" := (a_bin_op EqOp e1%E e2%E) (at level 80) : expr_scope.
-Notation "e1 !=ᶜ e2" := (a_un_op NegOp (a_bin_op EqOp e1%E e2%E)) (at level 80): expr_scope.
-Notation "~ᶜ e" := (a_un_op NegOp e%E) (at level 75, right associativity) : expr_scope.
-
-Notation "'allocᶜ' e1" := (a_alloc e1%E) (at level 80) : expr_scope.
-Notation "e1 =ᶜ e2" := (a_store e1%E e2%E) (at level 80) : expr_scope.
-
-Notation "'ifᶜ' ( e1 ) { e2 } 'elseᶜ' { e3 }" :=
-  (a_if e1%E (λ:<>, e2)%E (λ:<>, e3)%E)
-  (at level 200, e1, e2, e3 at level 200, only parsing) : expr_scope.
-
-Notation "'whileᶜ' ( e1 ) { e2 } " := (a_while (λ:<>, e1)%E (λ:<>, e2)%E)
-  (at level 200, e1, e2 at level 200, only parsing) : expr_scope.

theories/c_translation/translation.v

@@ -4,33 +4,47 @@ From iris.algebra Require Import frac auth.
 From iris_c.lib Require Import locking_heap mset flock U.
 From iris_c.c_translation Require Import proofmode.
 
+Notation "♯ l" := (a_ret (LitV l%Z%V)) (at level 8, format "♯ l").
+Notation "♯ l" := (a_ret (Lit l%Z%V)) (at level 8, format "♯ l") : expr_scope.
+
 Definition a_alloc : val := λ: "x",
-  a_bind (λ: "v", a_atomic_env (λ: <>, ref "v")) "x".
+  "v" ←ᶜ "x" ;;ᶜ
+  a_atomic_env (λ: <>, ref "v").
+Notation "'allocᶜ' e1" := (a_alloc e1%E) (at level 80) : expr_scope.
 
 Definition a_store : val := λ: "x1" "x2",
-  a_bind (λ: "vv",
-    a_atomic_env (λ: "env",
-      mset_add (Fst "vv") "env" ;;
-      Fst "vv" <- Snd "vv" ;;
-      Snd "vv"
-    )
-  ) (a_par "x1" "x2").
+  "vv" ←ᶜ "x1" |||ᶜ "x2" ;;ᶜ
+  a_atomic_env (λ: "env",
+    mset_add (Fst "vv") "env" ;;
+    Fst "vv" <- Snd "vv" ;;
+    Snd "vv"
+  ).
+Notation "e1 =ᶜ e2" := (a_store e1%E e2%E) (at level 80) : expr_scope.
 
 Definition a_load : val := λ: "x",
-  a_bind (λ: "v",
-    a_atomic_env (λ: "env",
-      assert: (mset_member "v" "env" = #false);;
-      !"v"
-    )
-  ) "x".
+  "v" ←ᶜ "x";;ᶜ
+  a_atomic_env (λ: "env",
+    assert: (mset_member "v" "env" = #false);;
+    !"v"
+  ).
+Notation "∗ᶜ e" :=
+  (a_load e)%E (at level 9, right associativity) : expr_scope.
 
 Definition a_un_op (op : un_op) : val := λ: "x",
-  a_bind (λ: "v", a_ret (UnOp op "v")) "x".
+  "v" ←ᶜ "x" ;;ᶜ
+  a_ret (UnOp op "v").
 
 Definition a_bin_op (op : bin_op) : val := λ: "x1" "x2",
-  a_bind (λ: "vv",
-    a_ret (BinOp op (Fst "vv") (Snd "vv"))
-  ) (a_par "x1" "x2").
+  "vv" ←ᶜ "x1" |||ᶜ "x2" ;;ᶜ
+  a_ret (BinOp op (Fst "vv") (Snd "vv")).
+Notation "e1 +ᶜ e2" := (a_bin_op PlusOp e1%E e2%E) (at level 80) : expr_scope.
+Notation "e1 -ᶜ e2" := (a_bin_op MinusOp e1%E e2%E) (at level 80) : expr_scope.
+Notation "e1 *ᶜ e2" := (a_bin_op MultOp e1%E e2%E) (at level 80) : expr_scope.
+Notation "e1 ≤ᶜ e2" := (a_bin_op LeOp e1%E e2%E) (at level 80) : expr_scope.
+Notation "e1 <ᶜ e2" := (a_bin_op LtOp e1%E e2%E) (at level 80) : expr_scope.
+Notation "e1 ==ᶜ e2" := (a_bin_op EqOp e1%E e2%E) (at level 80) : expr_scope.
+Notation "e1 !=ᶜ e2" := (a_un_op NegOp (a_bin_op EqOp e1%E e2%E)) (at level 80): expr_scope.
+Notation "~ᶜ e" := (a_un_op NegOp e%E) (at level 75, right associativity) : expr_scope.
 
 (* M () *)
 (* The eta expansion is used to turn it into a value *)
@@ -38,17 +52,28 @@ Definition a_seq : val := λ: <>,
   a_atomic_env (λ: "env", mset_clear "env").
 
 Definition a_seq_bind : val := λ: "f" "x",
-  a_bind (λ: "a", a_seq #();;; "f" "a") "x".
-
-Notation "e1 ;;;; e2" :=
-  (a_seq_bind (λ: <>, e2) e1)%E (at level 80, right associativity).
+  "a" ←ᶜ "x" ;;ᶜ
+  a_seq #() ;;ᶜ
+  "f" "a".
+Notation "e1 ;ᶜ e2" :=
+  (a_seq_bind (λ: <>, e2) e1)%E
+  (at level 100, e2 at level 200,
+   format "'[' '[hv' '[' e1 ']'  ;ᶜ  ']' '/' e2 ']'") : expr_scope.
 
 Definition a_if : val := λ: "cnd" "e1" "e2",
-  a_bind (λ: "c", if: "c" then "e1" #() else "e2" #()) "cnd".
+  "c" ←ᶜ "cnd" ;;ᶜ
+  if: "c" then "e1" #() else "e2" #().
+Notation "'ifᶜ' ( e1 ) { e2 } 'elseᶜ' { e3 }" :=
+  (a_if e1%E (λ:<>, e2)%E (λ:<>, e3)%E)
+  (at level 200, e1, e2, e3 at level 200,
+   format "'ifᶜ'  ( e1 )  {  e2  }  'elseᶜ'  {  e3  }") : expr_scope.
 
 Definition a_while: val :=
   rec: "while" "cnd" "bdy" :=
-    a_if ("cnd" #()) (λ:<>, "bdy" #() ;;;; "while" "cnd" "bdy") a_seq%E.
+    a_if ("cnd" #()) (λ: <>, "bdy" #() ;ᶜ "while" "cnd" "bdy") a_seq%E.
+Notation "'whileᶜ' ( e1 ) { e2 }" := (a_while (λ:<>, e1)%E (λ:<>, e2)%E)
+  (at level 200, e1, e2 at level 200,
+   format "'whileᶜ'  ( e1 )  {  e2  }") : expr_scope.
 
 Definition a_invoke: val := λ: "f" "arg",
   a_seq_bind (λ: "a", a_atomic (λ: <>, "f" "a")) "arg".
@@ -259,10 +284,8 @@ Section proofs.
   Qed.
 
   Lemma a_while_spec  R Φ (c b: expr) `{Closed [] c} `{Closed [] b} :
-    ▷ awp  (a_if c
-                 (λ:<>, (λ:<>, b) #() ;;;; a_while (λ:<>, c) (λ:<>, b))
-                 a_seq)%E R Φ -∗
-    awp (a_while (λ:<>, c) (λ:<>, b))%E R Φ.
+    ▷ AWP a_if c (λ: <>, (λ: <>, b) #() ;ᶜ whileᶜ (c) { b }) a_seq @ R {{ Φ }} -∗
+    AWP whileᶜ (c) { b } @ R {{ Φ }}.
   Proof.
     iIntros "H".
     awp_lam. awp_lam. awp_seq.
@@ -270,8 +293,8 @@ Section proofs.
   Qed.
 
   Lemma a_if_spec R Φ (e e1 e2 : expr) `{Closed [] e1} `{Closed [] e2} :
-    AsVal e1 ->
-    AsVal e2 ->
+    AsVal e1 →
+    AsVal e2 →
     awp e R (λ v, (⌜v = #true⌝ ∧ awp (e1 #()) R Φ) ∨
                   (⌜v = #false⌝ ∧ awp (e2 #()) R Φ)) -∗
     awp (a_if e e1 e2) R Φ.
@@ -369,4 +392,3 @@ End proofs.
 (* Make sure that we only use the provided rules and don't break the abstraction *)
 Typeclasses Opaque a_alloc a_store a_load a_un_op a_bin_op a_seq a_seq_bind a_if a_while a_invoke.
 Opaque a_alloc a_store a_load a_un_op a_bin_op a_seq a_seq_bind a_if a_while a_invoke a_ret.
-

theories/tests/fact.v

@@ -10,14 +10,14 @@ Definition incr : val := λ: "l",
 Definition factorial_body : val := λ: "n" "c" "r",
   a_while
       (λ:<>, a_bin_op LtOp (a_load (a_ret "c")) (a_ret "n"))
-      (λ:<>, incr "c" ;;;;
+      (λ:<>, incr "c" ;ᶜ
              a_store (a_ret "r")
              (a_bin_op MultOp (a_load (a_ret "r")) (a_load (a_ret "c")))).
 
 Definition factorial : val := λ: "n",
   a_bind ( λ: "r",
      a_bind (λ: "k",
-       factorial_body "n" "k" "r" ;;;;
+       factorial_body "n" "k" "r" ;ᶜ
          (a_load (a_ret "r")))
       (a_alloc (a_ret #0%V)))
          (a_alloc (a_ret #1%V)).

theories/tests/gcd.v

@@ -14,7 +14,7 @@ Definition gcd : val := λ: "a" "b",
              ((a_bin_op MinusOp (a_load (a_ret "b")) (a_load (a_ret "a")))))
             (λ:<>, a_store (a_ret "a")
              ((a_bin_op MinusOp (a_load (a_ret "a")) (a_load (a_ret "b")))))))
-     ;;;; a_load (a_ret "a").
+     ;ᶜ a_load (a_ret "a").
 
 Section gcd_spec.
   Context `{amonadG Σ}.

theories/tests/lists.v

@@ -47,10 +47,10 @@ Definition in_place_reverse : val := λ: "hd",
     a_while
       (λ:<>, a_un_op NegOp (a_bin_op EqOp (a_load (a_ret "i")) (a_ret NONEV)))
       (λ:<>, a_bind (λ: "k",
-               a_list_store_next (a_load (a_ret "i")) (a_load (a_ret "j")) ;;;;
-               a_store (a_ret "j") (a_load (a_ret "i"))  ;;;;
+               a_list_store_next (a_load (a_ret "i")) (a_load (a_ret "j")) ;ᶜ
+               a_store (a_ret "j") (a_load (a_ret "i"))  ;ᶜ
                a_store (a_ret "i") (a_load (a_ret "k")))
-             (a_alloc (a_list_next (a_load (a_ret "i"))))) ;;;;
+             (a_alloc (a_list_next (a_load (a_ret "i"))))) ;ᶜ
     (a_load (a_ret "j"))
   ) (a_alloc (a_ret NONEV))) (a_alloc (a_ret "hd")).
 

theories/tests/test1.v

@@ -9,7 +9,7 @@ Section test.
 
   Lemma test1 (l : loc) :
     l ↦C[LLvl]{1/2} #1 -∗ l ↦C[LLvl]{1/2} #1 -∗
-    awp (a_seq #();;; a_load (a_ret #l)) True (λ v, ⌜v = #1⌝ ∗ l ↦C #1).
+    awp (a_seq #();;ᶜ a_load (a_ret #l)) True (λ v, ⌜v = #1⌝ ∗ l ↦C #1).
   Proof.
     iIntros "Hl1 Hl2". iCombine "Hl1 Hl2" as "Hl".
     rewrite Qp_half_half.
@@ -22,7 +22,7 @@ Section test.
 
   Lemma test2 (l r : loc) R :
     l ↦C #3 -∗ r ↦C #0 -∗
-    awp (a_store (a_ret #l) (a_ret #1);;; a_seq #();;; a_load (a_ret #l)) R (λ v, ⌜v = #1⌝).
+    awp (a_store (a_ret #l) (a_ret #1);;ᶜ a_seq #();;ᶜ a_load (a_ret #l)) R (λ v, ⌜v = #1⌝).
   Proof.
     iIntros "Hl Hr".
     iApply awp_bind.
@@ -37,9 +37,9 @@ Section test.
 
   Definition swap : val := λ: "l1" "l2",
      a_bind (λ: "r",
-         (a_store (a_ret "r") (a_load (a_ret "l1"))) ;;;;
-         (a_store (a_ret "l1") (a_load (a_ret "l2"))) ;;;;
-         ((a_store (a_ret "l2") (a_load (a_ret "r")))) ;;; a_seq #())
+         (a_store (a_ret "r") (a_load (a_ret "l1"))) ;ᶜ
+         (a_store (a_ret "l1") (a_load (a_ret "l2"))) ;ᶜ
+         ((a_store (a_ret "l2") (a_load (a_ret "r")))) ;;ᶜ a_seq #())
      (a_alloc (a_ret #0)).
 
   Lemma swap_spec (l1 l2 : loc) (v1 v2: val) R :
@@ -77,7 +77,7 @@ Section test.
   Definition assignF : val := λ: "lv",
     let: "l" := Fst "lv" in
     let: "v" := Snd "lv" in
-    a_store (a_ret "l") (a_ret "v") ;;;; a_ret "v".
+    a_store (a_ret "l") (a_ret "v") ;ᶜ a_ret "v".
 
   Lemma invoke_assignF_1 l (v v' : val) R :
     l ↦C v -∗

theories/vcgen/dcexpr.v

@@ -264,7 +264,7 @@ Fixpoint dcexpr_interp (E: known_locs) (de: dcexpr) : expr :=
   | dCStore de1 de2 => a_store (dcexpr_interp E de1) (dcexpr_interp E de2)
   | dCBinOp op de1 de2 => a_bin_op op (dcexpr_interp E de1) (dcexpr_interp E de2)
   | dCUnOp op de => a_un_op op (dcexpr_interp E de)
-  | dCSeq de1 de2 => (dcexpr_interp E de1) ;;;; (dcexpr_interp E de2)
+  | dCSeq de1 de2 => dcexpr_interp E de1 ;ᶜ dcexpr_interp E de2
   | dCUnknown e1 => e1
   end.
 
@@ -405,7 +405,7 @@ Proof. by rewrite /IntoDCexpr=> ->. Qed.
 Global Instance into_dcexpr_sequence E e1 e2 de1 de2:
   IntoDCexpr E e1 de1 →
   IntoDCexpr E e2 de2 →
-  IntoDCexpr E (e1 ;;;; e2) (dCSeq de1 de2).
+  IntoDCexpr E (e1 ;ᶜ e2) (dCSeq de1 de2).
 Proof. by rewrite /IntoDCexpr=> -> ->. Qed.
 
 Global Instance into_dcexpr_unknown E e `{Closed [] e}:

theories/vcgen/tests/fact.v

@@ -11,14 +11,14 @@ Definition incr : val := λ: "l",
 Definition factorial_body : val := λ: "n" "c" "r",
   a_while
       (λ:<>, a_bin_op LtOp (a_load (a_ret "c")) (a_ret "n"))
-      (λ:<>, incr "c" ;;;;
+      (λ:<>, incr "c" ;ᶜ
              a_store (a_ret "r")
              (a_bin_op MultOp (a_load (a_ret "r")) (a_load (a_ret "c")))).
 
 Definition factorial : val := λ: "n",
   a_bind ( λ: "r",
      a_bind (λ: "k",
-       factorial_body "n" "k" "r" ;;;;
+       factorial_body "n" "k" "r" ;ᶜ
          (a_load (a_ret "r")))
       (a_alloc (a_ret #0%V)))
          (a_alloc (a_ret #1%V)).

theories/vcgen/tests/swap.v

@@ -9,9 +9,9 @@ Section tests_vcg.
   Context `{amonadG Σ}.
 
   Definition swap : val := λ: "l1" "l2" "r",
-    (a_store (a_ret "r") (a_load (a_ret "l1"))) ;;;;
-    (a_store (a_ret "l1") (a_load (a_ret "l2"))) ;;;;
-    (a_store (a_ret "l2") (a_load (a_ret "r"))) ;;;;
+    (a_store (a_ret "r") (a_load (a_ret "l1"))) ;ᶜ
+    (a_store (a_ret "l1") (a_load (a_ret "l2"))) ;ᶜ
+    (a_store (a_ret "l2") (a_load (a_ret "r"))) ;ᶜ
     (a_ret #0).
 
   Lemma swap_spec_by_vcg_opt (l1 l2 r : loc) (v1 v2: val) R :
@@ -25,9 +25,9 @@ Section tests_vcg.
 
 Definition swap_with_alloc : val := λ: "l1" "l2",
      a_bind (λ: "r",
-         (a_store (a_ret "r") (a_load (a_ret "l1"))) ;;;;
-         (a_store (a_ret "l1") (a_load (a_ret "l2"))) ;;;;
-         ((a_store (a_ret "l2") (a_load (a_ret "r")))) ;;;; a_ret #())
+         (a_store (a_ret "r") (a_load (a_ret "l1"))) ;ᶜ
+         (a_store (a_ret "l1") (a_load (a_ret "l2"))) ;ᶜ
+         ((a_store (a_ret "l2") (a_load (a_ret "r")))) ;ᶜ a_ret #())
      (a_alloc (a_ret #0)).
 
   Lemma swap_spec (l1 l2 : loc) (v1 v2: val) R :

theories/vcgen/tests/test.v

@@ -2,7 +2,7 @@ From iris.heap_lang Require Export proofmode notation.
 From iris.algebra Require Import frac.
 From iris.bi Require Import big_op.
 From iris_c.vcgen Require Import dcexpr splitenv denv vcgen vcg_solver.
-From iris_c.c_translation Require Import monad translation proofmode notation.
+From iris_c.c_translation Require Import monad translation proofmode.
 From iris_c.lib Require Import locking_heap U.
 
 Section tests_vcg.
@@ -10,9 +10,8 @@ Section tests_vcg.
 
   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).
+    AWP (♯l =ᶜ ♯2 ;ᶜ ♯1 +ᶜ (♯l =ᶜ ♯1)) +ᶜ (♯s =ᶜ ♯4)
+    {{ v, ⌜v = #6⌝ ∧ s ↦C[LLvl] #4 ∗ l ↦C[LLvl] #1 }}.
   Proof.
     iIntros "Hs Hl".
     vcg_solver. eauto with iFrame.
@@ -20,8 +19,7 @@ Section tests_vcg.
 
   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).
+    AWP (♯l =ᶜ ♯2 ;ᶜ ∗ᶜ ♯l) +ᶜ (♯s =ᶜ ♯4) {{ v, ⌜v = #6⌝ ∧ s ↦C[LLvl] #4 ∗ l ↦C #2 }}.
   Proof.
     iIntros "Hs Hl".
     vcg_solver.
@@ -30,9 +28,7 @@ Section tests_vcg.
 
   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).
+    AWP ♯l =ᶜ ♯2 ;ᶜ ♯1 +ᶜ (♯l =ᶜ ♯1) {{ _, l ↦C[LLvl] #1 }}.
   Proof.
     iIntros "Hl". vcg_solver. iModIntro. eauto with iFrame.
   Qed.
@@ -40,20 +36,15 @@ Section tests_vcg.
   Lemma test_seq4 (l k : loc) :
     l ↦C #0 -∗
     k ↦C #0 -∗
-    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 #k) (a_ret #2);;;;
-         a_bin_op PlusOp (a_ret #1) (a_store (a_ret #k) (a_ret #1)))) True
-    (λ v, ⌜v = #4⌝ ∧ l ↦C[LLvl] #1 ∗ k ↦C[LLvl] #1).
+    AWP (♯l =ᶜ ♯2 ;ᶜ ♯1 +ᶜ (♯l =ᶜ ♯1)) +ᶜ (♯k =ᶜ ♯2 ;ᶜ ♯1 +ᶜ (♯k =ᶜ ♯1))
+      {{ v, ⌜v = #4⌝ ∧ l ↦C[LLvl] #1 ∗ k ↦C[LLvl] #1 }}.
   Proof.
     iIntros "Hl Hk".
     vcg_solver. iModIntro. by eauto with iFrame.
   Qed.
 
-  Definition stupid (l : loc) :=
-    a_store (a_ret #l) (a_ret #1);;;;(a_ret #0).
+  Definition stupid (l : loc) : expr :=
+    a_store (a_ret #l) (a_ret #1);ᶜ a_ret #0.
 
   Lemma test_seq_fail (l : loc) :
     l ↦C[ULvl] #0 -∗
@@ -66,12 +57,7 @@ Section tests_vcg.
   Lemma test_seq5 (l k : loc) :
     l ↦C #0 -∗
     k ↦C #0 -∗
-    awp (a_bin_op PlusOp (a_ret #0)
-          ((a_store (a_ret #l) (a_ret #1));;;;
-           (a_store (a_ret #k) (a_ret #2));;;;
-           (a_ret #0)))
-        True
-        (λ v, ⌜v = #0⌝ ∗ l ↦C #1 ∗ k ↦C #2).
+    AWP ♯0 +ᶜ (♯l =ᶜ ♯1 ;ᶜ ♯k =ᶜ ♯2 ;ᶜ ♯0) {{ v, ⌜v = #0⌝ ∗ l ↦C #1 ∗ k ↦C #2 }}.
   Proof.
     iIntros "Hl Hk". vcg_solver.
     repeat iModIntro. by eauto with iFrame.
@@ -80,16 +66,8 @@ Section tests_vcg.
   Lemma test_sp1 (l k : loc) :
     l ↦C #0 -∗
     k ↦C #0 -∗
-    awp (a_bin_op PlusOp (a_ret #1)
-          ((a_store (a_ret #l) (a_ret #1));;;;
-           (a_bin_op PlusOp
-              (a_store (a_ret #k) (a_ret #2))
-              (a_load (a_ret #l)));;;;
-           (a_bin_op PlusOp
-              (a_load (a_ret #k))
-              (a_store (a_ret #l) (a_ret #2)))))
-        True
-        (λ v, ⌜v = #5⌝ ∗ l ↦C[LLvl] #2 ∗ k ↦C #2).
+    AWP ♯1 +ᶜ (♯l =ᶜ ♯1 ;ᶜ (♯k =ᶜ ♯2) +ᶜ ∗ᶜ ♯l ;ᶜ ∗ᶜ ♯k +ᶜ (♯l =ᶜ ♯2))
+      {{ v, ⌜v = #5⌝ ∗ l ↦C[LLvl] #2 ∗ k ↦C #2 }}.
   Proof.
     iIntros "Hl Hk". vcg_solver.
     repeat iModIntro. rewrite ?Qp_half_half.
@@ -98,14 +76,7 @@ Section tests_vcg.
 
   Lemma test_sp2 (l : loc) :
     l ↦C #0 -∗
-    awp (a_bin_op PlusOp (a_ret #1)
-          ((a_store (a_ret #l) (a_ret #1));;;;
-           (a_bin_op PlusOp
-              (a_load (a_ret #l))
-              (a_load (a_ret #l)));;;;
-          (a_store (a_ret #l) (a_ret #2))))
-        True
-        (λ v, ⌜v = #3⌝ ∗ l ↦C[LLvl] #2).
+    AWP ♯1 +ᶜ (♯l =ᶜ ♯1 ;ᶜ ∗ᶜ ♯l +ᶜ ∗ᶜ ♯l ;ᶜ ♯l =ᶜ ♯2) {{ v, ⌜v = #3⌝ ∗ l ↦C[LLvl] #2 }}.
   Proof.
     iIntros "Hl". vcg_solver.
     repeat iModIntro. rewrite ?Qp_half_half.
@@ -114,7 +85,7 @@ Section tests_vcg.
 
   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).
+    AWP a_ret (LitV s) =ᶜ ∗ᶜ (a_ret (LitV l)) @ R {{ _, s ↦C[LLvl] #1 ∗ l ↦C #1 }}.
   Proof.
     iIntros "Hs Hl".
     vcg_solver. eauto with iFrame.
@@ -122,8 +93,7 @@ Section tests_vcg.
 
   Lemma store_load_load (s1 s2 l : loc) R :
     s1 ↦C #0 -∗ l ↦C #1 -∗ s2 ↦C #0 -∗
-       awp (a_store (a_ret #s1) (a_load (a_ret #l)) ;;;;
-           (a_bin_op PlusOp (a_load (a_ret #s1)) (a_ret #42))) R (λ _, s1 ↦C #1 ∗ l ↦C #1).
+    AWP ♯s1 =ᶜ ∗ᶜ ♯l ;ᶜ ∗ᶜ ♯s1 +ᶜ ♯42 @ R {{ _, s1 ↦C #1 ∗ l ↦C #1 }}.
       (* (a_store (a_ret #s2) (a_load (a_ret #l)))) R  (λ _, s1 ↦U #1 ∗ l ↦U #1). *)
   Proof.
     iIntros "Hs1 Hl Hs2". vcg_solver. iModIntro.
@@ -132,14 +102,12 @@ Section tests_vcg.
 
   Lemma test3 (l : loc) :
     l ↦C #1 -∗
-    awp (a_bin_op PlusOp (a_store (a_ret #l) (a_ret #2))
-                         (a_store (a_ret #l) (a_ret #2)))%E True (λ v, True).
+    AWP (♯l =ᶜ ♯2) +ᶜ (♯l =ᶜ ♯2) {{ _, True }}.
   Proof. iIntros "Hl". vcg_solver. Abort.
 
   Lemma test_while (l : loc) R :
     l ↦C #1 -∗
-    awp (a_while (λ: <>, ((a_bin_op LtOp) (∗ᶜ ♯l)) ♯2)
-                 (λ: <>, ♯l =ᶜ ♯1))%E R (λ _, True).
+    AWP whileᶜ (∗ᶜ ♯l <ᶜ ♯2) { ♯l =ᶜ ♯1 } @ R {{ _, True }}.
   Proof.
     iIntros "Hl".
     iLöb as "IH".

theories/vcgen/tests/unknowns.v

@@ -40,7 +40,7 @@ Section tests_vcg.
     k ↦C #1 -∗
     awp (a_bin_op PlusOp
           (a_store (a_ret #l) (a_ret #2))
-          (a_store (a_ret #k) e1 ;;;; e2)) True (λ v, l ↦C[LLvl] #2 ∗ k ↦C #11).
+          (a_store (a_ret #k) e1 ;ᶜ e2)) True (λ v, l ↦C[LLvl] #2 ∗ k ↦C #11).
   Proof.
     iIntros "He1 He2 Hl Hk". vcg_solver.
     iIntros "Hk".

theories/vcgen/vcg_solver.v

@@ -2,7 +2,7 @@ From iris.heap_lang Require Export proofmode notation.
 From iris.algebra Require Import frac.
 From iris.bi Require Import big_op.
 From iris_c.vcgen Require Import dcexpr splitenv denv vcgen.
-From iris_c.c_translation Require Import monad translation proofmode notation.
+From iris_c.c_translation Require Import monad translation proofmode.
 From iris_c.lib Require Import locking_heap U.
 From iris.proofmode Require Import environments coq_tactics.
 Import env_notations.

theories/vcgen/vcgen.v

@@ -11,7 +11,7 @@ TODO
 [DONE] Fix all the unknown cases, introduce a function for that (which should be