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: |
|---|---|---|
| create-freelist | persistence_create_freelist#(LPT; FREELIST) {FREELIST := []; let N = 0 in while N < # LPT do {/* (prepost-create-freelist: invariant N ≤ # LPT ∧ freelist-cons(subarray(LPT, 0, N), FREELIST) wfbound # LPT - N) */; if LPT[N].flags = LP_FREE then FREELIST := FREELIST + N; N := N + 1} } | An Axiom |
| format | persistence_format# (VOLSIZE, SIZE, WMAXINO0; LPT, FREELIST, GCHEAP, WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, WBUFLEB, AROFS, LOG, LEBSIZE; ERR) {if SIZE = LEB_SIZE then {LPT := mklparray(VOLSIZE); LPT := fill(LPT, mklp(0, 0, LP_FREE, 0)); let ADR = @(0, 0, 0) in awbuf_format#(VOLSIZE, SIZE, LPT, ADR, WMAXINO0; ; WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, WBUFLEB, AROFS, ERR); if ERR ≠ ESUCCESS then debug#("persistence: wbuf format failed") else {awbuf_get_leb_size#(WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, WBUFLEB, AROFS; ; LEBSIZE); LOG := []; persistence_create_freelist#(LPT; FREELIST); gc_heap_empty#(; GCHEAP)}} else abort } | An Axiom |
| requires-commit | persistence_requires_commit#(WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, WBUFLEB, AROFS; ; COMMIT?) {awbuf_requires_commit#(WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, WBUFLEB, AROFS; ; COMMIT?)} | An Axiom |
| create-gcheap | persistence_create_gcheap#(LOG; LPT, GCHEAP) {gc_heap_empty#(; GCHEAP); let N = 0 in while N < # LPT do {/* (prepost-create-gcheap : invariant N ≤ # LPT ∧ bin-heap-inv(GCHEAP, LPT) ∧ gc-heap(LPT, LOG, N) = keyset(GCHEAP) ∧ id-idx(LPT`, LPT) wfbound # LPT - N) */; if LPT[N].flags = LP_GROUP_NODES ∧ ¬ N ∈ LOG then let KI = key-index(LPT[N].ref-size, N) in gc_heap_insert#(KI; GCHEAP, LPT); N := N + 1} } | An Axiom |
| replay-log | persistence_replay_log#(LEBSIZE; LOG0, LPT) {while LOG0 ≠ [] do {/* (prepost-replay-log : invariant ∃ log. LOG0` = log + LOG0 ∧ LPT = replay-log(LPT`, log) ∧ valid-indices(LPT, LOG0`) ∧ ¬ dups(LOG0`) wfbound # LOG0) */; let N = LOG0.head in {LPT[N].flags := LP_GROUP_NODES; LPT[N].size := LEBSIZE; LOG0 := LOG0.tail}} } | An Axiom |
| recover | persistence_recover# (; WROOTADR0, WMAXINO0, LOG0, ORPHANS, LOG, LPT, FREELIST, GCHEAP, LEBSIZE, WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, WBUFLEB, AROFS; ERR) {awbuf_recover#(; WROOTADR0, WMAXINO0, ORPHANS, LOG0, LPT, WROOTADR, WMAXINO, WLOG, WLPT, WORPHANS, WVOL; WBUFLEB, AROFS, ERR); LOG := LOG0; if ERR ≠ ESUCCESS then debug#("persistence: wbuf recover failed") else {awbuf_get_leb_size#(WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, WBUFLEB, AROFS; ; LEBSIZE); let LOG0 = LOG in persistence_replay_log#(LEBSIZE; LOG0, LPT); persistence_replay_lpt#(LOG, LEBSIZE, WROOTADR, WMAXINO, WLOG, WLPT, WORPHANS, WBUFLEB, AROFS; LPT, WVOL); persistence_create_freelist#(LPT; FREELIST); persistence_create_gcheap#(LOG; LPT, GCHEAP)} } | An Axiom |
| deallocate-gnd | persistence_deallocate_gnd#(N, LOG, WROOTADR, WMAXINO, WLOG, WLPT, WORPHANS, WBUFLEB, AROFS; LPT, FREELIST, GCHEAP, WVOL; ERR) {if synced(WVOL) ∧ N < # LPT ∧ LPT[N].flags = LP_GROUP_NODES ∧ ¬ N ∈ LOG then let AROFS0 = ? in {awbuf_is_readonly#(WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, WBUFLEB, AROFS; ; AROFS0); if AROFS0 then ERR := EROFS else {awbuf_unmap#(N, WROOTADR, WMAXINO, WLOG, WLPT, WORPHANS, WBUFLEB, AROFS; WVOL); LPT[N].flags := LP_FREE; LPT[N].ref-size := 0; LPT[N].size := 0; FREELIST := FREELIST + N; gc_heap_remove#(LPT[N].gcheapidx; GCHEAP, LPT); ERR := ESUCCESS}} else abort } | An Axiom |
| allocate-ind | persistence_allocate_ind#(WROOTADR, WMAXINO, WLOG, WLPT, WORPHANS, AROFS; LPT, FREELIST, WVOL, WBUFLEB; ERR) {if synced(WVOL) then let N = ? in {persistence_allocate_leb#(WROOTADR, WMAXINO, WLOG, WLPT, WORPHANS, WBUFLEB, AROFS; N, LPT, FREELIST, WVOL; ERR); if ERR = ESUCCESS then {awbuf_move_buf#(N, 0, WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, AROFS; WBUFLEB; ERR); if ERR ≠ ESUCCESS then FREELIST := N + FREELIST else LPT[N].flags := LP_INDEX_NODES}} else abort } | An Axiom |
| allocate-gnd | persistence_allocate_gnd#(WROOTADR, WMAXINO, WLPT, WORPHANS, AROFS; LOG, LPT, FREELIST, WLOG, WVOL, WBUFLEB; ERR) {if synced(WVOL) then let N = ? in {persistence_allocate_leb#(WROOTADR, WMAXINO, WLOG, WLPT, WORPHANS, WBUFLEB, AROFS; N, LPT, FREELIST, WVOL; ERR); if ERR = ESUCCESS then {awbuf_add_log_leb#(N, 0, WROOTADR, WMAXINO, WVOL, WLPT, WORPHANS, AROFS; WLOG, WBUFLEB; ERR); if ERR ≠ ESUCCESS then FREELIST := N + FREELIST}; if ERR = ESUCCESS then {LPT[N].flags := LP_GROUP_NODES; LOG := LOG + N}} else abort } | An Axiom |
| allocate-leb | persistence_allocate_leb#(WROOTADR, WMAXINO, WLOG, WLPT, WORPHANS, WBUFLEB, AROFS; N, LPT, FREELIST, WVOL; ERR) {let AROFS0 = ? in {awbuf_is_readonly#(WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, WBUFLEB, AROFS; ; AROFS0); if AROFS0 then ERR := EROFS else if FREELIST = [] then ERR := ENOSPC else {N := FREELIST.head; awbuf_remap#(N, WROOTADR, WMAXINO, WLOG, WLPT, WORPHANS, WBUFLEB, AROFS; WVOL; ERR); if ERR = ESUCCESS then {FREELIST := FREELIST.tail; LPT[N].size := 0; LPT[N].ref-size := 0}}} } | An Axiom |
| get-gc-block | persistence_get_gc_block#(GCHEAP; N; ERR) {let empty? = ? in {gc_heap_is_empty#(GCHEAP; empty?); if empty? then ERR := ENOSPC else {gc_heap_get_min#(GCHEAP; N); ERR := ESUCCESS}}} | An Axiom |
| get-gblock-refsize | persistence_get_gblock_refsize#(LNUM, LPT; ; N){if LNUM < # LPT ∧ LPT[LNUM].flags = LP_GROUP_NODES then N := LPT[LNUM].ref-size else abort} | An Axiom |
| set-gblock-refsize | persistence_set_gblock_refsize#(LNUM, N, LOG; LPT, GCHEAP) {if LNUM < # LPT ∧ LPT[LNUM].flags = LP_GROUP_NODES then {LPT[LNUM].ref-size := N; if ¬ LNUM ∈ LOG then gc_heap_update#(LPT[LNUM].gcheapidx, N; GCHEAP, LPT)} else abort } | An Axiom |
| get-iblock-refsize | persistence_get_iblock_refsize#(LNUM, LPT; ; N){if LNUM < # LPT ∧ LPT[LNUM].flags = LP_INDEX_NODES then N := LPT[LNUM].ref-size else abort} | An Axiom |
| set-iblock-refsize | persistence_set_iblock_refsize#(LNUM, N; LPT){if LNUM < # LPT ∧ LPT[LNUM].flags = LP_INDEX_NODES then LPT[LNUM].ref-size := N else abort} | An Axiom |
| heap-add-log | persistence_gc_heap_add_log#(; LOG, LPT, GCHEAP) {while LOG ≠ [] do {/* (prepost-gcheap-add-log : invariant bin-heap-inv(GCHEAP, LPT) ∧ keyset(GCHEAP) = gc-heap(LPT, LOG) ∧ id-idx(LPT`, LPT) ∧ ¬ dups(LOG) ∧ (∀ n. n ∈ LOG → n < # LPT ∧ LPT[n].flags = LP_GROUP_NODES) wfbound # LOG) */; let LNUM = LOG.head in let KI = key-index(LPT[LNUM].ref-size, LNUM) in gc_heap_insert#(KI; GCHEAP, LPT); LOG := LOG.tail} } | An Axiom |
| cleanup-lpt | persistence_cleanup_lpt#(WROOTADR, WMAXINO, WLOG, WLPT, WORPHANS, WBUFLEB, AROFS; LPT, FREELIST, GCHEAP, WVOL) {let N = 0 in while N < # LPT do {/* (prepost-cleanup-lpt : invariant N ≤ # LPT ∧ # LPT = # LPT` ∧ id-idx(cleanup-lpt(LPT`, N), LPT) ∧ awbuf-inv(WVOL, WBUFLEB) ∧ avol-cleanup-lpt-unchanged(WVOL`, WVOL, LPT`) ∧ freelist-cons(LPT, FREELIST) ∧ keyset(GCHEAP) = gc-heap(cleanup-lpt(LPT`, N), []) ∧ bin-heap-inv(GCHEAP, LPT) ∧ WBUFLEB = nobuffer ∧ synced(WVOL) wfbound # LPT - N) */; if LPT[N].ref-size = 0 ∧ LPT[N].flags ≠ LP_FREE then {if LPT[N].flags = LP_GROUP_NODES then gc_heap_remove#(LPT[N].gcheapidx; GCHEAP, LPT); LPT[N].flags := LP_FREE; LPT[N].size := 0; FREELIST := FREELIST + N; awbuf_unmap#(N, WROOTADR, WMAXINO, WLOG, WLPT, WORPHANS, WBUFLEB, AROFS; WVOL)}; N := N + 1} } | An Axiom |
| commit | persistence_commit#(WROOTADR0, WMAXINO0; ORPHANS0, LOG, LPT, FREELIST, GCHEAP, WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, WBUFLEB, AROFS; ERR) {if synced(WVOL) then {awbuf_destroy_buf#(WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, AROFS; WBUFLEB; ERR); if ERR = ESUCCESS then awbuf_commit#(LPT, WROOTADR0, WMAXINO0, WVOL, WBUFLEB; ORPHANS0, WROOTADR, WMAXINO, WLOG, WLPT, WORPHANS, AROFS; ERR); if ERR = ESUCCESS then {persistence_gc_heap_add_log#(; LOG, LPT, GCHEAP); persistence_cleanup_lpt#(WROOTADR, WMAXINO, WLOG, WLPT, WORPHANS, WBUFLEB, AROFS; LPT, FREELIST, GCHEAP, WVOL)}} else abort } | An Axiom |
| add-ind | persistence_add_ind#(IND, LEBSIZE, WROOTADR, WMAXINO, WLOG, WLPT, WORPHANS, WBUFLEB; ADR, LPT, WVOL, AROFS; ERR) {if ¬ AROFS → WBUFLEB.isbuf? ∧ WBUFLEB.leb < # LPT ∧ LPT[WBUFLEB.leb].flags = LP_INDEX_NODES ∧ WVOL[WBUFLEB.leb].mapped? ∧ (LPT[WBUFLEB.leb].size + IND.flashsize ≤ LEB_SIZE → LPT[WBUFLEB.leb].size = # WVOL[WBUFLEB.leb].data) then let AROFS0 = ? in {awbuf_is_readonly#(WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, WBUFLEB, AROFS; ; AROFS0); if AROFS0 then ERR := EROFS else let BUF = mkbuf(IND.flashsize), SIZE = ?, WBUFLEB0 = ? in {awbuf_get_buf#(WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, WBUFLEB, AROFS; ; WBUFLEB0); encode_index_node#(IND, 0; SIZE, BUF; ERR); if ERR = ESUCCESS then if ¬ LPT[WBUFLEB0.leb].size + SIZE ≤ LEBSIZE then {debug#("persistence: trying to write beyond LEB size"); awbuf_enter_readonly#(WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, WBUFLEB; ; AROFS); ERR := ENOSPC} else {awbuf_write_buf#(SIZE, BUF, WROOTADR, WMAXINO, WLOG, WLPT, WORPHANS, WBUFLEB; WVOL, AROFS; ERR); if ERR = ESUCCESS then {ADR := @(WBUFLEB0.leb, LPT[WBUFLEB0.leb].size, SIZE); LPT[WBUFLEB0.leb].size := LPT[WBUFLEB0.leb].size + SIZE} else LPT[WBUFLEB0.leb].size := LEBSIZE} else {debug#("persistence: could not encode index node"); awbuf_enter_readonly#(WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, WBUFLEB; ; AROFS)}}} else abort } | An Axiom |
| read-gnd | persistence_read_gnd#(ADR, WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, WBUFLEB, AROFS; GND; ERR) {if ADR.lnum < # WVOL ∧ WVOL[ADR.lnum].mapped? ∧ ADR.pos + ADR.size ≤ # WVOL[ADR.lnum].data ∧ (∃ gnd. abs-node(subarray(WVOL[ADR.lnum].data, ADR.pos, ADR.size), gnd)) then let BUF = mkbuf(ADR.size) in {awbuf_read_buf#(ADR.lnum, ADR.pos, ADR.size, WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, WBUFLEB, AROFS; BUF; ERR); if ERR = ESUCCESS then decode_group_node#(0, ADR.size, BUF; GND; ERR)} else abort } | An Axiom |
| read-ind | persistence_read_ind#(ADR, WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, WBUFLEB, AROFS; IND; ERR) {if ADR.lnum < # WVOL ∧ WVOL[ADR.lnum].mapped? ∧ ADR.pos + ADR.size ≤ # WVOL[ADR.lnum].data ∧ (∃ ind. abs-node(subarray(WVOL[ADR.lnum].data, ADR.pos, ADR.size), ind)) then let BUF = mkbuf(ADR.size) in {awbuf_read_buf#(ADR.lnum, ADR.pos, ADR.size, WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, WBUFLEB, AROFS; BUF; ERR); if ERR = ESUCCESS then decode_index_node#(0, ADR.size, BUF; IND; ERR)} else abort } | An Axiom |
| read-gblock-nodes | persistence_read_gblock_nodes#(LNUM, LEBSIZE, WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, WBUFLEB, AROFS; ADRLIST, NODELIST; ERR) {if LNUM < # WVOL ∧ WVOL[LNUM].mapped? ∧ (∃ gndx, lax. abs-nodes(WVOL[LNUM].data, gndx, lax, true)) then let BUF = mkbuf(LEBSIZE), OFFSET = 0 in {awbuf_read_buf#(LNUM, 0, LEBSIZE, WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, WBUFLEB, AROFS; BUF; ERR); while ERR = ESUCCESS ∧ OFFSET < LEBSIZE do {/* (inv-read-gblock-nodes : invariant (ERR = ESUCCESS ∨ ERR = ENOENT ∨ ⌊ERR⌋ ) ∧ ( ERR = ESUCCESS ∨ ERR = ENOENT → read-gblock-inv(LNUM, OFFSET, ADRLIST, NODELIST, ADRLIST`, NODELIST`, WVOL[LNUM].data, ERR = ENOENT)) wfbound (ERR ≠ ESUCCESS ⊃ 0;LEBSIZE - OFFSET)) */; if ¬ OFFSET + NODE_HEADER_SIZE ≤ # BUF ∨ isempty(BUF, OFFSET, NODE_HEADER_SIZE) then ERR := ENOENT else let NDHD = ? in {decode_header#(OFFSET, BUF; NDHD; ERR); if ERR ≠ ESUCCESS then debug# ("persistence: read_gblock_nodes could not decode header in LEB " + LNUM.toString + " at offset " + OFFSET.toString) else let SIZE = 2 * NODE_HEADER_SIZE + align↑(NDHD.size, 2 * NODE_HEADER_SIZE) in {if OFFSET + SIZE > LEBSIZE then {debug# ( "persistence: read_gblock_nodes ignoring node of size " + SIZE.toString + " at offset " + OFFSET.toString + " in LEB " + LNUM.toString); ERR := ENOENT} else if ¬ range= (BUF, OFFSET + NODE_HEADER_SIZE + align↑(NDHD.size, 2 * NODE_HEADER_SIZE), validtrailer, 0, NODE_HEADER_SIZE) then {ERR := ENOENT; debug# ("persistence: read_gblock_nodes partial node at offset " + OFFSET.toString + " in LEB " + LNUM.toString)} else if ¬ NDHD.ispadding then let GND = ? in {decode_group_node#(OFFSET, SIZE, BUF; GND; ERR); if ERR ≠ ESUCCESS then debug# ( "persistence: read_gblock_nodes could not decode node at offset " + OFFSET.toString + " in LEB " + LNUM.toString) else {NODELIST := NODELIST + GND; ADRLIST := ADRLIST + @(LNUM, OFFSET, SIZE)}}; if ERR = ESUCCESS then OFFSET := OFFSET + SIZE}}}; if ERR = ENOENT then ERR := ESUCCESS} else abort } | An Axiom |
| encode-padding-node | persistence_encode_padding_node#(; BUF; ERR) {let SIZE = # BUF - 2 * NODE_HEADER_SIZE in {encode_header#(nodeheader(SIZE, true), 0; BUF; ERR); BUF := copy(validtrailer, 0, BUF, # BUF - NODE_HEADER_SIZE, NODE_HEADER_SIZE)} } | An Axiom |
| replay-lpt | persistence_replay_lpt#(LOG, LEBSIZE, WROOTADR, WMAXINO, WLOG, WLPT, WORPHANS, WBUFLEB, AROFS; LPT, WVOL) {let N = 0 in while N < # LPT do {/* (prepost-replay-lpt : invariant N ≤ # LPT` ∧ awbuf-inv(WVOL, WBUFLEB) ∧ WBUFLEB = nobuffer ∧ LPT = replay-lpt(LPT`, LOG, N) ∧ # LPT` = # WVOL` ∧ avol-replay-lpt-unchanged(WVOL`, WVOL, LPT`, LOG) ∧ synced(WVOL) wfbound # LPT - N) */; if LPT[N].flags ≠ LP_FREE ∧ ¬ N ∈ LOG then {if LPT[N].flags = LP_INDEX_NODES then LPT[N].size := LEBSIZE; if LPT[N].ref-size = 0 then {LPT[N].flags := LP_FREE; LPT[N].size := 0; awbuf_unmap#(N, WROOTADR, WMAXINO, WLOG, WLPT, WORPHANS, WBUFLEB, AROFS; WVOL)}}; N := N + 1} } | An Axiom |
| encode-group-nodes | persistence_encode_group_nodes#(NODELIST, LNUM, N; ; BUF, ADRLIST, ERR) {ERR := ESUCCESS; BUF := mkbuf(NODELIST.flashsize); ADRLIST := []; let IDX = 0, OFFSET = 0 in while ERR = ESUCCESS ∧ IDX < # NODELIST do {/* (prepost-encode-group-nodes : invariant IDX ≤ # NODELIST ∧ (ERR = ESUCCESS ∨ ⌊ERR⌋ ) ∧ ( ERR = ESUCCESS → # BUF = # BUF` ∧ (∃ gndx0, gndx1. NODELIST = gndx0 + gndx1 ∧ # gndx0 = IDX ∧ OFFSET = gndx0.flashsize ∧ (∃ lax, buf0, buf1. lax.to-adr(LNUM) = ADRLIST ∧ BUF = buf0 + buf1 ∧ # buf0 = OFFSET ∧ abs-nodes(buf0, N, gndx0, lax, false)))) wfbound # NODELIST - IDX) */; let SIZE = ? in {encode_group_node#(NODELIST[IDX], OFFSET; SIZE, BUF; ERR); ADRLIST := ADRLIST + @(LNUM, N + OFFSET, SIZE); OFFSET := OFFSET + SIZE}; IDX := IDX + 1} } | An Axiom |
| add-gnds | persistence_add_gnds#(NODELIST, LOG, LEBSIZE, WROOTADR, WMAXINO, WLOG, WLPT, WORPHANS, WBUFLEB; ADRLIST, LPT, WVOL, AROFS; ERR) {if ¬ AROFS → WBUFLEB.isbuf? ∧ WBUFLEB.leb < # LPT ∧ LPT[WBUFLEB.leb].flags = LP_GROUP_NODES ∧ WBUFLEB.leb ∈ LOG ∧ WVOL[WBUFLEB.leb].mapped? ∧ (NODELIST ≠ [] ∧ LPT[WBUFLEB.leb].size + NODELIST.flashsize ≤ LEB_SIZE → LPT[WBUFLEB.leb].size = # WVOL[WBUFLEB.leb].data) then let AROFS0 = ? in {awbuf_is_readonly#(WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, WBUFLEB, AROFS; ; AROFS0); if AROFS0 then ERR := EROFS else if NODELIST = [] then {ADRLIST := []; ERR := ESUCCESS} else let BUF = ?, WBUFLEB0 = ? in {awbuf_get_buf#(WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, WBUFLEB, AROFS; ; WBUFLEB0); persistence_encode_group_nodes#(NODELIST, WBUFLEB0.leb, LPT[WBUFLEB0.leb].size; ; BUF, ADRLIST, ERR); if ERR = ESUCCESS then if ¬ LPT[WBUFLEB0.leb].size + # BUF ≤ LEBSIZE then {debug#("persistence: trying to write beyond LEB size"); awbuf_enter_readonly#(WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, WBUFLEB; ; AROFS); ERR := ENOSPC} else {awbuf_write_buf#(# BUF, BUF, WROOTADR, WMAXINO, WLOG, WLPT, WORPHANS, WBUFLEB; WVOL, AROFS; ERR); if ERR = ESUCCESS then LPT[WBUFLEB0.leb].size := LPT[WBUFLEB0.leb].size + # BUF else {debug#("persistence: adding group node to LEB " + WBUFLEB0.leb.toString + " failed"); LPT[WBUFLEB0.leb].size := LEBSIZE}} else {debug#("persistence: could not encode group node"); awbuf_enter_readonly#(WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, WBUFLEB; ; AROFS)}}} else abort } | An Axiom |
| sync | persistence_sync#(LEBSIZE, WROOTADR, WMAXINO, WLOG, WLPT, WORPHANS, WBUFLEB; LPT, WVOL, AROFS; ERR) {if WBUFLEB.isbuf? ∧ ¬ AROFS → WBUFLEB.leb < # LPT ∧ LPT[WBUFLEB.leb].size ≤ LEB_SIZE ∧ WVOL[WBUFLEB.leb].mapped? ∧ LPT[WBUFLEB.leb].size = # WVOL[WBUFLEB.leb].data ∧ LPT[WBUFLEB.leb].flags ≠ LP_FREE ∧ is-aligned(LPT[WBUFLEB.leb].size, 2 * NODE_HEADER_SIZE) then {ERR := ESUCCESS; let WBUFLEB0 = ?, AROFS0 = ?, PAGESIZE = ? in {awbuf_get_buf#(WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, WBUFLEB, AROFS; ; WBUFLEB0); awbuf_is_readonly#(WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, WBUFLEB, AROFS; ; AROFS0); awbuf_get_page_size#(WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, WBUFLEB, AROFS; ; PAGESIZE); if ¬ AROFS0 then if WBUFLEB0.isbuf? then let OFFSET = LPT[WBUFLEB0.leb].size in if ¬ is-aligned(OFFSET, PAGESIZE) then let SIZE = PAGESIZE - OFFSET % PAGESIZE in let BUF = mkbuf(SIZE) in {persistence_encode_padding_node#(; BUF; ERR); if ERR = ESUCCESS then {awbuf_write_buf#(# BUF, BUF, WROOTADR, WMAXINO, WLOG, WLPT, WORPHANS, WBUFLEB; WVOL, AROFS; ERR); if ERR = ESUCCESS then LPT[WBUFLEB0.leb].size := LPT[WBUFLEB0.leb].size + SIZE else {debug#("persistence: flushing of LEB " + WBUFLEB0.leb.toString + " failed"); LPT[WBUFLEB0.leb].size := LEBSIZE; awbuf_enter_readonly#(WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, WBUFLEB; ; AROFS)}} else {debug#("persistence: could not encode padding node"); awbuf_enter_readonly#(WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, WBUFLEB; ; AROFS)}} else ERR := EROFS}} else abort } | An Axiom |
| get-block-free-size | persistence_get_block_free_size#(LPT, LEBSIZE, WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, WBUFLEB, AROFS; ; N) {let WBUFLEB0 = ? in {awbuf_get_buf#(WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, WBUFLEB, AROFS; ; WBUFLEB0); if WBUFLEB0 = nobuffer then N := 0 else N := LEBSIZE - LPT[WBUFLEB0.leb].size} } | An Axiom |
| is-log-empty | persistence_is_log_empty#(LOG; ; EMPTY?){EMPTY? := LOG = []} | An Axiom |
| is-readonly | persistence_is_readonly#(WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, WBUFLEB, AROFS; ; ROFS) {awbuf_is_readonly#(WROOTADR, WMAXINO, WLOG, WVOL, WLPT, WORPHANS, WBUFLEB, AROFS; ; ROFS)} | An Axiom |
| get-leb-size | persistence_get_leb_size#(LEBSIZE; ; N){N := LEBSIZE} | An Axiom |
| inv-read-gblock-nodes | lpt-free-unref(lpt), log = log0, bufs-log-only(bleb, log, lpt0), # lpt0 = # avol, buf-ro-rw-mode(isbuf, bleb, lpt0, avol), lpt-leb-size(lpt), lpt-ram-flash(lpt0, lpt, log), m = LEB_SIZE, awbuf-inv(avol, bleb), # lpt = # avol, m0 < # avol, avol[m0].mapped?, ∃ gndx, lax. abs-nodes(avol[m0].data, gndx, lax, true), ax = ax0, gndx0 = gndx1 ⊦ ⟪persistence_read_gblock_nodes#(m0, m, adr, m1, log0, avol, lpt, ns, bleb, isbuf; ax0, gndx1; err)⟫ ( (err = ESUCCESS ∨ ⌊err⌋ ) ∧ (err = ESUCCESS → (∃ lax, gndx. ax0 = ax + lax.to-adr(m0) ∧ gndx1 = gndx0 + gndx ∧ abs-nodes(avol[m0].data, gndx, lax, true)))) | A Proof Obligation |
| inv-add-ind | lpt-free-unref(lpt), lpt-free-unref(lpt0), freelist-cons(lpt, freelist), log = log0, bin-heap-inv(gch, lpt), keyset(gch) = gc-heap(lpt, log), bufs-log-only(bleb, log, lpt), # lpt = # avol, log-group-block(log, lpt), buf-ro-rw-mode(isbuf, bleb, lpt, avol), lpt-leb-size(lpt), lpt-leb-size(lpt0), lpt-ram-flash(lpt, lpt0, log), m = LEB_SIZE, awbuf-inv(avol, bleb), # lpt0 = # avol, ¬ isbuf → bleb.isbuf? ∧ bleb.leb < # lpt ∧ lpt[bleb.leb].flags = LP_INDEX_NODES ∧ avol[bleb.leb].mapped? ∧ (lpt[bleb.leb].size + ind.flashsize ≤ LEB_SIZE → lpt[bleb.leb].size = # avol[bleb.leb].data) ⊦ ⟪persistence_add_ind#(ind, m, adr, m0, log0, lpt0, ns, bleb; adr0, lpt, avol, isbuf; err)⟫ ( lpt-free-unref(lpt) ∧ freelist-cons(lpt, freelist) ∧ bin-heap-inv(gch, lpt) ∧ keyset(gch) = gc-heap(lpt, log) ∧ bufs-log-only(bleb, log, lpt) ∧ # lpt = # avol ∧ log-group-block(log, lpt) ∧ buf-ro-rw-mode(isbuf, bleb, lpt, avol) ∧ lpt-leb-size(lpt) ∧ lpt-ram-flash(lpt, lpt0, log) ∧ awbuf-inv(avol, bleb) ∧ # lpt0 = # avol) | A Proof Obligation |
| inv-format | m = LEB_SIZE ⊦ ⟪persistence_format#(m0, m, m1; lpt, freelist, gch, adr, m2, log, avol, lpt0, ns, bleb, isbuf, log0, m3; err)⟫ ( err = ESUCCESS → synced(avol) ∧ lpt-free-unref(lpt) ∧ lpt-free-unref(lpt0) ∧ freelist-cons(lpt, freelist) ∧ log0 = log ∧ bin-heap-inv(gch, lpt) ∧ keyset(gch) = gc-heap(lpt, log0) ∧ bufs-log-only(bleb, log0, lpt) ∧ # lpt = # avol ∧ ¬ dups(log0) ∧ log-group-block(log0, lpt) ∧ buf-ro-rw-mode(isbuf, bleb, lpt, avol) ∧ lpt-leb-size(lpt) ∧ lpt-leb-size(lpt0) ∧ lpt-ram-flash(lpt, lpt0, log0) ∧ m3 = LEB_SIZE ∧ awbuf-inv(avol, bleb) ∧ # lpt0 = # avol) | A Proof Obligation |
| inv-requires-commit | lpt-free-unref(lpt), log = log0, bufs-log-only(bleb, log, lpt0), # lpt0 = # avol, buf-ro-rw-mode(isbuf, bleb, lpt0, avol), lpt-leb-size(lpt), lpt-ram-flash(lpt0, lpt, log), awbuf-inv(avol, bleb), # lpt = # avol ⊦ ⟪persistence_requires_commit#(adr, m, log0, avol, lpt, ns, bleb, isbuf; ; isbuf0)⟫ true | A Proof Obligation |
| inv-deallocate-gnd | lpt-free-unref(lpt), lpt-free-unref(lpt0), freelist-cons(lpt, freelist), log = log0, bin-heap-inv(gch, lpt), keyset(gch) = gc-heap(lpt, log), bufs-log-only(bleb, log, lpt), # lpt = # avol, ¬ dups(log), log-group-block(log, lpt), buf-ro-rw-mode(isbuf, bleb, lpt, avol), lpt-leb-size(lpt), lpt-leb-size(lpt0), lpt-ram-flash(lpt, lpt0, log), awbuf-inv(avol, bleb), # lpt0 = # avol, synced(avol), n < # lpt, lpt[n].flags = LP_GROUP_NODES, ¬ n ∈ log ⊦ ⟪persistence_deallocate_gnd#(n, log, adr, m, log0, lpt0, ns, bleb, isbuf; lpt, freelist, gch, avol; err)⟫ ( lpt-free-unref(lpt) ∧ freelist-cons(lpt, freelist) ∧ bin-heap-inv(gch, lpt) ∧ keyset(gch) = gc-heap(lpt, log) ∧ bufs-log-only(bleb, log, lpt) ∧ # lpt = # avol ∧ log-group-block(log, lpt) ∧ buf-ro-rw-mode(isbuf, bleb, lpt, avol) ∧ lpt-leb-size(lpt) ∧ lpt-ram-flash(lpt, lpt0, log) ∧ awbuf-inv(avol, bleb) ∧ # lpt0 = # avol) | A Proof Obligation |
| inv-allocate-ind | lpt-free-unref(lpt), lpt-free-unref(lpt0), freelist-cons(lpt, freelist), log = log0, bin-heap-inv(gch, lpt), keyset(gch) = gc-heap(lpt, log), bufs-log-only(bleb, log, lpt), # lpt = # avol, log-group-block(log, lpt), buf-ro-rw-mode(isbuf, bleb, lpt, avol), lpt-leb-size(lpt), lpt-leb-size(lpt0), lpt-ram-flash(lpt, lpt0, log), awbuf-inv(avol, bleb), # lpt0 = # avol, synced(avol) ⊦ ⟪persistence_allocate_ind#(adr, m, log0, lpt0, ns, isbuf; lpt, freelist, avol, bleb; err)⟫ ( lpt-free-unref(lpt) ∧ freelist-cons(lpt, freelist) ∧ bin-heap-inv(gch, lpt) ∧ keyset(gch) = gc-heap(lpt, log) ∧ bufs-log-only(bleb, log, lpt) ∧ # lpt = # avol ∧ log-group-block(log, lpt) ∧ buf-ro-rw-mode(isbuf, bleb, lpt, avol) ∧ lpt-leb-size(lpt) ∧ lpt-ram-flash(lpt, lpt0, log) ∧ awbuf-inv(avol, bleb) ∧ # lpt0 = # avol) | A Proof Obligation |
| inv-allocate-gnd | lpt-free-unref(lpt), lpt-free-unref(lpt0), freelist-cons(lpt, freelist), log = log0, bin-heap-inv(gch, lpt), keyset(gch) = gc-heap(lpt, log), bufs-log-only(bleb, log, lpt), # lpt = # avol, ¬ dups(log), log-group-block(log, lpt), buf-ro-rw-mode(isbuf, bleb, lpt, avol), lpt-leb-size(lpt), lpt-leb-size(lpt0), lpt-ram-flash(lpt, lpt0, log), awbuf-inv(avol, bleb), # lpt0 = # avol, synced(avol) ⊦ ⟪persistence_allocate_gnd#(adr, m, lpt0, ns, isbuf; log, lpt, freelist, log0, avol, bleb; err)⟫ ( lpt-free-unref(lpt) ∧ freelist-cons(lpt, freelist) ∧ log = log0 ∧ bin-heap-inv(gch, lpt) ∧ keyset(gch) = gc-heap(lpt, log) ∧ bufs-log-only(bleb, log, lpt) ∧ # lpt = # avol ∧ ¬ dups(log) ∧ log-group-block(log, lpt) ∧ buf-ro-rw-mode(isbuf, bleb, lpt, avol) ∧ lpt-leb-size(lpt) ∧ lpt-ram-flash(lpt, lpt0, log) ∧ awbuf-inv(avol, bleb) ∧ # lpt0 = # avol) | A Proof Obligation |
| inv-get-gc-block | lpt-free-unref(lpt), freelist-cons(lpt, freelist), log = log0, bin-heap-inv(gch, lpt), keyset(gch) = gc-heap(lpt, log), bufs-log-only(bleb, log, lpt), # lpt = # avol, ¬ dups(log), log-group-block(log, lpt), buf-ro-rw-mode(isbuf, bleb, lpt, avol), lpt-leb-size(lpt), lpt-ram-flash(lpt, lpt0, log), n = n0 ⊦ ⟪persistence_get_gc_block#(gch; n0; err)⟫ ((err = ENOSPC ∨ err = ESUCCESS) ∧ (err ≠ ESUCCESS → n0 = n) ∧ (err = ESUCCESS → n0 < # lpt ∧ lpt[n0].flags = LP_GROUP_NODES ∧ ¬ n0 ∈ log)) | A Proof Obligation |
| inv-get-gblock-refsize | lpt-free-unref(lpt), freelist-cons(lpt, freelist), bin-heap-inv(gch, lpt), keyset(gch) = gc-heap(lpt, log), bufs-log-only(bleb, log, lpt), # lpt = # avol, log-group-block(log, lpt), buf-ro-rw-mode(isbuf, bleb, lpt, avol), lpt-leb-size(lpt), lpt-ram-flash(lpt, lpt0, log), m < # lpt, lpt[m].flags = LP_GROUP_NODES ⊦ ⟪persistence_get_gblock_refsize#(m, lpt; ; n)⟫ true | A Proof Obligation |
| inv-set-gblock-refsize | lpt-free-unref(lpt), freelist-cons(lpt, freelist), log = log0, bin-heap-inv(gch, lpt), keyset(gch) = gc-heap(lpt, log), bufs-log-only(bleb, log, lpt), # lpt = # avol, ¬ dups(log), log-group-block(log, lpt), buf-ro-rw-mode(isbuf, bleb, lpt, avol), lpt-leb-size(lpt), lpt-ram-flash(lpt, lpt0, log), m < # lpt, lpt[m].flags = LP_GROUP_NODES ⊦ ⟪persistence_set_gblock_refsize#(m, n, log; lpt, gch)⟫ ( lpt-free-unref(lpt) ∧ freelist-cons(lpt, freelist) ∧ bin-heap-inv(gch, lpt) ∧ keyset(gch) = gc-heap(lpt, log) ∧ bufs-log-only(bleb, log, lpt) ∧ # lpt = # avol ∧ log-group-block(log, lpt) ∧ buf-ro-rw-mode(isbuf, bleb, lpt, avol) ∧ lpt-leb-size(lpt) ∧ lpt-ram-flash(lpt, lpt0, log)) | A Proof Obligation |
| inv-get-iblock-refsize | lpt-free-unref(lpt), freelist-cons(lpt, freelist), bin-heap-inv(gch, lpt), keyset(gch) = gc-heap(lpt, log), bufs-log-only(bleb, log, lpt), # lpt = # avol, log-group-block(log, lpt), buf-ro-rw-mode(isbuf, bleb, lpt, avol), lpt-leb-size(lpt), lpt-ram-flash(lpt, lpt0, log), m < # lpt, lpt[m].flags = LP_INDEX_NODES ⊦ ⟪persistence_get_iblock_refsize#(m, lpt; ; n)⟫ true | A Proof Obligation |
| inv-set-iblock-refsize | lpt-free-unref(lpt), freelist-cons(lpt, freelist), bin-heap-inv(gch, lpt), keyset(gch) = gc-heap(lpt, log), bufs-log-only(bleb, log, lpt), # lpt = # avol, log-group-block(log, lpt), buf-ro-rw-mode(isbuf, bleb, lpt, avol), lpt-leb-size(lpt), lpt-ram-flash(lpt, lpt0, log), m < # lpt, lpt[m].flags = LP_INDEX_NODES ⊦ ⟪persistence_set_iblock_refsize#(m, n; lpt)⟫ ( lpt-free-unref(lpt) ∧ freelist-cons(lpt, freelist) ∧ bin-heap-inv(gch, lpt) ∧ keyset(gch) = gc-heap(lpt, log) ∧ bufs-log-only(bleb, log, lpt) ∧ # lpt = # avol ∧ log-group-block(log, lpt) ∧ buf-ro-rw-mode(isbuf, bleb, lpt, avol) ∧ lpt-leb-size(lpt) ∧ lpt-ram-flash(lpt, lpt0, log)) | A Proof Obligation |
| inv-recover | adr = adr0, m = m0, log = log0, lpt = lpt0, avol ↓ avol0, ns = ns0, synced(avol0), lpt-free-unref(lpt1), lpt-free-unref(lpt0), freelist-cons(lpt1, log1), log2 = log0, bin-heap-inv(gch, lpt1), keyset(gch) = gc-heap(lpt1, log2), bufs-log-only(bleb, log2, lpt1), # lpt1 = # avol0, ¬ dups(log2), log-group-block(log2, lpt1), buf-ro-rw-mode(isbuf, bleb, lpt1, avol0), lpt-leb-size(lpt1), lpt-leb-size(lpt0), lpt-ram-flash(lpt1, lpt0, log2), m1 = LEB_SIZE, awbuf-inv(avol0, bleb), # lpt0 = # avol0 ⊦ ⟪persistence_recover#(; adr1, m2, log3, ns1, log4, lpt2, freelist, gch0, m3, adr, m, log, avol, lpt, ns, bleb0, isbuf0; err)⟫ ( ( err = ESUCCESS → synced(avol) ∧ lpt-free-unref(lpt2) ∧ lpt-free-unref(lpt) ∧ freelist-cons(lpt2, freelist) ∧ log4 = log ∧ bin-heap-inv(gch0, lpt2) ∧ keyset(gch0) = gc-heap(lpt2, log4) ∧ bufs-log-only(bleb0, log4, lpt2) ∧ # lpt2 = # avol ∧ ¬ dups(log4) ∧ log-group-block(log4, lpt2) ∧ buf-ro-rw-mode(isbuf0, bleb0, lpt2, avol) ∧ lpt-leb-size(lpt2) ∧ lpt-leb-size(lpt) ∧ lpt-ram-flash(lpt2, lpt, log4) ∧ m3 = LEB_SIZE ∧ awbuf-inv(avol, bleb0) ∧ # lpt = # avol) ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ ( err = ESUCCESS → # avol = # avol0 ∧ adr1 = adr ∧ adr = adr0 ∧ m2 = m ∧ m = m0 ∧ log3 = log ∧ log = log0 ∧ ns1 = ns ∧ ns = ns0 ∧ lpt = lpt0 ∧ bleb0 = nobuffer ∧ id-idx(replay-lpt(replay-log(lpt, log), log, # lpt), lpt2))) | A Proof Obligation |
| inv-commit | lpt-free-unref(lpt), lpt-free-unref(lpt0), freelist-cons(lpt, freelist), log = log0, bin-heap-inv(gch, lpt), keyset(gch) = gc-heap(lpt, log), bufs-log-only(bleb, log, lpt), # lpt = # avol, ¬ dups(log), log-group-block(log, lpt), buf-ro-rw-mode(isbuf, bleb, lpt, avol), lpt-leb-size(lpt), lpt-leb-size(lpt0), lpt-ram-flash(lpt, lpt0, log), awbuf-inv(avol, bleb), # lpt0 = # avol, synced(avol) ⊦ ⟪persistence_commit#(adr, m; ns, log, lpt, freelist, gch, adr0, m0, log0, avol, lpt0, ns0, bleb, isbuf; err)⟫ ( lpt-free-unref(lpt) ∧ lpt-free-unref(lpt0) ∧ freelist-cons(lpt, freelist) ∧ log = log0 ∧ bin-heap-inv(gch, lpt) ∧ keyset(gch) = gc-heap(lpt, log) ∧ bufs-log-only(bleb, log, lpt) ∧ # lpt = # avol ∧ ¬ dups(log) ∧ log-group-block(log, lpt) ∧ buf-ro-rw-mode(isbuf, bleb, lpt, avol) ∧ lpt-leb-size(lpt) ∧ lpt-leb-size(lpt0) ∧ lpt-ram-flash(lpt, lpt0, log) ∧ awbuf-inv(avol, bleb) ∧ # lpt0 = # avol ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ (err = ESUCCESS → bleb = nobuffer) ∧ (err = ESUCCESS ↔ ¬ isbuf)) | A Proof Obligation |
| inv-read-gnd | lpt-free-unref(lpt), log = log0, bufs-log-only(bleb, log, lpt0), # lpt0 = # avol, buf-ro-rw-mode(isbuf, bleb, lpt0, avol), lpt-leb-size(lpt), lpt-ram-flash(lpt0, lpt, log), awbuf-inv(avol, bleb), # lpt = # avol, adr.lnum < # avol, avol[adr.lnum].mapped?, adr.pos + adr.size ≤ # avol[adr.lnum].data, ∃ gnd. abs-node(subarray(avol[adr.lnum].data, adr.pos, adr.size), gnd) ⊦ ⟪persistence_read_gnd#(adr, adr0, m, log0, avol, lpt, ns, bleb, isbuf; gnd0; err)⟫ ((err = ESUCCESS ∨ ⌊err⌋ ) ∧ (err = ESUCCESS → abs-node(subarray(avol[adr.lnum].data, adr.pos, adr.size), gnd0))) | A Proof Obligation |
| inv-read-ind | lpt-free-unref(lpt), log = log0, bufs-log-only(bleb, log, lpt0), # lpt0 = # avol, buf-ro-rw-mode(isbuf, bleb, lpt0, avol), lpt-leb-size(lpt), lpt-ram-flash(lpt0, lpt, log), awbuf-inv(avol, bleb), # lpt = # avol, adr.lnum < # avol, avol[adr.lnum].mapped?, adr.pos + adr.size ≤ # avol[adr.lnum].data, ∃ ind. abs-node(subarray(avol[adr.lnum].data, adr.pos, adr.size), ind) ⊦ ⟪persistence_read_ind#(adr, adr0, m, log0, avol, lpt, ns, bleb, isbuf; ind0; err)⟫ ((err = ESUCCESS ∨ ⌊err⌋ ) ∧ (err = ESUCCESS → abs-node(subarray(avol[adr.lnum].data, adr.pos, adr.size), ind0))) | A Proof Obligation |
| inv-add-gnds | lpt-free-unref(lpt), lpt-free-unref(lpt0), freelist-cons(lpt, freelist), log = log0, bin-heap-inv(gch, lpt), keyset(gch) = gc-heap(lpt, log), bufs-log-only(bleb, log, lpt), # lpt = # avol, ¬ dups(log), log-group-block(log, lpt), buf-ro-rw-mode(isbuf, bleb, lpt, avol), lpt-leb-size(lpt), lpt-leb-size(lpt0), lpt-ram-flash(lpt, lpt0, log), m = LEB_SIZE, awbuf-inv(avol, bleb), # lpt0 = # avol, ¬ isbuf → bleb.isbuf? ∧ bleb.leb < # lpt ∧ lpt[bleb.leb].flags = LP_GROUP_NODES ∧ bleb.leb ∈ log ∧ avol[bleb.leb].mapped? ∧ (gndx ≠ [] ∧ lpt[bleb.leb].size + gndx.flashsize ≤ LEB_SIZE → lpt[bleb.leb].size = # avol[bleb.leb].data) ⊦ ⟪persistence_add_gnds#(gndx, log, m, adr, m0, log0, lpt0, ns, bleb; ax, lpt, avol, isbuf; err)⟫ ( lpt-free-unref(lpt) ∧ freelist-cons(lpt, freelist) ∧ bin-heap-inv(gch, lpt) ∧ keyset(gch) = gc-heap(lpt, log) ∧ bufs-log-only(bleb, log, lpt) ∧ # lpt = # avol ∧ log-group-block(log, lpt) ∧ buf-ro-rw-mode(isbuf, bleb, lpt, avol) ∧ lpt-leb-size(lpt) ∧ lpt-ram-flash(lpt, lpt0, log) ∧ awbuf-inv(avol, bleb) ∧ # lpt0 = # avol) | A Proof Obligation |
| inv-sync | lpt-free-unref(lpt), lpt-free-unref(lpt0), freelist-cons(lpt, freelist), log = log0, bin-heap-inv(gch, lpt), keyset(gch) = gc-heap(lpt, log), bufs-log-only(bleb, log, lpt), # lpt = # avol, log-group-block(log, lpt), buf-ro-rw-mode(isbuf, bleb, lpt, avol), lpt-leb-size(lpt), lpt-leb-size(lpt0), lpt-ram-flash(lpt, lpt0, log), m = LEB_SIZE, awbuf-inv(avol, bleb), # lpt0 = # avol, bleb.isbuf? ∧ ¬ isbuf → bleb.leb < # lpt ∧ lpt[bleb.leb].size ≤ LEB_SIZE ∧ avol[bleb.leb].mapped? ∧ lpt[bleb.leb].size = # avol[bleb.leb].data ∧ lpt[bleb.leb].flags ≠ LP_FREE ∧ is-aligned(lpt[bleb.leb].size, 2 * NODE_HEADER_SIZE) ⊦ ⟪persistence_sync#(m, adr, m0, log0, lpt0, ns, bleb; lpt, avol, isbuf; err)⟫ ( lpt-free-unref(lpt) ∧ freelist-cons(lpt, freelist) ∧ bin-heap-inv(gch, lpt) ∧ keyset(gch) = gc-heap(lpt, log) ∧ bufs-log-only(bleb, log, lpt) ∧ # lpt = # avol ∧ log-group-block(log, lpt) ∧ buf-ro-rw-mode(isbuf, bleb, lpt, avol) ∧ lpt-leb-size(lpt) ∧ lpt-ram-flash(lpt, lpt0, log) ∧ awbuf-inv(avol, bleb) ∧ # lpt0 = # avol) | A Proof Obligation |
| inv-get-block-free-size | lpt-free-unref(lpt), lpt-free-unref(lpt0), freelist-cons(lpt, freelist), log = log0, bin-heap-inv(gch, lpt), keyset(gch) = gc-heap(lpt, log), bufs-log-only(bleb, log, lpt), # lpt = # avol, log-group-block(log, lpt), buf-ro-rw-mode(isbuf, bleb, lpt, avol), lpt-leb-size(lpt), lpt-leb-size(lpt0), lpt-ram-flash(lpt, lpt0, log), m = LEB_SIZE, awbuf-inv(avol, bleb), # lpt0 = # avol ⊦ ⟪persistence_get_block_free_size#(lpt, m, adr, m0, log0, avol, lpt0, ns, bleb, isbuf; ; n)⟫ true | A Proof Obligation |
| inv-is-log-empty | log = log0, keyset(gch) = gc-heap(lpt, log), bufs-log-only(bleb, log, lpt), ¬ dups(log), log-group-block(log, lpt), lpt-ram-flash(lpt, lpt0, log) ⊦ ⟪persistence_is_log_empty#(log; ; empty?)⟫ true | A Proof Obligation |
| inv-is-readonly | lpt-free-unref(lpt), log = log0, bufs-log-only(bleb, log, lpt0), # lpt0 = # avol, buf-ro-rw-mode(isbuf, bleb, lpt0, avol), lpt-leb-size(lpt), lpt-ram-flash(lpt0, lpt, log), awbuf-inv(avol, bleb), # lpt = # avol ⊦ ⟪persistence_is_readonly#(adr, m, log0, avol, lpt, ns, bleb, isbuf; ; isbuf0)⟫ true | A Proof Obligation |
| inv-get-leb-size | m = LEB_SIZE ⊦ ⟪persistence_get_leb_size#(m; ; n)⟫ true | A Proof Obligation |
| adrlist-append-eq-size | # lax0 = # lax2 + 1 ⊦ lax0 + lax1 = lax2 + ladr ' ↔ ¬ ¬(lax1 = [] ∧ lax0 = lax2 + ladr ') | A User Theorem |
| adrlist-append-eq-size1 | ⊦ # lax2 + 1 < # lax0 → lax0 + lax1 ≠ lax2 + ladr ' | A User Theorem |
| elim-lp-upd-size | ⊦ lp.size:= n = mklp(lp.ref-size, n, lp.flags, lp.gcheapidx) | A User Theorem |
| elim-mapped | ⊦ avol[n].mapped? ↔ (∃ buf. avol[n] = mapped(buf)) | A User Theorem |
| flush-padding-space-aligned | ⊦ EB_PAGE_SIZE = n + m % EB_PAGE_SIZE ∧ is-aligned(m, 2 * NODE_HEADER_SIZE) → is-aligned(n, 2 * NODE_HEADER_SIZE) | A User Theorem |
| flush-padding-space-header | ⊦ EB_PAGE_SIZE = n + m % EB_PAGE_SIZE ∧ is-aligned(m, 2 * NODE_HEADER_SIZE) ∧ ¬ is-aligned(m, EB_PAGE_SIZE) → (2 * NODE_HEADER_SIZE ≤ n ↔ n ≠ 0) | A User Theorem |
| flush-padding-space-write | ⊦ n < # avol ∧ avol[n] = mapped(buf0) ∧ awbuf-inv(avol, bleb) ∧ EB_PAGE_SIZE = # buf1 + # buf0 % EB_PAGE_SIZE ∧ ¬ is-aligned(# buf0, EB_PAGE_SIZE) → ¬ LEB_SIZE < # buf0 + # buf1 | A User Theorem |
| id-idx-cleanup-lpt-backwards-fwd | n < # lpt0 ⊦ id-idx(cleanup-lpt(lpt0, n), lpt1) ∧ lpt0[n] = mklp(m0, m1, lpf0, m2) ∧ lpt1[n] = mklp(n0, n1, lpf1, n2) → m0 = n0 ∧ m1 = n1 ∧ lpf0 = lpf1 | A User Theorem |
| isprefix-size | ⊦ lax0 ⊑ lax2 + lax ∧ # lax = # gndx → ¬ # lax2 + # gndx < # lax0 | A User Theorem |
| nat-stuff0 | ⊦ n = n0 + n1 → (n0 < n ↔ n1 ≠ 0) | A User Theorem |
| prepost-cleanup-lpt | lpt0 = lpt, avol0 = avol, # avol = # lpt, awbuf-inv(avol, nobuffer), freelist-cons(lpt, freelist), bin-heap-inv(gch, lpt), keyset(gch) = gc-heap(lpt, []), synced(avol) ⊦ ⟪persistence_cleanup_lpt#(adr, m0, log, lpt1, ns, nobuffer, boolvar; lpt, freelist, gch, avol)⟫ ( id-idx(cleanup-lpt(lpt0), lpt) ∧ avol-cleanup-lpt-unchanged(avol0, avol, lpt0) ∧ freelist-cons(lpt, freelist) ∧ awbuf-inv(avol, nobuffer) ∧ bin-heap-inv(gch, lpt) ∧ keyset(gch) = gc-heap(lpt, []) ∧ synced(avol)) | A User Theorem |
| prepost-create-freelist | ⊦ ⟪persistence_create_freelist#(lpt; freelist)⟫ freelist-cons(lpt, freelist) | A User Theorem |
| prepost-create-gcheap | lpt0 = lpt ⊦ ⟪persistence_create_gcheap#(nx; lpt, gch)⟫ (bin-heap-inv(gch, lpt) ∧ gc-heap(lpt, nx) = keyset(gch) ∧ id-idx(lpt0, lpt)) | A User Theorem |
| prepost-encode-group-nodes | ⊦ ⟪persistence_encode_group_nodes#(gndx, n, n0; ; buf, ax, err)⟫ ((err = ESUCCESS ∨ ⌊err⌋ ) ∧ (err = ESUCCESS → (∃ lax. lax.to-adr(n) = ax ∧ # buf = gndx.flashsize ∧ abs-nodes(buf, n0, gndx, lax, false)))) | A User Theorem |
| prepost-encode-padding | buf0 = buf, is-aligned(# buf, 2 * NODE_HEADER_SIZE), # buf ≥ 2 * NODE_HEADER_SIZE ⊦ ⟪persistence_encode_padding_node#(; buf; err)⟫ ((err = ESUCCESS ∨ ⌊err⌋ ) ∧ # buf = # buf0 ∧ (err = ESUCCESS → abs-padding(buf))) | A User Theorem |
| prepost-gcheap-add-log | bin-heap-inv(gch, lpt), keyset(gch) = gc-heap(lpt, nx), lpt0 = lpt, ¬ dups(nx), ∀ n. n ∈ nx → n < # lpt ∧ lpt[n].flags = LP_GROUP_NODES ⊦ ⟪persistence_gc_heap_add_log#(; nx, lpt, gch)⟫ (nx = [] ∧ bin-heap-inv(gch, lpt) ∧ keyset(gch) = gc-heap(lpt, nx) ∧ id-idx(lpt0, lpt)) | A User Theorem |
| prepost-replay-log | lpt0 = lpt, nx0 = nx, valid-indices(lpt0, nx), ¬ dups(nx) ⊦ ⟪persistence_replay_log#(LEB_SIZE; nx, lpt)⟫ (lpt = replay-log(lpt0, nx0)) | A User Theorem |
| prepost-replay-lpt | lpt0 = lpt, avol0 = avol, awbuf-inv(avol, nobuffer), # lpt = # avol, synced(avol) ⊦ ⟪persistence_replay_lpt#(nx, LEB_SIZE, adr, m0, log0, lpt1, ns, nobuffer, boolvar; lpt, avol)⟫ (lpt = replay-lpt(lpt0, nx, # lpt0) ∧ awbuf-inv(avol, nobuffer) ∧ avol-replay-lpt-unchanged(avol0, avol, lpt0, nx)) | A User Theorem |
| range-eq-validtrailer | ⊦ is-aligned(# buf, NODE_HEADER_SIZE) ∧ is-aligned(m, NODE_HEADER_SIZE) → (range=(buf + mkempbuf(n), m, validtrailer, 0, NODE_HEADER_SIZE) ↔ range=(buf, m, validtrailer, 0, NODE_HEADER_SIZE)) | A User Theorem |