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

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

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 1480:
# links(entries[str], dirs) = files[entries[str]].nlink, # links(ino, dirs) = dirs[ino].nlink, # links(ino1, dirs) = dirs[ino1].nlink, entries[str] = dirs[ino1].entries[str], dirs[ino] = mkdir(dirs[ino].size, md1, dirs[ino].nlink, dirs[ino].nsubdirs, entries1), dirs[ino1] = mkdir(dirs[ino1].size, md, dirs[ino1].nlink, dirs[ino1].nsubdirs, entries), files[entries[str]] = mkfile(m, md2, files[entries[str]].nlink, content0), dom of < ino2, afs-cons(dirs, files), ispath(q0, ROOT_INO, ino, dirs, files), ispath(q, ROOT_INO, ino1, dirs, files), of-cons(of, dirs, files), pw(user, md1), pw(user, md), px(user, md1), px(user, md), px-parent(user, q0, ROOT_INO, dirs, files), px-parent(user, q, ROOT_INO, dirs, files), str ∈ dirs[ino1].entries, str ∈ entries, ino1 ∈ dirs, entries[str] ∈ files, ino ∈ dirs, ¬ str0 ∈ dirs[ino].entries, ¬ entries[str] ∈ dirs, ¬ str0 ∈ entries1, ¬ q + str ' ⊑ q0 + str0 ', ino = ino1 → md1 = md, links(ino, dirs) ≠ ∅ ∨ ino = ROOT_INO, links(ino1, dirs) ≠ ∅ ∨ ino1 = ROOT_INO ⊦ [fail#(; ; err); asynced := ?] ⟪skip⟫ true

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% ⊦ 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)