Proof step 73 from proof inv-allocate-gnd (previous step)

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 74:

  # lpt0 = # avol0, # lpt = # avol0, lpt[n0] = mklp(0, m3, LP_FREE, m2), err = err0, err = ESUCCESS, err1 = err, freelist = (n0 ' + nx0).tail, keyset(gch) = gc-heap(lpt, log1), log = log1, lpt1 = lpt[n0, mklp(lpt[n0].ref-size, 0, lpt[n0].flags, lpt[n0].gcheapidx)] [n0, lpt[n0, mklp(lpt[n0].ref-size, 0, lpt[n0].flags, lpt[n0].gcheapidx)][n0].ref-size:= 0 ], n0 < # lpt, n0 < # lpt[n0, mklp(lpt[n0].ref-size, 0, lpt[n0].flags, lpt[n0].gcheapidx)], n0 < # avol0, n0 < # lpt1, awbuf-inv(avol0[n0, mapped(mkbuf(0))], buffered(n0)), awbuf-inv(avol0, bleb), awbuf-inv(avol0[n0, mapped(mkbuf(0))], bleb), bin-heap-inv(gch, lpt), buf-ro-rw-mode(false, bleb, lpt, avol0), bufs-log-only(bleb, log1, lpt), freelist-cons(lpt, n0 ' + nx0), log-group-block(log1, lpt), lpt-free-unref(lpt0), lpt-free-unref(lpt), lpt-leb-size(lpt0), lpt-leb-size(lpt), lpt-ram-flash(lpt, lpt0, log1), synced(avol0), synced(avol0[n0, mapped(mkbuf(0))]), ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ n0 ' + nx0 = [], buffered(n0) = bleb, dups(log1), lpt-free-unref(lpt1[n0, lpt1[n0].flags:= LP_GROUP_NODES]) ∧ freelist-cons(lpt1[n0, lpt1[n0].flags:= LP_GROUP_NODES], freelist) ∧ log1 + n0 ' = log + n0 ' ∧ bin-heap-inv(gch, lpt1[n0, lpt1[n0].flags:= LP_GROUP_NODES]) ∧ keyset(gch) = gc-heap(lpt1[n0, lpt1[n0].flags:= LP_GROUP_NODES], log + n0 ') ∧ bufs-log-only(buffered(n0), log + n0 ', lpt1[n0, lpt1[n0].flags:= LP_GROUP_NODES]) ∧ # lpt1[n0, lpt1[n0].flags:= LP_GROUP_NODES] = # avol0 ∧ ¬ dups(log + n0 ') ∧ log-group-block(log + n0 ', lpt1[n0, lpt1[n0].flags:= LP_GROUP_NODES]) ∧ buf-ro-rw-mode(false, buffered(n0), lpt1[n0, lpt1[n0].flags:= LP_GROUP_NODES], avol0[n0, mapped(mkbuf(0))]) ∧ lpt-leb-size(lpt1[n0, lpt1[n0].flags:= LP_GROUP_NODES]) ∧ lpt-ram-flash(lpt1[n0, lpt1[n0].flags:= LP_GROUP_NODES], lpt0, log + n0 ')

Rule argument

Additional information