| # apebs0 = # wlar0, # apebs = # wlar, LEB_SIZE = (n1 + m0) + m1, apebs[n] = mkpeb(aehdr, avhdr, mkempbuf(m0) + subarray(buf, m2, m1) + mkempbuf(n1), m3, boolvar), vols0[v][m] = unmapped, m < # vols0[v], bflipset-cons(bflipset, wlar), bflipset-cons(bflipset, wlar0), id(apebs, apebs0, mapped-pebs(vols0)), is-aligned(m1, EB_PAGE_SIZE), is-aligned(m0, EB_PAGE_SIZE), ubi-io-inv(apebs), ubi-io-inv(apebs0), unique-sqns(apebs0), unique-sqns(apebs), valid-ebatbl(apebs0, wlar0, vols0, vtblpnum3), valid-ebatbl(apebs, wlar, vols0[v, vols0[v][m, ⌜n⌝ ]], vtblpnum3), valid-eraseq(apebs0, q0), valid-eraseq(wlar0, q0), valid-eraseq(q0), valid-eraseq(q), valid-eraseq(wlar, q), valid-eraseq(apebs, q), valid-global-sqn(apebs0, sqnum0), valid-global-sqn(apebs, sqnum), valid-vtbl(apebs0, vols0, wlar0, vtblpnum3), valid-vtbl(apebs, vols0, wlar, vtblpnum3), valid-wl(apebs0, wlar0), valid-wl(apebs, wlar), v ∈ vols0, m0 + m1 ≤ LEB_SIZE, m2 + m1 ≤ # buf, m1 ≤ LEB_SIZE, m1 + m2 ≤ # buf, q.lebrefs ⊆ q0.lebrefs ++ (v × m), m1 = 0 → q.lebrefs ⊆ q0.lebrefs, m1 ≠ 0 → m3 = m0 + m1, m1 = 0 → m3 = 0 ⊦ VTBL_VOLID ∈ vols0, vtblpnum3 ∈ q0, vtblpnum3 ∈ q, ∃ n0. vols0[v, vols0[v][m, ⌜n⌝ ]] = vols0[v, vols0[v][m, ⌜n0⌝ ]] ∧ (m1 ≠ 0 → apebs[n0].fill = m0 + m1) ∧ (m1 = 0 → apebs[n0].fill = 0) ∧ apebs[n0].data = mkempbuf(m0) + subarray(buf, m2, m1) + mkempbuf(n1) |
Used simplifier rules: ⊦ mkpeb(aehdr, avhdr, buf, m, boolvar).fill = m; (s)% ⊦ subarray(buf, n, 0) = mkbuf(0); (s)% ⊦ mkbuf(0) + buf = buf; (s)% ⊦ mkempbuf(n0) + mkempbuf(n1) = mkempbuf(n0 + n1); (s)%append-a: ⊦ (buf + buf0) + buf1 = buf + buf0 + buf1; from specification array-splice[buffer]% ⊦ mkpeb(aehdr, avhdr, buf, m, boolvar).data = buf; (s)% ⊦ buf + buf0 = buf + buf1 ↔ buf0 = buf1; (s) Used terms: n