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

Heuristic symbolic execution applied rule if right

And obtained the following new goals

• Proof step 27:

  # lpt = # avol, # buf1 = EB_PAGE_SIZE, avol[m4] = mapped(buf2), buf = copy(buf3, 0, copy(buf1, 0, mkbuf(align↓(m2 + n3, EB_PAGE_SIZE)), 0, m2), m2, align↓(m2 + n3, EB_PAGE_SIZE) - m2), m0 = m3, m1 = buffered(m4).leb, n0 = align↓(m2 + n3, EB_PAGE_SIZE), n1 = 0, buffered(m4).isbuf?, avol[m1].mapped?, m1 < # avol, m4 < # avol, ebm-vol-inv(avol), is-aligned(m0, EB_PAGE_SIZE), is-aligned(n0, EB_PAGE_SIZE), is-aligned(m3, EB_PAGE_SIZE), wbuf-cons(mkwbuf(buf1, m3, m2), mapped(buf2), false), # avol[m1].data ≤ m0, m0 + n0 ≤ LEB_SIZE, n1 + n0 ≤ # buf, # buf2 ≤ m3, n3 ≤ # buf3, m3 + m2 + n3 ≤ LEB_SIZE, align↓(m2 + n3, EB_PAGE_SIZE) ≤ # buf3 + m2, m2 ≤ EB_PAGE_SIZE, m2 ≤ align↓(m2 + n3, EB_PAGE_SIZE), EB_PAGE_SIZE ≤ m2 + n3, m3 + align↓(m2 + n3, EB_PAGE_SIZE) ≤ LEB_SIZE, 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, align↓(m2 + n3, EB_PAGE_SIZE) ≥ m2, m1 < # avol → m1 < # avol ∧ (avol[m1].mapped? → avol[m1].mapped? ∧ m1 < # avol) ⊦ [fail_or_success#(; ; err); if err = ESUCCESS then if n0 ≠ 0 then avol[m1] := mapped(avol[m1].data + mkempbuf(m0 - # avol[m1].data) + subarray(buf, n1, n0)) else choose n with n < n0 ∧ is-aligned(n, EB_PAGE_SIZE) in if n ≠ 0 then avol[m1] := mapped(avol[m1].data + mkempbuf(m0 - # avol[m1].data) + subarray(buf, n1, n)) ifnone skip] ( ebm-vol-inv(avol) ∧ # lpt = # avol → ⟪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 ∧ wbuf-cons(wbuf, avol[m4], rofs)))

• Proof step 86:

  # lpt = # avol, # buf1 = EB_PAGE_SIZE, avol[m4] = mapped(buf2), buf = copy(buf3, 0, copy(buf1, 0, mkbuf(align↓(m2 + n3, EB_PAGE_SIZE)), 0, m2), m2, align↓(m2 + n3, EB_PAGE_SIZE) - m2), m0 = m3, m1 = buffered(m4).leb, n0 = align↓(m2 + n3, EB_PAGE_SIZE), n1 = 0, buffered(m4).isbuf?, m4 < # avol, ebm-vol-inv(avol), is-aligned(m3, EB_PAGE_SIZE), wbuf-cons(mkwbuf(buf1, m3, m2), mapped(buf2), false), # buf2 ≤ m3, n3 ≤ # buf3, m3 + m2 + n3 ≤ LEB_SIZE, align↓(m2 + n3, EB_PAGE_SIZE) ≤ # buf3 + m2, m2 ≤ EB_PAGE_SIZE, m2 ≤ align↓(m2 + n3, EB_PAGE_SIZE), EB_PAGE_SIZE ≤ m2 + n3, m3 + align↓(m2 + n3, EB_PAGE_SIZE) ≤ LEB_SIZE, 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, align↓(m2 + n3, EB_PAGE_SIZE) ≥ m2, m1 < # avol → m1 < # avol ∧ (avol[m1].mapped? → avol[m1].mapped? ∧ m1 < # avol) ⊦ [abort] ( ebm-vol-inv(avol) ∧ # lpt = # avol → ⟪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 ∧ wbuf-cons(wbuf, avol[m4], rofs))), m1 < # avol ∧ avol[m1].mapped? ∧ # avol[m1].data ≤ m0 ∧ is-aligned(m0, EB_PAGE_SIZE) ∧ is-aligned(n0, EB_PAGE_SIZE) ∧ m0 + n0 ≤ LEB_SIZE ∧ n1 + n0 ≤ # buf

Rule argument

Additional information