| files0 -- m2 = files -- m2, (content.stream to m).buf = splice(buf, 0, (content0.stream to m1).buf, m3, n1), files[m2] = mkfile(m1, md, # links(m2, dirs), content0), files0[m2] = mkfile(m, md, m0, content), of[fd] = mkfile(m2, mode, m3), 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), m2 ∈ files0, fd ∈ of, m2 ∈ files, n1 ≤ n0, n0 ≤ # buf, n1 ≤ # buf, psynced → asynced, mode = MODE_W ∨ mode = MODE_RW ⊦ ⟨n0 := n1; f := mkfile(md, splice(buf, 0, (content0.stream to m1).buf, m3, n0)); fs := abs-files(files)[⌜m2⌝ , f]; ofh := abs-of(of[fd, mkfile(m2, mode, m3 + n0)]); psynced := ?⟩ (ofh = abs-of(of[fd, of[fd].pos:= (m3 + n0)]) ∧ fs = abs-files(files0) ∧ (psynced → asynced0) ∧ n1 = n0) |
files0 -- m2 = files -- m2, (content.stream to m).buf = splice(buf, 0, (content0.stream to m1).buf, m3, n1), of[fd] = mkfile(m2, mode, m3), files0[m2] = mkfile(m, md, m0, content), files[m2] = mkfile(m1, md, # links(m2, dirs), content0), 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), m2 ∈ files, fd ∈ of, m2 ∈ files0, n1 ≤ # buf, n0 ≤ # buf, n1 ≤ n0, psynced → asynced, mode = MODE_W ∨ mode = MODE_RW ⊦ ⟨f := mkfile(md, splice(buf, 0, (content0.stream to m1).buf, m3, n1)); fs := abs-files(files)[⌜m2⌝ , f]; ofh := abs-of(of[fd, mkfile(m2, mode, m3 + n1)]); psynced := ?⟩ (ofh = abs-of(of[fd, of[fd].pos:= (m3 + n1)]) ∧ fs = abs-files(files0) ∧ (psynced → asynced0) ∧ n1 = n1)