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

# apebs0 = # wlar, LEB_SIZE = n4 + align↑(datasize(buf, LEB_SIZE), EB_PAGE_SIZE), LEB_SIZE = n2 + n0, LEB_SIZE = n3 + align↑(datasize(buf, n0), EB_PAGE_SIZE), 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, m0 < # vols[v], n1 < # wlar, bflipset-cons(bflipset, wlar), is-aligned(n0, EB_PAGE_SIZE), ubi-io-inv(apebs0[n1, mkpeb(aehdr, avidhdr(v, m0, sqnum, datasize(buf, n0), checksum(buf, datasize(buf, n0))), mkempbuf(LEB_SIZE), 0, false)]), ubi-io-inv(apebs0), ubi-io-inv (apebs0 [n1, mkpeb (aehdr, avidhdr(v, m0, sqnum, datasize(buf, n0), checksum(buf, datasize(buf, n0))), subarray(buf, 0, n0) + mkempbuf(n2), align↑(datasize(buf, n0), EB_PAGE_SIZE), 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-peb (mkpeb (aehdr, avidhdr(v, m0, sqnum, datasize(buf, n0), checksum(buf, datasize(buf, n0))), subarray(buf, 0, n0) + mkempbuf(n2), align↑(datasize(buf, n0), EB_PAGE_SIZE), false)), valid-vtbl(apebs0, vols, wlar, vtblpnum1), valid-wl(apebs0, wlar), v ∈ vols, align↑(datasize(buf, LEB_SIZE), EB_PAGE_SIZE) ≤ LEB_SIZE, align↑(datasize(buf, n0), EB_PAGE_SIZE) ≤ # buf, align↑(datasize(buf, n0), EB_PAGE_SIZE) ≤ LEB_SIZE, n0 ≤ LEB_SIZE, n0 ≤ # buf ⊦ m = vtblpnum1, vtblpnum1 = n1, VTBL_VOLID ∈ vols, vtblpnum1 ∈ q, m ∈ q, ∃ buf0. buf = mkempbuf(n0) + buf0, valid-ebatbl (apebs0 [n1, mkpeb (aehdr, avidhdr(v, m0, sqnum, datasize(buf, n0), checksum(buf, datasize(buf, n0))), subarray(buf, 0, n0) + mkempbuf(n2), align↑(datasize(buf, n0), EB_PAGE_SIZE), 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, datasize(buf, n0), checksum(buf, datasize(buf, n0))), subarray(buf, 0, n0) + mkempbuf(n2), align↑(datasize(buf, n0), EB_PAGE_SIZE), 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, datasize(buf, n0), checksum(buf, datasize(buf, n0))), subarray(buf, 0, n0) + mkempbuf(n2), align↑(datasize(buf, n0), EB_PAGE_SIZE), false) ], wlar[m, wl-entry(m2, erasing)][n1, wl-entry(m1, used)]) ∧ valid-global-sqn (apebs0 [n1, mkpeb (aehdr, avidhdr(v, m0, sqnum, datasize(buf, n0), checksum(buf, datasize(buf, n0))), subarray(buf, 0, n0) + mkempbuf(n2), align↑(datasize(buf, n0), EB_PAGE_SIZE), false) ], sqnum + 1) ∧ unique-sqns (apebs0 [n1, mkpeb (aehdr, avidhdr(v, m0, sqnum, datasize(buf, n0), checksum(buf, datasize(buf, n0))), subarray(buf, 0, n0) + mkempbuf(n2), align↑(datasize(buf, n0), EB_PAGE_SIZE), false) ])

User applied rule case distinction

And obtained the following new goals

Rule argument

pos: right 7

Additional information

Used simplifier rules: ⊦ m < n ↔ ¬ n ≤ m; (ss)% ⊦ m < n → (n ≤ m ↔ false); (s)%m < # apebs ⊦ unique-sqns(apebs) → ( unique-sqns(apebs[m, apeb]) ↔ ¬ valid-peb(apeb) ∨ ¬ apeb.vidhdr.sqn ∈ valid-sqns(apeb.vidhdr.vol, apeb.vidhdr.leb, apebs) \ (valid-peb(apeb.vidhdr.vol, apeb.vidhdr.leb, apebs[m]) ⊃ {apebs[m].vidhdr.sqn} ;∅ )); (ss)% ⊦ mkpeb(aehdr, avhdr, buf, m, boolvar).vidhdr = avhdr; (s)% ⊦ avidhdr(v, m, m0, m1, m2).sqn = m0; (s)% ⊦ avidhdr(v, m, m0, m1, m2).vol = v; (s)% ⊦ avidhdr(v, m, m0, m1, m2).leb = m; (s)% ⊦ EB_PAGE_SIZE ≠ 0; (s)% ⊦ ¬ valid-peb(v, m, mkpeb(aehdr, empty, buf, m0, boolvar)); (s)% ⊦ bag \ ∅ = bag; (s)% ⊦ valid-global-sqn(apebs, n) → ¬ n ∈ valid-sqns(v, m, apebs); (s)%n ≠ 0, m % n = 0 ⊦ align↑(m, n) = m; (s)