[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 38 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 ⊦ ⟪wbuf := (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)); wbuf.nbytes := (m2 + n3) % EB_PAGE_SIZE⟫ ( # 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)), EB_PAGE_SIZE = 0

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

Proof step 39:
# lpt = # avol, # buf1 = EB_PAGE_SIZE, # 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))) ], rofs ↔ false, avol[m4] = mapped(buf2), err = err0, err = ESUCCESS, wbuf = mkwbuf(buf1, m3, m2), buffered(m4).isbuf?, avol[buffered(m4).leb].mapped?, m4 < # avol, buffered(m4).leb < # avol, ebm-vol-inv(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))) ]), 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, 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, 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, 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 + (m2 + n3) % EB_PAGE_SIZE ≤ # wbuf.content, (align↓(m2 + n3, EB_PAGE_SIZE) - m2) + (m2 + n3) % EB_PAGE_SIZE ≤ # buf3, align↓(m2 + n3, EB_PAGE_SIZE) ≥ m2, m3 ≥ # avol[buffered(m4).leb].data, ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ ⟪wbuf := ( (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)⟫ ( # 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)), EB_PAGE_SIZE = 0

Rule argument

Additional information

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