[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 1386 from proof inv-renam (previous step)

files[entries0[str]] = mkfile(m1, md1, # links(entries0[str], dirs), content), dirs[ino1] = mkdir(m0, md0, # links(ino1, dirs), m3, entries0), dirs[ino] = mkdir(m, md, # links(ino, dirs), m2, entries), err = ESUCCESS, new_dent = negdentry(str0), new_dent_inode = mkinode(entries0[str], md1, false, # links(entries0[str], dirs), 0, m1), new_inode = mkinode(ino, md, true, # links(ino, dirs), m2, m), old_dent = mkdentry(str, entries0[str]), old_dent_inode = mkinode(entries0[str], md1, false, # links(entries0[str], dirs), 0, m1), old_inode = mkinode(ino1, md0, true, # links(ino1, dirs), m3, m0), dom of < ino2, afs-cons(dirs, files), ispath(q, ROOT_INO, ino1, dirs, files), ispath(q0, ROOT_INO, ino, dirs, files), of-cons(of, dirs, files), pre-rename(old_inode, old_dent, old_dent_inode, new_inode, new_dent, new_dent_inode, dirs, files), pw(user, md0), pw(user, md), px(user, md0), px(user, md), px-parent(user, q, ROOT_INO, dirs, files), px-parent(user, q0, ROOT_INO, dirs, files), ino ∈ dirs, entries0[str] ∈ files, ino1 ∈ dirs, str ∈ entries0, links(ino1, dirs) ≠ ∅ ∨ ino1 = ROOT_INO, links(ino, dirs) ≠ ∅ ∨ ino = ROOT_INO ⊦ [afs_rename#(; old_inode, new_inode, old_dent_inode, new_dent_inode, old_dent, new_dent, err, dirs, files; asynced)] (afs-cons(dirs, files) → ⟪skip⟫ (of-cons(of, dirs, files) ∧ afs-cons(dirs, files))), str0 ∈ entries, entries0[str] ∈ dirs, q + str ' ⊑ q0 + str0 '

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 1387:
# links(entries0[str], dirs) = files[entries0[str]].nlink, # links(ino, dirs) = dirs[ino].nlink, # links(ino1, dirs) = dirs[ino1].nlink, entries0[str] = dirs[ino1].entries[str], files[entries0[str]] = mkfile(m1, md1, files[entries0[str]].nlink, content), dirs[ino1] = mkdir(dirs[ino1].size, md0, dirs[ino1].nlink, dirs[ino1].nsubdirs, entries0), dirs[ino] = mkdir(dirs[ino].size, md, dirs[ino].nlink, dirs[ino].nsubdirs, entries), err = ESUCCESS, new_dent = negdentry(str0), new_dent_inode = mkinode(entries0[str], md1, false, files[entries0[str]].nlink, 0, m1), new_inode = mkinode(ino, md, true, dirs[ino].nlink, dirs[ino].nsubdirs, dirs[ino].size), old_dent = mkdentry(str, entries0[str]), old_dent_inode = mkinode(entries0[str], md1, false, files[entries0[str]].nlink, 0, m1), old_inode = mkinode(ino1, md0, true, dirs[ino1].nlink, dirs[ino1].nsubdirs, dirs[ino1].size), dom of < ino2, afs-cons(dirs, files), ispath(q, ROOT_INO, ino1, dirs, files), ispath(q0, ROOT_INO, ino, dirs, files), of-cons(of, dirs, files), pw(user, md0), pw(user, md), px(user, md0), px(user, md), px-parent(user, q, ROOT_INO, dirs, files), px-parent(user, q0, ROOT_INO, dirs, files), str ∈ dirs[ino1].entries, ino ∈ dirs, entries0[str] ∈ files, ino1 ∈ dirs, str ∈ entries0, ¬ str0 ∈ dirs[ino].entries, ¬ str0 ∈ entries, ¬ entries0[str] ∈ dirs, ¬ q + str ' ⊑ q0 + str0 ', ino = ino1 → md = md0, links(ino1, dirs) ≠ ∅ ∨ ino1 = ROOT_INO, links(ino, dirs) ≠ ∅ ∨ ino = ROOT_INO ⊦ [afs_rename#(; old_inode, new_inode, old_dent_inode, new_dent_inode, old_dent, new_dent, err, dirs, files; asynced)] (afs-cons(dirs, files) → ⟪skip⟫ of-cons(of, dirs, files))

Rule argument

Additional information

Used simplifier rules: afs-cons-file-nlink: ⊦ afs-cons(dirs, files) ∧ ino ∈ files ∧ files[ino] = mkfile(m, md, n, content) → # links(ino, dirs) = n; (forward) from specification afs-base%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% ⊦ valid-file-ino(ino, dirs, files) ↔ ino ∈ files; (s)%⊦ valid-file-inode(inode, dirs, files) ↔ valid-file-ino(inode.ino, dirs, files) ∧ inode.nlink = files[inode.ino].nlink ∧ inode.nsubdirs = 0 ∧ ¬ inode.directory; (s)%⊦ valid-wb-inode(inode, dirs, files) ↔ valid-dir-inode(inode, dirs, files) ∨ valid-file-inode(inode, dirs, files); (s)% ⊦ mkinode(m, md, boolvar, m0, m1, m2).meta = md; (s)% ⊦ 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)% ⊦ mkdentry(str, m).dentry?; (s)% ⊦ mkdentry(str, m).name = str; (s)% ⊦ mkdentry(str, m).ino = m; (s)% ⊦ ¬ negdentry(str).dentry?; (s)% ⊦ valid-ino(ino, dirs, files) ↔ ino ∈ dirs ∨ ino ∈ files; (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)% ⊦ negdentry(str).negdentry?; (s)% ⊦ negdentry(str).name = str; (s)%⊦ valid-parent-ino(ino, dirs, files) ↔ ino ∈ dirs ∧ (links(ino, dirs) ≠ ∅ ∨ ino = ROOT_INO); (s)%⊦ valid-negdentry(ino, dent, dirs, files) ↔ valid-parent-ino(ino, dirs, files) ∧ ¬ dent.name ∈ dirs[ino].entries ∧ dent.negdentry?; (s)% ⊦ mkinode(m, md, boolvar, m0, m1, m2).ino = m; (s)%⊦ pre-rename (old_parent_inode, old_dent, old_child_inode, new_parent_inode, new_dent, new_child_inode, dirs, files) ↔ ( valid-negdentry(new_parent_inode.ino, new_dent, dirs, files) ∨ valid-dentry(new_parent_inode.ino, new_dent, dirs, files) ∧ valid-wb-inode(new_child_inode, dirs, files) ∧ new_child_inode.ino = new_dent.ino ∧ ( valid-file-ino(new_dent.ino, dirs, files) ↔ valid-file-ino(old_dent.ino, dirs, files)) ∧ ( valid-dir-ino(new_dent.ino, dirs, files) → new_dent.ino ≠ ROOT_INO ∧ dir-empty(new_dent.ino, dirs, files))) ∧ valid-dentry(old_parent_inode.ino, old_dent, dirs, files) ∧ valid-dir-inode(old_parent_inode, dirs, files) ∧ valid-dir-inode(new_parent_inode, dirs, files) ∧ ( new_parent_inode.ino = old_parent_inode.ino → new_parent_inode.meta = old_parent_inode.meta) ∧ valid-wb-inode(old_child_inode, dirs, files) ∧ old_child_inode.ino = old_dent.ino; (s)