Proof step 15 from proof crash-neutral-unlink (previous step)

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 16:

  # links(m, dirs) = dirs[m].nlink, c_inode.ino = entries[str], c_inode.nlink = files[entries[str]].nlink, c_inode.nsubdirs = 0, dirs[m] = mkdir(dirs[m].size, md0, dirs[m].nlink, dirs[m].nsubdirs, entries), entries[str] = dirs[m].entries[str], p_ino = m, afs-cons(dirs, files), m ∈ dirs, str ∈ entries, entries[str] ∈ files, str ∈ dirs[m].entries, dirs[p_ino, dirs[p_ino].entries:= (dirs[p_ino].entries -- mkdentry(str, entries[str]).name)][p_ino].size ≥ 1, links(m, dirs) ≠ ∅ ∨ m = ROOT_INO ⊦ ⟨let ino = mkdentry(str, entries[str]).ino in {files1 := files; files0 := files; dirs1 := dirs[p_ino, dirs[p_ino].entries:= (dirs[p_ino].entries -- mkdentry(str, entries[str]).name)] [p_ino, dirs[p_ino, dirs[p_ino].entries:= (dirs[p_ino].entries -- mkdentry(str, entries[str]).name)][p_ino] .size:= (dirs[p_ino, dirs[p_ino].entries:= (dirs[p_ino].entries -- mkdentry(str, entries[str]).name)][p_ino].size - 1) ]; afs_drop_nlink#(ino; dirs1, files)}; dent := negdentry(mkdentry(str, entries[str]).name); afs_inode_sync#(mkinode(m, md, true, # links(m, dirs), dirs[m].nsubdirs, dirs[m].size); dirs1, files); afs_inode_sync#(c_inode; dirs1, files); p_inode := (m ∈ dirs1 ⊃ mkinode(m, dirs1[m].meta, true, dirs1[m].nlink, dirs1[m].nsubdirs, dirs1[m].size) ;mkinode(m, files[m].meta, false, files[m].nlink, 0, files[m].size) ); c_inode := (c_inode.ino ∈ dirs1 ⊃ mkinode(c_inode.ino, dirs1[c_inode.ino].meta, true, dirs1[c_inode.ino].nlink, dirs1[c_inode.ino].nsubdirs, dirs1[c_inode.ino].size) ;mkinode(c_inode.ino, files[c_inode.ino].meta, false, files[c_inode.ino].nlink, 0, files[c_inode.ino].size) ); err := ESUCCESS; asynced := ?⟩ (asynced ∧ dirs \ orphans(dirs, files0) = dirs1 \ orphans(dirs1, files) ∧ files1 \ orphans(dirs, files1) = files \ orphans(dirs1, files)), ⟨fail#(; ; err); asynced := ?⟩ asynced, c_inode.directory

• Proof step 75:

  # links(m, dirs) = dirs[m].nlink, c_inode.ino = entries[str], c_inode.nlink = files[entries[str]].nlink, c_inode.nsubdirs = 0, dirs[m] = mkdir(dirs[m].size, md0, dirs[m].nlink, dirs[m].nsubdirs, entries), entries[str] = dirs[m].entries[str], p_ino = m, afs-cons(dirs, files), m ∈ dirs, str ∈ entries, entries[str] ∈ files, str ∈ dirs[m].entries, links(m, dirs) ≠ ∅ ∨ m = ROOT_INO ⊦ ⟨fail#(; ; err); asynced := ?⟩ asynced, c_inode.directory, str ∈ entries ∧ str ∈ entries ∧ dirs[p_ino, dirs[p_ino].entries:= (dirs[p_ino].entries -- mkdentry(str, entries[str]).name)][p_ino].size ≥ 1 ∧ str ∈ entries

Rule argument

Additional information