Proof step 33 from proof inv-unlink (previous step)

Heuristic symbolic execution applied rule let right

And obtained the following new goals

• Proof step 34:

  files[entries[str]] = mkfile(m0, md2, # links(entries[str], dirs), content), dirs[m] = mkdir(m1, md3, # links(m, dirs), m4, entries), c_inode = mkinode(entries[str], md0, false, # links(entries[str], dirs), 0, m3), dent = mkdentry(str, entries[str]), ino = dent.ino, p_ino = p_inode.ino, p_inode = mkinode(m, md, true, # links(m, dirs), m4, m1), dent.dentry?, afs-cons(dirs, files), dcache-cons(dcache, dirs, files), icache-cons(icache, dirs, files), pcache-cons(pcache, dirs, files), pre-unlink(p_inode, c_inode, dent, dirs, files), synced(dirs, icache, pcache), entries[str] ∈ files, str ∈ entries, m ∈ dirs, dirs[p_ino, dirs[p_ino].entries:= (dirs[p_ino].entries -- dent.name)][p_ino].size ≥ 1, asynced1 → synced(files, icache, pcache), links(m, dirs) ≠ ∅ ∨ m = ROOT_INO ⊦ [dirs := dirs[p_ino, dirs[p_ino].entries:= (dirs[p_ino].entries -- dent.name)] [p_ino, dirs[p_ino, dirs[p_ino].entries:= (dirs[p_ino].entries -- dent.name)][p_ino] .size:= (dirs[p_ino, dirs[p_ino].entries:= (dirs[p_ino].entries -- dent.name)][p_ino].size - 1) ]; afs_drop_nlink#(ino; dirs, files); dent := negdentry(dent.name); afs_inode_sync#(p_inode; dirs, files); afs_inode_sync#(c_inode; dirs, files); p_inode := getinode(p_inode.ino, dirs, files); c_inode := getinode(c_inode.ino, dirs, files); err := ESUCCESS; asynced := ?] ( afs-cons(dirs, files) → ⟪if err = ESUCCESS then let asynced = false in {icache_set#(c_inode, asynced; err, icache); icache_set#(p_inode, asynced; err, icache); dcache_delete#(p_inode.ino, dent.name; err, dcache)}⟫ ( icache-cons(icache, dirs, files) ∧ dcache-cons(dcache, dirs, files) ∧ pcache-cons(pcache, dirs, files) ∧ synced(dirs, icache, pcache) ∧ (asynced1 → synced(files, icache, pcache))))

Rule argument

Additional information