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-get-volume-size | abs(avol, bleb, wbuf, avol0, rofs), bleb0 = bleb, adr = adr0, m = m0, plog = plog0, lpt = lpt0, ns = ns0, rofs0 ↔ rofs, awbuf-inv(avol, bleb0), # lpt = # avol, wbuf-cons(bleb, wbuf, avol0, rofs), m1 = EB_PAGE_SIZE, ebm-vol-inv(avol0), # lpt0 = # avol0 ⊦ ⟪wbuf_get_volume_size#(adr0, m0, plog0, avol0, lpt0, ns0; ; n)⟫ ⟨awbuf_get_volume_size#(adr, m, plog, avol, lpt, ns, bleb0, rofs0; ; n0)⟩ ((abs(avol, bleb, wbuf, avol0, rofs) ∧ bleb0 = bleb ∧ adr = adr0 ∧ m = m0 ∧ plog = plog0 ∧ lpt = lpt0 ∧ ns = ns0 ∧ (rofs0 ↔ rofs)) ∧ n = n0) | A Proof Obligation |
| refine-move-buf | bleb = buffered(m) ∨ (bleb = nobuffer ∨ is-aligned(# avol[bleb.leb].data, EB_PAGE_SIZE)) ∧ m < # avol ∧ avol[m].mapped? ∧ m0 = # avol[m].data, abs(avol, bleb0, wbuf, avol0, rofs), bleb = bleb0, adr = adr0, m1 = m2, plog = plog0, lpt = lpt0, ns = ns0, rofs0 ↔ rofs, awbuf-inv(avol, bleb), # lpt = # avol, wbuf-cons(bleb0, wbuf, avol0, rofs), m3 = EB_PAGE_SIZE, ebm-vol-inv(avol0), # lpt0 = # avol0 ⊦ ⟪wbuf_move_buf#(m, m0, rofs, avol0; bleb0, wbuf; err)⟫ ⟨awbuf_move_buf#(m, m0, adr, m1, plog, avol, lpt, ns, rofs0; bleb; err0)⟩ ( (abs(avol, bleb0, wbuf, avol0, rofs) ∧ bleb = bleb0 ∧ adr = adr0 ∧ m1 = m2 ∧ plog = plog0 ∧ lpt = lpt0 ∧ ns = ns0 ∧ (rofs0 ↔ rofs)) ∧ err = err0) | A Proof Obligation |
| refine-write-buf | bleb ≠ nobuffer, # avol[bleb.leb].data + n ≤ LEB_SIZE, n ≤ # buf, abs(avol, bleb0, wbuf, avol0, rofs), bleb = bleb0, adr = adr0, m = m0, plog = plog0, lpt = lpt0, ns = ns0, rofs0 ↔ rofs, awbuf-inv(avol, bleb), # lpt = # avol, wbuf-cons(bleb0, wbuf, avol0, rofs), m1 = EB_PAGE_SIZE, ebm-vol-inv(avol0), # lpt0 = # avol0 ⊦ ⟪wbuf_write_buf#(n, buf, bleb0, m1, adr0, m0, plog0, lpt0, ns0; wbuf, rofs, avol0; err)⟫ ⟨awbuf_write_buf#(n, buf, adr, m, plog, lpt, ns, bleb; avol, rofs0; err0)⟩ ( (abs(avol, bleb0, wbuf, avol0, rofs) ∧ bleb = bleb0 ∧ adr = adr0 ∧ m = m0 ∧ plog = plog0 ∧ lpt = lpt0 ∧ ns = ns0 ∧ (rofs0 ↔ rofs)) ∧ err = err0) | A Proof Obligation |
| refine-commit | synced(avol), # lpt = # avol, abs(avol, bleb, wbuf, avol0, rofs), bleb0 = bleb, adr = adr0, m = m0, plog = plog0, lpt0 = lpt1, ns = ns0, rofs0 ↔ rofs, awbuf-inv(avol, bleb0), # lpt0 = # avol, wbuf-cons(bleb, wbuf, avol0, rofs), m1 = EB_PAGE_SIZE, ebm-vol-inv(avol0), # lpt1 = # avol0, ns1 = ns2, adr1 = adr2, m2 = m3 ⊦ ⟪wbuf_commit#(lpt, adr1, m2, avol0; ns1, adr0, m0, plog0, lpt1, ns0, rofs; err)⟫ ⟨awbuf_commit#(lpt, adr2, m3, avol, bleb0; ns2, adr, m, plog, lpt0, ns, rofs0; err0)⟩ ( (abs(avol, bleb, wbuf, avol0, rofs) ∧ bleb0 = bleb ∧ adr = adr0 ∧ m = m0 ∧ plog = plog0 ∧ lpt0 = lpt1 ∧ ns = ns0 ∧ (rofs0 ↔ rofs)) ∧ ns1 = ns2 ∧ err = err0) | A Proof Obligation |
| refine-requires-commit | abs(avol, bleb, wbuf, avol0, rofs), bleb0 = bleb, adr = adr0, m = m0, plog = plog0, lpt = lpt0, ns = ns0, rofs0 ↔ rofs, awbuf-inv(avol, bleb0), # lpt = # avol, wbuf-cons(bleb, wbuf, avol0, rofs), m1 = EB_PAGE_SIZE, ebm-vol-inv(avol0), # lpt0 = # avol0 ⊦ ⟪wbuf_requires_commit#(adr0, m0, plog0, avol0, lpt0, ns0; ; rofs1)⟫ ⟨awbuf_requires_commit#(adr, m, plog, avol, lpt, ns, bleb0, rofs0; ; rofs2)⟩ ( (abs(avol, bleb, wbuf, avol0, rofs) ∧ bleb0 = bleb ∧ adr = adr0 ∧ m = m0 ∧ plog = plog0 ∧ lpt = lpt0 ∧ ns = ns0 ∧ (rofs0 ↔ rofs)) ∧ (rofs1 ↔ rofs2)) | A Proof Obligation |
| refine-add-log-leb | m < # avol, avol[m].mapped?, m0 = # avol[m].data, synced(avol), abs(avol, bleb, wbuf, avol0, rofs), bleb0 = bleb, adr = adr0, m1 = m2, plog = plog0, lpt = lpt0, ns = ns0, rofs0 ↔ rofs, awbuf-inv(avol, bleb0), # lpt = # avol, wbuf-cons(bleb, wbuf, avol0, rofs), m3 = EB_PAGE_SIZE, ebm-vol-inv(avol0), # lpt0 = # avol0 ⊦ ⟪wbuf_add_log_leb#(m, m0, rofs, adr0, m2, avol0, lpt0, ns0; bleb, wbuf, plog0; err)⟫ ⟨awbuf_add_log_leb#(m, m0, adr, m1, avol, lpt, ns, rofs0; plog, bleb0; err0)⟩ ( (abs(avol, bleb, wbuf, avol0, rofs) ∧ bleb0 = bleb ∧ adr = adr0 ∧ m1 = m2 ∧ plog = plog0 ∧ lpt = lpt0 ∧ ns = ns0 ∧ (rofs0 ↔ rofs)) ∧ err = err0) | A Proof Obligation |
| refine-read-buf | m < # avol, n ≤ # buf, m0 + n ≤ LEB_SIZE, avol[m].mapped?, abs(avol, bleb, wbuf, avol0, rofs), bleb0 = bleb, adr = adr0, m1 = m2, plog = plog0, lpt = lpt0, ns = ns0, rofs0 ↔ rofs, awbuf-inv(avol, bleb0), # lpt = # avol, wbuf-cons(bleb, wbuf, avol0, rofs), m3 = EB_PAGE_SIZE, ebm-vol-inv(avol0), # lpt0 = # avol0, buf = buf0 ⊦ ⟪wbuf_read_buf#(m, m0, n, bleb, wbuf, adr0, m2, plog0, avol0, lpt0, ns0; buf; err)⟫ ⟨awbuf_read_buf#(m, m0, n, adr, m1, plog, avol, lpt, ns, bleb0, rofs0; buf0; err0)⟩ ( (abs(avol, bleb, wbuf, avol0, rofs) ∧ bleb0 = bleb ∧ adr = adr0 ∧ m1 = m2 ∧ plog = plog0 ∧ lpt = lpt0 ∧ ns = ns0 ∧ (rofs0 ↔ rofs)) ∧ buf = buf0 ∧ err = err0) | A Proof Obligation |
| refine-remap | synced(avol), m < # avol, buffered(m) ≠ bleb, abs(avol, bleb0, wbuf, avol0, rofs), bleb = bleb0, adr = adr0, m0 = m1, plog = plog0, lpt = lpt0, ns = ns0, rofs0 ↔ rofs, awbuf-inv(avol, bleb), # lpt = # avol, wbuf-cons(bleb0, wbuf, avol0, rofs), m2 = EB_PAGE_SIZE, ebm-vol-inv(avol0), # lpt0 = # avol0 ⊦ ⟪wbuf_remap#(m, bleb0, adr0, m1, plog0, lpt0, ns0; avol0; err)⟫ ⟨awbuf_remap#(m, adr, m0, plog, lpt, ns, bleb, rofs0; avol; err0)⟩ ( (abs(avol, bleb0, wbuf, avol0, rofs) ∧ bleb = bleb0 ∧ adr = adr0 ∧ m0 = m1 ∧ plog = plog0 ∧ lpt = lpt0 ∧ ns = ns0 ∧ (rofs0 ↔ rofs)) ∧ err = err0) | A Proof Obligation |
| refine-unmap | synced(avol), m < # avol, buffered(m) ≠ bleb, abs(avol, bleb0, wbuf, avol0, rofs), bleb = bleb0, adr = adr0, m0 = m1, plog = plog0, lpt = lpt0, ns = ns0, rofs0 ↔ rofs, awbuf-inv(avol, bleb), # lpt = # avol, wbuf-cons(bleb0, wbuf, avol0, rofs), m2 = EB_PAGE_SIZE, ebm-vol-inv(avol0), # lpt0 = # avol0 ⊦ ⟪wbuf_unmap#(m, bleb0, adr0, m1, plog0, lpt0, ns0; avol0)⟫ ⟨awbuf_unmap#(m, adr, m0, plog, lpt, ns, bleb, rofs0; avol)⟩ (abs(avol, bleb0, wbuf, avol0, rofs) ∧ bleb = bleb0 ∧ adr = adr0 ∧ m0 = m1 ∧ plog = plog0 ∧ lpt = lpt0 ∧ ns = ns0 ∧ (rofs0 ↔ rofs)) | A Proof Obligation |
| initialization | # lpt0 = m0, m1 = LEB_SIZE, adr0 = adr1, m2 = m3 ⊦ ⟪wbuf_format#(m0, m1, lpt0, adr0, m2; wbuf, m4, adr2, m5, plog0, avol0, lpt1, ns0, bleb0, rofs0; err)⟫ ( ( err = ESUCCESS → ⟨awbuf_format#(m0, m1, lpt0, adr1, m3; ; adr3, m6, plog1, avol1, lpt2, ns1, bleb1, rofs1, err0)⟩ ( ( abs(avol1, bleb0, wbuf, avol0, rofs0) ∧ bleb1 = bleb0 ∧ adr3 = adr2 ∧ m6 = m5 ∧ plog1 = plog0 ∧ lpt2 = lpt1 ∧ ns1 = ns0 ∧ (rofs1 ↔ rofs0)) ∧ err = err0)) ∧ ( err ≠ ESUCCESS → (∀ adr, m, plog, avol, lpt, ns, bleb, rofs. ⟨awbuf_format#(m0, m1, lpt0, adr1, m3; ; adr3, m6, plog1, avol1, lpt2, ns1, bleb1, rofs1, err0)⟩ (adr = adr3 ∧ m = m6 ∧ plog = plog1 ∧ avol = avol1 ∧ lpt = lpt2 ∧ ns = ns1 ∧ bleb = bleb1 ∧ (rofs ↔ rofs1) ∧ err = err0)))) | A Proof Obligation |
| recovery | adr0 = adr1, m0 = m1, plog0 = plog1, lpt0 = lpt1, avol0 ⊆ avol1, ns0 = ns1, abs(avol2, bleb0, wbuf, avol0, rofs0), bleb1 = bleb0, adr2 = adr1, m2 = m1, plog2 = plog1, lpt2 = lpt1, ns2 = ns1, rofs1 ↔ rofs0, awbuf-inv(avol2, bleb1), # lpt2 = # avol2, wbuf-cons(bleb0, wbuf, avol0, rofs0), m3 = EB_PAGE_SIZE, ebm-vol-inv(avol0), # lpt1 = # avol0, adr3 = adr4, m4 = m5, ns3 = ns4, log = plog3, lpt3 = lpt4 ⊦ ⟪wbuf_recover#(; adr3, m4, ns3, log, lpt3, wbuf0, m6, adr0, m0, plog0, avol1, lpt0, ns0, bleb2, rofs2; err)⟫ ( ( err = ESUCCESS → (∃ adr, m, plog, avol, lpt, ns, bleb, rofs. (adr = adr2 ∧ m = m2 ∧ plog = plog2 ∧ lpt = lpt2 ∧ avol ↓ avol2 ∧ ns = ns2) ∧ ⟨awbuf_recover#(; adr4, m5, ns4, plog3, lpt4, adr, m, plog, lpt, ns, avol; bleb, rofs, err0)⟩ ( ( abs(avol, bleb2, wbuf0, avol1, rofs2) ∧ bleb = bleb2 ∧ adr = adr0 ∧ m = m0 ∧ plog = plog0 ∧ lpt = lpt0 ∧ ns = ns0 ∧ (rofs ↔ rofs2)) ∧ adr3 = adr4 ∧ m4 = m5 ∧ ns3 = ns4 ∧ log = plog3 ∧ lpt3 = lpt4 ∧ err = err0))) ∧ ( err ≠ ESUCCESS → (∀ adr, m, plog, avol, lpt, ns, bleb, rofs. ⟨awbuf_recover#(; adr4, m5, ns4, plog3, lpt4, adr5, m7, plog4, lpt5, ns5, avol3; bleb3, rofs3, err0)⟩ ( adr = adr5 ∧ m = m7 ∧ plog = plog4 ∧ avol = avol3 ∧ lpt = lpt5 ∧ ns = ns5 ∧ bleb = bleb3 ∧ (rofs ↔ rofs3) ∧ adr3 = adr4 ∧ m4 = m5 ∧ ns3 = ns4 ∧ log = plog3 ∧ lpt3 = lpt4 ∧ err = err0)))) | A Proof Obligation |
| refine-get-leb-size | abs(avol, bleb, wbuf, avol0, rofs), bleb0 = bleb, adr = adr0, m = m0, plog = plog0, lpt = lpt0, ns = ns0, rofs0 ↔ rofs, awbuf-inv(avol, bleb0), # lpt = # avol, wbuf-cons(bleb, wbuf, avol0, rofs), m1 = EB_PAGE_SIZE, ebm-vol-inv(avol0), # lpt0 = # avol0 ⊦ ⟪wbuf_get_leb_size#(adr0, m0, plog0, avol0, lpt0, ns0; ; n)⟫ ⟨awbuf_get_leb_size#(adr, m, plog, avol, lpt, ns, bleb0, rofs0; ; n0)⟩ ((abs(avol, bleb, wbuf, avol0, rofs) ∧ bleb0 = bleb ∧ adr = adr0 ∧ m = m0 ∧ plog = plog0 ∧ lpt = lpt0 ∧ ns = ns0 ∧ (rofs0 ↔ rofs)) ∧ n = n0) | A Proof Obligation |
| refine-get-page-size | abs(avol, bleb, wbuf, avol0, rofs), bleb0 = bleb, adr = adr0, m = m0, plog = plog0, lpt = lpt0, ns = ns0, rofs0 ↔ rofs, awbuf-inv(avol, bleb0), # lpt = # avol, wbuf-cons(bleb, wbuf, avol0, rofs), m1 = EB_PAGE_SIZE, ebm-vol-inv(avol0), # lpt0 = # avol0 ⊦ ⟪wbuf_get_page_size#(m1; ; n)⟫ ⟨awbuf_get_page_size#(adr, m, plog, avol, lpt, ns, bleb0, rofs0; ; n0)⟩ ((abs(avol, bleb, wbuf, avol0, rofs) ∧ bleb0 = bleb ∧ adr = adr0 ∧ m = m0 ∧ plog = plog0 ∧ lpt = lpt0 ∧ ns = ns0 ∧ (rofs0 ↔ rofs)) ∧ n = n0) | A Proof Obligation |
| refine-destroy-buf | synced(avol), abs(avol, bleb, wbuf, avol0, rofs), bleb0 = bleb, adr = adr0, m = m0, plog = plog0, lpt = lpt0, ns = ns0, rofs0 ↔ rofs, awbuf-inv(avol, bleb0), # lpt = # avol, wbuf-cons(bleb, wbuf, avol0, rofs), m1 = EB_PAGE_SIZE, ebm-vol-inv(avol0), # lpt0 = # avol0 ⊦ ⟪wbuf_destroy_buf#(rofs; bleb; err)⟫ ⟨awbuf_destroy_buf#(adr, m, plog, avol, lpt, ns, rofs0; bleb0; err0)⟩ ( (abs(avol, bleb, wbuf, avol0, rofs) ∧ bleb0 = bleb ∧ adr = adr0 ∧ m = m0 ∧ plog = plog0 ∧ lpt = lpt0 ∧ ns = ns0 ∧ (rofs0 ↔ rofs)) ∧ err = err0) | A Proof Obligation |
| refine-get-buf | abs(avol, bleb, wbuf, avol0, rofs), bleb0 = bleb, adr = adr0, m = m0, plog = plog0, lpt = lpt0, ns = ns0, rofs0 ↔ rofs, awbuf-inv(avol, bleb0), # lpt = # avol, wbuf-cons(bleb, wbuf, avol0, rofs), m1 = EB_PAGE_SIZE, ebm-vol-inv(avol0), # lpt0 = # avol0 ⊦ ⟪wbuf_get_buf#(bleb; ; bleb1)⟫ ⟨awbuf_get_buf#(adr, m, plog, avol, lpt, ns, bleb0, rofs0; ; bleb2)⟩ ( (abs(avol, bleb, wbuf, avol0, rofs) ∧ bleb0 = bleb ∧ adr = adr0 ∧ m = m0 ∧ plog = plog0 ∧ lpt = lpt0 ∧ ns = ns0 ∧ (rofs0 ↔ rofs)) ∧ bleb1 = bleb2) | A Proof Obligation |
| refine-is-readonly | abs(avol, bleb, wbuf, avol0, rofs), bleb0 = bleb, adr = adr0, m = m0, plog = plog0, lpt = lpt0, ns = ns0, rofs0 ↔ rofs, awbuf-inv(avol, bleb0), # lpt = # avol, wbuf-cons(bleb, wbuf, avol0, rofs), m1 = EB_PAGE_SIZE, ebm-vol-inv(avol0), # lpt0 = # avol0 ⊦ ⟪wbuf_is_readonly#(rofs; ; rofs1)⟫ ⟨awbuf_is_readonly#(adr, m, plog, avol, lpt, ns, bleb0, rofs0; ; rofs2)⟩ ( (abs(avol, bleb, wbuf, avol0, rofs) ∧ bleb0 = bleb ∧ adr = adr0 ∧ m = m0 ∧ plog = plog0 ∧ lpt = lpt0 ∧ ns = ns0 ∧ (rofs0 ↔ rofs)) ∧ (rofs1 ↔ rofs2)) | A Proof Obligation |
| synced | synced(avol), abs(avol, bleb, wbuf, avol0, rofs), bleb0 = bleb, adr = adr0, m = m0, plog = plog0, lpt = lpt0, ns = ns0, rofs0 ↔ rofs, awbuf-inv(avol, bleb0), # lpt = # avol, wbuf-cons(bleb, wbuf, avol0, rofs), m1 = EB_PAGE_SIZE ⊦ true | A Proof Obligation |
| refine-enter-readonly | abs(avol, bleb, wbuf, avol0, rofs), bleb0 = bleb, adr = adr0, m = m0, plog = plog0, lpt = lpt0, ns = ns0, rofs0 ↔ rofs, awbuf-inv(avol, bleb0), # lpt = # avol, wbuf-cons(bleb, wbuf, avol0, rofs), m1 = EB_PAGE_SIZE, ebm-vol-inv(avol0), # lpt0 = # avol0 ⊦ ⟪wbuf_enter_readonly#(; ; rofs)⟫ ⟨awbuf_enter_readonly#(adr, m, plog, avol, lpt, ns, bleb0; ; rofs0)⟩ (abs(avol, bleb, wbuf, avol0, rofs) ∧ bleb0 = bleb ∧ adr = adr0 ∧ m = m0 ∧ plog = plog0 ∧ lpt = lpt0 ∧ ns = ns0 ∧ (rofs0 ↔ rofs)) | A Proof Obligation |
| abs-buffered | n < # avol0 ⊦ abs(avol0, buffered(n), mkwbuf(buf, m0, m1), avol1, false) ∧ avol1[n] = mapped(buf1) → avol0[n] = mapped(buf1 + subarray(buf, 0, m1)) | A User Theorem |
| abs-unbuffered | n < # avol0 ⊦ abs(avol0, bleb, wbuf, avol1, rofs) ∧ avol1[n] = mapped(buf) ∧ bleb ≠ buffered(n) → avol0[n] = mapped(buf) | A User Theorem |
| at-append-cut | ⊦ n < # buf0 → (buf0 + buf1)[n] = buf0[n] | A User Theorem |
| mod-to-aligndown-minus | ⊦ m ≠ 0 → n % m = n - align↓(n, m) | A User Theorem |
| nat0 | ⊦ n0 = n1 + n → (n1 + m ≤ n0 ↔ m ≤ n) | A User Theorem |
| nat1 | ⊦ n0 = n1 + n → (n0 ≤ n1 + m ↔ n ≤ m) | A User Theorem |