[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 390 from proof prepost-atomic-leb-change (previous step)

# apebs0 = # wlar, LEB_SIZE = n2 + n0, wlar[m] = wl-entry(m2, used), vols[v][m0] = ⌜m⌝ , wlar[n1] = wl-entry(m1, free), apebs0[n1] = mkpeb(aehdr, empty, mkempbuf(LEB_SIZE), 0, false), aehdr.valid?, m0 < # vols[v], n1 < # wlar, m < # wlar, bflipset-cons(bflipset, wlar), is-aligned(n0, EB_PAGE_SIZE), ubi-io-inv(apebs0[n1, mkpeb(aehdr, avidhdr(v, m0, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false)]), ubi-io-inv(apebs0), unique-sqns(apebs0), valid-ebatbl(apebs0, wlar, vols, vtblpnum1), valid-eraseq(q), valid-eraseq(wlar, q), valid-eraseq(apebs0, q), valid-eraseq(q + eq-entry(m, v × m0) '), valid-global-sqn(apebs0, sqnum), valid-peb(v, m0, apebs0[m]), valid-vtbl(apebs0, vols, wlar, vtblpnum1), valid-wl(apebs0, wlar), v ∈ vols, n0 ≤ LEB_SIZE ⊦ m = vtblpnum1, vtblpnum1 = n1, m ∈ q, vtblpnum1 ∈ q, VTBL_VOLID ∈ vols, valid-ebatbl (apebs0[n1, mkpeb(aehdr, avidhdr(v, m0, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false)], wlar[m, wl-entry(m2, erasing)][n1, wl-entry(m1, used)], vols[v, vols[v][m0, ⌜n1⌝ ]], vtblpnum1) ∧ bflipset-cons(bflipset -- m, wlar[m, wl-entry(m2, erasing)][n1, wl-entry(m1, used)]) ∧ valid-eraseq(apebs0[n1, mkpeb(aehdr, avidhdr(v, m0, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false)], q + eq-entry(m, v × m0) ') ∧ valid-eraseq(wlar[m, wl-entry(m2, erasing)][n1, wl-entry(m1, used)], q + eq-entry(m, v × m0) ') ∧ valid-wl (apebs0[n1, mkpeb(aehdr, avidhdr(v, m0, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false)], wlar[m, wl-entry(m2, erasing)][n1, wl-entry(m1, used)]) ∧ valid-global-sqn(apebs0[n1, mkpeb(aehdr, avidhdr(v, m0, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false)], sqnum + 1) ∧ unique-sqns(apebs0[n1, mkpeb(aehdr, avidhdr(v, m0, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false)]), ¬ mkpeb(aehdr, avidhdr(v, m0, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false).bad ∧ mkpeb(aehdr, avidhdr(v, m0, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false).echdr.valid? ∧ (∃ m3, m1, m2. mkpeb(aehdr, avidhdr(v, m0, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false).vidhdr = avidhdr(v, m0, m3, m1, m2) ∧ ( m1 ≠ 0 → m1 ≤ datasize(mkpeb(aehdr, avidhdr(v, m0, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false).data) ∧ m2 = checksum(mkpeb(aehdr, avidhdr(v, m0, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false).data, m1)))

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 391:
# apebs0 = # wlar, LEB_SIZE = n2 + n0, apebs0[n1] = mkpeb(aehdr, empty, mkempbuf(LEB_SIZE), 0, false), wlar[n1] = wl-entry(m1, free), vols[v][m0] = ⌜m⌝ , wlar[m] = wl-entry(m2, used), aehdr.valid?, m < # wlar, n1 < # wlar, m0 < # vols[v], bflipset-cons(bflipset, wlar), is-aligned(n0, EB_PAGE_SIZE), ubi-io-inv(apebs0), ubi-io-inv(apebs0[n1, mkpeb(aehdr, avidhdr(v, m0, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false)]), unique-sqns(apebs0), valid-ebatbl(apebs0, wlar, vols, vtblpnum1), valid-eraseq(q + eq-entry(m, v × m0) '), valid-eraseq(apebs0, q), valid-eraseq(wlar, q), valid-eraseq(q), valid-global-sqn(apebs0, sqnum), valid-peb(v, m0, apebs0[m]), valid-vtbl(apebs0, vols, wlar, vtblpnum1), valid-wl(apebs0, wlar), v ∈ vols, n0 ≤ LEB_SIZE ⊦ m = vtblpnum1, vtblpnum1 = n1, VTBL_VOLID ∈ vols, vtblpnum1 ∈ q, m ∈ q, ∃ m3, m5. avidhdr(v, m0, sqnum, 0, 0) = avidhdr(v, m0, m3, 0, m5), valid-ebatbl (apebs0[n1, mkpeb(aehdr, avidhdr(v, m0, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false)], wlar[m, wl-entry(m2, erasing)][n1, wl-entry(m1, used)], vols[v, vols[v][m0, ⌜n1⌝ ]], vtblpnum1) ∧ bflipset-cons(bflipset -- m, wlar[m, wl-entry(m2, erasing)][n1, wl-entry(m1, used)]) ∧ valid-eraseq(apebs0[n1, mkpeb(aehdr, avidhdr(v, m0, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false)], q + eq-entry(m, v × m0) ') ∧ valid-eraseq(wlar[m, wl-entry(m2, erasing)][n1, wl-entry(m1, used)], q + eq-entry(m, v × m0) ') ∧ valid-wl (apebs0[n1, mkpeb(aehdr, avidhdr(v, m0, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false)], wlar[m, wl-entry(m2, erasing)][n1, wl-entry(m1, used)]) ∧ valid-global-sqn(apebs0[n1, mkpeb(aehdr, avidhdr(v, m0, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false)], sqnum + 1) ∧ unique-sqns(apebs0[n1, mkpeb(aehdr, avidhdr(v, m0, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false)])

Rule argument

Additional information

Used simplifier rules: ⊦ m ≤ 0 ↔ m = 0; (s)% ⊦ datasize(mkempbuf(n)) = 0; (s)% ⊦ mkpeb(aehdr, avhdr, buf, m, boolvar).data = buf; (s)% ⊦ mkpeb(aehdr, avhdr, buf, m, boolvar).vidhdr = avhdr; (s)% ⊦ mkpeb(aehdr, avhdr, buf, m, boolvar).echdr = aehdr; (s)% ⊦ mkpeb(aehdr, avhdr, buf, m, boolvar).bad ↔ boolvar; (s)