move list RA to iris_staging

CHANGELOG.md

@@ -22,6 +22,8 @@ lemma.
   dedicated support from one of the involved maps/APIs. See
   [algebra.dyn_reservation_map](iris/algebra/dyn_reservation_map.v) for further
   information.
+* Demote the Camera structure on `list` to `iris_staging` since its composition
+  is not very well-behaved.
 
 **Changes in `base_logic`:**
 

_CoqProject

@@ -167,6 +167,9 @@ iris_heap_lang/lib/diverge.v
 iris_heap_lang/lib/arith.v
 iris_heap_lang/lib/array.v
 
+iris_staging/algebra/list.v
+iris_staging/base_logic/algebra.v
+
 iris_deprecated/base_logic/auth.v
 iris_deprecated/base_logic/sts.v
 iris_deprecated/base_logic/viewshifts.v

iris/base_logic/algebra.v

@@ -59,14 +59,6 @@ Section list_ofe.
   Proof. uPred.unseal; constructor=> n x ?. apply list_dist_lookup. Qed.
 End list_ofe.
 
-Section list_cmra.
-  Context {A : ucmra}.
-  Implicit Types l : list A.
-
-  Lemma list_validI l : ✓ l ⊣⊢ ∀ i, ✓ (l !! i).
-  Proof. uPred.unseal; constructor=> n x ?. apply list_lookup_validN. Qed.
-End list_cmra.
-
 Section excl.
   Context {A : ofe}.
   Implicit Types a b : A.

iris_staging/base_logic/algebra.v

+(* This is just an integration file for [iris_staging.algebra.list];
+both should be stabilized together. *)
+From iris.algebra Require Import cmra.
+From iris.staging.algebra Require Import list.
+From iris.base_logic Require Import bi derived.
+From iris.prelude Require Import options.
+
+Section upred.
+Context {M : ucmra}.
+
+(* Force implicit argument M *)
+Notation "P ⊢ Q" := (bi_entails (PROP:=uPredI M) P%I Q%I).
+Notation "P ⊣⊢ Q" := (equiv (A:=uPredI M) P%I Q%I).
+
+Section list_cmra.
+  Context {A : ucmra}.
+  Implicit Types l : list A.
+
+  Lemma list_validI l : ✓ l ⊣⊢ ∀ i, ✓ (l !! i).
+  Proof. uPred.unseal; constructor=> n x ?. apply list_lookup_validN. Qed.
+End list_cmra.
+End upred.