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

# 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, rofs ↔ false, avol[m4] = mapped(buf2), err = ESUCCESS, err = err0, wbuf = mkwbuf(buf1, m3, m2), 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), (align↓(m2 + n3, EB_PAGE_SIZE) - m2) + (m2 + n3) % EB_PAGE_SIZE ≤ # buf3, 0 + (m2 + n3) % EB_PAGE_SIZE ≤ # wbuf.content, 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 ⊦ EB_PAGE_SIZE = 0, # ( ( (wbuf.content:= copy(buf3, align↓(m2 + n3, EB_PAGE_SIZE) - m2, wbuf.content, 0, (m2 + n3) % EB_PAGE_SIZE)) .offset:= ( (wbuf.content:= copy(buf3, align↓(m2 + n3, EB_PAGE_SIZE) - m2, wbuf.content, 0, (m2 + n3) % EB_PAGE_SIZE)).offset + align↓(m2 + n3, EB_PAGE_SIZE))) .nbytes:= ((m2 + n3) % EB_PAGE_SIZE) ).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.content:= copy(buf3, align↓(m2 + n3, EB_PAGE_SIZE) - m2, wbuf.content, 0, (m2 + n3) % EB_PAGE_SIZE)) .offset:= ( (wbuf.content:= copy(buf3, align↓(m2 + n3, EB_PAGE_SIZE) - m2, wbuf.content, 0, (m2 + n3) % EB_PAGE_SIZE)).offset + align↓(m2 + n3, EB_PAGE_SIZE))) .nbytes:= ((m2 + n3) % EB_PAGE_SIZE), 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)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 41:
# lpt = # avol, # buf1 = EB_PAGE_SIZE, avol[m4] = mapped(buf2), m4 < # avol, ebm-vol-inv(avol), ebm-vol-inv (avol [m4, mapped ( buf2 + mkempbuf(m3 - # buf2) + copy(buf3, 0, copy(buf1, 0, mkbuf(align↓(m2 + n3, EB_PAGE_SIZE)), 0, m2), m2, align↓(m2 + n3, EB_PAGE_SIZE) - m2)) ]), is-aligned(m3, EB_PAGE_SIZE), wbuf-cons(mkwbuf(buf1, m3, m2), mapped(buf2), false), m3 + align↓(m2 + n3, EB_PAGE_SIZE) ≤ LEB_SIZE, # buf2 ≤ m3, m3 + m2 + n3 ≤ LEB_SIZE, EB_PAGE_SIZE ≤ m2 + n3, m2 ≤ EB_PAGE_SIZE, align↓(m2 + n3, EB_PAGE_SIZE) ≤ # buf3 + m2, n3 ≤ # buf3, m2 ≤ align↓(m2 + n3, EB_PAGE_SIZE) ⊦ wbuf-cons (mkwbuf (copy(buf3, align↓(m2 + n3, EB_PAGE_SIZE) - m2, buf1, 0, (m2 + n3) % EB_PAGE_SIZE), m3 + align↓(m2 + n3, EB_PAGE_SIZE), (m2 + n3) % EB_PAGE_SIZE), mapped ( buf2 + mkempbuf(m3 - # buf2) + copy(buf3, 0, copy(buf1, 0, mkbuf(align↓(m2 + n3, EB_PAGE_SIZE)), 0, m2), m2, align↓(m2 + n3, EB_PAGE_SIZE) - m2)), false)

Rule argument

Additional information

Used simplifier rules: n ≠ 0 ⊦ m % n ≤ n; (s)% ⊦ mapped(buf).data = buf; (s)%n ≠ 0 ⊦ m % n ≤ m; (s)% ⊦ mapped(buf) = mapped(buf0) ↔ buf = buf0; (s)%let: ⊦ n ≤ n0 ∧ n0 ≤ n1 → n ≤ n1; (forward) from specification nat% ⊦ m < # avol → avol[m, aleb][m] = aleb; (s)% ⊦ mkwbuf(buf, m, m0).nbytes:= m2 = mkwbuf(buf, m, m2); (s)% ⊦ mkwbuf(buf, m, m0).offset:= m1 = mkwbuf(buf, m1, m0); (s)% ⊦ mkwbuf(buf, m, m0).offset = m; (s)% ⊦ mkwbuf(buf, m, m0).content:= buf0 = mkwbuf(buf0, m, m0); (s)% ⊦ ¬ ⌊ESUCCESS⌋ ; (s)% ⊦ buffered(m).isbuf?; (s)% ⊦ aleb.mapped? ↔ (∃ buf. aleb = mapped(buf)); (as)%n ≠ 0 ⊦ align↓(m, n) + m % n = m; (s)% ⊦ mkwbuf(buf, m, m0).content = buf; (s)%n0 ≤ n ⊦ n - n0 ≤ m ↔ n ≤ m + n0; (s)% ⊦ m ≤ m; (s)% ⊦ m + n ≤ m + n0 ↔ n ≤ n0; (s)%n ≤ m ⊦ (m - n) + m0 ≤ n0 ↔ m + m0 ≤ n0 + n; (s)% ⊦ m ≤ n → (n < m ↔ false); (s)% ⊦ m ≤ n ↔ ¬ n < m; (ss)%c: ⊦ m + n = n + m; from specification nat-basic%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic% ⊦ n + 0 = n; (s)% ⊦ n ≥ m ↔ m ≤ n; (s)% ⊦ EB_PAGE_SIZE ≠ 0; (s)% ⊦ # avol[n, aleb] = # avol; (s)%append-a: ⊦ (buf + buf0) + buf1 = buf + buf0 + buf1; from specification array-splice[buffer]%# buf = n ⊦ subarray(buf, 0, n) = buf; (s)% ⊦ # mkbuf(n) = n; (s)% ⊦ # copy(buf, m, buf0, m0, n) = # buf0; (s)% ⊦ buffered(m).leb = m; (s)