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

# buf-opt0.buf = VFS_PAGE_SIZE, VFS_PAGE_SIZE = n1 + m2 % VFS_PAGE_SIZE, cache_icache[m3, mkientry(false, mkinode(m3, md, false, # links(m3, cache_dirs), 0, m))][ino] = mkientry(boolvar2, mkinode(m0, md0, boolvar1, m8, m9, m10)), cache_files[m3] = mkfile(m1, md2, # links(m3, cache_dirs), content1), (∅)[m3] = mkientry(boolvar0, mkinode(m4, md1, boolvar, m5, m6, m7)), 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 ∈ cache_files, m2 ≤ m, cache_sync → synced(cache_files, cache_icache, cache_pcache0), ∀ key. key ∈ cache_pcache0 → key.data? ⊦ m2 % VFS_PAGE_SIZE = 0, (ino = m3 ⊃ mkfile (m, md, # links(m3, cache_dirs), (content1 ⊕ mkcontent(m3, cache_pcache0))[m2 / VFS_PAGE_SIZE, fill(buf-opt0.buf, zero, m2 % VFS_PAGE_SIZE, n1)] upto m2) ;((cache_files ⊕ cache_pcache0) ⊕ cache_icache)[ino] ) = ( ( 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))] )[ino ], m3 ∈ cache_icache, ino ∈ cache_icache[m3, mkientry(false, mkinode(m3, md, false, # links(m3, cache_dirs), 0, m))] ∧ ¬ boolvar1

Heuristic use patterns applied rule insert rewrite lemma

And obtained the following new goals

Proof step 150:
⊦ ino ∈ icache ∧ icache[ino].inode.directory → (files ⊕ icache)[ino] = files[ino]
Proof step 151:
# buf-opt0.buf = VFS_PAGE_SIZE, VFS_PAGE_SIZE = n1 + m2 % VFS_PAGE_SIZE, (∅)[m3] = mkientry(boolvar0, mkinode(m4, md1, boolvar, m5, m6, m7)), cache_files[m3] = mkfile(m1, md2, # links(m3, cache_dirs), content1), cache_icache[m3, mkientry(false, mkinode(m3, md, false, # links(m3, cache_dirs), 0, m))][ino] = mkientry(boolvar2, mkinode(m0, md0, boolvar1, m8, m9, m10)), 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), ino ∈ cache_files, m3 ∈ cache_files, m2 ≤ m, cache_sync → synced(cache_files, cache_icache, cache_pcache0), ∀ key. key ∈ cache_pcache0 → key.data? ⊦ m2 % VFS_PAGE_SIZE = 0, (ino = m3 ⊃ mkfile (m, md, # links(m3, cache_dirs), (content1 ⊕ mkcontent(m3, cache_pcache0))[m2 / VFS_PAGE_SIZE, fill(buf-opt0.buf, zero, m2 % VFS_PAGE_SIZE, n1)] upto m2) ;((cache_files ⊕ cache_pcache0) ⊕ cache_icache)[ino] ) = ( ( 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))] )[ino ], m3 ∈ cache_icache, ino ∈ cache_icache[m3, mkientry(false, mkinode(m3, md, false, # links(m3, cache_dirs), 0, m))] ∧ ¬ boolvar1, ino ∈ cache_icache[m3, mkientry(false, mkinode(m3, md, false, # links(m3, cache_dirs), 0, m))] ∧ cache_icache[m3, mkientry(false, mkinode(m3, md, false, # links(m3, cache_dirs), 0, m))][ino].inode.directory
Proof step 193:
# buf-opt0.buf = VFS_PAGE_SIZE, VFS_PAGE_SIZE = n1 + m2 % VFS_PAGE_SIZE, (∅)[m3] = mkientry(boolvar0, mkinode(m4, md1, boolvar, m5, m6, m7)), cache_files[m3] = mkfile(m1, md2, # links(m3, cache_dirs), content1), cache_icache[m3, mkientry(false, mkinode(m3, md, false, # links(m3, cache_dirs), 0, m))][ino] = mkientry(boolvar2, mkinode(m0, md0, boolvar1, m8, m9, m10)), cache_icache[m3, mkientry(false, mkinode(m3, md, false, # links(m3, cache_dirs), 0, m))][ino].inode.directory, 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), ino ∈ cache_files, m3 ∈ cache_files, ino ∈ cache_icache[m3, mkientry(false, mkinode(m3, md, false, # links(m3, cache_dirs), 0, m))], m2 ≤ m, cache_sync → synced(cache_files, cache_icache, cache_pcache0), ∀ key. key ∈ cache_pcache0 → key.data? ⊦ m2 % VFS_PAGE_SIZE = 0, (ino = m3 ⊃ mkfile (m, md, # links(m3, cache_dirs), (content1 ⊕ mkcontent(m3, cache_pcache0))[m2 / VFS_PAGE_SIZE, fill(buf-opt0.buf, zero, m2 % VFS_PAGE_SIZE, n1)] upto m2) ;((cache_files ⊕ cache_pcache0) ⊕ cache_icache)[ino] ) = ( 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))] )[ino ], m3 ∈ cache_icache, ino ∈ cache_icache[m3, mkientry(false, mkinode(m3, md, false, # links(m3, cache_dirs), 0, m))] ∧ ¬ boolvar1

Rule argument

spec: cache-base name: at-icache-overwrite-no-file seq: ⊦ ino ∈ icache ∧ icache[ino].inode.directory → (files ⊕ icache)[ino] = files[ino] subst: [ino, icache, files] → [ino, cache_icache [m3, mkientry (false, mkinode(m3, md, false, # links(m3, cache_dirs), 0, m)) ], 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)) ]] flags: <all paths>

Additional information

Used terms: ino, cache_icache [m3, mkientry (false, mkinode(m3, md, false, # links(m3, cache_dirs), 0, m)) ], 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)) ]