enrich
   wlarray, 
   sqns, 
   encoding-vtbl
, 
   vtbl-conv, 
   erasequeue
with
   

   
   constants  WL_THRESHOLD : nat;
              UBI_WRITE_RETRIES : nat;
              UBI_ERASE_RETRIES : nat;
   functions  mapped-pebs : volumes → nat-set;
   predicates  ubi-cons : apebs × volumes × wlarray × queue × nat-set × nat × nat;
               bflipset-cons : nat-set × wlarray;
               valid-global-sqn : apebs × nat;
               unique-sqns : apebs;
               valid-eraseq : queue;
               valid-eraseq : wlarray × queue;
               valid-eraseq : apebs × queue;
               valid-wl : apebs × wlarray;
               valid-wl-entry : apeb × wlentry;
               valid-ebatbl : apebs × wlarray × volumes × nat;
               valid-vtbl : apebs × volumes × wlarray × nat;
               erase-worker-inv : apebs × wlarray × nat × error × apebs × volumes × wlarray × queue × erasequeueentry × queue × nat-set × nat × nat;
               write-once-inv : apebs × volumes × wlarray × queue × nat-set × nat × nat × volid × nat × nat × nat × buffer × error;
               id : apebs × apebs × nat-set;
   
   variables  bflipset : nat-set;
   
   

   

   axioms wl-threshold-nonzero :  ⊦ WL_THRESHOLD = 0 ↔ false;
          used for: s, ls;
          ubi-cons
          : ⊦   ubi-cons(apebs, vols, wlar, q, bflipset, n0, n1)
              ↔   # apebs = # wlar ∧ unique-sqns(apebs) ∧ valid-global-sqn(apebs, n1) ∧ valid-wl(apebs, wlar) ∧ valid-eraseq(q)
                ∧ valid-eraseq(wlar, q) ∧ valid-eraseq(apebs, q) ∧ ¬ VTBL_VOLID ∈ vols ∧ bflipset-cons(bflipset, wlar)
                ∧ valid-ebatbl(apebs, wlar, vols, n0) ∧ valid-vtbl(apebs, vols, wlar, n0);
          used for: s, ls;
          bflipset-cons :  ⊦ bflipset-cons(bflipset, wlar) ↔ (∀ n. n ∈ bflipset → n < # wlar ∧ wlar[n].status = used);
          used for: ls;
          valid-global-sqn :  ⊦ valid-global-sqn(apebs, n) ↔ (∀ v, m. valid-sqns(v, m, apebs) ≠ ∅ → n > valid-sqns(v, m, apebs).max);
          used for: ls;
          unique-sqns :  ⊦ unique-sqns(apebs) ↔ (∀ v, m. unique-elems(valid-sqns(v, m, apebs)));
          used for: ls;
          comment: holds if no two apebs with the same mapping have an identical sequence number;
          valid-wl
          : ⊦   valid-wl(apebs, wlar)
              ↔ (∀ n. 
                     n < # wlar
                   →   (wlar[n].status = erroneous ↔ apebs[n].bad) ∧ (wlar[n].status = free → apebs[n].vidhdr = empty)
                     ∧ (wlar[n].status ≠ erroneous ∧ wlar[n].status ≠ erasing → apebs[n].echdr = aechdr(wlar[n].ec))
                     ∧ (wlar[n].status = used → (∃ v, m. valid-peb(v, m, apebs[n]) ∧ apebs[n].vidhdr.sqn = valid-sqns(v, m, apebs).max)));
          used for: ls;
          comment: each entry in the wear leveling array corresponds to the contents of the corresponding PEB on flash;
          valid-eraseqd-base :  ⊦ valid-eraseq([]);
          used for: s, ls;
          valid-eraseqd-rec :  ⊦ valid-eraseq(eqent ' + q) ↔ ¬ eqent.pnum ∈ q ∧ valid-eraseq(q);
          used for: ls;
          valid-eraseqw :  ⊦ valid-eraseq(wlar, q) ↔ (∀ n. n ∈ q ↔ n < # wlar ∧ wlar[n].status = erasing);
          used for: ls;
          valid-eraseqp-base :  ⊦ valid-eraseq(apebs, []);
          used for: s, ls;
          valid-eraseqp-rec
          : ⊦   valid-eraseq(apebs, eqent ' + q)
              ↔   eqent.pnum < # apebs
                ∧ (valid-peb(apebs[eqent.pnum]) → eqent.lebref = apebs[eqent.pnum].vidhdr.vol × apebs[eqent.pnum].vidhdr.leb) ∧ valid-eraseq(apebs, q);
          used for: ls;
          valid-ebatbl
          : ⊦   valid-ebatbl(apebs, wlar, vols, n0)
              ↔ (∀ v, m, n. 
                     vols[v][m] = ⌜n⌝  ∧ v ∈ vols ∧ m < # vols[v]
                   ↔   wlar[n].status = used ∧ n < # apebs ∧ n < # wlar ∧ apebs[n].vidhdr.valid? ∧ apebs[n].vidhdr.vol = v
                     ∧ apebs[n].vidhdr.leb = m ∧ n ≠ n0);
          used for: ls;
          comment: the volume header corresponds to the entry in the ebatbl, bounds are correct and the wear leveling entry is used. Furthermore, the volumes and their sizes correspond to the layout volume;
          valid-vtbl
          : ⊦   valid-vtbl(apebs, vols, wlar, n0)
              ↔   n0 < # apebs ∧ n0 < # wlar ∧ wlar[n0].status = used ∧ apebs[n0].vidhdr.vol = VTBL_VOLID
                ∧ apebs[n0].vidhdr.leb = VTBL_LNUM ∧ is-encoded(to-vtbl(vols), apebs[n0].data);
          used for: ls;
          write-once-inv
          : ⊦   write-once-inv(apebs, vols, wlar, q, bflipset, n0, n1, v, m, n2, n3, buf, err)
              ↔   ubi-cons(apebs, vols, wlar, q, bflipset, n0, n1) ∧ v ∈ vols ∧ m < # vols[v] ∧ (err = ESUCCESS ∨ ⌊err⌋ )
                ∧ (err ≠ ESUCCESS → vols[v][m] = unmapped) ∧ n3 ≤ # buf ∧ is-aligned(n2, EB_PAGE_SIZE) ∧ is-aligned(n3, EB_PAGE_SIZE)
                ∧ n2 + n3 ≤ LEB_SIZE;
          used for: s;
          erase-worker-inv
          : ⊦   erase-worker-inv(apebs0, wlar0, m, err, apebs, vols, wlar, q0, eqent, q1, bflipset, n0, n1)
              ↔   m ≤ UBI_ERASE_RETRIES + 1 ∧ eqent.pnum < # apebs ∧ id○(apebs, apebs0, eqent.pnum) ∧ id○(wlar, wlar0, eqent.pnum)
                ∧ ubi-cons(apebs, vols, wlar, q0 + (eqent + q1), bflipset, n0, n1) ∧ ubi-io-inv(apebs)
                ∧ (err = ESUCCESS → apebs[eqent.pnum].echdr = aechdr(wlar[eqent.pnum].ec) ∧ apebs[eqent.pnum].vidhdr = empty ∧ ¬ apebs[eqent.pnum].bad);
          used for: s;
          id-set
          : ⊦ id(apebs0, apebs1, ns) ↔ # apebs0 = # apebs1 ∧ (∀ n. n ∈ ns ∧ n < # apebs0 ∧ n < # apebs1 → apebs0[n] = apebs1[n]);
          used for: ls;
          mapped-pebs :  ⊦ n ∈ mapped-pebs(vols) ↔ (∃ v, m. v ∈ vols ∧ m < # vols[v] ∧ vols[v][m] = ⌜n⌝ );
          used for: ls;

   

   
end enrich