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

Heuristic conditional right split applied rule if right

And obtained the following new goals

• Proof step 32:

  # lpt0 = # avol, # lpt = # avol, # gndx = # lax, avol[m5] = mapped(buf1), ax1 = ax0, buf = copy(avol[m5].data + mkempbuf(LEB_SIZE - # avol[m5].data), 0, buf0, 0, LEB_SIZE), buf0 = mkbuf(LEB_SIZE), err = ESUCCESS, err = err1, err2 = err0, err2 = ESUCCESS, gndx2 = gndx1, m0 = m, m1 = 0, m2 = LEB_SIZE, m3 = m5, avol[m5].mapped?, m0 < m2, m5 < # avol, 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), 0 + LEB_SIZE ≤ #(avol[m5].data + mkempbuf(LEB_SIZE - # avol[m5].data)), 0 + LEB_SIZE ≤ # buf0, LEB_SIZE ≥ # avol[m5].data, err = ESUCCESS ∨ err = ENOENT → read-gblock-inv(m3, m0, ax, gndx0, ax1, gndx2, avol[m3].data, err = ENOENT), ¬ m0 + NODE_HEADER_SIZE ≤ # buf ∨ isempty(buf, m0, NODE_HEADER_SIZE), err = ESUCCESS ∨ err = ENOENT ∨ ⌊err⌋ , ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ ⟪err := ENOENT⟫ ( ( (err = ESUCCESS ∨ err = ENOENT ∨ ⌊err⌋ ) ∧ (err = ESUCCESS ∨ err = ENOENT → read-gblock-inv(m3, m0, ax, gndx0, ax1, gndx2, avol[m3].data, err = ENOENT))) ∧ (err ≠ ESUCCESS ⊃ 0;m2 - m0) < (err1 ≠ ESUCCESS ⊃ 0;m2 - m))

• Proof step 47:

  # lpt0 = # avol, # lpt = # avol, # gndx = # lax, avol[m5] = mapped(buf1), ax1 = ax0, buf = copy(avol[m5].data + mkempbuf(LEB_SIZE - # avol[m5].data), 0, buf0, 0, LEB_SIZE), buf0 = mkbuf(LEB_SIZE), err = ESUCCESS, err = err1, err2 = err0, err2 = ESUCCESS, gndx2 = gndx1, m0 = m, m1 = 0, m2 = LEB_SIZE, m3 = m5, avol[m5].mapped?, m0 < m2, m5 < # avol, 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), m0 + NODE_HEADER_SIZE ≤ # buf, 0 + LEB_SIZE ≤ #(avol[m5].data + mkempbuf(LEB_SIZE - # avol[m5].data)), 0 + LEB_SIZE ≤ # buf0, LEB_SIZE ≥ # avol[m5].data, err = ESUCCESS ∨ err = ENOENT → read-gblock-inv(m3, m0, ax, gndx0, ax1, gndx2, avol[m3].data, err = ENOENT), err = ESUCCESS ∨ err = ENOENT ∨ ⌊err⌋ , ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ ⟪let ndhd = ? in {decode_header#(m0, buf; ndhd; err); if err ≠ ESUCCESS then debug#("persistence: read_gblock_nodes could not decode header in LEB " + m3.toString + " at offset " + m0.toString) else let m = 2 * NODE_HEADER_SIZE + align↑(ndhd.size, 2 * NODE_HEADER_SIZE) in {if m2 < m0 + m then {debug# ("persistence: read_gblock_nodes ignoring node of size " + m.toString + " at offset " + m0.toString + " in LEB " + m3.toString); err := ENOENT} else if ¬ range=(buf, 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 " + m3.toString)} else if ¬ ndhd.ispadding then let gnd = ? in {decode_group_node#(m0, m, buf; gnd; err); if err ≠ ESUCCESS then debug# ("persistence: read_gblock_nodes could not decode node at offset " + m0.toString + " in LEB " + m3.toString) else {gndx0 := gndx0 + gnd '; ax := ax + @(m3, m0, m) '}}; if err = ESUCCESS then m0 := m0 + m}}⟫ ( ( (err = ESUCCESS ∨ err = ENOENT ∨ ⌊err⌋ ) ∧ (err = ESUCCESS ∨ err = ENOENT → read-gblock-inv(m3, m0, ax, gndx0, ax1, gndx2, avol[m3].data, err = ENOENT))) ∧ (err ≠ ESUCCESS ⊃ 0;m2 - m0) < (err1 ≠ ESUCCESS ⊃ 0;m2 - m)), isempty(buf, m0, NODE_HEADER_SIZE)

Rule argument

Additional information