Add various specs for slice skip/take

We had several low-level specs, especially in the untyped library, but
the typed library was missing many things that seem obvious in
retrospect.

There are six variants based on how ownership is divided, and it makes
sense to provide all of these specs since they are not obvious
consequences of more general specs:

1. SliceTake with `own_slice_small`. Straightforward.
2. SliceSkip with `own_slice_small`. Straightforward.
3. SliceTake with `own_slice`. Consumes the remainder of the slice to
  become the capacity of the prefix. This is the most distant from the
  code; it is not obvious that the original slice should no longer be
  used, even for reads.
4. SliceSkip with `own_slice`. The capacity is retained as-is.
5. std.SliceSplit with `own_slice_small`. This is a function in the
   Goose standard library that makes it easy to specify that doing
   `s[:n]` and `s[n:]` at the same time splits ownership, in a
   straightforward way. It is possible but more awkward to do this by
   directly writing `s[:n]` and `s[n:]` in the code.
6. std.SliceSplit with `own_slice`. Similar to the `own_slice_small`
   spec, because the capacity of the original slice is identical to the
   capacity of the skipped part. Splitting in this case allows using the
   original capacity as the capacity of the `s[n:]` end, while not
   allowing appending to the `s[:n]` end since this capacity aliases the
   `s[n:]`.

src/goose_lang/lib/slice/slice.v

@@ -739,6 +739,40 @@ Proof.
   word.
 Qed.
 
+Lemma own_slice_cap_take s t n vs :
+  uint.Z n ≤ uint.Z s.(Slice.sz) →
+  own_slice_small (slice_skip s t n) t (DfracOwn 1) (drop (uint.nat n) vs) ∗
+    own_slice_cap s t -∗
+  own_slice_cap (slice_take s n) t.
+Proof.
+  iIntros (Hn) "[Hskip Hcap]".
+  iDestruct (own_slice_cap_wf with "Hcap") as %Hwf.
+  rewrite /own_slice_cap /own_slice_small.
+  iDestruct "Hskip" as "[Hskip [%Hvs_len %Hskip_wf]]".
+  simpl in Hvs_len, Hskip_wf.
+  rewrite -> !word.unsigned_sub_nowrap in * by word.
+  rewrite length_drop in Hvs_len.
+  iDestruct "Hcap" as (extra Hextra_len) "Hcap".
+  iExists (drop (uint.nat n) vs ++ extra).
+  iSplit.
+  { iPureIntro.
+    simpl.
+    rewrite length_app length_drop.
+    word. }
+  simpl.
+  rewrite array_app.
+  iFrame "Hskip".
+
+  iExactEq "Hcap".
+  rewrite length_drop.
+  rewrite loc_add_assoc.
+  f_equal.
+  f_equal.
+  rewrite -Z.mul_add_distr_l.
+  f_equal.
+  word.
+Qed.
+
 (** We have full ownership, and take into the capacity.
 Cannot be typed, since [extra] might not be valid at this type. *)
 Lemma wp_SliceTake_full_cap {stk E s} t vs (n: u64):

src/goose_lang/lib/slice/typed_slice.v

@@ -264,6 +264,88 @@ Proof.
   iApply ("HΦ" with "[$]").
 Qed.
 
+Lemma wp_SliceTake_small {stk E s} t q vs (n: u64):
+  uint.Z n ≤ length vs →
+  {{{ own_slice_small s t q vs }}}
+    SliceTake (slice_val s) #n @ stk; E
+  {{{ RET (slice_val (slice_take s n)); own_slice_small (slice_take s n) t q (take (uint.nat n) vs) }}}.
+Proof.
+  iIntros (Hbound Φ) "Hs HΦ".
+  rewrite /own_slice_small.
+  wp_apply (slice.wp_SliceTake_small with "[$Hs]").
+  { rewrite list_untype_length //. }
+  rewrite /list.untype fmap_take //.
+Qed.
+
+Lemma wp_SliceSkip_small s t q vs (n : u64) :
+  uint.Z n ≤ length vs →
+  {{{ own_slice_small s t q vs }}}
+    SliceSkip t (slice_val s) #n
+  {{{ s', RET (slice_val s'); own_slice_small s' t q (drop (uint.nat n) vs) }}}.
+Proof.
+  iIntros (Hbound Φ) "Hs HΦ".
+  rewrite /own_slice_small. rewrite /list.untype fmap_drop.
+  wp_apply (slice.wp_SliceSkip_small with "[$Hs]").
+  { rewrite length_fmap; auto. }
+  auto.
+Qed.
+
+Lemma wp_SliceSkip_full s t q vs (n : u64) :
+  uint.Z n ≤ length vs →
+  {{{ own_slice s t q vs }}}
+    SliceSkip t (slice_val s) #n
+  {{{ s', RET (slice_val s'); own_slice s' t q (drop (uint.nat n) vs) }}}.
+Proof.
+  iIntros (Hbound Φ) "Hs HΦ".
+  iDestruct (own_slice_sz with "Hs") as %Hsz.
+  wp_apply slice.wp_SliceSkip.
+  { word. }
+  iApply "HΦ".
+  iApply own_slice_split.
+  iDestruct (own_slice_split_1 with "Hs") as "[Hs Hcap]".
+  rewrite /own_slice_small. rewrite /list.untype fmap_drop.
+  iDestruct (slice.slice_small_split with "Hs") as "[Hs1 $]".
+  { rewrite length_fmap; word. }
+  iApply (own_slice_cap_skip with "[$Hcap]").
+  { word. }
+Qed.
+
+(* construct the capacity of a slice_take expression from ownership over the
+rest of the slice (expressed using [slice_skip]) and the original capacity. *)
+Lemma own_slice_cap_take s t n vs :
+  uint.Z n ≤ uint.Z s.(Slice.sz) →
+  own_slice_small (slice_skip s t n) t (DfracOwn 1) (drop (uint.nat n) vs) ∗
+    own_slice_cap s t -∗
+  own_slice_cap (slice_take s n) t.
+Proof.
+  iIntros (Hn) "[Hskip Hcap]".
+  rewrite /own_slice_small.
+  iApply (slice.own_slice_cap_take with "[Hskip $Hcap]").
+  { auto. }
+  rewrite /list.untype fmap_drop. iFrame.
+Qed.
+
+(* Take a prefix s[:n] while retaining the capacity, which now includes the
+elements from n to the original length. Since the capacity must be fully owned,
+this variant requires full ownership of the slice and not a partial fraction. *)
+Lemma wp_SliceTake_full {stk E s} t vs (n: u64):
+  uint.Z n ≤ length vs →
+  {{{ own_slice s t (DfracOwn 1) vs }}}
+    SliceTake (slice_val s) #n @ stk; E
+  {{{ RET (slice_val (slice_take s n)); own_slice (slice_take s n) t (DfracOwn 1) (take (uint.nat n) vs) }}}.
+Proof.
+  iIntros (Hbound Φ) "Hs HΦ".
+  iDestruct (own_slice_sz with "Hs") as %Hsz.
+  iDestruct (own_slice_split_1 with "Hs") as "[Hs Hcap]".
+  iDestruct (own_slice_cap_wf with "Hcap") as %Hcap.
+  wp_apply (slice.wp_SliceTake).
+  { word. }
+  iApply "HΦ".
+  iDestruct (slice_small_split with "Hs") as "[$ Hdrop]".
+  { word. }
+  iApply own_slice_cap_take; [ word | ]. iFrame.
+Qed.
+
 Lemma wp_SliceSet stk E s t `{!IntoValForType V t} vs (i: u64) v :
   {{{ own_slice_small s t (DfracOwn 1) vs ∗ ⌜ is_Some (vs !! uint.nat i) ⌝ }}}
     SliceSet t (slice_val s) #i (to_val v) @ stk; E
@@ -487,19 +569,22 @@ Proof.
   word.
 Qed.
 
-Lemma wp_SliceCopy_full_typed stk E sl t q vs dst vs' :
+Lemma wp_SliceCopy_full stk E sl t q vs dst vs' :
   {{{ own_slice_small sl t q vs ∗ own_slice_small dst t (DfracOwn 1) vs' ∗ ⌜length vs = length vs'⌝}}}
     SliceCopy t (slice_val dst) (slice_val sl) @ stk; E
-  {{{ RET #(W64 (length vs)); own_slice_small sl t q vs ∗ own_slice_small dst t (DfracOwn 1) vs }}}.
+  {{{ (l: w64), RET #l; ⌜uint.nat l = length vs⌝ ∗ own_slice_small sl t q vs ∗ own_slice_small dst t (DfracOwn 1) vs }}}.
 Proof.
   iIntros (Φ) "(Hsrc & Hdst & %Hlen) HΦ".
+  iDestruct (own_slice_small_sz with "Hsrc") as %Hsz.
   wp_apply (wp_SliceCopy with "[$Hsrc $Hdst]"); [word|].
   iIntros "(? & ?)".
   rewrite Hlen.
   rewrite drop_all.
   list_simplifier.
   iApply "HΦ".
   iFrame.
+  iPureIntro.
+  word.
 Qed.
 
 Lemma wp_SliceCopy_subslice stk E sl (n1 n2: u64) t q vs dst vs' :

src/program_proof/marshal_stateless_proof.v

@@ -21,7 +21,7 @@ Proof.
   { rewrite /list.untype fmap_app take_app_length' //. }
   iIntros "Hs".
   wp_apply (wp_SliceSkip_small with "Hs").
-  { rewrite /list.untype length_fmap length_app /=. word. }
+  { len. }
   iIntros (s') "Hs'". wp_pures. iApply "HΦ". done.
 Qed.
 
@@ -35,7 +35,7 @@ Proof.
   { rewrite /list.untype fmap_app take_app_length' //. }
   iIntros "Hs".
   wp_apply (wp_SliceSkip_small with "Hs").
-  { rewrite /list.untype length_fmap length_app /=. word. }
+  { len. }
   iIntros (s') "Hs'". wp_pures. iApply "HΦ". done.
 Qed.
 
@@ -49,13 +49,15 @@ Proof.
   iMod (own_slice_small_persist with "Hs") as "#Hs".
   wp_rec. wp_pures.
   wp_apply (wp_SliceTake_small with "Hs").
-  { rewrite /list.untype fmap_app length_app !length_fmap. word. }
+  { len. }
   iIntros "Hs1".
   wp_apply (wp_SliceSkip_small with "Hs").
-  { rewrite /list.untype length_fmap length_app /=. word. }
+  { len. }
   iIntros (s') "Hs2". wp_pures. iApply "HΦ".
-  { rewrite /list.untype -fmap_take -fmap_drop.
-    rewrite take_app_length' // drop_app_length' //. iFrame. done. }
+  iModIntro.
+  rewrite take_app_length' //.
+  rewrite drop_app_length' //.
+  iFrame.
 Qed.
 
 Theorem wp_ReadBytesCopy s q (len: u64) (head tail : list u8) :
@@ -75,17 +77,17 @@ Proof.
   { rewrite length_app. word. }
   iDestruct (own_slice_small_acc with "Hb") as "[Hb Hbclose]".
   wp_apply (wp_SliceCopy_full with "[$Hs $Hb]").
-  { iPureIntro. rewrite !list_untype_length length_replicate length_take length_app. word. }
-  iIntros "[Hs Hb]".
+  { iPureIntro. len. }
+  iIntros (l) "(%Hl_val & Hs & Hb)".
   iDestruct (own_slice_combine with "Hs Hsclose") as "Hs".
   { word. }
   rewrite take_drop.
   wp_apply (wp_SliceSkip_small with "Hs").
-  { rewrite list_untype_length length_app. word. }
+  { len. }
   iIntros (s') "Hs'".
   wp_pures. iApply "HΦ". iModIntro. iSplitR "Hs'".
   - iApply "Hbclose". rewrite take_app_length' //.
-  - rewrite /list.untype -fmap_drop drop_app_length' //.
+  - rewrite drop_app_length' //.
 Qed.
 
 Theorem wp_ReadBool s q (bit: u8) (tail: list u8) :
@@ -99,9 +101,8 @@ Proof.
   wp_apply (wp_SliceGet with "[$Hs]"); [ auto | ].
   iIntros "Hs".
   wp_pures.
-  (* TODO: this wp seems to come from untyped library *)
   wp_apply (wp_SliceSkip_small with "Hs").
-  { rewrite list_untype_length /=. word. }
+  { len. }
   iIntros (s') "Hs".
   wp_pures. iModIntro.
   iApply "HΦ".
@@ -112,9 +113,7 @@ Proof.
       split.
     - inversion 1; subst; auto.
     - intros H.
-      do 2 f_equal.
-      apply (inj uint.Z). (* don't know how I even figured this out *)
-      change (uint.Z (U8 0)) with 0%Z; assumption.
+      repeat (f_equal; try word).
     }
     destruct (decide _), (decide _); auto; tauto.
   }
@@ -157,7 +156,7 @@ Proof.
     iIntros (ptr) "Hnew". wp_pures.
     iDestruct (slice.own_slice_to_small with "Hs") as "Hs".
     iDestruct (slice.own_slice_small_acc with "Hnew") as "[Hnew Hcl]".
-    wp_apply (wp_SliceCopy_full with "[Hnew Hs]").
+    wp_apply (slice.wp_SliceCopy_full with "[Hnew Hs]").
     { iFrame. iPureIntro. rewrite list_untype_length Hsz length_replicate //. }
     iIntros "[_ Hnew]". iDestruct ("Hcl" with "Hnew") as "Hnew".
     wp_pures. iApply "HΦ". iModIntro. iFrame. iPureIntro. simpl. word.
@@ -243,17 +242,8 @@ Theorem wp_WriteBool s (vs: list u8) (b: bool) :
 Proof.
   iIntros (Φ) "Hs HΦ". wp_rec. wp_pures.
   destruct b; wp_pures.
-  (* TODO: this also breaks through the typed slice library *)
-  - wp_apply (wp_SliceAppend' with "Hs"); auto.
-    iIntros (s') "Hs".
-    iApply "HΦ".
-    rewrite /own_slice.
-    rewrite list_untype_app //.
-  - wp_apply (wp_SliceAppend' with "Hs"); auto.
-    iIntros (s') "Hs".
-    iApply "HΦ".
-    rewrite /own_slice.
-    rewrite list_untype_app //.
+  - wp_apply (wp_SliceAppend with "Hs"); auto.
+  - wp_apply (wp_SliceAppend with "Hs"); auto.
 Qed.
 
 End goose_lang.

src/program_proof/std_proof.v

@@ -190,6 +190,24 @@ Proof.
   word.
 Qed.
 
+Lemma wp_SliceSplit_full s dq (xs: list w8) (n: w64) :
+  {{{ own_slice s byteT dq xs ∗ ⌜uint.Z n < Z.of_nat (length xs)⌝ }}}
+    SliceSplit (to_val s) #n
+  {{{ RET (to_val (slice_take s n), to_val (slice_skip s byteT n));
+      own_slice_small (slice_take s n) byteT dq (take (uint.nat n) xs) ∗
+      own_slice (slice_skip s byteT n) byteT dq (drop (uint.nat n) xs)
+  }}}.
+Proof.
+  iIntros (Φ) "[Hs %Hn] HΦ".
+  iDestruct (own_slice_sz with "Hs") as %Hsz.
+  iDestruct (own_slice_split_1 with "Hs") as "[Hs Hcap]".
+  wp_apply (wp_SliceSplit with "[$Hs]"); [ done | ].
+  iIntros "[Htake Hskip]".
+  iApply "HΦ". iFrame "Htake".
+  iApply own_slice_split; iFrame "Hskip".
+  iApply (own_slice_cap_skip with "Hcap"). word.
+Qed.
+
 Lemma wp_SumNoOverflow (x y : u64) stk E :
   ∀ Φ : val → iProp Σ,
     Φ #(bool_decide (uint.Z (word.add x y) = (uint.Z x + uint.Z y)%Z)) -∗