Library zoo_persistent.sstore_2

Require Import iris.base_logic.lib.ghost_map.

Require Import zoo.prelude.
Require Import zoo.common.fin_maps.
Require Import zoo.common.list.
Require Import zoo.common.treemap.
Require Import zoo.iris.base_logic.lib.mono_gmap.
Require Import zoo.base.
Require Import zoo_std.list.
Require Export zoo_persistent.sstore_2__code.
Require Import zoo_persistent.sstore_2__types.
Require Import zoo.options.

Implicit Type l r node cnode base root dst : location.
Implicit Type nodes : list location.
Implicit Type v t s : val.
Implicit Type σ σ₀ : gmap location val.

Module base.
  #[local] Definition generation :=
    nat.
  Implicit Type g : generation.

  #[local] Notation "data '.(gen)'" := (
    fst data
  )(at level 2,
    left associativity,
    format "data .(gen)"
  ) : stdpp_scope.
  #[local] Notation "data '.(val)'" := (
    snd data
  )(at level 2,
    left associativity,
    format "data .(val)"
  ) : stdpp_scope.

  #[local] Definition store :=
    gmap location (generation × val).
  Implicit Type ς : store.
  Implicit Type data : generation × val.

  Record descriptor := Descriptor
    { descriptor ۰ gen : generation
    ; descriptor ۰ store : store
    }.
  Add Printing Constructor descriptor.
  Implicit Type descr : descriptor.
  Implicit Type cnodes : gmap location descriptor.

  Class Sstore2G Σ `{zoo ۰ G : !ZooG Σ} :=
    { #[local] sstore_2 ۰ G ۰ nodes ۰ G :: ghost_mapG Σ location descriptor
    }.

  Definition sstore_2 ۰ Σ :=
    #[ghost_mapΣ location descriptor
    ].
  #[global] Instance subG ｰ sstore_2 ۰ Σ Σ `{zoo ۰ G : !ZooG Σ} :
    subG sstore_2 ۰ Σ Σ →
    Sstore2G Σ.

  Section sstore_2 ۰ G.
    Context `{sstore_2 ۰ G : Sstore2G Σ}.

    #[local] Definition metadata :=
      gname.
    Implicit Type γ : metadata.

    #[local] Definition store ۰ on σ ₀ ς :=
      ς ∪ (pair 0 <$> σ ₀ ).
    #[local] Definition store ۰ generation g ς :=
      map_Forall (λ r data, data .(gen ) ≤ g) ς.

    #[local] Definition descriptor ۰ wf σ ₀ descr :=
      dom descr.(descriptor ۰ store) ⊆ dom σ ₀ ∧
      store ۰ generation descr.(descriptor ۰ gen) descr.(descriptor ۰ store).

    Record delta := Delta
      { delta ۰ ref : location
      ; delta ۰ gen : generation
      ; delta ۰ val : val
      ; delta ۰ node : location
      }.
    Add Printing Constructor delta.
    Implicit Type δ : delta.
    Implicit Type δs : list delta.
    Implicit Type path : list (list delta).

    #[local] Notation "δ '.(delta۰data)'" := (
      pair δ.(delta ۰ gen) δ.(delta ۰ val)
    )(at level 2,
      left associativity,
      format "δ .(delta۰data)"
    ) : stdpp_scope.

    #[local] Definition delta ۰ patch δ :=
      (δ.(delta ۰ ref), δ .(delta ۰ data )).

    #[local] Definition deltas ۰ apply δs ς :=
      list_to_map (delta ۰ patch <$> δs) ∪ ς.
    #[local] Fixpoint deltas ۰ chain node δs dst : iProp Σ :=
      match δs with
      | [] ⇒
          ⌜node = dst ⌝
      | δ :: δs ⇒
          node ↦ᵣ ‘Diff ( #δ.(delta ۰ ref), #δ.(delta ۰ gen), δ.(delta ۰ val), #δ.(delta ۰ node) ) ∗
          deltas ۰ chain δ.(delta ۰ node) δs dst
      end.

    #[local] Definition edge : Set :=
      location × list delta.
    Implicit Type ϵ : edge.
    Implicit Type ϵs : gmap location edge.

    #[local] Definition cnodes ۰ auth γ cnodes :=
      ghost_map_auth γ 1 cnodes.
    #[local] Definition cnodes ۰ elem γ cnode descr :=
      ghost_map_elem γ cnode DfracDiscarded descr.

    #[local] Definition cnode ۰ model γ σ ₀ cnode descr ϵ ς : iProp Σ :=
      let cnode' := ϵ .1 in
      let δs := ϵ .2 in
      ⌜descriptor ۰ wf σ ₀ descr ⌝ ∗
      cnodes ۰ elem γ cnode descr ∗
      ⌜NoDup $ delta ۰ ref <$> δs ⌝ ∗
      ⌜store ۰ on σ ₀ descr.(descriptor ۰ store) = store ۰ on σ ₀ $ deltas ۰ apply δs ς ⌝ ∗
      deltas ۰ chain cnode δs cnode'.
    Definition sstore_2 ۰ model t σ ₀ σ : iProp Σ :=
      ∃ l γ g root ς ,
      ⌜t = #l ⌝ ∗
      ⌜σ = snd <$> ς ⌝ ∗
      l ↪[nroot .@"impl"] γ ∗
      l .[gen ] ↦ #g ∗
      l .[root ] ↦ #root ∗
      root ↦ᵣ §Root ∗
      ( [∗ map ] r ↦ data ∈ store ۰ on σ ₀ ς ,
        r .[ref_gen ] ↦ #data .(gen ) ∗
        r .[ref_value ] ↦ data .(val )
      ) ∗
      ⌜descriptor ۰ wf σ ₀ (Descriptor g ς)⌝ ∗
      if decide (g = 0) then
        cnodes ۰ auth γ ∅
      else
        ∃ cnodes ϵs base descr δs ,
        ⌜treemap ۰ rooted ϵs base ⌝ ∗
        cnodes ۰ auth γ cnodes ∗

        ⌜cnodes !! base = Some descr ⌝ ∗
        ⌜descr.(descriptor ۰ gen) < g ⌝ ∗
        cnode ۰ model γ σ ₀ base descr (root , δs ) ς ∗
        ⌜δs = [] → ς = descr.(descriptor ۰ store)⌝ ∗
        ⌜Forall (λ δ, ∃ data, ς !! δ.(delta ۰ ref) = Some data ∧ data .(gen ) = g) δs ⌝ ∗

        [∗ map ] cnode ↦ descr ; ϵ ∈ delete base cnodes ; ϵs ,
          ∃ descr',
          ⌜cnodes !! ϵ .1 = Some descr'⌝ ∗
          cnode ۰ model γ σ ₀ cnode descr ϵ descr'.(descriptor ۰ store).

    Definition sstore_2 ۰ snapshot s t σ : iProp Σ :=
      ∃ l γ g cnode descr ,
      ⌜t = #l ⌝ ∗
      ⌜s = (t , #g , #cnode )%V⌝ ∗
      ⌜σ = snd <$> descr.(descriptor ۰ store)⌝ ∗
      ⌜descr.(descriptor ۰ gen) ≤ g ⌝ ∗
      l ↪[nroot .@"impl"] γ ∗
      cnodes ۰ elem γ cnode descr.

    #[local] Instance deltas ۰ chain ｰ timeless node δs dst :
      Timeless (deltas ۰ chain node δs dst).
    #[global] Instance sstore_2 ۰ model ｰ timeless t σ ₀ σ :
      Timeless (sstore_2 ۰ model t σ ₀ σ).

    #[global] Instance sstore_2 ۰ snapshot ｰ persistent s t σ :
      Persistent (sstore_2 ۰ snapshot s t σ).

    #[local] Lemma store ۰ on ｰ dom σ ₀ ς :
      dom (store ۰ on σ ₀ ς) = dom σ ₀ ∪ dom ς.
    #[local] Lemma store ۰ on ｰ dom' σ ₀ ς :
      dom ς ⊆ dom σ ₀ →
      dom (store ۰ on σ ₀ ς) = dom σ ₀.
    #[local] Lemma store ۰ on ｰ lookup {σ ₀ ς} r data :
      store ۰ on σ ₀ ς !! r = Some data ↔
          ς !! r = Some data
        ∨ ς !! r = None ∧
          data .(gen ) = 0 ∧
          σ ₀ !! r = Some data .(val ).
    #[local] Lemma store ۰ on ｰ lookup' {σ ₀ ς} r data :
      ς !! r = Some data →
      store ۰ on σ ₀ ς !! r = Some data.
    #[local] Lemma store ۰ on ｰ insert r data σ ₀ ς :
      store ۰ on σ ₀ (<[r := data ]> ς) = <[r := data ]> (store ۰ on σ ₀ ς).
    #[local] Lemma store ۰ on ｰ insert ｰ support r v σ ₀ ς :
      σ ₀ !! r = None →
      dom ς ⊆ dom σ ₀ →
      store ۰ on (<[r := v ]> σ ₀) ς = <[r := (0, v )]> (store ۰ on σ ₀ ς).
    #[local] Lemma store ۰ on ｰ deltas ۰ apply σ ₀ δs ς :
      store ۰ on σ ₀ (deltas ۰ apply δs ς) = deltas ۰ apply δs (store ۰ on σ ₀ ς).

    #[local] Lemma store ۰ generation ｰ le {g ς} g' :
      g ≤ g' →
      store ۰ generation g ς →
      store ۰ generation g' ς.
    #[local] Lemma store ۰ generation ｰ insert g ς r data :
      store ۰ generation g ς →
      data .(gen ) ≤ g →
      store ۰ generation g (<[r := data ]> ς).

    #[local] Lemma deltas ۰ apply ｰ nil ς :
      deltas ۰ apply [] ς = ς.
    #[local] Lemma deltas ۰ apply ｰ cons δ δs ς :
      deltas ۰ apply (δ :: δs) ς = <[δ.(delta ۰ ref) := δ .(delta ۰ data )]> (deltas ۰ apply δs ς).
    #[local] Lemma deltas ۰ apply ｰ singleton δ ς :
      deltas ۰ apply [δ] ς = <[δ.(delta ۰ ref) := δ .(delta ۰ data )]> ς.
    #[local] Lemma deltas ۰ apply ｰ app δs1 δs2 ς :
      deltas ۰ apply (δs1 ++ δs2) ς = deltas ۰ apply δs1 (deltas ۰ apply δs2 ς).
    #[local] Lemma deltas ۰ apply ｰ snoc δs δ ς :
      deltas ۰ apply (δs ++ [δ]) ς = deltas ۰ apply δs (<[δ.(delta ۰ ref) := δ .(delta ۰ data )]> ς).
    #[local] Lemma deltas ۰ apply ｰ snoc' δs r g v node ς :
      deltas ۰ apply (δs ++ [Delta r g v node]) ς = deltas ۰ apply δs (<[r := (g , v )]> ς).
    #[local] Lemma deltas ۰ apply ｰ dom δs ς :
      dom (deltas ۰ apply δs ς) = list_to_set (delta ۰ ref <$> δs) ∪ dom ς.
    #[local] Lemma deltas ۰ apply ｰ lookup δs δ r data ς :
      NoDup (delta ۰ ref <$> δs) →
      δ ∈ δs →
      r = δ.(delta ۰ ref) →
      data = δ .(delta ۰ data ) →
      deltas ۰ apply δs ς !! r = Some data.
    #[local] Lemma deltas ۰ apply ｰ lookup' δs r data ς :
      NoDup (delta ۰ ref <$> δs) →
      (r , data ) ∈ delta ۰ patch <$> δs →
      deltas ۰ apply δs ς !! r = Some data.
    #[local] Lemma deltas ۰ apply ۰ lookup ｰ ne r δs ς :
      NoDup (delta ۰ ref <$> δs) →
      r ∉ (delta ۰ ref <$> δs ) →
      deltas ۰ apply δs ς !! r = ς !! r.
    #[local] Lemma deltas ۰ apply ｰ permutation δs1 δs2 ς :
      NoDup (delta ۰ ref <$> δs1) →
      δs1 ≡ₚ δs2 →
      deltas ۰ apply δs1 ς = deltas ۰ apply δs2 ς.
    #[local] Lemma deltas ۰ chain ｰ cons src δ δs dst :
      src ↦ᵣ ‘Diff ( #δ.(delta ۰ ref), #δ.(delta ۰ gen), δ.(delta ۰ val), #δ.(delta ۰ node) ) -∗
      deltas ۰ chain δ.(delta ۰ node) δs dst -∗
        deltas ۰ chain src (δ :: δs) dst.
    #[local] Lemma deltas ۰ chain ｰ nil ｰ inv src dst :
      deltas ۰ chain src [] dst ⊢
      ⌜src = dst ⌝.
    #[local] Lemma deltas ۰ chain ｰ cons ｰ inv src δ δs dst :
      deltas ۰ chain src (δ :: δs) dst ⊢
        src ↦ᵣ ‘Diff ( #δ.(delta ۰ ref), #δ.(delta ۰ gen), δ.(delta ۰ val), #δ.(delta ۰ node) ) ∗
        deltas ۰ chain δ.(delta ۰ node) δs dst.
    #[local] Lemma deltas ۰ chain ｰ snoc {src δs dst} r g v dst' :
      deltas ۰ chain src δs dst -∗
      dst ↦ᵣ ‘Diff ( #r , #g , v , #dst' ) -∗
      deltas ۰ chain src (δs ++ [Delta r g v dst']) dst'.
    #[local] Lemma deltas ۰ chain ｰ app₁ src δs1 δs2 dst :
      deltas ۰ chain src (δs1 ++ δs2) dst ⊢
        let node := default src $ delta ۰ node <$> last δs1 in
        deltas ۰ chain src δs1 node ∗
        deltas ۰ chain node δs2 dst.
    #[local] Lemma deltas ۰ chain ｰ app₂ src δs1 node δs2 dst :
      deltas ۰ chain src δs1 node -∗
      deltas ۰ chain node δs2 dst -∗
      deltas ۰ chain src (δs1 ++ δs2) dst.
    #[local] Lemma deltas ۰ chain ｰ snoc ｰ inv src δs δ dst :
      deltas ۰ chain src (δs ++ [δ]) dst ⊢
        let node := default src $ delta ۰ node <$> last δs in
        ⌜δ.(delta ۰ node) = dst ⌝ ∗
        deltas ۰ chain src δs node ∗
        node ↦ᵣ ‘Diff ( #δ.(delta ۰ ref), #δ.(delta ۰ gen), δ.(delta ۰ val), #dst ).
    #[local] Lemma deltas ۰ chain ｰ lookup {src δs dst} i δ :
      δs !! i = Some δ →
      deltas ۰ chain src δs dst ⊢
        deltas ۰ chain src (take ˖i δs) δ.(delta ۰ node) ∗
        deltas ۰ chain δ.(delta ۰ node) (drop ˖i δs) dst.
    #[local] Lemma deltas ۰ chain ｰ lookup' {src δs dst} i δ :
      δs !! i = Some δ →
      deltas ۰ chain src δs dst ⊢
        ∃ node ,
        ⌜ if i is 0 then
            node = src
          else
            ∃ δ',
            δs !! pred i = Some δ' ∧
            δ'.(delta ۰ node) = node
        ⌝ ∗
        deltas ۰ chain src (take i δs) node ∗
        node ↦ᵣ ‘Diff ( #δ.(delta ۰ ref), #δ.(delta ۰ gen), δ.(delta ۰ val), #δ.(delta ۰ node) ) ∗
        deltas ۰ chain δ.(delta ۰ node) (drop ˖i δs) dst.

    #[local] Definition cnodes ｰ alloc root :
      ⊢ |==>
        ∃ γ ,
        cnodes ۰ auth γ ∅.
    #[local] Definition cnodes ｰ lookup γ cnodes cnode descr :
      cnodes ۰ auth γ cnodes -∗
      cnodes ۰ elem γ cnode descr -∗
      ⌜cnodes !! cnode = Some descr ⌝.
    #[local] Lemma cnodes ｰ insert {γ cnodes} cnode descr :
      cnodes !! cnode = None →
      cnodes ۰ auth γ cnodes ⊢ |==>
        cnodes ۰ auth γ (<[cnode := descr ]> cnodes) ∗
        cnodes ۰ elem γ cnode descr.

    Lemma sstore_2 ۰ model ｰ valid t σ ₀ σ :
      sstore_2 ۰ model t σ ₀ σ ⊢
      ⌜dom σ ⊆ dom σ ₀ ⌝.
    Lemma sstore_2 ۰ model ｰ exclusive t σ ₀1 σ1 σ ₀2 σ2 :
      sstore_2 ۰ model t σ ₀1 σ1 -∗
      sstore_2 ۰ model t σ ₀2 σ2 -∗
      False.

    Lemma sstore_2 ٠ create ｰ spec :
      {{{
        True
      }}}
        sstore_2 ٠ create ()
      {{{
        t
      , RET t ;
        (∃ l , ⌜t = #l ⌝ ∗ meta_token l (↑nroot .@"user")) ∗
        sstore_2 ۰ model t ∅ ∅
      }}}.

    Lemma sstore_2 ٠ ref ｰ spec t σ ₀ σ v :
      {{{
        sstore_2 ۰ model t σ ₀ σ
      }}}
        sstore_2 ٠ ref t v
      {{{
        r
      , RET #r ;
        ⌜σ ₀ !! r = None ⌝ ∗
        sstore_2 ۰ model t (<[r := v ]> σ ₀) σ
      }}}.

    Lemma sstore_2 ٠ get ｰ spec {t σ ₀ σ r} v :
      (σ ∪ σ ₀ ) !! r = Some v →
      {{{
        sstore_2 ۰ model t σ ₀ σ
      }}}
        sstore_2 ٠ get t #r
      {{{
        RET v ;
        sstore_2 ۰ model t σ ₀ σ
      }}}.

    Lemma sstore_2 ٠ set ｰ spec t σ ₀ σ r v :
      r ∈ dom σ ₀ →
      {{{
        sstore_2 ۰ model t σ ₀ σ
      }}}
        sstore_2 ٠ set t #r v
      {{{
        RET ();
        sstore_2 ۰ model t σ ₀ (<[r := v ]> σ)
      }}}.

    Lemma sstore_2 ٠ capture ｰ spec t σ ₀ σ :
      {{{
        sstore_2 ۰ model t σ ₀ σ
      }}}
        sstore_2 ٠ capture t
      {{{
        s
      , RET s ;
        sstore_2 ۰ model t σ ₀ σ ∗
        sstore_2 ۰ snapshot s t σ
      }}}.

    #[local] Definition collect ۰ inv γ σ ₀ root ς cnodes ϵs base descr δs : iProp Σ :=
      root ↦ᵣ §Root ∗
      ( [∗ map ] r ↦ data ∈ store ۰ on σ ₀ ς ,
        r .[ref_gen ] ↦ #data .(gen ) ∗
        r .[ref_value ] ↦ data .(val )
      ) ∗
      ⌜treemap ۰ rooted ϵs base ⌝ ∗
      cnodes ۰ auth γ cnodes ∗

      ⌜cnodes !! base = Some descr ⌝ ∗
      cnode ۰ model γ σ ₀ base descr (root , δs ) ς ∗
      ⌜δs = [] → ς = descr.(descriptor ۰ store)⌝ ∗

      [∗ map ] cnode ↦ descr ; ϵ ∈ delete base cnodes ; ϵs ,
        ∃ descr',
        ⌜cnodes !! ϵ .1 = Some descr'⌝ ∗
        cnode ۰ model γ σ ₀ cnode descr ϵ descr'.(descriptor ۰ store).
    #[local] Lemma sstore_2 ٠ collect ｰ spec ｰ base ｰ chain {γ σ ₀ root ς cnodes ϵs base descr δs} i δ node acc :
      δs !! i = Some δ →
      δ.(delta ۰ node) = node →
      {{{
        collect ۰ inv γ σ ₀ root ς cnodes ϵs base descr δs
      }}}
        sstore_2 ٠ collect #node acc
      {{{
        acc'
      , RET (#root , acc');
        collect ۰ inv γ σ ₀ root ς cnodes ϵs base descr δs ∗
        plist ۰ model acc' acc $ tail $
          (λ δ, #δ.(delta ۰ node)) <$> reverse (drop i δs)
      }}}.
    #[local] Definition collect ｰ specification γ σ ₀ root ς cnodes ϵs base descr δs : iProp Σ :=
      ∀ cnode descr_cnode path acc ,
      {{{
        ⌜cnodes !! cnode = Some descr_cnode ⌝ ∗
        ⌜treemap ۰ path ϵs base cnode path ⌝ ∗
        collect ۰ inv γ σ ₀ root ς cnodes ϵs base descr δs
      }}}
        sstore_2 ٠ collect #cnode acc
      {{{
        acc'
      , RET (#root , acc');
        collect ۰ inv γ σ ₀ root ς cnodes ϵs base descr δs ∗
        plist ۰ model acc' acc $ tail $
          ((λ δ, #δ.(delta ۰ node)) <$> reverse δs ) ++
          ((λ δ, #δ.(delta ۰ node)) <$> reverse (concat path)) ++
          [ #cnode]
      }}}.
    #[local] Lemma sstore_2 ٠ collect ｰ spec ｰ chain {γ σ ₀ root ς cnodes ϵs base descr δs} cnode ϵ i 𝝳 node path acc :
      ϵs !! cnode = Some ϵ →
      ϵ .2 !! i = Some 𝝳 →
      𝝳.(delta ۰ node) = node →
      treemap ۰ path ϵs base ϵ .1 path →
      {{{
        collect ۰ inv γ σ ₀ root ς cnodes ϵs base descr δs ∗
        collect ｰ specification γ σ ₀ root ς cnodes ϵs base descr δs
      }}}
        sstore_2 ٠ collect #node acc
      {{{
        acc'
      , RET (#root , acc');
        collect ۰ inv γ σ ₀ root ς cnodes ϵs base descr δs ∗
        plist ۰ model acc' acc $ tail $
          ((λ δ, #δ.(delta ۰ node)) <$> reverse δs ) ++
          ((λ δ, #δ.(delta ۰ node)) <$> reverse (concat path)) ++
          ((λ δ, #δ.(delta ۰ node)) <$> reverse (drop i ϵ .2))
      }}}.
    #[local] Lemma sstore_2 ٠ collect ｰ spec {γ σ ₀ root ς cnodes ϵs base descr δs} cnode descr_cnode path acc :
      cnodes !! cnode = Some descr_cnode →
      treemap ۰ path ϵs base cnode path →
      {{{
        collect ۰ inv γ σ ₀ root ς cnodes ϵs base descr δs
      }}}
        sstore_2 ٠ collect #cnode acc
      {{{
        acc'
      , RET (#root , acc');
        collect ۰ inv γ σ ₀ root ς cnodes ϵs base descr δs ∗
        plist ۰ model acc' acc $ tail $
          ((λ δ, #δ.(delta ۰ node)) <$> reverse δs ) ++
          ((λ δ, #δ.(delta ۰ node)) <$> reverse (concat path)) ++
          [ #cnode]
      }}}.

    #[local] Definition revert ۰ pre₁ γ σ ₀ root ς cnodes ϵs base descr δs : iProp Σ :=
      ∃ v_root ,
      root ↦ᵣ v_root ∗
      ( [∗ map ] r ↦ data ∈ store ۰ on σ ₀ ς ,
        r .[ref_gen ] ↦ #data .(gen ) ∗
        r .[ref_value ] ↦ data .(val )
      ) ∗
      ⌜treemap ۰ rooted ϵs base ⌝ ∗
      cnodes ۰ auth γ cnodes ∗

      ⌜cnodes !! base = Some descr ⌝ ∗
      cnode ۰ model γ σ ₀ base descr (root , δs ) ς ∗
      ⌜δs = [] → ς = descr.(descriptor ۰ store)⌝ ∗

      [∗ map ] cnode ↦ descr ; ϵ ∈ delete base cnodes ; ϵs ,
        ∃ descr',
        ⌜cnodes !! ϵ .1 = Some descr'⌝ ∗
        cnode ۰ model γ σ ₀ cnode descr ϵ descr'.(descriptor ۰ store).
    #[local] Definition revert ۰ pre₂ γ σ ₀ ς cnodes ϵs base descr_base δs_base cnode descr_cnode δs_cnode node : iProp Σ :=
      ∃ v_node ,
      node ↦ᵣ v_node ∗
      ( [∗ map ] r ↦ data ∈ store ۰ on σ ₀ ς ,
        r .[ref_gen ] ↦ #data .(gen ) ∗
        r .[ref_value ] ↦ data .(val )
      ) ∗
      ⌜treemap ۰ rooted ϵs base ⌝ ∗
      cnodes ۰ auth γ cnodes ∗

      ⌜cnodes !! base = Some descr_base ⌝ ∗
      cnode ۰ model γ σ ₀ base descr_base (node , δs_base ) ς ∗

      ⌜cnodes !! cnode = Some descr_cnode ⌝ ∗
      cnode ۰ model γ σ ₀ cnode descr_cnode (node , δs_cnode ) ς ∗

      [∗ map ] cnode ↦ descr ; ϵ ∈ delete base $ delete cnode cnodes ; delete cnode ϵs ,
        ∃ descr',
        ⌜cnodes !! ϵ .1 = Some descr'⌝ ∗
        cnode ۰ model γ σ ₀ cnode descr ϵ descr'.(descriptor ۰ store).
    #[local] Definition revert ۰ post γ σ ₀ cnodes ϵs base descr : iProp Σ :=
      base ↦ᵣ §Root ∗
      ( [∗ map ] r ↦ data ∈ store ۰ on σ ₀ descr.(descriptor ۰ store),
        r .[ref_gen ] ↦ #data .(gen ) ∗
        r .[ref_value ] ↦ data .(val )
      ) ∗
      ⌜treemap ۰ rooted ϵs base ⌝ ∗
      cnodes ۰ auth γ cnodes ∗

      cnode ۰ model γ σ ₀ base descr (base , []) descr.(descriptor ۰ store) ∗

      [∗ map ] cnode ↦ descr ; ϵ ∈ delete base cnodes ; ϵs ,
        ∃ descr',
        ⌜cnodes !! ϵ .1 = Some descr'⌝ ∗
        cnode ۰ model γ σ ₀ cnode descr ϵ descr'.(descriptor ۰ store).
    #[local] Lemma sstore_2 ٠ revert ｰ spec ｰ aux {γ σ ₀ ς cnodes ϵs base descr_base δs_base cnode descr_cnode δs_cnode node} base' descr_base' path δs acc :
      cnodes !! base' = Some descr_base' →
      treemap ۰ path ϵs cnode base' path →
      ϵs !! cnode = Some (base , δs ) →
      0 < length δs_cnode →
      NoDup (delta ۰ ref <$> δs_cnode ++ δs_base) →
      list ۰ model' acc $ tail $
        ((λ δ, #δ.(delta ۰ node)) <$> reverse δs_cnode ) ++
        ((λ δ, #δ.(delta ۰ node)) <$> reverse (concat path)) ++
        [ #base'] →
      {{{
        revert ۰ pre₂ γ σ ₀ ς cnodes ϵs base descr_base δs_base cnode descr_cnode δs_cnode node
      }}}
        sstore_2 ٠ revert #node acc
      {{{
        ϵs
      , RET ();
        revert ۰ post γ σ ₀ cnodes ϵs base' descr_base'
      }}}.
    #[local] Lemma sstore_2 ٠ revert ｰ spec {γ σ ₀ root ς cnodes ϵs base descr_base δs} base' descr_base' path acc :
      cnodes !! base' = Some descr_base' →
      treemap ۰ path ϵs base base' path →
      list ۰ model' acc $ tail $
        ((λ δ, #δ.(delta ۰ node)) <$> reverse δs ) ++
        ((λ δ, #δ.(delta ۰ node)) <$> reverse (concat path)) ++
        [ #base'] →
      {{{
        revert ۰ pre₁ γ σ ₀ root ς cnodes ϵs base descr_base δs
      }}}
        sstore_2 ٠ revert #root acc
      {{{
        ϵs
      , RET ();
        revert ۰ post γ σ ₀ cnodes ϵs base' descr_base'
      }}}.
    #[local] Lemma sstore_2 ٠ reroot ｰ spec {γ σ ₀ root ς cnodes ϵs base descr δs} base' descr' path :
      cnodes !! base' = Some descr' →
      treemap ۰ path ϵs base base' path →
      {{{
        collect ۰ inv γ σ ₀ root ς cnodes ϵs base descr δs
      }}}
        sstore_2 ٠ reroot #base'
      {{{
        ϵs
      , RET ();
        revert ۰ post γ σ ₀ cnodes ϵs base' descr'
      }}}.

    Lemma sstore_2 ٠ restore ｰ spec t σ ₀ σ s σ' :
      {{{
        sstore_2 ۰ model t σ ₀ σ ∗
        sstore_2 ۰ snapshot s t σ'
      }}}
        sstore_2 ٠ restore t s
      {{{
        RET ();
        sstore_2 ۰ model t σ ₀ σ'
      }}}.
  End sstore_2 ۰ G.

  #[global] Opaque sstore_2 ۰ model.
  #[global] Opaque sstore_2 ۰ snapshot.
End base.

Require zoo_persistent.sstore_2__opaque.

Class Sstore2G Σ `{zoo ۰ G : !ZooG Σ} :=
  { #[local] sstore_2 ۰ G ۰ raw ۰ G :: base.Sstore2G Σ
  ; #[local] sstore_2 ۰ G ۰ support ۰ G :: MonoGmapG Σ location val
  }.

Definition sstore_2 ۰ Σ :=
  #[base.sstore_2 ۰ Σ
  ; mono_gmap ۰ Σ location val
  ].
#[global] Instance subG ｰ sstore_2 ۰ Σ Σ `{zoo ۰ G : !ZooG Σ} :
  subG sstore_2 ۰ Σ Σ →
  Sstore2G Σ.

Section sstore_2 ۰ G.
  Context `{sstore_2 ۰ G : Sstore2G Σ}.

  #[local] Definition metadata :=
    gname.
  Implicit Type γ : metadata.

  Definition sstore_2 ۰ model t σ : iProp Σ :=
    ∃ l γ σ ₀ ς ,
    ⌜t = #l ⌝ ∗
    ⌜σ ⊆ ς ∪ σ ₀ ⌝ ∗
    l ↪[nroot .@"user"] γ ∗
    mono_gmap ۰ auth γ (DfracOwn 1) σ ₀ ∗
    base.sstore_2 ۰ model t σ ₀ ς.

  Definition sstore_2 ۰ snapshot s t σ : iProp Σ :=
    ∃ l γ σ ₀ ς ,
    ⌜t = #l ⌝ ∗
    ⌜σ ⊆ ς ∪ σ ₀ ⌝ ∗
    l ↪[nroot .@"user"] γ ∗
    mono_gmap ۰ lb γ σ ₀ ∗
    base.sstore_2 ۰ snapshot s t ς.

  #[global] Instance sstore_2 ۰ model ｰ timeless t σ :
    Timeless (sstore_2 ۰ model t σ).

  #[global] Instance sstore_2 ۰ snapshot ｰ persistent s t σ :
    Persistent (sstore_2 ۰ snapshot s t σ).

  Lemma sstore_2 ۰ model ｰ exclusive t σ1 σ2 :
    sstore_2 ۰ model t σ1 -∗
    sstore_2 ۰ model t σ2 -∗
    False.

  Lemma sstore_2 ٠ create ｰ spec :
    {{{
      True
    }}}
      sstore_2 ٠ create ()
    {{{
      t
    , RET t ;
      sstore_2 ۰ model t ∅
    }}}.

  Lemma sstore_2 ٠ ref ｰ spec t σ v :
    {{{
      sstore_2 ۰ model t σ
    }}}
      sstore_2 ٠ ref t v
    {{{
      r
    , RET #r ;
      ⌜σ !! r = None ⌝ ∗
      sstore_2 ۰ model t (<[r := v ]> σ)
    }}}.

  Lemma sstore_2 ٠ get ｰ spec {t σ r} v :
    σ !! r = Some v →
    {{{
      sstore_2 ۰ model t σ
    }}}
      sstore_2 ٠ get t #r
    {{{
      RET v ;
      sstore_2 ۰ model t σ
    }}}.

  Lemma sstore_2 ٠ set ｰ spec t σ r v :
    r ∈ dom σ →
    {{{
      sstore_2 ۰ model t σ
    }}}
      sstore_2 ٠ set t #r v
    {{{
      RET ();
      sstore_2 ۰ model t (<[r := v ]> σ)
    }}}.

  Lemma sstore_2 ٠ capture ｰ spec t σ :
    {{{
      sstore_2 ۰ model t σ
    }}}
      sstore_2 ٠ capture t
    {{{
      s
    , RET s ;
      sstore_2 ۰ model t σ ∗
      sstore_2 ۰ snapshot s t σ
    }}}.

  Lemma sstore_2 ٠ restore ｰ spec t σ s σ' :
    {{{
      sstore_2 ۰ model t σ ∗
      sstore_2 ۰ snapshot s t σ'
    }}}
      sstore_2 ٠ restore t s
    {{{
      RET ();
      sstore_2 ۰ model t σ'
    }}}.
End sstore_2 ۰ G.

#[global] Opaque sstore_2 ۰ model.
#[global] Opaque sstore_2 ۰ snapshot.