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: |
|---|---|---|
| read | ebm_avol_read#(LNUM, OFFSET, N0, N, AVOL; BUF; ERR) {if LNUM < # AVOL ∧ AVOL[LNUM].mapped? ∧ N0 + N ≤ # BUF ∧ OFFSET + N ≤ LEB_SIZE then {fail_or_success#(; ; ERR); if ERR = ESUCCESS then BUF := copy(AVOL[LNUM].data + mkempbuf(LEB_SIZE - # AVOL[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 | ebm_avol_write#(LNUM, OFFSET, N0, N, BUF; AVOL; ERR) {if LNUM < # AVOL ∧ AVOL[LNUM].mapped? ∧ # AVOL[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 AVOL[LNUM] := mapped(AVOL[LNUM].data + mkempbuf(OFFSET - # AVOL[LNUM].data) + subarray(BUF, N0, N)) else choose N1 with N1 < N ∧ is-aligned(N1, EB_PAGE_SIZE) in if N1 ≠ 0 then AVOL[LNUM] := mapped(AVOL[LNUM].data + mkempbuf(OFFSET - # AVOL[LNUM].data) + subarray(BUF, N0, N1)) ifnone skip} else abort } | An Axiom |
| remap | ebm_avol_remap#(LNUM; AVOL; ERR) {if LNUM < # AVOL then {fail_or_success#(; ; ERR); if ERR = ESUCCESS then AVOL[LNUM] := mapped(mkbuf(0)) else {skip or AVOL[LNUM] := unmapped}} else abort } | An Axiom |
| change | ebm_avol_change#(LNUM, N, BUF; AVOL; ERR) {if LNUM < # AVOL ∧ N ≤ # BUF ∧ N ≤ LEB_SIZE ∧ is-aligned(N, EB_PAGE_SIZE) then {fail_or_success#(; ; ERR); if ERR = ESUCCESS then AVOL[LNUM] := mapped(subarray(BUF, 0, N))} else abort } | An Axiom |
| unmap | ebm_avol_unmap#(LNUM; AVOL){if LNUM < # AVOL then AVOL[LNUM] := unmapped else abort} | An Axiom |
| get-volume-size | ebm_avol_get_volume_size#(AVOL; ; N){N := # AVOL} | An Axiom |
| format | ebm_avol_format#(VOLSIZE; ; AVOL, ERR) {fail_or_success#(; ; ERR); if ERR = ESUCCESS then AVOL := fill(mkavolume(VOLSIZE), unmapped) else AVOL := ?} | An Axiom |
| recover | ebm_avol_recover#(; AVOL; ERR){fail_or_success#(; ; ERR); if ERR ≠ ESUCCESS then AVOL := ?} | An Axiom |
| sync-device | ebm_avol_sync_device#(AVOL; ; ERR){fail_or_success#(; ; ERR)} | An Axiom |
| get-leb-size | ebm_avol_get_leb_size#(AVOL; ; N){N := LEB_SIZE} | An Axiom |
| get-page-size | ebm_avol_get_page_size#(AVOL; ; N){N := EB_PAGE_SIZE} | An Axiom |
| inv-format | ⊦ ⟪ebm_avol_format#(m; ; avol, err)⟫ (err = ESUCCESS → ebm-vol-inv(avol)) | A Proof Obligation |
| inv-unmap | ebm-vol-inv(avol), m < # avol ⊦ ⟪ebm_avol_unmap#(m; avol)⟫ ebm-vol-inv(avol) | A Proof Obligation |
| inv-remap | ebm-vol-inv(avol), m < # avol ⊦ ⟪ebm_avol_remap#(m; avol; err)⟫ ebm-vol-inv(avol) | A Proof Obligation |
| inv-change | ebm-vol-inv(avol), m < # avol, n ≤ # buf, n ≤ LEB_SIZE, is-aligned(n, EB_PAGE_SIZE) ⊦ ⟪ebm_avol_change#(m, n, buf; avol; err)⟫ ebm-vol-inv(avol) | A Proof Obligation |
| inv-read | ebm-vol-inv(avol), m < # avol, avol[m].mapped?, n + n0 ≤ # buf, m0 + n0 ≤ LEB_SIZE ⊦ ⟪ebm_avol_read#(m, m0, n, n0, avol; buf; err)⟫ true | A Proof Obligation |
| inv-write | ebm-vol-inv(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 ⊦ ⟪ebm_avol_write#(m, m0, n0, n, buf; avol; err)⟫ ebm-vol-inv(avol) | A Proof Obligation |
| inv-recover | avol ⊆ avol0, ebm-vol-inv(avol) ⊦ ⟪ebm_avol_recover#(; avol0; err)⟫ (err = ESUCCESS → ebm-vol-inv(avol0)) | A Proof Obligation |
| crash-neutral-unmap | m < # avol, ebm-vol-inv(avol), avol ⊆ avol0 ⊦ ⟨ebm_avol_unmap#(m; avol)⟩ (avol ⊆ avol0) | A Proof Obligation |
| crash-neutral-remap | m < # avol, ebm-vol-inv(avol), avol ⊆ avol0 ⊦ ⟨ebm_avol_remap#(m; avol; err)⟩ (avol ⊆ avol0) | A Proof Obligation |
| crash-neutral-change | m < # avol, n ≤ # buf, n ≤ LEB_SIZE, is-aligned(n, EB_PAGE_SIZE), ebm-vol-inv(avol), avol ⊆ avol0 ⊦ ⟨ebm_avol_change#(m, n, buf; avol; err)⟩ (avol ⊆ avol0) | A Proof Obligation |
| crash-neutral-read | m < # avol, avol[m].mapped?, n + n0 ≤ # buf, m0 + n0 ≤ LEB_SIZE, ebm-vol-inv(avol), avol ⊆ avol0 ⊦ ⟨ebm_avol_read#(m, m0, n, n0, avol; buf; err)⟩ (avol ⊆ avol0) | 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), avol ⊆ avol0 ⊦ ⟨ebm_avol_write#(m, m0, n0, n, buf; avol; err)⟩ (avol ⊆ avol0) | A Proof Obligation |
| crash-neutral-get-volume-size | ebm-vol-inv(avol), avol ⊆ avol0 ⊦ ⟨ebm_avol_get_volume_size#(avol; ; n)⟩ (avol ⊆ avol0) | A Proof Obligation |
| inv-get-volume-size | ebm-vol-inv(avol) ⊦ ⟪ebm_avol_get_volume_size#(avol; ; n)⟫ true | A Proof Obligation |
| crash-neutral-sync-device | ebm-vol-inv(avol), avol ⊆ avol0 ⊦ ⟨ebm_avol_sync_device#(avol; ; err)⟩ (avol ⊆ avol0) | A Proof Obligation |
| inv-sync-device | ebm-vol-inv(avol) ⊦ ⟪ebm_avol_sync_device#(avol; ; err)⟫ true | A Proof Obligation |
| crash-neutral-get-leb-size | ebm-vol-inv(avol), avol ⊆ avol0 ⊦ ⟨ebm_avol_get_leb_size#(avol; ; n)⟩ (avol ⊆ avol0) | A Proof Obligation |
| crash-neutral-get-page-size | ebm-vol-inv(avol), avol ⊆ avol0 ⊦ ⟨ebm_avol_get_page_size#(avol; ; n)⟩ (avol ⊆ avol0) | A Proof Obligation |
| inv-get-leb-size | ebm-vol-inv(avol) ⊦ ⟪ebm_avol_get_leb_size#(avol; ; n)⟫ true | A Proof Obligation |
| inv-get-page-size | ebm-vol-inv(avol) ⊦ ⟪ebm_avol_get_page_size#(avol; ; n)⟫ true | A Proof Obligation |
| crash-neutral-recover | ebm-vol-inv(avol), avol ⊆ avol0 ⊦ ⟨ebm_avol_recover#(; avol; err)⟩ (avol ⊆ avol0) | A Proof Obligation |