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: |
|---|---|---|
| get-volume-size | apersistence_io_get_volume_size#(PROOTADR, PMAXINO, PLOG, PVOL, PLPT, PORPHANS; ; N){N := # PVOL} | An Axiom |
| format | apersistence_io_format#(VOLSIZE, SIZE, LPT, PROOTADR0, PMAXINO0; ; PROOTADR, PMAXINO, PLOG, PVOL, PLPT, PORPHANS, ERR) {if # LPT = VOLSIZE ∧ SIZE = LEB_SIZE then {fail_or_success#(; ; ERR); if ERR = ESUCCESS then {PVOL := fill(mkavolume(VOLSIZE), unmapped); PROOTADR := PROOTADR0; PMAXINO := PMAXINO0; PLOG := []; PLPT := LPT; PORPHANS := ∅} else PVOL := ?, PROOTADR := ?, PMAXINO := ?, PLOG := ?, PLPT := ?, PORPHANS := ?} else abort } | An Axiom |
| recover | apersistence_io_recover#(; PROOTADR0, PMAXINO0, ORPHANS, LOG, LPT, PROOTADR, PMAXINO, PLOG, PLPT, PORPHANS, PVOL; ERR) {fail_or_success#(; ; ERR); if ERR = ESUCCESS then PROOTADR0 := PROOTADR, PMAXINO0 := PMAXINO, LOG := PLOG, LPT := PLPT, ORPHANS := PORPHANS else PVOL := ?, PROOTADR := ?, PMAXINO := ?, PLOG := ?, PLPT := ?, PROOTADR0 := ?, PMAXINO0 := ?, LOG := ?, LPT := ?, ORPHANS := ?, PORPHANS := ? } | An Axiom |
| commit | apersistence_io_commit#(LPT, PROOTADR0, PMAXINO0, PVOL; ORPHANS, PROOTADR, PMAXINO, PLOG, PLPT, PORPHANS; ERR) {if # LPT = # PVOL then {fail_or_success#(; ; ERR); if ERR = ESUCCESS then {PROOTADR := PROOTADR0; PMAXINO := PMAXINO0; PLOG := []; PLPT := LPT; PORPHANS := ORPHANS}; ORPHANS := ?} else abort } | An Axiom |
| add-log-leb | apersistence_io_add_log_leb#(LNUM, PROOTADR, PMAXINO, PVOL, PLPT, PORPHANS; PLOG; ERR) {fail_or_success#(; ; ERR); if ERR = ESUCCESS then PLOG := PLOG + LNUM} | An Axiom |
| requires-commit | apersistence_io_requires_commit#(PROOTADR, PMAXINO, PLOG, PVOL, PLPT, PORPHANS; ; COMMIT?){COMMIT? := ?} | An Axiom |
| remap | apersistence_io_remap#(LNUM, PROOTADR, PMAXINO, PLOG, PLPT, PORPHANS; PVOL; ERR) {if LNUM < # PVOL then {fail_or_success#(; ; ERR); if ERR = ESUCCESS then PVOL[LNUM] := mapped(mkbuf(0)) else {skip or PVOL[LNUM] := unmapped}} else abort } | An Axiom |
| unmap | apersistence_io_unmap#(LNUM, PROOTADR, PMAXINO, PLOG, PLPT, PORPHANS; PVOL){if LNUM < # PVOL then PVOL[LNUM] := unmapped else abort} | An Axiom |
| read | apersistence_io_read#(LNUM, OFFSET, N0, N, PROOTADR, PMAXINO, PLOG, PVOL, PLPT, PORPHANS; BUF; ERR) {if LNUM < # PVOL ∧ PVOL[LNUM].mapped? ∧ N0 + N ≤ # BUF ∧ OFFSET + N ≤ LEB_SIZE then {fail_or_success#(; ; ERR); if ERR = ESUCCESS then BUF := copy(PVOL[LNUM].data + mkempbuf(LEB_SIZE - # PVOL[LNUM].data), OFFSET, BUF, N0, N) else choose BUF0 with # BUF0 = # BUF ∧ range=(BUF, 0, BUF0, 0, N0) ∧ range=(BUF, N0 + N, BUF0, N0 + N, # BUF - N0 + N) in BUF := BUF0} else abort } | An Axiom |
| write | apersistence_io_write#(LNUM, OFFSET, N0, N, BUF, PROOTADR, PMAXINO, PLOG, PLPT, PORPHANS; PVOL; ERR) {if LNUM < # PVOL ∧ PVOL[LNUM].mapped? ∧ # PVOL[LNUM].data ≤ OFFSET ∧ is-aligned(OFFSET, EB_PAGE_SIZE) ∧ is-aligned(N, EB_PAGE_SIZE) ∧ OFFSET + N ≤ LEB_SIZE ∧ N0 + N ≤ # BUF then {fail_or_success#(; ; ERR); if ERR = ESUCCESS then if N ≠ 0 then PVOL[LNUM] := mapped(PVOL[LNUM].data + mkempbuf(OFFSET - # PVOL[LNUM].data) + subarray(BUF, N0, N)) else choose N1 with N1 < N ∧ is-aligned(N1, EB_PAGE_SIZE) in if N1 ≠ 0 then PVOL[LNUM] := mapped(PVOL[LNUM].data + mkempbuf(OFFSET - # PVOL[LNUM].data) + subarray(BUF, N0, N1)) ifnone skip} else abort } | An Axiom |
| get-leb-size | apersistence_io_get_leb_size#(PROOTADR, PMAXINO, PLOG, PVOL, PLPT, PORPHANS; ; N){N := LEB_SIZE} | An Axiom |
| get-page-size | apersistence_io_get_page_size#(PROOTADR, PMAXINO, PLOG, PVOL, PLPT, PORPHANS; ; N){N := EB_PAGE_SIZE} | An Axiom |
| inv-format | # lpt = m, m0 = LEB_SIZE ⊦ ⟪apersistence_io_format#(m, m0, lpt, adr, m1; ; adr0, m2, plog, avol, lpt0, ns, err)⟫ (err = ESUCCESS → ebm-vol-inv(avol) ∧ # lpt0 = # avol) | A Proof Obligation |
| inv-recover | adr = adr0, m = m0, plog = plog0, lpt = lpt0, avol ⊆ avol0, ns = ns0, ebm-vol-inv(avol), # lpt0 = # avol ⊦ ⟪apersistence_io_recover#(; adr1, m1, ns1, log, lpt1, adr, m, plog, lpt, ns, avol0; err)⟫ (err = ESUCCESS → ebm-vol-inv(avol0) ∧ # lpt = # avol0) | A Proof Obligation |
| crash-neutral-get-volume-size | ebm-vol-inv(avol), # lpt = # avol, adr = adr0, m = m0, plog = plog0, lpt0 = lpt, avol ⊆ avol0, ns = ns0 ⊦ ⟨apersistence_io_get_volume_size#(adr0, m0, plog0, avol, lpt, ns0; ; n)⟩ (adr = adr0 ∧ m = m0 ∧ plog = plog0 ∧ lpt0 = lpt ∧ avol ⊆ avol0 ∧ ns = ns0) | A Proof Obligation |
| inv-get-volume-size | ebm-vol-inv(avol), # lpt = # avol ⊦ ⟪apersistence_io_get_volume_size#(adr, m, plog, avol, lpt, ns; ; n)⟫ true | A Proof Obligation |
| crash-neutral-commit | # lpt = # avol, ebm-vol-inv(avol), # lpt0 = # avol, adr = adr0, m = m0, plog = plog0, lpt1 = lpt0, avol ⊆ avol0, ns = ns0 ⊦ ⟨apersistence_io_commit#(lpt, adr1, m1, avol; ns1, adr0, m0, plog0, lpt0, ns0; err)⟩ (adr = adr0 ∧ m = m0 ∧ plog = plog0 ∧ lpt1 = lpt0 ∧ avol ⊆ avol0 ∧ ns = ns0) | A Proof Obligation |
| inv-commit | ebm-vol-inv(avol), # lpt = # avol, # lpt0 = # avol ⊦ ⟪apersistence_io_commit#(lpt0, adr, m, avol; ns, adr0, m0, plog, lpt, ns0; err)⟫ (# lpt = # avol) | A Proof Obligation |
| crash-neutral-add-log-leb | ebm-vol-inv(avol), # lpt = # avol, adr = adr0, m = m0, plog = plog0, lpt0 = lpt, avol ⊆ avol0, ns = ns0 ⊦ ⟨apersistence_io_add_log_leb#(m1, adr0, m0, avol, lpt, ns0; plog0; err)⟩ (adr = adr0 ∧ m = m0 ∧ plog = plog0 ∧ lpt0 = lpt ∧ avol ⊆ avol0 ∧ ns = ns0) | A Proof Obligation |
| crash-neutral-requires-commit | ebm-vol-inv(avol), # lpt = # avol, adr = adr0, m = m0, plog = plog0, lpt0 = lpt, avol ⊆ avol0, ns = ns0 ⊦ ⟨apersistence_io_requires_commit#(adr0, m0, plog0, avol, lpt, ns0; ; isbuf)⟩ (adr = adr0 ∧ m = m0 ∧ plog = plog0 ∧ lpt0 = lpt ∧ avol ⊆ avol0 ∧ ns = ns0) | A Proof Obligation |
| inv-add-log-leb | ebm-vol-inv(avol), # lpt = # avol ⊦ ⟪apersistence_io_add_log_leb#(m, adr, m0, avol, lpt, ns; plog; err)⟫ true | A Proof Obligation |
| inv-requires-commit | ebm-vol-inv(avol), # lpt = # avol ⊦ ⟪apersistence_io_requires_commit#(adr, m, plog, avol, lpt, ns; ; isbuf)⟫ true | A Proof Obligation |
| crash-neutral-remap | m < # avol, ebm-vol-inv(avol), # lpt = # avol, adr = adr0, m0 = m1, plog = plog0, lpt0 = lpt, avol ⊆ avol0, ns = ns0 ⊦ ⟨apersistence_io_remap#(m, adr0, m1, plog0, lpt, ns0; avol; err)⟩ (adr = adr0 ∧ m0 = m1 ∧ plog = plog0 ∧ lpt0 = lpt ∧ avol ⊆ avol0 ∧ ns = ns0) | A Proof Obligation |
| inv-remap | ebm-vol-inv(avol), # lpt = # avol, m < # avol ⊦ ⟪apersistence_io_remap#(m, adr, m0, plog, lpt, ns; avol; err)⟫ (ebm-vol-inv(avol) ∧ # lpt = # avol) | A Proof Obligation |
| crash-neutral-unmap | m < # avol, ebm-vol-inv(avol), # lpt = # avol, adr = adr0, m0 = m1, plog = plog0, lpt0 = lpt, avol ⊆ avol0, ns = ns0 ⊦ ⟨apersistence_io_unmap#(m, adr0, m1, plog0, lpt, ns0; avol)⟩ (adr = adr0 ∧ m0 = m1 ∧ plog = plog0 ∧ lpt0 = lpt ∧ avol ⊆ avol0 ∧ ns = ns0) | A Proof Obligation |
| inv-unmap | ebm-vol-inv(avol), # lpt = # avol, m < # avol ⊦ ⟪apersistence_io_unmap#(m, adr, m0, plog, lpt, ns; avol)⟫ (ebm-vol-inv(avol) ∧ # lpt = # avol) | A Proof Obligation |
| crash-neutral-read | m < # avol, avol[m].mapped?, n + n0 ≤ # buf, m0 + n0 ≤ LEB_SIZE, ebm-vol-inv(avol), # lpt = # avol, adr = adr0, m1 = m2, plog = plog0, lpt0 = lpt, avol ⊆ avol0, ns = ns0 ⊦ ⟨apersistence_io_read#(m, m0, n, n0, adr0, m2, plog0, avol, lpt, ns0; buf; err)⟩ (adr = adr0 ∧ m1 = m2 ∧ plog = plog0 ∧ lpt0 = lpt ∧ avol ⊆ avol0 ∧ ns = ns0) | A Proof Obligation |
| crash-neutral-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, ebm-vol-inv(avol), # lpt = # avol, adr = adr0, m1 = m2, plog = plog0, lpt0 = lpt, avol ⊆ avol0, ns = ns0 ⊦ ⟨apersistence_io_write#(m, m0, n0, n, buf, adr0, m2, plog0, lpt, ns0; avol; err)⟩ (adr = adr0 ∧ m1 = m2 ∧ plog = plog0 ∧ lpt0 = lpt ∧ avol ⊆ avol0 ∧ ns = ns0) | A Proof Obligation |
| inv-read | ebm-vol-inv(avol), # lpt = # avol, m < # avol, avol[m].mapped?, n + n0 ≤ # buf, m0 + n0 ≤ LEB_SIZE ⊦ ⟪apersistence_io_read#(m, m0, n, n0, adr, m1, plog, avol, lpt, ns; buf; err)⟫ true | A Proof Obligation |
| inv-write | ebm-vol-inv(avol), # lpt = # avol, 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 ⊦ ⟪apersistence_io_write#(m, m0, n0, n, buf, adr, m1, plog, lpt, ns; avol; err)⟫ (ebm-vol-inv(avol) ∧ # lpt = # avol) | A Proof Obligation |
| crash-neutral-get-leb-size | ebm-vol-inv(avol), # lpt = # avol, adr = adr0, m = m0, plog = plog0, lpt0 = lpt, avol ⊆ avol0, ns = ns0 ⊦ ⟨apersistence_io_get_leb_size#(adr0, m0, plog0, avol, lpt, ns0; ; n)⟩ (adr = adr0 ∧ m = m0 ∧ plog = plog0 ∧ lpt0 = lpt ∧ avol ⊆ avol0 ∧ ns = ns0) | A Proof Obligation |
| crash-neutral-get-page-size | ebm-vol-inv(avol), # lpt = # avol, adr = adr0, m = m0, plog = plog0, lpt0 = lpt, avol ⊆ avol0, ns = ns0 ⊦ ⟨apersistence_io_get_page_size#(adr0, m0, plog0, avol, lpt, ns0; ; n)⟩ (adr = adr0 ∧ m = m0 ∧ plog = plog0 ∧ lpt0 = lpt ∧ avol ⊆ avol0 ∧ ns = ns0) | A Proof Obligation |
| inv-get-leb-size | ebm-vol-inv(avol), # lpt = # avol ⊦ ⟪apersistence_io_get_leb_size#(adr, m, plog, avol, lpt, ns; ; n)⟫ true | A Proof Obligation |
| inv-get-page-size | ebm-vol-inv(avol), # lpt = # avol ⊦ ⟪apersistence_io_get_page_size#(adr, m, plog, avol, lpt, ns; ; n)⟫ true | A Proof Obligation |
| crash-neutral-recover | ebm-vol-inv(avol), # lpt = # avol, adr = adr0, m = m0, plog = plog0, lpt0 = lpt, avol ⊆ avol0, ns = ns0 ⊦ ⟨apersistence_io_recover#(; adr1, m1, ns1, log, lpt1, adr0, m0, plog0, lpt, ns0, avol; err)⟩ (adr = adr0 ∧ m = m0 ∧ plog = plog0 ∧ lpt0 = lpt ∧ avol ⊆ avol0 ∧ ns = ns0) | A Proof Obligation |