Consolidate =* and =*>

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.

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).

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.
 

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

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,28 +96,28 @@ 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.
     Fixpoint cmd c := cmd_body cmd c.
   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)).

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;

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 :=

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}.

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}.

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}.

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}.

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,

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,

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.