Proof step 275 from proof refine-mkdir (previous step)

Heuristic symbolic execution applied rule choose right

And obtained the following new goals

• Proof step 276:

  fs[ri[inodekey(m3)]] = inodenode(key, md1, true, m, m4, m5), dent = negdentry(str), dirs = abs-dirs(fs, ri), files = abs-files(fs, ri), p_inode = mkinode(m3, md0, true, m, m4, m5), fo.inodes?, orphans(fs, ri).inodes?, afs-cons(abs-dirs(fs, ri), abs-files(fs, ri)), file-node-cons(fs, ri), log-cons(log, fs), orphans-cons(fs, ri, orphans(fs, ri)), replay-cons-strong(fs, ri, orphans(fs, ri), fi, fo, log), ri-inj(fi), ri-inj(ri), ubifs-cons(fs, ri, orphans(fs, ri), fi, fo, log), ri[inodekey(m3)] ∈ fs, inodekey(m3) ∈ ri, ⌊err0⌋ , asynced → boolvar0, m ≠ 0 ∨ m3 = ROOT_INO, links(m3, abs-dirs(fs, ri)) ≠ ∅ ∨ m3 = ROOT_INO ⊦ ∃ ino. (¬ ino ∈ dirs ∧ ¬ ino ∈ files ∧ ino ≠ 0) ∧ ⟨afs_mkdir_ino#(p_inode.ino, md, ino; dent, err, dirs); 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(dent.ino, dirs, files); asynced := ?⟩ ( dirs = abs-dirs(fs, ri) ∧ files = abs-files(fs, ri) ∧ (asynced → boolvar) ∧ mkinode(m3, md0, true, fs[ri[inodekey(m3)]].nlink, fs[ri[inodekey(m3)]].nsubdirs, fs[ri[inodekey(m3)]].size) = p_inode ∧ p_inode1 = c_inode ∧ negdentry(str) = dent ∧ err0 = err), ⟨fail#(; ; err); asynced := ?⟩ ( (asynced → boolvar) ∧ mkinode(m3, md0, true, fs[ri[inodekey(m3)]].nlink, fs[ri[inodekey(m3)]].nsubdirs, fs[ri[inodekey(m3)]].size) = mkinode(m3, md0, true, m, m4, m5) ∧ err0 = err), n = 0, inodekey(n) ∈ ri, inodekey(n) ∈ fo, dentrykey(m3, str) ∈ ri, m = 0 ∧ m3 ≠ ROOT_INO

Rule argument

Additional information