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: |
|---|---|---|
| load | btree_io_load#(R, ADR, ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; RN, ZH; ERR) {if RN = null then let IND = ? in {apersistence_read_ind#(ADR, ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; IND; ERR); if ERR = ESUCCESS then choose R0 with ¬ R0 ∈ ZH ∧ R0 ≠ null in {ZH := ZH ++ R0; ZH[R0] := mkznode(R, mkzbrarray(BRANCH_SIZE), IND.leaf, false, IND.usedsize); RN := R0; let N = 0 in while N < IND.usedsize do {ZH[RN].zbranches[N] := load(IND.branches[N]); N := N + 1}} ifnone ERR := ENOMEM} else ERR := ESUCCESS } | An Axiom |
| io-save | btree_io_save#(R, ROOTADR, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS; ADR, ZH, ISTORE, PSTATE, PSYNCED; ERR) {let IND = save(ZH[R]), SIZE = 0 in {apersistence_get_block_free_size#(ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; ; SIZE); if SIZE < IND.flashsize then {apersistence_sync#(ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS; PSTATE, PSYNCED; ERR); if ERR = ESUCCESS then apersistence_allocate_ind#(ROOTADR, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSYNCED; ISTORE, PSTATE; ERR)} else ERR := ESUCCESS; if ERR = ESUCCESS then {apersistence_add_ind#(IND, ROOTADR, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS; ADR, ISTORE, PSTATE, PSYNCED; ERR); if ERR = ESUCCESS then let SIZE = 0 in {apersistence_get_iblock_refsize# (ADR.lnum, ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; ; SIZE); apersistence_set_iblock_refsize# (ADR.lnum, SIZE + ADR.size, ROOTADR, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; ISTORE)}}}; if ERR = ESUCCESS then ZH[R].dirty := false } | An Axiom |
| dirty | btree_io_dirty#(R, ADR, DIRTY, ROOTADR, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; ERR, ZH, ISTORE) {if DIRTY then {if ¬ ZH[R].dirty then let SIZE = 0 in {apersistence_get_iblock_refsize# (ADR.lnum, ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; ; SIZE); apersistence_set_iblock_refsize# (ADR.lnum, SIZE - ADR.size, ROOTADR, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; ISTORE)}; ZH[R].dirty := true} } | An Axiom |
| scan | btree_io_scan#(KEY, SKIP, R, ZH; POSITION) {POSITION := 0; while POSITION + SKIP < ZH[R].usedsize ∧ ZH[R].zbranches[POSITION].key < KEY do POSITION := POSITION + 1} | An Axiom |
| shift-left | btree_io_shift_left#(POSITION, R; ZH) {let N = POSITION in while N + 1 < ZH[R].usedsize do ZH[R].zbranches[N] := ZH[R].zbranches[N + 1], N := N + 1} | An Axiom |
| shift-n-left | btree_io_shift_n_left#(POSITION, N, R; ZH) {let M = POSITION in while M + N < ZH[R].usedsize do ZH[R].zbranches[M] := ZH[R].zbranches[M + N], M := M + 1} | An Axiom |
| shift-right | btree_io_shift_right#(POSITION, R; ZH) {let N = ZH[R].usedsize in while POSITION < N do ZH[R].zbranches[N] := ZH[R].zbranches[N - 1], N := N - 1} | An Axiom |
| split | btree_io_split#(POSITION, R; RL, RR, ERR, ZH) {let NUSED = ZH[R].usedsize in let LEFT = POSITION, RIGHT = NUSED - POSITION, RP = ZH[R].parent, LEAF = ZH[R].leaf, DIRTY = ZH[R].dirty in choose R0 with ¬ R0 ∈ ZH ∧ R0 ≠ null in {ZH := ZH ++ R0; ZH[R0] := mkznode(RP, mkzbrarray(BRANCH_SIZE), LEAF, DIRTY, RIGHT); RR := R0; RL := R; ZH[RL].usedsize := LEFT; let N = 0 in while N < RIGHT do ZH[RR].zbranches[N] := ZH[RL].zbranches[POSITION + N], N := N + 1; ZH[RL].dirty := true; ZH[RR].dirty := true; ERR := ESUCCESS} ifnone ERR := ENOMEM } | An Axiom |
| traverse-root | btree_traverse_root# (MOD, RP, ADRT, ROOTADR, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; DIRTY, EXISTS, ADR, RT, ZH, ISTORE; ERR) {btree_traverse# (MOD, RP, ADRT, ROOTADR, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; RT, DIRTY, EXISTS, ADR, ZH, ISTORE; ERR); if ERR = ESUCCESS then if ZH[RT].usedsize = BRANCH_SIZE then let RL = null, RR = null, POSITION = MIN_SIZE in {btree_io_split#(POSITION, RT; RL, RR, ERR, ZH); choose R with ¬ R ∈ ZH ∧ R ≠ null in {ZH := ZH ++ R; ZH[R] := mkznode(null, mkzbrarray(BRANCH_SIZE), false, true, 2); RT := R; DIRTY := true}; let KEY = ZH[RL].zbranches[POSITION - 1].key in {ZH[RL].parent := RT; ZH[RR].parent := RT; ZH[RT].zbranches[0] := mkzbranch(KEY, ADRT, RL); ZH[RT].zbranches[1] := mkzbranch(KEY, ADRT, RR)}} } | An Axiom |
| traverse | btree_traverse#(MOD, RP, ADR0, ROOTADR, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; R, DIRTY, EXISTS, ADR, ZH, ISTORE; ERR) {btree_io_load#(RP, ADR0, ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; R, ZH; ERR); if ERR = ESUCCESS then {if ZH[R].leaf then let N = 0 in {btree_io_scan#(MOD.key, 0, R, ZH; N); let FOUND = N < ZH[R].usedsize ∧ ZH[R].zbranches[N].key = MOD.key in {EXISTS := FOUND ∧ ZH[R].zbranches[N].entry?; if EXISTS then ADR := ZH[R].zbranches[N].adr; if MOD.contains? then {ERR := ESUCCESS; DIRTY := false} else if MOD.lookup? then {ERR := ESUCCESS; DIRTY := false} else if MOD.store? then {if ¬ FOUND then {btree_io_shift_right#(N, R; ZH); ZH[R].usedsize := ZH[R].usedsize + 1}; ZH[R].zbranches[N] := mkzentry(MOD.key, MOD.adr); DIRTY := true; ERR := ESUCCESS} else if MOD.remove? then if FOUND then {btree_io_shift_left#(N, R; ZH); ZH[R].usedsize := ZH[R].usedsize - 1; DIRTY := true; ERR := ESUCCESS} else {DIRTY := false; ERR := ESUCCESS}}} else let N = 0 in {btree_io_scan#(MOD.key, 1, R, ZH; N); let RC = ZH[R].zbranches[N].child, ADRC = ZH[R].zbranches[N].adr in {btree_traverse# (MOD, R, ADRC, ROOTADR, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; RC, DIRTY, EXISTS, ADR, ZH, ISTORE; ERR); if ERR = ESUCCESS then if ZH[RC].usedsize = BRANCH_SIZE then let RL = null, RR = null, POSITION = MIN_SIZE in {btree_io_split#(POSITION, RC; RL, RR, ERR, ZH); btree_io_shift_right#(N, R; ZH); ZH[R].zbranches[N].child := RL; ZH[R].zbranches[N].key := ZH[RL].zbranches[POSITION - 1].key; ZH[R].zbranches[N + 1].child := RR; ZH[R].usedsize := ZH[R].usedsize + 1; DIRTY := true} else if ZH[RC].usedsize = 0 ∧ ZH[R].usedsize ≠ 0 then {btree_io_shift_left#(N, R; ZH); ZH[R].usedsize := ZH[R].usedsize - 1; DIRTY := true; ZH := ZH -- RC} else ZH[R].zbranches[N].child := RC}}; btree_io_dirty#(R, ADR0, DIRTY, ROOTADR, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; ERR, ZH, ISTORE)} } | An Axiom |
| recover | btree_recover#(; MAXINO0, NL0, OS0, ADRT, ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; RT, ERR) {apersistence_recover#(; ADRT, MAXINO0, NL0, OS0, ROOTADR, NL, MAXINO, OS, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0; PSTATE, PSYNCED, ERR); RT := null } | An Axiom |
| commit | btree_commit#(MAXINO0, RT; OS0, ADRT, ZH, ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; ERR) {if dom remove-refsize0(GSTORE) ∩ GINVAL = ∅ ∧ PSTATE = unbuffered ∧ ADRT = ROOTADR then {ERR := ESUCCESS; let ADR = ADRT, DONE = false in {if RT ≠ null ∧ ZH[RT].dirty then {apersistence_allocate_ind#(ROOTADR, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSYNCED; ISTORE, PSTATE; ERR); if ERR = ESUCCESS then btree_commit_rec#(RT, ROOTADR, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS; ADR, ERR, ZH, ISTORE, PSTATE, PSYNCED); if ERR = ESUCCESS then {DONE := true; apersistence_sync#(ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS; PSTATE, PSYNCED; ERR)}}; if ERR = ESUCCESS then apersistence_commit#(ADR, MAXINO0, PSYNCED; OS0, ISTORE, GINVAL, GSTORE, ROOTADR, ISTORE0, GSTORE0, NL, MAXINO, OS; PSTATE, ERR); if ERR = ESUCCESS then ADRT := ADR else if DONE then {ZH[RT].dirty := true; let SIZE = 0 in {apersistence_get_iblock_refsize# (ADR.lnum, ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; ; SIZE); apersistence_set_iblock_refsize# (ADR.lnum, SIZE - ADR.size, ROOTADR, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; ISTORE)}}}} else abort } | An Axiom |
| commit-rec | btree_commit_rec#(R, ROOTADR, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS; ADR, ERR, ZH, ISTORE, PSTATE, PSYNCED) {ERR := ESUCCESS; if ¬ ZH[R].leaf then let N = 0 in while N < ZH[R].usedsize ∧ ERR = ESUCCESS do {let ADRC = ZH[R].zbranches[N].adr, RC = ZH[R].zbranches[N].child in if RC ≠ null ∧ ZH[RC].dirty then {btree_commit_rec#(RC, ROOTADR, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS; ADRC, ERR, ZH, ISTORE, PSTATE, PSYNCED); if ERR = ESUCCESS then ZH[R].zbranches[N].adr := ADRC}; N := N + 1}; if ERR = ESUCCESS then btree_io_save#(R, ROOTADR, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS; ADR, ZH, ISTORE, PSTATE, PSYNCED; ERR) } | An Axiom |
| btree-entries | btree_entries#(KEY, RP, ADR0, ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; R, DONE, NAMES, ZH; ERR) {btree_io_load#(RP, ADR0, ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; R, ZH; ERR); if ERR = ESUCCESS then if ZH[R].leaf then let N = 0 in {btree_io_scan#(KEY, 0, R, ZH; N); while N < ZH[R].usedsize ∧ KEY.ino = ZH[R].zbranches[N].key.ino ∧ ZH[R].zbranches[N].key.dentry? do {NAMES := NAMES ++ ZH[R].zbranches[N].key.name; N := N + 1}; DONE := N < ZH[R].usedsize} else let N = 0 in {btree_io_scan#(KEY, 1, R, ZH; N); while N < ZH[R].usedsize ∧ ¬ DONE do let RC = ZH[R].zbranches[N].child, ADRC = ZH[R].zbranches[N].adr in {btree_entries# (KEY, R, ADRC, ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; RC, DONE, NAMES, ZH; ERR); N := N + 1}} } | An Axiom |
| btree-truncate | btree_truncate#(KEY, RP, ADR0, ROOTADR, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; R, DIRTY, DONE, AS, ZH, ISTORE; ERR) {btree_io_load#(RP, ADR0, ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; R, ZH; ERR); if ERR = ESUCCESS then if ZH[R].leaf then let POSITION = 0, N = 0 in {btree_io_scan#(KEY, 0, R, ZH; POSITION); while POSITION + N < ZH[R].usedsize ∧ KEY.ino = ZH[R].zbranches[POSITION + N].key.ino ∧ ZH[R].zbranches[POSITION + N].key.data? do {if ZH[R].zbranches[POSITION + N].entry? then AS := AS ++ ZH[R].zbranches[POSITION + N].adr; DIRTY := true; N := N + 1}; btree_io_shift_n_left#(POSITION, N, R; ZH); DONE := POSITION + N < ZH[R].usedsize; ZH[R].usedsize := ZH[R].usedsize - N} else let N = 0 in {btree_io_scan#(KEY, 1, R, ZH; N); while N < ZH[R].usedsize ∧ ¬ DONE do let RC = ZH[R].zbranches[N].child, ADRC = ZH[R].zbranches[N].adr in {btree_truncate# (KEY, R, ADRC, ROOTADR, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; RC, DIRTY, DONE, AS, ZH, ISTORE; ERR); ZH[R].zbranches[N].child := RC; if ZH[RC].usedsize = 0 ∧ ZH[R].usedsize ≠ 0 then {btree_io_shift_left#(N, R; ZH); ZH[R].usedsize := ZH[R].usedsize - 1; ZH := ZH -- RC} else N := N + 1}}; btree_io_dirty#(R, ADR0, DIRTY, ROOTADR, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; ERR, ZH, ISTORE) } | An Axiom |
| remove | btree_index_remove#(KEY, ADRT, ROOTADR, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; OLDADR, EXISTS, RT, ZH, ISTORE) {choose DIRTY, ERR with true in btree_traverse_root# (remove(KEY), null, ADRT, ROOTADR, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; DIRTY, EXISTS, OLDADR, RT, ZH, ISTORE; ERR) } | An Axiom |
| store | btree_index_store#(KEY, ADR, ADRT, ROOTADR, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; OLDADR, EXISTS, RT, ZH, ISTORE) {choose DIRTY, ERR with true in btree_traverse_root# (store(KEY, ADR), null, ADRT, ROOTADR, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED ; DIRTY, EXISTS, OLDADR, RT, ZH, ISTORE ; ERR) } | An Axiom |
| lookup | btree_index_lookup#(KEY, ADRT, ROOTADR, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; EXISTS, ADR, RT, ZH, ISTORE; ERR) {choose DIRTY with true in btree_traverse_root# (lookup(KEY), null, ADRT, ROOTADR, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; DIRTY, EXISTS, ADR, RT, ZH, ISTORE; ERR) } | An Axiom |
| contains | btree_index_contains#(KEY, ADRT, ROOTADR, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; EXISTS, RT, ZH, ISTORE; ERR) {choose DIRTY, ADR with true in btree_traverse_root# (contains(KEY), null, ADRT, ROOTADR, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; DIRTY, EXISTS, ADR, RT, ZH, ISTORE; ERR) } | An Axiom |
| entries | btree_index_entries#(KEY, ADRT, ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; NAMES, RT, ZH; ERR) {let DONE = false in btree_entries# (dentrykey(KEY.ino, ""), null, ADRT, ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; RT, DONE, NAMES, ZH; ERR) } | An Axiom |
| truncate | btree_index_truncate#(KEY, N, ADRT, ROOTADR, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; AS, RT, ZH, ISTORE) {let DIRTY = false, DONE = false, ERR = ? in btree_truncate# (datakey(KEY.ino, (N + VFS_PAGE_SIZE - 1) / VFS_PAGE_SIZE), null, ADRT, ROOTADR, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED ; RT, DIRTY, DONE, AS, ZH, ISTORE ; ERR) } | An Axiom |
| deallocate-gnd | btree_deallocate_gnd#(N, ROOTADR, ISTORE, ISTORE0, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; GINVAL, GSTORE; ERR) {if PSYNCED ∧ N ∈ GSTORE ∧ ¬ N ∈ NL then apersistence_deallocate_gnd#(N, ROOTADR, ISTORE, ISTORE0, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; GINVAL, GSTORE; ERR) else abort } | An Axiom |
| allocate-gnd | btree_allocate_gnd#(ROOTADR, ISTORE, ISTORE0, GSTORE0, MAXINO, OS, PSYNCED; GINVAL, GSTORE, NL, PSTATE; ERR) {if PSYNCED then apersistence_allocate_gnd#(ROOTADR, ISTORE, ISTORE0, GSTORE0, MAXINO, OS, PSYNCED; GINVAL, GSTORE, NL, PSTATE; ERR) else abort} | An Axiom |
| get-gblock-refsize | btree_get_gblock_refsize#(LNUM, ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; ; N) {if LNUM ∈ GSTORE then apersistence_get_gblock_refsize#(LNUM, ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; ; N) else abort } | An Axiom |
| set-gblock-refsize | btree_set_gblock_refsize#(LNUM, N, ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; GSTORE) {if LNUM ∈ GSTORE then apersistence_set_gblock_refsize#(LNUM, N, ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; GSTORE) else abort } | An Axiom |
| add-gnds | btree_add_gnds#(GNDLIST, ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE0, NL, MAXINO, OS; ADRLIST, GSTORE, PSTATE, PSYNCED; ERR) {if NL ≠ [] ∧ PSTATE.journal? then apersistence_add_gnds#(GNDLIST, ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE0, NL, MAXINO, OS; ADRLIST, GSTORE, PSTATE, PSYNCED; ERR) else abort } | An Axiom |
| get-gc-block | btree_get_gc_block#(ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; N; ERR) {apersistence_get_gc_block#(ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; N; ERR)} | An Axiom |
| read-gblock | btree_read_gblock_nodes#(LNUM, ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; ADRLIST, GNDLIST; ERR) {if LNUM ∈ GSTORE ∧ ¬ LNUM ∈ GINVAL then apersistence_read_gblock_nodes# (LNUM, ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; ADRLIST, GNDLIST; ERR) else abort } | An Axiom |
| read-gnd | btree_read_gnd#(ADR, ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; GND; ERR) {if ADR ∈ GSTORE ∧ ¬ ADR.lnum ∈ GINVAL then apersistence_read_gnd#(ADR, ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; GND; ERR) else abort } | An Axiom |
| requires-commit | btree_requires_commit#(ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; ; COMMIT?) {apersistence_requires_commit#(ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; ; COMMIT?)} | An Axiom |
| format | btree_format#(VOLSIZE, SIZE, MAXINO0; ADRT, ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; RT, ERR) {if SIZE = LEB_SIZE then {RT := null; apersistence_format#(VOLSIZE, SIZE, MAXINO0; ; ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED, ERR); let N = ? in {apersistence_get_leb_size#(ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; ; N); if ERR = ESUCCESS then let IND = indexnode(mkbrarray(BRANCH_SIZE), true, 0) in let SIZE = IND.flashsize in {if SIZE > N then {debug#("btree: initial index node to large"); ERR := ENOSPC}; if ERR = ESUCCESS then apersistence_allocate_ind#(ROOTADR, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSYNCED; ISTORE, PSTATE; ERR); if ERR = ESUCCESS then apersistence_add_ind# (IND, ROOTADR, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS; ADRT, ISTORE, PSTATE, PSYNCED; ERR); if ERR = ESUCCESS then apersistence_set_iblock_refsize# (ADRT.lnum, SIZE, ROOTADR, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; ISTORE); if ERR = ESUCCESS then apersistence_sync#(ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS; PSTATE, PSYNCED; ERR); if ERR = ESUCCESS then let NS = ∅ in apersistence_commit# (ADRT, MAXINO0, PSYNCED; NS, ISTORE, GINVAL, GSTORE, ROOTADR, ISTORE0, GSTORE0, NL, MAXINO, OS; PSTATE, ERR)}}} else abort } | An Axiom |
| sync | btree_sync#(ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS; PSTATE, PSYNCED; ERR) {apersistence_sync#(ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS; PSTATE, PSYNCED; ERR)} | An Axiom |
| get-block-free-size | btree_get_block_free_size#(ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; ; N) {apersistence_get_block_free_size#(ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; ; N)} | An Axiom |
| is-log-empty | btree_is_log_empty#(ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; ; EMPTY?) {apersistence_is_log_empty#(ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; ; EMPTY?)} | An Axiom |
| get-leb-size | btree_get_leb_size(ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; ; N) {apersistence_get_leb_size#(ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; ; N)} | An Axiom |
| inv-is-log-empty | btree-inv(rp, adr, istore, istore0, zh, ri, fi), inv-journal(nx, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, nx, gstore, istore, syn) ⊦ ⟪btree_is_log_empty#(adr, istore, istore0, ginval, gstore, gstore0, nx, maxino, ginval0, pstate, syn; ; syn0)⟫ true | A Proof Obligation |
| inv-recover | adr = adr0, istore = remove-refsize0(crash(istore0, istore1)), istore2 = istore1, ginval = ginval0, gstore = crash(gstore0, gstore1, ginval0, nx), gstore2 = gstore1, nx0 = nx, maxino = maxino0, ginval1 = ginval2, syn, btree-inv(rp, adr0, istore0, istore1, zh, ri, fi), inv-journal(nx, gstore0, gstore1, ginval0), inv-index(istore0, istore1), inv-state(pstate, nx, gstore0, istore0, syn) ⊦ ⟪btree_recover#(; maxino1, nx1, ginval3, adr1, adr, istore, istore2, ginval, gstore, gstore2, nx0, maxino, ginval1, pstate0, syn0; rp0, err)⟫ ( err = ESUCCESS → syn0 ∧ (∃ ri, fi. btree-inv(rp0, adr, istore, istore2, zh0, ri, fi)) ∧ inv-journal(nx0, gstore, gstore2, ginval) ∧ inv-index(istore, istore2) ∧ inv-state(pstate0, nx0, gstore, istore, syn0)) | A Proof Obligation |
| inv-commit | btree-inv(rp, adr, istore, istore0, zh, ri, fi), inv-journal(nx, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, nx, gstore, istore, syn), dom remove-refsize0(gstore) ∩ ginval = ∅, pstate = unbuffered, adr0 = adr ⊦ ⟪btree_commit#(maxino, rp; ginval0, adr0, zh, adr, istore, istore0, ginval, gstore, gstore0, nx, maxino0, ginval1, pstate, syn; err)⟫ ( (∃ ri, fi. btree-inv(rp, adr, istore, istore0, zh, ri, fi)) ∧ inv-journal(nx, gstore, gstore0, ginval) ∧ inv-index(istore, istore0) ∧ inv-state(pstate, nx, gstore, istore, syn)) | A Proof Obligation |
| inv-remove | btree-inv(rp, adr, istore, istore0, zh, ri, fi), inv-journal(nx, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, nx, gstore, istore, syn) ⊦ ⟪btree_index_remove#(key, adr0, adr, istore0, ginval, gstore, gstore0, nx, maxino, ginval0, pstate, syn; adr1, syn0, rp, zh, istore)⟫ ((∃ ri, fi. btree-inv(rp, adr, istore, istore0, zh, ri, fi)) ∧ inv-index(istore, istore0) ∧ inv-state(pstate, nx, gstore, istore, syn)) | A Proof Obligation |
| inv-store | btree-inv(rp, adr, istore, istore0, zh, ri, fi), inv-journal(nx, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, nx, gstore, istore, syn) ⊦ ⟪btree_index_store#(key, adr0, adr1, adr, istore0, ginval, gstore, gstore0, nx, maxino, ginval0, pstate, syn; adr2, syn0, rp, zh, istore)⟫ ((∃ ri, fi. btree-inv(rp, adr, istore, istore0, zh, ri, fi)) ∧ inv-index(istore, istore0) ∧ inv-state(pstate, nx, gstore, istore, syn)) | A Proof Obligation |
| inv-lookup | btree-inv(rp, adr, istore, istore0, zh, ri, fi), inv-journal(nx, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, nx, gstore, istore, syn) ⊦ ⟪btree_index_lookup#(key, adr0, adr, istore0, ginval, gstore, gstore0, nx, maxino, ginval0, pstate, syn; syn0, adr1, rp, zh, istore; err)⟫ ((∃ ri, fi. btree-inv(rp, adr, istore, istore0, zh, ri, fi)) ∧ inv-index(istore, istore0) ∧ inv-state(pstate, nx, gstore, istore, syn)) | A Proof Obligation |
| inv-contains | btree-inv(rp, adr, istore, istore0, zh, ri, fi), inv-journal(nx, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, nx, gstore, istore, syn) ⊦ ⟪btree_index_contains#(key, adr0, adr, istore0, ginval, gstore, gstore0, nx, maxino, ginval0, pstate, syn; syn0, rp, zh, istore; err)⟫ ((∃ ri, fi. btree-inv(rp, adr, istore, istore0, zh, ri, fi)) ∧ inv-index(istore, istore0) ∧ inv-state(pstate, nx, gstore, istore, syn)) | A Proof Obligation |
| inv-entries | btree-inv(rp, adr, istore, istore0, zh, ri, fi), inv-journal(nx, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, nx, gstore, istore, syn) ⊦ ⟪btree_index_entries#(key, adr0, adr, istore, istore0, ginval, gstore, gstore0, nx, maxino, ginval0, pstate, syn; strings, rp, zh; err)⟫ ∃ ri, fi. btree-inv(rp, adr, istore, istore0, zh, ri, fi) | A Proof Obligation |
| inv-truncate | btree-inv(rp, adr, istore, istore0, zh, ri, fi), inv-journal(nx, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, nx, gstore, istore, syn) ⊦ ⟪btree_index_truncate#(key, n, adr0, adr, istore0, ginval, gstore, gstore0, nx, maxino, ginval0, pstate, syn; as, rp, zh, istore)⟫ ((∃ ri, fi. btree-inv(rp, adr, istore, istore0, zh, ri, fi)) ∧ inv-index(istore, istore0) ∧ inv-state(pstate, nx, gstore, istore, syn)) | A Proof Obligation |
| inv-deallocate-gnd | btree-inv(rp, adr, istore, istore0, zh, ri, fi), inv-journal(nx, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, nx, gstore, istore, syn), syn, n ∈ gstore, ¬ n ∈ nx ⊦ ⟪btree_deallocate_gnd#(n, adr, istore, istore0, gstore0, nx, maxino, ginval0, pstate, syn; ginval, gstore; err)⟫ (inv-journal(nx, gstore, gstore0, ginval) ∧ inv-state(pstate, nx, gstore, istore, syn)) | A Proof Obligation |
| inv-allocate-gnd | btree-inv(rp, adr, istore, istore0, zh, ri, fi), inv-journal(nx, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, nx, gstore, istore, syn), syn ⊦ ⟪btree_allocate_gnd#(adr, istore, istore0, gstore0, maxino, ginval0, syn; ginval, gstore, nx, pstate; err)⟫ (inv-journal(nx, gstore, gstore0, ginval) ∧ inv-state(pstate, nx, gstore, istore, syn)) | A Proof Obligation |
| inv-get-gblock-refsize | btree-inv(rp, adr, istore, istore0, zh, ri, fi), inv-journal(nx, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, nx, gstore, istore, syn), maxino ∈ gstore ⊦ ⟪btree_get_gblock_refsize#(maxino, adr, istore, istore0, ginval, gstore, gstore0, nx, maxino0, ginval0, pstate, syn; ; n)⟫ true | A Proof Obligation |
| inv-set-gblock-refsize | btree-inv(rp, adr, istore, istore0, zh, ri, fi), inv-journal(nx, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, nx, gstore, istore, syn), maxino ∈ gstore ⊦ ⟪btree_set_gblock_refsize#(maxino, n, adr, istore, istore0, ginval, gstore0, nx, maxino0, ginval0, pstate, syn; gstore)⟫ (inv-journal(nx, gstore, gstore0, ginval) ∧ inv-state(pstate, nx, gstore, istore, syn)) | A Proof Obligation |
| inv-add-gnds | btree-inv(rp, adr, istore, istore0, zh, ri, fi), inv-journal(nx, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, nx, gstore, istore, syn), nx ≠ [], pstate.journal? ⊦ ⟪btree_add_gnds#(gndx, adr, istore, istore0, ginval, gstore0, nx, maxino, ginval0; ax, gstore, pstate, syn; err)⟫ (inv-journal(nx, gstore, gstore0, ginval) ∧ inv-state(pstate, nx, gstore, istore, syn)) | A Proof Obligation |
| inv-get-gc-block | btree-inv(rp, adr, istore, istore0, zh, ri, fi), inv-journal(nx, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, nx, gstore, istore, syn) ⊦ ⟪btree_get_gc_block#(adr, istore, istore0, ginval, gstore, gstore0, nx, maxino, ginval0, pstate, syn; n; err)⟫ true | A Proof Obligation |
| inv-read-gblock | btree-inv(rp, adr, istore, istore0, zh, ri, fi), inv-journal(nx, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, nx, gstore, istore, syn), maxino ∈ gstore, ¬ maxino ∈ ginval ⊦ ⟪btree_read_gblock_nodes#(maxino, adr, istore, istore0, ginval, gstore, gstore0, nx, maxino0, ginval0, pstate, syn; ax, gndx; err)⟫ true | A Proof Obligation |
| inv-read-gnd | btree-inv(rp, adr, istore, istore0, zh, ri, fi), inv-journal(nx, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, nx, gstore, istore, syn), adr0 ∈ gstore, ¬ adr0.lnum ∈ ginval ⊦ ⟪btree_read_gnd#(adr0, adr, istore, istore0, ginval, gstore, gstore0, nx, maxino, ginval0, pstate, syn; gnd; err)⟫ true | A Proof Obligation |
| inv-format | maxino = LEB_SIZE ⊦ ⟪btree_format#(maxino0, maxino, maxino1; adr, adr0, istore, istore0, ginval, gstore, gstore0, nx, maxino2, ginval0, pstate, syn; rp, err)⟫ ( ( err = ESUCCESS → syn ∧ (∃ ri, fi. btree-inv(rp, adr0, istore, istore0, zh, ri, fi)) ∧ inv-journal(nx, gstore, gstore0, ginval) ∧ inv-index(istore, istore0) ∧ inv-state(pstate, nx, gstore, istore, syn)) ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ (err = ESUCCESS → btree-inv(rp, adr0, istore, istore0, zh, ∅, ∅) ∧ gstore = ∅ ∧ ginval = ∅ ∧ maxino2 = maxino1 ∧ nx = [] ∧ ginval0 = ∅)) | A Proof Obligation |
| inv-requires-commit | btree-inv(rp, adr, istore, istore0, zh, ri, fi), inv-journal(nx, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, nx, gstore, istore, syn) ⊦ ⟪btree_requires_commit#(adr, istore, istore0, ginval, gstore, gstore0, nx, maxino, ginval0, pstate, syn; ; syn0)⟫ true | A Proof Obligation |
| inv-sync | btree-inv(rp, adr, istore, istore0, zh, ri, fi), inv-journal(nx, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, nx, gstore, istore, syn) ⊦ ⟪btree_sync#(adr, istore, istore0, ginval, gstore, gstore0, nx, maxino, ginval0; pstate, syn; err)⟫ inv-state(pstate, nx, gstore, istore, syn) | A Proof Obligation |
| inv-get-block-free-size | btree-inv(rp, adr, istore, istore0, zh, ri, fi), inv-journal(nx, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, nx, gstore, istore, syn) ⊦ ⟪btree_get_block_free_size#(adr, istore, istore0, ginval, gstore, gstore0, nx, maxino, ginval0, pstate, syn; ; n)⟫ true | A Proof Obligation |
| inv-get-leb-size | btree-inv(rp, adr, istore, istore0, zh, ri, fi), inv-journal(nx, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, nx, gstore, istore, syn) ⊦ ⟪btree_get_leb_size(adr, istore, istore0, ginval, gstore, gstore0, nx, maxino, ginval0, pstate, syn; ; n)⟫ true | A Proof Obligation |
| inv-commit-rec | adr0 = adr1, istore1 = istore, inv-journal(nx, gstore, gstore0, ginval), inv-index(istore, istore0), pstate.index?, inv-state(pstate, nx, gstore, istore, bv), btree-inv(r0, adr0, istore, istore0, zh, ri, fi), r0 ∈ zh, zh[r0].dirty ⊦ ⟪btree_commit_rec#(r0, adr0, istore0, ginval, gstore, gstore0, nx, ino, ns; adr1, err, zh, istore, pstate, bv)⟫ ( istore1 ⊑ istore ∧ inv-state(pstate, nx, gstore, istore, bv) ∧ inv-journal(nx, gstore, gstore0, ginval) ∧ inv-index(istore, istore0) ∧ (err ≠ ESUCCESS → btree-inv(r0, adr0, istore, istore0, zh, ri, fi)) ∧ ( err = ESUCCESS → btree-inv(r0, adr1, istore, istore, zh, ri, ri) ∧ btree-inv (r0, adr0, istore[adr1.lnum, istore[adr1.lnum].ref-size:= (istore[adr1.lnum].ref-size - adr1.size)], istore0, zh[r0, zh[r0].dirty:= true], ri, fi) ∧ ¬ zh[r0].dirty)) | A User Theorem |
| inv-commit-rec-ind | adr0 = adr1, istore1 = istore, inv-journal(nx, gstore, gstore0, ginval), inv-index(istore, istore0), pstate.index?, inv-state(pstate, nx, gstore, istore, bv), ((btree(rp, r0, adr0, height, dirty, ri, nodes(istore) | as, as, alladrs, ok) * P))(zh), r0 ∈ zh, zh[r0].dirty, alladrs ⊆ dom nodes(istore), as0 ⊆ dom nodes(istore), as ∩ as0 = ∅, refsize-cons(istore, as0 ∪ as) ⊦ ⟪btree_commit_rec#(r0, adr, istore0, ginval, gstore, gstore0, nx, ino, ns; adr1, err, zh, istore, pstate, bv)⟫ ( istore1 ⊑ istore ∧ inv-state(pstate, nx, gstore, istore, bv) ∧ inv-journal(nx, gstore, gstore0, ginval) ∧ inv-index(istore, istore0) ∧ r0 ∈ zh ∧ (err = ESUCCESS → ¬ zh[r0].dirty ∧ pstate.index?) ∧ (∃ as1, alladrs1. refsize-cons(istore, as0 ∪ as1) ∧ as1 ∩ dom nodes(istore1) ⊆ as ∧ as1 ∩ as0 = ∅ ∧ alladrs1 ⊆ alladrs ∪ as1 ∧ ((btree(rp, r0, (err = ESUCCESS ⊃ adr1;adr0), height, err ≠ ESUCCESS, ri, nodes(istore) | as1, as1, alladrs1, ok) * P))(zh))) | A User Theorem |
| inv-io-save | adr0 = adr1, r ∈ zh, zh[r].dirty, btree-sub-clean(r, zh[r].usedsize, zh), ((btree(rp, r, adr0, height, dirty, ri, nodes(istore), as, alladrs, ok) * P))(zh), as0 ⊆ dom nodes(istore), alladrs ⊆ dom nodes(istore), refsize-cons(istore, as0 ∪ as), inv-journal(nx, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, nx, gstore, istore, syn), pstate.index?, istore1 = istore ⊦ ⟪btree_io_save#(r, adr, istore0, ginval, gstore, gstore0, nx, maxino, ginval0; adr1, zh, istore, pstate, syn; err)⟫ ( refsize-cons(istore, as0 ∪ (err = ESUCCESS ⊃ as ++ adr1;as)) ∧ inv-index(istore, istore0) ∧ inv-state(pstate, nx, gstore, istore, syn) ∧ istore1 ⊑ istore ∧ r ∈ zh ∧ (err = ESUCCESS → ¬ adr1 ∈ as) ∧ (∃ as0, alladrs0. as0 = (err = ESUCCESS ⊃ as ++ adr1;as) ∧ alladrs0 = (err = ESUCCESS ⊃ (alladrs -- adr0) ++ adr1;alladrs) ∧ dom nodes(istore) = dom nodes(istore1) ∪ (err = ESUCCESS ⊃ {adr1} ;∅) ∧ (err = ESUCCESS → ¬ adr1 ∈ istore1) ∧ ((btree(rp, r, (err = ESUCCESS ⊃ adr1;adr0), height, err ≠ ESUCCESS, ri, nodes(istore), as0, alladrs0, ok) * P))(zh)) ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ (err = ESUCCESS → pstate.index? ∧ ¬ zh[r].dirty)) | A User Theorem |