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

# 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) ⊦ ⟪lpt1[buffered(n1).leb] := mklp(lpt1[buffered(n1).leb].ref-size, LEB_SIZE, lpt1[buffered(n1).leb].flags, lpt1[buffered(n1).leb].gcheapidx); 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) ∧ freelist-cons(lpt1, freelist) ∧ bin-heap-inv(gch, lpt1) ∧ keyset(gch) = gc-heap(lpt1, log0) ∧ bufs-log-only(buffered(n1), log0, lpt1) ∧ # lpt1 = # avol0 ∧ log-group-block(log0, lpt1) ∧ buf-ro-rw-mode(isbuf1, buffered(n1), lpt1, avol0[n1, mapped(avol0[n1].data + subarray(buf1, 0, n))]) ∧ lpt-leb-size(lpt1) ∧ lpt-ram-flash(lpt1, lpt0, log0))

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

Proof step 83:
# 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)

Rule argument

Additional information

Used simplifier rules: ⊦ buffered(m).leb = m; (s)% ⊦ buffered(m).isbuf?; (s)% ⊦ m < n ↔ ¬ n ≤ m; (ss)%fle-01: ⊦ m ≤ n ∧ n < n0 → m < n0; (forward) from specification nat%fle: ⊦ m < n ∧ n ≤ n0 → m < n0; (forward) from specification nat% ⊦ ¬ n < n; (s)