Proof step 54 from proof inv-write-buf (previous step)

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 55:

  # lpt = # avol[m1, mapped(avol[m1].data + mkempbuf(m0 - # avol[m1].data) + subarray(buf2, n1, n))], # buf1 = EB_PAGE_SIZE, # lpt = # avol, rofs ↔ false, avol[m4] = mapped(buf), buf2 = copy(buf3, 0, copy(buf1, 0, mkbuf(align↓(m2 + n3, EB_PAGE_SIZE)), 0, m2), m2, align↓(m2 + n3, EB_PAGE_SIZE) - m2), err = err0, m0 = m3, m1 = buffered(m4).leb, n0 = align↓(m2 + n3, EB_PAGE_SIZE), n1 = 0, wbuf = mkwbuf(buf1, m3, m2), buffered(m4).isbuf?, avol[m1].mapped?, m1 < # avol, n < n0, m4 < # avol, ebm-vol-inv(avol[m1, mapped(avol[m1].data + mkempbuf(m0 - # avol[m1].data) + subarray(buf2, n1, n))]), ebm-vol-inv(avol), is-aligned(n, EB_PAGE_SIZE), is-aligned(m3, EB_PAGE_SIZE), wbuf-cons(mkwbuf(buf1, m3, m2), mapped(buf), false), n1 + n ≤ # buf2, 0 + m2 ≤ # mkbuf(align↓(m2 + n3, EB_PAGE_SIZE)), 0 + m2 ≤ # buf1, m2 + (align↓(m2 + n3, EB_PAGE_SIZE) - m2) ≤ # copy(buf1, 0, mkbuf(align↓(m2 + n3, EB_PAGE_SIZE)), 0, m2), 0 + (align↓(m2 + n3, EB_PAGE_SIZE) - m2) ≤ # buf3, EB_PAGE_SIZE ≤ m2 + n3, m2 ≤ align↓(m2 + n3, EB_PAGE_SIZE), m2 ≤ EB_PAGE_SIZE, align↓(m2 + n3, EB_PAGE_SIZE) ≤ # buf3 + m2, m3 + m2 + n3 ≤ LEB_SIZE, n3 ≤ # buf3, # buf ≤ m3, m3 + align↓(m2 + n3, EB_PAGE_SIZE) ≤ LEB_SIZE, m0 ≥ # avol[m1].data, align↓(m2 + n3, EB_PAGE_SIZE) ≥ m2, ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ ⟪if err = ESUCCESS then {wbuf.content := copy(buf3, align↓(m2 + n3, EB_PAGE_SIZE) - m2, wbuf.content, 0, (m2 + n3) % EB_PAGE_SIZE); wbuf.offset := wbuf.offset + align↓(m2 + n3, EB_PAGE_SIZE); wbuf.nbytes := (m2 + n3) % EB_PAGE_SIZE} else rofs := true⟫ ( # wbuf.content = EB_PAGE_SIZE ∧ m4 < # avol[m1, mapped(avol[m1].data + mkempbuf(m0 - # avol[m1].data) + subarray(buf2, n1, n))] ∧ wbuf-cons(wbuf, avol[m1, mapped(avol[m1].data + mkempbuf(m0 - # avol[m1].data) + subarray(buf2, n1, n))][m4], rofs)), err = ESUCCESS, n = 0

Rule argument

Additional information