Proof step 1132 from proof refine-truncate (previous step)

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 1133:

  boolvar1 ↔ boolvar2, fs[ri[inodekey(m)]] = inodenode(key, md0, false, m1, 0, m4), buf-opt = buf-opt0, err = err0, 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, orphans(fs, ri)), replay-cons-strong(fs, ri, orphans(fs, ri), fi, fo, log), ri-inj(ri), ri-inj(fi), ubifs-cons(fs, ri, orphans(fs, ri), fi, fo, log), inodekey(m) ∈ ri, ri[inodekey(m)] ∈ fs, m2 ≤ n, ⌊err0⌋ , asynced → boolvar4 ⊦ [inode := mkinode(m, md, false, m1, 0, m2); boolvar4 := boolvar, adr2 := adr; ro0 := orphans(fs, ri); files := abs-files(fs, ri); dirs := abs-dirs(fs, ri); if err = ESUCCESS then {aubifs_core_index_store#(inodekey(m), adr2, fi, ro0, fo, fs, log, boolvar4; ri); aubifs_core_index_truncate#(inodekey(m), min(n, m2), fi, ro0, fo, fs, log, boolvar4; ri); boolvar1 := false; inode := mkinode (inode.ino, inodenode(inodekey(m), md, false, m1, 0, n).meta, inodenode(inodekey(m), md, false, m1, 0, n).directory, inodenode(inodekey(m), md, false, m1, 0, n).nlink, inodenode(inodekey(m), md, false, m1, 0, n).nsubdirs, inodenode(inodekey(m), md, false, m1, 0, n).size); if boolvar1 then buf-opt := some(inodenode(inodekey(m), md, false, m1, 0, n).data)}] ( ubifs-cons(fs, ri, ro0, fi, fo, log) ∧ replay-cons-strong(fs, ri, ro0, fi, fo, log) ∧ file-node-cons(fs, ri) ∧ orphans-cons(fs, ri, ro0) ∧ ri-inj(ri) → ⟨p_inode := mkinode(m, md, false, m1, 0, m2); afs_truncate#(n, m2 / VFS_PAGE_SIZE; buf-opt0, p_inode, boolvar2, err1, 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 → boolvar4) ∧ buf-opt = buf-opt0 ∧ inode = p_inode ∧ (boolvar1 ↔ boolvar2) ∧ err = err1)), m2 % VFS_PAGE_SIZE = 0, buf-opt0.some?, datakey(m, m2 / VFS_PAGE_SIZE) ∈ ri

Rule argument

Additional information