enrich
   afs-pre, 
   icache, 
   dcache, 
   pcache
with
   

   
   
   functions  . ⊕ . : file-heap × icache → file-heap;
              . ⊕ . : file-heap × pcache → file-heap;
              mkcontent : nat × pcache → file-content;
              . ⊕ . : file-content × file-content → file-content;
   predicates  icache-cons : icache × dir-heap × file-heap;
               dcache-cons : dcache × dir-heap × file-heap;
               pcache-cons : pcache × dir-heap × file-heap;
               ientry-clean-cons : inode × dir-heap × file-heap;
               ientry-dirty-cons : inode × dir-heap × file-heap;
               synced : nat × icache × pcache;
               synced : dir-heap × icache × pcache;
               synced : file-heap × icache × pcache;
               synced : nat × icache;
               synced : nat × nat × pcache;
   
   variables  afs_dirs : dir-heap;
              cache_dirs : dir-heap;
              afs_files : file-heap;
              cache_files : file-heap;
              cache_icache : icache;
              cache_dcache : dcache;
              cache_pcache : pcache;
              cache_sync : bool;
              cache_asynced : bool;
              afs_asynced : bool;
   
   

   

   axioms ientry-clean-cons :  ⊦ ientry-clean-cons(inode, dirs, files) ↔ valid-ino(inode.ino, dirs, files) ∧ valid-inode(inode, dirs, files);
          used for: s, ls;
          ientry-dirty-cons :  ⊦ ientry-dirty-cons(inode, dirs, files) ↔ valid-file-inode(inode, dirs, files);
          used for: s, ls;
          icache-cons
          : ⊦   icache-cons(icache, dirs, files)
              ↔ (∀ ino. 
                     ino ∈ icache
                   →   icache[ino].inode.ino = ino
                     ∧ (icache[ino].dirty
                       ⊃ valid-file-inode(icache[ino].inode, dirs, files)
                       ;valid-ino(ino, dirs, files) ∧ valid-inode(icache[ino].inode, dirs, files)
                       ));
          dcache-cons
          : ⊦   dcache-cons(dcache, dirs, files)
              ↔ (∀ key. key ∈ dcache → key.dentry? ∧ key.name = dcache[key].name ∧ valid-dentry(key.ino, dcache[key], dirs, files));
          pcache-cons
          : ⊦   pcache-cons(pcache, dirs, files)
              ↔ (∀ key. 
                     key ∈ pcache
                   →   key.data? ∧ # pcache[key].page = VFS_PAGE_SIZE ∧ valid-file-ino(key.ino, dirs, files)
                     ∧ (¬ pcache[key].dirty → key.part ∈ files[key.ino].content ∧ pcache[key].page = files[key.ino].content[key.part]));
          in-icache-overwrite :  ⊦ ino ∈ files ⊕ icache ↔ ino ∈ files;
          used for: ls, s;
          at-icache-overwrite
          : ⊦   ino ∈ icache ∧ ¬ icache[ino].inode.directory
              → (files ⊕ icache)[ino] = mkfile(icache[ino].inode.size, icache[ino].inode.meta, icache[ino].inode.nlink, files[ino].content);
          used for: ls, s;
          at-icache-overwrite-not-cached :  ⊦ ¬ ino ∈ icache → (files ⊕ icache)[ino] = files[ino];
          used for: ls, s;
          at-icache-overwrite-no-file :  ⊦ ino ∈ icache ∧ icache[ino].inode.directory → (files ⊕ icache)[ino] = files[ino];
          used for: ls, s;
          in-pcache-overwrite :  ⊦ ino ∈ files ⊕ pcache ↔ ino ∈ files;
          used for: ls, s;
          at-pcache-overwrite
          :  ⊦ (files ⊕ pcache)[ino] = mkfile(files[ino].size, files[ino].meta, files[ino].nlink, files[ino].content ⊕ mkcontent(ino, pcache));
          used for: ls, s;
          in-mkcontent :  ⊦ n ∈ mkcontent(ino, pcache) ↔ datakey(ino, n) ∈ pcache;
          used for: ls, s;
          at-mkcontent :  ⊦ mkcontent(ino, pcache)[n] = pcache[datakey(ino, n)].page;
          used for: ls, s;
          in-overwrite-content :  ⊦ n ∈ content0 ⊕ content1 ↔ n ∈ content0 ∨ n ∈ content1;
          used for: ls, s;
          at-overwrite-content-new :  ⊦ n ∈ content1 → (content0 ⊕ content1)[n] = content1[n];
          used for: ls, s;
          at-overwrite-content-old :  ⊦ ¬ n ∈ content1 → (content0 ⊕ content1)[n] = content0[n];
          used for: ls, s;
          synced-inode :  ⊦ synced(ino, icache) ↔ ino ∈ icache → ¬ icache[ino].dirty;
          used for: s, ls;
          synced-pages :  ⊦ synced(ino, m, pcache) ↔ (∀ n. n ≤ m ∧ datakey(ino, n) ∈ pcache → ¬ pcache[datakey(ino, n)].dirty);
          used for: s, ls;
          synced-ino
          :  ⊦ synced(ino, icache, pcache) ↔ (ino ∈ icache → ¬ icache[ino].dirty) ∧ (∀ n. datakey(ino, n) ∈ pcache → ¬ pcache[datakey(ino, n)].dirty);
          used for: s, ls;
          synced-dirs :  ⊦ synced(dirs, icache, pcache) ↔ (∀ ino. ino ∈ dirs → synced(ino, icache, pcache));
          synced-files :  ⊦ synced(files, icache, pcache) ↔ (∀ ino. ino ∈ files → synced(ino, icache, pcache));

   

   
end enrich