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

# lpt1 = # avol0, # lpt4 = # avol0, keyset(gch1) = gc-heap(lpt1, log3), remove-refsize0(istore2) = istore2, remove-refsize0(gstore2) = gstore2, elems log3 ∩ ns3 = ∅, dom gstore2 ∪ elems log3 = dom gstore1 ∪ ns3, ns3 < # avol0, abs-gstore(avol0, lpt1, gstore1, ns3), abs-istore(avol0, lpt1, istore1), awbuf-inv(avol0, bleb1), bin-heap-inv(gch1, lpt1), buf-ro-rw-mode(pstate0 = readonly, bleb1, lpt1, avol0), bufs-log-only(bleb1, log3, lpt1), flash-lpt-cons(lpt4, istore2, gstore2), freelist-cons(lpt1, log4), inv(istore2), inv(istore1), inv(gstore2), inv(gstore1 \ ns3), log-group-block(log3, lpt1), lpt-free-unref(lpt1), lpt-free-unref(lpt4), lpt-leb-size(lpt1), lpt-leb-size(lpt4), lpt-ram-flash(lpt1, lpt4, log3), synced(avol0), avol ↓ avol0, istore2 ⊑ istore1, ¬ dups(log3), pstate0 = unbuffered → isbuf0, pstate0.index? → pstate0.lnum ∈ istore1, pstate0.journal? → log3 ≠ [] ∧ pstate0.lnum = log3.last ∧ pstate0.lnum ∈ gstore1, pstate0 ≠ unbuffered ∧ pstate0 ≠ readonly → bleb1 = buffered(pstate0.lnum), pstate0 = unbuffered → bleb1 = nobuffer ⊦ [awbuf_get_leb_size#(adr1, m2, log3, avol, lpt4, ns2, nobuffer, false; ; m7); let log1 = log3 in {lpt1 := lpt4; lpt0 := lpt4; persistence_replay_log#(m7; log1, lpt4)}; persistence_replay_lpt#(log3, m7, adr1, m2, log3, lpt1, ns2, nobuffer, false; lpt4, avol); persistence_create_freelist#(lpt4; freelist); persistence_create_gcheap#(log3; lpt4, gch)] ( synced(avol) ∧ lpt-free-unref(replay-lpt(replay-log(lpt0, log3), log3, # lpt0)) ∧ lpt-free-unref(lpt0) ∧ freelist-cons(replay-lpt(replay-log(lpt0, log3), log3, # lpt0), freelist) ∧ bin-heap-inv(gch, lpt4) ∧ keyset(gch) = gc-heap(replay-lpt(replay-log(lpt0, log3), log3, # lpt0), log3) ∧ # lpt4 = # avol ∧ log-group-block(log3, lpt4) ∧ lpt-leb-size(replay-lpt(replay-log(lpt0, log3), log3, # lpt0)) ∧ lpt-leb-size(lpt0) ∧ lpt-ram-flash(lpt4, lpt0, log3) ∧ m7 = LEB_SIZE ∧ awbuf-inv(avol, nobuffer) ∧ # lpt0 = # avol ∧ # avol = # avol0 ∧ lpt1 = lpt0 ∧ id-idx(replay-lpt(replay-log(lpt0, log3), log3, # lpt0), lpt4) → ⟨istore := remove-refsize0(crash(istore1, istore2)), gstore := crash(gstore1, gstore2, ns3, log3); ns0 := ns2; m0 := m2; log0 := log3; adr0 := adr1; apersistence_recover#(; adr4, m5, log6, ns6, adr1, log3, m2, ns2, istore, istore2, ns3, gstore, gstore2; pstate, isbuf0, err1)⟩ ( abs-istore(avol, lpt4, istore) ∧ abs-gstore(avol, lpt4, gstore, ns3) ∧ adr1 = adr4 ∧ m2 = m5 ∧ log3 = log6 ∧ ns3 < # lpt4 ∧ ns2 = ns6 ∧ flash-lpt-cons(lpt0, istore2, gstore2) ∧ pstate = unbuffered ∧ adr0 = adr4 ∧ m0 = m5 ∧ log0 = log6 ∧ ns0 = ns6 ∧ ESUCCESS = err1))

Heuristic unfold applied rule call right

And obtained the following new goals

Proof step 17:
# lpt4 = # avol0, # lpt1 = # avol0, isbuf ↔ false, adr = adr1, bleb = nobuffer, keyset(gch1) = gc-heap(lpt1, log3), log = log3, lpt = lpt4, m = m2, ns = ns2, remove-refsize0(gstore2) = gstore2, remove-refsize0(istore2) = istore2, elems log3 ∩ ns3 = ∅, dom gstore2 ∪ elems log3 = dom gstore1 ∪ ns3, ns3 < # avol0, abs-gstore(avol0, lpt1, gstore1, ns3), abs-istore(avol0, lpt1, istore1), awbuf-inv(avol0, bleb1), bin-heap-inv(gch1, lpt1), buf-ro-rw-mode(pstate0 = readonly, bleb1, lpt1, avol0), bufs-log-only(bleb1, log3, lpt1), flash-lpt-cons(lpt4, istore2, gstore2), freelist-cons(lpt1, log4), inv(gstore1 \ ns3), inv(gstore2), inv(istore1), inv(istore2), log-group-block(log3, lpt1), lpt-free-unref(lpt4), lpt-free-unref(lpt1), lpt-leb-size(lpt4), lpt-leb-size(lpt1), lpt-ram-flash(lpt1, lpt4, log3), synced(avol0), avol ↓ avol0, istore2 ⊑ istore1, pstate0 = unbuffered → bleb1 = nobuffer, pstate0 ≠ unbuffered ∧ pstate0 ≠ readonly → bleb1 = buffered(pstate0.lnum), pstate0.journal? → log3 ≠ [] ∧ pstate0.lnum = log3.last ∧ pstate0.lnum ∈ gstore1, pstate0.index? → pstate0.lnum ∈ istore1, pstate0 = unbuffered → isbuf0 ⊦ [n := LEB_SIZE; let log1 = log3 in {lpt1 := lpt4; lpt0 := lpt4; persistence_replay_log#(n; log1, lpt4)}; persistence_replay_lpt#(log3, n, adr1, m2, log3, lpt1, ns2, nobuffer, false; lpt4, avol); persistence_create_freelist#(lpt4; freelist); persistence_create_gcheap#(log3; lpt4, gch)] ( synced(avol) ∧ lpt-free-unref(replay-lpt(replay-log(lpt0, log3), log3, # lpt0)) ∧ lpt-free-unref(lpt0) ∧ freelist-cons(replay-lpt(replay-log(lpt0, log3), log3, # lpt0), freelist) ∧ bin-heap-inv(gch, lpt4) ∧ keyset(gch) = gc-heap(replay-lpt(replay-log(lpt0, log3), log3, # lpt0), log3) ∧ # lpt4 = # avol ∧ log-group-block(log3, lpt4) ∧ lpt-leb-size(replay-lpt(replay-log(lpt0, log3), log3, # lpt0)) ∧ lpt-leb-size(lpt0) ∧ lpt-ram-flash(lpt4, lpt0, log3) ∧ n = LEB_SIZE ∧ awbuf-inv(avol, nobuffer) ∧ # lpt0 = # avol ∧ # avol = # avol0 ∧ lpt1 = lpt0 ∧ id-idx(replay-lpt(replay-log(lpt0, log3), log3, # lpt0), lpt4) → ⟨istore := remove-refsize0(crash(istore1, istore2)), gstore := crash(gstore1, gstore2, ns3, log3); ns0 := ns2; m0 := m2; log0 := log3; adr0 := adr1; apersistence_recover#(; adr4, m5, log6, ns6, adr1, log3, m2, ns2, istore, istore2, ns3, gstore, gstore2; pstate, isbuf0, err1)⟩ ( abs-istore(avol, lpt4, istore) ∧ abs-gstore(avol, lpt4, gstore, ns3) ∧ adr1 = adr4 ∧ m2 = m5 ∧ log3 = log6 ∧ ns3 < # lpt4 ∧ ns2 = ns6 ∧ flash-lpt-cons(lpt0, istore2, gstore2) ∧ pstate = unbuffered ∧ adr0 = adr4 ∧ m0 = m5 ∧ log0 = log6 ∧ ns0 = ns6 ∧ ESUCCESS = err1)), dups(log3)

Rule argument

pos: right 1

Additional information

Used simplifier rules: awbuf_get_leb_size# (WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, WBUFLEB, AROFS; ; N) {N := LEB_SIZE};