Proof step 64 from proof inv-read-gblock-nodes (previous step)

Heuristic symbolic execution applied rule let right

And obtained the following new goals

• Proof step 65:

  # gndx = # lax, # lpt = # avol, # lpt0 = # avol, LEB_SIZE = n0 + # buf1, avol[m5] = mapped(buf1), err = ESUCCESS, m = 2 * NODE_HEADER_SIZE + align↑(ndhd.size, 2 * NODE_HEADER_SIZE), m0 = m1, m2 = LEB_SIZE, m5 < # avol, m1 < LEB_SIZE, abs-nodes(buf1, gndx, lax, true), awbuf-inv(avol, bleb), buf-ro-rw-mode(isbuf, bleb, lpt0, avol), bufs-log-only(bleb, log0, lpt0), lpt-free-unref(lpt), lpt-leb-size(lpt), lpt-ram-flash(lpt0, lpt, log0), read-gblock-inv(m5, m1, ax, gndx0, ax1, gndx2, buf1, false), m1 + NODE_HEADER_SIZE ≤ LEB_SIZE, # buf1 ≤ LEB_SIZE, err = ESUCCESS → is-encoded(ndhd, subarray(buf1 + mkempbuf(n0), m1, NODE_HEADER_SIZE)), err = ESUCCESS ∨ ⌊err⌋ ⊦ ⟪if m2 < m0 + m then {debug#("persistence: read_gblock_nodes ignoring node of size " + m.toString + " at offset " + m0.toString + " in LEB " + m5.toString); err := ENOENT} else if ¬ range= (copy(avol[m5].data + mkempbuf(n0), 0, mkbuf(LEB_SIZE), 0, LEB_SIZE), m0 + NODE_HEADER_SIZE + align↑(ndhd.size, 2 * NODE_HEADER_SIZE), validtrailer, 0, NODE_HEADER_SIZE) then {err := ENOENT; debug#("persistence: read_gblock_nodes partial node at offset " + m0.toString + " in LEB " + m5.toString)} else if ¬ ndhd.ispadding then let gnd = ? in {decode_group_node#(m0, m, copy(avol[m5].data + mkempbuf(n0), 0, mkbuf(LEB_SIZE), 0, LEB_SIZE); gnd; err); if err ≠ ESUCCESS then debug#("persistence: read_gblock_nodes could not decode node at offset " + m0.toString + " in LEB " + m5.toString) else {gndx0 := gndx0 + gnd '; ax := ax + @(m5, m0, m) '}}; if err = ESUCCESS then m0 := m0 + m⟫ ( (err = ESUCCESS ∨ err = ENOENT ∨ ⌊err⌋ ) ∧ (err = ESUCCESS ∨ err = ENOENT → read-gblock-inv(m5, m0, ax, gndx0, ax1, gndx2, avol[m5].data, err = ENOENT)) ∧ (err ≠ ESUCCESS ⊃ 0;m2 - m0) < m2 - m1), isempty(buf1 + mkempbuf(n0), m1, NODE_HEADER_SIZE)

Rule argument

Additional information