Proof step 252 from proof inv-truncate-buff-some (previous step)

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 253:

  # buf-opt.buf = VFS_PAGE_SIZE, files0[m0] = mkfile(m1, md1, # links(m0, dirs), content0), err = ESUCCESS, ino = m0, n = m5, size = m2, buf-opt.some?, afs-cons(dirs, files0[m0, mkfile(m5, md0, # links(m0, dirs), content0 upto min(m5, m2))]), afs-cons(dirs, files0), dcache-cons(dcache, dirs, files0), icache-cons(icache, dirs, files0), pcache-cons(pcache, dirs, files0), synced(dirs, icache, pcache), m0 ∈ files0, asynced1 → synced(files0, icache, pcache), ∀ key. key ∈ pcache → key.data? ⊦ ⟪inode0 := mkinode(m0, md0, false, # links(m0, dirs), 0, m5); ino0 := m0; files := files0[m0, mkfile(m1, md1, # links(m0, dirs), content0 upto min(m5, m2))]; skip; skip⟫ ( icache-cons (icache[m0, mkientry(false, mkinode(m0, md0, false, # links(m0, dirs), 0, m5))], dirs, files[ino0, (ino0 ∈ files ⊃ files[ino0].size:= inode0.size;files[ino0]).meta:= inode0.meta]) ∧ dcache-cons(dcache, dirs, files[ino0, (ino0 ∈ files ⊃ files[ino0].size:= inode0.size;files[ino0]).meta:= inode0.meta]) ∧ pcache-cons (truncate(ino, min(n, size), pcache), dirs, files[ino0, (ino0 ∈ files ⊃ files[ino0].size:= inode0.size;files[ino0]).meta:= inode0.meta]) ∧ synced(dirs, icache[m0, mkientry(false, mkinode(m0, md0, false, # links(m0, dirs), 0, m5))], truncate(ino, min(n, size), pcache)) ∧ ( asynced1 → synced (files[ino0, (ino0 ∈ files ⊃ files[ino0].size:= inode0.size;files[ino0]).meta:= inode0.meta], icache[m0, mkientry(false, mkinode(m0, md0, false, # links(m0, dirs), 0, m5))], truncate(ino, min(n, size), pcache)))), m2 ≤ m5 ∧ m2 % VFS_PAGE_SIZE ≠ 0

Rule argument

Additional information