This proof is broken down into the following layers, organized top-down:
| Layer | Functionality |
|---|---|
| dir | Directories and top-level NFS API. |
| typed | Inode allocation, and hiding invariant from all lower layers. |
| byte | Byte-based files of variable size. |
| block | Block-based files, from gathering up blocks by Pos per inode from indirect layer. |
| indirect | Indirect blocks accessed by abstract position Pos. Organized into a tree rooted at an inode. |
| inode | High-level inodes with efficient in-memory access and on-disk encoding. Block allocation. |
| jrnl | Assumed transaction-system interface. |
Some interesting libraries implementing parts of the file system include:
| Library | Purpose |
|---|---|
| nfs spec | Definitions to define the NFS specification. Also see postconditions in dir_fs.dfy. |
| mem_dirent | In-memory, lazily read directories with in-place updates. |
| mem_inode | In-memory inodes with in-place updates. |
| pos | Organizes blocks in inode into a tree, determining how indirect each block is interpreted. |
| super | Static file-system configuration and disk layout. |