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 a⇩₀i :: "'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 a⇩₀i, uncurry0 (RETURN (PR_CONST a⇩₀))) ∈ unit_assn⇧^k →⇩_a A"
    "(uncurry Lei,uncurry (RETURN oo PR_CONST (⊴))) ∈ A⇧^k *⇩_a A⇧^k →⇩_a bool_assn"
    "(succsi,RETURN o PR_CONST succs) ∈ A⇧^k →⇩_a list_assn A"
    "(keyi,RETURN o PR_CONST key) ∈ A⇧^k →⇩_a K"
    "(copyi, RETURN o COPY) ∈ A⇧^k →⇩_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 \<^term>‹insert_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,a⇩₀);
    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' a⇩₀ = 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_assn⇧^k *⇩_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 a⇩₀" "PR_CONST (⊴)" "PR_CONST succs" "PR_CONST key"

lemma [def_pat_rules]:
  "a⇩₀ ≡ UNPROTECT a⇩₀" "(⊴) ≡ 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_assn⇧^d →⇩_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_assn⇧^k →⇩_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_assn⇧^k →⇩_a bool_assn"
  unfolding hm.hms_fold_custom_empty by sepref

sepref_definition dfs_map'_impl is
  "uncurry dfs_map'"
  :: "A⇧^d *⇩_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 a⇩₀"
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 a⇩₀›]
  also note dfs_correct[OF ‹V a⇩₀› ‹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. a⇩₀ →* x ∧ x →⇧⁺ x))"
  if "V a⇩₀"
  supply dfs_map_empty[OF ‹V a⇩₀›, 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 a⇩₀i Lei keyi copyi),
    uncurry0 (SPEC (λr. r = (∃x. a⇩₀ →* x ∧ x →⇧⁺ x)))
   ) ∈ unit_assn⇧^k →⇩_a bool_assn" if "V a⇩₀"
  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 a⇩₀›
      ] .

lemma dfs_map_impl'_hoare_triple:
  "<↑(V a⇩₀)> 
    dfs_map_impl' succsi a⇩₀i Lei keyi copyi 
  <λr. ↑(r ⟷ (∃ x. a⇩₀ →* 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 *)