enrich
   dir-heap, 
   file-heap, 
   path
, 
   alink-set
, 
   nat-div
, 
   root-ino
, 
   inode
, 
   dentry

with
   

   
   
   functions  orphans : dir-heap × file-heap → nat-set;
              lookup : path × nat × dir-heap × file-heap → nat;
              meta : path × nat × dir-heap × file-heap → metadata;
              links : nat × dir-heap → alink-set;
              subdirs : nat × dir-heap → stringset;
              getinode : nat × dir-heap × file-heap → inode;
              . upto . : file-content × nat → file-content;
   predicates  afs-cons : dir-heap × file-heap;
               dir-empty : nat × dir-heap × file-heap;
               valid-ino : nat × dir-heap × file-heap;
               valid-dir-ino : nat × dir-heap × file-heap;
               valid-parent-ino : nat × dir-heap × file-heap;
               valid-file-ino : nat × dir-heap × file-heap;
               valid-dentry : nat × dentry × dir-heap × file-heap;
               valid-dentry : dentry × dir-heap × file-heap;
               valid-negdentry : nat × dentry × dir-heap × file-heap;
               valid-inode : inode × dir-heap × file-heap;
               valid-content : nat × file-heap;
               valid-pagesize : nat × nat × file-heap;
               ispath : path × nat × dir-heap × file-heap;
               ispath : path × nat × nat × dir-heap × file-heap;
   
   variables  ino : nat;
              p_ino : nat;
              dent : dentry;
              name : string;
   
   

   

   axioms afs-cons
          : ⊦   afs-cons(dirs, files)
              ↔ (∀ ino. 
                     ROOT_INO ∈ dirs ∧ (ino ∈ dirs ∧ ino ≠ ROOT_INO ∧ links(ino, dirs) = ∅ → dir-empty(ino, dirs, files))
                   ∧ (  ino ∈ dirs
                      →   ¬ ino ∈ files ∧ dirs[ino].nlink = # links(ino, dirs) ∧ dirs[ino].nlink ≤ 1 ∧ dirs[ino].size = # dirs[ino].entries
                        ∧ dirs[ino].nsubdirs = # subdirs(ino, dirs))
                   ∧ (ino ∈ files → ¬ ino ∈ dirs ∧ files[ino].nlink = # links(ino, dirs))
                   ∧ (∀ name. ino ∈ dirs ∧ name ∈ dirs[ino].entries → valid-ino(dirs[ino].entries[name], dirs, files))
                   ∧ (∀ n. ino ∈ files ∧ n ∈ files[ino].content → valid-pagesize(ino, n, files)));
          orphans :  ⊦ ino ∈ orphans(dirs, files) ↔ valid-ino(ino, dirs, files) ∧ links(ino, dirs) = ∅ ∧ ino ≠ ROOT_INO;
          getinode
          : ⊦   getinode(ino, dirs, files)
              = (ino ∈ dirs
                ⊃ mkinode(ino, dirs[ino].meta, true, dirs[ino].nlink, dirs[ino].nsubdirs, dirs[ino].size)
                ;mkinode(ino, files[ino].meta, false, files[ino].nlink, 0, files[ino].size)
                );
          used for: s, ls;
          dir-empty :  ⊦ dir-empty(ino, dirs, files) ↔ dirs[ino].entries = ∅;
          used for: s, ls;
          valid-ino :  ⊦ valid-ino(ino, dirs, files) ↔ ino ∈ dirs ∨ ino ∈ files;
          used for: s, ls, ss, lss;
          valid-dir-ino :  ⊦ valid-dir-ino(ino, dirs, files) ↔ ino ∈ dirs;
          used for: s, ls;
          valid-parent-ino :  ⊦ valid-parent-ino(ino, dirs, files) ↔ ino ∈ dirs ∧ (links(ino, dirs) ≠ ∅ ∨ ino = ROOT_INO);
          used for: s, ls, ss, lss;
          valid-file-ino :  ⊦ valid-file-ino(ino, dirs, files) ↔ ino ∈ files;
          used for: s, ls;
          valid-negdentry
          :  ⊦ valid-negdentry(ino, dent, dirs, files) ↔ valid-parent-ino(ino, dirs, files) ∧ ¬ dent.name ∈ dirs[ino].entries ∧ dent.negdentry?;
          used for: s, ls, ss, lss;
          valid-dentry :  ⊦ valid-dentry(dent, dirs, files) ↔ (∃ ino. valid-dentry(ino, dent, dirs, files));
          used for: s, ls;
          valid-dentry-with-parent
          : ⊦   valid-dentry(ino, dent, dirs, files)
              ↔   valid-parent-ino(ino, dirs, files) ∧ valid-ino(dent.ino, dirs, files) ∧ dent.name ∈ dirs[ino].entries
                ∧ dent.ino = dirs[ino].entries[dent.name] ∧ dent.dentry?;
          used for: s, ls, ss, lss;
          valid-inode :  ⊦ valid-inode(inode, dirs, files) ↔ inode = getinode(inode.ino, dirs, files);
          used for: s, ls;
          links :  ⊦ alink ∈ links(ino, dirs) ↔ alink.pino ∈ dirs ∧ alink.name ∈ dirs[alink.pino].entries ∧ ino = dirs[alink.pino].entries[alink.name];
          used for: s, ls, ss, lss;
          subdirs :  ⊦ str ∈ subdirs(ino, dirs) ↔ ino ∈ dirs ∧ str ∈ dirs[ino].entries ∧ dirs[ino].entries[str] ∈ dirs;
          used for: s, ls, ss, lss;
          expath :  ⊦ ispath(p, n, dirs, files) ↔ (∃ m. ispath(p, n, m, dirs, files));
          path-here :  ⊦ ispath(ε, n, m, dirs, files) ↔ valid-ino(n, dirs, files) ∧ m = n;
          used for: s, ls, ss, lss;
          path-rec
          : ⊦   ispath(str ' + p, n, m, dirs, files)
              ↔ valid-dir-ino(n, dirs, files) ∧ str ∈ dirs[n].entries ∧ ispath(p, dirs[n].entries[str], m, dirs, files);
          used for: s, ls, ss, lss;
          lookup-here :  ⊦ valid-ino(n, dirs, files) → lookup(ε, n, dirs, files) = n;
          used for: s, ls;
          lookup-rec :  ⊦ ino ∈ dirs ∧ str ∈ dirs[n].entries → lookup(str ' + p, n, dirs, files) = lookup(p, dirs[n].entries[str], dirs, files);
          used for: s, ls;
          meta
          : ⊦   ispath(p, n, dirs, files)
              →   meta(p, n, dirs, files)
                = (lookup(p, n, dirs, files) ∈ dirs ⊃ dirs[lookup(p, n, dirs, files)].meta;files[lookup(p, n, dirs, files)].meta);
          in-upto :  ⊦ m ∈ content upto n ↔ m * VFS_PAGE_SIZE < n ∧ m ∈ content;
          used for: s, ls, ss, lss;
          at-upto :  ⊦ m * VFS_PAGE_SIZE < n ∧ m ∈ content → (content upto n)[m] = content[m];
          used for: s, ls;
          valid-content :  ⊦ valid-content(ino, files) ↔ (∀ n. n ∈ files[ino].content → n * VFS_PAGE_SIZE < files[ino].size);
          used for: ls;
          valid-pagesize :  ⊦ valid-pagesize(ino, n, files) ↔ # files[ino].content[n] = VFS_PAGE_SIZE;
          used for: s, ls;

   

   
end enrich