| # apebs = # wlar, apebs[n4] = mkpeb(aehdr, avhdr, buf2, m0, false), vols[v][vtblpnum3] = ⌜n4⌝ , avols[v][vtblpnum3] = mapped(buf2, m), wlar[n4] = wl-entry(m1, used), buf0 = buf1, buf1 = mkbuf(vtblpnum5 + n1), n = vtblpnum5, n0 = 0, vtblpnum = 0, vtblpnum0 = vols[v][vtblpnum3].pnum, aehdr.valid?, avhdr.valid?, vtblpnum3 < # vols[v], vtblpnum3 < # avols[v], n4 < # wlar, abs(avols, apebs, vols, q), bflipset-cons(bflipset, wlar), ebm-cons(avols), is-aligned(vtblpnum5, EB_PAGE_SIZE), is-aligned(n1, 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(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 + n1 ≤ LEB_SIZE, n3 + n1 ≤ # buf, n1 + n3 ≤ # buf, m ≤ vtblpnum5, m0 ≤ vtblpnum5, ⌊err0⌋ ⊦ vols[v][vtblpnum3] = unmapped, n1 = 0, vtblpnum4 = n4, ubi-io-read-data-pre(vtblpnum0, vtblpnum, n0, n, buf0, apebs), VTBL_VOLID ∈ vols |
Used simplifier rules: ⊦ mkpeb(aehdr, avhdr, buf, m, boolvar).bad ↔ boolvar; (s)%let: ⊦ n ≤ n0 ∧ n0 ≤ n1 → n ≤ n1; (forward) from specification nat% ⊦ ¬ m + n < m; (s)% ⊦ m < n → n ≠ 0; (s)%fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat%f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic% ⊦ m ≤ n ↔ ¬ n < m; (ss)% ⊦ ⌜m⌝ .pnum = m; (s)% ⊦ unmapped ≠ ⌜m⌝ ; (s)% ⊦ m ≤ m + n; (s)% ⊦ # 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)%⊦ ubi-io-read-data-pre(n, n0, m0, n1, buf, apebs) ↔ n < # apebs ∧ ¬ apebs[n].bad ∧ n0 + n1 ≤ LEB_SIZE ∧ m0 + n1 ≤ # buf; (s)