| # lpt3 = # avol0, # lpt1 = # avol0, # lpt = # avol0, adr = adr2, adr = adr, adr3 = adr, avol1 = avol0, bleb2 = bleb1, keyset(gch1) = gc-heap(lpt1, log2), log = log2, log = log, lpt = lpt3, lpt = lpt, lpt2 = lpt, m = m4, m = m, m2 = m, ns = ns2, ns = ns, ns3 = ns, nx2 = log, awbuf-inv(avol0, bleb1), bin-heap-inv(gch1, lpt1), buf-ro-rw-mode(isbuf1, bleb1, lpt1, avol0), bufs-log-only(bleb1, log2, lpt1), freelist-cons(lpt1, log5), log-group-block(log2, lpt1), lpt-free-unref(lpt3), lpt-free-unref(lpt1), lpt-leb-size(lpt3), lpt-leb-size(lpt1), lpt-ram-flash(lpt1, lpt3, log2), synced(avol0), avol ↓ avol0 ⊦ [awbuf_recover#(; adr0, m1, ns0, log1, lpt0, adr, m, log, lpt, ns, avol; bleb, isbuf, err)] ( (err = ESUCCESS → synced(avol) ∧ awbuf-inv(avol, bleb) ∧ # lpt = # avol) → ⟪log0 := log1; if err ≠ ESUCCESS then debug#("persistence: wbuf recover failed") else {awbuf_get_leb_size#(adr, m, log, avol, lpt, ns, bleb, isbuf; ; m0); let log1 = log0 in persistence_replay_log#(m0; log1, lpt0); persistence_replay_lpt#(log0, m0, adr, m, log, lpt, ns, bleb, isbuf; lpt0, avol); persistence_create_freelist#(lpt0; freelist); persistence_create_gcheap#(log0; lpt0, gch)}⟫ ( ( err = ESUCCESS → synced(avol) ∧ lpt-free-unref(lpt0) ∧ lpt-free-unref(lpt) ∧ freelist-cons(lpt0, freelist) ∧ log0 = 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) ∧ m0 = LEB_SIZE ∧ awbuf-inv(avol, bleb) ∧ # lpt = # avol) ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ ( err = ESUCCESS → # avol = # avol0 ∧ adr0 = adr2 ∧ adr = adr2 ∧ m1 = m4 ∧ m = m4 ∧ log1 = log2 ∧ log = log2 ∧ ns0 = ns2 ∧ ns = ns2 ∧ lpt = lpt3 ∧ bleb = nobuffer ∧ id-idx(replay-lpt(replay-log(lpt3, log2), log2, # avol0), lpt0)))), dups(log2) |
# lpt1 = # avol0, # lpt3 = # avol0, adr = adr2, keyset(gch1) = gc-heap(lpt1, log2), log = log2, lpt = lpt3, m = m4, ns = ns2, awbuf-inv(avol0, bleb1), bin-heap-inv(gch1, lpt1), buf-ro-rw-mode(isbuf1, bleb1, lpt1, avol0), bufs-log-only(bleb1, log2, lpt1), freelist-cons(lpt1, log5), log-group-block(log2, lpt1), lpt-free-unref(lpt1), lpt-free-unref(lpt3), lpt-leb-size(lpt1), lpt-leb-size(lpt3), lpt-ram-flash(lpt1, lpt3, log2), synced(avol0), avol ↓ avol0, ¬ dups(log2) ⊦ [awbuf_recover#(; adr0, m1, ns0, log1, lpt0, adr, m, log, lpt, ns, avol; bleb, isbuf, err)] ( (err = ESUCCESS → synced(avol) ∧ awbuf-inv(avol, bleb) ∧ # lpt = # avol) → ⟪log0 := log1; if err ≠ ESUCCESS then debug#("persistence: wbuf recover failed") else {awbuf_get_leb_size#(adr, m, log, avol, lpt, ns, bleb, isbuf; ; m0); let log1 = log0 in persistence_replay_log#(m0; log1, lpt0); persistence_replay_lpt#(log0, m0, adr, m, log, lpt, ns, bleb, isbuf; lpt0, avol); persistence_create_freelist#(lpt0; freelist); persistence_create_gcheap#(log0; lpt0, gch)}⟫ ( ( err = ESUCCESS → synced(avol) ∧ lpt-free-unref(lpt0) ∧ lpt-free-unref(lpt) ∧ freelist-cons(lpt0, freelist) ∧ log0 = 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) ∧ m0 = LEB_SIZE ∧ awbuf-inv(avol, bleb) ∧ # lpt = # avol) ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ ( err = ESUCCESS → # avol = # avol0 ∧ adr0 = adr2 ∧ adr = adr2 ∧ m1 = m4 ∧ m = m4 ∧ log1 = log2 ∧ log = log2 ∧ ns0 = ns2 ∧ ns = ns2 ∧ lpt = lpt3 ∧ bleb = nobuffer ∧ id-idx(replay-lpt(replay-log(lpt3, log2), log2, # avol0), lpt0))))