Proof step 226 from proof refine-create (previous step)

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 227:

  fs[ri[inodekey(m3)]] = inodenode(key, md1, true, m, m4, m5), adr4 = adr1, c_inode = p_inode1, dent = negdentry(str), dirs = abs-dirs(fs0, ri), err = ENOSPC, files = abs-files(fs0, ri), fs0 = fs, m0 = fs0[ri[inodekey(m3)]].nlink, m1 = fs0[ri[inodekey(m3)]].nsubdirs, m2 = fs0[ri[inodekey(m3)]].size, nd = inodenode(inodekey(n), md, false, 1, 0, 0), nd0 = dentrynode(dentrykey(m3, str), n), nd1 = inodenode(inodekey(m3), md0, true, m, m4, m5 + 1), old_dent = negdentry(str), p_inode = mkinode(m3, md0, true, fs0[ri[inodekey(m3)]].nlink, fs0[ri[inodekey(m3)]].nsubdirs, fs0[ri[inodekey(m3)]].size), p_inode0 = mkinode(m3, md0, true, m0, m1, m2), ro = orphans(fs, ri), ro0 = orphans(fs0, ri), fs0[ri[inodekey(m3)]].inode?, orphans(fs, ri).inodes?, fo.inodes?, afs-cons(abs-dirs(fs, ri), abs-files(fs, ri)), file-node-cons(fs, ri), log-cons(log, fs), orphans-cons(fs, ri, ro0), orphans-cons(fs, ri, orphans(fs, ri)), replay-cons-strong(fs, ri, ro0, fi, fo, log), replay-cons-strong(fs, ri, orphans(fs, ri), fi, fo, log), ri-inj(ri), ri-inj(fi), ubifs-cons(fs, ri, ro0, fi, fo, log), ubifs-cons(fs, ri, orphans(fs, ri), fi, fo, log), ri[inodekey(m3)] ∈ fs, ri[inodekey(m3)] ∈ fs0, inodekey(m3) ∈ ri, asynced → boolvar0, ∀ adr1, adr2, adr3. ¬(new(adr1 ' + (adr2 ' + adr3), fs) ∧ ¬ dups(adr1 ' + adr2 ' + adr3 ')), links(m3, abs-dirs(fs, ri)) ≠ ∅ ∨ m3 = ROOT_INO, m ≠ 0 ∨ m3 = ROOT_INO, fs0[ri[inodekey(m3)]].trunc? ∨ fs0[ri[inodekey(m3)]].inode? ⊦ ⟨afs_create#(md; p_inode0, p_inode1, old_dent, err0, dirs, files; asynced)⟩ ( dirs = abs-dirs(fs, ri) ∧ files = abs-files(fs, ri) ∧ orphans(abs-dirs(fs, ri), abs-files(fs, ri)) = abs-keys(ro0) ∧ (asynced → boolvar) ∧ p_inode = p_inode0 ∧ c_inode = p_inode1 ∧ dent = old_dent ∧ err = err0), n = 0, inodekey(n) ∈ ri, inodekey(n) ∈ fo, dentrykey(m3, str) ∈ ri, m = 0 ∧ m3 ≠ ROOT_INO

Rule argument

Additional information