Theory Liveness_Subsumption_Impl

subsection ‹Imperative Implementation›

theory Liveness_Subsumption_Impl
  imports Liveness_Subsumption_Map Heap_Hash_Map Worklist_Algorithms_Tracing
begin

no_notation Ref.update (‹_ := _› 62)

locale Liveness_Search_Space_Key_Impl_Defs =
  Liveness_Search_Space_Key_Defs _ _ _ _ _ _ key for key :: "'a  'k" +
  fixes A :: "'a  ('ai :: heap)  assn"
  fixes succsi :: "'ai  'ai list Heap"
  fixes a0i :: "'ai Heap"
  fixes Lei :: "'ai  'ai  bool Heap"
  fixes keyi :: "'ai  'ki :: {hashable, heap} Heap"
  fixes copyi :: "'ai  'ai Heap"

locale Liveness_Search_Space_Key_Impl =
  Liveness_Search_Space_Key_Impl_Defs +
  Liveness_Search_Space_Key +
  fixes K
  assumes pure_K[safe_constraint_rules]: "is_pure K"
    assumes left_unique_K[safe_constraint_rules]: "IS_LEFT_UNIQUE (the_pure K)"
    assumes right_unique_K[safe_constraint_rules]: "IS_RIGHT_UNIQUE (the_pure K)"
  assumes refinements[sepref_fr_rules]:
    "(uncurry0 a0i, uncurry0 (RETURN (PR_CONST a0)))  unit_assnk a A"
    "(uncurry Lei,uncurry (RETURN oo PR_CONST (⊴)))  Ak *a Ak a bool_assn"
    "(succsi,RETURN o PR_CONST succs)  Ak a list_assn A"
    "(keyi,RETURN o PR_CONST key)  Ak a K"
    "(copyi, RETURN o COPY)  Ak a A"

context Liveness_Search_Space_Key_Defs
begin

― ‹The lemma has this form to avoid unwanted eta-expansions.
  The eta-expansions arise from the type of terminsert_map_set v S.›
lemma insert_map_set_alt_def: "((), insert_map_set v S) = (
  let
    k = key v; (S', S) = op_map_extract k S
  in
    case S' of
      Some S1  ((), S(k  (insert v S1)))
    | None  ((), S(k  {v}))
)
"
  unfolding insert_map_set_def op_map_extract_def by (auto simp: Let_def split: option.split)

lemma check_subsumption_map_set_alt_def: "check_subsumption_map_set v S = (
  let
    k = key v; (S', S) = op_map_extract k S;
    S1' = (case S' of Some S1  S1 | None  {})
  in ( x  S1'. v  x)
)
"
  unfolding check_subsumption_map_set_def op_map_extract_def by (auto simp: Let_def)

lemma check_subsumption_map_set_extract: "(S, check_subsumption_map_set v S) = (
  let
    k = key v; (S', S) = op_map_extract k S
  in (
    case S' of
      Some S1  (let r = ( x  S1. v  x) in (op_map_update k S1 S, r))
    | None  (S, False)
  )
)
"
  unfolding check_subsumption_map_set_def op_map_extract_def op_map_update_def op_map_delete_def
  by (auto simp: Let_def split: option.split)

lemma check_subsumption_map_list_extract: "(S, check_subsumption_map_list v S) = (
  let
    k = key v; (S', S) = op_map_extract k S
  in (
    case S' of
      Some S1  (let r = ( x  set S1. x  v) in (op_map_update k S1 S, r))
    | None  (S, False)
  )
)
"
  unfolding check_subsumption_map_list_def op_map_extract_def op_map_update_def op_map_delete_def
  by (auto simp: Let_def split: option.split)

lemma push_map_list_alt_def: "((), push_map_list v S) = (
  let
    k = key v; (S', S) = op_map_extract k S
  in
    case S' of
      Some S1  ((), S(k  v # S1))
    | None  ((), S(k  [v]))
)
"
  unfolding push_map_list_def op_map_extract_def by (auto simp: Let_def split: option.split)

― ‹The check for emptiness may be superfluous if we thread through the pre-condition›
lemma pop_map_list_alt_def: "((), pop_map_list v S) = (
  let
    k = key v; (S', S) = op_map_extract k S
  in
    case S' of
      Some S1  ((), S(k  if op_list_is_empty S1 then [] else tl S1))
    | None  ((), S(k  []))
)
"
  unfolding pop_map_list_def op_map_extract_def by (auto simp: Let_def split: option.split)

lemmas alt_defs =
  insert_map_set_alt_def check_subsumption_map_set_extract
  check_subsumption_map_list_extract pop_map_list_alt_def push_map_list_alt_def

lemma dfs_map_alt_def:
  "dfs_map = (λ P. do {
    (P,ST,r)  RECT (λdfs (P,ST,v).
      let (ST, b) = (ST, check_subsumption_map_list v ST) in
      if b then RETURN (P, ST, True)
      else do {
        let (P, b1) = (P, check_subsumption_map_set v P) in
        if b1 then
          RETURN (P, ST, False)
        else do {
            let (_, ST1) = ((), push_map_list (COPY v) ST);
            (P1, ST2, r) 
              nfoldli (succs v) (λ(_,_,b). ¬b) (λv' (P,ST,_). dfs (P,ST,v')) (P,ST1,False);
            let (_, ST') = ((), pop_map_list (COPY v) ST2);
            let (_, P')  = ((), insert_map_set (COPY v) P1);
            TRACE (ExploredState);
            RETURN (P', ST', r)
          }
      }
    ) (P,Map.empty,a0);
    RETURN (r, P)
  })"
  unfolding dfs_map_def
  unfolding Let_def
  unfolding COPY_def
  unfolding TRACE_bind
  by auto

definition dfs_map' where
  "dfs_map' a P  do {
    (P,ST,r)  RECT (λdfs (P,ST,v).
      let (ST, b) = (ST, check_subsumption_map_list v ST) in
      if b then RETURN (P, ST, True)
      else do {
        let (P, b1) = (P, check_subsumption_map_set v P) in
        if b1 then
          RETURN (P, ST, False)
        else do {
            let (_, ST1) = ((), push_map_list (COPY v) ST);
            (P1, ST2, r) 
              nfoldli (succs v) (λ(_,_,b). ¬b) (λv' (P,ST,_). dfs (P,ST,v')) (P,ST1,False);
            let (_, ST') = ((), pop_map_list (COPY v) ST2);
            let (_, P')  = ((), insert_map_set (COPY v) P1);
            TRACE (ExploredState);
            RETURN (P', ST', r)
          }
      }
    ) (P,Map.empty,a);
    RETURN (r, P)
  }"

lemma dfs_map'_id:
  "dfs_map' a0 = dfs_map"
  apply (subst dfs_map_alt_def)
  unfolding dfs_map'_def TRACE_bind ..

end (* Search Space Nodes Empty Key Impl Defs 1 *)

definition (in imp_map_delete) [code_unfold]: "hms_delete = delete"

lemma (in imp_map_delete) hms_delete_rule [sep_heap_rules]:
  "<hms_assn A m mi> hms_delete k mi <hms_assn A (m(k := None))>t"
  unfolding hms_delete_def hms_assn_def
  apply (sep_auto eintros del: exI)
  subgoal for mh
    apply (rule exI[where x = "mh(k := None)"])
    apply (rule ent_frame_fwd[OF map_assn_delete[where A = A]], frame_inference)
    by (sep_auto simp: map_upd_eq_restrict)
  done

context imp_map_delete
begin

lemma hms_delete_hnr:
  "(uncurry hms_delete, uncurry (RETURN oo op_map_delete)) 
  id_assnk *a (hms_assn A)d a hms_assn A"
  by sepref_to_hoare sep_auto

sepref_decl_impl delete: hms_delete_hnr uses op_map_delete.fref[where V = Id] .

end

lemma fold_insert_set:
  "fold insert xs S = set xs  S"
  by (induction xs arbitrary: S) auto

lemma set_alt_def:
  "set xs = fold insert xs {}"
  by (simp add: fold_insert_set)

context Liveness_Search_Space_Key_Impl
begin

sepref_register
  "PR_CONST a0" "PR_CONST (⊴)" "PR_CONST succs" "PR_CONST key"

lemma [def_pat_rules]:
  "a0  UNPROTECT a0" "(⊴)  UNPROTECT (⊴)" "succs  UNPROTECT succs" "key  UNPROTECT key"
  by simp_all

abbreviation "passed_assn  hm.hms_assn' K (lso_assn A)"

(* This is to make the pre-processing phase pick the right type for the input *)
lemma [intf_of_assn]:
  "intf_of_assn (hm.hms_assn' a b) TYPE(('aa, 'bb) i_map)"
  by simp

sepref_definition dfs_map_impl is
  "PR_CONST dfs_map" :: "passed_assnd a prod_assn bool_assn passed_assn"
  unfolding PR_CONST_def
  apply (subst dfs_map_alt_def)
  unfolding TRACE'_def[symmetric]
  unfolding alt_defs
  unfolding Bex_set list_ex_foldli
  unfolding fold_lso_bex
  unfolding lso_fold_custom_empty hm.hms_fold_custom_empty HOL_list.fold_custom_empty
  by sepref

sepref_register dfs_map

lemmas [sepref_fr_rules] = dfs_map_impl.refine_raw

lemma passed_empty_refine[sepref_fr_rules]:
  "(uncurry0 hm.hms_empty, uncurry0 (RETURN (PR_CONST hm.op_hms_empty)))  unit_assnk a passed_assn"
proof -
  have "hn_refine emp hm.hms_empty emp (hm.hms_assn' K (lso_assn A)) (RETURN hm.op_hms_empty)"
    using sepref_fr_rules(17)[simplified] .
  then show ?thesis
    by - (rule hfrefI, auto simp: pure_unit_rel_eq_empty)
qed

sepref_register hm.op_hms_empty

sepref_thm dfs_map_impl' is
  "uncurry0 (do {(r, p)  dfs_map Map.empty; RETURN r})" :: "unit_assnk a bool_assn"
  unfolding hm.hms_fold_custom_empty by sepref

sepref_definition dfs_map'_impl is
  "uncurry dfs_map'"
  :: "Ad *a (hm.hms_assn' K (lso_assn A))d a bool_assn ×a hm.hms_assn' K (lso_assn A)"
  unfolding dfs_map'_def
  unfolding PR_CONST_def TRACE'_def[symmetric]
  unfolding alt_defs
  unfolding Bex_set list_ex_foldli
  unfolding fold_lso_bex
  unfolding lso_fold_custom_empty hm.hms_fold_custom_empty HOL_list.fold_custom_empty
  by sepref

concrete_definition (in -) dfs_map_impl'
  uses Liveness_Search_Space_Key_Impl.dfs_map_impl'.refine_raw is "(uncurry0 ?f,_)_"

lemma (in Liveness_Search_Space_Key) dfs_map_empty:
  "dfs_map Map.empty   (bool_rel ×r map_set_rel) dfs_spec" if "V a0"
proof -
  have "liveness_compatible {}"
    unfolding liveness_compatible_def by auto
  have "(Map.empty, {})  map_set_rel"
    unfolding map_set_rel_def by auto
  note dfs_map_dfs_refine[OF this V a0]
  also note dfs_correct[OF V a0 liveness_compatible {}]
  finally show ?thesis
    by auto
qed

lemma (in Liveness_Search_Space_Key) dfs_map_empty_correct:
  "do {(r, p)  dfs_map Map.empty; RETURN r}  SPEC (λ r. r  ( x. a0 →* x  x + x))"
  if "V a0"
  supply dfs_map_empty[OF V a0, THEN Orderings.order.trans, refine_vcg]
  apply refine_vcg
  unfolding dfs_spec_def pw_le_iff by (auto simp: refine_pw_simps)

lemma dfs_map_impl'_hnr:
  "(uncurry0 (dfs_map_impl' succsi a0i Lei keyi copyi),
    uncurry0 (SPEC (λr. r = (x. a0 →* x  x + x)))
   )  unit_assnk a bool_assn" if "V a0"
  using
    dfs_map_impl'.refine[
      OF Liveness_Search_Space_Key_Impl_axioms,
      FCOMP dfs_map_empty_correct[THEN Id_SPEC_refine, THEN nres_relI],
      OF V a0
      ] .

lemma dfs_map_impl'_hoare_triple:
  "<(V a0)> 
    dfs_map_impl' succsi a0i Lei keyi copyi 
  <λr. (r  ( x. a0 →* x  x + x))>t"
  using dfs_map_impl'_hnr[to_hnr]
  unfolding hn_refine_def
  apply clarsimp
  apply (erule cons_post_rule)
  by (sep_auto simp: pure_def)

end (* Liveness Search Space Key Impl *)

end (* Theory *)