Theory EPAC_Perfectly_Shared_Vars

theory EPAC_Perfectly_Shared_Vars
  imports EPAC_Perfectly_Shared
    PAC_Checker.PAC_Checker_Relation
    PAC_Checker.PAC_Map_Rel
begin
thm import_variableS_def
  term hm.assn
  term iam.assn
  term is_iam
  term iam_rel

type_synonym ('string2, 'nat) shared_vars_c = ‹'string2 list × ('string2, 'nat) fmap›

definition perfect_shared_vars_rel_c :: ‹('string2 × 'string) set ⇒ (('string2, nat) shared_vars_c × (nat, 'string)shared_vars) set› where
  ‹perfect_shared_vars_rel_c R =
  {((𝒱, 𝒜), (𝒟', 𝒱', 𝒜')). (∀i∈#dom_m 𝒱'. i < length 𝒱) ∧
  (∀i∈#dom_m 𝒱'. i < length 𝒱 ∧ (𝒱 ! i, the (fmlookup 𝒱' i))∈ R) ∧
  (𝒜, 𝒜') ∈ ⟨R,nat_rel⟩fmap_rel}›

text ‹Random conditions with the idea to use machine words eventually›

definition find_new_idx_c :: ‹('string, nat) shared_vars_c ⇒ (memory_allocation × nat)  nres› where
  ‹find_new_idx_c = (λ(𝒱, 𝒜). let k = length 𝒱 in if k < 2^63-1 then RETURN (Allocated, k) else RETURN (Mem_Out, 0) )›

definition insert_variable_c :: ‹'string ⇒ nat ⇒ ('string, nat) shared_vars_c ⇒ ('string, nat) shared_vars_c›  where
  ‹insert_variable_c v k' = (λ(𝒱, 𝒜). (𝒱 @ [v], fmupd v k' 𝒜))›

definition import_variable_c :: ‹'string ⇒  ('string, nat) shared_vars_c ⇒ (memory_allocation × ('string, nat) shared_vars_c × nat)  nres› where
  ‹import_variable_c v = (λ(𝒱𝒜). do {
  (err, k') ← find_new_idx_c (𝒱𝒜);
  if alloc_failed err then do {let k'=k'; RETURN (err, (𝒱𝒜), k')}
  else do{
    ASSERT(k' < 2^63-1);
    RETURN (Allocated, insert_variable_c v k' 𝒱𝒜, k')
    }
    })›

lemma import_variable_c_alt_def:
  ‹import_variable_c v = (λ(𝒱, 𝒜). do {
  (err, k') ← find_new_idx_c (𝒱, 𝒜);
  if alloc_failed err then do {let k'=k'; RETURN (err, (𝒱, 𝒜), k')}
  else do{
    ASSERT(k' < 2^63-1);
    RETURN (Allocated, (𝒱 @ [v], fmupd v k' 𝒜), k')
    }
    })›
  unfolding import_variable_c_def insert_variable_c_def
  by auto


lemma import_variable_c_import_variableS:
  fixes A' :: ‹(nat,'string) shared_vars›
  assumes
    A: ‹(A,A')∈perfect_shared_vars_rel_c R› and
    v: ‹(v,v')∈R› ‹single_valued R› ‹single_valued (R¯)›
  shows ‹import_variable_c v A ≤⇓(Id ×r (perfect_shared_vars_rel_c R ×r nat_rel)) (import_variableS v' A')›
proof -
  have [refine]: ‹RETURN x2g ≤ ⇓ Id (RES UNIV)› for x2g :: nat
    by auto
  have [refine]: ‹find_new_idx_c a ≤ ⇓ {((err, k), (err', k')). err=err' ∧ k=k' ∧ (¬alloc_failed err ⟶ k < 2^63-1 ∧ k = length (fst a))} (find_new_idx b)›
    if ‹(a,b) ∈ perfect_shared_vars_rel_c R›
    for b :: ‹(nat,'string) shared_vars› and a
    using that unfolding find_new_idx_c_def find_new_idx_def
    by (cases b; cases a)
      (auto intro!: RETURN_RES_refine simp: Let_def perfect_shared_vars_rel_c_def)

  show ?thesis
    unfolding import_variable_c_alt_def import_variableS_def find_new_idx_def[symmetric]
    apply refine_vcg
    subgoal using A by (auto simp: perfect_shared_vars_rel_c_def)
    subgoal by auto
    subgoal using A by (auto simp: perfect_shared_vars_rel_c_def)
    subgoal by auto
    subgoal
      using A v by (force simp: perfect_shared_vars_rel_c_def dest: in_diffD intro!: fmap_rel_fmupd_fmap_rel)
   done
qed


definition is_new_variable_c :: ‹'string ⇒ ('string, 'nat) shared_vars_c ⇒ bool nres› where
  ‹is_new_variable_c v = (λ(𝒱, 𝒱').
  RETURN (v ∉# dom_m 𝒱')
  )›

lemma fset_fmdom_dom_m: ‹fset (fmdom A) = set_mset (dom_m A)›
  by (simp add: dom_m_def)

lemma fmap_rel_nat_rel_dom_m_iff:
  ‹(A, B) ∈ ⟨R, S⟩fmap_rel ⟹ (v,v')∈R ⟹ v∈#dom_m A ⟷v'∈# dom_m B›
  by (auto simp: fmap_rel_alt_def distinct_mset_dom fset_fmdom_dom_m
    dest!: multi_member_split
    simp del: fmap_rel_nat_the_fmlookup)


lemma is_new_variable_c_is_new_variableS:
  shows ‹(uncurry is_new_variable_c, uncurry is_new_variableS) ∈ R ×r perfect_shared_vars_rel_c R →f ⟨bool_rel⟩nres_rel›
  by (use  in ‹auto simp: perfect_shared_vars_rel_c_def fmap_rel_nat_rel_dom_m
    fmap_rel_nat_rel_dom_m_iff is_new_variable_c_def is_new_variableS_def
    intro!: frefI nres_relI›)


definition get_var_pos_c :: ‹ ('string, nat) shared_vars_c ⇒ _ ⇒ nat nres› where
  ‹get_var_pos_c = (λ(xs, 𝒱) x. do {
    ASSERT(x ∈# dom_m 𝒱);
    RETURN (the (fmlookup 𝒱 x))
  })›


lemma get_var_pos_c_get_var_posS:
  fixes A' :: ‹(nat,'string) shared_vars›
  assumes
    V: ‹single_valued R› ‹single_valued (R¯)›
  shows ‹(uncurry get_var_pos_c, uncurry get_var_posS) ∈ perfect_shared_vars_rel_c R ×r R →f ⟨nat_rel⟩nres_rel›
  unfolding get_var_pos_c_def get_var_posS_def uncurry_def
    apply (clarify intro!: frefI nres_relI)
  apply refine_vcg
  subgoal using assms by (auto simp: perfect_shared_vars_rel_c_def fmap_rel_nat_rel_dom_m_iff)
  subgoal
    using assms by (auto simp: perfect_shared_vars_rel_c_def fmap_rel_nat_rel_dom_m_iff dest: fmap_rel_fmlookup_rel)
  done



definition get_var_name_c :: ‹ ('string, nat) shared_vars_c ⇒ nat ⇒ 'string nres› where
  ‹get_var_name_c = (λ(xs, 𝒱) x. do {
    ASSERT(x < length xs);
    RETURN (xs ! x)
  })›


lemma get_var_name_c_get_var_nameS:
  fixes A' :: ‹(nat,'string) shared_vars›
  assumes
    V: ‹single_valued R› ‹single_valued (R¯)›
  shows ‹(uncurry get_var_name_c, uncurry get_var_nameS) ∈ perfect_shared_vars_rel_c R ×r Id →f ⟨R⟩nres_rel›
  unfolding get_var_name_c_def get_var_nameS_def uncurry_def
    apply (clarify intro!: frefI nres_relI)
  apply refine_vcg
  subgoal using assms by (auto dest!: multi_member_split simp: perfect_shared_vars_rel_c_def)
  subgoal
    using assms by (auto simp: perfect_shared_vars_rel_c_def fmap_rel_nat_rel_dom_m_iff
      dest: multi_member_split)
  done

abbreviation perfect_shared_vars_assn :: ‹(string, nat) shared_vars_c ⇒ _ ⇒ assn› where
  ‹perfect_shared_vars_assn ≡ arl_assn string_assn ×a hm_fmap_assn string_assn uint64_nat_assn›
abbreviation shared_vars_assn where
  ‹shared_vars_assn ≡ hr_comp perfect_shared_vars_assn (perfect_shared_vars_rel_c Id)›

lemmas [sepref_fr_rules] = hm.lookup_hnr[FCOMP op_map_lookup_fmlookup]

sepref_definition get_var_pos_c_impl
  is ‹uncurry get_var_pos_c›
  :: ‹perfect_shared_vars_assnk *a string_assnk →a uint64_nat_assn›
  supply [simp] = in_dom_m_lookup_iff
  unfolding get_var_pos_c_def fmlookup'_def[symmetric]
  by sepref

sepref_definition is_new_variable_c_impl
  is ‹uncurry is_new_variable_c›
  :: ‹string_assnk  *a  perfect_shared_vars_assnk →a bool_assn›
  supply [simp] = in_dom_m_lookup_iff
  unfolding is_new_variable_c_def fmlookup'_def[symmetric] in_dom_m_lookup_iff
  by sepref

definition nth_uint64 where
  ‹nth_uint64 = (!)›

definition arl_get' :: ‹'a::heap array_list ⇒ integer ⇒ 'a Heap› where
  [code del]: ‹arl_get' a i = arl_get a (nat_of_integer i)›

definition arl_get_u :: ‹'a::heap array_list ⇒ uint64 ⇒ 'a Heap› where
  ‹arl_get_u ≡ λa i. arl_get' a (integer_of_uint64 i)›

lemma arl_get_hnr_u[sepref_fr_rules]:
  assumes ‹CONSTRAINT is_pure A›
  shows ‹(uncurry arl_get_u, uncurry (RETURN ∘∘ op_list_get))
     ∈ [pre_list_get]a (arl_assn A)k *a uint64_nat_assnk → A›
proof -
  obtain A' where
    A: ‹pure A' = A›
    using assms pure_the_pure by auto
  then have A': ‹the_pure A = A'›
    by auto
  have [simp]: ‹the_pure (λa c. ↑ ((c, a) ∈ A')) = A'›
    unfolding pure_def[symmetric] by auto
  show ?thesis
    by sepref_to_hoare
      (sep_auto simp: uint64_nat_rel_def br_def array_assn_def is_array_def
        hr_comp_def list_rel_pres_length param_nth arl_assn_def
        A' A[symmetric] pure_def arl_get_u_def Array.nth'_def arl_get'_def
     nat_of_uint64_code[symmetric])
qed


definition arl_get_u' where
  [symmetric, code]: ‹arl_get_u' = arl_get_u›

lemma arl_get'_nth'[code]: ‹arl_get' = (λ(a, n). Array.nth' a)›
  unfolding arl_get_def arl_get'_def Array.nth'_def
  by (intro ext) auto

definition nat_of_uint64_s :: ‹nat ⇒ nat› where
  [simp]: ‹nat_of_uint64_s x = x›

lemma [refine]:
  ‹(return o nat_of_uint64, RETURN o nat_of_uint64_s) ∈ uint64_nat_assnk →a nat_assn›
  by (sepref_to_hoare)
    (sep_auto simp: uint64_nat_rel_def br_def)


sepref_definition get_var_name_c_impl
  is ‹uncurry get_var_name_c›
  :: ‹perfect_shared_vars_assnk *a uint64_nat_assnk →a string_assn›
  supply [simp] = in_dom_m_lookup_iff
  unfolding get_var_name_c_def fmlookup'_def[symmetric]
  by sepref

lemma [sepref_fr_rules]:
  ‹(uncurry is_new_variable_c_impl, uncurry is_new_variableS) ∈ string_assnk *a shared_vars_assnk →a bool_assn›
  using is_new_variable_c_impl.refine[FCOMP is_new_variable_c_is_new_variableS, of Id]
  by auto

lemma [sepref_fr_rules]:
  ‹(uncurry get_var_pos_c_impl, uncurry get_var_posS) ∈ shared_vars_assnk *a string_assnk →a uint64_nat_assn›
  using get_var_pos_c_impl.refine[FCOMP get_var_pos_c_get_var_posS, of Id]
  by auto

lemma [sepref_fr_rules]:
  ‹(uncurry get_var_name_c_impl, uncurry get_var_nameS) ∈ shared_vars_assnk *a  uint64_nat_assnk →a string_assn›
  using get_var_name_c_impl.refine[FCOMP get_var_name_c_get_var_nameS, of Id]
 by auto

sepref_register get_var_nameS get_var_posS is_new_variableS


abbreviation memory_allocation_rel :: ‹(memory_allocation × memory_allocation) set› where
  ‹memory_allocation_rel ≡ Id›

abbreviation memory_allocation_assn :: ‹memory_allocation ⇒ memory_allocation ⇒ assn› where
  ‹memory_allocation_assn ≡ id_assn›

instantiation memory_allocation :: default
begin
  definition default_memory_allocation :: ‹memory_allocation› where
    ‹default_memory_allocation = Allocated›
instance
  ..
end

term import_polyS
lemma [sepref_import_param]:
  ‹(Allocated, Allocated) ∈ memory_allocation_rel›
  ‹(Mem_Out, Mem_Out) ∈ memory_allocation_rel›
  ‹(alloc_failed, alloc_failed) ∈ memory_allocation_rel → bool_rel›
  by auto

lemma pow_2_63_1: ‹2 ^ 63 - 1 = (9223372036854775807 :: nat)›
  by auto
definition zero_uint64_nat where
  ‹zero_uint64_nat = 0›
sepref_register zero_uint64_nat
lemma [sepref_fr_rules]:
  ‹(uncurry0 (return 0), uncurry0 (RETURN zero_uint64_nat))∈unit_assnk →a uint64_nat_assn›
  unfolding zero_uint64_nat_def uint64_nat_rel_def br_def
  by sepref_to_hoare sep_auto

definition length_uint64_nat where
 [simp]: ‹length_uint64_nat = length›

definition length_arl_u_code :: ‹('a::heap) array_list ⇒ uint64 Heap› where
  ‹length_arl_u_code xs = do {
   n ← arl_length xs;
  return (uint64_of_nat n)}›

definition uint64_max :: nat where
  ‹uint64_max = 2 ^64 - 1›

lemma nat_of_uint64_uint64_of_nat: ‹b ≤ uint64_max ⟹ nat_of_uint64 (uint64_of_nat b) = b›
  unfolding uint64_of_nat_def uint64_max_def
  apply simp
  apply transfer
  by (auto simp: take_bit_nat_eq_self)

lemma length_arl_u_hnr[sepref_fr_rules]:
  ‹(length_arl_u_code, RETURN o length_uint64_nat) ∈
     [λxs. length xs ≤ uint64_max]a (arl_assn R)k → uint64_nat_assn›
  by sepref_to_hoare
    (sep_auto simp: uint64_nat_rel_def
      length_arl_u_code_def arl_assn_def nat_of_uint64_uint64_of_nat
      arl_length_def hr_comp_def is_array_list_def list_rel_pres_length[symmetric]
      br_def)

lemma find_new_idx_c_alt_def:
  ‹find_new_idx_c = (λ(𝒱, 𝒜). let k = length 𝒱 in if k < 2^63-1 then RETURN (Allocated, length_uint64_nat 𝒱) else RETURN (Mem_Out, 0) )›
  unfolding find_new_idx_c_def Let_def by auto


sepref_definition find_new_idx_c_impl
  is ‹find_new_idx_c›
  :: ‹perfect_shared_vars_assnk →aid_assn ×a uint64_nat_assn›
  supply [simp] = uint64_max_def
  unfolding find_new_idx_c_alt_def pow_2_63_1 zero_uint64_nat_def[symmetric]
  by sepref

instantiation String.literal :: default
begin
definition default_literal :: ‹String.literal› where
  ‹default_literal = String.implode ''''›
instance
  ..
end

sepref_definition insert_variable_c_impl
  is ‹uncurry2 (RETURN ooo insert_variable_c)›
  :: ‹string_assnk *a uint64_nat_assnk *a perfect_shared_vars_assnd →a perfect_shared_vars_assn›
  supply arl_append_hnr[sepref_fr_rules]
    marl_append_hnr[sepref_fr_rules del]
  unfolding insert_variable_c_def
  by sepref

lemmas [sepref_fr_rules] =
  find_new_idx_c_impl.refine insert_variable_c_impl.refine

sepref_definition import_variable_c_impl
  is ‹uncurry import_variable_c›
  :: ‹string_assnk *a perfect_shared_vars_assnd →a id_assn ×a perfect_shared_vars_assn ×a uint64_nat_assn›
  unfolding import_variable_c_def
  by sepref

lemma import_variable_c_import_variableS':
  assumes ‹single_valued R› ‹single_valued (R¯)›
  shows ‹(uncurry import_variable_c, uncurry import_variableS) ∈ R ×r perfect_shared_vars_rel_c R →f
    ⟨memory_allocation_rel ×r perfect_shared_vars_rel_c R ×r nat_rel⟩nres_rel›
  using import_variable_c_import_variableS[OF _ _ assms]
  by (auto intro!: frefI nres_relI)


lemma [sepref_fr_rules]:
  ‹(uncurry import_variable_c_impl, uncurry import_variableS)
  ∈ string_assnk *a  shared_vars_assnd →a memory_allocation_assn ×a shared_vars_assn ×a uint64_nat_assn›
  using import_variable_c_impl.refine[FCOMP import_variable_c_import_variableS', of Id]
 by auto

definition empty_shared_vars :: ‹(nat, string) shared_vars› where
  ‹empty_shared_vars =  ({#}, fmempty, fmempty)›


definition empty_shared_vars_int :: ‹(string, nat) shared_vars_c› where
  ‹empty_shared_vars_int =  ([], fmempty)›

sepref_definition empty_shared_vars_int_impl
  is ‹uncurry0 (RETURN empty_shared_vars_int)›
  :: ‹unit_assnk →a perfect_shared_vars_assn›
  unfolding empty_shared_vars_int_def
    arl.fold_custom_empty
  by sepref

lemma empty_shared_vars_int_empty_shared_vars:
  ‹(uncurry0 (RETURN empty_shared_vars_int), uncurry0 (RETURN empty_shared_vars)) ∈ unit_rel →f ⟨perfect_shared_vars_rel_c R⟩nres_rel›
  by (auto intro!: frefI nres_relI simp: perfect_shared_vars_rel_c_def empty_shared_vars_int_def
    empty_shared_vars_def)

lemma [sepref_fr_rules]:
  ‹(uncurry0 empty_shared_vars_int_impl, uncurry0 (RETURN empty_shared_vars))
  ∈ unit_assnk →a shared_vars_assn›
  using empty_shared_vars_int_impl.refine[FCOMP empty_shared_vars_int_empty_shared_vars, of Id]
  by auto
sepref_register empty_shared_vars
end