[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 2 from proof write-inv-strong-rec (previous step)

files1[ino] = mkfile(m2, md0, m3, content), write-inv(n0, n1, mkinode(ino, md, boolvar, m0, m4, m1), buf, n, dirs, files0, files1), ino ∈ files1, (n0 + n) % VFS_PAGE_SIZE + min(n1 - n0 + n, n2) ≤ VFS_PAGE_SIZE ⊦ write-inv (n0, n1, mkinode(ino, md, boolvar, m0, m4, m1), buf, n + min(n1 - n0 + n, n2), dirs, files0, files1 [ino, mkfile (m2, md0, m3, content[(n0 + n) / VFS_PAGE_SIZE, copy(buf, n, getpage((n0 + n) / VFS_PAGE_SIZE, content), (n0 + n) % VFS_PAGE_SIZE, min(n1 - n0 + n, n2))]) ])

User applied rule insert rewrite lemma

And obtained the following new goals

Proof step 3:
⊦ write-inv(n0, n1, inode, buf, n, dirs, files0, files1) ↔ afs-cons(dirs, files1) ∧ inode.ino ∈ files0 ∧ inode.ino ∈ files1 ∧ files0[inode.ino].size = inode.size ∧ files1[inode.ino].size = files0[inode.ino].size ∧ files1[inode.ino].meta = files0[inode.ino].meta ∧ files1 -- inode.ino = files0 -- inode.ino ∧ n0 + n ≤ n1 ∧ n1 - n0 ≤ # buf ∧ write-inv(n0, n1, buf, n, files0[inode.ino].content, files1[inode.ino].content)
Proof step 4:
files1[ino] = mkfile(m2, md0, m3, content), write-inv(n0, n1, mkinode(ino, md, boolvar, m0, m4, m1), buf, n, dirs, files0, files1), ino ∈ files1, (n0 + n) % VFS_PAGE_SIZE + min(n1 - n0 + n, n2) ≤ VFS_PAGE_SIZE ⊦ afs-cons (dirs, files1 [ino, mkfile (m2, md0, m3, content[(n0 + n) / VFS_PAGE_SIZE, copy(buf, n, getpage((n0 + n) / VFS_PAGE_SIZE, content), (n0 + n) % VFS_PAGE_SIZE, min(n1 - n0 + n, n2))]) ]) ∧ mkinode(ino, md, boolvar, m0, m4, m1).ino ∈ files0 ∧ mkinode(ino, md, boolvar, m0, m4, m1).ino ∈ files1 [ino, mkfile (m2, md0, m3, content[(n0 + n) / VFS_PAGE_SIZE, copy(buf, n, getpage((n0 + n) / VFS_PAGE_SIZE, content), (n0 + n) % VFS_PAGE_SIZE, min(n1 - n0 + n, n2))]) ] ∧ files0[mkinode(ino, md, boolvar, m0, m4, m1).ino].size = mkinode(ino, md, boolvar, m0, m4, m1).size ∧ files1 [ino, mkfile (m2, md0, m3, content[(n0 + n) / VFS_PAGE_SIZE, copy(buf, n, getpage((n0 + n) / VFS_PAGE_SIZE, content), (n0 + n) % VFS_PAGE_SIZE, min(n1 - n0 + n, n2))]) ] [mkinode(ino, md, boolvar, m0, m4, m1).ino ] .size = files0[mkinode(ino, md, boolvar, m0, m4, m1).ino].size ∧ files1 [ino, mkfile (m2, md0, m3, content[(n0 + n) / VFS_PAGE_SIZE, copy(buf, n, getpage((n0 + n) / VFS_PAGE_SIZE, content), (n0 + n) % VFS_PAGE_SIZE, min(n1 - n0 + n, n2))]) ] [mkinode(ino, md, boolvar, m0, m4, m1).ino ] .meta = files0[mkinode(ino, md, boolvar, m0, m4, m1).ino].meta ∧ files1 [ino, mkfile (m2, md0, m3, content[(n0 + n) / VFS_PAGE_SIZE, copy(buf, n, getpage((n0 + n) / VFS_PAGE_SIZE, content), (n0 + n) % VFS_PAGE_SIZE, min(n1 - n0 + n, n2))]) ] -- mkinode(ino, md, boolvar, m0, m4, m1).ino = files0 -- mkinode(ino, md, boolvar, m0, m4, m1).ino ∧ n0 + n + min(n1 - n0 + n, n2) ≤ n1 ∧ n1 - n0 ≤ # buf ∧ write-inv (n0, n1, buf, n + min(n1 - n0 + n, n2), files0[mkinode(ino, md, boolvar, m0, m4, m1).ino].content, files1 [ino, mkfile (m2, md0, m3, content[(n0 + n) / VFS_PAGE_SIZE, copy(buf, n, getpage((n0 + n) / VFS_PAGE_SIZE, content), (n0 + n) % VFS_PAGE_SIZE, min(n1 - n0 + n, n2))]) ] [mkinode(ino, md, boolvar, m0, m4, m1).ino ] .content)

Rule argument

spec: <toplevel> name: write-inv-strong seq: ⊦ write-inv(n0, n1, inode, buf, n, dirs, files0, files1) ↔ afs-cons(dirs, files1) ∧ inode.ino ∈ files0 ∧ inode.ino ∈ files1 ∧ files0[inode.ino].size = inode.size ∧ files1[inode.ino].size = files0[inode.ino].size ∧ files1[inode.ino].meta = files0[inode.ino].meta ∧ files1 -- inode.ino = files0 -- inode.ino ∧ n0 + n ≤ n1 ∧ n1 - n0 ≤ # buf ∧ write-inv (n0, n1, buf, n, files0[inode.ino].content, files1[inode.ino].content) subst: [files1, files0, dirs, n, buf, inode, n1, n0] → [files1 [ino, mkfile (m2, md0, m3, content [(n0 + n) / VFS_PAGE_SIZE, copy (buf, n, getpage((n0 + n) / VFS_PAGE_SIZE, content), (n0 + n) % VFS_PAGE_SIZE, min(n1 - n0 + n, n2)) ]) ], files0, dirs, n + min(n1 - n0 + n, n2), buf, mkinode(ino, md, boolvar, m0, m4, m1), n1, n0] flags: <all paths>

Additional information

Used terms: files1 [ino, mkfile (m2, md0, m3, content [(n0 + n) / VFS_PAGE_SIZE, copy (buf, n, getpage((n0 + n) / VFS_PAGE_SIZE, content), (n0 + n) % VFS_PAGE_SIZE, min(n1 - n0 + n, n2)) ]) ], files0, dirs, n + min(n1 - n0 + n, n2), buf, mkinode(ino, md, boolvar, m0, m4, m1), n1, n0