| # lpt0 = # avol0, # lpt1 = # avol0, adr = adr0, keyset(gch) = gc-heap(lpt1, log2), log = log0, log2 = log0, lpt = lpt0, m = m0, m1 = LEB_SIZE, ns = ns0, awbuf-inv(avol0, bleb), bin-heap-inv(gch, lpt1), buf-ro-rw-mode(isbuf, bleb, lpt1, avol0), bufs-log-only(bleb, log2, lpt1), freelist-cons(lpt1, log1), log-group-block(log2, lpt1), lpt-free-unref(lpt0), lpt-free-unref(lpt1), lpt-leb-size(lpt0), lpt-leb-size(lpt1), lpt-ram-flash(lpt1, lpt0, log2), synced(avol0), avol ↓ 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))), dups(log2) |
# lpt1 = # avol0, # lpt0 = # avol0, adr = adr0, keyset(gch) = gc-heap(lpt1, log0), log = log0, lpt = lpt0, m = m0, ns = ns0, awbuf-inv(avol0, bleb), bin-heap-inv(gch, lpt1), buf-ro-rw-mode(isbuf, bleb, lpt1, avol0), bufs-log-only(bleb, log0, lpt1), freelist-cons(lpt1, log1), log-group-block(log0, lpt1), lpt-free-unref(lpt1), lpt-free-unref(lpt0), lpt-leb-size(lpt1), lpt-leb-size(lpt0), lpt-ram-flash(lpt1, lpt0, log0), synced(avol0), avol ↓ avol0, ¬ dups(log0) ⊦ ⟪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, log) ∧ bufs-log-only(bleb0, log, lpt2) ∧ # lpt2 = # avol ∧ ¬ dups(log) ∧ log-group-block(log, lpt2) ∧ buf-ro-rw-mode(isbuf0, bleb0, lpt2, avol) ∧ lpt-leb-size(lpt2) ∧ lpt-leb-size(lpt) ∧ lpt-ram-flash(lpt2, lpt, log) ∧ m3 = LEB_SIZE ∧ awbuf-inv(avol, bleb0) ∧ # lpt = # avol) ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ ( err = ESUCCESS → # avol = # avol0 ∧ adr1 = adr0 ∧ adr = adr0 ∧ m2 = m0 ∧ m = m0 ∧ log3 = log0 ∧ log = log0 ∧ ns1 = ns0 ∧ ns = ns0 ∧ lpt = lpt0 ∧ bleb0 = nobuffer ∧ id-idx(replay-lpt(replay-log(lpt0, log0), log0, # avol0), lpt2)))