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

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 34:

  # lpt = # avol [buffered(m4).leb, mapped ( avol[buffered(m4).leb].data + mkempbuf(m3 - # avol[buffered(m4).leb].data) + subarray (copy(buf3, 0, copy(buf1, 0, mkbuf(align↓(m2 + n3, EB_PAGE_SIZE)), 0, m2), m2, align↓(m2 + n3, EB_PAGE_SIZE) - m2), 0, align↓(m2 + n3, EB_PAGE_SIZE))) ], # buf1 = EB_PAGE_SIZE, # lpt = # avol, avol[m4] = mapped(buf2), err = ESUCCESS, err = err0, buffered(m4).isbuf?, avol[buffered(m4).leb].mapped?, buffered(m4).leb < # avol, m4 < # avol, ebm-vol-inv (avol [buffered(m4).leb, mapped ( avol[buffered(m4).leb].data + mkempbuf(m3 - # avol[buffered(m4).leb].data) + subarray (copy(buf3, 0, copy(buf1, 0, mkbuf(align↓(m2 + n3, EB_PAGE_SIZE)), 0, m2), m2, align↓(m2 + n3, EB_PAGE_SIZE) - m2), 0, align↓(m2 + n3, EB_PAGE_SIZE))) ]), ebm-vol-inv(avol), is-aligned(m3, EB_PAGE_SIZE), wbuf-cons(mkwbuf(buf1, m3, m2), mapped(buf2), false), 0 + align↓(m2 + n3, EB_PAGE_SIZE) ≤ # copy(buf3, 0, copy(buf1, 0, mkbuf(align↓(m2 + n3, EB_PAGE_SIZE)), 0, m2), m2, align↓(m2 + n3, EB_PAGE_SIZE) - m2), 0 + (align↓(m2 + n3, EB_PAGE_SIZE) - m2) ≤ # buf3, m2 + (align↓(m2 + n3, EB_PAGE_SIZE) - m2) ≤ # copy(buf1, 0, mkbuf(align↓(m2 + n3, EB_PAGE_SIZE)), 0, m2), 0 + m2 ≤ # buf1, 0 + m2 ≤ # mkbuf(align↓(m2 + n3, EB_PAGE_SIZE)), 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, # buf2 ≤ m3, m3 + align↓(m2 + n3, EB_PAGE_SIZE) ≤ LEB_SIZE, m3 ≥ # avol[buffered(m4).leb].data, align↓(m2 + n3, EB_PAGE_SIZE) ≥ m2, ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ ⟪wbuf := mkwbuf(buf1, m3, m2); rofs := false; 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 [buffered(m4).leb, mapped ( avol[buffered(m4).leb].data + mkempbuf(m3 - # avol[buffered(m4).leb].data) + subarray (copy(buf3, 0, copy(buf1, 0, mkbuf(align↓(m2 + n3, EB_PAGE_SIZE)), 0, m2), m2, align↓(m2 + n3, EB_PAGE_SIZE) - m2), 0, align↓(m2 + n3, EB_PAGE_SIZE))) ] ∧ wbuf-cons (wbuf, avol [buffered(m4).leb, mapped ( avol[buffered(m4).leb].data + mkempbuf(m3 - # avol[buffered(m4).leb].data) + subarray (copy(buf3, 0, copy(buf1, 0, mkbuf(align↓(m2 + n3, EB_PAGE_SIZE)), 0, m2), m2, align↓(m2 + n3, EB_PAGE_SIZE) - m2), 0, align↓(m2 + n3, EB_PAGE_SIZE))) ] [m4 ], rofs))

Rule argument

Additional information