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

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

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]

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

:: ‹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
in_dom_m_lookup_iff
fmlookup'_def[symmetric]
vars_llist_alt_def
by sepref

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

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)

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"

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.

›

‹(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>‹
in f (next_token)
›

This code is equal to (in the HOL sense of equality):
\<^term>‹
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
```