This is a listing of all goals defined over the current specification. Axioms are marked yellow, proved theorems green and unproved theorems blue. Click on individual names to get more information on the proof.
| Name: | Sequent: | Type: |
|---|---|---|
| refine-read-gnd | adr ∈ gstore, ¬ adr.lnum ∈ ginval, abs-istore(avol, lpt, istore), abs-gstore(avol, lpt, gstore, ginval), adr0 = adr1, maxino = m, log = log0, ginval < # lpt, ns = ns0, flash-lpt-cons(lpt0, istore0, gstore0), isbuf → synced(avol), pstate = unbuffered → bleb = nobuffer, pstate = readonly ↔ isbuf0, pstate ≠ unbuffered ∧ pstate ≠ readonly → bleb = buffered(pstate.lnum), inv-journal(log, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, log, gstore, istore, isbuf), lpt-free-unref(lpt), lpt-free-unref(lpt0), freelist-cons(lpt, freelist), log0 = log1, bin-heap-inv(gch, lpt), keyset(gch) = gc-heap(lpt, log0), bufs-log-only(bleb, log0, lpt), # lpt = # avol, ¬ dups(log0), log-group-block(log0, lpt), buf-ro-rw-mode(isbuf0, bleb, lpt, avol), lpt-leb-size(lpt), lpt-leb-size(lpt0), lpt-ram-flash(lpt, lpt0, log0), m0 = LEB_SIZE, awbuf-inv(avol, bleb), # lpt0 = # avol, gnd = gnd0 ⊦ ⟪persistence_read_gnd#(adr, adr1, m, log1, avol, lpt0, ns0, bleb, isbuf0; gnd; err)⟫ ⟨apersistence_read_gnd#(adr, adr0, istore, istore0, ginval, gstore, gstore0, log, maxino, ns, pstate, isbuf; gnd0; err0)⟩ ( ( abs-istore(avol, lpt, istore) ∧ abs-gstore(avol, lpt, gstore, ginval) ∧ adr0 = adr1 ∧ maxino = m ∧ log = log0 ∧ ginval < # lpt ∧ ns = ns0 ∧ flash-lpt-cons(lpt0, istore0, gstore0) ∧ (isbuf → synced(avol)) ∧ (pstate = unbuffered → bleb = nobuffer) ∧ (pstate = readonly ↔ isbuf0) ∧ (pstate ≠ unbuffered ∧ pstate ≠ readonly → bleb = buffered(pstate.lnum))) ∧ gnd = gnd0 ∧ err = err0) | A Proof Obligation |
| refine-read-ind | adr ∈ istore, abs-istore(avol, lpt, istore), abs-gstore(avol, lpt, gstore, ginval), adr0 = adr1, maxino = m, log = log0, ginval < # lpt, ns = ns0, flash-lpt-cons(lpt0, istore0, gstore0), isbuf → synced(avol), pstate = unbuffered → bleb = nobuffer, pstate = readonly ↔ isbuf0, pstate ≠ unbuffered ∧ pstate ≠ readonly → bleb = buffered(pstate.lnum), inv-journal(log, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, log, gstore, istore, isbuf), lpt-free-unref(lpt), lpt-free-unref(lpt0), freelist-cons(lpt, freelist), log0 = log1, bin-heap-inv(gch, lpt), keyset(gch) = gc-heap(lpt, log0), bufs-log-only(bleb, log0, lpt), # lpt = # avol, ¬ dups(log0), log-group-block(log0, lpt), buf-ro-rw-mode(isbuf0, bleb, lpt, avol), lpt-leb-size(lpt), lpt-leb-size(lpt0), lpt-ram-flash(lpt, lpt0, log0), m0 = LEB_SIZE, awbuf-inv(avol, bleb), # lpt0 = # avol, ind = ind0 ⊦ ⟪persistence_read_ind#(adr, adr1, m, log1, avol, lpt0, ns0, bleb, isbuf0; ind; err)⟫ ⟨apersistence_read_ind#(adr, adr0, istore, istore0, ginval, gstore, gstore0, log, maxino, ns, pstate, isbuf; ind0; err0)⟩ ( ( abs-istore(avol, lpt, istore) ∧ abs-gstore(avol, lpt, gstore, ginval) ∧ adr0 = adr1 ∧ maxino = m ∧ log = log0 ∧ ginval < # lpt ∧ ns = ns0 ∧ flash-lpt-cons(lpt0, istore0, gstore0) ∧ (isbuf → synced(avol)) ∧ (pstate = unbuffered → bleb = nobuffer) ∧ (pstate = readonly ↔ isbuf0) ∧ (pstate ≠ unbuffered ∧ pstate ≠ readonly → bleb = buffered(pstate.lnum))) ∧ ind = ind0 ∧ err = err0) | A Proof Obligation |
| refine-read-gblock-nodes | m ∈ gstore, ¬ m ∈ ginval, abs-istore(avol, lpt, istore), abs-gstore(avol, lpt, gstore, ginval), adr = adr0, maxino = m0, log = log0, ginval < # lpt, ns = ns0, flash-lpt-cons(lpt0, istore0, gstore0), isbuf → synced(avol), pstate = unbuffered → bleb = nobuffer, pstate = readonly ↔ isbuf0, pstate ≠ unbuffered ∧ pstate ≠ readonly → bleb = buffered(pstate.lnum), inv-journal(log, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, log, gstore, istore, isbuf), lpt-free-unref(lpt), lpt-free-unref(lpt0), freelist-cons(lpt, freelist), log0 = log1, bin-heap-inv(gch, lpt), keyset(gch) = gc-heap(lpt, log0), bufs-log-only(bleb, log0, lpt), # lpt = # avol, ¬ dups(log0), log-group-block(log0, lpt), buf-ro-rw-mode(isbuf0, bleb, lpt, avol), lpt-leb-size(lpt), lpt-leb-size(lpt0), lpt-ram-flash(lpt, lpt0, log0), m1 = LEB_SIZE, awbuf-inv(avol, bleb), # lpt0 = # avol, ax = ax0, gndx = gndx0 ⊦ ⟪persistence_read_gblock_nodes#(m, m1, adr0, m0, log1, avol, lpt0, ns0, bleb, isbuf0; ax, gndx; err)⟫ ⟨apersistence_read_gblock_nodes#(m, adr, istore, istore0, ginval, gstore, gstore0, log, maxino, ns, pstate, isbuf; ax0, gndx0; err0)⟩ ( ( abs-istore(avol, lpt, istore) ∧ abs-gstore(avol, lpt, gstore, ginval) ∧ adr = adr0 ∧ maxino = m0 ∧ log = log0 ∧ ginval < # lpt ∧ ns = ns0 ∧ flash-lpt-cons(lpt0, istore0, gstore0) ∧ (isbuf → synced(avol)) ∧ (pstate = unbuffered → bleb = nobuffer) ∧ (pstate = readonly ↔ isbuf0) ∧ (pstate ≠ unbuffered ∧ pstate ≠ readonly → bleb = buffered(pstate.lnum))) ∧ ax = ax0 ∧ gndx = gndx0 ∧ err = err0) | A Proof Obligation |
| refine-get-gc-block | abs-istore(avol, lpt, istore), abs-gstore(avol, lpt, gstore, ginval), adr = adr0, maxino = m, log = log0, ginval < # lpt, ns = ns0, flash-lpt-cons(lpt0, istore0, gstore0), isbuf → synced(avol), pstate = unbuffered → bleb = nobuffer, pstate = readonly ↔ isbuf0, pstate ≠ unbuffered ∧ pstate ≠ readonly → bleb = buffered(pstate.lnum), inv-journal(log, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, log, gstore, istore, isbuf), lpt-free-unref(lpt), lpt-free-unref(lpt0), freelist-cons(lpt, freelist), log0 = log1, bin-heap-inv(gch, lpt), keyset(gch) = gc-heap(lpt, log0), bufs-log-only(bleb, log0, lpt), # lpt = # avol, ¬ dups(log0), log-group-block(log0, lpt), buf-ro-rw-mode(isbuf0, bleb, lpt, avol), lpt-leb-size(lpt), lpt-leb-size(lpt0), lpt-ram-flash(lpt, lpt0, log0), m0 = LEB_SIZE, awbuf-inv(avol, bleb), # lpt0 = # avol, n = n0 ⊦ ⟪persistence_get_gc_block#(gch; n; err)⟫ ⟨apersistence_get_gc_block#(adr, istore, istore0, ginval, gstore, gstore0, log, maxino, ns, pstate, isbuf; n0; err0)⟩ ( ( abs-istore(avol, lpt, istore) ∧ abs-gstore(avol, lpt, gstore, ginval) ∧ adr = adr0 ∧ maxino = m ∧ log = log0 ∧ ginval < # lpt ∧ ns = ns0 ∧ flash-lpt-cons(lpt0, istore0, gstore0) ∧ (isbuf → synced(avol)) ∧ (pstate = unbuffered → bleb = nobuffer) ∧ (pstate = readonly ↔ isbuf0) ∧ (pstate ≠ unbuffered ∧ pstate ≠ readonly → bleb = buffered(pstate.lnum))) ∧ n = n0 ∧ err = err0) | A Proof Obligation |
| refine-set-gblock-refsize | m ∈ gstore, abs-istore(avol, lpt, istore), abs-gstore(avol, lpt, gstore, ginval), adr = adr0, maxino = m0, log = log0, ginval < # lpt, ns = ns0, flash-lpt-cons(lpt0, istore0, gstore0), isbuf → synced(avol), pstate = unbuffered → bleb = nobuffer, pstate = readonly ↔ isbuf0, pstate ≠ unbuffered ∧ pstate ≠ readonly → bleb = buffered(pstate.lnum), inv-journal(log, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, log, gstore, istore, isbuf), lpt-free-unref(lpt), lpt-free-unref(lpt0), freelist-cons(lpt, freelist), log0 = log1, bin-heap-inv(gch, lpt), keyset(gch) = gc-heap(lpt, log0), bufs-log-only(bleb, log0, lpt), # lpt = # avol, ¬ dups(log0), log-group-block(log0, lpt), buf-ro-rw-mode(isbuf0, bleb, lpt, avol), lpt-leb-size(lpt), lpt-leb-size(lpt0), lpt-ram-flash(lpt, lpt0, log0), m1 = LEB_SIZE, awbuf-inv(avol, bleb), # lpt0 = # avol ⊦ ⟪persistence_set_gblock_refsize#(m, n, log0; lpt, gch)⟫ ⟨apersistence_set_gblock_refsize#(m, n, adr, istore, istore0, ginval, gstore0, log, maxino, ns, pstate, isbuf; gstore)⟩ ( abs-istore(avol, lpt, istore) ∧ abs-gstore(avol, lpt, gstore, ginval) ∧ adr = adr0 ∧ maxino = m0 ∧ log = log0 ∧ ginval < # lpt ∧ ns = ns0 ∧ flash-lpt-cons(lpt0, istore0, gstore0) ∧ (isbuf → synced(avol)) ∧ (pstate = unbuffered → bleb = nobuffer) ∧ (pstate = readonly ↔ isbuf0) ∧ (pstate ≠ unbuffered ∧ pstate ≠ readonly → bleb = buffered(pstate.lnum))) | A Proof Obligation |
| refine-set-iblock-refsize | m ∈ istore, abs-istore(avol, lpt, istore), abs-gstore(avol, lpt, gstore, ginval), adr = adr0, maxino = m0, log = log0, ginval < # lpt, ns = ns0, flash-lpt-cons(lpt0, istore0, gstore0), isbuf → synced(avol), pstate = unbuffered → bleb = nobuffer, pstate = readonly ↔ isbuf0, pstate ≠ unbuffered ∧ pstate ≠ readonly → bleb = buffered(pstate.lnum), inv-journal(log, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, log, gstore, istore, isbuf), lpt-free-unref(lpt), lpt-free-unref(lpt0), freelist-cons(lpt, freelist), log0 = log1, bin-heap-inv(gch, lpt), keyset(gch) = gc-heap(lpt, log0), bufs-log-only(bleb, log0, lpt), # lpt = # avol, ¬ dups(log0), log-group-block(log0, lpt), buf-ro-rw-mode(isbuf0, bleb, lpt, avol), lpt-leb-size(lpt), lpt-leb-size(lpt0), lpt-ram-flash(lpt, lpt0, log0), m1 = LEB_SIZE, awbuf-inv(avol, bleb), # lpt0 = # avol ⊦ ⟪persistence_set_iblock_refsize#(m, n; lpt)⟫ ⟨apersistence_set_iblock_refsize#(m, n, adr, istore0, ginval, gstore, gstore0, log, maxino, ns, pstate, isbuf; istore)⟩ ( abs-istore(avol, lpt, istore) ∧ abs-gstore(avol, lpt, gstore, ginval) ∧ adr = adr0 ∧ maxino = m0 ∧ log = log0 ∧ ginval < # lpt ∧ ns = ns0 ∧ flash-lpt-cons(lpt0, istore0, gstore0) ∧ (isbuf → synced(avol)) ∧ (pstate = unbuffered → bleb = nobuffer) ∧ (pstate = readonly ↔ isbuf0) ∧ (pstate ≠ unbuffered ∧ pstate ≠ readonly → bleb = buffered(pstate.lnum))) | A Proof Obligation |
| refine-get-gblock-refsize | m ∈ gstore, abs-istore(avol, lpt, istore), abs-gstore(avol, lpt, gstore, ginval), adr = adr0, maxino = m0, log = log0, ginval < # lpt, ns = ns0, flash-lpt-cons(lpt0, istore0, gstore0), isbuf → synced(avol), pstate = unbuffered → bleb = nobuffer, pstate = readonly ↔ isbuf0, pstate ≠ unbuffered ∧ pstate ≠ readonly → bleb = buffered(pstate.lnum), inv-journal(log, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, log, gstore, istore, isbuf), lpt-free-unref(lpt), lpt-free-unref(lpt0), freelist-cons(lpt, freelist), log0 = log1, bin-heap-inv(gch, lpt), keyset(gch) = gc-heap(lpt, log0), bufs-log-only(bleb, log0, lpt), # lpt = # avol, ¬ dups(log0), log-group-block(log0, lpt), buf-ro-rw-mode(isbuf0, bleb, lpt, avol), lpt-leb-size(lpt), lpt-leb-size(lpt0), lpt-ram-flash(lpt, lpt0, log0), m1 = LEB_SIZE, awbuf-inv(avol, bleb), # lpt0 = # avol ⊦ ⟪persistence_get_gblock_refsize#(m, lpt; ; n)⟫ ⟨apersistence_get_gblock_refsize#(m, adr, istore, istore0, ginval, gstore, gstore0, log, maxino, ns, pstate, isbuf; ; n0)⟩ ( ( abs-istore(avol, lpt, istore) ∧ abs-gstore(avol, lpt, gstore, ginval) ∧ adr = adr0 ∧ maxino = m0 ∧ log = log0 ∧ ginval < # lpt ∧ ns = ns0 ∧ flash-lpt-cons(lpt0, istore0, gstore0) ∧ (isbuf → synced(avol)) ∧ (pstate = unbuffered → bleb = nobuffer) ∧ (pstate = readonly ↔ isbuf0) ∧ (pstate ≠ unbuffered ∧ pstate ≠ readonly → bleb = buffered(pstate.lnum))) ∧ n = n0) | A Proof Obligation |
| refine-get-iblock-refsize | m ∈ istore, abs-istore(avol, lpt, istore), abs-gstore(avol, lpt, gstore, ginval), adr = adr0, maxino = m0, log = log0, ginval < # lpt, ns = ns0, flash-lpt-cons(lpt0, istore0, gstore0), isbuf → synced(avol), pstate = unbuffered → bleb = nobuffer, pstate = readonly ↔ isbuf0, pstate ≠ unbuffered ∧ pstate ≠ readonly → bleb = buffered(pstate.lnum), inv-journal(log, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, log, gstore, istore, isbuf), lpt-free-unref(lpt), lpt-free-unref(lpt0), freelist-cons(lpt, freelist), log0 = log1, bin-heap-inv(gch, lpt), keyset(gch) = gc-heap(lpt, log0), bufs-log-only(bleb, log0, lpt), # lpt = # avol, ¬ dups(log0), log-group-block(log0, lpt), buf-ro-rw-mode(isbuf0, bleb, lpt, avol), lpt-leb-size(lpt), lpt-leb-size(lpt0), lpt-ram-flash(lpt, lpt0, log0), m1 = LEB_SIZE, awbuf-inv(avol, bleb), # lpt0 = # avol ⊦ ⟪persistence_get_iblock_refsize#(m, lpt; ; n)⟫ ⟨apersistence_get_iblock_refsize#(m, adr, istore, istore0, ginval, gstore, gstore0, log, maxino, ns, pstate, isbuf; ; n0)⟩ ( ( abs-istore(avol, lpt, istore) ∧ abs-gstore(avol, lpt, gstore, ginval) ∧ adr = adr0 ∧ maxino = m0 ∧ log = log0 ∧ ginval < # lpt ∧ ns = ns0 ∧ flash-lpt-cons(lpt0, istore0, gstore0) ∧ (isbuf → synced(avol)) ∧ (pstate = unbuffered → bleb = nobuffer) ∧ (pstate = readonly ↔ isbuf0) ∧ (pstate ≠ unbuffered ∧ pstate ≠ readonly → bleb = buffered(pstate.lnum))) ∧ n = n0) | A Proof Obligation |
| refine-allocate-gnd | isbuf, abs-istore(avol, lpt, istore), abs-gstore(avol, lpt, gstore, ginval), adr = adr0, maxino = m, log = log0, ginval < # lpt, ns = ns0, flash-lpt-cons(lpt0, istore0, gstore0), isbuf → synced(avol), pstate = unbuffered → bleb = nobuffer, pstate = readonly ↔ isbuf0, pstate ≠ unbuffered ∧ pstate ≠ readonly → bleb = buffered(pstate.lnum), inv-journal(log, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, log, gstore, istore, isbuf), lpt-free-unref(lpt), lpt-free-unref(lpt0), freelist-cons(lpt, freelist), log0 = log1, bin-heap-inv(gch, lpt), keyset(gch) = gc-heap(lpt, log0), bufs-log-only(bleb, log0, lpt), # lpt = # avol, ¬ dups(log0), log-group-block(log0, lpt), buf-ro-rw-mode(isbuf0, bleb, lpt, avol), lpt-leb-size(lpt), lpt-leb-size(lpt0), lpt-ram-flash(lpt, lpt0, log0), m0 = LEB_SIZE, awbuf-inv(avol, bleb), # lpt0 = # avol ⊦ ⟪persistence_allocate_gnd#(adr0, m, lpt0, ns0, isbuf0; log0, lpt, freelist, log1, avol, bleb; err)⟫ ⟨apersistence_allocate_gnd#(adr, istore, istore0, gstore0, maxino, ns, isbuf; ginval, gstore, log, pstate; err0)⟩ ( ( abs-istore(avol, lpt, istore) ∧ abs-gstore(avol, lpt, gstore, ginval) ∧ adr = adr0 ∧ maxino = m ∧ log = log0 ∧ ginval < # lpt ∧ ns = ns0 ∧ flash-lpt-cons(lpt0, istore0, gstore0) ∧ (isbuf → synced(avol)) ∧ (pstate = unbuffered → bleb = nobuffer) ∧ (pstate = readonly ↔ isbuf0) ∧ (pstate ≠ unbuffered ∧ pstate ≠ readonly → bleb = buffered(pstate.lnum))) ∧ err = err0) | A Proof Obligation |
| refine-deallocate-gnd | isbuf, n ∈ gstore, ¬ n ∈ log, abs-istore(avol, lpt, istore), abs-gstore(avol, lpt, gstore, ginval), adr = adr0, maxino = m, log = log0, ginval < # lpt, ns = ns0, flash-lpt-cons(lpt0, istore0, gstore0), isbuf → synced(avol), pstate = unbuffered → bleb = nobuffer, pstate = readonly ↔ isbuf0, pstate ≠ unbuffered ∧ pstate ≠ readonly → bleb = buffered(pstate.lnum), inv-journal(log, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, log, gstore, istore, isbuf), lpt-free-unref(lpt), lpt-free-unref(lpt0), freelist-cons(lpt, freelist), log0 = log1, bin-heap-inv(gch, lpt), keyset(gch) = gc-heap(lpt, log0), bufs-log-only(bleb, log0, lpt), # lpt = # avol, ¬ dups(log0), log-group-block(log0, lpt), buf-ro-rw-mode(isbuf0, bleb, lpt, avol), lpt-leb-size(lpt), lpt-leb-size(lpt0), lpt-ram-flash(lpt, lpt0, log0), m0 = LEB_SIZE, awbuf-inv(avol, bleb), # lpt0 = # avol ⊦ ⟪persistence_deallocate_gnd#(n, log0, adr0, m, log1, lpt0, ns0, bleb, isbuf0; lpt, freelist, gch, avol; err)⟫ ⟨apersistence_deallocate_gnd#(n, adr, istore, istore0, gstore0, log, maxino, ns, pstate, isbuf; ginval, gstore; err0)⟩ ( ( abs-istore(avol, lpt, istore) ∧ abs-gstore(avol, lpt, gstore, ginval) ∧ adr = adr0 ∧ maxino = m ∧ log = log0 ∧ ginval < # lpt ∧ ns = ns0 ∧ flash-lpt-cons(lpt0, istore0, gstore0) ∧ (isbuf → synced(avol)) ∧ (pstate = unbuffered → bleb = nobuffer) ∧ (pstate = readonly ↔ isbuf0) ∧ (pstate ≠ unbuffered ∧ pstate ≠ readonly → bleb = buffered(pstate.lnum))) ∧ err = err0) | A Proof Obligation |
| refine-allocate-ind | isbuf, abs-istore(avol, lpt, istore), abs-gstore(avol, lpt, gstore, ginval), adr = adr0, maxino = m, log = log0, ginval < # lpt, ns = ns0, flash-lpt-cons(lpt0, istore0, gstore0), isbuf → synced(avol), pstate = unbuffered → bleb = nobuffer, pstate = readonly ↔ isbuf0, pstate ≠ unbuffered ∧ pstate ≠ readonly → bleb = buffered(pstate.lnum), inv-journal(log, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, log, gstore, istore, isbuf), lpt-free-unref(lpt), lpt-free-unref(lpt0), freelist-cons(lpt, freelist), log0 = log1, bin-heap-inv(gch, lpt), keyset(gch) = gc-heap(lpt, log0), bufs-log-only(bleb, log0, lpt), # lpt = # avol, ¬ dups(log0), log-group-block(log0, lpt), buf-ro-rw-mode(isbuf0, bleb, lpt, avol), lpt-leb-size(lpt), lpt-leb-size(lpt0), lpt-ram-flash(lpt, lpt0, log0), m0 = LEB_SIZE, awbuf-inv(avol, bleb), # lpt0 = # avol ⊦ ⟪persistence_allocate_ind#(adr0, m, log1, lpt0, ns0, isbuf0; lpt, freelist, avol, bleb; err)⟫ ⟨apersistence_allocate_ind#(adr, istore0, ginval, gstore, gstore0, log, maxino, ns, isbuf; istore, pstate; err0)⟩ ( ( abs-istore(avol, lpt, istore) ∧ abs-gstore(avol, lpt, gstore, ginval) ∧ adr = adr0 ∧ maxino = m ∧ log = log0 ∧ ginval < # lpt ∧ ns = ns0 ∧ flash-lpt-cons(lpt0, istore0, gstore0) ∧ (isbuf → synced(avol)) ∧ (pstate = unbuffered → bleb = nobuffer) ∧ (pstate = readonly ↔ isbuf0) ∧ (pstate ≠ unbuffered ∧ pstate ≠ readonly → bleb = buffered(pstate.lnum))) ∧ err = err0) | A Proof Obligation |
| refine-commit | isbuf, dom remove-refsize0(gstore) ∩ ginval = ∅, abs-istore(avol, lpt, istore), abs-gstore(avol, lpt, gstore, ginval), adr = adr0, maxino = m, log = log0, ginval < # lpt, ns = ns0, flash-lpt-cons(lpt0, istore0, gstore0), isbuf → synced(avol), pstate = unbuffered → bleb = nobuffer, pstate = readonly ↔ isbuf0, pstate ≠ unbuffered ∧ pstate ≠ readonly → bleb = buffered(pstate.lnum), inv-journal(log, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, log, gstore, istore, isbuf), lpt-free-unref(lpt), lpt-free-unref(lpt0), freelist-cons(lpt, freelist), log0 = log1, bin-heap-inv(gch, lpt), keyset(gch) = gc-heap(lpt, log0), bufs-log-only(bleb, log0, lpt), # lpt = # avol, ¬ dups(log0), log-group-block(log0, lpt), buf-ro-rw-mode(isbuf0, bleb, lpt, avol), lpt-leb-size(lpt), lpt-leb-size(lpt0), lpt-ram-flash(lpt, lpt0, log0), m0 = LEB_SIZE, awbuf-inv(avol, bleb), # lpt0 = # avol, ns1 = ns2, adr1 = adr2, m1 = m2 ⊦ ⟪persistence_commit#(adr1, m1; ns1, log0, lpt, freelist, gch, adr0, m, log1, avol, lpt0, ns0, bleb, isbuf0; err)⟫ ⟨apersistence_commit#(adr2, m2, isbuf; ns2, istore, ginval, gstore, adr, istore0, gstore0, log, maxino, ns; pstate, err0)⟩ ( ( abs-istore(avol, lpt, istore) ∧ abs-gstore(avol, lpt, gstore, ginval) ∧ adr = adr0 ∧ maxino = m ∧ log = log0 ∧ ginval < # lpt ∧ ns = ns0 ∧ flash-lpt-cons(lpt0, istore0, gstore0) ∧ (isbuf → synced(avol)) ∧ (pstate = unbuffered → bleb = nobuffer) ∧ (pstate = readonly ↔ isbuf0) ∧ (pstate ≠ unbuffered ∧ pstate ≠ readonly → bleb = buffered(pstate.lnum))) ∧ ns1 = ns2 ∧ err = err0) | A Proof Obligation |
| refine-requires-commit | abs-istore(avol, lpt, istore), abs-gstore(avol, lpt, gstore, ginval), adr = adr0, maxino = m, log = log0, ginval < # lpt, ns = ns0, flash-lpt-cons(lpt0, istore0, gstore0), isbuf → synced(avol), pstate = unbuffered → bleb = nobuffer, pstate = readonly ↔ isbuf0, pstate ≠ unbuffered ∧ pstate ≠ readonly → bleb = buffered(pstate.lnum), inv-journal(log, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, log, gstore, istore, isbuf), lpt-free-unref(lpt), lpt-free-unref(lpt0), freelist-cons(lpt, freelist), log0 = log1, bin-heap-inv(gch, lpt), keyset(gch) = gc-heap(lpt, log0), bufs-log-only(bleb, log0, lpt), # lpt = # avol, ¬ dups(log0), log-group-block(log0, lpt), buf-ro-rw-mode(isbuf0, bleb, lpt, avol), lpt-leb-size(lpt), lpt-leb-size(lpt0), lpt-ram-flash(lpt, lpt0, log0), m0 = LEB_SIZE, awbuf-inv(avol, bleb), # lpt0 = # avol ⊦ ⟪persistence_requires_commit#(adr0, m, log1, avol, lpt0, ns0, bleb, isbuf0; ; isbuf1)⟫ ⟨apersistence_requires_commit#(adr, istore, istore0, ginval, gstore, gstore0, log, maxino, ns, pstate, isbuf; ; isbuf2)⟩ ( ( abs-istore(avol, lpt, istore) ∧ abs-gstore(avol, lpt, gstore, ginval) ∧ adr = adr0 ∧ maxino = m ∧ log = log0 ∧ ginval < # lpt ∧ ns = ns0 ∧ flash-lpt-cons(lpt0, istore0, gstore0) ∧ (isbuf → synced(avol)) ∧ (pstate = unbuffered → bleb = nobuffer) ∧ (pstate = readonly ↔ isbuf0) ∧ (pstate ≠ unbuffered ∧ pstate ≠ readonly → bleb = buffered(pstate.lnum))) ∧ (isbuf1 ↔ isbuf2)) | A Proof Obligation |
| recovery | adr0 = adr1, m0 = m1, log0 = log1, lpt = lpt0, avol ↓ avol0, ns1 = ns2, abs-istore(avol0, lpt1, istore1), abs-gstore(avol0, lpt1, gstore1, ns3), adr2 = adr1, m2 = m1, log2 = log3, ns3 < # lpt1, ns4 = ns2, flash-lpt-cons(lpt0, istore2, gstore2), isbuf0 → synced(avol0), pstate0 = unbuffered → bleb = nobuffer, pstate0 = readonly ↔ isbuf1, pstate0 ≠ unbuffered ∧ pstate0 ≠ readonly → bleb = buffered(pstate0.lnum), synced(avol0), inv-journal(log2, gstore1, gstore2, ns3), inv-index(istore1, istore2), inv-state(pstate0, log2, gstore1, istore1, isbuf0), lpt-free-unref(lpt1), lpt-free-unref(lpt0), freelist-cons(lpt1, log4), log3 = log1, bin-heap-inv(gch, lpt1), keyset(gch) = gc-heap(lpt1, log3), bufs-log-only(bleb, log3, lpt1), # lpt1 = # avol0, ¬ dups(log3), log-group-block(log3, lpt1), buf-ro-rw-mode(isbuf1, bleb, lpt1, avol0), lpt-leb-size(lpt1), lpt-leb-size(lpt0), lpt-ram-flash(lpt1, lpt0, log3), m3 = LEB_SIZE, awbuf-inv(avol0, bleb), # lpt0 = # avol0, adr3 = adr4, m4 = m5, log5 = log6, ns5 = ns6 ⊦ ⟪persistence_recover#(; adr3, m4, log5, ns5, log7, lpt2, freelist, gch0, m6, adr0, m0, log0, avol, lpt, ns1, bleb0, isbuf2; err)⟫ ( ( err = ESUCCESS → (∃ adr, istore, istore0, ginval, gstore, gstore0, log, maxino, ns, pstate, isbuf. ( adr = adr2 ∧ istore = remove-refsize0(crash(istore1, istore2)) ∧ istore0 = istore2 ∧ ginval = ns3 ∧ gstore = crash(gstore1, gstore2, ns3, log2) ∧ gstore0 = gstore2 ∧ log = log2 ∧ maxino = m2 ∧ ns = ns4) ∧ ⟨apersistence_recover#(; adr4, m5, log6, ns6, adr, log, maxino, ns, istore, istore0, ginval, gstore, gstore0; pstate, isbuf, err0)⟩ ( ( abs-istore(avol, lpt2, istore) ∧ abs-gstore(avol, lpt2, gstore, ginval) ∧ adr = adr0 ∧ maxino = m0 ∧ log = log7 ∧ ginval < # lpt2 ∧ ns = ns1 ∧ flash-lpt-cons(lpt, istore0, gstore0) ∧ (isbuf → synced(avol)) ∧ (pstate = unbuffered → bleb0 = nobuffer) ∧ (pstate = readonly ↔ isbuf2) ∧ (pstate ≠ unbuffered ∧ pstate ≠ readonly → bleb0 = buffered(pstate.lnum))) ∧ adr3 = adr4 ∧ m4 = m5 ∧ log5 = log6 ∧ ns5 = ns6 ∧ err = err0))) ∧ ( err ≠ ESUCCESS → (∀ adr, istore, istore0, ns, gstore, gstore0, log, m, ns0, 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 ∧ ns0 = ns7 ∧ pstate = pstate1 ∧ (isbuf ↔ isbuf3) ∧ adr3 = adr4 ∧ m4 = m5 ∧ log5 = log6 ∧ ns5 = ns6 ∧ err = err0)))) | A Proof Obligation |
| initialization | m0 = LEB_SIZE, m1 = m2 ⊦ ⟪persistence_format#(m3, m0, m1; lpt, freelist, gch, adr0, m4, log0, avol, lpt0, ns1, bleb, isbuf0, log1, m5; err)⟫ ( ( err = ESUCCESS → ⟨apersistence_format#(m3, m0, m2; ; adr1, istore1, istore2, ginval, gstore1, gstore2, log2, maxino, ns2, pstate0, isbuf1, err0)⟩ ( ( abs-istore(avol, lpt, istore1) ∧ abs-gstore(avol, lpt, gstore1, ginval) ∧ adr1 = adr0 ∧ maxino = m4 ∧ log2 = log1 ∧ ginval < # lpt ∧ ns2 = ns1 ∧ flash-lpt-cons(lpt0, istore2, gstore2) ∧ (isbuf1 → synced(avol)) ∧ (pstate0 = unbuffered → bleb = nobuffer) ∧ (pstate0 = readonly ↔ isbuf0) ∧ (pstate0 ≠ unbuffered ∧ pstate0 ≠ readonly → bleb = buffered(pstate0.lnum))) ∧ err = err0)) ∧ ( err ≠ ESUCCESS → (∀ adr, istore, istore0, ns, gstore, gstore0, log, m, ns0, pstate, isbuf. ⟨apersistence_format#(m3, m0, m2; ; adr1, istore1, istore2, ginval, gstore1, gstore2, log2, maxino, ns2, pstate0, isbuf1, err0)⟩ ( adr = adr1 ∧ istore = istore1 ∧ istore0 = istore2 ∧ ns = ginval ∧ gstore = gstore1 ∧ gstore0 = gstore2 ∧ log = log2 ∧ m = maxino ∧ ns0 = ns2 ∧ pstate = pstate0 ∧ (isbuf ↔ isbuf1) ∧ err = err0)))) | A Proof Obligation |
| refine-add-gnds | pstate.journal? ∨ pstate = readonly, abs-istore(avol, lpt, istore), abs-gstore(avol, lpt, gstore, ginval), adr = adr0, maxino = m, log = log0, ginval < # lpt, ns = ns0, flash-lpt-cons(lpt0, istore0, gstore0), isbuf → synced(avol), pstate = unbuffered → bleb = nobuffer, pstate = readonly ↔ isbuf0, pstate ≠ unbuffered ∧ pstate ≠ readonly → bleb = buffered(pstate.lnum), inv-journal(log, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, log, gstore, istore, isbuf), lpt-free-unref(lpt), lpt-free-unref(lpt0), freelist-cons(lpt, freelist), log0 = log1, bin-heap-inv(gch, lpt), keyset(gch) = gc-heap(lpt, log0), bufs-log-only(bleb, log0, lpt), # lpt = # avol, ¬ dups(log0), log-group-block(log0, lpt), buf-ro-rw-mode(isbuf0, bleb, lpt, avol), lpt-leb-size(lpt), lpt-leb-size(lpt0), lpt-ram-flash(lpt, lpt0, log0), m0 = LEB_SIZE, awbuf-inv(avol, bleb), # lpt0 = # avol, ax = ax0, gndx = gndx0 ⊦ ⟪persistence_add_gnds#(gndx, log0, m0, adr0, m, log1, lpt0, ns0, bleb; ax, lpt, avol, isbuf0; err)⟫ ⟨apersistence_add_gnds#(gndx0, adr, istore, istore0, ginval, gstore0, log, maxino, ns; ax0, gstore, pstate, isbuf; err0)⟩ ( ( abs-istore(avol, lpt, istore) ∧ abs-gstore(avol, lpt, gstore, ginval) ∧ adr = adr0 ∧ maxino = m ∧ log = log0 ∧ ginval < # lpt ∧ ns = ns0 ∧ flash-lpt-cons(lpt0, istore0, gstore0) ∧ (isbuf → synced(avol)) ∧ (pstate = unbuffered → bleb = nobuffer) ∧ (pstate = readonly ↔ isbuf0) ∧ (pstate ≠ unbuffered ∧ pstate ≠ readonly → bleb = buffered(pstate.lnum))) ∧ ax = ax0 ∧ err = err0) | A Proof Obligation |
| refine-add-ind | pstate.index? ∨ pstate = readonly, abs-istore(avol, lpt, istore), abs-gstore(avol, lpt, gstore, ginval), adr = adr0, maxino = m, log = log0, ginval < # lpt, ns = ns0, flash-lpt-cons(lpt0, istore0, gstore0), isbuf → synced(avol), pstate = unbuffered → bleb = nobuffer, pstate = readonly ↔ isbuf0, pstate ≠ unbuffered ∧ pstate ≠ readonly → bleb = buffered(pstate.lnum), inv-journal(log, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, log, gstore, istore, isbuf), lpt-free-unref(lpt), lpt-free-unref(lpt0), freelist-cons(lpt, freelist), log0 = log1, bin-heap-inv(gch, lpt), keyset(gch) = gc-heap(lpt, log0), bufs-log-only(bleb, log0, lpt), # lpt = # avol, ¬ dups(log0), log-group-block(log0, lpt), buf-ro-rw-mode(isbuf0, bleb, lpt, avol), lpt-leb-size(lpt), lpt-leb-size(lpt0), lpt-ram-flash(lpt, lpt0, log0), m0 = LEB_SIZE, awbuf-inv(avol, bleb), # lpt0 = # avol, adr1 = adr2 ⊦ ⟪persistence_add_ind#(ind, m0, adr0, m, log1, lpt0, ns0, bleb; adr1, lpt, avol, isbuf0; err)⟫ ⟨apersistence_add_ind#(ind, adr, istore0, ginval, gstore, gstore0, log, maxino, ns; adr2, istore, pstate, isbuf; err0)⟩ ( ( abs-istore(avol, lpt, istore) ∧ abs-gstore(avol, lpt, gstore, ginval) ∧ adr = adr0 ∧ maxino = m ∧ log = log0 ∧ ginval < # lpt ∧ ns = ns0 ∧ flash-lpt-cons(lpt0, istore0, gstore0) ∧ (isbuf → synced(avol)) ∧ (pstate = unbuffered → bleb = nobuffer) ∧ (pstate = readonly ↔ isbuf0) ∧ (pstate ≠ unbuffered ∧ pstate ≠ readonly → bleb = buffered(pstate.lnum))) ∧ adr1 = adr2 ∧ err = err0) | A Proof Obligation |
| refine-sync | abs-istore(avol, lpt, istore), abs-gstore(avol, lpt, gstore, ginval), adr = adr0, maxino = m, log = log0, ginval < # lpt, ns = ns0, flash-lpt-cons(lpt0, istore0, gstore0), isbuf → synced(avol), pstate = unbuffered → bleb = nobuffer, pstate = readonly ↔ isbuf0, pstate ≠ unbuffered ∧ pstate ≠ readonly → bleb = buffered(pstate.lnum), inv-journal(log, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, log, gstore, istore, isbuf), lpt-free-unref(lpt), lpt-free-unref(lpt0), freelist-cons(lpt, freelist), log0 = log1, bin-heap-inv(gch, lpt), keyset(gch) = gc-heap(lpt, log0), bufs-log-only(bleb, log0, lpt), # lpt = # avol, ¬ dups(log0), log-group-block(log0, lpt), buf-ro-rw-mode(isbuf0, bleb, lpt, avol), lpt-leb-size(lpt), lpt-leb-size(lpt0), lpt-ram-flash(lpt, lpt0, log0), m0 = LEB_SIZE, awbuf-inv(avol, bleb), # lpt0 = # avol ⊦ ⟪persistence_sync#(m0, adr0, m, log1, lpt0, ns0, bleb; lpt, avol, isbuf0; err)⟫ ⟨apersistence_sync#(adr, istore, istore0, ginval, gstore, gstore0, log, maxino, ns; pstate, isbuf; err0)⟩ ( ( abs-istore(avol, lpt, istore) ∧ abs-gstore(avol, lpt, gstore, ginval) ∧ adr = adr0 ∧ maxino = m ∧ log = log0 ∧ ginval < # lpt ∧ ns = ns0 ∧ flash-lpt-cons(lpt0, istore0, gstore0) ∧ (isbuf → synced(avol)) ∧ (pstate = unbuffered → bleb = nobuffer) ∧ (pstate = readonly ↔ isbuf0) ∧ (pstate ≠ unbuffered ∧ pstate ≠ readonly → bleb = buffered(pstate.lnum))) ∧ err = err0) | A Proof Obligation |
| refine-get-block-free-size | abs-istore(avol, lpt, istore), abs-gstore(avol, lpt, gstore, ginval), adr = adr0, maxino = m, log = log0, ginval < # lpt, ns = ns0, flash-lpt-cons(lpt0, istore0, gstore0), isbuf → synced(avol), pstate = unbuffered → bleb = nobuffer, pstate = readonly ↔ isbuf0, pstate ≠ unbuffered ∧ pstate ≠ readonly → bleb = buffered(pstate.lnum), inv-journal(log, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, log, gstore, istore, isbuf), lpt-free-unref(lpt), lpt-free-unref(lpt0), freelist-cons(lpt, freelist), log0 = log1, bin-heap-inv(gch, lpt), keyset(gch) = gc-heap(lpt, log0), bufs-log-only(bleb, log0, lpt), # lpt = # avol, ¬ dups(log0), log-group-block(log0, lpt), buf-ro-rw-mode(isbuf0, bleb, lpt, avol), lpt-leb-size(lpt), lpt-leb-size(lpt0), lpt-ram-flash(lpt, lpt0, log0), m0 = LEB_SIZE, awbuf-inv(avol, bleb), # lpt0 = # avol ⊦ ⟪persistence_get_block_free_size#(lpt, m0, adr0, m, log1, avol, lpt0, ns0, bleb, isbuf0; ; n)⟫ ⟨apersistence_get_block_free_size#(adr, istore, istore0, ginval, gstore, gstore0, log, maxino, ns, pstate, isbuf; ; n0)⟩ ( ( abs-istore(avol, lpt, istore) ∧ abs-gstore(avol, lpt, gstore, ginval) ∧ adr = adr0 ∧ maxino = m ∧ log = log0 ∧ ginval < # lpt ∧ ns = ns0 ∧ flash-lpt-cons(lpt0, istore0, gstore0) ∧ (isbuf → synced(avol)) ∧ (pstate = unbuffered → bleb = nobuffer) ∧ (pstate = readonly ↔ isbuf0) ∧ (pstate ≠ unbuffered ∧ pstate ≠ readonly → bleb = buffered(pstate.lnum))) ∧ n = n0) | A Proof Obligation |
| synced | isbuf, abs-istore(avol, lpt, istore), abs-gstore(avol, lpt, gstore, ginval), adr = adr0, maxino = m, log = log0, ginval < # lpt, ns = ns0, flash-lpt-cons(lpt0, istore0, gstore0), isbuf → synced(avol), pstate = unbuffered → bleb = nobuffer, pstate = readonly ↔ isbuf0, pstate ≠ unbuffered ∧ pstate ≠ readonly → bleb = buffered(pstate.lnum), inv-journal(log, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, log, gstore, istore, isbuf), lpt-free-unref(lpt), lpt-free-unref(lpt0), freelist-cons(lpt, freelist), log0 = log1, bin-heap-inv(gch, lpt), keyset(gch) = gc-heap(lpt, log0), bufs-log-only(bleb, log0, lpt), # lpt = # avol, ¬ dups(log0), log-group-block(log0, lpt), buf-ro-rw-mode(isbuf0, bleb, lpt, avol), lpt-leb-size(lpt), lpt-leb-size(lpt0), lpt-ram-flash(lpt, lpt0, log0), m0 = LEB_SIZE ⊦ synced(avol) | A Proof Obligation |
| refine-is-log-empty | abs-istore(avol, lpt, istore), abs-gstore(avol, lpt, gstore, ginval), adr = adr0, maxino = m, log = log0, ginval < # lpt, ns = ns0, flash-lpt-cons(lpt0, istore0, gstore0), isbuf → synced(avol), pstate = unbuffered → bleb = nobuffer, pstate = readonly ↔ isbuf0, pstate ≠ unbuffered ∧ pstate ≠ readonly → bleb = buffered(pstate.lnum), inv-journal(log, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, log, gstore, istore, isbuf), lpt-free-unref(lpt), lpt-free-unref(lpt0), freelist-cons(lpt, freelist), log0 = log1, bin-heap-inv(gch, lpt), keyset(gch) = gc-heap(lpt, log0), bufs-log-only(bleb, log0, lpt), # lpt = # avol, ¬ dups(log0), log-group-block(log0, lpt), buf-ro-rw-mode(isbuf0, bleb, lpt, avol), lpt-leb-size(lpt), lpt-leb-size(lpt0), lpt-ram-flash(lpt, lpt0, log0), m0 = LEB_SIZE, awbuf-inv(avol, bleb), # lpt0 = # avol ⊦ ⟪persistence_is_log_empty#(log0; ; empty?)⟫ ⟨apersistence_is_log_empty#(adr, istore, istore0, ginval, gstore, gstore0, log, maxino, ns, pstate, isbuf; ; isbuf1)⟩ ( ( abs-istore(avol, lpt, istore) ∧ abs-gstore(avol, lpt, gstore, ginval) ∧ adr = adr0 ∧ maxino = m ∧ log = log0 ∧ ginval < # lpt ∧ ns = ns0 ∧ flash-lpt-cons(lpt0, istore0, gstore0) ∧ (isbuf → synced(avol)) ∧ (pstate = unbuffered → bleb = nobuffer) ∧ (pstate = readonly ↔ isbuf0) ∧ (pstate ≠ unbuffered ∧ pstate ≠ readonly → bleb = buffered(pstate.lnum))) ∧ (empty? ↔ isbuf1)) | A Proof Obligation |
| refine-is-readonly | abs-istore(avol, lpt, istore), abs-gstore(avol, lpt, gstore, ginval), adr = adr0, maxino = m, log = log0, ginval < # lpt, ns = ns0, flash-lpt-cons(lpt0, istore0, gstore0), isbuf → synced(avol), pstate = unbuffered → bleb = nobuffer, pstate = readonly ↔ isbuf0, pstate ≠ unbuffered ∧ pstate ≠ readonly → bleb = buffered(pstate.lnum), inv-journal(log, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, log, gstore, istore, isbuf), lpt-free-unref(lpt), lpt-free-unref(lpt0), freelist-cons(lpt, freelist), log0 = log1, bin-heap-inv(gch, lpt), keyset(gch) = gc-heap(lpt, log0), bufs-log-only(bleb, log0, lpt), # lpt = # avol, ¬ dups(log0), log-group-block(log0, lpt), buf-ro-rw-mode(isbuf0, bleb, lpt, avol), lpt-leb-size(lpt), lpt-leb-size(lpt0), lpt-ram-flash(lpt, lpt0, log0), m0 = LEB_SIZE, awbuf-inv(avol, bleb), # lpt0 = # avol ⊦ ⟪persistence_is_readonly#(adr0, m, log1, avol, lpt0, ns0, bleb, isbuf0; ; isbuf1)⟫ ⟨apersistence_is_readonly#(adr, istore, istore0, ginval, gstore, gstore0, log, maxino, ns, pstate, isbuf; ; isbuf2)⟩ ( ( abs-istore(avol, lpt, istore) ∧ abs-gstore(avol, lpt, gstore, ginval) ∧ adr = adr0 ∧ maxino = m ∧ log = log0 ∧ ginval < # lpt ∧ ns = ns0 ∧ flash-lpt-cons(lpt0, istore0, gstore0) ∧ (isbuf → synced(avol)) ∧ (pstate = unbuffered → bleb = nobuffer) ∧ (pstate = readonly ↔ isbuf0) ∧ (pstate ≠ unbuffered ∧ pstate ≠ readonly → bleb = buffered(pstate.lnum))) ∧ (isbuf1 ↔ isbuf2)) | A Proof Obligation |
| refine-get-leb-size | abs-istore(avol, lpt, istore), abs-gstore(avol, lpt, gstore, ginval), adr = adr0, maxino = m, log = log0, ginval < # lpt, ns = ns0, flash-lpt-cons(lpt0, istore0, gstore0), isbuf → synced(avol), pstate = unbuffered → bleb = nobuffer, pstate = readonly ↔ isbuf0, pstate ≠ unbuffered ∧ pstate ≠ readonly → bleb = buffered(pstate.lnum), inv-journal(log, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, log, gstore, istore, isbuf), lpt-free-unref(lpt), lpt-free-unref(lpt0), freelist-cons(lpt, freelist), log0 = log1, bin-heap-inv(gch, lpt), keyset(gch) = gc-heap(lpt, log0), bufs-log-only(bleb, log0, lpt), # lpt = # avol, ¬ dups(log0), log-group-block(log0, lpt), buf-ro-rw-mode(isbuf0, bleb, lpt, avol), lpt-leb-size(lpt), lpt-leb-size(lpt0), lpt-ram-flash(lpt, lpt0, log0), m0 = LEB_SIZE, awbuf-inv(avol, bleb), # lpt0 = # avol ⊦ ⟪persistence_get_leb_size#(m0; ; n)⟫ ⟨apersistence_get_leb_size#(adr, istore, istore0, ginval, gstore, gstore0, log, maxino, ns, pstate, isbuf; ; n0)⟩ ( ( abs-istore(avol, lpt, istore) ∧ abs-gstore(avol, lpt, gstore, ginval) ∧ adr = adr0 ∧ maxino = m ∧ log = log0 ∧ ginval < # lpt ∧ ns = ns0 ∧ flash-lpt-cons(lpt0, istore0, gstore0) ∧ (isbuf → synced(avol)) ∧ (pstate = unbuffered → bleb = nobuffer) ∧ (pstate = readonly ↔ isbuf0) ∧ (pstate ≠ unbuffered ∧ pstate ≠ readonly → bleb = buffered(pstate.lnum))) ∧ n = n0) | A Proof Obligation |
| fwd-in-gstore-lpt | ⊦ n ∈ gstore ∧ abs-gstore(avol, lpt, gstore, ginval) → n < # lpt ∧ lpt[n].ref-size = gstore[n].ref-size ∧ lpt[n].flags = LP_GROUP_NODES | A User Theorem |
| fwd-in-istore-lpt | ⊦ n ∈ istore ∧ abs-istore(avol, lpt, istore) → n < # lpt ∧ lpt[n].ref-size = istore[n].ref-size ∧ lpt[n].flags = LP_INDEX_NODES | A User Theorem |