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

# lpt1 = # avol, # lpt0 = # avol, EB_PAGE_SIZE = # buf1 + # buf0 % EB_PAGE_SIZE, lpt1[n] = mklp(m3, # buf0, lpf, m4), avol[n] = mapped(buf0), keyset(gch) = gc-heap(lpt1, log0), buffered(n).isbuf?, buffered(n).leb < # lpt1, n < # avol, abs-padding(buf1), awbuf-inv(avol, buffered(n)), bin-heap-inv(gch, lpt1), buf-ro-rw-mode(false, buffered(n), lpt1, avol), 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, ⌊err0⌋ ⊦ ⟪awbuf_enter_readonly#(adr, m2, log0, avol, lpt0, ns, buffered(n); ; isbuf1)⟫ ( lpt-free-unref (lpt1[buffered(n).leb, mklp(lpt1[buffered(n).leb].ref-size, LEB_SIZE, lpt1[buffered(n).leb].flags, lpt1[buffered(n).leb].gcheapidx)]) ∧ freelist-cons (lpt1[buffered(n).leb, mklp(lpt1[buffered(n).leb].ref-size, LEB_SIZE, lpt1[buffered(n).leb].flags, lpt1[buffered(n).leb].gcheapidx)], freelist) ∧ bin-heap-inv (gch, lpt1[buffered(n).leb, mklp(lpt1[buffered(n).leb].ref-size, LEB_SIZE, lpt1[buffered(n).leb].flags, lpt1[buffered(n).leb].gcheapidx)]) ∧ keyset(gch) = gc-heap (lpt1[buffered(n).leb, mklp(lpt1[buffered(n).leb].ref-size, LEB_SIZE, lpt1[buffered(n).leb].flags, lpt1[buffered(n).leb].gcheapidx)], log0) ∧ bufs-log-only (buffered(n), log0, lpt1[buffered(n).leb, mklp(lpt1[buffered(n).leb].ref-size, LEB_SIZE, lpt1[buffered(n).leb].flags, lpt1[buffered(n).leb].gcheapidx)]) ∧ # lpt1[buffered(n).leb, mklp(lpt1[buffered(n).leb].ref-size, LEB_SIZE, lpt1[buffered(n).leb].flags, lpt1[buffered(n).leb].gcheapidx)] = # avol ∧ log-group-block (log0, lpt1[buffered(n).leb, mklp(lpt1[buffered(n).leb].ref-size, LEB_SIZE, lpt1[buffered(n).leb].flags, lpt1[buffered(n).leb].gcheapidx)]) ∧ buf-ro-rw-mode (isbuf1, buffered(n), lpt1[buffered(n).leb, mklp(lpt1[buffered(n).leb].ref-size, LEB_SIZE, lpt1[buffered(n).leb].flags, lpt1[buffered(n).leb].gcheapidx)], avol) ∧ lpt-leb-size (lpt1[buffered(n).leb, mklp(lpt1[buffered(n).leb].ref-size, LEB_SIZE, lpt1[buffered(n).leb].flags, lpt1[buffered(n).leb].gcheapidx)]) ∧ lpt-ram-flash (lpt1[buffered(n).leb, mklp(lpt1[buffered(n).leb].ref-size, LEB_SIZE, lpt1[buffered(n).leb].flags, lpt1[buffered(n).leb].gcheapidx)], lpt0, log0)), buf1 = mkbuf(0), lpf = LP_FREE, is-aligned(# buf0, EB_PAGE_SIZE)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 122:
# lpt0 = # avol, # lpt1 = # avol, EB_PAGE_SIZE = # buf1 + # buf0 % EB_PAGE_SIZE, avol[n] = mapped(buf0), lpt1[n] = mklp(m3, # buf0, lpf, m4), keyset(gch) = gc-heap(lpt1, log0), buf1 ≠ mkbuf(0), lpf ≠ LP_FREE, n < # avol, abs-padding(buf1), awbuf-inv(avol, buffered(n)), bin-heap-inv(gch, lpt1), buf-ro-rw-mode(false, buffered(n), lpt1, avol), 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), # buf0 + # buf1 ≤ LEB_SIZE, # buf0 ≤ LEB_SIZE, ⌊err0⌋ , ¬ is-aligned(# buf0, EB_PAGE_SIZE) ⊦ ⟪awbuf_enter_readonly#(adr, m2, log0, avol, lpt0, ns, buffered(n); ; isbuf1)⟫ ( (lpt1[n].flags = LP_FREE → lpt1[n].ref-size = 0) ∧ freelist-cons(lpt1[n, mklp(lpt1[n].ref-size, LEB_SIZE, lpt1[n].flags, lpt1[n].gcheapidx)], freelist) ∧ bin-heap-inv(gch, lpt1[n, mklp(lpt1[n].ref-size, LEB_SIZE, lpt1[n].flags, lpt1[n].gcheapidx)]) ∧ keyset(gch) = gc-heap(lpt1[n, mklp(lpt1[n].ref-size, LEB_SIZE, lpt1[n].flags, lpt1[n].gcheapidx)], log0) ∧ log-group-block(log0, lpt1[n, mklp(lpt1[n].ref-size, LEB_SIZE, lpt1[n].flags, lpt1[n].gcheapidx)]) ∧ buf-ro-rw-mode(isbuf1, buffered(n), lpt1[n, mklp(lpt1[n].ref-size, LEB_SIZE, lpt1[n].flags, lpt1[n].gcheapidx)], avol) ∧ lpt-ram-flash(lpt1[n, mklp(lpt1[n].ref-size, LEB_SIZE, lpt1[n].flags, lpt1[n].gcheapidx)], lpt0, log0))

Rule argument

Additional information

Used simplifier rules: ⊦ m ≤ m; (s)% ⊦ mklp(n2, n3, lpf, m).size = n3; (s)% ⊦ m < n → (n ≤ m ↔ false); (s)%⊦ lpt-leb-size(lpt) → (lpt-leb-size(lpt[n, lp]) ↔ # lpt ≤ n ∨ lp.size ≤ LEB_SIZE); (s)% ⊦ # lpt[n, lp] = # lpt; (s)%lpt[n].flags = lp.flags ⊦ bufs-log-only(bleb, nx, lpt) → bufs-log-only(bleb, nx, lpt[n, lp]); (s)% ⊦ mklp(n2, n3, lpf, m).gcheapidx = m; (s)% ⊦ mklp(n2, n3, lpf, m).ref-size = n2; (s)% ⊦ mklp(n2, n3, lpf, m).flags = lpf; (s)%⊦ lpt-free-unref(lpt) → ( lpt-free-unref(lpt[n, lp]) ↔ n < # lpt ∧ lp.flags = LP_FREE → lp.ref-size = 0); (s)% ⊦ buffered(m).isbuf?; (s)% ⊦ buffered(m).leb = m; (s)