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: |
|---|---|---|
| erase | mtd_asm_erase#(PNUM; PEBS; ERR) {if PNUM < # PEBS ∧ ¬ PEBS[PNUM].bad then {fail_or_success#(; ; ERR); if ERR = ESUCCESS then PEBS[PNUM] := mkpeb(emptypeb, 0, PEBS[PNUM].bad)} else abort } | An Axiom |
| read | mtd_asm_read#(PNUM, OFFSET, N0, N, PEBS; BUF; BITFLIPS, ERR) {if PNUM < # PEBS ∧ ¬ PEBS[PNUM].bad ∧ OFFSET + N ≤ PEB_SIZE ∧ N0 + N ≤ # BUF then {fail_or_success#(; ; ERR); BITFLIPS := ?; if ERR = ESUCCESS then BUF := copy(PEBS[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 | mtd_asm_write#(PNUM, OFFSET, N0, N, BUF; PEBS; ERR) {if PNUM < # PEBS ∧ ¬ PEBS[PNUM].bad ∧ PEBS[PNUM].fill ≤ OFFSET ∧ OFFSET + N ≤ PEB_SIZE ∧ N0 + N ≤ # BUF ∧ is-aligned(OFFSET, EB_PAGE_SIZE) ∧ is-aligned(N, EB_PAGE_SIZE) then {fail_or_success#(; ; ERR); if ERR = ESUCCESS then {PEBS[PNUM].data := copy(BUF, N0, PEBS[PNUM].data, OFFSET, N); PEBS[PNUM].fill := OFFSET + N} else choose N1 with (N1 < N ∨ N1 = 0 ∧ N = 0) ∧ is-aligned(N1, EB_PAGE_SIZE) in if N1 ≠ 0 then {PEBS[PNUM].data := copy(BUF, N0, PEBS[PNUM].data, OFFSET, N1); PEBS[PNUM].fill := OFFSET + N1}} else abort } | An Axiom |
| isbad | mtd_asm_isbad#(PNUM, PEBS; ; ISBAD, ERR) {if PNUM < # PEBS then {fail_or_success#(; ; ERR); if ERR = ESUCCESS then ISBAD := PEBS[PNUM].bad else ISBAD := ?} else abort} | An Axiom |
| markbad | mtd_asm_markbad#(PNUM; PEBS; ERR) {if PNUM < # PEBS ∧ ¬ PEBS[PNUM].bad then {fail_or_success#(; ; ERR); if ERR = ESUCCESS then PEBS[PNUM].bad := true} else abort} | An Axiom |
| blockcount | mtd_asm_get_blockcount#(PEBS; ; N){N := # PEBS} | An Axiom |
| init | mtd_asm_init#(; ; PEBS, ERR){fail_or_success#(; ; ERR); choose pebs with ERR = ESUCCESS → mtd-cons(pebs) in PEBS := pebs} | An Axiom |
| peb-size | mtd_asm_get_peb_size#(PEBS; ; N){N := PEB_SIZE} | An Axiom |
| page-size | mtd_asm_get_page_size#(PEBS; ; N){N := EB_PAGE_SIZE} | An Axiom |
| inv-init | ⊦ ⟪mtd_asm_init#(; ; pebs, err)⟫ ((err = ESUCCESS → mtd-cons(pebs)) ∧ (err = ESUCCESS ∨ ⌊err⌋ )) | A Proof Obligation |
| inv-crash | pebs = pebs0, mtd-cons(pebs0) ⊦ ⟪skip⟫ mtd-cons(pebs) | A Proof Obligation |
| inv-erase | mtd-cons(pebs), m < # pebs, ¬ pebs[m].bad ⊦ ⟪mtd_asm_erase#(m; pebs; err)⟫ mtd-cons(pebs) | A Proof Obligation |
| inv-read | mtd-cons(pebs), m < # pebs, ¬ pebs[m].bad, m0 + n ≤ PEB_SIZE, n0 + n ≤ # buf ⊦ ⟪mtd_asm_read#(m, m0, n0, n, pebs; buf; bitflips, err)⟫ true | A Proof Obligation |
| inv-write | mtd-cons(pebs), m < # pebs, ¬ pebs[m].bad, pebs[m].fill ≤ m0, m0 + n ≤ PEB_SIZE, n0 + n ≤ # buf, is-aligned(m0, EB_PAGE_SIZE), is-aligned(n, EB_PAGE_SIZE) ⊦ ⟪mtd_asm_write#(m, m0, n0, n, buf; pebs; err)⟫ mtd-cons(pebs) | A Proof Obligation |
| inv-isbad | mtd-cons(pebs), m < # pebs ⊦ ⟪mtd_asm_isbad#(m, pebs; ; isbad, err)⟫ true | A Proof Obligation |
| inv-markbad | mtd-cons(pebs), m < # pebs, ¬ pebs[m].bad ⊦ ⟪mtd_asm_markbad#(m; pebs; err)⟫ mtd-cons(pebs) | A Proof Obligation |
| inv-blockcount | mtd-cons(pebs) ⊦ ⟪mtd_asm_get_blockcount#(pebs; ; n)⟫ true | A Proof Obligation |
| crash-neutral-erase | m < # pebs, ¬ pebs[m].bad, mtd-cons(pebs), pebs0 = pebs ⊦ ⟨mtd_asm_erase#(m; pebs; err)⟩ (pebs0 = pebs) | A Proof Obligation |
| crash-neutral-read | m < # pebs, ¬ pebs[m].bad, m0 + n ≤ PEB_SIZE, n0 + n ≤ # buf, mtd-cons(pebs), pebs0 = pebs ⊦ ⟨mtd_asm_read#(m, m0, n0, n, pebs; buf; bitflips, err)⟩ (pebs0 = pebs) | A Proof Obligation |
| crash-neutral-write | m < # pebs, ¬ pebs[m].bad, pebs[m].fill ≤ m0, m0 + n ≤ PEB_SIZE, n0 + n ≤ # buf, is-aligned(m0, EB_PAGE_SIZE), is-aligned(n, EB_PAGE_SIZE), mtd-cons(pebs), pebs0 = pebs ⊦ ⟨mtd_asm_write#(m, m0, n0, n, buf; pebs; err)⟩ (pebs0 = pebs) | A Proof Obligation |
| crash-neutral-isbad | m < # pebs, mtd-cons(pebs), pebs0 = pebs ⊦ ⟨mtd_asm_isbad#(m, pebs; ; isbad, err)⟩ (pebs0 = pebs) | A Proof Obligation |
| crash-neutral-markbad | m < # pebs, ¬ pebs[m].bad, mtd-cons(pebs), pebs0 = pebs ⊦ ⟨mtd_asm_markbad#(m; pebs; err)⟩ (pebs0 = pebs) | A Proof Obligation |
| crash-neutral-blockcount | mtd-cons(pebs), pebs0 = pebs ⊦ ⟨mtd_asm_get_blockcount#(pebs; ; n)⟩ (pebs0 = pebs) | A Proof Obligation |
| crash-neutral-peb-size | mtd-cons(pebs), pebs0 = pebs ⊦ ⟨mtd_asm_get_peb_size#(pebs; ; n)⟩ (pebs0 = pebs) | A Proof Obligation |
| crash-neutral-page-size | mtd-cons(pebs), pebs0 = pebs ⊦ ⟨mtd_asm_get_page_size#(pebs; ; n)⟩ (pebs0 = pebs) | A Proof Obligation |
| inv-peb-size | mtd-cons(pebs) ⊦ ⟪mtd_asm_get_peb_size#(pebs; ; n)⟫ true | A Proof Obligation |
| inv-page-size | mtd-cons(pebs) ⊦ ⟪mtd_asm_get_page_size#(pebs; ; n)⟫ true | A Proof Obligation |
| reduce-mtd-cons | ⊦ mtd-cons(pebs0) → (mtd-cons(pebs1) ↔ (∀ n. n < # pebs1 ∧ (n < # pebs0 → mtd-valid-peb(pebs0[n])) → mtd-valid-peb(pebs1[n]))) | A User Theorem |