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

# buf-opt0.buf = VFS_PAGE_SIZE, VFS_PAGE_SIZE = n1 + 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), afs_files = ((cache_files ⊕ cache_pcache0) ⊕ cache_icache )[m3, mkfile(m0, md0, # links(m3, cache_dirs), content0[m2 / VFS_PAGE_SIZE, fill(buf-opt0.buf, zero, m2 % VFS_PAGE_SIZE, n1)] upto m2) ], cache_dirs2 = cache_dirs, dirs = cache_dirs, files = afs_files, ino = inode.ino, inode = mkinode(m3, md, false, # links(m3, cache_dirs), 0, m), buf-opt0.some?, 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, ino ∈ files, m2 ≤ m, cache_sync → synced(cache_files, cache_icache, cache_pcache0), ∀ key. key ∈ cache_pcache0 → key.data? ⊦ ∃ err0. ⌊err0⌋ ∧ ⟨err := err0; asynced0 := ?⟩ ( (cache_files ⊕ cache_pcache0) ⊕ cache_icache = ( cache_files [m3, mkfile(m, md, # links(m3, cache_dirs), content1[m2 / VFS_PAGE_SIZE, fill(buf-opt0.buf, zero, m2 % VFS_PAGE_SIZE, n1)] upto m2) ] ⊕ truncate(m3, m2, cache_pcache0)[datakey(m3, m2 / VFS_PAGE_SIZE), mkpentry(false, fill(buf-opt0.buf, zero, m2 % VFS_PAGE_SIZE, n1))]) ⊕ cache_icache[m3, mkientry(false, mkinode(m3, md, false, # links(m3, cache_dirs), 0, m))] ∧ (asynced0 ↔ asynced1) ∧ some(fill(buf-opt0.buf, zero, m2 % VFS_PAGE_SIZE, n1)) = buf-opt0 ∧ mkinode(m3, md, false, # links(m3, cache_dirs), 0, m) = mkinode(m3, md, false, # links(m3, cache_dirs), 0, m2) ∧ asynced2 ∧ ESUCCESS = err), m2 % VFS_PAGE_SIZE = 0, ∃ asynced. dirs = cache_dirs2 ∧ files[ino, files[ino].size:= inode.size][ino, files[ino, files[ino].size:= inode.size][ino].meta:= inode.meta] = ( cache_files [m3, mkfile(m, md, # links(m3, cache_dirs2), content1[m2 / VFS_PAGE_SIZE, fill(buf-opt0.buf, zero, m2 % VFS_PAGE_SIZE, n1)] upto m2) ] ⊕ truncate(m3, m2, cache_pcache0)[datakey(m3, m2 / VFS_PAGE_SIZE), mkpentry(false, fill(buf-opt0.buf, zero, m2 % VFS_PAGE_SIZE, n1))]) ⊕ cache_icache[m3, mkientry(false, mkinode(m3, md, false, # links(m3, cache_dirs2), 0, m))] ∧ (asynced ↔ asynced1) ∧ (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) ) = (m3 ∈ dirs ⊃ mkinode(m3, dirs[m3].meta, true, dirs[m3].nlink, dirs[m3].nsubdirs, dirs[m3].size) ;mkinode (m3, files[ino, files[ino].size:= inode.size][ino, files[ino, files[ino].size:= inode.size][ino].meta:= inode.meta][m3].meta, false, files[ino, files[ino].size:= inode.size][ino, files[ino, files[ino].size:= inode.size][ino].meta:= inode.meta][m3].nlink, 0, files[ino, files[ino].size:= inode.size][ino, files[ino, files[ino].size:= inode.size][ino].meta:= inode.meta][m3].size) ) ∧ ESUCCESS = ESUCCESS

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 127:
# buf-opt0.buf = VFS_PAGE_SIZE, VFS_PAGE_SIZE = n1 + m2 % VFS_PAGE_SIZE, 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), m2 % VFS_PAGE_SIZE ≠ 0, ((cache_files ⊕ cache_pcache0) ⊕ cache_icache )[m3, mkfile(m, md, # links(m3, cache_dirs), content0[m2 / VFS_PAGE_SIZE, fill(buf-opt0.buf, zero, m2 % VFS_PAGE_SIZE, n1)] upto m2) ] ≠ ( cache_files [m3, mkfile(m, md, # links(m3, cache_dirs), content1[m2 / VFS_PAGE_SIZE, fill(buf-opt0.buf, zero, m2 % VFS_PAGE_SIZE, n1)] upto m2) ] ⊕ truncate(m3, m2, cache_pcache0)[datakey(m3, m2 / VFS_PAGE_SIZE), mkpentry(false, fill(buf-opt0.buf, zero, m2 % VFS_PAGE_SIZE, n1))]) ⊕ cache_icache[m3, mkientry(false, mkinode(m3, md, false, # links(m3, cache_dirs), 0, m))], buf-opt0.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), m3 ∈ cache_files, m2 ≤ m, cache_sync → synced(cache_files, cache_icache, cache_pcache0), ∀ key. key ∈ cache_pcache0 → key.data? ⊦ ∃ err0. ⌊err0⌋ ∧ ⟨err := err0; asynced0 := ?⟩ ( (cache_files ⊕ cache_pcache0) ⊕ cache_icache = ( cache_files [m3, mkfile(m, md, # links(m3, cache_dirs), content1[m2 / VFS_PAGE_SIZE, fill(buf-opt0.buf, zero, m2 % VFS_PAGE_SIZE, n1)] upto m2) ] ⊕ truncate(m3, m2, cache_pcache0)[datakey(m3, m2 / VFS_PAGE_SIZE), mkpentry(false, fill(buf-opt0.buf, zero, m2 % VFS_PAGE_SIZE, n1))]) ⊕ cache_icache[m3, mkientry(false, mkinode(m3, md, false, # links(m3, cache_dirs), 0, m))] ∧ (asynced0 ↔ asynced1) ∧ some(fill(buf-opt0.buf, zero, m2 % VFS_PAGE_SIZE, n1)) = buf-opt0 ∧ mkinode(m3, md, false, # links(m3, cache_dirs), 0, m) = mkinode(m3, md, false, # links(m3, cache_dirs), 0, m2) ∧ asynced2 ∧ ESUCCESS = err)

Rule argument

Additional information

Used simplifier rules: ⊦ mkfile(m, md, m0, content).size = m; (s)% ⊦ mkfile(m, md, m0, content).nlink = m0; (s)% ⊦ mkfile(m, md, m0, content).meta = md; (s)% ⊦ mkfile(m, md, m0, content).meta:= md0 = mkfile(m, md0, m0, content); (s)% ⊦ mkinode(m, md, boolvar, m0, m1, m2).meta = md; (s)% ⊦ files[ino, af][ino, af0] = files[ino, af0]; (s)% ⊦ mkfile(m, md, m0, content).size:= m1 = mkfile(m1, md, m0, content); (s)% ⊦ mkinode(m, md, boolvar, m0, m1, m2).size = m2; (s)% ⊦ files[ino, af][ino0] = (ino0 = ino ∧ ino ∈ files ⊃ af;files[ino0]); (s)% ⊦ ino ∈ files ⊕ pcache ↔ ino ∈ files; (s)% ⊦ ino ∈ files ⊕ icache ↔ ino ∈ files; (s)% ⊦ ino ∈ files[ino0, af] ↔ ino ∈ files; (s)% ⊦ mkinode(m, md, boolvar, m0, m1, m2).ino = m; (s)