[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 449 from proof refine-truncate (previous step)

boolvar ↔ datakey(mkinode(m, md, false, fs[ri[inodekey(m)]].nlink, 0, m2).ino, m2 / VFS_PAGE_SIZE) ∈ ri, 0 = fs[ri[inodekey(m)]].nsubdirs, boolvar, dirs = abs-dirs(fs, ri), err = ESUCCESS, err = err0, files = abs-files(fs, ri), inode = mkinode(m, md, false, fs[ri[inodekey(m)]].nlink, 0, m2), key1 = inodekey(mkinode(m, md, false, fs[ri[inodekey(m)]].nlink, 0, m2).ino), m0 = fs[ri[inodekey(m)]].nlink, nd = fs[ri[datakey(mkinode(m, md, false, fs[ri[inodekey(m)]].nlink, 0, m2).ino, m2 / VFS_PAGE_SIZE)]], nd0 = inodenode (inodekey(mkinode(m, md, false, fs[ri[inodekey(m)]].nlink, 0, m2).ino), mkinode(m, md, false, fs[ri[inodekey(m)]].nlink, 0, m2).meta, mkinode(m, md, false, fs[ri[inodekey(m)]].nlink, 0, m2).directory, fs[ri[inodekey(m)]].nlink, mkinode(m, md, false, fs[ri[inodekey(m)]].nlink, 0, m2).nsubdirs, n), ro = orphans(fs, ri), ro0 = orphans(fs, ri), nd.data?, fs[ri[inodekey(m)]].inode?, 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), inodekey(m) ∈ ri, ri[inodekey(m)] ∈ fs, datakey(mkinode(m, md, false, fs[ri[inodekey(m)]].nlink, 0, m2).ino, m2 / VFS_PAGE_SIZE) ∈ ri, ri[datakey(mkinode(m, md, false, fs[ri[inodekey(m)]].nlink, 0, m2).ino, m2 / VFS_PAGE_SIZE)] ∈ fs, inode.size % VFS_PAGE_SIZE + (VFS_PAGE_SIZE - inode.size % VFS_PAGE_SIZE) ≤ # nd.data, m2 ≤ n, VFS_PAGE_SIZE ≥ inode.size % VFS_PAGE_SIZE, asynced → boolvar4, ⌊err0⌋ ∨ err0 = ESUCCESS ⊦ [aubifs_core_journal_add3# (truncnode(key1, min(n, inode.size)), nd0, nd.data:= fill(nd.data, zero, inode.size % VFS_PAGE_SIZE, VFS_PAGE_SIZE - inode.size % VFS_PAGE_SIZE), ri, fi, ro, fo ; adr1, adr0, adr, fs, log ; boolvar4, err); if err = ESUCCESS then aubifs_core_index_store#(datakey(inode.ino, m2 / VFS_PAGE_SIZE), adr, fi, ro, fo, fs, log, boolvar4; ri); buf-opt := buf-opt0; boolvar1 := boolvar2; nd.data := fill(nd.data, zero, inode.size % VFS_PAGE_SIZE, VFS_PAGE_SIZE - inode.size % VFS_PAGE_SIZE); if err = ESUCCESS then {aubifs_core_index_store#(inodekey(inode.ino), adr0, fi, ro, fo, fs, log, boolvar4; ri); aubifs_core_index_truncate#(key1, min(n, inode.size), fi, ro, fo, fs, log, boolvar4; ri); boolvar1 := boolvar; inode := mkinode(inode.ino, nd0.meta, nd0.directory, nd0.nlink, nd0.nsubdirs, nd0.size); if boolvar1 then buf-opt := some(nd.data)}] ( ubifs-cons(fs, ri, ro0, fi, fo, log) ∧ replay-cons-strong(fs, ri, ro0, fi, fo, log) ∧ file-node-cons(fs, ri) ∧ orphans-cons(fs, ri, ro0) ∧ ri-inj(ri) ∧ log-cons(log, fs) → ⟨p_inode := mkinode(m, md, false, m0, 0, m2); afs_truncate#(n, m2 / VFS_PAGE_SIZE; buf-opt0, p_inode, boolvar2, err1, dirs, files, asynced)⟩ ( dirs = abs-dirs(fs, ri) ∧ files = abs-files(fs, ri) ∧ orphans(abs-dirs(fs, ri), abs-files(fs, ri)) = abs-keys(ro0) ∧ (asynced → boolvar4) ∧ buf-opt = buf-opt0 ∧ inode = p_inode ∧ (boolvar1 ↔ boolvar2) ∧ err = err1)), m2 % VFS_PAGE_SIZE = 0, VFS_PAGE_SIZE = 0, fs[ri[inodekey(m)]].directory, buf-opt0.some?

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 450:
0 = fs[ri[inodekey(m)]].nsubdirs, dirs = abs-dirs(fs, ri), files = abs-files(fs, ri), inode = mkinode(m, md, false, fs[ri[inodekey(m)]].nlink, 0, m2), m0 = fs[ri[inodekey(m)]].nlink, nd = fs[ri[datakey(m, m2 / VFS_PAGE_SIZE)]], nd0 = inodenode(inodekey(m), md, false, fs[ri[inodekey(m)]].nlink, 0, n), ro = orphans(fs, ri), m2 % VFS_PAGE_SIZE ≠ 0, fs[ri[datakey(m, m2 / VFS_PAGE_SIZE)]].data?, fs[ri[inodekey(m)]].inode?, 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), inodekey(m) ∈ ri, ri[inodekey(m)] ∈ fs, ri[datakey(m, m2 / VFS_PAGE_SIZE)] ∈ fs, datakey(m, m2 / VFS_PAGE_SIZE) ∈ ri, m2 ≤ n, ¬ fs[ri[inodekey(m)]].directory, ¬ buf-opt0.some?, asynced → boolvar4 ⊦ [aubifs_core_journal_add3# (truncnode(inodekey(m), min(n, inode.size)), nd0, nd.data:= fill(nd.data, zero, inode.size % VFS_PAGE_SIZE, VFS_PAGE_SIZE - inode.size % VFS_PAGE_SIZE), ri, fi, orphans(fs, ri), fo ; adr1, adr0, adr, fs, log ; boolvar4, err0); if err0 = ESUCCESS then aubifs_core_index_store#(datakey(inode.ino, m2 / VFS_PAGE_SIZE), adr, fi, ro, fo, fs, log, boolvar4; ri); buf-opt := buf-opt0; boolvar1 := boolvar2; nd.data := fill(nd.data, zero, inode.size % VFS_PAGE_SIZE, VFS_PAGE_SIZE - inode.size % VFS_PAGE_SIZE); if err0 = ESUCCESS then {aubifs_core_index_store#(inodekey(inode.ino), adr0, fi, ro, fo, fs, log, boolvar4; ri); aubifs_core_index_truncate#(inodekey(m), min(n, inode.size), fi, ro, fo, fs, log, boolvar4; ri); boolvar1 := true; inode := mkinode(inode.ino, nd0.meta, nd0.directory, nd0.nlink, nd0.nsubdirs, nd0.size); if boolvar1 then buf-opt := some(nd.data)}] ( ubifs-cons(fs, ri, ro, fi, fo, log) ∧ replay-cons-strong(fs, ri, ro, fi, fo, log) ∧ file-node-cons(fs, ri) ∧ orphans-cons(fs, ri, ro) ∧ ri-inj(ri) ∧ log-cons(log, fs) → ⟨p_inode := mkinode(m, md, false, m0, 0, m2); afs_truncate#(n, m2 / VFS_PAGE_SIZE; buf-opt0, p_inode, boolvar2, err1, dirs, files, asynced)⟩ ( dirs = abs-dirs(fs, ri) ∧ files = abs-files(fs, ri) ∧ orphans(abs-dirs(fs, ri), abs-files(fs, ri)) = abs-keys(ro) ∧ (asynced → boolvar4) ∧ buf-opt = buf-opt0 ∧ inode = p_inode ∧ (boolvar1 ↔ boolvar2) ∧ err0 = err1))

Rule argument

Additional information

Used simplifier rules: ubifs-file-in: ⊦ datakey(ino, n) ∈ ri ∧ ubifs-cons(fs, ri, ro, fi, fo, log) → inodekey(ino) ∈ ri; (forward) from specification aubifs-inv%ubifs-file-notdir: ⊦ datakey(ino, n) ∈ ri ∧ ubifs-cons(fs, ri, ro, fi, fo, log) → ¬ fs[ri[inodekey(ino)]].directory; (forward) from specification aubifs-inv% ⊦ ¬ ⌊ESUCCESS⌋ ; (s)%c: ⊦ m + n = n + m; from specification nat-basic%a: ⊦ (m + n0) + n1 = m + n0 + n1; from specification nat-basic% ⊦ m ≤ m; (s)% ⊦ m + n ≤ m + n0 ↔ n ≤ n0; (s)%n ≤ m ⊦ (m - n) + m0 ≤ n0 ↔ m + m0 ≤ n0 + n; (s)%⊦ datakey(m, n) ∈ ri ∧ ubifs-cons(fs, ri, ro, fi, fo, log) → # fs[ri[datakey(m, n)]].data = VFS_PAGE_SIZE; (s)%n ≠ 0 ⊦ m % n ≤ n; (s)% ⊦ n ≥ m ↔ m ≤ n; (s)% ⊦ mkinode(m, md, boolvar, m0, m1, m2).size = m2; (s)% ⊦ VFS_PAGE_SIZE ≠ 0; (s)% ⊦ mkinode(m, md, boolvar, m0, m1, m2).nsubdirs = m1; (s)% ⊦ mkinode(m, md, boolvar, m0, m1, m2).directory ↔ boolvar; (s)% ⊦ mkinode(m, md, boolvar, m0, m1, m2).meta = md; (s)% ⊦ mkinode(m, md, boolvar, m0, m1, m2).ino = m; (s)