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: |
|---|---|---|
| read-gnd | apersistence_read_gnd#(ADR, ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; GND; ERR) {if ADR ∈ GSTORE ∧ ¬ ADR.lnum ∈ GINVAL then {fail_or_success#(; ; ERR); if ERR = ESUCCESS then GND := GSTORE[ADR] else GND := ?} else abort} | An Axiom |
| read-ind | apersistence_read_ind#(ADR, ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; IND; ERR) {if ADR ∈ ISTORE then {fail_or_success#(; ; ERR); if ERR = ESUCCESS then IND := ISTORE[ADR] else IND := ?} else abort} | An Axiom |
| read-gblock | apersistence_read_gblock_nodes#(LNUM, ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; ADRLIST, GNDLIST; ERR) {if LNUM ∈ GSTORE ∧ ¬ LNUM ∈ GINVAL then {fail_or_success#(; ; ERR); if ERR = ESUCCESS then ADRLIST := ADRLIST + GSTORE[LNUM].ladrlist.to-adr(LNUM), GNDLIST := GNDLIST + GSTORE[LNUM].gndlist else ADRLIST := ?, GNDLIST := ?} else abort } | An Axiom |
| get-gc-block | apersistence_get_gc_block#(ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; N; ERR) {ERR := ENOSPC or choose N0 with N0 ∈ dom GSTORE ∧ ¬ N0 ∈ NL in {N := N0; ERR := ESUCCESS} ifnone ERR := ENOSPC} | An Axiom |
| add-ind | apersistence_add_ind#(IND, ROOTADR, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS; ADR, ISTORE, PSTATE, PSYNCED; ERR) {if PSTATE.index? ∨ PSTATE = readonly then if PSTATE = readonly then ERR := EROFS else {choose OFFSET, ERR0 with ¬ @(PSTATE.lnum, OFFSET, IND.flashsize) ∈ ISTORE ∧ ERR0 = ESUCCESS ∨ ⌊ERR0⌋ in ADR := @(PSTATE.lnum, OFFSET, IND.flashsize), ERR := ERR0; if ERR = ESUCCESS then {ISTORE[PSTATE.lnum].indlist := ISTORE[PSTATE.lnum].indlist + IND; ISTORE[PSTATE.lnum].ladrlist := ISTORE[PSTATE.lnum].ladrlist + @(ADR.pos, ADR.size)} else ADR := ?, PSTATE := readonly; PSYNCED := ?} else abort } | An Axiom |
| set-gblock-refsize | apersistence_set_gblock_refsize#(LNUM, N, ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; GSTORE) {if LNUM ∈ GSTORE then GSTORE[LNUM].ref-size := N else abort} | An Axiom |
| set-iblock-refsize | apersistence_set_iblock_refsize#(LNUM, N, ROOTADR, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; ISTORE) {if LNUM ∈ ISTORE then ISTORE[LNUM].ref-size := N else abort} | An Axiom |
| get-gblock-refsize | apersistence_get_gblock_refsize#(LNUM, ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; ; N) {if LNUM ∈ GSTORE then N := GSTORE[LNUM].ref-size else abort} | An Axiom |
| get-iblock-refsize | apersistence_get_iblock_refsize#(LNUM, ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; ; N) {if LNUM ∈ ISTORE then N := ISTORE[LNUM].ref-size else abort} | An Axiom |
| allocate-gnd | apersistence_allocate_gnd#(ROOTADR, ISTORE, ISTORE0, GSTORE0, MAXINO, OS, PSYNCED; GINVAL, GSTORE, NL, PSTATE; ERR) {if PSYNCED then if PSTATE = readonly then ERR := EROFS else {fail_or_success#(; ; ERR); if ERR = ESUCCESS then choose N with ¬ N ∈ GSTORE in GSTORE[N] := groupblock([], [], 0), NL := NL + N, GINVAL := GINVAL -- N, PSTATE := journal(N)} else abort } | An Axiom |
| deallocate-gnd | apersistence_deallocate_gnd#(N, ROOTADR, ISTORE, ISTORE0, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; GINVAL, GSTORE; ERR) {if PSYNCED ∧ N ∈ GSTORE ∧ ¬ N ∈ NL then {fail_or_success#(; ; ERR); if ERR = ESUCCESS then GSTORE := GSTORE -- N, GINVAL := GINVAL ++ N} else abort } | An Axiom |
| allocate-ind | apersistence_allocate_ind#(ROOTADR, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSYNCED; ISTORE, PSTATE; ERR) {if PSYNCED then {fail_or_success#(; ; ERR); if ERR = ESUCCESS then choose N with ¬ N ∈ ISTORE in ISTORE[N] := indexblock([], [], 0), PSTATE := index(N)} else abort } | An Axiom |
| requires-commit | apersistence_requires_commit#(ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; ; COMMIT?){COMMIT? := ?} | An Axiom |
| format | apersistence_format#(VOLSIZE, SIZE, MAXINO0; ; ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED, ERR) {if SIZE = LEB_SIZE then {fail_or_success#(; ; ERR); if ERR = ESUCCESS then PSTATE := unbuffered, PSYNCED := true, MAXINO := MAXINO0, OS := ∅, NL := [], GSTORE := ∅, GSTORE0 := ∅, ISTORE := ∅, ISTORE0 := ∅, GINVAL := ∅, ROOTADR := ? else PSTATE := ?, PSYNCED := ?, MAXINO := ?, OS := ?, NL := ?, GSTORE := ?, GSTORE0 := ?, ISTORE := ?, ISTORE0 := ?, GINVAL := ?, ROOTADR := ?} else abort } | An Axiom |
| recovery | apersistence_recover#(; ROOTADR0, MAXINO0, NL0, OS0, ROOTADR, NL, MAXINO, OS, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0; PSTATE, PSYNCED, ERR) {fail_or_success#(; ; ERR); if ERR = ESUCCESS then PSTATE := unbuffered, PSYNCED := true, ROOTADR0 := ROOTADR, MAXINO0 := MAXINO, NL0 := NL, OS0 := OS else PSTATE := ?, PSYNCED := ?, ROOTADR := ?, ISTORE := ?, ISTORE0 := ?, GINVAL := ?, GSTORE := ?, GSTORE0 := ?, NL := ?, MAXINO := ?, OS := ?, ROOTADR0 := ?, MAXINO0 := ?, NL0 := ?, OS0 := ? } | An Axiom |
| commit | apersistence_commit#(ROOTADR0, MAXINO0, PSYNCED; OS0, ISTORE, GINVAL, GSTORE, ROOTADR, ISTORE0, GSTORE0, NL, MAXINO, OS; PSTATE, ERR) {if PSYNCED ∧ dom remove-refsize0(GSTORE) ∩ GINVAL = ∅ then {fail_or_success#(; ; ERR); if ERR = ESUCCESS then {ISTORE := remove-refsize0(ISTORE); ISTORE0 := ISTORE; GSTORE := remove-refsize0(GSTORE); GSTORE0 := GSTORE; GINVAL := ∅; ROOTADR := ROOTADR0; OS := OS0; NL := []; MAXINO := MAXINO0; PSTATE := unbuffered} else PSTATE := readonly; OS0 := ?} else abort } | An Axiom |
| add-gnds | apersistence_add_gnds#(GNDLIST, ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE0, NL, MAXINO, OS; ADRLIST, GSTORE, PSTATE, PSYNCED; ERR) {if PSTATE.journal? ∨ PSTATE = readonly then if PSTATE = readonly then ERR := EROFS else {choose LADRLIST, ERR0 with (⌊ERR0⌋ ∨ ERR0 = ESUCCESS) ∧ ¬ dups(GSTORE[PSTATE.lnum].ladrlist + LADRLIST) ∧ # LADRLIST ≤ # GNDLIST ∧ inv-flashsize(prefixn(# LADRLIST, GNDLIST), LADRLIST) ∧ (ERR0 = ESUCCESS ↔ # LADRLIST = # GNDLIST) in {ADRLIST := LADRLIST.to-adr(PSTATE.lnum), ERR := ERR0; GSTORE[PSTATE.lnum].gndlist := GSTORE[PSTATE.lnum].gndlist + prefixn(# LADRLIST, GNDLIST); GSTORE[PSTATE.lnum].ladrlist := GSTORE[PSTATE.lnum].ladrlist + LADRLIST; if ERR ≠ ESUCCESS then ADRLIST := ?, PSTATE := readonly}; PSYNCED := ?} else abort } | An Axiom |
| sync | apersistence_sync#(ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS; PSTATE, PSYNCED; ERR) {if PSTATE = readonly then ERR := EROFS else if PSTATE = unbuffered then ERR := ESUCCESS else {fail_or_success#(; ; ERR); PSYNCED := ERR = ESUCCESS; skip or PSTATE := readonly} } | An Axiom |
| get-block-free-size | apersistence_get_block_free_size#(ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; ; N) {if PSTATE = unbuffered then N := 0 else choose N0 with N0 ≤ LEB_SIZE in N := N0} | An Axiom |
| is-log-empty | apersistence_is_log_empty#(ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; ; EMPTY?){EMPTY? := NL = []} | An Axiom |
| is-readonly | apersistence_is_readonly#(ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; ; ROFS){ROFS := PSTATE = readonly} | An Axiom |
| get-leb-size | apersistence_get_leb_size#(ROOTADR, ISTORE, ISTORE0, GINVAL, GSTORE, GSTORE0, NL, MAXINO, OS, PSTATE, PSYNCED; ; N){N := LEB_SIZE} | An Axiom |
| inv-format | maxino = LEB_SIZE ⊦ ⟪apersistence_format#(maxino0, maxino, maxino1; ; adr, istore, istore0, ginval, gstore, gstore0, nx, maxino2, ginval0, pstate, syn, err)⟫ (err = ESUCCESS → syn ∧ inv-journal(nx, gstore, gstore0, ginval) ∧ inv-index(istore, istore0) ∧ inv-state(pstate, nx, gstore, istore, syn)) | A Proof Obligation |
| inv-read-gnd | inv-journal(nx, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, nx, gstore, istore, syn), adr ∈ gstore, ¬ adr.lnum ∈ ginval ⊦ ⟪apersistence_read_gnd#(adr, adr0, istore, istore0, ginval, gstore, gstore0, nx, maxino, ginval0, pstate, syn; gnd; err)⟫ true | A Proof Obligation |
| inv-read-ind | inv-journal(nx, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, nx, gstore, istore, syn), adr ∈ istore ⊦ ⟪apersistence_read_ind#(adr, adr0, istore, istore0, ginval, gstore, gstore0, nx, maxino, ginval0, pstate, syn; ind; err)⟫ true | A Proof Obligation |
| inv-read-gblock | inv-journal(nx, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, nx, gstore, istore, syn), maxino ∈ gstore, ¬ maxino ∈ ginval ⊦ ⟪apersistence_read_gblock_nodes#(maxino, adr, istore, istore0, ginval, gstore, gstore0, nx, maxino0, ginval0, pstate, syn; ax, gndx; err)⟫ true | A Proof Obligation |
| inv-get-gc-block | inv-journal(nx, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, nx, gstore, istore, syn) ⊦ ⟪apersistence_get_gc_block#(adr, istore, istore0, ginval, gstore, gstore0, nx, maxino, ginval0, pstate, syn; n; err)⟫ true | A Proof Obligation |
| inv-add-ind | inv-journal(nx, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, nx, gstore, istore, syn), pstate.index? ∨ pstate = readonly ⊦ ⟪apersistence_add_ind#(ind, adr, istore0, ginval, gstore, gstore0, nx, maxino, ginval0; adr0, istore, pstate, syn; err)⟫ (inv-index(istore, istore0) ∧ inv-state(pstate, nx, gstore, istore, syn)) | A Proof Obligation |
| inv-set-gblock-refsize | inv-journal(nx, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, nx, gstore, istore, syn), maxino ∈ gstore ⊦ ⟪apersistence_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-set-iblock-refsize | inv-journal(nx, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, nx, gstore, istore, syn), maxino ∈ istore ⊦ ⟪apersistence_set_iblock_refsize#(maxino, n, adr, istore0, ginval, gstore, gstore0, nx, maxino0, ginval0, pstate, syn; istore)⟫ (inv-index(istore, istore0) ∧ inv-state(pstate, nx, gstore, istore, syn)) | A Proof Obligation |
| inv-get-gblock-refsize | inv-journal(nx, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, nx, gstore, istore, syn), maxino ∈ gstore ⊦ ⟪apersistence_get_gblock_refsize#(maxino, adr, istore, istore0, ginval, gstore, gstore0, nx, maxino0, ginval0, pstate, syn; ; n)⟫ true | A Proof Obligation |
| inv-get-iblock-refsize | inv-journal(nx, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, nx, gstore, istore, syn), maxino ∈ istore ⊦ ⟪apersistence_get_iblock_refsize#(maxino, adr, istore, istore0, ginval, gstore, gstore0, nx, maxino0, ginval0, pstate, syn; ; n)⟫ true | A Proof Obligation |
| inv-allocate-gnd | inv-journal(nx, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, nx, gstore, istore, syn), syn ⊦ ⟪apersistence_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-deallocate-gnd | inv-journal(nx, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, nx, gstore, istore, syn), syn, n ∈ gstore, ¬ n ∈ nx ⊦ ⟪apersistence_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-ind | inv-journal(nx, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, nx, gstore, istore, syn), syn ⊦ ⟪apersistence_allocate_ind#(adr, istore0, ginval, gstore, gstore0, nx, maxino, ginval0, syn; istore, pstate; err)⟫ (inv-index(istore, istore0) ∧ inv-state(pstate, nx, gstore, istore, syn)) | A Proof Obligation |
| inv-requires-commit | inv-journal(nx, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, nx, gstore, istore, syn) ⊦ ⟪apersistence_requires_commit#(adr, istore, istore0, ginval, gstore, gstore0, nx, maxino, ginval0, pstate, syn; ; syn0)⟫ true | A Proof Obligation |
| crash-neutral-requires-commit | inv-journal(nx, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, nx, gstore, istore, syn), syn, adr = adr0, istore1 = remove-refsize0(crash(istore, istore0)), istore2 = istore0, ginval0 = ginval, gstore1 = crash(gstore, gstore0, ginval, nx), gstore2 = gstore0, nx0 = nx, maxino = maxino0, ginval1 = ginval2 ⊦ ⟨apersistence_requires_commit#(adr0, istore, istore0, ginval, gstore, gstore0, nx, maxino0, ginval2, pstate, syn; ; syn0)⟩ ( syn ∧ adr = adr0 ∧ istore1 = remove-refsize0(crash(istore, istore0)) ∧ istore2 = istore0 ∧ ginval0 = ginval ∧ gstore1 = crash(gstore, gstore0, ginval, nx) ∧ gstore2 = gstore0 ∧ nx0 = nx ∧ maxino = maxino0 ∧ ginval1 = ginval2) | A Proof Obligation |
| crash-neutral-allocate-ind | syn, inv-journal(nx, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, nx, gstore, istore, syn), syn, adr = adr0, istore1 = remove-refsize0(crash(istore, istore0)), istore2 = istore0, ginval0 = ginval, gstore1 = crash(gstore, gstore0, ginval, nx), gstore2 = gstore0, nx0 = nx, maxino = maxino0, ginval1 = ginval2 ⊦ ⟨apersistence_allocate_ind#(adr0, istore0, ginval, gstore, gstore0, nx, maxino0, ginval2, syn; istore, pstate; err)⟩ ( syn ∧ adr = adr0 ∧ istore1 = remove-refsize0(crash(istore, istore0)) ∧ istore2 = istore0 ∧ ginval0 = ginval ∧ gstore1 = crash(gstore, gstore0, ginval, nx) ∧ gstore2 = gstore0 ∧ nx0 = nx ∧ maxino = maxino0 ∧ ginval1 = ginval2) | A Proof Obligation |
| crash-neutral-deallocate-gnd | syn, n ∈ gstore, ¬ n ∈ nx, inv-journal(nx, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, nx, gstore, istore, syn), syn, adr = adr0, istore1 = remove-refsize0(crash(istore, istore0)), istore2 = istore0, ginval0 = ginval, gstore1 = crash(gstore, gstore0, ginval, nx), gstore2 = gstore0, nx0 = nx, maxino = maxino0, ginval1 = ginval2 ⊦ ⟨apersistence_deallocate_gnd#(n, adr0, istore, istore0, gstore0, nx, maxino0, ginval2, pstate, syn; ginval, gstore; err)⟩ ( syn ∧ adr = adr0 ∧ istore1 = remove-refsize0(crash(istore, istore0)) ∧ istore2 = istore0 ∧ ginval0 = ginval ∧ gstore1 = crash(gstore, gstore0, ginval, nx) ∧ gstore2 = gstore0 ∧ nx0 = nx ∧ maxino = maxino0 ∧ ginval1 = ginval2) | A Proof Obligation |
| crash-neutral-allocate-gnd | syn, inv-journal(nx, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, nx, gstore, istore, syn), syn, adr = adr0, istore1 = remove-refsize0(crash(istore, istore0)), istore2 = istore0, ginval0 = ginval, gstore1 = crash(gstore, gstore0, ginval, nx), gstore2 = gstore0, nx0 = nx, maxino = maxino0, ginval1 = ginval2 ⊦ ⟨apersistence_allocate_gnd#(adr0, istore, istore0, gstore0, maxino0, ginval2, syn; ginval, gstore, nx, pstate; err)⟩ ( syn ∧ adr = adr0 ∧ istore1 = remove-refsize0(crash(istore, istore0)) ∧ istore2 = istore0 ∧ ginval0 = ginval ∧ gstore1 = crash(gstore, gstore0, ginval, nx) ∧ gstore2 = gstore0 ∧ nx0 = nx ∧ maxino = maxino0 ∧ ginval1 = ginval2) | A Proof Obligation |
| crash-neutral-get-iblock-refsize | maxino ∈ istore, inv-journal(nx, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, nx, gstore, istore, syn), syn, adr = adr0, istore1 = remove-refsize0(crash(istore, istore0)), istore2 = istore0, ginval0 = ginval, gstore1 = crash(gstore, gstore0, ginval, nx), gstore2 = gstore0, nx0 = nx, maxino0 = maxino1, ginval1 = ginval2 ⊦ ⟨apersistence_get_iblock_refsize#(maxino, adr0, istore, istore0, ginval, gstore, gstore0, nx, maxino1, ginval2, pstate, syn; ; n)⟩ ( syn ∧ adr = adr0 ∧ istore1 = remove-refsize0(crash(istore, istore0)) ∧ istore2 = istore0 ∧ ginval0 = ginval ∧ gstore1 = crash(gstore, gstore0, ginval, nx) ∧ gstore2 = gstore0 ∧ nx0 = nx ∧ maxino0 = maxino1 ∧ ginval1 = ginval2) | A Proof Obligation |
| crash-neutral-get-gblock-refsize | maxino ∈ gstore, inv-journal(nx, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, nx, gstore, istore, syn), syn, adr = adr0, istore1 = remove-refsize0(crash(istore, istore0)), istore2 = istore0, ginval0 = ginval, gstore1 = crash(gstore, gstore0, ginval, nx), gstore2 = gstore0, nx0 = nx, maxino0 = maxino1, ginval1 = ginval2 ⊦ ⟨apersistence_get_gblock_refsize#(maxino, adr0, istore, istore0, ginval, gstore, gstore0, nx, maxino1, ginval2, pstate, syn; ; n)⟩ ( syn ∧ adr = adr0 ∧ istore1 = remove-refsize0(crash(istore, istore0)) ∧ istore2 = istore0 ∧ ginval0 = ginval ∧ gstore1 = crash(gstore, gstore0, ginval, nx) ∧ gstore2 = gstore0 ∧ nx0 = nx ∧ maxino0 = maxino1 ∧ ginval1 = ginval2) | A Proof Obligation |
| crash-neutral-set-iblock-refsize | maxino ∈ istore, inv-journal(nx, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, nx, gstore, istore, syn), syn, adr = adr0, istore1 = remove-refsize0(crash(istore, istore0)), istore2 = istore0, ginval0 = ginval, gstore1 = crash(gstore, gstore0, ginval, nx), gstore2 = gstore0, nx0 = nx, maxino0 = maxino1, ginval1 = ginval2 ⊦ ⟨apersistence_set_iblock_refsize#(maxino, n, adr0, istore0, ginval, gstore, gstore0, nx, maxino1, ginval2, pstate, syn; istore)⟩ ( syn ∧ adr = adr0 ∧ istore1 = remove-refsize0(crash(istore, istore0)) ∧ istore2 = istore0 ∧ ginval0 = ginval ∧ gstore1 = crash(gstore, gstore0, ginval, nx) ∧ gstore2 = gstore0 ∧ nx0 = nx ∧ maxino0 = maxino1 ∧ ginval1 = ginval2) | A Proof Obligation |
| crash-neutral-set-gblock-refsize | maxino ∈ gstore, inv-journal(nx, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, nx, gstore, istore, syn), syn, adr = adr0, istore1 = remove-refsize0(crash(istore, istore0)), istore2 = istore0, ginval0 = ginval, gstore1 = crash(gstore, gstore0, ginval, nx), gstore2 = gstore0, nx0 = nx, maxino0 = maxino1, ginval1 = ginval2 ⊦ ⟨apersistence_set_gblock_refsize#(maxino, n, adr0, istore, istore0, ginval, gstore0, nx, maxino1, ginval2, pstate, syn; gstore)⟩ ( syn ∧ adr = adr0 ∧ istore1 = remove-refsize0(crash(istore, istore0)) ∧ istore2 = istore0 ∧ ginval0 = ginval ∧ gstore1 = crash(gstore, gstore0, ginval, nx) ∧ gstore2 = gstore0 ∧ nx0 = nx ∧ maxino0 = maxino1 ∧ ginval1 = ginval2) | A Proof Obligation |
| crash-neutral-add-ind | pstate.index? ∨ pstate = readonly, inv-journal(nx, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, nx, gstore, istore, syn), syn, adr = adr0, istore1 = remove-refsize0(crash(istore, istore0)), istore2 = istore0, ginval0 = ginval, gstore1 = crash(gstore, gstore0, ginval, nx), gstore2 = gstore0, nx0 = nx, maxino = maxino0, ginval1 = ginval2 ⊦ ⟨apersistence_add_ind#(ind, adr0, istore0, ginval, gstore, gstore0, nx, maxino0, ginval2; adr1, istore, pstate, syn; err)⟩ ( syn ∧ adr = adr0 ∧ istore1 = remove-refsize0(crash(istore, istore0)) ∧ istore2 = istore0 ∧ ginval0 = ginval ∧ gstore1 = crash(gstore, gstore0, ginval, nx) ∧ gstore2 = gstore0 ∧ nx0 = nx ∧ maxino = maxino0 ∧ ginval1 = ginval2) | A Proof Obligation |
| crash-neutral-get-gc-block | inv-journal(nx, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, nx, gstore, istore, syn), syn, adr = adr0, istore1 = remove-refsize0(crash(istore, istore0)), istore2 = istore0, ginval0 = ginval, gstore1 = crash(gstore, gstore0, ginval, nx), gstore2 = gstore0, nx0 = nx, maxino = maxino0, ginval1 = ginval2 ⊦ ⟨apersistence_get_gc_block#(adr0, istore, istore0, ginval, gstore, gstore0, nx, maxino0, ginval2, pstate, syn; n; err)⟩ ( syn ∧ adr = adr0 ∧ istore1 = remove-refsize0(crash(istore, istore0)) ∧ istore2 = istore0 ∧ ginval0 = ginval ∧ gstore1 = crash(gstore, gstore0, ginval, nx) ∧ gstore2 = gstore0 ∧ nx0 = nx ∧ maxino = maxino0 ∧ ginval1 = ginval2) | A Proof Obligation |
| crash-neutral-read-gblock | maxino ∈ gstore, ¬ maxino ∈ ginval, inv-journal(nx, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, nx, gstore, istore, syn), syn, adr = adr0, istore1 = remove-refsize0(crash(istore, istore0)), istore2 = istore0, ginval0 = ginval, gstore1 = crash(gstore, gstore0, ginval, nx), gstore2 = gstore0, nx0 = nx, maxino0 = maxino1, ginval1 = ginval2 ⊦ ⟨apersistence_read_gblock_nodes#(maxino, adr0, istore, istore0, ginval, gstore, gstore0, nx, maxino1, ginval2, pstate, syn; ax, gndx; err)⟩ ( syn ∧ adr = adr0 ∧ istore1 = remove-refsize0(crash(istore, istore0)) ∧ istore2 = istore0 ∧ ginval0 = ginval ∧ gstore1 = crash(gstore, gstore0, ginval, nx) ∧ gstore2 = gstore0 ∧ nx0 = nx ∧ maxino0 = maxino1 ∧ ginval1 = ginval2) | A Proof Obligation |
| crash-neutral-read-ind | adr ∈ istore, inv-journal(nx, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, nx, gstore, istore, syn), syn, adr0 = adr1, istore1 = remove-refsize0(crash(istore, istore0)), istore2 = istore0, ginval0 = ginval, gstore1 = crash(gstore, gstore0, ginval, nx), gstore2 = gstore0, nx0 = nx, maxino = maxino0, ginval1 = ginval2 ⊦ ⟨apersistence_read_ind#(adr, adr1, istore, istore0, ginval, gstore, gstore0, nx, maxino0, ginval2, pstate, syn; ind; err)⟩ ( syn ∧ adr0 = adr1 ∧ istore1 = remove-refsize0(crash(istore, istore0)) ∧ istore2 = istore0 ∧ ginval0 = ginval ∧ gstore1 = crash(gstore, gstore0, ginval, nx) ∧ gstore2 = gstore0 ∧ nx0 = nx ∧ maxino = maxino0 ∧ ginval1 = ginval2) | A Proof Obligation |
| crash-neutral-read-gnd | adr ∈ gstore, ¬ adr.lnum ∈ ginval, inv-journal(nx, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, nx, gstore, istore, syn), syn, adr0 = adr1, istore1 = remove-refsize0(crash(istore, istore0)), istore2 = istore0, ginval0 = ginval, gstore1 = crash(gstore, gstore0, ginval, nx), gstore2 = gstore0, nx0 = nx, maxino = maxino0, ginval1 = ginval2 ⊦ ⟨apersistence_read_gnd#(adr, adr1, istore, istore0, ginval, gstore, gstore0, nx, maxino0, ginval2, pstate, syn; gnd; err)⟩ ( syn ∧ adr0 = adr1 ∧ istore1 = remove-refsize0(crash(istore, istore0)) ∧ istore2 = istore0 ∧ ginval0 = ginval ∧ gstore1 = crash(gstore, gstore0, ginval, nx) ∧ gstore2 = gstore0 ∧ nx0 = nx ∧ maxino = maxino0 ∧ ginval1 = ginval2) | A Proof Obligation |
| crash-neutral-commit | syn, dom remove-refsize0(gstore) ∩ ginval = ∅, inv-journal(nx, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, nx, gstore, istore, syn), syn, adr = adr0, istore1 = remove-refsize0(crash(istore, istore0)), istore2 = istore0, ginval0 = ginval, gstore1 = crash(gstore, gstore0, ginval, nx), gstore2 = gstore0, nx0 = nx, maxino = maxino0, ginval1 = ginval2 ⊦ ⟨apersistence_commit#(adr1, maxino1, syn; ginval3, istore, ginval, gstore, adr0, istore0, gstore0, nx, maxino0, ginval2; pstate, err)⟩ ( syn ∧ adr = adr0 ∧ istore1 = remove-refsize0(crash(istore, istore0)) ∧ istore2 = istore0 ∧ ginval0 = ginval ∧ gstore1 = crash(gstore, gstore0, ginval, nx) ∧ gstore2 = gstore0 ∧ nx0 = nx ∧ maxino = maxino0 ∧ ginval1 = ginval2) | A Proof Obligation |
| inv-commit | inv-journal(nx, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, nx, gstore, istore, syn), syn, dom remove-refsize0(gstore) ∩ ginval = ∅ ⊦ ⟪apersistence_commit#(adr, maxino, syn; ginval0, istore, ginval, gstore, adr0, istore0, gstore0, nx, maxino0, ginval1; pstate, err)⟫ (inv-journal(nx, gstore, gstore0, ginval) ∧ inv-index(istore, istore0) ∧ inv-state(pstate, nx, gstore, istore, syn)) | A Proof Obligation |
| inv-recovery | 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, inv-journal(nx, gstore0, gstore1, ginval0), inv-index(istore0, istore1), inv-state(pstate, nx, gstore0, istore0, syn) ⊦ ⟪apersistence_recover#(; adr1, maxino1, nx1, ginval3, adr, nx0, maxino, ginval1, istore, istore2, ginval, gstore, gstore2; pstate0, syn0, err)⟫ (err = ESUCCESS → syn0 ∧ inv-journal(nx0, gstore, gstore2, ginval) ∧ inv-index(istore, istore2) ∧ inv-state(pstate0, nx0, gstore, istore, syn0)) | A Proof Obligation |
| crash-neutral-add-gnds | pstate.journal? ∨ pstate = readonly, inv-journal(nx, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, nx, gstore, istore, syn), syn, adr = adr0, istore1 = remove-refsize0(crash(istore, istore0)), istore2 = istore0, ginval0 = ginval, gstore1 = crash(gstore, gstore0, ginval, nx), gstore2 = gstore0, nx0 = nx, maxino = maxino0, ginval1 = ginval2 ⊦ ⟨apersistence_add_gnds#(gndx, adr0, istore, istore0, ginval, gstore0, nx, maxino0, ginval2; ax, gstore, pstate, syn; err)⟩ ( syn ∧ adr = adr0 ∧ istore1 = remove-refsize0(crash(istore, istore0)) ∧ istore2 = istore0 ∧ ginval0 = ginval ∧ gstore1 = crash(gstore, gstore0, ginval, nx) ∧ gstore2 = gstore0 ∧ nx0 = nx ∧ maxino = maxino0 ∧ ginval1 = ginval2) | A Proof Obligation |
| inv-add-gnds | inv-journal(nx, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, nx, gstore, istore, syn), pstate.journal? ∨ pstate = readonly ⊦ ⟪apersistence_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 |
| crash-neutral-sync | inv-journal(nx, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, nx, gstore, istore, syn), syn, adr = adr0, istore1 = remove-refsize0(crash(istore, istore0)), istore2 = istore0, ginval0 = ginval, gstore1 = crash(gstore, gstore0, ginval, nx), gstore2 = gstore0, nx0 = nx, maxino = maxino0, ginval1 = ginval2 ⊦ ⟨apersistence_sync#(adr0, istore, istore0, ginval, gstore, gstore0, nx, maxino0, ginval2; pstate, syn; err)⟩ ( syn ∧ adr = adr0 ∧ istore1 = remove-refsize0(crash(istore, istore0)) ∧ istore2 = istore0 ∧ ginval0 = ginval ∧ gstore1 = crash(gstore, gstore0, ginval, nx) ∧ gstore2 = gstore0 ∧ nx0 = nx ∧ maxino = maxino0 ∧ ginval1 = ginval2) | A Proof Obligation |
| inv-sync | inv-journal(nx, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, nx, gstore, istore, syn) ⊦ ⟪apersistence_sync#(adr, istore, istore0, ginval, gstore, gstore0, nx, maxino, ginval0; pstate, syn; err)⟫ inv-state(pstate, nx, gstore, istore, syn) | A Proof Obligation |
| crash-neutral-get-block-free-size | inv-journal(nx, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, nx, gstore, istore, syn), syn, adr = adr0, istore1 = remove-refsize0(crash(istore, istore0)), istore2 = istore0, ginval0 = ginval, gstore1 = crash(gstore, gstore0, ginval, nx), gstore2 = gstore0, nx0 = nx, maxino = maxino0, ginval1 = ginval2 ⊦ ⟨apersistence_get_block_free_size#(adr0, istore, istore0, ginval, gstore, gstore0, nx, maxino0, ginval2, pstate, syn; ; n)⟩ ( syn ∧ adr = adr0 ∧ istore1 = remove-refsize0(crash(istore, istore0)) ∧ istore2 = istore0 ∧ ginval0 = ginval ∧ gstore1 = crash(gstore, gstore0, ginval, nx) ∧ gstore2 = gstore0 ∧ nx0 = nx ∧ maxino = maxino0 ∧ ginval1 = ginval2) | A Proof Obligation |
| inv-get-block-free-size | inv-journal(nx, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, nx, gstore, istore, syn) ⊦ ⟪apersistence_get_block_free_size#(adr, istore, istore0, ginval, gstore, gstore0, nx, maxino, ginval0, pstate, syn; ; n)⟫ true | A Proof Obligation |
| crash-neutral-is-log-empty | inv-journal(nx, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, nx, gstore, istore, syn), syn, adr = adr0, istore1 = remove-refsize0(crash(istore, istore0)), istore2 = istore0, ginval0 = ginval, gstore1 = crash(gstore, gstore0, ginval, nx), gstore2 = gstore0, nx0 = nx, maxino = maxino0, ginval1 = ginval2 ⊦ ⟨apersistence_is_log_empty#(adr0, istore, istore0, ginval, gstore, gstore0, nx, maxino0, ginval2, pstate, syn; ; syn0)⟩ ( syn ∧ adr = adr0 ∧ istore1 = remove-refsize0(crash(istore, istore0)) ∧ istore2 = istore0 ∧ ginval0 = ginval ∧ gstore1 = crash(gstore, gstore0, ginval, nx) ∧ gstore2 = gstore0 ∧ nx0 = nx ∧ maxino = maxino0 ∧ ginval1 = ginval2) | A Proof Obligation |
| inv-is-log-empty | inv-journal(nx, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, nx, gstore, istore, syn) ⊦ ⟪apersistence_is_log_empty#(adr, istore, istore0, ginval, gstore, gstore0, nx, maxino, ginval0, pstate, syn; ; syn0)⟫ true | A Proof Obligation |
| crash-neutral-is-readonly | inv-journal(nx, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, nx, gstore, istore, syn), syn, adr = adr0, istore1 = remove-refsize0(crash(istore, istore0)), istore2 = istore0, ginval0 = ginval, gstore1 = crash(gstore, gstore0, ginval, nx), gstore2 = gstore0, nx0 = nx, maxino = maxino0, ginval1 = ginval2 ⊦ ⟨apersistence_is_readonly#(adr0, istore, istore0, ginval, gstore, gstore0, nx, maxino0, ginval2, pstate, syn; ; syn0)⟩ ( syn ∧ adr = adr0 ∧ istore1 = remove-refsize0(crash(istore, istore0)) ∧ istore2 = istore0 ∧ ginval0 = ginval ∧ gstore1 = crash(gstore, gstore0, ginval, nx) ∧ gstore2 = gstore0 ∧ nx0 = nx ∧ maxino = maxino0 ∧ ginval1 = ginval2) | A Proof Obligation |
| inv-is-readonly | inv-journal(nx, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, nx, gstore, istore, syn) ⊦ ⟪apersistence_is_readonly#(adr, istore, istore0, ginval, gstore, gstore0, nx, maxino, ginval0, pstate, syn; ; syn0)⟫ true | A Proof Obligation |
| crash-neutral-recovery | inv-journal(nx, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, nx, gstore, istore, syn), syn, adr = adr0, istore1 = remove-refsize0(crash(istore, istore0)), istore2 = istore0, ginval0 = ginval, gstore1 = crash(gstore, gstore0, ginval, nx), gstore2 = gstore0, nx0 = nx, maxino = maxino0, ginval1 = ginval2 ⊦ ⟨apersistence_recover#(; adr1, maxino1, nx1, ginval3, adr0, nx, maxino0, ginval2, istore, istore0, ginval, gstore, gstore0; pstate, syn, err)⟩ ( syn ∧ adr = adr0 ∧ istore1 = remove-refsize0(crash(istore, istore0)) ∧ istore2 = istore0 ∧ ginval0 = ginval ∧ gstore1 = crash(gstore, gstore0, ginval, nx) ∧ gstore2 = gstore0 ∧ nx0 = nx ∧ maxino = maxino0 ∧ ginval1 = ginval2) | A Proof Obligation |
| crash-neutral-get-leb-size | inv-journal(nx, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, nx, gstore, istore, syn), syn, adr = adr0, istore1 = remove-refsize0(crash(istore, istore0)), istore2 = istore0, ginval0 = ginval, gstore1 = crash(gstore, gstore0, ginval, nx), gstore2 = gstore0, nx0 = nx, maxino = maxino0, ginval1 = ginval2 ⊦ ⟨apersistence_get_leb_size#(adr0, istore, istore0, ginval, gstore, gstore0, nx, maxino0, ginval2, pstate, syn; ; n)⟩ ( syn ∧ adr = adr0 ∧ istore1 = remove-refsize0(crash(istore, istore0)) ∧ istore2 = istore0 ∧ ginval0 = ginval ∧ gstore1 = crash(gstore, gstore0, ginval, nx) ∧ gstore2 = gstore0 ∧ nx0 = nx ∧ maxino = maxino0 ∧ ginval1 = ginval2) | A Proof Obligation |
| inv-get-leb-size | inv-journal(nx, gstore, gstore0, ginval), inv-index(istore, istore0), inv-state(pstate, nx, gstore, istore, syn) ⊦ ⟪apersistence_get_leb_size#(adr, istore, istore0, ginval, gstore, gstore0, nx, maxino, ginval0, pstate, syn; ; n)⟫ true | A Proof Obligation |