This is a listing of all goals defined over the current specification. Axioms are marked yellow, proved theorems green and unproved theorems blue. Click on individual names to get more information on the proof.
| Name: | Sequent: | Type: |
|---|---|---|
| mkdir | posix_mkdir#(PATH, MD, USER, FS, OFH; ERR, ROOT; PSYNCED) {choose E with pre-mkdir(PATH, MD, E, USER, ROOT, FS, OFH) in ERR := E; if ERR = ESUCCESS then ROOT[PATH] := dnode(MD, ∅); PSYNCED := ?} | An Axiom |
| rmdir | posix_rmdir#(PATH, USER, FS, OFH; ERR, ROOT; PSYNCED) {choose E with pre-rmdir(PATH, E, USER, ROOT, FS, OFH) in ERR := E; if ERR = ESUCCESS then ROOT := ROOT -- PATH; PSYNCED := ?} | An Axiom |
| create | posix_create#(PATH, MD, USER, OFH; ERR, ROOT, FS; PSYNCED) {choose E with pre-create(PATH, MD, E, USER, ROOT, FS, OFH) in ERR := E; if ERR = ESUCCESS then choose FID with ¬ FID ∈ FS in {ROOT[PATH] := fnode(FID); FS[FID] := mkfile(MD, mkbuf(0))}; PSYNCED := ? } | An Axiom |
| open | posix_open#(PATH, MODE, USER, ROOT, FS; FD, ERR, OFH) {choose E with pre-open(PATH, MODE, E, USER, ROOT, FS, OFH) in ERR := E; if ERR = ESUCCESS then let FID = ROOT[PATH].fid in choose N with ¬ N ∈ OFH in {OFH[N] := mkfh(FID, MODE, 0); FD := N} } | An Axiom |
| close | posix_close#(FD, USER, ROOT; ERR, FS, OFH) {choose E with pre-close(FD, E, USER, ROOT, FS, OFH) in ERR := E; if ERR = ESUCCESS then let FID = OFH[FD].fid in {OFH := OFH -- FD; if ¬ FID ∈ OFH.fids ∧ ¬ FID ∈ ROOT.fids then FS := FS -- FID} } | An Axiom |
| read | posix_read#(FD, USER, ROOT, FS; BUF, N, ERR, OFH) {if N ≤ # BUF then {choose E with pre-read(FD, N, E, USER, ROOT, FS, OFH) in ERR := E; if ERR = ESUCCESS then let FH = OFH[FD] in let FDATA = FS[FH.fid] in choose N0 with N0 ≤ N ∧ FH.pos + N0 ≤ # FDATA.content in {N := N0; BUF := copy(FDATA.content, FH.pos, BUF, 0, N); OFH[FD].pos := FH.pos + N} ifnone N := 0 else N := ?} else abort } | An Axiom |
| write | posix_write#(FD, BUF, USER, ROOT; N, ERR, FS, OFH; PSYNCED) {if N ≤ # BUF then {choose E with pre-write(FD, BUF, N, E, USER, ROOT, FS, OFH) in ERR := E; if ERR = ESUCCESS then let FH = OFH[FD] in let FDATA = FS[FH.fid] in choose N0 with N0 ≤ N in {N := N0; FDATA.content := splice(BUF, 0, FDATA.content, FH.pos, N); FS[FH.fid] := FDATA; OFH[FD].pos := FH.pos + N} else N := ?; PSYNCED := ?} else abort } | An Axiom |
| seek | posix_seek#(FD, WHENCE, USER, ROOT, FS; N, ERR, OFH) {choose E with pre-seek(FD, N, WHENCE, E, USER, ROOT, FS, OFH) in ERR := E; if ERR = ESUCCESS then let FH = OFH[FD] in let FDATA = FS[FH.fid] in {if WHENCE = SEEK_CUR then N := FH.pos + N else if WHENCE = SEEK_END then N := # FDATA.content + N; OFH[FD].pos := N} } | An Axiom |
| renam | posix_rename#(PATH, PATH', USER, OFH; ERR, ROOT, FS; PSYNCED) {choose E with pre-renam(PATH, PATH', E, USER, ROOT, FS, OFH) in ERR := E; if ERR = ESUCCESS then let DIR = ROOT[PATH], EXISTS = PATH' ∈ ROOT, TREE = ROOT[PATH'] in {ROOT := (ROOT -- PATH)[PATH', DIR]; if EXISTS ∧ ¬ TREE.dir? ∧ ¬ TREE.fid ∈ OFH.fids ∧ ¬ TREE.fid ∈ ROOT.fids then FS := FS -- TREE.fid}; PSYNCED := ? } | An Axiom |
| link | posix_link#(PATH, PATH', USER, FS, OFH; ERR, ROOT; PSYNCED) {choose E with pre-link(PATH, PATH', E, USER, ROOT, FS, OFH) in ERR := E; if ERR = ESUCCESS then let FID = ROOT[PATH].fid in ROOT[PATH'] := fnode(FID); PSYNCED := ? } | An Axiom |
| unlink | posix_unlink#(PATH, USER, OFH; ERR, ROOT, FS; PSYNCED) {choose E with pre-unlink(PATH, E, USER, ROOT, FS, OFH) in ERR := E; if ERR = ESUCCESS then let FID = ROOT[PATH].fid in {ROOT := ROOT -- PATH; if ¬ FID ∈ OFH.fids ∧ ¬ FID ∈ ROOT.fids then FS := FS -- FID}; PSYNCED := ? } | An Axiom |
| truncate | posix_truncate#(PATH, N, USER, ROOT, OFH; ERR, FS; PSYNCED) {choose E with pre-truncate(PATH, N, E, USER, ROOT, FS, OFH) in ERR := E; if ERR = ESUCCESS then let FID = ROOT[PATH].fid in let BUF = FS[FID].content in FS[FID].content := resize(BUF, N); PSYNCED := ? } | An Axiom |
| readmeta | posix_readmeta#(PATH, USER, ROOT, FS, OFH; MD, NLINK, SIZE, ERR) {choose E with pre-readmeta(PATH, E, USER, ROOT, FS, OFH) in ERR := E; if ERR = ESUCCESS then if ROOT[PATH].dir? then MD := ROOT[PATH].meta, NLINK := # ROOT[PATH].subdirs + 2, SIZE := # ROOT[PATH].entries else let FID = ROOT[PATH].fid in MD := FS[FID].meta, NLINK := count(FID, ROOT.fids), SIZE := # FS[FID].content } | An Axiom |
| writemeta | posix_writemeta#(PATH, MD, USER, OFH; ERR, ROOT, FS; PSYNCED) {choose E with pre-writemeta(PATH, MD, E, USER, ROOT, FS, OFH) in ERR := E; if ERR = ESUCCESS then if ROOT[PATH].dir? then ROOT[PATH].meta := MD else let FID = ROOT[PATH].fid in FS[FID].meta := MD; PSYNCED := ? } | An Axiom |
| readdir | posix_readdir#(PATH, USER, ROOT, FS, OFH; NAMES, ERR) {choose E with pre-readdir(PATH, E, USER, ROOT, FS, OFH) in ERR := E; if ERR = ESUCCESS then NAMES := dom ROOT[PATH].entries else NAMES := ?} | An Axiom |
| format | posix_format#(N, DOSYNC, SIZE, MD; ; ROOT, FS, OFH, PSYNCED, ERR) {if SIZE = LEB_SIZE then { ROOT := dnode(MD, ∅), FS := ∅, OFH := ∅, PSYNCED := true, ERR := ESUCCESS or {ROOT := ?, FS := ?, OFH := ?, PSYNCED := ?; choose E with ⌊E⌋ in ERR := E}} else abort } | An Axiom |
| recover | posix_recover#(DOSYNC; ROOT, FS, OFH; PSYNCED, ERR) {fail_or_success#(; ; ERR); if ERR ≠ ESUCCESS then ROOT := ?, FS := ?, OFH := ?, PSYNCED := ? else PSYNCED := true} | An Axiom |
| fsyncdir | posix_fsyncdir#(PATH, ISDATASYNC, USER; ; PSYNCED, ERR){fail_or_success#(; ; ERR); PSYNCED := ?} | An Axiom |
| fsync | posix_fsync#(PATH, ISDATASYNC, USER, ROOT, FS, OFH; ; PSYNCED, ERR) {choose E with pre-fsync(PATH, ISDATASYNC, E, USER, ROOT, FS, OFH) in ERR := E; PSYNCED := ?} | An Axiom |
| sync | posix_sync#(; ; PSYNCED, ERR){fail_or_success#(; ; ERR); PSYNCED := ERR = ESUCCESS} | An Axiom |
| inv-format | m = LEB_SIZE ⊦ ⟪posix_format#(n, psynced, m, md; ; root, fs, ofh, psynced0, err)⟫ (err = ESUCCESS → psynced0 ∧ root.dir? ∧ fids-cons(root, fs, ofh)) | A Proof Obligation |
| inv-readdir | root.dir?, fids-cons(root, fs, ofh) ⊦ ⟪posix_readdir#(path, user, root, fs, ofh; strings, err)⟫ true | A Proof Obligation |
| inv-writemeta | root.dir?, fids-cons(root, fs, ofh) ⊦ ⟪posix_writemeta#(path, md, user, ofh; err, root, fs; psynced)⟫ (root.dir? ∧ fids-cons(root, fs, ofh)) | A Proof Obligation |
| inv-readmeta | root.dir?, fids-cons(root, fs, ofh) ⊦ ⟪posix_readmeta#(path, user, root, fs, ofh; md, m, m0, err)⟫ true | A Proof Obligation |
| inv-truncate | root.dir?, fids-cons(root, fs, ofh) ⊦ ⟪posix_truncate#(path, n, user, root, ofh; err, fs; psynced)⟫ fids-cons(root, fs, ofh) | A Proof Obligation |
| inv-unlink | root.dir?, fids-cons(root, fs, ofh) ⊦ ⟪posix_unlink#(path, user, ofh; err, root, fs; psynced)⟫ (root.dir? ∧ fids-cons(root, fs, ofh)) | A Proof Obligation |
| inv-link | root.dir?, fids-cons(root, fs, ofh) ⊦ ⟪posix_link#(path, path', user, fs, ofh; err, root; psynced)⟫ (root.dir? ∧ fids-cons(root, fs, ofh)) | A Proof Obligation |
| inv-renam | root.dir?, fids-cons(root, fs, ofh) ⊦ ⟪posix_rename#(path, path', user, ofh; err, root, fs; psynced)⟫ (root.dir? ∧ fids-cons(root, fs, ofh)) | A Proof Obligation |
| inv-seek | root.dir?, fids-cons(root, fs, ofh) ⊦ ⟪posix_seek#(fd, whence, user, root, fs; n, err, ofh)⟫ fids-cons(root, fs, ofh) | A Proof Obligation |
| inv-write | root.dir?, fids-cons(root, fs, ofh), n ≤ # buf ⊦ ⟪posix_write#(fd, buf, user, root; n, err, fs, ofh; psynced)⟫ fids-cons(root, fs, ofh) | A Proof Obligation |
| inv-read | root.dir?, fids-cons(root, fs, ofh), n ≤ # buf ⊦ ⟪posix_read#(fd, user, root, fs; buf, n, err, ofh)⟫ fids-cons(root, fs, ofh) | A Proof Obligation |
| inv-close | root.dir?, fids-cons(root, fs, ofh) ⊦ ⟪posix_close#(fd, user, root; err, fs, ofh)⟫ fids-cons(root, fs, ofh) | A Proof Obligation |
| inv-open | root.dir?, fids-cons(root, fs, ofh) ⊦ ⟪posix_open#(path, mode, user, root, fs; fd, err, ofh)⟫ fids-cons(root, fs, ofh) | A Proof Obligation |
| inv-create | root.dir?, fids-cons(root, fs, ofh) ⊦ ⟪posix_create#(path, md, user, ofh; err, root, fs; psynced)⟫ (root.dir? ∧ fids-cons(root, fs, ofh)) | A Proof Obligation |
| inv-rmdir | root.dir?, fids-cons(root, fs, ofh) ⊦ ⟪posix_rmdir#(path, user, fs, ofh; err, root; psynced)⟫ (root.dir? ∧ fids-cons(root, fs, ofh)) | A Proof Obligation |
| inv-mkdir | root.dir?, fids-cons(root, fs, ofh) ⊦ ⟪posix_mkdir#(path, md, user, fs, ofh; err, root; psynced)⟫ (root.dir? ∧ fids-cons(root, fs, ofh)) | A Proof Obligation |
| inv-recover | posix-crash(tree, fs, ofh, root, fs0, ofh0), psynced, tree.dir?, fids-cons(tree, fs, ofh) ⊦ ⟪posix_recover#(psynced0; root, fs0, ofh0; psynced1, err)⟫ (err = ESUCCESS → psynced1 ∧ root.dir? ∧ fids-cons(root, fs0, ofh0)) | A Proof Obligation |
| crash-neutral-readdir | root.dir?, fids-cons(root, fs, ofh), psynced, posix-crash(root, fs, ofh, tree, fs0, ofh0) ⊦ ⟨posix_readdir#(path, user, root, fs, ofh; strings, err)⟩ (psynced ∧ posix-crash(root, fs, ofh, tree, fs0, ofh0)) | A Proof Obligation |
| crash-neutral-writemeta | root.dir?, fids-cons(root, fs, ofh), psynced, posix-crash(root, fs, ofh, tree, fs0, ofh0) ⊦ ⟨posix_writemeta#(path, md, user, ofh; err, root, fs; psynced)⟩ (psynced ∧ posix-crash(root, fs, ofh, tree, fs0, ofh0)) | A Proof Obligation |
| crash-neutral-readmeta | root.dir?, fids-cons(root, fs, ofh), psynced, posix-crash(root, fs, ofh, tree, fs0, ofh0) ⊦ ⟨posix_readmeta#(path, user, root, fs, ofh; md, m, m0, err)⟩ (psynced ∧ posix-crash(root, fs, ofh, tree, fs0, ofh0)) | A Proof Obligation |
| crash-neutral-truncate | root.dir?, fids-cons(root, fs, ofh), psynced, posix-crash(root, fs, ofh, tree, fs0, ofh0) ⊦ ⟨posix_truncate#(path, n, user, root, ofh; err, fs; psynced)⟩ (psynced ∧ posix-crash(root, fs, ofh, tree, fs0, ofh0)) | A Proof Obligation |
| crash-neutral-unlink | root.dir?, fids-cons(root, fs, ofh), psynced, posix-crash(root, fs, ofh, tree, fs0, ofh0) ⊦ ⟨posix_unlink#(path, user, ofh; err, root, fs; psynced)⟩ (psynced ∧ posix-crash(root, fs, ofh, tree, fs0, ofh0)) | A Proof Obligation |
| crash-neutral-link | root.dir?, fids-cons(root, fs, ofh), psynced, posix-crash(root, fs, ofh, tree, fs0, ofh0) ⊦ ⟨posix_link#(path, path', user, fs, ofh; err, root; psynced)⟩ (psynced ∧ posix-crash(root, fs, ofh, tree, fs0, ofh0)) | A Proof Obligation |
| crash-neutral-renam | root.dir?, fids-cons(root, fs, ofh), psynced, posix-crash(root, fs, ofh, tree, fs0, ofh0) ⊦ ⟨posix_rename#(path, path', user, ofh; err, root, fs; psynced)⟩ (psynced ∧ posix-crash(root, fs, ofh, tree, fs0, ofh0)) | A Proof Obligation |
| crash-neutral-seek | root.dir?, fids-cons(root, fs, ofh), psynced, posix-crash(root, fs, ofh, tree, fs0, ofh0) ⊦ ⟨posix_seek#(fd, whence, user, root, fs; n, err, ofh)⟩ (psynced ∧ posix-crash(root, fs, ofh, tree, fs0, ofh0)) | A Proof Obligation |
| crash-neutral-write | n ≤ # buf, root.dir?, fids-cons(root, fs, ofh), psynced, posix-crash(root, fs, ofh, tree, fs0, ofh0) ⊦ ⟨posix_write#(fd, buf, user, root; n, err, fs, ofh; psynced)⟩ (psynced ∧ posix-crash(root, fs, ofh, tree, fs0, ofh0)) | A Proof Obligation |
| crash-neutral-read | n ≤ # buf, root.dir?, fids-cons(root, fs, ofh), psynced, posix-crash(root, fs, ofh, tree, fs0, ofh0) ⊦ ⟨posix_read#(fd, user, root, fs; buf, n, err, ofh)⟩ (psynced ∧ posix-crash(root, fs, ofh, tree, fs0, ofh0)) | A Proof Obligation |
| crash-neutral-close | root.dir?, fids-cons(root, fs, ofh), psynced, posix-crash(root, fs, ofh, tree, fs0, ofh0) ⊦ ⟨posix_close#(fd, user, root; err, fs, ofh)⟩ (psynced ∧ posix-crash(root, fs, ofh, tree, fs0, ofh0)) | A Proof Obligation |
| crash-neutral-open | root.dir?, fids-cons(root, fs, ofh), psynced, posix-crash(root, fs, ofh, tree, fs0, ofh0) ⊦ ⟨posix_open#(path, mode, user, root, fs; fd, err, ofh)⟩ (psynced ∧ posix-crash(root, fs, ofh, tree, fs0, ofh0)) | A Proof Obligation |
| crash-neutral-create | root.dir?, fids-cons(root, fs, ofh), psynced, posix-crash(root, fs, ofh, tree, fs0, ofh0) ⊦ ⟨posix_create#(path, md, user, ofh; err, root, fs; psynced)⟩ (psynced ∧ posix-crash(root, fs, ofh, tree, fs0, ofh0)) | A Proof Obligation |
| crash-neutral-rmdir | root.dir?, fids-cons(root, fs, ofh), psynced, posix-crash(root, fs, ofh, tree, fs0, ofh0) ⊦ ⟨posix_rmdir#(path, user, fs, ofh; err, root; psynced)⟩ (psynced ∧ posix-crash(root, fs, ofh, tree, fs0, ofh0)) | A Proof Obligation |
| crash-neutral-mkdir | root.dir?, fids-cons(root, fs, ofh), psynced, posix-crash(root, fs, ofh, tree, fs0, ofh0) ⊦ ⟨posix_mkdir#(path, md, user, fs, ofh; err, root; psynced)⟩ (psynced ∧ posix-crash(root, fs, ofh, tree, fs0, ofh0)) | A Proof Obligation |
| crash-neutral-recover | root.dir?, fids-cons(root, fs, ofh), psynced, posix-crash(root, fs, ofh, tree, fs0, ofh0) ⊦ ⟨posix_recover#(psynced0; root, fs, ofh; psynced, err)⟩ (psynced ∧ posix-crash(root, fs, ofh, tree, fs0, ofh0)) | A Proof Obligation |
| crash-neutral-fsyncdir | root.dir?, fids-cons(root, fs, ofh), psynced, posix-crash(root, fs, ofh, tree, fs0, ofh0) ⊦ ⟨posix_fsyncdir#(path, psynced0, user; ; psynced, err)⟩ (psynced ∧ posix-crash(root, fs, ofh, tree, fs0, ofh0)) | A Proof Obligation |
| crash-neutral-fsync | root.dir?, fids-cons(root, fs, ofh), psynced, posix-crash(root, fs, ofh, tree, fs0, ofh0) ⊦ ⟨posix_fsync#(path, psynced0, user, root, fs, ofh; ; psynced, err)⟩ (psynced ∧ posix-crash(root, fs, ofh, tree, fs0, ofh0)) | A Proof Obligation |
| crash-neutral-sync | root.dir?, fids-cons(root, fs, ofh), psynced, posix-crash(root, fs, ofh, tree, fs0, ofh0) ⊦ ⟨posix_sync#(; ; psynced, err)⟩ (psynced ∧ posix-crash(root, fs, ofh, tree, fs0, ofh0)) | A Proof Obligation |
| inv-fsyncdir | ⊦ ⟪posix_fsyncdir#(path, psynced, user; ; psynced0, err)⟫ true | A Proof Obligation |
| inv-fsync | root.dir?, fids-cons(root, fs, ofh) ⊦ ⟪posix_fsync#(path, psynced, user, root, fs, ofh; ; psynced0, err)⟫ true | A Proof Obligation |
| inv-sync | ⊦ ⟪posix_sync#(; ; psynced, err)⟫ true | A Proof Obligation |
| fid-in-fs | ⊦ fids-cons(root, fs, ofh) ∧ fd ∈ ofh ∧ ofh[fd] = mkfh(fid, mode, m) → fid ∈ fs | A User Theorem |
| fids-cons-reduce | ⊦ fids-cons(tree0, fs0, ofh0) → (fids-cons(tree1, fs1, ofh1) ↔ (∀ fid. (fid ∈ fs0 ↔ fid ∈ tree0.fids ∨ fid ∈ ofh0.fids) → (fid ∈ fs1 ↔ fid ∈ tree1.fids ∨ fid ∈ ofh1.fids))) | A User Theorem |
| fids-exists | ⊦ ∃ fids. ∀ fid. fid ∈ fids ↔ fid ∈ tree.fids | A User Theorem |
| rename-fids | fids-cons(root, fs, ofh) ⊦ [posix_rename#(path, path', user, ofh; err, root, fs; psynced)] fids-cons(root, fs, ofh) | A User Theorem |
| rename-root | root.dir? ⊦ [posix_rename#(path, path', user, ofh; err, root, fs; psynced)] root.dir? | A User Theorem |