Theory EPAC_Efficient_Checker_Synthesis
theory EPAC_Efficient_Checker_Synthesis
imports EPAC_Efficient_Checker
EPAC_Perfectly_Shared_Vars
PAC_Checker.PAC_Checker_Synthesis
EPAC_Steps_Refine
PAC_Checker.PAC_Checker_Synthesis
begin
lemma in_set_rel_inD: ‹(x,y) ∈⟨R⟩list_rel ⟹ a ∈ set x ⟹ ∃b ∈ set y. (a,b)∈ R›
by (metis (no_types, lifting) Un_iff list.set_intros(1) list_relE3 list_rel_append1 set_append split_list_first)
lemma perfectly_shared_monom_eqD: ‹(a, ab) ∈ perfectly_shared_monom 𝒱 ⟹ ab = map ((the ∘∘ fmlookup) (fst (snd 𝒱))) a›
by (induction a arbitrary: ab)
(auto simp: append_eq_append_conv2 append_eq_Cons_conv Cons_eq_append_conv
list_rel_append1 list_rel_split_right_iff perfectly_shared_var_rel_def br_def)
lemma perfectly_shared_monom_unique_left:
‹(x, y) ∈ perfectly_shared_monom 𝒱 ⟹ (x, y') ∈ perfectly_shared_monom 𝒱 ⟹ y = y'›
using perfectly_shared_monom_eqD by blast
lemma perfectly_shared_monom_unique_right:
‹(𝒱, 𝒟𝒱) ∈ perfectly_shared_vars_rel ⟹
(x, y) ∈ perfectly_shared_monom 𝒱 ⟹ (x', y) ∈ perfectly_shared_monom 𝒱 ⟹ x = x'›
by (induction x arbitrary: x' y)
(auto simp: append_eq_append_conv2 append_eq_Cons_conv Cons_eq_append_conv
list_rel_split_left_iff perfectly_shared_vars_rel_def perfectly_shared_vars_def
list_rel_append1 list_rel_split_right_iff perfectly_shared_var_rel_def br_def
add_mset_eq_add_mset
dest!: multi_member_split[of _ ‹dom_m _›])
lemma perfectly_shared_polynom_unique_left:
‹(x, y) ∈ perfectly_shared_polynom 𝒱 ⟹ (x, y') ∈ perfectly_shared_polynom 𝒱 ⟹ y = y'›
by (induction x arbitrary: y y')
(auto dest: perfectly_shared_monom_unique_left simp: list_rel_split_right_iff)
lemma perfectly_shared_polynom_unique_right:
‹(𝒱, 𝒟𝒱) ∈ perfectly_shared_vars_rel ⟹
(x, y) ∈ perfectly_shared_polynom 𝒱 ⟹ (x', y) ∈ perfectly_shared_polynom 𝒱 ⟹ x = x'›
by (induction x arbitrary: x' y)
(auto dest: perfectly_shared_monom_unique_right simp: list_rel_split_left_iff
list_rel_split_right_iff)
definition (in -)perfect_shared_var_order_s :: ‹(nat, string)shared_vars ⇒ nat ⇒ nat ⇒ ordered nres› where
‹perfect_shared_var_order_s 𝒟 x y = do {
eq ← perfectly_shared_strings_equal_l 𝒟 x y;
if eq then RETURN EQUAL
else do {
x ← get_var_nameS 𝒟 x;
y ← get_var_nameS 𝒟 y;
if (x, y) ∈ var_order_rel then RETURN (LESS)
else RETURN (GREATER)
}}›
lemma perfect_shared_var_order_s_perfect_shared_var_order:
assumes ‹(𝒱, 𝒱𝒟) ∈ perfectly_shared_vars_rel› and
‹(i, i') ∈ perfectly_shared_var_rel 𝒱›and
‹(j, j') ∈ perfectly_shared_var_rel 𝒱›
shows ‹perfect_shared_var_order_s 𝒱 i j ≤⇓Id (perfect_shared_var_order 𝒱𝒟 i' j')›
proof -
show ?thesis
unfolding perfect_shared_var_order_s_def perfect_shared_var_order_def
apply (refine_rcg perfectly_shared_strings_equal_l_perfectly_shared_strings_equal
get_var_nameS_spec)
subgoal using assms by metis
subgoal using assms by metis
subgoal using assms by metis
subgoal by auto
subgoal using assms by auto
subgoal using assms by metis
subgoal using assms by metis
subgoal using assms by metis
subgoal by auto
done
qed
definition (in -) perfect_shared_term_order_rel_s
:: ‹(nat, string) shared_vars ⇒ nat list⇒ nat list ⇒ ordered nres›
where
‹perfect_shared_term_order_rel_s 𝒱 xs ys = do {
(b, _, _) ← WHILE⇩T (λ(b, xs, ys). b = UNKNOWN)
(λ(b, xs, ys). do {
if xs = [] ∧ ys = [] then RETURN (EQUAL, xs, ys)
else if xs = [] then RETURN (LESS, xs, ys)
else if ys = [] then RETURN (GREATER, xs, ys)
else do {
ASSERT(xs ≠ [] ∧ ys ≠ []);
eq ← perfect_shared_var_order_s 𝒱 (hd xs) (hd ys);
if eq = EQUAL then RETURN (b, tl xs, tl ys)
else RETURN (eq, xs, ys)
}
}) (UNKNOWN, xs, ys);
RETURN b
}›
lemma perfect_shared_term_order_rel_s_perfect_shared_term_order_rel:
assumes ‹(𝒱, 𝒱𝒟) ∈ perfectly_shared_vars_rel› and
‹(xs, xs') ∈ perfectly_shared_monom 𝒱› and
‹(ys, ys') ∈ perfectly_shared_monom 𝒱›
shows ‹perfect_shared_term_order_rel_s 𝒱 xs ys ≤ ⇓Id (perfect_shared_term_order_rel 𝒱𝒟 xs' ys')›
using assms
unfolding perfect_shared_term_order_rel_s_def perfect_shared_term_order_rel_def
apply (refine_rcg WHILET_refine[where R = ‹Id ×⇩r perfectly_shared_monom 𝒱 ×⇩r perfectly_shared_monom 𝒱›]
perfect_shared_var_order_s_perfect_shared_var_order)
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by (auto simp: neq_Nil_conv)
subgoal by (auto simp: neq_Nil_conv)
subgoal by auto
subgoal by (auto simp: neq_Nil_conv)
subgoal by auto
subgoal by auto
done
fun mergeR :: "_ ⇒ _ ⇒ 'a list ⇒ 'a list ⇒ 'a list nres"
where
"mergeR Φ f (x#xs) (y#ys) = do {
ASSERT(Φ x y);
b ← f x y;
if b then do {zs ← mergeR Φ f xs (y#ys); RETURN (x # zs)}
else do {zs ← mergeR Φ f (x#xs) ys; RETURN (y # zs)}
}"
| "mergeR Φ f xs [] = RETURN xs"
| "mergeR Φ f [] ys = RETURN ys"
lemma mergeR_merge:
assumes ‹⋀x y. x∈set xs ∪ set ys ⟹ y∈set xs ∪ set ys ⟹Φ x y› and
‹⋀x y. x∈set xs ∪ set ys ⟹ y∈set xs ∪ set ys ⟹ f x y ≤ ⇓Id (RETURN (f' x y))› and
‹(xs,xs')∈Id›and
‹(ys,ys')∈Id›
shows
‹mergeR Φ f xs ys ≤ ⇓Id (RETURN (merge f' xs' ys'))›
proof -
have xs: ‹xs' = xs› ‹ys' = ys›
using assms
by auto
show ?thesis
using assms(1,2) unfolding xs
apply (induction f' xs ys arbitrary: xs' ys' rule: merge.induct)
subgoal for f' x xs y ys
unfolding mergeR.simps merge.simps
apply (refine_rcg)
subgoal by simp
subgoal premises p
using p(1,2,3,4,5) p(4)[of x y, simplified]
apply auto
apply (smt RES_sng_eq_RETURN insert_compr ireturn_rule nres_order_simps(20) specify_left)
apply (smt RES_sng_eq_RETURN insert_compr ireturn_rule nres_order_simps(20) specify_left)
done
done
subgoal by auto
subgoal by auto
done
qed
lemma merge_alt:
"RETURN (merge f xs ys) = SPEC(λzs. zs = merge f xs ys ∧ set zs = set xs ∪ set ys)"
by (induction f xs ys rule: merge.induct)
(clarsimp_all simp: Collect_conv_if insert_commute)
fun msortR :: "_ ⇒ _ ⇒ 'a list ⇒ 'a list nres"
where
"msortR Φ f [] = RETURN []"
| "msortR Φ f [x] = RETURN [x]"
| "msortR Φ f xs = do {
as ← msortR Φ f (take (size xs div 2) xs);
bs ← msortR Φ f (drop (size xs div 2) xs);
mergeR Φ f as bs
}"
lemma set_msort[simp]: ‹set (msort f xs) = set xs›
by (meson mset_eq_setD mset_msort)
lemma msortR_msort:
assumes ‹⋀x y. x∈set xs ⟹ y∈set xs ⟹Φ x y› and
‹⋀x y. x∈set xs ⟹ y∈set xs ⟹ f x y ≤ ⇓Id (RETURN (f' x y))›
shows
‹msortR Φ f xs ≤ ⇓Id (RETURN (msort f' xs))›
proof -
have a: ‹set (take (length xs div 2) (y # xs)) ⊆ insert x (insert y (set xs))›
‹set (drop (length xs div 2) (y # xs)) ⊆ insert x (insert y (set xs))›
for x y xs
by (auto dest: in_set_takeD in_set_dropD)
have H: ‹RETURN (msort f' (x#y#xs)) = do {
let as = msort f' (take (size (x#y#xs) div 2) (x#y#xs));
let bs = msort f' (drop (size (x#y#xs) div 2) (x#y#xs));
ASSERT(set (as) ⊆ set (x#y#xs));
ASSERT(set (bs) ⊆ set (x#y#xs));
RETURN (merge f' as bs)}› for x y xs f'
unfolding Let_def
by (auto simp: a)
show ?thesis
supply RETURN_as_SPEC_refine[refine2 del]
using assms
apply (induction f' xs rule: msort.induct)
subgoal by auto
subgoal by auto
subgoal premises p for f' x y xs
using p
unfolding msortR.simps H
apply (refine_vcg mergeR_merge p)
subgoal by (auto dest!: in_set_takeD)
subgoal by (auto dest!: in_set_takeD)
subgoal by (auto dest!: in_set_takeD)
subgoal by (auto dest!: in_set_takeD)
subgoal by (auto dest!: in_set_dropD)
subgoal by (auto dest!: in_set_dropD)
subgoal by (auto dest!: in_set_dropD)
subgoal by (auto dest!: in_set_dropD)
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
done
done
qed
lemma merge_list_rel:
assumes ‹⋀x y x' y'. x∈set xs ⟹ y∈set ys ⟹ x'∈set xs' ⟹ y'∈set ys' ⟹ (x,x')∈R ⟹ (y,y')∈R ⟹ f x y = f' x' y'› and
‹(xs,xs') ∈ ⟨R⟩list_rel› and
‹(ys,ys') ∈ ⟨R⟩list_rel›
shows ‹(merge f xs ys, merge f' xs' ys') ∈ ⟨R⟩list_rel›
proof -
show ?thesis
using assms
proof (induction f' xs' ys' arbitrary: f xs ys rule: merge.induct)
case (1 f' x' xs' y' y's)
have ‹f' x' y' ⟹
(PAC_Checker_Init.merge f (tl xs) ys, PAC_Checker_Init.merge f' xs' (y' # y's)) ∈ ⟨R⟩list_rel›
apply (rule 1)
apply assumption
apply (rule 1(3); auto dest: in_set_tlD)
using 1(4-5) apply (auto simp: list_rel_split_left_iff)
done
moreover have ‹¬f' x' y' ⟹
(PAC_Checker_Init.merge f ( xs) (tl ys), PAC_Checker_Init.merge f' (x' # xs') (y's)) ∈ ⟨R⟩list_rel›
apply (rule 1)
apply assumption
apply (rule 1(3); auto dest: in_set_tlD)
using 1(4-5) apply (auto simp: list_rel_split_left_iff)
done
ultimately show ?case
using 1(1,4-5) 1(3)[of ‹hd xs› ‹hd ys› x' y']
by (auto simp: list_rel_split_left_iff)
qed (auto simp: list_rel_split_left_iff)
qed
lemma msort_list_rel:
assumes ‹⋀x y x' y'. x∈set xs ⟹ y∈set xs ⟹ x'∈set xs' ⟹ y'∈set xs' ⟹ (x,x')∈R ⟹ (y,y')∈R ⟹ f x y = f' x' y'› and
‹(xs,xs') ∈ ⟨R⟩list_rel›
shows ‹(msort f xs, msort f' xs') ∈ ⟨R⟩list_rel›
proof -
show ?thesis
using assms
proof (induction f' xs' arbitrary: xs f rule: msort.induct)
case (3 f'' v vb vc)
have xs: ‹
(msort f (take (length xs div 2) xs), msort f'' (take (length (v # vb # vc) div 2) (v # vb # vc))) ∈ ⟨R⟩list_rel›
‹(msort f (drop (length xs div 2) xs), msort f'' (drop (length (v # vb # vc) div 2) (v # vb # vc))) ∈ ⟨R⟩list_rel›
subgoal
apply (rule 3)
using 3(3-) apply (force dest!: in_set_dropD in_set_takeD list_rel_imp_same_length)
using 3(4) apply (auto simp: list_rel_imp_same_length dest: list_rel_takeD)
done
subgoal
apply (rule 3)
using 3(3-) apply (force dest!: in_set_dropD in_set_takeD list_rel_imp_same_length
dest: )
using 3(4) apply (auto simp: list_rel_imp_same_length dest: list_rel_dropD)
done
done
have H: ‹(PAC_Checker_Init.merge f (msort f (x # take (length xsaa div 2) (xa # xsaa)))
(msort f (drop (length xsaa div 2) (xa # xsaa))),
PAC_Checker_Init.merge f'' (msort f'' (v # take (length vc div 2) (vb # vc)))
(msort f'' (drop (length vc div 2) (vb # vc))))
∈ ⟨R⟩list_rel›
if ‹xs = x # xa # xsaa› and
‹ (x, v) ∈ R› and
‹(xa, vb) ∈ R› and
‹ (xa, vb) ∈ R›
for x xa xsaa
apply (rule merge_list_rel)
subgoal for xb y x' y'
by (rule 3(3))
(use that in ‹auto dest: in_set_takeD in_set_dropD›)
subgoal
by (use xs(1) 3(4) that in auto)
subgoal
by (use xs(2) 3(4) that in auto)
done
show ?case
using 3(3-) H by (auto simp: list_rel_split_left_iff)
qed (auto simp: list_rel_split_left_iff intro!: )
qed
lemma msortR_alt_def:
‹(msortR Φ f xs) = REC⇩T(λmsortR' xs.
if length xs ≤ 1 then RETURN xs else do {
let xs1 = (take ((size xs) div 2) xs);
let xs2 = (drop ((size xs) div 2) xs);
as ← msortR' xs1;
bs ← msortR' xs2;
(mergeR Φ f as bs)
}) xs
›
apply (induction Φ f xs rule: msortR.induct)
subgoal
by (subst RECT_unfold, refine_mono) auto
subgoal
by (subst RECT_unfold, refine_mono) auto
subgoal
by (subst RECT_unfold, refine_mono) auto
done
definition sort_poly_spec_s where
‹sort_poly_spec_s 𝒱 xs = msortR (λxs ys. (∀a∈set (fst xs). a ∈# dom_m (fst (snd 𝒱))) ∧ (∀a∈set(fst ys). a ∈# dom_m (fst (snd 𝒱))))
(λxs ys. do {a ← perfect_shared_term_order_rel_s 𝒱 (fst xs) (fst ys); RETURN (a ≠ GREATER)}) xs›
lemma sort_poly_spec_s_sort_poly_spec:
assumes ‹(𝒱, 𝒱𝒟) ∈ perfectly_shared_vars_rel› and
‹(xs, xs') ∈ perfectly_shared_polynom 𝒱› and
‹vars_llist xs' ⊆ set_mset 𝒱𝒟›
shows
‹sort_poly_spec_s 𝒱 xs
≤⇓(perfectly_shared_polynom 𝒱)
(sort_poly_spec xs')
›
proof -
have [iff]: ‹sorted_wrt (rel2p (Id ∪ term_order_rel)) (map fst (msort (λxs ys. rel2p (Id ∪ term_order_rel) (fst xs) (fst ys)) xs'))›
unfolding sorted_wrt_map
apply (rule sorted_msort)
apply (smt Un_iff pair_in_Id_conv rel2p_def term_order_rel_trans transp_def)
apply (auto simp: rel2p_def)
using total_on_lexord_less_than_char_linear var_order_rel_def by auto
have [iff]:
‹(a,b)∈ ⟨⟨(perfectly_shared_var_rel 𝒱)¯⟩list_rel ×⇩r int_rel⟩list_rel ⟷ (b,a)∈perfectly_shared_polynom 𝒱› for a b
by (metis converse_Id converse_iff inv_list_rel_eq inv_prod_rel_eq)
show ?thesis
unfolding sort_poly_spec_s_def
apply (rule order_trans[OF msortR_msort[where
f'=‹ λxs ys. (map (the o fmlookup (fst (snd 𝒱))) (fst xs), map (the o fmlookup (fst (snd 𝒱))) (fst ys)) ∈ Id ∪ term_order_rel›]])
subgoal for x y
apply (cases x, cases y)
using assms by (auto simp: list_rel_append1 list_rel_split_right_iff perfectly_shared_var_rel_def br_def
perfectly_shared_vars_rel_def append_eq_append_conv2 append_eq_Cons_conv Cons_eq_append_conv
dest!: split_list split: prod.splits)
subgoal for x y
using assms(2,3) apply -
apply (frule in_set_rel_inD)
apply assumption
apply (frule in_set_rel_inD[of _ _ _ y])
apply assumption
apply (elim bexE)+
subgoal for x' y'
apply (refine_vcg perfect_shared_term_order_rel_s_perfect_shared_term_order_rel[OF assms(1), THEN order_trans,
of _ ‹fst x'› _ ‹fst y'›])
subgoal
by (cases x', cases x) auto
subgoal
by (cases y', cases y) auto
subgoal
using assms
apply (clarsimp dest!: split_list intro!: perfect_shared_term_order_rel_spec[THEN order_trans]
simp: append_eq_append_conv2 append_eq_Cons_conv Cons_eq_append_conv
vars_llist_def)
apply (rule perfect_shared_term_order_rel_spec[THEN order_trans])
apply auto[]
apply auto[]
apply simp
apply (clarsimp_all simp: perfectly_shared_monom_eqD)
apply (cases x, cases y, cases x', cases y')
apply (clarsimp_all simp flip: perfectly_shared_monom_eqD)
apply (case_tac xa)
apply (clarsimp_all simp flip: perfectly_shared_monom_eqD simp: lexord_irreflexive)
by (meson lexord_irreflexive term_order_rel_trans var_order_rel_antisym)
done
done
unfolding sort_poly_spec_def conc_fun_RES
apply auto
apply (subst Image_iff)
apply (rule_tac x= ‹msort (λxs ys. rel2p (Id ∪ term_order_rel) (fst xs) (fst ys)) (xs')› in bexI)
apply (auto intro!: msort_list_rel simp flip: perfectly_shared_monom_eqD
simp: assms)
apply (auto simp: rel2p_def)
done
qed
definition msort_coeff_s :: ‹(nat,string)shared_vars ⇒ nat list ⇒ nat list nres› where
‹msort_coeff_s 𝒱 xs = msortR (λa b. a ∈ set xs ∧ b ∈ set xs)
(λa b. do {
x ← get_var_nameS 𝒱 a;
y ← get_var_nameS 𝒱 b;
RETURN(a = b ∨ var_order x y)
}) xs›
lemma perfectly_shared_var_rel_unique_left:
‹(x, y) ∈ perfectly_shared_var_rel 𝒱 ⟹ (x, y') ∈ perfectly_shared_var_rel 𝒱 ⟹ y = y'›
using perfectly_shared_monom_unique_left[of ‹[x]› ‹[y]› 𝒱 ‹[y']›] by auto
lemma perfectly_shared_var_rel_unique_right:
‹(𝒱, 𝒟𝒱) ∈ perfectly_shared_vars_rel ⟹ (x, y) ∈ perfectly_shared_var_rel 𝒱 ⟹ (x', y) ∈ perfectly_shared_var_rel 𝒱 ⟹ x = x'›
using perfectly_shared_monom_unique_right[of 𝒱 𝒟𝒱 ‹[x]› ‹[y]› ‹[x']›]
by auto
lemma msort_coeff_s_sort_coeff:
fixes xs' :: ‹string list› and
𝒱 :: ‹(nat,string)shared_vars›
assumes
‹(xs, xs') ∈ perfectly_shared_monom 𝒱› and
‹(𝒱, 𝒟𝒱) ∈ perfectly_shared_vars_rel› and
‹set xs' ⊆ set_mset 𝒟𝒱›
shows ‹msort_coeff_s 𝒱 xs ≤ ⇓(perfectly_shared_monom 𝒱) (sort_coeff xs')›
proof -
have H: ‹x ∈ set xs ⟹ ∃x' ∈ set xs'. (x,x') ∈ perfectly_shared_var_rel 𝒱 ∧ x' ∈# 𝒟𝒱› for x
using assms(1,3) by (auto dest: in_set_rel_inD)
define f where
‹f x y ⟷ x = y ∨ var_order (fst (snd 𝒱) ∝ x) (fst (snd 𝒱) ∝ y)› for x y
have [simp]: ‹x ∈ set xs ⟹ x' ∈ set xs' ⟹ (x, x') ∈ perfectly_shared_var_rel 𝒱 ⟹
fst (snd 𝒱) ∝ x = x'› for x x'
using assms(2)
by (auto simp: perfectly_shared_vars_rel_def perfectly_shared_var_rel_def br_def)
have [intro]: ‹transp (λx y. x = y ∨ (x, y) ∈ var_order_rel)›
by (smt transE trans_var_order_rel transp_def)
have [intro]: ‹sorted_wrt (rel2p (Id ∪ var_order_rel)) (msort (λa b. a = b ∨ var_order a b) xs')›
using var_roder_rel_total by (auto intro!: sorted_msort simp: rel2p_def[abs_def])
show ?thesis
unfolding msort_coeff_s_def
apply (rule msortR_msort[of _ _ _ f, THEN order_trans])
subgoal by auto
subgoal for x y
unfolding f_def
apply (frule H[of x])
apply (frule H[of y])
apply (elim bexE)
apply (refine_vcg get_var_nameS_spec2[THEN order_trans] assms)
apply (solves auto)
apply (solves auto)
apply (subst Down_id_eq)
apply (refine_vcg get_var_nameS_spec2[THEN order_trans] assms)
apply (solves auto)
apply (solves auto)
apply (auto simp: perfectly_shared_var_rel_def br_def)
done
subgoal
apply (subst Down_id_eq)
apply (auto simp: sort_coeff_def intro!: RETURN_RES_refine)
apply (rule_tac x = ‹msort (λa b. a = b ∨ var_order a b) xs'› in exI)
apply (force intro!: msort_list_rel assms simp: f_def
dest: perfectly_shared_var_rel_unique_left
perfectly_shared_var_rel_unique_right[OF assms(2)])
done
done
qed
type_synonym sllist_polynomial = ‹(nat list × int) list›
definition sort_all_coeffs_s :: ‹(nat,string)shared_vars ⇒ sllist_polynomial ⇒ sllist_polynomial nres› where
‹sort_all_coeffs_s 𝒱 xs = monadic_nfoldli xs (λ_. RETURN True) (λ(a, n) b. do {ASSERT((a,n)∈set xs);a ← msort_coeff_s 𝒱 a; RETURN ((a, n) # b)}) []›
fun merge_coeffs0_s :: ‹sllist_polynomial ⇒ sllist_polynomial› where
‹merge_coeffs0_s[] = []› |
‹merge_coeffs0_s [(xs, n)] = (if n = 0 then [] else [(xs, n)])› |
‹merge_coeffs0_s ((xs, n) # (ys, m) # p) =
(if xs = ys
then if n + m ≠ 0 then merge_coeffs0_s ((xs, n + m) # p) else merge_coeffs0_s p
else if n = 0 then merge_coeffs0_s ((ys, m) # p)
else(xs, n) # merge_coeffs0_s ((ys, m) # p))›
lemma merge_coeffs0_s_merge_coeffs0:
fixes xs :: ‹sllist_polynomial› and
𝒱 :: ‹(nat,string)shared_vars›
assumes
‹(xs, xs') ∈ perfectly_shared_polynom 𝒱› and
𝒱: ‹(𝒱, 𝒟𝒱) ∈ perfectly_shared_vars_rel›
shows ‹(merge_coeffs0_s xs, merge_coeffs0 xs') ∈ perfectly_shared_polynom 𝒱›
using assms
apply (induction xs' arbitrary: xs rule: merge_coeffs0.induct)
subgoal by auto
subgoal by (auto simp: list_rel_split_left_iff)
subgoal premises p for xs n ys m p xsa
using p(1)[of ‹(_, _ + _) # tl (tl xsa)›] p(2)[of ‹tl (tl xsa)›] p(3)[of ‹tl xsa›] p(4)[of ‹tl xsa›] p(5-)
using perfectly_shared_monom_unique_right[OF 𝒱, of _ xs]
perfectly_shared_monom_unique_left[of ‹fst (hd xsa)› _ 𝒱]
apply (auto 4 1 simp: list_rel_split_left_iff
dest: )
apply smt
done
done
lemma list_rel_mono_strong: ‹A ∈ ⟨R⟩list_rel ⟹ (⋀xs. fst xs ∈ set (fst A) ⟹ snd xs ∈ set (snd A) ⟹ xs ∈ R ⟹ xs ∈ R') ⟹ A ∈ ⟨R'⟩list_rel›
unfolding list_rel_def
apply (cases A)
apply (simp add: list.rel_mono_strong)
done
definition full_normalize_poly_s where
‹full_normalize_poly_s 𝒱 p = do {
p ← sort_all_coeffs_s 𝒱 p;
p ← sort_poly_spec_s 𝒱 p;
RETURN (merge_coeffs0_s p)
}›
lemma sort_all_coeffs_s_sort_all_coeffs:
fixes xs :: ‹sllist_polynomial› and
𝒱 :: ‹(nat,string)shared_vars›
assumes
‹(xs, xs') ∈ perfectly_shared_polynom 𝒱› and
𝒱: ‹(𝒱, 𝒟𝒱) ∈ perfectly_shared_vars_rel› and
‹vars_llist xs' ⊆ set_mset 𝒟𝒱›
shows ‹sort_all_coeffs_s 𝒱 xs ≤ ⇓(perfectly_shared_polynom 𝒱) (sort_all_coeffs xs')›
proof -
have [refine]: ‹(xs, xs') ∈ ⟨{(a,b). a∈set xs ∧ (a,b)∈ perfectly_shared_monom 𝒱 ×⇩r int_rel}⟩list_rel›
by (rule list_rel_mono_strong[OF assms(1)])
(use assms(3) in auto)
show ?thesis
unfolding sort_all_coeffs_s_def sort_all_coeffs_def
apply (refine_vcg 𝒱 msort_coeff_s_sort_coeff)
subgoal by auto
subgoal by auto
subgoal by auto
subgoal using assms by (auto dest!: split_list)
subgoal by auto
done
qed
definition vars_llist_in_s :: ‹(nat, string) shared_vars ⇒ llist_polynomial ⇒ bool› where
‹vars_llist_in_s = (λ(𝒱,𝒟,𝒟') p. vars_llist p ⊆ set_mset (dom_m 𝒟'))›
lemma vars_llist_in_s_vars_llist[simp]:
assumes ‹(𝒱, 𝒟𝒱) ∈ perfectly_shared_vars_rel›
shows ‹vars_llist_in_s 𝒱 p ⟷ vars_llist p ⊆ set_mset 𝒟𝒱›
using assms unfolding perfectly_shared_vars_rel_def perfectly_shared_vars_def vars_llist_in_s_def
by auto
definition (in -)add_poly_l_s :: ‹(nat,string)shared_vars ⇒ sllist_polynomial × sllist_polynomial ⇒ sllist_polynomial nres› where
‹add_poly_l_s 𝒟 = REC⇩T
(λadd_poly_l (p, q).
case (p,q) of
(p, []) ⇒ RETURN p
| ([], q) ⇒ RETURN q
| ((xs, n) # p, (ys, m) # q) ⇒ do {
comp ← perfect_shared_term_order_rel_s 𝒟 xs ys;
if comp = EQUAL then if n + m = 0 then add_poly_l (p, q)
else do {
pq ← add_poly_l (p, q);
RETURN ((xs, n + m) # pq)
}
else if comp = LESS
then do {
pq ← add_poly_l (p, (ys, m) # q);
RETURN ((xs, n) # pq)
}
else do {
pq ← add_poly_l ((xs, n) # p, q);
RETURN ((ys, m) # pq)
}
})›
lemma add_poly_l_s_add_poly_l:
fixes xs :: ‹sllist_polynomial × sllist_polynomial›
assumes ‹(𝒱, 𝒱𝒟) ∈ perfectly_shared_vars_rel› and
‹(xs, xs') ∈ perfectly_shared_polynom 𝒱 ×⇩r perfectly_shared_polynom 𝒱›
shows ‹add_poly_l_s 𝒱 xs ≤ ⇓(perfectly_shared_polynom 𝒱) (add_poly_l_prep 𝒱𝒟 xs')›
proof -
have x: ‹x ∈ ⟨perfectly_shared_monom 𝒱 ×⇩r int_rel⟩list_rel ⟹ x ∈ ⟨perfectly_shared_monom 𝒱 ×⇩r int_rel⟩list_rel› for x
by auto
show ?thesis
unfolding add_poly_l_s_def add_poly_l_prep_def
apply (refine_rcg assms perfect_shared_term_order_rel_s_perfect_shared_term_order_rel)
apply (rule x)
subgoal by auto
apply (rule x)
subgoal by auto
subgoal by auto
subgoal by auto
apply (rule x)
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
by (auto)
qed
definition (in -) mult_monoms_s :: ‹(nat,string)shared_vars ⇒ nat list ⇒ nat list ⇒ nat list nres› where
‹mult_monoms_s 𝒟 xs ys = REC⇩T (λf (xs, ys).
do {
if xs = [] then RETURN ys
else if ys = [] then RETURN xs
else do {
ASSERT(xs ≠ [] ∧ ys ≠ []);
comp ← perfect_shared_var_order_s 𝒟 (hd xs) (hd ys);
if comp = EQUAL then do {
pq ← f (tl xs, tl ys);
RETURN (hd xs # pq)
}
else if comp = LESS then do {
pq ← f (tl xs, ys);
RETURN (hd xs # pq)
}
else do {
pq ← f (xs, tl ys);
RETURN (hd ys # pq)
}
}
}) (xs, ys)›
lemma mult_monoms_s_simps:
‹mult_monoms_s 𝒱 xs ys =
do {
if xs = [] then RETURN ys
else if ys = [] then RETURN xs
else do {
ASSERT(xs ≠ [] ∧ ys ≠ []);
comp ← perfect_shared_var_order_s 𝒱 (hd xs) (hd ys);
if comp = EQUAL then do {
pq ← mult_monoms_s 𝒱 (tl xs) (tl ys);
RETURN (hd xs # pq)
}
else if comp = LESS then do {
pq ← mult_monoms_s 𝒱 (tl xs) ys;
RETURN (hd xs # pq)
}
else do {
pq ← mult_monoms_s 𝒱 xs (tl ys);
RETURN (hd ys # pq)
}
}
}›
apply (subst mult_monoms_s_def)
apply (subst RECT_unfold, refine_mono)
unfolding prod.case[of _ ‹(xs,ys)›]
apply (subst mult_monoms_s_def[symmetric])+
apply (auto intro!: bind_cong[OF refl])
done
lemma mult_monoms_s_mult_monoms_prep:
fixes xs
assumes ‹(𝒱, 𝒱𝒟) ∈ perfectly_shared_vars_rel› and
‹(xs, xs') ∈ perfectly_shared_monom 𝒱›
‹(ys, ys') ∈ perfectly_shared_monom 𝒱›
shows ‹mult_monoms_s 𝒱 xs ys ≤ ⇓(perfectly_shared_monom 𝒱) ((mult_monoms_prep 𝒱𝒟 xs' ys'))›
proof -
have [refine]: ‹((xs, ys), xs', ys') ∈ perfectly_shared_monom 𝒱 ×⇩r perfectly_shared_monom 𝒱›
using assms by auto
have x: ‹a ≤ ⇓ (perfectly_shared_monom 𝒱) b ⟹ a ≤ ⇓ (perfectly_shared_monom 𝒱) b› for a b
by auto
show ?thesis
using assms unfolding mult_monoms_s_def mult_monoms_prep_def
apply (refine_vcg perfect_shared_var_order_s_perfect_shared_var_order)
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by (auto simp: neq_Nil_conv)
subgoal by (auto simp: neq_Nil_conv)
subgoal by auto
apply (rule x)
subgoal by (auto simp: neq_Nil_conv)
subgoal by (auto simp: neq_Nil_conv)
subgoal by auto
apply (rule x)
subgoal by (auto simp: neq_Nil_conv)
subgoal by (auto simp: neq_Nil_conv)
apply (rule x)
subgoal by (auto simp: neq_Nil_conv)
subgoal by (auto simp: neq_Nil_conv)
done
qed
definition (in -) mult_term_s
:: ‹(nat,string)shared_vars⇒ sllist_polynomial ⇒ _ ⇒ sllist_polynomial ⇒ sllist_polynomial nres›
where
‹mult_term_s = (λ𝒱 qs (p, m) b. nfoldli qs (λ_. True) (λ(q, n) b. do {pq ← mult_monoms_s 𝒱 p q; RETURN ((pq, m * n) # b)}) b)›
definition mult_poly_s :: ‹(nat,string) shared_vars⇒ sllist_polynomial ⇒ sllist_polynomial ⇒ sllist_polynomial nres› where
‹mult_poly_s 𝒱 p q = nfoldli p (λ_. True) (mult_term_s 𝒱 q) []›
lemma mult_term_s_mult_monoms_prop:
fixes xs
assumes ‹(𝒱, 𝒱𝒟) ∈ perfectly_shared_vars_rel› and
‹(xs, xs') ∈ perfectly_shared_polynom 𝒱›
‹(ys, ys') ∈ perfectly_shared_monom 𝒱 ×⇩r int_rel›
‹(zs, zs') ∈ perfectly_shared_polynom 𝒱›
shows ‹mult_term_s 𝒱 xs ys zs ≤ ⇓(perfectly_shared_polynom 𝒱) (mult_monoms_prop 𝒱𝒟 xs' ys' zs')›
proof -
show ?thesis
using assms
unfolding mult_term_s_def mult_monoms_prop_def
by (refine_rcg mult_monoms_s_mult_monoms_prep)
auto
qed
lemma mult_poly_s_mult_poly_raw_prop:
fixes xs
assumes ‹(𝒱, 𝒱𝒟) ∈ perfectly_shared_vars_rel› and
‹(xs, xs') ∈ perfectly_shared_polynom 𝒱›
‹(ys, ys') ∈ perfectly_shared_polynom 𝒱›
shows ‹mult_poly_s 𝒱 xs ys ≤ ⇓(perfectly_shared_polynom 𝒱) (mult_poly_raw_prop 𝒱𝒟 xs' ys')›
proof -
show ?thesis
using assms
unfolding mult_poly_s_def mult_poly_raw_prop_def
by (refine_rcg mult_term_s_mult_monoms_prop)
auto
qed
lemma op_eq_uint64_nat[sepref_fr_rules]:
‹(uncurry (return oo ((=) :: uint64 ⇒ _)), uncurry (RETURN oo (=))) ∈
uint64_nat_assn⇧k *⇩a uint64_nat_assn⇧k →⇩a bool_assn›
by sepref_to_hoare (sep_auto simp: uint64_nat_rel_def br_def)
abbreviation ordered_assn :: ‹ordered ⇒ _ ⇒ _› where
‹ordered_assn ≡ id_assn›
lemma op_eq_ordered_assn[sepref_fr_rules]:
‹(uncurry (return oo ((=) :: ordered ⇒ _)), uncurry (RETURN oo (=))) ∈
ordered_assn⇧k *⇩a ordered_assn⇧k →⇩a bool_assn›
by sepref_to_hoare (sep_auto simp: uint64_nat_rel_def br_def)
abbreviation monom_s_rel where
‹monom_s_rel ≡ ⟨uint64_nat_rel⟩list_rel›
abbreviation monom_s_assn where
‹monom_s_assn ≡ list_assn uint64_nat_assn›
abbreviation poly_s_assn where
‹poly_s_assn ≡ list_assn (monom_s_assn ×⇩a int_assn)›
sepref_decl_intf wordered is ordered
sepref_register EQUAL LESS GREATER UNKNOWN get_var_nameS perfect_shared_var_order_s perfect_shared_term_order_rel_s
lemma [sepref_fr_rules]:
‹(uncurry0 (return EQUAL), uncurry0 (RETURN EQUAL)) ∈ unit_assn⇧k →⇩a id_assn›
‹(uncurry0 (return LESS), uncurry0 (RETURN LESS)) ∈ unit_assn⇧k →⇩a id_assn›
‹(uncurry0 (return GREATER), uncurry0 (RETURN GREATER)) ∈ unit_assn⇧k →⇩a id_assn›
‹(uncurry0 (return UNKNOWN), uncurry0 (RETURN UNKNOWN)) ∈ unit_assn⇧k →⇩a id_assn›
by (sepref_to_hoare; sep_auto)+
sepref_definition perfect_shared_var_order_s_impl
is ‹uncurry2 perfect_shared_var_order_s›
:: ‹shared_vars_assn⇧k *⇩a uint64_nat_assn⇧k *⇩a uint64_nat_assn⇧k →⇩a id_assn›
unfolding perfect_shared_var_order_s_def perfectly_shared_strings_equal_l_def
term_order_rel'_def[symmetric]
term_order_rel'_alt_def
var_order_rel''
by sepref
lemmas [sepref_fr_rules] = perfect_shared_var_order_s_impl.refine
sepref_definition perfect_shared_term_order_rel_s_impl
is ‹uncurry2 perfect_shared_term_order_rel_s›
:: ‹shared_vars_assn⇧k *⇩a monom_s_assn⇧k *⇩a monom_s_assn⇧k →⇩a id_assn›
unfolding perfect_shared_term_order_rel_s_def
by sepref
lemmas [sepref_fr_rules] = perfect_shared_term_order_rel_s_impl.refine
sepref_definition add_poly_l_prep_impl
is ‹uncurry add_poly_l_s›
:: ‹shared_vars_assn⇧k *⇩a (poly_s_assn ×⇩a poly_s_assn)⇧k →⇩a poly_s_assn›
unfolding add_poly_l_s_def
HOL_list.fold_custom_empty
term_order_rel'_def[symmetric]
term_order_rel'_alt_def
by sepref
lemma [sepref_fr_rules]:
‹(return o is_Nil, RETURN o is_Nil)∈ (list_assn R)⇧k →⇩a bool_assn›
by (sepref_to_hoare)
(sep_auto split: list.splits)
sepref_definition mult_monoms_s_impl
is ‹uncurry2 mult_monoms_s›
:: ‹shared_vars_assn⇧k *⇩a monom_s_assn⇧k *⇩a monom_s_assn⇧k →⇩a monom_s_assn›
unfolding mult_monoms_s_def conv_to_is_Nil
unfolding
HOL_list.fold_custom_empty
term_order_rel'_def[symmetric]
term_order_rel'_alt_def
by sepref
lemmas [sepref_fr_rules] =
mult_monoms_s_impl.refine
sepref_definition mult_term_s_impl
is ‹uncurry3 mult_term_s›
:: ‹shared_vars_assn⇧k *⇩a poly_s_assn⇧k *⇩a (monom_s_assn ×⇩a int_assn)⇧k *⇩a poly_s_assn⇧k→⇩a poly_s_assn›
unfolding mult_term_s_def conv_to_is_Nil
unfolding
HOL_list.fold_custom_empty
term_order_rel'_def[symmetric]
term_order_rel'_alt_def
by sepref
lemmas [sepref_fr_rules] =
mult_term_s_impl.refine
sepref_definition mult_poly_s_impl
is ‹uncurry2 mult_poly_s›
:: ‹shared_vars_assn⇧k *⇩a poly_s_assn⇧k *⇩a poly_s_assn⇧k→⇩a poly_s_assn›
unfolding mult_poly_s_def conv_to_is_Nil
unfolding
HOL_list.fold_custom_empty
by sepref
lemmas [sepref_fr_rules] =
mult_poly_s_impl.refine
sepref_register take drop
lemma [sepref_fr_rules]:
assumes ‹CONSTRAINT is_pure R›
shows ‹(uncurry (return oo take), uncurry (RETURN oo take)) ∈ nat_assn⇧k *⇩a (list_assn R)⇧k →⇩a list_assn R›
apply sepref_to_hoare
using assms unfolding is_pure_conv CONSTRAINT_def
apply (sep_auto simp add: list_assn_pure_conv)
apply (sep_auto simp: pure_def list_rel_takeD)
done
lemma [sepref_fr_rules]:
assumes ‹CONSTRAINT is_pure R›
shows ‹(uncurry (return oo drop), uncurry (RETURN oo drop)) ∈ nat_assn⇧k *⇩a (list_assn R)⇧k →⇩a list_assn R›
apply sepref_to_hoare
using assms unfolding is_pure_conv CONSTRAINT_def
apply (sep_auto simp add: list_assn_pure_conv)
apply (sep_auto simp: pure_def list_rel_dropD)
done
definition mergeR_vars :: ‹(nat, string) shared_vars ⇒ sllist_polynomial ⇒ sllist_polynomial ⇒ sllist_polynomial nres› where
‹mergeR_vars 𝒱 = mergeR
(λxs ys. (∀a∈set (fst xs). a ∈# dom_m (fst (snd 𝒱))) ∧ (∀a∈set(fst ys). a ∈# dom_m (fst (snd 𝒱))))
(λxs ys. do {a ← perfect_shared_term_order_rel_s 𝒱 (fst xs) (fst ys); RETURN (a ≠ GREATER)})›
lemma mergeR_alt_def:
‹(mergeR Φ f xs ys) = REC⇩T(λmergeR xs.
case xs of
([], ys) ⇒ RETURN ys
| (xs, []) ⇒ RETURN xs
| (x # xs, y # ys) ⇒ do {
ASSERT(Φ x y);
b ← f x y;
if b then do {
zs ← mergeR (xs, y # ys);
RETURN (x # zs)
}
else do {
zs ← mergeR (x # xs, ys);
RETURN (y # zs)
}
})
(xs, ys)›
apply (induction Φ f xs ys rule: mergeR.induct)
subgoal
apply (subst RECT_unfold, refine_mono)
apply (simp add:)
apply (rule bind_cong[OF refl])+
apply auto
done
subgoal
by (subst RECT_unfold, refine_mono)
(simp split: list.splits)
subgoal
by (subst RECT_unfold, refine_mono) auto
done
sepref_definition mergeR_vars_impl
is ‹uncurry2 mergeR_vars›
:: ‹shared_vars_assn⇧k *⇩a poly_s_assn⇧k *⇩a poly_s_assn⇧k →⇩a poly_s_assn›
supply [[goals_limit = 1]]
unfolding mergeR_vars_def mergeR_alt_def
by sepref
lemmas [sepref_fr_rules] =
mergeR_vars_impl.refine
abbreviation msortR_vars where
‹msortR_vars ≡ sort_poly_spec_s›
lemmas msortR_vars_def = sort_poly_spec_s_def
sepref_register mergeR_vars msortR_vars
sepref_definition msortR_vars_impl
is ‹uncurry msortR_vars›
:: ‹shared_vars_assn⇧k *⇩a poly_s_assn⇧k →⇩a poly_s_assn›
supply [[goals_limit = 1]]
unfolding msortR_vars_def msortR_alt_def mergeR_vars_def[symmetric]
by sepref
lemmas [sepref_fr_rules] =
msortR_vars_impl.refine
fun merge_coeffs_s :: ‹sllist_polynomial ⇒ sllist_polynomial› where
‹merge_coeffs_s [] = []› |
‹merge_coeffs_s [(xs, n)] = [(xs, n)]› |
‹merge_coeffs_s ((xs, n) # (ys, m) # p) =
(if xs = ys
then if n + m ≠ 0 then merge_coeffs_s ((xs, n + m) # p) else merge_coeffs_s p
else (xs, n) # merge_coeffs_s ((ys, m) # p))›
lemma perfectly_shared_merge_coeffs_merge_coeffs:
assumes
‹(𝒱, 𝒟𝒱) ∈ perfectly_shared_vars_rel›
‹(xs, xs') ∈ perfectly_shared_polynom 𝒱›
shows ‹(merge_coeffs_s xs, merge_coeffs xs') ∈ (perfectly_shared_polynom 𝒱)›
using assms
apply (induction xs arbitrary: xs' rule: merge_coeffs_s.induct)
subgoal
by auto
subgoal
by (auto simp: list_rel_split_right_iff)
subgoal
by(auto simp: list_rel_split_right_iff dest: perfectly_shared_monom_unique_left
perfectly_shared_monom_unique_right)
done
definition normalize_poly_s :: ‹_› where
‹normalize_poly_s 𝒱 p = do {
p ← msortR_vars 𝒱 p;
RETURN (merge_coeffs_s p)
}›
lemma normalize_poly_s_normalize_poly_s:
assumes
‹(𝒱, 𝒟𝒱) ∈ perfectly_shared_vars_rel›
‹(xs, xs') ∈ perfectly_shared_polynom 𝒱› and
‹vars_llist xs' ⊆ set_mset 𝒟𝒱›
shows ‹normalize_poly_s 𝒱 xs ≤ ⇓ (perfectly_shared_polynom 𝒱) (normalize_poly xs')›
unfolding normalize_poly_s_def normalize_poly_def
by (refine_rcg sort_poly_spec_s_sort_poly_spec[unfolded msortR_vars_def[symmetric]] assms
perfectly_shared_merge_coeffs_merge_coeffs)
definition check_linear_combi_l_s_dom_err :: ‹sllist_polynomial ⇒ nat ⇒ string nres› where
‹check_linear_combi_l_s_dom_err p r = SPEC (λ_. True)›
definition mult_poly_full_s :: ‹_› where
‹mult_poly_full_s 𝒱 p q = do {
pq ← mult_poly_s 𝒱 p q;
normalize_poly_s 𝒱 pq
}›
lemma mult_poly_full_s_mult_poly_full_prop:
assumes
‹(𝒱, 𝒟𝒱) ∈ perfectly_shared_vars_rel›
‹(xs, xs') ∈ perfectly_shared_polynom 𝒱› and
‹(ys, ys') ∈ perfectly_shared_polynom 𝒱› and
‹vars_llist xs' ⊆ set_mset 𝒟𝒱› and
‹vars_llist ys' ⊆ set_mset 𝒟𝒱›
shows ‹mult_poly_full_s 𝒱 xs ys ≤ ⇓ (perfectly_shared_polynom 𝒱) (mult_poly_full_prop 𝒟𝒱 xs' ys')›
unfolding mult_poly_full_s_def mult_poly_full_prop_def
by (refine_rcg mult_poly_s_mult_poly_raw_prop assms normalize_poly_s_normalize_poly_s)
(use assms in auto)
definition (in -)linear_combi_l_prep_s
:: ‹nat ⇒ _ ⇒ (nat, string) shared_vars ⇒ _ ⇒ (sllist_polynomial × (llist_polynomial × nat) list × string code_status) nres›
where
‹linear_combi_l_prep_s i A 𝒱 xs = do {
WHILE⇩T
(λ(p, xs, err). xs ≠ [] ∧ ¬is_cfailed err)
(λ(p, xs, _). do {
ASSERT(xs ≠ []);
let (q :: llist_polynomial, i) = hd xs;
if (i ∉# dom_m A ∨ ¬(vars_llist_in_s 𝒱 q))
then do {
err ← check_linear_combi_l_s_dom_err p i;
RETURN (p, xs, error_msg i err)
} else do {
ASSERT(fmlookup A i ≠ None);
let r = the (fmlookup A i);
if q = [([], 1)]
then do {
pq ← add_poly_l_s 𝒱 (p, r);
RETURN (pq, tl xs, CSUCCESS)}
else do {
(no_new, q) ← normalize_poly_sharedS 𝒱 (q);
q ← mult_poly_full_s 𝒱 q r;
pq ← add_poly_l_s 𝒱 (p, q);
RETURN (pq, tl xs, CSUCCESS)
}
}
})
([], xs, CSUCCESS)
}›
lemma normalize_poly_sharedS_normalize_poly_shared:
assumes
‹(𝒱, 𝒟𝒱) ∈ perfectly_shared_vars_rel›
‹(xs, xs') ∈ Id›
shows ‹normalize_poly_sharedS 𝒱 xs
≤ ⇓(bool_rel ×⇩r perfectly_shared_polynom 𝒱)
(normalize_poly_shared 𝒟𝒱 xs')›
proof -
have [refine]: ‹full_normalize_poly xs ≤ ⇓ Id (full_normalize_poly xs')›
using assms by auto
show ?thesis
unfolding normalize_poly_sharedS_def normalize_poly_shared_def
by (refine_rcg assms import_poly_no_newS_import_poly_no_new)
qed
lemma linear_combi_l_prep_s_linear_combi_l_prep:
assumes
‹(𝒱, 𝒟𝒱) ∈ perfectly_shared_vars_rel›
‹(A,B) ∈ ⟨nat_rel, perfectly_shared_polynom 𝒱⟩fmap_rel›
‹(xs,xs') ∈ Id›
shows ‹linear_combi_l_prep_s i A 𝒱 xs
≤ ⇓(perfectly_shared_polynom 𝒱 ×⇩r Id ×⇩r Id)
(linear_combi_l_prep2 j B 𝒟𝒱 xs')›
proof -
have [refine]: ‹check_linear_combi_l_s_dom_err a b
≤ ⇓ Id
(check_linear_combi_l_dom_err c d)› for a b c d
unfolding check_linear_combi_l_dom_err_def check_linear_combi_l_s_dom_err_def
by auto
show ?thesis
unfolding linear_combi_l_prep_s_def linear_combi_l_prep2_def
apply (refine_rcg normalize_poly_sharedS_normalize_poly_shared
mult_poly_full_s_mult_poly_full_prop add_poly_l_s_add_poly_l)
subgoal using assms by auto
subgoal by auto
subgoal by auto
subgoal using assms by auto
subgoal by auto
subgoal using fmap_rel_nat_rel_dom_m[OF assms(2)] unfolding in_dom_m_lookup_iff by auto
subgoal using assms by auto
subgoal using assms by auto
subgoal using assms by auto
subgoal by auto
subgoal using assms by auto
subgoal by auto
subgoal using assms by auto
subgoal by auto
subgoal using assms by auto
subgoal using assms by auto
subgoal by auto
subgoal by auto
done
qed
definition check_linear_combi_l_s_mult_err :: ‹sllist_polynomial ⇒ sllist_polynomial ⇒ string nres› where
‹check_linear_combi_l_s_mult_err pq r = SPEC (λ_. True)›
definition weak_equality_l_s :: ‹sllist_polynomial ⇒ sllist_polynomial ⇒ bool nres› where
‹weak_equality_l_s p q = RETURN (p = q)›
definition check_linear_combi_l_s where
‹check_linear_combi_l_s spec A 𝒱 i xs r = do {
(mem_err, r) ← import_poly_no_newS 𝒱 r;
if mem_err ∨ i ∈# dom_m A ∨ xs = []
then do {
err ← check_linear_combi_l_pre_err i (i ∈# dom_m A) (xs = []) (mem_err);
RETURN (error_msg i err, r)
}
else do {
(p, _, err) ← linear_combi_l_prep_s i A 𝒱 xs;
if (is_cfailed err)
then do {
RETURN (err, r)
}
else do {
b ← weak_equality_l_s p r;
b' ← weak_equality_l_s r spec;
if b then (if b' then RETURN (CFOUND, r) else RETURN (CSUCCESS, r)) else do {
c ← check_linear_combi_l_s_mult_err p r;
RETURN (error_msg i c, r)
}
}
}}›
definition weak_equality_l_s' :: ‹_› where
‹weak_equality_l_s' _ = weak_equality_l_s›
definition weak_equality_l' :: ‹_› where
‹weak_equality_l' _ = weak_equality_l›
lemma weak_equality_l_s_weak_equality_l:
fixes a :: sllist_polynomial and b :: llist_polynomial and 𝒱 :: ‹(nat,string)shared_vars›
assumes
‹(𝒱, 𝒟𝒱) ∈ perfectly_shared_vars_rel›
‹(a,b) ∈ perfectly_shared_polynom 𝒱›
‹(c,d) ∈ perfectly_shared_polynom 𝒱›
shows
‹weak_equality_l_s' 𝒱 a c ≤⇓bool_rel (weak_equality_l' 𝒟𝒱 b d)›
using assms perfectly_shared_polynom_unique_left[OF assms(2), of d]
perfectly_shared_polynom_unique_right[OF assms(1,2), of c]
unfolding weak_equality_l_s_def weak_equality_l_def weak_equality_l'_def
weak_equality_l_s'_def
by auto
lemma check_linear_combi_l_s_check_linear_combi_l:
assumes
‹(𝒱, 𝒟𝒱) ∈ perfectly_shared_vars_rel›
‹(A,B) ∈ ⟨nat_rel, perfectly_shared_polynom 𝒱⟩fmap_rel› and
‹(xs,xs')∈ Id›
‹(r,r')∈Id›
‹(i,j)∈nat_rel›
‹(spec, spec') ∈ perfectly_shared_polynom 𝒱›
shows ‹check_linear_combi_l_s spec A 𝒱 i r xs
≤ ⇓(Id ×⇩r perfectly_shared_polynom 𝒱)
(check_linear_combi_l_prop spec' B 𝒟𝒱 j r' xs')›
proof -
have [refine]: ‹check_linear_combi_l_pre_err a b c d ≤ ⇓Id (check_linear_combi_l_pre_err u x y z)›
for a b c d u x y z
by (auto simp: check_linear_combi_l_pre_err_def)
have [refine]: ‹check_linear_combi_l_s_mult_err a b ≤ ⇓Id (check_linear_combi_l_mult_err u x)›
for a b u x
by (auto simp: check_linear_combi_l_s_mult_err_def check_linear_combi_l_mult_err_def)
show ?thesis
unfolding check_linear_combi_l_s_def check_linear_combi_l_prop_def
apply (refine_rcg import_poly_no_newS_import_poly_no_new assms
linear_combi_l_prep_s_linear_combi_l_prep weak_equality_l_s_weak_equality_l[unfolded weak_equality_l'_def
weak_equality_l_s'_def])
subgoal using assms by auto
subgoal using assms by auto
subgoal using assms by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal using assms by auto
done
qed
definition check_extension_l_s_new_var_multiple_err :: ‹string ⇒ sllist_polynomial ⇒ string nres› where
‹check_extension_l_s_new_var_multiple_err v p = SPEC (λ_. True)›
definition check_extension_l_s_side_cond_err
:: ‹string ⇒ sllist_polynomial ⇒ sllist_polynomial ⇒ sllist_polynomial ⇒ string nres›
where
‹check_extension_l_s_side_cond_err v p p' q = SPEC (λ_. True)›
term is_new_variable
definition (in -)check_extension_l2_s
:: ‹_ ⇒ _ ⇒ (nat,string)shared_vars ⇒ nat ⇒ string ⇒ llist_polynomial ⇒
(string code_status × sllist_polynomial × (nat,string)shared_vars × nat) nres›
where
‹check_extension_l2_s spec A 𝒱 i v p = do {
n ← is_new_variableS v 𝒱;
let pre = i ∉# dom_m A ∧ n;
let nonew = vars_llist_in_s 𝒱 p;
(mem, p, 𝒱) ← import_polyS 𝒱 p;
let pre = (pre ∧ ¬alloc_failed mem);
if ¬pre
then do {
c ← check_extension_l_dom_err i;
RETURN (error_msg i c, [], 𝒱, 0)
} else do {
if ¬nonew
then do {
c ← check_extension_l_s_new_var_multiple_err v p;
RETURN (error_msg i c, [], 𝒱, 0)
}
else do {
(mem', 𝒱, v') ← import_variableS v 𝒱;
if alloc_failed mem'
then do {
c ← check_extension_l_dom_err i;
RETURN (error_msg i c, [], 𝒱, 0)
} else
do {
p2 ← mult_poly_full_s 𝒱 p p;
let p'' = map (λ(a,b). (a, -b)) p;
q ← add_poly_l_s 𝒱 (p2, p'');
eq ← weak_equality_l_s q [];
if eq then do {
RETURN (CSUCCESS, p, 𝒱, v')
} else do {
c ← check_extension_l_s_side_cond_err v p p'' q;
RETURN (error_msg i c, [], 𝒱, v')
}
}
}
}
}›
lemma list_rel_tlD: ‹(a, b) ∈ ⟨R⟩list_rel ⟹ (tl a, tl b) ∈ ⟨R⟩list_rel›
by (metis list.sel(2) list.sel(3) list_rel_simp(1) list_rel_simp(2) list_rel_simp(4) neq_NilE)
lemma check_extension_l2_prop_alt_def:
‹check_extension_l2_prop spec A 𝒱 i v p = do {
n ← is_new_variable v 𝒱;
let pre = i ∉# dom_m A ∧ n;
let nonew = vars_llist p ⊆ set_mset 𝒱;
(mem, p, 𝒱) ← import_poly 𝒱 p;
(mem', 𝒱, va) ← if pre ∧ nonew ∧ ¬ alloc_failed mem then import_variable v 𝒱 else RETURN (mem, 𝒱, v);
let pre = ((pre ∧ ¬alloc_failed mem) ∧ ¬alloc_failed mem');
if ¬pre
then do {
c ← check_extension_l_dom_err i;
RETURN (error_msg i c, [], 𝒱, va)
} else do {
if ¬nonew
then do {
c ← check_extension_l_new_var_multiple_err v p;
RETURN (error_msg i c, [], 𝒱, va)
}
else do {
ASSERT(vars_llist p ⊆ set_mset 𝒱);
p2 ← mult_poly_full_prop 𝒱 p p;
ASSERT(vars_llist p2 ⊆ set_mset 𝒱);
let p'' = map (λ(a,b). (a, -b)) p;
ASSERT(vars_llist p'' ⊆ set_mset 𝒱);
q ← add_poly_l_prep 𝒱 (p2, p'');
ASSERT(vars_llist q ⊆ set_mset 𝒱);
eq ← weak_equality_l q [];
if eq then do {
RETURN (CSUCCESS, p, 𝒱, va)
} else do {
c ← check_extension_l_side_cond_err v p q;
RETURN (error_msg i c, [], 𝒱, va)
}
}
}
}›
unfolding check_extension_l2_prop_def Let_def check_extension_l_side_cond_err_def
is_new_variable_def
by (auto intro!: bind_cong[OF refl])
lemma check_extension_l2_prop_alt_def2:
‹check_extension_l2_prop spec A 𝒱 i v p = do {
n ← is_new_variable v 𝒱;
let pre = i ∉# dom_m A ∧ n;
let nonew = vars_llist p ⊆ set_mset 𝒱;
(mem, p, 𝒱) ← import_poly 𝒱 p;
let pre = (pre ∧ ¬alloc_failed mem);
if ¬pre
then do {
c ← check_extension_l_dom_err i;
RETURN (error_msg i c, [], 𝒱, v)
} else do {
if ¬nonew
then do {
c ← check_extension_l_new_var_multiple_err v p;
RETURN (error_msg i c, [], 𝒱, v)
}
else do {
(mem', 𝒱, va) ← import_variable v 𝒱;
if (alloc_failed mem')
then do {
c ← check_extension_l_dom_err i;
RETURN (error_msg i c, [], 𝒱, va)
}
else do {
ASSERT(vars_llist p ⊆ set_mset 𝒱);
p2 ← mult_poly_full_prop 𝒱 p p;
ASSERT(vars_llist p2 ⊆ set_mset 𝒱);
let p'' = map (λ(a,b). (a, -b)) p;
ASSERT(vars_llist p'' ⊆ set_mset 𝒱);
q ← add_poly_l_prep 𝒱 (p2, p'');
ASSERT(vars_llist q ⊆ set_mset 𝒱);
eq ← weak_equality_l q [];
if eq then do {
RETURN (CSUCCESS, p, 𝒱, va)
} else do {
c ← check_extension_l_side_cond_err v p q;
RETURN (error_msg i c, [], 𝒱, va)
}
}
}
}
}›
unfolding check_extension_l2_prop_alt_def
unfolding Let_def check_extension_l_side_cond_err_def de_Morgan_conj
not_not
by (subst if_conn(2))
(auto intro!: bind_cong[OF refl])
lemma list_rel_mapI: ‹(xs,ys) ∈ ⟨R⟩list_rel ⟹ (⋀x y. x ∈ set xs ⟹ y ∈ set ys ⟹ (x,y)∈R ⟹ (f x, g y) ∈ S) ⟹ (map f xs, map g ys) ∈ ⟨S⟩list_rel›
by (induction xs arbitrary: ys)
(auto simp: list_rel_split_right_iff)
lemma perfectly_shared_var_rel_perfectly_shared_monom_mono:
‹(∀xs. xs ∈ perfectly_shared_var_rel 𝒜 ⟶ xs ∈ perfectly_shared_var_rel 𝒜') ⟷
(∀xs. xs ∈ perfectly_shared_monom 𝒜 ⟶ xs ∈ perfectly_shared_monom 𝒜')›
by (metis list_rel_mono old.prod.exhaust list_rel_simp(2) list_rel_simp(4))
lemma perfectly_shared_var_rel_perfectly_shared_polynom_mono:
‹(∀xs. xs ∈ perfectly_shared_var_rel 𝒜 ⟶ xs ∈ perfectly_shared_var_rel 𝒜') ⟷
(∀xs. xs ∈ perfectly_shared_polynom 𝒜 ⟶ xs ∈ perfectly_shared_polynom 𝒜')›
unfolding perfectly_shared_var_rel_perfectly_shared_monom_mono
apply (auto intro: list_rel_mono)
apply (drule_tac x = ‹[(a,1)]› in spec)
apply (drule_tac x = ‹[(b,1)]› in spec)
apply auto
done
lemma check_extension_l2_s_check_extension_l2:
assumes
‹(𝒱, 𝒟𝒱) ∈ perfectly_shared_vars_rel›
‹(A,B) ∈ ⟨nat_rel, perfectly_shared_polynom 𝒱⟩fmap_rel› and
‹(r,r')∈Id›
‹(i,j)∈nat_rel›
‹(spec, spec') ∈ perfectly_shared_polynom 𝒱›
‹(v,v')∈Id›
shows ‹check_extension_l2_s spec A 𝒱 i v r
≤ ⇓{((err, p, A, v), (err', p', A', v')).
(err, err') ∈ Id ∧
(¬is_cfailed err ⟶
(p, p') ∈ perfectly_shared_polynom A ∧ (v, v') ∈ perfectly_shared_var_rel A ∧
(A, A') ∈ {(a,b). (a,b) ∈ perfectly_shared_vars_rel ∧ perfectly_shared_polynom 𝒱 ⊆ perfectly_shared_polynom a})}
(check_extension_l2_prop spec' B 𝒟𝒱 j v' r')›
proof -
have [refine]: ‹check_extension_l_s_new_var_multiple_err a b ≤⇓Id (check_extension_l_new_var_multiple_err a' b')› for a a' b b'
by (auto simp: check_extension_l_s_new_var_multiple_err_def check_extension_l_new_var_multiple_err_def)
have [refine]: ‹check_extension_l_dom_err i ≤ ⇓ (Id) (check_extension_l_dom_err j)›
by (auto simp: check_extension_l_dom_err_def)
have [refine]: ‹check_extension_l_s_side_cond_err a b c d ≤ ⇓Id (check_extension_l_side_cond_err a' b' c')› for a b c d a' b' c' d'
by (auto simp: check_extension_l_s_side_cond_err_def check_extension_l_side_cond_err_def)
have G: ‹(a, b) ∈ import_poly_rel 𝒱 x ⟹ ¬alloc_failed (fst a) ⟹
(snd (snd a), snd (snd b)) ∈ perfectly_shared_vars_rel› for a b x
by auto
show ?thesis
unfolding check_extension_l2_s_def check_extension_l2_prop_alt_def2 nres_monad3
apply (refine_rcg import_polyS_import_poly assms mult_poly_full_s_mult_poly_full_prop
import_variableS_import_variable[unfolded perfectly_shared_var_rel_perfectly_shared_polynom_mono]
is_new_variable_spec)
subgoal using assms by auto
subgoal using assms by (auto simp add: perfectly_shared_vars_rel_def perfectly_shared_vars_def)
subgoal using assms by (auto)
subgoal using assms by (auto)
subgoal using assms by (auto)
subgoal using assms by auto
subgoal by auto
subgoal using assms by auto
subgoal using assms by auto
subgoal using assms by auto
subgoal using assms by auto
apply (rule add_poly_l_s_add_poly_l)
subgoal by auto
subgoal for _ _ x x' x1 x2 x1a x2a x1b x2b x1c x2c xa x'a x1d x2d x1e x2e x1f x2f x1g x2g p2 p2a
using assms
by ( auto intro!: list_rel_mapI[of _ _ ‹perfectly_shared_monom x1g ×⇩r int_rel›])
apply (rule weak_equality_l_s_weak_equality_l[unfolded weak_equality_l'_def
weak_equality_l_s'_def])
defer apply assumption
subgoal by auto
subgoal by auto
subgoal by auto
subgoal using assms by auto
apply (solves auto)
done
qed
definition PAC_checker_l_step_s
:: ‹sllist_polynomial ⇒ string code_status × (nat,string)shared_vars × _ ⇒ (llist_polynomial, string, nat) pac_step ⇒ _›
where
‹PAC_checker_l_step_s = (λspec (st', 𝒱, A) st. do {
ASSERT (¬is_cfailed st');
case st of
CL _ _ _ ⇒
do {
r ← full_normalize_poly (pac_res st);
(eq, r) ← check_linear_combi_l_s spec A 𝒱 (new_id st) (pac_srcs st) r;
let _ = eq;
if ¬is_cfailed eq
then RETURN (merge_cstatus st' eq, 𝒱, fmupd (new_id st) r A)
else RETURN (eq, 𝒱, A)
}
| Del _ ⇒
do {
eq ← check_del_l spec A (pac_src1 st);
let _ = eq;
if ¬is_cfailed eq
then RETURN (merge_cstatus st' eq, 𝒱, fmdrop (pac_src1 st) A)
else RETURN (eq, 𝒱, A)
}
| Extension _ _ _ ⇒
do {
r ← full_normalize_poly (pac_res st);
(eq, r, 𝒱, v) ← check_extension_l2_s spec A (𝒱) (new_id st) (new_var st) r;
if ¬is_cfailed eq
then do {
r ← add_poly_l_s 𝒱 ([([v], -1)], r);
RETURN (st', 𝒱, fmupd (new_id st) r A)
}
else RETURN (eq, 𝒱, A)
}}
)›
lemma is_cfailed_merge_cstatus:
"is_cfailed (merge_cstatus c d) ⟷ is_cfailed c ∨ is_cfailed d"
by (cases c; cases d) auto
lemma (in -) fmap_rel_mono2:
‹x ∈ ⟨A,B⟩fmap_rel ⟹ B ⊆B' ⟹ x ∈ ⟨A,B'⟩fmap_rel›
by (auto simp: fmap_rel_alt_def)
lemma PAC_checker_l_step_s_PAC_checker_l_step_s:
assumes
‹(𝒱, 𝒟𝒱) ∈ perfectly_shared_vars_rel›
‹(A,B) ∈ ⟨nat_rel, perfectly_shared_polynom 𝒱⟩fmap_rel› and
‹(spec, spec') ∈ perfectly_shared_polynom 𝒱› and
‹(err, err') ∈ Id› and
‹(st,st')∈Id›
shows ‹PAC_checker_l_step_s spec (err, 𝒱, A) st
≤ ⇓{((err, 𝒱', A'), (err', 𝒟𝒱', B')).
(err, err') ∈ Id ∧
(¬is_cfailed err ⟶ ((𝒱', 𝒟𝒱') ∈ perfectly_shared_vars_rel ∧(A',B') ∈ ⟨nat_rel, perfectly_shared_polynom 𝒱'⟩fmap_rel ∧
perfectly_shared_polynom 𝒱 ⊆ perfectly_shared_polynom 𝒱'))}
(PAC_checker_l_step_prep spec' (err', 𝒟𝒱, B) st')›
proof -
have [refine]: ‹check_del_l spec A (EPAC_Checker_Specification.pac_step.pac_src1 st)
≤ ⇓ Id
(check_del_l spec' B
(EPAC_Checker_Specification.pac_step.pac_src1 st'))›
by (auto simp: check_del_l_def)
have HID: ‹f = f' ⟹ f ≤ ⇓Id f'› for f f'
by auto
show ?thesis
unfolding PAC_checker_l_step_s_def PAC_checker_l_step_prep_def pac_step.case_eq_if
prod.simps
apply (refine_rcg check_linear_combi_l_s_check_linear_combi_l
check_extension_l2_s_check_extension_l2 add_poly_l_s_add_poly_l)
subgoal using assms by auto
subgoal using assms by auto
apply (rule HID)
subgoal using assms by auto
subgoal using assms by auto
subgoal using assms by auto
subgoal by auto
subgoal using assms by auto
subgoal using assms by auto
subgoal using assms by auto
subgoal by auto
subgoal using assms by (auto simp: is_cfailed_merge_cstatus intro!: fmap_rel_fmupd_fmap_rel)
subgoal by auto
subgoal using assms by auto
apply (rule HID)
subgoal using assms by auto
subgoal using assms by auto
subgoal using assms by auto
subgoal using assms by auto
subgoal using assms by auto
subgoal using assms by auto
subgoal using assms by auto
subgoal using assms by auto
subgoal by auto
subgoal by auto
subgoal using assms by (auto intro!: fmap_rel_fmupd_fmap_rel intro: fmap_rel_mono2)
subgoal by auto
subgoal by auto
subgoal using assms by (auto intro!: fmap_rel_fmdrop_fmap_rel)
subgoal by auto
done
qed
lemma PAC_checker_l_step_s_PAC_checker_l_step_s2:
assumes
‹(st,st')∈Id›
‹(spec, spec') ∈ perfectly_shared_polynom (fst (snd err𝒱A))› and
‹((err𝒱A), (err'𝒟𝒱B)) ∈ Id ×⇩r perfectly_shared_vars_rel ×⇩r ⟨nat_rel, perfectly_shared_polynom (fst (snd err𝒱A))⟩fmap_rel›
shows ‹PAC_checker_l_step_s spec (err𝒱A) st
≤ ⇓{((err, 𝒱', A'), (err', 𝒟𝒱', B')).
(err, err') ∈ Id ∧
(¬is_cfailed err ⟶ ((𝒱', 𝒟𝒱') ∈ perfectly_shared_vars_rel ∧(A',B') ∈ ⟨nat_rel, perfectly_shared_polynom 𝒱'⟩fmap_rel ∧
perfectly_shared_polynom (fst (snd err𝒱A)) ⊆ perfectly_shared_polynom 𝒱'))}
(PAC_checker_l_step_prep spec' (err'𝒟𝒱B) st')›
using PAC_checker_l_step_s_PAC_checker_l_step_s[of ‹fst (snd err𝒱A)› ‹fst (snd err'𝒟𝒱B)›
‹snd (snd err𝒱A)› ‹snd (snd err'𝒟𝒱B)› spec spec' ‹fst (err𝒱A)› ‹fst (err'𝒟𝒱B)› st st' ] assms
by (cases err𝒱A; cases err'𝒟𝒱B)
auto
definition fully_normalize_and_import where
‹fully_normalize_and_import 𝒱 p = do {
p ← sort_all_coeffs p;
(err, p, 𝒱) ← import_polyS 𝒱 p;
if alloc_failed err
then RETURN (err, p, 𝒱)
else do {
p ← normalize_poly_s 𝒱 p;
RETURN (err, p, 𝒱)
}}›
fun vars_llist_l where
‹vars_llist_l [] = []› |
‹vars_llist_l (x#xs) = fst x @ vars_llist_l xs›
lemma set_vars_llist_l[simp]: ‹set(vars_llist_l xs) = vars_llist xs›
by (induction xs)
(auto)
lemma vars_llist_l_append[simp]: ‹vars_llist_l (a @ b) = vars_llist_l a @ vars_llist_l b›
by (induction a) auto
definition (in -) remap_polys_s_with_err :: ‹llist_polynomial ⇒ llist_polynomial ⇒ (nat, string) shared_vars ⇒ (nat, llist_polynomial) fmap ⇒
(string code_status × (nat, string) shared_vars × (nat, sllist_polynomial) fmap × sllist_polynomial) nres› where
‹remap_polys_s_with_err spec spec0 = (λ(𝒱:: (nat, string) shared_vars) A. do{
ASSERT(vars_llist spec ⊆ vars_llist spec0);
dom ← SPEC(λdom. set_mset (dom_m A) ⊆ dom ∧ finite dom);
(mem, 𝒱) ← import_variablesS (vars_llist_l spec0) 𝒱;
(mem', spec, 𝒱) ← if ¬alloc_failed mem then import_polyS 𝒱 spec else RETURN (mem, [], 𝒱);
failed ← SPEC(λb::bool. alloc_failed mem ∨ alloc_failed mem' ⟶ b);
if failed
then do {
c ← remap_polys_l_dom_err;
RETURN (error_msg (0 :: nat) c, 𝒱, fmempty, [])
}
else do {
(err, 𝒱, A) ← FOREACH⇩C dom (λ(err, 𝒱, A'). ¬is_cfailed err)
(λi (err, 𝒱, A').
if i ∈# dom_m A
then do {
(err', p, 𝒱) ← import_polyS 𝒱 (the (fmlookup A i));
if alloc_failed err' then RETURN((CFAILED ''memory out'', 𝒱, A'))
else do {
p ← full_normalize_poly_s 𝒱 p;
eq ← weak_equality_l_s' 𝒱 p spec;
let 𝒱 = 𝒱;
RETURN((if eq then CFOUND else CSUCCESS), 𝒱, fmupd i p A')
}
} else RETURN (err, 𝒱, A'))
(CSUCCESS, 𝒱, fmempty);
RETURN (err, 𝒱, A, spec)
}})›
lemma full_normalize_poly_alt_def:
‹full_normalize_poly p0 = do {
p ← sort_all_coeffs p0;
ASSERT(vars_llist p ⊆ vars_llist p0);
p ← sort_poly_spec p;
ASSERT(vars_llist p ⊆ vars_llist p0);
RETURN (merge_coeffs0 p)
}› (is ‹?A = ?B›)
proof -
have sort_poly_spec1: ‹(p,p')∈ Id ⟹ sort_poly_spec p ≤ ⇓ Id (sort_poly_spec p')› for p p'
by auto
have sort_all_coeffs2: ‹sort_all_coeffs xs ≤⇓{(ys,ys'). (ys,ys') ∈ Id ∧ vars_llist ys ⊆ vars_llist xs} (sort_all_coeffs xs)› for xs
proof -
term xs
have [refine]: ‹(xs, xs) ∈ ⟨{(ys,ys'). (ys,ys') ∈ Id ∧ ys ∈ set xs}⟩list_rel›
by (rule list_rel_mono_strong[of _ Id])
(auto)
have [refine]: ‹(x1a,x1)∈ Id ⟹ sort_coeff x1a ≤ ⇓ {(ys,ys'). (ys,ys') ∈ Id ∧ set ys ⊆ set x1a} (sort_coeff x1)› for x1a x1
unfolding sort_coeff_def
by (auto intro!: RES_refine dest: mset_eq_setD)
show ?thesis
unfolding sort_all_coeffs_def
apply refine_vcg
subgoal by auto
subgoal by auto
subgoal by (auto dest!: split_list)
done
qed
have sort_poly_spec1: ‹(p,p')∈ Id ⟹ sort_poly_spec p ≤ ⇓ Id (sort_poly_spec p')› for p p'
by auto
have sort_poly_spec2: ‹(p,p')∈Id ⟹ sort_poly_spec p ≤ ⇓ {(ys,ys'). (ys,ys') ∈ Id ∧ vars_llist ys ⊆ vars_llist p} (sort_poly_spec p')›
for p p'
by (auto simp: sort_poly_spec_def intro!: RES_refine dest: vars_llist_mset_eq)
have ‹?A ≤ ⇓Id ?B›
unfolding full_normalize_poly_def
by (refine_rcg sort_poly_spec1) auto
moreover have ‹?B ≤ ⇓Id ?A›
unfolding full_normalize_poly_def
apply (rule bind_refine[OF sort_all_coeffs2])
apply (refine_vcg sort_poly_spec2)
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
done
ultimately show ?thesis
by auto
qed
definition full_normalize_poly' :: ‹_› where
‹full_normalize_poly' _ = full_normalize_poly›
lemma full_normalize_poly_s_full_normalize_poly:
fixes xs :: ‹sllist_polynomial› and
𝒱 :: ‹(nat,string)shared_vars›
assumes
‹(xs, xs') ∈ perfectly_shared_polynom 𝒱› and
𝒱: ‹(𝒱, 𝒟𝒱) ∈ perfectly_shared_vars_rel› and
‹vars_llist xs' ⊆ set_mset 𝒟𝒱›
shows ‹full_normalize_poly_s 𝒱 xs ≤ ⇓(perfectly_shared_polynom 𝒱) (full_normalize_poly' 𝒟𝒱 xs')›
proof -
show ?thesis
unfolding full_normalize_poly_s_def full_normalize_poly_alt_def full_normalize_poly'_def
apply (refine_rcg sort_all_coeffs_s_sort_all_coeffs assms
sort_poly_spec_s_sort_poly_spec merge_coeffs0_s_merge_coeffs0)
subgoal using assms by auto
done
qed
lemma remap_polys_l2_with_err_prep_alt_def:
‹remap_polys_l2_with_err_prep spec spec0 = (λ(𝒱:: (nat, string) vars) A. do{
ASSERT(vars_llist spec ⊆ vars_llist spec0);
dom ← SPEC(λdom. set_mset (dom_m A) ⊆ dom ∧ finite dom);
(mem, 𝒱) ← SPEC(λ(mem, 𝒱'). ¬alloc_failed mem ⟶ set_mset 𝒱' = set_mset 𝒱 ∪ vars_llist spec0);
(mem', spec, 𝒱) ← if ¬alloc_failed mem then import_poly 𝒱 spec else SPEC(λ_. True);
failed ← SPEC(λb::bool. alloc_failed mem ∨ alloc_failed mem' ⟶ b);
if failed
then do {
c ← remap_polys_l_dom_err;
SPEC (λ(mem, _, _, _). mem = error_msg (0::nat) c)
}
else do {
(err, 𝒱, A) ← FOREACH⇩C dom (λ(err, 𝒱, A'). ¬is_cfailed err)
(λi (err, 𝒱, A').
if i ∈# dom_m A
then do {
(err', p, 𝒱) ← import_poly 𝒱 (the (fmlookup A i));
if alloc_failed err' then RETURN((CFAILED ''memory out'', 𝒱, A'))
else do {
ASSERT(vars_llist p ⊆ set_mset 𝒱);
p ← full_normalize_poly' 𝒱 p;
eq ← weak_equality_l' 𝒱 p spec;
let 𝒱 = 𝒱;
RETURN((if eq then CFOUND else CSUCCESS), 𝒱, fmupd i p A')
}
} else RETURN (err, 𝒱, A'))
(CSUCCESS, 𝒱, fmempty);
RETURN (err, 𝒱, A, spec)
}})›
unfolding full_normalize_poly'_def weak_equality_l'_def
by(auto simp: remap_polys_l2_with_err_prep_def
intro!: ext bind_cong[OF refl])
lemma remap_polys_s_with_err_remap_polys_l2_with_err_prep:
fixes 𝒱 :: ‹(nat, string) shared_vars›
assumes
𝒱: ‹(𝒱, 𝒟𝒱) ∈ perfectly_shared_vars_rel› and
AB: ‹(A,B) ∈ ⟨nat_rel, Id⟩fmap_rel› and
‹(spec, spec') ∈ ⟨⟨Id⟩list_rel ×⇩r int_rel⟩list_rel› and
spec0: ‹(spec0, spec0') ∈ ⟨⟨Id⟩list_rel ×⇩r int_rel⟩list_rel›
shows
‹remap_polys_s_with_err spec spec0 𝒱 A ≤
⇓{((err, 𝒱, A, fspec), (err', 𝒱', A', fspec')).
(err, err') ∈ Id ∧
( ¬is_cfailed err ⟶ (fspec, fspec') ∈ perfectly_shared_polynom 𝒱 ∧
((err, 𝒱, A), (err', 𝒱', A')) ∈ Id ×⇩r perfectly_shared_vars_rel ×⇩r⟨nat_rel, perfectly_shared_polynom 𝒱⟩fmap_rel)}
(remap_polys_l2_with_err_prep spec' spec0' 𝒟𝒱 B)›
proof -
have vars_spec: ‹(vars_llist_l spec0, vars_llist_l spec0) ∈ Id›
by auto
have [refine]: ‹import_variablesS (vars_llist_l spec0) 𝒱
≤ ⇓ {((mem, 𝒱𝒱), (mem', 𝒱𝒱')). mem=mem' ∧ (¬alloc_failed mem ⟶ (𝒱𝒱, 𝒱𝒱') ∈ perfectly_shared_vars_rel ∧
perfectly_shared_polynom 𝒱 ⊆ perfectly_shared_polynom 𝒱𝒱)}
(SPEC (λ(mem, 𝒱'). ¬alloc_failed mem ⟶ set_mset 𝒱' = set_mset 𝒟𝒱 ∪ vars_llist spec0'))›
apply (rule import_variablesS_import_variables[OF 𝒱 vars_spec, THEN order_trans])
apply (rule ref_two_step'[THEN order_trans])
apply (rule import_variables_spec)
apply (use spec0 in ‹auto simp: conc_fun_RES
dest!: spec[of _ ‹𝒟𝒱 + mset (vars_llist_l spec0)›]›)
by (meson perfectly_shared_var_rel_perfectly_shared_polynom_mono subset_eq)
have 1: ‹inj_on id (dom :: nat set)› for dom
by (auto simp: inj_on_def)
have [refine]: ‹(x2e, x2c) ∈ perfectly_shared_vars_rel ⟹
((CSUCCESS, x2e, fmempty), CSUCCESS, x2c, fmempty)
∈ {((mem,𝒜, A), (mem',𝒜', A')). (mem,mem') ∈ Id ∧
(¬is_cfailed mem ⟶ ((𝒜, A), (𝒜', A'))∈ perfectly_shared_vars_rel ×⇩r⟨nat_rel, perfectly_shared_polynom 𝒜⟩fmap_rel ∧
perfectly_shared_polynom x2e ⊆ perfectly_shared_polynom 𝒜)}›
for x2e x2c
by auto
have [simp]: ‹A ∝ xb = B ∝ xb› for xb
using AB unfolding fmap_rel_alt_def apply auto by (metis in_dom_m_lookup_iff)
show ?thesis
unfolding remap_polys_s_with_err_def remap_polys_l2_with_err_prep_alt_def Let_def
apply (refine_rcg import_polyS_import_poly 1 full_normalize_poly_s_full_normalize_poly
weak_equality_l_s_weak_equality_l)
subgoal using assms by auto
subgoal using assms by auto
subgoal by auto
subgoal by auto
subgoal using assms by auto
subgoal by (auto intro!: RETURN_RES_refine)
subgoal by auto
subgoal by auto
subgoal by (clarsimp intro!: RETURN_RES_refine)
subgoal by auto
subgoal by auto
subgoal by auto
subgoal using assms by auto
subgoal using assms by auto
subgoal by auto
subgoal using assms by auto
subgoal using assms by auto
subgoal using assms by auto
subgoal by auto
subgoal by simp
subgoal by auto
subgoal
by (auto intro!: fmap_rel_fmupd_fmap_rel
intro: fmap_rel_mono2)
subgoal by auto
subgoal
by (auto intro!: fmap_rel_fmupd_fmap_rel
intro: fmap_rel_mono2)
done
qed
definition PAC_checker_l_s where
‹PAC_checker_l_s spec A b st = do {
(S, _) ← WHILE⇩T
(λ((b, A), n). ¬is_cfailed b ∧ n ≠ [])
(λ((bA), n). do {
ASSERT(n ≠ []);
S ← PAC_checker_l_step_s spec bA (hd n);
RETURN (S, tl n)
})
((b, A), st);
RETURN S
}›
lemma PAC_checker_l_s_PAC_checker_l_prep_s:
assumes
‹(𝒱, 𝒟𝒱) ∈ perfectly_shared_vars_rel›
‹(A,B) ∈ ⟨nat_rel, perfectly_shared_polynom 𝒱⟩fmap_rel› and
‹(spec, spec') ∈ perfectly_shared_polynom 𝒱› and
‹(err, err') ∈ Id› and
‹(st,st')∈Id›
shows ‹PAC_checker_l_s spec (𝒱, A) err st
≤ ⇓{((err, 𝒱', A'), (err', 𝒟𝒱', B')).
(err, err') ∈ Id ∧
(¬is_cfailed err ⟶ ((𝒱', 𝒟𝒱') ∈ perfectly_shared_vars_rel ∧(A',B') ∈ ⟨nat_rel, perfectly_shared_polynom 𝒱'⟩fmap_rel))}
(PAC_checker_l2 spec' (𝒟𝒱, B) err' st')›
proof -
show ?thesis
unfolding PAC_checker_l_s_def PAC_checker_l2_def
apply (refine_rcg PAC_checker_l_step_s_PAC_checker_l_step_s2
WHILET_refine[where R = ‹{((err, 𝒱', A'), err', 𝒟𝒱', B').
(err, err') ∈ Id ∧ (¬ is_cfailed err ⟶
(𝒱', 𝒟𝒱') ∈ perfectly_shared_vars_rel ∧
(A', B') ∈ ⟨nat_rel, perfectly_shared_polynom 𝒱'⟩fmap_rel ∧
perfectly_shared_polynom 𝒱 ⊆ perfectly_shared_polynom 𝒱')}×⇩rId›])
subgoal using assms by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal using assms by auto
subgoal by auto
subgoal by force
subgoal by auto
done
qed
definition full_checker_l_s
:: ‹llist_polynomial ⇒ (nat, llist_polynomial) fmap ⇒ (_, string, nat) pac_step list ⇒
(string code_status × _) nres›
where
‹full_checker_l_s spec A st = do {
spec' ← full_normalize_poly spec;
(b, 𝒱, A, spec') ← remap_polys_s_with_err spec' spec ({#}, fmempty, fmempty) A;
if is_cfailed b
then RETURN (b, 𝒱, A)
else do {
PAC_checker_l_s spec' (𝒱, A) b st
}
}›
lemma full_checker_l_s_full_checker_l_prep:
assumes
‹(A,B) ∈ ⟨nat_rel, Id⟩fmap_rel› and
‹(spec, spec') ∈ ⟨⟨Id⟩list_rel ×⇩r int_rel⟩list_rel› and
‹(st,st')∈Id›
shows ‹full_checker_l_s spec A st
≤ ⇓{((err, _), (err', _)). (err, err') ∈ Id}
(full_checker_l_prep spec' B st')›
proof -
have [refine]: ‹full_normalize_poly spec ≤ ⇓ (⟨⟨Id⟩list_rel ×⇩r int_rel⟩list_rel) (full_normalize_poly spec')›
using assms by auto
have [refine]: ‹(({#}, fmempty, fmempty), {#}) ∈ perfectly_shared_vars_rel›
by (auto simp: perfectly_shared_vars_rel_def perfectly_shared_vars_def)
have H: ‹(x1d, x1a) ∈ perfectly_shared_vars_rel›
‹(x1e, x1b) ∈ ⟨nat_rel, perfectly_shared_polynom x1d⟩fmap_rel›
‹(x2e, x2b) ∈ perfectly_shared_polynom x1d›
‹(x1c, x1) ∈ Id›
if ‹(x, x')
∈ {((err, 𝒱, A, fspec), err', 𝒱', A', fspec').
(err, err') ∈ Id ∧
(¬ is_cfailed err ⟶
(fspec, fspec') ∈ perfectly_shared_polynom 𝒱 ∧
((err, 𝒱, A), err', 𝒱', A')
∈ Id ×⇩r perfectly_shared_vars_rel ×⇩r ⟨nat_rel, perfectly_shared_polynom 𝒱⟩fmap_rel)}›
‹x2a = (x1b, x2b)›
‹x2 = (x1a, x2a)›
‹x' = (x1, x2)›
‹x2d = (x1e, x2e)›
‹x2c = (x1d, x2d)›
‹x = (x1c, x2c)›
‹¬ is_cfailed x1c›
for spec' spec'a x x' x1 x2 x1a x2a x1b x2b x1c x2c x1d x2d x1e x2e
using that by auto
term PAC_checker_l2
thm PAC_checker_l_s_PAC_checker_l_prep_s
show ?thesis
unfolding full_checker_l_s_def full_checker_l_prep_def
apply (refine_rcg PAC_checker_l_s_PAC_checker_l_prep_s[THEN order_trans]
remap_polys_s_with_err_remap_polys_l2_with_err_prep assms)
subgoal by (auto simp: perfectly_shared_vars_rel_def perfectly_shared_vars_def)
subgoal using assms by auto
apply (rule H(1); assumption)
apply (rule H(2); assumption)
apply (rule H(3); assumption)
apply (rule H(4); assumption)
subgoal by (auto intro!: conc_fun_R_mono)
done
qed
lemma full_checker_l_s_full_checker_l_prep':
‹(uncurry2 full_checker_l_s, uncurry2 full_checker_l_prep)∈
(⟨⟨Id⟩list_rel ×⇩r int_rel⟩list_rel ×⇩r ⟨nat_rel, Id⟩fmap_rel) ×⇩r Id →⇩f
⟨{((err, _), (err', _)). (err, err') ∈ Id}⟩nres_rel›
by (auto intro!: frefI nres_relI full_checker_l_s_full_checker_l_prep[THEN order_trans])
definition merge_coeff_s :: ‹(nat,string)shared_vars ⇒ nat list ⇒ nat list ⇒ nat list ⇒ nat list nres› where
‹merge_coeff_s 𝒱 xs = mergeR (λa b. a ∈ set xs ∧ b ∈ set xs)
(λa b. do {
x ← get_var_nameS 𝒱 a;
y ← get_var_nameS 𝒱 b;
RETURN(a = b ∨ var_order x y)
})›
term get_var_nameS
sepref_definition merge_coeff_s_impl
is ‹uncurry3 merge_coeff_s›
:: ‹shared_vars_assn⇧k *⇩a (monom_s_assn)⇧k *⇩a (monom_s_assn)⇧k *⇩a (monom_s_assn)⇧k →⇩a monom_s_assn›
supply [[goals_limit=1]]
unfolding merge_coeff_s_def mergeR_alt_def var_order'_def[symmetric]
by sepref
sepref_register merge_coeff_s msort_coeff_s sort_all_coeffs_s
lemmas [sepref_fr_rules] = merge_coeff_s_impl.refine
lemma msort_coeff_s_alt_def:
‹msort_coeff_s 𝒱 xs = do {
let zs = COPY xs;
REC⇩T
(λmsortR' xsa. if length xsa ≤ 1 then RETURN (ASSN_ANNOT monom_s_assn xsa) else do {
let xs1 = ASSN_ANNOT monom_s_assn (take (length xsa div 2) xsa);
let xs2 = ASSN_ANNOT monom_s_assn (drop (length xsa div 2) xsa);
as ← msortR' xs1;
let as = ASSN_ANNOT monom_s_assn as;
bs ← msortR' xs2;
let bs = ASSN_ANNOT monom_s_assn bs;
merge_coeff_s 𝒱 zs as bs
})
xs}›
unfolding msort_coeff_s_def merge_coeff_s_def[symmetric]
msortR_alt_def ASSN_ANNOT_def Let_def COPY_def
by auto
sepref_definition msort_coeff_s_impl
is ‹uncurry msort_coeff_s›
:: ‹shared_vars_assn⇧k *⇩a (monom_s_assn)⇧k →⇩a monom_s_assn›
supply [[goals_limit=1]]
unfolding msort_coeff_s_alt_def
unfolding var_order'_def[symmetric]
by sepref
lemmas [sepref_fr_rules] = msort_coeff_s_impl.refine
sepref_definition sort_all_coeffs_s'_impl
is ‹uncurry sort_all_coeffs_s›
:: ‹shared_vars_assn⇧k *⇩a poly_s_assn⇧d →⇩a poly_s_assn›
unfolding sort_all_coeffs_s_def HOL_list.fold_custom_empty
by sepref
lemmas [sepref_fr_rules] = sort_all_coeffs_s'_impl.refine
lemma merge_coeffs0_s_alt_def:
‹(RETURN o merge_coeffs0_s) p =
REC⇩T(λf p.
(case p of
[] ⇒ RETURN []
| [p] => if snd (COPY p)= 0 then RETURN [] else RETURN [p]
| (a # b # p) ⇒
(let (xs, n) = COPY a; (ys, m) = COPY b in
if xs = ys
then if n + m ≠ 0 then f ((xs, n + m) # (COPY p)) else f p
else if n = 0 then
do {p ← f (b # (COPY p));
RETURN p}
else do {p ← f (b # (COPY p));
RETURN (a # p)})))
p›
unfolding COPY_def Let_def
apply (subst eq_commute)
apply (induction p rule: merge_coeffs0_s.induct)
subgoal by (subst RECT_unfold, refine_mono) auto
subgoal by (subst RECT_unfold, refine_mono) auto
subgoal by (subst RECT_unfold, refine_mono) (auto simp: let_to_bind_conv)
done
lemma [sepref_import_param]: ‹(((=)), ((=))) ∈ ⟨uint64_nat_rel⟩ list_rel → ⟨uint64_nat_rel⟩ list_rel → bool_rel›
proof -
have ‹IS_LEFT_UNIQUE (⟨uint64_nat_rel⟩ list_rel)›
by (intro safe_constraint_rules)
moreover have ‹IS_RIGHT_UNIQUE (⟨uint64_nat_rel⟩ list_rel)›
by (intro safe_constraint_rules)
ultimately show ?thesis
by (sep_auto simp: IS_LEFT_UNIQUE_def single_valued_def
simp flip: inv_list_rel_eq)
qed
lemma is_pure_monom_s_assn: ‹is_pure monom_s_assn›
‹is_pure (monom_s_assn ×⇩a int_assn)›
by (auto simp add: list_assn_pure_conv)
sepref_definition merge_coeffs0_s_impl
is ‹RETURN o merge_coeffs0_s›
:: ‹poly_s_assn⇧k →⇩a poly_s_assn›
unfolding merge_coeffs0_s_alt_def HOL_list.fold_custom_empty
by sepref
lemmas [sepref_fr_rules] = merge_coeffs0_s_impl.refine
sepref_definition full_normalize_poly'_impl
is ‹uncurry full_normalize_poly_s›
:: ‹shared_vars_assn⇧k *⇩a poly_s_assn⇧k →⇩a poly_s_assn›
unfolding full_normalize_poly_s_def
by sepref
lemma weak_equality_l_s_alt_def:
‹weak_equality_l_s = RETURN oo (λp q. p = q)›
unfolding weak_equality_l_s_def weak_equality_l_s_def by (auto intro!: ext)
lemma [sepref_import_param]
: ‹(((=)), ((=))) ∈ ⟨⟨uint64_nat_rel⟩ list_rel ×⇩r int_rel⟩ list_rel → ⟨⟨uint64_nat_rel⟩ list_rel ×⇩r int_rel⟩ list_rel → bool_rel›
proof -
let ?A = ‹⟨⟨uint64_nat_rel⟩ list_rel ×⇩r int_rel⟩ list_rel›
have ‹IS_LEFT_UNIQUE (⟨uint64_nat_rel⟩ list_rel)›
by (intro safe_constraint_rules)
then have ‹IS_LEFT_UNIQUE (?A)›
by (intro safe_constraint_rules)
moreover have ‹IS_RIGHT_UNIQUE (⟨uint64_nat_rel⟩ list_rel)›
by (intro safe_constraint_rules)
then have ‹IS_RIGHT_UNIQUE (?A)›
by (intro safe_constraint_rules)
ultimately show ?thesis
by (sep_auto simp: IS_LEFT_UNIQUE_def single_valued_def
simp flip: inv_list_rel_eq)
qed
sepref_definition weak_equality_l_s_impl
is ‹uncurry weak_equality_l_s›
:: ‹poly_s_assn⇧k *⇩a poly_s_assn⇧k →⇩a bool_assn›
unfolding weak_equality_l_s_alt_def
by sepref
code_printing constant arl_get_u' ⇀ (SML) "(fn/ ()/ =>/ Array.sub/ ((fn/ (a,b)/ =>/ a) ((_)),/ Word32.toInt ((_))))"
abbreviation polys_s_assn where
‹polys_s_assn ≡ hm_fmap_assn uint64_nat_assn poly_s_assn›
sepref_definition import_monom_no_newS_impl
is ‹uncurry (import_monom_no_newS :: (nat,string)shared_vars ⇒ _ ⇒( bool × _) nres)›
:: ‹shared_vars_assn⇧k *⇩a (list_assn string_assn)⇧k →⇩a bool_assn ×⇩a list_assn uint64_nat_assn›
unfolding import_monom_no_newS_def HOL_list.fold_custom_empty
by sepref
sepref_register import_monom_no_newS import_poly_no_newS check_linear_combi_l_pre_err
lemmas [sepref_fr_rules] =
import_monom_no_newS_impl.refine weak_equality_l_s_impl.refine
sepref_definition import_poly_no_newS_impl
is ‹uncurry (import_poly_no_newS :: (nat,string)shared_vars ⇒ llist_polynomial ⇒( bool × sllist_polynomial) nres)›
:: ‹shared_vars_assn⇧k *⇩a poly_assn⇧k →⇩a bool_assn ×⇩a poly_s_assn›
unfolding import_poly_no_newS_def HOL_list.fold_custom_empty
by sepref
lemmas [sepref_fr_rules] =
import_poly_no_newS_impl.refine
definition check_linear_combi_l_pre_err_impl where
‹check_linear_combi_l_pre_err_impl i pd p mem =
(if pd then ''The polynomial with id '' @ show (nat_of_uint64 i) @ '' was not found'' else '''') @
(if p then ''The co-factor from '' @ show (nat_of_uint64 i) @ '' was empty'' else '''')@
(if mem then ''Memory out'' 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_linear_combi_l_pre_err_impl x y))),
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 check_linear_combi_l_pre_err_impl_def check_linear_combi_l_pre_err_def list_assn_pure_conv
apply sepref_to_hoare
apply sep_auto
done
lemma vars_llist_in_s_single: ‹RETURN (vars_llist_in_s 𝒱 [(xs, a)]) =
REC⇩T (λf xs. case xs of
[] ⇒ RETURN True
| x # xs ⇒ do {
b ← is_new_variableS x 𝒱;
if b then RETURN False
else f xs
}) (xs)›
apply (subst eq_commute)
apply (cases 𝒱)
apply (induction xs)
subgoal
by (subst RECT_unfold, refine_mono)
(auto simp: vars_llist_in_s_def)
subgoal
by (subst RECT_unfold, refine_mono)
(auto simp: vars_llist_in_s_def is_new_variableS_def)
done
lemma vars_llist_in_s_alt_def: ‹(RETURN oo vars_llist_in_s) 𝒱 xs =
REC⇩T (λf xs. case xs of
[] ⇒ RETURN True
| (x, a) # xs ⇒ do {
b ← RETURN (vars_llist_in_s 𝒱 [(x, a)]);
if ¬b then RETURN False
else f xs
}) xs›
apply (subst eq_commute)
apply (cases 𝒱)
apply (induction xs)
subgoal
by (subst RECT_unfold, refine_mono)
(auto simp: vars_llist_in_s_def)
subgoal
by (subst RECT_unfold, refine_mono)
(auto simp: vars_llist_in_s_def is_new_variableS_def split: prod.splits)
done
sepref_definition vars_llist_in_s_impl
is ‹uncurry (RETURN oo vars_llist_in_s)›
:: ‹shared_vars_assn⇧k *⇩a poly_assn⇧k →⇩a bool_assn›
unfolding vars_llist_in_s_alt_def
vars_llist_in_s_single
by sepref
lemmas [sepref_fr_rules] = vars_llist_in_s_impl.refine
definition check_linear_combi_l_s_dom_err_impl :: ‹_ ⇒ uint64 ⇒ _› where
‹check_linear_combi_l_s_dom_err_impl x p =
''Poly not found in CL from x '' @ show (nat_of_uint64 p)›
lemma [sepref_fr_rules]:
‹(uncurry (return oo (check_linear_combi_l_s_dom_err_impl)),
uncurry (check_linear_combi_l_s_dom_err)) ∈ poly_s_assn⇧k *⇩a uint64_nat_assn⇧k →⇩a raw_string_assn›
unfolding check_linear_combi_l_s_dom_err_def check_linear_combi_l_s_dom_err_impl_def list_assn_pure_conv
apply sepref_to_hoare
apply sep_auto
done
sepref_register check_linear_combi_l_s_dom_err_impl mult_poly_s normalize_poly_s
sepref_definition normalize_poly_sharedS_impl
is ‹uncurry normalize_poly_sharedS›
:: ‹ shared_vars_assn⇧k *⇩a poly_assn⇧k →⇩a bool_assn ×⇩a poly_s_assn›
unfolding normalize_poly_sharedS_def
by sepref
lemmas [sepref_fr_rules] = normalize_poly_sharedS_impl.refine
mult_poly_s_impl.refine
lemma merge_coeffs_s_alt_def:
‹(RETURN o merge_coeffs_s) p =
REC⇩T(λf p.
(case p of
[] ⇒ RETURN []
| [_] => RETURN p
| ((xs, n) # (ys, m) # p) ⇒
(if xs = ys
then if n + m ≠ 0 then f ((xs, n + m) # COPY p) else f p
else do {p ← f ((ys, m) # p); RETURN ((xs, n) # p)})))
p›
apply (subst eq_commute)
apply (induction p rule: merge_coeffs_s.induct)
subgoal by (subst RECT_unfold, refine_mono) auto
subgoal by (subst RECT_unfold, refine_mono) auto
subgoal for x p y q
by (subst RECT_unfold, refine_mono) auto
done
sepref_definition merge_coeffs_s_impl
is ‹(RETURN o merge_coeffs_s)›
:: ‹poly_s_assn⇧k →⇩a poly_s_assn›
unfolding merge_coeffs_s_alt_def
HOL_list.fold_custom_empty
by sepref
lemmas [sepref_fr_rules] = merge_coeffs_s_impl.refine
sepref_definition normalize_poly_s_impl
is ‹uncurry normalize_poly_s›
:: ‹shared_vars_assn⇧k *⇩a poly_s_assn⇧k →⇩a poly_s_assn›
unfolding normalize_poly_s_def
by sepref
lemmas [sepref_fr_rules] = normalize_poly_s_impl.refine
sepref_definition mult_poly_full_s_impl
is ‹uncurry2 mult_poly_full_s›
:: ‹shared_vars_assn⇧k *⇩a poly_s_assn⇧k*⇩a poly_s_assn⇧k →⇩a poly_s_assn›
unfolding mult_poly_full_s_def
by sepref
lemmas [sepref_fr_rules] = mult_poly_full_s_impl.refine
add_poly_l_prep_impl.refine
sepref_register add_poly_l_s
sepref_definition linear_combi_l_prep_s_impl
is ‹uncurry3 linear_combi_l_prep_s›
:: ‹uint64_nat_assn⇧k *⇩a polys_s_assn⇧k *⇩a shared_vars_assn⇧k *⇩a
(list_assn (poly_assn ×⇩a uint64_nat_assn))⇧d →⇩a poly_s_assn ×⇩a (list_assn (poly_assn ×⇩a uint64_nat_assn)) ×⇩a status_assn raw_string_assn
›
supply [[goals_limit=1]]
unfolding linear_combi_l_prep_s_def
in_dom_m_lookup_iff
fmlookup'_def[symmetric] conv_to_is_Nil
unfolding is_Nil_def
HOL_list.fold_custom_empty
apply (rewrite in ‹op_HOL_list_empty› annotate_assn[where A=‹poly_s_assn›])
by sepref
lemmas [sepref_fr_rules] = linear_combi_l_prep_s_impl.refine
definition check_linear_combi_l_s_mult_err_impl :: ‹_ ⇒ _ ⇒ _› where
‹check_linear_combi_l_s_mult_err_impl x p =
''Unequal polynom found in CL '' @ show (map (λ(a,b). (map nat_of_uint64 a, b)) p) @
'' but '' @ show (map (λ(a,b). (map nat_of_uint64 a, b)) x)›
lemma [sepref_fr_rules]:
‹(uncurry (return oo (check_linear_combi_l_s_mult_err_impl)),
uncurry (check_linear_combi_l_s_mult_err)) ∈ poly_s_assn⇧k *⇩a poly_s_assn⇧k →⇩a raw_string_assn›
unfolding check_linear_combi_l_s_mult_err_impl_def check_linear_combi_l_s_mult_err_def list_assn_pure_conv
apply sepref_to_hoare
apply sep_auto
done
sepref_definition check_linear_combi_l_s_impl
is ‹uncurry5 check_linear_combi_l_s›
:: ‹poly_s_assn⇧k *⇩a polys_s_assn⇧k *⇩a shared_vars_assn⇧k *⇩a uint64_nat_assn⇧k *⇩a
(list_assn (poly_assn ×⇩a uint64_nat_assn))⇧d *⇩a poly_assn⇧k →⇩a status_assn raw_string_assn ×⇩a poly_s_assn
›
unfolding check_linear_combi_l_s_def
in_dom_m_lookup_iff
fmlookup'_def[symmetric]
by sepref
sepref_register fmlookup'
lemma check_extension_l2_s_alt_def:
‹check_extension_l2_s spec A 𝒱 i v p = do {
n ← is_new_variableS v 𝒱;
let t = fmlookup' i A;
pre ← RETURN (t = None);
let pre = pre ∧ n;
let nonew = vars_llist_in_s 𝒱 p;
(mem, p, 𝒱) ← import_polyS 𝒱 p;
let pre = (pre ∧ ¬alloc_failed mem);
if ¬pre
then do {
c ← check_extension_l_dom_err i;
RETURN (error_msg i c, [], 𝒱, 0)
} else do {
if ¬nonew
then do {
c ← check_extension_l_s_new_var_multiple_err v p;
RETURN (error_msg i c, [], 𝒱, 0)
}
else do {
(mem', 𝒱, v') ← import_variableS v 𝒱;
if alloc_failed mem'
then do {
c ← check_extension_l_dom_err i;
RETURN (error_msg i c, [], 𝒱, 0)
} else
do {
p2 ← mult_poly_full_s 𝒱 p p;
let p'' = map (λ(a,b). (a, -b)) p;
q ← add_poly_l_s 𝒱 (p2, p'');
eq ← weak_equality_l_s q [];
if eq then do {
RETURN (CSUCCESS, p, 𝒱, v')
} else do {
c ← check_extension_l_s_side_cond_err v p p'' q;
RETURN (error_msg i c, [], 𝒱, v')
}
}
}
}
}›
unfolding check_extension_l2_s_def fmlookup'_def[symmetric] Let_def
in_dom_m_lookup_iff
by (auto intro!: bind_cong[OF refl])
definition uminus_poly :: ‹_ ⇒ _› where
‹uminus_poly p' = map (λ(a, b). (a, - b)) p'›
lemma [sepref_import_param]: ‹(uminus_poly, uminus_poly) ∈ ⟨monom_s_rel ×⇩r int_rel⟩list_rel → ⟨monom_s_rel ×⇩r int_rel⟩list_rel›
proof -
have ‹(a, a') ∈ ⟨monom_s_rel ×⇩r int_rel⟩list_rel ⟹
(EPAC_Efficient_Checker_Synthesis.uminus_poly a,
EPAC_Efficient_Checker_Synthesis.uminus_poly a')
∈ ⟨monom_s_rel ×⇩r int_rel⟩list_rel› for a a'
apply (induction a arbitrary: a')
subgoal by (auto simp: uminus_poly_def)
subgoal for a as a'
by (cases a'; cases a)
(auto simp: uminus_poly_def)
done
then show ?thesis
by (auto intro!: frefI)
qed
sepref_register import_monomS import_polyS
sepref_definition import_monomS_impl
is ‹uncurry import_monomS›
:: ‹shared_vars_assn⇧d *⇩a monom_assn⇧k →⇩a memory_allocation_assn ×⇩a monom_s_assn ×⇩a shared_vars_assn›
supply [[goals_limit=1]]
unfolding import_monomS_def
HOL_list.fold_custom_empty
by sepref
lemmas [sepref_fr_rules] =
import_monomS_impl.refine
sepref_definition import_polyS_impl
is ‹uncurry import_polyS›
:: ‹shared_vars_assn⇧d *⇩a poly_assn⇧k →⇩a memory_allocation_assn ×⇩a poly_s_assn ×⇩a shared_vars_assn›
supply [[goals_limit=1]]
unfolding import_polyS_def
HOL_list.fold_custom_empty
by sepref
lemmas [sepref_fr_rules] =
import_polyS_impl.refine
definition check_extension_l_s_new_var_multiple_err_impl :: ‹String.literal ⇒ _ ⇒ _› where
‹check_extension_l_s_new_var_multiple_err_impl x p =
''Variable already defined '' @ show x @
'' but '' @ show (map (λ(a,b). (map nat_of_uint64 a, b)) p)›
lemma [sepref_fr_rules]:
‹(uncurry (return oo (check_extension_l_s_new_var_multiple_err_impl)),
uncurry (check_extension_l_s_new_var_multiple_err)) ∈ string_assn⇧k *⇩a poly_s_assn⇧k →⇩a raw_string_assn›
unfolding check_extension_l_s_new_var_multiple_err_impl_def check_extension_l_s_new_var_multiple_err_def list_assn_pure_conv
apply sepref_to_hoare
apply sep_auto
done
definition check_extension_l_s_side_cond_err_impl :: ‹String.literal ⇒ _ ⇒ _› where
‹check_extension_l_s_side_cond_err_impl x p p' q' =
''p^2- p != 0 '' @ show x @
'' but '' @ show (map (λ(a,b). (map nat_of_uint64 a, b)) p) @
'' and '' @ show (map (λ(a,b). (map nat_of_uint64 a, b)) p') @
'' and '' @ show (map (λ(a,b). (map nat_of_uint64 a, b)) q')›
abbreviation comp4 (infixl "oooo" 55) where "f oooo g ≡ λx. f ooo (g x)"
abbreviation comp5 (infixl "ooooo" 55) where "f ooooo g ≡ λx. f oooo (g x)"
lemma [sepref_fr_rules]:
‹(uncurry3 (return oooo (check_extension_l_s_side_cond_err_impl)),
uncurry3 (check_extension_l_s_side_cond_err)) ∈ string_assn⇧k *⇩a poly_s_assn⇧k*⇩a poly_s_assn⇧k*⇩a poly_s_assn⇧k →⇩a raw_string_assn›
unfolding check_extension_l_s_side_cond_err_impl_def check_extension_l_s_side_cond_err_def list_assn_pure_conv
apply sepref_to_hoare
apply sep_auto
done
sepref_register mult_poly_full_s weak_equality_l_s check_extension_l_s_side_cond_err check_extension_l2_s
check_linear_combi_l_s is_cfailed check_del_l
sepref_definition check_extension_l_impl
is ‹uncurry5 check_extension_l2_s›
:: ‹poly_s_assn⇧k *⇩a polys_s_assn⇧k *⇩a shared_vars_assn⇧d *⇩a uint64_nat_assn⇧k *⇩a
string_assn⇧k *⇩a poly_assn⇧k →⇩a status_assn raw_string_assn ×⇩a poly_s_assn ×⇩a shared_vars_assn ×⇩a uint64_nat_assn
›
supply [[goals_limit=1]]
unfolding check_extension_l2_s_alt_def
in_dom_m_lookup_iff
fmlookup'_def[symmetric]
not_not is_None_def
uminus_poly_def[symmetric]
HOL_list.fold_custom_empty
zero_uint64_nat_def[symmetric]
by sepref
lemma [sepref_fr_rules]:
‹(return o is_cfailed, RETURN o is_cfailed) ∈ (status_assn raw_string_assn)⇧k →⇩a bool_assn›
apply sepref_to_hoare
apply (sep_auto)
apply (case_tac x; case_tac xi; sep_auto)+
done
sepref_definition check_del_l_impl
is ‹uncurry2 check_del_l›
:: ‹poly_s_assn⇧k *⇩apolys_s_assn⇧k *⇩a uint64_nat_assn⇧k →⇩a status_assn raw_string_assn›
unfolding check_del_l_def
by sepref
lemmas [sepref_fr_rules] =
check_extension_l_impl.refine
check_linear_combi_l_s_impl.refine
check_del_l_impl.refine
sepref_definition PAC_checker_l_step_s_impl
is ‹uncurry2 PAC_checker_l_step_s›
:: ‹poly_s_assn⇧k *⇩a (status_assn raw_string_assn ×⇩a shared_vars_assn ×⇩a polys_s_assn)⇧d *⇩a
(pac_step_rel_assn (uint64_nat_assn) poly_assn string_assn)⇧k →⇩a status_assn raw_string_assn ×⇩a shared_vars_assn ×⇩a polys_s_assn
›
supply [[goals_limit = 1]]
supply [intro] = is_Mult_lastI
unfolding PAC_checker_l_step_s_def Let_def
pac_step.case_eq_if
HOL_list.fold_custom_empty
by sepref
lemmas [sepref_fr_rules] = PAC_checker_l_step_s_impl.refine
fun vars_llist_s2 :: ‹_ ⇒ _ list› where
‹vars_llist_s2 [] = []› |
‹vars_llist_s2 ((a,_) # xs) = a @ vars_llist_s2 xs›
lemma [sepref_import_param]:
‹(vars_llist_s2, vars_llist_s2) ∈ ⟨⟨string_rel⟩list_rel ×⇩r int_rel⟩list_rel → ⟨string_rel⟩list_rel›
apply (intro fun_relI)
subgoal for a b
apply (induction a arbitrary: b)
subgoal by auto
subgoal for a as b
by (cases a, cases b)
(force simp: list_rel_append1)+
done
done
sepref_register PAC_checker_l_step_s
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_s_impl
is ‹uncurry3 PAC_checker_l_s›
:: ‹poly_s_assn⇧k *⇩a (shared_vars_assn ×⇩a polys_s_assn)⇧d *⇩a(status_assn raw_string_assn)⇧d *⇩a
(list_assn (pac_step_rel_assn (uint64_nat_assn) poly_assn string_assn))⇧d →⇩a
status_assn raw_string_assn ×⇩a shared_vars_assn ×⇩a polys_s_assn
›
supply [[goals_limit = 1]]
supply [intro] = is_Mult_lastI
unfolding PAC_checker_l_s_def Let_def
pac_step.case_eq_if
neq_Nil_conv
conv_to_is_Nil is_Nil_def
by sepref
lemmas [sepref_fr_rules] = PAC_checker_l_s_impl.refine
definition memory_out_msg :: ‹string› where
‹memory_out_msg = ''memory out''›
lemma [sepref_fr_rules]: ‹(uncurry0 (return memory_out_msg), uncurry0 (RETURN memory_out_msg)) ∈ unit_assn⇧k →⇩a raw_string_assn›
unfolding memory_out_msg_def
by sepref_to_hoare sep_auto
definition (in -) remap_polys_l2_with_err_s :: ‹llist_polynomial ⇒ llist_polynomial ⇒ (nat, llist_polynomial) fmap ⇒ (nat, string) shared_vars ⇒
(string code_status × (nat, string) shared_vars × (nat, sllist_polynomial) fmap × sllist_polynomial) nres› where
‹remap_polys_l2_with_err_s spec spec0 A (𝒱 :: (nat, string) shared_vars) = do{
ASSERT(vars_llist spec ⊆ vars_llist spec0);
n ← upper_bound_on_dom A;
(mem, 𝒱) ← import_variablesS (vars_llist_s2 spec0) 𝒱;
(mem', spec, 𝒱) ← if ¬alloc_failed mem then import_polyS 𝒱 spec else RETURN (mem, [], 𝒱);
failed ← RETURN (alloc_failed mem ∨ alloc_failed mem' ∨ n ≥ 2^64);
if failed
then do {
c ← remap_polys_l_dom_err;
RETURN (error_msg (0::nat) c, 𝒱, fmempty, [])
}
else do {
(err, A, 𝒱) ← nfoldli ([0..<n]) (λ(err, A', 𝒱). ¬is_cfailed err)
(λi (err, A' :: (nat, sllist_polynomial) fmap, 𝒱 :: (nat,string) shared_vars).
if i ∈# dom_m A
then do {
(err', p, 𝒱 :: (nat,string) shared_vars) ← import_polyS (𝒱 :: (nat,string) shared_vars) (the (fmlookup A i));
if alloc_failed err' then RETURN((CFAILED ''memory out'', A', 𝒱 :: (nat,string) shared_vars))
else do {
p ← full_normalize_poly_s 𝒱 p;
eq ← weak_equality_l_s p spec;
RETURN((if eq then CFOUND else CSUCCESS), fmupd i p A', 𝒱 :: (nat,string) shared_vars)
}
} else RETURN (err, A', 𝒱 :: (nat,string) shared_vars))
(CSUCCESS, fmempty :: (nat, sllist_polynomial) fmap, 𝒱 :: (nat,string) shared_vars);
RETURN (err, 𝒱, A, spec)
}}›
lemma set_vars_llist_s2 [simp]: ‹set (vars_llist_s2 b) = vars_llist b›
by (induction b)
(auto simp: vars_llist_def)
sepref_register upper_bound_on_dom import_variablesS vars_llist_s2 memory_out_msg
sepref_definition import_variablesS_impl
is ‹uncurry import_variablesS›
:: ‹(list_assn string_assn)⇧k *⇩a shared_vars_assn⇧d →⇩a memory_allocation_assn ×⇩a shared_vars_assn›
unfolding import_variablesS_def
by sepref
lemmas [sepref_fr_rules] =
import_variablesS_impl.refine full_normalize_poly'_impl.refine
lemma [sepref_fr_rules]:
‹CONSTRAINT is_pure R ⟹ ((return o CFAILED), RETURN o CFAILED) ∈ R⇧k →⇩a status_assn R›
apply sepref_to_hoare
apply sep_auto
by (smt ent_refl_true is_pure_conv merge_pure_star pure_def)
sepref_definition remap_polys_l2_with_err_s_impl
is ‹uncurry3 remap_polys_l2_with_err_s›
:: ‹poly_assn⇧k *⇩a poly_assn⇧k *⇩a polys_assn_input⇧k *⇩a shared_vars_assn⇧d →⇩a
status_assn raw_string_assn ×⇩a shared_vars_assn ×⇩a polys_s_assn ×⇩a poly_s_assn›
supply [[goals_limit=1]]
supply [split] = option.splits
unfolding remap_polys_l2_with_err_s_def pow_2_64
in_dom_m_lookup_iff
fmlookup'_def[symmetric]
memory_out_msg_def[symmetric]
op_fmap_empty_def[symmetric] while_eq_nfoldli[symmetric]
unfolding
HOL_list.fold_custom_empty
apply (subst while_upt_while_direct)
apply simp
apply (rewrite in ‹(_, ⌑, _)› annotate_assn[where A=‹polys_s_assn›])
apply (rewrite at ‹fmupd ⌑› uint64_of_nat_conv_def[symmetric])
by sepref
lemmas [sepref_fr_rules] =
remap_polys_l2_with_err_s_impl.refine
definition full_checker_l_s2
:: ‹llist_polynomial ⇒ (nat, llist_polynomial) fmap ⇒ (_, string, nat) pac_step list ⇒
(string code_status × _) nres›
where
‹full_checker_l_s2 spec A st = do {
spec' ← full_normalize_poly spec;
(b, 𝒱, A, spec') ← remap_polys_l2_with_err_s spec' spec A ({#}, fmempty, fmempty);
if is_cfailed b
then RETURN (b, 𝒱, A)
else do {
PAC_checker_l_s spec' (𝒱, A) b st
}
}›
sepref_register remap_polys_l2_with_err_s full_checker_l_s2 PAC_checker_l_s
sepref_definition full_checker_l_s2_impl
is ‹uncurry2 full_checker_l_s2›
:: ‹poly_assn⇧k *⇩a polys_assn_input⇧k *⇩a (list_assn (pac_step_rel_assn (uint64_nat_assn) poly_assn string_assn))⇧k →⇩a
status_assn raw_string_assn ×⇩a shared_vars_assn ×⇩a polys_s_assn›
unfolding full_checker_l_s2_def
empty_shared_vars_def[symmetric]
by sepref
section ‹Correctness theorem›
context poly_embed
begin
definition fully_epac_assn where
‹fully_epac_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))))›
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 remap_polys_l2_with_err_s_remap_polys_s_with_err:
assumes ‹((spec, a, b, c), (spec', a', c', b')) ∈ Id›
shows ‹remap_polys_l2_with_err_s spec a b c
≤ ⇓ Id
(remap_polys_s_with_err spec' a' b' c')›
proof -
have [refine]: ‹(A, A') ∈ Id ⟹ upper_bound_on_dom A
≤ ⇓ {(n, dom). dom = set [0..<n]} (SPEC (λdom. set_mset (dom_m A') ⊆ dom ∧ finite dom))› for A A'
unfolding upper_bound_on_dom_def
apply (rule RES_refine)
apply (auto simp: upper_bound_on_dom_def)
done
have 3: ‹(n, dom) ∈ {(n, dom). dom = set [0..<n]} ⟹
([0..<n], dom) ∈ ⟨nat_rel⟩list_set_rel› for n dom
by (auto simp: list_set_rel_def br_def)
have 4: ‹(p,q) ∈ Id ⟹
weak_equality_l p spec ≤ ⇓Id (weak_equality_l q spec)› for p q spec
by auto
have 6: ‹a = b ⟹ (a, b) ∈ Id› for a b
by auto
have id: ‹f=g ⟹ f ≤⇓Id g› for f g
by auto
have [simp]: ‹vars_llist_s2 x = vars_llist_l x› for x
by (induction x rule: vars_llist_s2.induct) auto
show ?thesis
supply [[goals_limit=1]]
unfolding remap_polys_l2_with_err_s_def remap_polys_s_with_err_def
apply (refine_rcg
LFOc_refine[where R= ‹{((a,b,c), (a',b',c')). ((a,b,c), (a',c',b'))∈Id}›])
subgoal using assms by auto
subgoal using assms by auto
apply (rule id)
subgoal using assms by auto
subgoal using assms by auto
apply (rule id)
subgoal using assms by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
apply (rule 3)
subgoal by auto
subgoal by auto
subgoal using assms by auto
apply (rule id)
subgoal using assms by auto
subgoal by auto
subgoal by auto
apply (rule id)
subgoal by auto
apply (rule id)
subgoal unfolding weak_equality_l_s'_def by auto
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
done
qed
lemma full_checker_l_s2_full_checker_l_s:
‹(uncurry2 full_checker_l_s2, uncurry2 full_checker_l_s) ∈ (Id ×⇩r Id) ×⇩r Id →⇩f ⟨Id⟩nres_rel›
proof -
have id: ‹f=g ⟹ f ≤⇓Id g› for f g
by auto
show ?thesis
apply (intro frefI nres_relI)
unfolding uncurry_def
apply clarify
unfolding full_checker_l_s2_def
full_checker_l_s_def
apply (refine_rcg remap_polys_l2_with_err_s_remap_polys_s_with_err)
apply (rule id)
subgoal by auto
subgoal by auto
subgoal by auto
subgoal by auto
apply (rule id)
subgoal by auto
done
qed
lemma full_poly_input_assn_alt_def:
‹full_poly_input_assn = (hr_comp
(hr_comp (hr_comp polys_assn_input (⟨nat_rel, Id⟩fmap_rel))
(⟨nat_rel, fully_unsorted_poly_rel O mset_poly_rel⟩fmap_rel))
polys_rel)›
proof -
have [simp]: ‹⟨nat_rel, Id⟩fmap_rel = Id›
apply (auto simp: fmap_rel_def)
by (metis (no_types, hide_lams) fmap_ext_fmdom fmlookup_dom_iff fset_eqI option.sel)
show ?thesis
unfolding full_poly_input_assn_def
by auto
qed
lemma PAC_full_correctness:
‹(uncurry2 full_checker_l_s2_impl,
uncurry2 (λspec A _. PAC_checker_specification spec A))
∈ full_poly_assn⇧k *⇩a full_poly_input_assn⇧k *⇩a
fully_epac_assn⇧k →⇩a hr_comp (status_assn raw_string_assn ×⇩a shared_vars_assn ×⇩a polys_s_assn)
{((err, _), err', _). (err, err') ∈ code_status_status_rel}›
proof -
have 1: ‹(uncurry2 full_checker_l_s2, uncurry2 (λspec A _. PAC_checker_specification spec A))
∈ (⟨⟨Id⟩list_rel ×⇩r int_rel⟩list_rel O fully_unsorted_poly_rel O mset_poly_rel ×⇩r
(⟨nat_rel, Id⟩fmap_rel O ⟨nat_rel, fully_unsorted_poly_rel O mset_poly_rel⟩fmap_rel) O
polys_rel) ×⇩r
⟨p2rel
(⟨nat_rel, fully_unsorted_poly_rel O mset_poly_rel,
var_rel⟩EPAC_Checker.pac_step_rel_raw)⟩list_rel →⇩f ⟨(({((err, _), err', _).
(err, err') ∈ Id} O
{((b, A, st), b', A', st').
(¬ is_cfailed b ⟶ (A, A') ∈ {(x, y). y = set_mset x} ∧ (st, st') ∈ Id) ∧
(b, b') ∈ Id}) O
{((err, 𝒱, A), err', 𝒱', A').
((err, 𝒱, A), err', 𝒱', A')
∈ code_status_status_rel ×⇩r
vars_rel2 err ×⇩r
{(xs, ys).
¬ is_cfailed err ⟶
(xs, ys) ∈ ⟨nat_rel, sorted_poly_rel O mset_poly_rel⟩fmap_rel ∧
(∀i∈#dom_m xs. vars_llist (xs ∝ i) ⊆ 𝒱)}}) O
{((st, G), st', G').
(st, st') ∈ status_rel ∧ (st ≠ FAILED ⟶ (G, G') ∈ Id ×⇩r polys_rel)}⟩nres_rel›
using full_checker_l_s2_full_checker_l_s[
FCOMP full_checker_l_s_full_checker_l_prep',
FCOMP full_checker_l_prep_full_checker_l2',
FCOMP full_checker_l_full_checker',
FCOMP full_checker_spec',
unfolded full_poly_assn_def[symmetric]
full_poly_input_assn_def[symmetric]
fully_epac_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]
full_poly_input_assn_alt_def[symmetric]] by auto
have 2: ‹A ⊆ B ⟹ ⟨A⟩nres_rel ⊆ ⟨B⟩nres_rel› for A B
by (auto simp: nres_rel_def conc_fun_R_mono conc_trans_additional(6))
have 3: ‹(uncurry2 full_checker_l_s2, uncurry2 (λspec A _. PAC_checker_specification spec A))
∈ (⟨⟨Id⟩list_rel ×⇩r int_rel⟩list_rel O fully_unsorted_poly_rel O mset_poly_rel ×⇩r
(⟨nat_rel, Id⟩fmap_rel O ⟨nat_rel, fully_unsorted_poly_rel O mset_poly_rel⟩fmap_rel) O
polys_rel) ×⇩r
⟨p2rel
(⟨nat_rel, fully_unsorted_poly_rel O mset_poly_rel,
var_rel⟩EPAC_Checker.pac_step_rel_raw)⟩list_rel →⇩f
⟨{((err, _), err', _). (err, err') ∈ code_status_status_rel}⟩nres_rel›
apply (rule set_mp[OF _ 1])
unfolding fref_param1[symmetric]
apply (rule fun_rel_mono)
apply auto[]
apply (rule 2)
apply auto
done
have 4: ‹⟨nat_rel, Id⟩fmap_rel = Id›
apply (auto simp: fmap_rel_def)
by (metis (no_types, hide_lams) fmap_ext_fmdom fmlookup_dom_iff fset_eqI option.sel)
have H: ‹full_poly_assn = (hr_comp poly_assn
(⟨⟨Id⟩list_rel ×⇩r int_rel⟩list_rel O fully_unsorted_poly_rel O mset_poly_rel))›
‹full_poly_input_assn = hr_comp polys_assn_input
((Id O ⟨nat_rel, fully_unsorted_poly_rel O mset_poly_rel⟩fmap_rel) O polys_rel)›
unfolding full_poly_assn_def fully_epac_assn_def full_poly_input_assn_def
hr_comp_assoc O_assoc
by auto
show ?thesis
using full_checker_l_s2_impl.refine[FCOMP 3]
unfolding full_poly_assn_def[symmetric]
full_poly_input_assn_def[symmetric]
fully_epac_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]
full_poly_input_assn_alt_def[symmetric]
4 H[symmetric]
by auto
qed
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
end