Proof step 168 from proof eq-io-truncate (previous step)

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 169:

  boolvar ↔ m2 ≤ n0 ∧ pageno0 ≠ 0 ∧ (m2 / VFS_PAGE_SIZE ∈ content0 ∨ buf-opt.some?), VFS_PAGE_SIZE = n1 + m2 % VFS_PAGE_SIZE, files2[m] = mkfile(m3, md1, m4, content), ¬ boolvar, content0 = content, dirs0 = dirs1, ino = m, new_inode = mkinode(m, md, false, m4, 0, m2), pageno = min(n0, m2), pageno0 = m2 % VFS_PAGE_SIZE, m2 / VFS_PAGE_SIZE ∈ content, m ∈ files2, m2 ≤ n0, VFS_PAGE_SIZE ≤ # content[m2 / VFS_PAGE_SIZE], m2 ≤ n0 → pageno0 ≠ 0 → VFS_PAGE_SIZE ≠ 0 ⊦ ⟨files := files2[ino, files2[ino].content:= (content0 upto pageno)]; afs_inode_sync#(new_inode.size:= n0; dirs1, files); inode := (m ∈ dirs1 ⊃ mkinode(m, dirs1[m].meta, true, dirs1[m].nlink, dirs1[m].nsubdirs, dirs1[m].size) ;mkinode(m, files[m].meta, false, files[m].nlink, 0, files[m].size) ); err := ESUCCESS; asynced := ?⟩ ( buf-opt = some(fill(content[m2 / VFS_PAGE_SIZE], zero, m2 % VFS_PAGE_SIZE, n1)) ∧ inode = (m ∈ dirs0 ⊃ mkinode(m, dirs0[m].meta, true, dirs0[m].nlink, dirs0[m].nsubdirs, dirs0[m].size);mkinode(m, md, false, m4, 0, n0)) ∧ boolvar ∧ err = ESUCCESS ∧ dirs1 = dirs0 ∧ files = files2[m, mkfile(n0, md, m4, content[m2 / VFS_PAGE_SIZE, fill(content[m2 / VFS_PAGE_SIZE], zero, m2 % VFS_PAGE_SIZE, n1)] upto m2)]), ⟨fail#(; ; err); asynced := ?⟩ ( buf-opt = some(fill(content[m2 / VFS_PAGE_SIZE], zero, m2 % VFS_PAGE_SIZE, n1)) ∧ mkinode(m, md, false, m4, 0, m2) = mkinode(m, dirs1[m].meta, true, dirs1[m].nlink, dirs1[m].nsubdirs, dirs1[m].size) ∧ boolvar0 ∧ err = ESUCCESS ∧ files2 = files2[m, mkfile(n0, md, m4, content[m2 / VFS_PAGE_SIZE, fill(content[m2 / VFS_PAGE_SIZE], zero, m2 % VFS_PAGE_SIZE, n1)] upto m2)]), m2 % VFS_PAGE_SIZE = 0, VFS_PAGE_SIZE = 0, buf-opt.some?

Rule argument

Additional information