Theory ClientImpl
theory ClientImpl imports AllocBase Guar begin
abbreviation "ask ≡ Var(Nil)"
abbreviation "giv ≡ Var([0])"
abbreviation "rel ≡ Var([1])"
abbreviation "tok ≡ Var([2])"
axiomatization where
type_assumes:
"type_of(ask) = list(tokbag) ∧ type_of(giv) = list(tokbag) ∧
type_of(rel) = list(tokbag) ∧ type_of(tok) = nat" and
default_val_assumes:
"default_val(ask) = Nil ∧ default_val(giv) = Nil ∧
default_val(rel) = Nil ∧ default_val(tok) = 0"
definition
"client_rel_act ≡
{⟨s,t⟩ ∈ state*state.
∃nrel ∈ nat. nrel = length(s`rel) ∧
t = s(rel:=(s`rel)@[nth(nrel, s`giv)]) ∧
nrel < length(s`giv) ∧
nth(nrel, s`ask) ≤ nth(nrel, s`giv)}"
definition
"client_tok_act ≡ {⟨s,t⟩ ∈ state*state. t=s |
t = s(tok:=succ(s`tok mod NbT))}"
definition
"client_ask_act ≡ {⟨s,t⟩ ∈ state*state. t=s | (t=s(ask:=s`ask@[s`tok]))}"
definition
"client_prog ≡
mk_program({s ∈ state. s`tok ≤ NbT ∧ s`giv = Nil ∧
s`ask = Nil ∧ s`rel = Nil},
{client_rel_act, client_tok_act, client_ask_act},
⋃G ∈ preserves(lift(rel)) Int
preserves(lift(ask)) Int
preserves(lift(tok)). Acts(G))"
declare type_assumes [simp] default_val_assumes [simp]
lemma ask_value_type [simp,TC]: "s ∈ state ⟹ s`ask ∈ list(nat)"
unfolding state_def
apply (drule_tac a = ask in apply_type, auto)
done
lemma giv_value_type [simp,TC]: "s ∈ state ⟹ s`giv ∈ list(nat)"
unfolding state_def
apply (drule_tac a = giv in apply_type, auto)
done
lemma rel_value_type [simp,TC]: "s ∈ state ⟹ s`rel ∈ list(nat)"
unfolding state_def
apply (drule_tac a = rel in apply_type, auto)
done
lemma tok_value_type [simp,TC]: "s ∈ state ⟹ s`tok ∈ nat"
unfolding state_def
apply (drule_tac a = tok in apply_type, auto)
done
lemma client_type [simp,TC]: "client_prog ∈ program"
unfolding client_prog_def
apply (simp (no_asm))
done
declare client_prog_def [THEN def_prg_Init, simp]
declare client_prog_def [THEN def_prg_AllowedActs, simp]
declare client_prog_def [program]
declare client_rel_act_def [THEN def_act_simp, simp]
declare client_tok_act_def [THEN def_act_simp, simp]
declare client_ask_act_def [THEN def_act_simp, simp]
lemma client_prog_ok_iff:
"∀G ∈ program. (client_prog ok G) ⟷
(G ∈ preserves(lift(rel)) ∧ G ∈ preserves(lift(ask)) ∧
G ∈ preserves(lift(tok)) ∧ client_prog ∈ Allowed(G))"
by (auto simp add: ok_iff_Allowed client_prog_def [THEN def_prg_Allowed])
lemma client_prog_preserves:
"client_prog:(⋂x ∈ var-{ask, rel, tok}. preserves(lift(x)))"
apply (rule Inter_var_DiffI, force)
apply (rule ballI)
apply (rule preservesI, safety, auto)
done
lemma preserves_lift_imp_stable:
"G ∈ preserves(lift(ff)) ⟹ G ∈ stable({s ∈ state. P(s`ff)})"
apply (drule preserves_imp_stable)
apply (simp add: lift_def)
done
lemma preserves_imp_prefix:
"G ∈ preserves(lift(ff))
⟹ G ∈ stable({s ∈ state. ⟨k, s`ff⟩ ∈ prefix(nat)})"
by (erule preserves_lift_imp_stable)
lemma client_prog_Increasing_ask_rel:
"client_prog: program guarantees Incr(lift(ask)) ∩ Incr(lift(rel))"
unfolding guar_def
apply (auto intro!: increasing_imp_Increasing
simp add: client_prog_ok_iff Increasing.increasing_def preserves_imp_prefix)
apply (safety, force, force)+
done
declare nth_append [simp] append_one_prefix [simp]
lemma NbT_pos2: "0<NbT"
apply (cut_tac NbT_pos)
apply (rule Ord_0_lt, auto)
done
lemma ask_Bounded_lemma:
"⟦client_prog ok G; G ∈ program⟧
⟹ client_prog ⊔ G ∈
Always({s ∈ state. s`tok ≤ NbT} ∩
{s ∈ state. ∀elt ∈ set_of_list(s`ask). elt ≤ NbT})"
apply (rotate_tac -1)
apply (auto simp add: client_prog_ok_iff)
apply (rule invariantI [THEN stable_Join_Always2], force)
prefer 2
apply (fast intro: stable_Int preserves_lift_imp_stable, safety)
apply (auto dest: ActsD)
apply (cut_tac NbT_pos)
apply (rule NbT_pos2 [THEN mod_less_divisor])
apply (auto dest: ActsD preserves_imp_eq simp add: set_of_list_append)
done
lemma client_prog_ask_Bounded:
"client_prog ∈ program guarantees
Always({s ∈ state. ∀elt ∈ set_of_list(s`ask). elt ≤ NbT})"
apply (rule guaranteesI)
apply (erule ask_Bounded_lemma [THEN Always_weaken], auto)
done
lemma client_prog_stable_rel_le_giv:
"client_prog ∈ stable({s ∈ state. <s`rel, s`giv> ∈ prefix(nat)})"
by (safety, auto)
lemma client_prog_Join_Stable_rel_le_giv:
"⟦client_prog ⊔ G ∈ Incr(lift(giv)); G ∈ preserves(lift(rel))⟧
⟹ client_prog ⊔ G ∈ Stable({s ∈ state. <s`rel, s`giv> ∈ prefix(nat)})"
apply (rule client_prog_stable_rel_le_giv [THEN Increasing_preserves_Stable])
apply (auto simp add: lift_def)
done
lemma client_prog_Join_Always_rel_le_giv:
"⟦client_prog ⊔ G ∈ Incr(lift(giv)); G ∈ preserves(lift(rel))⟧
⟹ client_prog ⊔ G ∈ Always({s ∈ state. <s`rel, s`giv> ∈ prefix(nat)})"
by (force intro!: AlwaysI client_prog_Join_Stable_rel_le_giv)
lemma def_act_eq:
"A ≡ {⟨s, t⟩ ∈ state*state. P(s, t)} ⟹ A={⟨s, t⟩ ∈ state*state. P(s, t)}"
by auto
lemma act_subset: "A={⟨s,t⟩ ∈ state*state. P(s, t)} ⟹ A<=state*state"
by auto
lemma transient_lemma:
"client_prog ∈
transient({s ∈ state. s`rel = k ∧ ⟨k, h⟩ ∈ strict_prefix(nat)
∧ <h, s`giv> ∈ prefix(nat) ∧ h pfixGe s`ask})"
apply (rule_tac act = client_rel_act in transientI)
apply (simp (no_asm) add: client_prog_def [THEN def_prg_Acts])
apply (simp (no_asm) add: client_rel_act_def [THEN def_act_eq, THEN act_subset])
apply (auto simp add: client_prog_def [THEN def_prg_Acts] domain_def)
apply (rule ReplaceI)
apply (rule_tac x = "x (rel:= x`rel @ [nth (length (x`rel), x`giv) ]) " in exI)
apply (auto intro!: state_update_type app_type length_type nth_type, auto)
apply (blast intro: lt_trans2 prefix_length_le strict_prefix_length_lt)
apply (blast intro: lt_trans2 prefix_length_le strict_prefix_length_lt)
apply (simp (no_asm_use) add: gen_prefix_iff_nth)
apply (subgoal_tac "h ∈ list(nat)")
apply (simp_all (no_asm_simp) add: prefix_type [THEN subsetD, THEN SigmaD1])
apply (auto simp add: prefix_def Ge_def)
apply (drule strict_prefix_length_lt)
apply (drule_tac x = "length (x`rel) " in spec)
apply auto
apply (simp (no_asm_use) add: gen_prefix_iff_nth)
apply (auto simp add: id_def lam_def)
done
lemma strict_prefix_is_prefix:
"⟨xs, ys⟩ ∈ strict_prefix(A) ⟷ ⟨xs, ys⟩ ∈ prefix(A) ∧ xs≠ys"
unfolding strict_prefix_def id_def lam_def
apply (auto dest: prefix_type [THEN subsetD])
done
lemma induct_lemma:
"⟦client_prog ⊔ G ∈ Incr(lift(giv)); client_prog ok G; G ∈ program⟧
⟹ client_prog ⊔ G ∈
{s ∈ state. s`rel = k ∧ ⟨k,h⟩ ∈ strict_prefix(nat)
∧ <h, s`giv> ∈ prefix(nat) ∧ h pfixGe s`ask}
⟼w {s ∈ state. <k, s`rel> ∈ strict_prefix(nat)
∧ <s`rel, s`giv> ∈ prefix(nat) ∧
<h, s`giv> ∈ prefix(nat) ∧
h pfixGe s`ask}"
apply (rule single_LeadsTo_I)
prefer 2 apply simp
apply (frule client_prog_Increasing_ask_rel [THEN guaranteesD])
apply (rotate_tac [3] 2)
apply (auto simp add: client_prog_ok_iff)
apply (rule transient_lemma [THEN Join_transient_I1, THEN transient_imp_leadsTo, THEN leadsTo_imp_LeadsTo, THEN PSP_Stable, THEN LeadsTo_weaken])
apply (rule Stable_Int [THEN Stable_Int, THEN Stable_Int])
apply (erule_tac f = "lift (giv) " and a = "s`giv" in Increasing_imp_Stable)
apply (simp (no_asm_simp))
apply (erule_tac f = "lift (ask) " and a = "s`ask" in Increasing_imp_Stable)
apply (simp (no_asm_simp))
apply (erule_tac f = "lift (rel) " and a = "s`rel" in Increasing_imp_Stable)
apply (simp (no_asm_simp))
apply (erule client_prog_Join_Stable_rel_le_giv, blast, simp_all)
prefer 2
apply (blast intro: sym strict_prefix_is_prefix [THEN iffD2] prefix_trans prefix_imp_pfixGe pfixGe_trans)
apply (auto intro: strict_prefix_is_prefix [THEN iffD1, THEN conjunct1]
prefix_trans)
done
lemma rel_progress_lemma:
"⟦client_prog ⊔ G ∈ Incr(lift(giv)); client_prog ok G; G ∈ program⟧
⟹ client_prog ⊔ G ∈
{s ∈ state. <s`rel, h> ∈ strict_prefix(nat)
∧ <h, s`giv> ∈ prefix(nat) ∧ h pfixGe s`ask}
⟼w {s ∈ state. <h, s`rel> ∈ prefix(nat)}"
apply (rule_tac f = "λx ∈ state. length(h) #- length(x`rel)"
in LessThan_induct)
apply (auto simp add: vimage_def)
prefer 2 apply (force simp add: lam_def)
apply (rule single_LeadsTo_I)
prefer 2 apply simp
apply (subgoal_tac "h ∈ list(nat)")
prefer 2 apply (blast dest: prefix_type [THEN subsetD])
apply (rule induct_lemma [THEN LeadsTo_weaken])
apply (simp add: length_type lam_def)
apply (auto intro: strict_prefix_is_prefix [THEN iffD2]
dest: common_prefix_linear prefix_type [THEN subsetD])
apply (erule swap)
apply (rule imageI)
apply (force dest!: simp add: lam_def)
apply (simp add: length_type lam_def, clarify)
apply (drule strict_prefix_length_lt)+
apply (drule less_imp_succ_add, simp)+
apply clarify
apply simp
apply (erule diff_le_self [THEN ltD])
done
lemma progress_lemma:
"⟦client_prog ⊔ G ∈ Incr(lift(giv)); client_prog ok G; G ∈ program⟧
⟹ client_prog ⊔ G
∈ {s ∈ state. <h, s`giv> ∈ prefix(nat) ∧ h pfixGe s`ask}
⟼w {s ∈ state. <h, s`rel> ∈ prefix(nat)}"
apply (rule client_prog_Join_Always_rel_le_giv [THEN Always_LeadsToI],
assumption)
apply (force simp add: client_prog_ok_iff)
apply (rule LeadsTo_weaken_L)
apply (rule LeadsTo_Un [OF rel_progress_lemma
subset_refl [THEN subset_imp_LeadsTo]])
apply (auto intro: strict_prefix_is_prefix [THEN iffD2]
dest: common_prefix_linear prefix_type [THEN subsetD])
done
lemma client_prog_progress:
"client_prog ∈ Incr(lift(giv)) guarantees
(⋂h ∈ list(nat). {s ∈ state. <h, s`giv> ∈ prefix(nat) ∧
h pfixGe s`ask} ⟼w {s ∈ state. <h, s`rel> ∈ prefix(nat)})"
apply (rule guaranteesI)
apply (blast intro: progress_lemma, auto)
done
lemma client_prog_Allowed:
"Allowed(client_prog) =
preserves(lift(rel)) ∩ preserves(lift(ask)) ∩ preserves(lift(tok))"
apply (cut_tac v = "lift (ask)" in preserves_type)
apply (auto simp add: Allowed_def client_prog_def [THEN def_prg_Allowed]
cons_Int_distrib safety_prop_Acts_iff)
done
end