Proof step 151 from proof inv-io-save (previous step)

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 152:

  zh[r] = mkznode(r0, zbrar, boolvar, true, m0), adr = @(pstate.lnum, maxino, ind.flashsize), adr2 = adr1, err0 = err, ginval0 = ginval2, gstore = gstore1, gstore0 = gstore2, ind = save(mkznode(r0, zbrar, boolvar, true, m0)), istore = istore3[n, indexblock([], [], 0)], istore0 = istore2, pstate = index(n), remove-refsize0(istore2) = istore2, remove-refsize0(gstore1) = gstore1, syn, elems nx ∩ ginval2 = ∅, dom gstore1 ∪ elems nx = dom gstore2 ∪ ginval2, ((btree(rp, r, adr1, height, dirty, ri, nodes(istore3), as, alladrs, ok) * P))(zh), n0 < save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize, btree-sub-clean(r, m0, zh), inv(istore3[n, indexblock([], [], 0)]), inv(istore2), inv(istore3), inv(gstore1), inv(gstore2 \ ginval2), refsize-cons(istore3, as0 ∪ as), m ∈ istore3, r ∈ zh, n0 ≤ LEB_SIZE, as ⊆ dom nodes(istore3), as ⊆ alladrs, alladrs ⊆ dom nodes(istore3), as0 ⊆ dom nodes(istore3), istore2 ⊑ istore3[n, indexblock([], [], 0)], istore2 ⊑ istore3, height = 0 → as = ∅, ¬ @(pstate.lnum, maxino, ind.flashsize) ∈ istore ∧ err = ESUCCESS ∨ ⌊err⌋ , pstate.index? ∨ pstate.journal? ⊦ [if err0 = ESUCCESS then {istore[pstate.lnum].indlist := istore[pstate.lnum].indlist + ind; istore[pstate.lnum].ladrlist := istore[pstate.lnum].ladrlist + @(adr.pos, adr.size)} else adr := ?, pstate := readonly; syn := ?] ( inv(istore) ∧ istore2 ⊑ istore ∧ (pstate.journal? → nx ≠ [] ∧ pstate.lnum = nx.last ∧ pstate.lnum ∈ gstore2) ∧ (pstate.index? → pstate.lnum ∈ istore) ∧ (pstate = unbuffered → syn) → ⟪if err0 = ESUCCESS then let maxino = 0 in {apersistence_get_iblock_refsize# (adr.lnum, adr0, istore, istore2, ginval2, gstore2, gstore1, nx, maxino0, ginval, pstate, syn; ; maxino); apersistence_set_iblock_refsize# (adr.lnum, maxino + adr.size, adr0, istore2, ginval2, gstore2, gstore1, nx, maxino0, ginval, pstate, syn; istore)}; if err0 = ESUCCESS then zh[r].dirty := false⟫ ( refsize-cons(istore, as0 ∪ (err0 = ESUCCESS ⊃ as ++ adr;as)) ∧ inv(istore) ∧ istore2 ⊑ istore ∧ (pstate.journal? → nx ≠ [] ∧ pstate.lnum = nx.last ∧ pstate.lnum ∈ gstore2) ∧ (pstate.index? → pstate.lnum ∈ istore) ∧ (pstate = unbuffered → syn) ∧ istore3 ⊑ istore ∧ r ∈ zh ∧ (err0 = ESUCCESS → ¬ adr ∈ as) ∧ dom nodes(istore) = dom nodes(istore3) ∪ (err0 = ESUCCESS ⊃ ∅ ++ adr;∅) ∧ (err0 = ESUCCESS → ¬ adr ∈ istore3) ∧ (( btree (rp, r, (err0 = ESUCCESS ⊃ adr;adr1), height, err0 ≠ ESUCCESS, ri, nodes(istore), (err0 = ESUCCESS ⊃ as ++ adr;as), (err0 = ESUCCESS ⊃ (alladrs -- adr1) ++ adr;alladrs), ok) * P) )(zh) ∧ (err0 = ESUCCESS ∨ ⌊err0⌋ ) ∧ (err0 = ESUCCESS → pstate.index? ∧ ¬ zh[r].dirty))), dups(nx), n ∈ istore3, adr1 ∈ as

Rule argument

Additional information