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

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 1528:

  boolvar ↔ m2 ≤ n ∧ pageno0 ≠ 0 ∧ (m2 / VFS_PAGE_SIZE ∈ content ∨ buf-opt0.some?), fs[ri[inodekey(m)]] = inodenode(key, md0, false, m0, 0, m3), abs-files(fs, ri)[m] = mkfile(m1, md1, m4, content0), content = content0, files = abs-files(fs, ri), ino = m, pageno = min(n, m2), pageno0 = m2 % VFS_PAGE_SIZE, 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), ri[inodekey(m)] ∈ fs, inodekey(m) ∈ ri, ⌊err1⌋ , m2 ≤ n → pageno0 ≠ 0 → VFS_PAGE_SIZE ≠ 0, asynced → boolvar0, buf-opt0.some? → # buf-opt0.buf = VFS_PAGE_SIZE ⊦ ⟨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, 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), VFS_PAGE_SIZE = 0, m2 ≤ n ∧ m2 % VFS_PAGE_SIZE ≠ 0

Rule argument

Additional information