From b28164303b12a8d9a7dc6174abddbc1e8760078c Mon Sep 17 00:00:00 2001
From: Andres Erbsen <andres-github@andres.systems>
Date: Tue, 20 Jun 2023 13:44:58 +0000
Subject: [PATCH 1/2] inline and remove bedrock2.Notations

---
 bedrock2/src/bedrock2/FrameRule.v           |  2 +-
 bedrock2/src/bedrock2/Memory.v              |  2 +-
 bedrock2/src/bedrock2/Notations.v           | 18 -------------
 bedrock2/src/bedrock2/Semantics.v           |  6 ++++-
 bedrock2/src/bedrock2/WeakestPrecondition.v | 30 ++++++++++-----------
 5 files changed, 22 insertions(+), 36 deletions(-)
 delete mode 100644 bedrock2/src/bedrock2/Notations.v

diff --git a/bedrock2/src/bedrock2/FrameRule.v b/bedrock2/src/bedrock2/FrameRule.v
index 4d40a3633..370f71397 100644
--- a/bedrock2/src/bedrock2/FrameRule.v
+++ b/bedrock2/src/bedrock2/FrameRule.v
@@ -3,7 +3,7 @@ Require Import coqutil.sanity coqutil.Macros.subst coqutil.Macros.unique coqutil
 Require Import coqutil.Datatypes.PrimitivePair coqutil.Datatypes.HList.
 Require Import coqutil.Decidable.
 Require Import coqutil.Tactics.fwd coqutil.Tactics.Tactics.
-Require Import bedrock2.Notations bedrock2.Syntax.
+Require Import bedrock2.Syntax.
 Require Import coqutil.Map.Interface coqutil.Map.Properties coqutil.Map.OfListWord.
 Require Import coqutil.Word.Interface coqutil.Word.Bitwidth.
 Require Import bedrock2.MetricLogging.
diff --git a/bedrock2/src/bedrock2/Memory.v b/bedrock2/src/bedrock2/Memory.v
index 0804aeb52..09a76bf43 100644
--- a/bedrock2/src/bedrock2/Memory.v
+++ b/bedrock2/src/bedrock2/Memory.v
@@ -7,7 +7,7 @@ Require Import coqutil.Datatypes.PrimitivePair coqutil.Datatypes.HList coqutil.D
 Require Import coqutil.Map.Interface coqutil.Map.Properties.
 Require Import coqutil.Tactics.Tactics coqutil.Datatypes.Option.
 Require Import BinIntDef coqutil.Word.Interface coqutil.Word.LittleEndianList.
-Require Import bedrock2.Notations bedrock2.Syntax.
+Require Import bedrock2.Syntax.
 Require Import coqutil.Byte.
 Require Import coqutil.Map.OfListWord.
 
diff --git a/bedrock2/src/bedrock2/Notations.v b/bedrock2/src/bedrock2/Notations.v
deleted file mode 100644
index f5b86805c..000000000
--- a/bedrock2/src/bedrock2/Notations.v
+++ /dev/null
@@ -1,18 +0,0 @@
-Require Import coqutil.Macros.subst coqutil.Macros.unique.
-
-Notation "' x <- a | y ; f" :=
-  (match a with
-   | x => f
-   | _ => y
-   end)
-  (right associativity, at level 70, x pattern).
-
-Notation "'bind_ex' x <- a ; f" :=
-  (subst! a for a' in exists x, a' x /\ f)
-  (only parsing, right associativity, at level 60, f at level 200).
-Notation "'bind_ex_Some' x <- a ; f" :=
-  (subst! a for a' in exists x, a' = Some x /\ f)
-  (only parsing, right associativity, at level 60, f at level 200).
-Notation "'bind_eq' x <- a ; f" :=
-  (subst! a for a' in forall x, x = a' -> f)
-  (only parsing, right associativity, at level 60, f at level 200).
diff --git a/bedrock2/src/bedrock2/Semantics.v b/bedrock2/src/bedrock2/Semantics.v
index 99af00358..1820df16e 100644
--- a/bedrock2/src/bedrock2/Semantics.v
+++ b/bedrock2/src/bedrock2/Semantics.v
@@ -3,7 +3,7 @@ Require Import coqutil.Datatypes.PrimitivePair coqutil.Datatypes.HList.
 Require Import coqutil.Decidable.
 Require Import coqutil.Tactics.fwd.
 Require Import coqutil.Map.Properties.
-Require Import bedrock2.Notations bedrock2.Syntax coqutil.Map.Interface coqutil.Map.OfListWord.
+Require Import bedrock2.Syntax coqutil.Map.Interface coqutil.Map.OfListWord.
 Require Import BinIntDef coqutil.Word.Interface coqutil.Word.Bitwidth.
 Require Import bedrock2.MetricLogging.
 Require Export bedrock2.Memory.
@@ -89,6 +89,10 @@ Section semantics.
   (* this is the expr evaluator that is used to verify execution time, the just-correctness-oriented version is below *)
   Section WithMemAndLocals.
     Context (m : mem) (l : locals).
+
+    Local Notation "' x <- a | y ; f" := (match a with x => f | _ => y end)
+      (right associativity, at level 70, x pattern).
+
     Fixpoint eval_expr (e : expr) (mc : metrics) : option (word * metrics) :=
       match e with
       | expr.literal v => Some (word.of_Z v, addMetricInstructions 8
diff --git a/bedrock2/src/bedrock2/WeakestPrecondition.v b/bedrock2/src/bedrock2/WeakestPrecondition.v
index 03e3b9c03..ce45aa805 100644
--- a/bedrock2/src/bedrock2/WeakestPrecondition.v
+++ b/bedrock2/src/bedrock2/WeakestPrecondition.v
@@ -1,4 +1,4 @@
-Require Import coqutil.Macros.subst coqutil.Macros.unique bedrock2.Notations coqutil.Map.Interface coqutil.Map.OfListWord.
+Require Import coqutil.Macros.subst coqutil.Macros.unique coqutil.Map.Interface coqutil.Map.OfListWord.
 Require Import Coq.ZArith.BinIntDef coqutil.Word.Interface coqutil.Word.Bitwidth.
 Require Import coqutil.dlet bedrock2.Syntax bedrock2.Semantics.
 
@@ -12,11 +12,11 @@ Section WeakestPrecondition.
   Definition literal v (post : word -> Prop) : Prop :=
     dlet! v := word.of_Z v in post v.
   Definition get (l : locals) (x : String.string) (post : word -> Prop) : Prop :=
-    bind_ex_Some v <- map.get l x; post v.
+    exists v, map.get l x = Some v /\ post v.
   Definition load s m a (post : _ -> Prop) : Prop :=
-    bind_ex_Some v <- load s m a; post v.
+    exists v, load s m a = Some v /\ post v.
   Definition store sz m a v post :=
-    bind_ex_Some m <- store sz m a v; post m.
+    exists m', store sz m a v = Some m' /\ post m'.
 
   Section WithMemAndLocals.
     Context (m : mem) (l : locals).
@@ -65,15 +65,15 @@ Section WeakestPrecondition.
       match c with
       | cmd.skip => post t m l
       | cmd.set x ev =>
-        bind_ex v <- dexpr m l ev;
+        exists v, dexpr m l ev v /\
         dlet! l := map.put l x v in
         post t m l
       | cmd.unset x =>
         dlet! l := map.remove l x in
         post t m l
       | cmd.store sz ea ev =>
-        bind_ex a <- dexpr m l ea;
-        bind_ex v <- dexpr m l ev;
+        exists a, dexpr m l ea a /\
+        exists v, dexpr m l ev v /\
         store sz m a v (fun m =>
         post t m l)
       | cmd.stackalloc x n c =>
@@ -86,7 +86,7 @@ Section WeakestPrecondition.
           anybytes a n mStack' /\ map.split mCombined' m' mStack' /\
           post t' m' l')
       | cmd.cond br ct cf =>
-        bind_ex v <- dexpr m l br;
+        exists v, dexpr m l br v /\
         (word.unsigned v <> 0%Z -> rec ct t m l post) /\
         (word.unsigned v = 0%Z -> rec cf t m l post)
       | cmd.seq c1 c2 =>
@@ -96,20 +96,20 @@ Section WeakestPrecondition.
         Coq.Init.Wf.well_founded lt /\
         (exists v, inv v t m l) /\
         (forall v t m l, inv v t m l ->
-          bind_ex b <- dexpr m l e;
+          exists b, dexpr m l e b /\
           (word.unsigned b <> 0%Z -> rec c t m l (fun t' m l =>
             exists v', inv v' t' m l /\ lt v' v)) /\
           (word.unsigned b = 0%Z -> post t m l))
       | cmd.call binds fname arges =>
-        bind_ex args <- dexprs m l arges;
+        exists args, dexprs m l arges args /\
         call fname t m args (fun t m rets =>
-          bind_ex_Some l <- map.putmany_of_list_zip binds rets l;
-          post t m l)
+          exists l', map.putmany_of_list_zip binds rets l = Some l' /\
+          post t m l')
       | cmd.interact binds action arges =>
-        bind_ex args <- dexprs m l arges;
+        exists args, dexprs m l arges args /\
         exists mKeep mGive, map.split m mKeep mGive /\
         ext_spec t mGive action args (fun mReceive rets =>
-          bind_ex_Some l' <- map.putmany_of_list_zip binds rets l;
+          exists l', map.putmany_of_list_zip binds rets l = Some l' /\
           forall m', map.split m' mKeep mReceive ->
           post (cons ((mGive, action, args), (mReceive, rets)) t) m' l')
       end.
@@ -117,7 +117,7 @@ Section WeakestPrecondition.
   End WithFunctions.
 
   Definition func call '(innames, outnames, c) (t : trace) (m : mem) (args : list word) (post : trace -> mem -> list word -> Prop) :=
-      bind_ex_Some l <- map.of_list_zip innames args;
+      exists l, map.of_list_zip innames args = Some l /\
       cmd call c t m l (fun t m l =>
         list_map (get l) outnames (fun rets =>
         post t m rets)).

From 832f47eb4826594db5b3d1038bf4f30ae7b8b947 Mon Sep 17 00:00:00 2001
From: Andres Erbsen <andres-github@andres.systems>
Date: Tue, 20 Jun 2023 13:45:24 +0000
Subject: [PATCH 2/2] Consolidate =* and =*> to bedrock2.Map.Separation

---
 bedrock2/src/bedrock2/Map/Separation.v                   | 2 ++
 bedrock2/src/bedrock2Examples/indirect_add.v             | 1 -
 bedrock2/src/bedrock2Examples/indirect_add_heapletwise.v | 1 -
 bedrock2/src/bedrock2Examples/memconst.v                 | 1 -
 bedrock2/src/bedrock2Examples/memequal.v                 | 1 -
 bedrock2/src/bedrock2Examples/memmove.v                  | 1 -
 bedrock2/src/bedrock2Examples/memswap.v                  | 1 -
 bedrock2/src/bedrock2Examples/swap.v                     | 1 -
 bedrock2/src/bedrock2Examples/swap_by_add.v              | 2 +-
 bedrock2/src/bedrock2Examples/uint128_32.v               | 2 --
 10 files changed, 3 insertions(+), 10 deletions(-)

diff --git a/bedrock2/src/bedrock2/Map/Separation.v b/bedrock2/src/bedrock2/Map/Separation.v
index 3b3e97dd7..61a834a58 100644
--- a/bedrock2/src/bedrock2/Map/Separation.v
+++ b/bedrock2/src/bedrock2/Map/Separation.v
@@ -20,3 +20,5 @@ Declare Scope sep_scope.
 Delimit Scope sep_scope with sep.
 Infix "*" := sep (at level 40, left associativity) : sep_scope.
 Infix "⋆" := sep (at level 40, left associativity) : sep_scope.
+Notation "m =* P" := ((P%sep) m) (at level 70, only parsing).
+Notation "m =*> P" := (exists R, (sep P R) m) (at level 70, only parsing).
diff --git a/bedrock2/src/bedrock2Examples/indirect_add.v b/bedrock2/src/bedrock2Examples/indirect_add.v
index 78ddc2148..e59ef10d0 100644
--- a/bedrock2/src/bedrock2Examples/indirect_add.v
+++ b/bedrock2/src/bedrock2Examples/indirect_add.v
@@ -26,7 +26,6 @@ Section WithParameters.
 
   Definition f (a b : word) := word.add (word.add a b) b.
 
-  Local Notation "m =* P" := (P%sep m) (at level 70, only parsing). (* experiment *)
   Instance spec_of_indirect_add : spec_of "indirect_add" :=
     fnspec! "indirect_add" a b c / va Ra vb Rb vc Rc,
     { requires t m := m =* scalar a va * Ra /\ m =* scalar b vb * Rb /\ m =* scalar c vc * Rc;
diff --git a/bedrock2/src/bedrock2Examples/indirect_add_heapletwise.v b/bedrock2/src/bedrock2Examples/indirect_add_heapletwise.v
index 63c9bf8f8..e26318bb6 100644
--- a/bedrock2/src/bedrock2Examples/indirect_add_heapletwise.v
+++ b/bedrock2/src/bedrock2Examples/indirect_add_heapletwise.v
@@ -30,7 +30,6 @@ Section WithParameters.
 
   Definition f (a b : word) := word.add (word.add a b) b.
 
-  Local Notation "m =* P" := (P%sep m) (at level 70, only parsing). (* experiment *)
   Instance spec_of_indirect_add : spec_of "indirect_add" :=
     fnspec! "indirect_add" a b c / va Ra vb Rb vc Rc,
     { requires t m :=
diff --git a/bedrock2/src/bedrock2Examples/memconst.v b/bedrock2/src/bedrock2Examples/memconst.v
index 6633c2d2d..81e246be4 100644
--- a/bedrock2/src/bedrock2Examples/memconst.v
+++ b/bedrock2/src/bedrock2Examples/memconst.v
@@ -20,7 +20,6 @@ Local Notation string := String.string.
 
 (*Require Import bedrock2.ptsto_bytes.*)
 Local Notation "xs $@ a" := (Array.array ptsto (word.of_Z 1) a xs) (at level 10, format "xs $@ a").
-Local Notation "m =* P" := ((P%sep) m) (at level 70, only parsing) (* experiment*).
 
 Section WithParameters.
   Context {width} {BW: Bitwidth width}.
diff --git a/bedrock2/src/bedrock2Examples/memequal.v b/bedrock2/src/bedrock2Examples/memequal.v
index dad70b0fc..c18867845 100644
--- a/bedrock2/src/bedrock2Examples/memequal.v
+++ b/bedrock2/src/bedrock2Examples/memequal.v
@@ -23,7 +23,6 @@ Local Notation string := String.string.
 
 (*Require Import bedrock2.ptsto_bytes.*)
 Local Notation "xs $@ a" := (Array.array ptsto (word.of_Z 1) a xs) (at level 10, format "xs $@ a").
-Local Notation "m =* P" := ((P%sep) m) (at level 70, only parsing) (* experiment*).
 
 Section WithParameters.
   Context {width} {BW: Bitwidth width}.
diff --git a/bedrock2/src/bedrock2Examples/memmove.v b/bedrock2/src/bedrock2Examples/memmove.v
index 002d58b46..4aa826831 100644
--- a/bedrock2/src/bedrock2Examples/memmove.v
+++ b/bedrock2/src/bedrock2Examples/memmove.v
@@ -14,7 +14,6 @@ Local Notation string := String.string.
 (*Require Import bedrock2.ptsto_bytes.*)
 Require Import coqutil.Map.OfListWord.
 Local Notation "xs $@ a" := (map.of_list_word_at a xs) (at level 10, format "xs $@ a").
-Local Notation "m =* P" := ((P%sep) m) (at level 70, only parsing) (* experiment*).
 
 Section WithParameters.
   Context {width} {BW: Bitwidth width}.
diff --git a/bedrock2/src/bedrock2Examples/memswap.v b/bedrock2/src/bedrock2Examples/memswap.v
index 1917b2b8d..cd3af9e99 100644
--- a/bedrock2/src/bedrock2Examples/memswap.v
+++ b/bedrock2/src/bedrock2Examples/memswap.v
@@ -27,7 +27,6 @@ Local Notation string := String.string.
 
 (*Require Import bedrock2.ptsto_bytes.*)
 Local Notation "xs $@ a" := (Array.array ptsto (word.of_Z 1) a xs) (at level 10, format "xs $@ a").
-Local Notation "m =* P" := ((P%sep) m) (at level 70, only parsing) (* experiment*).
 
 Section WithParameters.
   Context {width} {BW: Bitwidth width}.
diff --git a/bedrock2/src/bedrock2Examples/swap.v b/bedrock2/src/bedrock2Examples/swap.v
index 7f685469d..9c3eaf5f6 100644
--- a/bedrock2/src/bedrock2Examples/swap.v
+++ b/bedrock2/src/bedrock2Examples/swap.v
@@ -32,7 +32,6 @@ Require Import coqutil.Tactics.rdelta.
 Section WithParameters.
   Context {word: word.word 32} {mem: map.map word Byte.byte}.
   Context {word_ok: word.ok word} {mem_ok: map.ok mem}.
-  Local Notation "m =* P" := ((P%sep) m) (at level 70, only parsing) (* experiment*).
 
   Instance spec_of_swap : spec_of "swap" :=
     fnspec! "swap" a_addr b_addr / a b R,
diff --git a/bedrock2/src/bedrock2Examples/swap_by_add.v b/bedrock2/src/bedrock2Examples/swap_by_add.v
index 708b5ffc2..81e7898be 100644
--- a/bedrock2/src/bedrock2Examples/swap_by_add.v
+++ b/bedrock2/src/bedrock2Examples/swap_by_add.v
@@ -26,7 +26,7 @@ Require Import coqutil.Tactics.eplace Coq.setoid_ring.Ring_tac.
 
 Section WithParameters.
   Context {mem: map.map word32 Byte.byte} {mem_ok: map.ok mem}.
-  Local Notation "m =* P" := ((P%sep) (m : mem)) (at level 70, only parsing) (* experiment*).
+  Implicit Types (R : mem -> Prop).
 
   Instance spec_of_swap : spec_of "swap" :=
     fnspec! "swap" a_addr b_addr / a b R,
diff --git a/bedrock2/src/bedrock2Examples/uint128_32.v b/bedrock2/src/bedrock2Examples/uint128_32.v
index d175dde51..040dcd51f 100644
--- a/bedrock2/src/bedrock2Examples/uint128_32.v
+++ b/bedrock2/src/bedrock2Examples/uint128_32.v
@@ -48,8 +48,6 @@ Local Ltac invert H := inversion H; clear H.
 Section WithParameters.
   Context {word: word.word 32} {mem: map.map word Byte.byte}.
   Context {word_ok: word.ok word} {mem_ok: map.ok mem}.
-  Local Notation "m =* P" := ((P%sep) m) (at level 70, only parsing) (* experiment*).
-  Local Notation "m =*> P" := (exists R, (sep P R) m) (at level 70, only parsing) (* experiment*).
   Import ProgramLogic.Coercions.
   Local Number Notation nat Nat.of_num_uint Nat.to_num_hex_uint (abstract after 5001) : core_scope.
   Local Number Notation nat Nat.of_num_uint Nat.to_num_uint (abstract after 5001) : core_scope.