| syn ↔ true, zh[rp] = mkznode(r, zbrar, boolvar, boolvar0, m), adr = adr3, adr0 = adr3, adr1 = adr3, ginval0 = ginval4, gstore = gstore1, gstore0 = gstore2, istore = istore1, istore0 = istore2, maxino = maxino2, maxino0 = maxino1, pstate = unbuffered, remove-refsize0(gstore1) = gstore1, remove-refsize0(istore1) = istore1, dom remove-refsize0(gstore2) ∩ ginval4 = ∅, elems nx ∩ ginval4 = ∅, dom gstore1 ∪ elems nx = dom gstore2 ∪ ginval4, btree-inv(rp, adr3, istore2, istore1, zh, ri, fi), inv(gstore2 \ ginval4), inv(gstore1), inv(istore2), inv(istore1), istore1 ⊑ istore2 ⊦ [fail_or_success#(; ; err); if err = ESUCCESS then {istore0 := remove-refsize0(istore0); istore := istore0; gstore0 := remove-refsize0(gstore0); gstore := gstore0; ginval0 := ∅; adr := adr0; ginval := ginval1; nx := []; maxino := maxino0; pstate := unbuffered} else pstate := readonly; ginval1 := ?] ( inv(gstore0 \ ginval0) ∧ inv(gstore) ∧ elems nx ∩ ginval0 = ∅ ∧ ¬ dups(nx) ∧ dom gstore ∪ elems nx = dom gstore0 ∪ ginval0 ∧ remove-refsize0(gstore) = gstore ∧ inv(istore0) ∧ inv(istore) ∧ istore ⊑ istore0 ∧ remove-refsize0(istore) = istore ∧ (pstate.journal? → nx ≠ [] ∧ pstate.lnum = nx.last ∧ pstate.lnum ∈ gstore0) ∧ (pstate.index? → pstate.lnum ∈ istore0) → ⟪syn0 := true; adr0 := adr; maxino2 := maxino, gstore1 := gstore, gstore2 := gstore0, ginval4 := ginval0, istore1 := istore, istore2 := istore0; if err = ESUCCESS then adr3 := adr1 else if false then {zh[rp].dirty := true; let maxino = 0 in {apersistence_get_iblock_refsize# (adr1.lnum, adr0, istore2, istore1, ginval4, gstore2, gstore1, nx, maxino2, ginval, pstate, syn0; ; maxino); apersistence_set_iblock_refsize# (adr1.lnum, maxino - adr1.size, adr0, istore1, ginval4, gstore2, gstore1, nx, maxino2, ginval, pstate, syn0; istore2)}}⟫ ( (∃ ri, fi. btree-inv(rp, adr0, istore2, istore1, zh, ri, fi)) ∧ inv(istore2) ∧ istore1 ⊑ istore2 ∧ (pstate.journal? → nx ≠ [] ∧ pstate.lnum = nx.last ∧ pstate.lnum ∈ gstore2) ∧ (pstate.index? → pstate.lnum ∈ istore2) ∧ (pstate = unbuffered → syn0))), dups(nx), rp ≠ null ∧ boolvar0 |
zh[rp] = mkznode(r, zbrar, boolvar, boolvar0, m), remove-refsize0(istore1) = istore1, remove-refsize0(gstore1) = gstore1, elems nx ∩ ginval4 = ∅, dom remove-refsize0(gstore2) ∩ ginval4 = ∅, dom gstore1 ∪ elems nx = dom gstore2 ∪ ginval4, btree-inv(rp, adr3, istore2, istore1, zh, ri, fi), inv(istore1), inv(istore2), inv(gstore1), inv(gstore2 \ ginval4), istore1 ⊑ istore2, ¬ dups(nx) ⊦ [fail_or_success#(; ; err); istore0 := istore2; istore := istore1; gstore0 := gstore2; gstore := gstore1; ginval0 := ginval4; adr := adr3; if err = ESUCCESS then {istore0 := remove-refsize0(istore0); istore := istore0; gstore0 := remove-refsize0(gstore0); gstore := gstore0; ginval0 := ∅; adr := adr3; ginval := ginval1; nx := []; maxino := maxino0; pstate := unbuffered} else pstate := readonly; ginval1 := ?] ( inv(gstore0 \ ginval0) ∧ inv(gstore) ∧ elems nx ∩ ginval0 = ∅ ∧ ¬ dups(nx) ∧ dom gstore ∪ elems nx = dom gstore0 ∪ ginval0 ∧ remove-refsize0(gstore) = gstore ∧ inv(istore0) ∧ inv(istore) ∧ istore ⊑ istore0 ∧ remove-refsize0(istore) = istore ∧ (pstate.journal? → nx ≠ [] ∧ pstate.lnum = nx.last ∧ pstate.lnum ∈ gstore0) ∧ (pstate.index? → pstate.lnum ∈ istore0) → ⟪syn0 := true; adr0 := adr; maxino2 := maxino, gstore1 := gstore, gstore2 := gstore0, ginval4 := ginval0, istore1 := istore, istore2 := istore0; if err = ESUCCESS then adr := adr3 else if false then {zh[rp].dirty := true; let maxino = 0 in {apersistence_get_iblock_refsize# (adr3.lnum, adr0, istore2, istore1, ginval4, gstore2, gstore1, nx, maxino2, ginval, pstate, syn0; ; maxino); apersistence_set_iblock_refsize# (adr3.lnum, maxino - adr3.size, adr0, istore1, ginval4, gstore2, gstore1, nx, maxino2, ginval, pstate, syn0; istore2)}}⟫ ( (∃ ri, fi. btree-inv(rp, adr0, istore2, istore1, zh, ri, fi)) ∧ inv(istore2) ∧ istore1 ⊑ istore2 ∧ (pstate.journal? → nx ≠ [] ∧ pstate.lnum = nx.last ∧ pstate.lnum ∈ gstore2) ∧ (pstate.index? → pstate.lnum ∈ istore2) ∧ (pstate = unbuffered → syn0))), rp ≠ null ∧ boolvar0