| boolvar ↔ m2 ≤ n ∧ pageno0 ≠ 0 ∧ (m2 / VFS_PAGE_SIZE ∈ content ∨ buf-opt0.some?), VFS_PAGE_SIZE = n0 + m2 % VFS_PAGE_SIZE, abs-files(fs, ri)[m] = mkfile(m0, md1, m1, content0), fs[ri[inodekey(m)]] = inodenode(key, md0, false, m3, 0, m5), fs[ri[datakey(m, m2 / VFS_PAGE_SIZE)]] = datanode(key0, buf0), content = content0, ino = m, pageno = min(n, m2), pageno0 = m2 % VFS_PAGE_SIZE, key0.data?, 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-cons(ri, fs), ri-inj(ri), ri-inj(fi), ubifs-cons(fs, ri, orphans(fs, ri), fi, fo, log), inodekey(m) ∈ ri, ri[inodekey(m)] ∈ fs, ri[datakey(m, m2 / VFS_PAGE_SIZE)] ∈ fs, datakey(m, m2 / VFS_PAGE_SIZE) ∈ ri, m2 ≤ n, asynced → boolvar0, m2 ≤ n → pageno0 ≠ 0 → VFS_PAGE_SIZE ≠ 0, ∀ adr, adr0, adr1. adr ∈ fs ∨ adr0 ∈ fs ∨ adr1 ∈ fs ∨ adr = adr0 ∨ adr = adr1 ∨ adr0 = adr1 ⊦ ⟨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, m3, 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, m3, 0, m2) = inode ∧ (boolvar2 ↔ boolvar) ∧ ENOSPC = err), ⟨err := ENOSPC; asynced := ?⟩ ((asynced → boolvar4) ∧ ENOSPC = err), m2 % VFS_PAGE_SIZE = 0, VFS_PAGE_SIZE = 0, m = 0, buf-opt0.some? |
boolvar ↔ m2 ≤ n ∧ pageno0 ≠ 0 ∧ (m2 / VFS_PAGE_SIZE ∈ content ∨ buf-opt0.some?), VFS_PAGE_SIZE = n0 + m2 % VFS_PAGE_SIZE, fs[ri[datakey(m, m2 / VFS_PAGE_SIZE)]] = datanode(key0, buf0), fs[ri[inodekey(m)]] = inodenode(key, md0, false, m3, 0, m5), abs-files(fs, ri)[m] = mkfile(m0, md1, m1, content0), content = content0, files = abs-files(fs, ri), ino = m, pageno = min(n, m2), pageno0 = m2 % VFS_PAGE_SIZE, key0.data?, 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-cons(ri, fs), ri-inj(fi), ri-inj(ri), ubifs-cons(fs, ri, orphans(fs, ri), fi, fo, log), datakey(m, m2 / VFS_PAGE_SIZE) ∈ ri, ri[datakey(m, m2 / VFS_PAGE_SIZE)] ∈ fs, ri[inodekey(m)] ∈ fs, inodekey(m) ∈ ri, m2 ≤ n, m2 ≤ n → pageno0 ≠ 0 → VFS_PAGE_SIZE ≠ 0, asynced → boolvar0, ∀ adr, adr0, adr1. adr ∈ fs ∨ adr0 ∈ fs ∨ adr1 ∈ fs ∨ adr = adr0 ∨ adr = adr1 ∨ adr0 = adr1 ⊦ ⟨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, m3, 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, m3, 0, m2) = inode ∧ (boolvar2 ↔ boolvar) ∧ ENOSPC = err), ⟨err := ENOSPC; asynced := ?⟩ ((asynced → boolvar4) ∧ ENOSPC = err), m2 % VFS_PAGE_SIZE = 0, VFS_PAGE_SIZE = 0, m = 0, buf-opt0.some?