Merge branch 'append_list' into 'master'

Append-only list RA

Closes #391

See merge request iris/iris!661

_CoqProject

@@ -170,7 +170,10 @@ iris_heap_lang/lib/arith.v
 iris_heap_lang/lib/array.v
 
 iris_staging/algebra/list.v
+iris_staging/algebra/max_prefix_list.v
+iris_staging/algebra/mono_list.v
 iris_staging/base_logic/algebra.v
+iris_staging/base_logic/mono_list.v
 iris_staging/heap_lang/interpreter.v
 iris_staging/algebra/monotone.v
 

iris_staging/algebra/max_prefix_list.v

+(* This file is still experimental. See its tracking issue
+https://gitlab.mpi-sws.org/iris/iris/-/issues/415 for details on remaining
+issues before stabilization. *)
+From iris.algebra Require Export agree list gmap updates.
+From iris.algebra Require Import local_updates proofmode_classes.
+From iris.prelude Require Import options.
+
+Definition max_prefix_list (A : Type) := gmap nat (agree A).
+Definition max_prefix_listR (A : ofe) := gmapUR nat (agreeR A).
+Definition max_prefix_listUR (A : ofe) := gmapUR nat (agreeR A).
+
+Definition to_max_prefix_list {A} (l : list A) : gmap nat (agree A) :=
+  to_agree <$> map_seq 0 l.
+Instance: Params (@to_max_prefix_list) 1 := {}.
+Typeclasses Opaque to_max_prefix_list.
+
+Section max_prefix_list.
+  Context {A : ofe}.
+  Implicit Types l : list A.
+
+  Global Instance to_max_prefix_list_ne : NonExpansive (@to_max_prefix_list A).
+  Proof. solve_proper. Qed.
+  Global Instance to_max_prefix_list_proper :
+    Proper ((≡) ==> (≡)) (@to_max_prefix_list A).
+  Proof. solve_proper. Qed.
+  Global Instance to_max_prefix_list_dist_inj n :
+    Inj (dist n) (dist n) (@to_max_prefix_list A).
+  Proof.
+    rewrite /to_max_prefix_list. intros l1 l2 Hl. apply list_dist_lookup=> i.
+    move: (Hl i). rewrite !lookup_fmap !lookup_map_seq Nat.sub_0_r.
+    rewrite !option_guard_True; [|lia..].
+    destruct (l1 !! i), (l2 !! i); inversion_clear 1;
+      constructor; by apply (inj to_agree).
+  Qed.
+  Global Instance to_max_prefix_list_inj : Inj (≡) (≡) (@to_max_prefix_list A).
+  Proof.
+    intros l1 l2. rewrite !equiv_dist=> ? n. by apply (inj to_max_prefix_list).
+  Qed.
+
+  Global Instance mono_list_lb_core_id (m : max_prefix_list A) : CoreId m := _.
+
+  Global Lemma to_max_prefix_list_valid l : ✓ to_max_prefix_list l.
+  Proof.
+    intros i. rewrite /to_max_prefix_list lookup_fmap.
+    by destruct (map_seq 0 l !! i).
+  Qed.
+  Global Lemma to_max_prefix_list_validN n l : ✓{n} to_max_prefix_list l.
+  Proof. apply cmra_valid_validN, to_max_prefix_list_valid. Qed.
+
+  Local Lemma to_max_prefix_list_app l1 l2 :
+    to_max_prefix_list (l1 ++ l2) ≡
+    to_max_prefix_list l1 ⋅ (to_agree <$> map_seq (length l1) l2).
+  Proof.
+    rewrite /to_max_prefix_list map_seq_app=> i /=. rewrite lookup_op !lookup_fmap.
+    destruct (map_seq 0 l1 !! i) as [x|] eqn:Hl1; simpl; last first.
+    { by rewrite lookup_union_r // left_id. }
+    rewrite (lookup_union_Some_l _ _ _ x) //=.
+    assert (map_seq (M:=gmap nat A) (length l1) l2 !! i = None) as ->.
+    { apply lookup_map_seq_None.
+      apply lookup_map_seq_Some in Hl1 as [_ ?%lookup_lt_Some]. lia. }
+    by rewrite /= right_id.
+  Qed.
+
+  Lemma to_max_prefix_list_op_l l1 l2 :
+    l1 `prefix_of` l2 →
+    to_max_prefix_list l1 ⋅ to_max_prefix_list l2 ≡ to_max_prefix_list l2.
+  Proof. intros [l ->]. by rewrite to_max_prefix_list_app assoc -core_id_dup. Qed.
+  Lemma to_max_prefix_list_op_r l1 l2 :
+    l1 `prefix_of` l2 →
+    to_max_prefix_list l2 ⋅ to_max_prefix_list l1 ≡ to_max_prefix_list l2.
+  Proof. intros. by rewrite comm to_max_prefix_list_op_l. Qed.
+
+  Lemma max_prefix_list_included_includedN (ml1 ml2 : max_prefix_list A) :
+    ml1 ≼ ml2 ↔ ∀ n, ml1 ≼{n} ml2.
+  Proof.
+    split; [intros; by apply: cmra_included_includedN|].
+    intros Hincl. exists ml2. apply equiv_dist=> n. destruct (Hincl n) as [l ->].
+    by rewrite assoc -core_id_dup.
+  Qed.
+
+  Local Lemma to_max_prefix_list_includedN_aux n l1 l2 :
+    to_max_prefix_list l1 ≼{n} to_max_prefix_list l2 →
+    l2 ≡{n}≡ l1 ++ drop (length l1) l2.
+  Proof.
+    rewrite lookup_includedN=> Hincl. apply list_dist_lookup=> i.
+    rewrite lookup_app. move: (Hincl i).
+    rewrite /to_max_prefix_list !lookup_fmap !lookup_map_seq Nat.sub_0_r.
+    rewrite !option_guard_True; [|lia..].
+    rewrite option_includedN_total fmap_None.
+    intros [Hi|(?&?&(a2&->&->)%fmap_Some&(a1&->&->)%fmap_Some&Ha)].
+    - rewrite lookup_drop Hi. apply lookup_ge_None in Hi. f_equiv; lia.
+    - f_equiv. symmetry. by apply to_agree_includedN.
+  Qed.
+  Lemma to_max_prefix_list_includedN n l1 l2 :
+    to_max_prefix_list l1 ≼{n} to_max_prefix_list l2 ↔ ∃ l, l2 ≡{n}≡ l1 ++ l.
+  Proof.
+    split.
+    - intros. eexists. by apply to_max_prefix_list_includedN_aux.
+    - intros [l ->]. rewrite to_max_prefix_list_app. apply: cmra_includedN_l.
+  Qed.
+  Lemma to_max_prefix_list_included l1 l2 :
+    to_max_prefix_list l1 ≼ to_max_prefix_list l2 ↔ ∃ l, l2 ≡ l1 ++ l.
+  Proof.
+    split.
+    - intros. eexists. apply equiv_dist=> n.
+      apply to_max_prefix_list_includedN_aux. by apply: cmra_included_includedN.
+    - intros [l ->]. rewrite to_max_prefix_list_app. apply: cmra_included_l.
+  Qed.
+  Lemma to_max_prefix_list_included_L `{!LeibnizEquiv A} l1 l2 :
+    to_max_prefix_list l1 ≼ to_max_prefix_list l2 ↔ l1 `prefix_of` l2.
+  Proof. rewrite to_max_prefix_list_included /prefix. naive_solver. Qed.
+
+  Local Lemma to_max_prefix_list_op_validN_aux n l1 l2 :
+    length l1 ≤ length l2 →
+    ✓{n} (to_max_prefix_list l1 ⋅ to_max_prefix_list l2) →
+    l2 ≡{n}≡ l1 ++ drop (length l1) l2.
+  Proof.
+    intros Hlen Hvalid. apply list_dist_lookup=> i. move: (Hvalid i).
+    rewrite /to_max_prefix_list lookup_op !lookup_fmap !lookup_map_seq Nat.sub_0_r.
+    rewrite !option_guard_True; [|lia..].
+    intros ?. rewrite lookup_app.
+    destruct (l1 !! i) as [x1|] eqn:Hi1, (l2 !! i) as [x2|] eqn:Hi2; simpl in *.
+    - f_equiv. symmetry. by apply to_agree_op_validN.
+    - apply lookup_lt_Some in Hi1; apply lookup_ge_None in Hi2. lia.
+    - apply lookup_ge_None in Hi1. rewrite lookup_drop -Hi2. f_equiv; lia.
+    - apply lookup_ge_None in Hi1. rewrite lookup_drop -Hi2. f_equiv; lia.
+  Qed.
+  Lemma to_max_prefix_list_op_validN n l1 l2 :
+    ✓{n} (to_max_prefix_list l1 ⋅ to_max_prefix_list l2) ↔
+    (∃ l, l2 ≡{n}≡ l1 ++ l) ∨ (∃ l, l1 ≡{n}≡ l2 ++ l).
+  Proof.
+    split.
+    - destruct (decide (length l1 ≤ length l2)).
+      + left. eexists. by eapply to_max_prefix_list_op_validN_aux.
+      + right. eexists. eapply to_max_prefix_list_op_validN_aux; [lia|by rewrite comm].
+    - intros [[l ->]|[l ->]].
+      + rewrite to_max_prefix_list_op_l; last by apply prefix_app_r.
+        apply to_max_prefix_list_validN.
+      + rewrite to_max_prefix_list_op_r; last by apply prefix_app_r.
+        apply to_max_prefix_list_validN.
+  Qed.
+  Lemma to_max_prefix_list_op_valid l1 l2 :
+    ✓ (to_max_prefix_list l1 ⋅ to_max_prefix_list l2) ↔
+    (∃ l, l2 ≡ l1 ++ l) ∨ (∃ l, l1 ≡ l2 ++ l).
+  Proof.
+    split.
+    - destruct (decide (length l1 ≤ length l2)).
+      + left. eexists. apply equiv_dist=> n'.
+        by eapply to_max_prefix_list_op_validN_aux, cmra_valid_validN.
+      + right. eexists. apply equiv_dist=> n'.
+        by eapply to_max_prefix_list_op_validN_aux,
+          cmra_valid_validN; [lia|by rewrite comm].
+    - intros [[l ->]|[l ->]].
+      + rewrite to_max_prefix_list_op_l; last by apply prefix_app_r.
+        apply to_max_prefix_list_valid.
+      + rewrite to_max_prefix_list_op_r; last by apply prefix_app_r.
+        apply to_max_prefix_list_valid.
+  Qed.
+  Lemma to_max_prefix_list_op_valid_L `{!LeibnizEquiv A} l1 l2 :
+    ✓ (to_max_prefix_list l1 ⋅ to_max_prefix_list l2) ↔
+    l1 `prefix_of` l2 ∨ l2 `prefix_of` l1.
+  Proof. rewrite to_max_prefix_list_op_valid /prefix. naive_solver. Qed.
+
+  Lemma max_prefix_list_local_update l1 l2 :
+    l1 `prefix_of` l2 →
+    (to_max_prefix_list l1, to_max_prefix_list l1) ~l~>
+      (to_max_prefix_list l2, to_max_prefix_list l2).
+  Proof.
+    intros [l ->]. rewrite to_max_prefix_list_app (comm _ (to_max_prefix_list l1)).
+    apply op_local_update=> n _. rewrite comm -to_max_prefix_list_app.
+    apply to_max_prefix_list_validN.
+  Qed.
+End max_prefix_list.

iris_staging/algebra/mono_list.v

+(* This file is still experimental. See its tracking issue
+https://gitlab.mpi-sws.org/iris/iris/-/issues/415 for details on remaining
+issues before stabilization. *)
+From iris.algebra Require Export auth dfrac.
+From iris.staging.algebra Require Export max_prefix_list.
+From iris.algebra Require Import updates local_updates proofmode_classes.
+From iris.prelude Require Import options.
+
+(** Authoritative CMRA of append-only lists, where the fragment represents a
+  snap-shot of the list, and the authoritative element can only grow by
+  appending. *)
+
+Definition mono_listR (A : ofe) : cmra  := authR (max_prefix_listUR A).
+Definition mono_listUR (A : ofe) : ucmra  := authUR (max_prefix_listUR A).
+
+Definition mono_list_auth {A : ofe} (q : dfrac) (l : list A) : mono_listR A :=
+  ●{q} (to_max_prefix_list l) ⋅ ◯ (to_max_prefix_list l).
+Definition mono_list_lb {A : ofe} (l : list A) : mono_listR A :=
+  ◯ (to_max_prefix_list l).
+Instance: Params (@mono_list_auth) 2 := {}.
+Instance: Params (@mono_list_lb) 1 := {}.
+Typeclasses Opaque mono_list_auth mono_list_lb.
+
+(** FIXME: Refactor these notations using custom entries once Coq bug #13654
+has been fixed. *)
+Notation "●ML{ dq } l" :=
+  (mono_list_auth dq l) (at level 20, format "●ML{ dq }  l").
+Notation "●ML{# q } l" :=
+  (mono_list_auth (DfracOwn q) l) (at level 20, format "●ML{# q }  l").
+Notation "●□ML l" := (mono_list_auth DfracDiscarded l) (at level 20).
+Notation "●ML l" := (mono_list_auth (DfracOwn 1) l) (at level 20).
+Notation "◯ML l" := (mono_list_lb l) (at level 20).
+
+Section mono_list_props.
+  Context {A : ofe}.
+  Implicit Types l : list A.
+  Implicit Types q : frac.
+  Implicit Types dq : dfrac.
+
+  (** Setoid properties *)
+  Global Instance mono_list_auth_ne dq : NonExpansive (@mono_list_auth A dq).
+  Proof. solve_proper. Qed.
+  Global Instance mono_list_auth_proper dq : Proper ((≡) ==> (≡)) (@mono_list_auth A dq).
+  Proof. solve_proper. Qed.
+  Global Instance mono_list_lb_ne : NonExpansive (@mono_list_lb A).
+  Proof. solve_proper. Qed.
+  Global Instance mono_list_lb_proper : Proper ((≡) ==> (≡)) (@mono_list_lb A).
+  Proof. solve_proper. Qed.
+
+  Global Instance mono_list_lb_dist_inj n : Inj (dist n) (dist n) (@mono_list_lb A).
+  Proof. rewrite /mono_list_lb. by intros ?? ?%(inj _)%(inj _). Qed.
+  Global Instance mono_list_lb_inj : Inj (≡) (≡) (@mono_list_lb A).
+  Proof. rewrite /mono_list_lb. by intros ?? ?%(inj _)%(inj _). Qed.
+
+  (** * Operation *)
+  Global Instance mono_list_lb_core_id l : CoreId (◯ML l).
+  Proof. rewrite /mono_list_lb. apply _. Qed.
+
+  Lemma mono_list_auth_dfrac_op dq1 dq2 l :
+    ●ML{dq1 ⋅ dq2} l ≡ ●ML{dq1} l ⋅ ●ML{dq2} l.
+  Proof.
+    rewrite /mono_list_auth auth_auth_dfrac_op.
+    rewrite (comm _ (●{dq2} _)) -!assoc (assoc _ (◯ _)).
+    by rewrite -core_id_dup (comm _ (◯ _)).
+  Qed.
+  Lemma mono_list_auth_frac_op q1 q2 l :
+    ●ML{#(q1 + q2)} l ≡ ●ML{#q1} l ⋅ ●ML{#q2} l.
+  Proof. by rewrite -mono_list_auth_dfrac_op dfrac_op_own. Qed.
+
+  Lemma mono_list_lb_op_l l1 l2 : l1 `prefix_of` l2 → ◯ML l1 ⋅ ◯ML l2 ≡ ◯ML l2.
+  Proof. intros ?. by rewrite /mono_list_lb -auth_frag_op to_max_prefix_list_op_l. Qed.
+  Lemma mono_list_lb_op_r l1 l2 : l1 `prefix_of` l2 → ◯ML l2 ⋅ ◯ML l1 ≡ ◯ML l2.
+  Proof. intros ?. by rewrite /mono_list_lb -auth_frag_op to_max_prefix_list_op_r. Qed.
+  Lemma mono_list_auth_lb_op dq l : ●ML{dq} l ≡ ●ML{dq} l ⋅ ◯ML l.
+  Proof.
+    by rewrite /mono_list_auth /mono_list_lb -!assoc -auth_frag_op -core_id_dup.
+  Qed.
+
+  Global Instance mono_list_lb_is_op l : IsOp' (◯ML l) (◯ML l) (◯ML l).
+  Proof. by rewrite /IsOp' /IsOp -core_id_dup. Qed.
+
+  (** * Validity *)
+  Lemma mono_list_auth_dfrac_validN n dq l : ✓{n} (●ML{dq} l) ↔ ✓ dq.
+  Proof.
+    rewrite /mono_list_auth auth_both_dfrac_validN.
+    naive_solver apply to_max_prefix_list_validN.
+  Qed.
+  Lemma mono_list_auth_validN n l : ✓{n} (●ML l).
+  Proof. by apply mono_list_auth_dfrac_validN. Qed.
+
+  Lemma mono_list_auth_dfrac_valid dq l : ✓ (●ML{dq} l) ↔ ✓ dq.
+  Proof.
+    rewrite /mono_list_auth auth_both_dfrac_valid.
+    naive_solver apply to_max_prefix_list_valid.
+  Qed.
+  Lemma mono_list_auth_valid l : ✓ (●ML l).
+  Proof. by apply mono_list_auth_dfrac_valid. Qed.
+
+  Lemma mono_list_auth_dfrac_op_validN n dq1 dq2 l1 l2 :
+    ✓{n} (●ML{dq1} l1 ⋅ ●ML{dq2} l2) ↔ ✓ (dq1 ⋅ dq2) ∧ l1 ≡{n}≡ l2.
+  Proof.
+    rewrite /mono_list_auth (comm _ (●{dq2} _)) -!assoc (assoc _ (◯ _)).
+    rewrite -auth_frag_op (comm _ (◯ _)) assoc. split.
+    - move=> /cmra_validN_op_l /auth_auth_dfrac_op_validN.
+      rewrite (inj_iff to_max_prefix_list). naive_solver.
+    - intros [? ->]. rewrite -core_id_dup -auth_auth_dfrac_op auth_both_dfrac_validN.
+      naive_solver apply to_max_prefix_list_validN.
+  Qed.
+  Lemma mono_list_auth_frac_op_validN n q1 q2 l1 l2 :
+    ✓{n} (●ML{#q1} l1 ⋅ ●ML{#q2} l2) ↔ (q1 + q2 ≤ 1)%Qp ∧ l1 ≡{n}≡ l2.
+  Proof. by apply mono_list_auth_dfrac_op_validN. Qed.
+  Lemma mono_list_auth_op_validN n l1 l2 : ✓{n} (●ML l1 ⋅ ●ML l2) ↔ False.
+  Proof. rewrite mono_list_auth_dfrac_op_validN. naive_solver. Qed.
+
+  Lemma mono_list_auth_dfrac_op_valid dq1 dq2 l1 l2 :
+    ✓ (●ML{dq1} l1 ⋅ ●ML{dq2} l2) ↔ ✓ (dq1 ⋅ dq2) ∧ l1 ≡ l2.
+  Proof.
+    rewrite cmra_valid_validN equiv_dist.
+    setoid_rewrite mono_list_auth_dfrac_op_validN. naive_solver eauto using O.
+  Qed.
+  Lemma mono_list_auth_frac_op_valid q1 q2 l1 l2 :
+    ✓ (●ML{#q1} l1 ⋅ ●ML{#q2} l2) ↔ (q1 + q2 ≤ 1)%Qp ∧ l1 ≡ l2.
+  Proof. by apply mono_list_auth_dfrac_op_valid. Qed.
+  Lemma mono_list_auth_op_valid l1 l2 : ✓ (●ML l1 ⋅ ●ML l2) ↔ False.
+  Proof. rewrite mono_list_auth_dfrac_op_valid. naive_solver. Qed.
+
+  Lemma mono_list_auth_dfrac_op_valid_L `{!LeibnizEquiv A} dq1 dq2 l1 l2 :
+    ✓ (●ML{dq1} l1 ⋅ ●ML{dq2} l2) ↔ ✓ (dq1 ⋅ dq2) ∧ l1 = l2.
+  Proof. unfold_leibniz. apply mono_list_auth_dfrac_op_valid. Qed.
+  Lemma mono_list_auth_frac_op_valid_L `{!LeibnizEquiv A} q1 q2 l1 l2 :
+    ✓ (●ML{#q1} l1 ⋅ ●ML{#q2} l2) ↔ (q1 + q2 ≤ 1)%Qp ∧ l1 = l2.
+  Proof. unfold_leibniz. apply mono_list_auth_frac_op_valid. Qed.
+
+  Lemma mono_list_both_dfrac_validN n dq l1 l2 :
+    ✓{n} (●ML{dq} l1 ⋅ ◯ML l2) ↔ ✓ dq ∧ ∃ l, l1 ≡{n}≡ l2 ++ l.
+  Proof.
+    rewrite /mono_list_auth /mono_list_lb -assoc
+      -auth_frag_op auth_both_dfrac_validN -to_max_prefix_list_includedN.
+    f_equiv; split.
+    - intros [Hincl _]. etrans; [apply: cmra_includedN_r|done].
+    - intros. split; [|by apply to_max_prefix_list_validN].
+      rewrite {2}(core_id_dup (to_max_prefix_list l1)). by f_equiv.
+  Qed.
+  Lemma mono_list_both_validN n l1 l2 :
+    ✓{n} (●ML l1 ⋅ ◯ML l2) ↔ ∃ l, l1 ≡{n}≡ l2 ++ l.
+  Proof. rewrite mono_list_both_dfrac_validN. split; [naive_solver|done]. Qed.
+
+  Lemma mono_list_both_dfrac_valid dq l1 l2 :
+    ✓ (●ML{dq} l1 ⋅ ◯ML l2) ↔ ✓ dq ∧ ∃ l, l1 ≡ l2 ++ l.
+  Proof.
+    rewrite /mono_list_auth /mono_list_lb -assoc -auth_frag_op
+      auth_both_dfrac_valid -max_prefix_list_included_includedN
+      -to_max_prefix_list_included.
+    f_equiv; split.
+    - intros [Hincl _]. etrans; [apply: cmra_included_r|done].
+    - intros. split; [|by apply to_max_prefix_list_valid].
+      rewrite {2}(core_id_dup (to_max_prefix_list l1)). by f_equiv.
+  Qed.
+  Lemma mono_list_both_valid l1 l2 :
+    ✓ (●ML l1 ⋅ ◯ML l2) ↔ ∃ l, l1 ≡ l2 ++ l.
+  Proof. rewrite mono_list_both_dfrac_valid. split; [naive_solver|done]. Qed.
+
+  Lemma mono_list_both_dfrac_valid_L `{!LeibnizEquiv A} dq l1 l2 :
+    ✓ (●ML{dq} l1 ⋅ ◯ML l2) ↔ ✓ dq ∧ l2 `prefix_of` l1.
+  Proof. rewrite /prefix. rewrite mono_list_both_dfrac_valid. naive_solver. Qed.
+  Lemma mono_list_both_valid_L `{!LeibnizEquiv A} l1 l2 :
+    ✓ (●ML l1 ⋅ ◯ML l2) ↔ l2 `prefix_of` l1.
+  Proof. rewrite /prefix. rewrite mono_list_both_valid. naive_solver. Qed.
+
+  Lemma mono_list_lb_op_validN n l1 l2 :
+    ✓{n} (◯ML l1 ⋅ ◯ML l2) ↔ (∃ l, l2 ≡{n}≡ l1 ++ l) ∨ (∃ l, l1 ≡{n}≡ l2 ++ l).
+  Proof. by rewrite auth_frag_op_validN to_max_prefix_list_op_validN. Qed.
+  Lemma mono_list_lb_op_valid l1 l2 :
+    ✓ (◯ML l1 ⋅ ◯ML l2) ↔ (∃ l, l2 ≡ l1 ++ l) ∨ (∃ l, l1 ≡ l2 ++ l).
+  Proof. by rewrite auth_frag_op_valid to_max_prefix_list_op_valid. Qed.
+  Lemma mono_list_lb_op_valid_L `{!LeibnizEquiv A} l1 l2 :
+    ✓ (◯ML l1 ⋅ ◯ML l2) ↔ l1 `prefix_of` l2 ∨ l2 `prefix_of` l1.
+  Proof. rewrite mono_list_lb_op_valid / prefix. naive_solver. Qed.
+
+  Lemma mono_list_lb_op_valid_1_L `{!LeibnizEquiv A} l1 l2 :
+    ✓ (◯ML l1 ⋅ ◯ML l2) → l1 `prefix_of` l2 ∨ l2 `prefix_of` l1.
+  Proof. by apply mono_list_lb_op_valid_L. Qed.
+  Lemma mono_list_lb_op_valid_2_L `{!LeibnizEquiv A} l1 l2 :
+    l1 `prefix_of` l2 ∨ l2 `prefix_of` l1 → ✓ (◯ML l1 ⋅ ◯ML l2).
+  Proof. by apply mono_list_lb_op_valid_L. Qed.
+
+  Lemma mono_list_lb_mono l1 l2 : l1 `prefix_of` l2 → ◯ML l1 ≼ ◯ML l2.
+  Proof. intros. exists (◯ML l2). by rewrite mono_list_lb_op_l. Qed.
+
+  Lemma mono_list_included dq l : ◯ML l ≼ ●ML{dq} l.
+  Proof. apply cmra_included_r. Qed.
+
+  (** * Update *)
+  Lemma mono_list_update {l1} l2 : l1 `prefix_of` l2 → ●ML l1 ~~> ●ML l2.
+  Proof. intros ?. by apply auth_update, max_prefix_list_local_update. Qed.
+  Lemma mono_list_update_auth_persist dq l : ●ML{dq} l ~~> ●□ML l.
+  Proof.
+    rewrite /mono_list_auth. apply cmra_update_op; [|done].
+    by apply auth_update_auth_persist.
+  Qed.
+End mono_list_props.

iris_staging/base_logic/mono_list.v

+(* This file is still experimental. See its tracking issue
+https://gitlab.mpi-sws.org/iris/iris/-/issues/415 for details on remaining
+issues before stabilization. *)
+(** Ghost state for a append-only list, wrapping the [mono_listR] RA. This
+  provides three assertions:
+  - an authoritative proposition [mono_list_auth_own γ q l] for the authoritative
+    list [l]
+  - a persistent assertion [mono_list_lb_own γ l] witnessing that the authoritative
+    list is at least [l]
+  - a persistent assertion [mono_list_idx_own γ i a] witnessing that the index [i]
+    is [a] in the authoritative list.
+
+The key rules are [mono_list_lb_own_valid], which asserts that an auth at [l]
+and a lower-bound at [l'] imply that [l' `prefix_of` l], and [mono_list_update],
+which allows one to grow the auth element by appending only. At any time the
+auth list can be "snapshotted" with [mono_list_lb_own_get] to produce a
+persistent lower-bound. *)
+From iris.proofmode Require Import tactics.
+From iris.staging.algebra Require Import mono_list.
+From iris.bi.lib Require Import fractional.
+From iris.base_logic.lib Require Export own.
+From iris.prelude Require Import options.
+
+Class mono_listG (A : Type) Σ :=
+  MonoListG { mono_list_inG :> inG Σ (mono_listR (leibnizO A)) }.
+Definition mono_listΣ (A : Type) : gFunctors :=
+  #[GFunctor (mono_listR (leibnizO A))].
+
+Global Instance subG_mono_listΣ {A Σ} :
+  subG (mono_listΣ A) Σ → (mono_listG A) Σ.
+Proof. solve_inG. Qed.
+
+Definition mono_list_auth_own_def `{!mono_listG A Σ}
+    (γ : gname) (q : Qp) (l : list A) : iProp Σ :=
+  own γ (●ML{#q} (l : listO (leibnizO A))).
+Definition mono_list_auth_own_aux : seal (@mono_list_auth_own_def). Proof. by eexists. Qed.
+Definition mono_list_auth_own := mono_list_auth_own_aux.(unseal).
+Definition mono_list_auth_own_eq :
+  @mono_list_auth_own = @mono_list_auth_own_def := mono_list_auth_own_aux.(seal_eq).
+Global Arguments mono_list_auth_own {A Σ _} γ q l.
+
+Definition mono_list_lb_own_def `{!mono_listG A Σ}
+    (γ : gname) (l : list A) : iProp Σ :=
+  own γ (◯ML (l : listO (leibnizO A))).
+Definition mono_list_lb_own_aux : seal (@mono_list_lb_own_def). Proof. by eexists. Qed.
+Definition mono_list_lb_own := mono_list_lb_own_aux.(unseal).
+Definition mono_list_lb_own_eq :
+  @mono_list_lb_own = @mono_list_lb_own_def := mono_list_lb_own_aux.(seal_eq).
+Global Arguments mono_list_lb_own {A Σ _} γ l.
+
+Definition mono_list_idx_own `{!mono_listG A Σ}
+    (γ : gname) (i : nat) (a : A) : iProp Σ :=
+  ∃ l : list A, ⌜ l !! i = Some a ⌝ ∗ mono_list_lb_own γ l.
+
+Local Ltac unseal := rewrite
+  /mono_list_idx_own ?mono_list_auth_own_eq /mono_list_auth_own_def
+  ?mono_list_lb_own_eq /mono_list_lb_own_def.
+
+Section mono_list_own.
+  Context `{!mono_listG A Σ}.
+  Implicit Types (l : list A) (i : nat) (a : A).
+
+  Global Instance mono_list_auth_own_timeless γ q l : Timeless (mono_list_auth_own γ q l).
+  Proof. unseal. apply _. Qed.
+  Global Instance mono_list_lb_own_timeless γ l : Timeless (mono_list_lb_own γ l).
+  Proof. unseal. apply _. Qed.
+  Global Instance mono_list_lb_own_persistent γ l : Persistent (mono_list_lb_own γ l).
+  Proof. unseal. apply _. Qed.
+  Global Instance mono_list_idx_own_timeless γ i a :
+    Timeless (mono_list_idx_own γ i a) := _.
+  Global Instance mono_list_idx_own_persistent γ i a :
+    Persistent (mono_list_idx_own γ i a) := _.
+
+  Global Instance mono_list_auth_own_fractional γ l :
+    Fractional (λ q, mono_list_auth_own γ q l).
+  Proof. unseal. intros p q. by rewrite -own_op mono_list_auth_frac_op. Qed.
+  Global Instance mono_list_auth_own_as_fractional γ q l :
+    AsFractional (mono_list_auth_own γ q l) (λ q, mono_list_auth_own γ q l) q.
+  Proof. split; [auto|apply _]. Qed.
+
+  Lemma mono_list_auth_own_agree γ q1 q2 l1 l2 :
+    mono_list_auth_own γ q1 l1 -∗
+    mono_list_auth_own γ q2 l2 -∗
+    ⌜(q1 + q2 ≤ 1)%Qp ∧ l1 = l2⌝.
+  Proof.
+    unseal. iIntros "H1 H2".
+    by iDestruct (own_valid_2 with "H1 H2") as %?%mono_list_auth_frac_op_valid_L.
+  Qed.
+  Lemma mono_list_auth_own_exclusive γ l1 l2 :
+    mono_list_auth_own γ 1 l1 -∗ mono_list_auth_own γ 1 l2 -∗ False.
+  Proof.
+    iIntros "H1 H2".
+    iDestruct (mono_list_auth_own_agree with "H1 H2") as %[]; done.
+  Qed.
+
+  Lemma mono_list_auth_lb_valid γ q l1 l2 :
+    mono_list_auth_own γ q l1 -∗
+    mono_list_lb_own γ l2 -∗
+    ⌜ (q ≤ 1)%Qp ∧ l2 `prefix_of` l1 ⌝.
+  Proof.
+    unseal. iIntros "Hauth Hlb".
+    by iDestruct (own_valid_2 with "Hauth Hlb") as %?%mono_list_both_dfrac_valid_L.
+  Qed.
+
+  Lemma mono_list_lb_valid γ l1 l2 :
+    mono_list_lb_own γ l1 -∗
+    mono_list_lb_own γ l2 -∗
+    ⌜ l1 `prefix_of` l2 ∨ l2 `prefix_of` l1 ⌝.
+  Proof.
+    unseal. iIntros "H1 H2".
+    by iDestruct (own_valid_2 with "H1 H2") as %?%mono_list_lb_op_valid_L.
+  Qed.
+
+  Lemma mono_list_idx_agree γ i a1 a2 :
+    mono_list_idx_own γ i a1 -∗ mono_list_idx_own γ i a2 -∗ ⌜ a1 = a2 ⌝.
+  Proof.
+    iDestruct 1 as (l1 Hl1) "H1". iDestruct 1 as (l2 Hl2) "H2".
+    iDestruct (mono_list_lb_valid with "H1 H2") as %Hpre.
+    iPureIntro.
+    destruct Hpre as [Hpre|Hpre]; eapply prefix_lookup in Hpre; eauto; congruence.
+  Qed.
+
+  Lemma mono_list_auth_idx_lookup γ q l i a :
+    mono_list_auth_own γ q l -∗ mono_list_idx_own γ i a -∗ ⌜ l !! i = Some a ⌝.
+  Proof.
+    iIntros "Hauth". iDestruct 1 as (l1 Hl1) "Hl1".
+    iDestruct (mono_list_auth_lb_valid with "Hauth Hl1") as %[_ Hpre].
+    iPureIntro.
+    eapply prefix_lookup in Hpre; eauto; congruence.
+  Qed.
+
+  Lemma mono_list_lb_own_get γ q l :
+    mono_list_auth_own γ q l -∗ mono_list_lb_own γ l.
+  Proof. intros. unseal. by apply own_mono, mono_list_included. Qed.
+  Lemma mono_list_lb_own_le {γ l} l' :
+    l' `prefix_of` l →
+    mono_list_lb_own γ l -∗ mono_list_lb_own γ l'.
+  Proof. unseal. intros. by apply own_mono, mono_list_lb_mono. Qed.
+
+  Lemma mono_list_idx_own_get {γ l} i a :
+    l !! i = Some a →
+    mono_list_lb_own γ l -∗ mono_list_idx_own γ i a.
+  Proof. iIntros (Hli) "Hl". iExists l. by iFrame. Qed.