Theory Micro_Rust_Runtime.Shareable_Resource
theory Shareable_Resource
imports
Separation_Lenses.SLens_Examples
Separation_Lenses.SLens_Pullback
Micro_Rust_Interfaces.Read_Write_Resource
Shallow_Separation_Logic.Shareable_Value
begin
section‹Reading/Writing shareable values›
text‹A ▩‹shareable_value› is an abstraction of a resource that can be read and written. We first
define read/write functions on ▩‹shareable_value› itself and prove its spec. Then, we lift them along
separation lenses to read/write functions on larger separation algebras. We then use the result to
instantiate an abstract interface to read-writable resources.›
definition read_shareable_value_core :: ‹('v shareable_value, 'v, 'r, 'abort, 'i, 'o) expression› where
‹read_shareable_value_core ≡ Expression (λr.
case r of
No_Value ⇒ Abort DanglingPointer r
| Shared_Value _ val ⇒ Success val r
)›
definition shareable_value_is :: ‹share ⇒ 'v ⇒ 'v shareable_value assert› where
‹shareable_value_is sh v ≡ ⟨0 < sh⟩ ⋆ ↑⇩s (Shared_Value (Abs_nonempty_share sh) v)›
lemma ucincl_shareable_value_is [simp, ucincl_intros]: ‹ucincl (shareable_value_is sh v)›
unfolding shareable_value_is_def by (simp add: uc_state_ucincl ucincl_intros)
lemma shareable_value_is_alt:
‹σ ∈ shareable_value_is sh v ⟷ 0 < sh ∧ σ ∈ ↑⇩s (Shared_Value (Abs_nonempty_share sh) v)›
by (simp add: shareable_value_is_def uc_state_ucincl asepconj_pure', simp add: apure_def)
lemma shareable_value_is_top_alt:
shows ‹shareable_value_is ⊤ v = {Shared_Value ⊤ v}›
by (safe; simp add: shareable_value_is_alt)
(auto simp add: shareable_value_is_def asat_def shareable_value_uc_state_top zero_share_def
simp flip: top_nonempty_share.abs_eq)
lemma ucincl_shared_value_top[simp, ucincl_intros]:
shows ‹ucincl {Shared_Value ⊤ v}›
by (simp flip: shareable_value_is_top_alt add: ucincl_intros)
lemma asepconj_float_pure:
shows ‹α ⋆ ⟨P⟩ = ⟨P⟩ ⋆ α›
and ‹α ⋆ ⟨P⟩ ⋆ β = ⟨P⟩ ⋆ α ⋆ β›
by (simp add: asepconj_comm asepconj_swap_top asepconj_pure)+
lemma shareable_value_split:
assumes ‹sh0 ♯ sh1›
and ‹0 < sh0› and ‹0 < sh1›
shows ‹shareable_value_is (sh0 + sh1) v ⤏ shareable_value_is sh0 v ⋆ shareable_value_is sh1 v›
proof -
from assms have ‹0 < sh0 + sh1›
by (simp add: less_supI2 plus_share_def)
from this show ?thesis
using assms by (simp add: shareable_value_is_def asepconj_ident uc_state_ucincl asepconj_simp
Abs_nonempty_share_inverse aentails_def eq_onp_same_args plus_nonempty_share.abs_eq plus_share_def
shareable_value_uc_state_asepconj zero_share_def)
qed
lemma shareable_value_combine:
shows ‹shareable_value_is sh0 v0 ⋆ shareable_value_is sh1 v1
⤏ ⟨v0 = v1⟩ ⋆ ⟨sh0 ♯ sh1⟩ ⋆ shareable_value_is (sh0 + sh1) v0›
proof (intro apure_entailsR apure_entailsR0)
assume "is_sat (shareable_value_is sh0 v0 ⋆ shareable_value_is sh1 v1)"
then show "v0 = v1"
unfolding shareable_value_is_def
by (metis (no_types, opaque_lifting) asepconj_bot_zero2 asepconj_comm asepconj_float_pure(2)
non_is_sat_empty shareable_value_uc_state_asepconj_general)
next
assume §: "is_sat (shareable_value_is sh0 v0 ⋆ shareable_value_is sh1 v1)"
then obtain "is_sat ⟨0 < sh1⟩" "is_sat ⟨0 < sh0⟩"
by (metis is_sat_pure is_sat_splitE shareable_value_is_def)
with § show "sh0 ♯ sh1"
apply (simp add: shareable_value_is_def asepconj_float_pure)
by (simp add: asepconj_simp asepconj_uc_state_general Abs_nonempty_share_inverse zero_share_def split: if_splits)
next
show "shareable_value_is sh0 v0 ⋆ shareable_value_is sh1 v1 ⤏ shareable_value_is (sh0 + sh1) v0"
apply (simp add: shareable_value_is_def asepconj_float_pure)
apply (intro apure_entailsL assocL_entails apure_entailsR apure_entailsR0)
apply (simp_all add: ucincl_intros uc_state_ucincl plus_share_def less_supI2)
by (simp add: aentails_def eq_onp_same_args plus_nonempty_share.abs_eq shareable_value_uc_state_asepconj_general zero_share_def)
qed
lemma eval_read_shareable_value_core:
shows ‹σ ↝⇩a ⟨y,read_shareable_value_core⟩ (a, σ') ⟷ (σ = No_Value ∧ a = DanglingPointer ∧ σ = σ')›
and ‹σ ↝⇩v ⟨y,read_shareable_value_core⟩ (v, σ') ⟷ (σ' = σ ∧ (case σ of No_Value ⇒ False | Shared_Value sh v' ⇒ v = v'))›
and ‹σ ↝⇩r ⟨y,read_shareable_value_core⟩ (r, σ') ⟷ False›
by (auto simp add: read_shareable_value_core_def evaluates_to_abort_def evaluates_to_value_def
evaluates_to_return_def deep_evaluates_nondet_basic.simps evaluate_def split!: shareable_value.splits)
corollary eval_value_read_shareable_value_core_local:
shows ‹is_local (eval_value y read_shareable_value_core) (shareable_value_is sh v)›
by (intro is_localI; case_tac σ_0; case_tac σ_1;
auto simp add: shareable_value_is_alt eval_return_def asat_def uc_state_def
eval_read_shareable_value_core shareable_value_upwards_closure_core eval_value_def)
corollary eval_return_read_shareable_value_core_local:
shows ‹is_local (eval_return y read_shareable_value_core) (shareable_value_is sh v)›
by (intro is_localI; simp add: eval_return_def eval_read_shareable_value_core)
corollary eval_abort_read_shareable_value_core_local:
shows ‹is_local (eval_abort y read_shareable_value_core) (shareable_value_is sh v)›
apply (intro is_localI; simp add: eval_abort_def eval_read_shareable_value_core)
apply fastforce
apply (simp add: asat_def shareable_value_is_alt shareable_value_upwards_closure_core(3) uc_state_def)
done
lemmas eval_read_shareable_value_core_local =
eval_value_read_shareable_value_core_local
eval_return_read_shareable_value_core_local
eval_abort_read_shareable_value_core_local
definition read_shareable_value :: ‹('v shareable_value, 'v, 'abort, 'i, 'o) function_body› where
‹read_shareable_value ≡ FunctionBody read_shareable_value_core›
definition read_shareable_value_contract :: ‹'v ⇒ share ⇒ ('v shareable_value, 'v, 'abort) function_contract›
where ‹read_shareable_value_contract ≡ λv sh.
let pre = shareable_value_is sh v in
let post = λr. shareable_value_is sh v ⋆ ⟨r = v⟩ in
make_function_contract pre post›
lemma read_shareable_value_contract_no_abort:
shows ‹function_contract_abort (read_shareable_value_contract a b) = ⊥›
by (simp add: read_shareable_value_contract_def pull_back_contract_def)
lemma read_shareable_value_spec:
shows ‹Γ; read_shareable_value ⊨⇩F read_shareable_value_contract v sh›
apply (intro satisfies_function_contractI;
clarsimp intro!: ucincl_intros simp add: read_shareable_value_contract_def)
apply (intro sstripleI; clarsimp simp add: read_shareable_value_def atriple_rel_def
asat_apure_distrib2 ucincl_intros asepconj_simp eval_read_shareable_value_core_local; safe?)
apply (auto simp add: eval_read_shareable_value_core shareable_value_is_alt
eval_return_def eval_abort_def eval_value_def shareable_value_uc_state asat_def)
done
definition write_shareable_value_core :: ‹'v ⇒ ('v shareable_value, unit, 'r, 'abort, 'i, 'o) expression› where
‹write_shareable_value_core val ≡ Expression (λr.
case r of
Shared_Value sh _ ⇒ if sh = ⊤ then Success () (Shared_Value ⊤ val) else Abort DanglingPointer r
| _ ⇒ Abort DanglingPointer r
)›
definition shareable_value_is_writable :: ‹'v shareable_value assert› where
‹shareable_value_is_writable ≡ { σ. case σ of No_Value ⇒ False | Shared_Value sh _ ⇒ sh = top }›
lemma shareable_value_is_writableE:
assumes ‹σ ⊨ shareable_value_is_writable›
and ‹⋀v. σ = Shared_Value ⊤ v ⟹ R›
shows R
using assms by (auto simp add: asat_def shareable_value_is_writable_def split!: shareable_value.splits)
lemma shareable_value_is_writable_alt:
shows ‹(⨆v0. shareable_value_is ⊤ v0) = shareable_value_is_writable›
by (intro asat_semequivI;
simp add: asat_def shareable_value_is_writable_def shareable_value_is_top_alt split!: shareable_value.splits)
lemma shareable_value_is_writable_ucincl[simp, ucincl_intros]:
shows ‹ucincl shareable_value_is_writable›
by (clarsimp intro!: ucincl_intros simp flip: shareable_value_is_writable_alt)
lemma shareable_value_is_writable_basic [simp]:
shows ‹Shared_Value ⊤ v ⊨ shareable_value_is_writable›
by (simp add: asat_def shareable_value_is_writable_def)
lemma eval_write_shareable_value_core:
shows ‹σ ↝⇩a ⟨y,write_shareable_value_core val⟩ (a, σ') ⟷ ( ¬(σ ⊨ shareable_value_is_writable) ∧ a = DanglingPointer ∧ σ = σ')›
and ‹σ ↝⇩v ⟨y,write_shareable_value_core val⟩ (v, σ') ⟷ (σ ⊨ shareable_value_is_writable ∧ σ' = Shared_Value top val)›
and ‹σ ↝⇩r ⟨y,write_shareable_value_core val⟩ (r, σ') ⟷ False›
by (auto simp add: write_shareable_value_core_def evaluates_to_abort_def evaluates_to_value_def
asat_def shareable_value_is_writable_def evaluates_to_return_def deep_evaluates_nondet_basic.simps evaluate_def
split!: shareable_value.splits if_splits)
corollary eval_value_write_shareable_value_core_local:
shows ‹is_local (eval_value y (write_shareable_value_core val)) shareable_value_is_writable›
by (intro is_localI) (auto simp: shareable_value_disjoint_top elim!: shareable_value_is_writableE)
corollary eval_return_write_shareable_value_core_local:
shows ‹is_local (eval_return y (write_shareable_value_core val)) shareable_value_is_writable›
by (intro is_localI; simp add: eval_return_def eval_write_shareable_value_core)
corollary eval_abort_write_shareable_value_core_local:
shows ‹is_local (eval_abort y (write_shareable_value_core val)) shareable_value_is_writable›
by (intro is_localI) (auto simp: shareable_value_disjoint_top elim!: shareable_value_is_writableE)
lemmas eval_write_shareable_value_core_local =
eval_value_write_shareable_value_core_local
eval_return_write_shareable_value_core_local
eval_abort_write_shareable_value_core_local
definition write_shareable_value :: ‹'v ⇒ ('v shareable_value, unit, 'abort, 'i, 'o) function_body› where
‹write_shareable_value val ≡ FunctionBody (write_shareable_value_core val)›
definition write_shareable_value_contract :: ‹'v ⇒ ('v shareable_value, unit, 'abort) function_contract›
where ‹write_shareable_value_contract ≡ λv.
let pre = ⨆v0. shareable_value_is ⊤ v0 in
let post = λr. shareable_value_is ⊤ v in
make_function_contract pre post›
lemma write_shareable_value_contract_no_abort:
shows ‹function_contract_abort (write_shareable_value_contract a) = ⊥›
by (simp add: write_shareable_value_contract_def pull_back_contract_def)
lemma write_shareable_value_spec:
shows ‹Γ; write_shareable_value v ⊨⇩F write_shareable_value_contract v›
proof -
have ‹Γ ; shareable_value_is_writable ⊢
function_body (write_shareable_value v) ⊣
(λr. shareable_value_is ⊤ v) ⨝
(λr. shareable_value_is ⊤ v) ⨝ ⊥›
apply (intro sstripleI)
apply (auto simp add: eval_write_shareable_value_core shareable_value_is_top_alt eval_value_def eval_return_def eval_abort_def
write_shareable_value_def asepconj_simp atriple_rel_def shareable_value_disjoint_top
is_local_def elim!: shareable_value_is_writableE)
done
then show ?thesis
by (intro satisfies_function_contractI) (auto simp add: shareable_value_is_writable_alt write_shareable_value_contract_def)
qed
text‹In any interesting application, the underlying separation algebra will not be equal to
▩‹shareable_value›, but contain it via a separation lens. In this case, we can use the pullback
mechanism to obtain read/write functions on the larger separation algebra:›
type_synonym ('s, 'v) shareable_resource = ‹('s, 'v shareable_value) lens›
definition resource_is :: ‹('s, 'v) shareable_resource ⇒ share ⇒ 'v ⇒ 's assert›
where ‹resource_is l sh v ≡ l¯ (shareable_value_is sh v)›
definition read_resource :: ‹('s, 'v) shareable_resource ⇒ ('s, 'v, 'abort, 'i, 'o) function_body›
where ‹read_resource l ≡ l¯ read_shareable_value›
definition write_resource :: ‹('s, 'v) shareable_resource⇒ 'v ⇒ ('s, unit, 'abort, 'i, 'o) function_body›
where ‹write_resource l v ≡ l¯ (write_shareable_value v)›
definition read_resource_contract :: ‹('s::sepalg, 'v) shareable_resource ⇒ 'v ⇒ share ⇒ ('s, 'v, 'abort) function_contract›
where ‹read_resource_contract l v sh ≡ l¯ (read_shareable_value_contract v sh)›
lemma read_resource_contract_no_abort:
shows ‹function_contract_abort (read_resource_contract a b c) = ⊥›
by (simp add: read_shareable_value_contract_no_abort read_resource_contract_def pull_back_contract_def
pull_back_assertion_def bot_fun_def)
definition write_resource_contract :: ‹('s::sepalg, 'v) shareable_resource ⇒ 'v ⇒ ('s, unit, 'abort) function_contract›
where ‹write_resource_contract l v ≡ l¯ (write_shareable_value_contract v)›
lemma write_resource_contract_no_abort:
shows ‹function_contract_abort (write_resource_contract a b) = ⊥›
by (simp add: write_shareable_value_contract_no_abort write_resource_contract_def pull_back_contract_def
pull_back_assertion_def bot_fun_def)
lemma resource_is_split:
assumes ‹is_valid_slens r›
and ‹sh0 ♯ sh1›
and ‹0 < sh0› and ‹0 < sh1›
shows ‹resource_is r (sh0 + sh1) v ⤏ resource_is r sh0 v ⋆ resource_is r sh1 v›
using assms
apply (clarsimp simp add: resource_is_def shareable_value_split simp flip: slens_pull_back_simps_generic)
apply (simp add: shareable_value_split slens_pull_back_intros_generic)
done
lemma resource_is_merge:
assumes ‹is_valid_slens r›
shows ‹resource_is r sh0 v0 ⋆ resource_is r sh1 v1 ⤏ ⟨sh0 ♯ sh1⟩ ⋆ ⟨v0 = v1⟩ ⋆ resource_is r (sh0 + sh1) v0›
using assms
apply (clarsimp simp add: resource_is_def shareable_value_split simp flip: slens_pull_back_simps_generic)
apply (metis asepconj_swap_top shareable_value_combine slens_pull_back_intros_generic(2))
done
lemma read_resource_spec:
assumes ‹is_valid_slens l›
shows ‹Γ; read_resource l ⊨⇩F read_resource_contract l v sh›
by (simp add: assms slens.pull_back_spec_universal read_resource_contract_def read_resource_def
read_shareable_value_spec read_shareable_value_contract_no_abort)
lemma write_resource_spec:
assumes ‹is_valid_slens l›
shows ‹Γ; write_resource l v ⊨⇩F write_resource_contract l v›
by (simp add: assms slens.pull_back_spec_universal write_resource_contract_def write_resource_def
write_shareable_value_spec write_shareable_value_contract_no_abort)
lemma resource_is_eval_lens_alt:
shows ‹σ ⊨ resource_is (share_map_eval_lens k) sh v
⟷ 0 < sh ∧ Shared_Value (Abs_nonempty_share sh) v ≼ rbt_share_map_α σ k›
by (clarsimp simp add: share_map_eval_lens_def resource_is_def pull_back_assertion_def asat_def
shareable_value_is_alt uc_state_def)
lemma rbt_share_map_decompose_resource:
fixes m :: ‹('k::linorder, 'v) rbt_share_map›
shows ‹m ⊨ ⋆⋆{# resource_is (share_map_eval_lens k) (Rep_nonempty_share sh) v .
(k, v, sh) ← rbt_share_map_mset m #}›
using Rep_nonempty_share by (auto intro!: rbt_share_map_decompose_generic
simp add: resource_is_eval_lens_alt zero_share_def Rep_nonempty_share_inverse)
subsection‹Construction RW resources from ▩‹shareable_value››
text‹In this section, we show that any separation lens to a ▩‹shareable_value› gives rise to an
interpretation of the above interface.›
text‹This is a bit of an odd thing. We don't want the code generator to try to produce code corresponding
to the above set definition, which really only exists for purely logical purposes. So, we tell the
code generator to replace it with an error instead. Note that ▩‹resource_is› has other arguments
beyond ▩‹l› on the LHS of its defining equation, so won't be invoked.›
declare [[code abort: resource_is]]
definition rw_resource_from_slens :: ‹('s, 'v) shareable_resource ⇒ ('s, 'v, 'abort, 'i, 'o) rw_resource› where
‹rw_resource_from_slens l ≡ make_rw_resource (resource_is l) (read_resource l) (write_resource l)›
lemma rw_resource_from_slens_contracts:
assumes valid: ‹is_valid_slens l›
shows ‹generic_read_contract (rw_resource_is (rw_resource_from_slens l))
= read_resource_contract l›
and ‹generic_write_contract (rw_resource_is (rw_resource_from_slens l))
= write_resource_contract l›
using assms by (auto intro!: ext simp add: generic_write_contract_def generic_read_contract_def
rw_resource_is_def rw_resource_from_slens_def resource_is_def
read_resource_contract_def read_shareable_value_contract_def
write_resource_contract_def write_shareable_value_contract_def
pull_back_contract_def slens_pull_back_simps_generic)
lemma read_resource_contract_concrete:
assumes valid: ‹is_valid_slens l›
shows ‹generic_read_contract (rw_resource_is (rw_resource_from_slens l))
= read_resource_contract l›
using assms rw_resource_from_slens_contracts by meson
lemma rw_resource_valid:
assumes ‹is_valid_slens l›
shows ‹standard_rw_resource (rw_resource_from_slens l)›
proof (intro standard_rw_resourceI)
fix sh v show ‹ucincl (rw_resource_is (rw_resource_from_slens l) sh v)›
by (simp add: assms resource_is_def rw_resource_from_slens_def slens.pull_back_ucincl)
next
fix sh0 sh1 :: share and v0 v1
from assms show
‹rw_resource_is (rw_resource_from_slens l) sh0 v0
⋆ rw_resource_is (rw_resource_from_slens l) sh1 v1
⤏ ⟨sh0 ♯ sh1⟩ ⋆ ⟨v0 = v1⟩ ⋆ rw_resource_is (rw_resource_from_slens l) (sh0 + sh1) v0›
by (clarsimp simp add: resource_is_merge rw_resource_from_slens_def)
next
fix sh0 sh1 :: share and v
fix sh0 sh1 :: share and v
assume ‹0 < sh0› and ‹0 < sh1› and ‹sh0 ♯ sh1›
from this and assms show
‹rw_resource_is (rw_resource_from_slens l) (sh0 + sh1) v ⤏
rw_resource_is (rw_resource_from_slens l) sh0 v ⋆ rw_resource_is (rw_resource_from_slens l) sh1 v›
by (clarsimp simp add: resource_is_merge rw_resource_from_slens_def resource_is_split)
next
fix Γ v
from assms show ‹Γ ; rw_resource_write (rw_resource_from_slens l) v
⊨⇩F generic_write_contract (rw_resource_is (rw_resource_from_slens l)) v›
by (simp add: rw_resource_from_slens_contracts)
(simp add: rw_resource_write_def rw_resource_from_slens_def write_resource_spec)
next
fix Γ sh v
from assms show ‹Γ ; rw_resource_read (rw_resource_from_slens l)
⊨⇩F generic_read_contract (rw_resource_is (rw_resource_from_slens l)) v sh›
by (simp add: rw_resource_from_slens_contracts)
(simp add: rw_resource_read_def rw_resource_from_slens_def read_resource_spec)
qed
lemma rw_resource_is_from_slens:
assumes ‹is_valid_slens l›
shows ‹σ ⊨ rw_resource_is (rw_resource_from_slens l) ⊤ x ⟷ lens_view l σ = Shared_Value ⊤ x›
by (clarsimp simp add: rw_resource_from_slens_def asat_def resource_is_def pull_back_assertion_def
shareable_value_is_top_alt)
end