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

# apebs0 = # wlar, LEB_SIZE = (n1 + n2) + vtblpnum5, apebs0[n4] = mkpeb(aehdr, avhdr, buf2, m0, false), wlar[n4] = wl-entry(m1, used), avols[v][vtblpnum3] = mapped(buf2, m), vols[v][vtblpnum3] = ⌜n4⌝ , apebs0[vols[v][vtblpnum3].pnum, mkpeb(aehdr, avhdr, subarray(buf2, 0, vtblpnum5) + subarray(buf, n3, n2) + mkempbuf(n1), vtblpnum5 + n2, false)] [vols[v][vtblpnum3].pnum ] = mkpeb(aehdr0, avhdr0, buf0, m2, boolvar), avhdr.valid?, aehdr.valid?, n4 < # wlar, n2 < n5, vtblpnum3 < # avols[v], vtblpnum3 < # vols[v], abs(avols, apebs0, vols, q), bflipset-cons(bflipset, wlar), ebm-cons(avols), is-aligned(n2, EB_PAGE_SIZE), is-aligned(n5, EB_PAGE_SIZE), is-aligned(vtblpnum5, EB_PAGE_SIZE), ubi-io-inv(apebs0[n4, mkpeb(aehdr, avhdr, subarray(buf2, 0, vtblpnum5) + subarray(buf, n3, n2) + mkempbuf(n1), vtblpnum5 + n2, false)]), ubi-io-inv(apebs0), ubi-io-peb-inv(mkpeb(aehdr, avhdr, buf2, m0, false)), unique-sqns(apebs0[n4, mkpeb(aehdr, avhdr, subarray(buf2, 0, vtblpnum5) + subarray(buf, n3, n2) + mkempbuf(n1), vtblpnum5 + n2, false)]), unique-sqns(apebs0), valid-ebatbl (apebs0[n4, mkpeb(aehdr, avhdr, subarray(buf2, 0, vtblpnum5) + subarray(buf, n3, n2) + mkempbuf(n1), vtblpnum5 + n2, false)], wlar, vols, vtblpnum4), valid-ebatbl(apebs0, wlar, vols, vtblpnum4), valid-eraseq(apebs0[n4, mkpeb(aehdr, avhdr, subarray(buf2, 0, vtblpnum5) + subarray(buf, n3, n2) + mkempbuf(n1), vtblpnum5 + n2, false)], q), valid-eraseq(apebs0, q), valid-eraseq(wlar, q), valid-eraseq(q), valid-global-sqn(apebs0[n4, mkpeb(aehdr, avhdr, subarray(buf2, 0, vtblpnum5) + subarray(buf, n3, n2) + mkempbuf(n1), vtblpnum5 + n2, false)], sqnum), valid-global-sqn(apebs0, sqnum), valid-vtbl(apebs0, vols, wlar, vtblpnum4), valid-wl(apebs0[n4, mkpeb(aehdr, avhdr, subarray(buf2, 0, vtblpnum5) + subarray(buf, n3, n2) + mkempbuf(n1), vtblpnum5 + n2, false)], wlar), valid-wl(apebs0, wlar), v ∈ vols, v ∈ avols, n3 + n2 ≤ # buf, vtblpnum5 ≤ LEB_SIZE, m0 ≤ LEB_SIZE, m ≤ LEB_SIZE, n2 + vtblpnum5 ≤ LEB_SIZE, m0 ≤ vtblpnum5, m ≤ vtblpnum5, n5 + n3 ≤ # buf, n3 + n5 ≤ # buf, vtblpnum5 + n5 ≤ LEB_SIZE, ⌊err3⌋ ⊦ ⟪debug#("ubi: moving data from PEB " + vols[v][vtblpnum3].pnum.toString); apebs := apebs0[vols[v][vtblpnum3].pnum, mkpeb(aehdr, avhdr, subarray(buf2, 0, vtblpnum5) + subarray(buf, n3, n2) + mkempbuf(n1), vtblpnum5 + n2, false)]; ubi_change# (v, vtblpnum3, vtblpnum5 + n5, copy(buf, n3, copy(buf0, 0, mkbuf(vtblpnum5 + n5), 0, vtblpnum5), vtblpnum5, n5), EB_PAGE_SIZE ; vols, wlar, q, bflipset, vtblpnum4, sqnum, apebs ; err)⟫ ⟨ebm_write#(v, vtblpnum3, vtblpnum5, n3, n5, buf; avols; err1)⟩ (abs(avols, apebs, vols, q) ∧ err = err1), n2 = 0, vtblpnum4 = n4, VTBL_VOLID ∈ vols

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 138:
# apebs0 = # wlar, LEB_SIZE = (n1 + n2) + vtblpnum5, apebs0[n4] = mkpeb(aehdr, avhdr, buf2, m0, false), wlar[n4] = wl-entry(m1, used), avols[v][vtblpnum3] = mapped(buf2, m), vols[v][vtblpnum3] = ⌜n4⌝ , n2 ≠ 0, vtblpnum4 ≠ n4, avhdr.valid?, aehdr.valid?, n4 < # wlar, n2 < n5, vtblpnum3 < # avols[v], vtblpnum3 < # vols[v], abs(avols, apebs0, vols, q), bflipset-cons(bflipset, wlar), ebm-cons(avols), is-aligned(n2, EB_PAGE_SIZE), is-aligned(n5, EB_PAGE_SIZE), is-aligned(vtblpnum5, EB_PAGE_SIZE), ubi-io-inv(apebs0[n4, mkpeb(aehdr, avhdr, subarray(buf2, 0, vtblpnum5) + subarray(buf, n3, n2) + mkempbuf(n1), vtblpnum5 + n2, false)]), ubi-io-inv(apebs0), ubi-io-peb-inv(mkpeb(aehdr, avhdr, buf2, m0, false)), unique-sqns(apebs0[n4, mkpeb(aehdr, avhdr, subarray(buf2, 0, vtblpnum5) + subarray(buf, n3, n2) + mkempbuf(n1), vtblpnum5 + n2, false)]), unique-sqns(apebs0), valid-ebatbl (apebs0[n4, mkpeb(aehdr, avhdr, subarray(buf2, 0, vtblpnum5) + subarray(buf, n3, n2) + mkempbuf(n1), vtblpnum5 + n2, false)], wlar, vols, vtblpnum4), valid-ebatbl(apebs0, wlar, vols, vtblpnum4), valid-eraseq(apebs0[n4, mkpeb(aehdr, avhdr, subarray(buf2, 0, vtblpnum5) + subarray(buf, n3, n2) + mkempbuf(n1), vtblpnum5 + n2, false)], q), valid-eraseq(apebs0, q), valid-eraseq(wlar, q), valid-eraseq(q), valid-global-sqn(apebs0[n4, mkpeb(aehdr, avhdr, subarray(buf2, 0, vtblpnum5) + subarray(buf, n3, n2) + mkempbuf(n1), vtblpnum5 + n2, false)], sqnum), valid-global-sqn(apebs0, sqnum), valid-vtbl(apebs0, vols, wlar, vtblpnum4), valid-wl(apebs0[n4, mkpeb(aehdr, avhdr, subarray(buf2, 0, vtblpnum5) + subarray(buf, n3, n2) + mkempbuf(n1), vtblpnum5 + n2, false)], wlar), valid-wl(apebs0, wlar), v ∈ vols, v ∈ avols, n3 + n2 ≤ # buf, vtblpnum5 ≤ LEB_SIZE, m0 ≤ LEB_SIZE, m ≤ LEB_SIZE, n2 + vtblpnum5 ≤ LEB_SIZE, m0 ≤ vtblpnum5, m ≤ vtblpnum5, n5 + n3 ≤ # buf, n3 + n5 ≤ # buf, vtblpnum5 + n5 ≤ LEB_SIZE, ⌊err3⌋ , ¬ VTBL_VOLID ∈ vols ⊦ ⟪debug#("ubi: moving data from PEB " + vols[v][vtblpnum3].pnum.toString); apebs := apebs0[vols[v][vtblpnum3].pnum, mkpeb(aehdr, avhdr, subarray(buf2, 0, vtblpnum5) + subarray(buf, n3, n2) + mkempbuf(n1), vtblpnum5 + n2, false)]; ubi_change# (v, vtblpnum3, vtblpnum5 + n5, copy(buf, n3, copy(subarray(buf2, 0, vtblpnum5) + subarray(buf, n3, n2) + mkempbuf(n1), 0, mkbuf(vtblpnum5 + n5), 0, vtblpnum5), vtblpnum5, n5), EB_PAGE_SIZE ; vols, wlar, q, bflipset, vtblpnum4, sqnum, apebs ; err)⟫ ⟨ebm_write#(v, vtblpnum3, vtblpnum5, n3, n5, buf; avols; err1)⟩ (abs(avols, apebs, vols, q) ∧ err = err1)

Rule argument

Additional information

Used simplifier rules: ⊦ mkpeb(aehdr, avhdr, buf, m, boolvar) = mkpeb(aehdr0, avhdr0, buf0, m0, boolvar0) ↔ aehdr = aehdr0 ∧ avhdr = avhdr0 ∧ buf = buf0 ∧ m = m0 ∧ (boolvar ↔ boolvar0); (s)%m < # apebs ⊦ apebs[m, apeb][m] = apeb; (s)% ⊦ m < n → (n ≤ m ↔ false); (s)% ⊦ m < n ↔ ¬ n ≤ m; (ss)% ⊦ ⌜m⌝ .pnum = m; (s)