[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 116 from proof refine-truncate-buff-none-cached (previous step)

# buf0 = VFS_PAGE_SIZE, asynced1 ↔ true, asynced ↔ false, VFS_PAGE_SIZE = n0 + m2 % VFS_PAGE_SIZE, ((cache_files ⊕ cache_pcache0) ⊕ cache_icache)[m3] = mkfile(m0, md0, # links(m3, cache_dirs), content0), cache_files[m3] = mkfile(m1, md2, # links(m3, cache_dirs), content1), cache_pcache0[datakey(m3, m2 / VFS_PAGE_SIZE)] = mkpentry(boolvar, buf0), afs_files = (cache_files ⊕ cache_pcache0) ⊕ cache_icache, buf = some(fill(some(buf0).buf, zero, m2 % VFS_PAGE_SIZE, n0)).buf, buf-opt0 = none, buf-opt1 = some(fill(some(buf0).buf, zero, m2 % VFS_PAGE_SIZE, n0)), cache_dirs0 = cache_dirs, cache_dirs1 = cache_dirs, cache_dirs2 = cache_dirs, cache_dirs3 = cache_dirs, cache_pcache = truncate(m3, m2, cache_pcache0), err = ESUCCESS, ino = m3, inode0 = mkinode(m3, md, false, # links(m3, cache_dirs), 0, m2), key = datakey(ino, pageno), pageno = m2 / VFS_PAGE_SIZE, pcache = cache_pcache, pe = mkpentry(asynced, buf), some(fill(some(buf0).buf, zero, m2 % VFS_PAGE_SIZE, n0)).some?, some(buf0).some?, afs-cons(cache_dirs, (cache_files ⊕ cache_pcache0) ⊕ cache_icache), afs-cons(cache_dirs, cache_files), dcache-cons(cache_dcache, cache_dirs, cache_files), icache-cons(cache_icache, cache_dirs, cache_files), pcache-cons(cache_pcache0, cache_dirs, cache_files), synced(cache_dirs, cache_icache, cache_pcache0), datakey(m3, m2 / VFS_PAGE_SIZE) ∈ cache_pcache0, m3 ∈ cache_files, m2 ≤ m, m2 % VFS_PAGE_SIZE + n0 ≤ # some(buf0).buf, cache_sync → synced(cache_files, cache_icache, cache_pcache0), ∀ key. key ∈ cache_pcache0 → key.data? ⊦ ⟨afs_truncate#(m, m2 / VFS_PAGE_SIZE; buf-opt0, inode0, asynced5, err0, cache_dirs, afs_files, cache_asynced)⟩ ( cache_dirs = cache_dirs3 ∧ afs_files = ( cache_files [m3, mkfile(m, md, # links(m3, cache_dirs2), content1[m2 / VFS_PAGE_SIZE, fill(buf0, zero, m2 % VFS_PAGE_SIZE, n0)] upto m2) ] ⊕ pcache[key, pe]) ⊕ cache_icache[m3, mkientry(false, mkinode(m3, md, false, # links(m3, cache_dirs0), 0, m))] ∧ ¬ cache_asynced ∧ buf-opt1 = buf-opt0 ∧ (m3 ∈ cache_dirs1 ⊃ mkinode(m3, cache_dirs1[m3].meta, true, cache_dirs1[m3].nlink, cache_dirs1[m3].nsubdirs, cache_dirs1[m3].size) ;mkinode(m3, md, false, # links(m3, cache_dirs1), 0, m) ) = inode0 ∧ (asynced1 ↔ asynced5) ∧ err = err0), m2 % VFS_PAGE_SIZE = 0, VFS_PAGE_SIZE = 0

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 117:
# buf0 = VFS_PAGE_SIZE, VFS_PAGE_SIZE = n0 + m2 % VFS_PAGE_SIZE, ((cache_files ⊕ cache_pcache0) ⊕ cache_icache)[m3] = mkfile(m0, md0, # links(m3, cache_dirs), content0), cache_files[m3] = mkfile(m1, md2, # links(m3, cache_dirs), content1), cache_pcache0[datakey(m3, m2 / VFS_PAGE_SIZE)] = mkpentry(boolvar, buf0), afs_files = (cache_files ⊕ cache_pcache0) ⊕ cache_icache, buf-opt0 = none, cache_dirs0 = cache_dirs, inode0 = mkinode(m3, md, false, # links(m3, cache_dirs), 0, m2), m2 % VFS_PAGE_SIZE ≠ 0, afs-cons(cache_dirs, (cache_files ⊕ cache_pcache0) ⊕ cache_icache), afs-cons(cache_dirs, cache_files), dcache-cons(cache_dcache, cache_dirs, cache_files), icache-cons(cache_icache, cache_dirs, cache_files), pcache-cons(cache_pcache0, cache_dirs, cache_files), synced(cache_dirs, cache_icache, cache_pcache0), datakey(m3, m2 / VFS_PAGE_SIZE) ∈ cache_pcache0, m3 ∈ cache_files, m2 ≤ m, cache_sync → synced(cache_files, cache_icache, cache_pcache0), ∀ key. key ∈ cache_pcache0 → key.data? ⊦ ⟨afs_truncate#(m, m2 / VFS_PAGE_SIZE; buf-opt0, inode0, asynced5, err0, cache_dirs, afs_files, cache_asynced)⟩ ( cache_dirs = cache_dirs0 ∧ afs_files = ( cache_files [m3, mkfile(m, md, # links(m3, cache_dirs0), content1[m2 / VFS_PAGE_SIZE, fill(buf0, zero, m2 % VFS_PAGE_SIZE, n0)] upto m2) ] ⊕ truncate(m3, m2, cache_pcache0)[datakey(m3, m2 / VFS_PAGE_SIZE), mkpentry(false, fill(buf0, zero, m2 % VFS_PAGE_SIZE, n0))]) ⊕ cache_icache[m3, mkientry(false, mkinode(m3, md, false, # links(m3, cache_dirs0), 0, m))] ∧ ¬ cache_asynced ∧ some(fill(buf0, zero, m2 % VFS_PAGE_SIZE, n0)) = buf-opt0 ∧ (m3 ∈ cache_dirs0 ⊃ mkinode(m3, cache_dirs0[m3].meta, true, cache_dirs0[m3].nlink, cache_dirs0[m3].nsubdirs, cache_dirs0[m3].size) ;mkinode(m3, md, false, # links(m3, cache_dirs0), 0, m) ) = inode0 ∧ asynced5 ∧ ESUCCESS = err0)

Rule argument

Additional information

Used simplifier rules: ⊦ m ≤ m; (s)%c: ⊦ m + n = n + m; from specification nat-basic% ⊦ some(buf).some?; (s)% ⊦ some(buf).buf = buf; (s)% ⊦ VFS_PAGE_SIZE ≠ 0; (s)