| # lpt = # avol0, # lpt4 = # avol0, # avol = # avol0, # lpt2 = # avol0, # avol2 = # avol0, adr = adr1, adr0 = adr4, adr2 = adr1, ginval = ns3, gstore = gstore2, gstore0 = gstore3, gstore3 = crash(gstore1, gstore2, ns3, log3), istore = istore2, istore0 = istore3, istore3 = remove-refsize0(crash(istore1, istore2)), keyset(gch) = gc-heap(replay-lpt(replay-log(lpt4, log3), log3, # avol0), log3), keyset(gch1) = gc-heap(lpt2, log3), log = log3, log0 = log6, log1 = log3, m = m5, m0 = m2, maxino = m2, ns = ns2, ns0 = ns6, ns1 = ns2, remove-refsize0(gstore2) = gstore2, remove-refsize0(istore2) = istore2, elems log3 ∩ ns3 = ∅, dom gstore2 ∪ elems log3 = dom gstore1 ∪ ns3, ns3 < # avol0, abs-gstore(avol0, lpt2, gstore1, ns3), abs-istore(avol0, lpt2, istore1), avol-replay-lpt-unchanged(avol, avol2, replay-log(lpt4, log3), log3), awbuf-inv(avol2, nobuffer), awbuf-inv(avol0, bleb1), bin-heap-inv(gch, lpt), bin-heap-inv(gch1, lpt2), buf-ro-rw-mode(pstate0 = readonly, bleb1, lpt2, avol0), bufs-log-only(bleb1, log3, lpt2), flash-lpt-cons(lpt4, istore2, gstore2), freelist-cons(replay-lpt(replay-log(lpt4, log3), log3, # avol0), freelist), freelist-cons(lpt2, log4), id-idx(replay-lpt(replay-log(lpt4, log3), log3, # avol0), lpt), inv(gstore1 \ ns3), inv(gstore2), inv(istore1), inv(istore2), log-group-block(log3, lpt), log-group-block(log3, lpt2), lpt-free-unref(lpt4), lpt-free-unref(lpt2), lpt-leb-size(replay-lpt(replay-log(lpt4, log3), log3, # avol0)), lpt-leb-size(lpt4), lpt-leb-size(lpt2), lpt-ram-flash(lpt, lpt4, log3), lpt-ram-flash(lpt2, lpt4, log3), synced(avol2), synced(avol0), synced(avol), valid-indices(lpt4, log3), 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 ⊦ ∃ err0. (⌊err0⌋ ∨ err0 = ESUCCESS) ∧ ⟨err := err0; if err = ESUCCESS then pstate := unbuffered, isbuf := true, adr0 := adr, m := maxino, log0 := log, ns0 := ns else pstate := ?, isbuf := ?, adr := ?, istore0 := ?, istore := ?, ginval := ?, gstore0 := ?, gstore := ?, log := ?, maxino := ?, ns := ?, adr0 := ?, m := ?, log0 := ?, ns0 := ?⟩ ( abs-istore(avol2, replay-lpt(replay-log(lpt4, log0), log0, # avol0), istore0) ∧ abs-gstore(avol2, replay-lpt(replay-log(lpt4, log0), log0, # avol0), gstore0, ginval) ∧ adr = adr0 ∧ maxino = m ∧ log = log0 ∧ ginval < # avol0 ∧ ns = ns0 ∧ flash-lpt-cons(lpt4, istore, gstore) ∧ pstate = unbuffered ∧ adr2 = adr0 ∧ m0 = m ∧ log1 = log0 ∧ ns1 = ns0 ∧ ESUCCESS = err), dups(log3) |
# avol2 = # avol0, # lpt2 = # avol0, # avol = # avol0, # lpt4 = # avol0, # lpt = # avol0, adr = adr1, gstore0 = crash(gstore1, gstore2, ns3, log3), istore0 = remove-refsize0(crash(istore1, istore2)), keyset(gch1) = gc-heap(lpt2, log3), keyset(gch) = gc-heap(replay-lpt(replay-log(lpt4, log3), log3, # avol0), log3), log = log3, m0 = m2, ns = ns2, remove-refsize0(istore2) = istore2, remove-refsize0(gstore2) = gstore2, elems log3 ∩ ns3 = ∅, dom gstore2 ∪ elems log3 = dom gstore1 ∪ ns3, ns3 < # avol0, abs-gstore(avol0, lpt2, gstore1, ns3), abs-istore(avol0, lpt2, istore1), avol-replay-lpt-unchanged(avol, avol2, replay-log(lpt4, log3), log3), awbuf-inv(avol0, bleb1), awbuf-inv(avol2, nobuffer), bin-heap-inv(gch1, lpt2), bin-heap-inv(gch, lpt), buf-ro-rw-mode(pstate0 = readonly, bleb1, lpt2, avol0), bufs-log-only(bleb1, log3, lpt2), flash-lpt-cons(lpt4, istore2, gstore2), freelist-cons(lpt2, log4), freelist-cons(replay-lpt(replay-log(lpt4, log3), log3, # avol0), freelist), id-idx(replay-lpt(replay-log(lpt4, log3), log3, # avol0), lpt), inv(istore2), inv(istore1), inv(gstore2), inv(gstore1 \ ns3), log-group-block(log3, lpt2), log-group-block(log3, lpt), lpt-free-unref(lpt2), lpt-free-unref(lpt4), lpt-leb-size(lpt2), lpt-leb-size(lpt4), lpt-leb-size(replay-lpt(replay-log(lpt4, log3), log3, # avol0)), lpt-ram-flash(lpt2, lpt4, log3), lpt-ram-flash(lpt, lpt4, log3), synced(avol), synced(avol0), synced(avol2), valid-indices(lpt4, log3), 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 ⊦ ∃ err0. (⌊err0⌋ ∨ err0 = ESUCCESS) ∧ ⟨err := err0; if err = ESUCCESS then pstate := unbuffered, isbuf := true, adr0 := adr, m := m2, log0 := log, ns0 := ns else pstate := ?, isbuf := ?, adr := ?, istore0 := ?, istore2 := ?, ns3 := ?, gstore0 := ?, gstore2 := ?, log := ?, m2 := ?, ns := ?, adr0 := ?, m := ?, log0 := ?, ns0 := ?⟩ ( abs-istore(avol2, replay-lpt(replay-log(lpt4, log0), log0, # avol0), istore0) ∧ abs-gstore(avol2, replay-lpt(replay-log(lpt4, log0), log0, # avol0), gstore0, ns3) ∧ adr = adr0 ∧ m2 = m ∧ log = log0 ∧ ns3 < # avol0 ∧ ns = ns0 ∧ flash-lpt-cons(lpt4, istore2, gstore2) ∧ pstate = unbuffered ∧ adr1 = adr0 ∧ m0 = m ∧ log3 = log0 ∧ ns2 = ns0 ∧ ESUCCESS = err)