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: |
|---|---|---|
| newino | aubifs_core_index_newino#(RI, FI, RO, FO, FS, LOG, CSYNCED; KEY) {choose n with ¬ inodekey(n) ∈ RI ∧ ¬ inodekey(n) ∈ FO ∧ n ≠ 0 in KEY := inodekey(n)} | An Axiom |
| lookup | aubifs_core_index_lookup#(KEY, RI, FI, RO, FO, FS, LOG, CSYNCED; EXISTS, ND; ERR) {if ri-cons(RI, FS) then {fail_or_success#(; ; ERR); if ERR = ESUCCESS then {EXISTS := KEY ∈ RI; if EXISTS then ND := FS[RI[KEY]] else ND := ?} else EXISTS := ?, ND := ?} else abort } | An Axiom |
| store | aubifs_core_index_store#(KEY, ADR, FI, RO, FO, FS, LOG, CSYNCED; RI) {if ¬ ADR ∈ RI ∧ ADR ∈ FS ∧ key-cons(KEY, FS[ADR]) then RI[KEY] := ADR else abort} | An Axiom |
| remove | aubifs_core_index_remove#(KEY, FI, RO, FO, FS, LOG, CSYNCED; RI){RI := RI -- KEY} | An Axiom |
| truncate | aubifs_core_index_truncate#(KEY, N, FI, RO, FO, FS, LOG, CSYNCED; RI){let KS = datakeys(KEY, N, RI) in RI := RI \ KS} | An Axiom |
| entries | aubifs_core_index_entries#(KEY, RI, FI, RO, FO, FS, LOG, CSYNCED; NAMES; ERR) {fail_or_success#(; ; ERR); if ERR = ESUCCESS then NAMES := dentries(KEY, RI) else NAMES := ?} | An Axiom |
| add4 | aubifs_core_journal_add4#(ND1, ND2, ND3, ND4, RI, FI, RO, FO; ADR1, ADR2, ADR3, ADR4, FS, LOG; CSYNCED, ERR) {if ri-cons(RI, FS) ∧ node-cons(ND1.key, ND1) ∧ node-cons(ND2.key, ND2) ∧ node-cons(ND3.key, ND3) ∧ node-cons(ND4.key, ND4) then { choose adr1, adr2, adr3, adr4 with new(adr1 ' + adr2 ' + (adr3 ' + adr4), FS) ∧ ¬ dups(adr1 ' + adr2 ' + adr3 ' + adr4 ') in {ADR1 := adr1, ADR2 := adr2, ADR3 := adr3, ADR4 := adr4; FS := FS[ADR1, ND1][ADR2, ND2][ADR3, ND3][ADR4, ND4], LOG := (((LOG + ADR1) + ADR2) + ADR3) + ADR4, ERR := ESUCCESS} ifnone ERR := ENOSPC or {fail#(; ; ERR); ADR1 := ?, ADR2 := ?, ADR3 := ?, ADR4 := ?}; CSYNCED := ?} else abort } | An Axiom |
| add3 | aubifs_core_journal_add3#(ND1, ND2, ND3, RI, FI, RO, FO; ADR1, ADR2, ADR3, FS, LOG; CSYNCED, ERR) {if ri-cons(RI, FS) ∧ node-cons(ND1.key, ND1) ∧ node-cons(ND2.key, ND2) ∧ node-cons(ND3.key, ND3) then { choose adr1, adr2, adr3 with new(adr1 ' + (adr2 ' + adr3), FS) ∧ ¬ dups(adr1 ' + adr2 ' + adr3 ') in {ADR1 := adr1, ADR2 := adr2, ADR3 := adr3; FS := FS[ADR1, ND1][ADR2, ND2][ADR3, ND3], LOG := ((LOG + ADR1) + ADR2) + ADR3, ERR := ESUCCESS} ifnone ERR := ENOSPC or {fail#(; ; ERR); ADR1 := ?, ADR2 := ?, ADR3 := ?}; CSYNCED := ?} else abort } | An Axiom |
| add2 | aubifs_core_journal_add2#(ND1, ND2, RI, FI, RO, FO; ADR1, ADR2, FS, LOG; CSYNCED, ERR) {if ri-cons(RI, FS) ∧ node-cons(ND1.key, ND1) ∧ node-cons(ND2.key, ND2) then { choose adr1, adr2 with new(adr1 ' + adr2 ', FS) ∧ ¬ dups(adr1 ' + adr2 ') in {ADR1 := adr1, ADR2 := adr2; FS := FS[ADR1, ND1][ADR2, ND2], LOG := (LOG + ADR1) + ADR2, ERR := ESUCCESS} ifnone ERR := ENOSPC or {fail#(; ; ERR); ADR1 := ?, ADR2 := ?}; CSYNCED := ?} else abort } | An Axiom |
| add1 | aubifs_core_journal_add1#(ND1, RI, FI, RO, FO; ADR1, FS, LOG; CSYNCED, ERR) {if ri-cons(RI, FS) ∧ node-cons(ND1.key, ND1) then { choose adr1 with new(adr1 ', FS) ∧ ¬ dups(adr1 ') in {ADR1 := adr1; FS[ADR1] := ND1, LOG := LOG + ADR1, ERR := ESUCCESS} ifnone ERR := ENOSPC or {fail#(; ; ERR); ADR1 := ?}; CSYNCED := ?} else abort } | An Axiom |
| get | aubifs_core_journal_get#(ADR, RI, FI, RO, FO, FS, LOG, CSYNCED; ND; ERR) {if ADR ∈ FS then {ND := FS[ADR], ERR := ESUCCESS or fail#(; ; ERR)} else abort} | An Axiom |
| gc | aubifs_core_journal_gc#(FI, RO, FO; RI, FS, LOG; CSYNCED) {if ri-cons(RI, FS) then {aubifs_core_gc_copy#(; RI, FS, LOG); aubifs_core_gc_drop#(RI, LOG; FS); CSYNCED := ?} else abort} | An Axiom |
| gc-drop | aubifs_core_gc_drop#(RI, LOG; FS){choose AS with AS ∩ range RI = ∅ ∧ LOG.toSet ∩ AS = ∅ in FS := FS \ AS} | An Axiom |
| gc-step | aubifs_core_gc_copy#(; RI, FS, LOG) {choose KX, AX with ¬ dups(KX) ∧ ¬ dups(AX) ∧ new(AX, FS) ∧ KX.toSet ⊆ dom RI ∧ # KX = # AX ∧ AX.toSet ∩ LOG.toSet = ∅ in {FS[AX] := FS[RI[KX]], LOG := LOG + AX; RI[KX] := AX} } | An Axiom |
| commit | aubifs_core_commit#(RI, RO; FS, FI, FO, LOG; CSYNCED, ERR) {if ri-cons(RI, FS) then { {choose AS with AS ∩ range RI = ∅ in FI := RI, FO := RO, FS := FS \ AS, LOG := [], ERR := ESUCCESS; CSYNCED := true} or {fail#(; ; ERR); CSYNCED := ?}} else abort } | An Axiom |
| check-commit | aubifs_core_check_commit#(RI, RO; FI, FO, FS, LOG, CSYNCED; ERR) {if ri-cons(RI, FS) then {aubifs_core_commit#(RI, RO; FS, FI, FO, LOG; CSYNCED, ERR) or ERR := ESUCCESS} else abort} | An Axiom |
| orphans-remove | aubifs_core_orphans_remove#(KEY, RI, FI, FO, FS, LOG, CSYNCED; RO){if KEY.inode? then RO := RO -- KEY else abort} | An Axiom |
| orphans-insert | aubifs_core_orphans_insert#(KEY, RI, FI, FO, FS, LOG, CSYNCED; RO){if KEY.inode? then RO := RO ++ KEY else abort} | An Axiom |
| orphans-contains | aubifs_core_orphans_contains#(KEY, RI, FI, RO, FO, FS, LOG, CSYNCED; EXISTS){if KEY.inode? then EXISTS := KEY ∈ RO else abort} | An Axiom |
| contains | aubifs_core_index_contains#(KEY, RI, FI, RO, FO, FS, LOG, CSYNCED; EXISTS; ERR) {fail_or_success#(; ; ERR); if ERR = ESUCCESS then EXISTS := KEY ∈ RI else EXISTS := ?} | An Axiom |
| format | aubifs_core_format#(VOLSIZE, SIZE, DOSYNC; ; RI, FI, RO, FO, FS, LOG, CSYNCED, ERR) {if SIZE = LEB_SIZE then {fail_or_success#(; ; ERR); if ERR = ESUCCESS then RI := ∅, FS := ∅, FI := ∅, FO := ∅, RO := ∅, LOG := [], CSYNCED := true else RI := ?, FS := ?, FI := ?, FO := ?, RO := ?, LOG := ?, CSYNCED := ?} else abort } | An Axiom |
| recover | aubifs_core_recover#(DOSYNC; AX, KS, FI, RO, FO, LOG, FS; RI, CSYNCED, ERR) {fail_or_success#(; ; ERR); if ERR = ESUCCESS then {RI := FI, RO := FO, AX := LOG; KS := RO; CSYNCED := true} else RI := ?, FI := ?, FS := ?, LOG := ?, RO := ?, FO := ?, AX := ?, KS := ?, CSYNCED := ? } | An Axiom |
| sync-01 | aubifs_core_journal_sync#(RI, FI, RO, FO, FS, LOG; ; CSYNCED, ERR){fail_or_success#(; ; ERR); CSYNCED := ERR = ESUCCESS} | An Axiom |
| add5 | aubifs_core_journal_add5#(ND1, ND2, ND3, ND4, ND5, RI, FI, RO, FO; ADR1, ADR2, ADR3, ADR4, ADR5, FS, LOG; CSYNCED, ERR) {if ri-cons(RI, FS) ∧ node-cons(ND1.key, ND1) ∧ node-cons(ND2.key, ND2) ∧ node-cons(ND3.key, ND3) ∧ node-cons(ND4.key, ND4) ∧ node-cons(ND5.key, ND5) then { choose adr1, adr2, adr3, adr4, adr5 with new(adr1 ' + adr2 ' + adr3 ' + (adr4 ' + adr5), FS) ∧ ¬ dups(adr1 ' + adr2 ' + adr3 ' + adr4 ' + adr5 ') in {ADR1 := adr1, ADR2 := adr2, ADR3 := adr3, ADR4 := adr4, ADR5 := adr5; FS := FS[ADR1, ND1][ADR2, ND2][ADR3, ND3][ADR4, ND4][ADR5, ND5], LOG := ((((LOG + ADR1) + ADR2) + ADR3) + ADR4) + ADR5, ERR := ESUCCESS} ifnone ERR := ENOSPC or {fail#(; ; ERR); ADR1 := ?, ADR2 := ?, ADR3 := ?, ADR4 := ?, ADR5 := ?}; CSYNCED := ?} else abort } | An Axiom |
| inv-format | ino = LEB_SIZE ⊦ ⟪aubifs_core_format#(ino0, ino, boolvar; ; ri, fi, ro, fo, fs, log, boolvar0, err)⟫ (err = ESUCCESS → boolvar0 ∧ ri-inj(ri) ∧ ri-inj(fi) ∧ log-cons(log, fs) ∧ ro.inodes? ∧ fo.inodes?) | A Proof Obligation |
| inv-sync | ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes? ⊦ ⟪aubifs_core_journal_sync#(ri, fi, ro, fo, fs, log; ; boolvar, err)⟫ true | A Proof Obligation |
| crash-neutral-sync | ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes?, boolvar, fi0 = fi, fo0 = fo, fs0 = fs, log0 = log ⊦ ⟨aubifs_core_journal_sync#(ri, fi, ro, fo, fs, log; ; boolvar, err)⟩ (boolvar ∧ fi0 = fi ∧ fo0 = fo ∧ fs0 = fs ∧ log0 = log) | A Proof Obligation |
| inv-orphans-remove | ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes?, key.inode? ⊦ ⟪aubifs_core_orphans_remove#(key, ri, fi, fo, fs, log, boolvar; ro)⟫ ro.inodes? | A Proof Obligation |
| inv-orphans-insert | ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes?, key.inode? ⊦ ⟪aubifs_core_orphans_insert#(key, ri, fi, fo, fs, log, boolvar; ro)⟫ ro.inodes? | A Proof Obligation |
| inv-orphans-contains | ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes?, key.inode? ⊦ ⟪aubifs_core_orphans_contains#(key, ri, fi, ro, fo, fs, log, boolvar; boolvar0)⟫ true | A Proof Obligation |
| inv-commit | ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes?, ri-cons(ri, fs) ⊦ ⟪aubifs_core_commit#(ri, ro; fs, fi, fo, log; boolvar, err)⟫ (ri-inj(fi) ∧ log-cons(log, fs) ∧ fo.inodes?) | A Proof Obligation |
| inv-check-commit | ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes?, ri-cons(ri, fs) ⊦ ⟪aubifs_core_check_commit#(ri, ro; fi, fo, fs, log, boolvar; err)⟫ (ri-inj(fi) ∧ log-cons(log, fs) ∧ fo.inodes?) | A Proof Obligation |
| inv-gc | ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes?, ri-cons(ri, fs) ⊦ ⟪aubifs_core_journal_gc#(fi, ro, fo; ri, fs, log; boolvar)⟫ (ri-inj(ri) ∧ log-cons(log, fs) ∧ ri-cons(ri, fs)) | A Proof Obligation |
| inv-add4 | ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes?, ri-cons(ri, fs), node-cons(nd.key, nd), node-cons(nd0.key, nd0), node-cons(nd1.key, nd1), node-cons(nd2.key, nd2) ⊦ ⟪aubifs_core_journal_add4#(nd, nd0, nd1, nd2, ri, fi, ro, fo; adr, adr0, adr1, adr2, fs, log; boolvar, err)⟫ (log-cons(log, fs) ∧ ri-cons(ri, fs)) | A Proof Obligation |
| inv-add3 | ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes?, ri-cons(ri, fs), node-cons(nd.key, nd), node-cons(nd0.key, nd0), node-cons(nd1.key, nd1) ⊦ ⟪aubifs_core_journal_add3#(nd, nd0, nd1, ri, fi, ro, fo; adr, adr0, adr1, fs, log; boolvar, err)⟫ (log-cons(log, fs) ∧ ri-cons(ri, fs)) | A Proof Obligation |
| inv-add2 | ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes?, ri-cons(ri, fs), node-cons(nd.key, nd), node-cons(nd0.key, nd0) ⊦ ⟪aubifs_core_journal_add2#(nd, nd0, ri, fi, ro, fo; adr, adr0, fs, log; boolvar, err)⟫ (log-cons(log, fs) ∧ ri-cons(ri, fs)) | A Proof Obligation |
| inv-add1 | ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes?, ri-cons(ri, fs), node-cons(nd.key, nd) ⊦ ⟪aubifs_core_journal_add1#(nd, ri, fi, ro, fo; adr, fs, log; boolvar, err)⟫ (log-cons(log, fs) ∧ ri-cons(ri, fs)) | A Proof Obligation |
| inv-get | ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes?, adr ∈ fs ⊦ ⟪aubifs_core_journal_get#(adr, ri, fi, ro, fo, fs, log, boolvar; nd; err)⟫ true | A Proof Obligation |
| inv-entries | ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes? ⊦ ⟪aubifs_core_index_entries#(key, ri, fi, ro, fo, fs, log, boolvar; strings; err)⟫ true | A Proof Obligation |
| inv-truncate | ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes? ⊦ ⟪aubifs_core_index_truncate#(key, n, fi, ro, fo, fs, log, boolvar; ri)⟫ ri-inj(ri) | A Proof Obligation |
| inv-remove | ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes? ⊦ ⟪aubifs_core_index_remove#(key, fi, ro, fo, fs, log, boolvar; ri)⟫ ri-inj(ri) | A Proof Obligation |
| inv-store | ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes?, ¬ adr ∈ ri, adr ∈ fs, key-cons(key, fs[adr]) ⊦ ⟪aubifs_core_index_store#(key, adr, fi, ro, fo, fs, log, boolvar; ri)⟫ ri-inj(ri) | A Proof Obligation |
| inv-lookup | ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes?, ri-cons(ri, fs) ⊦ ⟪aubifs_core_index_lookup#(key, ri, fi, ro, fo, fs, log, boolvar; boolvar0, nd; err)⟫ true | A Proof Obligation |
| inv-contains | ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes? ⊦ ⟪aubifs_core_index_contains#(key, ri, fi, ro, fo, fs, log, boolvar; boolvar0; err)⟫ true | A Proof Obligation |
| inv-newino | ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes? ⊦ ⟪aubifs_core_index_newino#(ri, fi, ro, fo, fs, log, boolvar; key)⟫ true | A Proof Obligation |
| crash-neutral-orphans-remove | key.inode?, ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes?, boolvar, fi0 = fi, fo0 = fo, fs0 = fs, log0 = log ⊦ ⟨aubifs_core_orphans_remove#(key, ri, fi, fo, fs, log, boolvar; ro)⟩ (boolvar ∧ fi0 = fi ∧ fo0 = fo ∧ fs0 = fs ∧ log0 = log) | A Proof Obligation |
| crash-neutral-orphans-insert | key.inode?, ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes?, boolvar, fi0 = fi, fo0 = fo, fs0 = fs, log0 = log ⊦ ⟨aubifs_core_orphans_insert#(key, ri, fi, fo, fs, log, boolvar; ro)⟩ (boolvar ∧ fi0 = fi ∧ fo0 = fo ∧ fs0 = fs ∧ log0 = log) | A Proof Obligation |
| crash-neutral-orphans-contains | key.inode?, ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes?, boolvar, fi0 = fi, fo0 = fo, fs0 = fs, log0 = log ⊦ ⟨aubifs_core_orphans_contains#(key, ri, fi, ro, fo, fs, log, boolvar; boolvar0)⟩ (boolvar ∧ fi0 = fi ∧ fo0 = fo ∧ fs0 = fs ∧ log0 = log) | A Proof Obligation |
| crash-neutral-commit | ri-cons(ri, fs), ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes?, boolvar, fi0 = fi, fo0 = fo, fs0 = fs, log0 = log ⊦ ⟨aubifs_core_commit#(ri, ro; fs, fi, fo, log; boolvar, err)⟩ (boolvar ∧ fi0 = fi ∧ fo0 = fo ∧ fs0 = fs ∧ log0 = log) | A Proof Obligation |
| crash-neutral-check-commit | ri-cons(ri, fs), ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes?, boolvar, fi0 = fi, fo0 = fo, fs0 = fs, log0 = log ⊦ ⟨aubifs_core_check_commit#(ri, ro; fi, fo, fs, log, boolvar; err)⟩ (boolvar ∧ fi0 = fi ∧ fo0 = fo ∧ fs0 = fs ∧ log0 = log) | A Proof Obligation |
| crash-neutral-gc | ri-cons(ri, fs), ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes?, boolvar, fi0 = fi, fo0 = fo, fs0 = fs, log0 = log ⊦ ⟨aubifs_core_journal_gc#(fi, ro, fo; ri, fs, log; boolvar)⟩ (boolvar ∧ fi0 = fi ∧ fo0 = fo ∧ fs0 = fs ∧ log0 = log) | A Proof Obligation |
| crash-neutral-add4 | ri-cons(ri, fs), node-cons(nd.key, nd), node-cons(nd0.key, nd0), node-cons(nd1.key, nd1), node-cons(nd2.key, nd2), ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes?, boolvar, fi0 = fi, fo0 = fo, fs0 = fs, log0 = log ⊦ ⟨aubifs_core_journal_add4#(nd, nd0, nd1, nd2, ri, fi, ro, fo; adr, adr0, adr1, adr2, fs, log; boolvar, err)⟩ (boolvar ∧ fi0 = fi ∧ fo0 = fo ∧ fs0 = fs ∧ log0 = log) | A Proof Obligation |
| crash-neutral-add3 | ri-cons(ri, fs), node-cons(nd.key, nd), node-cons(nd0.key, nd0), node-cons(nd1.key, nd1), ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes?, boolvar, fi0 = fi, fo0 = fo, fs0 = fs, log0 = log ⊦ ⟨aubifs_core_journal_add3#(nd, nd0, nd1, ri, fi, ro, fo; adr, adr0, adr1, fs, log; boolvar, err)⟩ (boolvar ∧ fi0 = fi ∧ fo0 = fo ∧ fs0 = fs ∧ log0 = log) | A Proof Obligation |
| crash-neutral-add2 | ri-cons(ri, fs), node-cons(nd.key, nd), node-cons(nd0.key, nd0), ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes?, boolvar, fi0 = fi, fo0 = fo, fs0 = fs, log0 = log ⊦ ⟨aubifs_core_journal_add2#(nd, nd0, ri, fi, ro, fo; adr, adr0, fs, log; boolvar, err)⟩ (boolvar ∧ fi0 = fi ∧ fo0 = fo ∧ fs0 = fs ∧ log0 = log) | A Proof Obligation |
| crash-neutral-add1 | ri-cons(ri, fs), node-cons(nd.key, nd), ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes?, boolvar, fi0 = fi, fo0 = fo, fs0 = fs, log0 = log ⊦ ⟨aubifs_core_journal_add1#(nd, ri, fi, ro, fo; adr, fs, log; boolvar, err)⟩ (boolvar ∧ fi0 = fi ∧ fo0 = fo ∧ fs0 = fs ∧ log0 = log) | A Proof Obligation |
| crash-neutral-get | adr ∈ fs, ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes?, boolvar, fi0 = fi, fo0 = fo, fs0 = fs, log0 = log ⊦ ⟨aubifs_core_journal_get#(adr, ri, fi, ro, fo, fs, log, boolvar; nd; err)⟩ (boolvar ∧ fi0 = fi ∧ fo0 = fo ∧ fs0 = fs ∧ log0 = log) | A Proof Obligation |
| crash-neutral-entries | ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes?, boolvar, fi0 = fi, fo0 = fo, fs0 = fs, log0 = log ⊦ ⟨aubifs_core_index_entries#(key, ri, fi, ro, fo, fs, log, boolvar; strings; err)⟩ (boolvar ∧ fi0 = fi ∧ fo0 = fo ∧ fs0 = fs ∧ log0 = log) | A Proof Obligation |
| crash-neutral-truncate | ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes?, boolvar, fi0 = fi, fo0 = fo, fs0 = fs, log0 = log ⊦ ⟨aubifs_core_index_truncate#(key, n, fi, ro, fo, fs, log, boolvar; ri)⟩ (boolvar ∧ fi0 = fi ∧ fo0 = fo ∧ fs0 = fs ∧ log0 = log) | A Proof Obligation |
| crash-neutral-remove | ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes?, boolvar, fi0 = fi, fo0 = fo, fs0 = fs, log0 = log ⊦ ⟨aubifs_core_index_remove#(key, fi, ro, fo, fs, log, boolvar; ri)⟩ (boolvar ∧ fi0 = fi ∧ fo0 = fo ∧ fs0 = fs ∧ log0 = log) | A Proof Obligation |
| crash-neutral-store | ¬ adr ∈ ri, adr ∈ fs, key-cons(key, fs[adr]), ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes?, boolvar, fi0 = fi, fo0 = fo, fs0 = fs, log0 = log ⊦ ⟨aubifs_core_index_store#(key, adr, fi, ro, fo, fs, log, boolvar; ri)⟩ (boolvar ∧ fi0 = fi ∧ fo0 = fo ∧ fs0 = fs ∧ log0 = log) | A Proof Obligation |
| crash-neutral-lookup | ri-cons(ri, fs), ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes?, boolvar, fi0 = fi, fo0 = fo, fs0 = fs, log0 = log ⊦ ⟨aubifs_core_index_lookup#(key, ri, fi, ro, fo, fs, log, boolvar; boolvar0, nd; err)⟩ (boolvar ∧ fi0 = fi ∧ fo0 = fo ∧ fs0 = fs ∧ log0 = log) | A Proof Obligation |
| crash-neutral-contains | ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes?, boolvar, fi0 = fi, fo0 = fo, fs0 = fs, log0 = log ⊦ ⟨aubifs_core_index_contains#(key, ri, fi, ro, fo, fs, log, boolvar; boolvar0; err)⟩ (boolvar ∧ fi0 = fi ∧ fo0 = fo ∧ fs0 = fs ∧ log0 = log) | A Proof Obligation |
| crash-neutral-newino | ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes?, boolvar, fi0 = fi, fo0 = fo, fs0 = fs, log0 = log ⊦ ⟨aubifs_core_index_newino#(ri, fi, ro, fo, fs, log, boolvar; key)⟩ (boolvar ∧ fi0 = fi ∧ fo0 = fo ∧ fs0 = fs ∧ log0 = log) | A Proof Obligation |
| crash-neutral-recover | ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes?, boolvar, fi0 = fi, fo0 = fo, fs0 = fs, log0 = log ⊦ ⟨aubifs_core_recover#(boolvar0; ax, ks, fi, ro, fo, log, fs; ri, boolvar, err)⟩ (boolvar ∧ fi0 = fi ∧ fo0 = fo ∧ fs0 = fs ∧ log0 = log) | A Proof Obligation |
| inv-recover | fi = fi0, fo = fo0, fs = fs0, log = log0, boolvar, ri-inj(ri), ri-inj(fi0), log-cons(log0, fs0), ro.inodes?, fo0.inodes? ⊦ ⟪aubifs_core_recover#(boolvar0; ax, ks, fi, ro0, fo, log, fs; ri0, boolvar1, err)⟫ (err = ESUCCESS → boolvar1 ∧ ri-inj(ri0) ∧ ri-inj(fi) ∧ log-cons(log, fs) ∧ ro0.inodes? ∧ fo.inodes?) | A Proof Obligation |
| crash-neutral-add5 | ri-cons(ri, fs), node-cons(nd.key, nd), node-cons(nd0.key, nd0), node-cons(nd1.key, nd1), node-cons(nd2.key, nd2), node-cons(nd3.key, nd3), ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes?, boolvar, fi0 = fi, fo0 = fo, fs0 = fs, log0 = log ⊦ ⟨aubifs_core_journal_add5#(nd, nd0, nd1, nd2, nd3, ri, fi, ro, fo; adr, adr0, adr1, adr2, adr3, fs, log; boolvar, err)⟩ (boolvar ∧ fi0 = fi ∧ fo0 = fo ∧ fs0 = fs ∧ log0 = log) | A Proof Obligation |
| inv-add5 | ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes?, ri-cons(ri, fs), node-cons(nd.key, nd), node-cons(nd0.key, nd0), node-cons(nd1.key, nd1), node-cons(nd2.key, nd2), node-cons(nd3.key, nd3) ⊦ ⟪aubifs_core_journal_add5#(nd, nd0, nd1, nd2, nd3, ri, fi, ro, fo; adr, adr0, adr1, adr2, adr3, fs, log; boolvar, err)⟫ (log-cons(log, fs) ∧ ri-cons(ri, fs)) | A Proof Obligation |