| abs-files(fs, ri)[m] = mkfile(m1, md1, m4, content0), fs[ri[inodekey(m)]] = inodenode(key, md0, false, m0, 0, m3), fo.inodes?, orphans(fs, ri).inodes?, afs-cons(abs-dirs(fs, ri), abs-files(fs, ri)), file-node-cons(fs, ri), log-cons(log, fs), orphans-cons(fs, ri, orphans(fs, ri)), replay-cons-strong(fs, ri, orphans(fs, ri), fi, fo, log), ri-inj(fi), ri-inj(ri), ubifs-cons(fs, ri, orphans(fs, ri), fi, fo, log), inodekey(m) ∈ ri, ri[inodekey(m)] ∈ fs, ⌊err0⌋ , buf-opt0.some? → # buf-opt0.buf = VFS_PAGE_SIZE, asynced → boolvar0 ⊦ ⟨choose err0 with ⌊err0⌋ in err := err0; asynced := ?⟩ ((asynced → boolvar4) ∧ err0 = err), ⟨let ino = m, content = content0, buf = ? in {pageno0 := m2 % VFS_PAGE_SIZE, pageno := min(n, m2); boolvar := m2 ≤ n ∧ pageno0 ≠ 0 ∧ (m2 / VFS_PAGE_SIZE ∈ content ∨ buf-opt0.some?); files := abs-files(fs, ri); buf-opt := buf-opt0; if boolvar then {pageno1 := m2 / VFS_PAGE_SIZE; if buf-opt.some? then buf := buf-opt.buf else buf := files[ino].content[pageno1]; buf := fill(buf, zero, pageno0, VFS_PAGE_SIZE - pageno0); content[pageno1] := buf; buf-opt := some(buf)}; files[ino].content := content upto pageno; let new_inode = mkinode(m, md, false, m0, 0, m2) in {new_inode.size := n; dirs := abs-dirs(fs, ri); afs_inode_sync#(new_inode; dirs, files)}; inode := (m ∈ dirs ⊃ mkinode(m, dirs[m].meta, true, dirs[m].nlink, dirs[m].nsubdirs, dirs[m].size) ;mkinode(m, files[m].meta, false, files[m].nlink, 0, files[m].size) ); err := ESUCCESS}; asynced := ?⟩ ( dirs = abs-dirs(fs, ri) ∧ files = abs-files(fs, ri) ∧ (asynced → boolvar4) ∧ buf-opt0 = buf-opt ∧ mkinode(m, md, false, m0, 0, m2) = inode ∧ (boolvar2 ↔ boolvar) ∧ err0 = err), m2 ≤ n ∧ m2 % VFS_PAGE_SIZE ≠ 0 |
fs[ri[inodekey(m)]] = inodenode(key, md0, false, m0, 0, m3), abs-files(fs, ri)[m] = mkfile(m1, md1, m4, content0), orphans(fs, ri).inodes?, fo.inodes?, afs-cons(abs-dirs(fs, ri), abs-files(fs, ri)), file-node-cons(fs, ri), log-cons(log, fs), orphans-cons(fs, ri, orphans(fs, ri)), replay-cons-strong(fs, ri, orphans(fs, ri), fi, fo, log), ri-inj(ri), ri-inj(fi), ubifs-cons(fs, ri, orphans(fs, ri), fi, fo, log), ri[inodekey(m)] ∈ fs, inodekey(m) ∈ ri, ⌊err1⌋ , asynced → boolvar0, buf-opt0.some? → # buf-opt0.buf = VFS_PAGE_SIZE ⊦ ∃ err0. ⌊err0⌋ ∧ ⟨err := err0; asynced := ?⟩ ((asynced → boolvar4) ∧ err1 = err), ⟨let ino = m, content = content0, buf = ? in {pageno0 := m2 % VFS_PAGE_SIZE, pageno := min(n, m2); boolvar := m2 ≤ n ∧ pageno0 ≠ 0 ∧ (m2 / VFS_PAGE_SIZE ∈ content ∨ buf-opt0.some?); files := abs-files(fs, ri); buf-opt := buf-opt0; if boolvar then {pageno1 := m2 / VFS_PAGE_SIZE; if buf-opt.some? then buf := buf-opt.buf else buf := files[ino].content[pageno1]; buf := fill(buf, zero, pageno0, VFS_PAGE_SIZE - pageno0); content[pageno1] := buf; buf-opt := some(buf)}; files[ino].content := content upto pageno; let new_inode = mkinode(m, md, false, m0, 0, m2) in {new_inode.size := n; dirs := abs-dirs(fs, ri); afs_inode_sync#(new_inode; dirs, files)}; inode := (m ∈ dirs ⊃ mkinode(m, dirs[m].meta, true, dirs[m].nlink, dirs[m].nsubdirs, dirs[m].size) ;mkinode(m, files[m].meta, false, files[m].nlink, 0, files[m].size) ); err := ESUCCESS}; asynced := ?⟩ ( dirs = abs-dirs(fs, ri) ∧ files = abs-files(fs, ri) ∧ (asynced → boolvar4) ∧ buf-opt0 = buf-opt ∧ mkinode(m, md, false, m0, 0, m2) = inode ∧ (boolvar2 ↔ boolvar) ∧ err1 = err), m2 ≤ n ∧ m2 % VFS_PAGE_SIZE ≠ 0