| files0 -- of[fd].ino = files -- of[fd].ino, (content.stream to m).buf = splice(buf, 0, (files[of[fd].ino].content.stream to files[of[fd].ino].size).buf, of[fd].pos, n1), files0[of[fd].ino] = mkfile(m, md, m0, content), fs = abs-files(files), md = files[of[fd].ino].meta, 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), fd ∈ of, of[fd].ino ∈ files, of[fd].ino ∈ files0, n1 ≤ # buf, n0 ≤ # buf, n1 ≤ n0, psynced → asynced, of[fd].mode = MODE_W ∨ of[fd].mode = MODE_RW ⊦ fd ∈ ofh ∧ (ofh[fd].mode = MODE_W ∨ ofh[fd].mode = MODE_RW) ∧ ⟨err0 := ESUCCESS; if err0 = ESUCCESS then let fh = ofh[fd] in let f = fs[fh.fid] in choose n with n ≤ n0 in {n0 := n; f.content := splice(buf, 0, f.content, fh.pos, n0); fs[fh.fid] := f; ofh[fd].pos := fh.pos + n0} else n0 := ?; psynced := ?⟩ (ofh = abs-of(of[fd, of[fd].pos:= (of[fd].pos + n0)]) ∧ fs = abs-files(files0) ∧ (psynced → asynced0) ∧ n1 = n0 ∧ ESUCCESS = err0) |
files0 -- of[fd].ino = files -- of[fd].ino, (content.stream to m).buf = splice(buf, 0, (files[of[fd].ino].content.stream to files[of[fd].ino].size).buf, of[fd].pos, n1), files0[of[fd].ino] = mkfile(m, files[of[fd].ino].meta, m0, content), 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), of[fd].ino ∈ files0, of[fd].ino ∈ files, fd ∈ of, n1 ≤ n0, n0 ≤ # buf, n1 ≤ # buf, psynced → asynced, of[fd].mode = MODE_W ∨ of[fd].mode = MODE_RW ⊦ fd ∈ ofh ∧ (ofh[fd].mode = MODE_W ∨ ofh[fd].mode = MODE_RW) ∧ ⟨err0 := ESUCCESS; if err0 = ESUCCESS then let fh = ofh[fd] in let f = fs[fh.fid] in choose n with n ≤ n0 in {n0 := n; f.content := splice(buf, 0, f.content, fh.pos, n0); fs[fh.fid] := f; ofh[fd].pos := fh.pos + n0} else n0 := ?; psynced := ?⟩ (ofh = abs-of(of[fd, of[fd].pos:= (of[fd].pos + n0)]) ∧ fs = abs-files(files0) ∧ (psynced → asynced0) ∧ n1 = n0 ∧ ESUCCESS = err0)