equal
deleted
inserted
replaced
26 simpler than for the generic RPC component. RelayArg returns an arbitrary |
26 simpler than for the generic RPC component. RelayArg returns an arbitrary |
27 memory call for illegal arguments. *) |
27 memory call for illegal arguments. *) |
28 IsLegalRcvArg :: "rpcOp => bool" |
28 IsLegalRcvArg :: "rpcOp => bool" |
29 RPCRelayArg :: "rpcOp => memOp" |
29 RPCRelayArg :: "rpcOp => memOp" |
30 |
30 |
31 axioms |
31 axiomatization where |
32 (* RPCFailure is different from MemVals and exceptions *) |
32 (* RPCFailure is different from MemVals and exceptions *) |
33 RFNoMemVal: "RPCFailure ~: MemVal" |
33 RFNoMemVal: "RPCFailure ~: MemVal" and |
34 NotAResultNotRF: "NotAResult ~= RPCFailure" |
34 NotAResultNotRF: "NotAResult ~= RPCFailure" and |
35 OKNotRF: "OK ~= RPCFailure" |
35 OKNotRF: "OK ~= RPCFailure" and |
36 BANotRF: "BadArg ~= RPCFailure" |
36 BANotRF: "BadArg ~= RPCFailure" |
37 |
37 |
38 defs |
38 defs |
39 IsLegalRcvArg_def: "IsLegalRcvArg ra == |
39 IsLegalRcvArg_def: "IsLegalRcvArg ra == |
40 case ra of (memcall m) => True |
40 case ra of (memcall m) => True |