| # apebs0 = # wlar0, # apebs = # wlar, LEB_SIZE = n2 + n, apebs0[n0] = mkpeb(aehdr, avhdr, subarray(buf, 0, n) + mkempbuf(n2), align↑(datasize(buf, n), EB_PAGE_SIZE), boolvar), vtblpnum < # vols[v], vtblpnum < # avols[v], abs(avols, apebs, vols, q), bflipset-cons(bflipset0, wlar0), bflipset-cons(bflipset, wlar), ebm-cons(avols), is-aligned(n, EB_PAGE_SIZE), ubi-io-inv(apebs0), ubi-io-inv(apebs), unique-sqns(apebs0), unique-sqns(apebs), valid-ebatbl(apebs0, wlar0, vols[v, vols[v][vtblpnum, ⌜n0⌝ ]], vtblpnum1), valid-ebatbl(apebs, wlar, vols, vtblpnum0), valid-eraseq(q0), valid-eraseq(wlar0, q0), valid-eraseq(apebs0, q0), valid-eraseq(apebs, q), valid-eraseq(wlar, q), valid-eraseq(q), valid-global-sqn(apebs0, sqnum0), valid-global-sqn(apebs, sqnum), valid-vtbl(apebs, vols, wlar, vtblpnum0), valid-vtbl(apebs0, vols, wlar0, vtblpnum1), valid-wl(apebs0, wlar0), valid-wl(apebs, wlar), v ∈ vols, v ∈ avols, n ≤ # buf, n ≤ LEB_SIZE, q0.lebrefs ⊆ q.lebrefs ++ (v × vtblpnum), vols[v][vtblpnum] = unmapped → id(apebs0, apebs, mapped-pebs(vols)), vols[v][vtblpnum] ≠ unmapped → id(apebs0, apebs, mapped-pebs(vols) -- vols[v][vtblpnum].pnum) ⊦ abs(avols[v, avols[v][vtblpnum, mapped(subarray(buf, 0, n) + mkempbuf(n2), n)]], apebs0, vols[v, vols[v][vtblpnum, ⌜n0⌝ ]], q), abs(avols[v, avols[v][vtblpnum, mapped(subarray(buf, 0, n) + mkempbuf(n2), n)]], apebs0, vols[v, vols[v][vtblpnum, ⌜n0⌝ ]], q0), VTBL_VOLID ∈ vols, abs○(avols[v, avols[v][vtblpnum, mapped(subarray(buf, 0, n) + mkempbuf(n2), n)]], apebs0, vols[v, vols[v][vtblpnum, ⌜n0⌝ ]], q, v, vtblpnum) ∧ align↑(datasize(buf, n), EB_PAGE_SIZE) ≤ n |
Used simplifier rules: lf-elim-unmapped: ⊦ vols[v][m] ≠ unmapped → (∃ n. vols[v][m] = ⌜n⌝ );%lf-mapped-in-apebs: ⊦ v ∈ vols ∧ m < # vols[v] ∧ vols[v][m] = ⌜n⌝ ∧ valid-ebatbl(apebs, wlar, vols, n0) → n < # apebs;% ⊦ m ≤ n ↔ ¬ n < m; (ss)% ⊦ EB_PAGE_SIZE ≠ 0; (s)%n ≠ 0, is-aligned(m, n) ⊦ m < align↑(m0, n) ↔ m < m0; (s)% ⊦ ¬ n < datasize(buf, n); (s)%⊦ v ∈ avols ∧ m < # avols[v] → ( abs○(avols[v, avols[v][m, leb]], apebs, vols, q, v, m) ↔ abs○(avols, apebs, vols, q, v, m)); (ss)%⊦ v ∈ vols ∧ m < # vols[v] → ( abs○(avols, apebs, vols[v, vols[v][m, ebae]], q, v, m) ↔ abs○(avols, apebs, vols, q, v, m)); (ss)%abs-idset-fwd: ⊦ id(apebs1, apebs0, mapped-pebs(vols)) ∧ valid-ebatbl(apebs0, wlar, vols, n0) ∧ abs(avols, apebs0, vols, q) → abs(avols, apebs1, vols, q); (forward) from specification ubi-abs% ⊦ abs(avols, apebs, vols, q) → abs○(avols, apebs, vols, q, v, m); (ss)%abs-vols-mapped: ⊦ v ∈ vols ∧ m < # vols[v] ∧ vols[v][m] = ⌜n⌝ ∧ abs(avols, apebs, vols, q) → avols[v][m].mapped?; (forward) from specification ubi-abs% ⊦ unmapped ≠ ⌜m⌝ ; (s)% ⊦ m ≠ n → (m ≤ n ↔ m < n); (s)% ⊦ ⌜m⌝ .pnum = m; (s)%⊦ abs(avols, apebs0, vols, q) ∧ v ∈ vols ∧ m < # vols[v] ∧ vols[v][m] = ⌜n⌝ ∧ id(apebs1, apebs0, mapped-pebs(vols) -- n) ∧ valid-ebatbl(apebs0, wlar, vols, n0) → abs○(avols, apebs1, vols, q, v, m); (ss)%# buf = n ⊦ subarray(buf, 0, n) = buf; (s)%n ≠ 0, m % n = 0 ⊦ align↑(m, n) = m; (s)