| # apebs0 = # wlar, # apebs1 = # wlar, # wlar0 = # wlar, # apebs = # wlar, # wlar2 = # wlar, wlar2[vtblpnum2] = wl-entry(m5, stat), vols[v][m] = ⌜vtblpnum2⌝ , apebs[vtblpnum2] = mkpeb(aechdr(m1), avidhdr(v1, m4, valid-sqns(v, m, apebs).max, m6, m7), buf, m3, false), apebs[vtblpnum1] = mkpeb(aehdr, empty, mkempbuf(LEB_SIZE), 0, false), wlar[vtblpnum2] = wl-entry(m1, used), wlar[vtblpnum1] = wl-entry(m0, free), apebs1[vtblpnum1] = mkpeb(aehdr0, avhdr0, buf, align↑(datasize(buf, LEB_SIZE), EB_PAGE_SIZE), boolvar), apebs0[vtblpnum1] = mkpeb(aehdr1, avhdr, buf0, m2, boolvar0), aehdr.valid?, vtblpnum1 < # wlar, m < # vols[v], vtblpnum2 < # wlar, bflipset-cons(bflipset1, wlar0), bflipset-cons(bflipset, wlar), bflipset-cons(bflipset0, wlar), bflipset-cons(bflipset1, wlar2), id(apebs0, apebs, mapped-pebs(vols) -- vtblpnum2), id(apebs1, apebs, mapped-pebs(vols)), id(apebs0, apebs, ((mapped-pebs(vols) -- vtblpnum2) ++ vtblpnum1) ∩ mapped-pebs(vols)), id○(wlar2, wlar0, vtblpnum2), id○(apebs0, apebs1, vtblpnum2), id○(apebs1, apebs, vtblpnum1), is-aligned(LEB_SIZE, EB_PAGE_SIZE), ubi-io-inv(apebs0), ubi-io-inv(apebs), ubi-io-inv(apebs1), ubi-io-peb-inv(mkpeb(aehdr1, avhdr, buf0, m2, boolvar0)), ubi-io-peb-inv(mkpeb(aechdr(m1), avidhdr(v1, m4, valid-sqns(v, m, apebs).max, m6, m7), buf, m3, false)), ubi-io-peb-inv(mkpeb(aehdr0, avhdr0, buf, align↑(datasize(buf, LEB_SIZE), EB_PAGE_SIZE), boolvar)), unique-sqns(apebs1), unique-sqns(apebs), unique-sqns(apebs0), valid-ebatbl(apebs1, wlar0, vols[v, vols[v][m, ⌜vtblpnum1⌝ ]], vtblpnum), valid-ebatbl(apebs, wlar, vols, vtblpnum4), valid-ebatbl(apebs0, wlar2, vols[v, vols[v][m, ⌜vtblpnum1⌝ ]], vtblpnum), valid-eraseq(q + eq-entry(vtblpnum2, v × m) '), valid-eraseq(wlar0, q + eq-entry(vtblpnum2, v × m) '), valid-eraseq(apebs1, q + eq-entry(vtblpnum2, v × m) '), valid-eraseq(q), valid-eraseq(wlar, q), valid-eraseq(apebs, q), valid-eraseq(wlar2, q), valid-eraseq(apebs0, q), valid-global-sqn(apebs1, sqnum0), valid-global-sqn(apebs, sqnum), valid-global-sqn(apebs0, sqnum0), valid-peb(mkpeb(aechdr(m1), avidhdr(v1, m4, valid-sqns(v, m, apebs).max, m6, m7), buf, m3, false)), valid-peb(v, m, mkpeb(aechdr(m1), avidhdr(v1, m4, valid-sqns(v, m, apebs).max, m6, m7), buf, m3, false)), valid-vtbl(apebs, vols, wlar, vtblpnum4), valid-vtbl(apebs1, vols, wlar0, vtblpnum), valid-vtbl(apebs0, vols, wlar2, vtblpnum), valid-wl(apebs1, wlar0), valid-wl(apebs, wlar), valid-wl(apebs0, wlar2), v ∈ vols, bflipset = ∅ → m1 + WL_THRESHOLD ≤ m0, ∀ n. (n = vtblpnum1 ∨ n ≠ vtblpnum2 ∧ n ∈ mapped-pebs(vols)) ∧ n < # wlar → apebs0[n] = apebs1[n] ⊦ stat = used, vtblpnum = vtblpnum2, vtblpnum2 = vtblpnum4, vtblpnum4 = vtblpnum1, vtblpnum2 ∈ q, vtblpnum4 ∈ q, VTBL_VOLID ∈ vols, vtblpnum ∈ q, buf0 = buf ∧ m2 ≤ m3, vols = vols[v, vols[v][m, ⌜vtblpnum1⌝ ]] ∧ id(apebs0, apebs, (mapped-pebs(vols) -- vtblpnum2) ++ vtblpnum1) |
Used simplifier rules: lf-valid-wl-bad: n < # wlar ⊦ apebs[n] = mkpeb(aehdr, avhdr, buf, m, true) ∧ valid-wl(apebs, wlar) → wlar[n].status = erroneous;%ubi-io-inv-fwd: n < # apebs ⊦ apebs[n] = apeb ∧ ubi-io-inv(apebs) → ubi-io-peb-inv(apeb);%ls-datasize-wear-level: ⊦ ubi-io-peb-inv(mkpeb(aehdr, avhdr, buf, m, false)) → ¬ m < align↑(datasize(buf, LEB_SIZE), EB_PAGE_SIZE);%⊦ mkpeb(aehdr, avhdr, buf, m, boolvar) = mkpeb(aehdr0, avhdr0, buf0, m0, boolvar0) ↔ aehdr = aehdr0 ∧ avhdr = avhdr0 ∧ buf = buf0 ∧ m = m0 ∧ (boolvar ↔ boolvar0); (s)% ⊦ m ≤ n ↔ ¬ n < m; (ss)% ⊦ m < n ↔ ¬ n ≤ m; (ss)% ⊦ m < n → (n ≤ m ↔ false); (s)%f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic%lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic% ⊦ m < n → n ≠ 0; (s)% ⊦ bflipset-cons(∅, wlar); (s)%size-zero-01: ⊦ ns ≠ ∅ → # ns ≠ 0; (forward) from specification set-basic[nat-set] Used terms: vtblpnum1