(*
 * 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 FsopSyncR
imports
  "../lib/CogentCorres"
  "../refine/AfsFsopR"
  "../refine/OstoreR"
begin

definition
 rsync_res :: "(afs_state \<times> (unit,ErrCode) R\<^sub>T) \<Rightarrow> FsopFsP\<^sub>T \<times> (32 word, unit) R \<Rightarrow> bool"
where
 "rsync_res \<equiv> (\<lambda>(afs, ra) (fsr, rc). ra = rc \<and> afs_fsop_rel afs (FsopFsP.fs_st\<^sub>f fsr))"

lemmas rsync_simp = rsync_res_def afs_fsop_rel_def Let_def 
   afmsu_def afs_fsop_match_step_updates_def match_afs_data_fs_state_def

lemma fold_comp[rule_format]:
  "xs = ys @ zs \<longrightarrow> fold f xs accu = (fold f zs (fold f ys accu))"
  by (induct_tac xs, simp+)

lemma corres_sync_err:
"afs_fsop_rel afs fs_st \<Longrightarrow>
 cogent_corres rsync_res (return (afs, R.Error e)) (\<lparr>FsopFsP.ex\<^sub>f = ex, fs_st\<^sub>f = fs_st\<rparr>, R.Error e)"
  by (simp add: rsync_res_def cogent_corres_def  return_def)

lemma length_updates_eqD:
 "afs_fsop_rel afs fs_st \<Longrightarrow>
 length (\<alpha>_updates (FsState.ostore_st\<^sub>f fs_st)) = length (a_medium_updates afs)"
 by (clarsimp simp: rsync_simp)

lemma afs_fsop_match_updates:
 "afs_fsop_match (fold id xs' a) (fold id ys' c) \<Longrightarrow> xs' = xs \<Longrightarrow> ys' = ys \<Longrightarrow>
  afs_fsop_match (fold id xs a) (fold id ys c)"
by simp

lemma updates_take_eq:
 "na \<le> (length xs - n) \<Longrightarrow>
  n \<le> length xs \<Longrightarrow>
  length xs = length ys \<Longrightarrow>
  take (min (length ys) n + min (length (drop n ys)) na) xs =
    take n xs @ take na (drop n xs)"
  by (simp add: min_absorb2 take_add)

lemma refine_sync:
notes length_drop[simp del]
assumes rel:"afs_fsop_rel afs fs_st"
shows
  "\<And>ex. cogent_corres rsync_res
         (afs_sync afs) (fsop_sync_fs (FsopFsP.make ex fs_st))"
  unfolding afs_sync_def fsop_sync_fs_def[simplified tuple_simps sanitizers, folded eIO_def]
using [[goals_limit=5]]
  apply (rule cogent_corres_conc_let_exec, simp only: prod.case_eq_if)
  apply (rule cogent_corres_conc_let_exec, simp only: prod.case_eq_if)
  apply (rule cogent_corres_if)
    apply (simp add: FsopFsP.make_def)
    apply (fold eRoFs_def)
    apply (rule corres_sync_err[OF rel])
   apply (rule cogent_corres_conc_let_exec, simp only: prod.case_eq_if)
   apply (rule cogent_corres_conc_let_exec, simp only: prod.case_eq_if)
   apply (simp only:  FsopFsP.defs)
   apply (fold ostoreWriteNone_def)

   apply (rule ostore_sync_ret)
       using rel apply (simp add: rsync_simp)
      using rel apply (simp add: rsync_simp)
     using rel apply (simp add: rsync_simp)
     apply (clarsimp)
    apply (rule_tac v="length (a_medium_updates afs)" in cogent_corres_select, simp)
    apply (simp add: Let_def)
    apply (rule cogent_corres_return)
    using rel apply (clarsimp simp add: rsync_simp prod.case_eq_if)
    apply (erule_tac x="length (a_medium_updates afs)" in allE)
    apply (clarsimp simp: updated_afs_def id_def a_afs_updated_def \<alpha>_ostore_uptodate_def)
    apply (drule afs_inv_steps_updated_afsD)
    apply (simp add: afs_inv_steps_def updated_afs_def a_afs_updated_def id_def)
   apply clarsimp
   apply (rule_tac v="n" in cogent_corres_select)
    apply (simp)
    using length_updates_eqD[OF rel]
    apply simp
   using length_updates_eqD[OF rel]
   apply (simp add: Let_def)
   apply (rule_tac v="e" in cogent_corres_select, simp)
   apply (rule cogent_corres_return)
   using rel apply (clarsimp simp add: rsync_simp updated_afs_def)
    apply (rule conjI)
    apply (simp add: afs_inv_steps_def updated_afs_def a_afs_updated_def id_def)
     apply (fold id_def)
     apply clarsimp
     apply (subst fold_comp[symmetric], rule refl)+
     apply (erule_tac x="n+na" in allE)
     apply (fastforce simp add: take_add length_drop)
   apply (rule conjI)
    using length_updates_eqD[OF rel]
    apply (fastforce simp add: length_drop)
   apply clarsimp
    apply (rename_tac na)
    apply (erule_tac x="n + na" in allE)
    apply (erule impE)
     apply (drule sym[where s="length _" and t = "length _"])
     apply (simp only: length_drop)
     apply (subst fold_comp[symmetric], rule refl)+
     apply (erule afs_fsop_match_updates)
     apply (fastforce simp only: take_add)+
   using rel
   apply (simp add: rsync_simp FsopFsP.defs)
 done
end