# Theory RPC

theory RPC
imports RPCParameters Memory
```(*  Title:      HOL/TLA/Memory/RPC.thy
Author:     Stephan Merz, University of Munich
*)

section ‹RPC-Memory example: RPC specification›

theory RPC
imports RPCParameters ProcedureInterface Memory
begin

type_synonym rpcSndChType = "(rpcOp,Vals) channel"
type_synonym rpcRcvChType = "memChType"
type_synonym rpcStType = "(PrIds ⇒ rpcState) stfun"

(* state predicates *)

definition RPCInit :: "rpcRcvChType ⇒ rpcStType ⇒ PrIds ⇒ stpred"
where "RPCInit rcv rst p == PRED ((rst!p = #rpcA) ∧ ¬Calling rcv p)"

(* actions *)

definition RPCFwd :: "rpcSndChType ⇒ rpcRcvChType ⇒ rpcStType ⇒ PrIds ⇒ action"
where "RPCFwd send rcv rst p == ACT
\$(Calling send p)
∧ \$(rst!p) = # rpcA
∧ IsLegalRcvArg<arg<\$(send!p)>>
∧ Call rcv p RPCRelayArg<arg<send!p>>
∧ (rst!p)\$ = # rpcB
∧ unchanged (rtrner send!p)"

definition RPCReject :: "rpcSndChType ⇒ rpcRcvChType ⇒ rpcStType ⇒ PrIds ⇒ action"
where "RPCReject send rcv rst p == ACT
\$(rst!p) = # rpcA
∧ ¬IsLegalRcvArg<arg<\$(send!p)>>
∧ Return send p #BadCall
∧ unchanged ((rst!p), (caller rcv!p))"

definition RPCFail :: "rpcSndChType ⇒ rpcRcvChType ⇒ rpcStType ⇒ PrIds ⇒ action"
where "RPCFail send rcv rst p == ACT
¬\$(Calling rcv p)
∧ Return send p #RPCFailure
∧ (rst!p)\$ = #rpcA
∧ unchanged (caller rcv!p)"

definition RPCReply :: "rpcSndChType ⇒ rpcRcvChType ⇒ rpcStType ⇒ PrIds ⇒ action"
where "RPCReply send rcv rst p == ACT
¬\$(Calling rcv p)
∧ \$(rst!p) = #rpcB
∧ Return send p res<rcv!p>
∧ (rst!p)\$ = #rpcA
∧ unchanged (caller rcv!p)"

definition RPCNext :: "rpcSndChType ⇒ rpcRcvChType ⇒ rpcStType ⇒ PrIds ⇒ action"
where "RPCNext send rcv rst p == ACT
(  RPCFwd send rcv rst p
∨ RPCReject send rcv rst p
∨ RPCFail send rcv rst p
∨ RPCReply send rcv rst p)"

(* temporal *)

definition RPCIPSpec :: "rpcSndChType ⇒ rpcRcvChType ⇒ rpcStType ⇒ PrIds ⇒ temporal"
where "RPCIPSpec send rcv rst p == TEMP
Init RPCInit rcv rst p
∧ □[ RPCNext send rcv rst p ]_(rst!p, rtrner send!p, caller rcv!p)
∧ WF(RPCNext send rcv rst p)_(rst!p, rtrner send!p, caller rcv!p)"

definition RPCISpec :: "rpcSndChType ⇒ rpcRcvChType ⇒ rpcStType ⇒ temporal"
where "RPCISpec send rcv rst == TEMP (∀p. RPCIPSpec send rcv rst p)"

lemmas RPC_action_defs =
RPCInit_def RPCFwd_def RPCReject_def RPCFail_def RPCReply_def RPCNext_def

lemmas RPC_temp_defs = RPCIPSpec_def RPCISpec_def

(* The RPC component engages in an action for process p only if there is an outstanding,
unanswered call for that process.
*)

lemma RPCidle: "⊢ ¬\$(Calling send p) ⟶ ¬RPCNext send rcv rst p"
by (auto simp: AReturn_def RPC_action_defs)

lemma RPCbusy: "⊢ \$(Calling rcv p) ∧ \$(rst!p) = #rpcB ⟶ ¬RPCNext send rcv rst p"
by (auto simp: RPC_action_defs)

(* RPC failure actions are visible. *)
lemma RPCFail_vis: "⊢ RPCFail send rcv rst p ⟶
<RPCNext send rcv rst p>_(rst!p, rtrner send!p, caller rcv!p)"
by (auto dest!: Return_changed [temp_use] simp: angle_def RPCNext_def RPCFail_def)

lemma RPCFail_Next_enabled: "⊢ Enabled (RPCFail send rcv rst p) ⟶
Enabled (<RPCNext send rcv rst p>_(rst!p, rtrner send!p, caller rcv!p))"
by (force elim!: enabled_mono [temp_use] RPCFail_vis [temp_use])

(* Enabledness of some actions *)
lemma RPCFail_enabled: "⋀p. basevars (rtrner send!p, caller rcv!p, rst!p) ⟹
⊢ ¬Calling rcv p ∧ Calling send p ⟶ Enabled (RPCFail send rcv rst p)"
by (tactic ‹action_simp_tac (@{context} addsimps [@{thm RPCFail_def},
@{thm AReturn_def}, @{thm caller_def}, @{thm rtrner_def}]) [exI]
[@{thm base_enabled}, @{thm Pair_inject}] 1›)

lemma RPCReply_enabled: "⋀p. basevars (rtrner send!p, caller rcv!p, rst!p) ⟹
⊢ ¬Calling rcv p ∧ Calling send p ∧ rst!p = #rpcB
⟶ Enabled (RPCReply send rcv rst p)"
by (tactic ‹action_simp_tac (@{context} addsimps [@{thm RPCReply_def},
@{thm AReturn_def}, @{thm caller_def}, @{thm rtrner_def}]) [exI]
[@{thm base_enabled}, @{thm Pair_inject}] 1›)

end
```