[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 96 from proof refine-write (previous step)

# apebs0 = # wlar, LEB_SIZE = (n4 + n) + vtblpnum5, LEB_SIZE = n1 + vtblpnum5, apebs0[n2] = mkpeb(aehdr, avhdr, buf2, m0, false), vols[v][vtblpnum3] = ⌜n2⌝ , avols[v][vtblpnum3] = mapped(buf2, m), wlar[n2] = wl-entry(m1, used), n1 = n0 + n, aehdr.valid?, avhdr.valid?, vtblpnum3 < # vols[v], vtblpnum3 < # avols[v], n2 < # wlar, abs(avols, apebs0, vols, q), bflipset-cons(bflipset, wlar), ebm-cons(avols), is-aligned(vtblpnum5, EB_PAGE_SIZE), is-aligned(n, EB_PAGE_SIZE), ubi-io-inv(apebs0), ubi-io-inv(apebs0[n2, mkpeb(aehdr, avhdr, subarray(buf2, 0, vtblpnum5) + subarray(buf, n3, n) + mkempbuf(n4), vtblpnum5 + n, false)]), ubi-io-peb-inv(mkpeb(aehdr, avhdr, buf2, m0, false)), unique-sqns(apebs0), unique-sqns(apebs0[n2, mkpeb(aehdr, avhdr, subarray(buf2, 0, vtblpnum5) + subarray(buf, n3, n) + mkempbuf(n4), vtblpnum5 + n, false)]), valid-ebatbl(apebs0, wlar, vols, vtblpnum4), valid-ebatbl (apebs0[n2, mkpeb(aehdr, avhdr, subarray(buf2, 0, vtblpnum5) + subarray(buf, n3, n) + mkempbuf(n4), vtblpnum5 + n, false)], wlar, vols, vtblpnum4), valid-eraseq(q), valid-eraseq(wlar, q), valid-eraseq(apebs0, q), valid-eraseq(apebs0[n2, mkpeb(aehdr, avhdr, subarray(buf2, 0, vtblpnum5) + subarray(buf, n3, n) + mkempbuf(n4), vtblpnum5 + n, false)], q), valid-global-sqn(apebs0, sqnum), valid-global-sqn(apebs0[n2, mkpeb(aehdr, avhdr, subarray(buf2, 0, vtblpnum5) + subarray(buf, n3, n) + mkempbuf(n4), vtblpnum5 + n, false)], sqnum), valid-vtbl(apebs0, vols, wlar, vtblpnum4), valid-wl(apebs0, wlar), valid-wl(apebs0[n2, mkpeb(aehdr, avhdr, subarray(buf2, 0, vtblpnum5) + subarray(buf, n3, n) + mkempbuf(n4), vtblpnum5 + n, false)], wlar), v ∈ vols, v ∈ avols, n + vtblpnum5 ≤ LEB_SIZE, m ≤ LEB_SIZE, m0 ≤ LEB_SIZE, vtblpnum5 + n ≤ LEB_SIZE, n + n3 ≤ # buf, m ≤ vtblpnum5, m0 ≤ vtblpnum5, vtblpnum5 ≤ LEB_SIZE, n3 + n ≤ # buf ⊦ ⟨avols[v][vtblpnum3] := mapped(subarray(avols[v][vtblpnum3].data, 0, vtblpnum5) + subarray(buf, n3, n) + mkempbuf(n0), vtblpnum5 + n)⟩ abs (avols, apebs0 [vols[v][vtblpnum3].pnum, mkpeb (apebs0[vols[v][vtblpnum3].pnum].echdr, apebs0[vols[v][vtblpnum3].pnum].vidhdr, subarray(apebs0[vols[v][vtblpnum3].pnum].data, 0, vtblpnum5) + subarray(buf, n3, n) + mkempbuf(n4), vtblpnum5 + n, apebs0[vols[v][vtblpnum3].pnum].bad) ], vols, q), n = 0, vtblpnum4 = n2, VTBL_VOLID ∈ vols

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 97:
# apebs0 = # wlar, LEB_SIZE = (n0 + n) + vtblpnum5, wlar[n2] = wl-entry(m1, used), avols[v][vtblpnum3] = mapped(buf2, m), vols[v][vtblpnum3] = ⌜n2⌝ , apebs0[n2] = mkpeb(aehdr, avhdr, buf2, m0, false), n ≠ 0, vtblpnum4 ≠ n2, avhdr.valid?, aehdr.valid?, vtblpnum3 < # avols[v], vtblpnum3 < # vols[v], n2 < # wlar, abs(avols, apebs0, vols, q), bflipset-cons(bflipset, wlar), ebm-cons(avols), is-aligned(n, EB_PAGE_SIZE), is-aligned(vtblpnum5, EB_PAGE_SIZE), ubi-io-inv(apebs0[n2, mkpeb(aehdr, avhdr, subarray(buf2, 0, vtblpnum5) + subarray(buf, n3, n) + mkempbuf(n0), vtblpnum5 + n, false)]), ubi-io-inv(apebs0), ubi-io-peb-inv(mkpeb(aehdr, avhdr, buf2, m0, false)), unique-sqns(apebs0[n2, mkpeb(aehdr, avhdr, subarray(buf2, 0, vtblpnum5) + subarray(buf, n3, n) + mkempbuf(n0), vtblpnum5 + n, false)]), unique-sqns(apebs0), valid-ebatbl (apebs0[n2, mkpeb(aehdr, avhdr, subarray(buf2, 0, vtblpnum5) + subarray(buf, n3, n) + mkempbuf(n0), vtblpnum5 + n, false)], wlar, vols, vtblpnum4), valid-ebatbl(apebs0, wlar, vols, vtblpnum4), valid-eraseq(apebs0[n2, mkpeb(aehdr, avhdr, subarray(buf2, 0, vtblpnum5) + subarray(buf, n3, n) + mkempbuf(n0), vtblpnum5 + n, false)], q), valid-eraseq(apebs0, q), valid-eraseq(wlar, q), valid-eraseq(q), valid-global-sqn(apebs0[n2, mkpeb(aehdr, avhdr, subarray(buf2, 0, vtblpnum5) + subarray(buf, n3, n) + mkempbuf(n0), vtblpnum5 + n, false)], sqnum), valid-global-sqn(apebs0, sqnum), valid-vtbl(apebs0, vols, wlar, vtblpnum4), valid-wl(apebs0[n2, mkpeb(aehdr, avhdr, subarray(buf2, 0, vtblpnum5) + subarray(buf, n3, n) + mkempbuf(n0), vtblpnum5 + n, false)], wlar), valid-wl(apebs0, wlar), v ∈ avols, v ∈ vols, n3 + n ≤ # buf, vtblpnum5 ≤ LEB_SIZE, m0 ≤ vtblpnum5, m ≤ vtblpnum5, n + n3 ≤ # buf, vtblpnum5 + n ≤ LEB_SIZE, m0 ≤ LEB_SIZE, m ≤ LEB_SIZE, n + vtblpnum5 ≤ LEB_SIZE, ¬ VTBL_VOLID ∈ vols ⊦ ⟨avols[v][vtblpnum3] := mapped(subarray(avols[v][vtblpnum3].data, 0, vtblpnum5) + subarray(buf, n3, n) + mkempbuf(n0), vtblpnum5 + n)⟩ abs (avols, apebs0 [vols[v][vtblpnum3].pnum, mkpeb (apebs0[vols[v][vtblpnum3].pnum].echdr, apebs0[vols[v][vtblpnum3].pnum].vidhdr, subarray(apebs0[vols[v][vtblpnum3].pnum].data, 0, vtblpnum5) + subarray(buf, n3, n) + mkempbuf(n0), vtblpnum5 + n, apebs0[vols[v][vtblpnum3].pnum].bad) ], vols, q)

Rule argument

Additional information

Used simplifier rules: lf-mapped-in-apebs: ⊦ v ∈ vols ∧ m < # vols[v] ∧ vols[v][m] = ⌜n⌝ ∧ valid-ebatbl(apebs, wlar, vols, n0) → n < # apebs;% ⊦ # apebs[n, apeb] = # apebs; (s)%eqs: ⊦ m = n + n0 ∧ m = n + n1 → n0 = n1; (forward) from specification nat-basic%c: ⊦ m + n = n + m; from specification nat-basic%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic