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

# buf0 = VFS_PAGE_SIZE, asynced0 ↔ m2 ≤ m ∧ old_ino ≠ 0 ∧ m2 / VFS_PAGE_SIZE ∈ content, VFS_PAGE_SIZE = n0 + m2 % VFS_PAGE_SIZE, cache_pcache0[datakey(m3, m2 / VFS_PAGE_SIZE)] = mkpentry(boolvar, buf0), cache_files[m3] = mkfile(m1, md2, # links(m3, cache_dirs), content1), ((cache_files ⊕ cache_pcache0) ⊕ cache_icache)[m3] = mkfile(m0, md0, # links(m3, cache_dirs), content0), afs_files = (cache_files ⊕ cache_pcache0) ⊕ cache_icache, afs_files0 = afs_files[ino, afs_files[ino].content:= (content[pageno, fill(afs_files[ino].content[pageno], zero, old_ino, VFS_PAGE_SIZE - old_ino)] upto size)], asynced0, buf-opt = none, cache_dirs2 = cache_dirs, content = content0, ino = m3, new_inode = mkinode(m3, md, false, # links(m3, cache_dirs), 0, m2), old_ino = m2 % VFS_PAGE_SIZE, pageno = m2 / VFS_PAGE_SIZE, size = min(m, m2), afs-cons(cache_dirs, cache_files), afs-cons(cache_dirs, (cache_files ⊕ cache_pcache0) ⊕ cache_icache), 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), m3 ∈ cache_files, datakey(m3, m2 / VFS_PAGE_SIZE) ∈ cache_pcache0, pageno ∈ afs_files[ino].content, m2 ≤ m, old_ino + (VFS_PAGE_SIZE - old_ino) ≤ # afs_files[ino].content[pageno], VFS_PAGE_SIZE ≥ old_ino, m2 ≤ m → old_ino ≠ 0 → VFS_PAGE_SIZE ≠ 0, cache_sync → synced(cache_files, cache_icache, cache_pcache0), ∀ key. key ∈ cache_pcache0 → key.data? ⊦ ⟨afs_inode_sync#(new_inode.size:= m; cache_dirs, afs_files0); inode := (m3 ∈ cache_dirs ⊃ mkinode(m3, cache_dirs[m3].meta, true, cache_dirs[m3].nlink, cache_dirs[m3].nsubdirs, cache_dirs[m3].size) ;mkinode(m3, afs_files0[m3].meta, false, afs_files0[m3].nlink, 0, afs_files0[m3].size) ); err := ESUCCESS; asynced := ?⟩ ( cache_dirs = cache_dirs2 ∧ afs_files0 = ( 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) ] ⊕ 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_dirs2), 0, m))] ∧ ¬ asynced ∧ some(fill(buf0, zero, m2 % VFS_PAGE_SIZE, n0)) = some(fill(afs_files[ino].content[pageno], zero, old_ino, VFS_PAGE_SIZE - old_ino)) ∧ (m3 ∈ cache_dirs2 ⊃ mkinode(m3, cache_dirs2[m3].meta, true, cache_dirs2[m3].nlink, cache_dirs2[m3].nsubdirs, cache_dirs2[m3].size) ;mkinode(m3, md, false, # links(m3, cache_dirs2), 0, m) ) = inode ∧ asynced0 ∧ ESUCCESS = err), m2 % VFS_PAGE_SIZE = 0, VFS_PAGE_SIZE = 0

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 143:
# buf0 = VFS_PAGE_SIZE, VFS_PAGE_SIZE = n0 + m2 % VFS_PAGE_SIZE, cache_pcache0[datakey(m3, m2 / VFS_PAGE_SIZE)] = mkpentry(boolvar, buf0), cache_files[m3] = mkfile(m1, md2, # links(m3, cache_dirs), content1), ((cache_files ⊕ cache_pcache0) ⊕ cache_icache)[m3] = mkfile(m0, md0, # links(m3, cache_dirs), content0), afs_files0 = ((cache_files ⊕ cache_pcache0) ⊕ cache_icache )[m3, mkfile (m0, md0, # links(m3, cache_dirs), 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) ], cache_dirs2 = cache_dirs, m2 % VFS_PAGE_SIZE ≠ 0, afs-cons(cache_dirs, cache_files), afs-cons(cache_dirs, (cache_files ⊕ cache_pcache0) ⊕ cache_icache), 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), m3 ∈ cache_files, datakey(m3, m2 / VFS_PAGE_SIZE) ∈ cache_pcache0, m2 / VFS_PAGE_SIZE ∈ content0, m2 ≤ m, VFS_PAGE_SIZE ≤ # content0[m2 / VFS_PAGE_SIZE], cache_sync → synced(cache_files, cache_icache, cache_pcache0), ∀ key. key ∈ cache_pcache0 → key.data? ⊦ ⟨afs_inode_sync#(mkinode(m3, md, false, # links(m3, cache_dirs), 0, m); cache_dirs, afs_files0); inode := (m3 ∈ cache_dirs ⊃ mkinode(m3, cache_dirs[m3].meta, true, cache_dirs[m3].nlink, cache_dirs[m3].nsubdirs, cache_dirs[m3].size) ;mkinode(m3, afs_files0[m3].meta, false, afs_files0[m3].nlink, 0, afs_files0[m3].size) ); err := ESUCCESS; asynced := ?⟩ ( cache_dirs = cache_dirs2 ∧ afs_files0 = ( 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) ] ⊕ 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_dirs2), 0, m))] ∧ ¬ asynced ∧ fill(buf0, zero, m2 % VFS_PAGE_SIZE, n0) = fill (((cache_files ⊕ cache_pcache0) ⊕ cache_icache)[m3].content[m2 / VFS_PAGE_SIZE], zero, m2 % VFS_PAGE_SIZE, VFS_PAGE_SIZE - m2 % VFS_PAGE_SIZE) ∧ (m3 ∈ cache_dirs2 ⊃ mkinode(m3, cache_dirs2[m3].meta, true, cache_dirs2[m3].nlink, cache_dirs2[m3].nsubdirs, cache_dirs2[m3].size) ;mkinode(m3, md, false, # links(m3, cache_dirs2), 0, m) ) = inode ∧ ESUCCESS = err)

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)% ⊦ some(buf) = some(buf0) ↔ buf = buf0; (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)