Handle WPs for primitives better

Make proofs more natural for Fork and ArbitraryInt wp_apply didn't
recognize `Fork` and `ArbitraryInt`, and they also didn't have specs using
new goose's to_val.

Author: tchajed

new/golang/theory.v

@@ -1,7 +1,7 @@
 From Perennial.goose_lang Require Export lang.
 From New.golang Require Export defn.
 From New.golang.theory Require Export exception list typing loop struct
-  mem slice map interface defer typing builtin chan pkg auto globals.
+  mem slice map interface defer typing builtin primitive chan pkg auto globals.
 
 Export uPred. (* XXX: inherited from proof_prelude.v; not sure why it's here. *)
 Global Set Default Proof Using "Type".

new/golang/theory/primitive.v

@@ -0,0 +1,34 @@
+From New Require Export notation.
+From New.golang.theory Require Export typing proofmode.
+From Perennial Require Import base.
+
+Set Default Proof Using "Type".
+
+Section wps.
+
+Context `{sem: ffi_semantics} `{!ffi_interp ffi} `{!heapGS Σ}.
+
+(* use new goose's to_val for the return value *)
+Lemma wp_fork s E e Φ :
+  ▷ WP e @ s; ⊤ {{ _, True }} -∗ ▷ Φ #() -∗ WP Fork e @ s; E {{ Φ }}.
+Proof.
+  iIntros "Hwp HΦ".
+  wp_apply (lifting.wp_fork with "[$Hwp]").
+  replace (LitV LitUnit) with #().
+  { iFrame "HΦ". }
+  rewrite to_val_unseal //.
+Qed.
+
+(* use new goose's to_val for the return value *)
+Lemma wp_ArbitraryInt s E Φ :
+  ▷ (∀ (x: w64), Φ #x) -∗ WP ArbitraryInt @ s; E {{ Φ }}.
+Proof.
+  iIntros "HΦ".
+  wp_apply (lifting.wp_ArbitraryInt).
+  iIntros (x) "_".
+  replace (LitV x) with #x.
+  { iApply "HΦ". }
+  rewrite to_val_unseal //.
+Qed.
+
+End wps.

new/golang/theory/proofmode.v

@@ -524,6 +524,8 @@ Ltac2 wp_bind_apply () : unit :=
                      lazy_match! e with
                      | App (Val _) (Val _) => ()
                      | App ?e1 (Val _) => f e1
+                     | Fork _ => ()
+                     | ArbitraryInt => ()
                      | _ => fail
                      end
                    in f e

new/golang/theory/slice.v

@@ -2,7 +2,7 @@ From Perennial.Helpers Require Import List ListLen Fractional NamedProps.
 From iris.algebra Require Import dfrac.
 From Perennial.goose_lang Require Import ipersist.
 From New.golang.defn Require Export slice.
-From New.golang.theory Require Export list mem exception loop typing auto.
+From New.golang.theory Require Export list mem exception loop typing primitive auto.
 From Perennial Require Import base.
 
 Set Default Proof Using "Type".
@@ -266,11 +266,8 @@ Proof.
     [apply bool_decide_eq_true_1 in Hlt2|apply bool_decide_eq_false_1 in Hlt2];
     wp_pures.
   {
-    wp_bind ArbitraryInt.
-    iApply (wp_ArbitraryInt with "[//]"). iNext.
-    iIntros (?) "_".
-    replace (LitV x) with (#x).
-    2:{ rewrite to_val_unseal //. }
+    wp_apply (wp_ArbitraryInt).
+    iIntros (?).
     wp_pures.
     rewrite slice_val_fold.
     iApply "HΦ".
@@ -604,12 +601,8 @@ Proof.
       destruct (bool_decide_reflect P); wp_auto
   end.
   - admit. (* TODO: slice.slice reasoning, going into capacity *)
-  - wp_bind (ArbitraryInt).
-    iApply (wp_ArbitraryInt with "[//]").
-    iIntros "!>" (x) "_". wp_auto.
-    replace (LitV x) with (#x).
-    2:{ rewrite to_val_unseal //. }
-    wp_auto.
+  - wp_apply (wp_ArbitraryInt).
+    iIntros (x). wp_auto.
     wp_apply wp_slice_make2. iIntros (s') "[Hs_new Hnew_cap]".
     wp_auto.
     admit. (* TODO: need wp for slice.copy *)

new/proof/asyncfile.v

@@ -652,15 +652,12 @@ Proof.
     iNext. by iFrame "∗#".
   }
 
-  wp_bind (Fork _)%E.
-  iApply (wp_fork with "[HpreIdx HpreData HdurIdx Hfile]").
+  wp_apply (wp_fork with "[HpreIdx HpreData HdurIdx Hfile]").
   {
-    iNext.
     wp_apply (wp_AsyncFile__flushThread with "[-]").
     { iFrame "∗#". }
     done.
   }
-  iNext. wp_auto.
   iApply "HΦ".
   iFrame "∗#".
 Qed.

new/proof/go_etcd_io/etcd/client/v3/concurrency.v

@@ -107,12 +107,9 @@ Proof.
   unshelve wp_apply wp_chan_make as "* Hdonec"; try tc_solve.
   wp_alloc s as "Hs".
   wp_auto.
-  wp_bind (Fork _).
   iPersist "cancel donec keepAlive".
-  iApply (wp_fork with "[Hdonec Hcancel]").
+  wp_apply (wp_fork with "[Hdonec Hcancel]").
   {
-    iNext.
-    wp_auto.
     wp_apply wp_with_defer as "%defer defer".
     simpl subst.
     wp_auto.
@@ -152,7 +149,6 @@ Proof.
       iFrame.
     }
   }
-  iNext.
   iDestruct (struct_fields_split with "Hs") as "hs".
   simpl. iClear "Hctx". iNamed "hs".
   iPersist "Hclient Hid".

new/proof/go_etcd_io/etcd/client/v3/leasing.v

@@ -165,26 +165,19 @@ Proof.
   replace (Z.to_nat (sint.Z (W32 2))) with (2%nat) by done.
   iEval (simpl) in "H".
   iDestruct "H" as "[Hwg_done1 Hwg_done2]".
-  wp_bind (Fork _).
-  iApply (wp_fork with "[Hwg_done1 session_monitor]").
+  wp_apply (wp_fork with "[Hwg_done1 session_monitor]").
   {
-    iNext. wp_auto.
     wp_apply wp_with_defer as "%defer defer".
     simpl subst.
     wp_auto.
     (* TODO: wp_monitorSession. *)
     admit.
   }
-  iNext. wp_auto.
-  wp_bind (Fork _).
-  iApply (wp_fork with "[Hwg_done2]").
+  wp_apply (wp_fork with "[Hwg_done2]").
   {
-    iNext. wp_auto.
     (* TODO: wp_clearOldRevokes. *)
     admit.
   }
-  iNext.
-  wp_auto.
   (* TODO: wp_waitSession. *)
   admit.
 Admitted.

new/proof/std.v

@@ -146,19 +146,15 @@ Proof.
   wp_auto.
   wp_apply (wp_newJoinHandle P) as "%l #Hhandle".
   iPersist "f h".
-  wp_bind (Fork _).
-  iApply (wp_fork with "[Hwp]").
-  - iModIntro. wp_auto.
-    (* NOTE: it's important not to do a pure reduction here since it would
+  wp_apply (wp_fork with "[Hwp]").
+  - (* NOTE: it's important not to do a pure reduction here since it would
     produce a substitution into the lambda *)
     wp_apply "Hwp".
     iIntros "HP".
     wp_auto.
     wp_apply (wp_JoinHandle__finish with "[$Hhandle $HP]").
     done.
-  - iModIntro.
-    wp_auto.
-    iApply "HΦ".
+  - iApply "HΦ".
     iFrame "#".
 Qed.
 

src/program_proof/grove_shared/urpc_proof.v

@@ -664,12 +664,11 @@ Proof.
   }
   iMod (inv_alloc urpc_clientN _ (reply_chan_inner Γ client) with "[Hr]") as "#Hchan_inv".
   { iNext. iExists ∅. iFrame. rewrite big_sepS_empty //. }
-  wp_bind (Fork _).
-  iApply wp_fork.
-  { iNext. wp_pures. iApply wp_Client__replyThread. repeat iExists _.
+  wp_apply wp_fork.
+  { iApply wp_Client__replyThread. repeat iExists _.
     iSplit. 1:iFrame "mu conn pending".
     iSplit; done. }
-  iNext. wp_pures. iModIntro. iApply "HΦ".
+  wp_pures. iModIntro. iApply "HΦ".
   iExists _, _, _, _. iSplit; first by iFrame "#". iSplit; done.
 Qed.