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

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

Heuristic elimination applied rule insert elim lemma

And obtained the following new goals

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

Rule argument

spec: ablock, inst: index-store name: elim seq: ⊦ (indx = iblock.indlist ∧ lax = iblock.ladrlist) ∧ m = iblock.ref-size ↔ iblock = indexblock(indx, lax, m) subst: [iblock, indx, lax, m] → [istore4[index(m2).lnum], indx0, lax0, m]

Additional information

Used simplifier rules: ⊦ (indx = iblock.indlist ∧ lax = iblock.ladrlist) ∧ m = iblock.ref-size ↔ iblock = indexblock(indx, lax, m); (elim) Used terms: istore4[index(m2).lnum], indx0, lax0, m