enrich
   ubi-base, 
   recovery-entries

with
   

   
   
   
   predicates  . ⊆ . : volumes × volumes;
               . ⌈ . ⌉ : volumes × volumes × queue;
               is-max : apebs × volumes × wlarray × queue × nat-set × nat × nat;
               indices-erasing : wlarray × nat-list;
               valid-eraseq-stronger : apebs × queue;
              comment: valid-eraseq + no pebs with maxsqnum in eraseq;
               valid-eraseq-strong : apebs × vtbl × queue;
              comment: valid-eraseq-stronger - pebs outside vtbl with maxsqnum may be in eraseq;
               valid-vtbl-weak : apebs × nat;
               valid-recs : apebs × wlarray × recoveryentries;
               valid-recs-sqns : apebs × recoveryentries;
               unmapped-vols : volumes;
               scan-all-inv : nat × apebs × recoveryentries × wlarray × queue × nat-set × nat-list × nat × error;
               . ⊥ . : recoveryentries × volumes;
   
   
   
   

   

   axioms vols-le
          : ⊦   vols0 ⊆ vols1
              ↔ (∀ v. 
                     (v ∈ vols0 ↔ v ∈ vols1)
                   ∧ (v ∈ vols0 → # vols0[v] = # vols1[v] ∧ (∀ m. m < # vols0[v] ∧ vols0[v][m] ≠ unmapped → vols0[v][m] = vols1[v][m])));
          used for: ls;
          vols-eraseq-bound
          : ⊦   vols1⌈vols0, q0⌉
              ↔ (∀ v, m. 
                     v ∈ vols0 ∧ v ∈ vols1 ∧ m < # vols0[v] ∧ m < # vols1[v] ∧ vols0[v][m] = unmapped ∧ vols1[v][m] ≠ unmapped
                   → eq-entry(vols1[v][m].pnum, v × m) ∈ q0);
          used for: ls;
          vols-is-max-weak
          : ⊦   is-max(apebs, vols, wlar, q, bflipset, n0, n1)
              ↔ ubi-cons(apebs, vols, wlar, q, bflipset, n0, n1) ∧ (∃ vtbl. is-encoded(vtbl, apebs[n0].data) ∧ valid-eraseq-strong(apebs, vtbl, q));
          valid-eraseq-stronger-base :  ⊦ valid-eraseq-stronger(apebs, []);
          used for: s, ls;
          valid-eraseq-stronger-rec
          : ⊦   valid-eraseq-stronger(apebs, eqent ' + q)
              ↔   eqent.pnum < # apebs ∧ ¬ eqent.pnum ∈ q
                ∧ (∀ v, m. 
                       (valid-peb(v, m, apebs[eqent.pnum]) ↔ eqent.lebref = v × m)
                     ∧ (eqent.lebref = v × m → apebs[eqent.pnum].vidhdr.sqn ≠ valid-sqns(v, m, apebs).max))
                ∧ valid-eraseq-stronger(apebs, q);
          used for: ls;
          valid-eraseq-strong-base :  ⊦ valid-eraseq-strong(apebs, vtbl, []);
          used for: s, ls;
          valid-eraseq-strong-rec
          : ⊦   valid-eraseq-strong(apebs, vtbl, eqent ' + q)
              ↔   eqent.pnum < # apebs ∧ ¬ eqent.pnum ∈ q
                ∧ (∀ v, m. 
                       (valid-peb(v, m, apebs[eqent.pnum]) ↔ eqent.lebref = v × m)
                     ∧ (eqent.lebref = v × m ∧ v ∈ vtbl ∧ m < vtbl[v] → apebs[eqent.pnum].vidhdr.sqn ≠ valid-sqns(v, m, apebs).max))
                ∧ valid-eraseq-strong(apebs, vtbl, q);
          used for: ls;
          disj :  ⊦ recs ⊥ vols ↔ (∀ v, m. ¬ v × m ∈ recs ∨ ¬ v ∈ vols ∨ ¬ m < # vols[v] ∨ vols[v][m] = unmapped);
          used for: ls;
          valid-vtbl-weak
          : ⊦   valid-vtbl-weak(apebs, n)
              ↔   n < # apebs ∧ valid-peb(VTBL_VOLID, VTBL_LNUM, apebs[n]) ∧ apebs[n].vidhdr.sqn = valid-sqns(VTBL_VOLID, VTBL_LNUM, apebs).max
                ∧ (∃ vtbl. is-encoded(vtbl, apebs[n].data) ∧ ¬ VTBL_VOLID ∈ vtbl);
          valid-recs
          : ⊦   valid-recs(apebs, wlar, recs)
              ↔ (∀ ladr, m. 
                     ladr ∈ recs ∧ recs[ladr].pnum = m
                   ↔ wlar[m].status = used ∧ m < # apebs ∧ apebs[m].vidhdr.vol = ladr.vol ∧ apebs[m].vidhdr.leb = ladr.leb);
          used for: ls;
          valid-recs-sqns
          : ⊦   valid-recs-sqns(apebs, recs)
              ↔ (∀ ladr. ladr ∈ recs → recs[ladr].pnum < # apebs ∧ apebs[recs[ladr].pnum].vidhdr.sqn = recs[ladr].sqn);
          used for: ls;
          unmapped-vols :  ⊦ unmapped-vols(vols) ↔ (∀ v, m. v ∈ vols ∧ m < # vols[v] → vols[v][m] = unmapped);
          used for: ls;
          scan-all-inv
          : ⊦   scan-all-inv(n, apebs, recs, wlar, q, bflipset, nx, n1, err)
              ↔ ¬
                ¬
                (  n ≤ # apebs ∧ (err = ESUCCESS ∨ ⌊err⌋ )
                 ∧ (  err = ESUCCESS
                    →   ubi-io-inv(apebs) ∧ unique-sqns(apebs) ∧ # apebs = # wlar ∧ ¬ dups(nx) ∧ nx < n ∧ indices-erasing(wlar, nx)
                      ∧ valid-global-sqn(subarray(apebs, 0, n), n1) ∧ valid-eraseq(subarray(wlar, 0, n), q)
                      ∧ bflipset-cons(bflipset, subarray(wlar, 0, n)) ∧ valid-eraseq-stronger(subarray(apebs, 0, n), q)
                      ∧ valid-wl(subarray(apebs, 0, n), subarray(wlar, 0, n)) ∧ valid-recs-sqns(apebs, recs)
                      ∧ valid-recs(subarray(apebs, 0, n), subarray(wlar, 0, n), recs)));
          used for: s;
          indices-erasing-base :  ⊦ indices-erasing(wlar, []);
          used for: s, ls;
          indices-erasing-rec :  ⊦ indices-erasing(wlar, n ' + nx) ↔ n < # wlar ∧ wlar[n].status = erasing ∧ indices-erasing(wlar, nx);
          used for: s, ls;

   

   
end enrich