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: |
|---|---|---|
| contains | index_index_contains#(KEY, PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; EXISTS; ERR) {fail_or_success#(; ; ERR); if ERR = ESUCCESS then EXISTS := KEY ∈ PRI else EXISTS := ?} | An Axiom |
| lookup | index_index_lookup#(KEY, PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; EXISTS, ADR; ERR) {fail_or_success#(; ; ERR); if ERR = ESUCCESS then {EXISTS := KEY ∈ PRI; if EXISTS then ADR := PRI[KEY] else ADR := ?} else EXISTS := ?, ADR := ?} | An Axiom |
| store | index_index_store#(KEY, ADR, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; OLDADR, EXISTS, PRI) {if ¬ ADR ∈ PRI ∧ ADR ∈ PSTORE ∧ key-cons(KEY, PSTORE[ADR].nd) then {EXISTS := KEY ∈ PRI; if EXISTS then OLDADR := PRI[KEY] else OLDADR := ?; PRI[KEY] := ADR} else abort } | An Axiom |
| remove | index_index_remove#(KEY, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; OLDADR, EXISTS, PRI) {EXISTS := KEY ∈ PRI; if EXISTS then {OLDADR := PRI[KEY]; PRI := PRI -- KEY} else OLDADR := ?} | An Axiom |
| truncate | index_index_truncate#(KEY, N, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; AS, PRI) {let KS = datakeys(KEY, N, PRI) in PRI := PRI \ KS, AS := PRI[KS]} | An Axiom |
| entries | index_index_entries#(KEY, PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; NAMES; ERR) {fail_or_success#(; ; ERR); if ERR = ESUCCESS then NAMES := dentries(KEY, PRI) else NAMES := ?} | An Axiom |
| read-gnd | index_read_gnd#(ADR, PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; GND; ERR) {if ADR ∈ PSTORE ∧ ¬ ADR.lnum ∈ PINVAL then {fail_or_success#(; ; ERR); if ERR = ESUCCESS then GND := PSTORE[ADR] else GND := ?} else abort} | An Axiom |
| read-gblock | index_read_gblock_nodes#(LNUM, PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; ADRLIST, GNDLIST; ERR) {if LNUM ∈ PSTORE ∧ ¬ LNUM ∈ PINVAL then {fail_or_success#(; ; ERR); if ERR = ESUCCESS then ADRLIST := ADRLIST + PSTORE[LNUM].ladrlist.to-adr(LNUM), GNDLIST := GNDLIST + PSTORE[LNUM].gndlist else ADRLIST := ?, GNDLIST := ?} else abort } | An Axiom |
| get-gc-block | index_get_gc_block#(PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; N; ERR) {ERR := ENOSPC or choose N0 with N0 ∈ dom PSTORE ∧ ¬ N0 ∈ PNL in {N := N0; ERR := ESUCCESS} ifnone ERR := ENOSPC} | An Axiom |
| set-gblock-refsize | index_set_gblock_refsize#(LNUM, N, PRI, PFI, PINVAL, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; PSTORE) {if LNUM ∈ PSTORE then PSTORE[LNUM].ref-size := N else abort} | An Axiom |
| get-gblock-refsize | index_get_gblock_refsize#(LNUM, PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; ; N) {if LNUM ∈ PSTORE then N := PSTORE[LNUM].ref-size else abort} | An Axiom |
| allocate-gnd | index_allocate_gnd#(PRI, PFI, PSTORE0, PMAXINO, P_OS, ISYNCED; PINVAL, PSTORE, PNL; ERR) {if ISYNCED then {fail_or_success#(; ; ERR); if ERR = ESUCCESS then choose N with ¬ N ∈ PSTORE in PSTORE[N] := groupblock([], [], 0), PNL := PNL + N, PINVAL := PINVAL -- N} else abort } | An Axiom |
| deallocate-gnd | index_deallocate_gnd#(N, PRI, PFI, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; PINVAL, PSTORE; ERR) {if ISYNCED ∧ N ∈ PSTORE ∧ ¬ N ∈ PNL then {fail_or_success#(; ; ERR); if ERR = ESUCCESS then PSTORE := PSTORE -- N, PINVAL := PINVAL ++ N} else abort } | An Axiom |
| commit | index_commit#(PMAXINO0, PRI, ISYNCED; P_OS0, PINVAL, PSTORE, PFI, PSTORE0, PNL, PMAXINO, P_OS; ERR) {if ISYNCED ∧ dom remove-refsize0(PSTORE) ∩ PINVAL = ∅ then {fail_or_success#(; ; ERR); if ERR = ESUCCESS then {PSTORE := remove-refsize0(PSTORE); PSTORE0 := PSTORE; PINVAL := ∅; P_OS := P_OS0; PNL := []; PMAXINO := PMAXINO0; PFI := PRI}; P_OS0 := ?} else abort } | An Axiom |
| requires-commit | index_requires_commit#(PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; ; COMMIT?){COMMIT? := ?} | An Axiom |
| format | index_format#(VOLSIZE, SIZE, PMAXINO0; ; PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED, ERR) {if SIZE = LEB_SIZE then {fail_or_success#(; ; ERR); if ERR = ESUCCESS then PMAXINO := PMAXINO0, ISYNCED := true, P_OS := ∅, PNL := [], PSTORE := ∅, PSTORE0 := ∅, PINVAL := ∅, PRI := ∅, PFI := ∅ else PMAXINO := ?, ISYNCED := ?, P_OS := ?, PNL := ?, PSTORE := ?, PSTORE0 := ?, PINVAL := ?, PRI := ?, PFI := ?} else abort } | An Axiom |
| recovery | index_recover#(; PMAXINO0, PNL0, P_OS0, PFI, PNL, PMAXINO, P_OS, PINVAL, PSTORE, PSTORE0; PRI, ISYNCED, ERR) {fail_or_success#(; ; ERR); if ERR = ESUCCESS then PMAXINO0 := PMAXINO, ISYNCED := true, PNL0 := PNL, P_OS0 := P_OS, PRI := PFI else PINVAL := ?, ISYNCED := ?, PSTORE := ?, PSTORE0 := ?, PNL := ?, PMAXINO := ?, P_OS := ?, PMAXINO0 := ?, PNL0 := ?, P_OS0 := ?, PRI := ?, PFI := ? } | An Axiom |
| add-gnds | index_add_gnds#(GNDLIST, PRI, PFI, PINVAL, PSTORE0, PNL, PMAXINO, P_OS; ADRLIST, PSTORE; ISYNCED, ERR) {if PNL ≠ [] then {choose LADRLIST, ERR0 with (⌊ERR0⌋ ∨ ERR0 = ESUCCESS) ∧ ¬ dups(PSTORE[PNL.last].ladrlist + LADRLIST) ∧ # LADRLIST ≤ # GNDLIST ∧ inv-flashsize(prefixn(# LADRLIST, GNDLIST), LADRLIST) ∧ (ERR0 = ESUCCESS ↔ # LADRLIST = # GNDLIST) in {ADRLIST := LADRLIST.to-adr(PNL.last), ERR := ERR0; PSTORE[PNL.last].gndlist := PSTORE[PNL.last].gndlist + prefixn(# LADRLIST, GNDLIST); PSTORE[PNL.last].ladrlist := PSTORE[PNL.last].ladrlist + LADRLIST; if ERR ≠ ESUCCESS then ADRLIST := ?}; ISYNCED := ?} else abort } | An Axiom |
| sync | index_sync#(PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS; ; ISYNCED, ERR) {fail_or_success#(; ; ERR); if ERR = ESUCCESS then ISYNCED := true else ISYNCED := ?} | An Axiom |
| get-block-free-size | index_get_block_free_size#(PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; ; N){choose N0 with N0 ≤ LEB_SIZE in N := N0} | An Axiom |
| is-log-empty | index_is_log_empty#(PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; ; EMPTY?){EMPTY? := PNL = []} | An Axiom |
| get-leb-size | index_get_leb_size(PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; ; N){N := LEB_SIZE} | An Axiom |
| inv-contains | inv-journal(nx, gstore, gstore0, ginval), ri-inj(fi), ri-inj(fi0) ⊦ ⟪index_index_contains#(key, fi, fi0, ginval, gstore, gstore0, nx, maxino, ginval0, syn; syn0; err)⟫ true | A Proof Obligation |
| inv-lookup | inv-journal(nx, gstore, gstore0, ginval), ri-inj(fi), ri-inj(fi0) ⊦ ⟪index_index_lookup#(key, fi, fi0, ginval, gstore, gstore0, nx, maxino, ginval0, syn; syn0, adr; err)⟫ true | A Proof Obligation |
| inv-store | inv-journal(nx, gstore, gstore0, ginval), ri-inj(fi), ri-inj(fi0), ¬ adr ∈ fi, adr ∈ gstore, key-cons(key, gstore[adr].nd) ⊦ ⟪index_index_store#(key, adr, fi0, ginval, gstore, gstore0, nx, maxino, ginval0, syn; adr0, syn0, fi)⟫ ri-inj(fi) | A Proof Obligation |
| inv-remove | inv-journal(nx, gstore, gstore0, ginval), ri-inj(fi), ri-inj(fi0) ⊦ ⟪index_index_remove#(key, fi0, ginval, gstore, gstore0, nx, maxino, ginval0, syn; adr, syn0, fi)⟫ ri-inj(fi) | A Proof Obligation |
| inv-truncate | inv-journal(nx, gstore, gstore0, ginval), ri-inj(fi), ri-inj(fi0) ⊦ ⟪index_index_truncate#(key, n, fi0, ginval, gstore, gstore0, nx, maxino, ginval0, syn; as, fi)⟫ ri-inj(fi) | A Proof Obligation |
| inv-entries | inv-journal(nx, gstore, gstore0, ginval), ri-inj(fi), ri-inj(fi0) ⊦ ⟪index_index_entries#(key, fi, fi0, ginval, gstore, gstore0, nx, maxino, ginval0, syn; strings; err)⟫ true | A Proof Obligation |
| inv-read-gnd | inv-journal(nx, gstore, gstore0, ginval), ri-inj(fi), ri-inj(fi0), adr ∈ gstore, ¬ adr.lnum ∈ ginval ⊦ ⟪index_read_gnd#(adr, fi, fi0, ginval, gstore, gstore0, nx, maxino, ginval0, syn; gnd; err)⟫ true | A Proof Obligation |
| inv-read-gblock | inv-journal(nx, gstore, gstore0, ginval), ri-inj(fi), ri-inj(fi0), maxino ∈ gstore, ¬ maxino ∈ ginval ⊦ ⟪index_read_gblock_nodes#(maxino, fi, fi0, ginval, gstore, gstore0, nx, maxino0, ginval0, syn; ax, gndx; err)⟫ true | A Proof Obligation |
| inv-get-gc-block | inv-journal(nx, gstore, gstore0, ginval), ri-inj(fi), ri-inj(fi0) ⊦ ⟪index_get_gc_block#(fi, fi0, ginval, gstore, gstore0, nx, maxino, ginval0, syn; n; err)⟫ true | A Proof Obligation |
| inv-set-gblock-refsize | inv-journal(nx, gstore, gstore0, ginval), ri-inj(fi), ri-inj(fi0), maxino ∈ gstore ⊦ ⟪index_set_gblock_refsize#(maxino, n, fi, fi0, ginval, gstore0, nx, maxino0, ginval0, syn; gstore)⟫ inv-journal(nx, gstore, gstore0, ginval) | A Proof Obligation |
| inv-get-gblock-refsize | inv-journal(nx, gstore, gstore0, ginval), ri-inj(fi), ri-inj(fi0), maxino ∈ gstore ⊦ ⟪index_get_gblock_refsize#(maxino, fi, fi0, ginval, gstore, gstore0, nx, maxino0, ginval0, syn; ; n)⟫ true | A Proof Obligation |
| inv-allocate-gnd | inv-journal(nx, gstore, gstore0, ginval), ri-inj(fi), ri-inj(fi0), syn ⊦ ⟪index_allocate_gnd#(fi, fi0, gstore0, maxino, ginval0, syn; ginval, gstore, nx; err)⟫ inv-journal(nx, gstore, gstore0, ginval) | A Proof Obligation |
| inv-deallocate-gnd | inv-journal(nx, gstore, gstore0, ginval), ri-inj(fi), ri-inj(fi0), syn, n ∈ gstore, ¬ n ∈ nx ⊦ ⟪index_deallocate_gnd#(n, fi, fi0, gstore0, nx, maxino, ginval0, syn; ginval, gstore; err)⟫ inv-journal(nx, gstore, gstore0, ginval) | A Proof Obligation |
| inv-commit | inv-journal(nx, gstore, gstore0, ginval), ri-inj(fi), ri-inj(fi0), syn, dom remove-refsize0(gstore) ∩ ginval = ∅ ⊦ ⟪index_commit#(maxino, fi, syn; ginval0, ginval, gstore, fi0, gstore0, nx, maxino0, ginval1; err)⟫ (inv-journal(nx, gstore, gstore0, ginval) ∧ ri-inj(fi0)) | A Proof Obligation |
| inv-requires-commit | inv-journal(nx, gstore, gstore0, ginval), ri-inj(fi), ri-inj(fi0) ⊦ ⟪index_requires_commit#(fi, fi0, ginval, gstore, gstore0, nx, maxino, ginval0, syn; ; syn0)⟫ true | A Proof Obligation |
| inv-recovery | ginval = ginval0, gstore = crash(gstore0, gstore1, ginval0, nx), gstore2 = gstore1, nx0 = nx, maxino = maxino0, ginval1 = ginval2, fi = fi0, syn, inv-journal(nx, gstore0, gstore1, ginval0), ri-inj(fi1), ri-inj(fi0) ⊦ ⟪index_recover#(; maxino1, nx1, ginval3, fi, nx0, maxino, ginval1, ginval, gstore, gstore2; fi2, syn0, err)⟫ (err = ESUCCESS → syn0 ∧ inv-journal(nx0, gstore, gstore2, ginval) ∧ ri-inj(fi2) ∧ ri-inj(fi)) | A Proof Obligation |
| crash-neutral-requires-commit | inv-journal(nx, gstore, gstore0, ginval), ri-inj(fi), ri-inj(fi0), syn, ginval0 = ginval, gstore1 = crash(gstore, gstore0, ginval, nx), gstore2 = gstore0, nx0 = nx, maxino = maxino0, ginval1 = ginval2, fi1 = fi0 ⊦ ⟨index_requires_commit#(fi, fi0, ginval, gstore, gstore0, nx, maxino0, ginval2, syn; ; syn0)⟩ ( syn ∧ ginval0 = ginval ∧ gstore1 = crash(gstore, gstore0, ginval, nx) ∧ gstore2 = gstore0 ∧ nx0 = nx ∧ maxino = maxino0 ∧ ginval1 = ginval2 ∧ fi1 = fi0) | A Proof Obligation |
| crash-neutral-commit | syn, dom remove-refsize0(gstore) ∩ ginval = ∅, inv-journal(nx, gstore, gstore0, ginval), ri-inj(fi), ri-inj(fi0), syn, ginval0 = ginval, gstore1 = crash(gstore, gstore0, ginval, nx), gstore2 = gstore0, nx0 = nx, maxino = maxino0, ginval1 = ginval2, fi1 = fi0 ⊦ ⟨index_commit#(maxino1, fi, syn; ginval3, ginval, gstore, fi0, gstore0, nx, maxino0, ginval2; err)⟩ ( syn ∧ ginval0 = ginval ∧ gstore1 = crash(gstore, gstore0, ginval, nx) ∧ gstore2 = gstore0 ∧ nx0 = nx ∧ maxino = maxino0 ∧ ginval1 = ginval2 ∧ fi1 = fi0) | A Proof Obligation |
| crash-neutral-deallocate-gnd | syn, n ∈ gstore, ¬ n ∈ nx, inv-journal(nx, gstore, gstore0, ginval), ri-inj(fi), ri-inj(fi0), syn, ginval0 = ginval, gstore1 = crash(gstore, gstore0, ginval, nx), gstore2 = gstore0, nx0 = nx, maxino = maxino0, ginval1 = ginval2, fi1 = fi0 ⊦ ⟨index_deallocate_gnd#(n, fi, fi0, gstore0, nx, maxino0, ginval2, syn; ginval, gstore; err)⟩ ( syn ∧ ginval0 = ginval ∧ gstore1 = crash(gstore, gstore0, ginval, nx) ∧ gstore2 = gstore0 ∧ nx0 = nx ∧ maxino = maxino0 ∧ ginval1 = ginval2 ∧ fi1 = fi0) | A Proof Obligation |
| crash-neutral-allocate-gnd | syn, inv-journal(nx, gstore, gstore0, ginval), ri-inj(fi), ri-inj(fi0), syn, ginval0 = ginval, gstore1 = crash(gstore, gstore0, ginval, nx), gstore2 = gstore0, nx0 = nx, maxino = maxino0, ginval1 = ginval2, fi1 = fi0 ⊦ ⟨index_allocate_gnd#(fi, fi0, gstore0, maxino0, ginval2, syn; ginval, gstore, nx; err)⟩ ( syn ∧ ginval0 = ginval ∧ gstore1 = crash(gstore, gstore0, ginval, nx) ∧ gstore2 = gstore0 ∧ nx0 = nx ∧ maxino = maxino0 ∧ ginval1 = ginval2 ∧ fi1 = fi0) | A Proof Obligation |
| crash-neutral-get-gblock-refsize | maxino ∈ gstore, inv-journal(nx, gstore, gstore0, ginval), ri-inj(fi), ri-inj(fi0), syn, ginval0 = ginval, gstore1 = crash(gstore, gstore0, ginval, nx), gstore2 = gstore0, nx0 = nx, maxino0 = maxino1, ginval1 = ginval2, fi1 = fi0 ⊦ ⟨index_get_gblock_refsize#(maxino, fi, fi0, ginval, gstore, gstore0, nx, maxino1, ginval2, syn; ; n)⟩ ( syn ∧ ginval0 = ginval ∧ gstore1 = crash(gstore, gstore0, ginval, nx) ∧ gstore2 = gstore0 ∧ nx0 = nx ∧ maxino0 = maxino1 ∧ ginval1 = ginval2 ∧ fi1 = fi0) | A Proof Obligation |
| crash-neutral-set-gblock-refsize | maxino ∈ gstore, inv-journal(nx, gstore, gstore0, ginval), ri-inj(fi), ri-inj(fi0), syn, ginval0 = ginval, gstore1 = crash(gstore, gstore0, ginval, nx), gstore2 = gstore0, nx0 = nx, maxino0 = maxino1, ginval1 = ginval2, fi1 = fi0 ⊦ ⟨index_set_gblock_refsize#(maxino, n, fi, fi0, ginval, gstore0, nx, maxino1, ginval2, syn; gstore)⟩ ( syn ∧ ginval0 = ginval ∧ gstore1 = crash(gstore, gstore0, ginval, nx) ∧ gstore2 = gstore0 ∧ nx0 = nx ∧ maxino0 = maxino1 ∧ ginval1 = ginval2 ∧ fi1 = fi0) | A Proof Obligation |
| crash-neutral-get-gc-block | inv-journal(nx, gstore, gstore0, ginval), ri-inj(fi), ri-inj(fi0), syn, ginval0 = ginval, gstore1 = crash(gstore, gstore0, ginval, nx), gstore2 = gstore0, nx0 = nx, maxino = maxino0, ginval1 = ginval2, fi1 = fi0 ⊦ ⟨index_get_gc_block#(fi, fi0, ginval, gstore, gstore0, nx, maxino0, ginval2, syn; n; err)⟩ ( syn ∧ ginval0 = ginval ∧ gstore1 = crash(gstore, gstore0, ginval, nx) ∧ gstore2 = gstore0 ∧ nx0 = nx ∧ maxino = maxino0 ∧ ginval1 = ginval2 ∧ fi1 = fi0) | A Proof Obligation |
| crash-neutral-read-gblock | maxino ∈ gstore, ¬ maxino ∈ ginval, inv-journal(nx, gstore, gstore0, ginval), ri-inj(fi), ri-inj(fi0), syn, ginval0 = ginval, gstore1 = crash(gstore, gstore0, ginval, nx), gstore2 = gstore0, nx0 = nx, maxino0 = maxino1, ginval1 = ginval2, fi1 = fi0 ⊦ ⟨index_read_gblock_nodes#(maxino, fi, fi0, ginval, gstore, gstore0, nx, maxino1, ginval2, syn; ax, gndx; err)⟩ ( syn ∧ ginval0 = ginval ∧ gstore1 = crash(gstore, gstore0, ginval, nx) ∧ gstore2 = gstore0 ∧ nx0 = nx ∧ maxino0 = maxino1 ∧ ginval1 = ginval2 ∧ fi1 = fi0) | A Proof Obligation |
| crash-neutral-read-gnd | adr ∈ gstore, ¬ adr.lnum ∈ ginval, inv-journal(nx, gstore, gstore0, ginval), ri-inj(fi), ri-inj(fi0), syn, ginval0 = ginval, gstore1 = crash(gstore, gstore0, ginval, nx), gstore2 = gstore0, nx0 = nx, maxino = maxino0, ginval1 = ginval2, fi1 = fi0 ⊦ ⟨index_read_gnd#(adr, fi, fi0, ginval, gstore, gstore0, nx, maxino0, ginval2, syn; gnd; err)⟩ ( syn ∧ ginval0 = ginval ∧ gstore1 = crash(gstore, gstore0, ginval, nx) ∧ gstore2 = gstore0 ∧ nx0 = nx ∧ maxino = maxino0 ∧ ginval1 = ginval2 ∧ fi1 = fi0) | A Proof Obligation |
| crash-neutral-entries | inv-journal(nx, gstore, gstore0, ginval), ri-inj(fi), ri-inj(fi0), syn, ginval0 = ginval, gstore1 = crash(gstore, gstore0, ginval, nx), gstore2 = gstore0, nx0 = nx, maxino = maxino0, ginval1 = ginval2, fi1 = fi0 ⊦ ⟨index_index_entries#(key, fi, fi0, ginval, gstore, gstore0, nx, maxino0, ginval2, syn; strings; err)⟩ ( syn ∧ ginval0 = ginval ∧ gstore1 = crash(gstore, gstore0, ginval, nx) ∧ gstore2 = gstore0 ∧ nx0 = nx ∧ maxino = maxino0 ∧ ginval1 = ginval2 ∧ fi1 = fi0) | A Proof Obligation |
| crash-neutral-truncate | inv-journal(nx, gstore, gstore0, ginval), ri-inj(fi), ri-inj(fi0), syn, ginval0 = ginval, gstore1 = crash(gstore, gstore0, ginval, nx), gstore2 = gstore0, nx0 = nx, maxino = maxino0, ginval1 = ginval2, fi1 = fi0 ⊦ ⟨index_index_truncate#(key, n, fi0, ginval, gstore, gstore0, nx, maxino0, ginval2, syn; as, fi)⟩ ( syn ∧ ginval0 = ginval ∧ gstore1 = crash(gstore, gstore0, ginval, nx) ∧ gstore2 = gstore0 ∧ nx0 = nx ∧ maxino = maxino0 ∧ ginval1 = ginval2 ∧ fi1 = fi0) | A Proof Obligation |
| crash-neutral-remove | inv-journal(nx, gstore, gstore0, ginval), ri-inj(fi), ri-inj(fi0), syn, ginval0 = ginval, gstore1 = crash(gstore, gstore0, ginval, nx), gstore2 = gstore0, nx0 = nx, maxino = maxino0, ginval1 = ginval2, fi1 = fi0 ⊦ ⟨index_index_remove#(key, fi0, ginval, gstore, gstore0, nx, maxino0, ginval2, syn; adr, syn0, fi)⟩ ( syn ∧ ginval0 = ginval ∧ gstore1 = crash(gstore, gstore0, ginval, nx) ∧ gstore2 = gstore0 ∧ nx0 = nx ∧ maxino = maxino0 ∧ ginval1 = ginval2 ∧ fi1 = fi0) | A Proof Obligation |
| crash-neutral-store | ¬ adr ∈ fi, adr ∈ gstore, key-cons(key, gstore[adr].nd), inv-journal(nx, gstore, gstore0, ginval), ri-inj(fi), ri-inj(fi0), syn, ginval0 = ginval, gstore1 = crash(gstore, gstore0, ginval, nx), gstore2 = gstore0, nx0 = nx, maxino = maxino0, ginval1 = ginval2, fi1 = fi0 ⊦ ⟨index_index_store#(key, adr, fi0, ginval, gstore, gstore0, nx, maxino0, ginval2, syn; adr0, syn0, fi)⟩ ( syn ∧ ginval0 = ginval ∧ gstore1 = crash(gstore, gstore0, ginval, nx) ∧ gstore2 = gstore0 ∧ nx0 = nx ∧ maxino = maxino0 ∧ ginval1 = ginval2 ∧ fi1 = fi0) | A Proof Obligation |
| crash-neutral-lookup | inv-journal(nx, gstore, gstore0, ginval), ri-inj(fi), ri-inj(fi0), syn, ginval0 = ginval, gstore1 = crash(gstore, gstore0, ginval, nx), gstore2 = gstore0, nx0 = nx, maxino = maxino0, ginval1 = ginval2, fi1 = fi0 ⊦ ⟨index_index_lookup#(key, fi, fi0, ginval, gstore, gstore0, nx, maxino0, ginval2, syn; syn0, adr; err)⟩ ( syn ∧ ginval0 = ginval ∧ gstore1 = crash(gstore, gstore0, ginval, nx) ∧ gstore2 = gstore0 ∧ nx0 = nx ∧ maxino = maxino0 ∧ ginval1 = ginval2 ∧ fi1 = fi0) | A Proof Obligation |
| crash-neutral-contains | inv-journal(nx, gstore, gstore0, ginval), ri-inj(fi), ri-inj(fi0), syn, ginval0 = ginval, gstore1 = crash(gstore, gstore0, ginval, nx), gstore2 = gstore0, nx0 = nx, maxino = maxino0, ginval1 = ginval2, fi1 = fi0 ⊦ ⟨index_index_contains#(key, fi, fi0, ginval, gstore, gstore0, nx, maxino0, ginval2, syn; syn0; err)⟩ ( syn ∧ ginval0 = ginval ∧ gstore1 = crash(gstore, gstore0, ginval, nx) ∧ gstore2 = gstore0 ∧ nx0 = nx ∧ maxino = maxino0 ∧ ginval1 = ginval2 ∧ fi1 = fi0) | A Proof Obligation |
| crash-neutral-add-gnds | nx ≠ [], inv-journal(nx, gstore, gstore0, ginval), ri-inj(fi), ri-inj(fi0), syn, ginval0 = ginval, gstore1 = crash(gstore, gstore0, ginval, nx), gstore2 = gstore0, nx0 = nx, maxino = maxino0, ginval1 = ginval2, fi1 = fi0 ⊦ ⟨index_add_gnds#(gndx, fi, fi0, ginval, gstore0, nx, maxino0, ginval2; ax, gstore; syn, err)⟩ ( syn ∧ ginval0 = ginval ∧ gstore1 = crash(gstore, gstore0, ginval, nx) ∧ gstore2 = gstore0 ∧ nx0 = nx ∧ maxino = maxino0 ∧ ginval1 = ginval2 ∧ fi1 = fi0) | A Proof Obligation |
| inv-add-gnds | inv-journal(nx, gstore, gstore0, ginval), ri-inj(fi), ri-inj(fi0), nx ≠ [] ⊦ ⟪index_add_gnds#(gndx, fi, fi0, ginval, gstore0, nx, maxino, ginval0; ax, gstore; syn, err)⟫ inv-journal(nx, gstore, gstore0, ginval) | A Proof Obligation |
| crash-neutral-sync | inv-journal(nx, gstore, gstore0, ginval), ri-inj(fi), ri-inj(fi0), syn, ginval0 = ginval, gstore1 = crash(gstore, gstore0, ginval, nx), gstore2 = gstore0, nx0 = nx, maxino = maxino0, ginval1 = ginval2, fi1 = fi0 ⊦ ⟨index_sync#(fi, fi0, ginval, gstore, gstore0, nx, maxino0, ginval2; ; syn, err)⟩ ( syn ∧ ginval0 = ginval ∧ gstore1 = crash(gstore, gstore0, ginval, nx) ∧ gstore2 = gstore0 ∧ nx0 = nx ∧ maxino = maxino0 ∧ ginval1 = ginval2 ∧ fi1 = fi0) | A Proof Obligation |
| inv-sync | inv-journal(nx, gstore, gstore0, ginval), ri-inj(fi), ri-inj(fi0) ⊦ ⟪index_sync#(fi, fi0, ginval, gstore, gstore0, nx, maxino, ginval0; ; syn, err)⟫ true | A Proof Obligation |
| crash-neutral-get-block-free-size | inv-journal(nx, gstore, gstore0, ginval), ri-inj(fi), ri-inj(fi0), syn, ginval0 = ginval, gstore1 = crash(gstore, gstore0, ginval, nx), gstore2 = gstore0, nx0 = nx, maxino = maxino0, ginval1 = ginval2, fi1 = fi0 ⊦ ⟨index_get_block_free_size#(fi, fi0, ginval, gstore, gstore0, nx, maxino0, ginval2, syn; ; n)⟩ ( syn ∧ ginval0 = ginval ∧ gstore1 = crash(gstore, gstore0, ginval, nx) ∧ gstore2 = gstore0 ∧ nx0 = nx ∧ maxino = maxino0 ∧ ginval1 = ginval2 ∧ fi1 = fi0) | A Proof Obligation |
| inv-get-block-free-size | inv-journal(nx, gstore, gstore0, ginval), ri-inj(fi), ri-inj(fi0) ⊦ ⟪index_get_block_free_size#(fi, fi0, ginval, gstore, gstore0, nx, maxino, ginval0, syn; ; n)⟫ true | A Proof Obligation |
| inv-format | maxino = LEB_SIZE ⊦ ⟪index_format#(maxino0, maxino, maxino1; ; fi, fi0, ginval, gstore, gstore0, nx, maxino2, ginval0, syn, err)⟫ (err = ESUCCESS → syn ∧ inv-journal(nx, gstore, gstore0, ginval) ∧ ri-inj(fi) ∧ ri-inj(fi0)) | A Proof Obligation |
| crash-neutral-is-log-empty | inv-journal(nx, gstore, gstore0, ginval), ri-inj(fi), ri-inj(fi0), syn, ginval0 = ginval, gstore1 = crash(gstore, gstore0, ginval, nx), gstore2 = gstore0, nx0 = nx, maxino = maxino0, ginval1 = ginval2, fi1 = fi0 ⊦ ⟨index_is_log_empty#(fi, fi0, ginval, gstore, gstore0, nx, maxino0, ginval2, syn; ; syn0)⟩ ( syn ∧ ginval0 = ginval ∧ gstore1 = crash(gstore, gstore0, ginval, nx) ∧ gstore2 = gstore0 ∧ nx0 = nx ∧ maxino = maxino0 ∧ ginval1 = ginval2 ∧ fi1 = fi0) | A Proof Obligation |
| inv-is-log-empty | inv-journal(nx, gstore, gstore0, ginval), ri-inj(fi), ri-inj(fi0) ⊦ ⟪index_is_log_empty#(fi, fi0, ginval, gstore, gstore0, nx, maxino, ginval0, syn; ; syn0)⟫ true | A Proof Obligation |
| crash-neutral-recovery | inv-journal(nx, gstore, gstore0, ginval), ri-inj(fi), ri-inj(fi0), syn, ginval0 = ginval, gstore1 = crash(gstore, gstore0, ginval, nx), gstore2 = gstore0, nx0 = nx, maxino = maxino0, ginval1 = ginval2, fi1 = fi0 ⊦ ⟨index_recover#(; maxino1, nx1, ginval3, fi0, nx, maxino0, ginval2, ginval, gstore, gstore0; fi, syn, err)⟩ ( syn ∧ ginval0 = ginval ∧ gstore1 = crash(gstore, gstore0, ginval, nx) ∧ gstore2 = gstore0 ∧ nx0 = nx ∧ maxino = maxino0 ∧ ginval1 = ginval2 ∧ fi1 = fi0) | A Proof Obligation |
| crash-neutral-get-leb-size | inv-journal(nx, gstore, gstore0, ginval), ri-inj(fi), ri-inj(fi0), syn, ginval0 = ginval, gstore1 = crash(gstore, gstore0, ginval, nx), gstore2 = gstore0, nx0 = nx, maxino = maxino0, ginval1 = ginval2, fi1 = fi0 ⊦ ⟨index_get_leb_size(fi, fi0, ginval, gstore, gstore0, nx, maxino0, ginval2, syn; ; n)⟩ ( syn ∧ ginval0 = ginval ∧ gstore1 = crash(gstore, gstore0, ginval, nx) ∧ gstore2 = gstore0 ∧ nx0 = nx ∧ maxino = maxino0 ∧ ginval1 = ginval2 ∧ fi1 = fi0) | A Proof Obligation |
| inv-get-leb-size | inv-journal(nx, gstore, gstore0, ginval), ri-inj(fi), ri-inj(fi0) ⊦ ⟪index_get_leb_size(fi, fi0, ginval, gstore, gstore0, nx, maxino, ginval0, syn; ; n)⟫ true | A Proof Obligation |