[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 22 from proof prepost-io-write-data (previous step)

# apebs = # wlar, LEB_SIZE = (n0 + m2) + m0, apebs[n] = mkpeb(aehdr, avhdr, buf0, m, false), wlar[n] = wl-entry(m3, used), aehdr.valid?, avhdr.valid?, n < # wlar, bflipset-cons(bflipset, wlar), is-aligned(m2, EB_PAGE_SIZE), is-aligned(m0, EB_PAGE_SIZE), ubi-io-inv(apebs), ubi-io-inv(apebs[n, mkpeb(aehdr, avhdr, subarray(buf0, 0, m0) + subarray(buf, m1, m2) + mkempbuf(n0), m0 + m2, false)]), ubi-io-peb-inv(mkpeb(aehdr, avhdr, buf0, m, false)), unique-sqns(apebs), valid-ebatbl(apebs, wlar, vols, n3), valid-eraseq(apebs, q), valid-eraseq(wlar, q), valid-eraseq(q), valid-global-sqn(apebs, n2), valid-peb(mkpeb(aehdr, avhdr, buf0, m, false)), valid-vtbl(apebs, vols, wlar, n3), valid-wl(apebs, wlar), m ≤ LEB_SIZE, m ≤ m0, m1 + m2 ≤ # buf, m0 + m2 ≤ LEB_SIZE, m0 ≤ LEB_SIZE, m2 + m0 ≤ LEB_SIZE ⊦ n3 = n, n3 ∈ q, VTBL_VOLID ∈ vols, n ∈ q, unique-sqns(apebs[n, mkpeb(aehdr, avhdr, subarray(buf0, 0, m0) + subarray(buf, m1, m2) + mkempbuf(n0), m0 + m2, false)]) ∧ valid-global-sqn(apebs[n, mkpeb(aehdr, avhdr, subarray(buf0, 0, m0) + subarray(buf, m1, m2) + mkempbuf(n0), m0 + m2, false)], n2) ∧ valid-wl(apebs[n, mkpeb(aehdr, avhdr, subarray(buf0, 0, m0) + subarray(buf, m1, m2) + mkempbuf(n0), m0 + m2, false)], wlar) ∧ valid-eraseq(apebs[n, mkpeb(aehdr, avhdr, subarray(buf0, 0, m0) + subarray(buf, m1, m2) + mkempbuf(n0), m0 + m2, false)], q) ∧ valid-ebatbl(apebs[n, mkpeb(aehdr, avhdr, subarray(buf0, 0, m0) + subarray(buf, m1, m2) + mkempbuf(n0), m0 + m2, false)], wlar, vols, n3)

User applied rule insert rewrite lemma

And obtained the following new goals

Proof step 23:
m < # apebs ⊦ apebs[m] = mkpeb(aehdr, avhdr, buf0, m0, boolvar0) ∧ valid-peb(mkpeb(aehdr, avhdr, buf0, m0, boolvar0)) ∧ valid-peb(mkpeb(aehdr, avhdr, buf1, m1, boolvar1)) → (valid-global-sqn(apebs[m, mkpeb(aehdr, avhdr, buf1, m1, boolvar1)], n) ↔ valid-global-sqn(apebs, n))
Proof step 24:
# apebs = # wlar, LEB_SIZE = (n0 + m2) + m0, wlar[n] = wl-entry(m3, used), apebs[n] = mkpeb(aehdr, avhdr, buf0, m, false), avhdr.valid?, aehdr.valid?, n < # wlar, bflipset-cons(bflipset, wlar), is-aligned(m0, EB_PAGE_SIZE), is-aligned(m2, EB_PAGE_SIZE), ubi-io-inv(apebs[n, mkpeb(aehdr, avhdr, subarray(buf0, 0, m0) + subarray(buf, m1, m2) + mkempbuf(n0), m0 + m2, false)]), ubi-io-inv(apebs), ubi-io-peb-inv(mkpeb(aehdr, avhdr, buf0, m, false)), unique-sqns(apebs), valid-ebatbl(apebs, wlar, vols, n3), valid-eraseq(q), valid-eraseq(wlar, q), valid-eraseq(apebs, q), valid-global-sqn(apebs, n2), valid-peb(mkpeb(aehdr, avhdr, buf0, m, false)), valid-vtbl(apebs, vols, wlar, n3), valid-wl(apebs, wlar), m2 + m0 ≤ LEB_SIZE, m0 ≤ LEB_SIZE, m0 + m2 ≤ LEB_SIZE, m1 + m2 ≤ # buf, m ≤ m0, m ≤ LEB_SIZE ⊦ n3 = n, n ∈ q, VTBL_VOLID ∈ vols, n3 ∈ q, unique-sqns(apebs[n, mkpeb(aehdr, avhdr, subarray(buf0, 0, m0) + subarray(buf, m1, m2) + mkempbuf(n0), m0 + m2, false)]) ∧ valid-global-sqn(apebs[n, mkpeb(aehdr, avhdr, subarray(buf0, 0, m0) + subarray(buf, m1, m2) + mkempbuf(n0), m0 + m2, false)], n2) ∧ valid-wl(apebs[n, mkpeb(aehdr, avhdr, subarray(buf0, 0, m0) + subarray(buf, m1, m2) + mkempbuf(n0), m0 + m2, false)], wlar) ∧ valid-eraseq(apebs[n, mkpeb(aehdr, avhdr, subarray(buf0, 0, m0) + subarray(buf, m1, m2) + mkempbuf(n0), m0 + m2, false)], q) ∧ valid-ebatbl(apebs[n, mkpeb(aehdr, avhdr, subarray(buf0, 0, m0) + subarray(buf, m1, m2) + mkempbuf(n0), m0 + m2, false)], wlar, vols, n3), n < # apebs ∧ apebs[n] = mkpeb(aehdr, avhdr, buf0, m, false) ∧ valid-peb(mkpeb(aehdr, avhdr, buf0, m, false)) ∧ valid-peb(mkpeb(aehdr, avhdr, subarray(buf0, 0, m0) + subarray(buf, m1, m2) + mkempbuf(n0), m0 + m2, false))
Proof step 27:
# apebs = # wlar, LEB_SIZE = (n0 + m2) + m0, wlar[n] = wl-entry(m3, used), apebs[n] = mkpeb(aehdr, avhdr, buf0, m, false), avhdr.valid?, aehdr.valid?, n < # wlar, n < # apebs, bflipset-cons(bflipset, wlar), is-aligned(m0, EB_PAGE_SIZE), is-aligned(m2, EB_PAGE_SIZE), ubi-io-inv(apebs[n, mkpeb(aehdr, avhdr, subarray(buf0, 0, m0) + subarray(buf, m1, m2) + mkempbuf(n0), m0 + m2, false)]), ubi-io-inv(apebs), ubi-io-peb-inv(mkpeb(aehdr, avhdr, buf0, m, false)), unique-sqns(apebs), valid-ebatbl(apebs, wlar, vols, n3), valid-eraseq(q), valid-eraseq(wlar, q), valid-eraseq(apebs, q), valid-global-sqn(apebs, n2), valid-peb(mkpeb(aehdr, avhdr, buf0, m, false)), valid-peb(mkpeb(aehdr, avhdr, subarray(buf0, 0, m0) + subarray(buf, m1, m2) + mkempbuf(n0), m0 + m2, false)), valid-vtbl(apebs, vols, wlar, n3), valid-wl(apebs, wlar), m2 + m0 ≤ LEB_SIZE, m0 ≤ LEB_SIZE, m0 + m2 ≤ LEB_SIZE, m1 + m2 ≤ # buf, m ≤ m0, m ≤ LEB_SIZE ⊦ n3 = n, n ∈ q, VTBL_VOLID ∈ vols, n3 ∈ q, unique-sqns(apebs[n, mkpeb(aehdr, avhdr, subarray(buf0, 0, m0) + subarray(buf, m1, m2) + mkempbuf(n0), m0 + m2, false)]) ∧ valid-global-sqn(apebs, n2) ∧ valid-wl(apebs[n, mkpeb(aehdr, avhdr, subarray(buf0, 0, m0) + subarray(buf, m1, m2) + mkempbuf(n0), m0 + m2, false)], wlar) ∧ valid-eraseq(apebs[n, mkpeb(aehdr, avhdr, subarray(buf0, 0, m0) + subarray(buf, m1, m2) + mkempbuf(n0), m0 + m2, false)], q) ∧ valid-ebatbl(apebs[n, mkpeb(aehdr, avhdr, subarray(buf0, 0, m0) + subarray(buf, m1, m2) + mkempbuf(n0), m0 + m2, false)], wlar, vols, n3)

Rule argument

spec: ubi-base name: valid-global-sqn-write-valid seq: m < # apebs ⊦ apebs[m] = mkpeb(aehdr, avhdr, buf0, m0, boolvar0) ∧ valid-peb(mkpeb(aehdr, avhdr, buf0, m0, boolvar0)) ∧ valid-peb(mkpeb(aehdr, avhdr, buf1, m1, boolvar1)) → ( valid-global-sqn (apebs[m, mkpeb(aehdr, avhdr, buf1, m1, boolvar1)], n) ↔ valid-global-sqn(apebs, n)) subst: [buf0, m0, boolvar0, n, boolvar1, m1, buf1, avhdr, aehdr, m, apebs] → [buf0, m, false, n2, false, m0 + m2, subarray(buf0, 0, m0) + subarray(buf, m1, m2) + mkempbuf(n0), avhdr, aehdr, n, apebs] flags: <all paths>

Additional information

Used terms: buf0, m, false, n2, false, m0 + m2, subarray(buf0, 0, m0) + subarray(buf, m1, m2) + mkempbuf(n0), avhdr, aehdr, n, apebs