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

VFS_PAGE_SIZE = n0 + m2 % VFS_PAGE_SIZE, cache_files[m1] = mkfile(m3, md1, # links(m1, cache_dirs), content), ((cache_files ⊕ cache_pcache0) ⊕ cache_icache)[m1] = mkfile(m0, md0, # links(m1, cache_dirs), content0), afs_files = (cache_files ⊕ cache_pcache0) ⊕ cache_icache, buf-opt = none, cache_dirs0 = cache_dirs, dirs = cache_dirs, files = afs_files, inode = mkinode(m1, md, false, # links(m1, cache_dirs), 0, m2), n = m, old_ino = 0, pageno = m2 / VFS_PAGE_SIZE, 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), m2 / VFS_PAGE_SIZE ∈ content, m1 ∈ cache_files, m2 ≤ m, cache_sync → synced(cache_files, cache_icache, cache_pcache0), ∀ key. key ∈ cache_pcache0 → key.data? ⊦ ⟨fail#(; ; err); asynced := ?⟩ ( dirs = cache_dirs0 ∧ files = ( cache_files [m1, mkfile (m, md, # links(m1, cache_dirs0), content[m2 / VFS_PAGE_SIZE, fill(content[m2 / VFS_PAGE_SIZE], zero, m2 % VFS_PAGE_SIZE, n0)] upto m2) ] ⊕ truncate(m1, m2, cache_pcache0) [datakey(m1, m2 / VFS_PAGE_SIZE), mkpentry(false, fill(content[m2 / VFS_PAGE_SIZE], zero, m2 % VFS_PAGE_SIZE, n0)) ]) ⊕ cache_icache[m1, mkientry(false, mkinode(m1, md, false, # links(m1, cache_dirs0), 0, m))] ∧ ¬ asynced ∧ some(fill(content[m2 / VFS_PAGE_SIZE], zero, m2 % VFS_PAGE_SIZE, n0)) = buf-opt ∧ (m1 ∈ cache_dirs0 ⊃ mkinode(m1, cache_dirs0[m1].meta, true, cache_dirs0[m1].nlink, cache_dirs0[m1].nsubdirs, cache_dirs0[m1].size) ;mkinode(m1, md, false, # links(m1, cache_dirs0), 0, m) ) = inode ∧ asynced0 ∧ ESUCCESS = err), ⟨let ino = inode.ino, content = files[inode.ino].content, buf = ? in {old_ino := inode.size % VFS_PAGE_SIZE, size := min(n, inode.size); asynced0 := inode.size ≤ n ∧ old_ino ≠ 0 ∧ (pageno ∈ content ∨ buf-opt.some?); if asynced0 then {if buf-opt.some? then buf := buf-opt.buf else buf := files[ino].content[pageno]; buf := fill(buf, zero, old_ino, VFS_PAGE_SIZE - old_ino); content[pageno] := buf; buf-opt := some(buf)}; files[ino].content := content upto size; let new_inode = inode in {new_inode.size := n; afs_inode_sync#(new_inode; dirs, files)}; inode := getinode(inode.ino, dirs, files); err := ESUCCESS}; asynced := ?⟩ ( dirs = cache_dirs0 ∧ files = ( cache_files [m1, mkfile (m, md, # links(m1, cache_dirs0), content[m2 / VFS_PAGE_SIZE, fill(content[m2 / VFS_PAGE_SIZE], zero, m2 % VFS_PAGE_SIZE, n0)] upto m2) ] ⊕ truncate(m1, m2, cache_pcache0) [datakey(m1, m2 / VFS_PAGE_SIZE), mkpentry(false, fill(content[m2 / VFS_PAGE_SIZE], zero, m2 % VFS_PAGE_SIZE, n0)) ]) ⊕ cache_icache[m1, mkientry(false, mkinode(m1, md, false, # links(m1, cache_dirs0), 0, m))] ∧ ¬ asynced ∧ some(fill(content[m2 / VFS_PAGE_SIZE], zero, m2 % VFS_PAGE_SIZE, n0)) = buf-opt ∧ (m1 ∈ cache_dirs0 ⊃ mkinode(m1, cache_dirs0[m1].meta, true, cache_dirs0[m1].nlink, cache_dirs0[m1].nsubdirs, cache_dirs0[m1].size) ;mkinode(m1, md, false, # links(m1, cache_dirs0), 0, m) ) = inode ∧ asynced0 ∧ ESUCCESS = err), m2 % VFS_PAGE_SIZE = 0, VFS_PAGE_SIZE = 0, datakey(m1, m2 / VFS_PAGE_SIZE) ∈ cache_pcache0

Heuristic simplifier applied rule simplifier

And obtained the following new goals

Proof step 118:
VFS_PAGE_SIZE = n0 + m2 % VFS_PAGE_SIZE, cache_files[m1] = mkfile(m3, md1, # links(m1, cache_dirs), content), ((cache_files ⊕ cache_pcache0) ⊕ cache_icache)[m1] = mkfile(m0, md0, # links(m1, cache_dirs), content0), 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), m2 / VFS_PAGE_SIZE ∈ content, m1 ∈ cache_files, m2 ≤ m, ¬ datakey(m1, m2 / VFS_PAGE_SIZE) ∈ cache_pcache0, cache_sync → synced(cache_files, cache_icache, cache_pcache0), ∀ key. key ∈ cache_pcache0 → key.data? ⊦ ⟨let ino = m1, content = content0, buf = ? in {old_ino := m2 % VFS_PAGE_SIZE, size := min(m, m2); asynced0 := m2 ≤ m ∧ old_ino ≠ 0 ∧ m2 / VFS_PAGE_SIZE ∈ content; buf-opt := none; afs_files := (cache_files ⊕ cache_pcache0) ⊕ cache_icache; if asynced0 then {pageno := m2 / VFS_PAGE_SIZE; if buf-opt.some? then buf := buf-opt.buf else buf := afs_files[ino].content[pageno]; buf := fill(buf, zero, old_ino, VFS_PAGE_SIZE - old_ino); content[pageno] := buf; buf-opt := some(buf)}; afs_files[ino].content := content upto size; let new_inode = mkinode(m1, md, false, # links(m1, cache_dirs), 0, m2) in {new_inode.size := m; cache_dirs1 := cache_dirs; cache_dirs2 := cache_dirs; afs_inode_sync#(new_inode; cache_dirs, afs_files)}; inode := (m1 ∈ cache_dirs ⊃ mkinode(m1, cache_dirs[m1].meta, true, cache_dirs[m1].nlink, cache_dirs[m1].nsubdirs, cache_dirs[m1].size) ;mkinode(m1, afs_files[m1].meta, false, afs_files[m1].nlink, 0, afs_files[m1].size) ); err := ESUCCESS}; asynced := ?⟩ ( cache_dirs = cache_dirs2 ∧ afs_files = ( cache_files [m1, mkfile (m, md, # links(m1, cache_dirs2), content[m2 / VFS_PAGE_SIZE, fill(content[m2 / VFS_PAGE_SIZE], zero, m2 % VFS_PAGE_SIZE, n0)] upto m2) ] ⊕ truncate(m1, m2, cache_pcache0) [datakey(m1, m2 / VFS_PAGE_SIZE), mkpentry(false, fill(content[m2 / VFS_PAGE_SIZE], zero, m2 % VFS_PAGE_SIZE, n0)) ]) ⊕ cache_icache[m1, mkientry(false, mkinode(m1, md, false, # links(m1, cache_dirs2), 0, m))] ∧ ¬ asynced ∧ some(fill(content[m2 / VFS_PAGE_SIZE], zero, m2 % VFS_PAGE_SIZE, n0)) = buf-opt ∧ (m1 ∈ cache_dirs2 ⊃ mkinode(m1, cache_dirs2[m1].meta, true, cache_dirs2[m1].nlink, cache_dirs2[m1].nsubdirs, cache_dirs2[m1].size) ;mkinode(m1, md, false, # links(m1, cache_dirs2), 0, m) ) = inode ∧ asynced0 ∧ ESUCCESS = err)

Rule argument

Additional information

Used simplifier rules: ⊦ mkfile(m, md, m0, content).content = content; (s)%⊦ getinode(ino, dirs, files) = (ino ∈ dirs ⊃ mkinode (ino, dirs[ino].meta, true, dirs[ino].nlink, dirs[ino].nsubdirs, dirs[ino].size) ;mkinode (ino, files[ino].meta, false, files[ino].nlink, 0, files[ino].size) ); (s)% ⊦ ¬ none.some?; (s)% ⊦ mkinode(m, md, boolvar, m0, m1, m2).size = m2; (s)% ⊦ mkinode(m, md, boolvar, m0, m1, m2).ino = m; (s)% ⊦ some(buf) ≠ none; (s)% ⊦ VFS_PAGE_SIZE ≠ 0; (s)