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

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 27:

  # links(m, dirs0) = dirs0[m].nlink, dirs0[m] = mkdir(dirs0[m].size, md1, dirs0[m].nlink, dirs0[m].nsubdirs, entries), dent = negdentry(str), dirs = dirs0[p_ino, dirs0[p_ino].entries:= dirs0[p_ino].entries[dent.name, ino]] [p_ino, dirs0[p_ino, dirs0[p_ino].entries:= dirs0[p_ino].entries[dent.name, ino]][p_ino] .size:= (dirs0[p_ino, dirs0[p_ino].entries:= dirs0[p_ino].entries[dent.name, ino]][p_ino].size + 1) ], files = (files0 ++ ino)[ino, mkfile(0, md, 1, ∅)], p_ino = m, p_inode = mkinode(m, md0, true, dirs0[m].nlink, dirs0[m].nsubdirs, dirs0[m].size), afs-cons(dirs0, files0), dcache-cons(dcache, dirs0, files0), icache-cons(icache, dirs0, files0), pcache-cons(pcache, dirs0, files0), synced(dirs0, icache, pcache), m ∈ dirs0, asynced1 → synced(files0, icache, pcache), links(m, dirs0) ≠ ∅ ∨ m = ROOT_INO ⊦ [afs_inode_sync#(p_inode; dirs, files); p_inode := (p_inode.ino ∈ dirs ⊃ mkinode(p_inode.ino, dirs[p_inode.ino].meta, true, dirs[p_inode.ino].nlink, dirs[p_inode.ino].nsubdirs, dirs[p_inode.ino].size) ;mkinode(p_inode.ino, files[p_inode.ino].meta, false, files[p_inode.ino].nlink, 0, files[p_inode.ino].size) ); c_inode := getinode(mkdentry(dent.name, ino).ino, dirs, files); asynced := ?] ( afs-cons(dirs, files) → ⟪if ESUCCESS = ESUCCESS then let asynced = false in {err := ESUCCESS; icache_set#(p_inode, asynced; err, icache); icache_set#(c_inode, asynced; err, icache); dcache_set#(p_inode.ino, mkdentry(dent.name, ino).name, mkdentry(dent.name, ino); 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)))), ino = 0, ino ∈ dirs0, ino ∈ files0, str ∈ entries, str ∈ dirs0[m].entries

Rule argument

Additional information