Theory Extract_Certificate

section ‹Extracting Certificates From \munta›

theory Extract_Certificate
  imports
    Worklist_Algorithms.Unified_PW_Impl
    Worklist_Algorithms.Next_Key
    Difference_Bound_Matrices.DBM_Operations_Impl_Refine
    Worklist_Algorithms.Leadsto_Impl
begin

subsection ‹Turning a map into a list›

definition list_of_map where
  "list_of_map m ≡ do
      {
        (xs, m) ← WHILEIT
          (λ (xs, m'). finite (dom m') ∧ m = m' ++ map_of xs ∧ dom m' ∩ dom (map_of xs) = {})
             (λ (_, m). Map.empty ≠ m)
            (λ (xs, m). do
              {
                k ← next_key m;
                let (x, m) = op_map_extract k m;
                ASSERT (x ≠ None);
                RETURN ((k, the x) # xs, m)
              }
            )
            ([], m);
        RETURN xs
      }
  "

context
begin

private definition
  "ran_of_map_var = (inv_image (measure (card o dom)) (λ (a, b). b))"

private lemma wf_ran_of_map_var:
  "wf ran_of_map_var"
  unfolding ran_of_map_var_def by auto

private lemma insert_restrict_ran:
  "insert v (ran (m |` (- {k}))) = ran m " if "m k = Some v"
  using that unfolding ran_def restrict_map_def by force

private lemma 1:
  "(m |` (- {x}))(x ↦ y) = m" if "m x = Some y"
  using that unfolding restrict_map_def by auto

private lemma 2:
  "(m1 ++ m2)(x ↦ y) = m1(x ↦ y) ++ m2" if "x ∉ dom m2"
  using that by auto

lemma list_of_map_correct[refine]:
  "list_of_map m ≤ SPEC (λ r. map_of r = m)" if "finite (dom m)"
  using that unfolding list_of_map_def next_key_def
  apply (refine_vcg wf_ran_of_map_var)
         apply (clarsimp; fail)+
  subgoal for s xs m' x v xs' xs1 xs'1
    unfolding dom_def apply (clarsimp simp: map_upd_eq_restrict)
    apply (subst 2, solves auto)
    apply (subst 1)
     apply auto
    done
  unfolding ran_of_map_var_def by (fastforce intro: card_Diff1_less split: if_split_asm)+

end ― ‹End of private context for auxiliary facts and definitions›

context
  fixes K :: "_ ⇒ _ :: {hashable, heap} ⇒ assn"
  assumes is_pure_K[safe_constraint_rules]: "is_pure K"
  and left_unique_K[safe_constraint_rules]: "IS_LEFT_UNIQUE (the_pure K)"
  and right_unique_K[safe_constraint_rules]: "IS_RIGHT_UNIQUE (the_pure K)"
  notes [sepref_fr_rules] = hm_it_next_key_next_key''[OF is_pure_K]
begin

sepref_definition list_of_map_impl is
  "list_of_map" :: "(hm.hms_assn' K A)d →a (list_assn (K ×a A))"
  unfolding list_of_map_def hm.hms_assn'_id_hms_assn[symmetric]
  unfolding op_map_is_empty_def[symmetric]
  unfolding hm.hms_fold_custom_empty HOL_list.fold_custom_empty
  by sepref

end (* Anonymous context for setup *)

lemmas list_of_map_impl_code[code] =
  list_of_map_impl_def[of "pure Id", simplified, OF Sepref_Constraints.safe_constraint_rules(41)]

context
  notes [sepref_fr_rules] = hm_it_next_key_next_key'[folded hm.hms_assn'_id_hms_assn]
begin

sepref_definition list_of_map_impl' is
  "list_of_map" :: "(hm.hms_assn A)d →a (list_assn (id_assn ×a A))"
  unfolding list_of_map_def hm.hms_assn'_id_hms_assn[symmetric]
  unfolding op_map_is_empty_def[symmetric]
  unfolding hm.hms_fold_custom_empty HOL_list.fold_custom_empty
  by sepref

end (* Anonymous context for setup *)

context Worklist_Map2_Impl
begin

definition extract_certificate :: "_ nres" where
  "extract_certificate = do {
   (_, passed) ← pw_algo_map2;
   list_of_map passed
  }"

context
begin

private definition
  "pw_algo_map2_copy = pw_algo_map2"

sepref_register pw_algo_map2_copy

lemma pw_algo_map2_copy_fold:
  "PR_CONST pw_algo_map2_copy = pw_algo_map2"
  unfolding pw_algo_map2_copy_def by simp

lemmas [sepref_fr_rules] =
  pw_algo_map2_impl.refine_raw[folded pw_algo_map2_copy_fold]
  list_of_map_impl.refine[OF pure_K left_unique_K right_unique_K]

sepref_thm extract_certificate_impl is
  "uncurry0 extract_certificate" :: "unit_assnk →a (list_assn (K ×a lso_assn A))"
  unfolding extract_certificate_def pw_algo_map2_copy_def[symmetric] by sepref

end

end

concrete_definition extract_certificate_impl
  uses Worklist_Map2_Impl.extract_certificate_impl.refine_raw

end