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

# apebs0 = # wlar, LEB_SIZE = n3 + align↑(datasize(buf, n0), EB_PAGE_SIZE), LEB_SIZE = n2 + n0, LEB_SIZE = n4 + align↑(datasize(buf, LEB_SIZE), EB_PAGE_SIZE), 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), lref = v × m0, q0 = q, vtblpnum = m, aehdr.valid?, n1 < # wlar[vtblpnum, wlar[vtblpnum].status:= erasing], vtblpnum < # wlar, n1 < # wlar, m0 < # vols[v], m < # 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))), subarray(buf, 0, n0) + mkempbuf(n2), align↑(datasize(buf, n0), EB_PAGE_SIZE), false) ]), ubi-io-inv(apebs0), ubi-io-inv(apebs0[n1, mkpeb(aehdr, avidhdr(v, m0, sqnum, datasize(buf, n0), checksum(buf, datasize(buf, n0))), mkempbuf(LEB_SIZE), 0, false)]), unique-sqns(apebs0), valid-ebatbl(apebs0, wlar, vols, vtblpnum1), valid-eraseq(q), valid-eraseq(wlar, q), valid-eraseq(apebs0, 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 ≤ # buf, n0 ≤ LEB_SIZE, align↑(datasize(buf, n0), EB_PAGE_SIZE) ≤ LEB_SIZE, align↑(datasize(buf, n0), EB_PAGE_SIZE) ≤ # buf, align↑(datasize(buf, LEB_SIZE), EB_PAGE_SIZE) ≤ LEB_SIZE ⊦ m = vtblpnum1, vtblpnum1 = n1, m ∈ q, vtblpnum1 ∈ q, VTBL_VOLID ∈ vols, ∃ buf0. buf = mkempbuf(n0) + buf0, # apebs0 = # wlar[vtblpnum, wlar[vtblpnum].status:= erasing][n1, wl-entry(wlar[vtblpnum, wlar[vtblpnum].status:= erasing][n1].ec, used)] ∧ 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) ]) ∧ 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) ∧ 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[vtblpnum, wlar[vtblpnum].status:= erasing][n1, wl-entry(wlar[vtblpnum, wlar[vtblpnum].status:= erasing][n1].ec, used)]) ∧ valid-eraseq(q0 + eq-entry(m, v × m0) ') ∧ valid-eraseq (wlar[vtblpnum, wlar[vtblpnum].status:= erasing][n1, wl-entry(wlar[vtblpnum, wlar[vtblpnum].status:= erasing][n1].ec, used)], q0 + eq-entry(m, v × m0) ') ∧ 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) ], q0 + eq-entry(m, v × m0) ') ∧ bflipset-cons (bflipset -- m, wlar[vtblpnum, wlar[vtblpnum].status:= erasing][n1, wl-entry(wlar[vtblpnum, wlar[vtblpnum].status:= erasing][n1].ec, used)]) ∧ 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[vtblpnum, wlar[vtblpnum].status:= erasing][n1, wl-entry(wlar[vtblpnum, wlar[vtblpnum].status:= erasing][n1].ec, used)], vols[v, vols[v][m0, ⌜n1⌝ ]], vtblpnum1) ∧ valid-vtbl (apebs0, vols, wlar[vtblpnum, wlar[vtblpnum].status:= erasing][n1, wl-entry(wlar[vtblpnum, wlar[vtblpnum].status:= erasing][n1].ec, used)], vtblpnum1) ∧ q + eq-entry(vtblpnum, lref) = q0 + eq-entry(m, v × m0) ' ∧ id (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) ], apebs0, mapped-pebs(vols)) ∧ vols[v, vols[v][m0, ⌜n1⌝ ]] = vols[v, vols[v][m0, ⌜n1⌝ ]]

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Rule argument

Additional information

Used simplifier rules: lf-mapped-valid-peb: ⊦ v ∈ vols ∧ m < # vols[v] ∧ vols[v][m] = ⌜n⌝ ∧ valid-ebatbl(apebs, wlar, vols, n0) ∧ valid-wl(apebs, wlar) → valid-peb(v, m, apebs[n]);%lf-mapped-info: ⊦ v ∈ vols ∧ m < # vols[v] ∧ vols[v][m] = ⌜n⌝ ∧ valid-ebatbl(apebs, wlar, vols, n0) → wlar[n].status = used ∧ n ≠ n0 ∧ n < # wlar;%lf-used-valid-peb: ⊦ n < # wlar ∧ wlar[n] = wl-entry(m, used) ∧ apebs[n] = apeb ∧ valid-wl(apebs, wlar) → valid-peb(apeb);%lf-used-info: ⊦ n < # wlar ∧ wlar[n] = wl-entry(m, used) ∧ valid-eraseq(wlar, q) → ¬ n ∈ q;% ⊦ eq-entry(m, lref).pnum = m; (s)% ⊦ valid-eraseq(q + eqent ') ↔ ¬ eqent.pnum ∈ q ∧ valid-eraseq(q); (ss)% ⊦ id(apebs, apebs, ns); (s)%¬ n ∈ ns ⊦ id(apebs1[n, apeb], apebs0, ns) ↔ id(apebs1, apebs0, ns); (s)%n < # wlar, stat ≠ used ⊦ wlar[n] = wl-entry(m, stat) ∧ valid-ebatbl(apebs, wlar, vols, n0) → ¬ n ∈ mapped-pebs(vols); (s)% ⊦ used ≠ free; (s)% ⊦ q + q0 = q + q1 ↔ q0 = q1; (s)%m ≠ n ⊦ wlar[m, wle][n] = wlar[n]; (s)% ⊦ ¬ valid-peb(mkpeb(aehdr, empty, buf, m, boolvar)); (s)% ⊦ wl-entry(m, stat).status = stat; (s)%n < # wlar ⊦ valid-eraseq(wlar, q) ∧ wlar[n] = wl-entry(m, free) → ¬ n ∈ q; (s)% ⊦ v ∈ vols → vols[v, vols[v]] = vols; (s)% ⊦ ebatbl[n] = ebae → ebatbl[n, ebae] = ebatbl; (s)%⊦ m ≠ n0 → ( valid-vtbl(apebs, vols, wlar[m, wle], n0) ↔ valid-vtbl(apebs, vols, wlar, n0)); (s)%m < # wlar ⊦ wlar[m, wle][m, wle0] = wlar[m, wle0]; (s)% ⊦ wl-entry(m, stat).ec = m; (s)% ⊦ m < # wlar → wlar[m, wle][m] = wle; (s)%a: ⊦ (q + q0) + q1 = q + q0 + q1; from specification list[erasequeue-base]% ⊦ q + eqent ' = q0 + eqent0 ' ↔ q = q0 ∧ eqent = eqent0; (ws)% ⊦ q + eqent = q + eqent '; (s)% ⊦ # wlar[n, wle] = # wlar; (s)% ⊦ wle.status:= stat = wl-entry(wle.ec, stat); (s)