Proof step 99 from proof prepost-write-once (previous step)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

• Proof step 100:

  # apebs2 = # wlar0, # apebs0 = # wlar, q0.head = eq-entry(m4, lref), LEB_SIZE = (n2 + m0) + m1, apebs2[vtblpnum1] = mkpeb(aehdr, empty, mkempbuf(LEB_SIZE), 0, false), wlar0[vtblpnum1] = wl-entry(m5, free), vols0[v][m] = unmapped, n ≠ 0, vtblpnum2 ≠ vtblpnum1, aehdr.valid?, m < # vols0[v], vtblpnum1 < # wlar0, n < m1, n < LEB_SIZE, bflipset-cons(bflipset, wlar0), bflipset-cons(bflipset, wlar), id(apebs2, apebs0, mapped-pebs(vols0)), is-aligned(m0, EB_PAGE_SIZE), is-aligned(m1, EB_PAGE_SIZE), is-aligned(n, EB_PAGE_SIZE), ubi-io-inv(apebs2), ubi-io-inv(apebs0), ubi-io-inv(apebs2[vtblpnum1, mkpeb(aehdr, avidhdr(v, m, sqnum, 0, 0), mkempbuf(LEB_SIZE), 0, false)]), ubi-io-inv (apebs2[vtblpnum1, mkpeb(aehdr, avidhdr(v, m, sqnum, 0, 0), mkempbuf(m0) + subarray(buf, m2, n) + mkempbuf(LEB_SIZE - m0 - n), m0 + n, false)]), unique-sqns(apebs2), unique-sqns(apebs0), valid-ebatbl(apebs2, wlar0, vols0, vtblpnum2), valid-ebatbl(apebs0, wlar, vols0, vtblpnum2), valid-eraseq(apebs2, q1), valid-eraseq(wlar0, q1), valid-eraseq(q1), valid-eraseq(q0), valid-eraseq(wlar, q0), valid-eraseq(apebs0, q0), valid-global-sqn(apebs2, sqnum), valid-global-sqn(apebs0, sqnum), valid-vtbl(apebs2, vols0, wlar0, vtblpnum2), valid-vtbl(apebs0, vols0, wlar, vtblpnum2), valid-wl(apebs2, wlar0), valid-wl(apebs0, wlar), v ∈ vols0, n + m0 ≤ LEB_SIZE, m0 + m1 ≤ LEB_SIZE, m1 + m2 ≤ # buf, m1 ≤ LEB_SIZE, m2 + n ≤ # buf, m0 ≤ LEB_SIZE, q1.lebrefs ⊆ q0.lebrefs, ⌊err0⌋ , ¬ vtblpnum2 ∈ q1, ¬ VTBL_VOLID ∈ vols0, ¬ vtblpnum2 ∈ q0, apebs0 = apebs2 ∧ wlar = wlar0 ∧ q0 = q1 ∨ id○(apebs0, apebs2, vtblpnum1) ∧ id○(wlar, wlar0, vtblpnum1) ∧ q0 = eq-entry(vtblpnum1, lref) ' + q1 ⊦ ⟪ubi_wl_put_peb#(v × m, vtblpnum1; wlar0, q1); skip⟫ ( # apebs2 = # wlar0 ∧ unique-sqns (apebs2[vtblpnum1, mkpeb(aehdr, avidhdr(v, m, sqnum, 0, 0), mkempbuf(m0) + subarray(buf, m2, n) + mkempbuf(LEB_SIZE - m0 - n), m0 + n, false)]) ∧ valid-global-sqn (apebs2[vtblpnum1, mkpeb(aehdr, avidhdr(v, m, sqnum, 0, 0), mkempbuf(m0) + subarray(buf, m2, n) + mkempbuf(LEB_SIZE - m0 - n), m0 + n, false)], sqnum + 1) ∧ valid-wl (apebs2[vtblpnum1, mkpeb(aehdr, avidhdr(v, m, sqnum, 0, 0), mkempbuf(m0) + subarray(buf, m2, n) + mkempbuf(LEB_SIZE - m0 - n), m0 + n, false)], wlar0) ∧ valid-eraseq(q1) ∧ valid-eraseq(wlar0, q1) ∧ valid-eraseq (apebs2[vtblpnum1, mkpeb(aehdr, avidhdr(v, m, sqnum, 0, 0), mkempbuf(m0) + subarray(buf, m2, n) + mkempbuf(LEB_SIZE - m0 - n), m0 + n, false)], q1) ∧ bflipset-cons(bflipset, wlar0) ∧ valid-ebatbl (apebs2[vtblpnum1, mkpeb(aehdr, avidhdr(v, m, sqnum, 0, 0), mkempbuf(m0) + subarray(buf, m2, n) + mkempbuf(LEB_SIZE - m0 - n), m0 + n, false)], wlar0, vols0, vtblpnum2) ∧ valid-vtbl(apebs2, vols0, wlar0, vtblpnum2) ∧ id (apebs2[vtblpnum1, mkpeb(aehdr, avidhdr(v, m, sqnum, 0, 0), mkempbuf(m0) + subarray(buf, m2, n) + mkempbuf(LEB_SIZE - m0 - n), m0 + n, false)], apebs0, mapped-pebs(vols0)) ∧ q1.lebrefs ⊆ q0.lebrefs ++ (v × m))

Rule argument

Additional information

Used simplifier rules: ⊦ LEB_SIZE ≠ 0; (s)%fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat%lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic%f: ⊦ m < n → n ≠ 0; (forward) from specification nat-basic%fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat%⊦ m ≠ n0 → ( valid-vtbl(apebs[m, apeb], vols, wlar, n0) ↔ valid-vtbl(apebs, vols, wlar, n0)); (s)% ⊦ m < n → n ≠ 0; (s)% ⊦ ⌊err⌋ → err ≠ ESUCCESS; (s)% ⊦ # apebs[n, apeb] = # apebs; (s)%m < # apebs ⊦ apebs[m, apeb][m, apeb0] = apebs[m, apeb0]; (s)% ⊦ m < n → (n ≤ m ↔ false); (s)% ⊦ m < n ↔ ¬ n ≤ m; (ss)% ⊦ mkpeb(aehdr, avhdr, buf, m, boolvar).bad ↔ boolvar; (s)%append-a: ⊦ (buf + buf0) + buf1 = buf + buf0 + buf1; from specification array-splice[buffer]% ⊦ n1 ≤ n0 → subarray(mkempbuf(n0), 0, n1) = mkempbuf(n1); (s)% ⊦ mkpeb(aehdr, avhdr, buf, m, boolvar).vidhdr = avhdr; (s)% ⊦ mkpeb(aehdr, avhdr, buf, m, boolvar).echdr = aehdr; (s)% ⊦ # mkempbuf(n) = n; (s)% ⊦ mkpeb(aehdr, avhdr, buf, m, boolvar).data = buf; (s)% ⊦ m < # apebs → apebs[m, apeb][m] = apeb; (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)%n0 ≤ n ⊦ m ≤ n - n0 ↔ m + n0 ≤ n; (s)% ⊦ m ≤ n → (n < m ↔ false); (s)% ⊦ m ≤ n ↔ ¬ n < m; (ss)% ⊦ n ≥ m ↔ m ≤ n; (s)