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: |
|---|---|---|
| remap | awbuf_remap#(LNUM, WROOTADR, WMAXINO, WLOG, WLPT, WORPHANS, WBUFLEB, AROFS; WVOL; ERR) {if synced(WVOL) ∧ LNUM < # WVOL ∧ buffered(LNUM) ≠ WBUFLEB then {fail_or_success#(; ; ERR); if ERR = ESUCCESS then WVOL[LNUM] := mapped(mkbuf(0)) else {skip or WVOL[LNUM] := unmapped}} else abort } | An Axiom |
| read-buf | awbuf_read_buf#(LNUM, OFFSET, N, WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, WBUFLEB, AROFS; BUF; ERR) {if LNUM < # WVOL ∧ N ≤ # BUF ∧ OFFSET + N ≤ LEB_SIZE ∧ WVOL[LNUM].mapped? then {fail_or_success#(; ; ERR); if ERR = ESUCCESS then BUF := copy(WVOL[LNUM].data + mkempbuf(LEB_SIZE - # WVOL[LNUM].data), OFFSET, BUF, 0, N) else choose BUF0 with # BUF0 = # BUF ∧ range=(BUF0, N, BUF, N, # BUF - N) in BUF := BUF0} else abort } | An Axiom |
| write-buf | awbuf_write_buf#(N, BUF, WROOTADR, WMAXINO, WLOG, WLPT, WORPHANS, WBUFLEB; WVOL, AROFS; ERR) {if WBUFLEB ≠ nobuffer ∧ # WVOL[WBUFLEB.leb].data + N ≤ LEB_SIZE ∧ N ≤ # BUF then if AROFS then ERR := EROFS else {fail_or_success#(; ; ERR); let LNUM = WBUFLEB.leb in if ERR = ESUCCESS then WVOL[LNUM] := mapped(WVOL[LNUM].data + subarray(BUF, 0, N)) else { choose N0 with N0 ≠ 0 ∧ N0 < N ∧ is-aligned(# WVOL[LNUM].data + N0, EB_PAGE_SIZE) in WVOL[LNUM] := mapped(WVOL[LNUM].data + subarray(BUF, 0, N0)) ifnone skip or skip; AROFS := true}} else abort } | An Axiom |
| unmap | awbuf_unmap#(LNUM, WROOTADR, WMAXINO, WLOG, WLPT, WORPHANS, WBUFLEB, AROFS; WVOL) {if synced(WVOL) ∧ LNUM < # WVOL ∧ buffered(LNUM) ≠ WBUFLEB then WVOL[LNUM] := unmapped else abort} | An Axiom |
| get-volume-size | awbuf_get_volume_size#(WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, WBUFLEB, AROFS; ; N){N := # WVOL} | An Axiom |
| format | awbuf_format#(VOLSIZE, SIZE, LPT, WROOTADR0, WMAXINO0; ; WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, WBUFLEB, AROFS, ERR) {if # LPT = VOLSIZE ∧ SIZE = LEB_SIZE then {fail_or_success#(; ; ERR); if ERR = ESUCCESS then {WVOL := fill(mkavolume(VOLSIZE), unmapped); WROOTADR := WROOTADR0; WMAXINO := WMAXINO0; WLOG := []; WLPT := LPT; WORPHANS := ∅; WBUFLEB := nobuffer; AROFS := false} else WVOL := ?, WBUFLEB := ?, AROFS := ?, WROOTADR := ?, WMAXINO := ?, WLOG := ?, WLPT := ?, WORPHANS := ?} else abort } | An Axiom |
| recover | awbuf_recover#(; WROOTADR0, WMAXINO0, ORPHANS, LOG, LPT, WROOTADR, WMAXINO, WLOG, WLPT, WORPHANS, WVOL; WBUFLEB, AROFS, ERR) {fail_or_success#(; ; ERR); if ERR = ESUCCESS then WBUFLEB := nobuffer, AROFS := false, WROOTADR0 := WROOTADR, WMAXINO0 := WMAXINO, LOG := WLOG, LPT := WLPT, ORPHANS := WORPHANS else WVOL := ?, WBUFLEB := ?, AROFS := ?, WROOTADR := ?, WMAXINO := ?, WLOG := ?, WLPT := ?, WROOTADR0 := ?, WMAXINO0 := ?, LOG := ?, LPT := ?, ORPHANS := ?, WORPHANS := ? } | An Axiom |
| add-log-leb | awbuf_add_log_leb#(LNUM, OFFSET, WROOTADR, WMAXINO, WVOL, WLPT, WORPHANS, AROFS; WLOG, WBUFLEB; ERR) {if LNUM < # WVOL ∧ WVOL[LNUM].mapped? ∧ OFFSET = # WVOL[LNUM].data ∧ synced(WVOL) then {fail_or_success#(; ; ERR); if ERR = ESUCCESS then WLOG := WLOG + LNUM, WBUFLEB := buffered(LNUM)} else abort } | An Axiom |
| requires-commit | awbuf_requires_commit#(WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, WBUFLEB, AROFS; ; COMMIT?){COMMIT? := ?} | An Axiom |
| commit | awbuf_commit#(LPT, WROOTADR0, WMAXINO0, WVOL, WBUFLEB; ORPHANS, WROOTADR, WMAXINO, WLOG, WLPT, WORPHANS, AROFS; ERR) {if synced(WVOL) ∧ # LPT = # WVOL then {fail_or_success#(; ; ERR); if ERR = ESUCCESS then {WROOTADR := WROOTADR0; WMAXINO := WMAXINO0; WLOG := []; WLPT := LPT; WORPHANS := ORPHANS} else AROFS := true; ORPHANS := ?} else abort } | An Axiom |
| move-buf | awbuf_move_buf#(LNUM, OFFSET, WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, AROFS; WBUFLEB; ERR) {if WBUFLEB = buffered(LNUM) ∨ (WBUFLEB = nobuffer ∨ is-aligned(# WVOL[WBUFLEB.leb].data, EB_PAGE_SIZE)) ∧ LNUM < # WVOL ∧ WVOL[LNUM].mapped? ∧ OFFSET = # WVOL[LNUM].data then {fail_or_success#(; ; ERR); if ERR = ESUCCESS then WBUFLEB := buffered(LNUM)} else abort } | An Axiom |
| get-leb-size | awbuf_get_leb_size#(WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, WBUFLEB, AROFS; ; N){N := LEB_SIZE} | An Axiom |
| get-page-size | awbuf_get_page_size#(WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, WBUFLEB, AROFS; ; N){N := EB_PAGE_SIZE} | An Axiom |
| destroy-buf | awbuf_destroy_buf#(WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, AROFS; WBUFLEB; ERR) {if synced(WVOL) then if AROFS then ERR := EROFS else WBUFLEB := nobuffer, ERR := ESUCCESS else abort} | An Axiom |
| get-buf | awbuf_get_buf#(WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, WBUFLEB, AROFS; ; WBUFLEB0){WBUFLEB0 := WBUFLEB} | An Axiom |
| is-readonly | awbuf_is_readonly#(WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, WBUFLEB, AROFS; ; AROFS0){AROFS0 := AROFS} | An Axiom |
| enter-readonly | awbuf_enter_readonly#(WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, WBUFLEB; ; AROFS){AROFS := true} | An Axiom |
| inv-format | # lpt = m, m0 = LEB_SIZE ⊦ ⟪awbuf_format#(m, m0, lpt, adr, m1; ; adr0, m2, nx, avol, lpt0, ns, bleb, isbuf, err)⟫ (err = ESUCCESS → synced(avol) ∧ awbuf-inv(avol, bleb) ∧ # lpt0 = # avol) | A Proof Obligation |
| synced-get-volume-size | ⟨awbuf_get_volume_size#(adr, m, nx, avol, lpt, ns, bleb, isbuf; ; n)⟩ (adr0 = adr ∧ m0 = m ∧ nx0 = nx ∧ lpt0 = lpt ∧ avol0 ↓ avol ∧ ns0 = ns), awbuf-inv(avol, bleb), # lpt = # avol ⊦ ⟨awbuf_get_volume_size#(adr, m, nx, avol, lpt, ns, bleb, isbuf; ; n)⟩ (synced(avol) ∧ adr0 = adr ∧ m0 = m ∧ nx0 = nx ∧ lpt0 = lpt ∧ avol0 ↓ avol ∧ ns0 = ns), adr0 = adr ∧ m0 = m ∧ nx0 = nx ∧ lpt0 = lpt ∧ avol0 ↓ avol ∧ ns0 = ns | A Proof Obligation |
| synced-get-buf | ⟨awbuf_get_buf#(adr, m, nx, avol, lpt, ns, bleb, isbuf; ; bleb0)⟩ (adr0 = adr ∧ m0 = m ∧ nx0 = nx ∧ lpt0 = lpt ∧ avol0 ↓ avol ∧ ns0 = ns), awbuf-inv(avol, bleb), # lpt = # avol ⊦ ⟨awbuf_get_buf#(adr, m, nx, avol, lpt, ns, bleb, isbuf; ; bleb0)⟩ (synced(avol) ∧ adr0 = adr ∧ m0 = m ∧ nx0 = nx ∧ lpt0 = lpt ∧ avol0 ↓ avol ∧ ns0 = ns), adr0 = adr ∧ m0 = m ∧ nx0 = nx ∧ lpt0 = lpt ∧ avol0 ↓ avol ∧ ns0 = ns | A Proof Obligation |
| synced-is-readonly | ⟨awbuf_is_readonly#(adr, m, nx, avol, lpt, ns, bleb, isbuf; ; isbuf0)⟩ (adr0 = adr ∧ m0 = m ∧ nx0 = nx ∧ lpt0 = lpt ∧ avol0 ↓ avol ∧ ns0 = ns), awbuf-inv(avol, bleb), # lpt = # avol ⊦ ⟨awbuf_is_readonly#(adr, m, nx, avol, lpt, ns, bleb, isbuf; ; isbuf0)⟩ (synced(avol) ∧ adr0 = adr ∧ m0 = m ∧ nx0 = nx ∧ lpt0 = lpt ∧ avol0 ↓ avol ∧ ns0 = ns), adr0 = adr ∧ m0 = m ∧ nx0 = nx ∧ lpt0 = lpt ∧ avol0 ↓ avol ∧ ns0 = ns | A Proof Obligation |
| synced-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, ⟨awbuf_move_buf#(m, m0, adr, m1, nx, avol, lpt, ns, isbuf; bleb; err)⟩ (adr0 = adr ∧ m2 = m1 ∧ nx0 = nx ∧ lpt0 = lpt ∧ avol0 ↓ avol ∧ ns0 = ns), awbuf-inv(avol, bleb), # lpt = # avol ⊦ ⟨awbuf_move_buf#(m, m0, adr, m1, nx, avol, lpt, ns, isbuf; bleb; err)⟩ (synced(avol) ∧ adr0 = adr ∧ m2 = m1 ∧ nx0 = nx ∧ lpt0 = lpt ∧ avol0 ↓ avol ∧ ns0 = ns), adr0 = adr ∧ m2 = m1 ∧ nx0 = nx ∧ lpt0 = lpt ∧ avol0 ↓ avol ∧ ns0 = ns | A Proof Obligation |
| synced-destroy-buf | synced(avol), ⟨awbuf_destroy_buf#(adr, m, nx, avol, lpt, ns, isbuf; bleb; err)⟩ (adr0 = adr ∧ m0 = m ∧ nx0 = nx ∧ lpt0 = lpt ∧ avol0 ↓ avol ∧ ns0 = ns), awbuf-inv(avol, bleb), # lpt = # avol ⊦ ⟨awbuf_destroy_buf#(adr, m, nx, avol, lpt, ns, isbuf; bleb; err)⟩ (synced(avol) ∧ adr0 = adr ∧ m0 = m ∧ nx0 = nx ∧ lpt0 = lpt ∧ avol0 ↓ avol ∧ ns0 = ns), adr0 = adr ∧ m0 = m ∧ nx0 = nx ∧ lpt0 = lpt ∧ avol0 ↓ avol ∧ ns0 = ns | A Proof Obligation |
| synced-write-buf | bleb ≠ nobuffer, # avol[bleb.leb].data + n ≤ LEB_SIZE, n ≤ # buf, ⟨awbuf_write_buf#(n, buf, adr, m, nx, lpt, ns, bleb; avol, isbuf; err)⟩ (adr0 = adr ∧ m0 = m ∧ nx0 = nx ∧ lpt0 = lpt ∧ avol0 ↓ avol ∧ ns0 = ns), awbuf-inv(avol, bleb), # lpt = # avol ⊦ ⟨awbuf_write_buf#(n, buf, adr, m, nx, lpt, ns, bleb; avol, isbuf; err)⟩ (synced(avol) ∧ adr0 = adr ∧ m0 = m ∧ nx0 = nx ∧ lpt0 = lpt ∧ avol0 ↓ avol ∧ ns0 = ns), adr0 = adr ∧ m0 = m ∧ nx0 = nx ∧ lpt0 = lpt ∧ avol0 ↓ avol ∧ ns0 = ns | A Proof Obligation |
| synced-commit | synced(avol), # lpt = # avol, ⟨awbuf_commit#(lpt, adr, m, avol, bleb; ns, adr0, m0, nx, lpt0, ns0, isbuf; err)⟩ (adr1 = adr0 ∧ m1 = m0 ∧ nx0 = nx ∧ lpt1 = lpt0 ∧ avol0 ↓ avol ∧ ns1 = ns0), awbuf-inv(avol, bleb), # lpt0 = # avol ⊦ ⟨awbuf_commit#(lpt, adr, m, avol, bleb; ns, adr0, m0, nx, lpt0, ns0, isbuf; err)⟩ (synced(avol) ∧ adr1 = adr0 ∧ m1 = m0 ∧ nx0 = nx ∧ lpt1 = lpt0 ∧ avol0 ↓ avol ∧ ns1 = ns0), adr1 = adr0 ∧ m1 = m0 ∧ nx0 = nx ∧ lpt1 = lpt0 ∧ avol0 ↓ avol ∧ ns1 = ns0 | A Proof Obligation |
| synced-requires-commit | ⟨awbuf_requires_commit#(adr, m, nx, avol, lpt, ns, bleb, isbuf; ; isbuf0)⟩ (adr0 = adr ∧ m0 = m ∧ nx0 = nx ∧ lpt0 = lpt ∧ avol0 ↓ avol ∧ ns0 = ns), awbuf-inv(avol, bleb), # lpt = # avol ⊦ ⟨awbuf_requires_commit#(adr, m, nx, avol, lpt, ns, bleb, isbuf; ; isbuf0)⟩ (synced(avol) ∧ adr0 = adr ∧ m0 = m ∧ nx0 = nx ∧ lpt0 = lpt ∧ avol0 ↓ avol ∧ ns0 = ns), adr0 = adr ∧ m0 = m ∧ nx0 = nx ∧ lpt0 = lpt ∧ avol0 ↓ avol ∧ ns0 = ns | A Proof Obligation |
| synced-add-log-leb | m < # avol, avol[m].mapped?, m0 = # avol[m].data, synced(avol), ⟨awbuf_add_log_leb#(m, m0, adr, m1, avol, lpt, ns, isbuf; nx, bleb; err)⟩ (adr0 = adr ∧ m2 = m1 ∧ nx0 = nx ∧ lpt0 = lpt ∧ avol0 ↓ avol ∧ ns0 = ns), awbuf-inv(avol, bleb), # lpt = # avol ⊦ ⟨awbuf_add_log_leb#(m, m0, adr, m1, avol, lpt, ns, isbuf; nx, bleb; err)⟩ (synced(avol) ∧ adr0 = adr ∧ m2 = m1 ∧ nx0 = nx ∧ lpt0 = lpt ∧ avol0 ↓ avol ∧ ns0 = ns), adr0 = adr ∧ m2 = m1 ∧ nx0 = nx ∧ lpt0 = lpt ∧ avol0 ↓ avol ∧ ns0 = ns | A Proof Obligation |
| synced-read-buf | m < # avol, n ≤ # buf, m0 + n ≤ LEB_SIZE, avol[m].mapped?, ⟨awbuf_read_buf#(m, m0, n, adr, m1, nx, avol, lpt, ns, bleb, isbuf; buf; err)⟩ (adr0 = adr ∧ m2 = m1 ∧ nx0 = nx ∧ lpt0 = lpt ∧ avol0 ↓ avol ∧ ns0 = ns), awbuf-inv(avol, bleb), # lpt = # avol ⊦ ⟨awbuf_read_buf#(m, m0, n, adr, m1, nx, avol, lpt, ns, bleb, isbuf; buf; err)⟩ (synced(avol) ∧ adr0 = adr ∧ m2 = m1 ∧ nx0 = nx ∧ lpt0 = lpt ∧ avol0 ↓ avol ∧ ns0 = ns), adr0 = adr ∧ m2 = m1 ∧ nx0 = nx ∧ lpt0 = lpt ∧ avol0 ↓ avol ∧ ns0 = ns | A Proof Obligation |
| synced-remap | synced(avol), m < # avol, buffered(m) ≠ bleb, ⟨awbuf_remap#(m, adr, m0, nx, lpt, ns, bleb, isbuf; avol; err)⟩ (adr0 = adr ∧ m1 = m0 ∧ nx0 = nx ∧ lpt0 = lpt ∧ avol0 ↓ avol ∧ ns0 = ns), awbuf-inv(avol, bleb), # lpt = # avol ⊦ ⟨awbuf_remap#(m, adr, m0, nx, lpt, ns, bleb, isbuf; avol; err)⟩ (synced(avol) ∧ adr0 = adr ∧ m1 = m0 ∧ nx0 = nx ∧ lpt0 = lpt ∧ avol0 ↓ avol ∧ ns0 = ns), adr0 = adr ∧ m1 = m0 ∧ nx0 = nx ∧ lpt0 = lpt ∧ avol0 ↓ avol ∧ ns0 = ns | A Proof Obligation |
| synced-unmap | synced(avol), m < # avol, buffered(m) ≠ bleb, ⟨awbuf_unmap#(m, adr, m0, nx, lpt, ns, bleb, isbuf; avol)⟩ (adr0 = adr ∧ m1 = m0 ∧ nx0 = nx ∧ lpt0 = lpt ∧ avol0 ↓ avol ∧ ns0 = ns), awbuf-inv(avol, bleb), # lpt = # avol ⊦ ⟨awbuf_unmap#(m, adr, m0, nx, lpt, ns, bleb, isbuf; avol)⟩ (synced(avol) ∧ adr0 = adr ∧ m1 = m0 ∧ nx0 = nx ∧ lpt0 = lpt ∧ avol0 ↓ avol ∧ ns0 = ns), adr0 = adr ∧ m1 = m0 ∧ nx0 = nx ∧ lpt0 = lpt ∧ avol0 ↓ avol ∧ ns0 = ns | A Proof Obligation |
| synced-get-page-size | ⟨awbuf_get_page_size#(adr, m, nx, avol, lpt, ns, bleb, isbuf; ; n)⟩ (adr0 = adr ∧ m0 = m ∧ nx0 = nx ∧ lpt0 = lpt ∧ avol0 ↓ avol ∧ ns0 = ns), awbuf-inv(avol, bleb), # lpt = # avol ⊦ ⟨awbuf_get_page_size#(adr, m, nx, avol, lpt, ns, bleb, isbuf; ; n)⟩ (synced(avol) ∧ adr0 = adr ∧ m0 = m ∧ nx0 = nx ∧ lpt0 = lpt ∧ avol0 ↓ avol ∧ ns0 = ns), adr0 = adr ∧ m0 = m ∧ nx0 = nx ∧ lpt0 = lpt ∧ avol0 ↓ avol ∧ ns0 = ns | A Proof Obligation |
| synced-get-leb-size | ⟨awbuf_get_leb_size#(adr, m, nx, avol, lpt, ns, bleb, isbuf; ; n)⟩ (adr0 = adr ∧ m0 = m ∧ nx0 = nx ∧ lpt0 = lpt ∧ avol0 ↓ avol ∧ ns0 = ns), awbuf-inv(avol, bleb), # lpt = # avol ⊦ ⟨awbuf_get_leb_size#(adr, m, nx, avol, lpt, ns, bleb, isbuf; ; n)⟩ (synced(avol) ∧ adr0 = adr ∧ m0 = m ∧ nx0 = nx ∧ lpt0 = lpt ∧ avol0 ↓ avol ∧ ns0 = ns), adr0 = adr ∧ m0 = m ∧ nx0 = nx ∧ lpt0 = lpt ∧ avol0 ↓ avol ∧ ns0 = ns | A Proof Obligation |
| inv-get-buf | awbuf-inv(avol, bleb), # lpt = # avol ⊦ ⟪awbuf_get_buf#(adr, m, nx, avol, lpt, ns, bleb, isbuf; ; bleb0)⟫ true | A Proof Obligation |
| crash-neutral-get-buf | awbuf-inv(avol, bleb), # lpt = # avol, synced(avol0), adr = adr0, m = m0, nx = nx0, lpt0 = lpt, avol0 ↓ avol, ns = ns0 ⊦ ⟨awbuf_get_buf#(adr0, m0, nx0, avol, lpt, ns0, bleb, isbuf; ; bleb0)⟩ (synced(avol0) ∧ adr = adr0 ∧ m = m0 ∧ nx = nx0 ∧ lpt0 = lpt ∧ avol0 ↓ avol ∧ ns = ns0) | A Proof Obligation |
| inv-unmap | awbuf-inv(avol, bleb), # lpt = # avol, synced(avol), m < # avol, buffered(m) ≠ bleb ⊦ ⟪awbuf_unmap#(m, adr, m0, nx, lpt, ns, bleb, isbuf; avol)⟫ (awbuf-inv(avol, bleb) ∧ # lpt = # avol) | A Proof Obligation |
| inv-remap | awbuf-inv(avol, bleb), # lpt = # avol, synced(avol), m < # avol, buffered(m) ≠ bleb ⊦ ⟪awbuf_remap#(m, adr, m0, nx, lpt, ns, bleb, isbuf; avol; err)⟫ (awbuf-inv(avol, bleb) ∧ # lpt = # avol) | A Proof Obligation |
| inv-read-buf | awbuf-inv(avol, bleb), # lpt = # avol, m < # avol, n ≤ # buf, m0 + n ≤ LEB_SIZE, avol[m].mapped? ⊦ ⟪awbuf_read_buf#(m, m0, n, adr, m1, nx, avol, lpt, ns, bleb, isbuf; buf; err)⟫ true | A Proof Obligation |
| inv-write-buf | awbuf-inv(avol, bleb), # lpt = # avol, bleb ≠ nobuffer, # avol[bleb.leb].data + n ≤ LEB_SIZE, n ≤ # buf ⊦ ⟪awbuf_write_buf#(n, buf, adr, m, nx, lpt, ns, bleb; avol, isbuf; err)⟫ (awbuf-inv(avol, bleb) ∧ # lpt = # avol) | A Proof Obligation |
| inv-recover | adr = adr0, m = m0, nx = nx0, lpt = lpt0, avol ↓ avol0, ns = ns0, awbuf-inv(avol0, bleb), # lpt0 = # avol0 ⊦ ⟪awbuf_recover#(; adr1, m1, ns1, nx1, lpt1, adr, m, nx, lpt, ns, avol; bleb0, isbuf, err)⟫ (err = ESUCCESS → synced(avol) ∧ awbuf-inv(avol, bleb0) ∧ # lpt = # avol) | A Proof Obligation |
| crash-neutral-unmap | synced(avol), m < # avol, buffered(m) ≠ bleb, awbuf-inv(avol, bleb), # lpt = # avol, synced(avol0), adr = adr0, m0 = m1, nx = nx0, lpt0 = lpt, avol0 ↓ avol, ns = ns0 ⊦ ⟨awbuf_unmap#(m, adr0, m1, nx0, lpt, ns0, bleb, isbuf; avol)⟩ (synced(avol0) ∧ adr = adr0 ∧ m0 = m1 ∧ nx = nx0 ∧ lpt0 = lpt ∧ avol0 ↓ avol ∧ ns = ns0) | A Proof Obligation |
| crash-neutral-remap | synced(avol), m < # avol, buffered(m) ≠ bleb, awbuf-inv(avol, bleb), # lpt = # avol, synced(avol0), adr = adr0, m0 = m1, nx = nx0, lpt0 = lpt, avol0 ↓ avol, ns = ns0 ⊦ ⟨awbuf_remap#(m, adr0, m1, nx0, lpt, ns0, bleb, isbuf; avol; err)⟩ (synced(avol0) ∧ adr = adr0 ∧ m0 = m1 ∧ nx = nx0 ∧ lpt0 = lpt ∧ avol0 ↓ avol ∧ ns = ns0) | A Proof Obligation |
| crash-neutral-read-buf | m < # avol, n ≤ # buf, m0 + n ≤ LEB_SIZE, avol[m].mapped?, awbuf-inv(avol, bleb), # lpt = # avol, synced(avol0), adr = adr0, m1 = m2, nx = nx0, lpt0 = lpt, avol0 ↓ avol, ns = ns0 ⊦ ⟨awbuf_read_buf#(m, m0, n, adr0, m2, nx0, avol, lpt, ns0, bleb, isbuf; buf; err)⟩ (synced(avol0) ∧ adr = adr0 ∧ m1 = m2 ∧ nx = nx0 ∧ lpt0 = lpt ∧ avol0 ↓ avol ∧ ns = ns0) | A Proof Obligation |
| crash-neutral-write-buf | bleb ≠ nobuffer, # avol[bleb.leb].data + n ≤ LEB_SIZE, n ≤ # buf, awbuf-inv(avol, bleb), # lpt = # avol, synced(avol0), adr = adr0, m = m0, nx = nx0, lpt0 = lpt, avol0 ↓ avol, ns = ns0 ⊦ ⟨awbuf_write_buf#(n, buf, adr0, m0, nx0, lpt, ns0, bleb; avol, isbuf; err)⟩ (synced(avol0) ∧ adr = adr0 ∧ m = m0 ∧ nx = nx0 ∧ lpt0 = lpt ∧ avol0 ↓ avol ∧ ns = ns0) | A Proof Obligation |
| crash-neutral-get-volume-size | awbuf-inv(avol, bleb), # lpt = # avol, synced(avol0), adr = adr0, m = m0, nx = nx0, lpt0 = lpt, avol0 ↓ avol, ns = ns0 ⊦ ⟨awbuf_get_volume_size#(adr0, m0, nx0, avol, lpt, ns0, bleb, isbuf; ; n)⟩ (synced(avol0) ∧ adr = adr0 ∧ m = m0 ∧ nx = nx0 ∧ lpt0 = lpt ∧ avol0 ↓ avol ∧ ns = ns0) | A Proof Obligation |
| inv-get-volume-size | awbuf-inv(avol, bleb), # lpt = # avol ⊦ ⟪awbuf_get_volume_size#(adr, m, nx, avol, lpt, ns, bleb, isbuf; ; n)⟫ true | A Proof Obligation |
| crash-neutral-add-log-leb | m < # avol, avol[m].mapped?, m0 = # avol[m].data, synced(avol), awbuf-inv(avol, bleb), # lpt = # avol, synced(avol0), adr = adr0, m1 = m2, nx = nx0, lpt0 = lpt, avol0 ↓ avol, ns = ns0 ⊦ ⟨awbuf_add_log_leb#(m, m0, adr0, m2, avol, lpt, ns0, isbuf; nx0, bleb; err)⟩ (synced(avol0) ∧ adr = adr0 ∧ m1 = m2 ∧ nx = nx0 ∧ lpt0 = lpt ∧ avol0 ↓ avol ∧ ns = ns0) | A Proof Obligation |
| inv-add-log-leb | awbuf-inv(avol, bleb), # lpt = # avol, m < # avol, avol[m].mapped?, m0 = # avol[m].data, synced(avol) ⊦ ⟪awbuf_add_log_leb#(m, m0, adr, m1, avol, lpt, ns, isbuf; nx, bleb; err)⟫ awbuf-inv(avol, bleb) | A Proof Obligation |
| crash-neutral-requires-commit | awbuf-inv(avol, bleb), # lpt = # avol, synced(avol0), adr = adr0, m = m0, nx = nx0, lpt0 = lpt, avol0 ↓ avol, ns = ns0 ⊦ ⟨awbuf_requires_commit#(adr0, m0, nx0, avol, lpt, ns0, bleb, isbuf; ; isbuf0)⟩ (synced(avol0) ∧ adr = adr0 ∧ m = m0 ∧ nx = nx0 ∧ lpt0 = lpt ∧ avol0 ↓ avol ∧ ns = ns0) | A Proof Obligation |
| crash-neutral-commit | synced(avol), # lpt = # avol, awbuf-inv(avol, bleb), # lpt0 = # avol, synced(avol0), adr = adr0, m = m0, nx = nx0, lpt1 = lpt0, avol0 ↓ avol, ns = ns0 ⊦ ⟨awbuf_commit#(lpt, adr1, m1, avol, bleb; ns1, adr0, m0, nx0, lpt0, ns0, isbuf; err)⟩ (synced(avol0) ∧ adr = adr0 ∧ m = m0 ∧ nx = nx0 ∧ lpt1 = lpt0 ∧ avol0 ↓ avol ∧ ns = ns0) | A Proof Obligation |
| inv-requires-commit | awbuf-inv(avol, bleb), # lpt = # avol ⊦ ⟪awbuf_requires_commit#(adr, m, nx, avol, lpt, ns, bleb, isbuf; ; isbuf0)⟫ true | A Proof Obligation |
| inv-commit | awbuf-inv(avol, bleb), # lpt = # avol, synced(avol), # lpt0 = # avol ⊦ ⟪awbuf_commit#(lpt0, adr, m, avol, bleb; ns, adr0, m0, nx, lpt, ns0, isbuf; err)⟫ (# lpt = # avol) | A Proof Obligation |
| crash-neutral-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, awbuf-inv(avol, bleb), # lpt = # avol, synced(avol0), adr = adr0, m1 = m2, nx = nx0, lpt0 = lpt, avol0 ↓ avol, ns = ns0 ⊦ ⟨awbuf_move_buf#(m, m0, adr0, m2, nx0, avol, lpt, ns0, isbuf; bleb; err)⟩ (synced(avol0) ∧ adr = adr0 ∧ m1 = m2 ∧ nx = nx0 ∧ lpt0 = lpt ∧ avol0 ↓ avol ∧ ns = ns0) | A Proof Obligation |
| inv-move-buf | awbuf-inv(avol, bleb), # lpt = # avol, bleb = buffered(m) ∨ (bleb = nobuffer ∨ is-aligned(# avol[bleb.leb].data, EB_PAGE_SIZE)) ∧ m < # avol ∧ avol[m].mapped? ∧ m0 = # avol[m].data ⊦ ⟪awbuf_move_buf#(m, m0, adr, m1, nx, avol, lpt, ns, isbuf; bleb; err)⟫ awbuf-inv(avol, bleb) | A Proof Obligation |
| crash-neutral-get-leb-size | awbuf-inv(avol, bleb), # lpt = # avol, synced(avol0), adr = adr0, m = m0, nx = nx0, lpt0 = lpt, avol0 ↓ avol, ns = ns0 ⊦ ⟨awbuf_get_leb_size#(adr0, m0, nx0, avol, lpt, ns0, bleb, isbuf; ; n)⟩ (synced(avol0) ∧ adr = adr0 ∧ m = m0 ∧ nx = nx0 ∧ lpt0 = lpt ∧ avol0 ↓ avol ∧ ns = ns0) | A Proof Obligation |
| crash-neutral-get-page-size | awbuf-inv(avol, bleb), # lpt = # avol, synced(avol0), adr = adr0, m = m0, nx = nx0, lpt0 = lpt, avol0 ↓ avol, ns = ns0 ⊦ ⟨awbuf_get_page_size#(adr0, m0, nx0, avol, lpt, ns0, bleb, isbuf; ; n)⟩ (synced(avol0) ∧ adr = adr0 ∧ m = m0 ∧ nx = nx0 ∧ lpt0 = lpt ∧ avol0 ↓ avol ∧ ns = ns0) | A Proof Obligation |
| inv-get-leb-size | awbuf-inv(avol, bleb), # lpt = # avol ⊦ ⟪awbuf_get_leb_size#(adr, m, nx, avol, lpt, ns, bleb, isbuf; ; n)⟫ true | A Proof Obligation |
| inv-get-page-size | awbuf-inv(avol, bleb), # lpt = # avol ⊦ ⟪awbuf_get_page_size#(adr, m, nx, avol, lpt, ns, bleb, isbuf; ; n)⟫ true | A Proof Obligation |
| crash-neutral-destroy-buf | synced(avol), awbuf-inv(avol, bleb), # lpt = # avol, synced(avol0), adr = adr0, m = m0, nx = nx0, lpt0 = lpt, avol0 ↓ avol, ns = ns0 ⊦ ⟨awbuf_destroy_buf#(adr0, m0, nx0, avol, lpt, ns0, isbuf; bleb; err)⟩ (synced(avol0) ∧ adr = adr0 ∧ m = m0 ∧ nx = nx0 ∧ lpt0 = lpt ∧ avol0 ↓ avol ∧ ns = ns0) | A Proof Obligation |
| inv-destroy-buf | awbuf-inv(avol, bleb), # lpt = # avol, synced(avol) ⊦ ⟪awbuf_destroy_buf#(adr, m, nx, avol, lpt, ns, isbuf; bleb; err)⟫ awbuf-inv(avol, bleb) | A Proof Obligation |
| crash-neutral-is-readonly | awbuf-inv(avol, bleb), # lpt = # avol, synced(avol0), adr = adr0, m = m0, nx = nx0, lpt0 = lpt, avol0 ↓ avol, ns = ns0 ⊦ ⟨awbuf_is_readonly#(adr0, m0, nx0, avol, lpt, ns0, bleb, isbuf; ; isbuf0)⟩ (synced(avol0) ∧ adr = adr0 ∧ m = m0 ∧ nx = nx0 ∧ lpt0 = lpt ∧ avol0 ↓ avol ∧ ns = ns0) | A Proof Obligation |
| inv-is-readonly | awbuf-inv(avol, bleb), # lpt = # avol ⊦ ⟪awbuf_is_readonly#(adr, m, nx, avol, lpt, ns, bleb, isbuf; ; isbuf0)⟫ true | A Proof Obligation |
| synced-enter-readonly | ⟨awbuf_enter_readonly#(adr, m, nx, avol, lpt, ns, bleb; ; isbuf)⟩ (adr0 = adr ∧ m0 = m ∧ nx0 = nx ∧ lpt0 = lpt ∧ avol0 ↓ avol ∧ ns0 = ns), awbuf-inv(avol, bleb), # lpt = # avol ⊦ ⟨awbuf_enter_readonly#(adr, m, nx, avol, lpt, ns, bleb; ; isbuf)⟩ (synced(avol) ∧ adr0 = adr ∧ m0 = m ∧ nx0 = nx ∧ lpt0 = lpt ∧ avol0 ↓ avol ∧ ns0 = ns), adr0 = adr ∧ m0 = m ∧ nx0 = nx ∧ lpt0 = lpt ∧ avol0 ↓ avol ∧ ns0 = ns | A Proof Obligation |
| crash-neutral-enter-readonly | awbuf-inv(avol, bleb), # lpt = # avol, synced(avol0), adr = adr0, m = m0, nx = nx0, lpt0 = lpt, avol0 ↓ avol, ns = ns0 ⊦ ⟨awbuf_enter_readonly#(adr0, m0, nx0, avol, lpt, ns0, bleb; ; isbuf)⟩ (synced(avol0) ∧ adr = adr0 ∧ m = m0 ∧ nx = nx0 ∧ lpt0 = lpt ∧ avol0 ↓ avol ∧ ns = ns0) | A Proof Obligation |
| inv-enter-readonly | awbuf-inv(avol, bleb), # lpt = # avol ⊦ ⟪awbuf_enter_readonly#(adr, m, nx, avol, lpt, ns, bleb; ; isbuf)⟫ true | A Proof Obligation |
| crash-neutral-recover | awbuf-inv(avol, bleb), # lpt = # avol, synced(avol0), adr = adr0, m = m0, nx = nx0, lpt0 = lpt, avol0 ↓ avol, ns = ns0 ⊦ ⟨awbuf_recover#(; adr1, m1, ns1, nx1, lpt1, adr0, m0, nx0, lpt, ns0, avol; bleb, isbuf, err)⟩ (synced(avol0) ∧ adr = adr0 ∧ m = m0 ∧ nx = nx0 ∧ lpt0 = lpt ∧ avol0 ↓ avol ∧ ns = ns0) | A Proof Obligation |
| fwd-buffered-mapped | ⊦ awbuf-inv(avol, buffered(n)) → n < # avol ∧ avol[n].mapped? | A User Theorem |