Proof step 93 from proof refine-read (previous step)

Heuristic symbolic execution applied rule let right

And obtained the following new goals

• Proof step 94:

  files[m3] = mkfile(m1, md, m2, content), of[fd] = mkfile(m3, mode0, m4), err0 = ESUCCESS, f = abs-files(files)[fh.fid], fh = ofh[fd], ofh = abs-of(of), root.dir?, dom of < ino2, abs(root, ROOT_INO)(dirs), afs-cons(dirs, files), fids-cons(root, abs-files(files), abs-of(of)), of-cons(of, dirs, files), of-cons(of[fd, mkfile(m3, mode0, m4 + ino)], dirs, files), read-inv(m4, m4 + n0, mkinode(m3, md, false, m2, 0, m1), buf0, buf0, 0, dirs, files), read-inv(m4, m4 + n0, mkinode(m3, md, false, m2, 0, m1), buf0, buf1, ino, dirs, files), fh.fid ∈ abs-files(files), fd ∈ of, fd ∈ ofh, n0 ≤ # buf0, m4 ≤ m1, psynced → asynced, ⌊err1⌋ ∨ err1 = ESUCCESS ⊦ ⟨choose n with n ≤ n0 ∧ fh.pos + n ≤ # f.content in {n0 := n; buf0 := copy(f.content, fh.pos, buf0, 0, n0); ofh[fd].pos := fh.pos + n0} ifnone n0 := 0⟩ (ofh = abs-of(of[fd, of[fd].pos:= (m4 + n0)]) ∧ (psynced → asynced) ∧ buf1 = buf0 ∧ ino = n0 ∧ ESUCCESS = err0), ino = 0, mode0 ≠ MODE_R ∧ mode0 ≠ MODE_RW

• Proof step 142:

  files[m3] = mkfile(m1, md, m2, content), of[fd] = mkfile(m3, mode0, m4), err0 = ESUCCESS, fh = ofh[fd], ofh = abs-of(of), root.dir?, dom of < ino2, abs(root, ROOT_INO)(dirs), afs-cons(dirs, files), fids-cons(root, abs-files(files), abs-of(of)), of-cons(of, dirs, files), of-cons(of[fd, mkfile(m3, mode0, m4 + ino)], dirs, files), read-inv(m4, m4 + n0, mkinode(m3, md, false, m2, 0, m1), buf0, buf0, 0, dirs, files), read-inv(m4, m4 + n0, mkinode(m3, md, false, m2, 0, m1), buf0, buf1, ino, dirs, files), fd ∈ of, fd ∈ ofh, n0 ≤ # buf0, m4 ≤ m1, psynced → asynced, ⌊err1⌋ ∨ err1 = ESUCCESS ⊦ ino = 0, fh.fid ∈ abs-files(files), mode0 ≠ MODE_R ∧ mode0 ≠ MODE_RW

Rule argument

Additional information