Proof step 9 from proof refine-get-gc-block (previous step)

Heuristic symbolic execution applied rule or right

And obtained the following new goals

• Proof step 10:

  # lpt0 = # avol, # lpt = # avol, adr = adr0, gstore = gstore1, gstore0 = gstore2, istore = istore1, istore0 = istore2, keyset(gch) = gc-heap(lpt, log0), log = log0, maxino = m, ns = ns0, remove-refsize0(istore1) = istore1, remove-refsize0(gstore1) = gstore1, elems log0 ∩ ginval = ∅, dom gstore1 ∪ elems log0 = dom gstore2 ∪ ginval, ginval < # avol, abs-gstore(avol, lpt, gstore2, ginval), abs-istore(avol, lpt, istore2), awbuf-inv(avol, bleb), bin-heap-inv(gch, lpt), buf-ro-rw-mode(pstate = readonly, bleb, lpt, avol), bufs-log-only(bleb, log0, lpt), flash-lpt-cons(lpt0, istore1, gstore1), freelist-cons(lpt, freelist), inv(istore1), inv(istore2), inv(gstore1), inv(gstore2 \ ginval), log-group-block(log0, lpt), lpt-free-unref(lpt0), lpt-free-unref(lpt), lpt-leb-size(lpt0), lpt-leb-size(lpt), lpt-ram-flash(lpt, lpt0, log0), istore1 ⊑ istore2, err1 ≠ ESUCCESS → n1 = n0, err1 = ESUCCESS → n1 < # avol ∧ lpt[n1].flags = LP_GROUP_NODES ∧ ¬ n1 ∈ log0, pstate = unbuffered → isbuf, pstate.index? → pstate.lnum ∈ istore2, pstate.journal? → log0 ≠ [] ∧ pstate.lnum = log0.last ∧ pstate.lnum ∈ gstore2, pstate ≠ unbuffered ∧ pstate ≠ readonly → bleb = buffered(pstate.lnum), pstate = unbuffered → bleb = nobuffer, isbuf → synced(avol), err1 = ENOSPC ∨ err1 = ESUCCESS ⊦ ⟨choose n with n ∈ dom gstore0 ∧ ¬ n ∈ log in {n0 := n; err := ESUCCESS} ifnone err := ENOSPC⟩ ( (isbuf → synced(avol)) ∧ (pstate = unbuffered → bleb = nobuffer) ∧ (pstate ≠ unbuffered ∧ pstate ≠ readonly → bleb = buffered(pstate.lnum)) ∧ n1 = n0 ∧ err1 = err), ⟨err := ENOSPC⟩ ( (isbuf → synced(avol)) ∧ (pstate = unbuffered → bleb = nobuffer) ∧ (pstate ≠ unbuffered ∧ pstate ≠ readonly → bleb = buffered(pstate.lnum)) ∧ n1 = n0 ∧ err1 = err), dups(log0)

Rule argument

Additional information