Bump std++ and Iris

Need some fixes for std++ moving string functions into a module

new/proof/marshal.v

@@ -126,7 +126,7 @@ Proof.
   iApply struct_fields_split in "enc"; eauto.
   { constructor. compute.
     decide_reflect. }
-  rewrite /struct_fields struct.val_unseal /struct.val_def /= /append.
+  rewrite /struct_fields struct.val_unseal /struct.val_def /= /String.append.
   iNamed "enc".
   repeat (wp_load || wp_pures || wp_store).
 

src/Helpers/ProofCaching.v

@@ -124,7 +124,7 @@ Ltac cached_reduce :=
   match goal with |- ?u => let v := cached_eval u in change_no_check v end.
 
 Ltac iCache_go P Hs pat :=
-  let Hs := words Hs in
+  let Hs := String.words Hs in
   let Hs := (eval vm_compute in (INamed <$> Hs)) in
   let Δ := iGetCtx in
   let js := reduction.pm_eval (envs_split base.Left Hs Δ) in

src/goose_lang/lang.v

@@ -885,7 +885,7 @@ Definition bin_op_eval_string (op : bin_op) (s1 s2 : string) : option base_lit :
   end.
 
 Definition string_to_bytes (s:string): list u8 :=
-  (λ x, W8 $ Ascii.nat_of_ascii x) <$> list_ascii_of_string s.
+  (λ x, W8 $ Ascii.nat_of_ascii x) <$> String.list_ascii_of_string s.
 
 Definition bin_op_eval_string_word (op : bin_op) (s1 : string) {width} {word: Interface.word width} (w2 : word): option base_lit :=
   match op with

src/goose_lang/lib/string/string.v

@@ -10,14 +10,14 @@ Context `{ffi_sem: ffi_semantics} `{!ffi_interp ffi} `{!heapGS Σ}.
 Context {ext_ty: ext_types ext}.
 
 Definition bytes_to_string (l:list u8) : string :=
-  string_of_list_ascii (u8_to_ascii <$> l).
+  String.string_of_list_ascii (u8_to_ascii <$> l).
 
 Lemma bytes_to_string_to_bytes l :
   string_to_bytes $ bytes_to_string l = l.
 Proof.
   rewrite /string_to_bytes /bytes_to_string /=.
   rewrite -{2}(list_fmap_id l).
-  rewrite list_ascii_of_string_of_list_ascii.
+  rewrite String.list_ascii_of_string_of_list_ascii.
   rewrite -list_fmap_compose.
   apply list_fmap_ext.
   intros.

src/goose_lang/wpc_proofmode.v

@@ -353,7 +353,7 @@ Ltac wpc_frame_go pat d js :=
   ].
 
 Ltac wpc_frame_pat d pat :=
-  let js := (eval cbv in (INamed <$> words pat)) in
+  let js := (eval cbv in (INamed <$> String.words pat)) in
   wpc_frame_go pat d js.
 
 Tactic Notation "wpc_frame" constr(pat) := wpc_frame_pat base.Left pat.