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

# apebs = # wlar, EB_PAGE_SIZE = EB_PAGE_SIZE, LEB_SIZE = LEB_SIZE, vols[v][vtblpnum3] = ⌜n4⌝ , avols[v][vtblpnum3] = mapped(buf2, m), wlar[n4] = wl-entry(m1, used), apebs[n4] = mkpeb(aehdr, avhdr, buf2, m0, false), avols0 = avols, buf0 = subarray(copy(buf2, 0, mkbuf(vtblpnum5 + n1), 0, vtblpnum5), 0, vtblpnum5) + subarray(buf, n3, n1) + subarray (copy(buf2, 0, mkbuf(vtblpnum5 + n1), 0, vtblpnum5), vtblpnum5 + n1, # copy(buf2, 0, mkbuf(vtblpnum5 + n1), 0, vtblpnum5) - vtblpnum5 - n1), n0 = vtblpnum5 + n1, v0 = v, vtblpnum6 = vtblpnum3, vtblpnum7 = LEB_SIZE, vtblpnum8 = EB_PAGE_SIZE, aehdr.valid?, avhdr.valid?, vtblpnum3 < # vols[v], n4 < # wlar, vtblpnum3 < # avols[v], abs(avols, apebs, vols, q), bflipset-cons(bflipset, wlar), ebm-cons(avols), is-aligned(vtblpnum5, EB_PAGE_SIZE), is-aligned(n1, EB_PAGE_SIZE), is-aligned(vtblpnum5 + n1, EB_PAGE_SIZE), ubi-cons(apebs, vols, wlar, q, bflipset, vtblpnum4, sqnum), ubi-io-inv(apebs), ubi-io-peb-inv(mkpeb(aehdr, avhdr, buf2, m0, false)), unique-sqns(apebs), valid-ebatbl(apebs, wlar, vols, vtblpnum4), valid-eraseq(q), valid-eraseq(wlar, q), valid-eraseq(apebs, q), valid-global-sqn(apebs, sqnum), valid-vtbl(apebs, vols, wlar, vtblpnum4), valid-wl(apebs, wlar), v ∈ vols, v ∈ avols, vtblpnum5 ≤ LEB_SIZE, m ≤ LEB_SIZE, m0 ≤ LEB_SIZE, n1 + n3 ≤ # buf, m ≤ vtblpnum5, m0 ≤ vtblpnum5, n3 + n1 ≤ # buf, vtblpnum5 + n1 ≤ LEB_SIZE, vtblpnum5 + n1 ≤ # ( subarray(copy(buf2, 0, mkbuf(vtblpnum5 + n1), 0, vtblpnum5), 0, vtblpnum5) + subarray(buf, n3, n1) + subarray (copy(buf2, 0, mkbuf(vtblpnum5 + n1), 0, vtblpnum5), vtblpnum5 + n1, # copy(buf2, 0, mkbuf(vtblpnum5 + n1), 0, vtblpnum5) - vtblpnum5 - n1)), ⌊err3⌋ ⊦ [ubi_change# (v, vtblpnum3, vtblpnum5 + n1, subarray(copy(buf2, 0, mkbuf(vtblpnum5 + n1), 0, vtblpnum5), 0, vtblpnum5) + subarray(buf, n3, n1) + subarray (copy(buf2, 0, mkbuf(vtblpnum5 + n1), 0, vtblpnum5), vtblpnum5 + n1, # copy(buf2, 0, mkbuf(vtblpnum5 + n1), 0, vtblpnum5) - vtblpnum5 - n1), EB_PAGE_SIZE ; vols, wlar, q, bflipset, vtblpnum4, sqnum, apebs ; err0)] ( ⟨ebm_change#(v0, vtblpnum6, n0, buf0; avols0; err1)⟩ (abs(avols0, apebs, vols, q) ∧ err0 = err1) → ⟨ebm_write#(v, vtblpnum3, vtblpnum5, n3, n1, buf; avols; err1)⟩ (abs(avols, apebs, vols, q) ∧ err0 = err1)), n1 = 0, vtblpnum4 = n4, VTBL_VOLID ∈ vols

Heuristic simplifier applied rule simplifier

And obtained the following new goals

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

Rule argument

Additional information

Used simplifier rules: m ≠ 0, is-aligned(n1, m) ⊦ is-aligned(n0 + n1, m) ↔ is-aligned(n0, m); (s)% ⊦ EB_PAGE_SIZE ≠ 0; (s)%⊦ ubi-cons(apebs, vols, wlar, q, bflipset, n0, n1) ↔ # apebs = # wlar ∧ unique-sqns(apebs) ∧ valid-global-sqn(apebs, n1) ∧ valid-wl(apebs, wlar) ∧ valid-eraseq(q) ∧ valid-eraseq(wlar, q) ∧ valid-eraseq(apebs, q) ∧ ¬ VTBL_VOLID ∈ vols ∧ bflipset-cons(bflipset, wlar) ∧ valid-ebatbl(apebs, wlar, vols, n0) ∧ valid-vtbl(apebs, vols, wlar, n0); (s)% ⊦ # subarray(buf, m, n) = n; (s)% ⊦ #(buf + buf0) = # buf + # buf0; (s)%append-a: ⊦ (buf + buf0) + buf1 = buf + buf0 + buf1; from specification array-splice[buffer]% ⊦ buf + mkbuf(0) = buf; (s)% ⊦ subarray(buf, n, 0) = mkbuf(0); (s)%n1 + n2 ≤ m0, m0 + m1 ≤ # buf ⊦ subarray(copy(buf0, n0, buf, n1, n2), m0, m1) = subarray(buf, m0, m1); (s)% ⊦ m ≤ m; (s)% ⊦ m + n ≤ m + n0 ↔ n ≤ n0; (s)% ⊦ m ≤ m + n; (s)% ⊦ m - m = 0; (s)% ⊦ m + n - m = n; (s)% ⊦ # copy(buf, m, buf0, m0, n) = # buf0; (s)%m1 + n ≤ # buf ⊦ subarray(copy(buf0, m0, buf, m1, n), m1, n) = subarray(buf0, m0, n); (s)% ⊦ ¬ m + n < m; (s)% ⊦ m ≤ n ↔ ¬ n < m; (ss)% ⊦ # mkbuf(n) = n; (s)%c: ⊦ m + n = n + m; from specification nat-basic%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic% ⊦ n + 0 = n; (s)