Proof step 98 from proof write-prepost-partial (previous step)

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 99:

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

Rule argument

Additional information