This is a listing of all goals defined over the current specification. Axioms are yellow, proof obligations purple and theorems green. Click on individual names to get more information on the proof.
| Name: | Sequent: | Type: |
|---|---|---|
| case | ⊦ posix-event = mkdir(posix-event.path, posix-event.meta, posix-event.err) ∨ posix-event = rmdir(posix-event.path, posix-event.err) ∨ posix-event = create(posix-event.path, posix-event.meta, posix-event.err) ∨ posix-event = unlink(posix-event.path, posix-event.err) ∨ posix-event = renam(posix-event.path, posix-event.path', posix-event.err) ∨ posix-event = link(posix-event.path, posix-event.path', posix-event.err) ∨ posix-event = open(posix-event.path, posix-event.fd, posix-event.mode, posix-event.err) ∨ posix-event = close(posix-event.fd, posix-event.err) ∨ posix-event = read(posix-event.fd, posix-event.buf, posix-event.n, posix-event.err) ∨ posix-event = write(posix-event.fd, posix-event.buf, posix-event.n, posix-event.err) ∨ posix-event = seek(posix-event.fd, posix-event.n, posix-event.whence, posix-event.err) ∨ posix-event = readmeta(posix-event.path, posix-event.meta, posix-event.err) ∨ posix-event = writemeta(posix-event.path, posix-event.meta, posix-event.err) ∨ posix-event = readdir(posix-event.path, posix-event.names, posix-event.err) ∨ posix-event = truncate(posix-event.path, posix-event.n, posix-event.err) ∨ posix-event = crash | An Axiom |
| gen | An Axiom | |
| inj-16 | ⊦ mkdir(p, md, err) = mkdir(p0, md0, err0) ↔ p = p0 ∧ md = md0 ∧ err = err0 | An Axiom |
| inj-17 | ⊦ rmdir(p, err) = rmdir(p0, err0) ↔ p = p0 ∧ err = err0 | An Axiom |
| inj-18 | ⊦ truncate(p, m, err) = truncate(p0, m0, err0) ↔ p = p0 ∧ m = m0 ∧ err = err0 | An Axiom |
| inj-19 | ⊦ create(p, md, err) = create(p0, md0, err0) ↔ p = p0 ∧ md = md0 ∧ err = err0 | An Axiom |
| inj-20 | ⊦ readdir(p, strings, err) = readdir(p0, strings0, err0) ↔ p = p0 ∧ strings = strings0 ∧ err = err0 | An Axiom |
| inj-21 | ⊦ unlink(p, err) = unlink(p0, err0) ↔ p = p0 ∧ err = err0 | An Axiom |
| inj-22 | ⊦ writemeta(p, md, err) = writemeta(p0, md0, err0) ↔ p = p0 ∧ md = md0 ∧ err = err0 | An Axiom |
| inj-23 | ⊦ renam(p, p0, err) = renam(p1, p2, err0) ↔ p = p1 ∧ p0 = p2 ∧ err = err0 | An Axiom |
| inj-24 | ⊦ readmeta(p, md, err) = readmeta(p0, md0, err0) ↔ p = p0 ∧ md = md0 ∧ err = err0 | An Axiom |
| inj-25 | ⊦ link(p, p0, err) = link(p1, p2, err0) ↔ p = p1 ∧ p0 = p2 ∧ err = err0 | An Axiom |
| inj-26 | ⊦ seek(m, m0, whence, err) = seek(m1, m2, whence0, err0) ↔ m = m1 ∧ m0 = m2 ∧ whence = whence0 ∧ err = err0 | An Axiom |
| inj-27 | ⊦ open(p, m, mode, err) = open(p0, m0, mode0, err0) ↔ p = p0 ∧ m = m0 ∧ mode = mode0 ∧ err = err0 | An Axiom |
| inj-28 | ⊦ write(m, buf, m0, err) = write(m1, buf0, m2, err0) ↔ m = m1 ∧ buf = buf0 ∧ m0 = m2 ∧ err = err0 | An Axiom |
| inj-29 | ⊦ close(m, err) = close(m0, err0) ↔ m = m0 ∧ err = err0 | An Axiom |
| inj-30 | ⊦ read(m, buf, m0, err) = read(m1, buf0, m2, err0) ↔ m = m1 ∧ buf = buf0 ∧ m0 = m2 ∧ err = err0 | An Axiom |
| sel-32 | ⊦ truncate(p, m, err).err = err | An Axiom |
| sel-33 | ⊦ mkdir(p, md, err).path = p | An Axiom |
| sel-34 | ⊦ truncate(p, m, err).n = m | An Axiom |
| sel-35 | ⊦ mkdir(p, md, err).meta = md | An Axiom |
| sel-36 | ⊦ truncate(p, m, err).path = p | An Axiom |
| sel-37 | ⊦ mkdir(p, md, err).err = err | An Axiom |
| sel-38 | ⊦ readdir(p, strings, err).err = err | An Axiom |
| sel-39 | ⊦ rmdir(p, err).path = p | An Axiom |
| sel-40 | ⊦ readdir(p, strings, err).names = strings | An Axiom |
| sel-41 | ⊦ rmdir(p, err).err = err | An Axiom |
| sel-42 | ⊦ readdir(p, strings, err).path = p | An Axiom |
| sel-43 | ⊦ create(p, md, err).path = p | An Axiom |
| sel-44 | ⊦ writemeta(p, md, err).err = err | An Axiom |
| sel-45 | ⊦ create(p, md, err).meta = md | An Axiom |
| sel-46 | ⊦ writemeta(p, md, err).meta = md | An Axiom |
| sel-47 | ⊦ create(p, md, err).err = err | An Axiom |
| sel-48 | ⊦ writemeta(p, md, err).path = p | An Axiom |
| sel-49 | ⊦ unlink(p, err).path = p | An Axiom |
| sel-50 | ⊦ readmeta(p, md, err).err = err | An Axiom |
| sel-51 | ⊦ unlink(p, err).err = err | An Axiom |
| sel-52 | ⊦ readmeta(p, md, err).path = p | An Axiom |
| sel-53 | ⊦ renam(p, p0, err).path = p | An Axiom |
| sel-54 | ⊦ readmeta(p, md, err).meta = md | An Axiom |
| sel-55 | ⊦ renam(p, p0, err).path' = p0 | An Axiom |
| sel-56 | ⊦ seek(m, m0, whence, err).err = err | An Axiom |
| sel-57 | ⊦ renam(p, p0, err).err = err | An Axiom |
| sel-58 | ⊦ seek(m, m0, whence, err).whence = whence | An Axiom |
| sel-59 | ⊦ link(p, p0, err).path = p | An Axiom |
| sel-60 | ⊦ seek(m, m0, whence, err).n = m0 | An Axiom |
| sel-61 | ⊦ link(p, p0, err).path' = p0 | An Axiom |
| sel-62 | ⊦ seek(m, m0, whence, err).fd = m | An Axiom |
| sel-63 | ⊦ link(p, p0, err).err = err | An Axiom |
| sel-64 | ⊦ write(m, buf, m0, err).err = err | An Axiom |
| sel-65 | ⊦ open(p, m, mode, err).path = p | An Axiom |
| sel-66 | ⊦ write(m, buf, m0, err).n = m0 | An Axiom |
| sel-67 | ⊦ open(p, m, mode, err).fd = m | An Axiom |
| sel-68 | ⊦ write(m, buf, m0, err).buf = buf | An Axiom |
| sel-69 | ⊦ open(p, m, mode, err).mode = mode | An Axiom |
| sel-70 | ⊦ write(m, buf, m0, err).fd = m | An Axiom |
| sel-71 | ⊦ open(p, m, mode, err).err = err | An Axiom |
| sel-72 | ⊦ read(m, buf, m0, err).err = err | An Axiom |
| sel-73 | ⊦ close(m, err).fd = m | An Axiom |
| sel-74 | ⊦ read(m, buf, m0, err).n = m0 | An Axiom |
| sel-75 | ⊦ close(m, err).err = err | An Axiom |
| sel-76 | ⊦ read(m, buf, m0, err).buf = buf | An Axiom |
| sel-77 | ⊦ read(m, buf, m0, err).fd = m | An Axiom |
| disj-106 | ⊦ mkdir(p, md, err) ≠ rmdir(p0, err0) | An Axiom |
| disj-107 | ⊦ readdir(p, strings, err) ≠ truncate(p0, m, err0) | An Axiom |
| disj-108 | ⊦ mkdir(p, md, err) ≠ create(p0, md0, err0) | An Axiom |
| disj-109 | ⊦ writemeta(p, md, err) ≠ truncate(p0, m, err0) | An Axiom |
| disj-110 | ⊦ mkdir(p, md, err) ≠ unlink(p0, err0) | An Axiom |
| disj-111 | ⊦ writemeta(p, md, err) ≠ readdir(p0, strings, err0) | An Axiom |
| disj-112 | ⊦ mkdir(p, md, err) ≠ renam(p0, p1, err0) | An Axiom |
| disj-113 | ⊦ mkdir(p, md, err) ≠ readmeta(p0, md0, err0) | An Axiom |
| disj-114 | ⊦ mkdir(p, md, err) ≠ link(p0, p1, err0) | An Axiom |
| disj-115 | ⊦ readmeta(p, md, err) ≠ truncate(p0, m, err0) | An Axiom |
| disj-116 | ⊦ mkdir(p, md, err) ≠ open(p0, m, mode, err0) | An Axiom |
| disj-117 | ⊦ rmdir(p, err) ≠ readmeta(p0, md, err0) | An Axiom |
| disj-118 | ⊦ mkdir(p, md, err) ≠ close(m, err0) | An Axiom |
| disj-119 | ⊦ seek(m, m0, whence, err) ≠ truncate(p, m1, err0) | An Axiom |
| disj-120 | ⊦ mkdir(p, md, err) ≠ read(m, buf, m0, err0) | An Axiom |
| disj-121 | ⊦ seek(m, m0, whence, err) ≠ readdir(p, strings, err0) | An Axiom |
| disj-122 | ⊦ mkdir(p, md, err) ≠ write(m, buf, m0, err0) | An Axiom |
| disj-123 | ⊦ seek(m, m0, whence, err) ≠ writemeta(p, md, err0) | An Axiom |
| disj-124 | ⊦ mkdir(p, md, err) ≠ seek(m, m0, whence, err0) | An Axiom |
| disj-125 | ⊦ readmeta(p, md, err) ≠ readdir(p0, strings, err0) | An Axiom |
| disj-126 | ⊦ create(p, md, err) ≠ readmeta(p0, md0, err0) | An Axiom |
| disj-127 | ⊦ write(m, buf, m0, err) ≠ truncate(p, m1, err0) | An Axiom |
| disj-128 | ⊦ mkdir(p, md, err) ≠ writemeta(p0, md0, err0) | An Axiom |
| disj-129 | ⊦ write(m, buf, m0, err) ≠ readdir(p, strings, err0) | An Axiom |
| disj-130 | ⊦ mkdir(p, md, err) ≠ readdir(p0, strings, err0) | An Axiom |
| disj-131 | ⊦ write(m, buf, m0, err) ≠ writemeta(p, md, err0) | An Axiom |
| disj-132 | ⊦ mkdir(p, md, err) ≠ truncate(p0, m, err0) | An Axiom |
| disj-133 | ⊦ readmeta(p, md, err) ≠ writemeta(p0, md0, err0) | An Axiom |
| disj-134 | ⊦ rmdir(p, err) ≠ create(p0, md, err0) | An Axiom |
| disj-135 | ⊦ write(m, buf, m0, err) ≠ seek(m1, m2, whence, err0) | An Axiom |
| disj-136 | ⊦ rmdir(p, err) ≠ unlink(p0, err0) | An Axiom |
| disj-137 | ⊦ read(m, buf, m0, err) ≠ truncate(p, m1, err0) | An Axiom |
| disj-138 | ⊦ rmdir(p, err) ≠ renam(p0, p1, err0) | An Axiom |
| disj-139 | ⊦ read(m, buf, m0, err) ≠ readdir(p, strings, err0) | An Axiom |
| disj-140 | ⊦ rmdir(p, err) ≠ link(p0, p1, err0) | An Axiom |
| disj-141 | ⊦ read(m, buf, m0, err) ≠ writemeta(p, md, err0) | An Axiom |
| disj-142 | ⊦ rmdir(p, err) ≠ open(p0, m, mode, err0) | An Axiom |
| disj-143 | ⊦ unlink(p, err) ≠ readmeta(p0, md, err0) | An Axiom |
| disj-144 | ⊦ rmdir(p, err) ≠ close(m, err0) | An Axiom |
| disj-145 | ⊦ read(m, buf, m0, err) ≠ seek(m1, m2, whence, err0) | An Axiom |
| disj-146 | ⊦ rmdir(p, err) ≠ read(m, buf, m0, err0) | An Axiom |
| disj-147 | ⊦ read(m, buf, m0, err) ≠ write(m1, buf0, m2, err0) | An Axiom |
| disj-148 | ⊦ rmdir(p, err) ≠ write(m, buf, m0, err0) | An Axiom |
| disj-149 | ⊦ close(m, err) ≠ truncate(p, m0, err0) | An Axiom |
| disj-150 | ⊦ rmdir(p, err) ≠ seek(m, m0, whence, err0) | An Axiom |
| disj-151 | ⊦ close(m, err) ≠ readdir(p, strings, err0) | An Axiom |
| disj-152 | ⊦ seek(m, m0, whence, err) ≠ readmeta(p, md, err0) | An Axiom |
| disj-153 | ⊦ close(m, err) ≠ writemeta(p, md, err0) | An Axiom |
| disj-154 | ⊦ rmdir(p, err) ≠ writemeta(p0, md, err0) | An Axiom |
| disj-155 | ⊦ renam(p, p0, err) ≠ readmeta(p1, md, err0) | An Axiom |
| disj-156 | ⊦ rmdir(p, err) ≠ readdir(p0, strings, err0) | An Axiom |
| disj-157 | ⊦ close(m, err) ≠ seek(m0, m1, whence, err0) | An Axiom |
| disj-158 | ⊦ rmdir(p, err) ≠ truncate(p0, m, err0) | An Axiom |
| disj-159 | ⊦ close(m, err) ≠ write(m0, buf, m1, err0) | An Axiom |
| disj-160 | ⊦ create(p, md, err) ≠ unlink(p0, err0) | An Axiom |
| disj-161 | ⊦ close(m, err) ≠ read(m0, buf, m1, err0) | An Axiom |
| disj-162 | ⊦ create(p, md, err) ≠ renam(p0, p1, err0) | An Axiom |
| disj-163 | ⊦ open(p, m, mode, err) ≠ truncate(p0, m0, err0) | An Axiom |
| disj-164 | ⊦ create(p, md, err) ≠ link(p0, p1, err0) | An Axiom |
| disj-165 | ⊦ open(p, m, mode, err) ≠ readdir(p0, strings, err0) | An Axiom |
| disj-166 | ⊦ create(p, md, err) ≠ open(p0, m, mode, err0) | An Axiom |
| disj-167 | ⊦ open(p, m, mode, err) ≠ writemeta(p0, md, err0) | An Axiom |
| disj-168 | ⊦ create(p, md, err) ≠ close(m, err0) | An Axiom |
| disj-169 | ⊦ write(m, buf, m0, err) ≠ readmeta(p, md, err0) | An Axiom |
| disj-170 | ⊦ create(p, md, err) ≠ read(m, buf, m0, err0) | An Axiom |
| disj-171 | ⊦ open(p, m, mode, err) ≠ seek(m0, m1, whence, err0) | An Axiom |
| disj-172 | ⊦ create(p, md, err) ≠ write(m, buf, m0, err0) | An Axiom |
| disj-173 | ⊦ open(p, m, mode, err) ≠ write(m0, buf, m1, err0) | An Axiom |
| disj-174 | ⊦ create(p, md, err) ≠ seek(m, m0, whence, err0) | An Axiom |
| disj-175 | ⊦ open(p, m, mode, err) ≠ read(m0, buf, m1, err0) | An Axiom |
| disj-176 | ⊦ link(p, p0, err) ≠ readmeta(p1, md, err0) | An Axiom |
| disj-177 | ⊦ open(p, m, mode, err) ≠ close(m0, err0) | An Axiom |
| disj-178 | ⊦ create(p, md, err) ≠ writemeta(p0, md0, err0) | An Axiom |
| disj-179 | ⊦ link(p, p0, err) ≠ truncate(p1, m, err0) | An Axiom |
| disj-180 | ⊦ create(p, md, err) ≠ readdir(p0, strings, err0) | An Axiom |
| disj-181 | ⊦ link(p, p0, err) ≠ readdir(p1, strings, err0) | An Axiom |
| disj-182 | ⊦ create(p, md, err) ≠ truncate(p0, m, err0) | An Axiom |
| disj-183 | ⊦ link(p, p0, err) ≠ writemeta(p1, md, err0) | An Axiom |
| disj-184 | ⊦ unlink(p, err) ≠ renam(p0, p1, err0) | An Axiom |
| disj-185 | ⊦ read(m, buf, m0, err) ≠ readmeta(p, md, err0) | An Axiom |
| disj-186 | ⊦ unlink(p, err) ≠ link(p0, p1, err0) | An Axiom |
| disj-187 | ⊦ link(p, p0, err) ≠ seek(m, m0, whence, err0) | An Axiom |
| disj-188 | ⊦ unlink(p, err) ≠ open(p0, m, mode, err0) | An Axiom |
| disj-189 | ⊦ link(p, p0, err) ≠ write(m, buf, m0, err0) | An Axiom |
| disj-190 | ⊦ unlink(p, err) ≠ close(m, err0) | An Axiom |
| disj-191 | ⊦ link(p, p0, err) ≠ read(m, buf, m0, err0) | An Axiom |
| disj-192 | ⊦ unlink(p, err) ≠ read(m, buf, m0, err0) | An Axiom |
| disj-193 | ⊦ link(p, p0, err) ≠ close(m, err0) | An Axiom |
| disj-194 | ⊦ unlink(p, err) ≠ write(m, buf, m0, err0) | An Axiom |
| disj-195 | ⊦ link(p, p0, err) ≠ open(p1, m, mode, err0) | An Axiom |
| disj-196 | ⊦ unlink(p, err) ≠ seek(m, m0, whence, err0) | An Axiom |
| disj-197 | ⊦ renam(p, p0, err) ≠ truncate(p1, m, err0) | An Axiom |
| disj-198 | ⊦ open(p, m, mode, err) ≠ readmeta(p0, md, err0) | An Axiom |
| disj-199 | ⊦ renam(p, p0, err) ≠ readdir(p1, strings, err0) | An Axiom |
| disj-200 | ⊦ unlink(p, err) ≠ writemeta(p0, md, err0) | An Axiom |
| disj-201 | ⊦ renam(p, p0, err) ≠ writemeta(p1, md, err0) | An Axiom |
| disj-202 | ⊦ unlink(p, err) ≠ readdir(p0, strings, err0) | An Axiom |
| disj-203 | ⊦ close(m, err) ≠ readmeta(p, md, err0) | An Axiom |
| disj-204 | ⊦ unlink(p, err) ≠ truncate(p0, m, err0) | An Axiom |
| disj-205 | ⊦ renam(p, p0, err) ≠ seek(m, m0, whence, err0) | An Axiom |
| disj-206 | ⊦ renam(p, p0, err) ≠ link(p1, p2, err0) | An Axiom |
| disj-207 | ⊦ renam(p, p0, err) ≠ write(m, buf, m0, err0) | An Axiom |
| disj-208 | ⊦ renam(p, p0, err) ≠ open(p1, m, mode, err0) | An Axiom |
| disj-209 | ⊦ renam(p, p0, err) ≠ read(m, buf, m0, err0) | An Axiom |
| disj-210 | ⊦ renam(p, p0, err) ≠ close(m, err0) | An Axiom |
| disj-01 | ⊦ truncate(p, m, err) ≠ crash | An Axiom |
| disj-02 | ⊦ readdir(p, strings, err) ≠ crash | An Axiom |
| disj-03 | ⊦ writemeta(p, md, err) ≠ crash | An Axiom |
| disj-04 | ⊦ readmeta(p, md, err) ≠ crash | An Axiom |
| disj-05 | ⊦ seek(m, m0, whence, err) ≠ crash | An Axiom |
| disj-06 | ⊦ write(m, buf, m0, err) ≠ crash | An Axiom |
| disj-07 | ⊦ read(m, buf, m0, err) ≠ crash | An Axiom |
| disj-08 | ⊦ close(m, err) ≠ crash | An Axiom |
| disj-09 | ⊦ open(p, m, mode, err) ≠ crash | An Axiom |
| disj-10 | ⊦ link(p, p0, err) ≠ crash | An Axiom |
| disj-11 | ⊦ renam(p, p0, err) ≠ crash | An Axiom |
| disj-12 | ⊦ unlink(p, err) ≠ crash | An Axiom |
| disj-13 | ⊦ create(p, md, err) ≠ crash | An Axiom |
| disj-14 | ⊦ rmdir(p, err) ≠ crash | An Axiom |
| disj-15 | ⊦ mkdir(p, md, err) ≠ crash | An Axiom |