[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 173 from proof prepost-write-once (previous step)

# apebs2 = # wlar0, # apebs0 = # wlar, q0.head = eq-entry(m4, lref), LEB_SIZE = n1 + m0, vols0[v][m] = unmapped, apebs2[vtblpnum] = mkpeb(aehdr, empty, mkempbuf(LEB_SIZE), 0, false), wlar0[vtblpnum] = wl-entry(m5, free), aehdr.valid?, vtblpnum < # wlar0, m < # vols0[v], bflipset-cons(bflipset, wlar0), bflipset-cons(bflipset, wlar), id(apebs2, apebs0, mapped-pebs(vols0)), is-aligned(m0, EB_PAGE_SIZE), ubi-io-inv(apebs2), ubi-io-inv(apebs0), ubi-io-inv(apebs2[vtblpnum, mkpeb(aehdr, avidhdr(v, m, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false)]), unique-sqns(apebs2), unique-sqns(apebs0), valid-ebatbl(apebs2, wlar0, vols0, vtblpnum2), valid-ebatbl(apebs0, wlar, vols0, vtblpnum2), valid-eraseq(apebs2, q1), valid-eraseq(wlar0, q1), valid-eraseq(q1), valid-eraseq(q0), valid-eraseq(wlar, q0), valid-eraseq(apebs0, q0), valid-global-sqn(apebs2, sqnum), valid-global-sqn(apebs0, sqnum), valid-peb(mkpeb(aehdr, avidhdr(v, m, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false)), valid-vtbl(apebs2, vols0, wlar0, vtblpnum2), valid-vtbl(apebs0, vols0, wlar, vtblpnum2), valid-wl(apebs2, wlar0), valid-wl(apebs0, wlar), v ∈ vols0, m0 ≤ LEB_SIZE, m2 ≤ # buf, q1.lebrefs ⊆ q0.lebrefs, apebs0 = apebs2 ∧ wlar = wlar0 ∧ q0 = q1 ∨ id○(apebs0, apebs2, vtblpnum) ∧ id○(wlar, wlar0, vtblpnum) ∧ q0 = eq-entry(vtblpnum, lref) ' + q1 ⊦ vtblpnum = vtblpnum2, valid-wl(apebs2[vtblpnum, mkpeb(aehdr, avidhdr(v, m, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false)], wlar0[vtblpnum, wl-entry(m5, used)]), vtblpnum2 ∈ q0, VTBL_VOLID ∈ vols0, vtblpnum2 ∈ q1

User applied rule insert rewrite lemma

And obtained the following new goals

Proof step 174:
n < # apebs, # apebs = # wlar ⊦ valid-wl(apebs, wlar) ∧ valid-peb(apeb) ∧ (valid-sqns(apeb.vidhdr.vol, apeb.vidhdr.leb, apebs) ≠ ∅ → apeb.vidhdr.sqn > valid-sqns(apeb.vidhdr.vol, apeb.vidhdr.leb, apebs).max) ∧ apeb.vidhdr.vol ∈ vols ∧ apeb.vidhdr.leb < # vols[apeb.vidhdr.vol] ∧ vols[apeb.vidhdr.vol][apeb.vidhdr.leb] = unmapped ∧ valid-ebatbl(apebs, wlar, vols, n0) ∧ valid-vtbl(apebs, vols, wlar, n0) ∧ ¬ VTBL_VOLID ∈ vols ∧ apeb.echdr.ec = m0 → valid-wl(apebs[n, apeb], wlar[n, wl-entry(m0, used)])
Proof step 175:
# apebs0 = # wlar, # apebs2 = # wlar0, q0.head = eq-entry(m4, lref), LEB_SIZE = n1 + m0, wlar0[vtblpnum] = wl-entry(m5, free), apebs2[vtblpnum] = mkpeb(aehdr, empty, mkempbuf(LEB_SIZE), 0, false), vols0[v][m] = unmapped, aehdr.valid?, m < # vols0[v], vtblpnum < # wlar0, bflipset-cons(bflipset, wlar), bflipset-cons(bflipset, wlar0), id(apebs2, apebs0, mapped-pebs(vols0)), is-aligned(m0, EB_PAGE_SIZE), ubi-io-inv(apebs2[vtblpnum, mkpeb(aehdr, avidhdr(v, m, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false)]), ubi-io-inv(apebs0), ubi-io-inv(apebs2), unique-sqns(apebs0), unique-sqns(apebs2), valid-ebatbl(apebs0, wlar, vols0, vtblpnum2), valid-ebatbl(apebs2, wlar0, vols0, vtblpnum2), valid-eraseq(apebs0, q0), valid-eraseq(wlar, q0), valid-eraseq(q0), valid-eraseq(q1), valid-eraseq(wlar0, q1), valid-eraseq(apebs2, q1), valid-global-sqn(apebs0, sqnum), valid-global-sqn(apebs2, sqnum), valid-peb(mkpeb(aehdr, avidhdr(v, m, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false)), valid-vtbl(apebs0, vols0, wlar, vtblpnum2), valid-vtbl(apebs2, vols0, wlar0, vtblpnum2), valid-wl(apebs0, wlar), valid-wl(apebs2, wlar0), v ∈ vols0, m2 ≤ # buf, m0 ≤ LEB_SIZE, q1.lebrefs ⊆ q0.lebrefs, apebs0 = apebs2 ∧ wlar = wlar0 ∧ q0 = q1 ∨ id○(apebs0, apebs2, vtblpnum) ∧ id○(wlar, wlar0, vtblpnum) ∧ q0 = eq-entry(vtblpnum, lref) ' + q1 ⊦ vtblpnum = vtblpnum2, valid-wl(apebs2[vtblpnum, mkpeb(aehdr, avidhdr(v, m, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false)], wlar0[vtblpnum, wl-entry(m5, used)]), vtblpnum2 ∈ q1, VTBL_VOLID ∈ vols0, vtblpnum2 ∈ q0, vtblpnum < # apebs2 ∧ # apebs2 = # wlar0 ∧ valid-wl(apebs2, wlar0) ∧ valid-peb(mkpeb(aehdr, avidhdr(v, m, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false)) ∧ ( valid-sqns (mkpeb(aehdr, avidhdr(v, m, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false).vidhdr.vol, mkpeb(aehdr, avidhdr(v, m, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false).vidhdr.leb, apebs2) ≠ ∅ → mkpeb(aehdr, avidhdr(v, m, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false).vidhdr.sqn > valid-sqns (mkpeb(aehdr, avidhdr(v, m, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false).vidhdr.vol, mkpeb(aehdr, avidhdr(v, m, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false).vidhdr.leb, apebs2) .max) ∧ mkpeb(aehdr, avidhdr(v, m, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false).vidhdr.vol ∈ vols0 ∧ mkpeb(aehdr, avidhdr(v, m, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false).vidhdr.leb < # vols0[mkpeb(aehdr, avidhdr(v, m, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false).vidhdr.vol] ∧ vols0[mkpeb(aehdr, avidhdr(v, m, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false).vidhdr.vol] [mkpeb(aehdr, avidhdr(v, m, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false).vidhdr.leb ] = unmapped ∧ valid-ebatbl(apebs2, wlar0, vols0, vtblpnum2) ∧ valid-vtbl(apebs2, vols0, wlar0, vtblpnum2) ∧ ¬ VTBL_VOLID ∈ vols0 ∧ mkpeb(aehdr, avidhdr(v, m, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false).echdr.ec = m5

Rule argument

spec: ubi-base name: valid-wl-map seq: n < # apebs, # apebs = # wlar ⊦ valid-wl(apebs, wlar) ∧ valid-peb(apeb) ∧ ( valid-sqns(apeb.vidhdr.vol, apeb.vidhdr.leb, apebs) ≠ ∅ → apeb.vidhdr.sqn > valid-sqns(apeb.vidhdr.vol, apeb.vidhdr.leb, apebs) .max) ∧ apeb.vidhdr.vol ∈ vols ∧ apeb.vidhdr.leb < # vols[apeb.vidhdr.vol] ∧ vols[apeb.vidhdr.vol][apeb.vidhdr.leb] = unmapped ∧ valid-ebatbl(apebs, wlar, vols, n0) ∧ valid-vtbl(apebs, vols, wlar, n0) ∧ ¬ VTBL_VOLID ∈ vols ∧ apeb.echdr.ec = m0 → valid-wl(apebs[n, apeb], wlar[n, wl-entry(m0, used)]) subst: [vols, n0, m0, wlar, apeb, n, apebs] → [vols0, vtblpnum2, m5, wlar0, mkpeb (aehdr, avidhdr(v, m, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false), vtblpnum, apebs2] flags: <all paths>

Additional information

Used terms: vols0, vtblpnum2, m5, wlar0, mkpeb(aehdr, avidhdr(v, m, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false), vtblpnum, apebs2