Proof step 230 from proof inv-write (previous step)

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

• Proof step 231:

  m5 + n1 = m5 / VFS_PAGE_SIZE * VFS_PAGE_SIZE + VFS_PAGE_SIZE, of[fd] = mkfile(m, mode, m0), files1[m] = mkfile(m5, md, # links(m, dirs), content0), err = err0, err2 = ESUCCESS, m5 = n2 + m5 / VFS_PAGE_SIZE * VFS_PAGE_SIZE, dom of < ino3, m5 < m0 + ino4, afs-cons(dirs, files), afs-cons(dirs, files1), of-cons(of, dirs, files), of-cons(of, dirs, files1), m ∈ files1, m5 / VFS_PAGE_SIZE ∈ content0, fd ∈ of, m5 % VFS_PAGE_SIZE + n1 ≤ VFS_PAGE_SIZE, n ≤ # buf0, n2 + n1 ≤ VFS_PAGE_SIZE, ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ [ino0 := m5; dirs1 := dirs; if err = ESUCCESS then afs_write_inode# ( (m ∈ dirs ⊃ mkinode(m, dirs[m].meta, true, dirs[m].nlink, dirs[m].nsubdirs, dirs[m].size) ;mkinode (m, files1 [m, files1 [m, files1 [m, mkfile (m5, md, # links(m, dirs), content0[m5 / VFS_PAGE_SIZE, fill(content0[m5 / VFS_PAGE_SIZE], zero, m5 % VFS_PAGE_SIZE, n1)] upto m5) ] [m ] .size:= m5 ] [m ] .meta:= md ] [m ] .meta, false, files1 [m, files1 [m, files1 [m, mkfile (m5, md, # links(m, dirs), content0[m5 / VFS_PAGE_SIZE, fill(content0[m5 / VFS_PAGE_SIZE], zero, m5 % VFS_PAGE_SIZE, n1)] upto m5) ] [m ] .size:= m5 ] [m ] .meta:= md ] [m ] .nlink, 0, files1 [m, files1 [m, files1 [m, mkfile (m5, md, # links(m, dirs), content0[m5 / VFS_PAGE_SIZE, fill(content0[m5 / VFS_PAGE_SIZE], zero, m5 % VFS_PAGE_SIZE, n1)] upto m5) ] [m ] .size:= m5 ] [m ] .meta:= md ] [m ] .size) ) .size:= (m0 + ino4) ; err, dirs, files ; asynced); if err ≠ ESUCCESS then ino4 := (m0 ≤ ino0 ⊃ ino0 - m0;0), err := ESUCCESS; of[fd].pos := m0 + ino4] (dirs1 = dirs → of-cons(of, dirs, files) ∧ dom of < ino3 ∧ afs-cons(dirs, files)), ino4 = 0, n = 0, n2 = 0, err1 = ESUCCESS ∧ ¬ isdir, mode ≠ MODE_W ∧ mode ≠ MODE_RW

Rule argument

Additional information