| ubi-cons(apebs, vols, wlar, q, bflipset, vtblpnum, sqnum), ubi-io-inv(apebs), n0 ≤ # buf, n < # wlar, n0 ≤ LEB_SIZE, wlar[n].status = free, apebs0 = apebs, is-aligned(n0, EB_PAGE_SIZE), v ∈ vols ∧ m < # vols[v] ∨ v = VTBL_VOLID ∧ m = VTBL_LNUM, vols0 = vols, q0 = q, vtblpnum0 = vtblpnum ⊦ ⟪ubi_atomic_leb_change#(v, m, n, n0, buf, EB_PAGE_SIZE; vols, wlar, q, bflipset, vtblpnum, sqnum, apebs; err)⟫ ( (err = ESUCCESS ∨ ⌊err⌋ ) ∧ id○(apebs, apebs0, n) ∧ ubi-io-inv(apebs) ∧ # apebs = # wlar ∧ unique-sqns(apebs) ∧ valid-global-sqn(apebs, sqnum) ∧ valid-wl(apebs, wlar) ∧ valid-eraseq(q) ∧ valid-eraseq(wlar, q) ∧ valid-eraseq(apebs, q) ∧ ¬ VTBL_VOLID ∈ vols ∧ bflipset-cons(bflipset, wlar) ∧ ( v ∈ vols0 ∨ is-encoded(to-vtbl(vols0), subarray(buf, 0, n0)) ∧ n0 = LEB_SIZE ∨ err ≠ ESUCCESS → valid-ebatbl(apebs, wlar, vols, vtblpnum) ∧ valid-vtbl(apebs, vols, wlar, vtblpnum)) ∧ ( err = ESUCCESS ∧ v = VTBL_VOLID ∧ m = VTBL_LNUM → (∀ v0, m0. ¬ v0 ∈ vols0 ∧ is-encoded(to-vtbl(vols0)[v0, m0], subarray(buf, 0, n0)) ∧ n0 = LEB_SIZE → valid-ebatbl(apebs, wlar, vols[v0, fill(mkebatbl(m0), unmapped)], vtblpnum) ∧ valid-vtbl(apebs, vols[v0, fill(mkebatbl(m0), unmapped)], wlar, vtblpnum))) ∧ (err = ESUCCESS ∧ v ∈ vols0 ∧ vols0[v][m] ≠ unmapped → q = q0 + eq-entry(vols0[v][m].pnum, v × m)) ∧ (err = ESUCCESS ∧ v = VTBL_VOLID ∧ m = VTBL_LNUM → q = q0 + eq-entry(vtblpnum0, v × m)) ∧ id(apebs, apebs0, mapped-pebs(vols0)) ∧ (v = VTBL_VOLID ∧ m = VTBL_LNUM ∨ err ≠ ESUCCESS → vols = vols0) ∧ (v ∈ vols0 ∧ err = ESUCCESS → vols = vols0[v, vols0[v][m, ⌜n⌝ ]]) ∧ ( err = ESUCCESS → apebs[n].fill = align↑(datasize(buf, n0), EB_PAGE_SIZE) ∧ apebs[n].data = subarray(buf, 0, n0) + mkempbuf(LEB_SIZE - n0) ∧ q.lebrefs ⊆ q0.lebrefs ++ (v × m)) ∧ (err ≠ ESUCCESS → q.lebrefs = q0.lebrefs)) |