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

# lpt1 = # avol0, # lpt0 = # avol0, adr0 = adr1, adr3 = adr4, keyset(gch) = gc-heap(lpt1, log1), log0 = log1, log5 = log6, m0 = m1, m4 = m5, ns1 = ns2, ns5 = ns6, remove-refsize0(gstore2) = gstore2, remove-refsize0(istore2) = istore2, elems log1 ∩ ns3 = ∅, dom gstore2 ∪ elems log1 = dom gstore1 ∪ ns3, ns3 < # avol0, abs-gstore(avol0, lpt1, gstore1, ns3), abs-istore(avol0, lpt1, istore1), awbuf-inv(avol0, bleb), bin-heap-inv(gch, lpt1), buf-ro-rw-mode(pstate0 = readonly, bleb, lpt1, avol0), bufs-log-only(bleb, log1, lpt1), flash-lpt-cons(lpt0, istore2, gstore2), freelist-cons(lpt1, log4), inv(gstore1 \ ns3), inv(gstore2), inv(istore1), inv(istore2), log-group-block(log1, lpt1), lpt-free-unref(lpt1), lpt-free-unref(lpt0), lpt-leb-size(lpt1), lpt-leb-size(lpt0), lpt-ram-flash(lpt1, lpt0, log1), synced(avol0), avol ↓ avol0, istore2 ⊑ istore1, ¬ dups(log1), pstate0 = unbuffered → bleb = nobuffer, pstate0 ≠ unbuffered ∧ pstate0 ≠ readonly → bleb = buffered(pstate0.lnum), pstate0.journal? → log1 ≠ [] ∧ pstate0.lnum = log1.last ∧ pstate0.lnum ∈ gstore1, pstate0.index? → pstate0.lnum ∈ istore1, pstate0 = unbuffered → isbuf0 ⊦ ⟪persistence_recover#(; adr3, m4, log5, ns5, log7, lpt2, freelist, gch0, m6, adr0, m0, log0, avol, lpt0, ns1, bleb0, isbuf2; err)⟫ ( ( err = ESUCCESS → ⟨istore := remove-refsize0(crash(istore1, istore2)), gstore := crash(gstore1, gstore2, ns3, log1); apersistence_recover#(; adr4, m5, log6, ns6, adr1, log1, m1, ns2, istore, istore2, ns3, gstore, gstore2; pstate, isbuf, err0)⟩ ( abs-istore(avol, lpt2, istore) ∧ abs-gstore(avol, lpt2, gstore, ns3) ∧ adr1 = adr0 ∧ m1 = m0 ∧ log1 = log7 ∧ ns3 < # lpt2 ∧ ns2 = ns1 ∧ flash-lpt-cons(lpt0, istore2, gstore2) ∧ (isbuf → synced(avol)) ∧ (pstate = unbuffered → bleb0 = nobuffer) ∧ (pstate = readonly ↔ isbuf2) ∧ (pstate ≠ unbuffered ∧ pstate ≠ readonly → bleb0 = buffered(pstate.lnum)) ∧ adr3 = adr4 ∧ m4 = m5 ∧ log5 = log6 ∧ ns5 = ns6 ∧ ESUCCESS = err0)) ∧ ( err ≠ ESUCCESS → (∀ adr, istore, istore0, ns, gstore, gstore0, log, m, ns0, pstate, isbuf. ⟨apersistence_recover# (; adr4, m5, log6, ns6, adr5, log8, maxino0, ns7, istore3, istore4, ginval0, gstore3, gstore4; pstate1, isbuf3, err0)⟩ ( adr = adr5 ∧ istore = istore3 ∧ istore0 = istore4 ∧ ns = ginval0 ∧ gstore = gstore3 ∧ gstore0 = gstore4 ∧ log = log8 ∧ m = maxino0 ∧ ns0 = ns7 ∧ pstate = pstate1 ∧ (isbuf ↔ isbuf3) ∧ adr3 = adr4 ∧ m4 = m5 ∧ log5 = log6 ∧ ns5 = ns6 ∧ err = err0))))

User applied rule insert program lemma

And obtained the following new goals

Rule argument

spec: persistence-asm name: inv-recover seq: adr = adr0, m = m0, log = log0, lpt = lpt0, avol ↓ avol0, ns = ns0, synced(avol0), lpt-free-unref(lpt1), lpt-free-unref(lpt0), freelist-cons(lpt1, log1), log2 = log0, bin-heap-inv(gch, lpt1), keyset(gch) = gc-heap(lpt1, log2), bufs-log-only(bleb, log2, lpt1), # lpt1 = # avol0, ¬ dups(log2), log-group-block(log2, lpt1), buf-ro-rw-mode(isbuf, bleb, lpt1, avol0), lpt-leb-size(lpt1), lpt-leb-size(lpt0), lpt-ram-flash(lpt1, lpt0, log2), m1 = LEB_SIZE, awbuf-inv(avol0, bleb), # lpt0 = # avol0 ⊦ ⟪persistence_recover# (; adr1, m2, log3, ns1, log4, lpt2, freelist, gch0, m3, adr, m, log, avol, lpt, ns, bleb0, isbuf0 ; err)⟫ ( ( err = ESUCCESS → synced(avol) ∧ lpt-free-unref(lpt2) ∧ lpt-free-unref(lpt) ∧ freelist-cons(lpt2, freelist) ∧ log4 = log ∧ bin-heap-inv(gch0, lpt2) ∧ keyset(gch0) = gc-heap(lpt2, log4) ∧ bufs-log-only(bleb0, log4, lpt2) ∧ # lpt2 = # avol ∧ ¬ dups(log4) ∧ log-group-block(log4, lpt2) ∧ buf-ro-rw-mode(isbuf0, bleb0, lpt2, avol) ∧ lpt-leb-size(lpt2) ∧ lpt-leb-size(lpt) ∧ lpt-ram-flash(lpt2, lpt, log4) ∧ m3 = LEB_SIZE ∧ awbuf-inv(avol, bleb0) ∧ # lpt = # avol) ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ ( err = ESUCCESS → # avol = # avol0 ∧ adr1 = adr ∧ adr = adr0 ∧ m2 = m ∧ m = m0 ∧ log3 = log ∧ log = log0 ∧ ns1 = ns ∧ ns = ns0 ∧ lpt = lpt0 ∧ bleb0 = nobuffer ∧ id-idx (replay-lpt(replay-log(lpt, log), log, # lpt), lpt2))) subst: [isbuf0, bleb0, ns, lpt, avol, log, m, adr, m3, gch0, freelist, lpt2, log4, ns1, log3, m2, adr1, err, avol0, lpt1, log1, log2, gch, bleb, isbuf, m1, adr0, m0, log0, lpt0, ns0] → [isbuf2, bleb0, ns1, lpt0, avol, log0, m0, adr0, m6, gch0, freelist, lpt2, log7, ns5, log5, m4, adr3, err, avol0, lpt1, log4, log1, gch, bleb, pstate0 = readonly, LEB_SIZE, adr0, m0, log0, lpt0, ns1] flags: List([[1,0,0]])

Additional information