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: |
|---|---|---|
| wl-worker | ubi_wear_leveling_worker#(LEBSIZE, PAGESIZE; VOLS, WLARRAY, ERASEQ, BFLIPSET, VTBLPNUM, SQNUM, APEBS; ERR) {let VALID = ?, TO = ?, FROM = ? in {ubi_get_pebs_for_wl#(WLARRAY; TO, FROM, BFLIPSET; VALID); if VALID then let AVHDR = ?, BITFLIPS = ? in {aubi_io_read_vidhdr#(FROM, APEBS; AVHDR; BITFLIPS, ERR); if ERR = ESUCCESS then let BUF = mkbuf(LEBSIZE) in {aubi_io_read_data#(FROM, 0, 0, LEBSIZE, APEBS; BUF; BITFLIPS, ERR); if ERR = ESUCCESS then ubi_atomic_leb_change# (AVHDR.vol, AVHDR.leb, TO, LEBSIZE, BUF, PAGESIZE; VOLS, WLARRAY, ERASEQ, BFLIPSET, VTBLPNUM, SQNUM, APEBS; ERR); if ERR ≠ ESUCCESS then debug#("ubi: wear-leveling of PEB " + FROM.toString + " to PEB " + TO.toString + " failed"); if ERR = ESUCCESS then {ubi_erase_worker_helper#(FROM; WLARRAY, APEBS; ERR); if ERR = ESUCCESS then ERASEQ := ERASEQ.butlast}}} else ERR := ENOSPC} } | An Axiom |
| next-sqnum | ubi_next_sqnum#(; SQNUM; N){N := SQNUM; SQNUM := SQNUM + 1} | An Axiom |
| wl-get-peb | ubi_wl_get_peb#(; PNUM, WLARRAY, ERASEQ, APEBS; ERR) {let FOUND = ?, N = ? in {ubi_wl_get_free_min#(WLARRAY; N; FOUND); if ¬ FOUND then if ERASEQ ≠ [] then {PNUM := ERASEQ.head.pnum; ubi_erase_worker_helper#(PNUM; WLARRAY, APEBS; ERR); if ERR = ESUCCESS then {ERASEQ := ERASEQ.tail; if WLARRAY[PNUM].status ≠ free then ERR := ENOSPC} else ERR := ENOSPC} else ERR := ENOSPC else {ubi_wl_find_free_max_below#(N + WL_THRESHOLD, WLARRAY; PNUM); ERR := ESUCCESS}} } | An Axiom |
| wl-put-peb | ubi_wl_put_peb#(LREF, PNUM; WLARRAY, ERASEQ){WLARRAY[PNUM].status := erasing; ERASEQ := ERASEQ + eq-entry(PNUM, LREF)} | An Axiom |
| write-once | ubi_write_once#(VOLID, LNUM, OFFSET, N0, N, BUF; VOLS, WLARRAY, ERASEQ, SQNUM, APEBS; ERR) {let PNUM = ? in {ubi_wl_get_peb#(; PNUM, WLARRAY, ERASEQ, APEBS; ERR); if ERR = ESUCCESS then let M = ? in {ubi_next_sqnum#(; SQNUM; M); aubi_io_write_vidhdr#(PNUM, avidhdr(VOLID, LNUM, M, 0, 0); APEBS; ERR); if ERR = ESUCCESS then {if N ≠ 0 then aubi_io_write_data#(PNUM, OFFSET, N0, N, BUF; APEBS; ERR); if ERR = ESUCCESS then {VOLS[VOLID][LNUM] := ⌜PNUM⌝ ; WLARRAY[PNUM].status := used} else ubi_wl_put_peb#(VOLID × LNUM, PNUM; WLARRAY, ERASEQ); skip} else ubi_wl_put_peb#(none, PNUM; WLARRAY, ERASEQ)}} } | An Axiom |
| erase-worker | ubi_erase_worker#(; WLARRAY, ERASEQ, APEBS) {if ERASEQ ≠ [] then let EQENT = ERASEQ.head, ERR = ? in {ubi_erase_worker_helper#(EQENT.pnum; WLARRAY, APEBS; ERR); if ERR = ESUCCESS then ERASEQ := ERASEQ.tail} } | An Axiom |
| erase-worker-helper | ubi_erase_worker_helper#(PNUM; WLARRAY, APEBS; ERR) {ERR := EIO; let TRIES = 0 in {while ERR ≠ ESUCCESS ∧ TRIES ≤ UBI_ERASE_RETRIES do {WLARRAY[PNUM].ec := WLARRAY[PNUM].ec + 1; aubi_io_sync_erase#(PNUM; APEBS; ERR); if ERR = ESUCCESS then aubi_io_write_echdr#(PNUM, aechdr(WLARRAY[PNUM].ec); APEBS; ERR) else debug#("ubi: erase of PEB " + PNUM.toString + " failed"); TRIES := TRIES + 1}; if ERR = ESUCCESS then WLARRAY[PNUM].status := free else {aubi_io_markbad#(PNUM; APEBS; ERR); if ERR = ESUCCESS then WLARRAY[PNUM].status := erroneous else debug#("ubi: marking PEB " + PNUM.toString + " as bad failed")}} } | An Axiom |
| atomic-leb-change | ubi_atomic_leb_change#(VOLID, LNUM, TO, N, BUF, PAGESIZE; VOLS, WLARRAY, ERASEQ, BFLIPSET, VTBLPNUM, SQNUM, APEBS; ERR) {ERR := ESUCCESS; N := datasize(BUF, N); let M = ? in {ubi_next_sqnum#(; SQNUM; M); let AVHDR = avidhdr(VOLID, LNUM, M, N, 0) in {if N ≠ 0 then AVHDR.checksum := checksum(BUF, N); aubi_io_write_vidhdr#(TO, AVHDR; APEBS; ERR); if ERR = ESUCCESS then if N > 0 then aubi_io_write_data_wl#(TO, align↑(N, PAGESIZE), BUF; APEBS; ERR); if ERR = ESUCCESS then {if VOLID = VTBL_VOLID ∧ LNUM = VTBL_LNUM then {ubi_wl_put_peb#(VTBL_VOLID × VTBL_LNUM, VTBLPNUM; WLARRAY, ERASEQ); BFLIPSET := BFLIPSET -- VTBLPNUM; VTBLPNUM := TO} else {if VOLS[VOLID][LNUM] ≠ unmapped then let PNUM = VOLS[VOLID][LNUM].pnum in {ubi_wl_put_peb#(VOLID × LNUM, PNUM; WLARRAY, ERASEQ); BFLIPSET := BFLIPSET -- PNUM}; VOLS[VOLID][LNUM] := ⌜TO⌝ }; WLARRAY[TO].status := used} else ubi_wl_put_peb#(none, TO; WLARRAY, ERASEQ)}} } | An Axiom |
| create-volume | ubi_create_volume#(VOLID, N, LEBSIZE, PAGESIZE; VOLS, WLARRAY, ERASEQ, BFLIPSET, VTBLPNUM, SQNUM, APEBS; ERR) {if VOLID ∈ VOLS ∨ VOLID = VTBL_VOLID then ERR := EINVAL else if ENCODED_NAT_SIZE + (# VOLS + 1) * (ENCODED_VOLID_SIZE + ENCODED_NAT_SIZE) > LEBSIZE then ERR := ENOSPC else let PNUM = ? in {ubi_erase_all#(VOLS, BFLIPSET, VTBLPNUM, SQNUM; WLARRAY, ERASEQ, APEBS; ERR); if ERR = ESUCCESS then {ubi_wl_get_peb#(; PNUM, WLARRAY, ERASEQ, APEBS; ERR); if ERR = ESUCCESS then let VTBL = to-vtbl(VOLS) in {VTBL[VOLID] := N; let BUF = mkbuf(LEBSIZE), VTBL = to-vtbl(VOLS) in {VTBL[VOLID] := N; encode_vtbl#(; VTBL, BUF; ERR); if ERR = ESUCCESS then {ubi_atomic_leb_change# (VTBL_VOLID, VTBL_LNUM, PNUM, LEBSIZE, BUF, PAGESIZE ; VOLS, WLARRAY, ERASEQ, BFLIPSET, VTBLPNUM, SQNUM, APEBS ; ERR); if ERR = ESUCCESS then {VOLS[VOLID] := mkebatbl(N); VOLS[VOLID] := fill(VOLS[VOLID], unmapped)}}}}}} } | An Axiom |
| write-multiple | ubi_write_multiple#(VOLID, LNUM, OFFSET, N0, N, BUF, BFLIPSET, VTBLPNUM; VOLS, WLARRAY, ERASEQ, SQNUM, APEBS; ERR) {ERR := EIO; let TRIES = 0 in while ERR ≠ ESUCCESS ∧ TRIES ≤ UBI_WRITE_RETRIES do {/* (prepost-write-multiple : invariant ubi-cons(APEBS, VOLS, WLARRAY, ERASEQ, BFLIPSET, VTBLPNUM, SQNUM) ∧ ubi-io-inv(APEBS) ∧ VOLID ∈ VOLS ∧ LNUM < # VOLS[VOLID] ∧ (VOLS`)[VOLID][LNUM] = unmapped ∧ id(APEBS, APEBS`, mapped-pebs(VOLS`)) ∧ ERASEQ.lebrefs ⊆ ERASEQ`.lebrefs ++ (VOLID × LNUM) ∧ N0 + N ≤ # BUF ∧ (N = 0 → ERASEQ.lebrefs ⊆ ERASEQ`.lebrefs) ∧ (ERR = ESUCCESS ∨ ⌊ERR⌋ ) ∧ (ERR ≠ ESUCCESS → VOLS = VOLS`) ∧ ( ERR = ESUCCESS → (∃ n. VOLS = (VOLS`)[VOLID, (VOLS`)[VOLID][LNUM, ⌜n⌝ ]] ∧ (N ≠ 0 → APEBS[n].fill = OFFSET + N) ∧ (N = 0 → APEBS[n].fill = 0) ∧ APEBS[n].data = mkempbuf(OFFSET) + subarray(BUF, N0, N) + mkempbuf(LEB_SIZE - N - OFFSET))) ∧ is-aligned(OFFSET, EB_PAGE_SIZE) ∧ is-aligned(N, EB_PAGE_SIZE) ∧ OFFSET + N ≤ LEB_SIZE wfbound UBI_WRITE_RETRIES + 1 - TRIES) */; ubi_write_once#(VOLID, LNUM, OFFSET, N0, N, BUF; VOLS, WLARRAY, ERASEQ, SQNUM, APEBS; ERR); TRIES := TRIES +1} } | An Axiom |
| get-volume-size | ubi_get_volume_size#(VOLID, VOLS; ; N){if VOLID ∈ VOLS then N := # VOLS[VOLID] else abort} | An Axiom |
| format | ubi_format#(; WLARRAY, VTBLPNUM, LEBSIZE, APEBS, VOLS, ERASEQ, BFLIPSET, SQNUM; PAGESIZE, ERR) {aubi_io_format#(; ; APEBS, ERR); aubi_io_get_leb_size#(APEBS; ; LEBSIZE); aubi_io_get_page_size#(APEBS; ; PAGESIZE); if ERR ≠ ESUCCESS then debug#("ubi: ubi-io format failed") else let N = ?, PNUM = 0 in {aubi_io_get_blockcount#(APEBS; ; N); WLARRAY := mkwlarray(N); VTBLPNUM := N; ERR := ESUCCESS; while PNUM < N ∧ ERR = ESUCCESS do {/* (inv-format : invariant PNUM ≤ # APEBS ∧ N = # APEBS ∧ # WLARRAY = # APEBS ∧ (ERR = ESUCCESS ∨ ⌊ERR⌋ ) ∧ ( ERR = ESUCCESS → ubi-io-initial(APEBS) ∧ VTBLPNUM ≤ # APEBS ∧ (∀ n3. n3 < PNUM → (APEBS[n3].bad → WLARRAY[n3] = wl-entry(0, erroneous)) ∧ ( ¬ APEBS[n3].bad → APEBS[n3].echdr.valid? ∧ WLARRAY[n3] = wl-entry(APEBS[n3].echdr.ec, free) ∧ APEBS[n3].vidhdr = empty)) ∧ (VTBLPNUM ≠ # APEBS → ¬ APEBS[VTBLPNUM].bad)) wfbound N - PNUM) */; let ISBAD = ? in {aubi_io_isbad#(PNUM, APEBS; ; ISBAD, ERR); if ERR = ESUCCESS then if ¬ ISBAD then let AEHDR = ?, BITFLIPS = ? in {aubi_io_read_echdr#(PNUM, APEBS; AEHDR; BITFLIPS, ERR); if ERR = ESUCCESS ∧ VTBLPNUM = N then VTBLPNUM := PNUM; if ERR = ESUCCESS ∧ AEHDR.valid? then WLARRAY[PNUM] := wl-entry(AEHDR.ec, free)} else WLARRAY[PNUM] := wl-entry(0, erroneous); PNUM := PNUM + 1}}; if ERR = ESUCCESS then if VTBLPNUM = N then ERR := ENOSPC else {aubi_io_write_vidhdr#(VTBLPNUM, avidhdr(VTBL_VOLID, VTBL_LNUM, 0, 0, 0); APEBS; ERR); if ERR = ESUCCESS then if ENCODED_NAT_SIZE > LEBSIZE then ERR := ENOSPC else let BUF = mkbuf(LEBSIZE), VTBL = ∅ in {encode_vtbl#(; VTBL, BUF; ERR); if ERR = ESUCCESS then aubi_io_write_data#(VTBLPNUM, 0, 0, LEBSIZE, BUF; APEBS; ERR)}; VOLS := ∅; WLARRAY[VTBLPNUM].status := used; ERASEQ := []; SQNUM := 1; BFLIPSET := ∅}} } | An Axiom |
| fix-ecs | ubi_fix_ecs#(N; INVALIDECS, WLARRAY) {while INVALIDECS ≠ [] do {/* (prepost-fix-ecs : invariant ∃ nx. INVALIDECS` = nx + INVALIDECS ∧ WLARRAY = (WLARRAY`).mapIndices(nx, λ wle. wle.ec:= N) ∧ valid-indices(WLARRAY, nx) ∧ ¬ dups(INVALIDECS`) wfbound # INVALIDECS) */; WLARRAY[INVALIDECS.head].ec := N; INVALIDECS := INVALIDECS.tail} } | An Axiom |
| scan-all | ubi_scan_all#(LEBSIZE, APEBS; RECS, WLARRAY, ERASEQ, BFLIPSET, SQNUM; VALIDCOUNT, VALIDECSUM, INVALIDECS, ERR) {RECS := ∅; BFLIPSET := ∅; VALIDCOUNT := 0; VALIDECSUM := 0; INVALIDECS := []; let N = ?, PNUM = 0 in {ERASEQ := []; SQNUM := 0; ERR := ESUCCESS; aubi_io_get_blockcount#(APEBS; ; N); WLARRAY := mkwlarray(N); WLARRAY := fill(WLARRAY, wl-entry(0, free)); while PNUM < N ∧ ERR = ESUCCESS do {/* (prepost-scan-all: invariant scan-all-inv(PNUM, APEBS, RECS, WLARRAY, ERASEQ, BFLIPSET, INVALIDECS, SQNUM, ERR) wfbound # APEBS - PNUM) */; let ISBAD = ? in {aubi_io_isbad#(PNUM, APEBS; ; ISBAD, ERR); if ERR = ESUCCESS then if ISBAD then WLARRAY[PNUM].status := erroneous else let AEHDR = ?, BITFLIPS = ? in {aubi_io_read_echdr#(PNUM, APEBS; AEHDR; BITFLIPS, ERR); if ERR = ESUCCESS then if ¬ AEHDR.valid? then {INVALIDECS := PNUM + INVALIDECS; WLARRAY[PNUM].status := erasing; ERASEQ := ERASEQ + eq-entry(PNUM, none)} else let AVHDR = ? in {VALIDCOUNT := VALIDCOUNT + 1; VALIDECSUM := VALIDECSUM + AEHDR.ec; WLARRAY[PNUM].ec := AEHDR.ec; aubi_io_read_vidhdr#(PNUM, APEBS; AVHDR; BITFLIPS, ERR); if ERR = ESUCCESS then if AVHDR = empty then if BITFLIPS then {WLARRAY[PNUM].status := erasing; ERASEQ := ERASEQ + eq-entry(PNUM, none)} else WLARRAY[PNUM].status := free else if AVHDR.valid? then let BUF = mkbuf(LEBSIZE) in {if AVHDR.size ≠ 0 then let BITFLIPS0 = ? in {aubi_io_read_data#(PNUM, 0, 0, LEBSIZE, APEBS; BUF; BITFLIPS0, ERR); BITFLIPS := BITFLIPS ∨ BITFLIPS0}; if ERR = ESUCCESS then let LADR = AVHDR.vol × AVHDR.leb, N = 0 in {if LADR ∈ RECS then N := RECS[LADR].sqn; if AVHDR.size ≠ 0 → AVHDR.size ≤ datasize(BUF) ∧ AVHDR.checksum = checksum(BUF, AVHDR.size) then {SQNUM := max(SQNUM, AVHDR.sqn + 1); if AVHDR.sqn ≥ N then {WLARRAY[PNUM].status := used; if BITFLIPS then BFLIPSET := BFLIPSET ++ PNUM; if LADR ∈ RECS then let PNUM0 = RECS[LADR].pnum in {BFLIPSET := BFLIPSET -- PNUM0; WLARRAY[PNUM0].status := erasing; ERASEQ := ERASEQ + eq-entry(PNUM0, AVHDR.vol × AVHDR.leb)}; RECS[LADR] := recovery-entry(PNUM, AVHDR.sqn)} else {WLARRAY[PNUM].status := erasing; ERASEQ := ERASEQ + eq-entry(PNUM, LADR.vol × LADR.leb)}} else {WLARRAY[PNUM].status := erasing; ERASEQ := ERASEQ + eq-entry(PNUM, none)}}} else {WLARRAY[PNUM].status := erasing; ERASEQ := ERASEQ + eq-entry(PNUM, none)}}}; PNUM := PNUM + 1}}} } | An Axiom |
| init-vols | ubi_init_vols_mappings#(VTBLPNUM, APEBS; RECS, VOLS, WLARRAY, ERASEQ, BFLIPSET) {RECS := RECS -- (VTBL_VOLID × VTBL_LNUM); while RECS ≠ ∅ do {/* (prepost-init-vols-mappings : invariant unique-sqns(APEBS) ∧ valid-vtbl(APEBS, VOLS, WLARRAY, VTBLPNUM) ∧ ¬ VTBL_VOLID ∈ VOLS ∧ ¬ VTBL_VOLID × VTBL_LNUM ∈ RECS ∧ # APEBS = # WLARRAY ∧ valid-wl(APEBS, WLARRAY) ∧ valid-eraseq(WLARRAY, ERASEQ) ∧ (∃ vtbl. is-encoded(vtbl, APEBS[VTBLPNUM].data) ∧ valid-eraseq-strong(APEBS, vtbl, ERASEQ)) ∧ bflipset-cons(BFLIPSET, WLARRAY) ∧ RECS ⊥ VOLS ∧ ERASEQ` ⊆ ERASEQ ∧ (∀ v, m, n. v × m ∈ RECS ∧ RECS[v × m].pnum = n ∨ v ∈ VOLS ∧ m < # VOLS[v] ∧ VOLS[v][m] = ⌜n⌝ ↔ WLARRAY[n].status = used ∧ n < # APEBS ∧ APEBS[n].vidhdr.valid? ∧ APEBS[n].vidhdr.vol = v ∧ APEBS[n].vidhdr.leb = m ∧ n ≠ VTBLPNUM) wfbound # RECS) */; choose LADR with LADR ∈ RECS in let N = RECS[LADR].pnum in {if LADR.vol ∈ VOLS ∧ LADR.leb < # VOLS[LADR.vol] then VOLS[LADR.vol][LADR.leb] := ⌜N⌝ else {WLARRAY[N].status := erasing; ERASEQ := ERASEQ + eq-entry(N, LADR.vol × LADR.leb); BFLIPSET := BFLIPSET -- N}; RECS := RECS -- LADR}} } | An Axiom |
| init-vols-sizes | ubi_init_vols_sizes#(RECS, WLARRAY, APEBS; VTBL, VOLS) {VOLS := ∅; while VTBL ≠ ∅ do {/* (prepost-init-vols-sizes : invariant to-vtbl(VOLS) ⊥ VTBL ∧ is-encoded(to-vtbl(VOLS) ∪ VTBL, APEBS[RECS[VTBL_VOLID × VTBL_LNUM].pnum].data) ∧ valid-vtbl-weak(APEBS, RECS[VTBL_VOLID × VTBL_LNUM].pnum) ∧ valid-recs(APEBS, WLARRAY, RECS) ∧ RECS[VTBL_VOLID × VTBL_LNUM].pnum < # APEBS ∧ VTBL_VOLID × VTBL_LNUM ∈ RECS ∧ unmapped-vols(VOLS) ∧ # APEBS = # WLARRAY wfbound # VTBL) */; choose VOLID with VOLID ∈ VTBL in {VOLS[VOLID] := mkebatbl(VTBL[VOLID]); VOLS[VOLID] := fill(VOLS[VOLID], unmapped); VTBL := VTBL -- VOLID}} } | An Axiom |
| recover | ubi_recover#(APEBS; VOLS, WLARRAY, ERASEQ, BFLIPSET, VTBLPNUM, SQNUM, LEBSIZE; PAGESIZE, ERR) {aubi_io_recovery#(APEBS); VOLS := ∅; aubi_io_get_leb_size#(APEBS; ; LEBSIZE); aubi_io_get_page_size#(APEBS; ; PAGESIZE); let RECS = ∅, INVALIDECS = [], VALIDCOUNT = 0, VALIDECSUM = 0 in {ubi_scan_all#(LEBSIZE, APEBS; RECS, WLARRAY, ERASEQ, BFLIPSET, SQNUM; VALIDCOUNT, VALIDECSUM, INVALIDECS, ERR); if ¬ VTBL_VOLID × VTBL_LNUM ∈ RECS then ERR := EINVAL; if ERR = ESUCCESS then let BUF = mkbuf(LEBSIZE), BITFLIPS = ? in {VTBLPNUM := RECS[VTBL_VOLID × VTBL_LNUM].pnum; aubi_io_read_data#(VTBLPNUM, 0, 0, LEBSIZE, APEBS; BUF; BITFLIPS, ERR); if BITFLIPS then BFLIPSET := BFLIPSET ++ VTBLPNUM; if ERR = ESUCCESS then let VTBL = ? in {decode_vtbl#(BUF; ; VTBL, ERR); if ERR = ESUCCESS then {ubi_init_vols_sizes#(RECS, WLARRAY, APEBS; VTBL, VOLS); ubi_init_vols_mappings#(VTBLPNUM, APEBS; RECS, VOLS, WLARRAY, ERASEQ, BFLIPSET); let N = (VALIDCOUNT = 0 ⊃ 0;VALIDECSUM / VALIDCOUNT) in ubi_fix_ecs#(N; INVALIDECS, WLARRAY)}}}} } | An Axiom |
| change | ubi_change#(VOLID, LNUM, N, BUF, PAGESIZE; VOLS, WLARRAY, ERASEQ, BFLIPSET, VTBLPNUM, SQNUM, APEBS; ERR) {if N ≤ LEB_SIZE ∧ N ≤ # BUF ∧ VOLID ∈ VOLS ∧ LNUM < # VOLS[VOLID] ∧ is-aligned(N, EB_PAGE_SIZE) then let TO = ? in {ubi_wl_get_peb#(; TO, WLARRAY, ERASEQ, APEBS; ERR); if ERR = ESUCCESS then ubi_atomic_leb_change#(VOLID, LNUM, TO, N, BUF, PAGESIZE; VOLS, WLARRAY, ERASEQ, BFLIPSET, VTBLPNUM, SQNUM, APEBS; ERR); if ERR ≠ ESUCCESS then debug#("ubi: change to PEB " + TO.toString + " failed")} else abort } | An Axiom |
| map | ubi_map#(VOLID, LNUM, PAGESIZE; VOLS, WLARRAY, ERASEQ, BFLIPSET, VTBLPNUM, SQNUM, APEBS; ERR) {if VOLID ∈ VOLS ∧ LNUM < # VOLS[VOLID] ∧ VOLS[VOLID][LNUM] = unmapped then let BUF = mkbuf(0) in ubi_write#(VOLID, LNUM, 0, 0, 0, BUF, PAGESIZE; VOLS, WLARRAY, ERASEQ, BFLIPSET, VTBLPNUM, SQNUM, APEBS; ERR) else abort } | An Axiom |
| erase | ubi_erase#(VOLID, LNUM, VTBLPNUM, SQNUM; VOLS, WLARRAY, ERASEQ, BFLIPSET, APEBS; ERR) {if VOLID ∈ VOLS ∧ LNUM < # VOLS[VOLID] then {ubi_unmap#(VOLID, LNUM; VOLS, WLARRAY, ERASEQ, BFLIPSET); ubi_erase_all#(VOLS, BFLIPSET, VTBLPNUM, SQNUM; WLARRAY, ERASEQ, APEBS; ERR)} else abort } | An Axiom |
| unmap | ubi_unmap#(VOLID, LNUM; VOLS, WLARRAY, ERASEQ, BFLIPSET) {if VOLID ∈ VOLS ∧ LNUM < # VOLS[VOLID] then let EBAENT = VOLS[VOLID][LNUM] in if EBAENT ≠ unmapped then let PNUM = EBAENT.pnum in {VOLS[VOLID][LNUM] := unmapped; BFLIPSET := BFLIPSET -- PNUM; ubi_wl_put_peb#(VOLID × LNUM, PNUM; WLARRAY, ERASEQ)} else abort } | An Axiom |
| write | ubi_write#(VOLID, LNUM, OFFSET, N0, N, BUF, PAGESIZE; VOLS, WLARRAY, ERASEQ, BFLIPSET, VTBLPNUM, SQNUM, APEBS; ERR) {if VOLID ∈ VOLS ∧ LNUM < # VOLS[VOLID] ∧ OFFSET + N ≤ LEB_SIZE ∧ N0 + N ≤ # BUF ∧ is-aligned(N, EB_PAGE_SIZE) ∧ is-aligned(OFFSET, EB_PAGE_SIZE) ∧ (VOLS[VOLID][LNUM] ≠ unmapped → APEBS[VOLS[VOLID][LNUM].pnum].fill ≤ OFFSET) then let EBAENT = VOLS[VOLID][LNUM] in if EBAENT = unmapped then ubi_write_multiple#(VOLID, LNUM, OFFSET, N0, N, BUF, BFLIPSET, VTBLPNUM; VOLS, WLARRAY, ERASEQ, SQNUM, APEBS; ERR) else if N ≠ 0 then {aubi_io_write_data#(EBAENT.pnum, OFFSET, N0, N, BUF; APEBS; ERR); if ERR ≠ ESUCCESS then {debug#("ubi: failed to write to PEB " + EBAENT.pnum.toString); let BUF0 = mkbuf(OFFSET + N), BITFLIPS = ? in {aubi_io_read_data#(EBAENT.pnum, 0, 0, OFFSET, APEBS; BUF0; BITFLIPS, ERR); if ERR = ESUCCESS then {BUF0 := copy(BUF, N0, BUF0, OFFSET, N); debug#("ubi: moving data from PEB " + EBAENT.pnum.toString); ubi_change# (VOLID, LNUM, OFFSET + N, BUF0, PAGESIZE; VOLS, WLARRAY, ERASEQ, BFLIPSET, VTBLPNUM, SQNUM, APEBS; ERR)} else debug#("ubi: failed to read data from PEB " + EBAENT.pnum.toString)}}} else ERR := ESUCCESS else abort } | An Axiom |
| read | ubi_read#(VOLID, LNUM, OFFSET, N0, N, VOLS, LEBSIZE, APEBS; BUF, BFLIPSET; ERR) {if VOLID ∈ VOLS ∧ LNUM < # VOLS[VOLID] ∧ OFFSET + N ≤ LEBSIZE ∧ N0 + N ≤ # BUF then let EBAENT = VOLS[VOLID][LNUM] in if EBAENT = unmapped then {BUF := fill(BUF, empty, N0, N); ERR := ESUCCESS} else let PNUM = EBAENT.pnum, BITFLIPS = ? in {aubi_io_read_data#(PNUM, OFFSET, N0, N, APEBS; BUF; BITFLIPS, ERR); if ERR = ESUCCESS ∧ BITFLIPS then BFLIPSET := BFLIPSET ++ PNUM} else abort } | An Axiom |
| get-pebs-for-wl | ubi_get_pebs_for_wl#(WLARRAY; TO, FROM, BFLIPSET; VALID) {VALID := false; let FOUND = ?, N = ? in {ubi_wl_get_free_min#(WLARRAY; N; FOUND); if FOUND then {ubi_wl_find_free_max_below#(N + 2 * WL_THRESHOLD, WLARRAY; TO); if BFLIPSET ≠ ∅ then choose N with N ∈ BFLIPSET in {FROM := N; BFLIPSET := BFLIPSET -- N; VALID := true} else {ubi_wl_get_used_min#(WLARRAY; FROM; FOUND); if FOUND ∧ WLARRAY[TO].ec ≥ WLARRAY[FROM].ec + WL_THRESHOLD then VALID := true}}} } | An Axiom |
| find-max-below | ubi_wl_find_free_max_below#(N, WLARRAY; PNUM) {let FOUND = false, M = 0 in while M < # WLARRAY do {/* (prepost-wl-free-max-below : invariant M ≤ # WLARRAY ∧ (FOUND → PNUM < # WLARRAY ∧ WLARRAY[PNUM].status = free ∧ WLARRAY[PNUM].ec = below(free-ecs(WLARRAY, M), N).max) ∧ (¬ FOUND ↔ below(free-ecs(WLARRAY, M), N) = ∅) wfbound # WLARRAY - M) */; if WLARRAY[M].status = free ∧ WLARRAY[M].ec < N ∧ (¬ FOUND ∨ WLARRAY[M].ec > WLARRAY[PNUM].ec) then {FOUND := true; PNUM := M}; M := M + 1} } | An Axiom |
| get-free-min | ubi_wl_get_free_min#(WLARRAY; N; FOUND) {FOUND := false; let M = 0 in while M < # WLARRAY do {/* (prepost-wl-get-free-min : invariant M ≤ # WLARRAY ∧ (FOUND → N = free-ecs(WLARRAY, M).min) ∧ (¬ FOUND ↔ free-ecs(WLARRAY, M) = ∅) wfbound # WLARRAY - M) */; if WLARRAY[M].status = free ∧ (¬ FOUND ∨ WLARRAY[M].ec < N) then {FOUND := true; N := WLARRAY[M].ec}; M := M + 1} } | An Axiom |
| sync-device | ubi_sync_device#(VOLS, BFLIPSET, VTBLPNUM, SQNUM; WLARRAY, ERASEQ, APEBS; ERR) {ubi_erase_all#(VOLS, BFLIPSET, VTBLPNUM, SQNUM; WLARRAY, ERASEQ, APEBS; ERR)} | An Axiom |
| get-used-min | ubi_wl_get_used_min#(WLARRAY; PNUM; FOUND) {FOUND := false; let M = 0 in while M < # WLARRAY do {/* (prepost-wl-get-used-min : invariant M ≤ # WLARRAY ∧ (FOUND → PNUM < M ∧ WLARRAY[PNUM].status = used ∧ WLARRAY[PNUM].ec = used-ecs(WLARRAY, M).min) ∧ (¬ FOUND ↔ used-ecs(WLARRAY, M) = ∅) wfbound # WLARRAY - M) */; if WLARRAY[M].status = used ∧ (¬ FOUND ∨ WLARRAY[M].ec < WLARRAY[PNUM].ec) then {FOUND := true; PNUM := M}; M := M + 1} } | An Axiom |
| get-leb-size | ubi_get_leb_size#(LEBSIZE; ; N){N := LEBSIZE} | An Axiom |
| get-page-size | ubi_get_page_size#(PAGESIZE; ; N){N := PAGESIZE} | An Axiom |
| erase-all | ubi_erase_all#(VOLS, BFLIPSET, VTBLPNUM, SQNUM; WLARRAY, ERASEQ, APEBS; ERR) {ERR := ESUCCESS; while ERR = ESUCCESS ∧ ERASEQ ≠ [] do {/* (inv-erase-all : invariant ubi-cons(APEBS, VOLS, WLARRAY, ERASEQ, BFLIPSET, VTBLPNUM, SQNUM) ∧ ubi-io-inv(APEBS) ∧ id(APEBS, APEBS`, mapped-pebs(VOLS)) ∧ ERASEQ ⊆ ERASEQ` ∧ (ERR = ESUCCESS ∨ ⌊ERR⌋ ) wfbound (ERR = ESUCCESS ⊃ # ERASEQ;0)) */; ubi_erase_worker_helper#(ERASEQ.head.pnum; WLARRAY, APEBS; ERR); if ERR = ESUCCESS then ERASEQ := ERASEQ.tail} } | An Axiom |
| inv-erase-worker | ubi-cons(apebs, vols, wlar, q, bflipset, vtblpnum, sqnum), ubi-io-inv(apebs) ⊦ ⟪ubi_erase_worker#(; wlar, q, apebs)⟫ (ubi-cons(apebs, vols, wlar, q, bflipset, vtblpnum, sqnum) ∧ ubi-io-inv(apebs)) | A Proof Obligation |
| inv-wl-worker | ubi-cons(apebs, vols, wlar, q, bflipset, vtblpnum, sqnum), vtblpnum0 = LEB_SIZE, vtblpnum1 = EB_PAGE_SIZE, ubi-io-inv(apebs), vols0 = vols, apebs0 = apebs, q0 = q ⊦ ⟪ubi_wear_leveling_worker#(vtblpnum0, vtblpnum1; vols, wlar, q, bflipset, vtblpnum, sqnum, apebs; err)⟫ ( ubi-cons(apebs, vols, wlar, q, bflipset, vtblpnum, sqnum) ∧ ubi-io-inv(apebs) ∧ ( vols0 = vols ∧ id(apebs, apebs0, mapped-pebs(vols)) ∧ q.lebrefs ⊆ q0.lebrefs ++ (VTBL_VOLID × VTBL_LNUM) ∨ (∃ v, m, n. v ∈ vols0 ∧ m < # vols0[v] ∧ vols0[v][m] ≠ unmapped ∧ vols = vols0[v, vols0[v][m, ⌜n⌝ ]] ∧ id(apebs, apebs0, mapped-pebs(vols0) -- vols0[v][m].pnum) ∧ apebs[n].data = apebs0[vols0[v][m].pnum].data ∧ apebs[n].fill ≤ apebs0[vols0[v][m].pnum].fill ∧ q.lebrefs ⊆ q0.lebrefs ++ (v × m)))) | A Proof Obligation |
| inv-create-volume | ubi-cons(apebs, vols, wlar, q, bflipset, vtblpnum, sqnum), vtblpnum0 = LEB_SIZE, vtblpnum1 = EB_PAGE_SIZE, ubi-io-inv(apebs), apebs0 = apebs, vols0 = vols, q0 = q ⊦ ⟪ubi_create_volume#(v, n, vtblpnum0, vtblpnum1; vols, wlar, q, bflipset, vtblpnum, sqnum, apebs; err)⟫ ( ubi-cons(apebs, vols, wlar, q, bflipset, vtblpnum, sqnum) ∧ ubi-io-inv(apebs) ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ id(apebs, apebs0, mapped-pebs(vols)) ∧ (err = ESUCCESS → ¬ v ∈ vols0 ∧ vols = vols0[v, fill(mkebatbl(n), unmapped)] ∧ q.lebrefs ⊆ {VTBL_VOLID × VTBL_LNUM} ) ∧ (err ≠ ESUCCESS → q.lebrefs ⊆ q0.lebrefs ∧ vols = vols0)) | A Proof Obligation |
| inv-get-volume-size | ubi-cons(apebs, vols, wlar, q, bflipset, vtblpnum, sqnum), v ∈ vols ⊦ ⟪ubi_get_volume_size#(v, vols; ; n)⟫ true | A Proof Obligation |
| inv-format | ⊦ ⟪ubi_format#(; wlar, vtblpnum, vtblpnum0, apebs, vols, q, bflipset, sqnum; vtblpnum1, err)⟫ ( ( err = ESUCCESS → ubi-cons(apebs, vols, wlar, q, bflipset, vtblpnum, sqnum) ∧ vtblpnum0 = LEB_SIZE ∧ vtblpnum1 = EB_PAGE_SIZE ∧ ubi-io-inv(apebs)) ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ (err = ESUCCESS → vols = ∅)) | A Proof Obligation |
| inv-recover | apebs = apebs0, ubi-cons(apebs0, vols, wlar, q, bflipset, vtblpnum, vtblpnum0), vtblpnum1 = LEB_SIZE, vtblpnum2 = EB_PAGE_SIZE, ubi-io-inv(apebs0) ⊦ ⟪ubi_recover#(apebs; vols0, wlar0, q0, bflipset0, vtblpnum3, sqnum, vtblpnum4; vtblpnum5, err)⟫ ( ( err = ESUCCESS → ubi-cons(apebs, vols0, wlar0, q0, bflipset0, vtblpnum3, sqnum) ∧ vtblpnum4 = LEB_SIZE ∧ vtblpnum5 = EB_PAGE_SIZE ∧ ubi-io-inv(apebs)) ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ (err = ESUCCESS → is-max(apebs, vols0, wlar0, q0, bflipset0, vtblpnum3, sqnum) ∧ q0.lebrefs ⊆ q.lebrefs ∧ vols ⊆ vols0 ∧ vols0⌈vols, q⌉)) | A Proof Obligation |
| inv-change | ubi-cons(apebs, vols, wlar, q, bflipset, vtblpnum, sqnum), vtblpnum0 = EB_PAGE_SIZE, ubi-io-inv(apebs), n0 ≤ LEB_SIZE, n0 ≤ # buf, v ∈ vols, vtblpnum1 < # vols[v], is-aligned(n0, EB_PAGE_SIZE), vols0 = vols, apebs0 = apebs, q0 = q ⊦ ⟪ubi_change#(v, vtblpnum1, n0, buf, vtblpnum0; vols, wlar, q, bflipset, vtblpnum, sqnum, apebs; err)⟫ ( ubi-cons(apebs, vols, wlar, q, bflipset, vtblpnum, sqnum) ∧ ubi-io-inv(apebs) ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ (err ≠ ESUCCESS → vols = vols0 ∧ id(apebs, apebs0, mapped-pebs(vols)) ∧ q.lebrefs ⊆ q0.lebrefs) ∧ ( err = ESUCCESS → v ∈ vols0 ∧ vtblpnum1 < # vols0[v] ∧ q.lebrefs ⊆ q0.lebrefs ++ (v × vtblpnum1) ∧ (vols0[v][vtblpnum1] ≠ unmapped → id(apebs, apebs0, mapped-pebs(vols0) -- vols0[v][vtblpnum1].pnum)) ∧ (vols0[v][vtblpnum1] = unmapped → id(apebs, apebs0, mapped-pebs(vols0))) ∧ (∃ n. vols = vols0[v, vols0[v][vtblpnum1, ⌜n⌝ ]] ∧ apebs[n].data = subarray(buf, 0, n0) + mkempbuf(LEB_SIZE - n0) ∧ apebs[n].fill = align↑(datasize(buf, n0), EB_PAGE_SIZE)))) | A Proof Obligation |
| inv-map | ubi-cons(apebs, vols, wlar, q, bflipset, vtblpnum, sqnum), vtblpnum0 = EB_PAGE_SIZE, ubi-io-inv(apebs), v ∈ vols, vtblpnum1 < # vols[v], vols[v][vtblpnum1] = unmapped ⊦ ⟪ubi_map#(v, vtblpnum1, vtblpnum0; vols, wlar, q, bflipset, vtblpnum, sqnum, apebs; err)⟫ (ubi-cons(apebs, vols, wlar, q, bflipset, vtblpnum, sqnum) ∧ ubi-io-inv(apebs)) | A Proof Obligation |
| inv-erase | ubi-cons(apebs, vols, wlar, q, bflipset, vtblpnum, sqnum), ubi-io-inv(apebs), v ∈ vols, vtblpnum0 < # vols[v] ⊦ ⟪ubi_erase#(v, vtblpnum0, vtblpnum, sqnum; vols, wlar, q, bflipset, apebs; err)⟫ (ubi-cons(apebs, vols, wlar, q, bflipset, vtblpnum, sqnum) ∧ ubi-io-inv(apebs)) | A Proof Obligation |
| inv-unmap | ubi-cons(apebs, vols, wlar, q, bflipset, vtblpnum, sqnum), v ∈ vols, vtblpnum0 < # vols[v] ⊦ ⟪ubi_unmap#(v, vtblpnum0; vols, wlar, q, bflipset)⟫ ubi-cons(apebs, vols, wlar, q, bflipset, vtblpnum, sqnum) | A Proof Obligation |
| inv-write | ubi-cons(apebs, vols, wlar, q, bflipset, vtblpnum, sqnum), vtblpnum0 = EB_PAGE_SIZE, ubi-io-inv(apebs), v ∈ vols, vtblpnum1 < # vols[v], vtblpnum2 + n ≤ LEB_SIZE, n0 + n ≤ # buf, is-aligned(n, EB_PAGE_SIZE), is-aligned(vtblpnum2, EB_PAGE_SIZE), vols[v][vtblpnum1] ≠ unmapped → apebs[vols[v][vtblpnum1].pnum].fill ≤ vtblpnum2 ⊦ ⟪ubi_write#(v, vtblpnum1, vtblpnum2, n0, n, buf, vtblpnum0; vols, wlar, q, bflipset, vtblpnum, sqnum, apebs; err)⟫ (ubi-cons(apebs, vols, wlar, q, bflipset, vtblpnum, sqnum) ∧ ubi-io-inv(apebs)) | A Proof Obligation |
| inv-read | ubi-cons(apebs, vols, wlar, q, bflipset, vtblpnum, sqnum), vtblpnum0 = LEB_SIZE, ubi-io-inv(apebs), v ∈ vols, vtblpnum1 < # vols[v], vtblpnum2 + n ≤ vtblpnum0, n0 + n ≤ # buf ⊦ ⟪ubi_read#(v, vtblpnum1, vtblpnum2, n0, n, vols, vtblpnum0, apebs; buf, bflipset; err)⟫ ubi-cons(apebs, vols, wlar, q, bflipset, vtblpnum, sqnum) | A Proof Obligation |
| inv-sync-device | ubi-cons(apebs, vols, wlar, q, bflipset, vtblpnum, sqnum), ubi-io-inv(apebs), apebs0 = apebs, q0 = q ⊦ ⟪ubi_sync_device#(vols, bflipset, vtblpnum, sqnum; wlar, q, apebs; err)⟫ ( ubi-cons(apebs, vols, wlar, q, bflipset, vtblpnum, sqnum) ∧ ubi-io-inv(apebs) ∧ id(apebs, apebs0, mapped-pebs(vols)) ∧ q ⊆ q0 ∧ (err = ESUCCESS ∨ ⌊err⌋ )) | A Proof Obligation |
| inv-get-leb-size | vtblpnum = LEB_SIZE ⊦ ⟪ubi_get_leb_size#(vtblpnum; ; n)⟫ true | A Proof Obligation |
| inv-get-page-size | vtblpnum = EB_PAGE_SIZE ⊦ ⟪ubi_get_page_size#(vtblpnum; ; n)⟫ true | A Proof Obligation |
| inv-erase-all | ubi-cons(apebs, vols, wlar, q, bflipset, vtblpnum, sqnum), ubi-io-inv(apebs), apebs0 = apebs, q0 = q ⊦ ⟪ubi_erase_all#(vols, bflipset, vtblpnum, sqnum; wlar, q, apebs; err)⟫ ( ubi-cons(apebs, vols, wlar, q, bflipset, vtblpnum, sqnum) ∧ ubi-io-inv(apebs) ∧ id(apebs, apebs0, mapped-pebs(vols)) ∧ q ⊆ q0 ∧ (err = ESUCCESS → q = []) ∧ (err = ESUCCESS ∨ ⌊err⌋ )) | A Proof Obligation |
| lf-cmp-peb | n ≤ n0, n0 < n + m ⊦ apebs[n0] = apeb0 ∧ cmp(apebs, apeb, n, m) → apeb0 = apeb | A User Theorem |
| lf-mapped-info | ⊦ v ∈ vols ∧ m < # vols[v] ∧ vols[v][m] = ⌜n⌝ ∧ valid-ebatbl(apebs, wlar, vols, n0) → wlar[n].status = used ∧ n ≠ n0 ∧ n < # wlar | A User Theorem |
| lf-mapped-valid-peb | ⊦ v ∈ vols ∧ m < # vols[v] ∧ vols[v][m] = ⌜n⌝ ∧ valid-ebatbl(apebs, wlar, vols, n0) ∧ valid-wl(apebs, wlar) → valid-peb(v, m, apebs[n]) | A User Theorem |
| lf-used-info | ⊦ n < # wlar ∧ wlar[n] = wl-entry(m, used) ∧ valid-eraseq(wlar, q) → ¬ n ∈ q | A User Theorem |
| lf-used-valid-peb | ⊦ n < # wlar ∧ wlar[n] = wl-entry(m, used) ∧ apebs[n] = apeb ∧ valid-wl(apebs, wlar) → valid-peb(apeb) | A User Theorem |
| lf-valid-eraseq-middle-wlar | ⊦ valid-eraseq(wlar, q0 + eq-entry(m, lref) ' + q1) → m < # wlar | A User Theorem |
| lf-valid-eraseq-stronger-notin-recs | # apebs = # wlar ⊦ valid-eraseq-stronger(apebs, q) ∧ valid-eraseq(wlar, q) ∧ valid-recs(apebs, wlar, recs) ∧ valid-wl(apebs, wlar) ∧ ¬ v × m ∈ recs → valid-sqns(v, m, apebs) = ∅ | A User Theorem |
| lf-valid-recs-in-apebs | m0 ≤ # apebs ⊦ v × m ∈ recs ∧ recs[v × m] = recovery-entry(n0, n1) ∧ valid-recs(subarray(apebs, 0, m0), subarray(wlar, 0, m0), recs) → n0 < m0 | A User Theorem |
| lf-valid-recs-max | m ≤ # apebs, # apebs = # wlar ⊦ valid-recs(subarray(apebs, 0, m), subarray(wlar, 0, m), recs) ∧ valid-recs-sqns(apebs, recs) ∧ valid-wl(subarray(apebs, 0, m), subarray(wlar, 0, m)) ∧ v × n ∈ recs ∧ recs[v × n] = recovery-entry(m0, m1) → m1 = valid-sqns(v, n, apebs, m).max | A User Theorem |
| lf-valid-recs-notin-eraseq | ⊦ v × m ∈ recs ∧ recs[v × m] = recovery-entry(n0, n1) ∧ valid-recs(apebs, wlar, recs) ∧ valid-eraseq(wlar, q) → ¬ n0 ∈ q | A User Theorem |
| lf-valid-recs-sqns-vidhdr | ⊦ v × m ∈ recs ∧ recs[v × m] = recovery-entry(n0, n1) ∧ valid-recs-sqns(apebs, recs) → apebs[n0].vidhdr.sqn = n1 | A User Theorem |
| lf-valid-recs-valid-peb | m0 ≤ # apebs, # apebs = # wlar ⊦ v × m ∈ recs ∧ recs[v × m] = recovery-entry(n0, n1) ∧ valid-recs(subarray(apebs, 0, m0), subarray(wlar, 0, m0), recs) ∧ valid-wl(subarray(apebs, 0, m0), subarray(wlar, 0, m0)) → valid-peb(v, m, apebs[n0]) | A User Theorem |
| lf-valid-vtbl-neq-erasing | ⊦ wlar[m] = wl-entry(m0, erasing) ∧ valid-vtbl(apebs, vols, wlar, n) → n ≠ m | A User Theorem |
| lf-valid-vtbl-neq-free | ⊦ wlar[m] = wl-entry(m0, free) ∧ valid-vtbl(apebs, vols, wlar, n) → n ≠ m | A User Theorem |
| lf-valid-wl-bad | n < # wlar ⊦ apebs[n] = mkpeb(aehdr, avhdr, buf, m, true) ∧ valid-wl(apebs, wlar) → wlar[n].status = erroneous | A User Theorem |
| lf-valid-wl-free-emptyvidhdr | n < # wlar, n < # apebs ⊦ wlar[n] = wl-entry(m, free) ∧ valid-wl(apebs, wlar) ∧ ubi-io-inv(apebs) → apebs[n].vidhdr = empty ∧ apebs[n].echdr.valid? ∧ apebs[n].fill = 0 | A User Theorem |
| lf-valid-wl-not-erroneous | n < # wlar, stat ≠ erroneous ⊦ apebs[n] = mkpeb(aehdr, avhdr, buf, m, boolvar) ∧ wlar[n] = wl-entry(m0, stat) ∧ valid-wl(apebs, wlar) → ¬ boolvar | A User Theorem |
| lf-vtbl-info | ⊦ valid-vtbl(apebs, vols, wlar, n) ∧ valid-eraseq(wlar, q) → ¬ n ∈ q | A User Theorem |
| ls-add2-add2-samelimit | ⊦ n = n0 + n1 ∧ m1 = m2 + n1 ∧ n = m0 + m1 → m0 + m2 = n0 | A User Theorem |
| ls-array-append-length0 | # buf0 = 0 ⊦ buf + buf0 = buf | A User Theorem |
| ls-datasize-empbuf-append-lower | ⊦ datasize(mkempbuf(n) + buf, n) = 0 | A User Theorem |
| ls-datasize-wear-level | ⊦ ubi-io-peb-inv(mkpeb(aehdr, avhdr, buf, m, false)) → ¬ m < align↑(datasize(buf, LEB_SIZE), EB_PAGE_SIZE) | A User Theorem |
| ls-datasize-zero | n ≤ # buf ⊦ datasize(buf, n) = 0 ↔ (∃ buf0. buf = mkempbuf(n) + buf0) | A User Theorem |
| ls-max | ⊦ (bag ++ n).max = (bag = ∅ ⊃ n;(bag.max > n ⊃ bag.max;n)) | A User Theorem |
| ls-subarray-datasize | n ≤ # buf ⊦ LEB_SIZE = align↑(datasize(buf, n), EB_PAGE_SIZE) + n0 ∧ LEB_SIZE = n + n1 ∧ is-aligned(n, EB_PAGE_SIZE) → subarray(buf, 0, align↑(datasize(buf, n), EB_PAGE_SIZE)) + mkempbuf(n0) = subarray(buf, 0, n) + mkempbuf(n1) | A User Theorem |
| ls-valid-global-sqn-vtbl | ⊦ valid-global-sqn(apebs, sqnum) ∧ valid-vtbl(apebs, vols, wlar, vtblpnum) ∧ valid-wl(apebs, wlar) → ¬ sqnum ≤ valid-sqns(VTBL_VOLID, VTBL_LNUM, apebs).max | A User Theorem |
| nat-sum-leq | ⊦ m = n0 + n1 → (m ≤ n1 ↔ n0 = 0) | A User Theorem |
| prepost-atomic-leb-change | ubi-cons(apebs, vols, wlar, q, bflipset, vtblpnum, sqnum), ubi-io-inv(apebs), n0 ≤ # buf, n < # wlar, n0 ≤ LEB_SIZE, wlar[n].status = free, apebs0 = apebs, is-aligned(n0, EB_PAGE_SIZE), v ∈ vols ∧ m < # vols[v] ∨ v = VTBL_VOLID ∧ m = VTBL_LNUM, vols0 = vols, q0 = q, vtblpnum0 = vtblpnum ⊦ ⟪ubi_atomic_leb_change#(v, m, n, n0, buf, EB_PAGE_SIZE; vols, wlar, q, bflipset, vtblpnum, sqnum, apebs; err)⟫ ( (err = ESUCCESS ∨ ⌊err⌋ ) ∧ id○(apebs, apebs0, n) ∧ ubi-io-inv(apebs) ∧ # apebs = # wlar ∧ unique-sqns(apebs) ∧ valid-global-sqn(apebs, sqnum) ∧ valid-wl(apebs, wlar) ∧ valid-eraseq(q) ∧ valid-eraseq(wlar, q) ∧ valid-eraseq(apebs, q) ∧ ¬ VTBL_VOLID ∈ vols ∧ bflipset-cons(bflipset, wlar) ∧ ( v ∈ vols0 ∨ is-encoded(to-vtbl(vols0), subarray(buf, 0, n0)) ∧ n0 = LEB_SIZE ∨ err ≠ ESUCCESS → valid-ebatbl(apebs, wlar, vols, vtblpnum) ∧ valid-vtbl(apebs, vols, wlar, vtblpnum)) ∧ ( err = ESUCCESS ∧ v = VTBL_VOLID ∧ m = VTBL_LNUM → (∀ v0, m0. ¬ v0 ∈ vols0 ∧ is-encoded(to-vtbl(vols0)[v0, m0], subarray(buf, 0, n0)) ∧ n0 = LEB_SIZE → valid-ebatbl(apebs, wlar, vols[v0, fill(mkebatbl(m0), unmapped)], vtblpnum) ∧ valid-vtbl(apebs, vols[v0, fill(mkebatbl(m0), unmapped)], wlar, vtblpnum))) ∧ (err = ESUCCESS ∧ v ∈ vols0 ∧ vols0[v][m] ≠ unmapped → q = q0 + eq-entry(vols0[v][m].pnum, v × m)) ∧ (err = ESUCCESS ∧ v = VTBL_VOLID ∧ m = VTBL_LNUM → q = q0 + eq-entry(vtblpnum0, v × m)) ∧ id(apebs, apebs0, mapped-pebs(vols0)) ∧ (v = VTBL_VOLID ∧ m = VTBL_LNUM ∨ err ≠ ESUCCESS → vols = vols0) ∧ (v ∈ vols0 ∧ err = ESUCCESS → vols = vols0[v, vols0[v][m, ⌜n⌝ ]]) ∧ ( err = ESUCCESS → apebs[n].fill = align↑(datasize(buf, n0), EB_PAGE_SIZE) ∧ apebs[n].data = subarray(buf, 0, n0) + mkempbuf(LEB_SIZE - n0) ∧ q.lebrefs ⊆ q0.lebrefs ++ (v × m)) ∧ (err ≠ ESUCCESS → q.lebrefs = q0.lebrefs)) | A User Theorem |
| prepost-erase-worker-helper | ubi-cons(apebs, vols, wlar, q0 + eq-entry(m, lref) ' + q1, bflipset, vtblpnum, sqnum), m < # wlar, ubi-io-inv(apebs), wlar = wlar0, apebs = apebs0 ⊦ ⟪ubi_erase_worker_helper#(m; wlar, apebs; err)⟫ ( (err = ESUCCESS → ubi-cons(apebs, vols, wlar, q0 + q1, bflipset, vtblpnum, sqnum)) ∧ (err ≠ ESUCCESS → ubi-cons(apebs, vols, wlar, q0 + eq-entry(m, lref) ' + q1, bflipset, vtblpnum, sqnum)) ∧ ubi-io-inv(apebs) ∧ wlar[m].status ≠ used ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ id○(wlar, wlar0, m) ∧ id○(apebs, apebs0, m) ∧ id(apebs, apebs0, mapped-pebs(vols))) | A User Theorem |
| prepost-fix-ecs | valid-indices(wlar, nx), wlar0 = wlar, nx0 = nx, ¬ dups(nx) ⊦ ⟪ubi_fix_ecs#(n; nx, wlar)⟫ (wlar = wlar0.mapIndices(nx0, λ wle. wle.ec:= n)) | A User Theorem |
| prepost-get-peb | ubi-cons(apebs, vols, wlar, q, bflipset, vtblpnum, sqnum), ubi-io-inv(apebs), wlar0 = wlar, q0 = q, apebs0 = apebs ⊦ ⟪ubi_wl_get_peb#(; n, wlar, q, apebs; err)⟫ ( (err = ESUCCESS ∨ ⌊err⌋ ) ∧ (err ≠ ESUCCESS → ubi-cons(apebs, vols, wlar, q, bflipset, vtblpnum, sqnum)) ∧ ubi-io-inv(apebs) ∧ q.lebrefs ⊆ q0.lebrefs ∧ id(apebs, apebs0, mapped-pebs(vols)) ∧ ( err = ESUCCESS → n < # apebs ∧ wlar[n].status = free ∧ (apebs0 = apebs ∧ wlar0 = wlar ∧ q0 = q ∨ id○(apebs0, apebs, n) ∧ id○(wlar0, wlar, n) ∧ q0 ≠ [] ∧ q0 = eq-entry(n, q0.head.lebref) + q) ∧ ubi-cons(apebs, vols, wlar, q, bflipset, vtblpnum, sqnum))) | A User Theorem |
| prepost-get-pebs-for-wl | ubi-cons(apebs, vols, wlar, q, bflipset, vtblpnum, sqnum), bflipset0 = bflipset ⊦ ⟪ubi_get_pebs_for_wl#(wlar; n, m, bflipset; boolvar)⟫ ( ubi-cons(apebs, vols, wlar, q, bflipset, vtblpnum, sqnum) ∧ ( boolvar → n < # wlar ∧ wlar[n].status = free ∧ m < # wlar ∧ wlar[m].status = used ∧ (bflipset0 = ∅ → wlar[n].ec ≥ wlar[m].ec + WL_THRESHOLD))) | A User Theorem |
| prepost-init-vols-mappings | valid-vtbl(apebs, vols, wlar, n), valid-recs(apebs, wlar, recs), unmapped-vols(vols), ¬ VTBL_VOLID ∈ vols, # wlar = # apebs, valid-eraseq-stronger(apebs, q), valid-wl(apebs, wlar), valid-eraseq(wlar, q), unique-sqns(apebs), bflipset-cons(bflipset, wlar), q0 = q ⊦ ⟪ubi_init_vols_mappings#(n, apebs; recs, vols, wlar, q, bflipset)⟫ ( valid-ebatbl(apebs, wlar, vols, n) ∧ valid-vtbl(apebs, vols, wlar, n) ∧ ¬ VTBL_VOLID ∈ vols ∧ # apebs = # wlar ∧ bflipset-cons(bflipset, wlar) ∧ valid-wl(apebs, wlar) ∧ valid-eraseq(wlar, q) ∧ q0 ⊆ q ∧ (∃ vtbl. is-encoded(vtbl, apebs[n].data) ∧ valid-eraseq-strong(apebs, vtbl, q))) | A User Theorem |
| prepost-init-vols-sizes | n < # apebs, valid-recs(apebs, wlar, recs), valid-vtbl-weak(apebs, n), is-encoded(vtbl, apebs[n].data), VTBL_VOLID × VTBL_LNUM ∈ recs, recs[VTBL_VOLID × VTBL_LNUM].pnum = n, # apebs = # wlar ⊦ ⟪ubi_init_vols_sizes#(recs, wlar, apebs; vtbl, vols)⟫ (valid-vtbl(apebs, vols, wlar, n) ∧ unmapped-vols(vols) ∧ ¬ VTBL_VOLID ∈ vols) | A User Theorem |
| prepost-io-write-data | ubi-cons(apebs, vols, wlar, q, bflipset, n0, n1), ubi-io-inv(apebs), n < # apebs, is-aligned(m0, EB_PAGE_SIZE), is-aligned(m2, EB_PAGE_SIZE), apebs[n].fill ≤ m0, m0 + m2 ≤ LEB_SIZE, m1 + m2 ≤ # buf, wlar[n].status = used, n0 ≠ n ⊦ ⟪aubi_io_write_data#(n, m0, m1, m2, buf; apebs; err)⟫ (ubi-cons(apebs, vols, wlar, q, bflipset, n0, n1) ∧ ubi-io-inv(apebs)) | A User Theorem |
| prepost-scan-all | ubi-io-inv(apebs), unique-sqns(apebs) ⊦ ⟪ubi_scan_all#(LEB_SIZE, apebs; recs, wlar, q, bflipset, n1; n2, n3, nx, err)⟫ scan-all-inv(# apebs, apebs, recs, wlar, q, bflipset, nx, n1, err) | A User Theorem |
| prepost-wl-free-max-below | ∃ m. m < # wlar ∧ wlar[m].ec < n ∧ wlar[m].status = free ⊦ ⟪ubi_wl_find_free_max_below#(n, wlar; m)⟫ (m < # wlar ∧ wlar[m].status = free ∧ wlar[m].ec = below(free-ecs(wlar), n).max) | A User Theorem |
| prepost-wl-get-free-min | ⊦ ⟪ubi_wl_get_free_min#(wlar; n; boolvar)⟫ ((boolvar → n = free-ecs(wlar).min) ∧ (¬ boolvar ↔ free-ecs(wlar) = ∅)) | A User Theorem |
| prepost-wl-get-used-min | ⊦ ⟪ubi_wl_get_used_min#(wlar; n; boolvar)⟫ ((boolvar → n < # wlar ∧ wlar[n].status = used ∧ wlar[n].ec = used-ecs(wlar).min) ∧ (¬ boolvar ↔ used-ecs(wlar) = ∅)) | A User Theorem |
| prepost-write-multiple | ubi-cons(apebs, vols, wlar, q, bflipset, vtblpnum, sqnum), ubi-io-inv(apebs), v ∈ vols, m < # vols[v], vols[v][m] = unmapped, m1 + m2 ≤ # buf, m0 + m1 ≤ LEB_SIZE, is-aligned(m0, EB_PAGE_SIZE), is-aligned(m1, EB_PAGE_SIZE), vols = vols0, apebs = apebs0, q = q0 ⊦ ⟪ubi_write_multiple#(v, m, m0, m2, m1, buf, bflipset, vtblpnum; vols, wlar, q, sqnum, apebs; err)⟫ ( ubi-cons(apebs, vols, wlar, q, bflipset, vtblpnum, sqnum) ∧ ubi-io-inv(apebs) ∧ id(apebs, apebs0, mapped-pebs(vols0)) ∧ q.lebrefs ⊆ q0.lebrefs ++ (v × m) ∧ (m1 = 0 → q.lebrefs ⊆ q0.lebrefs) ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ (err ≠ ESUCCESS → vols = vols0) ∧ ( err = ESUCCESS → (∃ n. vols = vols0[v, vols0[v][m, ⌜n⌝ ]] ∧ (m1 ≠ 0 → apebs[n].fill = m0 + m1) ∧ (m1 = 0 → apebs[n].fill = 0) ∧ apebs[n].data = mkempbuf(m0) + subarray(buf, m2, m1) + mkempbuf(LEB_SIZE - m1 - m0)))) | A User Theorem |
| prepost-write-once | ubi-cons(apebs, vols, wlar, q, bflipset, vtblpnum, sqnum), ubi-io-inv(apebs), v ∈ vols, m < # vols[v], vols[v][m] = unmapped, m1 + m2 ≤ # buf, m0 + m1 ≤ LEB_SIZE, is-aligned(m0, EB_PAGE_SIZE), is-aligned(m1, EB_PAGE_SIZE), vols = vols0, apebs = apebs0, q = q0 ⊦ ⟪ubi_write_once#(v, m, m0, m2, m1, buf; vols, wlar, q, sqnum, apebs; err)⟫ ( ubi-cons(apebs, vols, wlar, q, bflipset, vtblpnum, sqnum) ∧ ubi-io-inv(apebs) ∧ id(apebs, apebs0, mapped-pebs(vols0)) ∧ q.lebrefs ⊆ q0.lebrefs ++ (v × m) ∧ (m1 = 0 → q.lebrefs ⊆ q0.lebrefs) ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ (err ≠ ESUCCESS → vols = vols0) ∧ ( err = ESUCCESS → (∃ n. vols = vols0[v, vols0[v][m, ⌜n⌝ ]] ∧ (m1 ≠ 0 → apebs[n].fill = m0 + m1) ∧ (m1 = 0 → apebs[n].fill = 0) ∧ apebs[n].data = mkempbuf(m0) + subarray(buf, m2, m1) + mkempbuf(LEB_SIZE - m1 - m0)))) | A User Theorem |
| subbarray-alignup-datasize-empty | ⊦ n0 ≤ # buf ∧ n0 = n1 + align↑(datasize(buf, n0), EB_PAGE_SIZE) → subarray(buf, align↑(datasize(buf, n0), EB_PAGE_SIZE), n1) = mkempbuf(n1) | A User Theorem |
| ubi-io-inv-fillcount0 | n < # apebs ⊦ apebs[n] = mkpeb(aehdr, avhdr, buf, 0, false) ∧ ubi-io-inv(apebs) → (buf = mkempbuf(LEB_SIZE) ↔ true) | A User Theorem |
| ubi-io-inv-fwd | n < # apebs ⊦ apebs[n] = apeb ∧ ubi-io-inv(apebs) → ubi-io-peb-inv(apeb) | A User Theorem |
| ubi-is-max-unique | ⊦ is-max(apebs, vols0, wlar0, q0, bflipset0, n0, n1) ∧ is-max(apebs, vols1, wlar1, q1, bflipset1, m0, m1) → vols0 = vols1 | A User Theorem |
| valid-peb-write-valid-peb | n < # apebs ⊦ valid-peb(apebs[n]) ∧ m0 ≥ apebs[n].fill ∧ m0 ≤ LEB_SIZE ∧ ubi-io-inv(apebs) → valid-peb(mkpeb(apebs[n].echdr, apebs[n].vidhdr, subarray(apebs[n].data, 0, m0) + buf1, m1, false)) | A User Theorem |