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: |
|---|---|---|
| format | persistence_io_format#(VOLSIZE, SIZE, LPT, INDEXADR0, MAXINO0; SB, PAGESIZE, LEBSIZE, AVOL; LOGOFF, ERR) {if VOLSIZE = # LPT ∧ SIZE = LEB_SIZE then let N = 5 + 2 * lptlebs(VOLSIZE, SIZE) in {ebm_avol_format#(VOLSIZE + N; ; AVOL, ERR); if ERR ≠ ESUCCESS then debug#("persistence-io: ubi format failed"); if ERR = ESUCCESS then ebm_avol_get_leb_size#(AVOL; ; LEBSIZE); SB.indexaddr := INDEXADR0; SB.maxino := MAXINO0; SB.log := SB_LOG; SB.orph := SB_ORPH; SB.orphsize := 0; SB.lpt := SB_LPT; SB.main := N; if ERR = ESUCCESS then ebm_avol_get_page_size#(AVOL; ; PAGESIZE); if ERR = ESUCCESS then ebm_avol_remap#(SB.log; AVOL; ERR); if ERR = ESUCCESS then ebm_avol_remap#(SB.orph; AVOL; ERR); if ERR = ESUCCESS then let BUF = ? in {persistence_io_encode_lpt#(LPT, LEBSIZE; ; BUF, ERR); if ERR = ESUCCESS then persistence_io_write_lebs#(SB.lpt, lptlebs(VOLSIZE, LEBSIZE), BUF, LEBSIZE; AVOL; ERR)}; if ERR = ESUCCESS then persistence_io_write_superblock#(SB, PAGESIZE, LEBSIZE; AVOL; ERR); LOGOFF := LEBSIZE} else abort } | An Axiom |
| recover | persistence_io_recover#(; INDEXADR0, MAXINO0, ORPHANS, LOG, LPT, SB, LOGOFF, PAGESIZE, LEBSIZE, AVOL; ERR) {ebm_avol_recover#(; AVOL; ERR); if ERR ≠ ESUCCESS then debug#("persistence-io: ubi recover failed") else let VOLSIZE = ? in {ebm_avol_get_leb_size#(AVOL; ; LEBSIZE); ebm_avol_get_page_size#(AVOL; ; PAGESIZE); ebm_avol_get_volume_size#(AVOL; ; VOLSIZE); persistence_io_read_superblock#(PAGESIZE, LEBSIZE, AVOL; SB; ERR); if ERR ≠ ESUCCESS then debug#("persistence-io: reading superblock failed"); if ERR = ESUCCESS then {persistence_io_read_log#(SB, PAGESIZE, LEBSIZE, AVOL; LOGOFF; LOG, ERR); if ERR ≠ ESUCCESS then debug#("persistence-io: reading log failed")}; if ERR = ESUCCESS then {persistence_io_read_orphans#(SB, AVOL; ORPHANS; ERR); if ERR ≠ ESUCCESS then debug#("persistence-io: reading orphans failed")}; if ERR = ESUCCESS then {VOLSIZE := VOLSIZE - SB.main; let BUF = ? in {persistence_io_read_lebs#(SB.lpt, lptlebs(VOLSIZE, LEBSIZE), LEBSIZE, AVOL; ; BUF, ERR); if ERR = ESUCCESS then {LPT := mklparray(VOLSIZE); LPT := fill(LPT, mklp(0, 0, LP_FREE, 0)); persistence_io_decode_lpt#(BUF; LPT, ERR)}; if ERR ≠ ESUCCESS then debug#("persistence-io: reading LPT failed")}}; if ERR = ESUCCESS then {LOGOFF := LEBSIZE; INDEXADR0 := SB.indexaddr; MAXINO0 := SB.maxino}} } | An Axiom |
| commit | persistence_io_commit#(LPT, INDEXADR0, MAXINO0, PAGESIZE, LEBSIZE; ORPHANS, SB, AVOL, LOGOFF; ERR) {if # LPT + SB.main = # AVOL then let VOLSIZE = ? in {ebm_avol_get_volume_size#(AVOL; ; VOLSIZE); VOLSIZE := VOLSIZE - SB.main; let NEWSB = SB in {NEWSB.indexaddr := INDEXADR0; NEWSB.maxino := MAXINO0; NEWSB.orphsize := # ORPHANS; if NEWSB.log = SB_LOG then {NEWSB.log := SB_LOG + 1; NEWSB.orph := SB_ORPH + 1; NEWSB.lpt := SB_LPT + lptlebs(VOLSIZE, LEBSIZE)} else {NEWSB.log := SB_LOG; NEWSB.orph := SB_ORPH; NEWSB.lpt := SB_LPT}; ebm_avol_remap#(NEWSB.log; AVOL; ERR); if ERR = ESUCCESS then persistence_io_write_orphans#(NEWSB.orph, PAGESIZE, LEBSIZE; ORPHANS, AVOL; ERR); if ERR = ESUCCESS then let BUF = ? in {persistence_io_encode_lpt#(LPT, LEBSIZE; ; BUF, ERR); if ERR = ESUCCESS then persistence_io_write_lebs#(NEWSB.lpt, lptlebs(VOLSIZE, LEBSIZE), BUF, LEBSIZE; AVOL; ERR)}; if ERR = ESUCCESS then ebm_avol_sync_device#(AVOL; ; ERR); if ERR = ESUCCESS then persistence_io_write_superblock#(NEWSB, PAGESIZE, LEBSIZE; AVOL; ERR); if ERR = ESUCCESS then {SB := NEWSB; LOGOFF := 0}}} else abort } | An Axiom |
| get-volume-size | persistence_io_get_volume_size#(SB, AVOL; ; N){ebm_avol_get_volume_size#(AVOL; ; N); N := N - SB.main} | An Axiom |
| write-superblock | persistence_io_write_superblock#(NEWSB, PAGESIZE, LEBSIZE; AVOL; ERR) {let SIZE = encoding-size(NEWSB, PAGESIZE) in if SIZE ≤ LEBSIZE then let BUF = mkbuf(SIZE) in {encode_superblock#(NEWSB, 0, PAGESIZE; BUF, SIZE; ERR); if ERR = ESUCCESS then ebm_avol_change#(0, SIZE, BUF; AVOL; ERR)} else ERR := ENOSPC } | An Axiom |
| read-superblock | persistence_io_read_superblock#(PAGESIZE, LEBSIZE, AVOL; NEWSB; ERR) {let BUF = mkbuf(LEBSIZE) in {ebm_avol_read#(0, 0, 0, LEBSIZE, AVOL; BUF; ERR); if ERR = ESUCCESS then let SIZE = ? in decode_superblock#(0, BUF, PAGESIZE; NEWSB, SIZE; ERR)} } | An Axiom |
| add-log-leb | persistence_io_add_log_leb#(LNUM, SB, PAGESIZE, LEBSIZE; LOGOFF, AVOL; ERR) {if ¬ LOGOFF + PAGESIZE ≤ LEBSIZE then ERR := ECOMMIT else let BUF = mkbuf(PAGESIZE) in {encode_ref_node#(PAGESIZE, rnode(LNUM); BUF; ERR); if ERR = ESUCCESS then {ebm_avol_write#(SB.log, LOGOFF, 0, PAGESIZE, BUF; AVOL; ERR); if ERR = ESUCCESS then LOGOFF := LOGOFF + PAGESIZE else {LOGOFF := LEBSIZE; debug#("persistence-io: failed to add LEB " + LNUM.toString + " to log")}}} } | An Axiom |
| requires-commit | persistence_io_requires_commit#(LOGOFF, LEBSIZE; ; COMMIT?){COMMIT? := LOGOFF = LEBSIZE} | An Axiom |
| read-log | persistence_io_read_log#(SB, PAGESIZE, LEBSIZE, AVOL; LOGOFF; LOG, ERR) {LOG := []; ERR := ESUCCESS; LOGOFF := 0; let BUF = mkbuf(PAGESIZE) in while ERR = ESUCCESS ∧ LOGOFF < LEBSIZE do {/* (prepost-read-log : invariant LOGOFF ≤ LEB_SIZE ∧ # BUF = PAGESIZE ∧ is-aligned(LOGOFF, PAGESIZE) ∧ (ERR = ESUCCESS ∨ ERR = ENOENT ∨ ⌊ERR⌋ ) ∧ ebm-vol-inv(AVOL) ∧ SB.log < # AVOL ∧ AVOL[SB.log].mapped? ∧ (ERR = ESUCCESS → LOGOFF ≤ # AVOL[SB.log].data ∧ is-encoded(LOG, subarray(AVOL[SB.log].data, 0, LOGOFF))) ∧ (ERR = ENOENT → is-encoded(LOG, AVOL[SB.log].data)) wfbound LEB_SIZE - LOGOFF) */; ebm_avol_read#(SB.log, LOGOFF, 0, PAGESIZE, AVOL; BUF; ERR); if ERR = ESUCCESS then if isempty(BUF) then ERR := ENOENT else let RND = ? in {decode_ref_node#(PAGESIZE, BUF; RND; ERR); if ERR = ESUCCESS then LOG := LOG + RND.leb}; LOGOFF := LOGOFF + PAGESIZE}; if ERR = ENOENT then ERR := ESUCCESS } | An Axiom |
| remap | persistence_io_remap#(LNUM, SB; AVOL; ERR){if SB.main + LNUM < # AVOL then ebm_avol_remap#(SB.main + LNUM; AVOL; ERR) else abort} | An Axiom |
| encode-lpt | persistence_io_encode_lpt#(LPT, LEBSIZE; ; BUF, ERR) {ERR := ESUCCESS; BUF := mkbuf(lptsize(# LPT, LEBSIZE)); let N = 0, SIZE = ? in while ERR = ESUCCESS ∧ N < # LPT do {/* (prepost-encode-lpt : invariant N ≤ # LPT ∧ # BUF = lptsize(# LPT, LEB_SIZE) ∧ (ERR = ESUCCESS ∨ ⌊ERR⌋ ) ∧ (ERR = ESUCCESS → is-encoded(LPT, BUF, N)) wfbound # LPT - N) */; encode_lprops#(LPT[N], N * ENCODED_LPROPS_SIZE; BUF, SIZE; ERR); N := N + 1} } | An Axiom |
| decode-lpt | persistence_io_decode_lpt#(BUF; LPT, ERR) {ERR := ESUCCESS; let N = 0 in while ERR = ESUCCESS ∧ N < # LPT do {/* (prepost-decode-lpt : invariant N ≤ # LPT ∧ # BUF = lptsize(# LPT, LEB_SIZE) ∧ # LPT = # LPT` ∧ (ERR = ESUCCESS ∨ ⌊ERR⌋ ) ∧ (ERR = ESUCCESS → is-encoded(LPT, BUF, N)) wfbound # LPT - N) */; let SIZE = ? in decode_lprops#(N * ENCODED_LPROPS_SIZE, BUF; LPT[N], SIZE; ERR); N := N + 1} } | An Axiom |
| read-lebs | persistence_io_read_lebs#(LNUM, SIZE, LEBSIZE, AVOL; ; BUF, ERR) {ERR := ESUCCESS; BUF := mkbuf(SIZE * LEBSIZE); let N = 0 in while ERR = ESUCCESS ∧ N < SIZE do {/* (prepost-read-lebs : invariant N ≤ SIZE ∧ # BUF = SIZE * LEB_SIZE ∧ LNUM + SIZE ≤ # AVOL ∧ ebm-vol-inv(AVOL) ∧ mapped-full?(AVOL, LNUM, SIZE) ∧ (ERR = ESUCCESS ∨ ⌊ERR⌋ ) ∧ (ERR = ESUCCESS → subarray(BUF, 0, N * LEB_SIZE) = lebs(AVOL, LNUM, N)) wfbound SIZE - N) */; ebm_avol_read#(LNUM + N, 0, N * LEBSIZE, LEBSIZE, AVOL; BUF; ERR); N := N + 1} } | An Axiom |
| write-lebs | persistence_io_write_lebs#(LNUM, SIZE, BUF, LEBSIZE; AVOL; ERR) {ERR := ESUCCESS; let N = 0 in while ERR = ESUCCESS ∧ N < SIZE do {/* (prepost-write-lebs : invariant N ≤ SIZE ∧ ebm-vol-inv(AVOL) ∧ # BUF = SIZE * LEB_SIZE ∧ (ERR = ESUCCESS ∨ ⌊ERR⌋ ) ∧ # AVOL = # AVOL` ∧ range=(AVOL, 0, AVOL`, 0, LNUM) ∧ range=(AVOL, LNUM + SIZE, AVOL`, LNUM + SIZE, # AVOL` - LNUM + SIZE) ∧ (ERR = ESUCCESS → lebs(AVOL, LNUM, N) = subarray(BUF, 0, N * LEB_SIZE) ∧ mapped-full?(AVOL, LNUM, N)) wfbound SIZE - N) */; ebm_avol_remap#(LNUM + N; AVOL; ERR); if ERR = ESUCCESS then ebm_avol_write#(LNUM + N, 0, N * LEBSIZE, LEBSIZE, BUF; AVOL; ERR); N := N + 1} } | An Axiom |
| encode-orphans | persistence_io_encode_orphans#(PAGESIZE, LEBSIZE; ORPHANS, BUF; ERR) {if # ORPHANS * ENCODED_NAT_SIZE > LEBSIZE then ERR := ENOSPC else {ERR := ESUCCESS; BUF := mkbuf(align↑(# ORPHANS * ENCODED_NAT_SIZE, PAGESIZE)); let OFFSET = 0, SIZE = ? in while ERR = ESUCCESS ∧ ORPHANS ≠ ∅ do {/* (prepost-encode-orphans : invariant (ERR = ESUCCESS ∨ ⌊ERR⌋ ) ∧ is-aligned(# BUF, PAGESIZE) ∧ ORPHANS ⊆ ORPHANS` ∧ # BUF ≤ LEBSIZE ∧ ( ERR = ESUCCESS → OFFSET + # ORPHANS * ENCODED_NAT_SIZE ≤ # BUF ∧ is-encoded(ORPHANS` \ ORPHANS, subarray(BUF, 0, OFFSET))) wfbound # ORPHANS) */; choose N with N ∈ ORPHANS in {encode_nat#(N, OFFSET; BUF, SIZE; ERR); OFFSET := OFFSET + ENCODED_NAT_SIZE; ORPHANS := ORPHANS -- N}}} } | An Axiom |
| decode-orphans | persistence_io_decode_orphans#(SIZE, BUF; ; ORPHANS, ERR) {ORPHANS := ∅; ERR := ESUCCESS; let OFFSET = 0 in while ERR = ESUCCESS ∧ SIZE ≠ 0 do {/* (prepost-decode-orphans : invariant (ERR = ESUCCESS ∨ ⌊ERR⌋ ) ∧ OFFSET + SIZE * ENCODED_NAT_SIZE = # BUF ∧ ( ERR = ESUCCESS → (∃ orphans. is-encoded(ORPHANS, subarray(BUF, 0, OFFSET)) ∧ is-encoded(orphans, subarray(BUF, OFFSET, # BUF - OFFSET)) ∧ orphans ∩ ORPHANS = ∅)) wfbound SIZE) */; let N = ?, SIZE = ? in {decode_nat#(OFFSET, BUF; N, SIZE; ERR); if ERR = ESUCCESS then ORPHANS := ORPHANS ++ N; OFFSET := OFFSET + ENCODED_NAT_SIZE}; SIZE := SIZE - 1} } | An Axiom |
| read-orphans | persistence_io_read_orphans#(SB, AVOL; ORPHANS; ERR) {let BUF = mkbuf(SB.orphsize * ENCODED_NAT_SIZE) in {ebm_avol_read#(SB.orph, 0, 0, SB.orphsize * ENCODED_NAT_SIZE, AVOL; BUF; ERR); if ERR = ESUCCESS then persistence_io_decode_orphans#(SB.orphsize, BUF; ; ORPHANS, ERR)} } | An Axiom |
| write-orphans | persistence_io_write_orphans#(LNUM, PAGESIZE, LEBSIZE; ORPHANS, AVOL; ERR) {let BUF = mkbuf(0) in {persistence_io_encode_orphans#(PAGESIZE, LEBSIZE; ORPHANS, BUF; ERR); if ERR = ESUCCESS then ebm_avol_remap#(LNUM; AVOL; ERR); if ERR = ESUCCESS then ebm_avol_write#(LNUM, 0, 0, # BUF, BUF; AVOL; ERR)} } | An Axiom |
| unmap | persistence_io_unmap#(LNUM, SB; AVOL){if SB.main + LNUM < # AVOL then ebm_avol_unmap#(SB.main + LNUM; AVOL) else abort} | An Axiom |
| read | persistence_io_read#(LNUM, OFFSET, N0, N, SB, AVOL; BUF; ERR) {if SB.main + LNUM < # AVOL ∧ AVOL[SB.main + LNUM].mapped? ∧ N0 + N ≤ # BUF ∧ OFFSET + N ≤ LEB_SIZE then ebm_avol_read#(SB.main + LNUM, OFFSET, N0, N, AVOL; BUF; ERR) else abort } | An Axiom |
| write | persistence_io_write#(LNUM, OFFSET, N0, N, BUF, SB; AVOL; ERR) {if SB.main + LNUM < # AVOL ∧ AVOL[SB.main + LNUM].mapped? ∧ # AVOL[SB.main + LNUM].data ≤ OFFSET ∧ is-aligned(OFFSET, EB_PAGE_SIZE) ∧ is-aligned(N, EB_PAGE_SIZE) ∧ OFFSET + N ≤ LEB_SIZE ∧ N0 + N ≤ # BUF then ebm_avol_write#(SB.main + LNUM, OFFSET, N0, N, BUF; AVOL; ERR) else abort } | An Axiom |
| get-leb-size | persistence_io_get_leb_size#(LEBSIZE; ; N){N := LEBSIZE} | An Axiom |
| get-page-size | persistence_io_get_page_size#(PAGESIZE; ; N){N := PAGESIZE} | An Axiom |
| inv-format | m = # lpt, m0 = LEB_SIZE ⊦ ⟪persistence_io_format#(m, m0, lpt, adr, m1; sb, m2, m3, avol; logoff, err)⟫ ( ( err = ESUCCESS → (∃ lpt, log, orphans. persistence-io-inv(sb, logoff, avol, lpt, log, orphans)) ∧ m2 = EB_PAGE_SIZE ∧ m3 = LEB_SIZE ∧ ebm-vol-inv(avol)) ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ ( err = ESUCCESS → sb.indexaddr = adr ∧ sb.maxino = m1 ∧ subarray(avol, sb.main, # avol - sb.main) = fill(mkavolume(m), unmapped) ∧ is-encoded(lpt, lebs(avol, sb.lpt, lptlebs(# avol - sb.main, LEB_SIZE))) ∧ is-encoded([], avol[sb.log].data) ∧ is-encoded(∅, avol[sb.orph].data))) | A Proof Obligation |
| inv-recover | avol ⊆ avol0, ∃ lpt, log, orphans. persistence-io-inv(sb, m, avol, lpt, log, orphans), m0 = EB_PAGE_SIZE, m1 = LEB_SIZE, ebm-vol-inv(avol) ⊦ ⟪persistence_io_recover#(; adr, m2, orphans, log, lpt, sb0, logoff, m3, m4, avol0; err)⟫ ( ( err = ESUCCESS → (∃ lpt, log, orphans. persistence-io-inv(sb0, logoff, avol0, lpt, log, orphans)) ∧ m3 = EB_PAGE_SIZE ∧ m4 = LEB_SIZE ∧ ebm-vol-inv(avol0)) ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ ( err = ESUCCESS → sb0 = sb ∧ # avol0 = # avol ∧ adr = sb0.indexaddr ∧ m2 = sb0.maxino ∧ # lpt = # avol0 - sb0.main ∧ is-encoded(lpt, lebs(avol0, sb0.lpt, lptlebs(# avol0 - sb0.main, LEB_SIZE))) ∧ lebs(avol0, sb0.lpt, lptlebs(# avol0 - sb0.main, LEB_SIZE)) = lebs(avol, sb0.lpt, lptlebs(# avol0 - sb0.main, LEB_SIZE)) ∧ is-encoded(log, avol0[sb0.log].data) ∧ is-encoded-pad(orphans, sb0.orphsize, avol0[sb0.orph].data) ∧ avol0[sb0.orph] = avol[sb0.orph] ∧ avol0[sb0.log] = avol[sb0.log])) | A Proof Obligation |
| inv-commit | ∃ lpt, log, orphans. persistence-io-inv(sb, logoff, avol, lpt, log, orphans), m = EB_PAGE_SIZE, m0 = LEB_SIZE, ebm-vol-inv(avol), # lpt + sb.main = # avol, ns = orphans, sb0 = sb, avol0 = avol ⊦ ⟪persistence_io_commit#(lpt, adr, m1, m, m0; orphans, sb, avol, logoff; err)⟫ ( (∃ lpt, log, orphans. persistence-io-inv(sb, logoff, avol, lpt, log, orphans)) ∧ ebm-vol-inv(avol) ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ ( err = ESUCCESS → sb.indexaddr = adr ∧ sb.maxino = m1 ∧ is-encoded([], avol[sb.log].data) ∧ is-encoded(lpt, lebs(avol, sb.lpt, lptlebs(# avol - sb.main, LEB_SIZE))) ∧ is-encoded-pad(ns, sb.orphsize, avol[sb.orph].data)) ∧ ( err ≠ ESUCCESS → sb = sb0 ∧ avol[sb.log] = avol0[sb.log] ∧ avol[sb.orph] = avol0[sb.orph] ∧ lebs(avol, sb.lpt, lptlebs(# avol - sb.main, LEB_SIZE)) = lebs(avol0, sb.lpt, lptlebs(# avol - sb.main, LEB_SIZE))) ∧ sb.main = sb0.main ∧ # avol = # avol0 ∧ subarray(avol, sb.main, # avol - sb.main) = subarray(avol0, sb.main, # avol - sb.main)) | A Proof Obligation |
| inv-get-volume-size | ∃ lpt, log, orphans. persistence-io-inv(sb, logoff, avol, lpt, log, orphans), ebm-vol-inv(avol) ⊦ ⟪persistence_io_get_volume_size#(sb, avol; ; n)⟫ true | A Proof Obligation |
| inv-add-log-leb | ∃ lpt, log, orphans. persistence-io-inv(sb, logoff, avol, lpt, log, orphans), m = EB_PAGE_SIZE, m0 = LEB_SIZE, ebm-vol-inv(avol) ⊦ ⟪persistence_io_add_log_leb#(m1, sb, m, m0; logoff, avol; err)⟫ ((∃ lpt, log, orphans. persistence-io-inv(sb, logoff, avol, lpt, log, orphans)) ∧ ebm-vol-inv(avol)) | A Proof Obligation |
| inv-requires-commit | ∃ lpt, log, orphans. persistence-io-inv(sb, logoff, avol, lpt, log, orphans), m = LEB_SIZE ⊦ ⟪persistence_io_requires_commit#(logoff, m; ; boolvar)⟫ true | A Proof Obligation |
| inv-remap | ∃ lpt, log, orphans. persistence-io-inv(sb, logoff, avol, lpt, log, orphans), ebm-vol-inv(avol), sb.main + m < # avol ⊦ ⟪persistence_io_remap#(m, sb; avol; err)⟫ ((∃ lpt, log, orphans. persistence-io-inv(sb, logoff, avol, lpt, log, orphans)) ∧ ebm-vol-inv(avol)) | A Proof Obligation |
| inv-unmap | ∃ lpt, log, orphans. persistence-io-inv(sb, logoff, avol, lpt, log, orphans), ebm-vol-inv(avol), sb.main + m < # avol ⊦ ⟪persistence_io_unmap#(m, sb; avol)⟫ ((∃ lpt, log, orphans. persistence-io-inv(sb, logoff, avol, lpt, log, orphans)) ∧ ebm-vol-inv(avol)) | A Proof Obligation |
| inv-read | ∃ lpt, log, orphans. persistence-io-inv(sb, logoff, avol, lpt, log, orphans), ebm-vol-inv(avol), sb.main + m < # avol, avol[sb.main + m].mapped?, n + n0 ≤ # buf, m0 + n0 ≤ LEB_SIZE ⊦ ⟪persistence_io_read#(m, m0, n, n0, sb, avol; buf; err)⟫ true | A Proof Obligation |
| inv-write | ∃ lpt, log, orphans. persistence-io-inv(sb, logoff, avol, lpt, log, orphans), ebm-vol-inv(avol), sb.main + m < # avol, avol[sb.main + m].mapped?, # avol[sb.main + m].data ≤ m0, is-aligned(m0, EB_PAGE_SIZE), is-aligned(n, EB_PAGE_SIZE), m0 + n ≤ LEB_SIZE, n0 + n ≤ # buf ⊦ ⟪persistence_io_write#(m, m0, n0, n, buf, sb; avol; err)⟫ ((∃ lpt, log, orphans. persistence-io-inv(sb, logoff, avol, lpt, log, orphans)) ∧ ebm-vol-inv(avol)) | A Proof Obligation |
| inv-get-leb-size | m = LEB_SIZE ⊦ ⟪persistence_io_get_leb_size#(m; ; n)⟫ true | A Proof Obligation |
| inv-get-page-size | m = EB_PAGE_SIZE ⊦ ⟪persistence_io_get_page_size#(m; ; n)⟫ true | A Proof Obligation |
| avol-down-mapped-eq | n < # avol0 ⊦ avol0 ⊆ avol1 ∧ avol0[n] = mapped(buf) ∧ ebm-vol-inv(avol0) → avol1[n] = mapped(buf) | A User Theorem |
| avol-down-size | ⊦ m = # avol0 ∧ avol0 ⊆ avol1 → (n = # avol1 ↔ n = m) | A User Theorem |
| avol-down-size-le | ⊦ avol0 ⊆ avol1 → (n ≤ # avol1 ↔ n ≤ # avol0) | A User Theorem |
| avol-down-size-ls | ⊦ avol0 ⊆ avol1 → ¬ # avol1 < # avol0 | A User Theorem |
| id-circle-subarray-concrete-below | n0 < n, n + m + m0 ≤ # avol ⊦ id○(avol, avol0, (* n0)) → subarray(avol, (* n) + m, m0) = subarray(avol0, n + m, m0) | A User Theorem |
| idcircle-concrete-write | n0 ≠ n, m ≠ n0, n0 < # avol ⊦ avol0[(* n0)] = aleb0 ∧ id○(avol, avol0[(* n), aleb], (* m)) → avol[(* n0)] = aleb0 | A User Theorem |
| ls-del-notin | ¬ n ∈ ns ⊦ ns -- n = ns | A User Theorem |
| nat-stuff0 | ⊦ n = n0 + n1 ∧ n ≤ n1 + n2 → ¬ n2 < n0 | A User Theorem |
| nat-stuff1 | ⊦ n = n0 + n1 → (n0 + n1 + n2 ≤ n ↔ n2 = 0) | A User Theorem |
| nat-stuff2 | ⊦ n = 5 + n1 → n ≠ 0 | A User Theorem |
| nat-stuff3 | ⊦ n = 5 + n1 → n ≠ 1 | A User Theorem |
| prepost-add-log-leb | persistence-io-inv(sb, logoff, avol, lpt, log, orphans), ebm-vol-inv(avol), avol0 = avol ⊦ ⟪persistence_io_add_log_leb#(m, sb, EB_PAGE_SIZE, LEB_SIZE; logoff, avol; err)⟫ ( (err = ESUCCESS ∨ ⌊err⌋ ) ∧ ebm-vol-inv(avol) ∧ subarray(avol, sb.main, # lpt) = subarray(avol0, sb.main, # lpt) ∧ (err = ESUCCESS → persistence-io-inv(sb, logoff, avol, lpt, log + m, orphans)) ∧ (err ≠ ESUCCESS → persistence-io-inv(sb, logoff, avol, lpt, log, orphans))) | A User Theorem |
| prepost-decode-lpt | # buf = lptsize(# lpt, LEB_SIZE), buf0 = buf, lpt0 = lpt ⊦ ⟪persistence_io_decode_lpt#(buf; lpt, err)⟫ ((err = ESUCCESS ∨ ⌊err⌋ ) ∧ # buf = # buf0 ∧ (err = ESUCCESS → is-encoded(lpt, buf) ∧ # lpt = # lpt0)) | A User Theorem |
| prepost-decode-orphans | is-encoded(orphans0, buf), n = # orphans0, # buf = # orphans0 * ENCODED_NAT_SIZE ⊦ ⟪persistence_io_decode_orphans#(n, buf; ; orphans, err)⟫ ((err = ESUCCESS ∨ ⌊err⌋ ) ∧ (err = ESUCCESS → orphans = orphans0)) | A User Theorem |
| prepost-encode-lpt | ⊦ ⟪persistence_io_encode_lpt#(lpt, LEB_SIZE; ; buf, err)⟫ ((err = ESUCCESS ∨ ⌊err⌋ ) ∧ (err = ESUCCESS → is-encoded(lpt, buf) ∧ # buf = lptsize(# lpt, LEB_SIZE))) | A User Theorem |
| prepost-encode-orphans | orphans0 = orphans ⊦ ⟪persistence_io_encode_orphans#(EB_PAGE_SIZE, LEB_SIZE; orphans, buf; err)⟫ ((err = ESUCCESS ∨ ⌊err⌋ ) ∧ (err = ESUCCESS → is-encoded-pad(orphans0, # orphans0, buf) ∧ # buf ≤ LEB_SIZE)) | A User Theorem |
| prepost-read-lebs | ebm-vol-inv(avol), n + m ≤ # avol, mapped-full?(avol, n, m) ⊦ ⟪persistence_io_read_lebs#(n, m, LEB_SIZE, avol; ; buf, err)⟫ ((err = ESUCCESS ∨ ⌊err⌋ ) ∧ (err = ESUCCESS → buf = lebs(avol, n, m))) | A User Theorem |
| prepost-read-log | ebm-vol-inv(avol), sb.log < # avol, avol[sb.log].mapped?, is-encoded(log0, avol[sb.log].data) ⊦ ⟪persistence_io_read_log#(sb, EB_PAGE_SIZE, LEB_SIZE, avol; logoff; log, err)⟫ ((err = ESUCCESS ∨ ⌊err⌋ ) ∧ (err = ESUCCESS → log = log0)) | A User Theorem |
| prepost-read-orphans | persistence-io-inv(sb, logoff, avol, lpt, log, orphans0), ebm-vol-inv(avol) ⊦ ⟪persistence_io_read_orphans#(sb, avol; orphans; err)⟫ ((err = ESUCCESS ∨ ⌊err⌋ ) ∧ (err = ESUCCESS → orphans = orphans0)) | A User Theorem |
| prepost-read-superblock | # avol ≠ 0, avol[0].mapped?, is-encoded(sb0, avol[0].data), ebm-vol-inv(avol) ⊦ ⟪persistence_io_read_superblock#(EB_PAGE_SIZE, LEB_SIZE, avol; sb; err)⟫ ((err = ESUCCESS ∨ ⌊err⌋ ) ∧ (err = ESUCCESS → sb = sb0)) | A User Theorem |
| prepost-recover-main-same | avol0 = avol ⊦ [persistence_io_recover#(; adr, m, orphans, log, lpt, sb, n0, n1, n2, avol; err)] (err = ESUCCESS → avol0 = avol) | A User Theorem |
| prepost-write-lebs | ebm-vol-inv(avol), n + m ≤ # avol, # buf = m * LEB_SIZE, avol0 = avol ⊦ ⟪persistence_io_write_lebs#(n, m, buf, LEB_SIZE; avol; err)⟫ ( (err = ESUCCESS ∨ ⌊err⌋ ) ∧ # avol = # avol0 ∧ ebm-vol-inv(avol) ∧ range=(avol, 0, avol0, 0, n) ∧ range=(avol, n + m, avol0, n + m, # avol - n + m) ∧ (err = ESUCCESS → lebs(avol, n, m) = buf ∧ mapped-full?(avol, n, m))) | A User Theorem |
| prepost-write-orphans | n < # avol, ebm-vol-inv(avol), avol0 = avol, orphans0 = orphans ⊦ ⟪persistence_io_write_orphans#(n, EB_PAGE_SIZE, LEB_SIZE; orphans, avol; err)⟫ ( (err = ESUCCESS ∨ ⌊err⌋ ) ∧ ebm-vol-inv(avol) ∧ id○(avol, avol0, n) ∧ (err = ESUCCESS → avol[n].mapped? ∧ is-encoded-pad(orphans0, # orphans0, avol[n].data))) | A User Theorem |
| prepost-write-superblock | avol0 = avol, # avol ≠ 0, ebm-vol-inv(avol) ⊦ ⟪persistence_io_write_superblock#(sb, EB_PAGE_SIZE, LEB_SIZE; avol; err)⟫ ( (err = ESUCCESS ∨ ⌊err⌋ ) ∧ ebm-vol-inv(avol) ∧ (err = ESUCCESS → id○(avol, avol0, 0) ∧ (∃ buf. is-encoded(sb, buf) ∧ avol[0] = mapped(buf))) ∧ (err ≠ ESUCCESS → avol = avol0)) | A User Theorem |
| rangeeq-concrete-unfold | m ≠ 0 ⊦ range=(avol, (* n), avol0, (* n), (* m)) ↔ avol[n] = avol0[n] ∧ range=(avol, n + 1, avol0, n + 1, m - 1) | A User Theorem |
| rangeeq-lebs | ⊦ range=(avol, n, avol0, n, m + m0) → lebs(avol, n, m) = lebs(avol0, n, m) | A User Theorem |
| rangeeq-lebs-5 | n ≤ m0 ⊦ range=(avol, 0, avol0, 0, m + m0) → lebs(avol, m, n) = lebs(avol0, m, n) | A User Theorem |
| rangeeq-subarray | ⊦ range=(avol, 5 + n, avol0, 5 + n, n + m0) → subarray(avol, 5 + 2 * n, m0) = subarray(avol0, 5 + 2 * n, m0) | A User Theorem |
| rangeeq-subarray-5 | ⊦ range=(avol, 5 + n, avol0, 5 + n, m0) → subarray(avol, 5 + n, m0) = subarray(avol0, 5 + n, m0) | A User Theorem |
| rangeeq-till-leb5-fwd | m < 5 ⊦ range=(avol1, 0, avol0, 0, 5 + n) → avol1[(* m)] = avol0[m] | A User Theorem |
| rangeeq-write-right-concrete-below | n0 < n ⊦ range=(avol, (* n) + m, avol0[(* n0), aleb], (* n) + m, m1) ↔ range=(avol, n + m, avol0, n + m, m1) | A User Theorem |