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: |
|---|---|---|
| truncate | aubifs_truncate#(N, PAGENO, FI, RO, FO; PBUF-OPT, INODE, MODIFIED, ERR, RI, FS, LOG, CSYNCED) {if pre-truncate(INODE, N, PAGENO, PBUF-OPT, FS, RI, RO) then choose ADR1, ADR2, ADR3, EXISTS with true in let KEY1 = inodekey(INODE.ino), KEY2 = inodekey(INODE.ino), OFFSET = INODE.size % VFS_PAGE_SIZE, SIZE = min(N, INODE.size) in let KEY3 = datakey(INODE.ino, PAGENO), ND1 = truncnode(KEY1, SIZE), ND2 = inodenode(KEY2, INODE.meta, INODE.directory, INODE.nlink, INODE.nsubdirs, N), ND3 = ? in {if INODE.size ≤ N ∧ OFFSET ≠ 0 then if PBUF-OPT.some? then {ND3 := datanode(KEY3, PBUF-OPT.buf); EXISTS := true, ERR := ESUCCESS} else aubifs_core_index_lookup#(KEY3, RI, FI, RO, FO, FS, LOG, CSYNCED; EXISTS, ND3; ERR) else EXISTS := false, ERR := ESUCCESS; if ERR = ESUCCESS then if EXISTS then {ND3.data := fill(ND3.data, zero, OFFSET, VFS_PAGE_SIZE - OFFSET); aubifs_core_journal_add3#(ND1, ND2, ND3, RI, FI, RO, FO; ADR1, ADR2, ADR3, FS, LOG; CSYNCED, ERR); if ERR = ESUCCESS then aubifs_core_index_store#(KEY3, ADR3, FI, RO, FO, FS, LOG, CSYNCED; RI)} else aubifs_core_journal_add2#(ND1, ND2, RI, FI, RO, FO; ADR1, ADR2, FS, LOG; CSYNCED, ERR); if ERR = ESUCCESS then {aubifs_core_index_store#(KEY2, ADR2, FI, RO, FO, FS, LOG, CSYNCED; RI); aubifs_core_index_truncate#(KEY1, SIZE, FI, RO, FO, FS, LOG, CSYNCED; RI); MODIFIED := EXISTS; INODE := mkinode(INODE.ino, ND2.meta, ND2.directory, ND2.nlink, ND2.nsubdirs, ND2.size); if MODIFIED then PBUF-OPT := some(ND3.data)}} else abort } | An Axiom |
| lookup | aubifs_lookup#(P_INO, RI, FI, RO, FO, FS, LOG, CSYNCED; DENT, ERR) {if pre-lookup(P_INO, DENT, FS, RI, RO) then choose EXISTS, ND, KEY with true in {ERR := ESUCCESS; KEY := dentrykey(P_INO, DENT.name); aubifs_core_index_lookup#(KEY, RI, FI, RO, FO, FS, LOG, CSYNCED; EXISTS, ND; ERR); if ERR = ESUCCESS then if EXISTS then DENT := mkdentry(DENT.name, ND.ino), ERR := ESUCCESS else DENT := negdentry(DENT.name), ERR := ENOENT} else abort } | An Axiom |
| iget | aubifs_iget#(INO, RI, FI, RO, FO, FS, LOG, CSYNCED; INODE, ERR) {if pre-iget(INO, FS, RI) then let EXISTS = ? in {ERR := ESUCCESS; aubifs_iget_check#(INO, RI, FI, RO, FO, FS, LOG, CSYNCED; EXISTS, INODE, ERR)} else abort } | An Axiom |
| create | aubifs_create#(MD, FI, RO, FO; P_INODE, C_INODE, DENT, ERR, RI, FS, LOG, CSYNCED) {if pre-create(P_INODE, DENT, MD, FS, RI, RO) then choose ADR1, ADR2, ADR3, KEY1, KEY2, KEY3, ND1, ND2, ND3 with true in {KEY1 := inodekey(P_INODE.ino); KEY2 := dentrykey(P_INODE.ino, DENT.name); aubifs_core_index_newino#(RI, FI, RO, FO, FS, LOG, CSYNCED; KEY3); ND1 := inodenode(KEY1, P_INODE.meta, P_INODE.directory, P_INODE.nlink, P_INODE.nsubdirs, P_INODE.size + 1); ND2 := dentrynode(KEY2, KEY3.ino); ND3 := inodenode(KEY3, MD, false, 1, 0, 0); aubifs_core_journal_add3#(ND1, ND2, ND3, RI, FI, RO, FO; ADR1, ADR2, ADR3, FS, LOG; CSYNCED, ERR); if ERR = ESUCCESS then {aubifs_core_index_store#(KEY1, ADR1, FI, RO, FO, FS, LOG, CSYNCED; RI); aubifs_core_index_store#(KEY2, ADR2, FI, RO, FO, FS, LOG, CSYNCED; RI); aubifs_core_index_store#(KEY3, ADR3, FI, RO, FO, FS, LOG, CSYNCED; RI); DENT := mkdentry(DENT.name, KEY3.ino); P_INODE := mkinode(P_INODE.ino, ND1.meta, ND1.directory, ND1.nlink, ND1.nsubdirs, ND1.size); C_INODE := mkinode(KEY3.ino, ND3.meta, ND3.directory, ND3.nlink, ND3.nsubdirs, ND3.size)}} else abort } | An Axiom |
| mkdir | aubifs_mkdir#(MD, FI, RO, FO; P_INODE, C_INODE, DENT, ERR, RI, FS, LOG, CSYNCED) {if pre-mkdir(P_INODE, DENT, MD, FS, RI, RO) then choose ADR1, ADR2, ADR3, KEY1, KEY2, KEY3, ND1, ND2, ND3 with true in {KEY1 := inodekey(P_INODE.ino); KEY2 := dentrykey(P_INODE.ino, DENT.name); aubifs_core_index_newino#(RI, FI, RO, FO, FS, LOG, CSYNCED; KEY3); ND1 := inodenode(KEY1, P_INODE.meta, P_INODE.directory, P_INODE.nlink, P_INODE.nsubdirs + 1, P_INODE.size + 1); ND2 := dentrynode(KEY2, KEY3.ino); ND3 := inodenode(KEY3, MD, true, 1, 0, 0); aubifs_core_journal_add3#(ND1, ND2, ND3, RI, FI, RO, FO; ADR1, ADR2, ADR3, FS, LOG; CSYNCED, ERR); if ERR = ESUCCESS then {aubifs_core_index_store#(KEY1, ADR1, FI, RO, FO, FS, LOG, CSYNCED; RI); aubifs_core_index_store#(KEY2, ADR2, FI, RO, FO, FS, LOG, CSYNCED; RI); aubifs_core_index_store#(KEY3, ADR3, FI, RO, FO, FS, LOG, CSYNCED; RI); DENT := mkdentry(DENT.name, KEY3.ino); P_INODE := mkinode(P_INODE.ino, ND1.meta, ND1.directory, ND1.nlink, ND1.nsubdirs, ND1.size); C_INODE := mkinode(KEY3.ino, ND3.meta, ND3.directory, ND3.nlink, ND3.nsubdirs, ND3.size)}} else abort } | An Axiom |
| unlink | aubifs_unlink#(FI, FO; P_INODE, C_INODE, DENT, ERR, RI, RO, FS, LOG, CSYNCED) {if pre-unlink(P_INODE, C_INODE, DENT, FS, RI, RO) then choose INO, ADR1, ADR2, ADR3, KEY1, KEY2, KEY3, ND1, ND2, ND3 with INO = C_INODE.ino in {KEY1 := inodekey(P_INODE.ino); KEY2 := dentrykey(P_INODE.ino, DENT.name); KEY3 := inodekey(C_INODE.ino); ND1 := inodenode(KEY1, P_INODE.meta, P_INODE.directory, P_INODE.nlink, P_INODE.nsubdirs, P_INODE.size - 1); ND2 := dentrynode(KEY2, 0); ND3 := inodenode(KEY3, C_INODE.meta, C_INODE.directory, C_INODE.nlink - 1, C_INODE.nsubdirs, C_INODE.size); aubifs_core_journal_add3#(ND1, ND2, ND3, RI, FI, RO, FO; ADR1, ADR2, ADR3, FS, LOG; CSYNCED, ERR); if ERR = ESUCCESS then {aubifs_core_index_store#(KEY1, ADR1, FI, RO, FO, FS, LOG, CSYNCED; RI); aubifs_core_index_remove#(KEY2, FI, RO, FO, FS, LOG, CSYNCED; RI); aubifs_core_index_store#(KEY3, ADR3, FI, RO, FO, FS, LOG, CSYNCED; RI); if C_INODE.nlink = 1 then aubifs_core_orphans_insert#(KEY3, RI, FI, FO, FS, LOG, CSYNCED; RO); DENT := negdentry(DENT.name); P_INODE := mkinode(P_INODE.ino, ND1.meta, ND1.directory, ND1.nlink, ND1.nsubdirs, ND1.size); C_INODE := mkinode(INO, ND3.meta, ND3.directory, ND3.nlink, ND3.nsubdirs, ND3.size)}} else abort } | An Axiom |
| evict | aubifs_evict#(INODE, FI, FO, FS, LOG, CSYNCED; ERR, RI, RO) {if pre-evict(INODE.ino, FS, RI, RO) then {choose EXISTS, KEY with KEY = inodekey(INODE.ino) in {aubifs_core_orphans_contains#(KEY, RI, FI, RO, FO, FS, LOG, CSYNCED; EXISTS); if EXISTS then {aubifs_core_index_truncate#(KEY, 0, FI, RO, FO, FS, LOG, CSYNCED; RI); aubifs_core_orphans_remove#(KEY, RI, FI, FO, FS, LOG, CSYNCED; RO); aubifs_core_index_remove#(KEY, FI, RO, FO, FS, LOG, CSYNCED; RI)}}; ERR := ESUCCESS} else abort } | An Axiom |
| replay | aubifs_replay#(DOSYNC; RI, FI, RO, FO, FS, LOG, CSYNCED; ERR) {let AX = ?, KS = ? in {aubifs_core_recover#(DOSYNC; AX, KS, FI, RO, FO, LOG, FS; RI, CSYNCED, ERR); if ERR = ESUCCESS then aubifs_replayorphans#(FI, FO, FS, LOG, CSYNCED; KS, ERR, RI, RO); if ERR = ESUCCESS then aubifs_replaylog#(AX, FI, RO, FO, FS, LOG, CSYNCED; ERR, RI); if ERR = ESUCCESS then aubifs_core_journal_sync#(RI, FI, RO, FO, FS, LOG; ; CSYNCED, ERR)} } | An Axiom |
| readdir | aubifs_readdir#(INODE, RI, FI, RO, FO, FS, LOG, CSYNCED; NAMES, ERR) {if pre-readdir(INODE.ino, FS, RI) then choose KEY with true in {KEY := inodekey(INODE.ino); aubifs_core_index_entries#(KEY, RI, FI, RO, FO, FS, LOG, CSYNCED; NAMES; ERR)} else abort } | An Axiom |
| writepage | aubifs_writepage#(INODE, PAGENO, PBUF, FI, RO, FO; ERR, RI, FS, LOG, CSYNCED) {if pre-writepage(INODE, PAGENO, PBUF, FS, RI) then choose EXISTS, KEY1, ADR1, ND1 with EXISTS in let INO = INODE.ino in {KEY1 := datakey(INO, PAGENO); ND1 := datanode(KEY1, PBUF); aubifs_core_journal_add1#(ND1, RI, FI, RO, FO; ADR1, FS, LOG; CSYNCED, ERR); if ERR = ESUCCESS then aubifs_core_index_store#(KEY1, ADR1, FI, RO, FO, FS, LOG, CSYNCED; RI) else if ¬ EXISTS then aubifs_core_index_remove#(KEY1, FI, RO, FO, FS, LOG, CSYNCED; RI)} else abort } | An Axiom |
| readpage | aubifs_readpage#(INODE, PAGENO, RI, FI, RO, FO, FS, LOG, CSYNCED; PBUF, ERR) {if pre-readpage(INODE, PAGENO, PBUF, FS, RI) then choose KEY, EXISTS, ND with true in {ERR := ESUCCESS; KEY := datakey(INODE.ino, PAGENO); aubifs_core_index_lookup#(KEY, RI, FI, RO, FO, FS, LOG, CSYNCED; EXISTS, ND; ERR); if ERR = ESUCCESS then if EXISTS then PBUF := copy(ND.data, 0, PBUF, 0, VFS_PAGE_SIZE) else PBUF := fill(PBUF, zero)} else abort } | An Axiom |
| renam | aubifs_rename#(FI, FO; OLD_PARENT_INODE, NEW_PARENT_INODE, OLD_CHILD_INODE, NEW_CHILD_INODE, OLD_DENT, NEW_DENT, ERR, RI, RO, FS, LOG, CSYNCED) {if pre-rename(OLD_PARENT_INODE, OLD_DENT, OLD_CHILD_INODE, NEW_PARENT_INODE, NEW_DENT, NEW_CHILD_INODE, FS, RI, RO) then let OVERWRITE = NEW_DENT.dentry?, REPARENT = OLD_PARENT_INODE.ino ≠ NEW_PARENT_INODE.ino, IS_DIR = OLD_CHILD_INODE.directory in if REPARENT then if OVERWRITE then aubifs_rename_overwrite_reparent# (IS_DIR, OLD_CHILD_INODE, FI, FO ; OLD_PARENT_INODE, NEW_PARENT_INODE, NEW_CHILD_INODE, OLD_DENT, NEW_DENT, ERR, RI, RO, FS, LOG, CSYNCED) else aubifs_rename_new_reparent# (IS_DIR, OLD_CHILD_INODE, FI, RO, FO; OLD_PARENT_INODE, NEW_PARENT_INODE, OLD_DENT, NEW_DENT, ERR, RI, FS, LOG, CSYNCED) else {if OVERWRITE then aubifs_rename_overwrite_keep_parent# (IS_DIR, OLD_CHILD_INODE, FI, FO; OLD_PARENT_INODE, NEW_CHILD_INODE, OLD_DENT, NEW_DENT, ERR, RI, RO, FS, LOG, CSYNCED) else aubifs_rename_new_keep_parent# (IS_DIR, OLD_CHILD_INODE, FI, RO, FO; OLD_PARENT_INODE, OLD_DENT, NEW_DENT, ERR, RI, FS, LOG, CSYNCED); NEW_PARENT_INODE := OLD_PARENT_INODE} else abort } | An Axiom |
| link | aubifs_link#(OLD_DENT, FI, RO, FO; P_INODE, C_INODE, NEW_DENT, ERR, RI, FS, LOG, CSYNCED) {if pre-link(P_INODE, C_INODE, OLD_DENT, NEW_DENT, FS, RI, RO) then choose INO, ADR1, ADR2, ADR3, KEY1, KEY2, KEY3, ND1, ND2, ND3 with INO = C_INODE.ino in {KEY1 := inodekey(P_INODE.ino); KEY2 := dentrykey(P_INODE.ino, NEW_DENT.name); KEY3 := inodekey(INO); ND1 := inodenode(KEY1, P_INODE.meta, P_INODE.directory, P_INODE.nlink, P_INODE.nsubdirs, P_INODE.size + 1); ND2 := dentrynode(KEY2, INO); ND3 := inodenode(KEY3, C_INODE.meta, C_INODE.directory, C_INODE.nlink + 1, C_INODE.nsubdirs, C_INODE.size); aubifs_core_journal_add3#(ND1, ND2, ND3, RI, FI, RO, FO; ADR1, ADR2, ADR3, FS, LOG; CSYNCED, ERR); if ERR = ESUCCESS then {aubifs_core_index_store#(KEY1, ADR1, FI, RO, FO, FS, LOG, CSYNCED; RI); aubifs_core_index_store#(KEY2, ADR2, FI, RO, FO, FS, LOG, CSYNCED; RI); aubifs_core_index_store#(KEY3, ADR3, FI, RO, FO, FS, LOG, CSYNCED; RI); NEW_DENT := mkdentry(NEW_DENT.name, INO); P_INODE := mkinode(P_INODE.ino, ND1.meta, ND1.directory, ND1.nlink, ND1.nsubdirs, ND1.size); C_INODE := mkinode(INO, ND3.meta, ND3.directory, ND3.nlink, ND3.nsubdirs, ND3.size)}} else abort } | An Axiom |
| rmdir | aubifs_rmdir#(FI, FO; P_INODE, C_INODE, DENT, ERR, RI, RO, FS, LOG, CSYNCED) {if pre-rmdir(P_INODE, C_INODE, DENT, FS, RI, RO) then choose INO, ADR1, ADR2, ADR3, KEY1, KEY2, KEY3, ND1, ND2, ND3 with INO = C_INODE.ino in {KEY1 := inodekey(P_INODE.ino); KEY2 := dentrykey(P_INODE.ino, DENT.name); KEY3 := inodekey(C_INODE.ino); ND1 := inodenode(KEY1, P_INODE.meta, P_INODE.directory, P_INODE.nlink, P_INODE.nsubdirs - 1, P_INODE.size - 1); ND2 := dentrynode(KEY2, 0); ND3 := inodenode(KEY3, C_INODE.meta, C_INODE.directory, C_INODE.nlink - 1, C_INODE.nsubdirs, C_INODE.size); aubifs_core_journal_add3#(ND1, ND2, ND3, RI, FI, RO, FO; ADR1, ADR2, ADR3, FS, LOG; CSYNCED, ERR); if ERR = ESUCCESS then {aubifs_core_index_store#(KEY1, ADR1, FI, RO, FO, FS, LOG, CSYNCED; RI); aubifs_core_index_remove#(KEY2, FI, RO, FO, FS, LOG, CSYNCED; RI); aubifs_core_index_store#(KEY3, ADR3, FI, RO, FO, FS, LOG, CSYNCED; RI); aubifs_core_orphans_insert#(KEY3, RI, FI, FO, FS, LOG, CSYNCED; RO); DENT := negdentry(DENT.name); P_INODE := mkinode(P_INODE.ino, ND1.meta, ND1.directory, ND1.nlink, ND1.nsubdirs, ND1.size); C_INODE := mkinode(INO, ND3.meta, ND3.directory, ND3.nlink, ND3.nsubdirs, ND3.size)}} else abort } | An Axiom |
| replayone | aubifs_replayone#(ADR, FI, RO, FO, FS, LOG, CSYNCED; ERR, RI) {choose ND, EXISTS with true in {aubifs_core_journal_get#(ADR, RI, FI, RO, FO, FS, LOG, CSYNCED; ND; ERR); if ERR = ESUCCESS then {if ND.inode? then if ND.nlink ≠ 0 ∨ ND.key.ino = ROOT_INO then aubifs_core_index_store#(ND.key, ADR, FI, RO, FO, FS, LOG, CSYNCED; RI) else {if ¬ ND.directory then aubifs_core_index_truncate#(ND.key, 0, FI, RO, FO, FS, LOG, CSYNCED; RI); if ERR = ESUCCESS then aubifs_core_index_remove#(ND.key, FI, RO, FO, FS, LOG, CSYNCED; RI)}; if ND.dentry? then if ND.ino ≠ 0 then aubifs_core_index_store#(ND.key, ADR, FI, RO, FO, FS, LOG, CSYNCED; RI) else aubifs_core_index_remove#(ND.key, FI, RO, FO, FS, LOG, CSYNCED; RI); if ND.data? then {let KEY = inodekey(ND.key.ino) in aubifs_core_index_contains#(KEY, RI, FI, RO, FO, FS, LOG, CSYNCED; EXISTS; ERR); if ERR = ESUCCESS ∧ EXISTS then aubifs_core_index_store#(ND.key, ADR, FI, RO, FO, FS, LOG, CSYNCED; RI)}; if ND.trunc? then aubifs_core_index_truncate#(ND.key, ND.size, FI, RO, FO, FS, LOG, CSYNCED; RI)}} } | An Axiom |
| replayorphans | aubifs_replayorphans#(FI, FO, FS, LOG, CSYNCED; KS, ERR, RI, RO) {while KS ≠ ∅ do {/* (replayorphans-prepost: invariant KS = RO ∧ RO ⊆ RO` ∧ RI ⊖ RO = RI` ⊖ RO` ∧ KS.inodes? wfbound # KS) */; choose KEY with KEY ∈ KS in {aubifs_core_index_truncate#(KEY, 0, FI, RO, FO, FS, LOG, CSYNCED; RI); aubifs_core_index_remove#(KEY, FI, RO, FO, FS, LOG, CSYNCED; RI); aubifs_core_orphans_remove#(KEY, RI, FI, FO, FS, LOG, CSYNCED; RO); KS := KS -- KEY}} } | An Axiom |
| replaylog | aubifs_replaylog#(AX, FI, RO, FO, FS, LOG, CSYNCED; ERR, RI) {while ERR = ESUCCESS ∧ AX ≠ [] do {/* (replaylog-prog : invariant (ERR = ESUCCESS ∨ ⌊ERR⌋ ) ∧ (ERR = ESUCCESS → (∃ ax0. AX` = ax0 + AX ∧ replay-safe(AX, FS, RI) ∧ RI = replay-log(ax0, FS`, RI`))) wfbound # AX) */; let ADR = AX.head in aubifs_replayone#(ADR, FI, RO, FO, FS, LOG, CSYNCED; ERR, RI); AX := AX.tail} } | An Axiom |
| iget-check | aubifs_iget_check#(INO, RI, FI, RO, FO, FS, LOG, CSYNCED; EXISTS, INODE, ERR) {choose ND, KEY with true in if ERR = ESUCCESS then {KEY := inodekey(INO); aubifs_core_index_lookup#(KEY, RI, FI, RO, FO, FS, LOG, CSYNCED; EXISTS, ND; ERR); if ERR = ESUCCESS ∧ EXISTS then INODE := mkinode(INO, ND.meta, ND.directory, ND.nlink, (ND.directory ⊃ ND.nsubdirs;0), ND.size)} } | An Axiom |
| write-inode | aubifs_write_inode#(INODE, FI, RO, FO; ERR, RI, FS, LOG, CSYNCED) {if pre-write-inode(INODE, FS, RI, RO) then choose KEY, ND, ADR with true in {KEY := inodekey(INODE.ino); ND := inodenode(KEY, INODE.meta, INODE.directory, INODE.nlink, INODE.nsubdirs, INODE.size); aubifs_core_journal_add1#(ND, RI, FI, RO, FO; ADR, FS, LOG; CSYNCED, ERR); if ERR = ESUCCESS then aubifs_core_index_store#(KEY, ADR, FI, RO, FO, FS, LOG, CSYNCED; RI)} else abort } | An Axiom |
| check-commit | aubifs_check_commit#(RI, RO; ERR, FI, FO, FS, LOG, CSYNCED){aubifs_core_check_commit#(RI, RO; FI, FO, FS, LOG, CSYNCED; ERR)} | An Axiom |
| format | aubifs_format#(VOLSIZE, DOSYNC, SIZE, MD; RI, FI, RO, FO, FS, LOG, CSYNCED; ERR) {if SIZE = LEB_SIZE then {aubifs_core_format#(VOLSIZE, SIZE, DOSYNC; ; RI, FI, RO, FO, FS, LOG, CSYNCED, ERR); if ERR = ESUCCESS then let KEY = inodekey(ROOT_INO), ADR = ? in let ND = inodenode(KEY, MD, true, 0, 0, 0) in {aubifs_core_journal_add1#(ND, RI, FI, RO, FO; ADR, FS, LOG; CSYNCED, ERR); if ERR = ESUCCESS then aubifs_core_index_store#(KEY, ADR, FI, RO, FO, FS, LOG, CSYNCED; RI); if ERR = ESUCCESS then aubifs_core_journal_sync#(RI, FI, RO, FO, FS, LOG; ; CSYNCED, ERR)}} else abort } | An Axiom |
| gc | aubifs_gc#(FI, RO, FO; RI, FS, LOG, CSYNCED) {if orphans-cons(FS, RI, RO) then aubifs_core_journal_gc#(FI, RO, FO; RI, FS, LOG; CSYNCED) else abort} | An Axiom |
| sync | aubifs_sync#(RI, FI, RO, FO, FS, LOG; CSYNCED; ERR){aubifs_core_journal_sync#(RI, FI, RO, FO, FS, LOG; ; CSYNCED, ERR)} | An Axiom |
| fsync | aubifs_fsync#(INODE, ISDATASYNC; ; ERR){ERR := ESUCCESS} | An Axiom |
| fsyncdir | aubifs_fsyncdir#(INODE, ISDATASYNC; ; ERR){ERR := ESUCCESS} | An Axiom |
| rename-overwrite-reparent | aubifs_rename_overwrite_reparent# (IS_DIR, OLD_CHILD_INODE, FI, FO; OLD_PARENT_INODE, NEW_PARENT_INODE, NEW_CHILD_INODE, OLD_DENT, NEW_DENT, ERR, RI, RO, FS, LOG, CSYNCED) {if pre-rename-overwrite-reparent(OLD_PARENT_INODE, OLD_DENT, OLD_CHILD_INODE, NEW_PARENT_INODE, NEW_DENT, NEW_CHILD_INODE, FS, RI, RO) ∧ (IS_DIR ↔ OLD_CHILD_INODE.directory) then choose KEY1, KEY2, KEY3, KEY4, KEY5, ND1, ND2, ND3, ND4, ND5, ADR1, ADR2, ADR3, ADR4, ADR5 with true in {KEY1 := dentrykey(OLD_PARENT_INODE.ino, OLD_DENT.name); ND1 := dentrynode(KEY1, 0); KEY2 := dentrykey(NEW_PARENT_INODE.ino, NEW_DENT.name); ND2 := dentrynode(KEY2, OLD_DENT.ino); KEY3 := inodekey(OLD_PARENT_INODE.ino); ND3 := inodenode (KEY3, OLD_PARENT_INODE.meta, OLD_PARENT_INODE.directory, OLD_PARENT_INODE.nlink, OLD_PARENT_INODE.nsubdirs - (IS_DIR ⊃ 1;0), OLD_PARENT_INODE.size - 1); KEY4 := inodekey(NEW_PARENT_INODE.ino); ND4 := inodenode (KEY4, NEW_PARENT_INODE.meta, NEW_PARENT_INODE.directory, NEW_PARENT_INODE.nlink, NEW_PARENT_INODE.nsubdirs, NEW_PARENT_INODE.size); KEY5 := inodekey(NEW_DENT.ino); ND5 := inodenode (KEY5, NEW_CHILD_INODE.meta, NEW_CHILD_INODE.directory, NEW_CHILD_INODE.nlink - 1, NEW_CHILD_INODE.nsubdirs, NEW_CHILD_INODE.size); aubifs_core_journal_add5#(ND1, ND2, ND3, ND4, ND5, RI, FI, RO, FO; ADR1, ADR2, ADR3, ADR4, ADR5, FS, LOG; CSYNCED, ERR); if ERR = ESUCCESS then {aubifs_core_index_remove#(KEY1, FI, RO, FO, FS, LOG, CSYNCED; RI); aubifs_core_index_store#(KEY2, ADR2, FI, RO, FO, FS, LOG, CSYNCED; RI); aubifs_core_index_store#(KEY3, ADR3, FI, RO, FO, FS, LOG, CSYNCED; RI); aubifs_core_index_store#(KEY4, ADR4, FI, RO, FO, FS, LOG, CSYNCED; RI); aubifs_core_index_store#(KEY5, ADR5, FI, RO, FO, FS, LOG, CSYNCED; RI); if ND5.nlink = 0 then aubifs_core_orphans_insert#(KEY5, RI, FI, FO, FS, LOG, CSYNCED; RO); NEW_DENT := mkdentry(NEW_DENT.name, OLD_DENT.ino); OLD_DENT := negdentry(OLD_DENT.name); OLD_PARENT_INODE := mkinode(OLD_PARENT_INODE.ino, ND3.meta, ND3.directory, ND3.nlink, ND3.nsubdirs, ND3.size); NEW_CHILD_INODE := mkinode(NEW_CHILD_INODE.ino, ND5.meta, ND5.directory, ND5.nlink, ND5.nsubdirs, ND5.size)}} else abort } | An Axiom |
| rename-overwrite-keep-parent | aubifs_rename_overwrite_keep_parent# (IS_DIR, OLD_CHILD_INODE, FI, FO; PARENT_INODE, NEW_CHILD_INODE, OLD_DENT, NEW_DENT, ERR, RI, RO, FS, LOG, CSYNCED) {if pre-rename-overwrite-keep-parent(PARENT_INODE, OLD_DENT, OLD_CHILD_INODE, NEW_DENT, NEW_CHILD_INODE, FS, RI, RO) ∧ (IS_DIR ↔ OLD_CHILD_INODE.directory) then choose KEY1, KEY2, KEY3, KEY4, ND1, ND2, ND3, ND4, ADR1, ADR2, ADR3, ADR4 with true in let IDENTITY = OLD_DENT = NEW_DENT in {KEY1 := dentrykey(PARENT_INODE.ino, OLD_DENT.name); ND1 := dentrynode(KEY1, 0); KEY2 := dentrykey(PARENT_INODE.ino, NEW_DENT.name); ND2 := dentrynode(KEY2, OLD_DENT.ino); KEY3 := inodekey(PARENT_INODE.ino); KEY4 := inodekey(NEW_DENT.ino); if ¬ IDENTITY then {ND3 := inodenode (KEY3, PARENT_INODE.meta, PARENT_INODE.directory, PARENT_INODE.nlink, PARENT_INODE.nsubdirs - (IS_DIR ⊃ 1;0), PARENT_INODE.size - 1); ND4 := inodenode (KEY4, NEW_CHILD_INODE.meta, NEW_CHILD_INODE.directory, NEW_CHILD_INODE.nlink - 1, NEW_CHILD_INODE.nsubdirs, NEW_CHILD_INODE.size)} else {ND3 := inodenode(KEY3, PARENT_INODE.meta, PARENT_INODE.directory, PARENT_INODE.nlink, PARENT_INODE.nsubdirs, PARENT_INODE.size); ND4 := inodenode (KEY4, NEW_CHILD_INODE.meta, NEW_CHILD_INODE.directory, NEW_CHILD_INODE.nlink, NEW_CHILD_INODE.nsubdirs, NEW_CHILD_INODE.size)}; aubifs_core_journal_add4#(ND1, ND2, ND3, ND4, RI, FI, RO, FO; ADR1, ADR2, ADR3, ADR4, FS, LOG; CSYNCED, ERR); if ERR = ESUCCESS then {aubifs_core_index_remove#(KEY1, FI, RO, FO, FS, LOG, CSYNCED; RI); aubifs_core_index_store#(KEY2, ADR2, FI, RO, FO, FS, LOG, CSYNCED; RI); aubifs_core_index_store#(KEY3, ADR3, FI, RO, FO, FS, LOG, CSYNCED; RI); aubifs_core_index_store#(KEY4, ADR4, FI, RO, FO, FS, LOG, CSYNCED; RI); if ND4.nlink = 0 then aubifs_core_orphans_insert#(KEY4, RI, FI, FO, FS, LOG, CSYNCED; RO); NEW_DENT := mkdentry(NEW_DENT.name, OLD_DENT.ino); OLD_DENT := negdentry(OLD_DENT.name); PARENT_INODE := mkinode(PARENT_INODE.ino, ND3.meta, ND3.directory, ND3.nlink, ND3.nsubdirs, ND3.size); NEW_CHILD_INODE := mkinode(NEW_CHILD_INODE.ino, ND4.meta, ND4.directory, ND4.nlink, ND4.nsubdirs, ND4.size)}} else abort } | An Axiom |
| rename-new-keep-parent | aubifs_rename_new_keep_parent#(IS_DIR, OLD_CHILD_INODE, FI, RO, FO; PARENT_INODE, OLD_DENT, NEW_DENT, ERR, RI, FS, LOG, CSYNCED) {if pre-rename-new-keep-parent(PARENT_INODE, OLD_DENT, OLD_CHILD_INODE, NEW_DENT, FS, RI, RO) ∧ (IS_DIR ↔ OLD_CHILD_INODE.directory) then choose KEY1, KEY2, KEY3, ND1, ND2, ND3, ADR1, ADR2, ADR3 with true in {KEY1 := dentrykey(PARENT_INODE.ino, OLD_DENT.name); ND1 := dentrynode(KEY1, 0); KEY2 := dentrykey(PARENT_INODE.ino, NEW_DENT.name); ND2 := dentrynode(KEY2, OLD_DENT.ino); KEY3 := inodekey(PARENT_INODE.ino); ND3 := inodenode(KEY3, PARENT_INODE.meta, PARENT_INODE.directory, PARENT_INODE.nlink, PARENT_INODE.nsubdirs, PARENT_INODE.size); aubifs_core_journal_add3#(ND1, ND2, ND3, RI, FI, RO, FO; ADR1, ADR2, ADR3, FS, LOG; CSYNCED, ERR); if ERR = ESUCCESS then {aubifs_core_index_remove#(KEY1, FI, RO, FO, FS, LOG, CSYNCED; RI); aubifs_core_index_store#(KEY2, ADR2, FI, RO, FO, FS, LOG, CSYNCED; RI); aubifs_core_index_store#(KEY3, ADR3, FI, RO, FO, FS, LOG, CSYNCED; RI); NEW_DENT := mkdentry(NEW_DENT.name, OLD_DENT.ino); OLD_DENT := negdentry(OLD_DENT.name); PARENT_INODE := mkinode(PARENT_INODE.ino, ND3.meta, ND3.directory, ND3.nlink, ND3.nsubdirs, ND3.size)}} else abort } | An Axiom |
| rename-new-reparent | aubifs_rename_new_reparent# (IS_DIR, OLD_CHILD_INODE, FI, RO, FO; OLD_PARENT_INODE, NEW_PARENT_INODE, OLD_DENT, NEW_DENT, ERR, RI, FS, LOG, CSYNCED) {if pre-rename-new-reparent(OLD_PARENT_INODE, OLD_DENT, OLD_CHILD_INODE, NEW_PARENT_INODE, NEW_DENT, FS, RI, RO) ∧ (IS_DIR ↔ OLD_CHILD_INODE.directory) then choose KEY1, KEY2, KEY3, KEY4, ND1, ND2, ND3, ND4, ADR1, ADR2, ADR3, ADR4 with true in {KEY1 := dentrykey(OLD_PARENT_INODE.ino, OLD_DENT.name); ND1 := dentrynode(KEY1, 0); KEY2 := dentrykey(NEW_PARENT_INODE.ino, NEW_DENT.name); ND2 := dentrynode(KEY2, OLD_DENT.ino); KEY3 := inodekey(OLD_PARENT_INODE.ino); ND3 := inodenode (KEY3, OLD_PARENT_INODE.meta, OLD_PARENT_INODE.directory, OLD_PARENT_INODE.nlink, OLD_PARENT_INODE.nsubdirs - (IS_DIR ⊃ 1;0), OLD_PARENT_INODE.size - 1); KEY4 := inodekey(NEW_PARENT_INODE.ino); ND4 := inodenode (KEY4, NEW_PARENT_INODE.meta, NEW_PARENT_INODE.directory, NEW_PARENT_INODE.nlink, NEW_PARENT_INODE.nsubdirs + (IS_DIR ⊃ 1;0), NEW_PARENT_INODE.size + 1); aubifs_core_journal_add4#(ND1, ND2, ND3, ND4, RI, FI, RO, FO; ADR1, ADR2, ADR3, ADR4, FS, LOG; CSYNCED, ERR); if ERR = ESUCCESS then {aubifs_core_index_remove#(KEY1, FI, RO, FO, FS, LOG, CSYNCED; RI); aubifs_core_index_store#(KEY2, ADR2, FI, RO, FO, FS, LOG, CSYNCED; RI); aubifs_core_index_store#(KEY3, ADR3, FI, RO, FO, FS, LOG, CSYNCED; RI); aubifs_core_index_store#(KEY4, ADR4, FI, RO, FO, FS, LOG, CSYNCED; RI); NEW_DENT := mkdentry(NEW_DENT.name, OLD_DENT.ino); OLD_DENT := negdentry(OLD_DENT.name); OLD_PARENT_INODE := mkinode(OLD_PARENT_INODE.ino, ND3.meta, ND3.directory, ND3.nlink, ND3.nsubdirs, ND3.size); NEW_PARENT_INODE := mkinode(NEW_PARENT_INODE.ino, ND4.meta, ND4.directory, ND4.nlink, ND4.nsubdirs, ND4.size)}} else abort } | An Axiom |
| inv-gc | ubifs-cons(fs, ri, ro, fi, fo, log), replay-cons-strong(fs, ri, ro, fi, fo, log), file-node-cons(fs, ri), orphans-cons(fs, ri, ro), ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes?, orphans-cons(fs, ri, ro) ⊦ ⟪aubifs_gc#(fi, ro, fo; ri, fs, log, boolvar)⟫ ( ubifs-cons(fs, ri, ro, fi, fo, log) ∧ replay-cons-strong(fs, ri, ro, fi, fo, log) ∧ file-node-cons(fs, ri) ∧ orphans-cons(fs, ri, ro) ∧ ri-inj(ri) ∧ log-cons(log, fs)) | A Proof Obligation |
| inv-format | pageno = LEB_SIZE ⊦ ⟪aubifs_format#(pageno0, boolvar, pageno, md; ri, fi, ro, fo, fs, log, boolvar0; err)⟫ ( err = ESUCCESS → boolvar0 ∧ ubifs-cons(fs, ri, ro, fi, fo, log) ∧ replay-cons-strong(fs, ri, ro, fi, fo, log) ∧ file-node-cons(fs, ri) ∧ orphans-cons(fs, ri, ro) ∧ ri-inj(ri) ∧ ri-inj(fi) ∧ log-cons(log, fs) ∧ ro.inodes? ∧ fo.inodes?) | A Proof Obligation |
| inv-evict | ubifs-cons(fs, ri, ro, fi, fo, log), replay-cons-strong(fs, ri, ro, fi, fo, log), file-node-cons(fs, ri), orphans-cons(fs, ri, ro), ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes?, pre-evict(inode.ino, fs, ri, ro) ⊦ ⟪aubifs_evict#(inode, fi, fo, fs, log, boolvar; err, ri, ro)⟫ ( ubifs-cons(fs, ri, ro, fi, fo, log) ∧ replay-cons-strong(fs, ri, ro, fi, fo, log) ∧ file-node-cons(fs, ri) ∧ orphans-cons(fs, ri, ro) ∧ ri-inj(ri) ∧ ro.inodes?) | A Proof Obligation |
| inv-write-inode | ubifs-cons(fs, ri, ro, fi, fo, log), replay-cons-strong(fs, ri, ro, fi, fo, log), file-node-cons(fs, ri), orphans-cons(fs, ri, ro), ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes?, pre-write-inode(inode, fs, ri, ro) ⊦ ⟪aubifs_write_inode#(inode, fi, ro, fo; err, ri, fs, log, boolvar)⟫ ( ubifs-cons(fs, ri, ro, fi, fo, log) ∧ replay-cons-strong(fs, ri, ro, fi, fo, log) ∧ file-node-cons(fs, ri) ∧ orphans-cons(fs, ri, ro) ∧ ri-inj(ri) ∧ log-cons(log, fs)) | A Proof Obligation |
| inv-truncate | ubifs-cons(fs, ri, ro, fi, fo, log), replay-cons-strong(fs, ri, ro, fi, fo, log), file-node-cons(fs, ri), orphans-cons(fs, ri, ro), ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes?, pre-truncate(inode, n, pageno, buf-opt, fs, ri, ro) ⊦ ⟪aubifs_truncate#(n, pageno, fi, ro, fo; buf-opt, inode, boolvar, err, ri, fs, log, boolvar0)⟫ ( ubifs-cons(fs, ri, ro, fi, fo, log) ∧ replay-cons-strong(fs, ri, ro, fi, fo, log) ∧ file-node-cons(fs, ri) ∧ orphans-cons(fs, ri, ro) ∧ ri-inj(ri) ∧ log-cons(log, fs)) | A Proof Obligation |
| inv-readdir | ubifs-cons(fs, ri, ro, fi, fo, log), replay-cons-strong(fs, ri, ro, fi, fo, log), file-node-cons(fs, ri), orphans-cons(fs, ri, ro), ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes?, pre-readdir(inode.ino, fs, ri) ⊦ ⟪aubifs_readdir#(inode, ri, fi, ro, fo, fs, log, boolvar; strings, err)⟫ true | A Proof Obligation |
| inv-writepage | ubifs-cons(fs, ri, ro, fi, fo, log), replay-cons-strong(fs, ri, ro, fi, fo, log), file-node-cons(fs, ri), orphans-cons(fs, ri, ro), ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes?, pre-writepage(inode, pageno, buf, fs, ri) ⊦ ⟪aubifs_writepage#(inode, pageno, buf, fi, ro, fo; err, ri, fs, log, boolvar)⟫ ( ubifs-cons(fs, ri, ro, fi, fo, log) ∧ replay-cons-strong(fs, ri, ro, fi, fo, log) ∧ file-node-cons(fs, ri) ∧ orphans-cons(fs, ri, ro) ∧ ri-inj(ri) ∧ log-cons(log, fs)) | A Proof Obligation |
| inv-readpage | ubifs-cons(fs, ri, ro, fi, fo, log), replay-cons-strong(fs, ri, ro, fi, fo, log), file-node-cons(fs, ri), orphans-cons(fs, ri, ro), ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes?, pre-readpage(inode, pageno, buf, fs, ri) ⊦ ⟪aubifs_readpage#(inode, pageno, ri, fi, ro, fo, fs, log, boolvar; buf, err)⟫ true | A Proof Obligation |
| inv-renam | ubifs-cons(fs, ri, ro, fi, fo, log), replay-cons-strong(fs, ri, ro, fi, fo, log), file-node-cons(fs, ri), orphans-cons(fs, ri, ro), ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes?, pre-rename(old_parent_inode, old_dent, old_child_inode, new_parent_inode, new_dent, new_child_inode, fs, ri, ro) ⊦ ⟪aubifs_rename#(fi, fo; old_parent_inode, new_parent_inode, old_child_inode, new_child_inode, old_dent, new_dent, err, ri, ro, fs, log, boolvar)⟫ ( ubifs-cons(fs, ri, ro, fi, fo, log) ∧ replay-cons-strong(fs, ri, ro, fi, fo, log) ∧ file-node-cons(fs, ri) ∧ orphans-cons(fs, ri, ro) ∧ ri-inj(ri) ∧ log-cons(log, fs) ∧ ro.inodes?) | A Proof Obligation |
| inv-link | ubifs-cons(fs, ri, ro, fi, fo, log), replay-cons-strong(fs, ri, ro, fi, fo, log), file-node-cons(fs, ri), orphans-cons(fs, ri, ro), ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes?, pre-link(p_inode, c_inode, old_dent, new_dent, fs, ri, ro) ⊦ ⟪aubifs_link#(old_dent, fi, ro, fo; p_inode, c_inode, new_dent, err, ri, fs, log, boolvar)⟫ ( ubifs-cons(fs, ri, ro, fi, fo, log) ∧ replay-cons-strong(fs, ri, ro, fi, fo, log) ∧ file-node-cons(fs, ri) ∧ orphans-cons(fs, ri, ro) ∧ ri-inj(ri) ∧ log-cons(log, fs)) | A Proof Obligation |
| inv-rmdir | ubifs-cons(fs, ri, ro, fi, fo, log), replay-cons-strong(fs, ri, ro, fi, fo, log), file-node-cons(fs, ri), orphans-cons(fs, ri, ro), ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes?, pre-rmdir(p_inode, c_inode, dent, fs, ri, ro) ⊦ ⟪aubifs_rmdir#(fi, fo; p_inode, c_inode, dent, err, ri, ro, fs, log, boolvar)⟫ ( ubifs-cons(fs, ri, ro, fi, fo, log) ∧ replay-cons-strong(fs, ri, ro, fi, fo, log) ∧ file-node-cons(fs, ri) ∧ orphans-cons(fs, ri, ro) ∧ ri-inj(ri) ∧ log-cons(log, fs) ∧ ro.inodes?) | A Proof Obligation |
| inv-unlink | ubifs-cons(fs, ri, ro, fi, fo, log), replay-cons-strong(fs, ri, ro, fi, fo, log), file-node-cons(fs, ri), orphans-cons(fs, ri, ro), ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes?, pre-unlink(p_inode, c_inode, dent, fs, ri, ro) ⊦ ⟪aubifs_unlink#(fi, fo; p_inode, c_inode, dent, err, ri, ro, fs, log, boolvar)⟫ ( ubifs-cons(fs, ri, ro, fi, fo, log) ∧ replay-cons-strong(fs, ri, ro, fi, fo, log) ∧ file-node-cons(fs, ri) ∧ orphans-cons(fs, ri, ro) ∧ ri-inj(ri) ∧ log-cons(log, fs) ∧ ro.inodes?) | A Proof Obligation |
| inv-mkdir | ubifs-cons(fs, ri, ro, fi, fo, log), replay-cons-strong(fs, ri, ro, fi, fo, log), file-node-cons(fs, ri), orphans-cons(fs, ri, ro), ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes?, pre-mkdir(p_inode, dent, md, fs, ri, ro) ⊦ ⟪aubifs_mkdir#(md, fi, ro, fo; p_inode, c_inode, dent, err, ri, fs, log, boolvar)⟫ ( ubifs-cons(fs, ri, ro, fi, fo, log) ∧ replay-cons-strong(fs, ri, ro, fi, fo, log) ∧ file-node-cons(fs, ri) ∧ orphans-cons(fs, ri, ro) ∧ ri-inj(ri) ∧ log-cons(log, fs)) | A Proof Obligation |
| inv-create | ubifs-cons(fs, ri, ro, fi, fo, log), replay-cons-strong(fs, ri, ro, fi, fo, log), file-node-cons(fs, ri), orphans-cons(fs, ri, ro), ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes?, pre-create(p_inode, dent, md, fs, ri, ro) ⊦ ⟪aubifs_create#(md, fi, ro, fo; p_inode, c_inode, dent, err, ri, fs, log, boolvar)⟫ ( ubifs-cons(fs, ri, ro, fi, fo, log) ∧ replay-cons-strong(fs, ri, ro, fi, fo, log) ∧ file-node-cons(fs, ri) ∧ orphans-cons(fs, ri, ro) ∧ ri-inj(ri) ∧ log-cons(log, fs)) | A Proof Obligation |
| inv-lookup | ubifs-cons(fs, ri, ro, fi, fo, log), replay-cons-strong(fs, ri, ro, fi, fo, log), file-node-cons(fs, ri), orphans-cons(fs, ri, ro), ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes?, pre-lookup(p_ino, dent, fs, ri, ro) ⊦ ⟪aubifs_lookup#(p_ino, ri, fi, ro, fo, fs, log, boolvar; dent, err)⟫ true | A Proof Obligation |
| inv-iget | ubifs-cons(fs, ri, ro, fi, fo, log), replay-cons-strong(fs, ri, ro, fi, fo, log), file-node-cons(fs, ri), orphans-cons(fs, ri, ro), ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes?, pre-iget(ino, fs, ri) ⊦ ⟪aubifs_iget#(ino, ri, fi, ro, fo, fs, log, boolvar; inode, err)⟫ true | A Proof Obligation |
| inv-replay | fi = fi0, fo = fo0, fs = fs0, log = log0, boolvar, ubifs-cons(fs0, ri, ro, fi0, fo0, log0), replay-cons-strong(fs0, ri, ro, fi0, fo0, log0), file-node-cons(fs0, ri), orphans-cons(fs0, ri, ro), ri-inj(ri), ri-inj(fi0), log-cons(log0, fs0), ro.inodes?, fo0.inodes? ⊦ ⟪aubifs_replay#(boolvar0; ri0, fi, ro0, fo, fs, log, boolvar1; err)⟫ ( err = ESUCCESS → boolvar1 ∧ ubifs-cons(fs, ri0, ro0, fi, fo, log) ∧ replay-cons-strong(fs, ri0, ro0, fi, fo, log) ∧ file-node-cons(fs, ri0) ∧ orphans-cons(fs, ri0, ro0) ∧ ri-inj(ri0) ∧ ri-inj(fi) ∧ log-cons(log, fs) ∧ ro0.inodes? ∧ fo.inodes?) | A Proof Obligation |
| inv-check-commit | ubifs-cons(fs, ri, ro, fi, fo, log), replay-cons-strong(fs, ri, ro, fi, fo, log), file-node-cons(fs, ri), orphans-cons(fs, ri, ro), ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes? ⊦ ⟪aubifs_check_commit#(ri, ro; err, fi, fo, fs, log, boolvar)⟫ ( ubifs-cons(fs, ri, ro, fi, fo, log) ∧ replay-cons-strong(fs, ri, ro, fi, fo, log) ∧ file-node-cons(fs, ri) ∧ orphans-cons(fs, ri, ro) ∧ ri-inj(fi) ∧ log-cons(log, fs) ∧ fo.inodes?) | A Proof Obligation |
| inv-sync | ubifs-cons(fs, ri, ro, fi, fo, log), replay-cons-strong(fs, ri, ro, fi, fo, log), file-node-cons(fs, ri), orphans-cons(fs, ri, ro), ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes? ⊦ ⟪aubifs_sync#(ri, fi, ro, fo, fs, log; boolvar; err)⟫ true | A Proof Obligation |
| inv-fsync | ⊦ ⟪aubifs_fsync#(inode, boolvar; ; err)⟫ true | A Proof Obligation |
| inv-fsyncdir | ⊦ ⟪aubifs_fsyncdir#(inode, boolvar; ; err)⟫ true | A Proof Obligation |
| inv-rename-overwrite-reparent | ubifs-cons(fs, ri, ro, fi, fo, log), replay-cons-strong(fs, ri, ro, fi, fo, log), file-node-cons(fs, ri), orphans-cons(fs, ri, ro), ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes?, pre-rename-overwrite-reparent(old_parent_inode, old_dent, old_child_inode, new_parent_inode, new_dent, new_child_inode, fs, ri, ro), boolvar ↔ old_child_inode.directory ⊦ ⟪aubifs_rename_overwrite_reparent# (boolvar, old_child_inode, fi, fo; old_parent_inode, new_parent_inode, new_child_inode, old_dent, new_dent, err, ri, ro, fs, log, boolvar0)⟫ ( ubifs-cons(fs, ri, ro, fi, fo, log) ∧ replay-cons-strong(fs, ri, ro, fi, fo, log) ∧ file-node-cons(fs, ri) ∧ orphans-cons(fs, ri, ro) ∧ ri-inj(ri) ∧ log-cons(log, fs) ∧ ro.inodes?) | A Proof Obligation |
| inv-rename-new-keep-parent | ubifs-cons(fs, ri, ro, fi, fo, log), replay-cons-strong(fs, ri, ro, fi, fo, log), file-node-cons(fs, ri), orphans-cons(fs, ri, ro), ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes?, pre-rename-new-keep-parent(parent_inode, old_dent, old_child_inode, new_dent, fs, ri, ro), boolvar ↔ old_child_inode.directory ⊦ ⟪aubifs_rename_new_keep_parent#(boolvar, old_child_inode, fi, ro, fo; parent_inode, old_dent, new_dent, err, ri, fs, log, boolvar0)⟫ ( ubifs-cons(fs, ri, ro, fi, fo, log) ∧ replay-cons-strong(fs, ri, ro, fi, fo, log) ∧ file-node-cons(fs, ri) ∧ orphans-cons(fs, ri, ro) ∧ ri-inj(ri) ∧ log-cons(log, fs)) | A Proof Obligation |
| inv-rename-new-reparent | ubifs-cons(fs, ri, ro, fi, fo, log), replay-cons-strong(fs, ri, ro, fi, fo, log), file-node-cons(fs, ri), orphans-cons(fs, ri, ro), ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes?, pre-rename-new-reparent(old_parent_inode, old_dent, old_child_inode, new_parent_inode, new_dent, fs, ri, ro), boolvar ↔ old_child_inode.directory ⊦ ⟪aubifs_rename_new_reparent# (boolvar, old_child_inode, fi, ro, fo; old_parent_inode, new_parent_inode, old_dent, new_dent, err, ri, fs, log, boolvar0)⟫ ( ubifs-cons(fs, ri, ro, fi, fo, log) ∧ replay-cons-strong(fs, ri, ro, fi, fo, log) ∧ file-node-cons(fs, ri) ∧ orphans-cons(fs, ri, ro) ∧ ri-inj(ri) ∧ log-cons(log, fs)) | A Proof Obligation |
| inv-rename-overwrite-keep-parent | ubifs-cons(fs, ri, ro, fi, fo, log), replay-cons-strong(fs, ri, ro, fi, fo, log), file-node-cons(fs, ri), orphans-cons(fs, ri, ro), ri-inj(ri), ri-inj(fi), log-cons(log, fs), ro.inodes?, fo.inodes?, pre-rename-overwrite-keep-parent(parent_inode, old_dent, old_child_inode, new_dent, new_child_inode, fs, ri, ro), boolvar ↔ old_child_inode.directory ⊦ ⟪aubifs_rename_overwrite_keep_parent# (boolvar, old_child_inode, fi, fo; parent_inode, new_child_inode, old_dent, new_dent, err, ri, ro, fs, log, boolvar0)⟫ ( ubifs-cons(fs, ri, ro, fi, fo, log) ∧ replay-cons-strong(fs, ri, ro, fi, fo, log) ∧ file-node-cons(fs, ri) ∧ orphans-cons(fs, ri, ro) ∧ ri-inj(ri) ∧ log-cons(log, fs) ∧ ro.inodes?) | A Proof Obligation |
| at-del-ri | ⊦ (ri -- key0)[key1] = (key0 = key1 ⊃ (∅)[key0];ri[key1]) | A User Theorem |
| at-diff-ri | ⊦ (ri \ ks)[key] = (key ∈ ks ⊃ (∅)[key];ri[key]) | A User Theorem |
| at-fs | ⊦ fs[adr0, nd][adr1] = (adr0 = adr1 ⊃ nd;fs[adr1]) | A User Theorem |
| at-ri | ⊦ ri[key0, adr][key1] = (key0 = key1 ⊃ adr;ri[key1]) | A User Theorem |
| data-notin-del2 | ⊦ ubifs-cons(fs, ri, ro, fi, fo, log) ∧ ¬ adr0 ∈ fs ∧ adr0 ≠ adr1 → ¬ adr0 ∈ ri[key1, adr1] -- key2 | A User Theorem |
| data-notin-other1 | ⊦ ubifs-cons(fs, ri, ro, fi, fo, log) ∧ ¬ adr0 ∈ fs ∧ adr0 ≠ adr1 → ¬ adr0 ∈ ri[key1, adr1] | A User Theorem |
| data-notin-other2 | ⊦ ubifs-cons(fs, ri, ro, fi, fo, log) ∧ ¬ adr0 ∈ fs ∧ adr0 ≠ adr1 ∧ adr0 ≠ adr2 → ¬ adr0 ∈ ri[key1, adr1][key2, adr2] | A User Theorem |
| data-ubifs-cons | ⊦ datakey(ino, n) ∈ ri ∧ ri[datakey(ino, n)] ∈ fs ∧ ubifs-cons(fs, ri, ro, fi, fo, log) → fs[ri[datakey(ino, n)]].data? | A User Theorem |
| dentry-ubifs-cons | ⊦ dentrykey(ino, str) ∈ ri ∧ ri[dentrykey(ino, str)] ∈ fs ∧ ubifs-cons(fs, ri, ro, fi, fo, log) → fs[ri[dentrykey(ino, str)]].dentry? | A User Theorem |
| elim-data | ⊦ key.data? ↔ (∃ ino, n. key = datakey(ino, n)) | A User Theorem |
| elim-dentry | ⊦ key.dentry? ↔ (∃ ino, str. key = dentrykey(ino, str)) | A User Theorem |
| elim-inode | ⊦ key.inode? ↔ (∃ ino. key = inodekey(ino)) | A User Theorem |
| in-del-ri | ⊦ key ∈ ri -- key0 ↔ key0 ≠ key ∧ key ∈ ri | A User Theorem |
| in-diff-ri | ⊦ key ∈ ri \ ks ↔ key ∈ ri ∧ ¬ key ∈ ks | A User Theorem |
| in-ri | ⊦ key0 ∈ ri[key1, adr] ↔ key0 = key1 ∨ key0 ∈ ri | A User Theorem |
| inode-ubifs-cons | ⊦ inodekey(ino) ∈ ri ∧ ri[inodekey(ino)] ∈ fs ∧ ubifs-cons(fs, ri, ro, fi, fo, log) → fs[ri[inodekey(ino)]].inode? | A User Theorem |
| replay-prog | replay-safe(log, fs, fi ⊖ fo), fo.inodes?, fs0 = fs, fi0 = fi, fo0 = fo, log0 = log ⊦ ⟪aubifs_replay#(boolvar0; ri, fi, ro, fo, fs, log, boolvar; err)⟫ ((err = ESUCCESS ∨ ⌊err⌋ ) ∧ (err = ESUCCESS → ri = replay(log, fs, fi, fo) ∧ ro = ∅ ∧ fs = fs0 ∧ fi = fi0 ∧ fo = fo0 ∧ log = log0 ∧ boolvar)) | A User Theorem |
| replaylog-prog | ri0 = ri, err = ESUCCESS, replay-safe(ax, fs, ri) ⊦ ⟪aubifs_replaylog#(ax, fi, ro, fo, fs, log, boolvar; err, ri)⟫ ((err = ESUCCESS ∨ ⌊err⌋ ) ∧ (err = ESUCCESS → ri = replay-log(ax, fs, ri0))) | A User Theorem |
| replayone-prog | ri0 = ri, replay-safe(adr ', fs, ri) ⊦ ⟪aubifs_replayone#(adr, fi, ro, fo, fs, log, boolvar; err, ri)⟫ ((err = ESUCCESS ∨ ⌊err⌋ ) ∧ (err = ESUCCESS → ri = replay-one(adr, fs[adr], ri0))) | A User Theorem |
| replayorphans-prepost | ri = ri0, ro0 = ro, ks = ro, err = ESUCCESS, ks.inodes? ⊦ ⟪aubifs_replayorphans#(fi, fo, fs, log, boolvar; ks, err, ri, ro)⟫ ((err = ESUCCESS ∨ ⌊err⌋ ) ∧ (err = ESUCCESS → ks = ro ∧ ro = ∅ ∧ ri = ri0 ⊖ ro0)) | A User Theorem |
| size-eq | ⊦ (∀ key. key ∈ ks0 ↔ key ∈ ks1) → # ks0 = # ks1 | A User Theorem |
| ubifs-cons-dentry-target-not-in-orphans | ⊦ ubifs-cons(fs, ri, ro, fi, fo, log) ∧ dentrykey(ino, str) ∈ ri ∧ fs[ri[dentrykey(ino, str)]] = dentrynode(key, m) → ¬ inodekey(m) ∈ ro | A User Theorem |
| ubifs-cons-reduce | ⊦ ubifs-cons(fs0, ri0, ro0, fi0, fo0, log0) → ( ubifs-cons(fs1, ri1, ro1, fi1, fo1, log1) ↔ ¬ inodekey(0) ∈ ri1 ∧ (ro0.inodes? → ro1.inodes?) ∧ (fo0.inodes? → fo1.inodes?) ∧ (ro0 ⊆ dom ri0 → (∀ key. key ∈ ro1 → key ∈ ri1)) ∧ (fo0 ⊆ dom fi0 → (∀ key. key ∈ fo1 → key ∈ fi1)) ∧ (¬ dups(log0) → ¬ dups(log1)) ∧ (∀ key. ( key ∈ ri0 → ri0[key] ∈ fs0 ∧ fs0[ri0[key]].key = key ∧ (key.inode? → fs0[ri0[key]].inode? ∧ key.ino ≠ 0) ∧ ( key.dentry? → fs0[ri0[key]].dentry? ∧ inodekey(key.ino) ∈ ri0 ∧ inodekey(fs0[ri0[key]].ino) ∈ ri0 ∧ ¬ inodekey(key.ino) ∈ ro0 ∧ ¬ inodekey(fs0[ri0[key]].ino) ∈ ro0 ∧ fs0[ri0[inodekey(key.ino)]].directory) ∧ ( key.data? → fs0[ri0[key]].data? ∧ inodekey(key.ino) ∈ ri0 ∧ ¬ fs0[ri0[inodekey(key.ino)]].directory ∧ # fs0[ri0[key]].data = VFS_PAGE_SIZE)) → key ∈ ri1 → ri1[key] ∈ fs1 ∧ fs1[ri1[key]].key = key ∧ (key.inode? → fs1[ri1[key]].inode? ∧ key.ino ≠ 0) ∧ ( key.dentry? → fs1[ri1[key]].dentry? ∧ inodekey(key.ino) ∈ ri1 ∧ inodekey(fs1[ri1[key]].ino) ∈ ri1 ∧ ¬ inodekey(key.ino) ∈ ro1 ∧ ¬ inodekey(fs1[ri1[key]].ino) ∈ ro1 ∧ fs1[ri1[inodekey(key.ino)]].directory) ∧ ( key.data? → fs1[ri1[key]].data? ∧ inodekey(key.ino) ∈ ri1 ∧ ¬ fs1[ri1[inodekey(key.ino)]].directory ∧ # fs1[ri1[key]].data = VFS_PAGE_SIZE)) ∧ (∀ adr. ( adr ∈ log0 → adr ∈ fs0 ∧ (fs0[adr].inode? → fs0[adr].key.inode? ∧ fs0[adr].key.ino ≠ 0) ∧ (fs0[adr].dentry? → fs0[adr].key.dentry?) ∧ (fs0[adr].data? → fs0[adr].key.data?) ∧ (fs0[adr].trunc? → fs0[adr].key.inode?)) → adr ∈ log1 → adr ∈ fs1 ∧ (fs1[adr].inode? → fs1[adr].key.inode? ∧ fs1[adr].key.ino ≠ 0) ∧ (fs1[adr].dentry? → fs1[adr].key.dentry?) ∧ (fs1[adr].data? → fs1[adr].key.data?) ∧ (fs1[adr].trunc? → fs1[adr].key.inode?))) | A User Theorem |