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

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 86:

  apebs[m1] = mkpeb(aehdr, avhdr, buf2, 0, false), pebs[m1] = mkpeb(buf1, 2 * EB_PAGE_SIZE, false), err = err1, n = align↑(datasize(buf, n), EB_PAGE_SIZE), avhdr.valid?, aehdr.valid?, m1 < # apebs, m1 < # pebs, n2 < n, n2 < LEB_SIZE, n2 < # buf, n2 < datasize(buf, n), abs(pebs, apebs), abs-peb(mkpeb(buf1, 2 * EB_PAGE_SIZE, false), mkpeb(aehdr, avhdr, buf2, 0, false)), is-aligned(n2, EB_PAGE_SIZE), is-aligned(n, EB_PAGE_SIZE), mtd-cons(pebs), ubi-io-inv(apebs), 2 * EB_PAGE_SIZE + n2 ≤ PEB_SIZE, n ≤ LEB_SIZE, n ≤ # buf, ⌊err1⌋ ⊦ ⟨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, n2)).fill:= (2 * EB_PAGE_SIZE + n2)], apebs) ∧ err1 = err), n2 = 0

Rule argument

Additional information