Proof step 88 from proof inv-mkdir (previous step)

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 89:

  # links(ino0, dirs) = m0, dirs[ino0] = mkdir(m, md0, # links(ino0, dirs), m1, entries), dent = negdentry(str), err = ESUCCESS, p_ino = ino0, afs-cons(dirs, files), ispath(q, ROOT_INO, ino0, dirs, files), of-cons(of, dirs, files), pw(user, md0), px(user, md0), px-parent(user, q, ROOT_INO, dirs, files), ino0 ∈ dirs, links(ino0, dirs) ≠ ∅ ∨ ino0 = ROOT_INO ⊦ [dirs := ( dirs[p_ino, dirs[p_ino].entries:= dirs[p_ino].entries[dent.name, ino]] [p_ino, dirs[p_ino, dirs[p_ino].entries:= dirs[p_ino].entries[dent.name, ino]][p_ino] .size:= (dirs[p_ino, dirs[p_ino].entries:= dirs[p_ino].entries[dent.name, ino]][p_ino].size + 1) ] [p_ino, dirs[p_ino, dirs[p_ino].entries:= dirs[p_ino].entries[dent.name, ino]] [p_ino, dirs[p_ino, dirs[p_ino].entries:= dirs[p_ino].entries[dent.name, ino]][p_ino] .size:= (dirs[p_ino, dirs[p_ino].entries:= dirs[p_ino].entries[dent.name, ino]][p_ino].size + 1) ] [p_ino ] .nsubdirs:= ( dirs[p_ino, dirs[p_ino].entries:= dirs[p_ino].entries[dent.name, ino]] [p_ino, dirs[p_ino, dirs[p_ino].entries:= dirs[p_ino].entries[dent.name, ino]][p_ino] .size:= (dirs[p_ino, dirs[p_ino].entries:= dirs[p_ino].entries[dent.name, ino]][p_ino].size + 1) ] [p_ino ] .nsubdirs + 1) ] ++ ino )[ino, mkdir(0, md, 1, 0, ∅) ]; dent := mkdentry(dent.name, ino); err := ESUCCESS; afs_inode_sync#(mkinode(ino0, md0, true, m0, m1, m); dirs, files); inode := (ino0 ∈ dirs ⊃ mkinode(ino0, dirs[ino0].meta, true, dirs[ino0].nlink, dirs[ino0].nsubdirs, dirs[ino0].size) ;mkinode(ino0, files[ino0].meta, false, files[ino0].nlink, 0, files[ino0].size) ); c_inode := getinode(dent.ino, dirs, files); asynced := ?] (afs-cons(dirs, files) → of-cons(of, dirs, files)), ino = 0, ino ∈ dirs, ino ∈ files, str ∈ entries

Rule argument

Additional information