[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 566 from proof refine-rmdir (previous step)

dirs[entries[str]] = mkdir(0, md0, # links(entries[str], dirs), m2, ∅), dirs[ino1] = mkdir(# entries, md, # links(ino1, dirs), m1, entries), root[q + str '] = dnode(md1, ∅), c_inode = p_inode0, dent = mkdentry(str, entries[str]), err = ESUCCESS, fs = abs-files(files), inode = mkinode(ino1, md, true, # links(ino1, dirs), m1, # entries), p_inode = inode, p_inode0 = mkinode(entries[str], md0, true, # links(entries[str], dirs), m2, 0), root.dir?, root[q].dir?, dom of < ino0, abs(root, ROOT_INO)(dirs), afs-cons(dirs, files), fids-cons(root, abs-files(files), abs-of(of)), ispath(q, ROOT_INO, ino1, dirs, files), of-cons(of, dirs, files), pre-rmdir(p_inode, c_inode, dent, dirs, files), pw(user, md), px(user, md), px-parent(user, q, ROOT_INO, dirs, files), str ∈ entries, ino1 ∈ dirs, entries[str] ∈ dirs, psynced → asynced0, links(ino1, dirs) ≠ ∅ ∨ ino1 = ROOT_INO ⊦ [fail#(; ; err); asynced := ?; vfs_put_inode#(c_inode, of, asynced; err, dirs, files)] ( of-cons(of, dirs, files) ∧ afs-cons(dirs, files) → ⟨posix_rmdir#(q + str ', user, fs, abs-of(of); err1, root; psynced)⟩ (fs = abs-files(files) ∧ abs(root, ROOT_INO)(dirs) ∧ (psynced → asynced) ∧ err = err1))

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 567:
⊦ abs(tree, ROOT_INO)(dirs) ∧ fids-cons(tree, abs-files(files), ofh) ∧ afs-cons(dirs, files) ∧ ino ∈ dirs ∧ dirs[ino] = mkdir(n, md, m, m0, entries) ∧ str ∈ entries ∧ ispath(p, ROOT_INO, ino, dirs, files) → entries[str] ≠ ROOT_INO
Proof step 568:
# links(entries[str], dirs) = dirs[entries[str]].nlink, # entries = dirs[ino1].size, # links(ino1, dirs) = dirs[ino1].nlink, dirs[entries[str]].entries = ∅, 0 = dirs[entries[str]].size, entries[str] = dirs[ino1].entries[str], dirs[entries[str]] = mkdir(0, md0, dirs[entries[str]].nlink, dirs[entries[str]].nsubdirs, ∅), dirs[ino1] = mkdir(# entries, md, dirs[ino1].nlink, dirs[ino1].nsubdirs, entries), root[q + str '] = dnode(md1, ∅), root.dir?, root[q].dir?, dom of < ino0, abs(root, ROOT_INO)(dirs), afs-cons(dirs, files), fids-cons(root, abs-files(files), abs-of(of)), ispath(q, ROOT_INO, ino1, dirs, files), of-cons(of, dirs, files), pw(user, md), px(user, md), px-parent(user, q, ROOT_INO, dirs, files), str ∈ dirs[ino1].entries, str ∈ entries, ino1 ∈ dirs, entries[str] ∈ dirs, psynced → asynced0, links(ino1, dirs) ≠ ∅ ∨ ino1 = ROOT_INO ⊦ [fail#(; ; err); asynced := ?; files0 := files; vfs_put_inode#(mkinode(entries[str], md0, true, dirs[entries[str]].nlink, dirs[entries[str]].nsubdirs, 0), of, asynced; err, dirs, files)] ( of-cons(of, dirs, files) ∧ afs-cons(dirs, files) → ⟨posix_rmdir#(q + str ', user, abs-files(files0), abs-of(of); err1, root; psynced)⟩ (abs-files(files0) = abs-files(files) ∧ abs(root, ROOT_INO)(dirs) ∧ (psynced → asynced) ∧ err = err1))

Rule argument

Additional information

Used simplifier rules: abs-acyclic: ⊦ abs(tree, ROOT_INO)(dirs) ∧ fids-cons(tree, abs-files(files), ofh) ∧ afs-cons(dirs, files) ∧ ino ∈ dirs ∧ dirs[ino] = mkdir(n, md, m, m0, entries) ∧ str ∈ entries ∧ ispath(p, ROOT_INO, ino, dirs, files) → entries[str] ≠ ROOT_INO;%afs-cons-dir-nlink: ⊦ afs-cons(dirs, files) ∧ ino ∈ dirs ∧ dirs[ino] = mkdir(n0, md, n, n1, entries) → # links(ino, dirs) = n; (forward) from specification afs-base% ⊦ mkinode(m, md, boolvar, m0, m1, m2).directory ↔ boolvar; (s)% ⊦ mkinode(m, md, boolvar, m0, m1, m2).nsubdirs = m1; (s)% ⊦ mkinode(m, md, boolvar, m0, m1, m2).size = m2; (s)% ⊦ mkinode(m, md, boolvar, m0, m1, m2).nlink = m0; (s)% ⊦ valid-dir-ino(ino, dirs, files) ↔ ino ∈ dirs; (s)%⊦ valid-dir-inode(inode, dirs, files) ↔ valid-dir-ino(inode.ino, dirs, files) ∧ inode.nlink = dirs[inode.ino].nlink ∧ inode.size = dirs[inode.ino].size ∧ inode.nsubdirs = dirs[inode.ino].nsubdirs ∧ inode.directory; (s)% ⊦ dir-empty(ino, dirs, files) ↔ dirs[ino].entries = ∅; (s)% ⊦ mkdentry(str, m).dentry?; (s)% ⊦ mkdentry(str, m).name = str; (s)% ⊦ valid-ino(ino, dirs, files) ↔ ino ∈ dirs ∨ ino ∈ files; (s)%⊦ valid-parent-ino(ino, dirs, files) ↔ ino ∈ dirs ∧ (links(ino, dirs) ≠ ∅ ∨ ino = ROOT_INO); (s)%⊦ valid-dentry(ino, dent, dirs, files) ↔ valid-parent-ino(ino, dirs, files) ∧ valid-ino(dent.ino, dirs, files) ∧ dent.name ∈ dirs[ino].entries ∧ dent.ino = dirs[ino].entries[dent.name] ∧ dent.dentry?; (s)% ⊦ mkinode(m, md, boolvar, m0, m1, m2).ino = m; (s)% ⊦ mkdentry(str, m).ino = m; (s)%⊦ pre-rmdir(p_inode, c_inode, dent, dirs, files) ↔ dent.ino ≠ ROOT_INO ∧ valid-dentry(p_inode.ino, dent, dirs, files) ∧ dir-empty(dent.ino, dirs, files) ∧ valid-dir-inode(p_inode, dirs, files) ∧ valid-dir-inode(c_inode, dirs, files) ∧ c_inode.ino = dent.ino; (s)