[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 4 from proof recovery (previous step)

syn ↔ syn1, adr = adr2, adr0 = adr1, ginval = ginval4, ginval0 = ginval9, ginval1 = ginval5, ginval4 = ginval2, ginval5 = ginval6, ginval9 = ginval3, gstore = gstore2, gstore0 = gstore7, gstore2 = gstore1, gstore7 = crash(gstore4, gstore1, ginval3, nx1), istore = istore1, istore0 = istore3, istore3 = remove-refsize0(crash(istore2, istore1)), maxino = maxino1, maxino0 = maxino2, maxino2 = maxino3, nx = nx5, nx0 = nx2, nx2 = nx3, nx5 = nx1, pstate = pstate0, remove-refsize0(istore1) = istore1, remove-refsize0(gstore1) = gstore1, rp = rp0, elems nx1 ∩ ginval3 = ∅, dom gstore1 ∪ elems nx1 = dom gstore4 ∪ ginval3, btree-inv(rp1, adr2, istore2, istore1, zh, ri, fi3), btree-inv(rp1, adr2, istore2, istore1, zh, fi, fi0), inv(istore1), inv(istore2), inv(gstore1), inv(gstore4 \ ginval3), ri-inj(fi0), ri-inj(fi), istore1 ⊑ istore2, pstate1.index? → pstate1.lnum ∈ istore2, pstate1.journal? → nx1 ≠ [] ∧ pstate1.lnum = nx1.last ∧ pstate1.lnum ∈ gstore4 ⊦ ⟪apersistence_recover#(; adr0, maxino0, nx0, ginval1, adr, istore0, istore, ginval0, gstore0, gstore, nx, maxino, ginval, pstate, syn; err); rp := null⟫ ( ( err = ESUCCESS → (∃ fi3, syn0. ⟨gstore3 := crash(gstore4, gstore1, ginval3, nx1); index+persistence_recover#(; maxino3, nx3, ginval6, fi3, fi0, ginval3, gstore3, gstore1, nx1, maxino1, ginval2, syn0; err0)⟩ ( ginval3 = ginval0 ∧ gstore3 = gstore0 ∧ gstore1 = gstore ∧ nx1 = nx ∧ maxino1 = maxino ∧ ginval2 = ginval ∧ btree-inv(rp, adr, istore0, istore, zh0, fi3, fi0) ∧ (syn0 ↔ syn) ∧ maxino0 = maxino3 ∧ nx0 = nx3 ∧ ginval1 = ginval6 ∧ ESUCCESS = err0))) ∧ ( err ≠ ESUCCESS → (∀ fi, fi0, ginval, gstore, gstore0, nx, maxino, ginval0, syn. ⟨index+persistence_recover#(; maxino3, nx3, ginval6, fi1, fi2, ginval7, gstore5, gstore6, nx4, maxino4, ginval8, syn2; err0)⟩ ( fi = fi1 ∧ fi0 = fi2 ∧ ginval = ginval7 ∧ gstore = gstore5 ∧ gstore0 = gstore6 ∧ nx = nx4 ∧ maxino = maxino4 ∧ ginval0 = ginval8 ∧ (syn ↔ syn2) ∧ maxino0 = maxino3 ∧ nx0 = nx3 ∧ ginval1 = ginval6 ∧ err = err0)))), dups(nx1)

User applied rule insert program lemma

And obtained the following new goals

Proof step 5:
adr = adr0 ∧ istore = remove-refsize0(crash(istore0, istore1)) ∧ istore2 = istore1 ∧ ginval = ginval0 ∧ gstore = crash(gstore0, gstore1, ginval0, nx) ∧ gstore2 = gstore1 ∧ nx0 = nx ∧ maxino = maxino0 ∧ ginval1 = ginval2, syn, inv-journal(nx, gstore0, gstore1, ginval0), inv-index(istore0, istore1), inv-state(pstate, nx, gstore0, istore0, syn) ⊦ ⟪apersistence_recover#(; adr1, maxino1, nx1, ginval3, adr, istore, istore2, ginval, gstore, gstore2, nx0, maxino, ginval1, pstate0, syn0; err)⟫ (err = ESUCCESS → syn0 ∧ inv-journal(nx0, gstore, gstore2, ginval) ∧ inv-index(istore, istore2) ∧ inv-state(pstate0, nx0, gstore, istore, syn0))
Proof step 6:
syn ↔ syn1, syn3 ↔ true, adr = adr2, adr = adr, adr0 = adr1, adr3 = adr, ginval = ginval4, ginval = ginval2, ginval0 = ginval9, ginval0 = ginval0, ginval1 = ginval5, ginval10 = ginval0, ginval11 = ginval2, ginval4 = ginval2, ginval5 = ginval6, ginval9 = ginval3, gstore = gstore2, gstore = gstore1, gstore0 = gstore7, gstore0 = crash(gstore4, gstore1, ginval0, nx), gstore2 = gstore1, gstore7 = crash(gstore4, gstore1, ginval3, nx1), gstore8 = gstore4, gstore9 = gstore1, istore = istore1, istore0 = istore3, istore0 = remove-refsize0(crash(istore2, istore1)), istore3 = remove-refsize0(crash(istore2, istore1)), istore4 = istore2, istore5 = istore1, maxino = maxino1, maxino = maxino, maxino0 = maxino2, maxino2 = maxino3, maxino5 = maxino, nx = nx5, nx = nx, nx0 = nx2, nx2 = nx3, nx5 = nx1, nx6 = nx, pstate = pstate0, pstate2 = pstate1, remove-refsize0(gstore1) = gstore1, remove-refsize0(istore1) = istore1, rp = rp0, elems nx1 ∩ ginval3 = ∅, dom gstore1 ∪ elems nx1 = dom gstore4 ∪ ginval3, btree-inv(rp1, adr2, istore2, istore1, zh, fi, fi0), btree-inv(rp1, adr2, istore2, istore1, zh, ri, fi3), inv(gstore4 \ ginval3), inv(gstore1), inv(istore2), inv(istore1), inv-index(istore2, istore1), inv-journal(nx, gstore4, gstore1, ginval0), inv-state(pstate1, nx, gstore4, istore2, true), ri-inj(fi), ri-inj(fi0), istore1 ⊑ istore2, pstate1.journal? → nx1 ≠ [] ∧ pstate1.lnum = nx1.last ∧ pstate1.lnum ∈ gstore4, pstate1.index? → pstate1.lnum ∈ istore2 ⊦ [apersistence_recover#(; adr0, maxino0, nx0, ginval1, adr, istore0, istore, ginval0, gstore0, gstore, nx, maxino, ginval, pstate, syn; err)] ( (err = ESUCCESS → syn ∧ inv-journal(nx, gstore0, gstore, ginval0) ∧ inv-index(istore0, istore) ∧ inv-state(pstate, nx, gstore0, istore0, syn)) → ⟪rp := null⟫ ( ( err = ESUCCESS → (∃ fi3, syn0. ⟨gstore3 := crash(gstore4, gstore1, ginval3, nx1); index+persistence_recover#(; maxino3, nx3, ginval6, fi3, fi0, ginval3, gstore3, gstore1, nx1, maxino1, ginval2, syn0; err0)⟩ ( ginval3 = ginval0 ∧ gstore3 = gstore0 ∧ gstore1 = gstore ∧ nx1 = nx ∧ maxino1 = maxino ∧ ginval2 = ginval ∧ btree-inv(rp, adr, istore0, istore, zh0, fi3, fi0) ∧ (syn0 ↔ syn) ∧ maxino0 = maxino3 ∧ nx0 = nx3 ∧ ginval1 = ginval6 ∧ ESUCCESS = err0))) ∧ ( err ≠ ESUCCESS → (∀ fi, fi0, ginval, gstore, gstore0, nx, maxino, ginval0, syn. ⟨index+persistence_recover#(; maxino3, nx3, ginval6, fi1, fi2, ginval7, gstore5, gstore6, nx4, maxino4, ginval8, syn2; err0)⟩ ( fi = fi1 ∧ fi0 = fi2 ∧ ginval = ginval7 ∧ gstore = gstore5 ∧ gstore0 = gstore6 ∧ nx = nx4 ∧ maxino = maxino4 ∧ ginval0 = ginval8 ∧ (syn ↔ syn2) ∧ maxino0 = maxino3 ∧ nx0 = nx3 ∧ ginval1 = ginval6 ∧ err = err0))))), dups(nx1)

Rule argument

spec: apersistence-asm name: inv-recovery seq: adr = adr0 ∧ istore = remove-refsize0(crash(istore0, istore1)) ∧ istore2 = istore1 ∧ ginval = ginval0 ∧ gstore = crash(gstore0, gstore1, ginval0, nx) ∧ gstore2 = gstore1 ∧ nx0 = nx ∧ maxino = maxino0 ∧ ginval1 = ginval2, syn, inv-journal(nx, gstore0, gstore1, ginval0), inv-index(istore0, istore1), inv-state(pstate, nx, gstore0, istore0, syn) ⊦ ⟪apersistence_recover# (; adr1, maxino1, nx1, ginval3, adr, istore, istore2, ginval, gstore, gstore2, nx0, maxino, ginval1, pstate0, syn0 ; err)⟫ ( err = ESUCCESS → syn0 ∧ inv-journal(nx0, gstore, gstore2, ginval) ∧ inv-index(istore, istore2) ∧ inv-state(pstate0, nx0, gstore, istore, syn0)) subst: [syn0, pstate0, ginval1, maxino, nx0, gstore2, gstore, ginval, istore2, istore, adr, ginval3, nx1, maxino1, adr1, err, adr0, istore0, istore1, ginval0, gstore0, gstore1, nx, maxino0, ginval2, syn, pstate] → [syn, pstate, ginval, maxino, nx, gstore, gstore0, ginval0, istore, istore0, adr, ginval1, nx0, maxino0, adr0, err, adr, istore2, istore1, ginval0, gstore4, gstore1, nx, maxino, ginval2, true, pstate1] 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)