Proof step 107 from proof write-prepost (previous step)

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 108:

  ⟨afs_truncate#(m1, m1 / VFS_PAGE_SIZE; buf-opt, inode1, isdir, err, dirs1, files1, asynced1)⟩ ( buf-opt = buf-opt0 ∧ inode1 = mkinode(m, md, false, m3, 0, m1) ∧ (isdir ↔ isdir0) ∧ err = ESUCCESS ∧ dirs1 = dirs0 ∧ files1 = files0 ∧ (asynced1 ↔ asynced0)), # links(m, dirs1) = m3, files1 -- m = files0 -- m, files[m] = mkfile(m1, md, # links(m, dirs1), content1), files1[m] = mkfile(m1, md, # links(m, dirs1), content0), of1[fd] = mkfile(m, mode, m0), files0[m] = mkfile(m1, md, # links(m, dirs1), content), buf-opt = none, err = ESUCCESS, err0 = ESUCCESS, content.stream from m1 = σ⊥, ino2 = of1[fd].pos, inode1 = mkinode(m, md, false, # links(m, dirs1), 0, m1), n = ino, content0.stream to m1 = content.stream to m1, m1 < m0 + ino, afs-cons(dirs1, files1), of-cons(of1, dirs1, files1), write-inv(m0, m0 + n1, mkinode(m, md, false, # links(m, dirs1), 0, m1), buf, 0, dirs0, files0, files0), write-inv(m0, m0 + n1, mkinode(m, md, false, # links(m, dirs1), 0, m1), buf, ino, dirs0, files0, files), files1 ~ files0, m ∈ files, m ∈ files1, fd ∈ of1, n1 ≤ # buf, err1 = ESUCCESS ∨ ⌊err1⌋ ⊦ ino = 0, n1 = 0, (err0 = ESUCCESS ⊃ ( files [mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).ino, files[mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).ino] .meta:= mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).meta ] [mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).ino, files [mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).ino, files[mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).ino] .meta:= mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).meta ] [mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).ino ] .size:= mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).size ] [of1[fd].ino ] .content .stream to files [mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).ino, files[mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).ino] .meta:= mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).meta ] [mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).ino, files [mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).ino, files[mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).ino] .meta:= mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).meta ] [mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).ino ] .size:= mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).size ] [of1[fd].ino ] .size ).buf = splice(buf, 0, (files1[of1[fd].ino].content.stream to files1[of1[fd].ino].size).buf, of1[fd].pos, n) ∧ of1[fd, of1[fd].pos:= (ino2 + n)] = of1[fd, of1[fd].pos:= (of1[fd].pos + n)] ∧ n ≤ n1 ∧ of1[fd].ino ∈ files1 ∧ of1[fd].ino ∈ files [mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).ino, files[mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).ino] .meta:= mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).meta ] [mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).ino, files [mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).ino, files[mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).ino] .meta:= mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).meta ] [mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).ino ] .size:= mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).size ] ∧ files [mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).ino, files[mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).ino] .meta:= mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).meta ] [mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).ino, files [mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).ino, files[mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).ino] .meta:= mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).meta ] [mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).ino ] .size:= mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).size ] [of1[fd].ino ] .meta = files1[of1[fd].ino].meta ∧ files [mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).ino, files[mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).ino] .meta:= mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).meta ] [mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).ino, files [mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).ino, files[mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).ino] .meta:= mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).meta ] [mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).ino ] .size:= mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).size ] -- of1[fd].ino = files1 -- of1[fd].ino ∧ (of1[fd].mode = MODE_W ∨ of1[fd].mode = MODE_RW) ; files [mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).ino, files[mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).ino] .meta:= mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).meta ] [mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).ino, files [mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).ino, files[mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).ino] .meta:= mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).meta ] [mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).ino ] .size:= mkinode(m, md, false, # links(m, dirs1), 0, of1[fd].pos + ino).size ] ~ files1 ∧ of1 = of1[fd, of1[fd].pos:= (ino2 + n)] ∧ (err0 = EBADFD ∧ (fd ∈ of1[fd, of1[fd].pos:= (ino2 + n)] → of1[fd].mode ≠ MODE_W ∧ of1[fd].mode ≠ MODE_RW) ∨ ⌊err0⌋ ) ), mode ≠ MODE_W ∧ mode ≠ MODE_RW

Rule argument

Additional information