Proof step 28 from proof refine-write-data-wl (previous step)

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 29:

  pebs[m1] = mkpeb(buf1, 2 * EB_PAGE_SIZE, false), apebs[m1] = mkpeb(aehdr, avhdr, buf2, 0, false), err = ESUCCESS, n = align↑(datasize(buf, n), EB_PAGE_SIZE), avhdr.valid?, aehdr.valid?, m1 < # pebs, m1 < # apebs, abs(pebs, apebs), abs-peb(mkpeb(buf1, 2 * EB_PAGE_SIZE, false), mkpeb(aehdr, avhdr, buf2, 0, false)), is-aligned(n, EB_PAGE_SIZE), mtd-cons(pebs), ubi-io-inv(apebs), n ≤ # buf, n ≤ LEB_SIZE, 2 * EB_PAGE_SIZE + n ≤ PEB_SIZE ⊦ ⟨if err = ESUCCESS then apebs[m1] := mkpeb(apebs[m1].echdr, apebs[m1].vidhdr, subarray(buf, 0, n) + mkempbuf(LEB_SIZE - n), n, apebs[m1].bad) else {m := m1; buf0 := buf; choose buf1 with # buf1 ≤ n ∧ is-aligned(# buf1, EB_PAGE_SIZE) ∧ ( datasize(buf1, # buf1) < datasize(buf0, n) ∨ checksum(buf1 + mkempbuf(n - # buf1), datasize(buf0, n)) ≠ checksum(buf0, datasize(buf0, n))) in apebs[m] := mkpeb(apebs[m].echdr, apebs[m].vidhdr, buf1 + mkempbuf(LEB_SIZE - # buf1), # buf1, apebs[m].bad)}⟩ (abs(pebs[m1, (pebs[m1].data:= copy(buf, 0, pebs[m1].data, 2 * EB_PAGE_SIZE, n)).fill:= (2 * EB_PAGE_SIZE + n)], apebs) ∧ ESUCCESS = err), datasize(buf, n) = 0

Rule argument

Additional information