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

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 29:

  adr4 = adr5, err = ESUCCESS, fs = fs1[adr1, nd1][adr2, nd0][adr3, nd], fs0 = fs1, log = ((log0 + adr1) + adr2) + adr3, nd = inodenode(inodekey(n), md, false, 1, 0, 0), nd0 = dentrynode(dentrykey(m, str), n), nd1 = inodenode(inodekey(m), md0, true, fs1[ri[inodekey(m)]].nlink, fs1[ri[inodekey(m)]].nsubdirs, fs1[ri[inodekey(m)]].size + 1), fs1[ri[inodekey(m)]].directory, fs1[ri[inodekey(m)]].inode?, fo.inodes?, ro.inodes?, file-node-cons(fs1, ri), log-cons(log0, fs1), new(adr1 ' + (adr2 ' + adr3), fs1), orphans-cons(fs1, ri, ro), replay-cons-strong(fs1, ri, ro, fi, fo, log0), ri-inj(fi), ri-inj(ri), ubifs-cons(fs1, ri, ro, fi, fo, log0), ri[inodekey(m)] ∈ fs1, inodekey(m) ∈ ri, fs1[ri[inodekey(m)]].nlink ≠ 0 ∨ m = ROOT_INO ⊦ ⟪boolvar := ?; if err = ESUCCESS then {ri0 := ri; ri1 := ri; ri2 := ri; aubifs_core_index_store#(inodekey(m), adr1, fi, ro, fo, fs, log, boolvar; ri); aubifs_core_index_store#(dentrykey(m, str), adr2, fi, ro, fo, fs, log, boolvar; ri); aubifs_core_index_store#(inodekey(n), adr3, fi, ro, fo, fs, log, boolvar; ri); dent := mkdentry(str, n); p_inode := mkinode (mkinode(m, md0, true, fs0[ri2[inodekey(m)]].nlink, fs0[ri1[inodekey(m)]].nsubdirs, fs0[ri0[inodekey(m)]].size).ino, nd1.meta, nd1.directory, nd1.nlink, nd1.nsubdirs, nd1.size); c_inode := mkinode (n, inodenode(inodekey(n), md, false, 1, 0, 0).meta, inodenode(inodekey(n), md, false, 1, 0, 0).directory, inodenode(inodekey(n), md, false, 1, 0, 0).nlink, inodenode(inodekey(n), md, false, 1, 0, 0).nsubdirs, inodenode(inodekey(n), md, false, 1, 0, 0).size)}⟫ (ubifs-cons(fs, ri, ro, fi, fo, log) ∧ replay-cons-strong(fs, ri, ro, fi, fo, log) ∧ file-node-cons(fs, ri) ∧ orphans-cons(fs, ri, ro)), n = 0, dups(adr1 ' + adr2 ' + adr3 '), inodekey(n) ∈ ri, inodekey(n) ∈ fo, dentrykey(m, str) ∈ ri, inodekey(m) ∈ ro

Rule argument

Additional information