Theory PAC_Checker_Synthesis

(*
  File:         PAC_Checker_Synthesis.thy
  Author:       Mathias Fleury, Daniela Kaufmann, JKU
  Maintainer:   Mathias Fleury, JKU
*)
theory PAC_Checker_Synthesis
  imports PAC_Checker WB_Sort PAC_Checker_Relation
    PAC_Checker_Init More_Loops PAC_Version
begin

section ‹Code Synthesis of the Complete Checker›

text ‹We here combine refine the full checker, using the initialisation provided in another file and
adding more efficient data structures (mostly replacing the set of variables by a more efficient
hash map).›

abbreviation vars_assn where
  ‹vars_assn ≡ hs.assn string_assn›

fun vars_of_monom_in where
  ‹vars_of_monom_in [] _ = True› |
  ‹vars_of_monom_in (x # xs) 𝒱 ⟷ x ∈ 𝒱 ∧ vars_of_monom_in xs 𝒱›

fun vars_of_poly_in where
  ‹vars_of_poly_in [] _ = True› |
  ‹vars_of_poly_in ((x, _) # xs) 𝒱 ⟷ vars_of_monom_in x 𝒱 ∧ vars_of_poly_in xs 𝒱›

lemma vars_of_monom_in_alt_def:
  ‹vars_of_monom_in xs 𝒱 ⟷ set xs ⊆ 𝒱›
  by (induction xs)
   auto

lemma vars_llist_alt_def:
  ‹vars_llist xs ⊆ 𝒱 ⟷ vars_of_poly_in xs 𝒱›
  by (induction xs)
   (auto simp: vars_llist_def vars_of_monom_in_alt_def)

lemma vars_of_monom_in_alt_def2:
  ‹vars_of_monom_in xs 𝒱 ⟷ fold (λx b. b ∧ x ∈ 𝒱) xs True›
  apply (subst foldr_fold[symmetric])
  subgoal by auto
  subgoal by (induction xs) auto
  done

sepref_definition vars_of_monom_in_impl
  is ‹uncurry (RETURN oo vars_of_monom_in)›
  :: ‹(list_assn string_assn)⇧k *⇩a vars_assn⇧k →⇩a bool_assn›
  unfolding vars_of_monom_in_alt_def2
  by sepref

declare vars_of_monom_in_impl.refine[sepref_fr_rules]

lemma vars_of_poly_in_alt_def2:
  ‹vars_of_poly_in xs 𝒱 ⟷ fold (λ(x, _) b. b ∧ vars_of_monom_in x 𝒱) xs True›
  apply (subst foldr_fold[symmetric])
  subgoal by auto
  subgoal by (induction xs) auto
  done


sepref_definition vars_of_poly_in_impl
  is ‹uncurry (RETURN oo vars_of_poly_in)›
  :: ‹(poly_assn)⇧k *⇩a vars_assn⇧k →⇩a bool_assn›
  unfolding vars_of_poly_in_alt_def2
  by sepref

declare vars_of_poly_in_impl.refine[sepref_fr_rules]


definition union_vars_monom :: ‹string list ⇒ string set ⇒ string set› where
‹union_vars_monom xs 𝒱 = fold insert xs 𝒱›

definition union_vars_poly :: ‹llist_polynomial ⇒ string set ⇒ string set› where
‹union_vars_poly xs 𝒱 = fold (λ(xs, _) 𝒱. union_vars_monom xs 𝒱) xs 𝒱›

lemma union_vars_monom_alt_def:
  ‹union_vars_monom xs 𝒱 = 𝒱 ∪ set xs›
  unfolding union_vars_monom_def
  apply (subst foldr_fold[symmetric])
  subgoal for x y
    by (cases x; cases y) auto
  subgoal
    by (induction xs) auto
  done

lemma union_vars_poly_alt_def:
  ‹union_vars_poly xs 𝒱 = 𝒱 ∪ vars_llist xs›
  unfolding union_vars_poly_def
  apply (subst foldr_fold[symmetric])
  subgoal for x y
    by (cases x; cases y)
      (auto simp: union_vars_monom_alt_def)
  subgoal
    by (induction xs)
     (auto simp: vars_llist_def union_vars_monom_alt_def)
   done

sepref_definition union_vars_monom_impl
  is ‹uncurry (RETURN oo union_vars_monom)›
  :: ‹monom_assn⇧k *⇩a vars_assn⇧d →⇩a vars_assn›
  unfolding union_vars_monom_def
  by sepref

declare union_vars_monom_impl.refine[sepref_fr_rules]

sepref_definition union_vars_poly_impl
  is ‹uncurry (RETURN oo union_vars_poly)›
  :: ‹poly_assn⇧k *⇩a vars_assn⇧d →⇩a vars_assn›
  unfolding union_vars_poly_def
  by sepref

declare union_vars_poly_impl.refine[sepref_fr_rules]


hide_const (open) Autoref_Fix_Rel.CONSTRAINT

fun status_assn where
  ‹status_assn _ CSUCCESS CSUCCESS = emp› |
  ‹status_assn _ CFOUND CFOUND = emp› |
  ‹status_assn R (CFAILED a) (CFAILED b) = R a b› |
  ‹status_assn _ _ _ = false›

lemma SUCCESS_hnr[sepref_fr_rules]:
  ‹(uncurry0 (return CSUCCESS), uncurry0 (RETURN CSUCCESS)) ∈ unit_assn⇧k →⇩a status_assn R›
  by (sepref_to_hoare)
    sep_auto

lemma FOUND_hnr[sepref_fr_rules]:
  ‹(uncurry0 (return CFOUND), uncurry0 (RETURN CFOUND)) ∈ unit_assn⇧k →⇩a status_assn R›
  by (sepref_to_hoare)
    sep_auto

lemma is_success_hnr[sepref_fr_rules]:
  ‹CONSTRAINT is_pure R ⟹
  ((return o is_cfound), (RETURN o is_cfound)) ∈ (status_assn R)⇧k →⇩a bool_assn›
  apply (sepref_to_hoare)
  apply (rename_tac xi x; case_tac xi; case_tac x)
  apply sep_auto+
  done

lemma is_cfailed_hnr[sepref_fr_rules]:
  ‹CONSTRAINT is_pure R ⟹
  ((return o is_cfailed), (RETURN o is_cfailed)) ∈ (status_assn R)⇧k →⇩a bool_assn›
  apply (sepref_to_hoare)
  apply (rename_tac xi x; case_tac xi; case_tac x)
  apply  sep_auto+
  done

lemma merge_cstatus_hnr[sepref_fr_rules]:
  ‹CONSTRAINT is_pure R ⟹
  (uncurry (return oo merge_cstatus), uncurry (RETURN oo merge_cstatus)) ∈
    (status_assn R)⇧k *⇩a  (status_assn R)⇧k →⇩a status_assn R›
  apply (sepref_to_hoare)
  by (case_tac b; case_tac bi; case_tac a; case_tac ai; sep_auto simp: is_pure_conv pure_app_eq)

sepref_definition add_poly_impl
  is ‹add_poly_l›
  :: ‹(poly_assn ×⇩a poly_assn)⇧k →⇩a poly_assn›
  supply [[goals_limit=1]]
  unfolding add_poly_l_def
    HOL_list.fold_custom_empty
    term_order_rel'_def[symmetric]
    term_order_rel'_alt_def
  by sepref


declare add_poly_impl.refine[sepref_fr_rules]


sepref_register mult_monomials
lemma mult_monoms_alt_def:
  ‹(RETURN oo mult_monoms) x y = REC⇩T
    (λf (p, q).
      case (p, q) of
        ([], _) ⇒ RETURN q
       | (_, []) ⇒ RETURN p
       | (x # p, y # q) ⇒
        (if x = y then do {
          pq ← f (p, q);
           RETURN (x # pq)}
        else if (x, y) ∈ var_order_rel
        then do {
          pq ← f (p, y # q);
          RETURN (x # pq)}
        else do {
          pq ←  f (x # p, q);
          RETURN (y # pq)}))
     (x, y)›
  apply (subst eq_commute)
  apply (induction x y rule: mult_monoms.induct)
  subgoal for p
    by (subst RECT_unfold, refine_mono) (auto split: list.splits)
  subgoal for p
    by (subst RECT_unfold, refine_mono) (auto split: list.splits)
  subgoal for x p y q
    by (subst RECT_unfold, refine_mono) (auto split: list.splits simp: let_to_bind_conv)
  done


sepref_definition mult_monoms_impl
  is ‹uncurry (RETURN oo mult_monoms)›
  :: ‹(monom_assn)⇧k *⇩a (monom_assn)⇧k →⇩a (monom_assn)›
  supply [[goals_limit=1]]
  unfolding mult_poly_raw_def
    HOL_list.fold_custom_empty
    var_order'_def[symmetric]
    term_order_rel'_alt_def
    mult_monoms_alt_def
    var_order_rel_var_order
  by sepref

declare mult_monoms_impl.refine[sepref_fr_rules]

sepref_definition mult_monomials_impl
  is ‹uncurry (RETURN oo mult_monomials)›
  :: ‹(monomial_assn)⇧k *⇩a (monomial_assn)⇧k →⇩a (monomial_assn)›
  supply [[goals_limit=1]]
  unfolding mult_monomials_def
    HOL_list.fold_custom_empty
    term_order_rel'_def[symmetric]
    term_order_rel'_alt_def
  by sepref


lemma map_append_alt_def2:
  ‹(RETURN o (map_append f b)) xs = REC⇩T
    (λg xs. case xs of [] ⇒ RETURN b
      | x # xs ⇒ do {
           y ← g xs;
           RETURN (f x # y)
     }) xs›
   apply (subst eq_commute)
  apply (induction f b xs rule: map_append.induct)
  subgoal by (subst RECT_unfold, refine_mono) auto
  subgoal by (subst RECT_unfold, refine_mono) auto
  done


definition map_append_poly_mult where
  ‹map_append_poly_mult x = map_append (mult_monomials x)›

declare mult_monomials_impl.refine[sepref_fr_rules]

sepref_definition map_append_poly_mult_impl
  is ‹uncurry2 (RETURN ooo map_append_poly_mult)›
  :: ‹monomial_assn⇧k *⇩a poly_assn⇧k *⇩a poly_assn⇧k →⇩a poly_assn›
  unfolding map_append_poly_mult_def
    map_append_alt_def2
  by sepref

declare map_append_poly_mult_impl.refine[sepref_fr_rules]

text ‹TODO @{thm map_by_foldl} is the worst possible implementation of map!›
sepref_definition mult_poly_raw_impl
  is ‹uncurry (RETURN oo mult_poly_raw)›
  :: ‹poly_assn⇧k *⇩a poly_assn⇧k →⇩a poly_assn›
  supply [[goals_limit=1]]
  supply [[eta_contract = false, show_abbrevs=false]]
  unfolding mult_poly_raw_def
    HOL_list.fold_custom_empty
    term_order_rel'_def[symmetric]
    term_order_rel'_alt_def
    foldl_conv_fold
    fold_eq_nfoldli
    map_append_poly_mult_def[symmetric]
    map_append_alt_def[symmetric]
  by sepref

declare mult_poly_raw_impl.refine[sepref_fr_rules]


sepref_definition mult_poly_impl
  is ‹uncurry mult_poly_full›
  :: ‹poly_assn⇧k *⇩a poly_assn⇧k →⇩a poly_assn›
  supply [[goals_limit=1]]
  unfolding mult_poly_full_def
    HOL_list.fold_custom_empty
    term_order_rel'_def[symmetric]
    term_order_rel'_alt_def
  by sepref

declare mult_poly_impl.refine[sepref_fr_rules]

lemma inverse_monomial:
  ‹monom_rel¯ ×⇩r int_rel = (monom_rel ×⇩r int_rel)¯›
  by (auto)

lemma eq_poly_rel_eq[sepref_import_param]:
  ‹((=), (=)) ∈ poly_rel → poly_rel → bool_rel›
  using list_rel_sv[of ‹monomial_rel›, OF single_valued_monomial_rel]
  using list_rel_sv[OF single_valued_monomial_rel'[unfolded IS_LEFT_UNIQUE_def inv_list_rel_eq]]
  unfolding inv_list_rel_eq[symmetric]
  by (auto intro!: frefI simp:
      rel2p_def single_valued_def p2rel_def
    simp del: inv_list_rel_eq)

sepref_definition weak_equality_l_impl
  is ‹uncurry weak_equality_l›
  :: ‹poly_assn⇧k *⇩a poly_assn⇧k →⇩a bool_assn›
  supply [[goals_limit=1]]
  unfolding weak_equality_l_def
  by sepref

declare weak_equality_l_impl.refine[sepref_fr_rules]
sepref_register add_poly_l mult_poly_full

abbreviation raw_string_assn :: ‹string ⇒ string ⇒ assn› where
  ‹raw_string_assn ≡ list_assn id_assn›

definition show_nat :: ‹nat ⇒ string› where
  ‹show_nat i = show i›

lemma [sepref_import_param]:
  ‹(show_nat, show_nat) ∈ nat_rel → ⟨Id⟩list_rel›
  by (auto intro: fun_relI)

lemma status_assn_pure_conv:
  ‹status_assn (id_assn) a b = id_assn a b›
  by (cases a; cases b)
    (auto simp: pure_def)


lemma [sepref_fr_rules]:
  ‹(uncurry3 (λx y. return oo (error_msg_not_equal_dom x y)), uncurry3 check_not_equal_dom_err) ∈
  poly_assn⇧k *⇩a poly_assn⇧k *⇩a poly_assn⇧k *⇩a poly_assn⇧k →⇩a raw_string_assn›
  unfolding show_nat_def[symmetric] list_assn_pure_conv
    prod_assn_pure_conv check_not_equal_dom_err_def
  by (sepref_to_hoare; sep_auto simp: error_msg_not_equal_dom_def)



lemma [sepref_fr_rules]:
  ‹(return o (error_msg_notin_dom o nat_of_uint64), RETURN o error_msg_notin_dom)
   ∈ uint64_nat_assn⇧k →⇩a raw_string_assn›
  ‹(return o (error_msg_reused_dom o nat_of_uint64), RETURN o error_msg_reused_dom)
    ∈ uint64_nat_assn⇧k →⇩a raw_string_assn›
  ‹(uncurry (return oo (λi. error_msg (nat_of_uint64 i))), uncurry (RETURN oo error_msg))
    ∈ uint64_nat_assn⇧k *⇩a raw_string_assn⇧k  →⇩a status_assn raw_string_assn›
  ‹(uncurry (return oo  error_msg), uncurry (RETURN oo error_msg))
   ∈ nat_assn⇧k *⇩a raw_string_assn⇧k  →⇩a status_assn raw_string_assn›
  unfolding error_msg_notin_dom_def list_assn_pure_conv list_rel_id_simp
  unfolding status_assn_pure_conv
  unfolding show_nat_def[symmetric]
  by (sepref_to_hoare; sep_auto simp: uint64_nat_rel_def br_def; fail)+

sepref_definition check_addition_l_impl
  is ‹uncurry6 check_addition_l›
  :: ‹poly_assn⇧k *⇩a polys_assn⇧k *⇩a vars_assn⇧k *⇩a uint64_nat_assn⇧k *⇩a uint64_nat_assn⇧k *⇩a
        uint64_nat_assn⇧k *⇩a poly_assn⇧k  →⇩a status_assn raw_string_assn›
  supply [[goals_limit=1]]
  unfolding mult_poly_full_def
    HOL_list.fold_custom_empty
    term_order_rel'_def[symmetric]
    term_order_rel'_alt_def
    check_addition_l_def
    in_dom_m_lookup_iff
    fmlookup'_def[symmetric]
    vars_llist_alt_def
  by sepref

declare check_addition_l_impl.refine[sepref_fr_rules]

sepref_register check_mult_l_dom_err

definition check_mult_l_dom_err_impl where
  ‹check_mult_l_dom_err_impl pd p ia i =
    (if pd then ''The polynomial with id '' @ show (nat_of_uint64 p) @ '' was not found'' else '''') @
    (if ia then ''The id of the resulting id '' @ show (nat_of_uint64 i) @ '' was already given'' else '''')›

definition check_mult_l_mult_err_impl where
  ‹check_mult_l_mult_err_impl p q pq r =
    ''Multiplying '' @ show p @ '' by '' @ show q @ '' gives '' @ show pq @ '' and not '' @ show r›

lemma [sepref_fr_rules]:
  ‹(uncurry3 ((λx y. return oo (check_mult_l_dom_err_impl x y))),
   uncurry3 (check_mult_l_dom_err)) ∈ bool_assn⇧k *⇩a uint64_nat_assn⇧k *⇩a bool_assn⇧k *⇩a uint64_nat_assn⇧k →⇩a raw_string_assn›
   unfolding check_mult_l_dom_err_def check_mult_l_dom_err_impl_def list_assn_pure_conv
   apply sepref_to_hoare
   apply sep_auto
   done

lemma [sepref_fr_rules]:
  ‹(uncurry3 ((λx y. return oo (check_mult_l_mult_err_impl x y))),
   uncurry3 (check_mult_l_mult_err)) ∈ poly_assn⇧k *⇩a poly_assn⇧k *⇩a poly_assn⇧k *⇩a poly_assn⇧k →⇩a raw_string_assn›
   unfolding check_mult_l_mult_err_def check_mult_l_mult_err_impl_def list_assn_pure_conv
   apply sepref_to_hoare
   apply sep_auto
   done

sepref_definition check_mult_l_impl
  is ‹uncurry6 check_mult_l›
  :: ‹poly_assn⇧k *⇩a polys_assn⇧k *⇩a vars_assn⇧k *⇩a uint64_nat_assn⇧k *⇩a poly_assn⇧k *⇩a uint64_nat_assn⇧k *⇩a poly_assn⇧k  →⇩a status_assn raw_string_assn›
  supply [[goals_limit=1]]
  unfolding check_mult_l_def
    HOL_list.fold_custom_empty
    term_order_rel'_def[symmetric]
    term_order_rel'_alt_def
    in_dom_m_lookup_iff
    fmlookup'_def[symmetric]
    vars_llist_alt_def
  by sepref

declare check_mult_l_impl.refine[sepref_fr_rules]

definition check_ext_l_dom_err_impl :: ‹uint64 ⇒ _›  where
  ‹check_ext_l_dom_err_impl p =
    ''There is already a polynomial with index '' @ show (nat_of_uint64 p)›

lemma [sepref_fr_rules]:
  ‹(((return o (check_ext_l_dom_err_impl))),
    (check_extension_l_dom_err)) ∈ uint64_nat_assn⇧k →⇩a raw_string_assn›
   unfolding check_extension_l_dom_err_def check_ext_l_dom_err_impl_def list_assn_pure_conv
   apply sepref_to_hoare
   apply sep_auto
   done


definition check_extension_l_no_new_var_err_impl :: ‹_ ⇒ _›  where
  ‹check_extension_l_no_new_var_err_impl p =
    ''No new variable could be found in polynomial '' @ show p›

lemma [sepref_fr_rules]:
  ‹(((return o (check_extension_l_no_new_var_err_impl))),
    (check_extension_l_no_new_var_err)) ∈ poly_assn⇧k →⇩a raw_string_assn›
   unfolding check_extension_l_no_new_var_err_impl_def check_extension_l_no_new_var_err_def
     list_assn_pure_conv
   apply sepref_to_hoare
   apply sep_auto
   done

definition check_extension_l_side_cond_err_impl :: ‹_ ⇒ _›  where
  ‹check_extension_l_side_cond_err_impl v p r s =
    ''Error while checking side conditions of extensions polynow, var is '' @ show v @
    '' polynomial is '' @ show p @ ''side condition p*p - p = '' @ show s @ '' and should be 0''›

lemma [sepref_fr_rules]:
  ‹((uncurry3 (λx y. return oo (check_extension_l_side_cond_err_impl x y))),
    uncurry3 (check_extension_l_side_cond_err)) ∈ string_assn⇧k *⇩a poly_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_register check_extension_l_dom_err fmlookup'
  check_extension_l_side_cond_err check_extension_l_no_new_var_err
  check_extension_l_new_var_multiple_err

definition uminus_poly :: ‹llist_polynomial ⇒ llist_polynomial› where
  ‹uminus_poly p' = map (λ(a, b). (a, - b)) p'›

sepref_register uminus_poly
lemma [sepref_import_param]:
  ‹(map (λ(a, b). (a, - b)), uminus_poly) ∈ poly_rel → poly_rel›
  unfolding uminus_poly_def
  apply (intro fun_relI)
  subgoal for p p'
    by (induction p p' rule: list_rel_induct)
     auto
  done

sepref_register vars_of_poly_in
  weak_equality_l

lemma [safe_constraint_rules]:
  ‹Sepref_Constraints.CONSTRAINT single_valued (the_pure monomial_assn)› and
  single_valued_the_monomial_assn:
    ‹single_valued (the_pure monomial_assn)›
    ‹single_valued ((the_pure monomial_assn)¯)›
  unfolding IS_LEFT_UNIQUE_def[symmetric]
  by (auto simp: step_rewrite_pure single_valued_monomial_rel single_valued_monomial_rel' Sepref_Constraints.CONSTRAINT_def)

sepref_definition check_extension_l_impl
  is ‹uncurry5 check_extension_l›
  :: ‹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 option.splits[split] single_valued_the_monomial_assn[simp]
  supply [[goals_limit=1]]
  unfolding
    HOL_list.fold_custom_empty
    term_order_rel'_def[symmetric]
    term_order_rel'_alt_def
    in_dom_m_lookup_iff
    fmlookup'_def[symmetric]
    vars_llist_alt_def
    check_extension_l_def
    not_not
    option.case_eq_if
    uminus_poly_def[symmetric]
    HOL_list.fold_custom_empty
  by sepref


declare check_extension_l_impl.refine[sepref_fr_rules]

sepref_definition check_del_l_impl
  is ‹uncurry2 check_del_l›
  :: ‹poly_assn⇧k *⇩a polys_assn⇧k *⇩a uint64_nat_assn⇧k →⇩a status_assn raw_string_assn›
  supply [[goals_limit=1]]
  unfolding check_del_l_def
    in_dom_m_lookup_iff
    fmlookup'_def[symmetric]
  by sepref

lemmas [sepref_fr_rules] = check_del_l_impl.refine

abbreviation pac_step_rel where
  ‹pac_step_rel ≡ p2rel (⟨Id, ⟨monomial_rel⟩list_rel, Id⟩ pac_step_rel_raw)›

sepref_register PAC_Polynomials_Operations.normalize_poly
  pac_src1 pac_src2 new_id pac_mult case_pac_step check_mult_l
  check_addition_l check_del_l check_extension_l

lemma pac_step_rel_assn_alt_def2:
  ‹hn_ctxt (pac_step_rel_assn nat_assn poly_assn id_assn) b bi =
       hn_val
        (p2rel
          (⟨nat_rel, poly_rel, Id :: (string × _) set⟩pac_step_rel_raw)) b bi›
  unfolding poly_assn_list hn_ctxt_def
  by (induction nat_assn poly_assn ‹id_assn :: string ⇒ _› b bi rule: pac_step_rel_assn.induct)
   (auto simp: p2rel_def hn_val_unfold pac_step_rel_raw.simps relAPP_def
    pure_app_eq)


lemma is_AddD_import[sepref_fr_rules]:
  assumes ‹CONSTRAINT is_pure K›  ‹CONSTRAINT is_pure V›
  shows
    ‹(return o pac_res, RETURN o pac_res) ∈ [λx. is_Add x ∨ is_Mult x ∨ is_Extension x]⇩a
       (pac_step_rel_assn K V R)⇧k → V›
    ‹(return o pac_src1, RETURN o pac_src1) ∈ [λx. is_Add x ∨ is_Mult x ∨ is_Del x]⇩a (pac_step_rel_assn K V R)⇧k → K›
    ‹(return o new_id, RETURN o new_id) ∈ [λx. is_Add x ∨ is_Mult x ∨ is_Extension x]⇩a (pac_step_rel_assn K V R)⇧k → K›
    ‹(return o is_Add, RETURN o is_Add) ∈  (pac_step_rel_assn K V R)⇧k →⇩a bool_assn›
    ‹(return o is_Mult, RETURN o is_Mult) ∈ (pac_step_rel_assn K V R)⇧k →⇩a bool_assn›
    ‹(return o is_Del, RETURN o is_Del) ∈ (pac_step_rel_assn K V R)⇧k →⇩a bool_assn›
    ‹(return o is_Extension, RETURN o is_Extension) ∈ (pac_step_rel_assn K V R)⇧k →⇩a bool_assn›
  using assms
  by (sepref_to_hoare; sep_auto simp: pac_step_rel_assn_alt_def is_pure_conv ent_true_drop pure_app_eq
      split: pac_step.splits; fail)+

lemma [sepref_fr_rules]:
  ‹CONSTRAINT is_pure K ⟹
  (return o pac_src2, RETURN o pac_src2) ∈ [λx. is_Add x]⇩a (pac_step_rel_assn K V R)⇧k → K›
  ‹CONSTRAINT is_pure V ⟹
  (return o pac_mult, RETURN o pac_mult) ∈ [λx. is_Mult x]⇩a (pac_step_rel_assn K V R)⇧k → V›
  ‹CONSTRAINT is_pure R ⟹
  (return o new_var, RETURN o new_var) ∈ [λx. is_Extension x]⇩a (pac_step_rel_assn K V R)⇧k → R›
  by (sepref_to_hoare; sep_auto simp: pac_step_rel_assn_alt_def is_pure_conv ent_true_drop pure_app_eq
      split: pac_step.splits; fail)+

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

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

lemma poly_rel_the_pure:
  ‹poly_rel = the_pure poly_assn› and
  nat_rel_the_pure:
  ‹nat_rel = the_pure nat_assn› and
 WTF_RF: ‹pure (the_pure nat_assn) = nat_assn›
  unfolding poly_assn_list
  by auto

lemma [safe_constraint_rules]:
    ‹CONSTRAINT IS_LEFT_UNIQUE uint64_nat_rel› and
  single_valued_uint64_nat_rel[safe_constraint_rules]:
    ‹CONSTRAINT single_valued uint64_nat_rel›
  by (auto simp: IS_LEFT_UNIQUE_def single_valued_def uint64_nat_rel_def br_def)

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

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
  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

sepref_definition remap_polys_l_impl
  is ‹uncurry2 remap_polys_l2›
  :: ‹poly_assn⇧k *⇩a vars_assn⇧d *⇩a polys_assn_input⇧d →⇩a
    status_assn raw_string_assn ×⇩a vars_assn ×⇩a polys_assn›
  supply [[goals_limit=1]] is_Mult_lastI[intro] indom_mI[dest]
  unfolding remap_polys_l2_def op_fmap_empty_def[symmetric] while_eq_nfoldli[symmetric]
    while_upt_while_direct pow_2_64
    in_dom_m_lookup_iff
    fmlookup'_def[symmetric]
    union_vars_poly_alt_def[symmetric]
  apply (rewrite at ‹fmupd ⌑› uint64_of_nat_conv_def[symmetric])
  apply (subst while_upt_while_direct)
  apply simp
  apply (rewrite at ‹op_fmap_empty› annotate_assn[where A=‹polys_assn›])
  by sepref

lemma remap_polys_l2_remap_polys_l:
  ‹(uncurry2 remap_polys_l2, uncurry2 remap_polys_l) ∈ (Id ×⇩r ⟨Id⟩set_rel) ×⇩r Id →⇩f ⟨Id⟩nres_rel›
  apply (intro frefI fun_relI nres_relI)
  using remap_polys_l2_remap_polys_l by auto

lemma [sepref_fr_rules]:
   ‹(uncurry2 remap_polys_l_impl,
     uncurry2 remap_polys_l) ∈ poly_assn⇧k *⇩a vars_assn⇧d *⇩a polys_assn_input⇧d →⇩a
       status_assn raw_string_assn ×⇩a vars_assn ×⇩a polys_assn›
   using hfcomp_tcomp_pre[OF remap_polys_l2_remap_polys_l remap_polys_l_impl.refine]
   by (auto simp: hrp_comp_def hfprod_def)

sepref_register remap_polys_l

sepref_definition full_checker_l_impl
  is ‹uncurry2 full_checker_l›
  :: ‹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
  by sepref

sepref_definition PAC_update_impl
  is ‹uncurry2 (RETURN ooo fmupd)›
  :: ‹nat_assn⇧k *⇩a poly_assn⇧k *⇩a (polys_assn_input)⇧d →⇩a polys_assn_input›
  unfolding comp_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

text ‹This is a hack for performance. There is no need to recheck that that a char is valid when
  working on chars coming from strings... It is not that important in most cases, but in our case
  the preformance difference is really large.›


definition unsafe_asciis_of_literal :: ‹_› where
  ‹unsafe_asciis_of_literal xs = String.asciis_of_literal xs›

definition unsafe_asciis_of_literal' :: ‹_› where
  [simp, symmetric, code]: ‹unsafe_asciis_of_literal' = unsafe_asciis_of_literal›

code_printing
  constant unsafe_asciis_of_literal' ⇀
    (SML) "!(List.map (fn c => let val k = Char.ord c in IntInf.fromInt k end) /o String.explode)"

text ‹
  Now comes the big and ugly and unsafe hack.

  Basically, we try to avoid the conversion to IntInf when calculating the hash. The performance
  gain is roughly 40\%, which is a LOT and definitively something we need to do. We are aware that the
  SML semantic encourages compilers to optimise conversions, but this does not happen here,
  corroborating our early observation on the verified SAT solver IsaSAT.x
›
definition raw_explode where
  [simp]: ‹raw_explode = String.explode›
code_printing
  constant raw_explode ⇀
    (SML) "String.explode"

definition ‹hashcode_literal' s ≡
    foldl (λh x. h * 33 + uint32_of_int (of_char x)) 5381
     (raw_explode s)›

lemmas [code] =
  hashcode_literal_def[unfolded String.explode_code
    unsafe_asciis_of_literal_def[symmetric]]

definition uint32_of_char where
  [symmetric, code_unfold]: ‹uint32_of_char x = uint32_of_int (int_of_char x)›


code_printing
  constant uint32_of_char ⇀
    (SML) "!(Word32.fromInt /o (Char.ord))"

lemma [code]: ‹hashcode s = hashcode_literal' s›
  unfolding hashcode_literal_def hashcode_list_def
  apply (auto simp: unsafe_asciis_of_literal_def hashcode_list_def
     String.asciis_of_literal_def hashcode_literal_def hashcode_literal'_def)
  done

text ‹We compile Pastèque in 🗏‹PAC_Checker_MLton.thy›.›
export_code PAC_checker_l_impl PAC_update_impl PAC_empty_impl the_error is_cfailed is_cfound
  int_of_integer Del Add Mult nat_of_integer String.implode remap_polys_l_impl
  fully_normalize_poly_impl union_vars_poly_impl empty_vars_impl
  full_checker_l_impl check_step_impl CSUCCESS
  Extension hashcode_literal' version
  in SML_imp module_name PAC_Checker


section ‹Correctness theorem›

context poly_embed
begin

definition full_poly_assn where
  ‹full_poly_assn = hr_comp poly_assn (fully_unsorted_poly_rel O mset_poly_rel)›

definition full_poly_input_assn where
  ‹full_poly_input_assn = hr_comp
        (hr_comp polys_assn_input
          (⟨nat_rel, fully_unsorted_poly_rel O mset_poly_rel⟩fmap_rel))
        polys_rel›

definition fully_pac_assn where
  ‹fully_pac_assn = (list_assn
        (hr_comp (pac_step_rel_assn uint64_nat_assn poly_assn string_assn)
          (p2rel
            (⟨nat_rel,
             fully_unsorted_poly_rel O
             mset_poly_rel, var_rel⟩pac_step_rel_raw))))›

definition code_status_assn where
  ‹code_status_assn = hr_comp (status_assn raw_string_assn)
                            code_status_status_rel›

definition full_vars_assn where
  ‹full_vars_assn = hr_comp (hs.assn string_assn)
                              (⟨var_rel⟩set_rel)›

lemma polys_rel_full_polys_rel:
  ‹polys_rel_full = Id ×⇩r polys_rel›
  by (auto simp: polys_rel_full_def)

definition full_polys_assn :: ‹_› where
‹full_polys_assn = hr_comp (hr_comp polys_assn
                              (⟨nat_rel,
                               sorted_poly_rel O mset_poly_rel⟩fmap_rel))
                            polys_rel›

text ‹

Below is the full correctness theorems. It basically states that:

  ▸ assuming that the input polynomials have no duplicate variables


Then:

▸ if the checker returns \<^term>‹CFOUND›, the spec is in the ideal
  and the PAC file is correct

▸ if the checker returns \<^term>‹CSUCCESS›, the PAC file is correct (but
there is no information on the spec, aka checking failed)

▸ if the checker return \<^term>‹CFAILED err›, then checking failed (and
\<^term>‹err› ∗‹might› give you an indication of the error, but the correctness
theorem does not say anything about that).


The input parameters are:

▸ the specification polynomial represented as a list

▸ the input polynomials as hash map (as an array of option polynomial)

▸ a represention of the PAC proofs.

›

lemma PAC_full_correctness: (* \htmllink{PAC-full-correctness} *)
  ‹(uncurry2 full_checker_l_impl,
     uncurry2 (λspec A _. PAC_checker_specification spec A))
    ∈ (full_poly_assn)⇧k *⇩a (full_poly_input_assn)⇧d *⇩a (fully_pac_assn)⇧k →⇩a hr_comp
      (code_status_assn ×⇩a full_vars_assn ×⇩a hr_comp polys_assn
                              (⟨nat_rel, sorted_poly_rel O mset_poly_rel⟩fmap_rel))
                            {((st, G), st', G').
                             st = st' ∧ (st ≠ FAILED ⟶ (G, G') ∈ Id ×⇩r polys_rel)}›
  using
    full_checker_l_impl.refine[FCOMP full_checker_l_full_checker',
      FCOMP full_checker_spec',
      unfolded full_poly_assn_def[symmetric]
        full_poly_input_assn_def[symmetric]
        fully_pac_assn_def[symmetric]
        code_status_assn_def[symmetric]
        full_vars_assn_def[symmetric]
        polys_rel_full_polys_rel
        hr_comp_prod_conv
        full_polys_assn_def[symmetric]]
      hr_comp_Id2
   by auto

text ‹

It would be more efficient to move the parsing to Isabelle, as this
would be more memory efficient (and also reduce the TCB). But now
comes the fun part: It cannot work. A stream (of a file) is consumed
by side effects. Assume that this would work. The code could look like:

\<^term>‹
  let next_token = read_file file
  in f (next_token)
›

This code is equal to (in the HOL sense of equality):
\<^term>‹
  let _ = read_file file;
      next_token = read_file file
  in f (next_token)
›

However, as an hypothetical \<^term>‹read_file› changes the underlying stream, we would get the next
token. Remark that this is already a weird point of ML compilers. Anyway, I see currently two
solutions to this problem:

▸ The meta-argument: use it only in the Refinement Framework in a setup where copies are
disallowed. Basically, this works because we can express the non-duplication constraints on the type
level. However, we cannot forbid people from expressing things directly at the HOL level.

▸ On the target language side, model the stream as the stream and the position. Reading takes two
arguments. First, the position to read. Second, the stream (and the current position) to read. If
the position to read does not match the current position, return an error. This would fit the
correctness theorem of the code generation (roughly ``if it terminates without exception, the answer
is the same''), but it is still unsatisfactory.
›

end

definition φ :: ‹string ⇒ nat› where
  ‹φ = (SOME φ. bij φ)›

lemma bij_φ: ‹bij φ›
  using someI[of ‹λφ :: string ⇒ nat. bij φ›]
  unfolding φ_def[symmetric]
  using poly_embed_EX
  by auto

global_interpretation PAC: poly_embed where
  φ = φ
  apply standard
  apply (use bij_φ in ‹auto simp: bij_def›)
  done


text ‹The full correctness theorem is @{thm PAC.PAC_full_correctness}.›

end