multicounter.v

From stdpp Require Import list.
From iris.algebra Require Import excl numbers gmap.
From iris.base_logic Require Export invariants saved_prop.
From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang proofmode notation.

(* move *)
Lemma list_sum_replicate n m : list_sum (replicate n m) = n * m.
Proof.
  revert m; induction n as [|n IHn]; first done; intros ?; rewrite /= IHn; lia.
Qed.

Lemma list_sum_le l1 l2 : Forall2 (≤) l1 l2 → list_sum l1 ≤ list_sum l2.
Proof.
  revert l2; induction l1 as [|x l1 IHl1]; first by inversion 1.
  intros [|y l2]; first by inversion 1.
  inversion 1 as [|????? Hfa2]; simplify_eq.
  specialize (IHl1 l2 Hfa2); simpl; lia.
Qed.

(* end of move *)

Definition new_counter: val := λ: "n", AllocN "n" #0.

Definition incr: val := λ: "c" "i", FAA ("c" +ₗ "i") #1;; #().

Definition read_aux: val :=
  rec: "read_aux" "proph" "acc" "c" "n" :=
    if: "n" = #0 then "acc" else
      let: "x" := Resolve !"c" "proph" #() in
      "read_aux" "proph" ("acc" + "x") ("c" +ₗ #1) ("n" - #1).

Definition read: val :=
  λ: "c" "n", let: "p" := NewProph in read_aux "p" #0 "c" "n".

Section proof.
  Record counter_data := CData {
    c_len : nat;
    c_exact : gname;
    c_lowers : list gname;
    c_read_ops : gname
  }.

  Global Instance counter_data_eq_dec : EqDecision counter_data.
  Proof. solve_decision. Qed.
  Global Program Instance counter_data_countable : Countable counter_data :=
    inj_countable' (λ cd, (cd.(c_len), cd.(c_exact), cd.(c_lowers), cd.(c_read_ops)))
      (λ p, {|c_len := p.1.1.1; c_exact := p.1.1.2; c_lowers := p.1.2; c_read_ops := p.2 |}) _.
  Next Obligation.
  Proof. intros []; done. Qed.

  Global Instance: Inhabited counter_data := populate (CData inhabitant inhabitant inhabitant inhabitant).

  Record read_data := RData {
    r_start : nat;
    r_proph : proph_id;
    r_final : nat;
    r_uppers : list gname;
    r_reads : gname;
    r_pred : gname;
  }.

  Notation read_dataO := (leibnizO read_data).

Global Instance: Inhabited read_data :=
  populate (RData inhabitant inhabitant inhabitant inhabitant inhabitant inhabitant).

  Context `{!heapGS Σ}.
  Context `{!inG Σ (authUR (optionUR (exclR nat)))}.
  Context `{!inG Σ (authUR natO)}.
  Context `{!inG Σ (authUR max_natUR)}.
  Context `{!inG Σ (authUR (optionUR min_natR))}.
  Context `{!inG Σ (authUR (optionUR (exclR (list nat))))}.
  Context `{!savedPredG Σ nat}.

  Context `{!inG Σ (authUR (gmapUR nat (agreeR read_dataO)))}.

  Definition CName := nroot .@ "counter".

  Definition cdata c (cd : counter_data) : iProp Σ :=
    ∃ (l : loc), ⌜c = #l⌝ ∗ meta l nroot cd.

  Definition Counter_full (c : val) (n : nat) : iProp Σ :=
    ∃ cd, cdata c cd ∗ own cd.(c_exact) (● Excl' n).
  Definition Counter_frag (c : val) (n : nat) : iProp Σ :=
    ∃ cd, cdata c cd ∗ own cd.(c_exact) (◯ Excl' n).

  Definition ReadOps_full γrdops (M : gmap nat read_data) : iProp Σ :=
    own γrdops (● (to_agree <$> M : gmapUR nat (agreeR read_dataO))).
  Definition ReadOp_frag γrdops rid rd : iProp Σ :=
    own γrdops (◯ {[ rid := to_agree rd]}).

  Definition read_seq_full γ reads := own γ (● Excl' reads).
  Definition read_seq_frag γ reads := own γ (◯ Excl' reads).

  Definition val_to_nat (v : val) : nat :=
    match v with
    | LitV (LitInt z) => Z.to_nat z
    | _ => 0
    end.

  Definition prophecy_to_nats (vs : list (val * val)) : list nat :=
    val_to_nat ∘ fst <$> vs.

  Definition lists_sum_is l1 l2 s := list_sum l1 + list_sum l2 = s.

  Definition read_uppers_maintained start names reads cnts : iProp Σ :=
    ∃ start_cnts,
      ⌜list_sum start_cnts = start⌝ ∗
      ([∗ list] γ; k ∈ names; start_cnts, own γ (● Some (MinNat k))) ∗
      ([∗ list] γ; k ∈ names; cnts, own γ (◯ Some (MinNat k))) ∗
      ([∗ list] i ↦ k ∈ reads, ∃ γ, ⌜names !! i = Some γ⌝ ∗ own γ (◯ Some (MinNat k))).

  Definition linearization_point c rd cnts pred : iProp Σ :=
    (⌜rd.(r_start) ≤ rd.(r_final)⌝ -∗
       if bool_decide (list_sum cnts < rd.(r_final)) then
         ∀ k, Counter_full c k ={⊤ ∖ ↑CName}=∗
              Counter_full c k ∗ (pred k)
       else
         pred rd.(r_final) ∨ ∃ reads, read_seq_frag rd.(r_reads) reads)%I.

  Definition read_state_inv c rid cnts : iProp Σ :=
    ∃ rd cd pred (reads : list nat) pvs,
      cdata c cd ∗
      ReadOp_frag cd.(c_read_ops) rid rd ∗
      saved_pred_own rd.(r_pred) DfracDiscarded pred ∗
      read_seq_full rd.(r_reads) reads ∗
      ([∗ list] i ↦ k ∈ reads,
        ∃ γ, ⌜cd.(c_lowers) !! i = Some γ⌝ ∗ own γ (◯ MaxNat k)) ∗
      read_uppers_maintained rd.(r_start) rd.(r_uppers) reads cnts ∗
      proph rd.(r_proph) pvs ∗
      ⌜lists_sum_is reads (prophecy_to_nats (take (cd.(c_len) - length reads) pvs)) rd.(r_final)⌝ ∗
      linearization_point c rd cnts pred.

  Definition all_read_ops c cd M cnts : iProp Σ :=
    cdata c cd ∗ ReadOps_full cd.(c_read_ops) M ∗ [∗ set] rid ∈ dom M, read_state_inv c rid cnts.

  Definition read_state_local c rid p reads final pred : iProp Σ :=
    ∃ rd cd,
      ⌜rd.(r_proph) = p⌝ ∗
      ⌜rd.(r_final) = final⌝ ∗
      cdata c cd ∗
      ReadOp_frag cd.(c_read_ops) rid rd ∗
      saved_pred_own rd.(r_pred) DfracDiscarded pred ∗
      read_seq_frag rd.(r_reads) reads.

  Definition counter_inv c cd : iProp Σ :=
    ∃ (l : loc) cnts M,
      ⌜c = #l⌝ ∗
      cdata c cd ∗
      Counter_full c (list_sum cnts) ∗
      ⌜length cnts = cd.(c_len)⌝ ∧
      l ↦∗ ((λ k : nat, #k) <$> cnts) ∗
      ([∗ list] k; γlwr ∈ cnts; cd.(c_lowers), own γlwr (● (MaxNat k))) ∗
      all_read_ops c cd M cnts.

  Definition is_counter c : iProp Σ := ∃ cd, inv CName (counter_inv c cd).

(* Lemmas *)

  Lemma ReadOps_init : ⊢ |==> ∃ γ, ReadOps_full γ ∅.
  Proof. iApply own_alloc; rewrite fmap_empty; apply auth_auth_valid; done. Qed.

  Lemma ReadOps_alloc γ M rd :
    ReadOps_full γ M ==∗ ∃ rid, ⌜rid ∉ dom M⌝ ∗ ReadOps_full γ ({[rid := rd]} ∪ M) ∗ ReadOp_frag γ rid rd.
  Proof.
    iIntros "HM".
    iMod (own_update _ _ (● (to_agree <$> ({[fresh (dom M) := rd]} ∪ M) : gmapUR nat (agreeR read_dataO)) ⋅
                            ◯ {[fresh (dom M) := to_agree rd]}) with "HM") as "[HM Hrid]".
    { apply auth_update_alloc.
      rewrite map_fmap_union map_fmap_singleton -insert_union_singleton_l.
      eapply @alloc_singleton_local_update; last done.
      apply not_elem_of_dom_1.
      rewrite dom_fmap.
      apply is_fresh. }
    iExists _; iFrame.
    iModIntro; iPureIntro; apply is_fresh.
  Qed.

  Lemma ReadOps_lookup γ M rid rd :
    ReadOps_full γ M -∗ ReadOp_frag γ rid rd -∗ ⌜M !! rid = Some rd⌝.
  Proof.
    iIntros "HM Hrid".
    iDestruct (own_valid_2 with "HM Hrid") as %[Hincl _]%auth_both_valid_discrete.
    apply singleton_included_l in Hincl as [rd' [Hrd'1 Hrd'2]].
    rewrite lookup_fmap in Hrd'1.
    destruct lookup; last by inversion Hrd'1.
    rewrite -Hrd'1 /= in Hrd'2.
    apply Some_included_1 in Hrd'2 as [Hrd'2|Hrd'2].
    - apply to_agree_inj, leibniz_equiv in Hrd'2; simplify_eq; done.
    - apply to_agree_included, leibniz_equiv in Hrd'2; simplify_eq; done.
  Qed.

  Lemma ReadOps_agree γ rid rd rd' : ReadOp_frag γ rid rd -∗ ReadOp_frag γ rid rd' -∗ ⌜rd = rd'⌝.
  Proof.
    iIntros "Hrid1 Hrid2".
    iDestruct (own_valid_2 with "Hrid1 Hrid2") as %Hvl.
    rewrite -auth_frag_op auth_frag_valid in Hvl.
    specialize (Hvl rid).
    rewrite lookup_op !lookup_singleton -Some_op in Hvl.
    apply to_agree_op_inv_L in Hvl; done.
  Qed.

  Lemma read_seq_init reads : ⊢ |==> ∃ γ, read_seq_full γ reads ∗ read_seq_frag γ reads.
  Proof.
    rewrite /read_seq_full /read_seq_frag; setoid_rewrite <- own_op.
    iApply own_alloc; apply auth_both_valid; done.
  Qed.

  Lemma read_seq_agree γ reads reads' : read_seq_full γ reads -∗ read_seq_frag γ reads' -∗ ⌜reads = reads'⌝.
  Proof.
    iIntros "Hfl Hfr".
    iDestruct (own_valid_2 with "Hfl Hfr") as %[Hvl _]%auth_both_valid_discrete.
    apply Excl_included, leibniz_equiv in Hvl; done.
  Qed.

  Lemma read_seq_frag_unique γ reads reads' : read_seq_frag γ reads -∗ read_seq_frag γ reads' -∗ False.
  Proof.
    iIntros "Hfl Hfr".
    iDestruct (own_valid_2 with "Hfl Hfr") as %Hvl.
    rewrite auth_frag_valid /= in Hvl; done.
  Qed.

  Lemma read_seq_update γ reads reads' :
    read_seq_full γ reads -∗ read_seq_frag γ reads ==∗ read_seq_full γ reads' ∗ read_seq_frag γ reads'.
  Proof.
    iIntros "Hfl Hfr".
    iMod (own_update_2 _ _ _ (● _ ⋅ ◯ _) with "Hfl Hfr") as "[Hfl Hfr]"; last by iFrame.
    apply auth_update.
    apply option_local_update.
    apply exclusive_local_update; done.
  Qed.

  Lemma cdata_agree c cd cd' : cdata c cd -∗ cdata c cd' -∗ ⌜cd = cd'⌝.
  Proof.
    iDestruct 1 as (? ->) "H1"; iDestruct 1 as (? ?) "H2"; simplify_eq.
    iApply (meta_agree with "H1 H2").
  Qed.

  Lemma Counter_agree c n m : Counter_full c n -∗ Counter_frag c m -∗ ⌜n = m⌝.
  Proof.
    iDestruct 1 as (?) "[#Hcd Hfl]".
    iDestruct 1 as (?) "[#Hcd' Hfr]".
    iDestruct (cdata_agree with "Hcd Hcd'") as %?; simplify_eq.
    iDestruct (own_valid_2 with "Hfl Hfr") as %Hvl.
    apply auth_both_valid_discrete in Hvl as
        [?%Excl_included%leibniz_equiv _]; done.
  Qed.

  Lemma Counter_update c n m : Counter_full c n -∗ Counter_frag c n ==∗ Counter_full c m ∗ Counter_frag c m.
  Proof.
    iDestruct 1 as (?) "[#Hcd Hfl]".
    iDestruct 1 as (?) "[#Hcd' Hfr]".
    iDestruct (cdata_agree with "Hcd Hcd'") as %?; simplify_eq.
    iMod (own_update_2 _ _ _ (● Excl' m ⋅ ◯ Excl' m) with "Hfl Hfr") as "[Hfl Hfr]".
    { apply auth_update, option_local_update, exclusive_local_update; done. }
    iModIntro; iSplitL "Hfl"; iExists _; iFrame; done.
  Qed.

  Lemma linearization_point_incr c rd cnts1 cnt cnts2 pred :
    Counter_full c (list_sum (cnts1 ++ cnt + 1 :: cnts2)) ∗
    linearization_point c rd (cnts1 ++ cnt :: cnts2) pred ={⊤ ∖ ↑CName}=∗
      Counter_full c (list_sum (cnts1 ++ cnt + 1 :: cnts2)) ∗
      linearization_point c rd (cnts1 ++ cnt + 1 :: cnts2) pred.
  Proof.
    rewrite /linearization_point; iIntros "[Hc H]".
    destruct (decide (rd.(r_start) ≤ rd.(r_final))); last by iModIntro; iFrame; iIntros "%".
    iSpecialize ("H" with "[//]").
    replace (list_sum (cnts1 ++ cnt + 1 :: cnts2)) with (list_sum (cnts1 ++ cnt :: cnts2) + 1)
      by by rewrite !list_sum_app /=; lia.
    destruct (decide (list_sum (cnts1 ++ cnt :: cnts2) < r_final rd)).
    - rewrite bool_decide_eq_true_2; last done.
      destruct (decide (list_sum (cnts1 ++ cnt :: cnts2) + 1 < r_final rd)).
      + rewrite bool_decide_eq_true_2; last done.
        iModIntro; iFrame; done.
      + assert (list_sum (cnts1 ++ cnt :: cnts2) + 1 = r_final rd) as -> by lia.
        iMod ("H" with "Hc") as "[Hc Hpred]".
        iModIntro; iFrame.
        iIntros "_".
        rewrite bool_decide_eq_false_2; last lia; eauto.
    - repeat (rewrite bool_decide_eq_false_2; last lia).
      iModIntro; iFrame; done.
  Qed.

  Lemma read_uppers_maintained_incr start names reads cnts1 cnt cnts2 :
    read_uppers_maintained start names reads (cnts1 ++ cnt :: cnts2) -∗
     read_uppers_maintained start names reads (cnts1 ++ cnt + 1 :: cnts2).
  Proof.
    iDestruct 1 as (start_cnts) "(? & HFull & Hfrag & Hreads)".
    iExists _; iFrame.
    iDestruct (big_sepL2_app_inv_r with "Hfrag") as (?? ->) "[$ Hfr2]".
    iDestruct (big_sepL2_cons_inv_r with "Hfr2") as (?? ->) "[Hfr $]"; simpl.
    assert ((MinNat cnt) = (MinNat cnt) ⋅ (MinNat (cnt + 1))) as ->
        by by rewrite min_nat_op_min; f_equal; lia.
    rewrite Some_op auth_frag_op own_op.
    iDestruct "Hfr" as "[_ $]".
  Qed.

  Lemma make_read_uppers_maintained cnts :
    ⊢ |==> ∃ names, read_uppers_maintained (list_sum cnts) names [] cnts.
  Proof.
    rewrite /read_uppers_maintained /=.
    iInduction cnts as [|cnt cnts] "IH".
    { iExists [], []; simpl; eauto. }
    iMod "IH" as (names start_cnts Hsums) "(Hmins & Hcnts & _)".
    iMod (own_alloc (● Some (MinNat cnt) ⋅
      ◯ Some (MinNat cnt))) as (γ) "[Hfl Hfr]";
      first by apply auth_both_valid.
    iModIntro.
    iExists (γ :: names), (cnt :: start_cnts); simpl; iFrame; auto with lia.
  Qed.

  Lemma read_uppers_maintained_progress start names reads n cnts :
    cnts !! length reads = Some n →
    read_uppers_maintained start names reads cnts -∗
     read_uppers_maintained start names (reads ++ [n]) cnts.
  Proof.
    intros Hlu.
    iDestruct 1 as (start_cnts) "(? & HFull & Hfrag & Hreads)".
    iDestruct (big_sepL2_length with "Hfrag") as %?.
    pose proof Hlu as ?%lookup_lt_Some.
    destruct (lookup_lt_is_Some_2 names (length reads)) as [γ Hγ]; first lia.
    iDestruct (big_sepL2_lookup_acc _ _ _ (length reads) with "Hfrag") as "[#Hγ Hrest]"; [done|done|].
    iDestruct ("Hrest" with  "[$]") as "Hfrag".
    iExists _; iFrame.
    iSplit; last done.
    replace (length reads + 0) with (length reads) by lia.
    iExists _; iSplit; done.
  Qed.

  Lemma read_uppers_maintained_done start names reads cnts :
    length cnts = length reads →
    read_uppers_maintained start names reads cnts -∗ ⌜start ≤ list_sum reads⌝.
  Proof.
    intros Hlen.
    iDestruct 1 as (start_cnts) "(<- & HFull & Hfrag & Hreads)".
    iAssert (⌜∀ i, option_Forall2 (≤) (start_cnts !! i) (reads !! i)⌝)%I as %?;
      last first.
    { iPureIntro; apply list_sum_le, Forall2_lookup; done. }
    iIntros (i).
    iDestruct (big_sepL2_length with "HFull") as %?.
    iDestruct (big_sepL2_length with "Hfrag") as %?.
    destruct (reads !! i) eqn:Hreadsi.
    - iDestruct (big_sepL_lookup with "Hreads") as (γ Hγ) "Hfr"; first done.
      pose proof Hγ as ?%lookup_lt_Some.
      destruct (lookup_lt_is_Some_2 start_cnts i) as [s Hs]; first lia.
      rewrite Hs.
      iDestruct (big_sepL2_lookup with "HFull") as "Hfl"; [done|done|].
      iDestruct (own_valid_2 with "Hfl Hfr")
        as %[Hincl _]%auth_both_valid_discrete.
      apply Some_included_1 in Hincl as [Hincl|Hincl].
      { apply leibniz_equiv in Hincl; simplify_eq; eauto. }
      destruct Hincl as [[] Hincl%leibniz_equiv].
      rewrite min_nat_op_min in Hincl.
      simplify_eq.
      iPureIntro; constructor; lia.
    - pose proof Hreadsi as ?%lookup_ge_None_1.
      rewrite (lookup_ge_None_2 start_cnts i); [done|lia].
  Qed.

  Lemma read_state_inv_incr c rid cnts1 cnt cnts2 :
    Counter_full c (list_sum (cnts1 ++ cnt + 1 :: cnts2)) -∗
    read_state_inv c rid (cnts1 ++ cnt :: cnts2) ={⊤ ∖ ↑CName}=∗
    Counter_full c (list_sum (cnts1 ++ cnt + 1 :: cnts2)) ∗
    read_state_inv c rid (cnts1 ++ cnt + 1 :: cnts2).
  Proof.
    iIntros "Hcn Hrsi".
    iDestruct "Hrsi" as (rd cd pred reads pvs)
      "(#Hmeta & #Hfr & #Hspred & Hrds & Hrdsmax & Huppers & Hproph & Hfin & Hlp)".
    iDestruct (read_uppers_maintained_incr with "Huppers") as "Huppers".
    iMod (linearization_point_incr with "[$Hcn $Hlp]") as "[$ Hlp]".
    iModIntro; iExists _, _, _, _, _; iSplit; iFrame "#"; iFrame; done.
  Qed.

  Lemma all_read_ops_incr c cd M cnts1 cnt cnts2 :
    Counter_full c (list_sum (cnts1 ++ cnt + 1 :: cnts2)) -∗
    all_read_ops c cd M (cnts1 ++ cnt :: cnts2) ={⊤ ∖ ↑CName}=∗
    Counter_full c (list_sum (cnts1 ++ cnt + 1 :: cnts2)) ∗
    all_read_ops c cd M (cnts1 ++ cnt + 1 :: cnts2).
  Proof.
    rewrite /all_read_ops.
    iIntros "Hcn (#Hcd & HM & Hrsis)".
    iInduction (dom M) as [|rid D] "IH" using set_ind_L.
    { rewrite !big_sepS_empty; iFrame; done. }
    rewrite !big_sepS_insert //; [].
    iDestruct "Hrsis" as "[Hrsi Hrsis]".
    iMod ("IH" with "Hcn HM Hrsis") as "(Hcn & HM & Hrsis)".
    iMod (read_state_inv_incr with "Hcn Hrsi") as "[Hcn Hrsi]".
    iFrame; done.
  Qed.

  Lemma make_read_state pred p pvs c cd M cnts :
    Counter_full c (list_sum cnts) -∗
    (∀ k, Counter_full c k ={⊤ ∖ ↑CName}=∗ Counter_full c k ∗ (pred k)) -∗
    ▷ all_read_ops c cd M cnts -∗ proph p pvs ={⊤ ∖ ↑CName}=∗
    ∃ rid rd, ⌜rid ∉ dom M⌝ ∗ Counter_full c (list_sum cnts) ∗
      ▷ all_read_ops c cd ({[rid := rd]} ∪ M) cnts ∗ read_state_local c rid p [] rd.(r_final) pred.
  Proof.
    iIntros "Hfull Hreadupd [#>Hcd [>HM Hrsis]] Hp".
    rewrite /ReadOps_full.
    iMod (saved_pred_alloc pred DfracDiscarded) as (γpred) "#Hpred"; first done.
    iMod (read_seq_init []) as (γreads) "[Hrdfl Hrdsfr]".
    iMod (make_read_uppers_maintained cnts) as (γuppers) "Hrum".
    set (rd := RData (list_sum cnts) p
                 (list_sum (prophecy_to_nats ((take cd.(c_len)) pvs))) γuppers γreads γpred).
    iMod (ReadOps_alloc with "HM") as (rid ?) "[HM #Hrid]".
    iAssert (|={⊤ ∖ ↑CName}=> Counter_full c (list_sum cnts) ∗
      linearization_point c rd cnts pred)%I with "[Hfull Hreadupd]" as ">[Hfull Hlp]".
    { rewrite /linearization_point.
      destruct (decide (list_sum cnts ≤ rd.(r_final))); last by iFrame;
        iModIntro; iIntros "%".
      destruct (decide (list_sum cnts < rd.(r_final))).
      - iModIntro. iFrame. iIntros "_". rewrite bool_decide_eq_true_2; done.
      - assert (rd.(r_final) = list_sum cnts) as -> by lia.
        iMod ("Hreadupd" with "Hfull") as "[Hfull HQ]".
        iModIntro. iFrame. iIntros "_".
        rewrite bool_decide_eq_false_2; [eauto|lia]. }
    iModIntro.
    iExists rid, rd.
    iFrame "Hfull".
    iSplit; first done.
    iSplitR "Hrdsfr"; last first.
    { iExists rd, cd. iFrame "#"; iFrame; done. }
    iNext.
    iFrame "#"; iFrame.
    rewrite dom_union_L dom_singleton_L.
    rewrite big_sepS_insert; last done.
    iFrame "Hrsis".
    iExists rd, cd, pred, [], pvs; iFrame "Hcd Hpred Hrid Hp Hrdfl Hrum Hlp".
    iSplit; first done.
    iPureIntro.
    rewrite /lists_sum_is /=.
    repeat f_equal; lia.
  Qed.

  Lemma progress_read c cd M n cnts rid p (reads : list nat) final pred :
    length cnts = cd.(c_len) →
    cnts !! length reads = Some n →
    ▷ (∃ γ : gname, ⌜cd.(c_lowers) !! (length reads) = Some γ⌝ ∗ own γ (◯ MaxNat n)) -∗
    ▷ all_read_ops c cd M cnts -∗
    ▷ read_state_local c rid p reads final pred -∗
    ▷ ∃ pvs, proph p pvs ∗
    (∀ w pvs', ⌜pvs = (#n,w) :: pvs'⌝ -∗ proph p pvs' ==∗
      all_read_ops c cd M cnts ∗ read_state_local c rid p (reads ++ [n]) final pred).
  Proof.
    iIntros (Hlen Hlu) "Hn [#Hcd [HM Hrsis]] Hls".
    iNext.
    iDestruct "Hls" as (rd cd' <- <-) "(#Hcd' & Hrid & #Hspred & Hreads)".
    iDestruct (cdata_agree with "Hcd Hcd'") as %<-.
    iDestruct (ReadOps_lookup with "HM Hrid") as %?.
    iDestruct (big_sepS_elem_of_acc _ _ rid with "Hrsis") as "[Hrsi Hrest]"; first by apply elem_of_dom.
    iClear "Hcd'".
    iDestruct "Hrsi" as (rd' cd' pred' reads' pvs)
      "(#Hcd' & Hrid' & #Hspred' & Hreads' & Hlowers & Hrum & Hp & %Hsums & Hlp)".
    iDestruct (cdata_agree with "Hcd Hcd'") as %<-.
    iDestruct (ReadOps_agree with "Hrid Hrid'") as %<-.
    iExists _; iFrame "Hp".
    iIntros (w pvs' Hpvs) "Hp".
    iDestruct (read_seq_agree with "Hreads' Hreads") as %->.
    iMod (read_seq_update _ _ (reads ++ [n]) with "Hreads' Hreads") as "[Hreads' Hreads]".
    iModIntro.
    iDestruct (read_uppers_maintained_progress with "Hrum") as "Hrum"; first done.
    iDestruct ("Hrest" with "[Hrum Hrid Hreads' Hlp Hp Hlowers Hn]") as "Hrsis".
    { iExists rd, cd, _, (_ ++ [_]), _; iFrame "#"; iFrame.
      iDestruct "Hn" as (? ?) "#Hn".
      iSplit.
      - simpl; iSplit; last done; iExists _; iFrame "#".
        replace (length reads + 0) with (length reads) by lia; done.
      - iPureIntro.
        revert Hsums.
        rewrite /lists_sum_is list_sum_app app_length /=.
        assert (cd.(c_len) > 0).
        { destruct cnts; first done; simpl in *; lia. }
        pose proof Hlu as ?%lookup_lt_Some%Nat.sub_gt.
        rewrite -Hlen.
        replace (cd.(c_len)) with (S (cd.(c_len) - 1)) by lia.
        replace (length cnts - (length reads + 1)) with
          ((length cnts - length reads) - 1) by lia.
        destruct (length cnts - length reads) as [|diff] eqn:?; first done.
        replace (S diff - 1) with diff by lia.
        rewrite Hpvs /=; lia. }
    iSplitL "HM Hrsis"; first by iFrame.
    iExists _, _; iFrame "#"; iFrame; done.
  Qed.

  Lemma reads_less_than_current cnts lowers reads :
    length cnts = length reads →
    ([∗ list] k;γlwr ∈ cnts; lowers, own γlwr (● MaxNat k)) -∗
    ([∗ list] i↦k ∈ reads, ∃ γ : gname, ⌜lowers !! i = Some γ⌝ ∗
      own γ (◯ MaxNat k)) -∗
    ⌜list_sum reads ≤ list_sum cnts⌝.
  Proof.
    iIntros (Hlens) "Hfl Hfr".
    iAssert (⌜∀ i, option_Forall2 (≤) (reads !! i) (cnts !! i)⌝)%I as %?;
      last first.
    { iPureIntro; apply list_sum_le, Forall2_lookup; done. }
    iIntros (i).
    iDestruct (big_sepL2_length with "Hfl") as %?.
    destruct (reads !! i) eqn:Hreadsi.
    - iDestruct (big_sepL_lookup with "Hfr") as (γ Hγ) "Hfr"; first done.
      pose proof Hγ as ?%lookup_lt_Some.
      destruct (lookup_lt_is_Some_2 cnts i) as [s Hs]; first lia.
      rewrite Hs.
      iDestruct (big_sepL2_lookup with "Hfl") as "Hfl"; [done|done|].
      iDestruct (own_valid_2 with "Hfl Hfr")
        as %[Hincl _]%auth_both_valid_discrete.
      destruct Hincl as [[] Hincl%leibniz_equiv].
      rewrite max_nat_op in Hincl.
      simplify_eq.
      iPureIntro; constructor; lia.
    - pose proof Hreadsi as ?%lookup_ge_None_1.
      rewrite (lookup_ge_None_2 cnts i); [done|lia].
  Qed.

  Lemma read_done c cd M cnts rid p (reads : list nat) final pred :
    length cnts = cd.(c_len) →
    length cnts = length reads →
    ([∗ list] k; γlwr ∈ cnts; cd.(c_lowers), own γlwr (● (MaxNat k))) -∗
    all_read_ops c cd M cnts -∗
    read_state_local c rid p reads final pred -∗
    ([∗ list] k; γlwr ∈ cnts; cd.(c_lowers), own γlwr (● (MaxNat k))) ∗
    all_read_ops c cd M cnts ∗
    ⌜list_sum reads = final⌝ ∗
    ∃ pred', ▷ (∀ n, pred' n ≡ pred n) ∗ pred' (list_sum reads).
  Proof.
    iIntros (Hlen Hlen') "Hmaxs [#Hcd [HM Hrsis]] Hls".
    iDestruct "Hls" as (rd cd' <- <-) "(#Hcd' & Hrid & #Hspred & Hreads)".
    iDestruct (cdata_agree with "Hcd Hcd'") as %<-.
    iDestruct (ReadOps_lookup with "HM Hrid") as %?.
    iDestruct (big_sepS_elem_of_acc _ _ rid with "Hrsis") as "[Hrsi Hrest]";
      first by apply elem_of_dom.
    iClear "Hcd'".
    iDestruct "Hrsi" as (rd' cd' pred' reads' pvs)
      "(#Hcd' & Hrid' & #Hspred' & Hreads' & Hlowers & Hrum & Hp & %Hsums & Hlp)".
    iDestruct (cdata_agree with "Hcd Hcd'") as %<-.
    iDestruct (ReadOps_agree with "Hrid Hrid'") as %<-.
    iDestruct (read_seq_agree with "Hreads' Hreads") as %->.
    replace (c_len cd - length reads) with 0 in Hsums by lia.
    rewrite /lists_sum_is /= in Hsums.
    rewrite /linearization_point.
    iDestruct (read_uppers_maintained_done with "Hrum") as %?; first done.
    iSpecialize ("Hlp" with "[]"); first by eauto with lia.
    iDestruct (reads_less_than_current with "Hmaxs Hlowers") as %?; first done.
    rewrite bool_decide_eq_false_2; last lia.
    iDestruct "Hlp" as "[Hlp|Hlp]"; last first.
    { iDestruct "Hlp" as (?) "Hreads2".
      iDestruct (read_seq_frag_unique with "Hreads Hreads2") as %?; done. }
    iFrame "Hmaxs".
    iSplitR "Hlp"; last first.
    { replace rd.(r_final) with (list_sum reads) by lia.
      iSplit; first done.
      iExists pred'; iFrame "Hlp".
      iIntros (?);
      iApply (saved_pred_agree with "Hspred' Hspred"). }
    iDestruct ("Hrest" with "[Hrum Hrid Hreads' Hlowers Hp Hreads]") as "Hrsis".
    { iExists rd, cd, _, _, _; iFrame "#"; iFrame.
      iSplit.
      - replace (c_len cd - length reads) with 0 by lia; done.
      - iIntros "_".
        rewrite bool_decide_eq_false_2; last lia.
        iRight; iExists _; iFrame. }
    iFrame; iFrame "#".
  Qed.

  Lemma wp_new_counter (n : nat) :
    {{{ ⌜0 < n⌝ }}}
      new_counter #n
    {{{c cd, RET c; Counter_frag c 0 ∗ cdata c cd ∗ ⌜cd.(c_len) = n⌝ ∗ is_counter c}}}.
  Proof.
    iIntros (Φ) "%Hnp HΦ".
    rewrite /new_counter; wp_pures.
    iApply wp_fupd.
    wp_apply wp_allocN; [lia|done|].
    iIntros (c) "[Hc Hm]".
    iAssert (meta_token c ⊤) with "[Hm]" as "Hm".
    { destruct n; first lia.
      replace (Z.to_nat (S n)) with (S n) by lia.
      iDestruct "Hm" as "[Hm _]".
      rewrite Loc.add_0. done. }
    iMod (own_alloc (● Excl' 0 ⋅ ◯ Excl' 0)) as (γ) "[HFl HFr]";
      first by apply auth_both_valid.
    iAssert (|==> ∃ lowers, ⌜length lowers = n⌝ ∧ [∗ list] γlwr ∈ lowers, own γlwr (● (MaxNat 0)))%I as "Hlwrs".
    { iInduction n as [|n] "IH"; first lia.
      destruct (decide (n = 0)) as [->|]; simpl.
      - iMod (own_alloc (● MaxNat 0)) as (γlwr) "Hmn"; first by apply auth_auth_valid.
        iModIntro; iExists [_]; simpl; iFrame; done.
      - iMod ("IH" with "[]") as (lowers) "[% Hlowers]"; first by eauto with lia.
        iMod (own_alloc (● MaxNat 0)) as (γlwr) "Hmn"; first by apply auth_auth_valid.
        iModIntro; iExists (lowers ++ [γlwr]).
        iSplit; first by rewrite app_length /=; auto with lia.
        rewrite big_sepL_app /=; iFrame. }
    iMod "Hlwrs" as (lowers) "[%Hlen Hlwrs]".
    iMod (own_alloc (● ∅)) as (γrdops) "Hrdops"; first by apply auth_auth_valid.
    set (cd := {|c_len := n; c_exact := γ; c_lowers := lowers; c_read_ops := γrdops |}).
    iMod (meta_set _ _ cd nroot with "Hm") as "#Hm"; first done.
    iAssert (cdata #c cd) as "Hcd"; first by iExists _; iFrame "#".
    iMod (inv_alloc _ _ (counter_inv #c cd) with "[HFl Hc Hlwrs Hrdops]") as "#IH".
    { iNext; iExists c, (replicate n 0), ∅.
      iSplit; first done.
      iSplit; first by iExists _; iFrame "#".
      iFrame "Hrdops"; rewrite dom_empty_L big_sepS_empty.
      iSplitL "HFl".
      { rewrite list_sum_replicate.
        replace (n * 0) with 0 by lia.
        iExists _; iFrame "#"; iFrame. }
      rewrite replicate_length; iSplit; first done.
      simpl.
      rewrite big_sepL2_replicate_l; last done.
      replace (Z.to_nat n) with n by lia.
      rewrite fmap_replicate.
      iFrame.
      iSplit; last done.
      iExists _; iSplit; done. }
    iModIntro.
    rewrite /Counter_frag.
    iApply ("HΦ" $! #c cd).
    iSplit; last first.
    { by repeat iSplit; [by iExists _; eauto|done|by iExists _; eauto]. }
    iExists _; iFrame "#"; done.
  Qed.

  Lemma wp_incr (Q : nat → iProp Σ) c cd i :
    {{{ ⌜i < cd.(c_len)⌝ ∗ cdata c cd ∗ is_counter c ∗
        (∀ k, Counter_full c k ={⊤ ∖ ↑CName}=∗ Counter_full c (k + 1) ∗ (Q k)) }}}
      incr c #i
    {{{k, RET #(); Q k}}}.
  Proof.
    iIntros (Φ) "(% & #Hcd & Hinv & Hupd) HΦ".
    iPoseProof "Hcd" as (?) "[-> _]".
    iDestruct "Hinv" as (cd') "#Hinv".
    rewrite /incr; wp_pures.
    wp_bind (FAA _ _).
    iInv CName as (l' cnts M)
      "(>%Heq & >#Hcd' & >Hfull & >%Hlen & >Hcnts & >Hmaxs & Hallrops)".
    iDestruct (cdata_agree with "Hcd Hcd'") as %<-.
    simplify_eq Heq; intros <-.
    destruct (lookup_lt_is_Some_2 cnts i) as [cnt Hcnt]; first lia.
    destruct (elem_of_list_split_length cnts i cnt) as (cnts1 & cnts2 & -> & ->);
      first done.
    rewrite app_length /= in Hlen.
    rewrite fmap_app /= array_app array_cons !fmap_length.
    iDestruct "Hcnts" as "[Hcnts1 [Hcnt Hcnts2]]".
    iDestruct (big_sepL2_app_inv_l with "Hmaxs") as
      (lowers1 lwrlowers2 Hlowerseq) "[Hmaxs1 Hmaxmaxs2]".
    iDestruct (big_sepL2_cons_inv_l with "Hmaxmaxs2") as
      (γlwr lowers2 ->) "[Hmax Hmaxs2]".
    wp_faa.
    iMod ("Hupd" with "Hfull") as "[Hfull HQ]".
    iMod (own_update with "Hmax") as "[Hmax _]".
    { apply auth_update_alloc, (max_nat_local_update _ _ (MaxNat (cnt + 1)));
        simpl; lia. }
    replace (list_sum (cnts1 ++ cnt :: cnts2) + 1)
      with (list_sum (cnts1 ++ cnt + 1 :: cnts2))
      by by rewrite !list_sum_app /=; lia.
    iMod (all_read_ops_incr with "Hfull Hallrops") as "[Hfull Hallrops]".
    iModIntro.
    iSplitR "HΦ HQ"; last first.
    { wp_pures; iModIntro. iApply "HΦ"; iFrame. }
    iNext.
    iExists l, (cnts1 ++ cnt + 1 :: cnts2), M.
    iSplit; first done.
    iFrame "Hfull Hallrops".
    iFrame "Hcd".
    iSplit; first by rewrite app_length.
    rewrite fmap_app array_app array_cons !fmap_length; iFrame.
    replace ((cnt + 1)%nat : Z) with (cnt + 1)%Z; last lia.
    iFrame.
    rewrite Hlowerseq.
    iApply (big_sepL2_app with "Hmaxs1").
    rewrite big_sepL2_cons; iFrame.
  Qed.

  Lemma wp_read_aux (Q : nat → iProp Σ) p (l : loc) cd rid reads final :
    length reads ≤ cd.(c_len) →
    {{{ cdata #l cd ∗ inv CName (counter_inv #l cd) ∗ read_state_local #l rid p (reads : list nat) final Q }}}
      read_aux #p #(list_sum reads) #(l +ₗ (length reads)) #(cd.(c_len) - length reads)
    {{{RET #final; Q final }}}.
  Proof.
    iIntros (Hlens Φ) "(#Hcd & #Hic & Hls) HΦ".
    iAssert (WP read_aux #p #(list_sum reads) #(l +ₗ (length reads)) #(cd.(c_len) - length reads)
        {{ v, ⌜v = #final⌝ ∗ Q final}} -∗
        WP read_aux #p #(list_sum reads) #(l +ₗ (length reads)) #(c_len cd - length reads) {{ v, Φ v }}
      )%I with "[HΦ]" as "H".
    { iIntros "H".
      iDestruct (wp_frame_step_r' with "[$H $HΦ]") as "H".
      iApply (wp_wand with "H").
      iIntros (?) "[H1 H2]". iDestruct "H1" as (->) "H1".
      iApply "H2"; done. }
    iApply "H".
    iLöb as "IH" forall (reads Hlens).
    rewrite {2}/read_aux.
    destruct (cd.(c_len) - length reads) as [|n] eqn:Hn.
    - do 7 wp_pure.
      wp_bind (BinOp _ _ _).
      iInv CName as (l' cnts M)
        "(>%Heq & _ & >Hfull & >%Hlen & >Hcnts & >Hmaxs & Hallrops)" "Hclose".
      simplify_eq.
      wp_pures.
      iDestruct (read_done with "Hmaxs Hallrops Hls") as "(Hmaxs & Hallrops & %Hrdsfin & H)"; [done|lia|].
      iMod ("Hclose" with "[Hfull Hcnts Hmaxs Hallrops]") as "_".
      { iNext. iExists _, _, _; iFrame; eauto. }
      iModIntro.
      rewrite bool_decide_eq_true_2; last by eauto with f_equal lia.
      wp_pures.
      iModIntro.
      iSplit; first by simplify_eq.
      iDestruct "H" as (?) "[Heq H]".
      iSpecialize ("Heq" $! final).
      rewrite Hrdsfin.
      iRewrite -"Heq"; done.
    - wp_pures.
      rewrite bool_decide_eq_false_2; last by intros ?; simplify_eq; lia.
      wp_pures.
      wp_bind (Resolve _ _ _).
      iInv CName as (l' cnts M)
        "(>%Heq & _ & >Hfull & >%Hlen & >Hcnts & >Hmaxs & Hallrops)" "Hclose".
      simplify_eq.
      destruct (lookup_lt_is_Some_2 cnts (length reads)) as [cnt Hcnt]; first lia.
      edestruct (elem_of_list_split_length cnts (length reads)) as (cnts1 & cnts2 & Hcnts & Hreadscnts1);
        first eassumption.
      rewrite Hcnts.
      iDestruct (big_sepL2_app_inv_l with "Hmaxs") as (lowers1 lowers2 Hlowers) "[Hmaxs1 Hmaxs2]".
      iDestruct (big_sepL2_cons_inv_l with "Hmaxs2") as (γlwr ? ->) "[Hmax Hmaxs2]".
      iDestruct (big_sepL2_length with "Hmaxs1") as %?.
      iMod (own_update _ _ (● MaxNat cnt ⋅ ◯ MaxNat cnt) with "Hmax") as "[Hmax #Hmaxfr]".
      { apply auth_update_alloc, max_nat_local_update; done. }
      iDestruct (progress_read with "[] [$] [$]") as (pvs) "[>Hp Hback]".
      { rewrite -Hcnts; done. }
      { rewrite lookup_app_r; last lia.
        replace (length reads - length cnts1) with 0 by lia.
        done. }
      { iNext; iExists _; iFrame "#".
        iPureIntro.
        rewrite Hlowers.
        rewrite lookup_app_r; last lia.
        replace (length reads - length lowers1) with 0 by lia.
        done. }
      wp_apply (wp_resolve with "[$]"); first done.
      rewrite fmap_app /= array_app array_cons !fmap_length.
      iDestruct "Hcnts" as "[Hcnts1 [Hcnt Hcnts2]]".
      rewrite Hreadscnts1.
      wp_load.
      iModIntro.
      iIntros (pvs' ->) "Hp".
      iMod ("Hback" with "[] Hp") as "(Hallrops & Hls)"; first done.
      iMod ("Hclose" with "[Hfull Hcnts1 Hcnt Hcnts2 Hmaxs1 Hmax Hmaxs2 Hallrops]") as "_".
      { iNext. iExists _, _, _; iFrame "Hfull Hallrops Hcd".
        iSplit; first done.
        iSplit; first by rewrite -Hcnts.
        rewrite fmap_app /= array_app array_cons !fmap_length; iFrame "Hcnts1 Hcnts2 Hcnt".
        rewrite Hlowers.
        iApply (big_sepL2_app with "Hmaxs1").
        iApply big_sepL2_cons; iFrame. }
      iModIntro.
      do 5 wp_pure.
      replace (l' +ₗ length cnts1 +ₗ 1) with (l' +ₗ length (reads ++ [cnt])); last first.
      { rewrite Loc.add_assoc. rewrite app_length /=. f_equal; lia. }
      replace #(c_len cd - length cnts1 - 1) with #(c_len cd - length (reads ++ [cnt])); last first.
      { rewrite app_length /=; do 2 f_equal; lia. }
      replace #(list_sum reads + cnt) with #(list_sum (reads ++ [cnt])); last first.
      { repeat f_equal. rewrite list_sum_app /=; lia. }
      iApply ("IH" $! (reads ++ [cnt]) with "[] [$]").
      rewrite -Hlen Hcnts !app_length /=; eauto with lia.
  Qed.

  Lemma wp_read (Q : nat → iProp Σ) c cd :
    {{{ cdata c cd ∗ is_counter c ∗
        (∀ k, Counter_full c k ={⊤ ∖ ↑CName}=∗ Counter_full c k ∗ (Q k)) }}}
      read c #cd.(c_len)
    {{{k, RET #k; Q k}}}.
  Proof.
    iIntros (Φ) "(#Hcd & Hinv & Hupd) HΦ".
    iPoseProof "Hcd" as (?) "[-> _]".
    iDestruct "Hinv" as (cd') "#Hinv".
    rewrite /read; wp_pures.
    wp_apply wp_new_proph; first done.
    iIntros (pvs p) "Hp".
    iApply fupd_wp.
    iInv CName as (l' cnts M)
      "(>%Heq & >#Hcd' & >Hfull & >%Hlen & >Hcnts & >Hmaxs & Hallrops)" "Hclose".
    iDestruct (cdata_agree with "Hcd Hcd'") as %<-.
    simplify_eq.
    iMod (make_read_state with "Hfull Hupd Hallrops Hp") as (rid rd ?) "(Hfull & Hallrops & Hls)".
    iMod ("Hclose" with "[Hfull Hmaxs Hcnts Hallrops]") as "_".
    { iNext. iExists _, _, _; iFrame; eauto. }
    iModIntro.
    wp_pures.
    replace #0 with #(list_sum []) by done.
    replace #l' with #(l' +ₗ @length nat []) at 5 by rewrite /= Loc.add_0 //.
    replace #cd.(c_len) with #(cd.(c_len) - @length nat []) by by simpl; repeat f_equal; lia.
    wp_apply (wp_read_aux with "[Hls]"); [simpl; lia|by iFrame; iFrame "#"|].
    iIntros "?"; iApply "HΦ"; done.
  Qed.

  Lemma wp_incr_seq c cd i k :
    {{{ ⌜i < cd.(c_len)⌝ ∗ cdata c cd ∗ is_counter c ∗ Counter_frag c k }}}
      incr c #i
    {{{ RET #(); Counter_frag c (k + 1) }}}.
  Proof.
    iIntros (Φ) "(% & #Hcd & #Hinv & Hfrag) HΦ".
    wp_apply (wp_incr (λ n, ⌜n = k⌝ ∗ Counter_frag c (n + 1))%I with "[Hfrag]").
    { iSplit; first done. iFrame "#".
      iIntros (?) "Hfull".
      iDestruct (Counter_agree with "Hfull Hfrag") as %->.
      iMod (Counter_update with "Hfull Hfrag") as "[Hfull Hfrag]"; by iFrame. }
    iIntros (?) "[-> ?]"; iApply "HΦ"; done.
  Qed.

  Lemma wp_read_seq c cd k :
    {{{ cdata c cd ∗ is_counter c ∗ Counter_frag c k }}}
      read c #cd.(c_len)
    {{{m, RET #m; ⌜m = k⌝ ∗ Counter_frag c k }}}.
  Proof.
    iIntros (Φ) "(#Hcd & #Hinv & Hfrag) HΦ".
    wp_apply (wp_read (λ n, ⌜n = k⌝ ∗ Counter_frag c n)%I with "[Hfrag]").
    { iSplit; first done. iFrame "#".
      iIntros (?) "Hfull".
      iDestruct (Counter_agree with "Hfull Hfrag") as %->.
      by iFrame. }
    iIntros (?) "[-> ?]"; iApply "HΦ"; iFrame; done.
  Qed.

  Definition conc_counter_at_least c cd γ k : iProp Σ :=
    cdata c cd ∗ is_counter c ∗
    inv (nroot .@ "conc_counter") (∃ m, Counter_frag c m ∗ own γ (● MaxNat m)) ∗
    own γ (◯ MaxNat k).

  Lemma wp_new_conc (n : nat) :
    {{{ ⌜0 < n⌝ }}}
      new_counter #n
    {{{c cd γ, RET c; ⌜cd.(c_len) = n⌝ ∗ conc_counter_at_least c cd γ 0 }}}.
  Proof.
    iIntros (Φ) "%Hnp HΦ".
    iApply wp_fupd.
    wp_apply wp_new_counter; first done.
    iIntros (c cd) "(Hfr & #Hcd & % & #Hinv)".
    iMod (own_alloc (● MaxNat 0 ⋅ ◯ MaxNat 0)) as (γ) "[Hmfl Hmfr]".
    { apply auth_both_valid_discrete; done. }
    iMod (inv_alloc (nroot .@ "conc_counter") _
            (∃ m, Counter_frag c m ∗ own γ (● MaxNat m))
           with "[Hfr Hmfl]") as "#Hccinv".
    { iNext; iExists _; iFrame. }
    iModIntro; iApply "HΦ"; iSplit; first done.
    iFrame; iFrame "#".
  Qed.

  Lemma wp_incr_conc c cd i γ k :
    {{{ ⌜i < cd.(c_len)⌝ ∗ conc_counter_at_least c cd γ k }}}
      incr c #i
    {{{ RET #(); conc_counter_at_least c cd γ (k + 1) }}}.
  Proof.
    iIntros (Φ) "(% & #Hcd & #Hinv & #Hccinv & #Hal) HΦ".
    wp_apply (wp_incr (λ _,  conc_counter_at_least c cd γ (k + 1))%I).
    { iSplit; first done. iFrame "#".
      iIntros (?) "Hfl".
      iInv (nroot .@ "conc_counter") as (m) ">[Hfr Hmax]".
      iDestruct (Counter_agree with "Hfl Hfr") as %->.
      iMod (Counter_update _ _ (m + 1) with "Hfl Hfr") as "[Hfull Hfrag]".
      iDestruct (own_valid_2 with "Hmax Hal") as %Hvl.
      assert (k ≤ m).
      { apply auth_both_valid_discrete in Hvl as [[[] Hmxs%leibniz_equiv] _].
        rewrite max_nat_op in Hmxs; simplify_eq; lia. }
      iMod (own_update _ _ (● MaxNat (m + 1) ⋅ ◯ MaxNat (m + 1)) with "Hmax") as "[Hmax Hal']".
      { apply auth_update_alloc, max_nat_local_update; simpl; lia. }
      replace (◯ MaxNat (m + 1)) with (◯ MaxNat (m + 1) ⋅ ◯ MaxNat (k + 1)); last first.
      { rewrite -auth_frag_op max_nat_op; repeat f_equal; lia. }
      iDestruct "Hal'" as "[_ Hal']".
      iModIntro.
      iSplitL "Hfrag Hmax"; first by iNext; iExists _; iFrame.
      iModIntro; iFrame. }
    iIntros (?) "?"; iApply "HΦ"; done.
  Qed.

  Lemma wp_read_conc c cd γ m :
    {{{ conc_counter_at_least c cd γ m }}}
      read c #cd.(c_len)
    {{{k, RET #k; ⌜m ≤ k⌝ }}}.
  Proof.
    iIntros (Φ) "(#Hcd & #Hinv & #Hccinv & #Hal) HΦ".
    wp_apply (wp_read (λ k,  ⌜m ≤ k⌝)%I).
    { iSplit; first done. iFrame "#".
      iIntros (?) "Hfl".
      iInv (nroot .@ "conc_counter") as (mx) ">[Hfr Hmax]".
      iDestruct (Counter_agree with "Hfl Hfr") as %->.
      iDestruct (own_valid_2 with "Hmax Hal") as %Hvl.
      assert (m ≤ mx).
      { apply auth_both_valid_discrete in Hvl as [[[] Hmxs%leibniz_equiv] _].
        rewrite max_nat_op in Hmxs; simplify_eq; lia. }
      iModIntro.
      iSplitL "Hfr Hmax"; first by iNext; iExists _; iFrame.
      iModIntro; iFrame; done. }
    iIntros (?) "?"; iApply "HΦ"; done.
  Qed.

End proof.