| # apebs0 = # wlar, n0 + n2 = n5 + n1, LEB_SIZE = (n5 + n1) + vtblpnum5, LEB_SIZE = n7 + vtblpnum5, apebs0[n4] = mkpeb(aehdr, avhdr, buf2, m0, false), wlar[n4] = wl-entry(m1, used), avols2[v][vtblpnum3] = mapped(buf2, m), vols[v][vtblpnum3] = ⌜n4⌝ , n7 = n6 + n5, avhdr.valid?, aehdr.valid?, vtblpnum3 < # avols2[v], n4 < # wlar, vtblpnum3 < # vols[v], n2 < n5, abs(avols2, apebs0, vols, q), abs (avols2[v, avols2[v][vtblpnum3, mapped(subarray(buf2, 0, vtblpnum5) + subarray(buf0, n3, n2) + mkempbuf(n0), vtblpnum5 + n2)]], apebs0[n4, mkpeb(aehdr, avhdr, subarray(buf2, 0, vtblpnum5) + subarray(buf0, n3, n2) + mkempbuf(n0), vtblpnum5 + n2, false)], vols, q), abs (avols2[v, avols2[v][vtblpnum3, mapped((subarray(buf2, 0, vtblpnum5) + subarray(buf0, n3, n5)) + mkempbuf(n1), vtblpnum5 + n5)]], apebs1, vols0, q0), bflipset-cons(bflipset, wlar), ebm-cons(avols2), ebm-cons(avols2[v, avols2[v][vtblpnum3, mapped(subarray(buf2, 0, vtblpnum5) + subarray(buf0, n3, n2) + mkempbuf(n0), vtblpnum5 + n2)]]), is-aligned(vtblpnum5, EB_PAGE_SIZE), is-aligned(n2, EB_PAGE_SIZE), is-aligned(n5, EB_PAGE_SIZE), ubi-io-inv(apebs0), ubi-io-inv(apebs0[n4, mkpeb(aehdr, avhdr, subarray(buf2, 0, vtblpnum5) + subarray(buf0, n3, n2) + mkempbuf(n0), vtblpnum5 + n2, false)]), ubi-io-peb-inv(mkpeb(aehdr, avhdr, buf2, m0, false)), unique-sqns(apebs0[n4, mkpeb(aehdr, avhdr, subarray(buf2, 0, vtblpnum5) + subarray(buf0, n3, n2) + mkempbuf(n0), vtblpnum5 + n2, false)]), unique-sqns(apebs0), valid-ebatbl (apebs0[n4, mkpeb(aehdr, avhdr, subarray(buf2, 0, vtblpnum5) + subarray(buf0, n3, n2) + mkempbuf(n0), vtblpnum5 + n2, false)], wlar, vols, vtblpnum4), valid-ebatbl(apebs0, wlar, vols, vtblpnum4), valid-eraseq(apebs0[n4, mkpeb(aehdr, avhdr, subarray(buf2, 0, vtblpnum5) + subarray(buf0, n3, n2) + mkempbuf(n0), vtblpnum5 + n2, false)], q), valid-eraseq(apebs0, q), valid-eraseq(wlar, q), valid-eraseq(q), valid-global-sqn(apebs0[n4, mkpeb(aehdr, avhdr, subarray(buf2, 0, vtblpnum5) + subarray(buf0, n3, n2) + mkempbuf(n0), vtblpnum5 + n2, false)], sqnum), valid-global-sqn(apebs0, sqnum), valid-vtbl(apebs0, vols, wlar, vtblpnum4), valid-wl(apebs0[n4, mkpeb(aehdr, avhdr, subarray(buf2, 0, vtblpnum5) + subarray(buf0, n3, n2) + mkempbuf(n0), vtblpnum5 + n2, false)], wlar), valid-wl(apebs0, wlar), v ∈ avols2, v ∈ vols, n5 + vtblpnum5 ≤ LEB_SIZE, vtblpnum5 + n5 ≤ LEB_SIZE, vtblpnum5 ≤ LEB_SIZE, m0 ≤ LEB_SIZE, m ≤ LEB_SIZE, n2 + vtblpnum5 ≤ LEB_SIZE, m0 ≤ vtblpnum5, m ≤ vtblpnum5, n5 + n3 ≤ # buf0, n3 + n2 ≤ # buf0, n3 + n5 ≤ # buf0, ⌊err3⌋ ⊦ ⟨avols2[v][vtblpnum3] := mapped(subarray(avols2[v][vtblpnum3].data, 0, vtblpnum5) + subarray(buf0, n3, n5) + mkempbuf(n6), vtblpnum5 + n5)⟩ abs(avols2, apebs1, vols0, q0), n2 = 0, vtblpnum4 = n4, VTBL_VOLID ∈ vols |
Used simplifier rules: lf-mapped-in-apebs: ⊦ v ∈ vols ∧ m < # vols[v] ∧ vols[v][m] = ⌜n⌝ ∧ valid-ebatbl(apebs, wlar, vols, n0) → n < # apebs;%⊦ 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% ⊦ m ≠ n → (m ≤ n ↔ m < n); (s)% ⊦ m < n → m ≤ n; (s)%append-a: ⊦ (buf + buf0) + buf1 = buf + buf0 + buf1; from specification array-splice[buffer]%f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic%lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic%fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat% ⊦ LEB_SIZE ≠ 0; (s)% ⊦ m < m + n ↔ n ≠ 0; (s)%# buf = n ⊦ subarray(buf, 0, n) = buf; (s)%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% ⊦ avols[v, evol][v] = evol; (s)% ⊦ m < # evol → evol[m, leb][m] = leb; (s)% ⊦ # apebs[n, apeb] = # apebs; (s)