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

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 220:

  # buf = # buf0, # gndx = # lax, # lpt = # avol, # lpt0 = # avol, avol[m5] = mapped(buf1), buf0 = mkbuf(LEB_SIZE), err = err0, m0 = 0, m2 = LEB_SIZE, m3 = m5, n = LEB_SIZE, 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), range=(buf, n, buf0, n, # buf0 - n), ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ ⟪gndx0 := gndx1; ax := ax0; buf2 := buf; while err = ESUCCESS ∧ m0 < m2 do {/* (inv-read-gblock-nodes : invariant (err = ESUCCESS ∨ err = ENOENT ∨ ⌊err⌋ ) ∧ (err = ESUCCESS ∨ err = ENOENT → read-gblock-inv(m3, m0, ax, gndx0, ax`, gndx0`, avol[m3].data, err = ENOENT)) wfbound (err ≠ ESUCCESS ⊃ 0;m2 - m0)) */; if ¬ m0 + NODE_HEADER_SIZE ≤ # buf2 ∨ isempty(buf2, m0, NODE_HEADER_SIZE) then err := ENOENT else let ndhd = ? in {decode_header#(m0, buf2; 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=(buf2, 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, buf2; 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}}}; if err = ENOENT then err := ESUCCESS⟫ ((err = ESUCCESS ∨ ⌊err⌋ ) ∧ (err = ESUCCESS → ax = ax0 + lax.to-adr(m5) ∧ gndx0 = gndx1 + gndx)), err = ESUCCESS

Rule argument

Additional information