Proof step 25 from proof inv-rename-dir-dentry (previous step)

Heuristic conditional right split applied rule if right

And obtained the following new goals

• Proof step 26:

  dirs[m0] = mkdir(m6, md6, # links(m0, dirs), m9, entries1), dirs[m] = mkdir(m2, md4, # links(m, dirs), m5, entries), dirs[entries[str]] = mkdir(m1, md3, # links(entries[str], dirs), m3, ∅), dirs[entries1[str0]] = mkdir(m4, md5, # links(entries1[str0], dirs), m7, entries0), afs-cons(dirs, files), dcache-cons(dcache, dirs, files), icache-cons(icache, dirs, files), pcache-cons(pcache, dirs, files), pre-rename (mkinode(m0, md2, true, # links(m0, dirs), m9, m6), mkdentry(str0, entries1[str0]), mkinode(entries1[str0], md0, true, # links(entries1[str0], dirs), m7, m4), mkinode(m, md1, true, # links(m, dirs), m5, m2), mkdentry(str, entries[str]), mkinode(entries[str], md, true, # links(entries[str], dirs), m3, m1), dirs, files), synced(dirs, icache, pcache), m0 ∈ dirs, m ∈ dirs, entries1[str0] ∈ dirs, entries[str] ∈ dirs, str0 ∈ entries1, str ∈ entries, asynced → synced(files, icache, pcache), m = m0 → md1 = md2, links(m0, dirs) ≠ ∅ ∨ m0 = ROOT_INO, links(m, dirs) ≠ ∅ ∨ m = ROOT_INO ⊦ ⟪let asynced0 = true in {old_parent_inode := mkinode(m0, md2, true, # links(m0, dirs), m9, m6); old_dent := mkdentry(str0, entries1[str0]); old_child_inode := mkinode(entries1[str0], md0, true, # links(entries1[str0], dirs), m7, m4); new_parent_inode := mkinode(m, md1, true, # links(m, dirs), m5, m2); new_dent := mkdentry(str, entries[str]); new_child_inode := mkinode(entries[str], md, true, # links(entries[str], dirs), m3, m1); afs_rename#(; old_parent_inode, new_parent_inode, old_child_inode, new_child_inode, old_dent, new_dent, err, dirs, files; asynced1); if err = ESUCCESS then let asynced = false in {icache_set#(old_parent_inode, asynced; err, icache); icache_set#(new_parent_inode, asynced; err, icache); if asynced0 then icache_set#(new_child_inode, asynced; err, icache); dcache_delete#(old_parent_inode.ino, old_dent.name; err, dcache); dcache_set#(new_parent_inode.ino, new_dent.name, new_dent; err, dcache)}}⟫ ( icache-cons(icache, dirs, files) ∧ dcache-cons(dcache, dirs, files) ∧ pcache-cons(pcache, dirs, files) ∧ afs-cons(dirs, files) ∧ synced(dirs, icache, pcache) ∧ (asynced → synced(files, icache, pcache))), entries[str] = ROOT_INO

• Proof step 604:

  dirs[m0] = mkdir(m6, md6, # links(m0, dirs), m9, entries1), dirs[m] = mkdir(m2, md4, # links(m, dirs), m5, entries), dirs[entries[str]] = mkdir(m1, md3, # links(entries[str], dirs), m3, ∅), dirs[entries1[str0]] = mkdir(m4, md5, # links(entries1[str0], dirs), m7, entries0), afs-cons(dirs, files), dcache-cons(dcache, dirs, files), icache-cons(icache, dirs, files), pcache-cons(pcache, dirs, files), synced(dirs, icache, pcache), m0 ∈ dirs, m ∈ dirs, entries1[str0] ∈ dirs, entries[str] ∈ dirs, str0 ∈ entries1, str ∈ entries, asynced → synced(files, icache, pcache), m = m0 → md1 = md2, links(m0, dirs) ≠ ∅ ∨ m0 = ROOT_INO, links(m, dirs) ≠ ∅ ∨ m = ROOT_INO ⊦ ⟪abort⟫ ( icache-cons(icache, dirs, files) ∧ dcache-cons(dcache, dirs, files) ∧ pcache-cons(pcache, dirs, files) ∧ afs-cons(dirs, files) ∧ synced(dirs, icache, pcache) ∧ (asynced → synced(files, icache, pcache))), entries[str] = ROOT_INO, pre-rename (mkinode(m0, md2, true, # links(m0, dirs), m9, m6), mkdentry(str0, entries1[str0]), mkinode(entries1[str0], md0, true, # links(entries1[str0], dirs), m7, m4), mkinode(m, md1, true, # links(m, dirs), m5, m2), mkdentry(str, entries[str]), mkinode(entries[str], md, true, # links(entries[str], dirs), m3, m1), dirs, files)

• Proof step 606:

  dirs[m0] = mkdir(m6, md6, # links(m0, dirs), m9, entries1), dirs[m] = mkdir(m2, md4, # links(m, dirs), m5, entries), dirs[entries[str]] = mkdir(m1, md3, # links(entries[str], dirs), m3, ∅), dirs[entries1[str0]] = mkdir(m4, md5, # links(entries1[str0], dirs), m7, entries0), afs-cons(dirs, files), dcache-cons(dcache, dirs, files), icache-cons(icache, dirs, files), pcache-cons(pcache, dirs, files), synced(dirs, icache, pcache), m0 ∈ dirs, m ∈ dirs, entries1[str0] ∈ dirs, entries[str] ∈ dirs, str0 ∈ entries1, str ∈ entries, asynced → synced(files, icache, pcache), m = m0 → md1 = md2, links(m0, dirs) ≠ ∅ ∨ m0 = ROOT_INO, links(m, dirs) ≠ ∅ ∨ m = ROOT_INO ⊦ entries[str] = ROOT_INO, str0 ∈ entries1 ∧ (str0 ∈ entries1 ∧ str0 ∈ entries1) ∧ str ∈ entries ∧ str ∈ entries ∧ str ∈ entries

Rule argument

Additional information