Proof step 1395 from proof inv-renam (previous step)

Heuristic conditional right split applied rule or split right

And obtained the following new goals

• Proof step 1396:

  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 ⊦ [let old_ino = old_parent_inode.ino, new_ino = new_parent_inode.ino, isdir0 = new_dent.dentry? in let isdir = old_ino = new_ino ∧ new_dent = old_dent in {dirs[old_ino].entries := dirs[old_ino].entries -- old_dent.name; if ¬ isdir then {dirs[old_ino].size := dirs[old_ino].size - 1; if old_dent.ino ∈ dirs then dirs[old_ino].nsubdirs := dirs[old_ino].nsubdirs - 1}; dirs[new_ino].entries[new_dent.name] := old_dent.ino; if isdir0 ∧ ¬ isdir then let ino = new_dent.ino in afs_drop_nlink#(ino; dirs, files); if ¬ isdir0 then {dirs[new_ino].size := dirs[new_ino].size + 1; if old_dent.ino ∈ dirs then dirs[new_ino].nsubdirs := dirs[new_ino].nsubdirs + 1}; new_dent := mkdentry(new_dent.name, old_dent.ino); old_dent := negdentry(old_dent.name); afs_inode_sync#(old_parent_inode; dirs, files); afs_inode_sync#(new_parent_inode; dirs, files); if isdir0 then {afs_inode_sync#(new_child_inode; dirs, files); new_child_inode := getinode(new_child_inode.ino, dirs, files)}; old_parent_inode := getinode(old_parent_inode.ino, dirs, files); new_parent_inode := getinode(new_parent_inode.ino, dirs, files); err := ESUCCESS}; asynced := ?] (afs-cons(dirs, files) → ⟪skip⟫ of-cons(of, dirs, files)), entries[str] ∈ dirs, str0 ∈ entries1, q + str ' ⊑ q0 + str0 '

• Proof step 1479:

  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 '

Rule argument

Additional information