[Imprint][Data Privacy Statement][E-Mail]

View long theorem info. View the proof. Back to main index. View the specification. View theorem base summary, View theorem base listing, the used properties by spec, the dependency list, the symbol table,

Proof step 918 from proof refine-truncate (previous step)

boolvar ↔ m2 ≤ n0 ∧ pageno0 ≠ 0 ∧ (m2 / VFS_PAGE_SIZE ∈ content ∨ buf-opt0.some?), fs0[ri0[inodekey(m)]] = inodenode(key0, md0, false, m1, 0, m4), abs-files(fs0, ri0)[m] = mkfile(m0, md1, m3, content0), boolvar, buf-opt = buf-opt0, content = content0, dirs = abs-dirs(fs0, ri0), files = abs-files(fs0, ri0), files0 = files[ino, files[ino].content:= (content[pageno1, fill(files[ino].content[pageno1], zero, pageno0, VFS_PAGE_SIZE - pageno0)] upto pageno)], ino = m, new_inode = mkinode(m, md, false, m1, 0, m2), pageno = min(n0, m2), pageno0 = m2 % VFS_PAGE_SIZE, pageno1 = m2 / VFS_PAGE_SIZE, orphans(fs0, ri0).inodes?, fo.inodes?, afs-cons(abs-dirs(fs0, ri0), abs-files(fs0, ri0)), file-node-cons (fs0[adr1, truncnode(inodekey(m), m2)][adr2, inodenode(inodekey(m), md, false, m1, 0, n0)], ri0[inodekey(m), adr2] \ datakeys(inodekey(m), m2, ri0[inodekey(m), adr2])), file-node-cons(fs0, ri0), log-cons(log0, fs0), orphans-cons (fs0[adr1, truncnode(inodekey(m), m2)][adr2, inodenode(inodekey(m), md, false, m1, 0, n0)], ri0[inodekey(m), adr2] \ datakeys(inodekey(m), m2, ri0[inodekey(m), adr2]), orphans(fs0, ri0)), orphans-cons(fs0, ri0, orphans(fs0, ri0)), replay-cons-strong (fs0[adr1, truncnode(inodekey(m), m2)][adr2, inodenode(inodekey(m), md, false, m1, 0, n0)], ri0[inodekey(m), adr2] \ datakeys(inodekey(m), m2, ri0[inodekey(m), adr2]), orphans(fs0, ri0), fi, fo, (log0 + adr1 ') + adr2 '), replay-cons-strong(fs0, ri0, orphans(fs0, ri0), fi, fo, log0), ri-inj(ri0[inodekey(m), adr2] \ datakeys(inodekey(m), m2, ri0[inodekey(m), adr2])), ri-inj(ri0), ri-inj(fi), ubifs-cons (fs0[adr1, truncnode(inodekey(m), m2)][adr2, inodenode(inodekey(m), md, false, m1, 0, n0)], ri0[inodekey(m), adr2] \ datakeys(inodekey(m), m2, ri0[inodekey(m), adr2]), orphans(fs0, ri0), fi, fo, (log0 + adr1 ') + adr2 '), ubifs-cons(fs0, ri0, orphans(fs0, ri0), fi, fo, log0), inodekey(m) ∈ ri0, ri0[inodekey(m)] ∈ fs0, pageno1 ∈ files[ino].content, m2 ≤ n0, pageno0 + (VFS_PAGE_SIZE - pageno0) ≤ # files[ino].content[pageno1], VFS_PAGE_SIZE ≥ pageno0, asynced → boolvar0, m2 ≤ n0 → pageno0 ≠ 0 → VFS_PAGE_SIZE ≠ 0 ⊦ ⟨afs_inode_sync#(new_inode.size:= n0; dirs, files0); inode := (m ∈ dirs ⊃ mkinode(m, dirs[m].meta, true, dirs[m].nlink, dirs[m].nsubdirs, dirs[m].size) ;mkinode(m, files0[m].meta, false, files0[m].nlink, 0, files0[m].size) ); err := ESUCCESS; asynced := ?⟩ ( afs-cons(dirs, files0) → dirs = abs-dirs(fs0[adr1, truncnode(inodekey(m), m2)][adr2, inodenode(inodekey(m), md, false, m1, 0, n0)], ri0[inodekey(m), adr2]) ∧ files0 = abs-files (fs0[adr1, truncnode(inodekey(m), m2)][adr2, inodenode(inodekey(m), md, false, m1, 0, n0)], ri0[inodekey(m), adr2] \ datakeys(inodekey(m), m2, ri0[inodekey(m), adr2])) ∧ orphans (abs-dirs(fs0[adr1, truncnode(inodekey(m), m2)][adr2, inodenode(inodekey(m), md, false, m1, 0, n0)], ri0[inodekey(m), adr2]), abs-files(fs0[adr1, truncnode(inodekey(m), m2)][adr2, inodenode(inodekey(m), md, false, m1, 0, n0)], ri0[inodekey(m), adr2])) = abs-keys(orphans(fs0, ri0)) ∧ (asynced → boolvar4) ∧ buf-opt0 = some(fill(files[ino].content[pageno1], zero, pageno0, VFS_PAGE_SIZE - pageno0)) ∧ mkinode(m, md, false, m1, 0, n0) = inode ∧ ¬ boolvar ∧ ESUCCESS = err), m2 % VFS_PAGE_SIZE = 0, VFS_PAGE_SIZE = 0, adr1 = adr2, m = 0, buf-opt0.some?, adr2 ∈ fs0, adr1 ∈ fs0, datakey(m, m2 / VFS_PAGE_SIZE) ∈ ri0

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 919:
fs0[ri0[inodekey(m)]] = inodenode(key0, md0, false, m1, 0, m4), abs-files(fs0, ri0)[m] = mkfile(m0, md1, m3, content0), dirs = abs-dirs(fs0, ri0), files0 = abs-files(fs0, ri0) [m, mkfile (m0, md1, m3, content0[m2 / VFS_PAGE_SIZE, fill(content0[m2 / VFS_PAGE_SIZE], zero, m2 % VFS_PAGE_SIZE, VFS_PAGE_SIZE - m2 % VFS_PAGE_SIZE)] upto m2) ], m2 % VFS_PAGE_SIZE ≠ 0, adr1 ≠ adr2, m ≠ 0, orphans(fs0, ri0).inodes?, fo.inodes?, afs-cons(abs-dirs(fs0, ri0), abs-files(fs0, ri0)), file-node-cons (fs0[adr1, truncnode(inodekey(m), m2)][adr2, inodenode(inodekey(m), md, false, m1, 0, n0)], ri0[inodekey(m), adr2] \ datakeys(inodekey(m), m2, ri0[inodekey(m), adr2])), file-node-cons(fs0, ri0), log-cons(log0, fs0), orphans-cons (fs0[adr1, truncnode(inodekey(m), m2)][adr2, inodenode(inodekey(m), md, false, m1, 0, n0)], ri0[inodekey(m), adr2] \ datakeys(inodekey(m), m2, ri0[inodekey(m), adr2]), orphans(fs0, ri0)), orphans-cons(fs0, ri0, orphans(fs0, ri0)), replay-cons-strong (fs0[adr1, truncnode(inodekey(m), m2)][adr2, inodenode(inodekey(m), md, false, m1, 0, n0)], ri0[inodekey(m), adr2] \ datakeys(inodekey(m), m2, ri0[inodekey(m), adr2]), orphans(fs0, ri0), fi, fo, (log0 + adr1 ') + adr2 '), replay-cons-strong(fs0, ri0, orphans(fs0, ri0), fi, fo, log0), ri-inj(ri0[inodekey(m), adr2] \ datakeys(inodekey(m), m2, ri0[inodekey(m), adr2])), ri-inj(ri0), ri-inj(fi), ubifs-cons (fs0[adr1, truncnode(inodekey(m), m2)][adr2, inodenode(inodekey(m), md, false, m1, 0, n0)], ri0[inodekey(m), adr2] \ datakeys(inodekey(m), m2, ri0[inodekey(m), adr2]), orphans(fs0, ri0), fi, fo, (log0 + adr1 ') + adr2 '), ubifs-cons(fs0, ri0, orphans(fs0, ri0), fi, fo, log0), inodekey(m) ∈ ri0, ri0[inodekey(m)] ∈ fs0, m2 / VFS_PAGE_SIZE ∈ content0, m2 ≤ n0, VFS_PAGE_SIZE ≤ # content0[m2 / VFS_PAGE_SIZE], ¬ buf-opt0.some?, ¬ adr2 ∈ fs0, ¬ adr1 ∈ fs0, ¬ datakey(m, m2 / VFS_PAGE_SIZE) ∈ ri0, asynced → boolvar0 ⊦ ⟨afs_inode_sync#(mkinode(m, md, false, m1, 0, n0); dirs, files0); inode := (m ∈ dirs ⊃ mkinode(m, dirs[m].meta, true, dirs[m].nlink, dirs[m].nsubdirs, dirs[m].size) ;mkinode(m, files0[m].meta, false, files0[m].nlink, 0, files0[m].size) ); err := ESUCCESS; asynced := ?⟩ ¬ afs-cons(dirs, files0)

Rule argument

Additional information

Used simplifier rules: ⊦ mkfile(m, md, m0, content).content:= content0 = mkfile(m, md, m0, content0); (s)% ⊦ mkfile(m, md, m0, content).content = content; (s)%⊦ mkinode(m, md, boolvar, m0, m1, m2).size:= m6 = mkinode(m, md, boolvar, m0, m1, m6); (s)%c: ⊦ m + n = n + m; from specification nat-basic%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic% ⊦ m + n ≤ m + n0 ↔ n ≤ n0; (s)%n ≤ m ⊦ (m - n) + m0 ≤ n0 ↔ m + m0 ≤ n0 + n; (s)%n ≠ 0 ⊦ m % n ≤ n; (s)% ⊦ n ≥ m ↔ m ≤ n; (s)% ⊦ VFS_PAGE_SIZE ≠ 0; (s)%min-comm: ⊦ min(n0, n1) = min(n1, n0); from specification min-max% ⊦ n0 ≤ n1 → min(n0, n1) = n0; (s)