| fo0.inodes?, ro0.inodes?, log-cons(log0, fs0), ri-closed(ri0, fs0, ro0), ri-cons(ri0, fs0), key ∈ ro1, fo0 ⊆ dom fi0, ro0 ⊆ dom ri0, ∀ key. key ∈ ro1 → key ∈ ri1, ∀ key. key ∈ fo1 → key ∈ fi1, ∀ adr. ( adr ∈ log0 → (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?), ∀ key0. ( key0 ∈ ri0 → (key0.inode? → fs0[ri0[key0]].inode? ∧ key0.ino ≠ 0) ∧ ( key0.dentry? → fs0[ri0[key0]].dentry? ∧ inodekey(key0.ino) ∈ ri0 ∧ inodekey(fs0[ri0[key0]].ino) ∈ ri0 ∧ ¬ inodekey(key0.ino) ∈ ro0 ∧ ¬ inodekey(fs0[ri0[key0]].ino) ∈ ro0 ∧ fs0[ri0[inodekey(key0.ino)]].directory) ∧ ( key0.data? → fs0[ri0[key0]].data? ∧ inodekey(key0.ino) ∈ ri0 ∧ ¬ fs0[ri0[inodekey(key0.ino)]].directory ∧ # fs0[ri0[key0]].data = VFS_PAGE_SIZE)) → key0 ∈ ri1 → ri1[key0] ∈ fs1 ∧ fs1[ri1[key0]].key = key0 ∧ (key0.inode? → fs1[ri1[key0]].inode? ∧ key0.ino ≠ 0) ∧ ( key0.dentry? → fs1[ri1[key0]].dentry? ∧ inodekey(key0.ino) ∈ ri1 ∧ inodekey(fs1[ri1[key0]].ino) ∈ ri1 ∧ ¬ inodekey(key0.ino) ∈ ro1 ∧ ¬ inodekey(fs1[ri1[key0]].ino) ∈ ro1 ∧ fs1[ri1[inodekey(key0.ino)]].directory) ∧ ( key0.data? → fs1[ri1[key0]].data? ∧ inodekey(key0.ino) ∈ ri1 ∧ ¬ fs1[ri1[inodekey(key0.ino)]].directory ∧ # fs1[ri1[key0]].data = VFS_PAGE_SIZE) ⊦ # ro1 = 0, ro1 = ∅, dups(log0), inodekey(0) ∈ ri0, key ∈ ri1, inodekey(0) ∈ ri1 |
Used terms: key