enrich
   zbranch-array-ops
, 
   address-set-array-ops
, 
   zheap, 
   apersistence-base

with
   

   
   
   functions  btree : ref × ref × address × nat × bool × node-index × index-address-store × address-set × address-set × node-status → zheap → bool;
              bnode
             : ref × zbranch-array × nat × nat × nat × nat × bool × node-index × index-address-store × address-set × address-set → zheap → bool
             ;
   predicates  . ≡ . : (zheap → bool) × (zheap → bool);
               btree-inv : ref × address × index-store × index-store × zheap × node-index × node-index;
               btree-sub-clean : ref × nat × zheap;
               commit-inv
              : nat × persistence-state × index-store × index-store × nat-list × group-store × group-store × nat-set × bool × error × ref × ref × 
                address × nat × bool × node-index × index-store × address-set × address-set × address-set × (zheap → bool) × zheap
              ;
   
   variables  fi : node-index;
              alladrs : address-set;
   
   

   

   axioms congruent :  ⊦ P0 ≡ P1 ↔ P0 = P1;
          infinite-memory :  ⊦ ∃ r. r ≠ null ∧ ¬ r ∈ zh;
          btree-inv
          : ⊦   btree-inv(r, adr, istore, istore0, zh, ri, fi)
              ↔   (∃ height, dirty, as, alladrs. 
                       ((btree(null, r, adr, height, dirty, ri, nodes(istore), as, alladrs, ok) * true))(zh) ∧ refsize-cons(istore, as) ∧ adr ∈ istore
                     ∧ alladrs ⊆ dom nodes(istore))
                ∧ (∃ height, dirty, as, alladrs. 
                       ((btree(null, null, adr, height, false, fi, nodes(istore0), as, alladrs, ok) * true))(zh) ∧ refsize-cons(istore0, as)
                     ∧ alladrs ⊆ dom nodes(istore));
          used for: ls;
          btree
          : ⊦   ((btree(rp, r0, adr, height, dirty0, ri, iast, as, alladrs, nstat) * P))(zh0)
              ↔ (∃ r, zh, zbrar, dirty, nused. 
                     (r0 = null ⊃ ¬ dirty ∧ P(zh0);r = r0 ∧ zh = zh0) ∧ (dirty → dirty0) ∧ (adr ∈ as ↔ ¬ dirty) ∧ adr ∈ alladrs ∧ nsize(nused, nstat)
                   ∧ unmodified(adr, mkznode(rp, zbrar, height = 0, dirty, nused), iast)
                   ∧ ((  r => mkznode(rp, zbrar, height = 0, dirty, nused)
                       * bnode(r, zbrar, 0, nused, nused, height, dirty, ri, iast, as -- adr, alladrs -- adr) * P)
                     )(zh));
          bleaf
          : ⊦   bnode(rp, zbrar, m, len, nused, 0, dirty, ri, iast, as, alladrs)
              = (  ⌜m + len ≤ nused ∧ nused ≤ # zbrar ∧ # zbrar = BRANCH_SIZE⌝  ∧ ⌜sorted(zbrar, 0, nused)⌝  ∧ ⌜ri = payload(zbrar, m, len)⌝ 
                 ∧ ⌜as = ∅⌝  ∧ ⌜alladrs = ∅⌝  ∧ emp);
          used for: ls;
          bnode
          : ⊦   bnode(rp, zbrar, m, len, nused, height + 1, dirty, ri, iast, as, alladrs)
              = (  ⌜m + len ≤ nused ∧ nused ≤ # zbrar ∧ # zbrar = BRANCH_SIZE⌝  ∧ ⌜nused ≠ 0 ∧ sorted(zbrar, 0, nused - 1)⌝ 
                 ∧ _∃
                   (λ asar. 
                      _∃
                      (λ asar0. 
                           ⌜  # asar = nused ∧ disj(asar, 0, nused) ∧ union(asar, m, len) = as ∧ # asar0 = nused ∧ disj(asar0, 0, nused)
                            ∧ union(asar0, m, len) = alladrs
                           ⌝
                           
                         ∧ (λ n. 
                                ⌜zbrar[n].branch?⌝ 
                              ∧ btree(rp, zbrar[n].child, zbrar[n].adr, height, dirty, key-range(zbrar, n, nused, ri), iast, asar[n], asar0[n], ok)
                           )⊗_
                           (m, len
                           ))));
          btree-sub-clean
          : ⊦   btree-sub-clean(r, n, zh)
              ↔   r ∈ zh
                ∧ (  ¬ zh[r].leaf
                   → (∀ n0. 
                          n0 < zh[r].usedsize ∧ n0 < n ∧ zh[r].zbranches[n0].branch? ∧ zh[r].zbranches[n0].child ∈ zh
                        → ¬ zh[zh[r].zbranches[n0].child].dirty));
          commit-inv
          : ⊦   commit-inv
                (n, pstate, istore1, istore0, nx, gstore, gstore0, ginval, bv, err, rp, r, adr, height, dirty, ri, istore, as, as0, alladrs, P, zh)
              ↔   (∃ as1. 
                       refsize-cons(istore, as0 ∪ as1) ∧ as1 ∩ dom nodes(istore1) ⊆ as ∧ as1 ∩ as0 = ∅
                     ∧ ((btree(rp, r, adr, height, dirty, ri, nodes(istore) | as1, as1, alladrs, ok) * P))(zh))
                ∧ istore1 ⊑ istore ∧ r ∈ zh ∧ n ≤ zh[r].usedsize ∧ zh[r].dirty ∧ ¬ zh[r].leaf ∧ inv-journal(nx, gstore, gstore0, ginval)
                ∧ inv-index(istore, istore0) ∧ inv-state(pstate, nx, gstore, istore, bv)
                ∧ (err = ESUCCESS → pstate.index? ∧ btree-sub-clean(r, n, zh));

   

   
end enrich