[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 226 from proof inv-io-save (previous step)

zh[r] = mkznode(r0, zbrar, boolvar, true, m0), adr = @(pstate.lnum, maxino1, ind.flashsize), adr2 = adr1, err0 = ESUCCESS, err0 = err, err1 = err0, ginval0 = ginval2, gstore = gstore1, gstore0 = gstore2, ind = save(mkznode(r0, zbrar, boolvar, true, m0)), istore = istore4, istore0 = istore2, istore1 = istore4, istore3 = istore[pstate.lnum, istore[pstate.lnum].indlist:= (istore[pstate.lnum].indlist + ind)] [pstate.lnum, istore[pstate.lnum, istore[pstate.lnum].indlist:= (istore[pstate.lnum].indlist + ind)][pstate.lnum] .ladrlist:= (istore[pstate.lnum, istore[pstate.lnum].indlist:= (istore[pstate.lnum].indlist + ind)][pstate.lnum].ladrlist + @(adr.pos, adr.size)) ], maxino = 0, pstate = index(m), 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(istore4), as, alladrs, ok) * P))(zh), btree-sub-clean(r, m0, zh), inv(istore2), inv(istore4), inv(gstore1), inv(gstore2 \ ginval2), inv (istore[pstate.lnum, istore[pstate.lnum].indlist:= (istore[pstate.lnum].indlist + ind)] [pstate.lnum, istore[pstate.lnum, istore[pstate.lnum].indlist:= (istore[pstate.lnum].indlist + ind)][pstate.lnum] .ladrlist:= (istore[pstate.lnum, istore[pstate.lnum].indlist:= (istore[pstate.lnum].indlist + ind)][pstate.lnum].ladrlist + @(adr.pos, adr.size)) ]), refsize-cons(istore4, as0 ∪ as), m ∈ istore4, r ∈ zh, pstate.lnum ∈ istore[pstate.lnum, istore[pstate.lnum].indlist:= (istore[pstate.lnum].indlist + ind)], pstate.lnum ∈ istore, n ≤ LEB_SIZE, save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize ≤ n, save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize ≤ LEB_SIZE, as ⊆ alladrs, alladrs ⊆ dom nodes(istore4), as0 ⊆ dom nodes(istore4), as ⊆ dom nodes(istore4), istore2 ⊑ istore4, istore2 ⊑ istore[pstate.lnum, istore[pstate.lnum].indlist:= (istore[pstate.lnum].indlist + ind)] [pstate.lnum, istore[pstate.lnum, istore[pstate.lnum].indlist:= (istore[pstate.lnum].indlist + ind)][pstate.lnum] .ladrlist:= (istore[pstate.lnum, istore[pstate.lnum].indlist:= (istore[pstate.lnum].indlist + ind)][pstate.lnum].ladrlist + @(adr.pos, adr.size)) ], height = 0 → as = ∅, pstate = unbuffered → syn, pstate.index? → pstate.lnum ∈ istore[pstate.lnum, istore[pstate.lnum].indlist:= (istore[pstate.lnum].indlist + ind)] [pstate.lnum, istore[pstate.lnum, istore[pstate.lnum].indlist:= (istore[pstate.lnum].indlist + ind)][pstate.lnum] .ladrlist:= (istore[pstate.lnum, istore[pstate.lnum].indlist:= (istore[pstate.lnum].indlist + ind)][pstate.lnum].ladrlist + @(adr.pos, adr.size)) ], pstate.journal? → nx ≠ [] ∧ pstate.lnum = nx.last ∧ pstate.lnum ∈ gstore2, ¬ @(pstate.lnum, maxino1, ind.flashsize) ∈ istore ∧ err = ESUCCESS ∨ ⌊err⌋ , pstate.index? ∨ pstate.journal? ⊦ ⟪apersistence_get_iblock_refsize#(adr.lnum, adr0, istore3, istore2, ginval2, gstore2, gstore1, nx, maxino0, ginval, pstate, syn; ; maxino); apersistence_set_iblock_refsize# (adr.lnum, maxino + adr.size, adr0, istore2, ginval2, gstore2, gstore1, nx, maxino0, ginval, pstate, syn; istore3); if err1 = ESUCCESS then zh[r].dirty := false⟫ ( refsize-cons(istore3, as0 ∪ (err1 = ESUCCESS ⊃ as ++ adr;as)) ∧ inv(istore3) ∧ istore2 ⊑ istore3 ∧ (pstate.journal? → nx ≠ [] ∧ pstate.lnum = nx.last ∧ pstate.lnum ∈ gstore2) ∧ (pstate.index? → pstate.lnum ∈ istore3) ∧ (pstate = unbuffered → syn) ∧ istore1 ⊑ istore3 ∧ r ∈ zh ∧ (err1 = ESUCCESS → ¬ adr ∈ as) ∧ dom nodes(istore3) = dom nodes(istore1) ∪ (err1 = ESUCCESS ⊃ ∅ ++ adr;∅) ∧ (err1 = ESUCCESS → ¬ adr ∈ istore1) ∧ (( btree (rp, r, (err1 = ESUCCESS ⊃ adr;adr1), height, err1 ≠ ESUCCESS, ri, nodes(istore3), (err1 = ESUCCESS ⊃ as ++ adr;as), (err1 = ESUCCESS ⊃ (alladrs -- adr1) ++ adr;alladrs), ok) * P) )(zh) ∧ (err1 = ESUCCESS ∨ ⌊err1⌋ ) ∧ (err1 = ESUCCESS → pstate.index? ∧ ¬ zh[r].dirty)), dups(nx), adr1 ∈ as

Heuristic simplifier applied rule simplifier

And obtained the following new goals

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

Rule argument

Additional information

Used simplifier rules: prefix-notin-fwd: ⊦ ¬ adr ∈ istore ∧ istore0 ⊑ istore → ¬ adr ∈ istore0; (forward) from specification ablock-store-inv[index-store]%sub-trans: ⊦ as ⊆ as0 ∧ as0 ⊆ as1 → as ⊆ as1; (forward) from specification set-basic[node-store]% ⊦ @(m, m0, m1).lnum = m; (s)% ⊦ unbuffered ≠ index(m); (s)% ⊦ ¬ index(m).journal?; (s)% ⊦ ¬ ⌊ESUCCESS⌋ ; (s)% ⊦ index(m).index?; (s)% ⊦ n ∈ istore[n, iblock]; (s)% ⊦ istore[n, iblock][n, iblock0] = istore[n, iblock0]; (s)% ⊦ lax + ladr = lax + ladr '; (s)% ⊦ @(m, m0, m1).size = m1; (s)% ⊦ @(m, m0, m1).pos = m0; (s)% ⊦ (iblock.indlist:= indx).ladrlist = iblock.ladrlist; (s)% ⊦ istore[n, iblock][n] = iblock; (s)% ⊦ indx + ind = indx + ind '; (s)% ⊦ index(m).lnum = m; (s)