| # apebs = # wlar, LEB_SIZE = n2 + vtblpnum5 + n0, LEB_SIZE = n5 + vtblpnum5, apebs[n4] = mkpeb(aehdr, avhdr, buf2, m0, false), wlar[n4] = wl-entry(m1, used), avols[v][vtblpnum3] = mapped(buf2, m), vols[v][vtblpnum3] = ⌜n4⌝ , n5 = n1 + n0, avhdr.valid?, aehdr.valid?, vtblpnum3 < # avols[v], n4 < # wlar, vtblpnum3 < # vols[v], abs(avols[v, avols[v][vtblpnum3, mapped((subarray(buf2, 0, vtblpnum5) + subarray(buf0, n3, n0)) + mkempbuf(n2), vtblpnum5 + n0)]], apebs0, vols0, q0), abs(avols, apebs, vols, q), bflipset-cons(bflipset, wlar), ebm-cons(avols), is-aligned(n0, 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 ∈ vols, v ∈ avols, n0 + vtblpnum5 ≤ LEB_SIZE, vtblpnum5 + n0 ≤ LEB_SIZE, m0 ≤ vtblpnum5, m ≤ vtblpnum5, n0 + n3 ≤ # buf0, m0 ≤ LEB_SIZE, m ≤ LEB_SIZE, vtblpnum5 ≤ LEB_SIZE, n3 + n0 ≤ # buf0, ⌊err3⌋ ⊦ ⟨avols[v][vtblpnum3] := mapped(subarray(avols[v][vtblpnum3].data, 0, vtblpnum5) + subarray(buf0, n3, n0) + mkempbuf(n1), vtblpnum5 + n0)⟩ abs(avols, apebs0, vols0, q0), n0 = 0, vtblpnum4 = n4, VTBL_VOLID ∈ vols |
Used simplifier rules: ⊦ v ∈ vols ∧ m < # vols[v] ∧ abs(avols, apebs, vols, q) → m < # avols[v]; (ss)% ⊦ v ∈ vols ∧ abs(avols, apebs, vols, q) → v ∈ avols; (ss)% ⊦ n + 0 = n; (s)%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic%c: ⊦ m + n = n + m; from specification nat-basic%eqs: ⊦ m = n + n0 ∧ m = n + n1 → n0 = n1; (forward) from specification nat-basic% ⊦ mapped(buf, m).data = buf; (s)%⊦ v ∈ avols ∧ m < # avols[v] ∧ avols[v][m] = mapped(buf, n) ∧ ebm-cons(avols) → # buf = LEB_SIZE; (s)% ⊦ mapped(buf, m).mapped?; (s)%let: ⊦ n ≤ n0 ∧ n0 ≤ n1 → n ≤ n1; (forward) from specification nat%append-a: ⊦ (buf + buf0) + buf1 = buf + buf0 + buf1; from specification array-splice[buffer]