Proof step 158 from proof inv-format (previous step)

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 159:

  err = err0, gstore = ∅, gstore0 = ∅, istore = ∅, istore0 = (∅ )[n0, indexblock (indexnode(mkbrarray(BRANCH_SIZE), true, 0) ', @(maxino2, indexnode(mkbrarray(BRANCH_SIZE), true, 0).flashsize) ', indexnode(mkbrarray(BRANCH_SIZE), true, 0).flashsize) ], maxino = maxino4, nx = [], inv((∅)[n0, indexblock([], [], 0)]), inv((∅)[n0, indexblock(indexnode(mkbrarray(BRANCH_SIZE), true, 0) ', @(maxino2, indexnode(mkbrarray(BRANCH_SIZE), true, 0).flashsize) ', 0)]), inv ((∅ )[n0, indexblock (indexnode(mkbrarray(BRANCH_SIZE), true, 0) ', @(maxino2, indexnode(mkbrarray(BRANCH_SIZE), true, 0).flashsize) ', indexnode(mkbrarray(BRANCH_SIZE), true, 0).flashsize) ]), indexnode(mkbrarray(BRANCH_SIZE), true, 0).flashsize ≤ LEB_SIZE, ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ ⟪ginval0 := ∅; ginval := ∅; if err = ESUCCESS then {istore0 := remove-refsize0(istore0); istore := istore0; gstore0 := remove-refsize0(gstore0); gstore := gstore0; ginval0 := ∅; adr := @(index(n0).lnum, maxino2, indexnode(mkbrarray(BRANCH_SIZE), true, 0).flashsize); ginval := ∅; nx := []; maxino := maxino4; pstate := unbuffered} else pstate := readonly; ginval1 := ?⟫ ( ( err = ESUCCESS → (∃ ri, fi. btree-inv(null, adr, istore0, istore, zh, ri, fi)) ∧ 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)) ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ (err = ESUCCESS → btree-inv(null, adr, istore0, istore, zh, ∅, ∅) ∧ gstore0 = ∅ ∧ ginval0 = ∅ ∧ maxino = maxino4 ∧ nx = [] ∧ ginval = ∅))

Rule argument

Additional information