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: |
|---|---|---|
| initialization | ⊦ ⟪ubi_format#(; wlar, vtblpnum, vtblpnum0, apebs, vols, q, bflipset, sqnum; vtblpnum1, err)⟫ ( (err = ESUCCESS → ⟨ebm_format#(; ; avols0, err0)⟩ (abs(avols0, apebs, vols, q) ∧ err = err0)) ∧ (err ≠ ESUCCESS → (∀ avols. ⟨ebm_format#(; ; avols0, err0)⟩ (avols = avols0 ∧ err = err0)))) | A Proof Obligation |
| refine-change | v ∈ avols, vtblpnum < # avols[v], n ≤ LEB_SIZE, n ≤ # buf, is-aligned(n, EB_PAGE_SIZE), abs(avols, apebs, vols, q), ebm-cons(avols), ubi-cons(apebs, vols, wlar, q, bflipset, vtblpnum0, sqnum), vtblpnum1 = LEB_SIZE, vtblpnum2 = EB_PAGE_SIZE, ubi-io-inv(apebs) ⊦ ⟪ubi_change#(v, vtblpnum, n, buf, vtblpnum2; vols, wlar, q, bflipset, vtblpnum0, sqnum, apebs; err)⟫ ⟨ebm_change#(v, vtblpnum, n, buf; avols; err0)⟩ (abs(avols, apebs, vols, q) ∧ err = err0) | A Proof Obligation |
| refine-map | v ∈ avols, vtblpnum < # avols[v], ¬ avols[v][vtblpnum].mapped?, abs(avols, apebs, vols, q), ebm-cons(avols), ubi-cons(apebs, vols, wlar, q, bflipset, vtblpnum0, sqnum), vtblpnum1 = LEB_SIZE, vtblpnum2 = EB_PAGE_SIZE, ubi-io-inv(apebs) ⊦ ⟪ubi_map#(v, vtblpnum, vtblpnum2; vols, wlar, q, bflipset, vtblpnum0, sqnum, apebs; err)⟫ ⟨ebm_map#(v, vtblpnum; avols; err0)⟩ (abs(avols, apebs, vols, q) ∧ err = err0) | A Proof Obligation |
| refine-unmap | v ∈ avols, vtblpnum < # avols[v], abs(avols, apebs, vols, q), ebm-cons(avols), ubi-cons(apebs, vols, wlar, q, bflipset, vtblpnum0, sqnum), vtblpnum1 = LEB_SIZE, vtblpnum2 = EB_PAGE_SIZE, ubi-io-inv(apebs) ⊦ ⟪ubi_unmap#(v, vtblpnum; vols, wlar, q, bflipset)⟫ ⟨ebm_unmap#(v, vtblpnum; avols)⟩ abs(avols, apebs, vols, q) | A Proof Obligation |
| refine-create-volume | ¬ v ∈ avols, abs(avols, apebs, vols, q), ebm-cons(avols), ubi-cons(apebs, vols, wlar, q, bflipset, vtblpnum, sqnum), vtblpnum0 = LEB_SIZE, vtblpnum1 = EB_PAGE_SIZE, ubi-io-inv(apebs) ⊦ ⟪ubi_create_volume#(v, n, vtblpnum0, vtblpnum1; vols, wlar, q, bflipset, vtblpnum, sqnum, apebs; err)⟫ ⟨ebm_create_volume#(v, n; avols; err0)⟩ (abs(avols, apebs, vols, q) ∧ err = err0) | A Proof Obligation |
| refine-erase | v ∈ avols, vtblpnum < # avols[v], abs(avols, apebs, vols, q), ebm-cons(avols), ubi-cons(apebs, vols, wlar, q, bflipset, vtblpnum0, sqnum), vtblpnum1 = LEB_SIZE, vtblpnum2 = EB_PAGE_SIZE, ubi-io-inv(apebs) ⊦ ⟪ubi_erase#(v, vtblpnum, vtblpnum0, sqnum; vols, wlar, q, bflipset, apebs; err)⟫ ⟨ebm_erase#(v, vtblpnum; avols; err0)⟩ (abs(avols, apebs, vols, q) ∧ err = err0) | A Proof Obligation |
| refine-get-volume-size | v ∈ avols, abs(avols, apebs, vols, q), ebm-cons(avols), ubi-cons(apebs, vols, wlar, q, bflipset, vtblpnum, sqnum), vtblpnum0 = LEB_SIZE, vtblpnum1 = EB_PAGE_SIZE, ubi-io-inv(apebs) ⊦ ⟪ubi_get_volume_size#(v, vols; ; n)⟫ ⟨ebm_get_volume_size#(v, avols; ; n0)⟩ (abs(avols, apebs, vols, q) ∧ n = n0) | A Proof Obligation |
| refine-read | v ∈ avols, vtblpnum < # avols[v], vtblpnum0 + n ≤ LEB_SIZE, n0 + n ≤ # buf, abs(avols, apebs, vols, q), ebm-cons(avols), ubi-cons(apebs, vols, wlar, q, bflipset, vtblpnum1, sqnum), vtblpnum2 = LEB_SIZE, vtblpnum3 = EB_PAGE_SIZE, ubi-io-inv(apebs), buf = buf0 ⊦ ⟪ubi_read#(v, vtblpnum, vtblpnum0, n0, n, vols, vtblpnum2, apebs; buf, bflipset; err)⟫ ⟨ebm_read#(v, vtblpnum, vtblpnum0, n0, n, avols; buf0; err0)⟩ (abs(avols, apebs, vols, q) ∧ buf = buf0 ∧ err = err0) | A Proof Obligation |
| refine-write | v ∈ avols, vtblpnum < # avols[v], vtblpnum0 + n ≤ LEB_SIZE, is-aligned(vtblpnum0, EB_PAGE_SIZE), is-aligned(n, EB_PAGE_SIZE), n + n0 ≤ # buf, avols[v][vtblpnum].mapped? → vtblpnum0 ≥ avols[v][vtblpnum].fill, abs(avols, apebs, vols, q), ebm-cons(avols), ubi-cons(apebs, vols, wlar, q, bflipset, vtblpnum1, sqnum), vtblpnum2 = LEB_SIZE, vtblpnum3 = EB_PAGE_SIZE, ubi-io-inv(apebs) ⊦ ⟪ubi_write#(v, vtblpnum, vtblpnum0, n0, n, buf, vtblpnum3; vols, wlar, q, bflipset, vtblpnum1, sqnum, apebs; err)⟫ ⟨ebm_write#(v, vtblpnum, vtblpnum0, n0, n, buf; avols; err0)⟩ (abs(avols, apebs, vols, q) ∧ err = err0) | A Proof Obligation |
| recovery | apebs = apebs0, abs(avols0, apebs0, vols, q), ebm-cons(avols0), 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 → (∃ avols. (avols0 ⊆ avols ∧ (ebm-cons(avols0) → ebm-cons(avols))) ∧ ⟨ebm_recover#(; avols; err0)⟩ (abs(avols, apebs, vols0, q0) ∧ err = err0))) ∧ (err ≠ ESUCCESS → (∀ avols. ⟨ebm_recover#(; avols1; err0)⟩ (avols = avols1 ∧ err = err0)))) | A Proof Obligation |
| refine-sync-device | abs(avols, apebs, vols, q), ebm-cons(avols), ubi-cons(apebs, vols, wlar, q, bflipset, vtblpnum, sqnum), vtblpnum0 = LEB_SIZE, vtblpnum1 = EB_PAGE_SIZE, ubi-io-inv(apebs) ⊦ ⟪ubi_sync_device#(vols, bflipset, vtblpnum, sqnum; wlar, q, apebs; err)⟫ ⟨ebm_sync_device#(avols; ; err0)⟩ (abs(avols, apebs, vols, q) ∧ err = err0) | A Proof Obligation |
| refine-get-leb-size | abs(avols, apebs, vols, q), ebm-cons(avols), ubi-cons(apebs, vols, wlar, q, bflipset, vtblpnum, sqnum), vtblpnum0 = LEB_SIZE, vtblpnum1 = EB_PAGE_SIZE, ubi-io-inv(apebs) ⊦ ⟪ubi_get_leb_size#(vtblpnum0; ; n)⟫ ⟨ebm_get_leb_size#(avols; ; n0)⟩ (abs(avols, apebs, vols, q) ∧ n = n0) | A Proof Obligation |
| refine-get-page-size | abs(avols, apebs, vols, q), ebm-cons(avols), ubi-cons(apebs, vols, wlar, q, bflipset, vtblpnum, sqnum), vtblpnum0 = LEB_SIZE, vtblpnum1 = EB_PAGE_SIZE, ubi-io-inv(apebs) ⊦ ⟪ubi_get_page_size#(vtblpnum1; ; n)⟫ ⟨ebm_get_page_size#(avols; ; n0)⟩ (abs(avols, apebs, vols, q) ∧ n = n0) | A Proof Obligation |
| refine-erase-worker | abs(avols, apebs, vols, q), ebm-cons(avols), ubi-cons(apebs, vols, wlar, q, bflipset, vtblpnum, sqnum), vtblpnum0 = LEB_SIZE, vtblpnum1 = EB_PAGE_SIZE, ubi-io-inv(apebs) ⊦ ⟪ubi_erase_worker#(; wlar, q, apebs)⟫ ⟨skip⟩ abs(avols, apebs, vols, q) | A Proof Obligation |
| refine-wl-worker | abs(avols, apebs, vols, q), ebm-cons(avols), ubi-cons(apebs, vols, wlar, q, bflipset, vtblpnum, sqnum), vtblpnum0 = LEB_SIZE, vtblpnum1 = EB_PAGE_SIZE, ubi-io-inv(apebs) ⊦ ⟪ubi_wear_leveling_worker#(vtblpnum0, vtblpnum1; vols, wlar, q, bflipset, vtblpnum, sqnum, apebs; err)⟫ ⟨skip⟩ abs(avols, apebs, vols, q) | A Proof Obligation |
| emptyleb-mkempbuf | ⊦ mkempbuf(LEB_SIZE) = emptyleb | A User Theorem |
| lf-elim-unmapped | ⊦ vols[v][m] ≠ unmapped → (∃ n. vols[v][m] = ⌜n⌝ ) | A User Theorem |
| lf-mapped-data | ⊦ v ∈ vols ∧ m < # vols[v] ∧ vols[v][m] = ⌜n⌝ ∧ apebs[n] = mkpeb(aehdr, avhdr, buf0, m0, boolvar) ∧ avols[v][m] = mapped(buf1, m1) ∧ abs(avols, apebs, vols, q) → buf1 = buf0 | A User Theorem |
| lf-mapped-in-apebs | ⊦ v ∈ vols ∧ m < # vols[v] ∧ vols[v][m] = ⌜n⌝ ∧ valid-ebatbl(apebs, wlar, vols, n0) → n < # apebs | A User Theorem |
| lf-mapped-not-bad | ⊦ v ∈ vols ∧ m < # vols[v] ∧ vols[v][m] = ⌜n⌝ ∧ valid-ebatbl(apebs, wlar, vols, n0) ∧ valid-wl(apebs, wlar) ∧ apebs[n] = mkpeb(aehdr, avhdr, buf, m0, boolvar) → ¬ boolvar | A User Theorem |
| lf-mapped-valid-vidhdr | ⊦ v ∈ vols ∧ m < # vols[v] ∧ vols[v][m] = ⌜n⌝ ∧ valid-ebatbl(apebs, wlar, vols, n0) ∧ apebs[n] = mkpeb(aehdr, avhdr, buf, m0, boolvar) → avhdr.valid? | A User Theorem |
| rangeeq-emptyleb-datasize | ⊦ # buf = n0 + n1 ∧ range=(buf, n0, emptyleb, 0, n1) ∧ n ≤ # buf → (n0 < datasize(buf, n) ↔ false) | A User Theorem |