| dirs1 = dirs, err = err0, file0 = of[fd], files2 = files, fs = abs-files(files), n = n0, of2 = of, ofh = abs-of(of), root.dir?, dom of < ino, abs(root, ROOT_INO)(dirs), afs-cons(dirs, files), fids-cons(root, abs-files(files), abs-of(of)), of-cons(of, dirs, files), n0 ≤ # buf, psynced → asynced ⊦ ∀ n, err, of, dirs, files, asynced. (err = ESUCCESS ⊃ (files[file0.ino].content.stream to files[file0.ino].size).buf = splice(buf, 0, (files2[file0.ino].content.stream to files2[file0.ino].size).buf, file0.pos, n) ∧ fd ∈ of2 ∧ of = of2[fd, file0.pos:= (file0.pos + n)] ∧ n ≤ n0 ∧ file0.ino ∈ files2 ∧ file0.ino ∈ files ∧ files[file0.ino].meta = files2[file0.ino].meta ∧ files -- file0.ino = files2 -- file0.ino ∧ (file0.mode = MODE_W ∨ file0.mode = MODE_RW) ;files ~ files2 ∧ of2 = of ∧ (err = EBADFD ∧ (fd ∈ of → file0.mode ≠ MODE_W ∧ file0.mode ≠ MODE_RW) ∨ ⌊err⌋ ) ) → dirs1 = dirs → ⟨posix_write#(fd, buf, user, root; n0, err0, fs, ofh; psynced)⟩ (ofh = abs-of(of) ∧ fs = abs-files(files) ∧ abs(root, ROOT_INO)(dirs) ∧ (psynced → asynced) ∧ n = n0 ∧ err = err0) |
fs = abs-files(files), ofh = abs-of(of), root.dir?, dom of < ino, abs(root, ROOT_INO)(dirs), afs-cons(dirs, files), fids-cons(root, abs-files(files), abs-of(of)), of-cons(of, dirs, files), n0 ≤ # buf, psynced → asynced, (err1 = ESUCCESS ⊃ (files0[of[fd].ino].content.stream to files0[of[fd].ino].size).buf = splice(buf, 0, (files[of[fd].ino].content.stream to files[of[fd].ino].size).buf, of[fd].pos, n1) ∧ fd ∈ of ∧ of0 = of[fd, of[fd].pos:= (of[fd].pos + n1)] ∧ n1 ≤ n0 ∧ of[fd].ino ∈ files ∧ of[fd].ino ∈ files0 ∧ files0[of[fd].ino].meta = files[of[fd].ino].meta ∧ files0 -- of[fd].ino = files -- of[fd].ino ∧ (of[fd].mode = MODE_W ∨ of[fd].mode = MODE_RW) ;files0 ~ files ∧ of = of0 ∧ (err1 = EBADFD ∧ (fd ∈ of0 → of0[fd].mode ≠ MODE_W ∧ of0[fd].mode ≠ MODE_RW) ∨ ⌊err1⌋ ) ) ⊦ ⟨posix_write#(fd, buf, user, root; n0, err0, fs, ofh; psynced)⟩ (ofh = abs-of(of0) ∧ fs = abs-files(files0) ∧ (psynced → asynced0) ∧ n1 = n0 ∧ err1 = err0)