| ⟪while err0 = ESUCCESS ∧ ¬ isdir0 do vfs_read_block#(n3, n2, inode, dirs, files, asynced; buf, n4, isdir0, err0)⟫ true, ⟨vfs_read_block#(n0, n1, inode, dirs, files, asynced; buf1, n, isdir, err)⟩ (buf1 = buf0 ∧ n = n9 ∧ (isdir ↔ isdir0) ∧ err = err0), ⟪vfs_read_block#(n0, n1, inode, dirs, files, asynced; buf1, n, isdir, err)⟫ ⟪n10 := n0, n11 := n1, buf2 := buf1, n12 := n; while err = ESUCCESS ∧ ¬ isdir do vfs_read_block#(n10, n11, inode, dirs, files, asynced; buf2, n12, isdir, err)⟫ true, VFS_PAGE_SIZE = n7 + (n0 + n6) % VFS_PAGE_SIZE, files[m] = mkfile(m3, md0, # links(m, dirs), content), buf = buf0, buf1 = copy(zeropage, (n0 + n6) % VFS_PAGE_SIZE, buf2, n6, min(n5, n7, n8)), err = ESUCCESS, inode = mkinode(m, md, boolvar, m0, m1, n8 + n0 + n6), ¬ isdir, n = n6 + min(n5, n7, n8), n1 = n5 + n0 + n6, n2 = n1, n3 = n0, n4 = n9, afs-cons(dirs, files), m ∈ files, n5 + n6 ≤ # buf2, n6 ≤ # buf2, n6 + min(n5, n7, n8) ≤ # buf2, (n0 + n6) % VFS_PAGE_SIZE + min(n5, n7, n8) ≤ VFS_PAGE_SIZE, ∀ n2, n3, n4, err, inode, m, md, boolvar, m0, m1, m2, isdir, dirs, files, buf, asynced. n2 - n3 + n4 < n5 → err = ESUCCESS ∧ inode = mkinode(m, md, boolvar, m0, m1, m2) ∧ ¬ isdir ∧ afs-cons(dirs, files) ∧ m ∈ files ∧ n4 ≤ # buf ∧ n3 + n4 ≤ m2 ∧ n3 + n4 ≤ n2 ∧ n2 ≤ # buf + n3 → ⟪vfs_read_block#(n3, n2, inode, dirs, files, asynced; buf, n4, isdir, err); while err = ESUCCESS ∧ ¬ isdir do vfs_read_block#(n3, n2, inode, dirs, files, asynced; buf, n4, isdir, err)⟫ true ⊦ ⟪while err0 = ESUCCESS ∧ ¬ isdir0 do vfs_read_block#(n0, n1, inode, dirs, files, asynced; buf0, n9, isdir0, err0)⟫ true, n5 = 0, n7 = 0, n8 = 0, (n0 + n6) / VFS_PAGE_SIZE ∈ content |