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 | wbuf_get_volume_size#(PROOTADR, PMAXINO, PLOG, PVOL, PLPT, PORPHANS; ; N) {apersistence_io_get_volume_size#(PROOTADR, PMAXINO, PLOG, PVOL, PLPT, PORPHANS; ; N)} | An Axiom |
| move-buf | wbuf_move_buf#(LNUM, OFFSET, ROFS, PVOL; BUFLEB, WBUF; ERR) {if ¬ ROFS → BUFLEB = buffered(LNUM) ∨ (BUFLEB = nobuffer ∨ WBUF.nbytes = 0) ∧ LNUM < # PVOL ∧ PVOL[LNUM].mapped? ∧ OFFSET = # PVOL[LNUM].data then if ROFS then ERR := EROFS else {ERR := ESUCCESS; if BUFLEB ≠ buffered(LNUM) then {BUFLEB := buffered(LNUM); WBUF.offset := OFFSET; WBUF.nbytes := 0}} else abort } | An Axiom |
| write-buf | wbuf_write_buf#(N, BUF, BUFLEB, PAGESIZE, PROOTADR, PMAXINO, PLOG, PLPT, PORPHANS; WBUF, ROFS, PVOL; ERR) {if BUFLEB ≠ nobuffer ∧ (¬ ROFS → WBUF.offset + WBUF.nbytes + N ≤ LEB_SIZE ∧ N ≤ # BUF) then if ROFS then ERR := EROFS else if WBUF.nbytes + N ≥ PAGESIZE then let N0 = align↓(WBUF.nbytes + N, PAGESIZE) in let N1 = N0 - WBUF.nbytes in let N2 = (WBUF.nbytes + N) % PAGESIZE in let BUF0 = mkbuf(N0) in {BUF0 := copy(WBUF.content, 0, BUF0, 0, WBUF.nbytes); BUF0 := copy(BUF, 0, BUF0, WBUF.nbytes, N1); apersistence_io_write#(BUFLEB.leb, WBUF.offset, 0, N0, BUF0, PROOTADR, PMAXINO, PLOG, PLPT, PORPHANS; PVOL; ERR); if ERR = ESUCCESS then {WBUF.content := copy(BUF, N1, WBUF.content, 0, N2); WBUF.offset := WBUF.offset + N0; WBUF.nbytes := N2} else ROFS := true} else {WBUF.content := copy(BUF, 0, WBUF.content, WBUF.nbytes, N); WBUF.nbytes := WBUF.nbytes + N; ERR := ESUCCESS} else abort } | An Axiom |
| read-buf | wbuf_read_buf#(LNUM, OFFSET, N, BUFLEB, WBUF, PROOTADR, PMAXINO, PLOG, PVOL, PLPT, PORPHANS; BUF; ERR) {if LNUM < # PVOL ∧ N ≤ # BUF ∧ OFFSET + N ≤ LEB_SIZE ∧ PVOL[LNUM].mapped? then {apersistence_io_read#(LNUM, OFFSET, 0, N, PROOTADR, PMAXINO, PLOG, PVOL, PLPT, PORPHANS; BUF; ERR); if ERR = ESUCCESS ∧ buffered(LNUM) = BUFLEB ∧ OFFSET ≤ WBUF.offset + WBUF.nbytes ∧ WBUF.offset ≤ OFFSET + N then let BEGINWBUF = (OFFSET ≤ WBUF.offset ⊃ 0;OFFSET - WBUF.offset), BEGINBUF = (OFFSET ≤ WBUF.offset ⊃ WBUF.offset - OFFSET;0) in BUF := copy(WBUF.content, BEGINWBUF, BUF, BEGINBUF, min(N - BEGINBUF, WBUF.nbytes - BEGINWBUF))} else abort } | An Axiom |
| commit | wbuf_commit#(LPT, PROOTADR0, PMAXINO0, PVOL; ORPHANS, PROOTADR, PMAXINO, PLOG, PLPT, PORPHANS, ROFS; ERR) {if # LPT = # PVOL then {apersistence_io_commit#(LPT, PROOTADR0, PMAXINO0, PVOL; ORPHANS, PROOTADR, PMAXINO, PLOG, PLPT, PORPHANS; ERR); if ERR ≠ ESUCCESS then ROFS := true} else abort } | An Axiom |
| requires-commit | wbuf_requires_commit#(PROOTADR, PMAXINO, PLOG, PVOL, PLPT, PORPHANS; ; COMMIT?) {apersistence_io_requires_commit#(PROOTADR, PMAXINO, PLOG, PVOL, PLPT, PORPHANS; ; COMMIT?)} | An Axiom |
| add-log-leb | wbuf_add_log_leb#(LNUM, OFFSET, ROFS, PROOTADR, PMAXINO, PVOL, PLPT, PORPHANS; BUFLEB, WBUF, PLOG; ERR) {if ¬ ROFS → BUFLEB = buffered(LNUM) ∨ (BUFLEB = nobuffer ∨ WBUF.nbytes = 0) ∧ LNUM < # PVOL ∧ PVOL[LNUM].mapped? ∧ OFFSET = # PVOL[LNUM].data then if ROFS then ERR := EROFS else {apersistence_io_add_log_leb#(LNUM, PROOTADR, PMAXINO, PVOL, PLPT, PORPHANS; PLOG; ERR); if ERR = ESUCCESS then wbuf_move_buf#(LNUM, OFFSET, ROFS, PVOL; BUFLEB, WBUF; ERR)} else abort } | An Axiom |
| remap | wbuf_remap#(LNUM, BUFLEB, PROOTADR, PMAXINO, PLOG, PLPT, PORPHANS; PVOL; ERR) {if LNUM < # PVOL ∧ buffered(LNUM) ≠ BUFLEB then apersistence_io_remap#(LNUM, PROOTADR, PMAXINO, PLOG, PLPT, PORPHANS; PVOL; ERR) else abort } | An Axiom |
| unmap | wbuf_unmap#(LNUM, BUFLEB, PROOTADR, PMAXINO, PLOG, PLPT, PORPHANS; PVOL) {if LNUM < # PVOL ∧ buffered(LNUM) ≠ BUFLEB then apersistence_io_unmap#(LNUM, PROOTADR, PMAXINO, PLOG, PLPT, PORPHANS; PVOL) else abort} | An Axiom |
| format | wbuf_format#(VOLSIZE, SIZE, LPT, PROOTADR0, PMAXINO0; WBUF, PAGESIZE, PROOTADR, PMAXINO, PLOG, PVOL, PLPT, PORPHANS, BUFLEB, ROFS; ERR) {if VOLSIZE = # LPT ∧ SIZE = LEB_SIZE then {apersistence_io_format#(VOLSIZE, SIZE, LPT, PROOTADR0, PMAXINO0; ; PROOTADR, PMAXINO, PLOG, PVOL, PLPT, PORPHANS, ERR); if ERR = ESUCCESS then {apersistence_io_get_page_size#(PROOTADR, PMAXINO, PLOG, PVOL, PLPT, PORPHANS; ; PAGESIZE); BUFLEB := nobuffer; WBUF.content := mkbuf(PAGESIZE); ROFS := false}} else abort } | An Axiom |
| recover | wbuf_recover#(; PROOTADR0, PMAXINO0, ORPHANS, LOG, LPT, WBUF, PAGESIZE, PROOTADR, PMAXINO, PLOG, PVOL, PLPT, PORPHANS, BUFLEB, ROFS; ERR) {apersistence_io_recover#(; PROOTADR0, PMAXINO0, ORPHANS, LOG, LPT, PROOTADR, PMAXINO, PLOG, PLPT, PORPHANS, PVOL; ERR); if ERR = ESUCCESS then {apersistence_io_get_page_size#(PROOTADR, PMAXINO, PLOG, PVOL, PLPT, PORPHANS; ; PAGESIZE); BUFLEB := nobuffer; WBUF.content := mkbuf(PAGESIZE); ROFS := false} } | An Axiom |
| get-leb-size | wbuf_get_leb_size#(PROOTADR, PMAXINO, PLOG, PVOL, PLPT, PORPHANS; ; N) {apersistence_io_get_leb_size#(PROOTADR, PMAXINO, PLOG, PVOL, PLPT, PORPHANS; ; N)} | An Axiom |
| get-page-size | wbuf_get_page_size#(PAGESIZE; ; N){N := PAGESIZE} | An Axiom |
| destroy-buf | wbuf_destroy_buf#(ROFS; BUFLEB; ERR){if ROFS then ERR := EROFS else {BUFLEB := nobuffer; ERR := ESUCCESS}} | An Axiom |
| get-buf | wbuf_get_buf#(BUFLEB; ; BUFLEB0){BUFLEB0 := BUFLEB} | An Axiom |
| is-readonly | wbuf_is_readonly#(ROFS; ; ROFS0){ROFS0 := ROFS} | An Axiom |
| enter-readonly | wbuf_enter_readonly#(; ; ROFS){ROFS := true} | An Axiom |
| inv-format | m = # lpt, m0 = LEB_SIZE ⊦ ⟪wbuf_format#(m, m0, lpt, adr, m1; wbuf, m2, adr0, m3, plog, avol, lpt0, ns, bleb, rofs; err)⟫ (err = ESUCCESS → wbuf-cons(bleb, wbuf, avol, rofs) ∧ m2 = EB_PAGE_SIZE ∧ ebm-vol-inv(avol) ∧ # lpt0 = # avol) | A Proof Obligation |
| inv-get-buf | wbuf-cons(bleb, wbuf, avol, rofs) ⊦ ⟪wbuf_get_buf#(bleb; ; bleb0)⟫ true | A Proof Obligation |
| inv-recover | adr = adr0, m = m0, plog = plog0, lpt = lpt0, avol ⊆ avol0, ns = ns0, wbuf-cons(bleb, wbuf, avol, rofs), m1 = EB_PAGE_SIZE, ebm-vol-inv(avol), # lpt0 = # avol ⊦ ⟪wbuf_recover#(; adr1, m2, ns1, log, lpt1, wbuf0, m3, adr, m, plog, avol0, lpt, ns, bleb0, rofs0; err)⟫ (err = ESUCCESS → wbuf-cons(bleb0, wbuf0, avol0, rofs0) ∧ m3 = EB_PAGE_SIZE ∧ ebm-vol-inv(avol0) ∧ # lpt = # avol0) | A Proof Obligation |
| inv-get-volume-size | wbuf-cons(bleb, wbuf, avol, rofs), ebm-vol-inv(avol), # lpt = # avol ⊦ ⟪wbuf_get_volume_size#(adr, m, plog, avol, lpt, ns; ; n)⟫ true | A Proof Obligation |
| inv-move-buf | wbuf-cons(bleb, wbuf, avol, rofs), ebm-vol-inv(avol), # lpt = # avol, ¬ rofs → bleb = buffered(m) ∨ (bleb = nobuffer ∨ wbuf.nbytes = 0) ∧ m < # avol ∧ avol[m].mapped? ∧ m0 = # avol[m].data ⊦ ⟪wbuf_move_buf#(m, m0, rofs, avol; bleb, wbuf; err)⟫ wbuf-cons(bleb, wbuf, avol, rofs) | A Proof Obligation |
| inv-write-buf | wbuf-cons(bleb, wbuf, avol, rofs), m = EB_PAGE_SIZE, ebm-vol-inv(avol), # lpt = # avol, bleb ≠ nobuffer, ¬ rofs → wbuf.offset + wbuf.nbytes + n ≤ LEB_SIZE ∧ n ≤ # buf ⊦ ⟪wbuf_write_buf#(n, buf, bleb, m, adr, m0, plog, lpt, ns; wbuf, rofs, avol; err)⟫ (wbuf-cons(bleb, wbuf, avol, rofs) ∧ ebm-vol-inv(avol) ∧ # lpt = # avol) | A Proof Obligation |
| inv-read-buf | wbuf-cons(bleb, wbuf, avol, rofs), ebm-vol-inv(avol), # lpt = # avol, m < # avol, n ≤ # buf, m0 + n ≤ LEB_SIZE, avol[m].mapped? ⊦ ⟪wbuf_read_buf#(m, m0, n, bleb, wbuf, adr, m1, plog, avol, lpt, ns; buf; err)⟫ true | A Proof Obligation |
| inv-commit | wbuf-cons(bleb, wbuf, avol, rofs), ebm-vol-inv(avol), # lpt = # avol, # lpt0 = # avol ⊦ ⟪wbuf_commit#(lpt0, adr, m, avol; ns, adr0, m0, plog, lpt, ns0, rofs; err)⟫ (wbuf-cons(bleb, wbuf, avol, rofs) ∧ # lpt = # avol) | A Proof Obligation |
| inv-requires-commit | wbuf-cons(bleb, wbuf, avol, rofs), ebm-vol-inv(avol), # lpt = # avol ⊦ ⟪wbuf_requires_commit#(adr, m, plog, avol, lpt, ns; ; rofs0)⟫ true | A Proof Obligation |
| inv-add-log-leb | wbuf-cons(bleb, wbuf, avol, rofs), ebm-vol-inv(avol), # lpt = # avol, ¬ rofs → bleb = buffered(m) ∨ (bleb = nobuffer ∨ wbuf.nbytes = 0) ∧ m < # avol ∧ avol[m].mapped? ∧ m0 = # avol[m].data ⊦ ⟪wbuf_add_log_leb#(m, m0, rofs, adr, m1, avol, lpt, ns; bleb, wbuf, plog; err)⟫ wbuf-cons(bleb, wbuf, avol, rofs) | A Proof Obligation |
| inv-remap | wbuf-cons(bleb, wbuf, avol, rofs), ebm-vol-inv(avol), # lpt = # avol, m < # avol, buffered(m) ≠ bleb ⊦ ⟪wbuf_remap#(m, bleb, adr, m0, plog, lpt, ns; avol; err)⟫ (wbuf-cons(bleb, wbuf, avol, rofs) ∧ ebm-vol-inv(avol) ∧ # lpt = # avol) | A Proof Obligation |
| inv-unmap | wbuf-cons(bleb, wbuf, avol, rofs), ebm-vol-inv(avol), # lpt = # avol, m < # avol, buffered(m) ≠ bleb ⊦ ⟪wbuf_unmap#(m, bleb, adr, m0, plog, lpt, ns; avol)⟫ (wbuf-cons(bleb, wbuf, avol, rofs) ∧ ebm-vol-inv(avol) ∧ # lpt = # avol) | A Proof Obligation |
| inv-get-leb-size | wbuf-cons(bleb, wbuf, avol, rofs), ebm-vol-inv(avol), # lpt = # avol ⊦ ⟪wbuf_get_leb_size#(adr, m, plog, avol, lpt, ns; ; n)⟫ true | A Proof Obligation |
| inv-get-page-size | m = EB_PAGE_SIZE ⊦ ⟪wbuf_get_page_size#(m; ; n)⟫ true | A Proof Obligation |
| inv-destroy-buf | wbuf-cons(bleb, wbuf, avol, rofs) ⊦ ⟪wbuf_destroy_buf#(rofs; bleb; err)⟫ wbuf-cons(bleb, wbuf, avol, rofs) | A Proof Obligation |
| inv-is-readonly | wbuf-cons(bleb, wbuf, avol, rofs) ⊦ ⟪wbuf_is_readonly#(rofs; ; rofs0)⟫ true | A Proof Obligation |
| inv-enter-readonly | wbuf-cons(bleb, wbuf, avol, rofs) ⊦ ⟪wbuf_enter_readonly#(; ; rofs)⟫ wbuf-cons(bleb, wbuf, avol, rofs) | A Proof Obligation |
| aligndown-simp | ⊦ m < EB_PAGE_SIZE ∧ EB_PAGE_SIZE ≤ n + m → (align↓(m + n, EB_PAGE_SIZE) < m ↔ false) | A User Theorem |