Fix proof of sync

new/golang/theory/globals.v

@@ -390,3 +390,11 @@ Proof.
 Qed.
 
 End init.
+
+Tactic Notation "wp_func_call" :=
+  (wp_bind (func_call _ _);
+   unshelve wp_apply (wp_func_call with "[]"); [| | tc_solve | | ]; try iFrame "#").
+
+Tactic Notation "wp_method_call" :=
+  (wp_bind (method_call _ _ _);
+   unshelve wp_apply (wp_method_call with "[]"); [| | tc_solve | |]; try iFrame "#").

new/golang/theory/list.v

@@ -43,8 +43,7 @@ Global Instance wp_list_Match (l : list V) (handleNil handleCons : val) :
     (match l with
      | nil => (handleNil #())%V
      | cons v l => (handleCons #v #l)%V
-     end)
-.
+     end).
 Proof.
   rewrite list.Match_unseal.
   intros ?????. iIntros "Hwp".
@@ -81,8 +80,7 @@ Qed.
 Global Instance wp_alist_cons (k : go_string) (l : list (go_string * val)) (v : val) :
   PureWp  True
     (list.Cons (PairV #k v) (alist_val l))
-    (alist_val ((pair k v) :: l))
-.
+    (alist_val ((pair k v) :: l)).
 Proof.
   iIntros (?????) "HΦ".
   rewrite alist_val_unseal list.Cons_unseal.
@@ -92,8 +90,7 @@ Qed.
 Global Instance wp_alist_lookup (k : go_string) (l : list (go_string * val)) :
   PureWp True
     (alist_lookup #k (alist_val l))
-    (match (alist_lookup_f k l) with | None => InjLV #() | Some v => InjRV v end)
-.
+    (match (alist_lookup_f k l) with | None => InjLV #() | Some v => InjRV v end).
 Proof.
   iIntros (?????) "HΦ".
   rewrite alist_val_unseal.
@@ -110,18 +107,14 @@ Proof.
     {
       rewrite bool_decide_eq_true in Heqb.
       subst.
-      wp_pures.
-      rewrite /ByteString.eqb bool_decide_true //.
+      rewrite ByteString.eqb_refl.
       by iApply "HΦ".
     }
     {
       rewrite bool_decide_eq_false in Heqb.
       wp_pures.
       iApply "IH".
-      destruct (ByteString.eqb g _)%go eqn:Hx.
-      { exfalso. apply Heqb. repeat f_equal. symmetry.
-        rewrite /ByteString.eqb bool_decide_eq_true // in Hx. }
-      by iApply "HΦ".
+      rewrite ByteString.eqb_ne //.
     }
   }
 Qed.

new/golang/theory/struct.v

@@ -185,11 +185,12 @@ Definition is_structT (t : go_type) : Prop :=
   end.
 
 Definition wp_struct_make (t : go_type) (l : list (go_string*val)) :
-  PureWp (is_structT t)
+  is_structT t →
+  PureWp True
   (struct.make t (alist_val l))
   (struct.val_aux t l).
 Proof.
-  intros ?????K.
+  intros ??????K.
   rewrite struct.make_unseal struct.val_aux_unseal.
   destruct t; try by exfalso.
   unfold struct.make_def.

new/proof/grove_ffi.v

@@ -31,13 +31,10 @@ Instance wp_struct_make_ConnectRet `{ffi_semantics} `{!ffi_interp ffi} `{!heapGS
   (struct.make ConnectRet (alist_val [("Err" ::= #err)%V; ("Connection" ::= #conn)%V]))
   #(ConnectRet.mk err conn).
 Proof.
-  pose proof wp_struct_make.
-  rewrite /PureWp => *. iIntros "Hwp".
-  wp_pure_lc "Hlc".
-  iEval (rewrite to_val_unseal /=) in "Hwp". by iApply "Hwp".
+  rewrite [in #(_ : ConnectRet.t)]to_val_unseal.
+  by apply wp_struct_make.
 Qed.
 
-
 Module ReceiveRet.
 Record t :=
   mk {
@@ -61,10 +58,8 @@ Instance wp_struct_make_ReceiveRet `{ffi_semantics} `{!ffi_interp ffi} `{!heapGS
   (struct.make ReceiveRet (alist_val [("Err" ::= #err)%V; ("Data" ::= #data)%V]))
   #(ReceiveRet.mk err data).
 Proof.
-  pose proof wp_struct_make.
-  rewrite /PureWp => *. iIntros "Hwp".
-  wp_pure_lc "Hlc".
-  iEval (rewrite to_val_unseal /=) in "Hwp". by iApply "Hwp".
+  rewrite [in #(_ : ReceiveRet.t)]to_val_unseal.
+  by apply wp_struct_make.
 Qed.
 
 (** * Specs for user-facing operations *)

new/proof/std.v

@@ -1,16 +1,19 @@
 From New.proof Require Import proof_prelude.
-From New.code.github_com.goose_lang Require Import std.
+From New.code.github_com.goose_lang Require std.
 From New.proof Require Import machine.
 
 Section wps.
 Context `{hG: heapGS Σ, !ffi_semantics _ _}.
 
 Lemma wp_SumNoOverflow (x y : u64) :
-  ∀ Φ : val → iProp Σ,
-    Φ #(bool_decide (uint.Z (word.add x y) = (uint.Z x + uint.Z y)%Z)) -∗
-    WP std.SumNoOverflow #x #y {{ Φ }}.
+  {{{ True }}}
+    func_call #std.pkg_name' #"SumNoOverflow" #x #y
+  {{{ RET #(bool_decide (uint.Z (word.add x y) = (uint.Z x + uint.Z y)%Z)); True }}}.
 Proof.
-  iIntros (Φ) "HΦ".
+  iIntros (Φ) "#Hdef HΦ".
+  wp_bind (func_call _ _).
+  unshelve wp_apply (wp_func_call with "[]"); [| | tc_solve | | ]; try iFrame "#".
+  wp_func_call.
   rewrite /SumNoOverflow. wp_pures.
   wp_alloc y_ptr as "Hy".
   wp_pures.

new/proof/structs/sync.v

@@ -37,3 +37,62 @@ Global Program Instance into_val_struct_Mutex_state `{ffi_syntax} :
 Final Obligation.
 intros. by rewrite to_val_unseal /= struct.val_aux_unseal /= to_val_unseal /=.
 Qed.
+
+Module Cond.
+Section def.
+Context `{ffi_syntax}.
+Record t := mk {
+  L : interface.t;
+}.
+End def.
+End Cond.
+
+Global Instance settable_Cond `{ffi_syntax}: Settable _ :=
+  settable! Cond.mk < Cond.L >.
+Global Instance into_val_Cond `{ffi_syntax} : IntoVal Cond.t :=
+  {
+    to_val_def := λ v, struct.val_aux Cond [("L" ::= #v.(Cond.L))]%V
+  }.
+
+Global Program Instance into_val_typed_Cond `{ffi_syntax} : IntoValTyped Cond.t Cond :=
+{|
+  default_val := Cond.mk (default_val _) ;
+  to_val_eqdec := ltac:(solve_decision);
+|}.
+Next Obligation.
+  rewrite to_val_unseal. solve_has_go_type.
+Qed.
+Next Obligation.
+  intros ?. repeat rewrite !to_val_unseal /=. rewrite zero_val_eq.
+  repeat rewrite struct.val_aux_unseal /=.
+  rewrite zero_val_eq /=.
+  repeat rewrite !to_val_unseal /=.
+  reflexivity.
+Qed.
+Final Obligation.
+(* FIXME: automation for this *)
+rewrite to_val_unseal => ? x y Heq.
+rewrite /= struct.val_aux_unseal /= in Heq.
+inversion Heq.
+destruct x, y.
+f_equal.
+simpl in *.
+apply to_val_inj in H0. subst. done.
+Qed.
+
+Program Global Instance into_val_struct_field_Cond_L `{ffi_syntax} : IntoValStructField "L" Cond Cond.L.
+Final Obligation.
+intros. rewrite to_val_unseal /= struct.val_aux_unseal /= zero_val_eq /= to_val_unseal /=.
+rewrite to_val_unseal /=. done.
+Qed.
+
+Instance wp_struct_make_Cond `{ffi_semantics} `{!ffi_interp ffi} `{!heapGS Σ} L :
+  PureWp True
+    (struct.make Cond (alist_val [
+      "L" ::= #L
+    ]))%V
+    #(Cond.mk L).
+Proof.
+  rewrite [in #(_ : Cond.t)]to_val_unseal.
+  by apply wp_struct_make.
+Qed.

new/proof/sync.v

@@ -101,10 +101,6 @@ Qed.
 Global Hint Mode WpMethodCall - - - - - - + + + - - : typeclass_instances.
 Global Hint Mode WpFuncCall - - - - - - + + - - : typeclass_instances.
 
-Tactic Notation "wp_method_call" :=
-  (wp_bind (method_call _ _ _);
-   unshelve wp_apply (wp_method_call with "[]"); [| | tc_solve | |]; try iFrame "#").
-
 Lemma wp_Mutex__Lock m R :
   {{{ is_defined ∗ is_Mutex m R }}}
     method_call #sync.pkg_name' #"Mutex'ptr" #"Lock" #m #()
@@ -211,14 +207,10 @@ Qed.
 
 (** This means [c] is a condvar with underyling Locker at address [m]. *)
 Definition is_Cond (c : loc) (m : interface.t) : iProp Σ :=
-  c ↦□ m.
+  c ↦s[Cond :: "L"]□ m.
 
 Global Instance is_Cond_persistent c m : Persistent (is_Cond c m) := _.
 
-Tactic Notation "wp_func_call" :=
-  (wp_bind (func_call _ _);
-   unshelve wp_apply (wp_func_call with "[]"); [| | tc_solve | | ]; try iFrame "#").
-
 Theorem wp_NewCond (m : interface.t) :
   {{{ is_defined }}}
     func_call #sync.pkg_name' #"NewCond" #m
@@ -228,7 +220,15 @@ Proof.
   wp_func_call. wp_call. wp_apply wp_fupd.
   wp_alloc c as "Hc".
   wp_pures.
-  iApply "HΦ". iMod (typed_pointsto_persist with "Hc") as "$".
+  iApply "HΦ".
+
+  iDestruct (struct_fields_split with "Hc") as "Hl".
+  rewrite /struct_fields /=.
+  repeat (iDestruct "Hl" as "[H1 Hl]";
+          unshelve iSpecialize ("H1" $! _ _ _ _ _ _ _); try tc_solve;
+          iNamed "H1").
+  simpl.
+  iMod (typed_pointsto_persist with "HL") as "$".
   done.
 Qed.
 

src/Helpers/ByteString.v

@@ -65,9 +65,58 @@ String Notation byte_string parse_string print_string
   (via IndByteString mapping [id_byte_string => IByteString] )
   : byte_string_scope.
 
-(* TODO: replace with more computationally efficient version *)
-#[local] Definition eqb (s1 s2: byte_string) : bool :=
-  bool_decide (s1 = s2).
+#[local] Fixpoint eqb (s1 s2: byte_string) : bool :=
+  match s1 with
+  | [] => match s2 with
+         | [] => true
+         | _ => false
+         end
+  | c1 :: s1' =>
+      match s2 with
+      | [] => false
+      | c2 :: s2' => if word.eqb c1 c2 then eqb s1' s2' else false
+      end
+  end.
+
+#[local] Lemma eqb_refl x :
+  eqb x x = true.
+Proof.
+  induction x; first done. simpl. rewrite word.eqb_eq //.
+Qed.
+
+#[local] Lemma eqb_eq x y :
+  x = y → eqb x y = true.
+Proof.
+  intros ?. subst. apply eqb_refl.
+Qed.
+
+#[local] Lemma eqb_true x y :
+  eqb x y = true → x = y.
+Proof.
+  revert y. induction x.
+  - by destruct y.
+  - destruct y; first done.
+    simpl.
+    destruct (word.eqb) eqn:?; last done.
+    apply word.eqb_true in Heqb. subst.
+    intros H. f_equal.
+    by apply IHx.
+Qed.
+
+#[local] Lemma eqb_false x y :
+  eqb x y = false → x ≠ y.
+Proof.
+  intros Heqb.
+  intros Heq. apply eqb_eq in Heq. rewrite Heqb in Heq. done.
+Qed.
+
+#[local] Lemma eqb_ne x y :
+  x ≠ y → eqb x y = false.
+Proof.
+  destruct eqb eqn:?.
+  { intros ?. apply eqb_true in Heqb. done. }
+  { done. }
+Qed.
 
 (* These theorems are not actually required, but they are a sanity check that
 the code above is implemented correctly. *)