| files[m] = mkfile(m1, md, m2, content), of[fd] = mkfile(m, mode, m0), err0 = ESUCCESS, f = abs-files(files)[fh.fid], fh = ofh[fd], n = n0, ofh = abs-of(of), root.dir?, dom of < ino0, abs(root, ROOT_INO)(dirs), afs-cons(dirs, files), fids-cons(root, abs-files(files), abs-of(of)), of-cons(of, dirs, files), fd ∈ ofh, fd ∈ of, fh.fid ∈ abs-files(files), psynced → asynced ⊦ ⟨ofh[fd] := mkfh(ofh[fd].fid, ofh[fd].mode, # f.content + n)⟩ (ofh = abs-of(of[fd, of[fd].pos:= (m1 + n0)]) ∧ (psynced → asynced) ∧ m1 + n0 = # f.content + n ∧ ESUCCESS = err0) |
Used simplifier rules: ⊦ fd ∈ abs-of(of) ↔ fd ∈ of; (s)%fd ∈ of ⊦ abs-of(of)[fd] = mkfh(⌜of[fd].ino⌝ , of[fd].mode, of[fd].pos); (s)% ⊦ mkfh(fid, mode, m).fid = fid; (s)% ⊦ ⌜ino⌝ ∈ abs-files(files) ↔ ino ∈ files; (s)% ⊦ mkfh(fid, mode, m).mode = mode; (s)%⊦ ino ∈ files → abs-files(files)[⌜ino⌝ ] = mkfile (files[ino].meta, (files[ino].content.stream to files[ino].size).buf); (s)% ⊦ mkfile(md, buf).content = buf; (s)% ⊦ mkfile(m, mode, m0).ino = m; (s)% ⊦ finp(σ0 to m); (s)%finp(σ) ⊦ # σ.buf = (# σ).n; (s)% ⊦ # content.stream = ∞; (s)% ⊦ ¬ ∞ < n∞; (s)%¬ # σ0 < ⌜n⌝ ⊦ #(σ0 to n) = ⌜n⌝ ; (s)% ⊦ ⌜m⌝ .n = m; (s)%⊦ abs-of(of)[fd, mkfh(⌜ino⌝ , mode, n)] = abs-of(of[fd, mkfile(ino, mode, n)]); (s)% ⊦ m + n = m + n0 ↔ n = n0; (s)%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic%c: ⊦ m + n = n + m; from specification nat-basic% ⊦ mkfile(m, mode, m0).mode = mode; (s)% ⊦ mkfile(m, mode, m0).pos:= m2 = mkfile(m, mode, m2); (s)%afs-cons-file-nlink: ⊦ afs-cons(dirs, files) ∧ ino ∈ files ∧ files[ino] = mkfile(m, md, n, content) → # links(ino, dirs) = n; (forward) from specification afs-base% ⊦ mkfile(m, md, m0, content).size = m; (s)