Bump dependencies

Fixes are due to https://gitlab.mpi-sws.org/iris/iris/-/merge_requests/1035
mit-pdos · Mar 7, 2024 · 772faf8 · 772faf8
1 parent 10b8791
commit 772faf8
Show file tree

Hide file tree

Showing 12 changed files with 16 additions and 12 deletions.
diff --git a/external/coqutil b/external/coqutil
diff --git a/external/iris b/external/iris
diff --git a/external/stdpp b/external/stdpp
diff --git a/src/goose_lang/lib/slice/pred_slice.v b/src/goose_lang/lib/slice/pred_slice.v
@@ -62,6 +62,7 @@ Proof.
     apply fmap_Some_2; eauto. }
   iIntros "[Hs %Hty]".
   iApply "HΦ"; iFrame.
+  iIntros "HΨ". iFrame. iApply ("Hxs" with "HΨ").
 Qed.
 
 Theorem wp_SliceAppend {stk E} s l v x :

diff --git a/src/program_proof/buf/bufmap_proof.v b/src/program_proof/buf/bufmap_proof.v
@@ -166,7 +166,7 @@ Proof using.
     iFrame.
 
     iIntros "!>" (b') "Hbuf".
-    iExists _.
+    iExists _, _, _; iFrame.
     iSplitR; first eauto.
     replace (am) with (<[a:=v]> am) at 1 by ( apply insert_id; eauto ).
     by iApply "Ham".

diff --git a/src/program_proof/examples/async_mem_alloc_inode_proof.v b/src/program_proof/examples/async_mem_alloc_inode_proof.v
@@ -71,7 +71,7 @@ Theorem is_inode_durable_read addr σ addrs :
 Proof.
   iNamed 1.
   iExists _; iFrame "∗ %".
-  iIntros "!> $ $".
+  iIntros "!> Haddr Hdata". iExists _; iFrame "∗%".
 Qed.
 
 Definition inode_linv (l:loc) (addr:u64) σ : iProp Σ :=
@@ -312,7 +312,7 @@ Proof.
   wp_loadField.
   iApply "HΦ".
   iFrame "∗ %".
-  iIntros "$".
+  iIntros "$". iFrame.
 Qed.
 
 Theorem wpc_Inode__UsedBlocks {l σ addr} :
@@ -914,7 +914,7 @@ Proof.
           wpc_apply (wpc_Barrier1 with "[$Hhdr]").
           iSplit.
           {
-            iLeft in "Hfupd". iFrame. iIntros "$". by subst.
+            iLeft in "Hfupd". iFrame. iIntros "$". iFrame "∗%". by subst.
           }
           iNext. iIntros "[%Hfalso ?]". exfalso. congruence.
       }

diff --git a/src/program_proof/examples/inode_proof.v b/src/program_proof/examples/inode_proof.v
@@ -71,7 +71,7 @@ Theorem is_inode_durable_read addr σ addrs :
 Proof.
   iNamed 1.
   iExists _; iFrame "∗ %".
-  iIntros "!> $ $".
+  iIntros "!> Haddr Hdata". iExists _; iFrame "∗%".
 Qed.
 
 Definition inode_linv (l:loc) (addr:u64) σ : iProp Σ :=
@@ -294,7 +294,7 @@ Proof.
   wp_loadField.
   iApply "HΦ".
   iFrame "∗ %".
-  iIntros "$".
+  iIntros "$". iFrame.
 Qed.
 
 Theorem wpc_Inode__UsedBlocks {l σ addr} :

diff --git a/src/program_proof/examples/replicated_block_proof.v b/src/program_proof/examples/replicated_block_proof.v
@@ -226,7 +226,7 @@ Section goose.
     wpc_apply (wpc_Read with "Haddr'").
     iSplit; [ | iNext ].
     { iLeft in "HQ".
-      iFrame. iIntros.
+      iFrame. iIntros. iFrame "HP".
       iApply rblock_linv_to_cinv; iFrame. iApply "Hlkinv". eauto. }
     iIntros (s) "(Haddr'&Hb)".
     iDestruct (own_slice_to_small with "Hb") as "Hb".

diff --git a/src/program_proof/obj/commit_proof.v b/src/program_proof/obj/commit_proof.v
@@ -1275,14 +1275,15 @@ Proof.
         iApply "HΦ". iModIntro. iFrame.
         iSplitL.
         2: { iIntros "%H". congruence. }
+        iIntros (H). iExists _; iFrame.
         done.
 
       * wp_pures.
         wp_load.
         iApply "HΦ". iModIntro. iFrame.
         iSplitL.
         2: { iIntros "%H". congruence. }
-        iIntros (??). intuition congruence.
+        iIntros (?). iExists _; iFrame. iIntros (?). intuition congruence.
 
     + wp_apply util_proof.wp_DPrintf.
       wp_store.

diff --git a/src/program_proof/obj/invariant.v b/src/program_proof/obj/invariant.v
@@ -192,7 +192,7 @@ Proof.
   rewrite /pointsto_txn.
   iIntros "H". iNamed "H".
   iFrame.
-  iIntros (v') "$H".
+  iIntros (v') "$". iExists _; iFrame.
 Qed.
 
 Theorem pointsto_txn_cur_map {A} γ (m : gmap addr A) (f : A -> {K & bufDataT K}) (xform : A -> A):

diff --git a/src/program_proof/vrsm/replica/init_proof.v b/src/program_proof/vrsm/replica/init_proof.v
@@ -135,6 +135,7 @@ Proof.
   iNamed "Hinit".
   iFrame "∗ His_conf #".
   iIntros.
+  iExists _. iFrame "His_conf_prop".
   iPureIntro.
   by apply elem_of_list_fmap_1.
 Qed.

diff --git a/src/program_proof/wal/sliding_proof.v b/src/program_proof/wal/sliding_proof.v
@@ -375,6 +375,7 @@ Proof.
   iIntros "Hb"; iSpecialize ("Hlog" with "Hb").
   iSpecialize ("Hlog_mutable" with "Hlog").
   iSplit; auto.
+  iExists _, _; iFrame "∗#".
 Qed.
 
 Theorem addrPosMap_lookup_inv σ pos :
+2 −0		src/coqutil/Byte.v
+90 −2		src/coqutil/Datatypes/List.v
+242 −4		src/coqutil/Datatypes/ListSet.v
+88 −0		src/coqutil/Datatypes/PropSet.v
+52 −1		src/coqutil/Datatypes/String.v
+51 −0		src/coqutil/Datatypes/ZList.v
+70 −0		src/coqutil/Map/Domain.v
+189 −0		src/coqutil/Map/MapEauto.v
+40 −23		src/coqutil/Map/Properties.v
+1 −14		src/coqutil/Tactics/Simp.v
+9 −0		src/coqutil/Tactics/forward.v
+12 −0		src/coqutil/Tactics/fwd_arith_hints.v
+13 −0		src/coqutil/Tactics/fwd_list_hints.v
+13 −0		src/coqutil/Tactics/invert_hyp.v