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

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

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