Theory EPAC_Efficient

theory EPAC_Efficient_Checker imports EPAC_Checker EPAC_Perfectly_Shared begin hide_const (open) PAC_Checker.full_checker_l hide_fact (open) PAC_Checker.full_checker_l_def type_synonym shared_poly = ‹(nat list × int) list› definition (in -) add_poly_l' where ‹add_poly_l' _ = add_poly_l› definition (in -)add_poly_l_prep :: ‹(nat,string)vars ⇒ llist_polynomial × llist_polynomial ⇒ llist_polynomial nres› where ‹add_poly_l_prep 𝒟 = 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 𝒟 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_alt_def[unfolded conc_Id id_apply]: fixes xs ys :: llist_polynomial assumes ‹⋃(set ` (fst`set xs)) ⊆ set_mset 𝒟› ‹⋃(set ` fst ` set ys) ⊆ set_mset 𝒟› shows ‹add_poly_l_prep 𝒟 (xs, ys) ≤ ⇓ Id (add_poly_l' 𝒟 (xs, ys))› proof - let ?Rx = ‹{(xs', ys'). (xs', ys') ∈ ⟨Id⟩ list_rel ∧ (∃xs₀. xs = xs₀ @ xs')}› let ?Ry = ‹{(xs', ys'). (xs', ys') ∈ ⟨Id⟩ list_rel ∧ (∃xs₀. ys = xs₀ @ xs')}› have [refine0]: ‹((xs, ys), xs, ys) ∈ ?Rx ×_r ?Ry› by auto have H: ‹(x1c, x1a) ∈ ⟨Id⟩list_rel ⟹ (x1c, x1a) ∈ ⟨Id⟩list_rel› for x1c x1a by auto have [intro!]: ‹f ≤ f' ⟹ do {a ← f; P a} ≤ do {a ← f'; P a}› for f f' :: ‹_ nres› and P unfolding pw_bind_inres pw_bind_nofail pw_le_iff by blast show ?thesis using assms unfolding add_poly_l'_def add_poly_l_def add_poly_l_prep_def apply (refine_vcg perfect_shared_term_order_rel_spec[THEN order_trans]) apply (rule H) subgoal by auto apply (rule H) subgoal by auto subgoal by auto apply (rule H) subgoal by auto subgoal by auto subgoal apply (rule specify_left) apply (rule perfect_shared_term_order_rel_spec[unfolded conc_Id id_apply]) subgoal by auto subgoal by auto subgoal premises p for comp supply [intro!] = p(3)[unfolded conc_Id id_apply] using p(1,2,4-) using ordered.exhaust[of comp False] by (auto simp: lexord_irreflexive dest: term_order_rel_irreflexive; fail)+ done done qed definition (in -)normalize_poly_shared :: ‹(nat,string) vars ⇒ llist_polynomial ⇒ (bool × llist_polynomial) nres› where ‹normalize_poly_shared 𝒜 xs = do { xs ← full_normalize_poly xs; import_poly_no_new 𝒜 xs }› definition normalize_poly_sharedS :: ‹(nat,string) shared_vars ⇒ llist_polynomial ⇒ (bool × shared_poly) nres› where ‹normalize_poly_sharedS 𝒜 xs = do { xs ← full_normalize_poly xs; import_poly_no_newS 𝒜 xs }› definition (in -) mult_monoms_prep :: ‹(nat,string)vars ⇒ term_poly_list ⇒ term_poly_list ⇒ term_poly_list nres› where ‹mult_monoms_prep 𝒟 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 𝒟 (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 (in -) mult_monoms_prep_mult_monoms: assumes ‹set xs ⊆ set_mset 𝒱› ‹set ys ⊆ set_mset 𝒱› shows ‹mult_monoms_prep 𝒱 xs ys ≤ ⇓Id (SPEC ((=) (mult_monoms xs ys)))› proof - have H: ‹f ≤ RES p ⟹ (⋀x. x ∈ p ⟹ (g x) ∈ Q) ⟹ do {x ← f; RETURN (g x)} ≤ RES Q› for f p g Q by (meson bind_le_nofailI le_RES_nofailI nres_order_simps(21) order.trans) have [dest]: ‹ (x, y) ∈ var_order_rel ⟹ (y, x) ∈ var_order_rel ⟹ x = y› for x y by (meson transE trans_var_order_rel var_order_rel_antisym) have [dest]: ‹ xa ≠ UNKNOWN ⟹ xa ≠ GREATER ⟹ xa ≠ LESS ⟹ xa = EQUAL › for xa by (cases xa) auto show ?thesis using assms apply (induction xs ys rule:mult_monoms.induct) subgoal unfolding mult_monoms_prep_def by (subst RECT_unfold, refine_mono) auto subgoal unfolding mult_monoms_prep_def by (subst RECT_unfold, refine_mono) auto subgoal apply (subst mult_monoms_prep_def) apply (subst RECT_unfold, refine_mono) apply (subst mult_monoms_prep_def[symmetric])+ apply (simp only: prod.simps) apply (refine_vcg perfect_shared_term_order_rel_spec[THEN order_trans] perfect_shared_var_order_spec[THEN order_trans]) subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by (auto intro!: H) done done qed definition mult_monoms_prop :: ‹(nat,string)vars⇒ llist_polynomial ⇒ _ ⇒ llist_polynomial ⇒ llist_polynomial nres› where ‹mult_monoms_prop = (λ𝒱 qs (p, m) b. nfoldli qs (λ_. True) (λ(q, n) b. do {pq ← mult_monoms_prep 𝒱 p q; RETURN ((pq, m * n) # b)}) b)› definition mult_poly_raw_prop :: ‹(nat,string) vars⇒ llist_polynomial ⇒ llist_polynomial ⇒ llist_polynomial nres› where ‹mult_poly_raw_prop 𝒱 p q = nfoldli p (λ_. True) (mult_monoms_prop 𝒱 q) []› lemma mult_monoms_prop_mult_monomials: assumes ‹vars_llist qs ⊆ set_mset 𝒱› ‹set (fst m) ⊆ set_mset 𝒱› shows ‹mult_monoms_prop 𝒱 qs m b ≤ ⇓{(xs, ys). mset xs = mset ys} (RES{map (mult_monomials m) qs @ b})› using assms unfolding mult_monoms_prop_def apply (cases m) apply (induction qs arbitrary: b) subgoal by (auto intro!: RETURN_RES_refine) subgoal for a qs aa b ba apply (cases a) apply (simp only: prod.simps nfoldli_simps(2) if_True nres_monad3 nres_monad1) apply (refine_vcg mult_monoms_prep_mult_monoms[THEN order_trans]) subgoal by auto subgoal by auto subgoal premises p supply [intro!] = p(1)[THEN order_trans] using p(2-) by (auto simp: conc_fun_RES mult_monomials_def) done done lemma mult_poly_raw_prop_mult_poly_raw: assumes ‹vars_llist qs ⊆ set_mset 𝒱› ‹vars_llist ps ⊆ set_mset 𝒱› shows ‹mult_poly_raw_prop 𝒱 ps qs ≤ (SPEC (λc. (c, PAC_Polynomials_Operations.mult_poly_raw ps qs) ∈ {(xs, ys). mset xs = mset ys}))› proof - have [simp]: ‹foldl (λb x. map (mult_monomials x) qs @ b) b ps = foldl (λb x. map (mult_monomials x) qs @ b) [] ps @ b› if ‹NO_MATCH [] b› for qs ps b apply (induction ps arbitrary: b) apply simp by (metis (no_types, lifting) append_assoc foldl_Cons self_append_conv) have H: ‹nfoldli ps (λ_. True) (mult_monoms_prop 𝒱 qs) b0 ≤ ⇓ {(xs, ys). mset xs = mset ys} (RES {foldl (λb x. map (mult_monomials x) qs @ b) b0 ps})› for b0 using assms apply (induction ps arbitrary: b0) subgoal by (auto intro!: RETURN_RES_refine) subgoal premises p supply [intro!] = p(1)[THEN order_trans] using p(2-) apply (simp only: prod.simps nfoldli_simps(2) if_True nres_monad3 nres_monad1) apply (refine_rcg mult_monoms_prop_mult_monomials) apply auto apply (rule specify_left) apply (subst RES_SPEC_eq[symmetric]) apply (rule mult_monoms_prop_mult_monomials[unfolded conc_fun_RES]) apply (auto simp: conc_fun_RES) done done show ?thesis unfolding mult_poly_raw_def mult_poly_raw_prop_def by (rule H[THEN order_trans]) (auto simp: conc_fun_RES) qed definition (in -) mult_poly_full_prop :: ‹_› where ‹mult_poly_full_prop 𝒱 p q = do { pq ← mult_poly_raw_prop 𝒱 p q; ASSERT(vars_llist pq ⊆ vars_llist p ∪ vars_llist q); normalize_poly pq }› lemma vars_llist_mset_eq: ‹mset p = mset q ⟹ vars_llist p = vars_llist q› by (auto simp: vars_llist_def dest!: mset_eq_setD) lemma mult_poly_full_prop_mult_poly_full: assumes ‹vars_llist qs ⊆ set_mset 𝒱› ‹vars_llist ps ⊆ set_mset 𝒱› ‹(ps, ps') ∈ Id› ‹(qs, qs') ∈ Id› shows ‹mult_poly_full_prop 𝒱 ps qs ≤ ⇓Id (mult_poly_full ps' qs')› proof - have [refine0]: ‹sort_poly_spec p ≤ ⇓ Id (sort_poly_spec p')› if ‹mset p= mset p'› for p p' using that unfolding sort_poly_spec_def by auto have H: ‹x ∈ A ⟹ x= x' ⟹ x' ∈ A› for x x' A by auto show ?thesis using assms unfolding mult_poly_full_prop_def mult_poly_full_def normalize_poly_def apply (refine_vcg mult_poly_raw_prop_mult_poly_raw) apply (rule H[of _ ‹{(xs, ys). mset xs = mset ys}›], assumption) subgoal by auto subgoal by (force dest: vars_llist_mset_eq vars_llist_mult_poly_raw[THEN set_mp]) subgoal by auto subgoal by auto done qed definition (in -) linear_combi_l_prep2 where ‹linear_combi_l_prep2 i A 𝒱 xs = do { ASSERT(linear_combi_l_pre i A (set_mset 𝒱) xs); 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 q₀ ⊆ set_mset 𝒱)) then do { err ← check_linear_combi_l_dom_err q₀ i; RETURN (p, xs, error_msg i err) } else do { ASSERT(fmlookup A i ≠ None); let r = the (fmlookup A i); ASSERT(vars_llist r ⊆ set_mset 𝒱); if q₀ = [([],1)] then do { pq ← add_poly_l_prep 𝒱 (p, r); RETURN (pq, tl xs, CSUCCESS) } else do { (_, q) ← normalize_poly_shared 𝒱 (q₀); ASSERT(vars_llist q ⊆ set_mset 𝒱); pq ← mult_poly_full_prop 𝒱 q r; ASSERT(vars_llist pq ⊆ set_mset 𝒱); pq ← add_poly_l_prep 𝒱 (p, pq); RETURN (pq, tl xs, CSUCCESS) } } }) ([], xs, CSUCCESS) }› lemma (in -) import_poly_no_new_spec: ‹import_poly_no_new 𝒱 xs ≤ ⇓Id (SPEC(λ(b, xs'). (¬b ⟶ xs = xs') ∧ (¬b ⟷ vars_llist xs ⊆ set_mset 𝒱)))› unfolding import_poly_no_new_def apply (refine_vcg WHILET_rule[where I = ‹ λ(b, xs', ys'). (¬b ⟶ xs = ys' @ xs') ∧ (¬b ⟶ vars_llist ys' ⊆ set_mset 𝒱) ∧ (b ⟶ ¬vars_llist xs ⊆ set_mset 𝒱)› and R = ‹measure (λ(b, xs, _). (if b then 0 else 1) + length xs)›] import_monom_no_new_spec[THEN order_trans]) subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by (clarsimp simp add: neq_Nil_conv) subgoal by auto subgoal by auto done lemma linear_combi_l_prep2_linear_combi_l: assumes 𝒱: ‹(𝒱,𝒱') ∈ {(x, y). y = set_mset x}›‹(i,i')∈nat_rel›‹(A,A')∈Id›‹(xs,xs')∈Id› shows ‹linear_combi_l_prep2 i A 𝒱 xs ≤ ⇓Id (linear_combi_l i' A' 𝒱' xs')› proof - have H1: ‹(if p ∨ q then P else Q) = (if p then P else if q then P else Q)› for p q P Q by auto have [intro!]: ‹check_linear_combi_l_dom_err x1e x2e ≤ ⇓ Id (check_linear_combi_l_dom_err x1e x2e)› for x1e x2e by auto have linear_combi_l_alt_def: ‹linear_combi_l i A 𝒱 xs = do { ASSERT(linear_combi_l_pre i A 𝒱 xs); WHILE_T (λ(p, xs, err). xs ≠ [] ∧ ¬is_cfailed err) (λ(p, xs, _). do { ASSERT(xs ≠ []); ASSERT (vars_llist p ⊆ 𝒱); let (q :: llist_polynomial, i) = hd xs; if (i ∉# dom_m A ∨ ¬(vars_llist q ⊆ 𝒱)) then do { err ← check_linear_combi_l_dom_err q i; RETURN (p, xs, error_msg i err) } else do { ASSERT(fmlookup A i ≠ None); let r = the (fmlookup A i); ASSERT (vars_llist r ⊆ 𝒱); if q = [([], 1)] then do { pq ← add_poly_l' 𝒱' (p, r); RETURN (pq, tl xs, CSUCCESS) } else do { q ← full_normalize_poly q; ASSERT (vars_llist q ⊆ 𝒱); let q = q; pq ← mult_poly_full q r; ASSERT (vars_llist pq ⊆ 𝒱); pq ← add_poly_l' 𝒱' (p, pq); RETURN (pq, tl xs, CSUCCESS) } } }) ([], xs, CSUCCESS) }› for i A 𝒱 xs unfolding Let_def linear_combi_l_def add_poly_l'_def by auto have H: ‹P = Q ⟹ P ≤⇓Id Q› for P Q by auto have [refine0]: ‹⇓ Id (SPEC (λ(b, xs'). (¬ b ⟶ xa = xs') ∧ (¬ b) = (vars_llist xa ⊆ set_mset 𝒱))) ≤ SPEC (λc. (c, q) ∈ {((b, c), d). ¬b ∧ c = d ∧ d = q})› if ‹vars_llist xa ⊆ set_mset 𝒱› ‹xa = q› for xa 𝒱 q using that by auto show ?thesis using assms unfolding linear_combi_l_prep2_def linear_combi_l_alt_def normalize_poly_shared_def nres_monad3 apply (refine_rcg import_poly_no_new_spec[THEN order_trans] mult_poly_full_prop_mult_poly_full[THEN order_trans] add_poly_alt_def[THEN order_trans]) subgoal using 𝒱 by auto subgoal by auto subgoal by auto subgoal by auto subgoal using 𝒱 by auto apply (rule H) subgoal by auto subgoal by auto subgoal by auto subgoal by (auto simp: vars_llist_def) subgoal by auto subgoal by (auto simp: vars_llist_def) subgoal by (auto simp: vars_llist_def) apply (rule H) subgoal by (auto simp: add_poly_l'_def) subgoal by auto apply (rule H) subgoal by auto subgoal by auto subgoal using 𝒱 by auto subgoal by auto apply (solves auto)[] apply (solves auto)[] apply (rule H) subgoal by auto subgoal using 𝒱 by (auto dest!: split_list) subgoal using 𝒱 by (auto dest!: split_list) subgoal by (auto simp: vars_llist_def) apply (rule H) subgoal by (auto simp: add_poly_l'_def) subgoal by auto done qed definition check_linear_combi_l_prop where ‹check_linear_combi_l_prop spec A 𝒱 i xs r = do { (mem_err, r) ← import_poly_no_new 𝒱 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_prep2 i A 𝒱 xs; if (is_cfailed err) then do { RETURN (err, r) } else do { b ← weak_equality_l p r; b' ← weak_equality_l r spec; if b then (if b' then RETURN (CFOUND, r) else RETURN (CSUCCESS, r)) else do { c ← check_linear_combi_l_mult_err p r; RETURN (error_msg i c, r) } } }}› lemma check_linear_combi_l_prop_check_linear_combi_l: assumes ‹(𝒱,𝒱') ∈ {(x, y). y = set_mset x}› ‹(A, A') ∈ Id› ‹(i,i')∈nat_rel› ‹(xs,xs')∈Id›‹(r,r')∈Id› ‹(spec,spec')∈Id› shows ‹check_linear_combi_l_prop spec A 𝒱 i xs r ≤ ⇓{((b,r'), b'). b=b' ∧ (¬is_cfailed b ⟶ r=r')} (check_linear_combi_l spec' A' 𝒱' i' xs' r')› proof - have [refine]: ‹import_poly_no_new 𝒱 r ≤ ⇓ {((mem, r'), b). (b=mem) ∧ (¬b ⟶ r'=r ∧ vars_llist r ⊆ set_mset 𝒱)} (RES UNIV)› apply (rule order_trans) apply (rule import_poly_no_new_spec) apply (auto simp: conc_fun_RES) done have H: ‹f=g ⟹ f ≤ ⇓Id g› for f g by auto show ?thesis using assms unfolding check_linear_combi_l_prop_def check_linear_combi_l_def apply (refine_vcg linear_combi_l_prep2_linear_combi_l) subgoal using assms by auto apply (rule H) subgoal by (auto simp: check_linear_combi_l_pre_err_def) subgoal by (auto simp:error_msg_def) subgoal using assms by auto subgoal by auto apply (rule H) subgoal by auto apply (rule H) subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto apply (rule H) subgoal by auto subgoal by auto done qed definition (in -)check_extension_l2_prop :: ‹_ ⇒ _ ⇒ string multiset ⇒ nat ⇒ string ⇒ llist_polynomial ⇒ (string code_status × llist_polynomial × string multiset × string) nres› where ‹check_extension_l2_prop spec A 𝒱 i v p = do { (pre, nonew, mem, mem', p, 𝒱, v) ← do { let pre = i ∉# dom_m A ∧ v ∉ set_mset 𝒱; let b = vars_llist p ⊆ set_mset 𝒱; (mem, p, 𝒱) ← import_poly 𝒱 p; (mem', 𝒱, v) ← if b ∧ pre ∧ ¬ alloc_failed mem then import_variable v 𝒱 else RETURN (mem, 𝒱, v); RETURN (pre ∧ ¬alloc_failed mem ∧ ¬ alloc_failed mem', b, mem, mem', p, 𝒱, v) }; 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 { 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, 𝒱, v) } else do { c ← check_extension_l_side_cond_err v p q; RETURN (error_msg i c, [], 𝒱, v) } } } }› lemma check_extension_l2_prop_check_extension_l2: assumes ‹(𝒱,𝒱') ∈ {(x, y). y = set_mset x}› ‹(spec, spec') ∈ Id› ‹(A, A') ∈ Id› ‹(i,i') ∈ nat_rel› ‹(v, v') ∈ Id› ‹(p, p') ∈ Id› shows ‹check_extension_l2_prop spec A 𝒱 i v p ≤⇓{((err, q, 𝒜, va), b). (b = err) ∧ (¬is_cfailed err ⟶ q=p ∧ v=va ∧ set_mset 𝒜 = insert v 𝒱')} (check_extension_l2 spec' A' 𝒱' i' v' p')› proof - have G[refine]: ‹do { (mem, pa, 𝒱') ← import_poly 𝒱 p; (mem', 𝒱', va) ← if vars_llist p ⊆ set_mset 𝒱 ∧ (i ∉# dom_m A ∧ v ∉# 𝒱) ∧ ¬ alloc_failed mem then import_variable v 𝒱' else RETURN (mem, 𝒱', v); RETURN ((i ∉# dom_m A ∧ v ∉# 𝒱) ∧ ¬ alloc_failed mem ∧ ¬ alloc_failed mem', vars_llist p ⊆ set_mset 𝒱, mem, mem', pa, 𝒱', va) } ≤ ⇓ {((pre, nonew, mem, mem', p', 𝒜, va), b). (b=pre)∧ (b ⟶ ¬alloc_failed mem ∧ ¬alloc_failed mem') ∧ (b ∧ nonew ⟶ (p'=p ∧ set_mset 𝒜 = set_mset 𝒱 ∪ vars_llist p ∪ {v} ∧ va = v)) ∧ ((nonew ⟷ vars_llist p ⊆ set_mset 𝒱))} (SPEC (λb. b ⟶ i' ∉# dom_m A' ∧ v' ∉ 𝒱'))› using assms unfolding conc_fun_RES import_variable_def nres_monad3 apply (subst (2) RES_SPEC_eq) apply (refine_vcg import_poly_spec[THEN order_trans]) apply (clarsimp simp: ) apply (rule conjI impI) apply (refine_vcg import_poly_spec[THEN order_trans]) apply (auto simp: vars_llist_def)[] apply (auto simp: vars_llist_def)[] apply (auto simp: vars_llist_def)[] done have H: ‹f=g ⟹ f ≤ ⇓Id g› for f g by auto show ?thesis using assms unfolding check_extension_l2_prop_def check_extension_l2_def apply (refine_vcg mult_poly_full_prop_mult_poly_full add_poly_alt_def[unfolded add_poly_l'_def, THEN order_trans] ) subgoal by auto apply (rule H) subgoal by auto subgoal by (simp add: error_msg_def) subgoal by auto apply (rule H) subgoal by (auto simp: check_extension_l_new_var_multiple_err_def) subgoal by (simp add: error_msg_def) subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal by auto subgoal using assms by (auto dest: split_list_first simp: vars_llist_def) subgoal by (auto simp: vars_llist_def) apply (rule H) subgoal by auto subgoal by auto apply (rule H) subgoal by auto subgoal by auto subgoal by (auto dest!: split_list_first simp: remove1_append) apply (rule H) subgoal by (auto simp: check_extension_l_new_var_multiple_err_def check_extension_l_side_cond_err_def) subgoal by (auto simp: error_msg_def) done qed definition PAC_checker_l_step_prep :: ‹_ ⇒ string code_status × string multiset × _ ⇒ (llist_polynomial, string, nat) pac_step ⇒ _› where ‹PAC_checker_l_step_prep = (λspec (st', 𝒱, A) st. do { ASSERT (PAC_checker_l_step_inv spec st' (set_mset 𝒱) A); ASSERT (¬is_cfailed st'); case st of CL _ _ _ ⇒ do { r ← full_normalize_poly (pac_res st); (eq, r) ← check_linear_combi_l_prop 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_prop spec A (𝒱) (new_id st) (new_var st) r; if ¬is_cfailed eq then do { r ← add_poly_l_prep 𝒱 ([([v], -1)], r); RETURN (st', 𝒱, fmupd (new_id st) r A) } else RETURN (eq, 𝒱, A) }} )› lemma PAC_checker_l_step_prep_PAC_checker_l_step: assumes ‹(state, state') ∈ {((st, 𝒱, A), (st', 𝒱', A')). (st,st')∈Id ∧ (A,A')∈Id ∧ (¬is_cfailed st ⟶ (𝒱,𝒱')∈ {(x, y). y = set_mset x})}› ‹(spec,spec')∈Id› ‹(step,step')∈Id› shows ‹PAC_checker_l_step_prep spec state step ≤ ⇓{((st, 𝒱, A), (st', 𝒱', A')). (st,st')∈Id ∧ (A,A')∈Id ∧ (¬is_cfailed st ⟶ (𝒱,𝒱')∈ {(x, y). y = set_mset x})} (PAC_checker_l_step spec' state' step')› proof - have H: ‹f=g ⟹ f ≤ ⇓Id g› for f g by auto show ?thesis using assms apply - unfolding PAC_checker_l_step_prep_def PAC_checker_l_step_def apply (simp only: split: prod.splits) apply (simp only: split:prod.splits pac_step.splits) apply (intro conjI impI allI) subgoal apply (refine_rcg check_linear_combi_l_prop_check_linear_combi_l) subgoal using assms by auto subgoal by auto apply (rule H) 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 done subgoal by auto subgoal by auto subgoal by auto subgoal apply (refine_rcg check_extension_l2_prop_check_extension_l2 add_poly_alt_def[unfolded add_poly_l'_def, THEN order_trans]) subgoal by auto subgoal by auto apply (rule H) 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 add: vars_llist_def) apply (rule H) subgoal by auto subgoal by auto subgoal by auto done subgoal by auto subgoal by auto subgoal by auto subgoal apply (refine_rcg) subgoal by auto subgoal by auto apply (rule H) subgoal by auto subgoal by auto subgoal by auto subgoal by auto done done qed definition (in -) remap_polys_l2_with_err :: ‹llist_polynomial ⇒ llist_polynomial ⇒ (nat, string) vars ⇒ (nat, llist_polynomial) fmap ⇒ (string code_status × (nat, string) vars × (nat, llist_polynomial) fmap) nres› where ‹remap_polys_l2_with_err 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); ASSERT(¬failed ⟶ spec = spec'); 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) }})› lemma remap_polys_l_with_err_alt_def: ‹remap_polys_l_with_err spec spec0 = (λ𝒱 A. do{ ASSERT (remap_polys_l_with_err_pre spec spec0 𝒱 A); dom ← SPEC(λdom. set_mset (dom_m A) ⊆ dom ∧ finite dom); 𝒱 ← RETURN (𝒱 ∪ vars_llist spec0); spec ← RETURN spec; failed ← SPEC(λ_::bool. True); 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' ← SPEC(λerr. err ≠ CFOUND); if is_cfailed err' then RETURN((err', 𝒱, A')) else do { p ← full_normalize_poly (the (fmlookup A i)); eq ← weak_equality_l p spec; 𝒱 ← RETURN(𝒱 ∪ vars_llist (the (fmlookup A i))); RETURN((if eq then CFOUND else CSUCCESS), 𝒱, fmupd i p A') } } else RETURN (err, 𝒱, A')) (CSUCCESS, 𝒱, fmempty); RETURN (err, 𝒱, A) }})› unfolding remap_polys_l_with_err_def by (auto intro!: ext bind_cong[OF refl]) lemma remap_polys_l2_with_err_polys_l2_with_err: assumes ‹(𝒱, 𝒱') ∈ {(x, y). y = set_mset x}› ‹(A,A') ∈ Id› ‹(spec, spec')∈Id› ‹(spec0, spec0')∈Id› shows ‹remap_polys_l2_with_err spec spec0 𝒱 A ≤ ⇓{((st, 𝒱, A), st', 𝒱', A'). (st, st') ∈ Id ∧ (A, A') ∈ Id ∧ (¬ is_cfailed st ⟶ (𝒱, 𝒱') ∈ {(x, y). y = set_mset x})} (remap_polys_l_with_err spec' spec0' 𝒱' A')› proof - have [refine]: ‹inj_on id dom› for dom by (auto simp: inj_on_def) have [refine]: ‹((CSUCCESS, 𝒱, fmempty), CSUCCESS, 𝒱', fmempty) ∈ {((st, 𝒱, A), st', 𝒱', A'). (st, st') ∈ Id ∧ (A, A') ∈ Id ∧ (¬ is_cfailed st ⟶ (𝒱, 𝒱') ∈ {(x, y). y = set_mset x})}› if ‹(𝒱, 𝒱') ∈ {(x, y). y = set_mset x}› for 𝒱 𝒱' using assms that by auto have [refine]: ‹import_poly x1c p ≤⇓{((mem, ys, 𝒜'), (err :: string code_status)). (alloc_failed mem ⟷ err = CFAILED ''memory out'') ∧ (¬alloc_failed mem ⟷ err = CSUCCESS) ∧ (¬ alloc_failed mem ⟶ ys = p ∧ set_mset 𝒜' = set_mset x1c ∪ ⋃ (set ` fst ` set p))} (SPEC (λerr. err ≠ CFOUND))› for x1c p apply (rule order_trans[OF import_poly_spec]) apply (auto simp: conc_fun_RES) done have id: ‹f=g ⟹ f ≤⇓Id g› for f g by auto have id2: ‹(f,g)∈{(x, y). y = set_mset x} ⟹ (f,g)∈{(x, y). y = set_mset x}› for f g by auto have [refine]: ‹ SPEC (λ(mem, 𝒱'). ¬ alloc_failed mem ⟶ set_mset 𝒱' = set_mset 𝒱 ∪ vars_llist spec0) ≤ SPEC (λc. (c, 𝒱' ∪ vars_llist spec0') ∈ {((mem, x), y). ¬ alloc_failed mem ⟶ y = set_mset x})› using assms by auto have [refine]: ‹(x, 𝒱''') ∈ {((mem, x), y). ¬ alloc_failed mem ⟶ y = set_mset x} ⟹ x = (x1, 𝒱'') ⟹ (if ¬ alloc_failed x1 then import_poly 𝒱'' spec else SPEC(λ_. True)) ≤ SPEC (λc. (c, spec') ∈ {((new, ys, 𝒜'), spec'). (¬ alloc_failed new ∧ ¬ alloc_failed x1 ⟶ ys = spec ∧ spec' = spec ∧ set_mset 𝒜' = set_mset 𝒱'' ∪ ⋃ (set ` mononoms spec))})› for 𝒱'' 𝒱''' x x1 using assms by (auto split: if_splits intro!: import_poly_spec[THEN order_trans]) have [simp]: ‹(⋃a∈set spec'. set (fst a)) ⊆ (⋃a∈set spec0'. set (fst a)) ⟹ set_mset 𝒱 ∪ (⋃x∈set spec0'. set (fst x)) ∪ (⋃x∈set spec'. set (fst x)) = set_mset 𝒱 ∪ (⋃x∈set spec0'. set (fst x))› by (auto) show ?thesis unfolding remap_polys_l2_with_err_def remap_polys_l_with_err_alt_def apply (refine_rcg) subgoal using assms unfolding remap_polys_l_with_err_pre_def by auto subgoal using assms by auto apply assumption subgoal by auto subgoal using assms by auto subgoal by (auto simp: error_msg_def) subgoal using assms by (simp add: ) subgoal by (auto intro!: RES_refine) subgoal using assms by (simp add: ) subgoal using assms by (simp add: remap_polys_l_with_err_pre_def vars_llist_def) subgoal using assms by auto subgoal using assms by auto subgoal by auto subgoal using assms by auto subgoal by (auto simp: vars_llist_def) apply (rule id) subgoal using assms by auto apply (rule id) subgoal using assms by auto apply (rule id2) subgoal using assms by (clarsimp simp add: vars_llist_def) subgoal using assms by auto subgoal using assms by auto subgoal using assms by auto done qed definition PAC_checker_l2 where ‹PAC_checker_l2 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_prep spec bA (hd n); RETURN (S, tl n) }) ((b, A), st); RETURN S }› lemma PAC_checker_l2_PAC_checker_l: assumes ‹(A, A') ∈ {(x, y). y = set_mset x} ×_r Id› ‹(spec, spec')∈Id› ‹(st, st')∈Id› ‹(b,b')∈Id› shows ‹PAC_checker_l2 spec A b st ≤ ⇓{((b, A, st), (b', A', st')). (¬is_cfailed b ⟶ (A, A') ∈ {(x, y). y = set_mset x} ∧ (st, st')∈Id) ∧ (b,b')∈Id} (PAC_checker_l spec' A' b' st')› proof - show ?thesis unfolding PAC_checker_l2_def PAC_checker_l_def apply (refine_rcg PAC_checker_l_step_prep_PAC_checker_l_step WHILET_refine[where R = ‹{(((b, A), st:: (llist_polynomial, string, nat) pac_step list), (b', A'), st'). (¬is_cfailed b ⟶ (A, A') ∈ {(x, y). y = set_mset x} ×_r Id) ∧ (b,b')∈Id ∧ (st,st')∈Id}›]) subgoal using assms by auto subgoal by auto subgoal by auto subgoal by auto subgoal using assms by auto subgoal by auto subgoal by auto subgoal by auto done qed definition (in -) remap_polys_l2_with_err_prep :: ‹llist_polynomial ⇒ llist_polynomial ⇒ (nat, string) vars ⇒ (nat, llist_polynomial) fmap ⇒ (string code_status × (nat, string) vars × (nat, llist_polynomial) fmap × llist_polynomial) nres› where ‹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) }})› lemma remap_polys_l2_with_err_prep_remap_polys_l2_with_err: assumes ‹(p, p') ∈ Id› ‹(q, q') ∈ Id› ‹(A,A') ∈ ⟨Id, Id⟩fmap_rel› and ‹(V,V') ∈ Id› shows ‹remap_polys_l2_with_err_prep p q V A ≤ ⇓{((b, A, st, spec'), (b', A', st')). ((b, A, st), (b', A', st')) ∈ Id ∧ (¬is_cfailed b ⟶ spec' = p')} (remap_polys_l2_with_err p' q' V' A')› proof - have [simp]: ‹⟨Id, Id⟩fmap_rel = Id› apply (auto simp: fmap_rel_def fmlookup_dom_iff intro!: fmap_ext dest: fmdom_notD) by (metis fmdom_notD fmlookup_dom_iff option.sel) have 1: ‹inj_on id (dom :: nat set)› for dom by auto have [refine]: ‹(x2e, x2c)∈Id ⟹ ((CSUCCESS, x2e, fmempty), CSUCCESS, x2c, fmempty) ∈ Id ×_r Id ×_r ⟨Id, Id⟩fmap_rel› for x2e x2c by auto have [refine]: ‹import_poly x y ≤ ⇓ Id (import_poly x' y')› if ‹(x,x') ∈ Id›‹(y,y') ∈ Id› for x x' y y' using that by auto have [refine]: ‹full_normalize_poly x ≤ ⇓ Id (full_normalize_poly x')› if ‹(x,x')∈Id› for x x' using that by auto have [refine]: ‹weak_equality_l x y ≤ ⇓ bool_rel (weak_equality_l x' y')› if ‹(x,x')∈Id› ‹(y,y')∈Id› for x x' y y' using that by auto show ?thesis unfolding remap_polys_l2_with_err_prep_def remap_polys_l2_with_err_def apply (refine_vcg 1) 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 using assms by auto subgoal by (auto intro!: RES_refine simp: error_msg_def) 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 by auto subgoal by auto subgoal using assms by auto subgoal by auto subgoal by auto subgoal using assms by auto done qed definition full_checker_l_prep :: ‹llist_polynomial ⇒ (nat, llist_polynomial) fmap ⇒ (_, string, nat) pac_step list ⇒ (string code_status × _) nres› where ‹full_checker_l_prep spec A st = do { spec' ← full_normalize_poly spec; (b, 𝒱, A, spec) ← remap_polys_l2_with_err_prep spec' spec {#} A; if is_cfailed b then RETURN (b, 𝒱, A) else do { let 𝒱 = 𝒱; PAC_checker_l2 spec (𝒱, A) b st } }› lemma remap_polys_l2_with_err_polys_l_with_err: assumes ‹(𝒱, 𝒱') ∈ {(x, y). y = set_mset x}› ‹(A,A') ∈ Id› ‹(spec, spec')∈Id› ‹(spec0, spec0')∈Id› shows ‹remap_polys_l2_with_err_prep spec spec0 𝒱 A ≤ ⇓{((st, 𝒱, A, spec''), st', 𝒱', A'). (st, st') ∈ Id ∧ (A, A') ∈ Id ∧ (¬ is_cfailed st ⟶ (𝒱, 𝒱') ∈ {(x, y). y = set_mset x} ∧ spec'' = spec)} (remap_polys_l_with_err spec' spec0' 𝒱' A')› proof - have [simp]: ‹⟨Id, Id⟩fmap_rel = Id› apply (auto simp: fmap_rel_def fmlookup_dom_iff intro!: fmap_ext dest: fmdom_notD) by (metis fmdom_notD fmlookup_dom_iff option.sel) have A: ‹(A, A') ∈ ⟨nat_rel, Id⟩fmap_rel› ‹(𝒱, 𝒱) ∈ Id› ‹(A',A') ∈ Id› ‹(spec',spec')∈ Id› ‹(spec0', spec0') ∈ Id› using assms(2) by auto show ?thesis apply (rule remap_polys_l2_with_err_prep_remap_polys_l2_with_err[THEN order_trans]) apply (rule assms A)+ apply (rule order_trans) apply (rule ref_two_step') apply (rule remap_polys_l2_with_err_polys_l2_with_err) apply (rule assms A)+ apply (subst conc_fun_chain) apply (rule conc_fun_R_mono) apply (use assms in auto) done qed lemma full_checker_l_prep_full_checker_l: assumes ‹(spec, spec')∈Id› ‹(st, st')∈Id› ‹(A,A')∈Id› shows ‹full_checker_l_prep spec A st ≤⇓{((b, A, st), (b', A', st')). (¬is_cfailed b ⟶ (A, A') ∈ {(x, y). y = set_mset x} ∧ (st, st')∈Id) ∧ (b,b')∈Id} (full_checker_l spec' A' st')› proof - have id: ‹f=g ⟹ f ≤⇓Id g› for f g by auto show ?thesis unfolding full_checker_l_prep_def full_checker_l_def apply (refine_rcg remap_polys_l2_with_err_polys_l_with_err PAC_checker_l2_PAC_checker_l remap_polys_l2_with_err_polys_l_with_err) apply (rule id) subgoal using assms by auto subgoal by auto apply (rule assms) subgoal by auto apply (rule assms) subgoal by auto subgoal using assms by auto subgoal by auto subgoal using assms by auto subgoal using assms by auto subgoal by auto done qed lemma full_checker_l_prep_full_checker_l2': shows ‹(uncurry2 full_checker_l_prep, uncurry2 full_checker_l) ∈ (Id ×_r Id) ×_r Id →_f ⟨{((b, A, st), (b', A', st')). (¬is_cfailed b ⟶ (A, A') ∈ {(x, y). y = set_mset x} ∧ (st, st')∈Id) ∧ (b,b')∈Id}⟩nres_rel› by (auto intro!: frefI nres_relI full_checker_l_prep_full_checker_l[THEN order_trans]) end

Theory EPAC_Efficient_Checker