| files[m] = mkfile(m1, md, # links(m, dirs), content), of[fd] = mkfile(m, mode, m0), root.dir?, dom of < ino2, abs(root, ROOT_INO)(dirs), afs-cons(dirs, files), fids-cons(root, abs-files(files), abs-of(of)), of-cons(of, dirs, files), read-inv(m0, m0 + n0, mkinode(m, md, false, # links(m, dirs), 0, m1), buf0, buf1, 0, dirs, files), read-inv(m0, m0 + n0, mkinode(m, md, false, # links(m, dirs), 0, m1), buf0, buf0, 0, dirs, files), fd ∈ of, m ∈ files, m0 + 0 ≤ # (content.stream to m1).buf, 0 + 0 ≤ # buf0, m0 ≤ m1, n0 ≤ # buf0, finp(content.stream) → ⌜m1⌝ < # content.stream ∨ ⌜m1⌝ = # content.stream, psynced → asynced ⊦ ⟨ofh := abs-of(of[fd, mkfile(m, mode, m0 + 0)])⟩ (ofh = abs-of(of[fd, of[fd].pos:= m0]) ∧ (psynced → asynced) ∧ buf1 = copy((content.stream to m1).buf, m0, buf0, 0, 0) ∧ 0 = 0), buf1 = buf0, mode ≠ MODE_R ∧ mode ≠ MODE_RW |
of[fd] = mkfile(m, mode, m0), files[m] = mkfile(m1, md, # links(m, dirs), content), root.dir?, dom of < ino2, abs(root, ROOT_INO)(dirs), afs-cons(dirs, files), fids-cons(root, abs-files(files), abs-of(of)), of-cons(of, dirs, files), read-inv(m0, m0 + n0, mkinode(m, md, false, # links(m, dirs), 0, m1), buf0, buf0, 0, dirs, files), read-inv(m0, m0 + n0, mkinode(m, md, false, # links(m, dirs), 0, m1), buf0, buf1, 0, dirs, files), m ∈ files, fd ∈ of, n0 ≤ # buf0, m0 ≤ m1, 0 + 0 ≤ # buf0, m0 + 0 ≤ # (content.stream to m1).buf, psynced → asynced, finp(content.stream) → ⌜m1⌝ < # content.stream ∨ ⌜m1⌝ = # content.stream ⊦ buf1 = buf0, mode ≠ MODE_R ∧ mode ≠ MODE_RW, abs-of(of[fd, mkfile(m, mode, m0 + 0)]) = abs-of(of[fd, of[fd].pos:= m0]) ∧ (psynced → asynced) ∧ buf1 = copy((content.stream to m1).buf, m0, buf0, 0, 0) ∧ 0 = 0