[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 59 from proof truncate-smaller (previous step)

VFS_PAGE_SIZE = n0 + m2 % VFS_PAGE_SIZE, files0[m] = mkfile(m0, md0, # links(m, dirs), content0), files = files1, files1 = files0 [m, mkfile(m0, md0, # links(m, dirs), content0[m2 / VFS_PAGE_SIZE, fill(content0[m2 / VFS_PAGE_SIZE], zero, m2 % VFS_PAGE_SIZE, n0)] upto m2) ], ino = inode.ino, inode = mkinode(m, md, false, # links(m, dirs), 0, m2), inode0 = mkinode(m, md, false, # links(m, dirs), 0, m2), afs-cons(dirs, files0), ino ∈ dirs, m ∈ files0, m2 / VFS_PAGE_SIZE ∈ content0 ⊦ [err := ESUCCESS; asynced := ?] (err = ESUCCESS ⊃ files [(inode0.ino ∈ dirs[ino, dirs[ino].meta:= inode.meta] ⊃ mkinode (inode0.ino, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].meta, true, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].nlink, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].nsubdirs, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].size) ;mkinode(inode0.ino, files[inode0.ino].meta, false, files[inode0.ino].nlink, 0, files[inode0.ino].size) ) .ino ] .content .stream to files [(inode0.ino ∈ dirs[ino, dirs[ino].meta:= inode.meta] ⊃ mkinode (inode0.ino, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].meta, true, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].nlink, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].nsubdirs, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].size) ;mkinode(inode0.ino, files[inode0.ino].meta, false, files[inode0.ino].nlink, 0, files[inode0.ino].size) ) .ino ] .size = files0 [(inode0.ino ∈ dirs[ino, dirs[ino].meta:= inode.meta] ⊃ mkinode (inode0.ino, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].meta, true, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].nlink, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].nsubdirs, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].size) ;mkinode(inode0.ino, files[inode0.ino].meta, false, files[inode0.ino].nlink, 0, files[inode0.ino].size) ) .ino ] .content .stream to files [(inode0.ino ∈ dirs[ino, dirs[ino].meta:= inode.meta] ⊃ mkinode (inode0.ino, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].meta, true, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].nlink, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].nsubdirs, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].size) ;mkinode(inode0.ino, files[inode0.ino].meta, false, files[inode0.ino].nlink, 0, files[inode0.ino].size) ) .ino ] .size ∧ (inode0.ino ∈ dirs[ino, dirs[ino].meta:= inode.meta] ⊃ mkinode (inode0.ino, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].meta, true, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].nlink, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].nsubdirs, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].size) ;mkinode(inode0.ino, files[inode0.ino].meta, false, files[inode0.ino].nlink, 0, files[inode0.ino].size) ) .ino ∈ files ∧ m2 = files [(inode0.ino ∈ dirs[ino, dirs[ino].meta:= inode.meta] ⊃ mkinode (inode0.ino, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].meta, true, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].nlink, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].nsubdirs, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].size) ;mkinode(inode0.ino, files[inode0.ino].meta, false, files[inode0.ino].nlink, 0, files[inode0.ino].size) ) .ino ] .size ∧ files0 [(inode0.ino ∈ dirs[ino, dirs[ino].meta:= inode.meta] ⊃ mkinode (inode0.ino, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].meta, true, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].nlink, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].nsubdirs, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].size) ;mkinode(inode0.ino, files[inode0.ino].meta, false, files[inode0.ino].nlink, 0, files[inode0.ino].size) ) .ino ] .nlink = files [(inode0.ino ∈ dirs[ino, dirs[ino].meta:= inode.meta] ⊃ mkinode (inode0.ino, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].meta, true, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].nlink, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].nsubdirs, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].size) ;mkinode(inode0.ino, files[inode0.ino].meta, false, files[inode0.ino].nlink, 0, files[inode0.ino].size) ) .ino ] .nlink ∧ files0 -- (inode0.ino ∈ dirs[ino, dirs[ino].meta:= inode.meta] ⊃ mkinode (inode0.ino, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].meta, true, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].nlink, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].nsubdirs, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].size) ;mkinode(inode0.ino, files[inode0.ino].meta, false, files[inode0.ino].nlink, 0, files[inode0.ino].size) ) .ino = files -- (inode0.ino ∈ dirs[ino, dirs[ino].meta:= inode.meta] ⊃ mkinode (inode0.ino, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].meta, true, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].nlink, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].nsubdirs, dirs[ino, dirs[ino].meta:= inode.meta][inode0.ino].size) ;mkinode(inode0.ino, files[inode0.ino].meta, false, files[inode0.ino].nlink, 0, files[inode0.ino].size) ) .ino ;⌊err⌋ ∧ files0 = files ), m2 % VFS_PAGE_SIZE = 0, ino ∈ files

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

Rule argument

Additional information