| # lpt4 = # avol0, # lpt1 = # avol0, isbuf ↔ isbuf2, adr = adr2, adr0 = adr3, adr2 = adr1, adr3 = adr4, bleb = bleb0, gch = gch0, keyset(gch1) = gc-heap(lpt1, log3), log = log3, log0 = log1, log1 = log5, log2 = log3, log5 = log6, log9 = log7, lpt = lpt4, lpt0 = lpt2, lpt3 = lpt4, m = m3, m0 = m1, m1 = m4, m3 = m2, m4 = m5, m7 = m6, ns = ns1, ns0 = ns5, ns1 = ns2, ns5 = ns6, 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 ⊦ [choose err0 with ⌊err0⌋ ∨ err0 = ESUCCESS in err := err0; if err = ESUCCESS then bleb := nobuffer, isbuf := false, adr0 := adr, m0 := m, log0 := log, lpt0 := lpt, ns0 := ns else avol := ?, bleb := ?, isbuf := ?, adr := ?, m := ?, log := ?, lpt := ?, adr0 := ?, m0 := ?, log0 := ?, lpt0 := ?, ns0 := ?, ns := ?; log9 := log0; if err ≠ ESUCCESS then debug#("persistence: wbuf recover failed") else {awbuf_get_leb_size#(adr, m, log, avol, lpt, ns, bleb, isbuf; ; m7); let log1 = log9 in persistence_replay_log#(m7; log1, lpt0); persistence_replay_lpt#(log9, m7, adr, m, log, lpt, ns, bleb, isbuf; lpt0, avol); persistence_create_freelist#(lpt0; freelist); persistence_create_gcheap#(log9; lpt0, gch)}] ( ( err = ESUCCESS → synced(avol) ∧ lpt-free-unref(lpt0) ∧ lpt-free-unref(lpt) ∧ freelist-cons(lpt0, freelist) ∧ log9 = log ∧ bin-heap-inv(gch, lpt0) ∧ keyset(gch) = gc-heap(lpt0, log) ∧ bufs-log-only(bleb, log, lpt0) ∧ # lpt0 = # avol ∧ ¬ dups(log) ∧ log-group-block(log, lpt0) ∧ buf-ro-rw-mode(isbuf, bleb, lpt0, avol) ∧ lpt-leb-size(lpt0) ∧ lpt-leb-size(lpt) ∧ lpt-ram-flash(lpt0, lpt, log) ∧ m7 = LEB_SIZE ∧ awbuf-inv(avol, bleb) ∧ # lpt = # avol) ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ ( err = ESUCCESS → # avol = # avol0 ∧ adr0 = adr1 ∧ adr = adr1 ∧ m0 = m2 ∧ m = m2 ∧ log0 = log2 ∧ log = log2 ∧ ns0 = ns2 ∧ ns = ns2 ∧ lpt = lpt3 ∧ bleb = nobuffer ∧ id-idx(replay-lpt(replay-log(lpt3, log2), log2, # lpt3), lpt0)) → ( err = ESUCCESS → ⟨istore := remove-refsize0(crash(istore1, istore2)), gstore := crash(gstore1, gstore2, ns3, log2); apersistence_recover#(; adr4, m5, log6, ns6, adr1, log2, m2, ns2, istore, istore2, ns3, gstore, gstore2; pstate, isbuf0, err0)⟩ ( abs-istore(avol, lpt0, istore) ∧ abs-gstore(avol, lpt0, gstore, ns3) ∧ adr1 = adr ∧ m2 = m ∧ log2 = log9 ∧ ns3 < # lpt0 ∧ ns2 = ns ∧ flash-lpt-cons(lpt, istore2, gstore2) ∧ (isbuf0 → synced(avol)) ∧ (pstate = unbuffered → bleb = nobuffer) ∧ (pstate = readonly ↔ isbuf) ∧ (pstate ≠ unbuffered ∧ pstate ≠ readonly → bleb = buffered(pstate.lnum)) ∧ adr0 = adr4 ∧ m0 = m5 ∧ log0 = log6 ∧ ns0 = ns6 ∧ ESUCCESS = err0)) ∧ ( err ≠ ESUCCESS → (∀ adr, istore, istore0, ns, gstore, gstore0, log, m, ns1, 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 ∧ ns1 = ns7 ∧ pstate = pstate1 ∧ (isbuf ↔ isbuf3) ∧ adr0 = adr4 ∧ m0 = m5 ∧ log0 = log6 ∧ ns0 = ns6 ∧ err = err0)))), dups(log3) |
# lpt1 = # avol0, # lpt4 = # avol0, isbuf ↔ isbuf2, adr = adr2, adr0 = adr3, adr2 = adr1, adr3 = adr4, bleb = bleb0, gch = gch0, keyset(gch1) = gc-heap(lpt1, log3), log = log3, log0 = log1, log1 = log5, log2 = log3, log5 = log6, log9 = log7, lpt = lpt4, lpt0 = lpt2, lpt3 = lpt4, m = m3, m0 = m1, m1 = m4, m3 = m2, m4 = m5, m7 = m6, ns = ns1, ns0 = ns5, ns1 = ns2, ns5 = ns6, 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, 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, ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ [err := err0; if err = ESUCCESS then bleb := nobuffer, isbuf := false, adr0 := adr, m0 := m, log0 := log, lpt0 := lpt, ns0 := ns else avol := ?, bleb := ?, isbuf := ?, adr := ?, m := ?, log := ?, lpt := ?, adr0 := ?, m0 := ?, log0 := ?, lpt0 := ?, ns0 := ?, ns := ?; log9 := log0; if err ≠ ESUCCESS then debug#("persistence: wbuf recover failed") else {awbuf_get_leb_size#(adr, m, log, avol, lpt, ns, bleb, isbuf; ; m7); let log1 = log9 in persistence_replay_log#(m7; log1, lpt0); persistence_replay_lpt#(log9, m7, adr, m, log, lpt, ns, bleb, isbuf; lpt0, avol); persistence_create_freelist#(lpt0; freelist); persistence_create_gcheap#(log9; lpt0, gch)}] ( ( err = ESUCCESS → synced(avol) ∧ lpt-free-unref(lpt0) ∧ lpt-free-unref(lpt) ∧ freelist-cons(lpt0, freelist) ∧ log9 = log ∧ bin-heap-inv(gch, lpt0) ∧ keyset(gch) = gc-heap(lpt0, log) ∧ bufs-log-only(bleb, log, lpt0) ∧ # lpt0 = # avol ∧ ¬ dups(log) ∧ log-group-block(log, lpt0) ∧ buf-ro-rw-mode(isbuf, bleb, lpt0, avol) ∧ lpt-leb-size(lpt0) ∧ lpt-leb-size(lpt) ∧ lpt-ram-flash(lpt0, lpt, log) ∧ m7 = LEB_SIZE ∧ awbuf-inv(avol, bleb) ∧ # lpt = # avol) ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ ( err = ESUCCESS → # avol = # avol0 ∧ adr0 = adr1 ∧ adr = adr1 ∧ m0 = m2 ∧ m = m2 ∧ log0 = log2 ∧ log = log2 ∧ ns0 = ns2 ∧ ns = ns2 ∧ lpt = lpt3 ∧ bleb = nobuffer ∧ id-idx(replay-lpt(replay-log(lpt3, log2), log2, # lpt3), lpt0)) → ( err = ESUCCESS → ⟨istore := remove-refsize0(crash(istore1, istore2)), gstore := crash(gstore1, gstore2, ns3, log2); apersistence_recover#(; adr4, m5, log6, ns6, adr1, log2, m2, ns2, istore, istore2, ns3, gstore, gstore2; pstate, isbuf0, err1)⟩ ( abs-istore(avol, lpt0, istore) ∧ abs-gstore(avol, lpt0, gstore, ns3) ∧ adr1 = adr ∧ m2 = m ∧ log2 = log9 ∧ ns3 < # lpt0 ∧ ns2 = ns ∧ flash-lpt-cons(lpt, istore2, gstore2) ∧ (isbuf0 → synced(avol)) ∧ (pstate = unbuffered → bleb = nobuffer) ∧ (pstate = readonly ↔ isbuf) ∧ (pstate ≠ unbuffered ∧ pstate ≠ readonly → bleb = buffered(pstate.lnum)) ∧ adr0 = adr4 ∧ m0 = m5 ∧ log0 = log6 ∧ ns0 = ns6 ∧ ESUCCESS = err1)) ∧ ( err ≠ ESUCCESS → (∀ adr, istore, istore0, ns, gstore, gstore0, log, m, ns1, pstate, isbuf. ⟨apersistence_recover# (; adr4, m5, log6, ns6, adr5, log8, maxino0, ns7, istore3, istore4, ginval0, gstore3, gstore4; pstate1, isbuf3, err1)⟩ ( adr = adr5 ∧ istore = istore3 ∧ istore0 = istore4 ∧ ns = ginval0 ∧ gstore = gstore3 ∧ gstore0 = gstore4 ∧ log = log8 ∧ m = maxino0 ∧ ns1 = ns7 ∧ pstate = pstate1 ∧ (isbuf ↔ isbuf3) ∧ adr0 = adr4 ∧ m0 = m5 ∧ log0 = log6 ∧ ns0 = ns6 ∧ err = err1)))), dups(log3)