| adr = adr1, adr0 = adr3, adr2 = adr1, ginval = ginval1, ginval0 = ginval2, gstore = gstore1, gstore0 = gstore2, ind = save(zh[r]), istore1 = istore, maxino = 0, maxino0 = maxino1, pstate = index(m), remove-refsize0(istore0) = istore0, remove-refsize0(gstore1) = gstore1, elems nx ∩ ginval2 = ∅, dom gstore1 ∪ elems nx = dom gstore2 ∪ ginval2, ((btree(rp, r, adr1, height, dirty, ri, nodes(istore), as, alladrs, ok) * P))(zh), zh[r].dirty, btree-sub-clean(r, zh[r].usedsize, zh), inv(istore0), inv(istore), inv(gstore1), inv(gstore2 \ ginval2), refsize-cons(istore, as0 ∪ as), m ∈ istore, r ∈ zh, as ⊆ alladrs, as ⊆ dom nodes(istore), alladrs ⊆ dom nodes(istore), as0 ⊆ dom nodes(istore), istore0 ⊑ istore ⊦ ⟪apersistence_get_block_free_size#(adr0, istore, istore0, ginval0, gstore0, gstore, nx, maxino0, ginval, pstate, syn; ; maxino); if maxino < ind.flashsize then {apersistence_sync#(adr0, istore, istore0, ginval0, gstore0, gstore, nx, maxino0, ginval; pstate, syn; err); if err = ESUCCESS then apersistence_allocate_ind#(adr0, istore0, ginval0, gstore0, gstore, nx, maxino0, ginval, syn; istore, pstate; err)} else err := ESUCCESS; if err = ESUCCESS then {apersistence_add_ind#(ind, adr0, istore0, ginval0, gstore0, gstore, nx, maxino0, ginval; adr, istore, pstate, syn; err); if err = ESUCCESS then let maxino = 0 in {apersistence_get_iblock_refsize# (adr.lnum, adr0, istore, istore0, ginval0, gstore0, gstore, nx, maxino0, ginval, pstate, syn; ; maxino); apersistence_set_iblock_refsize# (adr.lnum, maxino + adr.size, adr0, istore0, ginval0, gstore0, gstore, nx, maxino0, ginval, pstate, syn; istore)}}; if err = ESUCCESS then zh[r].dirty := false⟫ ( refsize-cons(istore, as0 ∪ (err = ESUCCESS ⊃ as ++ adr;as)) ∧ inv(istore) ∧ istore0 ⊑ istore ∧ (pstate.journal? → nx ≠ [] ∧ pstate.lnum = nx.last ∧ pstate.lnum ∈ gstore2) ∧ (pstate.index? → pstate.lnum ∈ istore) ∧ (pstate = unbuffered → syn) ∧ istore1 ⊑ istore ∧ r ∈ zh ∧ (err = ESUCCESS → ¬ adr ∈ as) ∧ dom nodes(istore) = dom nodes(istore1) ∪ (err = ESUCCESS ⊃ ∅ ++ adr;∅) ∧ (err = ESUCCESS → ¬ adr ∈ istore1) ∧ (( btree (rp, r, (err = ESUCCESS ⊃ adr;adr2), height, err ≠ ESUCCESS, ri, nodes(istore), (err = ESUCCESS ⊃ as ++ adr;as), (err = ESUCCESS ⊃ (alladrs -- adr2) ++ adr;alladrs), ok) * P) )(zh) ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ (err = ESUCCESS → pstate.index? ∧ ¬ zh[r].dirty)), dups(nx) |
remove-refsize0(gstore1) = gstore1, remove-refsize0(istore0) = istore0, elems nx ∩ ginval2 = ∅, dom gstore1 ∪ elems nx = dom gstore2 ∪ ginval2, ((btree(rp, r, adr1, height, dirty, ri, nodes(istore), as, alladrs, ok) * P))(zh), zh[r].dirty, btree-sub-clean(r, zh[r].usedsize, zh), inv(gstore2 \ ginval2), inv(gstore1), inv(istore), inv(istore0), refsize-cons(istore, as0 ∪ as), r ∈ zh, m ∈ istore, as0 ⊆ dom nodes(istore), alladrs ⊆ dom nodes(istore), as ⊆ dom nodes(istore), as ⊆ alladrs, istore0 ⊑ istore, ¬ dups(nx) ⊦ ⟪apersistence_get_block_free_size#(adr0, istore, istore0, ginval2, gstore2, gstore1, nx, maxino0, ginval, index(m), syn; ; maxino); pstate := index(m); istore1 := istore; ind := save(zh[r]); gstore0 := gstore2; if maxino < ind.flashsize then {apersistence_sync#(adr0, istore, istore0, ginval2, gstore0, gstore1, nx, maxino0, ginval; pstate, syn; err); if err = ESUCCESS then apersistence_allocate_ind#(adr0, istore0, ginval2, gstore0, gstore1, nx, maxino0, ginval, syn; istore, pstate; err)} else err := ESUCCESS; adr := adr1; if err = ESUCCESS then {apersistence_add_ind#(ind, adr0, istore0, ginval2, gstore0, gstore1, nx, maxino0, ginval; adr, istore, pstate, syn; err); if err = ESUCCESS then let maxino = 0 in {apersistence_get_iblock_refsize# (adr.lnum, adr0, istore, istore0, ginval2, gstore0, gstore1, nx, maxino0, ginval, pstate, syn; ; maxino); apersistence_set_iblock_refsize# (adr.lnum, maxino + adr.size, adr0, istore0, ginval2, gstore0, gstore1, nx, maxino0, ginval, pstate, syn; istore)}}; if err = ESUCCESS then zh[r].dirty := false⟫ ( refsize-cons(istore, as0 ∪ (err = ESUCCESS ⊃ as ++ adr;as)) ∧ inv(istore) ∧ istore0 ⊑ istore ∧ (pstate.journal? → nx ≠ [] ∧ pstate.lnum = nx.last ∧ pstate.lnum ∈ gstore2) ∧ (pstate.index? → pstate.lnum ∈ istore) ∧ (pstate = unbuffered → syn) ∧ istore1 ⊑ istore ∧ r ∈ zh ∧ (err = ESUCCESS → ¬ adr ∈ as) ∧ dom nodes(istore) = dom nodes(istore1) ∪ (err = ESUCCESS ⊃ ∅ ++ adr;∅) ∧ (err = ESUCCESS → ¬ adr ∈ istore1) ∧ (( btree (rp, r, (err = ESUCCESS ⊃ adr;adr1), height, err ≠ ESUCCESS, ri, nodes(istore), (err = ESUCCESS ⊃ as ++ adr;as), (err = ESUCCESS ⊃ (alladrs -- adr1) ++ adr;alladrs), ok) * P) )(zh) ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ (err = ESUCCESS → pstate.index? ∧ ¬ zh[r].dirty))