14 *) |
14 *) |
15 |
15 |
16 datatype rpcOp = memcall memOp | othercall Vals |
16 datatype rpcOp = memcall memOp | othercall Vals |
17 datatype rpcState = rpcA | rpcB |
17 datatype rpcState = rpcA | rpcB |
18 |
18 |
19 consts |
19 axiomatization RPCFailure :: Vals and BadCall :: Vals |
20 (* some particular return values *) |
20 where |
21 RPCFailure :: Vals |
|
22 BadCall :: Vals |
|
23 |
|
24 (* Translate an rpc call to a memory call and test if the current argument |
|
25 is legal for the receiver (i.e., the memory). This can now be a little |
|
26 simpler than for the generic RPC component. RelayArg returns an arbitrary |
|
27 memory call for illegal arguments. *) |
|
28 IsLegalRcvArg :: "rpcOp \<Rightarrow> bool" |
|
29 RPCRelayArg :: "rpcOp \<Rightarrow> memOp" |
|
30 |
|
31 axiomatization where |
|
32 (* RPCFailure is different from MemVals and exceptions *) |
21 (* RPCFailure is different from MemVals and exceptions *) |
33 RFNoMemVal: "RPCFailure \<notin> MemVal" and |
22 RFNoMemVal: "RPCFailure \<notin> MemVal" and |
34 NotAResultNotRF: "NotAResult \<noteq> RPCFailure" and |
23 NotAResultNotRF: "NotAResult \<noteq> RPCFailure" and |
35 OKNotRF: "OK \<noteq> RPCFailure" and |
24 OKNotRF: "OK \<noteq> RPCFailure" and |
36 BANotRF: "BadArg \<noteq> RPCFailure" |
25 BANotRF: "BadArg \<noteq> RPCFailure" |
37 |
26 |
38 defs |
27 (* Translate an rpc call to a memory call and test if the current argument |
39 IsLegalRcvArg_def: "IsLegalRcvArg ra == |
28 is legal for the receiver (i.e., the memory). This can now be a little |
40 case ra of (memcall m) \<Rightarrow> True |
29 simpler than for the generic RPC component. RelayArg returns an arbitrary |
41 | (othercall v) \<Rightarrow> False" |
30 memory call for illegal arguments. *) |
42 RPCRelayArg_def: "RPCRelayArg ra == |
31 |
43 case ra of (memcall m) \<Rightarrow> m |
32 definition IsLegalRcvArg :: "rpcOp \<Rightarrow> bool" |
44 | (othercall v) \<Rightarrow> undefined" |
33 where "IsLegalRcvArg ra == |
|
34 case ra of (memcall m) \<Rightarrow> True |
|
35 | (othercall v) \<Rightarrow> False" |
|
36 |
|
37 definition RPCRelayArg :: "rpcOp \<Rightarrow> memOp" |
|
38 where "RPCRelayArg ra == |
|
39 case ra of (memcall m) \<Rightarrow> m |
|
40 | (othercall v) \<Rightarrow> undefined" |
45 |
41 |
46 lemmas [simp] = RFNoMemVal NotAResultNotRF OKNotRF BANotRF |
42 lemmas [simp] = RFNoMemVal NotAResultNotRF OKNotRF BANotRF |
47 NotAResultNotRF [symmetric] OKNotRF [symmetric] BANotRF [symmetric] |
43 NotAResultNotRF [symmetric] OKNotRF [symmetric] BANotRF [symmetric] |
48 |
44 |
49 end |
45 end |