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

files1[m0] = mkfile(m, md0, # links(m0, dirs), content0), files = files1[m0, mkfile(m, md0, # links(m0, dirs), content0 upto m3)], ino = inode.ino, inode = mkinode(m0, md, false, # links(m0, dirs), 0, n), inode0 = mkinode(m0, md, false, # links(m0, dirs), 0, m3), m3 < n, afs-cons(dirs, files1), ino ∈ dirs, m0 ∈ files1 ⊦ [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 = ( files1 [(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 m3) + ( σ⊥ 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 - m3)) ∧ (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 ∧ n = 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 ∧ files1 [(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 ∧ files1 -- (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⌋ ∧ files1 = files ), ino ∈ files, m3 % VFS_PAGE_SIZE ≠ 0 ∧ m3 / VFS_PAGE_SIZE ∈ content0

Heuristic symbolic execution applied rule assign right

And obtained the following new goals

Rule argument

Additional information