Proof step 23 from proof inv-add-ind (previous step)

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 24:

  # buf1 = 2 * NODE_HEADER_SIZE + ind.alignedsize, # lpt1 = # avol, # lpt0 = # avol, isbuf1 ↔ false, lpt1[n] = mklp(m1, m3, LP_INDEX_NODES, m2), avol[n] = mapped(buf0), bleb1 = buffered(n), keyset(gch) = gc-heap(lpt1, log0), n < # avol, awbuf-inv(avol, buffered(n)), bin-heap-inv(gch, lpt1), buf-ro-rw-mode(false, buffered(n), lpt1, avol), bufs-log-only(buffered(n), log0, lpt1), freelist-cons(lpt1, freelist), log-group-block(log0, lpt1), lpt-free-unref(lpt1), lpt-free-unref(lpt0), lpt-leb-size(lpt1), lpt-leb-size(lpt0), lpt-ram-flash(lpt1, lpt0, log0), err = ESUCCESS → abs-node(buf1, ind) ∧ m4 = # buf1, m3 + # buf1 ≤ LEB_SIZE → m3 = # buf0, err = ESUCCESS ∨ ⌊err⌋ ⊦ ⟪if err = ESUCCESS then if ¬ lpt1[buffered(n).leb].size + m4 ≤ LEB_SIZE then {debug#("persistence: trying to write beyond LEB size"); awbuf_enter_readonly#(adr0, m0, log0, avol, lpt0, ns, bleb1; ; isbuf1); err := ENOSPC} else {awbuf_write_buf#(m4, buf1, adr0, m0, log0, lpt0, ns, bleb1; avol, isbuf1; err); if err = ESUCCESS then {adr := @(buffered(n).leb, lpt1[buffered(n).leb].size, m4); lpt1[buffered(n).leb] := mklp (lpt1[buffered(n).leb].ref-size, lpt1[buffered(n).leb].size + m4, lpt1[buffered(n).leb].flags, lpt1[buffered(n).leb].gcheapidx)} else lpt1[buffered(n).leb] := mklp(lpt1[buffered(n).leb].ref-size, LEB_SIZE, lpt1[buffered(n).leb].flags, lpt1[buffered(n).leb].gcheapidx)} else {debug#("persistence: could not encode index node"); awbuf_enter_readonly#(adr0, m0, log0, avol, lpt0, ns, bleb1; ; isbuf1)}⟫ ( lpt-free-unref(lpt1) ∧ freelist-cons(lpt1, freelist) ∧ bin-heap-inv(gch, lpt1) ∧ keyset(gch) = gc-heap(lpt1, log0) ∧ bufs-log-only(bleb1, log0, lpt1) ∧ # lpt1 = # avol ∧ log-group-block(log0, lpt1) ∧ buf-ro-rw-mode(isbuf1, bleb1, lpt1, avol) ∧ lpt-leb-size(lpt1) ∧ lpt-ram-flash(lpt1, lpt0, log0) ∧ awbuf-inv(avol, bleb1) ∧ # lpt0 = # avol)

Rule argument

Additional information