Proof step 178 from proof refine-write (previous step)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 179:

  # apebs0 = # wlar, LEB_SIZE = (n1 + n2) + vtblpnum5, apebs0[n4] = mkpeb(aehdr, avhdr, buf2, m0, false), wlar[n4] = wl-entry(m1, used), avols[v][vtblpnum3] = mapped(buf2, m), vols[v][vtblpnum3] = ⌜n4⌝ , apebs = apebs0[n4, mkpeb(aehdr, avhdr, subarray(buf2, 0, vtblpnum5) + subarray(buf, n3, n2) + mkempbuf(n1), vtblpnum5 + n2, false)], n2 ≠ 0, vtblpnum4 ≠ n4, avhdr.valid?, aehdr.valid?, vtblpnum3 < # vols[v], n2 < n5, vtblpnum3 < # avols[v], n4 < # wlar, abs(avols, apebs0, vols, q), abs (avols[v, avols[v][vtblpnum3, mapped(subarray(buf2, 0, vtblpnum5) + subarray(buf, n3, n2) + mkempbuf(n1), vtblpnum5 + n2)]], apebs0[n4, mkpeb(aehdr, avhdr, subarray(buf2, 0, vtblpnum5) + subarray(buf, n3, n2) + mkempbuf(n1), vtblpnum5 + n2, false)], vols, q), bflipset-cons(bflipset, wlar), ebm-cons(avols), ebm-cons(avols[v, avols[v][vtblpnum3, mapped(subarray(buf2, 0, vtblpnum5) + subarray(buf, n3, n2) + mkempbuf(n1), vtblpnum5 + n2)]]), is-aligned(n2, EB_PAGE_SIZE), is-aligned(n5, EB_PAGE_SIZE), is-aligned(vtblpnum5, EB_PAGE_SIZE), ubi-io-inv(apebs0), ubi-io-inv(apebs0[n4, mkpeb(aehdr, avhdr, subarray(buf2, 0, vtblpnum5) + subarray(buf, n3, n2) + mkempbuf(n1), 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(buf, n3, n2) + mkempbuf(n1), vtblpnum5 + n2, false)]), unique-sqns(apebs0), valid-ebatbl (apebs0[n4, mkpeb(aehdr, avhdr, subarray(buf2, 0, vtblpnum5) + subarray(buf, n3, n2) + mkempbuf(n1), vtblpnum5 + n2, false)], wlar, vols, vtblpnum4), valid-ebatbl(apebs0, wlar, vols, vtblpnum4), valid-eraseq(apebs0[n4, mkpeb(aehdr, avhdr, subarray(buf2, 0, vtblpnum5) + subarray(buf, n3, n2) + mkempbuf(n1), 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(buf, n3, n2) + mkempbuf(n1), 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(buf, n3, n2) + mkempbuf(n1), vtblpnum5 + n2, false)], wlar), valid-wl(apebs0, wlar), v ∈ avols, v ∈ vols, vtblpnum5 ≤ LEB_SIZE, n3 + n5 ≤ # buf, m0 ≤ LEB_SIZE, m ≤ LEB_SIZE, n2 + vtblpnum5 ≤ LEB_SIZE, m0 ≤ vtblpnum5, m ≤ vtblpnum5, n5 + n3 ≤ # buf, n3 + n2 ≤ # buf, vtblpnum5 + n5 ≤ LEB_SIZE, ⌊err3⌋ , ¬ VTBL_VOLID ∈ vols ⊦ [ubi_change# (v, vtblpnum3, vtblpnum5 + n5, subarray(buf2, 0, vtblpnum5) + subarray(buf, n3, n5), EB_PAGE_SIZE ; vols, wlar, q, bflipset, vtblpnum4, sqnum, apebs ; err)] ( ⟨avols0 := avols[v, avols[v][vtblpnum3, mapped(subarray(buf2, 0, vtblpnum5) + subarray(buf, n3, n2) + mkempbuf(n1), vtblpnum5 + n2)]]; ebm_change#(v, vtblpnum3, vtblpnum5 + n5, subarray(buf2, 0, vtblpnum5) + subarray(buf, n3, n5); avols0; err0)⟩ (abs(avols0, apebs, vols, q) ∧ err = err0) → ⟨ebm_write#(v, vtblpnum3, vtblpnum5, n3, n5, buf; avols; err1)⟩ (abs(avols, apebs, vols, q) ∧ err = err1))

Rule argument

Additional information

Used simplifier rules: ⊦ mapped(buf, m).mapped?; (s)% ⊦ m < # evol → evol[m, leb][m] = leb; (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% ⊦ # evol[n, leb] = # evol; (s)% ⊦ avols[v, evol][v] = evol; (s)%m ≠ 0, is-aligned(n1, m) ⊦ is-aligned(n0 + n1, m) ↔ is-aligned(n0, m); (s)% ⊦ EB_PAGE_SIZE ≠ 0; (s)%⊦ m ≠ n0 → ( valid-vtbl(apebs[m, apeb], vols, wlar, n0) ↔ valid-vtbl(apebs, vols, wlar, n0)); (s)% ⊦ # apebs[n, apeb] = # apebs; (s)%⊦ ubi-cons(apebs, vols, wlar, q, bflipset, n0, n1) ↔ # apebs = # wlar ∧ unique-sqns(apebs) ∧ valid-global-sqn(apebs, n1) ∧ valid-wl(apebs, wlar) ∧ valid-eraseq(q) ∧ valid-eraseq(wlar, q) ∧ valid-eraseq(apebs, q) ∧ ¬ VTBL_VOLID ∈ vols ∧ bflipset-cons(bflipset, wlar) ∧ valid-ebatbl(apebs, wlar, vols, n0) ∧ valid-vtbl(apebs, vols, wlar, n0); (s)% ⊦ v ∈ avols[v, evol]; (s)%c: ⊦ m + n = n + m; from specification nat-basic%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic% ⊦ m ≤ m; (s)% ⊦ m + n ≤ m + n0 ↔ n ≤ n0; (s)%append-a: ⊦ (buf + buf0) + buf1 = buf + buf0 + buf1; from specification array-splice[buffer]% ⊦ # subarray(buf, m, n) = n; (s)% ⊦ #(buf + buf0) = # buf + # buf0; (s)