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-commit | # lpt = # avol, m = sb.maxino, adr = sb.indexaddr, # avol0 = sb.main + # avol, avol = subarray(avol0, sb.main, # avol0 - sb.main), is-encoded(plog, avol0[sb.log].data), is-encoded(lpt0, lebs(avol0, sb.lpt, lptlebs(# avol, LEB_SIZE))), is-encoded-pad(ns, sb.orphsize, avol0[sb.orph].data), ebm-vol-inv(avol), # lpt0 = # avol, ∃ lpt, log, orphans. persistence-io-inv(sb, logoff, avol0, lpt, log, orphans), m0 = EB_PAGE_SIZE, m1 = LEB_SIZE, ebm-vol-inv(avol0), orphans = ns0, adr0 = adr1, m2 = m3 ⊦ ⟪persistence_io_commit#(lpt, adr0, m2, m0, m1; orphans, sb, avol0, logoff; err)⟫ ⟨apersistence_io_commit#(lpt, adr1, m3, avol; ns0, adr, m, plog, lpt0, ns; err0)⟩ ( ( m = sb.maxino ∧ adr = sb.indexaddr ∧ # avol0 = sb.main + # avol ∧ avol = subarray(avol0, sb.main, # avol0 - sb.main) ∧ is-encoded(plog, avol0[sb.log].data) ∧ is-encoded(lpt0, lebs(avol0, sb.lpt, lptlebs(# avol, LEB_SIZE))) ∧ is-encoded-pad(ns, sb.orphsize, avol0[sb.orph].data)) ∧ orphans = ns0 ∧ err = err0) | A Proof Obligation |
| refine-requires-commit | m = sb.maxino, adr = sb.indexaddr, # avol = sb.main + # avol0, avol0 = subarray(avol, sb.main, # avol - sb.main), is-encoded(plog, avol[sb.log].data), is-encoded(lpt, lebs(avol, sb.lpt, lptlebs(# avol0, LEB_SIZE))), is-encoded-pad(ns, sb.orphsize, avol[sb.orph].data), ebm-vol-inv(avol0), # lpt = # avol0, ∃ lpt0, log, orphans. persistence-io-inv(sb, logoff, avol, lpt0, log, orphans), m0 = EB_PAGE_SIZE, m1 = LEB_SIZE, ebm-vol-inv(avol) ⊦ ⟪persistence_io_requires_commit#(logoff, m1; ; boolvar)⟫ ⟨apersistence_io_requires_commit#(adr, m, plog, avol0, lpt, ns; ; boolvar0)⟩ ( ( m = sb.maxino ∧ adr = sb.indexaddr ∧ # avol = sb.main + # avol0 ∧ avol0 = subarray(avol, sb.main, # avol - sb.main) ∧ is-encoded(plog, avol[sb.log].data) ∧ is-encoded(lpt, lebs(avol, sb.lpt, lptlebs(# avol0, LEB_SIZE))) ∧ is-encoded-pad(ns, sb.orphsize, avol[sb.orph].data)) ∧ (boolvar ↔ boolvar0)) | A Proof Obligation |
| refine-add-log-leb | m = sb.maxino, adr = sb.indexaddr, # avol = sb.main + # avol0, avol0 = subarray(avol, sb.main, # avol - sb.main), is-encoded(plog, avol[sb.log].data), is-encoded(lpt, lebs(avol, sb.lpt, lptlebs(# avol0, LEB_SIZE))), is-encoded-pad(ns, sb.orphsize, avol[sb.orph].data), ebm-vol-inv(avol0), # lpt = # avol0, ∃ lpt0, log, orphans. persistence-io-inv(sb, logoff, avol, lpt0, log, orphans), m0 = EB_PAGE_SIZE, m1 = LEB_SIZE, ebm-vol-inv(avol) ⊦ ⟪persistence_io_add_log_leb#(m2, sb, m0, m1; logoff, avol; err)⟫ ⟨apersistence_io_add_log_leb#(m2, adr, m, avol0, lpt, ns; plog; err0)⟩ ( ( m = sb.maxino ∧ adr = sb.indexaddr ∧ # avol = sb.main + # avol0 ∧ avol0 = subarray(avol, sb.main, # avol - sb.main) ∧ is-encoded(plog, avol[sb.log].data) ∧ is-encoded(lpt, lebs(avol, sb.lpt, lptlebs(# avol0, LEB_SIZE))) ∧ is-encoded-pad(ns, sb.orphsize, avol[sb.orph].data)) ∧ err = err0) | A Proof Obligation |
| initialization | # lpt0 = m0, m1 = LEB_SIZE, adr0 = adr1, m2 = m3 ⊦ ⟪persistence_io_format#(m0, m1, lpt0, adr0, m2; sb, m4, m5, avol0; logoff, err)⟫ ( ( err = ESUCCESS → ⟨apersistence_io_format#(m0, m1, lpt0, adr1, m3; ; adr2, m6, plog, avol1, lpt1, ns0, err0)⟩ ( ( m6 = sb.maxino ∧ adr2 = sb.indexaddr ∧ # avol0 = sb.main + # avol1 ∧ avol1 = subarray(avol0, sb.main, # avol0 - sb.main) ∧ is-encoded(plog, avol0[sb.log].data) ∧ is-encoded(lpt1, lebs(avol0, sb.lpt, lptlebs(# avol1, LEB_SIZE))) ∧ is-encoded-pad(ns0, sb.orphsize, avol0[sb.orph].data)) ∧ err = err0)) ∧ ( err ≠ ESUCCESS → (∀ adr, m, log, avol, lpt, ns. ⟨apersistence_io_format#(m0, m1, lpt0, adr1, m3; ; adr2, m6, plog, avol1, lpt1, ns0, err0)⟩ (adr = adr2 ∧ m = m6 ∧ log = plog ∧ avol = avol1 ∧ lpt = lpt1 ∧ ns = ns0 ∧ err = err0)))) | A Proof Obligation |
| refine-get-volume-size | m = sb.maxino, adr = sb.indexaddr, # avol = sb.main + # avol0, avol0 = subarray(avol, sb.main, # avol - sb.main), is-encoded(plog, avol[sb.log].data), is-encoded(lpt, lebs(avol, sb.lpt, lptlebs(# avol0, LEB_SIZE))), is-encoded-pad(ns, sb.orphsize, avol[sb.orph].data), ebm-vol-inv(avol0), # lpt = # avol0, ∃ lpt0, log, orphans. persistence-io-inv(sb, logoff, avol, lpt0, log, orphans), m0 = EB_PAGE_SIZE, m1 = LEB_SIZE, ebm-vol-inv(avol) ⊦ ⟪persistence_io_get_volume_size#(sb, avol; ; n)⟫ ⟨apersistence_io_get_volume_size#(adr, m, plog, avol0, lpt, ns; ; n0)⟩ ( ( m = sb.maxino ∧ adr = sb.indexaddr ∧ # avol = sb.main + # avol0 ∧ avol0 = subarray(avol, sb.main, # avol - sb.main) ∧ is-encoded(plog, avol[sb.log].data) ∧ is-encoded(lpt, lebs(avol, sb.lpt, lptlebs(# avol0, LEB_SIZE))) ∧ is-encoded-pad(ns, sb.orphsize, avol[sb.orph].data)) ∧ n = n0) | A Proof Obligation |
| refine-remap | m < # avol, m0 = sb.maxino, adr = sb.indexaddr, # avol0 = sb.main + # avol, avol = subarray(avol0, sb.main, # avol0 - sb.main), is-encoded(plog, avol0[sb.log].data), is-encoded(lpt, lebs(avol0, sb.lpt, lptlebs(# avol, LEB_SIZE))), is-encoded-pad(ns, sb.orphsize, avol0[sb.orph].data), ebm-vol-inv(avol), # lpt = # avol, ∃ lpt0, log, orphans. persistence-io-inv(sb, logoff, avol0, lpt0, log, orphans), m1 = EB_PAGE_SIZE, m2 = LEB_SIZE, ebm-vol-inv(avol0) ⊦ ⟪persistence_io_remap#(m, sb; avol0; err)⟫ ⟨apersistence_io_remap#(m, adr, m0, plog, lpt, ns; avol; err0)⟩ ( ( m0 = sb.maxino ∧ adr = sb.indexaddr ∧ # avol0 = sb.main + # avol ∧ avol = subarray(avol0, sb.main, # avol0 - sb.main) ∧ is-encoded(plog, avol0[sb.log].data) ∧ is-encoded(lpt, lebs(avol0, sb.lpt, lptlebs(# avol, LEB_SIZE))) ∧ is-encoded-pad(ns, sb.orphsize, avol0[sb.orph].data)) ∧ err = err0) | A Proof Obligation |
| recovery | avol0 ⊆ avol1, m0 = sb.maxino, adr0 = sb.indexaddr, # avol0 = sb.main + # avol2, avol2 = subarray(avol0, sb.main, # avol0 - sb.main), is-encoded(log0, avol0[sb.log].data), is-encoded(lpt0, lebs(avol0, sb.lpt, lptlebs(# avol2, LEB_SIZE))), is-encoded-pad(ns0, sb.orphsize, avol0[sb.orph].data), ebm-vol-inv(avol2), # lpt0 = # avol2, ∃ lpt1, log1, orphans. persistence-io-inv(sb, m1, avol0, lpt1, log1, orphans), m2 = EB_PAGE_SIZE, m3 = LEB_SIZE, ebm-vol-inv(avol0), adr1 = adr2, m4 = m5, orphans = ns1, log1 = log2, lpt1 = lpt2 ⊦ ⟪persistence_io_recover#(; adr1, m4, orphans, log1, lpt1, sb0, logoff, m6, m7, avol1; err)⟫ ( ( err = ESUCCESS → (∃ adr, m, plog, avol, lpt, ns. (adr = adr0 ∧ m = m0 ∧ plog = log0 ∧ lpt = lpt0 ∧ avol2 ⊆ avol ∧ ns = ns0) ∧ ⟨apersistence_io_recover#(; adr2, m5, ns1, log2, lpt2, adr, m, plog, lpt, ns, avol; err0)⟩ ( ( m = sb0.maxino ∧ adr = sb0.indexaddr ∧ # avol1 = sb0.main + # avol ∧ avol = subarray(avol1, sb0.main, # avol1 - sb0.main) ∧ is-encoded(plog, avol1[sb0.log].data) ∧ is-encoded(lpt, lebs(avol1, sb0.lpt, lptlebs(# avol, LEB_SIZE))) ∧ is-encoded-pad(ns, sb0.orphsize, avol1[sb0.orph].data)) ∧ adr1 = adr2 ∧ m4 = m5 ∧ orphans = ns1 ∧ log1 = log2 ∧ lpt1 = lpt2 ∧ err = err0))) ∧ ( err ≠ ESUCCESS → (∀ adr, m, log, avol, lpt, ns. ⟨apersistence_io_recover#(; adr2, m5, ns1, log2, lpt2, adr3, m8, plog0, lpt3, ns2, avol3; err0)⟩ ( adr = adr3 ∧ m = m8 ∧ log = plog0 ∧ avol = avol3 ∧ lpt = lpt3 ∧ ns = ns2 ∧ adr1 = adr2 ∧ m4 = m5 ∧ orphans = ns1 ∧ log1 = log2 ∧ lpt1 = lpt2 ∧ err = err0)))) | A Proof Obligation |
| refine-unmap | m < # avol, m0 = sb.maxino, adr = sb.indexaddr, # avol0 = sb.main + # avol, avol = subarray(avol0, sb.main, # avol0 - sb.main), is-encoded(plog, avol0[sb.log].data), is-encoded(lpt, lebs(avol0, sb.lpt, lptlebs(# avol, LEB_SIZE))), is-encoded-pad(ns, sb.orphsize, avol0[sb.orph].data), ebm-vol-inv(avol), # lpt = # avol, ∃ lpt0, log, orphans. persistence-io-inv(sb, logoff, avol0, lpt0, log, orphans), m1 = EB_PAGE_SIZE, m2 = LEB_SIZE, ebm-vol-inv(avol0) ⊦ ⟪persistence_io_unmap#(m, sb; avol0)⟫ ⟨apersistence_io_unmap#(m, adr, m0, plog, lpt, ns; avol)⟩ ( m0 = sb.maxino ∧ adr = sb.indexaddr ∧ # avol0 = sb.main + # avol ∧ avol = subarray(avol0, sb.main, # avol0 - sb.main) ∧ is-encoded(plog, avol0[sb.log].data) ∧ is-encoded(lpt, lebs(avol0, sb.lpt, lptlebs(# avol, LEB_SIZE))) ∧ is-encoded-pad(ns, sb.orphsize, avol0[sb.orph].data)) | A Proof Obligation |
| refine-read | m < # avol, avol[m].mapped?, n + n0 ≤ # buf, m0 + n0 ≤ LEB_SIZE, m1 = sb.maxino, adr = sb.indexaddr, # avol0 = sb.main + # avol, avol = subarray(avol0, sb.main, # avol0 - sb.main), is-encoded(plog, avol0[sb.log].data), is-encoded(lpt, lebs(avol0, sb.lpt, lptlebs(# avol, LEB_SIZE))), is-encoded-pad(ns, sb.orphsize, avol0[sb.orph].data), ebm-vol-inv(avol), # lpt = # avol, ∃ lpt0, log, orphans. persistence-io-inv(sb, logoff, avol0, lpt0, log, orphans), m2 = EB_PAGE_SIZE, m3 = LEB_SIZE, ebm-vol-inv(avol0), buf = buf0 ⊦ ⟪persistence_io_read#(m, m0, n, n0, sb, avol0; buf; err)⟫ ⟨apersistence_io_read#(m, m0, n, n0, adr, m1, plog, avol, lpt, ns; buf0; err0)⟩ ( ( m1 = sb.maxino ∧ adr = sb.indexaddr ∧ # avol0 = sb.main + # avol ∧ avol = subarray(avol0, sb.main, # avol0 - sb.main) ∧ is-encoded(plog, avol0[sb.log].data) ∧ is-encoded(lpt, lebs(avol0, sb.lpt, lptlebs(# avol, LEB_SIZE))) ∧ is-encoded-pad(ns, sb.orphsize, avol0[sb.orph].data)) ∧ buf = buf0 ∧ err = err0) | A Proof Obligation |
| refine-write | m < # avol, avol[m].mapped?, # avol[m].data ≤ m0, is-aligned(m0, EB_PAGE_SIZE), is-aligned(n, EB_PAGE_SIZE), m0 + n ≤ LEB_SIZE, n0 + n ≤ # buf, m1 = sb.maxino, adr = sb.indexaddr, # avol0 = sb.main + # avol, avol = subarray(avol0, sb.main, # avol0 - sb.main), is-encoded(plog, avol0[sb.log].data), is-encoded(lpt, lebs(avol0, sb.lpt, lptlebs(# avol, LEB_SIZE))), is-encoded-pad(ns, sb.orphsize, avol0[sb.orph].data), ebm-vol-inv(avol), # lpt = # avol, ∃ lpt0, log, orphans. persistence-io-inv(sb, logoff, avol0, lpt0, log, orphans), m2 = EB_PAGE_SIZE, m3 = LEB_SIZE, ebm-vol-inv(avol0) ⊦ ⟪persistence_io_write#(m, m0, n0, n, buf, sb; avol0; err)⟫ ⟨apersistence_io_write#(m, m0, n0, n, buf, adr, m1, plog, lpt, ns; avol; err0)⟩ ( ( m1 = sb.maxino ∧ adr = sb.indexaddr ∧ # avol0 = sb.main + # avol ∧ avol = subarray(avol0, sb.main, # avol0 - sb.main) ∧ is-encoded(plog, avol0[sb.log].data) ∧ is-encoded(lpt, lebs(avol0, sb.lpt, lptlebs(# avol, LEB_SIZE))) ∧ is-encoded-pad(ns, sb.orphsize, avol0[sb.orph].data)) ∧ err = err0) | A Proof Obligation |
| refine-get-leb-size | m = sb.maxino, adr = sb.indexaddr, # avol = sb.main + # avol0, avol0 = subarray(avol, sb.main, # avol - sb.main), is-encoded(plog, avol[sb.log].data), is-encoded(lpt, lebs(avol, sb.lpt, lptlebs(# avol0, LEB_SIZE))), is-encoded-pad(ns, sb.orphsize, avol[sb.orph].data), ebm-vol-inv(avol0), # lpt = # avol0, ∃ lpt0, log, orphans. persistence-io-inv(sb, logoff, avol, lpt0, log, orphans), m0 = EB_PAGE_SIZE, m1 = LEB_SIZE, ebm-vol-inv(avol) ⊦ ⟪persistence_io_get_leb_size#(m1; ; n)⟫ ⟨apersistence_io_get_leb_size#(adr, m, plog, avol0, lpt, ns; ; n0)⟩ ( ( m = sb.maxino ∧ adr = sb.indexaddr ∧ # avol = sb.main + # avol0 ∧ avol0 = subarray(avol, sb.main, # avol - sb.main) ∧ is-encoded(plog, avol[sb.log].data) ∧ is-encoded(lpt, lebs(avol, sb.lpt, lptlebs(# avol0, LEB_SIZE))) ∧ is-encoded-pad(ns, sb.orphsize, avol[sb.orph].data)) ∧ n = n0) | A Proof Obligation |
| refine-get-page-size | m = sb.maxino, adr = sb.indexaddr, # avol = sb.main + # avol0, avol0 = subarray(avol, sb.main, # avol - sb.main), is-encoded(plog, avol[sb.log].data), is-encoded(lpt, lebs(avol, sb.lpt, lptlebs(# avol0, LEB_SIZE))), is-encoded-pad(ns, sb.orphsize, avol[sb.orph].data), ebm-vol-inv(avol0), # lpt = # avol0, ∃ lpt0, log, orphans. persistence-io-inv(sb, logoff, avol, lpt0, log, orphans), m0 = EB_PAGE_SIZE, m1 = LEB_SIZE, ebm-vol-inv(avol) ⊦ ⟪persistence_io_get_page_size#(m0; ; n)⟫ ⟨apersistence_io_get_page_size#(adr, m, plog, avol0, lpt, ns; ; n0)⟩ ( ( m = sb.maxino ∧ adr = sb.indexaddr ∧ # avol = sb.main + # avol0 ∧ avol0 = subarray(avol, sb.main, # avol - sb.main) ∧ is-encoded(plog, avol[sb.log].data) ∧ is-encoded(lpt, lebs(avol, sb.lpt, lptlebs(# avol0, LEB_SIZE))) ∧ is-encoded-pad(ns, sb.orphsize, avol[sb.orph].data)) ∧ n = n0) | A Proof Obligation |
| subarray-avol-write | n < m ⊦ # avol = main + m → subarray(avol[main + n, aleb], main, m) = subarray(avol, main, m)[n, aleb] | A User Theorem |