Proof step 21 from proof inv-write-data-wl (previous step)

Heuristic symbolic execution applied rule choose right

And obtained the following new goals

• Proof step 22:

  apebs[n2] = mkpeb(aehdr, avhdr, buf0, 0, false), n1 = align↑(datasize(buf, n1), EB_PAGE_SIZE), aehdr.valid?, avhdr.valid?, n2 < # apebs, is-aligned(# buf1, EB_PAGE_SIZE), ubi-io-inv(apebs), # buf1 ≤ n1, n1 ≤ LEB_SIZE, n1 ≤ # buf, datasize(buf1, # buf1) < datasize(buf, n1) ∨ checksum(buf1 + mkempbuf(n1 - # buf1), datasize(buf, n1)) ≠ checksum(buf, datasize(buf, n1)), ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ ⟪apebs[n2] := mkpeb(apebs[n2].echdr, apebs[n2].vidhdr, buf1 + mkempbuf(LEB_SIZE - # buf1), # buf1, apebs[n2].bad)⟫ ubi-io-inv(apebs), datasize(buf, n1) = 0, err0 = ESUCCESS

• Proof step 33:

  apebs[n2] = mkpeb(aehdr, avhdr, buf1, 0, false), n1 = align↑(datasize(buf, n1), EB_PAGE_SIZE), aehdr.valid?, avhdr.valid?, n2 < # apebs, ubi-io-inv(apebs), n1 ≤ LEB_SIZE, n1 ≤ # buf, ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ datasize(buf, n1) = 0, err0 = ESUCCESS, ∃ buf1. # buf1 ≤ n1 ∧ is-aligned(# buf1, EB_PAGE_SIZE) ∧ ( datasize(buf1, # buf1) < datasize(buf, n1) ∨ checksum(buf1 + mkempbuf(n1 - # buf1), datasize(buf, n1)) ≠ checksum(buf, datasize(buf, n1)))

• Proof step 35:

  apebs[n2] = mkpeb(aehdr, avhdr, buf1, 0, false), n1 = align↑(datasize(buf, n1), EB_PAGE_SIZE), aehdr.valid?, avhdr.valid?, n2 < # apebs, ubi-io-inv(apebs), n1 ≤ LEB_SIZE, n1 ≤ # buf, ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ datasize(buf, n1) = 0, err0 = ESUCCESS, ∀ buf1. # buf1 ≤ n1 → is-aligned(# buf1, EB_PAGE_SIZE) → ¬ datasize(buf1, # buf1) < datasize(buf, n1) → n1 ≥ # buf1

Rule argument

Additional information