Theory SM_Ample_Impl
theory SM_Ample_Impl
imports SM_Datastructures "../Analysis/SM_POR"
"HOL-Library.RBT_Mapping"
begin
text ‹
Given a sticky program, we implement
a valid ample-function by picking the transitions from the first
PID that qualifies as an ample-set›
context visible_prog
begin
definition ga_gample
:: "(cmdc×cmdc) set ⇒ pid_global_config ⇒ global_action set"
where
"ga_gample sticky_E gc ≡ let
lcs = pid_global_config.processes gc;
gs = pid_global_config.state gc;
as = find_min_idx_f (λlc.
let
c = local_config.command lc;
ls = local_config.state lc;
as = set (comp.succ_impl c)
in
if (∀(a,_)∈as. read_globals a = {} ∧ write_globals a = {}) then
let
as = {(a,c')∈as. la_en' (ls,gs) a}
in
if as={} ∨ (∃(a,c')∈as. (c,c')∈sticky_E) then
None
else
Some (c,as)
else
None
) lcs
in
case as of
Some (pid,c,as) ⇒ (λ(a,c'). (pid,c,a,c'))`as
| None ⇒ ga_gen gc"
definition "ga_ample sticky_E
≡ stutter_extend_en (ga_gample sticky_E)"
lemma ga_gample_subset: "ga_gample sticky_E gc ⊆ ga_gen gc"
unfolding ga_gample_def ga_gen_def
by (auto
simp: comp.astep_impl_def
split: option.splits if_split_asm
dest!: find_min_idx_f_SomeD)
lemma ga_gample_empty_iff: "ga_gample sticky_E gc = {} ⟷ ga_gen gc = {}"
unfolding ga_gample_def ga_gen_def
by (fastforce
simp: comp.astep_impl_def
split: option.splits if_split_asm
dest!: find_min_idx_f_SomeD)
lemma ga_ample_None_iff: "None ∈ ga_ample sticky_E gc ⟷ None ∈ ga_en gc"
by (auto
simp: ga_ample_def ga_en_def stutter_extend_en_def ga_gample_empty_iff)
lemma ga_ample_neq_en_eq:
assumes "ga_ample sticky_E gc ≠ ga_en gc"
shows "ga_ample sticky_E gc = Some`ga_gample sticky_E gc ∧ ga_en gc = Some`ga_gen gc"
using assms ga_gample_subset
unfolding ga_ample_def ga_en_def stutter_extend_en_def
by (auto split: if_split_asm simp: ga_gample_empty_iff)
lemma pid_pac_alt: "pid_pac pid = insert None (Some`{(pid',cac). pid'=pid})"
apply (auto simp: pid_pac_def split: option.splits)
apply (case_tac x)
apply auto
done
end
context sticky_prog begin
sublocale ample_prog prog is_vis_var sticky_E "ga_ample sticky_E"
proof -
have aux: "Some ` A = Some ` B ∩ pid_pac pid ⟷ A = {(pid', cac). (pid', cac) ∈ B ∧ pid' = pid}"
for A B pid
proof
assume 1: "Some ` A = Some ` B ∩ pid_pac pid"
show "A = {(pid', cac). (pid', cac) ∈ B ∧ pid' = pid}"
using 1
apply (auto simp: pid_pac_alt)
unfolding image_def
apply auto
using 1 by blast
next
show "Some ` A = Some ` B ∩ pid_pac pid" if "A = {(pid', cac). (pid', cac) ∈ B ∧ pid' = pid}"
using that by (auto simp: pid_pac_alt)
qed
show "ample_prog prog is_vis_var sticky_E (ga_ample sticky_E)"
apply unfold_locales
apply (frule ga_ample_neq_en_eq, clarsimp)
apply (intro conjI)
apply (auto
simp: ga_gample_def sticky_ga_def
dest!: find_min_idx_f_SomeD
split: option.splits if_split_asm) []
apply (fastforce
simp: ga_gample_def sticky_ga_def
dest!: find_min_idx_f_SomeD
split: option.splits if_split_asm) []
unfolding aux
apply (simp add: inj_image_eq_iff pid_pac_def)
apply (thin_tac "ga_ample c a = b" for a b c)
apply (simp add: ga_gample_def split: option.splits prod.splits)
apply (thin_tac "a ≠ ga_gen b" for a b)
apply (drule find_min_idx_f_SomeD)
apply clarsimp
apply (rename_tac gc pid c as)
apply (rule_tac x=pid in exI)
apply (auto
split: if_split_asm prod.splits
simp: ga_gen_def comp.astep_impl_def)
unfolding is_ample_static_def comp.astep_impl_def
apply force
done
qed
end
text ‹ The following locale expresses a correct ample-reduction on
the level of subset and stuttering-equivalences of traces ›
locale hl_reduction =
visible_prog +
ample: sa "⦇ g_V = UNIV, g_E = step, g_V0 = {pid_init_gc}, sa_L = pid_interp_gc ⦈"
for step +
assumes ample_accept_subset: "ample.accept w ⟹ lv.sa.accept w"
assumes ample_accept_stuttering: "lv.sa.accept w ⟹ ∃w'. w≈w' ∧ ample.accept w'"
locale hl_ample_reduction =
visible_prog +
ample: sa "⦇ g_V = UNIV, g_E = rel_of_enex (ample, ga_ex), g_V0 = {pid_init_gc},
sa_L = pid_interp_gc ⦈"
for ample +
assumes ample_accept_subset: "ample.accept w ⟹ lv.sa.accept w"
assumes ample_accept_stuttering: "lv.sa.accept w ⟹ ∃w'. w≈w' ∧ ample.accept w'"
begin
sublocale hl_reduction prog is_vis_var "rel_of_enex (ample, ga_ex)"
apply unfold_locales
using ample_accept_subset ample_accept_stuttering by auto
end
context sticky_prog
begin
sublocale hl_ample: hl_ample_reduction prog is_vis_var "ga_ample sticky_E"
apply unfold_locales
unfolding ample_rel_def[symmetric]
unfolding reduced_automaton_def[symmetric]
apply simp
apply simp
using ample_accept_subset
apply simp
apply (erule ample_accept_stuttering)
apply blast
done
end
text ‹Next, we implement the selection of a set of sticky edges›
context visible_prog begin
definition "cr_ample ≡ do {
sticky_E ← find_fas_init cfgc_G vis_edges;
RETURN (ga_ample (sticky_E))
}"
lemma cr_ample_reduction:
"cr_ample ≤ SPEC (hl_ample_reduction prog is_vis_var)"
unfolding cr_ample_def
apply (refine_vcg order_trans[OF find_fas_init_correct])
apply unfold_locales[]
apply simp
proof clarify
fix sticky_E
assume "is_fas cfgc_G sticky_E" "vis_edges ⊆ sticky_E"
then interpret sticky_prog prog is_vis_var sticky_E
by unfold_locales
show "hl_ample_reduction prog is_vis_var (ga_ample sticky_E)" by unfold_locales
qed
end
text ‹We derive an implementation for finding the feedback arcs,
and an efficient implementation for ga_gample.›
text ‹We replace finding the sticky edges by an efficient algorithm›
context visible_prog begin
definition ga_gample_m
:: "_ ⇒ _ ⇒ pid_global_config ⇒ global_action set"
where
"ga_gample_m mem sticky_E gc ≡ let
lcs = pid_global_config.processes gc;
gs = pid_global_config.state gc;
as = find_min_idx_f (λlc.
let
c = local_config.command lc;
ls = local_config.state lc;
as = set (comp.succ_impl c)
in
if (∀(a,_)∈as. read_globals a = {} ∧ write_globals a = {}) then
let
as = {(a,c')∈as. la_en' (ls,gs) a}
in
if as={} ∨ (∃(a,c')∈as. mem (c,c') sticky_E) then
None
else
Some (c,as)
else
None
) lcs
in
case as of
Some (pid,c,as) ⇒ (λ(a,c'). (pid,c,a,c'))`as
| None ⇒ ga_gen gc"
lemma ga_gample_m_refine:
fixes Rs :: "('si×'s) set"
shows "(ga_gample_m, ga_gample_m) ∈ (Id×⇩rId → Rs → bool_rel) → Rs → Id → ⟨Id⟩set_rel"
proof (intro fun_relI, simp)
fix m :: "cmdc×cmdc ⇒ 's ⇒ bool" and m' :: "cmdc×cmdc ⇒ 'si ⇒ bool"
and se se' gc
assume "(m',m)∈Id → Rs → bool_rel" and "(se',se)∈Rs"
hence "⋀c c'. (m' (c,c') se', m (c,c') se)∈Id"
by parametricity simp_all
hence A: "⋀c c'. m' (c,c') se' = m (c,c') se" by simp
show "ga_gample_m m' se' gc = ga_gample_m m se gc"
unfolding ga_gample_m_def
by (subst A) (rule refl)
qed
lemma ga_gample_eq_gample_m: "ga_gample = ga_gample_m (∈)"
unfolding ga_gample_def[abs_def] ga_gample_m_def[abs_def]
by auto
lemma stutter_extend_en_refine:
"(stutter_extend_en, stutter_extend_en) ∈ (R → ⟨Id⟩set_rel) → R → ⟨⟨Id⟩option_rel⟩set_rel"
unfolding stutter_extend_en_def[abs_def]
apply parametricity
by auto
lemma is_vis_var_refine: "(is_vis_var, is_vis_var) ∈ Id → bool_rel" by simp
lemma vis_edges_refine: "(λx. x∈vis_edges,vis_edges)∈⟨Id×⇩rId⟩fun_set_rel"
by (simp add: fun_set_rel_def br_def)
lemma [autoref_op_pat_def]:
"vis_edges ≡ Autoref_Tagging.OP vis_edges"
"ga_gample_m ≡ Autoref_Tagging.OP ga_gample_m"
"cfgc_G ≡ Autoref_Tagging.OP cfgc_G"
by simp_all
schematic_goal cr_ample_impl1_aux:
notes [autoref_rules] =
ga_gample_m_refine stutter_extend_en_refine is_vis_var_refine
cfgc_G_impl_refine
vis_edges_refine IdI[of prog]
shows "(RETURN (?c::?'c),cr_ample)∈?R"
unfolding cr_ample_def ga_ample_def ga_gample_eq_gample_m
using [[autoref_trace_failed_id, autoref_trace_intf_unif]]
by (autoref_monadic (plain, trace))
concrete_definition cr_ample_impl1 uses cr_ample_impl1_aux
lemma cr_ample_impl1_reduction:
"hl_ample_reduction prog is_vis_var cr_ample_impl1"
proof -
note cr_ample_impl1.refine[THEN nres_relD]
also note cr_ample_reduction
finally show ?thesis by simp
qed
end
text ‹The efficient implementation of @{const visible_prog.ga_gample} uses
the @{const collecti_index} function›
lemma collecti_index_cong:
assumes C: "⋀i. i<length l ⟹ f i (l!i) = f' i (l'!i)"
assumes [simp]: "l=l'"
shows "collecti_index f l = collecti_index f' l'"
proof -
{
fix i0 s0
assume "∀i<length l. f (i0+i) (l!i) = f' (i0+i) (l!i)"
hence "collecti_index' i0 s0 f l = collecti_index' i0 s0 f' l"
proof (induction l arbitrary: i0 s0)
case (Cons a l)
from Cons.prems[THEN spec, of 0] have
[simp]: "f i0 a = f' i0 a" by simp
from Cons.prems have
IHP: "∀i<length l. f (Suc i0+i) (l!i) = f' (Suc i0+i) (l!i)"
by auto
show ?case by (auto split: bool.splits simp: Cons.IH[OF IHP])
qed simp
} from this[of 0 "{}"] show ?thesis using assms by simp
qed
lemma find_min_idx_f_cong:
assumes "⋀x. x∈set l ⟹ f x = f' x"
assumes "l=l'"
shows "find_min_idx_f f l = find_min_idx_f f' l'"
unfolding assms(2)[symmetric]
using assms(1)
apply (induction l)
apply (auto split: option.split)
done
lemma find_min_idx_impl_collecti: "(
case find_min_idx_f f l of
Some (i,r) ⇒ {i} × s1 i r
| None ⇒ {(i,r) | i r. i<length l ∧ r∈s2 i (l!i)}
)
= (
collecti_index (λi x.
case f x of
Some r ⇒ (True, s1 i r)
| None ⇒ (False, s2 i x)
) l
)" (is "?l=?r" is "_ = collecti_index ?fc l")
proof (cases "∃i<length l. f (l!i) ≠ None")
define i where "i ≡ LEAST i. i < length l ∧ f (l ! i) ≠ None"
have C_ALT: "(∃i<length l. f (l!i) ≠ None)
⟷ (∃i. i < length l ∧ fst (?fc i (l ! i)))"
by (auto split: option.split)
have i_alt: "i = (LEAST i. i < length l ∧ fst (?fc i (l ! i)))"
unfolding i_def
apply (fo_rule arg_cong)
by (auto split: option.split)
{
case True
from LeastI_ex[OF True] obtain r where [simp]: "i<length l" "f (l!i) = Some r"
by (auto simp: i_def)
from True find_min_idx_f_LEAST_eq[of f l]
have "find_min_idx_f f l = Some (i, the (f (l ! i)))"
by (simp add: i_def)
hence LEQ: "?l = {i} × s1 i r" by simp
from collecti_index_collect[of ?fc l, folded i_alt] True C_ALT have
REQ: "?r = {i} × snd (?fc i (l!i))"
by simp
show "?l=?r" unfolding LEQ unfolding REQ by auto
}
{
case False
from False find_min_idx_f_LEAST_eq[of f l]
have "find_min_idx_f f l = None" by simp
hence LEQ: "?l = {(i,r) | i r. i<length l ∧ r∈s2 i (l!i)}" by simp
from False C_ALT collecti_index_collect[of ?fc l] have
REQ: "?r = {(i, x) |i x. i < length l ∧ x ∈ snd (?fc i (l ! i))}"
by auto
show "?l=?r" unfolding LEQ unfolding REQ using False by auto
}
qed
lemma find_min_idx_impl_collecti_scheme:
assumes "⋀x. s11 x = (case x of (i,r) ⇒ {i} × iss i r)"
assumes "s12 = {(i,r) | i r. i<length l ∧ r∈isn i (l!i)}"
assumes "⋀i. i<length l ⟹ f2 i (l!i) = (case f (l!i) of
Some r ⇒ (True, iss i r)
| None ⇒ (False, isn i (l!i)))"
shows "(case find_min_idx_f f l of Some x ⇒ s11 x | None ⇒ s12)
= (collecti_index f2 l)"
apply (simp only: assms(1,2,3) cong: collecti_index_cong)
apply (subst find_min_idx_impl_collecti)
apply simp
done
schematic_goal stutter_extend_en_list_aux: "(?c, stutter_extend_en)
∈ (R → ⟨S⟩list_set_rel) → R → ⟨⟨S⟩option_rel⟩list_set_rel"
unfolding stutter_extend_en_def[abs_def]
apply (autoref)
done
concrete_definition stutter_extend_en_list uses stutter_extend_en_list_aux
lemma succ_of_enex_impl_aux:
"{s'. ∃a∈en s. s'=ex a s} = (λa. ex a s)`en s" by auto
schematic_goal succ_of_enex_list_aux: "(?c, succ_of_enex) ∈
(Id → ⟨Id⟩list_set_rel) ×⇩r (Id → Id → Id) → Id → ⟨Id⟩list_set_rel"
unfolding succ_of_enex_def[abs_def]
unfolding succ_of_enex_impl_aux
by (autoref (trace, keep_goal))
concrete_definition succ_of_enex_list uses succ_of_enex_list_aux
schematic_goal pred_of_enex_list_aux: "(?c, pred_of_enex) ∈
(Id → ⟨Id⟩list_set_rel) ×⇩r (Id → Id → Id) → Id → Id → bool_rel"
unfolding pred_of_enex_def[abs_def]
by (autoref (trace, keep_goal))
concrete_definition pred_of_enex_list uses pred_of_enex_list_aux
definition "rel_of_enex_list enex ≡ rel_of_pred (pred_of_enex_list enex)"
lemma rel_of_enex_list_refine: "(rel_of_enex_list, rel_of_enex) ∈
(Id → ⟨Id⟩list_set_rel) ×⇩r (Id → Id → Id) → ⟨Id ×⇩r Id⟩ set_rel"
proof -
have 1: "rel_of_enex_list = rel_of_pred ∘ pred_of_enex_list" using rel_of_enex_list_def by force
have 2: "rel_of_enex = rel_of_pred ∘ pred_of_enex" by auto
have 3: "(rel_of_pred, rel_of_pred) ∈ (Id → Id → bool_rel) → ⟨Id ×⇩r Id⟩set_rel" by auto
show ?thesis unfolding 1 2 by (parametricity add: 3 pred_of_enex_list.refine)
qed
context visible_prog begin
definition "ga_gample_mi2 mem sticky_E (gc::pid_global_config) = (
let
lcs = pid_global_config.processes gc;
gs = pid_global_config.state gc
in
collecti_index (λ_ lc. let
c = local_config.command lc;
ls = local_config.state lc;
as = set (comp.succ_impl c);
s={(a,c')∈as. la_en' (ls,gs) a};
ample =
s≠{}
∧ (∀(a,_)∈as. read_globals a = {} ∧ write_globals a = {})
∧ (∀(a,c')∈s. ¬ mem (c,c') sticky_E)
in
(ample,{c}×s)
) lcs
)"
lemma ga_gample_mi2_impl:
"ga_gample_m mem sticky_E gc = ga_gample_mi2 mem sticky_E gc"
unfolding ga_gample_m_def ga_gample_mi2_def
apply simp
apply (rule find_min_idx_impl_collecti_scheme[where
iss="λpid (c,S). (λ(a,c'). (c,a,c'))`S" and
isn="λpid lc. {(c,a,c'). cfgc c a c'
∧ c = cmd_of_pid gc pid
∧ la_en' (local_config.state lc, pid_global_config.state gc) a}"]
)
apply auto []
unfolding ga_gen_def
apply auto []
apply (auto simp: comp.astep_impl_def)
done
definition "cr_ample_impl2 ≡
let sticky = find_fas_init_code (=) bounded_hashcode_nat
(def_hashmap_size TYPE(nat)) cfgc_G_impl (λx. x ∈ vis_edges)
in stutter_extend_en (ga_gample_mi2 (λx f. f x) sticky)"
definition "ample_step_impl2 ≡ rel_of_enex (cr_ample_impl2,ga_ex)"
lemma cr_ample_impl2_reduction:
"hl_reduction prog is_vis_var ample_step_impl2"
proof -
from cr_ample_impl1_reduction
interpret hl_ample_reduction prog is_vis_var cr_ample_impl1 .
have 1: "ample_step_impl2 = rel_of_enex (cr_ample_impl1, ga_ex)"
unfolding ample_step_impl2_def cr_ample_impl1_def cr_ample_impl2_def
unfolding ga_gample_mi2_impl[abs_def]
by simp
show ?thesis
apply unfold_locales
unfolding 1
apply simp
apply simp
apply (blast intro: ample_accept_subset ample_accept_stuttering)+
done
qed
end
text ‹Implementing the State›
type_synonym valuation_impl = "(ident,uint32) mapping"
definition "vi_α ≡ map_option Rep_uint32 ∘∘ Mapping.rep"
abbreviation "vi_rel ≡ br vi_α (λ_. True)"
abbreviation "val_rel ≡ br Rep_uint32 (λ_. True)"
lemma vi_rel_rew:
"(x = vi_α y) ⟷ (y,x)∈vi_rel"
"(vi_α y = x) ⟷ (y,x)∈vi_rel"
by (auto simp: br_def)
export_code Mapping.lookup Mapping.update Mapping.empty checking SML
lift_definition vi_empty :: "valuation_impl"
is "Map.empty::valuation" .
lemma [code]: "vi_empty = Mapping.empty" by transfer simp
lemma vi_empty_correct: "vi_α vi_empty = Map.empty"
unfolding vi_α_def
by transfer auto
lift_definition vi_lookup :: "valuation_impl ⇒ ident ⇀ uint32"
is "λvi::valuation. λx. vi x" .
lemma [code]: "vi_lookup = Mapping.lookup"
apply (intro ext)
unfolding vi_lookup_def Mapping.lookup_def map_fun_def[abs_def] o_def
id_apply option.map_comp Rep_uint32_inverse option.map_ident
by simp
lemma vi_lookup_correct: "vi_lookup v x = map_option Abs_uint32 (vi_α v x)"
unfolding vi_α_def
apply transfer
apply (simp add: option.map_comp o_def option.map_ident)
done
lift_definition vi_update :: "ident ⇒ uint32 ⇒ valuation_impl ⇒ valuation_impl"
is "λx v. λvi::valuation. vi(x↦v)" .
lemma [code]: "vi_update = Mapping.update"
by transfer simp
lemma vi_update_correct: "vi_α (vi_update k v m) = (vi_α m) (k↦Rep_uint32 v)"
unfolding vi_α_def
by transfer simp
export_code vi_lookup vi_update vi_empty checking SML
record local_state_impl =
variables :: valuation_impl
record global_state_impl =
variables :: valuation_impl
type_synonym focused_state_impl = "local_state_impl × global_state_impl"
type_synonym local_config_impl
= "(cmdc,local_state_impl) Gen_Scheduler.local_config"
type_synonym pid_global_config_impl
= "(cmdc,local_state_impl,global_state_impl) Pid_Scheduler.pid_global_config"
definition "local_state_rel ≡ {
(⦇ local_state_impl.variables = vi ⦈, ⦇ local_state.variables = v ⦈) | vi v.
v = vi_α vi
}"
definition "global_state_rel ≡ {
(⦇ global_state_impl.variables = vi ⦈, ⦇ global_state.variables = v ⦈) | vi v.
v = vi_α vi
}"
abbreviation "focused_state_rel ≡ local_state_rel ×⇩r global_state_rel"
definition "local_config_rel ≡ {
(⦇ local_config.command = ci, local_config.state=lsi ⦈,
⦇ local_config.command = c, local_config.state=ls ⦈) | ci c lsi ls.
(ci::cmdc,c)∈Id ∧ (lsi,ls)∈local_state_rel
}"
definition "global_config_rel ≡ {
(⦇ pid_global_config.processes = psi, pid_global_config.state = gsi ⦈,
⦇ pid_global_config.processes = ps, pid_global_config.state = gs ⦈) | psi ps gsi gs.
(psi,ps)∈⟨local_config_rel⟩list_rel ∧ (gsi,gs)∈global_state_rel
}"
definition "init_valuation_impl vd ≡ fold (λx v. vi_update x 0 v) vd (vi_empty)"
lemma init_valuation_impl:
"(init_valuation_impl, init_valuation) ∈ ⟨Id⟩list_rel → vi_rel"
proof -
{
fix vd m
have "m ++ init_valuation vd = fold (λx v. v(x↦0)) vd m"
apply (rule sym)
apply (induction vd arbitrary: m)
unfolding init_valuation_def[abs_def]
apply (auto intro!: ext simp: Map.map_add_def)
done
} note aux=this
have E1: "⋀vd. init_valuation vd = fold (λx v. v(x↦0)) vd Map.empty"
by (subst aux[symmetric]) simp
have E2: "⋀vdi vd. (vdi,vd)∈⟨Id⟩list_rel
⟹ (init_valuation_impl vdi, fold (λx v. v(x↦0)) vd Map.empty) ∈ vi_rel"
unfolding init_valuation_impl_def
apply parametricity
apply (auto simp: vi_update_correct vi_empty_correct br_def zero_uint32.rep_eq)
done
show ?thesis
apply (intro fun_relI)
apply (subst E1)
apply (rule E2)
by auto
qed
context cprog begin
definition init_pc_impl :: "proc_decl ⇒ local_config_impl" where
"init_pc_impl pd ≡ ⦇
local_config.command = comp.γ (proc_decl.body pd),
local_config.state = ⦇
local_state_impl.variables = init_valuation_impl (proc_decl.local_vars pd)
⦈
⦈"
lemma init_pc_impl: "(init_pc_impl, init_pc) ∈ Id → local_config_rel"
apply (rule fun_relI)
unfolding init_pc_impl_def init_pc_def local_config_rel_def local_state_rel_def
apply (simp del: pair_in_Id_conv, intro conjI)
apply simp
apply (simp only: vi_rel_rew)
apply (parametricity add: init_valuation_impl)
apply simp
done
definition pid_init_gc_impl :: "pid_global_config_impl" where
"pid_init_gc_impl ≡ ⦇
pid_global_config.processes = (map init_pc_impl (program.processes prog)),
pid_global_config.state = ⦇
global_state_impl.variables = init_valuation_impl (program.global_vars prog)
⦈
⦈"
lemma pid_init_gc_impl: "(pid_init_gc_impl, pid_init_gc) ∈ global_config_rel"
unfolding pid_init_gc_impl_def pid_init_gc_def global_config_rel_def global_state_rel_def
apply (simp del: pair_in_Id_conv, intro conjI)
apply (parametricity add: init_pc_impl)
apply simp
apply (simp only: vi_rel_rew)
apply (parametricity add: init_valuation_impl)
apply simp
done
end
lift_definition val_of_bool_impl :: "bool ⇒ uint32" is val_of_bool .
lemma [code]: "val_of_bool_impl b = (if b then 1 else 0)"
by transfer auto
lift_definition bool_of_val_impl :: "uint32 ⇒ bool" is bool_of_val .
lemma [code]: "bool_of_val_impl v = (v≠0)"
by transfer (auto simp: bool_of_val_def)
definition "set_of_rel R ≡ {(a,b) . R b a}"
definition "rel_of_set S ≡ λb a. (a,b)∈S"
lemma [simp]:
"(a,b)∈set_of_rel R ⟷ R b a"
"rel_of_set S b a ⟷ (a,b)∈S"
unfolding rel_of_set_def set_of_rel_def
by auto
lemma [simp]:
"set_of_rel (rel_of_set S) = S"
"rel_of_set (set_of_rel R) = R"
unfolding rel_of_set_def set_of_rel_def
by auto
lemma rel_fun_2set: "rel_fun A B = rel_of_set (set_of_rel A → set_of_rel B)"
unfolding rel_fun_def fun_rel_def
unfolding rel_of_set_def set_of_rel_def
by (auto)
lemma [simp]:
"set_of_rel cr_uint32 = val_rel"
"set_of_rel (=) = Id"
by (auto simp: br_def cr_uint32_def)
lemma bool_of_val_impl: "(bool_of_val_impl, bool_of_val) ∈ val_rel → bool_rel"
using bool_of_val_impl.transfer
by (simp add: rel_fun_2set)
lemma smod_by_div_abs: "a smod b = a - a sdiv b * b" for a b :: ‹'a::len word›
by (subst (2) sdiv_smod_id [of a b, symmetric]) simp
lift_definition sdiv_impl :: "uint32 ⇒ uint32 ⇒ uint32" is "(sdiv)" .
lift_definition smod_impl :: "uint32 ⇒ uint32 ⇒ uint32" is "(smod)" .
lemma [code]: "sdiv_impl x y = Abs_uint32' (Rep_uint32' x sdiv Rep_uint32' y)"
apply transfer
by simp
lemma [code]: "smod_impl a b = a - sdiv_impl a b * b"
by transfer (simp add: smod_by_div_abs)
context
includes bit_operations_syntax
begin
primrec eval_bin_op_impl_aux :: "bin_op ⇒ uint32 ⇒ uint32 ⇒ uint32" where
"eval_bin_op_impl_aux bo_plus v1 v2 = v1+v2"
| "eval_bin_op_impl_aux bo_minus v1 v2 = v1-v2"
| "eval_bin_op_impl_aux bo_mul v1 v2 = v1*v2"
| "eval_bin_op_impl_aux bo_div v1 v2 = sdiv_impl v1 v2"
| "eval_bin_op_impl_aux bo_mod v1 v2 = smod_impl v1 v2"
| "eval_bin_op_impl_aux bo_less v1 v2 = val_of_bool_impl (v1 < v2)"
| "eval_bin_op_impl_aux bo_less_eq v1 v2 = val_of_bool_impl (v1 ≤ v2)"
| "eval_bin_op_impl_aux bo_eq v1 v2 = val_of_bool_impl (v1 = v2)"
| "eval_bin_op_impl_aux bo_and v1 v2 = v1 AND v2"
| "eval_bin_op_impl_aux bo_or v1 v2 = v1 OR v2"
| "eval_bin_op_impl_aux bo_xor v1 v2 = v1 XOR v2"
end
lift_definition eval_bin_op_impl :: "bin_op ⇒ uint32 ⇒ uint32 ⇒ uint32"
is eval_bin_op .
lemma [code]: "eval_bin_op_impl bop v1 v2 = eval_bin_op_impl_aux bop v1 v2"
apply (cases bop)
apply (transfer; simp)+
done
primrec eval_un_op_impl_aux :: "un_op ⇒ uint32 ⇒ uint32" where
"eval_un_op_impl_aux uo_minus v = -v"
| "eval_un_op_impl_aux uo_not v = Bit_Operations.not v"
lift_definition eval_un_op_impl :: "un_op ⇒ uint32 ⇒ uint32"
is eval_un_op .
lemma [code]: "eval_un_op_impl uop v = eval_un_op_impl_aux uop v"
apply (cases uop)
apply simp_all
apply (transfer, simp)+
done
fun eval_exp_impl :: "exp ⇒ focused_state_impl ⇀ uint32" where
"eval_exp_impl (e_var x) (ls,gs) = do {
let lv = local_state_impl.variables ls;
let gv = global_state_impl.variables gs;
case vi_lookup lv x of
Some v ⇒ Some v
| None ⇒ (case vi_lookup gv x of
Some v ⇒ Some v
| None ⇒ None)
}"
| "eval_exp_impl (e_localvar x) (ls,gs) = vi_lookup (local_state_impl.variables ls) x"
| "eval_exp_impl (e_globalvar x) (ls,gs) = vi_lookup (global_state_impl.variables gs) x"
| "eval_exp_impl (e_const n) fs = do {
assert_option (n≥min_signed ∧ n≤max_signed);
Some (uint32_of_int n)
}"
| "eval_exp_impl (e_bin bop e1 e2) fs = do {
v1←eval_exp_impl e1 fs;
v2←eval_exp_impl e2 fs;
Some (eval_bin_op_impl bop v1 v2)
}"
| "eval_exp_impl (e_un uop e) fs = do {
v←eval_exp_impl e fs;
Some (eval_un_op_impl uop v)
}"
lemma map_option_bind: "map_option f (m⤜g) = m ⤜ (map_option f o g)"
by (auto split: Option.bind_split)
lemma val_option_rel_as_eq: "(a,b)∈⟨val_rel⟩option_rel ⟷ map_option Rep_uint32 a = b"
unfolding br_def
apply (cases a)
apply (cases b, simp_all)
apply (cases b, auto)
done
lemma eval_exp_impl: "(eval_exp_impl, eval_exp) ∈ Id → focused_state_rel → ⟨val_rel⟩option_rel"
proof -
{
fix e ls gs lsi gsi
assume "(lsi,ls)∈local_state_rel" "(gsi,gs)∈global_state_rel"
hence "map_option Rep_uint32 (eval_exp_impl e (lsi,gsi)) = eval_exp e (ls,gs)"
apply (induction e)
apply (auto
simp: local_state_rel_def global_state_rel_def br_def
simp: vi_lookup_correct vi_update_correct
simp: Abs_uint32_inverse[simplified] uint32_of_int.rep_eq signed_of_int_def
simp: option.map_comp option.map_ident o_def map_option_bind
simp: eval_bin_op_impl.rep_eq eval_un_op_impl.rep_eq
split: option.splits)
apply (drule sym)
apply (drule sym)
apply (simp split: Option.bind_split)
apply (drule sym)
apply (simp split: Option.bind_split)
done
} thus ?thesis
by (auto simp: val_option_rel_as_eq)
qed
text ‹Enabledness and effects of actions›
primrec la_en_impl :: "focused_state_impl ⇒ action ⇀ bool" where
"la_en_impl fs (AAssign e _ _) = do {
v ← eval_exp_impl e fs;
Some (bool_of_val_impl v)}"
| "la_en_impl fs (AAssign_local e _ _) = do {
v ← eval_exp_impl e fs;
Some (bool_of_val_impl v)}"
| "la_en_impl fs (AAssign_global e _ _) = do {
v ← eval_exp_impl e fs;
Some (bool_of_val_impl v)}"
| "la_en_impl fs (ATest e) = do {
v ← eval_exp_impl e fs;
Some (bool_of_val_impl v)}"
| "la_en_impl _ (ASkip) = Some True"
lemma param_rec_action[param]: "(rec_action, rec_action) ∈ (Id → Id → Id → A)
→ (Id → Id → Id → A)
→ (Id → Id → Id → A) → (Id → A) → A → Id → A"
apply (intro fun_relI)
subgoal for fi1 f1 fi2 f2 fi3 f3 fi4 f4 fi5 f5 ai a
apply simp
apply (induction a)
apply simp_all
apply (parametricity, simp_all?)+
done
done
lemma param_option_bind[param]:
"(Option.bind, Option.bind) ∈ ⟨A⟩option_rel → (A → ⟨B⟩option_rel) → ⟨B⟩option_rel"
unfolding Option.bind_def by parametricity
lemma la_en_impl: "(la_en_impl,la_en) ∈ focused_state_rel → Id → ⟨Id⟩option_rel"
unfolding la_en_impl_def la_en_def
by (parametricity add: eval_exp_impl bool_of_val_impl)
definition "la_en'_impl fs a ≡ case la_en_impl fs a of Some b ⇒ b | None ⇒ False"
lemma la_en'_impl: "(la_en'_impl,la_en') ∈ focused_state_rel → Id → bool_rel"
unfolding la_en'_impl_def[abs_def] la_en'_def[abs_def]
by (parametricity add: la_en_impl)
abbreviation "exists_var_impl v x ≡ vi_lookup v x ≠ None"
fun la_ex_impl :: "focused_state_impl ⇒ action ⇀ focused_state_impl" where
"la_ex_impl (ls,gs) (AAssign ge x e) = do {
v ← eval_exp_impl ge (ls,gs);
assert_option (bool_of_val_impl v);
v ← eval_exp_impl e (ls,gs);
if exists_var_impl (local_state_impl.variables ls) x then do {
let ls = local_state_impl.variables_update (vi_update x v) ls;
Some (ls,gs)
} else do {
assert_option (exists_var_impl (global_state_impl.variables gs) x);
let gs = global_state_impl.variables_update (vi_update x v) gs;
Some (ls,gs)
}
}"
| "la_ex_impl (ls,gs) (AAssign_local ge x e) = do {
v ← eval_exp_impl ge (ls,gs);
assert_option (bool_of_val_impl v);
v ← eval_exp_impl e (ls,gs);
assert_option (exists_var_impl (local_state_impl.variables ls) x);
let ls = local_state_impl.variables_update (vi_update x v) ls;
Some (ls,gs)
}"
| "la_ex_impl (ls,gs) (AAssign_global ge x e) = do {
v ← eval_exp_impl ge (ls,gs);
assert_option (bool_of_val_impl v);
v ← eval_exp_impl e (ls,gs);
assert_option (exists_var_impl (global_state_impl.variables gs) x);
let gs = global_state_impl.variables_update (vi_update x v) gs;
Some (ls,gs)
}"
| "la_ex_impl fs (ATest e) = do {
v ← eval_exp_impl e fs;
assert_option (bool_of_val_impl v);
Some fs
}"
| "la_ex_impl fs ASkip = Some fs"
lemma param_assert_option[param]:
"(assert_option, assert_option) ∈ bool_rel → ⟨unit_rel⟩option_rel"
unfolding assert_option_def by parametricity
lemma la_ex_impl: "(la_ex_impl, la_ex)
∈ focused_state_rel → Id → ⟨focused_state_rel⟩option_rel"
proof (intro fun_relI)
fix fsi fs and ai a :: action
assume "(fsi,fs)∈focused_state_rel" "(ai,a)∈Id"
thus "(la_ex_impl fsi ai, la_ex fs a)∈⟨focused_state_rel⟩option_rel"
apply (cases fs, cases fsi, clarsimp)
apply (cases a)
apply simp_all
apply (parametricity add: eval_exp_impl bool_of_val_impl)
apply (auto
simp: local_state_rel_def global_state_rel_def
simp: vi_lookup_correct vi_update_correct
simp: br_def
intro: domI) [7]
apply (parametricity add: eval_exp_impl bool_of_val_impl)
apply (auto
simp: local_state_rel_def global_state_rel_def
simp: vi_lookup_correct vi_update_correct
br_def intro: domI) [9]
apply (parametricity add: eval_exp_impl bool_of_val_impl)
apply (auto
simp: local_state_rel_def global_state_rel_def
simp: vi_lookup_correct vi_update_correct
br_def intro: domI) [4]
apply (parametricity add: eval_exp_impl bool_of_val_impl)
apply simp
done
qed
definition "la_ex'_impl fs a ≡ case la_ex_impl fs a of Some fs' ⇒ fs' | None ⇒ fs"
lemma la_ex'_impl: "(la_ex'_impl,la_ex') ∈ focused_state_rel → Id → focused_state_rel"
unfolding la_ex'_impl_def[abs_def] la_ex'_def[abs_def]
by (parametricity add: la_ex_impl)
lemma param_collecti_index: "(collecti_index, collecti_index) ∈
(nat_rel → B → bool_rel ×⇩r ⟨Id⟩set_rel) → ⟨B⟩list_rel → ⟨nat_rel ×⇩r Id⟩set_rel"
unfolding collecti_index'_def
apply parametricity
apply auto
done
export_code la_ex_impl la_en_impl checking SML
context visible_prog
begin
definition "ga_gample_mi3 mem sticky_E (gc::pid_global_config_impl) = (
let
lcs = pid_global_config.processes gc;
gs = pid_global_config.state gc
in
collecti_index (λ_ lc. let
c = local_config.command lc;
ls = local_config.state lc;
as = set (comp.succ_impl c);
s={(a,c')∈as. la_en'_impl (ls,gs) a};
ample =
s≠{}
∧ (∀(a,_)∈as. read_globals a = {} ∧ write_globals a = {})
∧ (∀(a,c')∈s. ¬ mem (c,c') sticky_E)
in
(ample,{c}×s)
) lcs
)"
lemma ga_gample_mi3_refine:
"(ga_gample_mi3, ga_gample_mi2)∈
Id → Id → global_config_rel → ⟨nat_rel ×⇩r Id⟩set_rel"
proof -
have [param]: "(comp.succ_impl,comp.succ_impl)∈Id→⟨Id×⇩rId⟩list_rel"
by simp
from la_en'_impl have aux1: "⋀fsi fs a. (fsi,fs)∈focused_state_rel ⟹
la_en'_impl fsi a = la_en' fs a"
apply (rule_tac IdD)
apply parametricity
by auto
show ?thesis
using [[goals_limit=1]]
apply (intro fun_relI)
unfolding ga_gample_mi3_def ga_gample_mi2_def
apply (parametricity add: param_collecti_index la_en'_impl)
apply (auto simp add: global_config_rel_def local_config_rel_def) []
apply (auto simp add: global_config_rel_def local_config_rel_def) []
apply (auto simp add: global_config_rel_def local_config_rel_def) []
apply (auto simp add: global_config_rel_def local_config_rel_def) []
apply simp
using aux1
apply (auto simp add: global_config_rel_def local_config_rel_def) []
apply simp_all
done
qed
definition (in cprog) "is_vis_edge is_vis_var ≡ λ(c,c').
∃(a,cc')∈set (comp.succ_impl c). c'=cc' ∧ (∃v∈write_globals a. is_vis_var v)"
lemma is_vis_edge_correct: "is_vis_edge is_vis_var = (λx. x∈vis_edges)"
unfolding is_vis_edge_def vis_edges_def
by (auto intro!: ext simp: comp.astep_impl_def)
definition "cr_ample_impl3 ≡
let sticky = find_fas_init_code (=) bounded_hashcode_nat
(def_hashmap_size TYPE(nat)) cfgc_G_impl (λx. x ∈ vis_edges)
in stutter_extend_en (ga_gample_mi3 (λx f. f x) sticky)"
lemma cr_ample_impl3_refine: "(cr_ample_impl3, cr_ample_impl2)
∈ global_config_rel → ⟨⟨nat_rel×⇩rId⟩option_rel⟩set_rel"
proof -
have [param]: "⋀R S. S=Id ⟹
(stutter_extend_en, stutter_extend_en)
∈ (R → ⟨S⟩set_rel) → R → ⟨⟨S⟩option_rel⟩set_rel"
apply (simp only: )
by (rule stutter_extend_en_refine)
show ?thesis
unfolding cr_ample_impl3_def cr_ample_impl2_def is_vis_edge_correct
apply (parametricity add: stutter_extend_en_refine ga_gample_mi3_refine)
apply (rule IdI)
by auto
qed
definition (in -) ga_gex_impl
:: "global_action ⇒ pid_global_config_impl ⇒ pid_global_config_impl"
where
"ga_gex_impl ga gc ≡ let
(pid,c,a,c') = ga;
fs = fs_of_pid gc pid;
(ls',gs') = la_ex'_impl fs a;
gc' = ⦇
pid_global_config.processes = (pid_global_config.processes gc)
[pid :=
⦇ local_config.command = c', local_config.state = ls'⦈
],
pid_global_config.state = gs'⦈
in
gc'"
lemma lc_of_pid_refine:
assumes V: "pid_valid gc pid"
assumes [param]: "(pidi,pid)∈nat_rel"
assumes GCI: "(gci,gc)∈global_config_rel"
shows "(lc_of_pid gci pidi, lc_of_pid gc pid)∈local_config_rel"
apply parametricity
apply fact
using GCI by (auto simp: global_config_rel_def)
lemma ls_of_pid_refine:
assumes "pid_valid gc pid"
assumes "(pidi,pid)∈nat_rel"
assumes "(gci,gc)∈global_config_rel"
shows "(ls_of_pid gci pidi, ls_of_pid gc pid)∈local_state_rel"
using lc_of_pid_refine[OF assms] unfolding local_config_rel_def by auto
lemma ga_gex_impl:
assumes V: "pid_valid gc pid"
assumes [param]: "(pidi,pid)∈Id" "(ci,c)∈Id"
"(ai,a)∈Id" and CI'I: "(ci',c')∈Id" and GCI[param]: "(gci,gc)∈global_config_rel"
shows "(ga_gex_impl (pidi,ci,ai,ci') gci, ga_gex (pid,c,a,c') gc) ∈ global_config_rel"
unfolding ga_gex_impl_def[abs_def] ga_gex_def[abs_def]
apply simp
apply (parametricity add: la_ex'_impl ls_of_pid_refine[OF V])
using GCI CI'I
apply (auto simp: global_config_rel_def local_config_rel_def) []
apply parametricity
apply auto []
using GCI
apply (auto simp: global_config_rel_def) []
done
definition (in -) "ga_ex_impl ≡ stutter_extend_ex ga_gex_impl"
fun ga_valid where
"ga_valid gc None = True"
| "ga_valid gc (Some (pid,c,a,c')) = pid_valid gc pid"
lemma ga_ex_impl:
assumes V: "ga_valid gc ga"
assumes P: "(gai,ga)∈Id" "(gci,gc)∈global_config_rel"
shows "(ga_ex_impl gai gci, ga_ex ga gc) ∈ global_config_rel"
using assms
apply (cases "(gc,ga)" rule: ga_valid.cases)
using P
apply (simp add: ga_ex_impl_def)
apply (simp add: ga_ex_impl_def ga_ex_def)
apply (parametricity add: ga_gex_impl)
by auto
definition "ample_step_impl3 ≡ rel_of_enex (cr_ample_impl3,ga_ex_impl)"
definition (in -) pid_interp_gc_impl
:: "(ident ⇒ bool) ⇒ pid_global_config_impl ⇒ exp set"
where
"pid_interp_gc_impl is_vis_var gci ≡ sm_props (
vi_α (global_state_impl.variables (pid_global_config.state gci)) |` Collect is_vis_var
)"
lemma pid_interp_gc_impl:
"(pid_interp_gc_impl is_vis_var, pid_interp_gc) ∈ global_config_rel → Id"
apply rule
unfolding pid_interp_gc_impl_def pid_interp_gc_def
apply (auto simp: global_config_rel_def global_state_rel_def
interp_gs_def sm_props_def br_def)
done
lemma cr_ample_impl3_sim_aux:
assumes GCI: "(gci, gc) ∈ global_config_rel"
assumes GA: "ga ∈ cr_ample_impl3 gci"
shows "∃gc'. ga∈cr_ample_impl2 gc
∧ gc'=ga_ex ga gc
∧ (ga_ex_impl ga gci, gc')∈global_config_rel"
proof (clarsimp, safe)
show G1: "ga∈cr_ample_impl2 gc"
using cr_ample_impl3_refine[param_fo, OF GCI] GA by auto
{
fix mem sticky_E gc pid c
assume "(pid,c)∈ga_gample_m mem sticky_E gc"
hence "pid_valid gc pid"
unfolding ga_gample_m_def
apply (auto split: option.splits)
apply (auto simp: ga_gen_def) []
apply (auto dest: find_min_idx_f_SomeD)
done
} note aux=this
from G1 have "ga_valid gc ga"
unfolding cr_ample_impl2_def stutter_extend_en_def
apply (simp split: if_split_asm)
unfolding ga_gample_mi2_impl[symmetric]
apply (auto dest: aux)
done
thus "(ga_ex_impl ga gci, ga_ex ga gc)∈global_config_rel"
by (parametricity add: ga_ex_impl GCI IdI[of ga])
qed
lemma cr_ample_impl3_sim_aux2:
assumes GCI: "(gci, gc) ∈ global_config_rel"
assumes GA: "ga ∈ cr_ample_impl2 gc"
shows "ga∈cr_ample_impl3 gci
∧ (ga_ex_impl ga gci, ga_ex ga gc) ∈ global_config_rel"
proof
show G1: "ga∈cr_ample_impl3 gci"
using cr_ample_impl3_refine[param_fo, OF GCI] GA by auto
from cr_ample_impl3_sim_aux[OF GCI G1] show
"(ga_ex_impl ga gci, ga_ex ga gc) ∈ global_config_rel"
by auto
qed
sublocale impl3: sa "⦇ g_V = UNIV, g_E = ample_step_impl3, g_V0 = {pid_init_gc_impl},
sa_L = pid_interp_gc_impl is_vis_var ⦈" by unfold_locales auto
sublocale impl3_sim: lbisimulation
global_config_rel
"⦇ g_V = UNIV, g_E = ample_step_impl3, g_V0 = {pid_init_gc_impl},
sa_L = pid_interp_gc_impl is_vis_var ⦈"
"⦇ g_V = UNIV, g_E = ample_step_impl2, g_V0 = {pid_init_gc},
sa_L = pid_interp_gc ⦈"
apply unfold_locales
apply simp
apply simp
apply simp
using pid_init_gc_impl
apply (auto dest: fun_relD) []
unfolding ample_step_impl2_def ample_step_impl3_def
apply (auto dest: cr_ample_impl3_sim_aux) []
using pid_interp_gc_impl
apply (auto dest: fun_relD) []
apply simp
using pid_init_gc_impl
apply (auto dest: fun_relD) []
defer
using pid_interp_gc_impl
apply (auto dest: fun_relD) []
apply auto
apply (auto dest: cr_ample_impl3_sim_aux2) []
done
text ‹Correctness of impl3›
lemma impl3_accept_subset: "impl3.accept w ⟹ lv.sa.accept w"
using impl3_sim.accept_bisim cr_ample_impl2_reduction hl_reduction.ample_accept_subset
by simp
lemma impl3_accept_stuttering: "lv.sa.accept w ⟹ ∃w'. w≈w' ∧ impl3.accept w'"
using impl3_sim.accept_bisim cr_ample_impl2_reduction hl_reduction.ample_accept_stuttering
by simp
text ‹Next, we go from sets of actions to lists of actions›
definition (in cprog) "ga_gample_mil4 mem sticky_Ei (gc::pid_global_config_impl) = (
let
lcs = pid_global_config.processes gc;
gs = pid_global_config.state gc
in
collecti_index_list (λ_ lc. let
c = local_config.command lc;
ls = local_config.state lc;
as = comp.succ_impl c;
s = filter (la_en'_impl (ls,gs) o fst) as;
ample = s≠[]
∧ (∀(a,_)∈set as. read_globals a = {} ∧ write_globals a = {})
∧ (∀(a,c')∈set s. ¬mem (c,c') sticky_Ei)
in
(ample,map (Pair c) s)
) lcs
)"
lemma ga_gample_mil4_refine:
"(ga_gample_mil4, ga_gample_mi3)
∈ (Id×⇩rId → Id → bool_rel) → Id → Id → ⟨nat_rel ×⇩r Id⟩list_set_rel"
apply (intro fun_relI)
unfolding ga_gample_mil4_def ga_gample_mi3_def
apply (parametricity)
apply simp
apply (rule IdI)
apply simp
apply (rule IdI)
apply (intro fun_relI)
apply (rule collecti_index_list_refine[param_fo])
apply (intro fun_relI)
apply (simp add: list_set_rel_def br_def distinct_map
comp.succ_impl_invar)
apply (auto simp: filter_empty_conv)
apply force
done
definition (in cprog) "cr_ample_impl4 is_vis_var ≡
let sticky = find_fas_init_code (=) bounded_hashcode_nat
(def_hashmap_size TYPE(nat)) cfgc_G_impl (is_vis_edge is_vis_var)
in stutter_extend_en_list (ga_gample_mil4 (λx f. f x) sticky)"
lemma cr_ample_impl4_refine:
"(cr_ample_impl4 is_vis_var, cr_ample_impl3)∈Id → ⟨⟨nat_rel ×⇩r Id⟩option_rel⟩list_set_rel"
unfolding cr_ample_impl4_def cr_ample_impl3_def
apply (parametricity add: stutter_extend_en_list.refine ga_gample_mil4_refine)
apply (simp_all add: is_vis_edge_correct)
done
text ‹Finally, we combine the ample-implementation and the executable implementation
to get a step function›
definition (in cprog) "ample_step_impl4 is_vis_var ≡
rel_of_enex_list (cr_ample_impl4 is_vis_var,ga_ex_impl)"
lemma ample_step_impl4:
"(ample_step_impl4 is_vis_var, ample_step_impl3) ∈ ⟨Id ×⇩r Id⟩ set_rel"
unfolding ample_step_impl4_def ample_step_impl3_def rel_of_pred_def
apply (parametricity add: rel_of_enex_list_refine cr_ample_impl4_refine[simplified])
by auto
sublocale impl4: sa "⦇ g_V = UNIV, g_E = ample_step_impl4 is_vis_var,
g_V0 = {pid_init_gc_impl}, sa_L = pid_interp_gc_impl is_vis_var ⦈" by unfold_locales auto
lemma impl4_accept_subset: "impl4.accept w ⟹ lv.sa.accept w"
using impl3_accept_subset ample_step_impl4
by simp
lemma impl4_accept_stuttering: "lv.sa.accept w ⟹ ∃w'. w≈w' ∧ impl4.accept w'"
using impl3_accept_stuttering ample_step_impl4
by simp
lemma (in -) pred_of_succ_of_enex_list:
fixes enex :: "('c ⇒ 'a list) × ('a ⇒ 'c ⇒ 'c)"
shows "pred_of_succ (set o succ_of_enex_list enex) = pred_of_enex_list enex"
proof -
{ fix x and l
have "glist_member (=) x l ⟷ x∈set l"
by (induction l) auto
} note [simp] = this
{
fix l :: "'a list" and g and l0
have "set (foldli l (λ_. True) (λx. glist_insert (=) (g x)) l0) = set l0 ∪ g`set l"
by (induction l arbitrary: l0) (auto simp: glist_insert_def)
} note [simp] = this
{
fix l::"'a list" and P i
have "foldli l Not (λx _. P x) i ⟷ i ∨ (∃x∈set l. P x)"
by (induction l arbitrary: i) auto
} note [simp] = this
show ?thesis
unfolding succ_of_enex_list_def[abs_def] pred_of_enex_list_def[abs_def]
by (auto simp: pred_of_succ_def gen_image_def gen_bex_def intro!: ext)
qed
lemma (in -) rel_of_succ_of_enex_list:
fixes enex :: "('c ⇒ 'a list) × ('a ⇒ 'c ⇒ 'c)"
shows "rel_of_succ (set o succ_of_enex_list enex) = rel_of_enex_list enex"
unfolding rel_of_enex_list_def
unfolding pred_of_succ_of_enex_list[symmetric]
by simp
definition (in cprog) "impl4_succ is_vis_var
≡ succ_of_enex_list (cr_ample_impl4 is_vis_var,ga_ex_impl)"
lemma impl4_succ_pred:
"rel_of_succ (set o (impl4_succ is_vis_var)) = ample_step_impl4 is_vis_var"
unfolding impl4_succ_def ample_step_impl4_def
by (simp add: rel_of_succ_of_enex_list)
end
export_code ga_ex_impl checking SML
definition "ccfg_E_succ_impl mst ≡ remdups o map snd o ccfg_succ_impl mst"
lemma (in cprog) ccfg_E_succ_impl: "ccfg_E_succ_impl (comp_info_of prog) = cfgc_E_succ"
apply (intro ext)
unfolding ccfg_E_succ_impl_def cfgc_E_succ_def
by (simp add: ccfg_succ_impl)
definition init_pc_impl_impl :: "comp_info ⇒ proc_decl ⇒ local_config_impl" where
"init_pc_impl_impl mst pd ≡ ⦇
local_config.command = comp_γ_impl mst (proc_decl.body pd),
local_config.state = ⦇
local_state_impl.variables = init_valuation_impl (proc_decl.local_vars pd)
⦈
⦈"
lemma (in cprog) init_pc_impl_impl: "init_pc_impl_impl (comp_info_of prog) = init_pc_impl"
apply (intro ext)
unfolding init_pc_impl_impl_def init_pc_impl_def
by (simp add: comp_γ_impl)
definition pid_init_gc_impl_impl :: "program ⇒ comp_info ⇒ pid_global_config_impl" where
"pid_init_gc_impl_impl prog mst ≡ ⦇
pid_global_config.processes = (map (init_pc_impl_impl mst) (program.processes prog)),
pid_global_config.state = ⦇
global_state_impl.variables = init_valuation_impl (program.global_vars prog)
⦈
⦈"
lemma (in cprog) pid_init_gc_impl_impl:
"pid_init_gc_impl_impl prog (comp_info_of prog) = pid_init_gc_impl"
unfolding pid_init_gc_impl_impl_def pid_init_gc_impl_def
by (simp add: init_pc_impl_impl)
definition "ccfg_V0_impl prog mst ≡ map (comp_γ_impl mst) (cfg_V0_list prog)"
lemma (in cprog) ccfg_V0_impl: "ccfg_V0_impl prog (comp_info_of prog) = cfgc_V0_list"
unfolding ccfg_V0_impl_def cfgc_V0_list_def
by (simp add: comp_γ_impl)
definition "ccfg_G_impl_impl prog mst ≡
⦇ gi_V = λ _. True, gi_E = ccfg_E_succ_impl mst, gi_V0 = ccfg_V0_impl prog mst ⦈"
lemma (in cprog) ccfg_G_impl_impl: "ccfg_G_impl_impl prog (comp_info_of prog) = cfgc_G_impl"
unfolding ccfg_G_impl_impl_def cfgc_G_impl_def
unfolding ccfg_E_succ_impl ccfg_V0_impl
by rule
definition "is_vis_edge_impl mst is_vis_var ≡ λ(c,c').
∃(a,cc')∈set (ccfg_succ_impl mst c). c'=cc' ∧ (∃v∈write_globals a. is_vis_var v)"
lemma (in cprog) is_vis_edge_impl: "is_vis_edge_impl (comp_info_of prog) = is_vis_edge"
apply (intro ext)
unfolding is_vis_edge_impl_def is_vis_edge_def
by (simp add: ccfg_succ_impl)
definition "ga_gample_mil4_impl mst mem sticky_Ei (gc::pid_global_config_impl) = (
let
lcs = pid_global_config.processes gc;
gs = pid_global_config.state gc
in
collecti_index_list (λ_ lc. let
c = local_config.command lc;
ls = local_config.state lc;
as = ccfg_succ_impl mst c;
s = filter (la_en'_impl (ls,gs) o fst) as;
ample = s≠[]
∧ (∀(a,_)∈set as. read_globals a = {} ∧ write_globals a = {})
∧ (∀(a,c')∈set s. ¬mem (c,c') sticky_Ei)
in
(ample,map (Pair c) s)
) lcs
)"
lemma (in cprog) ga_gample_mil4_impl: "ga_gample_mil4_impl (comp_info_of prog) = ga_gample_mil4"
apply (intro ext)
unfolding ga_gample_mil4_impl_def ga_gample_mil4_def
by (simp add: ccfg_succ_impl)
definition "cr_ample_impl4_impl prog mst is_vis_var ≡
let sticky = find_fas_init_code (=) bounded_hashcode_nat
(def_hashmap_size TYPE(nat)) (ccfg_G_impl_impl prog mst)
(is_vis_edge_impl mst is_vis_var)
in stutter_extend_en_list (ga_gample_mil4_impl mst (λx f. f x) sticky)"
lemma (in cprog) cr_ample_impl4_impl: "cr_ample_impl4_impl prog (comp_info_of prog) = cr_ample_impl4"
apply (intro ext)
unfolding cr_ample_impl4_impl_def cr_ample_impl4_def
by (simp add: ga_gample_mil4_impl ccfg_G_impl_impl is_vis_edge_impl)
definition "impl4_succ_impl prog mst is_vis_var
≡ succ_of_enex_list (cr_ample_impl4_impl prog mst is_vis_var,ga_ex_impl)"
lemma (in cprog) impl4_succ_impl:
"impl4_succ_impl prog (comp_info_of prog) = impl4_succ"
apply (intro ext)
unfolding impl4_succ_impl_def impl4_succ_def
by (simp add: cr_ample_impl4_impl)
definition "ample_step_impl4_impl prog mst is_vis_var
≡ rel_of_enex_list (cr_ample_impl4_impl prog mst is_vis_var,ga_ex_impl)"
lemma (in cprog) ample_step_impl4_impl:
"ample_step_impl4_impl prog (comp_info_of prog) = ample_step_impl4"
apply (intro ext)
unfolding ample_step_impl4_impl_def ample_step_impl4_def
by (simp add: cr_ample_impl4_impl)
export_code impl4_succ_impl pid_init_gc_impl_impl comp_info_of checking SML
end