Proof step 174 from proof inv-commit (previous step)

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 175:

  zh0[rp] = mkznode(r0, zbrar0, boolvar0, false, m4), zh[rp] = mkznode(r, zbrar, boolvar, true, m), istore2[m0] = indexblock(indx, lax, m3), err1 = ESUCCESS, err1 = err, ginval0 = ginval4, gstore = gstore1, gstore0 = gstore2, istore = istore1, istore0 = remove-refsize0(istore2), 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, adr, istore2[m0, indexblock(indx, lax, m3 - m2)], istore1, zh0[rp, mkznode(r0, zbrar0, boolvar0, true, m4)], ri, fi), btree-inv(rp, @(m0, m1, m2), istore2, istore2, zh0, ri, ri), btree-inv(rp, adr, istore3, istore1, zh, ri, fi), btree-inv(rp, adr, istore3[n, indexblock([], [], 0)], istore1, zh, ri, fi), inv(istore2), inv(gstore2 \ ginval4), inv(gstore1), inv(istore3), inv(istore1), inv(istore3[n, indexblock([], [], 0)]), rp ∈ zh, istore3[n, indexblock([], [], 0)] ⊑ istore2, istore1 ⊑ istore3, istore1 ⊑ istore3[n, indexblock([], [], 0)], istore1 ⊑ istore2, pstate1.journal? → nx ≠ [] ∧ pstate1.lnum = nx.last ∧ pstate1.lnum ∈ gstore2, pstate1.index? → pstate1.lnum ∈ istore2, ⌊err⌋ ∨ err = ESUCCESS ⊦ [ginval := ginval1; nx := []; maxino := maxino0; pstate := unbuffered; ginval1 := ?] ( inv(remove-refsize0(gstore0) \ ∅) ∧ inv(remove-refsize0(gstore0)) ∧ elems nx ∩ ∅ = ∅ ∧ ¬ dups(nx) ∧ dom remove-refsize0(gstore0) ∪ elems nx = dom remove-refsize0(gstore0) ∪ ∅ ∧ remove-refsize0(remove-refsize0(gstore0)) = remove-refsize0(gstore0) ∧ inv(istore0) ∧ inv(istore0) ∧ istore0 ⊑ istore0 ∧ remove-refsize0(istore0) = istore0 ∧ (pstate.journal? → nx ≠ [] ∧ pstate.lnum = nx.last ∧ pstate.lnum ∈ remove-refsize0(gstore0)) ∧ (pstate.index? → pstate.lnum ∈ istore0) → ⟪adr0 := @(m0, m1, m2); syn1 := true; pstate1 := pstate, maxino2 := maxino, gstore1 := remove-refsize0(gstore0), gstore2 := remove-refsize0(gstore0), ginval4 := ∅, istore1 := istore0; if err1 = ESUCCESS then adr := @(m0, m1, m2) else if true then {zh0[rp].dirty := true; let maxino = 0 in {apersistence_get_iblock_refsize# (m0, adr0, istore0, istore1, ginval4, gstore2, gstore1, nx, maxino2, ginval, pstate1, syn1; ; maxino); apersistence_set_iblock_refsize# (m0, maxino - m2, adr0, istore1, ginval4, gstore2, gstore1, nx, maxino2, ginval, pstate1, syn1; istore0)}}⟫ ( (∃ ri, fi. btree-inv(rp, adr0, istore0, istore1, zh0, ri, fi)) ∧ inv(istore0) ∧ istore1 ⊑ istore0 ∧ (pstate1.journal? → nx ≠ [] ∧ pstate1.lnum = nx.last ∧ pstate1.lnum ∈ gstore2) ∧ (pstate1.index? → pstate1.lnum ∈ istore0) ∧ (pstate1 = unbuffered → syn1))), pstate1 = readonly, pstate1 = unbuffered, dups(nx), n ∈ istore3

Rule argument

Additional information