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: |
|---|---|---|
| io-read | ubi_io_read#(PNUM, OFFSET, N0, N, PEBS; BUF; BITFLIPS, ERR) {if PNUM < # PEBS ∧ ¬ PEBS[PNUM].bad ∧ OFFSET + N ≤ PEB_SIZE ∧ N0 + N ≤ # BUF then {ERR := EIO; BITFLIPS := false; let TRIES = 0 in while ERR ≠ ESUCCESS ∧ TRIES ≤ UBI_READ_RETRIES do {/* (inv-io-read : invariant PNUM < # PEBS ∧ ¬ PEBS[PNUM].bad ∧ OFFSET + N ≤ PEB_SIZE ∧ N0 + N ≤ # BUF ∧ TRIES ≤ UBI_READ_RETRIES + 1 ∧ # BUF = # BUF` ∧ range=(BUF, 0, BUF`, 0, N0) ∧ range=(BUF, N0 + N, BUF`, N0 + N, # BUF` - N0 + N) ∧ (ERR = ESUCCESS ∨ ⌊ERR⌋ ) ∧ (ERR = ESUCCESS → subarray(BUF, N0, N) = subarray(PEBS[PNUM].data, OFFSET, N)) wfbound UBI_READ_RETRIES + 1 - TRIES) */; mtd_asm_read#(PNUM, OFFSET, N0, N, PEBS; BUF; BITFLIPS, ERR); if ERR ≠ ESUCCESS then debug#("ubi-io: failed to read from PEB " + PNUM.toString); TRIES := TRIES +1}} else abort } | An Axiom |
| read-echdr | ubi_io_read_echdr#(PNUM, PAGESIZE, PEBS; AEHDR; BITFLIPS, ERR) {if PNUM < # PEBS ∧ ¬ PEBS[PNUM].bad then let BUF = mkbuf(PAGESIZE) in {ubi_io_read#(PNUM, 0, 0, PAGESIZE, PEBS; BUF; BITFLIPS, ERR); if ERR = ESUCCESS then if isempty(BUF) then AEHDR := empty else let EHDR = ? in {decode_echeader#(PAGESIZE, BUF; EHDR; ERR); if ERR = ESUCCESS then AEHDR := aechdr(EHDR.ec)}} else abort } | An Axiom |
| write-echdr | ubi_io_write_echdr#(PNUM, AEHDR, PAGESIZE; PEBS; ERR) {if PNUM < # PEBS ∧ AEHDR.valid? ∧ ¬ PEBS[PNUM].bad ∧ PEBS[PNUM].fill = 0 then let BUF = mkbuf(PAGESIZE), EHDR = echdr(AEHDR.ec) in {encode_echeader#(PAGESIZE, EHDR; BUF; ERR); if ERR = ESUCCESS then mtd_asm_write#(PNUM, 0, 0, PAGESIZE, BUF; PEBS; ERR)} else abort } | An Axiom |
| read-vidhdr | ubi_io_read_vidhdr#(PNUM, PAGESIZE, PEBS; AVHDR; BITFLIPS, ERR) {if PNUM < # PEBS ∧ ¬ PEBS[PNUM].bad then let BUF = mkbuf(PAGESIZE) in {ubi_io_read#(PNUM, PAGESIZE, 0, PAGESIZE, PEBS; BUF; BITFLIPS, ERR); if ERR = ESUCCESS then if isempty(BUF) then AVHDR := empty else let VHDR = ? in {decode_vidheader#(PAGESIZE, BUF; VHDR; ERR); if ERR = ESUCCESS then AVHDR := avidhdr(VHDR.vol, VHDR.leb, VHDR.sqn, VHDR.size, VHDR.checksum)}} else abort } | An Axiom |
| write-vidhdr | ubi_io_write_vidhdr#(PNUM, AVHDR, PAGESIZE; PEBS; ERR) {if PNUM < # PEBS ∧ AVHDR.valid? ∧ ¬ PEBS[PNUM].bad ∧ PEBS[PNUM].fill = EB_PAGE_SIZE then let BUF = mkbuf(PAGESIZE), VHDR = vidhdr(AVHDR.vol, AVHDR.leb, AVHDR.sqn, AVHDR.size, AVHDR.checksum) in {encode_vidheader#(PAGESIZE, VHDR; BUF; ERR); if ERR = ESUCCESS then mtd_asm_write#(PNUM, PAGESIZE, 0, PAGESIZE, BUF; PEBS; ERR)} else abort } | An Axiom |
| read-data | ubi_io_read_data#(PNUM, OFFSET, N0, N, PAGESIZE, PEBS; BUF; BITFLIPS, ERR) {if PNUM < # PEBS ∧ ¬ PEBS[PNUM].bad ∧ OFFSET + N ≤ LEB_SIZE ∧ N0 + N ≤ # BUF then ubi_io_read#(PNUM, OFFSET + 2 * PAGESIZE, N0, N, PEBS; BUF; BITFLIPS, ERR) else abort } | An Axiom |
| write-data | ubi_io_write_data#(PNUM, OFFSET, N0, N, BUF, PAGESIZE; PEBS; ERR) {if PNUM < # PEBS ∧ ¬ PEBS[PNUM].bad ∧ PEBS[PNUM].fill ≤ OFFSET + 2 * EB_PAGE_SIZE ∧ OFFSET + N ≤ LEB_SIZE ∧ N0 + N ≤ # BUF ∧ is-aligned(OFFSET, EB_PAGE_SIZE) ∧ is-aligned(N, EB_PAGE_SIZE) then mtd_asm_write#(PNUM, OFFSET + 2 * PAGESIZE, N0, N, BUF; PEBS; ERR) else abort } | An Axiom |
| write-data-wl | ubi_io_write_data_wl#(PNUM, N, BUF, PAGESIZE; PEBS; ERR) {if PNUM < # PEBS ∧ ¬ PEBS[PNUM].bad ∧ PEBS[PNUM].fill = 2 * EB_PAGE_SIZE ∧ N ≤ LEB_SIZE ∧ N ≤ # BUF ∧ is-aligned(N, EB_PAGE_SIZE) then mtd_asm_write#(PNUM, 2 * PAGESIZE, 0, N, BUF; PEBS; ERR) else abort } | An Axiom |
| sync-erase | ubi_io_sync_erase#(PNUM; PEBS; ERR){if PNUM < # PEBS ∧ ¬ PEBS[PNUM].bad then mtd_asm_erase#(PNUM; PEBS; ERR) else abort} | An Axiom |
| markbad | ubi_io_markbad#(PNUM; PEBS; ERR){if PNUM < # PEBS ∧ ¬ PEBS[PNUM].bad then mtd_asm_markbad#(PNUM; PEBS; ERR) else abort} | An Axiom |
| isbad | ubi_io_isbad#(PNUM, PEBS; ; ISBAD, ERR){if PNUM < # PEBS then mtd_asm_isbad#(PNUM, PEBS; ; ISBAD, ERR) else abort} | An Axiom |
| get-blockcount | ubi_io_get_blockcount#(PEBS; ; N){mtd_asm_get_blockcount#(PEBS; ; N)} | An Axiom |
| format | ubi_io_format#(; PAGESIZE, PEBS; ERR) {mtd_asm_init#(; ; PEBS, ERR); mtd_asm_get_page_size#(PEBS; ; PAGESIZE); if ERR = ESUCCESS then let N = ? in {mtd_asm_get_blockcount#(PEBS; ; N); let M = 0 in while M < N ∧ ERR = ESUCCESS do {/* (inv-format : invariant M ≤ N ∧ N = # PEBS ∧ mtd-cons(PEBS) ∧ (ERR = ESUCCESS → ubi-io-initial(subarray(PEBS, 0, M))) ∧ (ERR = ESUCCESS ∨ ⌊ERR⌋ ) wfbound N - M) */; let ISBAD = ? in {mtd_asm_isbad#(M, PEBS; ; ISBAD, ERR); if ERR = ESUCCESS ∧ ¬ ISBAD then let AEHDR = ?, BITFLIPS = ? in {ubi_io_read_echdr#(M, PAGESIZE, PEBS; AEHDR; BITFLIPS, ERR); let N = (ERR = ESUCCESS ∧ AEHDR.valid? ⊃ AEHDR.ec + 1;0) in {mtd_asm_erase#(M; PEBS; ERR); if ERR = ESUCCESS then ubi_io_write_echdr#(M, aechdr(N), PAGESIZE; PEBS; ERR)}}}; M := M + 1}} } | An Axiom |
| recovery | ubi_io_recovery#(PEBS; ; PAGESIZE){mtd_asm_get_page_size#(PEBS; ; PAGESIZE)} | An Axiom |
| get-leb-size | ubi_io_get_leb_size#(PAGESIZE, PEBS; ; N){mtd_asm_get_peb_size#(PEBS; ; N); N := N - 2 * PAGESIZE} | An Axiom |
| get-page-size | ubi_io_get_page_size#(PAGESIZE; ; N){N := PAGESIZE} | An Axiom |
| inv-io-read | mtd-cons(pebs), m < # pebs, ¬ pebs[m].bad, m0 + n ≤ PEB_SIZE, n0 + n ≤ # buf, buf0 = buf ⊦ ⟪ubi_io_read#(m, m0, n0, n, pebs; buf; bitflips, err)⟫ ( # buf = # buf0 ∧ range=(buf, 0, buf0, 0, n0) ∧ range=(buf, n0 + n, buf0, n0 + n, # buf0 - n0 + n) ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ (err = ESUCCESS → subarray(buf, n0, n) = subarray(pebs[m].data, m0, n))) | A Proof Obligation |
| inv-read-echdr | m = EB_PAGE_SIZE, mtd-cons(pebs), m0 < # pebs, ¬ pebs[m0].bad ⊦ ⟪ubi_io_read_echdr#(m0, m, pebs; aehdr; bitflips, err)⟫ true | A Proof Obligation |
| inv-write-echdr | m = EB_PAGE_SIZE, mtd-cons(pebs), m0 < # pebs, aehdr.valid?, ¬ pebs[m0].bad, pebs[m0].fill = 0 ⊦ ⟪ubi_io_write_echdr#(m0, aehdr, m; pebs; err)⟫ mtd-cons(pebs) | A Proof Obligation |
| inv-read-vidhdr | m = EB_PAGE_SIZE, mtd-cons(pebs), m0 < # pebs, ¬ pebs[m0].bad ⊦ ⟪ubi_io_read_vidhdr#(m0, m, pebs; avhdr; bitflips, err)⟫ true | A Proof Obligation |
| inv-write-vidhdr | m = EB_PAGE_SIZE, mtd-cons(pebs), m0 < # pebs, avhdr.valid?, ¬ pebs[m0].bad, pebs[m0].fill = EB_PAGE_SIZE ⊦ ⟪ubi_io_write_vidhdr#(m0, avhdr, m; pebs; err)⟫ mtd-cons(pebs) | A Proof Obligation |
| inv-read-data | m = EB_PAGE_SIZE, mtd-cons(pebs), m0 < # pebs, ¬ pebs[m0].bad, m1 + n ≤ LEB_SIZE, n0 + n ≤ # buf ⊦ ⟪ubi_io_read_data#(m0, m1, n0, n, m, pebs; buf; bitflips, err)⟫ true | A Proof Obligation |
| inv-write-data | m = EB_PAGE_SIZE, mtd-cons(pebs), m0 < # pebs, ¬ pebs[m0].bad, pebs[m0].fill ≤ m1 + 2 * EB_PAGE_SIZE, m1 + n ≤ LEB_SIZE, n0 + n ≤ # buf, is-aligned(m1, EB_PAGE_SIZE), is-aligned(n, EB_PAGE_SIZE) ⊦ ⟪ubi_io_write_data#(m0, m1, n0, n, buf, m; pebs; err)⟫ mtd-cons(pebs) | A Proof Obligation |
| inv-write-data-wl | m = EB_PAGE_SIZE, mtd-cons(pebs), m0 < # pebs, ¬ pebs[m0].bad, pebs[m0].fill = 2 * EB_PAGE_SIZE, n ≤ LEB_SIZE, n ≤ # buf, is-aligned(n, EB_PAGE_SIZE) ⊦ ⟪ubi_io_write_data_wl#(m0, n, buf, m; pebs; err)⟫ mtd-cons(pebs) | A Proof Obligation |
| inv-sync-erase | mtd-cons(pebs), m < # pebs, ¬ pebs[m].bad ⊦ ⟪ubi_io_sync_erase#(m; pebs; err)⟫ mtd-cons(pebs) | A Proof Obligation |
| inv-markbad | mtd-cons(pebs), m < # pebs, ¬ pebs[m].bad ⊦ ⟪ubi_io_markbad#(m; pebs; err)⟫ mtd-cons(pebs) | A Proof Obligation |
| inv-isbad | mtd-cons(pebs), m < # pebs ⊦ ⟪ubi_io_isbad#(m, pebs; ; isbad, err)⟫ true | A Proof Obligation |
| inv-get-blockcount | mtd-cons(pebs) ⊦ ⟪ubi_io_get_blockcount#(pebs; ; n)⟫ true | A Proof Obligation |
| inv-format | ⊦ ⟪ubi_io_format#(; m, pebs; err)⟫ ((err = ESUCCESS → m = EB_PAGE_SIZE ∧ mtd-cons(pebs)) ∧ (err = ESUCCESS → ubi-io-initial(pebs)) ∧ (err = ESUCCESS ∨ ⌊err⌋ )) | A Proof Obligation |
| inv-recovery | pebs = pebs0, m = EB_PAGE_SIZE, mtd-cons(pebs0) ⊦ ⟪ubi_io_recovery#(pebs; ; m0)⟫ (m0 = EB_PAGE_SIZE ∧ mtd-cons(pebs)) | A Proof Obligation |
| inv-get-leb-size | m = EB_PAGE_SIZE, mtd-cons(pebs) ⊦ ⟪ubi_io_get_leb_size#(m, pebs; ; n)⟫ true | A Proof Obligation |
| inv-get-page-size | m = EB_PAGE_SIZE ⊦ ⟪ubi_io_get_page_size#(m; ; n)⟫ true | A Proof Obligation |