[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 161 from proof inv-read-gblock-nodes (previous step)

# gndx3 = # lax1, # gndx0 = # lax2, # lpt0 = # avol, # lpt = # avol, n0 + # buf = gnd.alignedsize + 2 * NODE_HEADER_SIZE + n1, LEB_SIZE = n0 + # buf0 + # buf, LEB_SIZE = n1 + # buf0 + 2 * NODE_HEADER_SIZE + gnd.alignedsize, avol[m5] = mapped(buf0 + buf), align↑(m2, 2 * NODE_HEADER_SIZE) = gnd.alignedsize, m5 < # avol, abs-node(subarray(buf + mkempbuf(n0), 0, 2 * NODE_HEADER_SIZE + gnd.alignedsize), gnd), abs-nodes(buf, # buf0, gndx0, lax2, true), abs-nodes(buf0, gndx3, lax1, false), awbuf-inv(avol, bleb), buf-ro-rw-mode(isbuf, bleb, lpt0, avol), bufs-log-only(bleb, log0, lpt0), is-aligned(# buf, NODE_HEADER_SIZE), is-encoded(nodeheader(m2, false), subarray(buf, 0, NODE_HEADER_SIZE)), lpt-free-unref(lpt), lpt-leb-size(lpt), lpt-ram-flash(lpt0, lpt, log0), range=(buf, NODE_HEADER_SIZE + gnd.alignedsize, validtrailer, 0, NODE_HEADER_SIZE), # buf0 + 2 * NODE_HEADER_SIZE + gnd.alignedsize ≤ LEB_SIZE, # buf0 + # buf ≤ LEB_SIZE, # buf0 + NODE_HEADER_SIZE ≤ LEB_SIZE ⊦ buf = mkbuf(0), isempty(buf, 0, NODE_HEADER_SIZE), ∃ gndx5, lax4, buf1, buf2. buf0 + buf = buf1 + buf2 ∧ # buf1 = # buf0 + 2 * NODE_HEADER_SIZE + gnd.alignedsize ∧ abs-nodes(buf1, gndx3 + gnd ', lax1 + @(# buf0, 2 * NODE_HEADER_SIZE + gnd.alignedsize) ', false) ∧ abs-nodes(buf2, # buf1, gndx5, lax4, true)

User applied rule insert rewrite lemma

And obtained the following new goals

Proof step 162:
⊦ is-encoded(nodeheader(m, boolvar0), subarray(buf, 0, NODE_HEADER_SIZE)) ∧ 2 * NODE_HEADER_SIZE + align↑(m, 2 * NODE_HEADER_SIZE) ≤ # buf ∧ range=(buf, NODE_HEADER_SIZE + align↑(m, 2 * NODE_HEADER_SIZE), validtrailer, 0, NODE_HEADER_SIZE) → ( abs-nodes(buf, n, gndx, lax, weak) ↔ (∃ buf0, buf1. buf = buf0 + buf1 ∧ ( boolvar0 ∧ abs-padding(buf0) ∧ abs-nodes(buf1, n + # buf0, gndx, lax, weak) ∨ # buf0 = gndx.head.flashsize ∧ gndx ≠ [] ∧ lax ≠ [] ∧ lax.head = @(n, # buf0) ∧ ¬ boolvar0 ∧ abs-node(buf0, gndx.head) ∧ abs-nodes(buf1, n + # buf0, gndx.tail, lax.tail, weak))))
Proof step 163:
# lpt = # avol, # lpt0 = # avol, # gndx0 = # lax2, # gndx3 = # lax1, n0 + # buf = gnd.alignedsize + 2 * NODE_HEADER_SIZE + n1, LEB_SIZE = n1 + # buf0 + 2 * NODE_HEADER_SIZE + gnd.alignedsize, LEB_SIZE = n0 + # buf0 + # buf, avol[m5] = mapped(buf0 + buf), align↑(m2, 2 * NODE_HEADER_SIZE) = gnd.alignedsize, m5 < # avol, abs-node(subarray(buf + mkempbuf(n0), 0, 2 * NODE_HEADER_SIZE + gnd.alignedsize), gnd), abs-nodes(buf0, gndx3, lax1, false), abs-nodes(buf, # buf0, gndx0, lax2, true), awbuf-inv(avol, bleb), buf-ro-rw-mode(isbuf, bleb, lpt0, avol), bufs-log-only(bleb, log0, lpt0), is-aligned(# buf, NODE_HEADER_SIZE), is-encoded(nodeheader(m2, false), subarray(buf, 0, NODE_HEADER_SIZE)), lpt-free-unref(lpt), lpt-leb-size(lpt), lpt-ram-flash(lpt0, lpt, log0), range=(buf, NODE_HEADER_SIZE + gnd.alignedsize, validtrailer, 0, NODE_HEADER_SIZE), # buf0 + NODE_HEADER_SIZE ≤ LEB_SIZE, # buf0 + # buf ≤ LEB_SIZE, # buf0 + 2 * NODE_HEADER_SIZE + gnd.alignedsize ≤ LEB_SIZE ⊦ buf = mkbuf(0), isempty(buf, 0, NODE_HEADER_SIZE), ∃ gndx5, lax4, buf1, buf2. buf0 + buf = buf1 + buf2 ∧ # buf1 = # buf0 + 2 * NODE_HEADER_SIZE + gnd.alignedsize ∧ abs-nodes(buf1, gndx3 + gnd ', lax1 + @(# buf0, 2 * NODE_HEADER_SIZE + gnd.alignedsize) ', false) ∧ abs-nodes(buf2, # buf1, gndx5, lax4, true), is-encoded(nodeheader(m2, false), subarray(buf, 0, NODE_HEADER_SIZE)) ∧ 2 * NODE_HEADER_SIZE + align↑(m2, 2 * NODE_HEADER_SIZE) ≤ # buf ∧ range=(buf, NODE_HEADER_SIZE + align↑(m2, 2 * NODE_HEADER_SIZE), validtrailer, 0, NODE_HEADER_SIZE)
Proof step 166:
# lpt = # avol, # lpt0 = # avol, # gndx0 = # lax2, # gndx3 = # lax1, n0 + # buf = gnd.alignedsize + 2 * NODE_HEADER_SIZE + n1, LEB_SIZE = n1 + # buf0 + 2 * NODE_HEADER_SIZE + gnd.alignedsize, LEB_SIZE = n0 + # buf0 + # buf, avol[m5] = mapped(buf0 + buf), align↑(m2, 2 * NODE_HEADER_SIZE) = gnd.alignedsize, m5 < # avol, abs-node(subarray(buf + mkempbuf(n0), 0, 2 * NODE_HEADER_SIZE + gnd.alignedsize), gnd), abs-nodes(buf0, gndx3, lax1, false), awbuf-inv(avol, bleb), buf-ro-rw-mode(isbuf, bleb, lpt0, avol), bufs-log-only(bleb, log0, lpt0), is-aligned(# buf, NODE_HEADER_SIZE), is-encoded(nodeheader(m2, false), subarray(buf, 0, NODE_HEADER_SIZE)), lpt-free-unref(lpt), lpt-leb-size(lpt), lpt-ram-flash(lpt0, lpt, log0), range=(buf, NODE_HEADER_SIZE + gnd.alignedsize, validtrailer, 0, NODE_HEADER_SIZE), range=(buf, NODE_HEADER_SIZE + align↑(m2, 2 * NODE_HEADER_SIZE), validtrailer, 0, NODE_HEADER_SIZE), # buf0 + NODE_HEADER_SIZE ≤ LEB_SIZE, # buf0 + # buf ≤ LEB_SIZE, # buf0 + 2 * NODE_HEADER_SIZE + gnd.alignedsize ≤ LEB_SIZE, 2 * NODE_HEADER_SIZE + align↑(m2, 2 * NODE_HEADER_SIZE) ≤ # buf, ∃ buf2, buf1. buf = buf2 + buf1 ∧ ( false ∧ abs-padding(buf2) ∧ abs-nodes(buf1, # buf0 + # buf2, gndx0, lax2, true) ∨ # buf2 = gndx0.head.flashsize ∧ gndx0 ≠ [] ∧ lax2 ≠ [] ∧ lax2.head = @(# buf0, # buf2) ∧ ¬ false ∧ abs-node(buf2, gndx0.head) ∧ abs-nodes(buf1, # buf0 + # buf2, gndx0.tail, lax2.tail, true)) ⊦ buf = mkbuf(0), isempty(buf, 0, NODE_HEADER_SIZE), ∃ gndx5, lax4, buf1, buf2. buf0 + buf = buf1 + buf2 ∧ # buf1 = # buf0 + 2 * NODE_HEADER_SIZE + gnd.alignedsize ∧ abs-nodes(buf1, gndx3 + gnd ', lax1 + @(# buf0, 2 * NODE_HEADER_SIZE + gnd.alignedsize) ', false) ∧ abs-nodes(buf2, # buf1, gndx5, lax4, true)

Rule argument

spec: abs-list, inst: encoding-group-node name: abs-nodes-valid-node seq: ⊦ is-encoded (nodeheader(m, boolvar0), subarray(buf, 0, NODE_HEADER_SIZE)) ∧ 2 * NODE_HEADER_SIZE + align↑(m, 2 * NODE_HEADER_SIZE) ≤ # buf ∧ range= (buf, NODE_HEADER_SIZE + align↑(m, 2 * NODE_HEADER_SIZE), validtrailer, 0, NODE_HEADER_SIZE) → ( abs-nodes(buf, n, gndx, lax, weak) ↔ (∃ buf0, buf1. buf = buf0 + buf1 ∧ ( boolvar0 ∧ abs-padding(buf0) ∧ abs-nodes(buf1, n + # buf0, gndx, lax, weak) ∨ # buf0 = gndx.head.flashsize ∧ gndx ≠ [] ∧ lax ≠ [] ∧ lax.head = @(n, # buf0) ∧ ¬ boolvar0 ∧ abs-node(buf0, gndx.head) ∧ abs-nodes (buf1, n + # buf0, gndx.tail, lax.tail, weak)))) subst: [m, boolvar0, weak, lax, gndx, n, buf] → [m2, false, true, lax2, gndx0, # buf0, buf] flags: <all paths>

Additional information

Used terms: m2, false, true, lax2, gndx0, # buf0, buf