[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 54 from proof inv-sync (previous step)

# lpt0 = # avol, # lpt1 = # avol0, # lpt0 = # avol0, isbuf1 ↔ isbuf, isbuf ↔ false, EB_PAGE_SIZE = # buf1 + # buf0 % EB_PAGE_SIZE, lpt1[n] = mklp(m3, # buf0, lpf, m4), avol0[n] = mapped(buf0), avol = avol0[m, mapped(avol0[m].data + subarray(buf1, 0, # buf1))], bleb1 = buffered(n), err = err0, err = ESUCCESS, keyset(gch) = gc-heap(lpt1, log0), m = buffered(n).leb, m0 = EB_PAGE_SIZE - lpt1[buffered(n).leb].size % EB_PAGE_SIZE, buffered(n).isbuf?, avol0[m].mapped?, buffered(n).leb < # lpt1, n < # avol0, m < # avol0, abs-padding(buf1), awbuf-inv(avol, buffered(n)), awbuf-inv(avol0, buffered(n)), bin-heap-inv(gch, lpt1), buf-ro-rw-mode(false, buffered(n), lpt1, avol0), bufs-log-only(buffered(n), log0, lpt1), freelist-cons(lpt1, freelist), is-aligned(# buf0, 2 * NODE_HEADER_SIZE), log-group-block(log0, lpt1), lpt-free-unref(lpt0), lpt-free-unref(lpt1), lpt-leb-size(lpt0), lpt-leb-size(lpt1), lpt-ram-flash(lpt1, lpt0, log0), # buf0 ≤ LEB_SIZE, # buf0 + # buf1 ≤ LEB_SIZE, 0 + # buf1 ≤ # buf1, EB_PAGE_SIZE ≥ lpt1[buffered(n).leb].size % EB_PAGE_SIZE, ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ ⟪lpt1[bleb1.leb] := mklp(lpt1[bleb1.leb].ref-size, lpt1[bleb1.leb].size + m0, lpt1[bleb1.leb].flags, lpt1[bleb1.leb].gcheapidx)⟫ ( lpt-free-unref(lpt1) ∧ freelist-cons(lpt1, freelist) ∧ bin-heap-inv(gch, lpt1) ∧ keyset(gch) = gc-heap(lpt1, log0) ∧ bufs-log-only(bleb1, log0, lpt1) ∧ # lpt1 = # avol ∧ log-group-block(log0, lpt1) ∧ buf-ro-rw-mode(isbuf1, bleb1, lpt1, avol) ∧ lpt-leb-size(lpt1) ∧ lpt-ram-flash(lpt1, lpt0, log0) ∧ awbuf-inv(avol, bleb1)), EB_PAGE_SIZE = 0, buf1 = mkbuf(0), lpf = LP_FREE, is-aligned(# buf0, EB_PAGE_SIZE)

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

Proof step 55:
# lpt0 = # avol0, # lpt1 = # avol0, # lpt0 = # avol, isbuf ↔ false, isbuf1 ↔ isbuf, EB_PAGE_SIZE = # buf1 + # buf0 % EB_PAGE_SIZE, avol0[n] = mapped(buf0), lpt1[n] = mklp(m3, # buf0, lpf, m4), avol = avol0[m, mapped(avol0[m].data + subarray(buf1, 0, # buf1))], bleb1 = buffered(n), err = ESUCCESS, err = err0, keyset(gch) = gc-heap(lpt1, log0), m = buffered(n).leb, m0 = EB_PAGE_SIZE - lpt1[buffered(n).leb].size % EB_PAGE_SIZE, bleb1.isbuf?, buffered(n).isbuf?, avol0[m].mapped?, bleb1.leb < # lpt1, m < # avol0, n < # avol0, buffered(n).leb < # lpt1, abs-padding(buf1), awbuf-inv(avol0, buffered(n)), awbuf-inv(avol, buffered(n)), bin-heap-inv(gch, lpt1), buf-ro-rw-mode(false, buffered(n), lpt1, avol0), bufs-log-only(buffered(n), log0, lpt1), freelist-cons(lpt1, freelist), is-aligned(# buf0, 2 * NODE_HEADER_SIZE), log-group-block(log0, lpt1), lpt-free-unref(lpt1), lpt-free-unref(lpt0), lpt-leb-size(lpt1), lpt-leb-size(lpt0), lpt-ram-flash(lpt1, lpt0, log0), 0 + # buf1 ≤ # buf1, # buf0 + # buf1 ≤ LEB_SIZE, # buf0 ≤ LEB_SIZE, EB_PAGE_SIZE ≥ lpt1[buffered(n).leb].size % EB_PAGE_SIZE, ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ EB_PAGE_SIZE = 0, buf1 = mkbuf(0), lpf = LP_FREE, is-aligned(# buf0, EB_PAGE_SIZE), lpt-free-unref(lpt1[bleb1.leb, mklp(lpt1[bleb1.leb].ref-size, lpt1[bleb1.leb].size + m0, lpt1[bleb1.leb].flags, lpt1[bleb1.leb].gcheapidx)]) ∧ freelist-cons (lpt1[bleb1.leb, mklp(lpt1[bleb1.leb].ref-size, lpt1[bleb1.leb].size + m0, lpt1[bleb1.leb].flags, lpt1[bleb1.leb].gcheapidx)], freelist) ∧ bin-heap-inv(gch, lpt1[bleb1.leb, mklp(lpt1[bleb1.leb].ref-size, lpt1[bleb1.leb].size + m0, lpt1[bleb1.leb].flags, lpt1[bleb1.leb].gcheapidx)]) ∧ keyset(gch) = gc-heap(lpt1[bleb1.leb, mklp(lpt1[bleb1.leb].ref-size, lpt1[bleb1.leb].size + m0, lpt1[bleb1.leb].flags, lpt1[bleb1.leb].gcheapidx)], log0) ∧ bufs-log-only (bleb1, log0, lpt1[bleb1.leb, mklp(lpt1[bleb1.leb].ref-size, lpt1[bleb1.leb].size + m0, lpt1[bleb1.leb].flags, lpt1[bleb1.leb].gcheapidx)]) ∧ # lpt1[bleb1.leb, mklp(lpt1[bleb1.leb].ref-size, lpt1[bleb1.leb].size + m0, lpt1[bleb1.leb].flags, lpt1[bleb1.leb].gcheapidx)] = # avol ∧ log-group-block (log0, lpt1[bleb1.leb, mklp(lpt1[bleb1.leb].ref-size, lpt1[bleb1.leb].size + m0, lpt1[bleb1.leb].flags, lpt1[bleb1.leb].gcheapidx)]) ∧ buf-ro-rw-mode (isbuf1, bleb1, lpt1[bleb1.leb, mklp(lpt1[bleb1.leb].ref-size, lpt1[bleb1.leb].size + m0, lpt1[bleb1.leb].flags, lpt1[bleb1.leb].gcheapidx)], avol) ∧ lpt-leb-size(lpt1[bleb1.leb, mklp(lpt1[bleb1.leb].ref-size, lpt1[bleb1.leb].size + m0, lpt1[bleb1.leb].flags, lpt1[bleb1.leb].gcheapidx)]) ∧ lpt-ram-flash (lpt1[bleb1.leb, mklp(lpt1[bleb1.leb].ref-size, lpt1[bleb1.leb].size + m0, lpt1[bleb1.leb].flags, lpt1[bleb1.leb].gcheapidx)], lpt0, log0) ∧ awbuf-inv(avol, bleb1)

Rule argument

Additional information

Used simplifier rules: elim-mapped: ⊦ avol[n].mapped? ↔ (∃ buf. avol[n] = mapped(buf));% ⊦ buffered(m).leb = m; (s)%# buf = n ⊦ subarray(buf, 0, n) = buf; (s)% ⊦ # avol[n, aleb] = # avol; (s)% ⊦ EB_PAGE_SIZE ≠ 0; (s)% ⊦ n ≥ m ↔ m ≤ n; (s)%n ≠ 0 ⊦ m % n ≤ n; (s)% ⊦ n + 0 = n; (s)%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic%c: ⊦ m + n = n + m; from specification nat-basic% ⊦ m ≤ m; (s)% ⊦ buffered(m).isbuf?; (s)% ⊦ ¬ ⌊ESUCCESS⌋ ; (s)