Proof step 16 from proof prepost-io-write-data (previous step)

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 17:

  # apebs = # wlar, apebs[n] = mkpeb(aehdr, avhdr, buf0, m, false), wlar[n] = wl-entry(m3, used), err0 = ESUCCESS, aehdr.valid?, avhdr.valid?, n < # apebs, n < # wlar, bflipset-cons(bflipset, wlar), is-aligned(m2, EB_PAGE_SIZE), is-aligned(m0, EB_PAGE_SIZE), ubi-io-inv (apebs [n, mkpeb(apebs[n].echdr, apebs[n].vidhdr, subarray(apebs[n].data, 0, m0) + subarray(buf, m1, m2) + mkempbuf(LEB_SIZE - m0 - m2), m0 + m2, apebs[n].bad) ]), ubi-io-inv(apebs), ubi-io-peb-inv(mkpeb(aehdr, avhdr, buf0, m, false)), unique-sqns(apebs), valid-ebatbl(apebs, wlar, vols, n3), valid-eraseq(apebs, q), valid-eraseq(wlar, q), valid-eraseq(q), valid-global-sqn(apebs, n2), valid-peb(mkpeb(aehdr, avhdr, buf0, m, false)), valid-vtbl(apebs, vols, wlar, n3), valid-wl(apebs, wlar), 0 + m0 ≤ # apebs[n].data, m ≤ m0, m1 + m2 ≤ # buf, m0 + m2 ≤ LEB_SIZE, LEB_SIZE - m0 ≥ m2, LEB_SIZE ≥ m0, ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ n3 = n, n3 ∈ q, VTBL_VOLID ∈ vols, n ∈ q, # apebs [n, mkpeb (apebs[n].echdr, apebs[n].vidhdr, subarray(apebs[n].data, 0, m0) + subarray(buf, m1, m2) + mkempbuf(LEB_SIZE - m0 - m2), m0 + m2, apebs[n].bad) ] = # wlar ∧ unique-sqns (apebs [n, mkpeb (apebs[n].echdr, apebs[n].vidhdr, subarray(apebs[n].data, 0, m0) + subarray(buf, m1, m2) + mkempbuf(LEB_SIZE - m0 - m2), m0 + m2, apebs[n].bad) ]) ∧ valid-global-sqn (apebs [n, mkpeb (apebs[n].echdr, apebs[n].vidhdr, subarray(apebs[n].data, 0, m0) + subarray(buf, m1, m2) + mkempbuf(LEB_SIZE - m0 - m2), m0 + m2, apebs[n].bad) ], n2) ∧ valid-wl (apebs [n, mkpeb (apebs[n].echdr, apebs[n].vidhdr, subarray(apebs[n].data, 0, m0) + subarray(buf, m1, m2) + mkempbuf(LEB_SIZE - m0 - m2), m0 + m2, apebs[n].bad) ], wlar) ∧ valid-eraseq (apebs [n, mkpeb (apebs[n].echdr, apebs[n].vidhdr, subarray(apebs[n].data, 0, m0) + subarray(buf, m1, m2) + mkempbuf(LEB_SIZE - m0 - m2), m0 + m2, apebs[n].bad) ], q) ∧ valid-ebatbl (apebs [n, mkpeb (apebs[n].echdr, apebs[n].vidhdr, subarray(apebs[n].data, 0, m0) + subarray(buf, m1, m2) + mkempbuf(LEB_SIZE - m0 - m2), m0 + m2, apebs[n].bad) ], wlar, vols, n3) ∧ valid-vtbl (apebs [n, mkpeb (apebs[n].echdr, apebs[n].vidhdr, subarray(apebs[n].data, 0, m0) + subarray(buf, m1, m2) + mkempbuf(LEB_SIZE - m0 - m2), m0 + m2, apebs[n].bad) ], vols, wlar, n3)

Rule argument

Additional information