[Imprint][Data Privacy Statement][E-Mail]

View long theorem info. View the proof. Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Proof step 361 from proof prepost-atomic-leb-change (previous step)

# apebs0 = # wlar, LEB_SIZE = n2 + n0, wlar[vtblpnum1] = wl-entry(m0, used), apebs0[n1] = mkpeb(aehdr, empty, mkempbuf(LEB_SIZE), 0, false), wlar[n1] = wl-entry(m1, free), aehdr.valid?, vtblpnum1 < # wlar, n1 < # wlar, bflipset-cons(bflipset -- vtblpnum1, wlar), bflipset-cons(bflipset, wlar), is-aligned(n0, EB_PAGE_SIZE), ubi-io-inv(apebs0), ubi-io-inv(apebs0[n1, mkpeb(aehdr, avidhdr(VTBL_VOLID, VTBL_LNUM, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false)]), unique-sqns(apebs0), valid-ebatbl(apebs0, wlar, vols, vtblpnum1), valid-eraseq(apebs0, q), valid-eraseq(wlar, q), valid-eraseq(q), valid-eraseq(q + eq-entry(vtblpnum1, VTBL_VOLID × VTBL_LNUM) '), valid-global-sqn(apebs0, sqnum), valid-global-sqn(apebs0, sqnum + 1), valid-peb(mkpeb(aehdr, avidhdr(VTBL_VOLID, VTBL_LNUM, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false)), valid-vtbl(apebs0, vols, wlar, vtblpnum1), valid-wl(apebs0, wlar), n0 ≤ LEB_SIZE ⊦ vtblpnum1 = n1, valid-wl (apebs0[n1, mkpeb(aehdr, avidhdr(VTBL_VOLID, VTBL_LNUM, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false)], wlar[vtblpnum1, wl-entry(m0, erasing)][n1, wl-entry(m1, used)]), VTBL_VOLID ∈ vols, vtblpnum1 ∈ q, n1 < # apebs0 ∧ # apebs0 = # wlar[vtblpnum1, wl-entry(m0, erasing)] ∧ valid-wl(apebs0, wlar[vtblpnum1, wl-entry(m0, erasing)]) ∧ valid-peb(mkpeb(aehdr, avidhdr(VTBL_VOLID, VTBL_LNUM, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false)) ∧ ( valid-sqns (mkpeb(aehdr, avidhdr(VTBL_VOLID, VTBL_LNUM, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false).vidhdr.vol, mkpeb(aehdr, avidhdr(VTBL_VOLID, VTBL_LNUM, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false).vidhdr.leb, apebs0) ≠ ∅ → mkpeb(aehdr, avidhdr(VTBL_VOLID, VTBL_LNUM, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false).vidhdr.sqn > valid-sqns (mkpeb(aehdr, avidhdr(VTBL_VOLID, VTBL_LNUM, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false).vidhdr.vol, mkpeb(aehdr, avidhdr(VTBL_VOLID, VTBL_LNUM, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false).vidhdr.leb, apebs0) .max) ∧ (∀ m. m < # wlar[vtblpnum1, wl-entry(m0, erasing)] ∧ m ≠ n1 ∧ wlar[vtblpnum1, wl-entry(m0, erasing)][m].status = used → apebs0[m].vidhdr.vol ≠ mkpeb(aehdr, avidhdr(VTBL_VOLID, VTBL_LNUM, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false).vidhdr.vol ∨ apebs0[m].vidhdr.leb ≠ mkpeb(aehdr, avidhdr(VTBL_VOLID, VTBL_LNUM, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false).vidhdr.leb) ∧ mkpeb(aehdr, avidhdr(VTBL_VOLID, VTBL_LNUM, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false).echdr.ec = m1

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 362:
# apebs0 = # wlar, LEB_SIZE = n2 + n0, wlar[n1] = wl-entry(m1, free), apebs0[n1] = mkpeb(aehdr, empty, mkempbuf(LEB_SIZE), 0, false), wlar[vtblpnum1] = wl-entry(m0, used), aehdr.valid?, valid-sqns(VTBL_VOLID, VTBL_LNUM, apebs0).max < sqnum, n1 < # wlar, vtblpnum1 < # wlar, bflipset-cons(bflipset, wlar), bflipset-cons(bflipset -- vtblpnum1, wlar), is-aligned(n0, EB_PAGE_SIZE), ubi-io-inv(apebs0[n1, mkpeb(aehdr, avidhdr(VTBL_VOLID, VTBL_LNUM, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false)]), ubi-io-inv(apebs0), unique-sqns(apebs0), valid-ebatbl(apebs0, wlar, vols, vtblpnum1), valid-eraseq(q + eq-entry(vtblpnum1, VTBL_VOLID × VTBL_LNUM) '), valid-eraseq(q), valid-eraseq(wlar, q), valid-eraseq(apebs0, q), valid-global-sqn(apebs0, sqnum + 1), valid-global-sqn(apebs0, sqnum), valid-peb(mkpeb(aehdr, avidhdr(VTBL_VOLID, VTBL_LNUM, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false)), valid-vtbl(apebs0, vols, wlar, vtblpnum1), valid-wl(apebs0, wlar), n0 ≤ LEB_SIZE ⊦ vtblpnum1 = n1, valid-wl (apebs0[n1, mkpeb(aehdr, avidhdr(VTBL_VOLID, VTBL_LNUM, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false)], wlar[vtblpnum1, wl-entry(m0, erasing)][n1, wl-entry(m1, used)]), vtblpnum1 ∈ q, VTBL_VOLID ∈ vols, aehdr.ec = m1 ∧ ( m < # wlar ∧ m ≠ n1 ∧ wlar[vtblpnum1, wl-entry(m0, erasing)][m].status = used → apebs0[m].vidhdr.vol ≠ VTBL_VOLID ∨ apebs0[m].vidhdr.leb ≠ VTBL_LNUM)

Rule argument

Additional information

Used simplifier rules: ls-valid-global-sqn-vtbl: ⊦ valid-global-sqn(apebs, sqnum) ∧ valid-vtbl(apebs, vols, wlar, vtblpnum) ∧ valid-wl(apebs, wlar) → ¬ sqnum ≤ valid-sqns(VTBL_VOLID, VTBL_LNUM, apebs).max;% ⊦ m < n → n ≠ 0; (s)%f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic% ⊦ m < n ↔ ¬ n ≤ m; (ss)% ⊦ mkpeb(aehdr, avhdr, buf, m, boolvar).echdr = aehdr; (s)% ⊦ m > n ↔ n < m; (s)% ⊦ avidhdr(v, m, m0, m1, m2).sqn = m0; (s)%⊦ valid-vtbl(apebs, vols, wlar, n0) ∧ valid-wl(apebs, wlar) → valid-sqns(VTBL_VOLID, VTBL_LNUM, apebs) ≠ ∅; (s)% ⊦ avidhdr(v, m, m0, m1, m2).leb = m; (s)% ⊦ avidhdr(v, m, m0, m1, m2).vol = v; (s)% ⊦ mkpeb(aehdr, avhdr, buf, m, boolvar).vidhdr = avhdr; (s)%stat ≠ erroneous ⊦ wlar[m] = wl-entry(m0, stat) ∧ valid-wl(apebs, wlar) → valid-wl(apebs, wlar[m, wl-entry(m1, erasing)]); (ss)% ⊦ used ≠ erroneous; (s)% ⊦ # wlar[n, wle] = # wlar; (s)