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

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 1119:

  boolvar ↔ m2 ≤ n ∧ pageno0 ≠ 0 ∧ (m2 / VFS_PAGE_SIZE ∈ content ∨ buf-opt0.some?), abs-files(fs, ri)[m] = mkfile(m0, md1, m3, content0), fs[ri[inodekey(m)]] = inodenode(key, md0, false, m1, 0, m4), content = content0, ino = m, pageno = min(n, m2), pageno0 = m2 % VFS_PAGE_SIZE, 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(m)] ∈ fs, inodekey(m) ∈ ri, m2 ≤ n, asynced → boolvar0, m2 ≤ n → pageno0 ≠ 0 → VFS_PAGE_SIZE ≠ 0, ∀ adr, adr0. adr ∈ fs ∨ adr0 ∈ fs ∨ adr = adr0 ⊦ ⟨files := abs-files(fs, ri); buf-opt := buf-opt0; if boolvar then {pageno1 := m2 / VFS_PAGE_SIZE; if buf-opt.some? then buf := buf-opt.buf else buf := files[ino].content[pageno1]; buf := fill(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, m1, 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, m1, 0, m2) = inode ∧ (boolvar2 ↔ boolvar) ∧ ENOSPC = err), ⟨err := ENOSPC; asynced := ?⟩ ((asynced → boolvar4) ∧ ENOSPC = err), m2 % VFS_PAGE_SIZE = 0, VFS_PAGE_SIZE = 0, buf-opt0.some?, datakey(m, m2 / VFS_PAGE_SIZE) ∈ ri

Rule argument

Additional information