| # apebs = # wlar, # apebs0 = # wlar0, LEB_SIZE = (n2 + vtblpnum5) + n, vols[v][vtblpnum3] = unmapped, apebs0[n3] = mkpeb(aehdr, avhdr, buf0, m, boolvar), err = err1, n = 0, vtblpnum3 < # avols[v], vtblpnum3 < # vols[v], abs(avols, apebs0, vols, q), abs(avols, apebs, vols, q), bflipset-cons(bflipset, wlar), bflipset-cons(bflipset, wlar0), ebm-cons(avols), id(apebs0, apebs, mapped-pebs(vols)), is-aligned(vtblpnum5, EB_PAGE_SIZE), is-aligned(n, EB_PAGE_SIZE), ubi-io-inv(apebs), ubi-io-inv(apebs0), unique-sqns(apebs), unique-sqns(apebs0), valid-ebatbl(apebs, wlar, vols, vtblpnum4), valid-ebatbl(apebs0, wlar0, vols0, vtblpnum4), valid-eraseq(q), valid-eraseq(wlar, q), valid-eraseq(apebs, q), valid-eraseq(apebs0, q0), valid-eraseq(wlar0, q0), valid-eraseq(q0), valid-global-sqn(apebs, sqnum), valid-global-sqn(apebs0, sqnum0), valid-vtbl(apebs, vols, wlar, vtblpnum4), valid-vtbl(apebs0, vols0, wlar0, vtblpnum4), valid-wl(apebs, wlar), valid-wl(apebs0, wlar0), v ∈ avols, v ∈ vols, vtblpnum5 + n ≤ LEB_SIZE, n4 + n ≤ # buf, n + n4 ≤ # buf, n ≤ LEB_SIZE, q0.lebrefs ⊆ q.lebrefs ++ (v × vtblpnum3), err1 = ESUCCESS → vols0 = vols[v, vols[v][vtblpnum3, ⌜n3⌝ ]] ∧ (n ≠ 0 → m = vtblpnum5 + n) ∧ (n = 0 → m = 0) ∧ buf0 = mkempbuf(vtblpnum5) + subarray(buf, n4, n) + mkempbuf(n2), err1 ≠ ESUCCESS → vols0 = vols, n = 0 → q0.lebrefs ⊆ q.lebrefs, err1 = ESUCCESS ∨ ⌊err1⌋ ⊦ ⟨skip⟩ (abs(avols, apebs0, vols0, q0) ∧ err1 = err), err = ESUCCESS, avols[v][vtblpnum3].mapped?, VTBL_VOLID ∈ vols, VTBL_VOLID ∈ vols0 |
Used simplifier rules: ⊦ n + 0 = n; (s)%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic%c: ⊦ m + n = n + m; from specification nat-basic% ⊦ 0 ≤ m; (s)% ⊦ EB_PAGE_SIZE ≠ 0; (s)%n ≠ 0 ⊦ is-aligned(0, n); (s)% ⊦ ⌊err⌋ → err ≠ ESUCCESS; (s)% ⊦ s1 ⊆ s2 → s1 ⊆ s2 ++ lref; (s)%⊦ q1.lebrefs ⊆ q0.lebrefs ∧ abs(avols, apebs, vols, q0) → abs(avols, apebs, vols, q1); (ss)