[Imprint][Data Privacy Statement][E-Mail]

Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Theorem base for Specification gjournal-asm

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:
newinogjournal_index_newino#(; KEY, JMAXINO){KEY := inodekey(JMAXINO); JMAXINO := JMAXINO + 1} An Axiom
containsgjournal_index_contains#(KEY, PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; EXISTS; ERR) {index_index_contains#(KEY, PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; EXISTS; ERR)} An Axiom
lookupgjournal_index_lookup#(KEY, PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; EXISTS, ND; ERR) {if ri-cons(PRI, nodes(PSTORE ↓, PINVAL)) then let ADR = ? in {index_index_lookup#(KEY, PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; EXISTS, ADR; ERR); if ERR = ESUCCESS ∧ EXISTS then let GND = ? in {index_read_gnd#(ADR, PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; GND; ERR); if ERR = ESUCCESS then ND := GND.nd}} else abort } An Axiom
storegjournal_index_store#(KEY, ADR, PFI, PINVAL, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; JMAXINO, PRI, PSTORE) {if ¬ ADR ∈ PRI ∧ ADR ∈ PSTORE ∧ key-cons(KEY, PSTORE[ADR].nd) then let EXISTS = ?, OLDADR = ? in {index_index_store#(KEY, ADR, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; OLDADR, EXISTS, PRI); let N = ? in {if EXISTS then {index_get_gblock_refsize#(OLDADR.lnum, PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; ; N); index_set_gblock_refsize#(OLDADR.lnum, N - OLDADR.size, PRI, PFI, PINVAL, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; PSTORE)}; index_get_gblock_refsize#(ADR.lnum, PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; ; N); index_set_gblock_refsize#(ADR.lnum, N + ADR.size, PRI, PFI, PINVAL, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; PSTORE)}; JMAXINO := max(KEY.ino + 1, JMAXINO)} else abort } An Axiom
removegjournal_index_remove#(KEY, PFI, PINVAL, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; PRI, PSTORE) {let EXISTS = ?, OLDADR = ? in {index_index_remove#(KEY, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; OLDADR, EXISTS, PRI); if EXISTS then let N = ? in {index_get_gblock_refsize#(OLDADR.lnum, PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; ; N); index_set_gblock_refsize#(OLDADR.lnum, N - OLDADR.size, PRI, PFI, PINVAL, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; PSTORE)}} } An Axiom
truncategjournal_index_truncate#(KEY, N, JVALID, PFI, PINVAL, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; PRI, PSTORE) {let AS = ? in {index_index_truncate#(KEY, N, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; AS, PRI); gjournal_remove_addresses#(JVALID, PRI, PFI, PINVAL, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; AS, PSTORE)} } An Axiom
entriesgjournal_index_entries#(KEY, PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; NAMES; ERR) {index_index_entries#(KEY, PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; NAMES; ERR)} An Axiom
gcgjournal_journal_gc#(DOSYNC, PFI, PSTORE0, PMAXINO, P_OS; JVALID, SQNUM, JMAXINO, PRI, PINVAL, PSTORE, PNL, ISYNCED) {if ri-cons(PRI, nodes(PSTORE ↓, PINVAL)) then let LNUM = ?, ERR = ? in {index_get_gc_block#(PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; LNUM; ERR); if ERR = ESUCCESS then let N = ? in {debug#("gjournal: garbage collecting LEB " + LNUM.toString); index_get_gblock_refsize#(LNUM, PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; ; N); if N ≠ 0 then let ADRLIST = [], GNDLIST = [], NDLIST = [] in {index_read_gblock_nodes#(LNUM, PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; ADRLIST, GNDLIST; ERR); if ERR ≠ ESUCCESS then debug#("gjournal: failed to read LEB " + LNUM.toString + " during GC") else gjournal_gc_referenced_nodes# (LNUM, PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; ADRLIST, GNDLIST; NDLIST, ERR); if ERR = ESUCCESS then {gjournal_gc_copy# (DOSYNC, PFI, PSTORE0, PMAXINO, P_OS; NDLIST, JVALID, SQNUM, JMAXINO, PRI, PINVAL, PSTORE, PNL, ISYNCED; ERR); if ERR ≠ ESUCCESS then debug#("gjournal: failed to copy nodes of LEB " + LNUM.toString + " to journal head during GC")}}}; if ERR = ESUCCESS then index_sync#(PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS; ; ISYNCED, ERR); if ERR = ESUCCESS then index_deallocate_gnd#(LNUM, PRI, PFI, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; PINVAL, PSTORE; ERR)} else abort } An Axiom
recovergjournal_recover#(DOSYNC0; LOG, KS, JMAXINO, JRO, PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; JVALID, SQNUM, DOSYNC, ERR) {SQNUM := 0; JVALID := false; DOSYNC := DOSYNC0; let JNL = ? in {index_recover#(; JMAXINO, JNL, JRO, PFI, PNL, PMAXINO, P_OS, PINVAL, PSTORE, PSTORE0; PRI, ISYNCED, ERR); if ERR ≠ ESUCCESS then debug#("gjournal: persistence recover failed") else {gjournal_restore_log#(JNL, PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; LOG; ERR); KS := JRO.keys}} } An Axiom
restore-loggjournal_restore_log#(JNL, PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; LOG; ERR) {LOG := []; ERR := ESUCCESS; while JNL ≠ [] ∧ ERR = ESUCCESS do {/* (term-restore-log: invariant elems JNL ⊆ dom PSTORE ∧ elems JNL ∩ PINVAL = ∅ ∧ inv(PSTORE) wfbound # JNL) */; gjournal_remove_nonend_blocks#(JNL.head, PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; LOG; ERR); JNL := JNL.tail} } An Axiom
remove-nonend-blocksgjournal_remove_nonend_blocks#(LNUM, PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; LOG; ERR) {let GNDLIST = [], DONE = false in {index_read_gblock_nodes#(LNUM, PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; LOG, GNDLIST; ERR); if ERR = ESUCCESS then while ¬ DONE ∧ GNDLIST ≠ [] do {/* (term-remove-nonend-blocks: invariant # GNDLIST ≤ # LOG ∧ inv(PSTORE) wfbound (DONE ⊃ 0;# GNDLIST)) */; if GNDLIST.last.end then DONE := true else {LOG := LOG.butlast; GNDLIST := GNDLIST.butlast}}} } An Axiom
check-commitgjournal_check_commit#(JMAXINO, JRO, PRI; PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; ERR) {if dom remove-refsize0(PSTORE) ∩ PINVAL = ∅ ∧ PRI.lebs ⊆ dom remove-refsize0(PSTORE) then let COMMIT? = false in {index_requires_commit#(PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; ; COMMIT?); if COMMIT? then gjournal_commit#(JMAXINO, JRO, PRI; PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; ERR) else ERR := ESUCCESS} else abort } An Axiom
commitgjournal_commit#(JMAXINO, JRO, PRI; PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; ERR) {if dom remove-refsize0(PSTORE) ∩ PINVAL = ∅ ∧ PRI.lebs ⊆ dom remove-refsize0(PSTORE) then {index_sync#(PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS; ; ISYNCED, ERR); if ERR = ESUCCESS then let JRO0 = JRO in index_commit#(JMAXINO, PRI, ISYNCED; JRO0, PINVAL, PSTORE, PFI, PSTORE0, PNL, PMAXINO, P_OS; ERR)} else abort } An Axiom
formatgjournal_format#(VOLSIZE, SIZE, DOSYNC0; JMAXINO, PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; JVALID, SQNUM, JRO, DOSYNC, ERR) {if SIZE = LEB_SIZE then {JMAXINO := ROOT_INO + 1; SQNUM := 0; JVALID := true; DOSYNC := DOSYNC0; index_format#(VOLSIZE, SIZE, JMAXINO; ; PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED, ERR); if ERR ≠ ESUCCESS then debug#("gjournal: persistence format failed"); JRO := ∅} else abort } An Axiom
orphans-containsgjournal_orphans_contains#(KEY, JRO; EXISTS){if KEY.inode? then EXISTS := KEY.ino ∈ JRO else abort} An Axiom
orphans-insertgjournal_orphans_insert#(KEY; JMAXINO, JRO){if KEY.inode? then {JRO := JRO ++ KEY.ino; JMAXINO := max(KEY.ino + 1, JMAXINO)} else abort} An Axiom
orphans-removegjournal_orphans_remove#(KEY; JRO){if KEY.inode? then JRO := JRO -- KEY.ino else abort} An Axiom
add4gjournal_journal_add4# (ND1, ND2, ND3, ND4, DOSYNC, PRI, PFI, PSTORE0, PMAXINO, P_OS; ADR1, ADR2, ADR3, ADR4, JVALID, SQNUM, PINVAL, PSTORE, PNL, ISYNCED; ERR) {let NDLIST = ND1 + ND2 + ND3 + ND4 ', ADRLIST = ? in {gjournal_journal_addn#(NDLIST, DOSYNC, PRI, PFI, PSTORE0, PMAXINO, P_OS; ADRLIST, JVALID, SQNUM, PINVAL, PSTORE, PNL, ISYNCED; ERR); if ERR = ESUCCESS then {ADR1 := ADRLIST[0]; ADR2 := ADRLIST[1]; ADR3 := ADRLIST[2]; ADR4 := ADRLIST[3]}} } An Axiom
add3gjournal_journal_add3# (ND1, ND2, ND3, DOSYNC, PRI, PFI, PSTORE0, PMAXINO, P_OS; ADR1, ADR2, ADR3, JVALID, SQNUM, PINVAL, PSTORE, PNL, ISYNCED; ERR) {let NDLIST = ND1 + ND2 + ND3 ', ADRLIST = ? in {gjournal_journal_addn#(NDLIST, DOSYNC, PRI, PFI, PSTORE0, PMAXINO, P_OS; ADRLIST, JVALID, SQNUM, PINVAL, PSTORE, PNL, ISYNCED; ERR); if ERR = ESUCCESS then {ADR1 := ADRLIST[0]; ADR2 := ADRLIST[1]; ADR3 := ADRLIST[2]}} } An Axiom
add2gjournal_journal_add2#(ND1, ND2, DOSYNC, PRI, PFI, PSTORE0, PMAXINO, P_OS; ADR1, ADR2, JVALID, SQNUM, PINVAL, PSTORE, PNL, ISYNCED; ERR) {let NDLIST = ND1 + ND2 ', ADRLIST = ? in {gjournal_journal_addn#(NDLIST, DOSYNC, PRI, PFI, PSTORE0, PMAXINO, P_OS; ADRLIST, JVALID, SQNUM, PINVAL, PSTORE, PNL, ISYNCED; ERR); if ERR = ESUCCESS then {ADR1 := ADRLIST[0]; ADR2 := ADRLIST[1]}} } An Axiom
add1gjournal_journal_add1#(ND1, DOSYNC, PRI, PFI, PSTORE0, PMAXINO, P_OS; ADR1, JVALID, SQNUM, PINVAL, PSTORE, PNL, ISYNCED; ERR) {let NDLIST = ND1 ', ADRLIST = ? in {gjournal_journal_addn#(NDLIST, DOSYNC, PRI, PFI, PSTORE0, PMAXINO, P_OS; ADRLIST, JVALID, SQNUM, PINVAL, PSTORE, PNL, ISYNCED; ERR); if ERR = ESUCCESS then ADR1 := ADRLIST[0]} } An Axiom
allocategjournal_journal_allocate#(SIZE, PRI, PFI, PSTORE0, PMAXINO, P_OS; JVALID, PINVAL, PSTORE, PNL, ISYNCED; ERR) {let N = ? in {index_get_leb_size(PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; ; N); if SIZE > N then ERR := ENOSPC else let N = ?, EMPTY? = ? in {index_is_log_empty#(PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; ; EMPTY?); if ¬ EMPTY? ∧ JVALID then index_get_block_free_size#(PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; ; N); if ¬ EMPTY? ∧ JVALID ∧ SIZE ≤ N then ERR := ESUCCESS else {index_sync#(PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS; ; ISYNCED, ERR); if ERR = ESUCCESS then index_allocate_gnd#(PRI, PFI, PSTORE0, PMAXINO, P_OS, ISYNCED; PINVAL, PSTORE, PNL; ERR); if ERR = ESUCCESS then JVALID := true}}} } An Axiom
getgjournal_journal_get#(ADR, PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; ND; ERR) {if ADR ∈ PSTORE ∧ ¬ ADR.lnum ∈ PINVAL then choose GND with true in {index_read_gnd#(ADR, PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; GND; ERR); if ERR = ESUCCESS then ND := GND.nd} else abort } An Axiom
addngjournal_journal_addn#(NDLIST, DOSYNC, PRI, PFI, PSTORE0, PMAXINO, P_OS; ADRLIST, JVALID, SQNUM, PINVAL, PSTORE, PNL, ISYNCED; ERR) {let GNDLIST = ?, SIZE = ? in {gjournal_journal_transaction#(NDLIST, SQNUM; ; GNDLIST, SIZE); gjournal_journal_allocate#(SIZE, PRI, PFI, PSTORE0, PMAXINO, P_OS; JVALID, PINVAL, PSTORE, PNL, ISYNCED; ERR); if ERR = ESUCCESS then index_add_gnds#(GNDLIST, PRI, PFI, PINVAL, PSTORE0, PNL, PMAXINO, P_OS; ADRLIST, PSTORE; ISYNCED, ERR); if ERR = ESUCCESS then {SQNUM := SQNUM + # NDLIST; if DOSYNC then let ERR0 = ? in index_sync#(PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS; ; ISYNCED, ERR0)} else JVALID := false} } An Axiom
transactiongjournal_journal_transaction#(NDLIST, SQNUM; ; GNDLIST, SIZE) {SIZE := 0; GNDLIST := []; let FIRST? = true in while NDLIST ≠ [] do {/* (inv-transaction : invariant ∃ ndx. NDLIST` = ndx + NDLIST ∧ (NDLIST = [] → transaction(NDLIST`, GNDLIST)) ∧ (NDLIST ≠ [] → transaction-prefix(NDLIST`, GNDLIST) ∧ # GNDLIST = # ndx) ∧ SIZE = GNDLIST.flashsize ∧ (FIRST? ↔ ndx = []) wfbound # NDLIST) */; let LAST? = # NDLIST = 1 in let GND = mkgnode(NDLIST.head, SQNUM + # GNDLIST, FIRST?, LAST?) in {GNDLIST := GNDLIST + GND; SIZE := SIZE + GND.flashsize; NDLIST := NDLIST.tail; FIRST? := false}} } An Axiom
remove-addressesgjournal_remove_addresses#(JVALID, PRI, PFI, PINVAL, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; AS, PSTORE) {while AS ≠ ∅ do {/* (inv-truncate : invariant (JVALID ∧ PNL ≠ [] → valid-journal-head(PNL, PSTORE, PINVAL)) ∧ dom PSTORE = dom PSTORE` ∧ AS ∩ range PRI = ∅ ∧ AS.lebs ⊆ dom PSTORE ∧ refsize-cons(PSTORE, range PRI ∪ AS) ∧ inv-journal(PNL, PSTORE, PSTORE0, PINVAL) ∧ PSTORE =○refsize PSTORE` wfbound # AS) */; choose N, ADR with ADR ∈ AS in {index_get_gblock_refsize#(ADR.lnum, PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; ; N); index_set_gblock_refsize#(ADR.lnum, N - ADR.size, PRI, PFI, PINVAL, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; PSTORE); AS := AS -- ADR}} } An Axiom
gc-referenced-nodesgjournal_gc_referenced_nodes#(LNUM, PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; ADRLIST, GNDLIST; NDLIST, ERR) {ERR := ESUCCESS; NDLIST := []; while ERR = ESUCCESS ∧ ADRLIST ≠ [] do {/* (prepost-gc-referenced-nodes : invariant (ERR = ESUCCESS ∨ ⌊ERR⌋ ) ∧ ( ERR = ESUCCESS → (∃ ax0, gndx0. ADRLIST` = ax0 + ADRLIST ∧ GNDLIST` = gndx0 + GNDLIST ∧ # ADRLIST` = # GNDLIST` ∧ # ADRLIST = # GNDLIST ∧ NDLIST = nodes(PSTORE ↓, PINVAL)[referenced-adrs(ax0, PRI)])) wfbound (ERR = ESUCCESS ⊃ # ADRLIST;0)) */; let EXISTS = ?, ADR0 = ? in {let ADR = ADRLIST.head, GND = GNDLIST.head in let KEY = GND.nd.key in {index_index_lookup#(KEY, PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; EXISTS, ADR0; ERR); if ERR = ESUCCESS ∧ EXISTS ∧ ADR0 = ADR then NDLIST := NDLIST + GND.nd}; if ERR = ESUCCESS then {ADRLIST := ADRLIST.tail; GNDLIST := GNDLIST.tail}}} } An Axiom
gc-copygjournal_gc_copy#(DOSYNC, PFI, PSTORE0, PMAXINO, P_OS; NDLIST, JVALID, SQNUM, JMAXINO, PRI, PINVAL, PSTORE, PNL, ISYNCED; ERR) {if NDLIST.keys.toSet ⊆ dom PRI ∧ ¬ dups(NDLIST.keys) ∧ range PRI ⊆ dom nodes(PSTORE ↓, PINVAL) ∧ key-cons(NDLIST) then {ERR := ESUCCESS; while ERR = ESUCCESS ∧ NDLIST ≠ [] do {/* (inv-gc-copy : invariant (ERR = ESUCCESS ∨ ⌊ERR⌋ ) ∧ (∃ ndx0. NDLIST` = ndx0 + NDLIST) ∧ JMAXINO ≥ JMAXINO` ∧ (JVALID ∧ PNL ≠ [] → valid-journal-head(PNL, PSTORE, PINVAL)) ∧ PRI.inos < JMAXINO ∧ PRI.lebs ⊆ dom PSTORE ∧ refsize-cons(PSTORE, range PRI) ∧ inv-journal(PNL, PSTORE, PSTORE0, PINVAL) ∧ ri-inj(PRI) ∧ NDLIST.keys.toSet ⊆ dom PRI ∧ range PRI ⊆ dom nodes(PSTORE ↓, PINVAL) ∧ dom PSTORE` ⊆ dom PSTORE ∧ (PNL.toSet \ PNL`.toSet) ∩ dom PSTORE` = ∅ ∧ (∃ ax, ndx0, ndx1. NDLIST` = ndx0 + ndx1 ∧ (ERR = ESUCCESS → ndx1 = NDLIST) ∧ new(ax, nodes(PSTORE` ↓, PINVAL`)) ∧ ¬ dups(ax) ∧ # ax = # ndx0 ∧ PRI = (PRI`)[ndx0.keys, ax] ∧ nodes(PSTORE ↓, PINVAL) = nodes(PSTORE` ↓, PINVAL`)[ax, ndx0] ∧ abs-log(PNL, PSTORE ↓) = abs-log(PNL`, PSTORE` ↓) + ax) wfbound (ERR = ESUCCESS ⊃ # NDLIST;0)) */; let SIZE = 0, EMPTY? = ? in {index_is_log_empty#(PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; ; EMPTY?); if ¬ EMPTY? then {index_get_block_free_size#(PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; ; SIZE); if SIZE < NDLIST.head.flashsize then SIZE := 0}; let NDLIST0 = [], ADRLIST = [], N = ? in {index_get_leb_size(PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; ; N); gjournal_split_nodes#(N - SIZE; NDLIST, NDLIST0); if NDLIST0 = [] then ERR := EINVAL else {gjournal_journal_addn# (NDLIST0, DOSYNC, PRI, PFI, PSTORE0, PMAXINO, P_OS; ADRLIST, JVALID, SQNUM, PINVAL, PSTORE, PNL, ISYNCED; ERR); if ERR = ESUCCESS then gjournal_gc_update_index# (JVALID, PFI, PINVAL, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; ADRLIST, NDLIST0, JMAXINO, PRI, PSTORE)}}}}} else abort } An Axiom
gc-update-indexgjournal_gc_update_index#(JVALID, PFI, PINVAL, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; ADRLIST, NDLIST, JMAXINO, PRI, PSTORE) {if NDLIST.keys.toSet ⊆ dom PRI ∧ # ADRLIST = # NDLIST ∧ key-cons(NDLIST) ∧ ADRLIST.toSet ∩ range PRI = ∅ ∧ ¬ dups(ADRLIST) ∧ nodes-cons(ADRLIST, NDLIST, PSTORE, PINVAL) then while ADRLIST ≠ [] do {/* (inv-gc-update-index : invariant # ADRLIST` = # NDLIST` ∧ (∃ ax0, ndx0. # ax0 = # ndx0 ∧ ADRLIST` = ax0 + ADRLIST ∧ NDLIST` = ndx0 + NDLIST ∧ PRI = (PRI`)[ndx0.keys, ax0]) ∧ dom PRI = dom PRI` ∧ inv-journal(PNL, PSTORE, PSTORE0, PINVAL) ∧ JMAXINO` ≤ JMAXINO ∧ PRI.inos < JMAXINO ∧ refsize-cons(PSTORE, range PRI) ∧ ri-inj(PRI) ∧ PRI.lebs ⊆ dom PSTORE ∧ dom PSTORE = dom PSTORE` ∧ nodes-cons(ADRLIST, NDLIST, PSTORE, PINVAL) ∧ nodes(PSTORE ↓, PINVAL) = nodes(PSTORE` ↓, PINVAL`) ∧ abs-log(PNL, PSTORE ↓) = abs-log(PNL`, PSTORE` ↓) ∧ (JVALID ∧ PNL ≠ [] → valid-journal-head(PNL, PSTORE, PINVAL)) wfbound # ADRLIST) */; gjournal_index_store#(NDLIST.head.key, ADRLIST.head, PFI, PINVAL, PSTORE0, PNL, PMAXINO, P_OS, ISYNCED; JMAXINO, PRI, PSTORE); ADRLIST := ADRLIST.tail; NDLIST := NDLIST.tail} else abort } An Axiom
split-nodesgjournal_split_nodes#(SIZE; NDLIST, NDLIST0) {NDLIST0 := []; while NDLIST ≠ [] ∧ NDLIST.head.flashsize ≤ SIZE do {/* (prepost-split-nodes: invariant NDLIST` = NDLIST0 + NDLIST ∧ SIZE` = NDLIST0.flashsize + SIZE wfbound # NDLIST) */; let ND = NDLIST.head in {NDLIST0 := NDLIST0 + ND; NDLIST := NDLIST.tail; SIZE := SIZE - ND.flashsize}} } An Axiom
syncgjournal_journal_sync#(PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS; ISYNCED; ERR) {index_sync#(PRI, PFI, PINVAL, PSTORE, PSTORE0, PNL, PMAXINO, P_OS; ; ISYNCED, ERR)} An Axiom
add5gjournal_journal_add5# (ND1, ND2, ND3, ND4, ND5, DOSYNC, PRI, PFI, PSTORE0, PMAXINO, P_OS; ADR1, ADR2, ADR3, ADR4, ADR5, JVALID, SQNUM, PINVAL, PSTORE, PNL, ISYNCED; ERR) {let NDLIST = ND1 + ND2 + ND3 + ND4 + ND5 ', ADRLIST = ? in {gjournal_journal_addn#(NDLIST, DOSYNC, PRI, PFI, PSTORE0, PMAXINO, P_OS; ADRLIST, JVALID, SQNUM, PINVAL, PSTORE, PNL, ISYNCED; ERR); if ERR = ESUCCESS then {ADR1 := ADRLIST[0]; ADR2 := ADRLIST[1]; ADR3 := ADRLIST[2]; ADR4 := ADRLIST[3]; ADR5 := ADRLIST[4]}} } An Axiom
inv-formatjmaxino = LEB_SIZE ⊦ ⟪gjournal_format# (jmaxino0, jmaxino, jvalid; jmaxino1, fi, fi0, jro, gstore, gstore0, nx, pmaxino, p_os, jvalid0; jvalid1, jmaxino2, jro0, jvalid2, err)⟫ ( err = ESUCCESS → jvalid0 ∧ jro0 < jmaxino1 ∧ p_os < pmaxino ∧ pmaxino ≤ jmaxino1 ∧ fi.inos < jmaxino1 ∧ fi0.inos < pmaxino ∧ jmaxino1 ≠ 0 ∧ pmaxino ≠ 0 ∧ (jvalid1 ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro)) ∧ fi.lebs ⊆ dom gstore ∧ fi0.lebs ⊆ dom gstore0 ∧ refsize-cons(gstore, range fi) ∧ refsize-cons(gstore0, range fi0) ∧ inv-journal(nx, gstore, gstore0, jro) ∧ ri-inj(fi) ∧ ri-inj(fi0)) A Proof Obligation
inv-newinojro < jmaxino, pmaxino ≤ jmaxino, fi.inos < jmaxino, jmaxino ≠ 0 ⊦ ⟪gjournal_index_newino#(; key, jmaxino)⟫ (jro < jmaxino ∧ pmaxino ≤ jmaxino ∧ fi.inos < jmaxino ∧ jmaxino ≠ 0) A Proof Obligation
inv-containsp_os < pmaxino, pmaxino ≤ jmaxino, fi.inos < jmaxino, fi0.inos < pmaxino, pmaxino ≠ 0, jvalid ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro), fi.lebs ⊆ dom gstore, fi0.lebs ⊆ dom gstore0, refsize-cons(gstore, range fi), refsize-cons(gstore0, range fi0), inv-journal(nx, gstore, gstore0, jro), ri-inj(fi), ri-inj(fi0) ⊦ ⟪gjournal_index_contains#(key, fi, fi0, jro, gstore, gstore0, nx, pmaxino, p_os, jvalid0; jvalid1; err)⟫ true A Proof Obligation
inv-lookupp_os < pmaxino, pmaxino ≤ jmaxino, fi.inos < jmaxino, fi0.inos < pmaxino, pmaxino ≠ 0, jvalid ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro), fi.lebs ⊆ dom gstore, fi0.lebs ⊆ dom gstore0, refsize-cons(gstore, range fi), refsize-cons(gstore0, range fi0), inv-journal(nx, gstore, gstore0, jro), ri-inj(fi), ri-inj(fi0), ri-cons(fi, nodes(gstore ↓, jro)) ⊦ ⟪gjournal_index_lookup#(key, fi, fi0, jro, gstore, gstore0, nx, pmaxino, p_os, jvalid0; jvalid1, nd; err)⟫ true A Proof Obligation
inv-storejro < jmaxino, p_os < pmaxino, pmaxino ≤ jmaxino, fi.inos < jmaxino, fi0.inos < pmaxino, jmaxino ≠ 0, pmaxino ≠ 0, jvalid ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro0), fi.lebs ⊆ dom gstore, fi0.lebs ⊆ dom gstore0, refsize-cons(gstore, range fi), refsize-cons(gstore0, range fi0), inv-journal(nx, gstore, gstore0, jro0), ri-inj(fi), ri-inj(fi0), ¬ adr ∈ fi, adr ∈ gstore, key-cons(key, gstore[adr].nd), gstore1 = gstore, fi1 = fi ⊦ ⟪gjournal_index_store#(key, adr, fi0, jro0, gstore0, nx, pmaxino, p_os, jvalid0; jmaxino, fi, gstore)⟫ ( jro < jmaxino ∧ pmaxino ≤ jmaxino ∧ fi.inos < jmaxino ∧ jmaxino ≠ 0 ∧ (jvalid ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro0)) ∧ fi.lebs ⊆ dom gstore ∧ refsize-cons(gstore, range fi) ∧ inv-journal(nx, gstore, gstore0, jro0) ∧ ri-inj(fi) ∧ gstore =○refsize gstore1 ∧ fi = fi1[key, adr]) A Proof Obligation
inv-removep_os < pmaxino, pmaxino ≤ jmaxino, fi.inos < jmaxino, fi0.inos < pmaxino, pmaxino ≠ 0, jvalid ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro), fi.lebs ⊆ dom gstore, fi0.lebs ⊆ dom gstore0, refsize-cons(gstore, range fi), refsize-cons(gstore0, range fi0), inv-journal(nx, gstore, gstore0, jro), ri-inj(fi), ri-inj(fi0) ⊦ ⟪gjournal_index_remove#(key, fi0, jro, gstore0, nx, pmaxino, p_os, jvalid0; fi, gstore)⟫ ( fi.inos < jmaxino ∧ (jvalid ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro)) ∧ fi.lebs ⊆ dom gstore ∧ refsize-cons(gstore, range fi) ∧ inv-journal(nx, gstore, gstore0, jro) ∧ ri-inj(fi)) A Proof Obligation
inv-truncatep_os < pmaxino, pmaxino ≤ jmaxino, fi.inos < jmaxino, fi0.inos < pmaxino, pmaxino ≠ 0, jvalid ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro), fi.lebs ⊆ dom gstore, fi0.lebs ⊆ dom gstore0, refsize-cons(gstore, range fi), refsize-cons(gstore0, range fi0), inv-journal(nx, gstore, gstore0, jro), ri-inj(fi), ri-inj(fi0), gstore1 = gstore ⊦ ⟪gjournal_index_truncate#(key, n, jvalid, fi0, jro, gstore0, nx, pmaxino, p_os, jvalid0; fi, gstore)⟫ ( fi.inos < jmaxino ∧ (jvalid ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro)) ∧ fi.lebs ⊆ dom gstore ∧ refsize-cons(gstore, range fi) ∧ inv-journal(nx, gstore, gstore0, jro) ∧ ri-inj(fi) ∧ gstore =○refsize gstore1) A Proof Obligation
inv-entriesp_os < pmaxino, pmaxino ≤ jmaxino, fi.inos < jmaxino, fi0.inos < pmaxino, pmaxino ≠ 0, jvalid ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro), fi.lebs ⊆ dom gstore, fi0.lebs ⊆ dom gstore0, refsize-cons(gstore, range fi), refsize-cons(gstore0, range fi0), inv-journal(nx, gstore, gstore0, jro), ri-inj(fi), ri-inj(fi0) ⊦ ⟪gjournal_index_entries#(key, fi, fi0, jro, gstore, gstore0, nx, pmaxino, p_os, jvalid0; strings; err)⟫ true A Proof Obligation
inv-gcjro < jmaxino, p_os < pmaxino, pmaxino ≤ jmaxino, fi.inos < jmaxino, fi0.inos < pmaxino, jmaxino ≠ 0, pmaxino ≠ 0, jvalid ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro0), fi.lebs ⊆ dom gstore, fi0.lebs ⊆ dom gstore0, refsize-cons(gstore, range fi), refsize-cons(gstore0, range fi0), inv-journal(nx, gstore, gstore0, jro0), ri-inj(fi), ri-inj(fi0), ri-cons(fi, nodes(gstore ↓, jro0)) ⊦ ⟪gjournal_journal_gc#(jvalid0, fi0, gstore0, pmaxino, p_os; jvalid, jmaxino0, jmaxino, fi, jro0, gstore, nx, jvalid1)⟫ ( jro < jmaxino ∧ pmaxino ≤ jmaxino ∧ fi.inos < jmaxino ∧ jmaxino ≠ 0 ∧ (jvalid ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro0)) ∧ fi.lebs ⊆ dom gstore ∧ refsize-cons(gstore, range fi) ∧ inv-journal(nx, gstore, gstore0, jro0) ∧ ri-inj(fi)) A Proof Obligation
inv-recoverjro = jro0, gstore = crash(gstore0, gstore1, jro0, nx), gstore2 = gstore1, nx0 = nx, pmaxino = jmaxino, p_os = jro1, fi = fi0, jvalid, jro2 < jmaxino0, jro1 < jmaxino, jmaxino ≤ jmaxino0, fi1.inos < jmaxino0, fi0.inos < jmaxino, jmaxino0 ≠ 0, jmaxino ≠ 0, jvalid0 ∧ nx ≠ [] → valid-journal-head(nx, gstore0, jro0), fi1.lebs ⊆ dom gstore0, fi0.lebs ⊆ dom gstore1, refsize-cons(gstore0, range fi1), refsize-cons(gstore1, range fi0), inv-journal(nx, gstore0, gstore1, jro0), ri-inj(fi1), ri-inj(fi0) ⊦ ⟪gjournal_recover# (jvalid1; log, ks, jmaxino1, jro3, fi2, fi, jro, gstore, gstore2, nx0, pmaxino, p_os, jvalid2; jvalid3, jmaxino2, jvalid4, err)⟫ ( err = ESUCCESS → jvalid2 ∧ jro3 < jmaxino1 ∧ p_os < pmaxino ∧ pmaxino ≤ jmaxino1 ∧ fi2.inos < jmaxino1 ∧ fi.inos < pmaxino ∧ jmaxino1 ≠ 0 ∧ pmaxino ≠ 0 ∧ (jvalid3 ∧ nx0 ≠ [] → valid-journal-head(nx0, gstore, jro)) ∧ fi2.lebs ⊆ dom gstore ∧ fi.lebs ⊆ dom gstore2 ∧ refsize-cons(gstore, range fi2) ∧ refsize-cons(gstore2, range fi) ∧ inv-journal(nx0, gstore, gstore2, jro) ∧ ri-inj(fi2) ∧ ri-inj(fi)) A Proof Obligation
inv-check-commitjro < jmaxino, p_os < pmaxino, pmaxino ≤ jmaxino, fi.inos < jmaxino, fi0.inos < pmaxino, jmaxino ≠ 0, pmaxino ≠ 0, jvalid ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro0), fi.lebs ⊆ dom gstore, fi0.lebs ⊆ dom gstore0, refsize-cons(gstore, range fi), refsize-cons(gstore0, range fi0), inv-journal(nx, gstore, gstore0, jro0), ri-inj(fi), ri-inj(fi0), dom remove-refsize0(gstore) ∩ jro0 = ∅, fi.lebs ⊆ dom remove-refsize0(gstore) ⊦ ⟪gjournal_check_commit#(jmaxino, jro, fi; fi0, jro0, gstore, gstore0, nx, pmaxino, p_os, jvalid0; err)⟫ ( p_os < pmaxino ∧ pmaxino ≤ jmaxino ∧ fi0.inos < pmaxino ∧ pmaxino ≠ 0 ∧ (jvalid ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro0)) ∧ fi.lebs ⊆ dom gstore ∧ fi0.lebs ⊆ dom gstore0 ∧ refsize-cons(gstore, range fi) ∧ refsize-cons(gstore0, range fi0) ∧ inv-journal(nx, gstore, gstore0, jro0) ∧ ri-inj(fi0)) A Proof Obligation
inv-commitjro < jmaxino, p_os < pmaxino, pmaxino ≤ jmaxino, fi.inos < jmaxino, fi0.inos < pmaxino, jmaxino ≠ 0, pmaxino ≠ 0, jvalid ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro0), fi.lebs ⊆ dom gstore, fi0.lebs ⊆ dom gstore0, refsize-cons(gstore, range fi), refsize-cons(gstore0, range fi0), inv-journal(nx, gstore, gstore0, jro0), ri-inj(fi), ri-inj(fi0), dom remove-refsize0(gstore) ∩ jro0 = ∅, fi.lebs ⊆ dom remove-refsize0(gstore) ⊦ ⟪gjournal_commit#(jmaxino, jro, fi; fi0, jro0, gstore, gstore0, nx, pmaxino, p_os, jvalid0; err)⟫ ( p_os < pmaxino ∧ pmaxino ≤ jmaxino ∧ fi0.inos < pmaxino ∧ pmaxino ≠ 0 ∧ (jvalid ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro0)) ∧ fi.lebs ⊆ dom gstore ∧ fi0.lebs ⊆ dom gstore0 ∧ refsize-cons(gstore, range fi) ∧ refsize-cons(gstore0, range fi0) ∧ inv-journal(nx, gstore, gstore0, jro0) ∧ ri-inj(fi0)) A Proof Obligation
inv-orphans-containsjro < jmaxino, key.inode? ⊦ ⟪gjournal_orphans_contains#(key, jro; jvalid)⟫ true A Proof Obligation
inv-orphans-insertjro < jmaxino, pmaxino ≤ jmaxino, fi.inos < jmaxino, jmaxino ≠ 0, key.inode? ⊦ ⟪gjournal_orphans_insert#(key; jmaxino, jro)⟫ (jro < jmaxino ∧ pmaxino ≤ jmaxino ∧ fi.inos < jmaxino ∧ jmaxino ≠ 0) A Proof Obligation
inv-orphans-removejro < jmaxino, key.inode? ⊦ ⟪gjournal_orphans_remove#(key; jro)⟫ (jro < jmaxino) A Proof Obligation
inv-add4p_os < pmaxino, pmaxino ≤ jmaxino, fi.inos < jmaxino, fi0.inos < pmaxino, pmaxino ≠ 0, jvalid ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro), fi.lebs ⊆ dom gstore, fi0.lebs ⊆ dom gstore0, refsize-cons(gstore, range fi), refsize-cons(gstore0, range fi0), inv-journal(nx, gstore, gstore0, jro), ri-inj(fi), ri-inj(fi0) ⊦ ⟪gjournal_journal_add4# (nd, nd0, nd1, nd2, jvalid0, fi, fi0, gstore0, pmaxino, p_os; adr, adr0, adr1, adr2, jvalid, jmaxino0, jro, gstore, nx, jvalid1; err)⟫ ( (jvalid ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro)) ∧ fi.lebs ⊆ dom gstore ∧ refsize-cons(gstore, range fi) ∧ inv-journal(nx, gstore, gstore0, jro)) A Proof Obligation
inv-add3p_os < pmaxino, pmaxino ≤ jmaxino, fi.inos < jmaxino, fi0.inos < pmaxino, pmaxino ≠ 0, jvalid ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro), fi.lebs ⊆ dom gstore, fi0.lebs ⊆ dom gstore0, refsize-cons(gstore, range fi), refsize-cons(gstore0, range fi0), inv-journal(nx, gstore, gstore0, jro), ri-inj(fi), ri-inj(fi0) ⊦ ⟪gjournal_journal_add3# (nd, nd0, nd1, jvalid0, fi, fi0, gstore0, pmaxino, p_os; adr, adr0, adr1, jvalid, jmaxino0, jro, gstore, nx, jvalid1; err)⟫ ( (jvalid ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro)) ∧ fi.lebs ⊆ dom gstore ∧ refsize-cons(gstore, range fi) ∧ inv-journal(nx, gstore, gstore0, jro)) A Proof Obligation
inv-add2p_os < pmaxino, pmaxino ≤ jmaxino, fi.inos < jmaxino, fi0.inos < pmaxino, pmaxino ≠ 0, jvalid ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro), fi.lebs ⊆ dom gstore, fi0.lebs ⊆ dom gstore0, refsize-cons(gstore, range fi), refsize-cons(gstore0, range fi0), inv-journal(nx, gstore, gstore0, jro), ri-inj(fi), ri-inj(fi0) ⊦ ⟪gjournal_journal_add2#(nd, nd0, jvalid0, fi, fi0, gstore0, pmaxino, p_os; adr, adr0, jvalid, jmaxino0, jro, gstore, nx, jvalid1; err)⟫ ( (jvalid ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro)) ∧ fi.lebs ⊆ dom gstore ∧ refsize-cons(gstore, range fi) ∧ inv-journal(nx, gstore, gstore0, jro)) A Proof Obligation
inv-add1p_os < pmaxino, pmaxino ≤ jmaxino, fi.inos < jmaxino, fi0.inos < pmaxino, pmaxino ≠ 0, jvalid ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro), fi.lebs ⊆ dom gstore, fi0.lebs ⊆ dom gstore0, refsize-cons(gstore, range fi), refsize-cons(gstore0, range fi0), inv-journal(nx, gstore, gstore0, jro), ri-inj(fi), ri-inj(fi0) ⊦ ⟪gjournal_journal_add1#(nd, jvalid0, fi, fi0, gstore0, pmaxino, p_os; adr, jvalid, jmaxino0, jro, gstore, nx, jvalid1; err)⟫ ( (jvalid ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro)) ∧ fi.lebs ⊆ dom gstore ∧ refsize-cons(gstore, range fi) ∧ inv-journal(nx, gstore, gstore0, jro)) A Proof Obligation
inv-getp_os < pmaxino, pmaxino ≤ jmaxino, fi.inos < jmaxino, fi0.inos < pmaxino, pmaxino ≠ 0, jvalid ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro), fi.lebs ⊆ dom gstore, fi0.lebs ⊆ dom gstore0, refsize-cons(gstore, range fi), refsize-cons(gstore0, range fi0), inv-journal(nx, gstore, gstore0, jro), ri-inj(fi), ri-inj(fi0), adr ∈ gstore, ¬ adr.lnum ∈ jro ⊦ ⟪gjournal_journal_get#(adr, fi, fi0, jro, gstore, gstore0, nx, pmaxino, p_os, jvalid0; nd; err)⟫ true A Proof Obligation
inv-addnp_os < pmaxino, pmaxino ≤ jmaxino, fi.inos < jmaxino, fi0.inos < pmaxino, pmaxino ≠ 0, jvalid ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro), fi.lebs ⊆ dom gstore, fi0.lebs ⊆ dom gstore0, refsize-cons(gstore, range fi), refsize-cons(gstore0, range fi0), inv-journal(nx, gstore, gstore0, jro), ri-inj(fi), ri-inj(fi0), gstore1 = gstore, nx0 = nx, jro0 = jro ⊦ ⟪gjournal_journal_addn#(ndx, jvalid0, fi, fi0, gstore0, pmaxino, p_os; ax, jvalid, jmaxino0, jro, gstore, nx, jvalid1; err)⟫ ( (jvalid ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro)) ∧ fi.lebs ⊆ dom gstore ∧ refsize-cons(gstore, range fi) ∧ inv-journal(nx, gstore, gstore0, jro) ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ dom gstore1 ⊆ dom gstore ∧ (nx.toSet \ nx0.toSet) ∩ dom gstore1 = ∅ ∧ ( err = ESUCCESS → # ax = # ndx ∧ ¬ dups(ax) ∧ nodes-cons(ax, ndx, gstore, jro) ∧ abs-log(nx, gstore ↓) = abs-log(nx0, gstore1 ↓) + ax ∧ nodes(gstore ↓, jro) = nodes(gstore1 ↓, jro0)[ax, ndx] ∧ new(ax, nodes(gstore1 ↓, jro0))) ∧ (err ≠ ESUCCESS → abs-log(nx, gstore ↓) = abs-log(nx0, gstore1 ↓) ∧ nodes(gstore ↓, jro) = nodes(gstore1 ↓, jro0))) A Proof Obligation
inv-transaction ⊦ ⟪gjournal_journal_transaction#(ndx, jmaxino; ; gndx, jmaxino0)⟫ (transaction(ndx, gndx) ∧ jmaxino0 = gndx.flashsize) A Proof Obligation
inv-allocatep_os < pmaxino, pmaxino ≤ jmaxino, fi.inos < jmaxino, fi0.inos < pmaxino, pmaxino ≠ 0, jvalid ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro), fi.lebs ⊆ dom gstore, fi0.lebs ⊆ dom gstore0, refsize-cons(gstore, range fi), refsize-cons(gstore0, range fi0), inv-journal(nx, gstore, gstore0, jro), ri-inj(fi), ri-inj(fi0), gstore1 = gstore, nx0 = nx, jro0 = jro ⊦ ⟪gjournal_journal_allocate#(jmaxino0, fi, fi0, gstore0, pmaxino, p_os; jvalid, jro, gstore, nx, jvalid0; err)⟫ ( (jvalid ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro)) ∧ fi.lebs ⊆ dom gstore ∧ refsize-cons(gstore, range fi) ∧ inv-journal(nx, gstore, gstore0, jro) ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ dom gstore1 ⊆ dom gstore ∧ (nx.toSet \ nx0.toSet) ∩ dom gstore1 = ∅ ∧ abs-log(nx, gstore ↓) = abs-log(nx0, gstore1 ↓) ∧ nodes(gstore ↓, jro) = nodes(gstore1 ↓, jro0) ∧ (err = ESUCCESS → jvalid ∧ nx ≠ [])) A Proof Obligation
inv-gc-copyjro < jmaxino, p_os < pmaxino, pmaxino ≤ jmaxino, fi.inos < jmaxino, fi0.inos < pmaxino, jmaxino ≠ 0, pmaxino ≠ 0, jvalid ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro0), fi.lebs ⊆ dom gstore, fi0.lebs ⊆ dom gstore0, refsize-cons(gstore, range fi), refsize-cons(gstore0, range fi0), inv-journal(nx, gstore, gstore0, jro0), ri-inj(fi), ri-inj(fi0), ndx.keys.toSet ⊆ dom fi, ¬ dups(ndx.keys), range fi ⊆ dom nodes(gstore ↓, jro0), key-cons(ndx), jmaxino0 = jmaxino, gstore1 = gstore, nx0 = nx, ndx2 = ndx, jro1 = jro0, fi1 = fi ⊦ ⟪gjournal_gc_copy#(jvalid0, fi0, gstore0, pmaxino, p_os; ndx, jvalid, jmaxino1, jmaxino, fi, jro0, gstore, nx, jvalid1; err)⟫ ( jro < jmaxino ∧ pmaxino ≤ jmaxino ∧ fi.inos < jmaxino ∧ jmaxino ≠ 0 ∧ (jvalid ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro0)) ∧ fi.lebs ⊆ dom gstore ∧ refsize-cons(gstore, range fi) ∧ inv-journal(nx, gstore, gstore0, jro0) ∧ ri-inj(fi) ∧ (err = ESUCCESS ∨ ⌊err⌋ ) ∧ jmaxino0 ≤ jmaxino ∧ dom gstore1 ⊆ dom gstore ∧ (nx.toSet \ nx0.toSet) ∩ dom gstore1 = ∅ ∧ (∃ ax, ndx0, ndx1. ndx2 = ndx0 + ndx1 ∧ (err = ESUCCESS → ndx1 = []) ∧ new(ax, nodes(gstore1 ↓, jro1)) ∧ # ax = # ndx0 ∧ ¬ dups(ax) ∧ fi = fi1[ndx0.keys, ax] ∧ nodes(gstore ↓, jro0) = nodes(gstore1 ↓, jro1)[ax, ndx0] ∧ abs-log(nx, gstore ↓) = abs-log(nx0, gstore1 ↓) + ax)) A Proof Obligation
inv-gc-update-indexjro < jmaxino, p_os < pmaxino, pmaxino ≤ jmaxino, fi.inos < jmaxino, fi0.inos < pmaxino, jmaxino ≠ 0, pmaxino ≠ 0, jvalid ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro0), fi.lebs ⊆ dom gstore, fi0.lebs ⊆ dom gstore0, refsize-cons(gstore, range fi), refsize-cons(gstore0, range fi0), inv-journal(nx, gstore, gstore0, jro0), ri-inj(fi), ri-inj(fi0), ndx.keys.toSet ⊆ dom fi, # ax = # ndx, key-cons(ndx), ax.toSet ∩ range fi = ∅, ¬ dups(ax), nodes-cons(ax, ndx, gstore, jro0), fi1 = fi, ndx0 = ndx, ax0 = ax, gstore1 = gstore, jro1 = jro0, nx0 = nx, jmaxino0 = jmaxino ⊦ ⟪gjournal_gc_update_index#(jvalid, fi0, jro0, gstore0, nx, pmaxino, p_os, jvalid0; ax, ndx, jmaxino, fi, gstore)⟫ ( jro < jmaxino ∧ pmaxino ≤ jmaxino ∧ fi.inos < jmaxino ∧ jmaxino ≠ 0 ∧ (jvalid ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro0)) ∧ fi.lebs ⊆ dom gstore ∧ refsize-cons(gstore, range fi) ∧ inv-journal(nx, gstore, gstore0, jro0) ∧ ri-inj(fi) ∧ fi = fi1[ndx0.keys, ax0] ∧ dom gstore = dom gstore1 ∧ nodes(gstore ↓, jro0) = nodes(gstore1 ↓, jro1) ∧ abs-log(nx, gstore ↓) = abs-log(nx0, gstore1 ↓) ∧ jmaxino0 ≤ jmaxino) A Proof Obligation
inv-syncp_os < pmaxino, pmaxino ≤ jmaxino, fi.inos < jmaxino, fi0.inos < pmaxino, pmaxino ≠ 0, jvalid ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro), fi.lebs ⊆ dom gstore, fi0.lebs ⊆ dom gstore0, refsize-cons(gstore, range fi), refsize-cons(gstore0, range fi0), inv-journal(nx, gstore, gstore0, jro), ri-inj(fi), ri-inj(fi0) ⊦ ⟪gjournal_journal_sync#(fi, fi0, jro, gstore, gstore0, nx, pmaxino, p_os; jvalid0; err)⟫ true A Proof Obligation
inv-add5p_os < pmaxino, pmaxino ≤ jmaxino, fi.inos < jmaxino, fi0.inos < pmaxino, pmaxino ≠ 0, jvalid ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro), fi.lebs ⊆ dom gstore, fi0.lebs ⊆ dom gstore0, refsize-cons(gstore, range fi), refsize-cons(gstore0, range fi0), inv-journal(nx, gstore, gstore0, jro), ri-inj(fi), ri-inj(fi0) ⊦ ⟪gjournal_journal_add5# (nd, nd0, nd1, nd2, nd3, jvalid0, fi, fi0, gstore0, pmaxino, p_os; adr, adr0, adr1, adr2, adr3, jvalid, jmaxino0, jro, gstore, nx, jvalid1; err)⟫ ( (jvalid ∧ nx ≠ [] → valid-journal-head(nx, gstore, jro)) ∧ fi.lebs ⊆ dom gstore ∧ refsize-cons(gstore, range fi) ∧ inv-journal(nx, gstore, gstore0, jro)) A Proof Obligation
abs-log-simp0 ⊦ ax0 = ax + ax2 → (ax0 = ax1 + ax2 ↔ ax = ax1) A User Theorem
abs-log-simp1 ⊦ ax0 = ax3 ∧ ax3 = ax + ax2 → (ax0 = ax1 + ax2 ↔ ax = ax1) A User Theorem
lf-inv-append-sizes ⊦ # gndx1 = # lax1 ∧ inv(groupblock(gndx0 + gndx1, lax0 + lax1, m)) → # gndx0 = # lax0 A User Theorem
ls-diff-rem-subseteq ⊦ as0 ⊆ as2 ∧ as = as2 ∪ as3 → (as0 \ as1) -- adr ⊆ as A User Theorem
ls-inv-prefix-app-prefixn ⊦ inv(groupblock(gndx0 + prefixn(# lax1, gndx1), lax0 + lax1, m)) ∧ # lax1 < # gndx1 → prefixn(# gndx0, lax0 + lax) = lax0 A User Theorem
ls-inv-prefixn-ladrs ⊦ inv(groupblock(gndx0 + gndx1, lax0 + lax1, n)) → prefixn(# gndx0 + # gndx1, lax0 + lax1) = lax0 + lax1 A User Theorem
ls-inv-reduce-jnlhead ⊦ inv(gstore \ ns) ∧ valid-journal-head(nx, gstore, ns) ∧ nx ≠ [] → (inv(gstore[nx.last, gblock] \ ns) ↔ inv(gblock)) A User Theorem
ls-union-subseteq ⊦ as = as1 ∪ as2 → (as0 ∪ as1 ⊆ as ↔ as0 ⊆ as) A User Theorem
prepost-gc-referenced-nodes# ax = # gndx, ax0 = ax, gndx0 = gndx, lnum ∈ gstore, ¬ lnum ∈ ginval, gstore[lnum].gndlist = gndx, gstore[lnum].ladrlist.to-adr(lnum) = ax, ri-cons(ri, nodes(gstore ↓, ginval)), inv(gstore \ ginval) ⊦ ⟪gjournal_gc_referenced_nodes#(lnum, ri, fi, ginval, gstore, gstore0, nx0, maxino, ns, boolvar0; ax, gndx; ndx, err)⟫ ((err = ESUCCESS ∨ ⌊err⌋ ) ∧ (err = ESUCCESS → ndx = nodes(gstore ↓, ginval)[referenced-adrs(ax0, ri)])) A User Theorem
prepost-split-nodesndx1 = ndx ⊦ ⟪gjournal_split_nodes#(n; ndx, ndx0)⟫ (ndx1 = ndx0 + ndx ∧ ndx0.flashsize ≤ n ∧ (ndx = [] ∨ ndx0.flashsize + ndx.head.flashsize > n)) A User Theorem
term-remove-nonend-blocksn ∈ gstore, ¬ n ∈ ginval, inv(gstore) ⊦ ⟪gjournal_remove_nonend_blocks#(n, ri, fi, ginval, gstore, gstore0, nx0, maxino, ns, boolvar0; log; err)⟫ true A User Theorem
term-restore-logelems nx ∩ ginval = ∅, elems nx ⊆ dom gstore, inv(gstore) ⊦ ⟪gjournal_restore_log#(nx, ri, fi, ginval, gstore, gstore0, nx0, maxino, ns, boolvar0; log; err)⟫ true A User Theorem