Theory EPAC_Checker_Synthesis

(*
  File:         PAC_Checker_Synthesis.thy
  Author:       Mathias Fleury, Daniela Kaufmann, JKU
  Maintainer:   Mathias Fleury, JKU
*)
theory EPAC_Checker_Synthesis
  imports EPAC_Checker EPAC_Version
    EPAC_Checker_Init
    EPAC_Steps_Refine
    PAC_Checker.More_Loops
    PAC_Checker.WB_Sort PAC_Checker.PAC_Checker_Relation
    PAC_Checker.PAC_Checker_Synthesis
begin
hide_fact (open) PAC_Checker.PAC_checker_l_def
hide_const (open) PAC_Checker.PAC_checker_l

section ‹Code Synthesis of the Complete Checker›

definition check_linear_combi_l_pre_err_impl :: ‹uint64 ⇒ bool ⇒ bool ⇒ bool ⇒ string› where
  ‹check_linear_combi_l_pre_err_impl i adom emptyl ivars =
  ''Precondition for '%' failed '' @ show (nat_of_uint64 i) @
  ''(already in domain: '' @ show adom @
  ''; empty CL'' @ show emptyl @
  ''; new vars: '' @ show ivars @ '')''›

abbreviation comp4 (infixl "oooo" 55) where "f oooo g ≡ λx. f ooo (g x)"

lemma [sepref_fr_rules]:
  ‹(uncurry3 (return oooo check_linear_combi_l_pre_err_impl),
   uncurry3 check_linear_combi_l_pre_err) ∈ uint64_nat_assn⇧k *⇩a bool_assn⇧k *⇩a bool_assn⇧k *⇩a bool_assn⇧k →⇩a raw_string_assn›
  unfolding list_assn_pure_conv check_linear_combi_l_pre_err_impl_def
    check_linear_combi_l_pre_err_def 
  apply sepref_to_hoare
  apply sep_auto
  done

definition check_linear_combi_l_dom_err_impl :: ‹ _ ⇒ uint64 ⇒ string› where
  ‹check_linear_combi_l_dom_err_impl xs i =
  ''Invalid polynomial '' @ show (nat_of_uint64 i)›

lemma [sepref_fr_rules]:
  ‹(uncurry (return oo (check_linear_combi_l_dom_err_impl)),
  uncurry (check_linear_combi_l_dom_err)) ∈ poly_assn⇧k *⇩a uint64_nat_assn⇧k →⇩a raw_string_assn›
  unfolding list_assn_pure_conv check_linear_combi_l_dom_err_impl_def
    check_linear_combi_l_dom_err_def
  apply sepref_to_hoare
  apply sep_auto
  done

definition check_linear_combi_l_mult_err_impl :: ‹ _ ⇒ _ ⇒ string› where
  ‹check_linear_combi_l_mult_err_impl xs ys =
  ''Invalid calculation, found'' @ show xs @ '' instead of '' @ show ys›

lemma [sepref_fr_rules]:
  ‹(uncurry (return oo check_linear_combi_l_mult_err_impl),
  uncurry check_linear_combi_l_mult_err) ∈ poly_assn⇧k *⇩a poly_assn⇧k →⇩a raw_string_assn›
  unfolding list_assn_pure_conv check_linear_combi_l_mult_err_impl_def
    check_linear_combi_l_mult_err_def
  apply sepref_to_hoare
  apply sep_auto
  done

sepref_definition linear_combi_l_impl
  is ‹uncurry3 linear_combi_l›
  :: ‹uint64_nat_assn⇧k *⇩a polys_assn⇧k *⇩a vars_assn⇧k *⇩a (list_assn (poly_assn ×⇩a uint64_nat_assn))⇧k  →⇩a
  poly_assn ×⇩a (list_assn (poly_assn ×⇩a uint64_nat_assn)) ×⇩a status_assn raw_string_assn›
  supply [[goals_limit=1]]
  unfolding linear_combi_l_def  check_linear_combi_l_def conv_to_is_Nil
    term_order_rel'_def[symmetric]
    term_order_rel'_alt_def
    in_dom_m_lookup_iff
    fmlookup'_def[symmetric]
    vars_llist_alt_def is_Nil_def
  unfolding
    HOL_list.fold_custom_empty
  apply (rewrite in ‹(op_HOL_list_empty, _)› annotate_assn[where A=‹poly_assn›])
  by sepref

definition has_failed :: ‹bool nres› where
  ‹has_failed = RES UNIV›

lemma [sepref_fr_rules]:
  ‹(uncurry0 (return False), uncurry0 has_failed)∈unit_assn⇧k →⇩a bool_assn›
  by sepref_to_hoare
    (sep_auto simp: has_failed_def)

declare linear_combi_l_impl.refine[sepref_fr_rules]
  sepref_register check_linear_combi_l_pre_err
sepref_definition check_linear_combi_l_impl
  is ‹uncurry5 check_linear_combi_l›
  :: ‹poly_assn⇧k *⇩a polys_assn⇧k *⇩a vars_assn⇧k *⇩a uint64_nat_assn⇧k *⇩a
        (list_assn (poly_assn ×⇩a uint64_nat_assn))⇧k *⇩a poly_assn⇧k  →⇩a status_assn raw_string_assn›
  supply [[goals_limit=1]]
  unfolding check_mult_l_def  check_linear_combi_l_def conv_to_is_Nil
    term_order_rel'_def[symmetric]
    term_order_rel'_alt_def
    in_dom_m_lookup_iff
    fmlookup'_def[symmetric]
    vars_llist_alt_def is_Nil_def
    has_failed_def[symmetric]
   by sepref

declare check_linear_combi_l_impl.refine[sepref_fr_rules]

sepref_register is_cfailed is_Del

definition PAC_checker_l_step' ::  _ where
  ‹PAC_checker_l_step' a b c d = PAC_checker_l_step a (b, c, d)›

lemma PAC_checker_l_step_alt_def:
  ‹PAC_checker_l_step a bcd e = (let (b,c,d) = bcd in PAC_checker_l_step' a b c d e)›
  unfolding PAC_checker_l_step'_def by auto

sepref_decl_intf ('k) acode_status is "('k) code_status"
sepref_decl_intf ('k, 'b, 'lbl) apac_step is "('k, 'b, 'lbl) pac_step"

sepref_register merge_cstatus full_normalize_poly new_var is_Add
find_theorems is_CL RETURN

sepref_register check_linear_combi_l check_extension_l2
    term check_extension_l2

definition check_extension_l2_cond :: ‹nat ⇒ _› where
  ‹check_extension_l2_cond i A 𝒱 v = SPEC (λb. b ⟶ fmlookup' i A = None ∧ v ∉ 𝒱)›

definition check_extension_l2_cond2 :: ‹nat ⇒ _› where
  ‹check_extension_l2_cond2 i A 𝒱 v = RETURN (fmlookup' i A = None ∧ v ∉ 𝒱)›


sepref_definition check_extension_l2_cond2_impl
  is ‹uncurry3 check_extension_l2_cond2›
    :: ‹uint64_nat_assn⇧k *⇩a polys_assn⇧k *⇩a vars_assn⇧k *⇩a string_assn⇧k →⇩a bool_assn›
  supply [[goals_limit=1]]
  unfolding check_extension_l2_cond2_def
    in_dom_m_lookup_iff
    fmlookup'_def[symmetric]
    not_not is_None_def
  by sepref

lemma check_extension_l2_cond2_check_extension_l2_cond:
  ‹(uncurry3 check_extension_l2_cond2, uncurry3 check_extension_l2_cond) ∈
  (((nat_rel ×⇩r Id) ×⇩r Id) ×⇩r Id) →⇩f ⟨bool_rel⟩nres_rel›
  by (auto intro!: RES_refine nres_relI frefI
    simp: check_extension_l2_cond_def check_extension_l2_cond2_def)

lemmas [sepref_fr_rules] =
  check_extension_l2_cond2_impl.refine[FCOMP check_extension_l2_cond2_check_extension_l2_cond]


definition check_extension_l_side_cond_err_impl :: ‹_ ⇒ _›  where
  ‹check_extension_l_side_cond_err_impl v r s =
    ''Error while checking side conditions of extensions polynow, var is '' @ show v @
    ''side condition p*p - p = '' @ show s @ '' and should be 0''›
term check_extension_l_side_cond_err
lemma [sepref_fr_rules]:
  ‹(uncurry2 (return ooo (check_extension_l_side_cond_err_impl)),
    uncurry2 (check_extension_l_side_cond_err)) ∈ string_assn⇧k *⇩a poly_assn⇧k *⇩a poly_assn⇧k →⇩a raw_string_assn›
   unfolding check_extension_l_side_cond_err_impl_def check_extension_l_side_cond_err_def
     list_assn_pure_conv
   apply sepref_to_hoare
   apply sep_auto
   done

definition check_extension_l_new_var_multiple_err_impl :: ‹_ ⇒ _›  where
  ‹check_extension_l_new_var_multiple_err_impl v p =
    ''Error while checking side conditions of extensions polynow, var is '' @ show v @
    '' but it either appears at least once in the polynomial or another new variable is created '' @
    show p @ '' but should not.''›

lemma [sepref_fr_rules]:
  ‹((uncurry (return oo (check_extension_l_new_var_multiple_err_impl))),
    uncurry (check_extension_l_new_var_multiple_err)) ∈ string_assn⇧k *⇩a poly_assn⇧k →⇩a raw_string_assn›
   unfolding check_extension_l_new_var_multiple_err_impl_def
     check_extension_l_new_var_multiple_err_def
     list_assn_pure_conv
   apply sepref_to_hoare
   apply sep_auto
   done

sepref_definition check_extension_l_impl
  is ‹uncurry5 check_extension_l2›
    :: ‹poly_assn⇧k *⇩a polys_assn⇧k *⇩a vars_assn⇧k *⇩a uint64_nat_assn⇧k *⇩a
    string_assn⇧k *⇩a poly_assn⇧k →⇩a status_assn raw_string_assn›
  supply [[goals_limit=1]]
  unfolding check_extension_l2_def
    in_dom_m_lookup_iff
    fmlookup'_def[symmetric]
    not_not is_None_def
    uminus_poly_def[symmetric]
    HOL_list.fold_custom_empty
    check_extension_l2_cond_def[symmetric]
    vars_llist_alt_def
  by sepref

lemmas [sepref_fr_rules] =
  check_extension_l_impl.refine

lemma is_Mult_lastI:
  ‹¬ is_CL b ⟹ ¬is_Extension b ⟹ is_Del b›
  by (cases b) auto

sepref_definition check_step_impl
  is ‹uncurry4 PAC_checker_l_step'›
  :: ‹poly_assn⇧k *⇩a (status_assn raw_string_assn)⇧d *⇩a vars_assn⇧d *⇩a polys_assn⇧d *⇩a (pac_step_rel_assn (uint64_nat_assn) poly_assn (string_assn :: string ⇒ _))⇧d →⇩a
    status_assn raw_string_assn ×⇩a vars_assn ×⇩a polys_assn›
  supply [[goals_limit=1]] is_Mult_lastI[intro] single_valued_uint64_nat_rel[simp]
  unfolding PAC_checker_l_step_def PAC_checker_l_step'_def
    pac_step.case_eq_if Let_def
     is_success_alt_def[symmetric]
    uminus_poly_def[symmetric]
    HOL_list.fold_custom_empty
  by sepref


declare check_step_impl.refine[sepref_fr_rules]

sepref_register PAC_checker_l_step PAC_checker_l_step' fully_normalize_poly_impl

definition PAC_checker_l' where
  ‹PAC_checker_l' p 𝒱 A status steps = PAC_checker_l p (𝒱, A) status steps›

lemma PAC_checker_l_alt_def:
  ‹PAC_checker_l p 𝒱A status steps =
    (let (𝒱, A) = 𝒱A in PAC_checker_l' p 𝒱 A status steps)›
  unfolding PAC_checker_l'_def by auto


lemma step_rewrite_pure:
  fixes K :: ‹('olbl × 'lbl) set›
  shows
    ‹pure (p2rel (⟨K, V, R⟩pac_step_rel_raw)) = pac_step_rel_assn (pure K) (pure V) (pure R)›
  apply (intro ext)
  apply (case_tac x; case_tac xa)
  apply simp_all
  apply (simp_all add: relAPP_def p2rel_def pure_def)
  unfolding pure_def[symmetric] list_assn_pure_conv
  apply (auto simp: pure_def relAPP_def)
  done

lemma safe_epac_step_rel_assn[safe_constraint_rules]:
  ‹CONSTRAINT is_pure K ⟹ CONSTRAINT is_pure V ⟹ CONSTRAINT is_pure R ⟹
  CONSTRAINT is_pure (EPAC_Checker.pac_step_rel_assn K V R)›
  by (auto simp: step_rewrite_pure(1)[symmetric] is_pure_conv)

sepref_definition PAC_checker_l_impl
  is ‹uncurry4 PAC_checker_l'›
  :: ‹poly_assn⇧k *⇩a vars_assn⇧d *⇩a polys_assn⇧d *⇩a (status_assn raw_string_assn)⇧d *⇩a
       (list_assn (pac_step_rel_assn (uint64_nat_assn) poly_assn string_assn))⇧k →⇩a
     status_assn raw_string_assn ×⇩a vars_assn ×⇩a polys_assn›
  supply [[goals_limit=1]] is_Mult_lastI[intro]
  unfolding PAC_checker_l_def is_success_alt_def[symmetric] PAC_checker_l_step_alt_def
    nres_bind_let_law[symmetric] PAC_checker_l'_def
    conv_to_is_Nil is_Nil_def
  apply (subst nres_bind_let_law)
  by sepref

declare PAC_checker_l_impl.refine[sepref_fr_rules]

abbreviation polys_assn_input where
  ‹polys_assn_input ≡ iam_fmap_assn nat_assn poly_assn›

definition remap_polys_l_dom_err_impl :: ‹_›  where
  ‹remap_polys_l_dom_err_impl =
    ''Error during initialisation. Too many polynomials where provided. If this happens,'' @
    ''please report the example to the authors, because something went wrong during '' @
    ''code generation (code generation to arrays is likely to be broken).''›

lemma [sepref_fr_rules]:
  ‹((uncurry0 (return (remap_polys_l_dom_err_impl))),
    uncurry0 (remap_polys_l_dom_err)) ∈ unit_assn⇧k →⇩a raw_string_assn›
   unfolding remap_polys_l_dom_err_def
     remap_polys_l_dom_err_def
     list_assn_pure_conv
   by sepref_to_hoare sep_auto

text ‹MLton is not able to optimise the calls to pow.›
lemma pow_2_64: ‹(2::nat) ^ 64 = 18446744073709551616›
  by auto

sepref_register upper_bound_on_dom op_fmap_empty

definition full_checker_l2
  :: ‹llist_polynomial ⇒ (nat, llist_polynomial) fmap ⇒ (_, string, nat) pac_step list ⇒
    (string code_status × _) nres›
where
  ‹full_checker_l2 spec A st = do {
    spec' ← full_normalize_poly spec;
    (b, 𝒱, A) ← remap_polys_l spec {} A;
    if is_cfailed b
    then RETURN (b, 𝒱, A)
    else do {
      PAC_checker_l spec' (𝒱, A) b st
    }
  }›

sepref_register remap_polys_l
find_theorems full_checker_l2
sepref_definition full_checker_l_impl
  is ‹uncurry2 full_checker_l2›
  :: ‹poly_assn⇧k *⇩a polys_assn_input⇧d *⇩a (list_assn (pac_step_rel_assn (uint64_nat_assn) poly_assn string_assn))⇧k →⇩a
    status_assn raw_string_assn ×⇩a vars_assn ×⇩a polys_assn›
  supply [[goals_limit=1]] is_Mult_lastI[intro]
  unfolding full_checker_l_def hs.fold_custom_empty
    union_vars_poly_alt_def[symmetric]
    PAC_checker_l_alt_def
    full_checker_l2_def
  by sepref

sepref_definition PAC_empty_impl
  is ‹uncurry0 (RETURN fmempty)›
  :: ‹unit_assn⇧k →⇩a polys_assn_input›
  unfolding op_iam_fmap_empty_def[symmetric] pat_fmap_empty
  by sepref

sepref_definition empty_vars_impl
  is ‹uncurry0 (RETURN {})›
  :: ‹unit_assn⇧k →⇩a vars_assn›
  unfolding hs.fold_custom_empty
  by sepref

end