-
Notifications
You must be signed in to change notification settings - Fork 0
/
Subprocess.thy
190 lines (137 loc) · 7.15 KB
/
Subprocess.thy
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
theory Subprocess
imports Main
begin
text "A simpler version of assume-guarantee reasoning that focuses on non-interference of state
updates alone, e.g. https://arxiv.org/pdf/2103.13743.pdf"
text "Goes back to Lamport & Abadi: https://lamport.azurewebsites.net/pubs/abadi-conjoining.pdf"
text "Each action operates on its own local state, which is defined as a 'v view type. The relationship
between 'v and 's is definable by a lens. This is different than the seL4 process model,
since that effectively only has a single lens whereas multiple lenses are required for
each action here."
record ('s, 'v) lens =
Get :: "'s \<Rightarrow> 'v"
Put :: "'v \<Rightarrow> 's \<Rightarrow> 's"
text "Well-behaved lenses must follow the 'lens laws' which ensure that they retrieve and update
the same part of the source state."
definition "well_behaved l \<equiv> (\<forall>ls lv. (Put l) ((Get l) ls) ls = ls \<and> (Get l) ((Put l) lv ls) = lv)"
text "A process is a representation of a program that proceeds through a sequence of states in
response to actions (inputs) of type 'e, i.e. a state machine."
type_synonym ('e, 's) process = "'e \<Rightarrow> 's \<Rightarrow> 's"
text "A local action is a step function on its own local state type 'a, where 'a is defineable as a lens
on some global state type 's"
record ('s, 'a) local_action =
lens :: "('s, 'a) lens"
step :: "'a \<Rightarrow> 'a"
text "An action mapping maps an action 'e to its corresponding local action"
type_synonym ('e, 's, 'a) action_mapping = "'e \<Rightarrow> ('s, 'a) local_action"
text "compose_local_actions defines how a global process can be defined from a set of local actions.
It uses the lens defined in the local action for each action type to get the local action state
from the global state, execute the local step function, and write the result back into
the global state."
definition compose_local_actions :: "('e, 's, 'a) action_mapping \<Rightarrow> ('e, 's) process" where
"compose_local_actions am = (\<lambda>e s.(
let locact = am e;
lns = (lens locact);
locact_s = (Get lns) s;
res = (step locact) locact_s in
(Put lns) res s
))"
text "'Action Simulation' is where each local implementation action simulates its corresponding
action in the model."
definition "local_simulates am_i am_m e s t = (
let proc_i = step (am_i e) in
let proc_m = step (am_m e) in
let impl_start = (Get (lens (am_i e))) s in
let model_start = (Get (lens (am_m e))) s in
proc_i impl_start = t \<longrightarrow> proc_m model_start = t)"
text "Basic notion of simulation."
definition "simulates impl_proc model_proc e s t = (impl_proc e s = t \<longrightarrow> model_proc e s = t)"
text "We want to show that in order to prove that an implementation process simulates another
process, we can instead decompose both processes each into a set of local actions. If the
local actions simulate each other, and the lenses used to define the local action states are
well-behaved, then the global implementation process simulates the global model."
theorem
assumes "well_behaved lm"
and "am_m = (\<lambda>e. \<lparr>lens=lm, step=stm\<rparr>)"
and "well_behaved li"
and "am_i = (\<lambda>e. \<lparr>lens=li, step=sti\<rparr> )"
and "model_proc \<equiv> compose_local_actions am_m"
and "impl_proc \<equiv> compose_local_actions am_i"
(* and "local_simulates am_i am_m e s t"*)
shows "simulates impl_proc model_proc e s t"
using assms
unfolding simulates_def local_simulates_def compose_local_actions_def well_behaved_def
by (metis local_action.select_convs(1))
theorem local_sim_imp_sim:
assumes "well_behaved (lens (am_m e))"
and "well_behaved (lens (am_i e))"
(* Don't even need this assumption, which is suspect *)
and "action_simulates am_i am_m e s t"
shows "simulates (compose_local_actions am_m) (compose_local_actions am_i) e s t"
using assms
unfolding simulates_def local_simulates_def compose_local_actions_def well_behaved_def
by metis
type_synonym ('s) invariant_func = "'s \<Rightarrow> bool"
(* Invariant: Unauthenticated users are always denied access" *)
definition "local_invariant am inv_f e s = (
let step_f = step (am e) in
let local_state = Get (lens (am e)) s in
let put = Put (lens (am e)) in
inv_f s \<and> inv_f (put (step_f local_state) s)
)"
text "Local invariance implies global invariance.
Note how well-behavedness of the lens isn't a required assumption, because all that matters
is that the invariant holds before and after the action completes."
text "An improvement would be to also define a selector (just the read part of a lens) on the global
state so that the invariant only needs to operate on the data that it cares about."
theorem local_inv_imp_inv:
assumes "local_invariant am_i inv_f e s"
shows "inv_f ((compose_local_actions am_i) e s)"
using assms
unfolding well_behaved_def local_invariant_def compose_local_actions_def
by metis
definition exec :: "('e, 's) process \<Rightarrow> 'e list \<Rightarrow> 's \<Rightarrow> 's" where
"exec stp es i = foldl (\<lambda>s e. stp e s) i es"
definition "refines I M es s s' = (exec I es s = s' \<longrightarrow> exec M es s = s')"
theorem assumes "simulates impl_proc model_proc e s t"
shows "refines impl_proc model_proc es s t"
oops
section "Test"
record data = x :: nat y :: nat
definition "data_lens = \<lparr> Get= (\<lambda>d. x d), Put = (\<lambda>n d. d\<lparr>x := n\<rparr>) \<rparr>"
theorem "well_behaved data_lens"
by (simp add: data_lens_def well_behaved_def)
section "Subprocs for banking"
text "operations: Open account, Transfer between accounts"
record account =
name :: string
balance :: int
record transaction =
src :: account
dst :: account
amount :: int
datatype BankingEvent =
OpenAccount string
| Transfer account account int
record banking_state_m =
accounts :: "account set"
ledger :: "transaction set"
definition "banking_step_m e s = (case e of
OpenAccount nm \<Rightarrow> s\<lparr> accounts := insert \<lparr>name=nm, balance=0\<rparr> (accounts s) \<rparr>
| Transfer srcAct dstAct amt \<Rightarrow> s\<lparr> ledger := insert \<lparr>src=srcAct, dst=dstAct, amount=amt \<rparr> (ledger s) \<rparr>)"
(* Subproc version *)
definition "open_account nm acts = insert \<lparr>name=nm, balance=0\<rparr> acts"
definition "transfer srcAct dstAct amt ledg = insert \<lparr>src=srcAct, dst=dstAct, amount=amt \<rparr> ledg"
datatype banking_subproc_view =
VOpenAccount "account set"
| VTransfer "transaction set"
definition "set_banking_state v s = (case v of
VOpenAccount as \<Rightarrow> s\<lparr> accounts := as \<rparr>
| VTransfer ts \<Rightarrow> s\<lparr> ledger := ts \<rparr> )"
definition "get_acts s = VOpenAccount (accounts s)"
definition "get_ledg s = ledger s"
definition "bank_subproc_mapping e = (case e of
OpenAccount nm \<Rightarrow> \<lparr> splens=\<lparr>Get=get_acts, Put=set_banking_state\<rparr>, spstep=(\<lambda>v. open_account nm acts) \<rparr>
| Transfer srcAct dstAct amt \<Rightarrow>
\<lparr>splens=\<lparr>Get=get_ledg, Put=set_banking_state\<rparr>, spstep=(\<lambda>ledg. transfer srcAct dstAct amt ledg) \<rparr>)"
end