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

View long theorem info. View the proof. 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,

Proof step 64 from proof inv-evict (previous step)

ro0.inodes?, fo.inodes?, file-node-cons(fs, (ri1 \ datakeys(inodekey(m), ri1)) -- inodekey(m)), file-node-cons(fs, ri1), log-cons(log, fs), orphans-cons(fs, (ri1 \ datakeys(inodekey(m), ri1)) -- inodekey(m), ro0 -- inodekey(m)), orphans-cons(fs, ri1, ro0), replay-cons-strong(fs, ri1, ro0, fi, fo, log), ri-inj(ri1), ri-inj(fi), ubifs-cons(fs, ri1, ro0, fi, fo, log), inodekey(m) ∈ ro0, inodekey(m) ∈ ri1, ∀ ino. inodekey(ino) ∈ ro0 → dentrykeys(inodekey(ino), ri1) = ∅, ∀ ino. inodekey(ino) ∈ ro0 → links(ino, fs, ri1) = ∅ ⊦ # ro0 = 0, m = ROOT_INO, ro0 = ∅, ubifs-cons(fs, (ri1 \ datakeys(inodekey(m), ri1)) -- inodekey(m), ro0 -- inodekey(m), fi, fo, log)

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 65:
fo.inodes?, ro0.inodes?, file-node-cons(fs, ri1), file-node-cons(fs, (ri1 \ datakeys(inodekey(m), ri1)) -- inodekey(m)), log-cons(log, fs), orphans-cons(fs, ri1, ro0), orphans-cons(fs, (ri1 \ datakeys(inodekey(m), ri1)) -- inodekey(m), ro0 -- inodekey(m)), replay-cons-strong(fs, ri1, ro0, fi, fo, log), ri-inj(fi), ri-inj(ri1), ubifs-cons(fs, ri1, ro0, fi, fo, log), inodekey(m) ∈ ri1, inodekey(m) ∈ ro0, ∀ ino. inodekey(ino) ∈ ro0 → links(ino, fs, ri1) = ∅, ∀ ino. inodekey(ino) ∈ ro0 → dentrykeys(inodekey(ino), ri1) = ∅ ⊦ # ro0 = 0, m = ROOT_INO, ro0 = ∅, (ro0 ⊆ dom ri1 → key ≠ inodekey(key.ino) ∧ key ∈ ro0 → ¬ key ∈ ri1 ∨ ¬ key.data? ∨ key.ino ≠ m) ∧ ( ri1[key0] ∈ fs ∧ fs[ri1[key0]].key = key0 ∧ (key0.inode? → fs[ri1[key0]].inode? ∧ key0.ino ≠ 0) ∧ ( key0.dentry? → fs[ri1[key0]].dentry? ∧ inodekey(key0.ino) ∈ ri1 ∧ inodekey(fs[ri1[key0]].ino) ∈ ri1 ∧ ¬ inodekey(key0.ino) ∈ ro0 ∧ ¬ inodekey(fs[ri1[key0]].ino) ∈ ro0 ∧ fs[ri1[inodekey(key0.ino)]].directory) ∧ ( key0.data? → fs[ri1[key0]].data? ∧ inodekey(key0.ino) ∈ ri1 ∧ ¬ fs[ri1[inodekey(key0.ino)]].directory ∧ # fs[ri1[key0]].data = VFS_PAGE_SIZE) → key0 ≠ inodekey(m) ∧ key0 ∈ ri1 ∧ (¬ key0.data? ∨ key0.ino ≠ m) → (key0.data? ∧ key0.ino = m ⊃ (∅)[key0];ri1[key0]) ∈ fs ∧ fs[(key0.data? ∧ key0.ino = m ⊃ (∅)[key0];ri1[key0])].key = key0 ∧ ( key0.data? → fs[ri1[key0]].data? ∧ key0.ino ≠ m ∧ inodekey(key0.ino) ∈ ri1 ∧ ¬ fs[ri1[inodekey(key0.ino)]].directory ∧ # fs[ri1[key0]].data = VFS_PAGE_SIZE))

Rule argument

Additional information

Used simplifier rules: 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?)));%at-diff-ri: ⊦ (ri \ ks)[key] = (key ∈ ks ⊃ (∅)[key];ri[key]);%at-del-ri: ⊦ (ri -- key0)[key1] = (key0 = key1 ⊃ (∅)[key0];ri[key1]);% ⊦ ¬ inodekey(m).data?; (s)% ⊦ key.dentry? → ¬ key.data?; (s)% ⊦ key.inode? → ¬ key.data?; (s)% ⊦ key ≠ key0 → (ri -- key0)[key] = ri[key]; (s)% ⊦ ubifs-cons(fs, ri, ro, fi, fo, log) → ¬ dups(log); (s)% ⊦ ubifs-cons(fs, ri, ro, fi, fo, log) ∧ key ∈ fo → key ∈ fi; (ss)% ⊦ inodekey(m).ino = m; (s)% ⊦ inodekey(m).inode?; (s)%⊦ key ∈ datakeys(key0, ri) ↔ key ∈ ri ∧ key.data? ∧ key0.inode? ∧ key.ino = key0.ino; (s)% ⊦ ubifs-cons(fs, ri, ro, fi, fo, log) ∧ key ∈ ro → key ∈ ri; (ss)% ⊦ key ∈ ks -- key0 ↔ key ≠ key0 ∧ key ∈ ks; (s)% ⊦ ks.inodes? → (ks -- key).inodes?; (ss)% ⊦ ubifs-cons(fs, ri, ro, fi, fo, log) → ¬ inodekey(0) ∈ ri; (s)% ⊦ key ∈ ri \ ks ↔ key ∈ ri ∧ ¬ key ∈ ks; (ls)% ⊦ inodekey(m) = inodekey(m0) ↔ m = m0; (s)% ⊦ key ∈ ri -- key0 ↔ key ≠ key0 ∧ key ∈ ri; (s)