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

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 415:

  # buf-opt0.buf = VFS_PAGE_SIZE, boolvar ↔ m2 ≤ n ∧ pageno0 ≠ 0 ∧ (m2 / VFS_PAGE_SIZE ∈ content ∨ buf-opt0.some?), VFS_PAGE_SIZE = n0 + m2 % VFS_PAGE_SIZE, abs-files(fs, ri)[m] = mkfile(m1, md1, m4, content0), fs[ri[inodekey(m)]] = inodenode(key, md0, false, m0, 0, m3), buf-opt = buf-opt0, content = content0, files = abs-files(fs, ri), ino = m, pageno = min(n, m2), pageno0 = m2 % VFS_PAGE_SIZE, pageno1 = m2 / VFS_PAGE_SIZE, orphans(fs, ri).inodes?, fo.inodes?, buf-opt.some?, buf-opt0.some?, 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), ri[inodekey(m)] ∈ fs, inodekey(m) ∈ ri, m2 ≤ n, ⌊err1⌋ , asynced → boolvar0, m2 ≤ n → pageno0 ≠ 0 → VFS_PAGE_SIZE ≠ 0 ⊦ ⟨buf := fill(buf-opt.buf, zero, pageno0, VFS_PAGE_SIZE - pageno0); content[pageno1] := buf; buf-opt := some(buf); files[ino].content := content upto pageno; let new_inode = mkinode(m, md, false, m0, 0, m2) in {new_inode.size := n; dirs := abs-dirs(fs, ri); afs_inode_sync#(new_inode; dirs, files)}; inode := (m ∈ dirs ⊃ mkinode(m, dirs[m].meta, true, dirs[m].nlink, dirs[m].nsubdirs, dirs[m].size) ;mkinode(m, files[m].meta, false, files[m].nlink, 0, files[m].size) ); err := ESUCCESS; asynced := ?⟩ ( dirs = abs-dirs(fs, ri) ∧ files = abs-files(fs, ri) ∧ (asynced → boolvar4) ∧ buf-opt0 = buf-opt ∧ mkinode(m, md, false, m0, 0, m2) = inode ∧ (boolvar2 ↔ boolvar) ∧ err1 = err), ⟨err := err1; asynced := ?⟩ ((asynced → boolvar4) ∧ err1 = err), m2 % VFS_PAGE_SIZE = 0, VFS_PAGE_SIZE = 0

Rule argument

Additional information