| files0[m] = mkfile(m1, md, # links(m, dirs0), content0), of[fd] = mkfile(m, mode, m0), dirs = dirs0[ino, dirs0[ino].meta:= inode.meta], dirs1 = dirs0, err = ESUCCESS, files = files0[m, mkfile(m1, md, # links(m, dirs0), content0 upto m1)], ino = inode.ino, ino4 = 0, inode = mkinode(m, md, false, # links(m, dirs0), 0, m1), inode0 = (inode1.ino ∈ dirs ⊃ mkinode(inode1.ino, dirs[inode1.ino].meta, true, dirs[inode1.ino].nlink, dirs[inode1.ino].nsubdirs, dirs[inode1.ino].size) ;mkinode(inode1.ino, files[inode1.ino].meta, false, files[inode1.ino].nlink, 0, files[inode1.ino].size) ), inode1 = mkinode(m, md, false, # links(m, dirs0), 0, m1), dom of < ino3, afs-cons(dirs0, files0), of-cons(of, dirs0, files0), ino ∈ dirs0, fd ∈ of, m ∈ files0, n0 ≤ # buf0 ⊦ [vfs_write_loop#(m0, inode0, m0 + n0, buf0, dirs; ino4, err, files, asynced); if ino4 ≠ 0 then err := ESUCCESS; if err = ESUCCESS then let ino = inode0.size in {n0 := ino4, ino1 := m0 + ino4; if ino4 ≠ 0 ∧ ino < ino1 then {inode0.size := ino1; afs_check_commit#(dirs, files; err; asynced); if err = ESUCCESS then afs_write_inode#(inode0; err, dirs, files; asynced)}; if err ≠ ESUCCESS then n0 := (m0 ≤ ino ⊃ ino - m0;0), err := ESUCCESS; of[fd].pos := m0 + n0}] (dirs1 = dirs → of-cons(of, dirs, files) ∧ dom of < ino3 ∧ afs-cons(dirs, files)), n0 = 0, ino ∈ files, mode ≠ MODE_W ∧ mode ≠ MODE_RW, m1 % VFS_PAGE_SIZE ≠ 0 ∧ m1 / VFS_PAGE_SIZE ∈ content0 |
Used simplifier rules: ⊦ mkfile(m, md, m0, content).size = m; (s)% ⊦ mkfile(m, md, m0, content).nlink = m0; (s)% ⊦ mkfile(m, md, m0, content).meta = md; (s)% ⊦ files[ino, af][ino0] = (ino0 = ino ∧ ino ∈ files ⊃ af;files[ino0]); (s)%⊦ of-cons(of, dirs, files) ∧ fd ∈ of ∧ of[fd] = mkfile(ino, mode, n) ∧ afs-cons(dirs, files) → ¬ ino ∈ dirs; (s)% ⊦ ino ∈ dirs[ino0, ad] ↔ ino ∈ dirs; (s)% ⊦ mkinode(m, md, boolvar, m0, m1, m2).meta = md; (s)% ⊦ mkinode(m, md, boolvar, m0, m1, m2).ino = m; (s)