[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 66 from proof refine-write-buf (previous step)

# 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)))

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 67:
# avol0 = # avol1, # lpt0 = # avol1, # buf1 = EB_PAGE_SIZE, avol0[m4] = mapped(buf2), avol1[m4] = mapped(buf), align↓(m2 + n3, EB_PAGE_SIZE) = n + m2, n0 < # avol1, 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, (n0 ≠ m4 → avol1[n0] = avol0[n0]) ∧ ( n0 = m4 → buf + subarray(buf3, 0, n3) = (buf2 + copy(buf3, 0, copy(buf1, 0, mkbuf(n + m2), 0, m2), m2, n)) + subarray(buf3, n, (m2 + n3) % EB_PAGE_SIZE))

Rule argument

Additional information

Used simplifier rules: lf-01: ⊦ m < n ∧ n = n0 → m < n0; (forward) from specification nat-basic% ⊦ mapped(buf) = mapped(buf0) ↔ buf = buf0; (s)%m1 + n ≤ # buf ⊦ subarray(copy(buf0, m0, buf, m1, n), m1, n) = subarray(buf0, m0, n); (s)%n ≠ 0 ⊦ m % n ≤ n; (s)% ⊦ EB_PAGE_SIZE ≠ 0; (s)%c: ⊦ m + n = n + m; from specification nat-basic%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic% ⊦ n + 0 = n; (s)% ⊦ mkwbuf(buf, m, m0).nbytes = m0; (s)% ⊦ mkwbuf(buf, m, m0).content = buf; (s)%⊦ abs⊕(mapped(buf), wbuf) = mapped(buf + subarray(wbuf.content, 0, wbuf.nbytes)); (s)%m < # avol ⊦ avol[m, aleb][m] = aleb; (s)% ⊦ m < n → (n ≤ m ↔ false); (s)% ⊦ m < n ↔ ¬ n ≤ m; (ss)% ⊦ m < # avol → avol[m, aleb][m] = aleb; (s)% ⊦ m ≠ n → avol[n, aleb][m] = avol[m]; (s)% ⊦ buffered(m) = buffered(m0) ↔ m = m0; (s)% ⊦ abs(avol0, bleb, wbuf, avol1, rofs) → (# avol1 = # avol0 ↔ true); (ss)% ⊦ # avol[n, aleb] = # avol; (s)