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

istore4[m2] = indexblock(indx, lax0, m), zh[r] = mkznode(r0, zbrar, boolvar, true, m0), istore0 = istore4 [m2, indexblock(indx + save(mkznode(r0, zbrar, boolvar, true, m0)) ', lax0 + @(m3, save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize) ', 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 (istore4 [m2, indexblock(indx + save(mkznode(r0, zbrar, boolvar, true, m0)) ', lax0 + @(m3, save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize) ', m) ]), inv(istore2), inv(istore4), inv(gstore1), inv(gstore2 \ ginval2), inv(indexblock(indx, lax0, m)), 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)) ', lax0 + @(m3, save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize) ', m) ], ¬ dups(nx), ¬ @(m2, m3, save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize) ∈ istore2, ¬ @(m2, m3, save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize) ∈ istore4, ¬ adr1 ∈ as, height = 0 → as = ∅ ⊦ ⟪apersistence_set_iblock_refsize# (index(m2).lnum, m + save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize, adr0, istore2, ginval2, gstore2, gstore1, nx, maxino1, ginval, index(m2), syn ; istore0); err := ESUCCESS; if err = ESUCCESS then zh[r].dirty := false⟫ ( refsize-cons(istore0, as0 ∪ (err = ESUCCESS ⊃ as ++ @(m2, m3, save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize);as)) ∧ inv(istore0) ∧ istore2 ⊑ istore0 ∧ m2 ∈ istore0 ∧ istore4 ⊑ istore0 ∧ r ∈ zh ∧ (err = ESUCCESS → ¬ @(m2, m3, save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize) ∈ as) ∧ dom nodes(istore0) = 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(istore0), (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))

User applied rule insert program lemma

And obtained the following new goals

Proof step 243:
inv-journal(nx, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, nx, gstore, istore, syn), maxino ∈ istore ⊦ ⟪apersistence_set_iblock_refsize#(maxino, n, adr, istore0, ginval, gstore, gstore0, nx, maxino0, ginval0, pstate, syn; istore)⟫ (inv-index(istore, istore0) ∧ inv-state(pstate, nx, gstore, istore, syn))
Proof step 244:
syn0 ↔ syn, zh[r] = mkznode(r0, zbrar, boolvar, true, m0), istore4[m2] = indexblock(indx, lax0, m), adr2 = adr0, ginval1 = ginval2, ginval3 = ginval, gstore3 = gstore2, gstore4 = gstore1, istore0 = istore4 [m2, indexblock(indx + save(mkznode(r0, zbrar, boolvar, true, m0)) ', lax0 + @(m3, save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize) ', m) ], istore1 = istore2, maxino2 = index(m2).lnum, maxino3 = maxino1, n0 = m + save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize, nx0 = nx, pstate0 = index(m2), 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(indexblock(indx, lax0, m)), inv(gstore2 \ ginval2), inv(gstore1), inv(istore4), inv(istore2), inv (istore4 [m2, indexblock(indx + save(mkznode(r0, zbrar, boolvar, true, m0)) ', lax0 + @(m3, save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize) ', m) ]), inv-index(istore0, istore2), inv-journal(nx, gstore2, gstore1, ginval2), inv-state(index(m2), nx, gstore2, istore0, syn), refsize-cons(istore4, as0 ∪ as), r ∈ zh, m2 ∈ istore4, index(m2).lnum ∈ istore0, 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)) ', lax0 + @(m3, save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize) ', m) ], istore2 ⊑ istore4, height = 0 → as = ∅ ⊦ [apersistence_set_iblock_refsize# (index(m2).lnum, m + save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize, adr0, istore2, ginval2, gstore2, gstore1, nx, maxino1, ginval, index(m2), syn ; istore0)] ( inv-index(istore0, istore1) ∧ inv-state(pstate0, nx0, gstore3, istore0, syn0) → ⟪err := ESUCCESS; if err = ESUCCESS then zh[r].dirty := false⟫ ( refsize-cons(istore0, as0 ∪ (err = ESUCCESS ⊃ as ++ @(m2, m3, save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize);as)) ∧ inv(istore0) ∧ istore2 ⊑ istore0 ∧ m2 ∈ istore0 ∧ istore4 ⊑ istore0 ∧ r ∈ zh ∧ (err = ESUCCESS → ¬ @(m2, m3, save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize) ∈ as) ∧ dom nodes(istore0) = 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(istore0), (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), @(m2, m3, save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize) ∈ istore2, @(m2, m3, save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize) ∈ istore4, adr1 ∈ as

Rule argument

spec: apersistence-asm name: inv-set-iblock-refsize seq: inv-journal(nx, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, nx, gstore, istore, syn), maxino ∈ istore ⊦ ⟪apersistence_set_iblock_refsize# (maxino, n, adr, istore0, ginval, gstore, gstore0, nx, maxino0, ginval0, pstate, syn ; istore)⟫ ( inv-index(istore, istore0) ∧ inv-state(pstate, nx, gstore, istore, syn)) subst: [syn, pstate, ginval0, maxino0, nx, gstore0, gstore, ginval, istore0, adr, n, maxino, istore] → [syn, index(m2), ginval, maxino1, nx, gstore1, gstore2, ginval2, istore2, adr0, m + save(mkznode(r0, zbrar, boolvar, true, m0)).flashsize, index(m2).lnum, istore0] flags: <all paths>

Additional information

Used simplifier rules: ⊦ inv-journal(nx, gstore, gstore0, ginval) ↔ inv(gstore \ ginval) ∧ inv(gstore0) ∧ elems nx ∩ ginval = ∅ ∧ ¬ dups(nx) ∧ dom gstore0 ∪ elems nx = dom gstore ∪ ginval ∧ remove-refsize0(gstore0) = gstore0; (s)%⊦ inv-index(istore, istore0) ↔ inv(istore) ∧ inv(istore0) ∧ istore0 ⊑ istore ∧ remove-refsize0(istore0) = istore0; (s)%⊦ inv-state(pstate, nx, gstore, istore, syn) ↔ ( pstate.journal? → nx ≠ [] ∧ pstate.lnum = nx.last ∧ pstate.lnum ∈ gstore) ∧ (pstate.index? → pstate.lnum ∈ istore) ∧ (pstate = unbuffered → syn); (s)% ⊦ ¬ index(m).journal?; (s)% ⊦ index(m).index?; (s)% ⊦ index(m).lnum = m; (s)% ⊦ n ∈ istore[n, iblock]; (s)% ⊦ unbuffered ≠ index(m); (s)