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

Heuristic symbolic execution applied rule if positive right

And obtained the following new goals

• Proof step 11:

  maxino0 = maxino4, maxino1 = LEB_SIZE ⊦ [fail_or_success#(; ; err); if err = ESUCCESS then pstate := unbuffered, syn := true, maxino := maxino0, ginval0 := ∅, nx := [], gstore0 := ∅, gstore := ∅, istore0 := ∅, istore := ∅, ginval := ∅, adr := ? else pstate := ?, syn := ?, maxino := ?, ginval0 := ?, nx := ?, gstore0 := ?, gstore := ?, istore0 := ?, istore := ?, ginval := ?, adr := ?] ( ( err = ESUCCESS → syn ∧ inv(gstore0 \ ginval) ∧ inv(gstore) ∧ elems nx ∩ ginval = ∅ ∧ ¬ dups(nx) ∧ dom gstore ∪ elems nx = dom gstore0 ∪ ginval ∧ 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)) → ⟪let n = ? in {apersistence_get_leb_size#(adr, istore0, istore, ginval, gstore0, gstore, nx, maxino, ginval0, pstate, syn; ; n); ginval := ginval0, ginval0 := ginval; if err = ESUCCESS then let ind = indexnode(mkbrarray(BRANCH_SIZE), true, 0) in let maxino1 = ind.flashsize in {if n < maxino1 then {debug#("btree: initial index node to large"); err := ENOSPC}; if err = ESUCCESS then apersistence_allocate_ind#(adr, istore, ginval0, gstore0, gstore, nx, maxino, ginval, syn; istore0, pstate; err); if err = ESUCCESS then apersistence_add_ind# (ind, adr, istore, ginval0, gstore0, gstore, nx, maxino, ginval; adr0, istore0, pstate, syn; err); if err = ESUCCESS then apersistence_set_iblock_refsize# (adr0.lnum, maxino1, adr, istore, ginval0, gstore0, gstore, nx, maxino, ginval, pstate, syn; istore0); if err = ESUCCESS then apersistence_sync#(adr, istore0, istore, ginval0, gstore0, gstore, nx, maxino, ginval; pstate, syn; err); if err = ESUCCESS then let ns = ∅ in apersistence_commit# (adr0, maxino4, syn; ns, istore0, ginval0, gstore0, adr, istore, gstore, nx, maxino, ginval; pstate, err)}}⟫ ( ( err = ESUCCESS → syn ∧ (∃ 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