[Imprint][Data Privacy Statement][E-Mail]

View long theorem info. View the proof. Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Proof step 64 from proof refine-write-buf (previous step)

# buf1 = EB_PAGE_SIZE, # lpt0 = # avol1, # avol0 = # avol1, avol1[m4] = mapped(buf), avol0[m4] = mapped(buf2), align↓(m2 + n3, EB_PAGE_SIZE) = n + m2, m4 < # avol1, m2 < EB_PAGE_SIZE, abs(avol1, buffered(m4), mkwbuf(buf1, # buf2, m2), avol0, false), awbuf-inv(avol1, buffered(m4)), ebm-vol-inv(avol0), is-aligned(# buf2, EB_PAGE_SIZE), is-aligned(n + m2, EB_PAGE_SIZE), n + (m2 + n3) % EB_PAGE_SIZE ≤ # buf3, # buf2 + n + m2 ≤ LEB_SIZE, n ≤ # buf3, # buf2 + m2 + n3 ≤ LEB_SIZE, EB_PAGE_SIZE ≤ m2 + n3, n3 ≤ # buf3, # buf + n3 ≤ LEB_SIZE ⊦ n + m2 = 0, n3 = 0, abs (avol1[m4, mapped(buf + subarray(buf3, 0, n3))], buffered(m4), mkwbuf(copy(buf3, n, buf1, 0, (m2 + n3) % EB_PAGE_SIZE), # buf2 + n + m2, (m2 + n3) % EB_PAGE_SIZE), avol0[m4, mapped(buf2 + copy(buf3, 0, copy(buf1, 0, mkbuf(n + m2), 0, m2), m2, n))], false)

User applied rule insert rewrite lemma

And obtained the following new goals

Proof step 65:
⊦ abs(avol0, bleb, wbuf, avol1, rofs) ↔ # avol0 = # avol1 ∧ (∀ n. n < # avol0 → (buffered(n) ≠ bleb → avol0[n] = avol1[n]) ∧ (¬ rofs ∧ buffered(n) = bleb → avol0[n] = abs⊕(avol1[n], wbuf)) ∧ ( rofs ∧ buffered(n) = bleb → wbuf.offset = # avol1[n].data ∧ avol0[n] = abs⊕(avol1[n], wbuf) ∨ wbuf.offset < # avol1[n].data ∧ wbuf.offset + wbuf.nbytes < # avol1[n].data ∧ avol0[n] = avol1[n] ∧ subarray(wbuf.content, 0, wbuf.nbytes) = subarray(avol1[n].data, wbuf.offset, wbuf.nbytes)))
Proof step 66:
# avol0 = # avol1, # lpt0 = # avol1, # buf1 = EB_PAGE_SIZE, avol0[m4] = mapped(buf2), avol1[m4] = mapped(buf), align↓(m2 + n3, EB_PAGE_SIZE) = n + m2, m2 < EB_PAGE_SIZE, m4 < # avol1, abs(avol1, buffered(m4), mkwbuf(buf1, # buf2, m2), avol0, false), awbuf-inv(avol1, buffered(m4)), ebm-vol-inv(avol0), is-aligned(n + m2, EB_PAGE_SIZE), is-aligned(# buf2, EB_PAGE_SIZE), # buf + n3 ≤ LEB_SIZE, n3 ≤ # buf3, EB_PAGE_SIZE ≤ m2 + n3, # buf2 + m2 + n3 ≤ LEB_SIZE, n ≤ # buf3, # buf2 + n + m2 ≤ LEB_SIZE, n + (m2 + n3) % EB_PAGE_SIZE ≤ # buf3 ⊦ n + m2 = 0, n3 = 0, # avol1[m4, mapped(buf + subarray(buf3, 0, n3))] = # avol0[m4, mapped(buf2 + copy(buf3, 0, copy(buf1, 0, mkbuf(n + m2), 0, m2), m2, n))] ∧ (∀ n0. n0 < # avol1[m4, mapped(buf + subarray(buf3, 0, n3))] → ( buffered(n0) ≠ buffered(m4) → avol1[m4, mapped(buf + subarray(buf3, 0, n3))][n0] = avol0[m4, mapped(buf2 + copy(buf3, 0, copy(buf1, 0, mkbuf(n + m2), 0, m2), m2, n))][n0]) ∧ ( ¬ false ∧ buffered(n0) = buffered(m4) → avol1[m4, mapped(buf + subarray(buf3, 0, n3))][n0] = abs⊕ (avol0[m4, mapped(buf2 + copy(buf3, 0, copy(buf1, 0, mkbuf(n + m2), 0, m2), m2, n))][n0], mkwbuf(copy(buf3, n, buf1, 0, (m2 + n3) % EB_PAGE_SIZE), # buf2 + n + m2, (m2 + n3) % EB_PAGE_SIZE))) ∧ ( false ∧ buffered(n0) = buffered(m4) → mkwbuf(copy(buf3, n, buf1, 0, (m2 + n3) % EB_PAGE_SIZE), # buf2 + n + m2, (m2 + n3) % EB_PAGE_SIZE).offset = # avol0[m4, mapped(buf2 + copy(buf3, 0, copy(buf1, 0, mkbuf(n + m2), 0, m2), m2, n))][n0].data ∧ avol1[m4, mapped(buf + subarray(buf3, 0, n3))][n0] = abs⊕ (avol0[m4, mapped(buf2 + copy(buf3, 0, copy(buf1, 0, mkbuf(n + m2), 0, m2), m2, n))][n0], mkwbuf(copy(buf3, n, buf1, 0, (m2 + n3) % EB_PAGE_SIZE), # buf2 + n + m2, (m2 + n3) % EB_PAGE_SIZE)) ∨ mkwbuf(copy(buf3, n, buf1, 0, (m2 + n3) % EB_PAGE_SIZE), # buf2 + n + m2, (m2 + n3) % EB_PAGE_SIZE).offset < # avol0[m4, mapped(buf2 + copy(buf3, 0, copy(buf1, 0, mkbuf(n + m2), 0, m2), m2, n))][n0].data ∧ mkwbuf(copy(buf3, n, buf1, 0, (m2 + n3) % EB_PAGE_SIZE), # buf2 + n + m2, (m2 + n3) % EB_PAGE_SIZE).offset + mkwbuf(copy(buf3, n, buf1, 0, (m2 + n3) % EB_PAGE_SIZE), # buf2 + n + m2, (m2 + n3) % EB_PAGE_SIZE).nbytes < # avol0[m4, mapped(buf2 + copy(buf3, 0, copy(buf1, 0, mkbuf(n + m2), 0, m2), m2, n))][n0].data ∧ avol1[m4, mapped(buf + subarray(buf3, 0, n3))][n0] = avol0[m4, mapped(buf2 + copy(buf3, 0, copy(buf1, 0, mkbuf(n + m2), 0, m2), m2, n))][n0] ∧ subarray (mkwbuf(copy(buf3, n, buf1, 0, (m2 + n3) % EB_PAGE_SIZE), # buf2 + n + m2, (m2 + n3) % EB_PAGE_SIZE).content, 0, mkwbuf(copy(buf3, n, buf1, 0, (m2 + n3) % EB_PAGE_SIZE), # buf2 + n + m2, (m2 + n3) % EB_PAGE_SIZE).nbytes) = subarray (avol0[m4, mapped(buf2 + copy(buf3, 0, copy(buf1, 0, mkbuf(n + m2), 0, m2), m2, n))][n0].data, mkwbuf(copy(buf3, n, buf1, 0, (m2 + n3) % EB_PAGE_SIZE), # buf2 + n + m2, (m2 + n3) % EB_PAGE_SIZE).offset, mkwbuf(copy(buf3, n, buf1, 0, (m2 + n3) % EB_PAGE_SIZE), # buf2 + n + m2, (m2 + n3) % EB_PAGE_SIZE).nbytes)))

Rule argument

spec: wbuf-abs name: abs-def seq: ⊦ abs(avol0, bleb, wbuf, avol1, rofs) ↔ # avol0 = # avol1 ∧ (∀ n. n < # avol0 → (buffered(n) ≠ bleb → avol0[n] = avol1[n]) ∧ ( ¬ rofs ∧ buffered(n) = bleb → avol0[n] = abs⊕(avol1[n], wbuf)) ∧ ( rofs ∧ buffered(n) = bleb → wbuf.offset = # avol1[n].data ∧ avol0[n] = abs⊕(avol1[n], wbuf) ∨ wbuf.offset < # avol1[n].data ∧ wbuf.offset + wbuf.nbytes < # avol1[n].data ∧ avol0[n] = avol1[n] ∧ subarray(wbuf.content, 0, wbuf.nbytes) = subarray (avol1[n].data, wbuf.offset, wbuf.nbytes))) subst: [rofs, avol1, wbuf, bleb, avol0] → [false, avol0 [m4, mapped ( buf2 + copy (buf3, 0, copy(buf1, 0, mkbuf(n + m2), 0, m2), m2, n)) ], mkwbuf (copy(buf3, n, buf1, 0, (m2 + n3) % EB_PAGE_SIZE), # buf2 + n + m2, (m2 + n3) % EB_PAGE_SIZE), buffered(m4), avol1[m4, mapped(buf + subarray(buf3, 0, n3))]] flags: <all paths>

Additional information

Used terms: false, avol0 [m4, mapped (buf2 + copy(buf3, 0, copy(buf1, 0, mkbuf(n + m2), 0, m2), m2, n)) ], mkwbuf (copy(buf3, n, buf1, 0, (m2 + n3) % EB_PAGE_SIZE), # buf2 + n + m2, (m2 + n3) % EB_PAGE_SIZE), buffered(m4), avol1[m4, mapped(buf + subarray(buf3, 0, n3))]