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-echdr | aubi_io_read_echdr#(PNUM, APEBS; AEHDR; BITFLIPS, ERR) {if ubi-io-read-echdr-pre(PNUM, APEBS) then {fail_or_success#(; ; ERR); BITFLIPS := ?; if ERR = ESUCCESS then AEHDR := APEBS[PNUM].echdr else AEHDR := ?} else abort } | An Axiom |
| write-echdr | aubi_io_write_echdr#(PNUM, AEHDR; APEBS; ERR) {if ubi-io-write-echdr-pre(PNUM, AEHDR, APEBS) then {fail_or_success#(; ; ERR); if ERR = ESUCCESS then APEBS[PNUM].echdr := AEHDR else choose AEHDR with ¬ AEHDR.valid? in APEBS[PNUM].echdr := AEHDR} else abort } | An Axiom |
| read-vidhdr | aubi_io_read_vidhdr#(PNUM, APEBS; AVHDR; BITFLIPS, ERR) {if ubi-io-read-vidhdr-pre(PNUM, APEBS) then {fail_or_success#(; ; ERR); BITFLIPS := ?; if ERR = ESUCCESS then AVHDR := APEBS[PNUM].vidhdr else AVHDR := ?} else abort } | An Axiom |
| write-vidhdr | aubi_io_write_vidhdr#(PNUM, AVHDR; APEBS; ERR) {if ubi-io-write-vidhdr-pre(PNUM, AVHDR, APEBS) then {fail_or_success#(; ; ERR); if ERR = ESUCCESS then APEBS[PNUM].vidhdr := AVHDR else choose AVHDR with ¬ AVHDR.valid? in APEBS[PNUM].vidhdr := AVHDR} else abort } | An Axiom |
| read-data | aubi_io_read_data#(PNUM, OFFSET, N0, N, APEBS; BUF; BITFLIPS, ERR) {if ubi-io-read-data-pre(PNUM, OFFSET, N0, N, BUF, APEBS) then {fail_or_success#(; ; ERR); BITFLIPS := ?; if ERR = ESUCCESS then BUF := copy(APEBS[PNUM].data, OFFSET, BUF, N0, N) else choose BUF0 with # BUF0 = # BUF ∧ range=(BUF0, 0, BUF, 0, N0) ∧ range=(BUF0, N0 + N, BUF, N0 + N, # BUF - N0 + N) in BUF := BUF0} else abort } | An Axiom |
| write-data | aubi_io_write_data#(PNUM, OFFSET, N0, N, BUF; APEBS; ERR) {if ubi-io-write-data-pre(PNUM, OFFSET, N0, N, BUF, APEBS) then {fail_or_success#(; ; ERR); if ERR = ESUCCESS then APEBS[PNUM] := mkpeb (APEBS[PNUM].echdr, APEBS[PNUM].vidhdr, subarray(APEBS[PNUM].data, 0, OFFSET) + subarray(BUF, N0, N) + mkempbuf(LEB_SIZE - OFFSET - N), OFFSET + N, APEBS[PNUM].bad) else choose N1 with (N1 < N ∨ N1 = 0 ∧ N = 0) ∧ is-aligned(N1, EB_PAGE_SIZE) in if N1 ≠ 0 then APEBS[PNUM] := mkpeb (APEBS[PNUM].echdr, APEBS[PNUM].vidhdr, subarray(APEBS[PNUM].data, 0, OFFSET) + subarray(BUF, N0, N1) + mkempbuf(LEB_SIZE - OFFSET - N1), OFFSET + N1, APEBS[PNUM].bad)} else abort } | An Axiom |
| write-data-wl | aubi_io_write_data_wl#(PNUM, N, BUF; APEBS; ERR) {if ubi-io-write-data-wl-pre(PNUM, N, BUF, APEBS) then {fail_or_success#(; ; ERR); if ERR = ESUCCESS then APEBS[PNUM] := mkpeb(APEBS[PNUM].echdr, APEBS[PNUM].vidhdr, subarray(BUF, 0, N) + mkempbuf(LEB_SIZE - N), N, APEBS[PNUM].bad) else choose BUF0 with # BUF0 ≤ N ∧ is-aligned(# BUF0, EB_PAGE_SIZE) ∧ ( datasize(BUF0, # BUF0) < datasize(BUF, N) ∨ checksum(BUF0 + mkempbuf(N - # BUF0), datasize(BUF, N)) ≠ checksum(BUF, datasize(BUF, N))) in APEBS[PNUM] := mkpeb(APEBS[PNUM].echdr, APEBS[PNUM].vidhdr, BUF0 + mkempbuf(LEB_SIZE - # BUF0), # BUF0, APEBS[PNUM].bad)} else abort } | An Axiom |
| sync-erase | aubi_io_sync_erase#(PNUM; APEBS; ERR) {if ubi-io-erase-pre(PNUM, APEBS) then {fail_or_success#(; ; ERR); if ERR = ESUCCESS then APEBS[PNUM] := mkpeb(empty, empty, mkempbuf(LEB_SIZE), 0, false) else {choose APEB with ubi-io-peb-inv(APEB) ∧ ¬ APEB.bad ∧ ¬ APEB.vidhdr.valid? in APEBS[PNUM] := APEB or skip}} else abort } | An Axiom |
| markbad | aubi_io_markbad#(PNUM; APEBS; ERR) {if ubi-io-markbad-pre(PNUM, APEBS) then {fail_or_success#(; ; ERR); if ERR = ESUCCESS then APEBS[PNUM].bad := true} else abort} | An Axiom |
| isbad | aubi_io_isbad#(PNUM, APEBS; ; ISBAD, ERR) {if ubi-io-isbad-pre(PNUM, APEBS) then {fail_or_success#(; ; ERR); if ERR = ESUCCESS then ISBAD := APEBS[PNUM].bad else ISBAD := ?} else abort} | An Axiom |
| get-blockcount | aubi_io_get_blockcount#(APEBS; ; N){N := # APEBS} | An Axiom |
| format | aubi_io_format#(; ; APEBS, ERR) {fail_or_success#(; ; ERR); if ERR = ESUCCESS then choose APEBS0 with ubi-io-initial(APEBS0) in APEBS := APEBS0 else APEBS := ?} | An Axiom |
| recovery | aubi_io_recovery#(APEBS){skip} | An Axiom |
| get-leb-size | aubi_io_get_leb_size#(APEBS; ; N){N := LEB_SIZE} | An Axiom |
| get-page-size | aubi_io_get_page_size#(APEBS; ; N){N := EB_PAGE_SIZE} | An Axiom |
| inv-format | ⊦ ⟪aubi_io_format#(; ; apebs, err)⟫ (err = ESUCCESS → ubi-io-inv(apebs)) | A Proof Obligation |
| inv-read-echdr | ubi-io-inv(apebs), ubi-io-read-echdr-pre(n, apebs) ⊦ ⟪aubi_io_read_echdr#(n, apebs; aehdr; bitflips, err)⟫ true | A Proof Obligation |
| inv-write-echdr | ubi-io-inv(apebs), ubi-io-write-echdr-pre(n, aehdr, apebs) ⊦ ⟪aubi_io_write_echdr#(n, aehdr; apebs; err)⟫ ubi-io-inv(apebs) | A Proof Obligation |
| inv-read-vidhdr | ubi-io-inv(apebs), ubi-io-read-vidhdr-pre(n, apebs) ⊦ ⟪aubi_io_read_vidhdr#(n, apebs; avhdr; bitflips, err)⟫ true | A Proof Obligation |
| inv-write-vidhdr | ubi-io-inv(apebs), ubi-io-write-vidhdr-pre(n, avhdr, apebs) ⊦ ⟪aubi_io_write_vidhdr#(n, avhdr; apebs; err)⟫ ubi-io-inv(apebs) | A Proof Obligation |
| inv-read-data | ubi-io-inv(apebs), ubi-io-read-data-pre(n, n0, n1, n2, buf, apebs) ⊦ ⟪aubi_io_read_data#(n, n0, n1, n2, apebs; buf; bitflips, err)⟫ true | A Proof Obligation |
| inv-write-data | ubi-io-inv(apebs), ubi-io-write-data-pre(n, n0, n1, n2, buf, apebs) ⊦ ⟪aubi_io_write_data#(n, n0, n1, n2, buf; apebs; err)⟫ ubi-io-inv(apebs) | A Proof Obligation |
| inv-write-data-wl | ubi-io-inv(apebs), ubi-io-write-data-wl-pre(n, n0, buf, apebs) ⊦ ⟪aubi_io_write_data_wl#(n, n0, buf; apebs; err)⟫ ubi-io-inv(apebs) | A Proof Obligation |
| inv-sync-erase | ubi-io-inv(apebs), ubi-io-erase-pre(n, apebs) ⊦ ⟪aubi_io_sync_erase#(n; apebs; err)⟫ ubi-io-inv(apebs) | A Proof Obligation |
| inv-markbad | ubi-io-inv(apebs), ubi-io-markbad-pre(n, apebs) ⊦ ⟪aubi_io_markbad#(n; apebs; err)⟫ ubi-io-inv(apebs) | A Proof Obligation |
| inv-isbad | ubi-io-inv(apebs), ubi-io-isbad-pre(n, apebs) ⊦ ⟪aubi_io_isbad#(n, apebs; ; isbad, err)⟫ true | A Proof Obligation |
| inv-get-blockcount | ubi-io-inv(apebs) ⊦ ⟪aubi_io_get_blockcount#(apebs; ; n)⟫ true | A Proof Obligation |
| crash-neutral-read-echdr | ubi-io-read-echdr-pre(n, apebs), ubi-io-inv(apebs), apebs0 = apebs ⊦ ⟨aubi_io_read_echdr#(n, apebs; aehdr; bitflips, err)⟩ (apebs0 = apebs) | A Proof Obligation |
| crash-neutral-write-echdr | ubi-io-write-echdr-pre(n, aehdr, apebs), ubi-io-inv(apebs), apebs0 = apebs ⊦ ⟨aubi_io_write_echdr#(n, aehdr; apebs; err)⟩ (apebs0 = apebs) | A Proof Obligation |
| crash-neutral-read-vidhdr | ubi-io-read-vidhdr-pre(n, apebs), ubi-io-inv(apebs), apebs0 = apebs ⊦ ⟨aubi_io_read_vidhdr#(n, apebs; avhdr; bitflips, err)⟩ (apebs0 = apebs) | A Proof Obligation |
| crash-neutral-write-vidhdr | ubi-io-write-vidhdr-pre(n, avhdr, apebs), ubi-io-inv(apebs), apebs0 = apebs ⊦ ⟨aubi_io_write_vidhdr#(n, avhdr; apebs; err)⟩ (apebs0 = apebs) | A Proof Obligation |
| crash-neutral-read-data | ubi-io-read-data-pre(n, n0, n1, n2, buf, apebs), ubi-io-inv(apebs), apebs0 = apebs ⊦ ⟨aubi_io_read_data#(n, n0, n1, n2, apebs; buf; bitflips, err)⟩ (apebs0 = apebs) | A Proof Obligation |
| crash-neutral-write-data | ubi-io-write-data-pre(n, n0, n1, n2, buf, apebs), ubi-io-inv(apebs), apebs0 = apebs ⊦ ⟨aubi_io_write_data#(n, n0, n1, n2, buf; apebs; err)⟩ (apebs0 = apebs) | A Proof Obligation |
| crash-neutral-write-data-wl | ubi-io-write-data-wl-pre(n, n0, buf, apebs), ubi-io-inv(apebs), apebs0 = apebs ⊦ ⟨aubi_io_write_data_wl#(n, n0, buf; apebs; err)⟩ (apebs0 = apebs) | A Proof Obligation |
| crash-neutral-sync-erase | ubi-io-erase-pre(n, apebs), ubi-io-inv(apebs), apebs0 = apebs ⊦ ⟨aubi_io_sync_erase#(n; apebs; err)⟩ (apebs0 = apebs) | A Proof Obligation |
| crash-neutral-markbad | ubi-io-markbad-pre(n, apebs), ubi-io-inv(apebs), apebs0 = apebs ⊦ ⟨aubi_io_markbad#(n; apebs; err)⟩ (apebs0 = apebs) | A Proof Obligation |
| crash-neutral-isbad | ubi-io-isbad-pre(n, apebs), ubi-io-inv(apebs), apebs0 = apebs ⊦ ⟨aubi_io_isbad#(n, apebs; ; isbad, err)⟩ (apebs0 = apebs) | A Proof Obligation |
| crash-neutral-get-blockcount | ubi-io-inv(apebs), apebs0 = apebs ⊦ ⟨aubi_io_get_blockcount#(apebs; ; n)⟩ (apebs0 = apebs) | A Proof Obligation |
| inv-recovery | apebs = apebs0, ubi-io-inv(apebs0) ⊦ ⟪aubi_io_recovery#(apebs)⟫ ubi-io-inv(apebs) | A Proof Obligation |
| crash-neutral-get-leb-size | ubi-io-inv(apebs), apebs0 = apebs ⊦ ⟨aubi_io_get_leb_size#(apebs; ; n)⟩ (apebs0 = apebs) | A Proof Obligation |
| crash-neutral-get-page-size | ubi-io-inv(apebs), apebs0 = apebs ⊦ ⟨aubi_io_get_page_size#(apebs; ; n)⟩ (apebs0 = apebs) | A Proof Obligation |
| inv-get-leb-size | ubi-io-inv(apebs) ⊦ ⟪aubi_io_get_leb_size#(apebs; ; n)⟫ true | A Proof Obligation |
| inv-get-page-size | ubi-io-inv(apebs) ⊦ ⟪aubi_io_get_page_size#(apebs; ; n)⟫ true | A Proof Obligation |
| crash-neutral-recovery | ubi-io-inv(apebs), apebs0 = apebs ⊦ ⟨aubi_io_recovery#(apebs)⟩ (apebs0 = apebs) | A Proof Obligation |