[Imprint][Data Privacy Statement][E-Mail]

View long theorem info. View the proof. Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Proof step 159 from proof inv-io-save (previous step)

zh[r] = mkznode(r0, zbrar, boolvar, true, m0), remove-refsize0(gstore1) = gstore1, remove-refsize0(istore2) = istore2, elems nx ∩ ginval2 = ∅, dom gstore1 ∪ elems nx = dom gstore2 ∪ ginval2, ((btree(rp, r, adr1, height, dirty, ri, nodes(istore3), as, alladrs, ok) * P))(zh), n0 < save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize, btree-sub-clean(r, m0, zh), inv(gstore2 \ ginval2), inv(gstore1), inv(istore3), inv(istore2), inv(istore3[n, indexblock([], [], 0)]), inv(istore3[n, indexblock(save(mkznode(r0, zbrar, boolvar, true, m0)) ', @(maxino1, save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize) ', 0)]), refsize-cons(istore3, as0 ∪ as), r ∈ zh, m ∈ istore3, n0 ≤ LEB_SIZE, as0 ⊆ dom nodes(istore3), alladrs ⊆ dom nodes(istore3), as ⊆ alladrs, as ⊆ dom nodes(istore3), istore2 ⊑ istore3, istore2 ⊑ istore3[n, indexblock([], [], 0)], istore2 ⊑ istore3[n, indexblock(save(mkznode(r0, zbrar, boolvar, true, m0)) ', @(maxino1, save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize) ', 0)], ¬ dups(nx), ¬ adr1 ∈ as, ¬ n ∈ istore3, height = 0 → as = ∅ ⊦ ⟪apersistence_get_iblock_refsize# (index(n).lnum, adr0, istore3[n, indexblock([], [], 0)] [index(n).lnum, istore3[n, indexblock([], [], 0)] [index(n).lnum, istore3[n, indexblock([], [], 0)][index(n).lnum] .indlist:= (istore3[n, indexblock([], [], 0)][index(n).lnum].indlist + save(mkznode(r0, zbrar, boolvar, true, m0)) ') ] [index(n).lnum ] .ladrlist:= ( istore3[n, indexblock([], [], 0)] [index(n).lnum, istore3[n, indexblock([], [], 0)][index(n).lnum] .indlist:= (istore3[n, indexblock([], [], 0)][index(n).lnum].indlist + save(mkznode(r0, zbrar, boolvar, true, m0)) ') ] [index(n).lnum ] .ladrlist + @ (@(index(n).lnum, maxino1, save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize).pos, @(index(n).lnum, maxino1, save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize).size) ') ], istore2, ginval2, gstore2, gstore1, nx, maxino0, ginval, index(n), syn ; ; maxino); istore := istore3[n, indexblock([], [], 0)] [index(n).lnum, istore3[n, indexblock([], [], 0)] [index(n).lnum, istore3[n, indexblock([], [], 0)][index(n).lnum] .indlist:= (istore3[n, indexblock([], [], 0)][index(n).lnum].indlist + save(mkznode(r0, zbrar, boolvar, true, m0)) ') ] [index(n).lnum ] .ladrlist:= ( istore3[n, indexblock([], [], 0)] [index(n).lnum, istore3[n, indexblock([], [], 0)][index(n).lnum] .indlist:= (istore3[n, indexblock([], [], 0)][index(n).lnum].indlist + save(mkznode(r0, zbrar, boolvar, true, m0)) ') ] [index(n).lnum ] .ladrlist + @ (@(index(n).lnum, maxino1, save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize).pos, @(index(n).lnum, maxino1, save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize).size) ') ]; apersistence_set_iblock_refsize# (index(n).lnum, maxino + @(index(n).lnum, maxino1, save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize).size, adr0, istore2, ginval2, gstore2, gstore1, nx, maxino0, ginval, index(n), syn ; istore); err0 := ESUCCESS; if err0 = ESUCCESS then zh[r].dirty := false⟫ ( refsize-cons(istore, as0 ∪ (err0 = ESUCCESS ⊃ as ++ @(n, maxino1, save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize);as)) ∧ inv(istore) ∧ istore2 ⊑ istore ∧ n ∈ istore ∧ istore3 ⊑ istore ∧ r ∈ zh ∧ (err0 = ESUCCESS → ¬ @(n, maxino1, save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize) ∈ as) ∧ dom nodes(istore) = dom nodes(istore3) ∪ (err0 = ESUCCESS ⊃ ∅ ++ @(n, maxino1, save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize);∅) ∧ (( btree (rp, r, (err0 = ESUCCESS ⊃ @(n, maxino1, save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize);adr1), height, err0 ≠ ESUCCESS, ri, nodes(istore), (err0 = ESUCCESS ⊃ as ++ @(n, maxino1, save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize);as), (err0 = ESUCCESS ⊃ (alladrs -- adr1) ++ @(n, maxino1, save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize);alladrs), ok) * P) )(zh) ∧ (err0 = ESUCCESS ∨ ⌊err0⌋ ) ∧ (err0 = ESUCCESS → ¬ zh[r].dirty))

Heuristic unfold applied rule call right

And obtained the following new goals

Proof step 160:
zh[r] = mkznode(r0, zbrar, boolvar, true, m0), adr = adr0, ginval0 = ginval2, gstore = gstore1, gstore0 = gstore2, istore = istore2, istore0 = istore3[n1, indexblock([], [], 0)] [index(n1).lnum, istore3[n1, indexblock([], [], 0)] [index(n1).lnum, istore3[n1, indexblock([], [], 0)][index(n1).lnum] .indlist:= (istore3[n1, indexblock([], [], 0)][index(n1).lnum].indlist + save(mkznode(r0, zbrar, boolvar, true, m0)) ') ] [index(n1).lnum ] .ladrlist:= ( istore3[n1, indexblock([], [], 0)] [index(n1).lnum, istore3[n1, indexblock([], [], 0)][index(n1).lnum] .indlist:= (istore3[n1, indexblock([], [], 0)][index(n1).lnum].indlist + save(mkznode(r0, zbrar, boolvar, true, m0)) ') ] [index(n1).lnum ] .ladrlist + @ (@(index(n1).lnum, maxino1, save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize).pos, @(index(n1).lnum, maxino1, save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize).size) ') ], maxino = maxino2, maxino0 = index(n1).lnum, pstate = index(n1), remove-refsize0(istore2) = istore2, remove-refsize0(gstore1) = gstore1, elems nx ∩ ginval2 = ∅, dom gstore1 ∪ elems nx = dom gstore2 ∪ ginval2, ((btree(rp, r, adr1, height, dirty, ri, nodes(istore3), as, alladrs, ok) * P))(zh), n0 < save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize, btree-sub-clean(r, m0, zh), inv(istore3[n1, indexblock(save(mkznode(r0, zbrar, boolvar, true, m0)) ', @(maxino1, save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize) ', 0)]), inv(istore3[n1, indexblock([], [], 0)]), inv(istore2), inv(istore3), inv(gstore1), inv(gstore2 \ ginval2), refsize-cons(istore3, as0 ∪ as), index(n1).lnum ∈ istore3[n1, indexblock([], [], 0)] [index(n1).lnum, istore3[n1, indexblock([], [], 0)][index(n1).lnum] .indlist:= (istore3[n1, indexblock([], [], 0)][index(n1).lnum].indlist + save(mkznode(r0, zbrar, boolvar, true, m0)) ') ], index(n1).lnum ∈ istore3[n1, indexblock([], [], 0)], m ∈ istore3, r ∈ zh, n0 ≤ LEB_SIZE, as ⊆ dom nodes(istore3), as ⊆ alladrs, alladrs ⊆ dom nodes(istore3), as0 ⊆ dom nodes(istore3), istore2 ⊑ istore3[n1, indexblock(save(mkznode(r0, zbrar, boolvar, true, m0)) ', @(maxino1, save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize) ', 0)], istore2 ⊑ istore3[n1, indexblock([], [], 0)], istore2 ⊑ istore3, height = 0 → as = ∅, index(n1).index? ∨ index(n1).journal? ⊦ ⟪if maxino0 ∈ istore0 then n := istore0[maxino0].ref-size else abort; istore := istore3[n1, indexblock([], [], 0)] [index(n1).lnum, istore3[n1, indexblock([], [], 0)] [index(n1).lnum, istore3[n1, indexblock([], [], 0)][index(n1).lnum] .indlist:= (istore3[n1, indexblock([], [], 0)][index(n1).lnum].indlist + save(mkznode(r0, zbrar, boolvar, true, m0)) ') ] [index(n1).lnum ] .ladrlist:= ( istore3[n1, indexblock([], [], 0)] [index(n1).lnum, istore3[n1, indexblock([], [], 0)][index(n1).lnum] .indlist:= (istore3[n1, indexblock([], [], 0)][index(n1).lnum].indlist + save(mkznode(r0, zbrar, boolvar, true, m0)) ') ] [index(n1).lnum ] .ladrlist + @ (@(index(n1).lnum, maxino1, save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize).pos, @(index(n1).lnum, maxino1, save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize).size) ') ]; apersistence_set_iblock_refsize# (index(n1).lnum, n + @(index(n1).lnum, maxino1, save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize).size, adr0, istore2, ginval2, gstore2, gstore1, nx, maxino2, ginval, index(n1), syn ; istore); err0 := ESUCCESS; if err0 = ESUCCESS then zh[r].dirty := false⟫ ( refsize-cons(istore, as0 ∪ (err0 = ESUCCESS ⊃ as ++ @(n1, maxino1, save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize);as)) ∧ inv(istore) ∧ istore2 ⊑ istore ∧ n1 ∈ istore ∧ istore3 ⊑ istore ∧ r ∈ zh ∧ (err0 = ESUCCESS → ¬ @(n1, maxino1, save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize) ∈ as) ∧ dom nodes(istore) = dom nodes(istore3) ∪ (err0 = ESUCCESS ⊃ ∅ ++ @(n1, maxino1, save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize);∅) ∧ (( btree (rp, r, (err0 = ESUCCESS ⊃ @(n1, maxino1, save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize);adr1), height, err0 ≠ ESUCCESS, ri, nodes(istore), (err0 = ESUCCESS ⊃ as ++ @(n1, maxino1, save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize);as), (err0 = ESUCCESS ⊃ (alladrs -- adr1) ++ @(n1, maxino1, save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize);alladrs), ok) * P) )(zh) ∧ (err0 = ESUCCESS ∨ ⌊err0⌋ ) ∧ (err0 = ESUCCESS → ¬ zh[r].dirty)), dups(nx), adr1 ∈ as, n1 ∈ istore3

Rule argument

pos: right 1

Additional information

Used simplifier rules: apersistence_get_iblock_refsize# (LNUM, ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED ; ; N ) {if LNUM ∈ ISTORE then N := ISTORE[LNUM].ref-size else abort};% ⊦ index(m).lnum = m; (s)% ⊦ istore[n, iblock][n] = iblock; (s)% ⊦ indexblock(indx, lax, m).indlist = indx; (s)% ⊦ [] + indx = indx; (s)%a: ⊦ (indx + indx0) + indx1 = indx + indx0 + indx1; from specification list[index-store]%⊦ indexblock(indx, lax, m).indlist:= indx0 = indexblock(indx0, lax, m); (s)% ⊦ istore[n, iblock][n, iblock0] = istore[n, iblock0]; (s)% ⊦ n ∈ istore[n, iblock]; (s)% ⊦ index(m).index?; (s)