(*
 * Copyright 2016, NICTA
 *
 * This software may be distributed and modified according to the terms of
 * the GNU General Public License version 2. Note that NO WARRANTY is provided.
 * See "LICENSE_GPLv2.txt" for details.
 *
 * @TAG(NICTA_GPL)
 *)

theory AfsS
imports
   "../lib/FunBucket"
   "../adt/VfsT"
   "../adt/WordArrayT"
   "../lib/CogentMonad"
begin

text {* High-level Correctness specification types *}

type_synonym byte = "U8"
type_synonym page = "U8 list"
type_synonym dir = "U8 list \<rightharpoonup> Ino"
type_synonym file_data = "page list"

datatype afs_inode_type =
  IDir "dir"
| IReg "file_data"
| ILnk  "U8 list"

definition "afs_inode_is_dir x \<equiv> \<exists>v. IDir v = x"
definition "afs_inode_is_reg x \<equiv> \<exists>v. IReg v = x"
definition "afs_inode_is_lnk x \<equiv> \<exists>v. ILnk v = x"

record afs_inode =
  i_type :: "afs_inode_type"
  i_ino :: "Ino"
  i_nlink :: "U32"
  i_size :: "U64"
  i_mtime :: "TimeT"
  i_ctime :: "TimeT"
  i_uid :: "U32"
  i_gid :: "U32"
  i_mode :: "Mode"
  i_flags :: "U32"

type_synonym readdir_ctx = "(U32 \<times> dir)" (* Remaining elements to read from the dir *)

type_synonym afs_map =  "Ino \<rightharpoonup> afs_inode" (* on-disk state *)

record afs_state =
  a_is_readonly :: "bool"
  a_current_time :: "TimeT"
  a_medium_afs :: "afs_map" (* On-medium FS observable when a crash happens or when sync fails before any update was applied *)
  a_medium_updates :: "(afs_map \<Rightarrow> afs_map) list" (* FIFO of on-medium updates *)

definition
  a_afs_updated_n :: "nat \<Rightarrow> afs_map \<Rightarrow> (afs_map \<Rightarrow> afs_map) list \<Rightarrow> afs_map"
where
 a_afs_updated_n_def[simp]:
 "a_afs_updated_n n afs_st updates = fold id (take n updates) afs_st"

definition
  a_afs_updated :: "afs_map \<Rightarrow> (afs_map \<Rightarrow> afs_map) list \<Rightarrow> afs_map"
where
 "a_afs_updated afs_st updates \<equiv> a_afs_updated_n (length updates) afs_st updates"

definition
  updated_afs :: "afs_state \<Rightarrow> afs_map"
where
  "updated_afs adata \<equiv> a_afs_updated (a_medium_afs adata) (a_medium_updates adata)"

abbreviation i_type_dir :: "afs_inode_type \<Rightarrow> dir"
 where
  "i_type_dir it \<equiv> (case it of IDir dir \<Rightarrow> dir)"

abbreviation i_dir :: "afs_inode \<Rightarrow> dir"
where
  "i_dir i \<equiv> i_type_dir (i_type i)"

definition
  i_dir_update :: "(dir \<Rightarrow> dir) \<Rightarrow> afs_inode \<Rightarrow> afs_inode"
 where
  i_dir_update_def[simp]:
  "i_dir_update m i \<equiv> i \<lparr>i_type:= IDir (m (i_dir i)) \<rparr>"
                                                  
abbreviation i_type_data :: "afs_inode_type \<Rightarrow> file_data"
where
  "i_type_data it \<equiv> (case it of IReg data \<Rightarrow> data)"
(*
abbreviation dirent_i_type :: "afs_inode_type \<Rightarrow> dirent_type"
where
 "dirent_i_type it \<equiv> (case it of IDir _ \<Rightarrow> DT_DIR | IReg _ \<Rightarrow> DT_REG | ILnk _ \<Rightarrow> DT_LNK)"
 *)
abbreviation i_data :: "afs_inode \<Rightarrow> file_data"
where
  "i_data i \<equiv> i_type_data (i_type i)"

abbreviation i_data_update :: "(file_data \<Rightarrow> file_data) \<Rightarrow> afs_inode \<Rightarrow> afs_inode"
 where
  "i_data_update m i \<equiv> i \<lparr>i_type:= IReg (m (i_data i)) \<rparr>"

abbreviation i_type_path :: "afs_inode_type \<Rightarrow> byte list"
where
  "i_type_path it \<equiv> (case it of ILnk path \<Rightarrow> path)"

abbreviation i_path :: "afs_inode \<Rightarrow> byte list"
where
  "i_path i \<equiv> i_type_path (i_type i)"

abbreviation i_path_update :: "(byte list \<Rightarrow> byte list) \<Rightarrow> afs_inode \<Rightarrow> afs_inode"
 where
  "i_path_update m i \<equiv> i \<lparr>i_type:= ILnk (m (i_path i)) \<rparr>"

primrec i_size_from_afs_inode_type :: "afs_inode_type \<Rightarrow> U64"
where
(* Can we prove anything about the size of a directory? *)
  "i_size_from_afs_inode_type (IDir dir) = undefined"
 |"i_size_from_afs_inode_type (IReg data) = count (concat data)"
 |"i_size_from_afs_inode_type (ILnk path) = count path"

abbreviation i_size_from_type :: "afs_inode \<Rightarrow> U64"
where
 "i_size_from_type i \<equiv> i_size_from_afs_inode_type $ i_type i"

definition
  afs_inode_to_vnode :: "afs_inode \<Rightarrow> VfsInode"
where
 "afs_inode_to_vnode i \<equiv> \<lparr>
    v_ino = i_ino i,
    v_nlink = i_nlink i,
    v_size =  i_size i,
    v_mtime = i_mtime i,
    v_ctime = i_ctime i,
    v_uid = i_uid i,
    v_gid = i_gid i,
    v_mode = i_mode i,
    v_flags = i_flags i\<rparr>"

definition
  afs_inode_from_vnode :: "vnode \<Rightarrow> afs_inode"
where
 "afs_inode_from_vnode v \<equiv> \<lparr>
    i_type = if (v_mode v AND s_IFREG \<noteq> 0) then IReg [] else if v_mode v AND s_IFDIR \<noteq> 0 then IDir Map.empty else ILnk [],
    i_ino = v_ino v,
    i_nlink = v_nlink v,
    i_size = v_size v,
    i_mtime = v_mtime v,
    i_ctime = v_ctime v,
    i_uid = v_uid v,
    i_gid = v_gid v,
    i_mode = v_mode v,
    i_flags = v_flags v\<rparr>"

definition
  error_if_readonly :: "afs_state \<Rightarrow> (((ErrCode \<times> afs_state), afs_state) R) cogent_monad"
where
  "error_if_readonly as \<equiv> return $ if a_is_readonly as then Error (eRoFs, as) else Success as"

definition
  nondet_error :: "ErrCode set \<Rightarrow> (ErrCode \<Rightarrow> 'a) \<Rightarrow> 'a cogent_monad"
where
  "nondet_error errs f \<equiv> CogentMonad.select errs >>= (return o f)"

text {*
 @{term afs_alloc_inum}: We ensure that it only returns inums not already in used
 (by checking it is in the set @{text "-dom as"}). The function can
  return an Error.
*} 
definition
  afs_alloc_inum :: "afs_map \<Rightarrow> ((unit, Ino) R) cogent_monad"
where
 "afs_alloc_inum as \<equiv>
    (do
     avail_inums \<leftarrow> return $ - dom as ;
     opt_inum \<leftarrow> select $ {option.None} \<union> option.Some ` avail_inums ;
     return $ if opt_inum = option.None then
        Error ()
      else        
        Success (the opt_inum)
     od)"


(* os_get_current_time *)
definition
 afs_get_current_time :: "afs_state \<Rightarrow> (afs_state \<times> TimeT) cogent_monad"
where
 "afs_get_current_time afs \<equiv> do
   time' \<leftarrow> return (a_current_time afs);
   time \<leftarrow> select {x. x \<ge> time'};
   return (afs\<lparr> a_current_time := time \<rparr>, time')
  od"


definition
  afs_init_inode :: "afs_state \<Rightarrow> vnode \<Rightarrow> vnode \<Rightarrow> VfsMode \<Rightarrow>
                      ((afs_state \<times> vnode, afs_state \<times> vnode) R) cogent_monad"
where
 "afs_init_inode adata vdir vnode mode \<equiv> do
     (adata, time) \<leftarrow> afs_get_current_time adata;
     uid \<leftarrow> return (v_uid vdir);
     gid \<leftarrow> return (v_gid vdir);
     vnode \<leftarrow> return (vnode\<lparr> v_ctime:=time, v_mtime:=time, v_uid:=uid,
                         v_gid:=gid, v_mode:=mode, v_nlink:=1, v_size:=0 \<rparr>);
     r \<leftarrow> afs_alloc_inum (updated_afs adata);
     return (case r of
       Error () \<Rightarrow> Error (adata, vnode)
       | Success inum \<Rightarrow> Success (adata, vnode\<lparr> v_ino := inum \<rparr>)
      )
  od"

definition
  read_afs_inode :: "afs_state \<Rightarrow> Ino \<Rightarrow> ((afs_inode,ErrCode) R\<^sub>T) cogent_monad"
where
 "read_afs_inode adata ino \<equiv>
   return (Success $ the $ updated_afs adata ino) \<sqinter>
     nondet_error {eIO, eNoMem, eInval, eBadF} Error"

definition
 afs_apply_updates_nondet :: "afs_state \<Rightarrow> afs_state cogent_monad"
where
 "afs_apply_updates_nondet afs  \<equiv> do
    (to_apply, updates) \<leftarrow> {(ap, up). ap @ up = a_medium_updates afs};
    return (afs \<lparr>a_medium_afs := fold id to_apply  (a_medium_afs afs),
                 a_medium_updates := updates\<rparr>)
  od"

definition
 afs_update :: "afs_state \<Rightarrow> (afs_map \<Rightarrow> afs_map) \<Rightarrow> (afs_state \<times> (unit, ErrCode)  R\<^sub>T) cogent_monad"
where
 "afs_update afs upd \<equiv> do
    afs \<leftarrow> afs_apply_updates_nondet (afs\<lparr>a_medium_updates := a_medium_updates afs @ [upd]\<rparr>) ;
    if a_medium_updates afs  = [] then 
      return (afs, Success ())
    else
      return (afs, Success ()) \<sqinter>
      nondet_error {eIO, eNoSpc, eNoMem} (\<lambda>e. (afs\<lparr>a_medium_updates:= butlast (a_medium_updates afs)\<rparr>,Error e))
  od"

definition
  afs_create :: "afs_state \<Rightarrow> vnode \<Rightarrow> U8 WordArray \<Rightarrow> VfsMode \<Rightarrow> vnode \<Rightarrow>
                   ((afs_state \<times> vnode \<times> vnode) \<times> (unit, ErrCode) R\<^sub>T) cogent_monad"
where
  "afs_create afs parentdir name mode vnode \<equiv>
  if a_is_readonly afs then
    return ((afs, parentdir, vnode), Error eRoFs)
   else do
   r \<leftarrow> afs_init_inode afs parentdir vnode  (mode OR s_IFREG) ;
   case r of
     Error (afs, vnode) \<Rightarrow> return ((afs, parentdir, vnode), Error eNFile)
   | Success (afs, vnode) \<Rightarrow> do
   r \<leftarrow> read_afs_inode afs (v_ino parentdir);
   case r of
      Error e \<Rightarrow> return ((afs, parentdir, vnode), Error e)
    | Success dir \<Rightarrow> do
     r  \<leftarrow> return (Success $ i_dir_update (\<lambda>d. d(\<alpha>wa name \<mapsto> v_ino vnode)) dir) \<sqinter> return (Error eNameTooLong);
     case r of
       Error e \<Rightarrow>  return ((afs, parentdir, vnode), Error e)
     | Success dir \<Rightarrow> do
   r \<leftarrow> select (Success ` {sz. sz > v_size parentdir }) \<sqinter> (return (Error eOverflow));
   case r of
     Error e \<Rightarrow>  return ((afs, parentdir, vnode), Error e)
    | Success newsz \<Rightarrow> do
   time \<leftarrow> return (v_ctime vnode);
   dir \<leftarrow> return (dir\<lparr>i_ctime:=time, i_mtime:=time\<rparr>);
   inode  \<leftarrow> return (afs_inode_from_vnode vnode);
   (afs, r) \<leftarrow> afs_update afs (\<lambda>f. f(i_ino inode \<mapsto> inode, i_ino dir \<mapsto> dir));
   case r of
     Error e \<Rightarrow> return ((afs, parentdir, vnode), Error e)
   | Success () \<Rightarrow>
      return ((afs, parentdir \<lparr> v_ctime := time, v_mtime := time, v_size := newsz \<rparr>, vnode), Success ())
      od
     od
    od
   od
 od"

text {* Sync can return an error non-deterministicaly. The only restriction
is that @{term afs_sync} can only return successfully if the list of updates is
empty. As the user expects, when calling sync all the updates related to an
inode should be synchronised to disk.
*}
definition
  afs_sync :: "afs_state \<Rightarrow> (afs_state \<times> (unit,ErrCode) R\<^sub>T) cogent_monad"
where
"afs_sync afs \<equiv>
  if a_is_readonly afs then
    return (afs, Error eRoFs)
  else do
    n \<leftarrow> select {0..length (a_medium_updates afs)};
    let updates = a_medium_updates afs;
        (to_apply, updates) = (take n updates,drop n updates);
        afs = a_medium_afs_update (fold (\<lambda>upd med. upd med) to_apply) afs;
        afs = a_medium_updates_update (\<lambda>_. updates) afs
    in if updates = [] then
      return (afs, Success ())
    else do
      e \<leftarrow> select {eIO, eNoMem, eNoSpc,eOverflow};
      return (afs\<lparr>a_is_readonly:= (e = eIO)\<rparr>, Error e)
    od
  od" 

(* Assumptions:  "v_ino parentdir \<in> dom (a_medium_afs (a_afs_updated afs))" 
                In other words, the v_inode for the parent dir must be represented in the afs data structure.
  nlinks of vnode < MaxWord -1
 *)

definition
  afs_unlink :: "afs_state \<Rightarrow> vnode \<Rightarrow> U8 WordArray \<Rightarrow> vnode \<Rightarrow>
                   ((afs_state \<times> vnode \<times> vnode) \<times> (unit, ErrCode) R\<^sub>T) cogent_monad"
where
  "afs_unlink afs parentdir name vnode \<equiv>
    do
     r \<leftarrow> error_if_readonly afs;
     case r of
       Error (e, afs) \<Rightarrow> return ((afs, parentdir, vnode), Error e)
     | Success afs \<Rightarrow> do
     (afs, time) \<leftarrow> afs_get_current_time afs;
     (* We need to use updated afs because inode might contain data blocks *)
     inode  \<leftarrow> return ((the $ updated_afs afs (v_ino vnode))\<lparr>i_nlink:= v_nlink vnode - 1, i_ctime:= time\<rparr>) ;
     newsize \<leftarrow> select {sz. sz < v_size parentdir};
     dir_ino \<leftarrow> return (v_ino parentdir);
     (afs, r) \<leftarrow> afs_update afs (\<lambda>f. f(dir_ino \<mapsto> (i_dir_update (\<lambda>d. d(\<alpha>wa name:=option.None)) (the $ f dir_ino)\<lparr>i_ctime:=time,i_mtime:=time\<rparr>),
                                            v_ino vnode \<mapsto> inode));
       case r of
         Error e \<Rightarrow>
          return ((afs, parentdir, vnode), Error e)
       | Success () \<Rightarrow>
         let vnode' = vnode \<lparr> v_nlink := v_nlink vnode - 1, v_ctime:= time\<rparr>;
             parentdir' = parentdir \<lparr> v_ctime := time, v_mtime := time, v_size := newsize \<rparr>
         in return ((afs, parentdir', vnode'), Success ())
     od
  od"

definition
  afs_iget :: "afs_state \<Rightarrow> Ino \<Rightarrow> vnode \<Rightarrow> (vnode \<times> (unit, ErrCode) R\<^sub>T) cogent_monad"
where
 "afs_iget afs inum vnode \<equiv>
  (if inum \<in> dom (updated_afs afs) then
    do
      r \<leftarrow> read_afs_inode afs inum;
      case r of
       Success inode \<Rightarrow>
        (* update vnode with inode *)
        return (afs_inode_to_vnode inode, Success ())
      | Error e \<Rightarrow>
       return (vnode, Error e)
    od
  else return (vnode, Error eNoEnt))
  "

definition
  afs_lookup :: "afs_state \<Rightarrow> vnode \<Rightarrow> U8 WordArray \<Rightarrow> ((Ino, ErrCode) R\<^sub>T) cogent_monad"
where
  "afs_lookup afs vdir name \<equiv>
   if wordarray_length name > bilbyFsMaxNameLen + 1 then
     return (Error eNameTooLong)
   else
   do
      r \<leftarrow> read_afs_inode afs (v_ino vdir);
   case r of
      Error e \<Rightarrow> return (Error e)
    | Success dir \<Rightarrow>
      (case i_dir dir (\<alpha>wa name) of
         None \<Rightarrow> return (Error eNoEnt)
       | Some ino \<Rightarrow> return (Success ino))
    od"

definition
  afs_link :: "afs_state \<Rightarrow> vnode \<Rightarrow> U8 WordArray \<Rightarrow> vnode \<Rightarrow>
                   ((afs_state \<times> vnode \<times> vnode) \<times> (unit, ErrCode) R\<^sub>T) cogent_monad"
where
  "afs_link afs parentdir name vnode \<equiv>
  if a_is_readonly afs then
    return ((afs, parentdir, vnode), Error eRoFs)
   else do
   r \<leftarrow> read_afs_inode afs (v_ino parentdir);
   case r of
      Error e \<Rightarrow> return ((afs, parentdir, vnode), Error e)
    | Success dir \<Rightarrow> do
     r  \<leftarrow> return (Success $ i_dir_update (\<lambda>d. d(\<alpha>wa name \<mapsto> v_ino vnode)) dir) \<sqinter> return (Error eNameTooLong);
     case r of
       Error e \<Rightarrow>  return ((afs, parentdir, vnode), Error e)
     | Success dir \<Rightarrow> do
   r \<leftarrow> select (Success ` {sz. sz > v_size parentdir }) \<sqinter> (return (Error eOverflow));
   case r of
     Error e \<Rightarrow>  return ((afs, parentdir, vnode), Error e)
    | Success newsz \<Rightarrow> do
   time \<leftarrow> return (v_ctime vnode);
   dir \<leftarrow> return (dir\<lparr>i_ctime:=time, i_mtime:=time, i_size := newsz\<rparr>);
   (* We need to use updated_afs because vnode might contain data blocks *)
   inode  \<leftarrow> return (the $ updated_afs afs (v_ino vnode));
   (afs, r) \<leftarrow> afs_update afs (\<lambda>f. f(i_ino inode \<mapsto> inode, i_ino dir \<mapsto> dir));
   case r of
     Error e \<Rightarrow> return ((afs, parentdir, vnode), Error e)
   | Success () \<Rightarrow>
      return ((afs, parentdir \<lparr> v_ctime := time, v_mtime := time, v_size := newsz \<rparr>, vnode \<lparr>v_nlink:= v_nlink vnode + 1\<rparr>), Success ())
      od
     od
    od
   od"

definition
  afs_mkdir :: "afs_state \<Rightarrow> vnode \<Rightarrow> U8 WordArray \<Rightarrow> VfsMode \<Rightarrow> vnode \<Rightarrow>
                   ((afs_state \<times> vnode \<times> vnode) \<times> (unit, ErrCode) R\<^sub>T) cogent_monad"
where
  "afs_mkdir afs parentdir name mode vnode \<equiv>
  if a_is_readonly afs then
    return ((afs, parentdir, vnode), Error eRoFs)
   else do
   r \<leftarrow> afs_init_inode afs parentdir vnode  (mode OR s_IFDIR) ;
   case r of
     Error (afs, vnode) \<Rightarrow> return ((afs, parentdir, vnode), Error eNFile)
   | Success (afs, vnode) \<Rightarrow> do
   r \<leftarrow> read_afs_inode afs (v_ino parentdir);
   case r of
      Error e \<Rightarrow> return ((afs, parentdir, vnode), Error e)
    | Success dir \<Rightarrow> do
     r  \<leftarrow> return (Success $ i_dir_update (\<lambda>d. d(\<alpha>wa name \<mapsto> v_ino vnode)) dir) \<sqinter> return (Error eNameTooLong);
     case r of
       Error e \<Rightarrow>  return ((afs, parentdir, vnode), Error e)
     | Success dir \<Rightarrow> do
   r \<leftarrow> select (Success ` {sz. sz > v_size parentdir }) \<sqinter> (return (Error eOverflow));
   case r of
     Error e \<Rightarrow>  return ((afs, parentdir, vnode), Error e)
    | Success newsz \<Rightarrow>
  do
   time \<leftarrow> return (v_ctime vnode);
   dir \<leftarrow> return (dir\<lparr>i_ctime:=time, i_mtime:=time, i_nlink := i_nlink dir + 1, i_size := newsz\<rparr>);
   vnode \<leftarrow> return (vnode \<lparr> v_nlink := 2\<rparr>);
   inode  \<leftarrow> return (afs_inode_from_vnode vnode);
   (afs, r) \<leftarrow> afs_update afs (\<lambda>f. f(i_ino inode \<mapsto> inode, i_ino dir \<mapsto> dir));
   case r of
     Error e \<Rightarrow> return ((afs, parentdir, vnode), Error e)
   | Success () \<Rightarrow>
      return ((afs, parentdir \<lparr>v_nlink:= v_nlink parentdir + 1, v_ctime := time, v_mtime := time, v_size := newsz \<rparr>, vnode), Success ())
      od
     od
    od
   od
 od"

definition
  afs_rmdir :: "afs_state \<Rightarrow> vnode \<Rightarrow> U8 WordArray \<Rightarrow> vnode \<Rightarrow>
                   ((afs_state \<times> vnode \<times> vnode) \<times> (unit, ErrCode) R\<^sub>T) cogent_monad"
where
  "afs_rmdir afs parentdir name vnode \<equiv>
    do
     r \<leftarrow> error_if_readonly afs;
     case r of
       Error (e, afs) \<Rightarrow> return ((afs, parentdir, vnode), Error e)
     | Success afs \<Rightarrow> 
     if dom (i_dir (the $ updated_afs afs (v_ino vnode))) \<noteq> {} then
       return ((afs, parentdir, vnode), Error eNotEmpty)
     else
     do
     (afs, time) \<leftarrow> afs_get_current_time afs;
     vnode' \<leftarrow> return (vnode \<lparr> v_nlink := 0 \<rparr>);
     (* no need to use updated afs since vnode must be an empty dir *)
     inode  \<leftarrow> return (afs_inode_from_vnode vnode);
     newsize \<leftarrow> select {sz. sz < v_size parentdir};
     dir_ino \<leftarrow> return (v_ino parentdir);
     parentdir' \<leftarrow> return (parentdir \<lparr> v_nlink := v_nlink parentdir - 1, v_ctime := time, v_mtime := time, v_size := newsize \<rparr>);
     (afs, r) \<leftarrow> afs_update afs (\<lambda>f. f(dir_ino \<mapsto> (i_dir_update (\<lambda>d. d(\<alpha>wa name:=option.None)) (the $ f dir_ino)\<lparr>i_ctime:=time,i_mtime:=time, i_nlink:= v_nlink parentdir'\<rparr>),
                                            v_ino vnode \<mapsto> inode));
       case r of
         Error e \<Rightarrow> return ((afs, parentdir, vnode), Error e)
       | Success () \<Rightarrow>
         return ((afs, parentdir', vnode'), Success ())
     od
  od"

definition
  afs_symlink :: "afs_state \<Rightarrow> vnode \<Rightarrow> U8 WordArray \<Rightarrow> U8 WordArray \<Rightarrow> VfsMode \<Rightarrow> vnode \<Rightarrow>
                   ((afs_state \<times> vnode \<times> vnode) \<times> (unit, ErrCode) R\<^sub>T) cogent_monad"
where
  "afs_symlink afs parentdir name symname mode vnode \<equiv>
  if a_is_readonly afs then
    return ((afs, parentdir, vnode), Error eRoFs)
  else if wordarray_length symname > bilbyFsBlockSize then
     return ((afs, parentdir, vnode), Error eNameTooLong)
   else do
   r \<leftarrow> afs_init_inode afs parentdir vnode  (mode OR s_IFLNK OR s_IRWXUGO) ;
   case r of
     Error (afs, vnode) \<Rightarrow> return ((afs, parentdir, vnode), Error eNFile)
   | Success (afs, vnode) \<Rightarrow> do
   r \<leftarrow> read_afs_inode afs (v_ino parentdir);
   case r of
      Error e \<Rightarrow> return ((afs, parentdir, vnode), Error e)
    | Success dir \<Rightarrow> do
     r  \<leftarrow> return (Success $ i_dir_update (\<lambda>d. d(\<alpha>wa name \<mapsto> v_ino vnode)) dir) \<sqinter> return (Error eNameTooLong);
     case r of
       Error e \<Rightarrow>  return ((afs, parentdir, vnode), Error e)
     | Success dir \<Rightarrow> do
   r \<leftarrow> select (Success ` {sz. sz > v_size parentdir }) \<sqinter> (return (Error eOverflow));
   case r of
     Error e \<Rightarrow>  return ((afs, parentdir, vnode), Error e)
    | Success newsz \<Rightarrow> do
   time \<leftarrow> return (v_ctime vnode);
   vnode \<leftarrow> return (vnode \<lparr> v_size := ucast $ wordarray_length symname \<rparr>);
   dir \<leftarrow> return (dir\<lparr>i_ctime:=time, i_mtime:=time, i_size := v_size vnode\<rparr>);
   inode \<leftarrow> return (afs_inode_from_vnode vnode);
   inode \<leftarrow> return (i_path_update (\<lambda>_. \<alpha>wa symname) inode);
   (afs, r) \<leftarrow> afs_update afs (\<lambda>f. f(i_ino inode \<mapsto> inode, i_ino dir \<mapsto> dir));
   case r of
     Error e \<Rightarrow> return ((afs, parentdir, vnode), Error e)
   | Success () \<Rightarrow>
      return ((afs, parentdir \<lparr> v_ctime := time, v_mtime := time, v_size := newsz \<rparr>, vnode), Success ())
      od
     od
    od
   od
 od"

definition
  pad_block :: "U8 list \<Rightarrow> U32 \<Rightarrow> U8 list"
where
 "pad_block data len \<equiv> data @ drop (length data) (replicate (unat len) 0)"

(* No support for holes for now *)

definition
  afs_readpage :: "afs_state \<Rightarrow> vnode \<Rightarrow> U64 \<Rightarrow> U8 WordArray \<Rightarrow>
                   ((afs_state \<times> vnode \<times> U8 WordArray) \<times> (unit, ErrCode) R\<^sub>T) cogent_monad"
where
  "afs_readpage afs vnode block buf \<equiv>
   if block > (v_size vnode >> unat bilbyFsBlockShift) then
    return ((afs, vnode, WordArrayT.make (replicate (unat bilbyFsBlockSize) 0)), Error eNoEnt)
   else if (block = (v_size vnode >> unat bilbyFsBlockShift)) \<and> ((v_size vnode) mod (ucast bilbyFsBlockSize) = 0)
        then return ((afs, vnode, buf), Success ())
        else do
          err \<leftarrow> {eIO, eNoMem, eInval, eBadF, eNoEnt};
          return ((afs, vnode, WordArrayT.make (pad_block ((i_data (the $ updated_afs afs (v_ino vnode))) ! unat block) bilbyFsBlockSize)), Success ()) \<sqinter> return ((afs, vnode, buf), Error err)
          od
"

definition
  afs_write_begin :: "afs_state \<Rightarrow> vnode \<Rightarrow> U64 \<Rightarrow> U32 \<Rightarrow> U8 WordArray \<Rightarrow>
                   ((afs_state \<times> vnode \<times> U8 WordArray) \<times> (unit, ErrCode) R\<^sub>T) cogent_monad"
where
  "afs_write_begin afs vnode pos len buf \<equiv>
  if a_is_readonly afs then
    return ((afs, vnode, buf), Error eRoFs)
  else 
    do
     ((afs, vnode, buf'), r) \<leftarrow> afs_readpage afs vnode (pos >> unat bilbyFsBlockShift) buf;
    case r of
      Error e \<Rightarrow> 
      return ((afs, vnode, buf'), if e = eNoEnt then Success () else Error e)
    | Success () \<Rightarrow>
      return ((afs, vnode, buf'), Success())
    od
"

definition
  afs_write_end :: "afs_state \<Rightarrow> vnode \<Rightarrow> U64 \<Rightarrow> U32 \<Rightarrow> U8 WordArray \<Rightarrow>
                   ((afs_state \<times> vnode) \<times> (unit, ErrCode) R\<^sub>T) cogent_monad"
where
  "afs_write_end afs vnode pos len addr \<equiv>
  if a_is_readonly afs then
    return ((afs, vnode), Error eRoFs)
  else 
    do
      newsize \<leftarrow> return (max (v_size vnode) (pos + ucast len));
      (afs, time) \<leftarrow> afs_get_current_time afs;
      vnode' \<leftarrow> return (vnode \<lparr> v_size:= newsize, v_mtime := time\<rparr>);
      block \<leftarrow> return (unat $ pos >> unat bilbyFsBlockShift);
      (afs, r) \<leftarrow> afs_update afs (\<lambda>f. f(v_ino vnode \<mapsto> i_data_update (\<lambda>data. data[block:= \<alpha>wa addr]) (the $ f (v_ino vnode)) \<lparr> i_size:= newsize \<rparr>));
       case r of
         Error e \<Rightarrow> return ((afs, vnode), Error e)
       | Success () \<Rightarrow>
         return ((afs, vnode'), Success())
    od
"

definition
  afs_evict_inode :: "afs_state \<Rightarrow> vnode \<Rightarrow>
                   (afs_state \<times> (unit, ErrCode) R\<^sub>T) cogent_monad"
where
  "afs_evict_inode afs vnode \<equiv>
  if a_is_readonly afs then
    return (afs, Error eRoFs)
  else 
    if v_nlink vnode \<noteq> 0 then
      return (afs, Success ())
    else 
     afs_update afs (\<lambda>f. f(v_ino vnode:= None))
"

definition
  afs_follow_link :: "afs_state \<Rightarrow> vnode \<Rightarrow> U8 WordArray \<Rightarrow>
                   ((afs_state \<times> vnode \<times> U8 WordArray) \<times> (unit, ErrCode) R\<^sub>T) cogent_monad"
where
  "afs_follow_link afs vnode path \<equiv>
  do
   r \<leftarrow> read_afs_inode afs (v_ino vnode);
   case r of
    Error e \<Rightarrow>
     return ((afs, vnode, path), Error e)
   | Success inode \<Rightarrow>
     let wa_path = WordArrayT.make (i_path inode);
         updated_path = wordarray_copy (path, wa_path, 0, 0, ucast (i_size inode))
     in return ((afs, vnode, updated_path), Success ())
   od
"

definition
  afs_rename :: "afs_state \<Rightarrow> vnode \<Rightarrow> U8 WordArray \<Rightarrow> vnode \<Rightarrow> U8 WordArray \<Rightarrow> vnode option \<Rightarrow>
                   ((afs_state \<times> vnode \<times> vnode \<times> vnode option) \<times> (unit, ErrCode) R\<^sub>T) cogent_monad"
where
  "afs_rename afs vdir oldname oldvnode newname onewvnode \<equiv>
  if a_is_readonly afs then
    return ((afs, vdir, oldvnode, onewvnode), Error eRoFs)
  else do
    old_is_dir \<leftarrow> return ( S_ISDIR (v_mode oldvnode));
    ncnt \<leftarrow> return (if old_is_dir then v_nlink oldvnode - 1 else v_nlink oldvnode);
    oldvnode' \<leftarrow> return (oldvnode \<lparr> v_nlink := ncnt \<rparr>);
    oldinode  \<leftarrow> return ((the $ updated_afs afs (v_ino oldvnode))\<lparr> i_nlink := ncnt \<rparr>);
    (afs, time) \<leftarrow> afs_get_current_time afs;
    newsz \<leftarrow> select UNIV;
    r \<leftarrow> read_afs_inode afs (v_ino vdir);
    case r of
    Error e \<Rightarrow> return ((afs, vdir, oldvnode, onewvnode), Error e)    
    | Success dir \<Rightarrow> do
    r  \<leftarrow> return (Success $ i_dir_update (\<lambda>d. d(\<alpha>wa oldname := None, 
                    \<alpha>wa newname := Some (v_ino oldvnode) )) dir) \<sqinter> return (Error eNameTooLong);
    case r of
     Error e \<Rightarrow> return ((afs, vdir, oldvnode, onewvnode), Error e)
    | Success dir \<Rightarrow> do
    dir \<leftarrow> return (dir\<lparr>i_ctime:=time, i_mtime:=time, i_size := newsz\<rparr>);   
    (case onewvnode of
    Some newvnode \<Rightarrow>
     let newinode = the $ updated_afs afs (v_ino newvnode);
         new_is_dir = afs_inode_is_dir (i_type newinode) 
     in if new_is_dir \<and> dom (i_dir newinode) \<noteq> {} then
         return ((afs, vdir, oldvnode, onewvnode), Error eNotEmpty)
      else
        do
         ncnt \<leftarrow> return (if new_is_dir then 0 else v_nlink newvnode - 1);
         newvnode' \<leftarrow> return (newvnode \<lparr> v_nlink := ncnt \<rparr>);
         newinode \<leftarrow> return (newinode \<lparr> i_nlink := ncnt \<rparr>);
         (afs, r) \<leftarrow> afs_update afs (\<lambda>f. f(i_ino oldinode \<mapsto> oldinode, i_ino dir \<mapsto> dir,
                                           i_ino newinode \<mapsto> newinode));
         case r of
           Error e \<Rightarrow> return ((afs, vdir, oldvnode, onewvnode), Error e)
         | Success () \<Rightarrow>
           let vdir' = vdir \<lparr> v_mtime := time, v_ctime := time, v_size := newsz \<rparr>
           in return ((afs, vdir', oldvnode', Some newvnode'), Success ())
       od
      | None \<Rightarrow>
        do
         (afs, r) \<leftarrow> afs_update afs (\<lambda>f. f(i_ino oldinode \<mapsto> oldinode, i_ino dir \<mapsto> dir));
         case r of
           Error e \<Rightarrow> return ((afs, vdir, oldvnode, onewvnode), Error e)
         | Success () \<Rightarrow>
           let vdir' = vdir \<lparr> v_mtime := time, v_ctime := time, v_size := newsz \<rparr>
           in return ((afs, vdir', oldvnode', None), Success ())
        od)
     od
  od
od
"

definition
  afs_move :: "afs_state \<Rightarrow> vnode \<Rightarrow> U8 WordArray \<Rightarrow> vnode \<Rightarrow> vnode \<Rightarrow> U8 WordArray \<Rightarrow> vnode option \<Rightarrow>
                   ((afs_state \<times> vnode \<times> vnode \<times> vnode \<times> vnode option) \<times> (unit, ErrCode) R\<^sub>T) cogent_monad"
where
  "afs_move afs oldvdir oldname oldvnode newvdir newname onewvnode \<equiv>
  if a_is_readonly afs then
    return ((afs, oldvdir, oldvnode, newvdir, onewvnode), Error eRoFs)
  else do
    old_is_dir \<leftarrow> return (S_ISDIR (v_mode oldvnode));
    ncnt \<leftarrow> return (if old_is_dir then v_nlink oldvnode - 1 else v_nlink oldvnode);
    oldvnode' \<leftarrow> return (oldvnode \<lparr> v_nlink := ncnt \<rparr>);
    oldinode  \<leftarrow> return ((the $ updated_afs afs (v_ino oldvnode))\<lparr> i_nlink := ncnt \<rparr>);
    (afs, time) \<leftarrow> afs_get_current_time afs;
    r \<leftarrow> read_afs_inode afs (v_ino oldvdir);
    case r of
    Error e \<Rightarrow> return ((afs, oldvdir, oldvnode, newvdir, onewvnode), Error e)    
    | Success olddir \<Rightarrow> do
    r  \<leftarrow> return (Success $ i_dir_update (\<lambda>d. d(\<alpha>wa oldname := None,
                    \<alpha>wa newname := Some (v_ino oldvnode) )) olddir) \<sqinter> return (Error eNameTooLong);
    case r of
     Error e \<Rightarrow> return ((afs, oldvdir, oldvnode, newvdir, onewvnode), Error e)
    | Success olddir \<Rightarrow> do
    onewsz \<leftarrow> select {sz. sz < v_size oldvdir};
    olddir \<leftarrow> return (olddir\<lparr>i_ctime:=time, i_mtime:=time, i_size := onewsz\<rparr>);   
    oldvdir' \<leftarrow> return (oldvdir \<lparr> v_mtime := time, v_ctime := time, v_size := onewsz \<rparr>);

    r \<leftarrow> read_afs_inode afs (v_ino newvdir);
    case r of
    Error e \<Rightarrow> return ((afs, oldvdir, oldvnode, newvdir, onewvnode), Error e)    
    | Success newdir \<Rightarrow> do
    r  \<leftarrow> return (Success $ i_dir_update (\<lambda>d. d(\<alpha>wa newname := Some (v_ino oldvnode) )) newdir)
          \<sqinter> return (Error eNameTooLong);
    case r of
     Error e \<Rightarrow> return ((afs, oldvdir, oldvnode, newvdir, onewvnode), Error e)
    | Success newdir \<Rightarrow> do
    nnewsz \<leftarrow> select {sz. sz > v_size newvdir};

    ncnt \<leftarrow> return (if old_is_dir then v_nlink newvdir + 1 else v_nlink newvdir);
    newvdir' \<leftarrow> return (newvdir \<lparr>v_ctime:=time, v_mtime:=time, v_nlink := ncnt, v_size := nnewsz \<rparr>);
    newdir \<leftarrow> return (newdir\<lparr>i_ctime:=time, i_mtime:=time, i_nlink := ncnt, i_size := nnewsz\<rparr>);

    (case onewvnode of
    Some newvnode \<Rightarrow>
     let newinode = the $ updated_afs afs (v_ino newvnode);
         new_is_dir = afs_inode_is_dir (i_type newinode) 
     in if new_is_dir \<and> dom (i_dir newinode) \<noteq> {} then
         return ((afs, oldvdir, oldvnode, newvdir, onewvnode), Error eNotEmpty)
      else
        do
         ncnt \<leftarrow> return (if new_is_dir then 0 else v_nlink newvnode - 1);
         newvnode' \<leftarrow> return (newvnode \<lparr> v_nlink := ncnt \<rparr>);
         newinode \<leftarrow> return (newinode \<lparr> i_nlink := ncnt \<rparr>);


         (afs, r) \<leftarrow> afs_update afs (\<lambda>f. f(i_ino oldinode \<mapsto> oldinode, i_ino olddir \<mapsto> olddir,
                                           i_ino newdir \<mapsto> newdir, i_ino newinode \<mapsto> newinode));
         case r of
           Error e \<Rightarrow> return ((afs, oldvdir, oldvnode, newvdir, onewvnode), Error e)
         | Success () \<Rightarrow>
           return ((afs, oldvdir', oldvnode', newvdir', Some newvnode'), Success ())
       od
      | None \<Rightarrow>
        do
         (afs, r) \<leftarrow> afs_update afs (\<lambda>f. f(i_ino oldinode \<mapsto> oldinode, i_ino olddir \<mapsto> olddir,
                                           i_ino newdir \<mapsto> newdir));
         case r of
           Error e \<Rightarrow> return ((afs, oldvdir, oldvnode, newvdir, onewvnode), Error e)
         | Success () \<Rightarrow>
           return ((afs, oldvdir', oldvnode', newvdir', None), Success ())
        od)
      od
    od
    od
    od
  od"

definition
  afs_dir_emit :: "readdir_ctx \<Rightarrow> U8 WordArray \<Rightarrow> Ino \<Rightarrow> VfsType  \<Rightarrow> ((readdir_ctx, readdir_ctx) LoopResult\<^sub>T) cogent_monad"
where
 "afs_dir_emit \<equiv> (\<lambda>(pos, entries) name ino vtype.
  do bool \<leftarrow> select UNIV;
    if bool then
      return (Iterate (pos, entries(\<alpha>wa name:= None)))
    else
      return (Break (pos, entries (\<alpha>wa name:= None)))
  od)
 "
(* VFS detects when readdir is called twice without removing
any entry from the readdir context. *)
definition
  afs_readdir :: "afs_state \<Rightarrow> readdir_ctx \<Rightarrow> BilbyFsReaddirContext\<^sub>T option \<Rightarrow> vnode \<Rightarrow> ((afs_state \<times> readdir_ctx \<times> BilbyFsReaddirContext\<^sub>T option) \<times> (unit, ErrCode) R\<^sub>T) cogent_monad"
where
  "afs_readdir afs rdctx obrdctx vdir =
    do
     r \<leftarrow> read_afs_inode afs (v_ino vdir);
     case r of
      Error e \<Rightarrow> return ((afs, rdctx, obrdctx), Error e)  
     | Success dir \<Rightarrow> do
      toemit \<leftarrow> select {entries. entries \<subseteq> dom (i_dir dir) };
      obrdctx \<leftarrow> select UNIV;
      pos \<leftarrow> select UNIV;
      return ((afs, (pos, (snd rdctx)|`(-toemit)), obrdctx),
                Success ())
    od
  od"

record vfsstat =
  vs_ino :: Ino
  vs_nlink :: U32
  vs_mode :: Mode
  vs_uid :: U32
  vs_gid :: U32
  vs_size :: U64
  vs_atime :: TimeT 
  vs_mtime :: TimeT
  vs_ctime :: TimeT
  vs_blksize :: U32
  vs_blocks :: U32

definition
  afs_getattr :: "afs_state \<Rightarrow> vfsstat \<Rightarrow> vnode \<Rightarrow> ((afs_state \<times> vfsstat)) cogent_monad"
where                                
  "afs_getattr afs stat vnode \<equiv>
   return (afs, stat
    \<lparr> vs_ino := v_ino vnode,
      vs_nlink := v_nlink vnode,
      vs_mode := v_mode vnode,
      vs_uid := v_uid vnode,
      vs_gid := v_gid vnode,
      vs_size := v_size vnode,
      vs_atime := v_mtime vnode,
      vs_mtime := v_mtime vnode,
      vs_ctime := v_ctime vnode,
      vs_blksize := bilbyFsBlockSize,
      vs_blocks := ucast (v_size vnode) div 512 + (if v_size vnode mod 512 > 0 then 1 else 0)
    \<rparr>)
    "

record iattr =
 iattr_valid :: U32
 iattr_mode :: Mode
 iattr_uid :: U32
 iattr_gid :: U32
 iattr_mtime :: TimeT
 iattr_ctime :: TimeT

definition iattr_is_set :: "iattr \<Rightarrow> U32 \<Rightarrow> bool"
where
 "iattr_is_set iattr flag \<equiv> iattr_valid iattr AND flag \<noteq> 0"
 
definition
  afs_setattr :: "afs_state \<Rightarrow> iattr \<Rightarrow> vnode \<Rightarrow> ((afs_state \<times> vnode) \<times> (unit, ErrCode) R\<^sub>T) cogent_monad"
where
  "afs_setattr afs iattr vnode \<equiv> 
  let 
    vnode' = (if iattr_is_set iattr vfs_ATTR_MODE then vnode \<lparr> v_mode := iattr_mode iattr \<rparr> else vnode);
    vnode' = (if iattr_is_set iattr vfs_ATTR_UID then vnode' \<lparr> v_uid := iattr_uid iattr \<rparr> else vnode');
    vnode' = (if iattr_is_set iattr vfs_ATTR_GID then vnode' \<lparr> v_gid := iattr_gid iattr \<rparr> else vnode');
    vnode' = (if iattr_is_set iattr vfs_ATTR_MTIME then vnode' \<lparr> v_mtime := iattr_mtime iattr \<rparr> else vnode');
    vnode' = (if iattr_is_set iattr vfs_ATTR_CTIME then vnode' \<lparr> v_ctime := iattr_ctime iattr \<rparr> else vnode')
  in do
    (afs, r) \<leftarrow> afs_update afs (\<lambda>f. f(v_ino vnode' \<mapsto>
      the (f(v_ino vnode'))\<lparr>i_mode:= v_mode vnode', i_uid := v_uid vnode', i_gid := v_gid vnode',
         i_mtime := v_mtime vnode', i_ctime := v_ctime vnode'\<rparr>));
    case r of
      Error e \<Rightarrow> return ((afs, vnode), Error e)
    | Success () \<Rightarrow>
      return ((afs, vnode'), Success())
   od"

end