Proof step 12 from proof inv-create (previous step)

Heuristic symbolic execution applied rule choose right

And obtained the following new goals

• Proof step 13:

  # links(m, dirs) = dirs[m].nlink, dirs[m] = mkdir(dirs[m].size, md1, dirs[m].nlink, dirs[m].nsubdirs, entries), dent = negdentry(str), p_inode = mkinode(m, md0, true, dirs[m].nlink, dirs[m].nsubdirs, dirs[m].size), afs-cons(dirs, files), m ∈ dirs, links(m, dirs) ≠ ∅ ∨ m = ROOT_INO ⊦ ⟪afs_create_ino#(p_inode.ino, md, ino; dent, err, dirs, files); afs_inode_sync#(p_inode; dirs, files); p_inode := getinode(p_inode.ino, dirs, files); c_inode := getinode(dent.ino, dirs, files); asynced := ?⟫ afs-cons(dirs, files), ino = 0, str ∈ entries, str ∈ dirs[m].entries, ino ∈ files, ino ∈ dirs

• Proof step 64:

  # links(m, dirs) = dirs[m].nlink, dirs[m] = mkdir(dirs[m].size, md1, dirs[m].nlink, dirs[m].nsubdirs, entries), dent = negdentry(str), p_inode = mkinode(m, md0, true, dirs[m].nlink, dirs[m].nsubdirs, dirs[m].size), afs-cons(dirs, files), m ∈ dirs, links(m, dirs) ≠ ∅ ∨ m = ROOT_INO ⊦ str ∈ entries, str ∈ dirs[m].entries, ∃ ino. ¬ ino ∈ dirs ∧ ¬ ino ∈ files ∧ ino ≠ 0

Rule argument

Additional information