1 | (**************************************************************************) |
---|
2 | (* ___ *) |
---|
3 | (* ||M|| *) |
---|
4 | (* ||A|| A project by Andrea Asperti *) |
---|
5 | (* ||T|| *) |
---|
6 | (* ||I|| Developers: *) |
---|
7 | (* ||T|| The HELM team. *) |
---|
8 | (* ||A|| http://helm.cs.unibo.it *) |
---|
9 | (* \ / *) |
---|
10 | (* \ / This file is distributed under the terms of the *) |
---|
11 | (* v GNU General Public License Version 2 *) |
---|
12 | (* *) |
---|
13 | (**************************************************************************) |
---|
14 | |
---|
15 | include "joint/linearise.ma". |
---|
16 | include "common/StatusSimulation.ma". |
---|
17 | include "joint/Traces.ma". |
---|
18 | include "joint/SemanticUtils.ma". |
---|
19 | |
---|
20 | definition graph_prog_params: |
---|
21 | ∀p:unserialized_params. |
---|
22 | (∀F.sem_unserialized_params p F) → |
---|
23 | joint_program (mk_graph_params p) → |
---|
24 | prog_params |
---|
25 | ≝ |
---|
26 | λp,p',prog. |
---|
27 | (mk_prog_params |
---|
28 | (make_sem_graph_params (mk_graph_params p) p') |
---|
29 | prog). |
---|
30 | |
---|
31 | definition lin_prog_params: |
---|
32 | ∀p:unserialized_params. |
---|
33 | (∀F.sem_unserialized_params p F) → |
---|
34 | joint_program (mk_lin_params p) → |
---|
35 | prog_params |
---|
36 | ≝ |
---|
37 | λp,p',prog. |
---|
38 | (mk_prog_params |
---|
39 | (make_sem_lin_params (mk_lin_params p) p') |
---|
40 | prog). |
---|
41 | |
---|
42 | (*CSC: Paolo, come to the rescue*) |
---|
43 | axiom choose_sigma: |
---|
44 | ∀p:unserialized_params. |
---|
45 | (∀F.sem_unserialized_params p F) → |
---|
46 | joint_program (mk_graph_params p) → |
---|
47 | identifier LabelTag → option ℕ. |
---|
48 | |
---|
49 | (*CSC: Paolo, come to the rescue*) |
---|
50 | axiom linearise_code_spec: |
---|
51 | ∀p : unserialized_params. |
---|
52 | ∀p':(∀F.sem_unserialized_params p F). |
---|
53 | ∀graph_prog:joint_program (mk_graph_params p). |
---|
54 | ∀graph_fun:joint_closed_internal_function (mk_graph_params p) |
---|
55 | (globals (graph_prog_params p p' graph_prog)). |
---|
56 | let sigma ≝ choose_sigma p p' graph_prog in |
---|
57 | let lin_fun ≝ linearise_int_fun … graph_fun in |
---|
58 | let g ≝ joint_if_code ?? (pi1 … graph_fun) in |
---|
59 | let c ≝ joint_if_code ?? (pi1 … lin_fun) in |
---|
60 | ∀entry : (Σl.bool_to_Prop (code_has_label … g l)). |
---|
61 | code_closed … c ∧ |
---|
62 | sigma entry = Some ? 0 ∧ |
---|
63 | ∀l,n.sigma l = Some ? n → |
---|
64 | ∃s. lookup … g l = Some ? s ∧ |
---|
65 | opt_Exists ? |
---|
66 | (λls.let 〈lopt, ts〉 ≝ ls in |
---|
67 | opt_All ? (eq ? l) lopt ∧ |
---|
68 | ts = graph_to_lin_statement … s ∧ |
---|
69 | opt_All ? |
---|
70 | (λnext.Or (sigma next = Some ? (S n)) |
---|
71 | (nth_opt … (S n) c = Some ? 〈None ?, GOTO … next〉)) |
---|
72 | (stmt_implicit_label … s)) (nth_opt … n c). |
---|
73 | |
---|
74 | definition graph_abstract_status: |
---|
75 | ∀p:unserialized_params. |
---|
76 | (∀F.sem_unserialized_params p F) → |
---|
77 | joint_program (mk_graph_params p) → |
---|
78 | abstract_status |
---|
79 | ≝ |
---|
80 | λp,p',prog. |
---|
81 | joint_abstract_status (graph_prog_params p p' prog). |
---|
82 | |
---|
83 | definition lin_abstract_status: |
---|
84 | ∀p:unserialized_params. |
---|
85 | (∀F.sem_unserialized_params p F) → |
---|
86 | joint_program (mk_lin_params p) → |
---|
87 | abstract_status |
---|
88 | ≝ |
---|
89 | λp,p',prog. |
---|
90 | joint_abstract_status (lin_prog_params p p' prog). |
---|
91 | |
---|
92 | (*CSC: BUG, the natural must be ≤ 2^16! *) |
---|
93 | (*CSC: already defined? *) |
---|
94 | definition pointer_of_block_and_lin_offset : |
---|
95 | ∀b:block. block_region b = Code → nat → cpointer ≝ |
---|
96 | λb,p,n. «mk_pointer b (mk_offset (bitvector_of_nat … n)), p». |
---|
97 | |
---|
98 | definition well_formed_status: |
---|
99 | ∀p,p',graph_prog. |
---|
100 | ∀sigma: identifier LabelTag → option ℕ. |
---|
101 | graph_abstract_status p p' graph_prog → Prop |
---|
102 | ≝ |
---|
103 | λp,p',graph_prog,sigma,s. |
---|
104 | sigma (point_of_pointer ? (make_sem_graph_params … (mk_graph_params … p) p') (pc ? s)) |
---|
105 | ≠ None …. |
---|
106 | |
---|
107 | definition sigma_pc_of_status: |
---|
108 | ∀p,p',graph_prog. |
---|
109 | ∀sigma: identifier LabelTag → option ℕ. |
---|
110 | ∀s:graph_abstract_status p p' graph_prog. |
---|
111 | well_formed_status … sigma s → ℕ |
---|
112 | ≝ |
---|
113 | λp,p',prog,sigma,s. |
---|
114 | match sigma (point_of_pointer ? (make_sem_graph_params … (mk_graph_params … p) p') (pc ? s)) |
---|
115 | return λx. x ≠ None ? → ℕ |
---|
116 | with |
---|
117 | [ None ⇒ λprf.⊥ |
---|
118 | | Some n ⇒ λ_.n ]. |
---|
119 | @(absurd ?? prf) // |
---|
120 | qed. |
---|
121 | |
---|
122 | lemma sigma_pc_of_status_ok: |
---|
123 | ∀p,p',graph_prog. |
---|
124 | ∀sigma: identifier LabelTag → option ℕ. |
---|
125 | ∀s:graph_abstract_status p p' graph_prog. |
---|
126 | ∀prf:well_formed_status … sigma s. |
---|
127 | sigma (point_of_pointer ? (make_sem_graph_params … (mk_graph_params … p) p') (pc ? s)) |
---|
128 | = Some … (sigma_pc_of_status … prf). |
---|
129 | #p #p' #prog #sigma #s whd in ⊢ (% → ?); |
---|
130 | whd in match sigma_pc_of_status; normalize nodelta cases (sigma ?) // |
---|
131 | #abs cases (absurd ?? abs) |
---|
132 | qed. |
---|
133 | |
---|
134 | definition linearise_status_fun: |
---|
135 | ∀p,p',graph_prog. |
---|
136 | ∀sigma: identifier LabelTag → option ℕ. |
---|
137 | let lin_prog ≝ linearise ? graph_prog in |
---|
138 | ∀s:graph_abstract_status p p' graph_prog. |
---|
139 | well_formed_status … sigma s → |
---|
140 | lin_abstract_status p p' lin_prog |
---|
141 | ≝ |
---|
142 | λp,p',graph_prog,sigma,s,prf. |
---|
143 | mk_state_pc ?? |
---|
144 | (pointer_of_block_and_lin_offset (pblock (pc ? s)) … |
---|
145 | (sigma_pc_of_status … sigma … prf)). |
---|
146 | [2: cases (pc ??) * normalize // |
---|
147 | | cases daemon (* TODO *) ] |
---|
148 | qed. |
---|
149 | |
---|
150 | axiom sigma_pc_commute: |
---|
151 | ∀p,p',graph_prog,s1,prf. |
---|
152 | sigma_pc_of_status p p' graph_prog (choose_sigma p p' graph_prog) s1 prf = |
---|
153 | point_of_pointer (lin_prog_params p p' (linearise p graph_prog)) |
---|
154 | (lin_prog_params p p' (linearise p graph_prog)) |
---|
155 | (pc (lin_prog_params p p' (linearise p graph_prog)) |
---|
156 | (linearise_status_fun p p' graph_prog (choose_sigma p p' graph_prog) s1 prf)). |
---|
157 | |
---|
158 | definition linearise_status_rel: |
---|
159 | ∀p,p',graph_prog. |
---|
160 | ∀sigma: identifier LabelTag → option ℕ. |
---|
161 | let lin_prog ≝ linearise ? graph_prog in |
---|
162 | status_rel |
---|
163 | (graph_abstract_status p p' graph_prog) |
---|
164 | (lin_abstract_status p p' lin_prog) |
---|
165 | ≝ λp,p',graph_prog,sigma.mk_status_rel … |
---|
166 | (λs1,s2. |
---|
167 | ∃prf: well_formed_status … sigma s1. |
---|
168 | s2 = linearise_status_fun p p' graph_prog sigma s1 prf) …. |
---|
169 | cases daemon (* TODO *) |
---|
170 | qed. |
---|
171 | |
---|
172 | axiom fetch_function_sigma_commute: |
---|
173 | ∀p,p',graph_prog,sigma,st1. |
---|
174 | ∀prf:well_formed_status ??? sigma st1. |
---|
175 | let lin_prog ≝ linearise ? graph_prog in |
---|
176 | fetch_function |
---|
177 | (lin_prog_params p p' lin_prog) |
---|
178 | (globals (lin_prog_params p p' lin_prog)) |
---|
179 | (ev_genv (lin_prog_params p p' lin_prog)) |
---|
180 | (pc (lin_prog_params p p' lin_prog) |
---|
181 | (linearise_status_fun p p' graph_prog sigma st1 prf)) |
---|
182 | = |
---|
183 | m_map … |
---|
184 | (linearise_int_fun ??) |
---|
185 | (fetch_function |
---|
186 | (graph_prog_params p p' graph_prog) |
---|
187 | (globals (graph_prog_params p p' graph_prog)) |
---|
188 | (ev_genv (graph_prog_params p p' graph_prog)) |
---|
189 | (pc (graph_prog_params p p' graph_prog) st1)). |
---|
190 | |
---|
191 | lemma stm_at_sigma_commute: |
---|
192 | ∀p,p',graph_prog,graph_fun,s1. |
---|
193 | let lin_prog ≝ linearise ? graph_prog in |
---|
194 | let sigma ≝ choose_sigma p p' graph_prog in |
---|
195 | ∀prf:well_formed_status ??? sigma s1. |
---|
196 | stmt_at (lin_prog_params p p' (linearise p graph_prog)) |
---|
197 | (globals (lin_prog_params p p' (linearise p graph_prog))) |
---|
198 | (joint_if_code (lin_prog_params p p' (linearise p graph_prog)) |
---|
199 | (globals (lin_prog_params p p' (linearise p graph_prog))) |
---|
200 | (linearise_int_fun p (globals (graph_prog_params p p' graph_prog)) graph_fun)) |
---|
201 | (point_of_pointer (lin_prog_params p p' (linearise p graph_prog)) |
---|
202 | (lin_prog_params p p' (linearise p graph_prog)) |
---|
203 | (pc (lin_prog_params p p' (linearise p graph_prog)) |
---|
204 | (linearise_status_fun p p' graph_prog sigma s1 prf))) |
---|
205 | = |
---|
206 | option_map … |
---|
207 | (graph_to_lin_statement …) |
---|
208 | (stmt_at (graph_prog_params p p' graph_prog) |
---|
209 | (globals (graph_prog_params p p' graph_prog)) |
---|
210 | (joint_if_code (graph_prog_params p p' graph_prog) |
---|
211 | (globals (graph_prog_params p p' graph_prog)) graph_fun) |
---|
212 | (point_of_pointer (graph_prog_params p p' graph_prog) |
---|
213 | (graph_prog_params p p' graph_prog) |
---|
214 | (pc (graph_prog_params p p' graph_prog) s1))). |
---|
215 | #p #p' #graph_prog #graph_fun #s1 #prf |
---|
216 | whd in match (stmt_at ????); |
---|
217 | whd in match (stmt_at ????); |
---|
218 | cases (linearise_code_spec … p' graph_prog graph_fun |
---|
219 | (joint_if_entry … graph_fun)) |
---|
220 | * #lin_code_closed #sigma_entry_is_zero #sigma_spec |
---|
221 | lapply (sigma_spec |
---|
222 | (point_of_pointer ? (graph_prog_params … p' graph_prog) (pc … s1))) |
---|
223 | -sigma_spec #sigma_spec cases (sigma_spec ??) [3: @(sigma_pc_of_status_ok … prf) |2: skip ] |
---|
224 | -sigma_spec #graph_stmt * #graph_lookup_ok >graph_lookup_ok -graph_lookup_ok |
---|
225 | whd in ⊢ (? → ???%); #sigma_spec whd in sigma_spec; |
---|
226 | inversion (nth_opt ???) in sigma_spec; [ #H whd in ⊢ (% → ?); #abs cases abs ] |
---|
227 | * #optlabel #lin_stm #lin_lookup_ok whd in ⊢ (% → ?); ** #_ |
---|
228 | #related_lin_stm_graph_stm #_ <related_lin_stm_graph_stm -related_lin_stm_graph_stm |
---|
229 | <sigma_pc_commute >lin_lookup_ok // |
---|
230 | qed. |
---|
231 | |
---|
232 | lemma fetch_statement_sigma_commute: |
---|
233 | ∀p,p',graph_prog,st1. |
---|
234 | let sigma ≝ choose_sigma p p' graph_prog in |
---|
235 | let lin_prog ≝ linearise ? graph_prog in |
---|
236 | ∀prf. |
---|
237 | fetch_statement |
---|
238 | (lin_prog_params p p' lin_prog) |
---|
239 | (lin_prog_params p p' lin_prog) |
---|
240 | (globals (lin_prog_params p p' lin_prog)) |
---|
241 | (ev_genv (lin_prog_params p p' lin_prog)) |
---|
242 | (pc (lin_prog_params p p' lin_prog) |
---|
243 | (linearise_status_fun p p' graph_prog sigma st1 prf)) |
---|
244 | = |
---|
245 | m_map … |
---|
246 | (λfun_stm. |
---|
247 | let 〈fun,stm〉 ≝ fun_stm in |
---|
248 | 〈linearise_int_fun ?? fun, graph_to_lin_statement ?? stm〉) |
---|
249 | (fetch_statement |
---|
250 | (graph_prog_params p p' graph_prog) |
---|
251 | (graph_prog_params p p' graph_prog) |
---|
252 | (globals (graph_prog_params p p' graph_prog)) |
---|
253 | (ev_genv (graph_prog_params p p' graph_prog)) |
---|
254 | (pc (graph_prog_params p p' graph_prog) st1)). |
---|
255 | #p #p' #graph_prog #s1 #prf |
---|
256 | whd in match fetch_statement; normalize nodelta |
---|
257 | >fetch_function_sigma_commute |
---|
258 | cases (fetch_function ????) [2://] |
---|
259 | #graph_fun whd in ⊢ (??%%); |
---|
260 | whd in ⊢ (???(match % with [ _ ⇒ ? | _ ⇒ ?])); |
---|
261 | >stm_at_sigma_commute cases (stmt_at ????) // |
---|
262 | qed. |
---|
263 | |
---|
264 | lemma linearise_ok: |
---|
265 | ∀p,p',graph_prog. |
---|
266 | let lin_prog ≝ linearise ? graph_prog in |
---|
267 | status_simulation |
---|
268 | (graph_abstract_status p p' graph_prog) |
---|
269 | (lin_abstract_status p p' lin_prog) ≝ |
---|
270 | λp,p',graph_prog. |
---|
271 | let sigma ≝ choose_sigma p p' graph_prog in |
---|
272 | mk_status_simulation … (linearise_status_rel p p' graph_prog sigma) …. |
---|
273 | #st1 #cl #st1' #st2 #move_st1_st1' #rel_st1_st2 #classified_st1_cl |
---|
274 | cases cl in classified_st1_cl; -cl #classified_st1_cl whd |
---|
275 | [4: |
---|
276 | cases rel_st1_st2 -rel_st1_st2 #wf_st1 #rel_st1_st2 >rel_st1_st2 -st2 |
---|
277 | whd in move_st1_st1'; |
---|
278 | letin lin_prog ≝ (linearise ? graph_prog) |
---|
279 | letin st2' ≝ (eval_state (globals (lin_prog_params p p' lin_prog)) … |
---|
280 | (ev_genv (lin_prog_params p p' lin_prog)) |
---|
281 | (linearise_status_fun … sigma st1 wf_st1)) |
---|
282 | whd in st2'; |
---|
283 | whd in match (fetch_statement ?????) in st2'; |
---|
284 | >fetch_function_sigma_commute in st2'; |
---|
285 | whd in match (fetch_function ????) in st2'; |
---|
286 | XXX |
---|
287 | check fetch_statement |
---|
288 | CSC |
---|
289 | %{} |
---|
290 | |
---|
291 | whd in classified_st1_cl; |
---|
292 | whd in classified_st1_cl:(??%?); |
---|
293 | inversion (fetch_statement ?????) in classified_st1_cl; |
---|
294 | |
---|
295 | <classified_st1_cl -cl |
---|
296 | whd in ⊢ (match % with [_ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ] ?); |
---|
297 | inversion (fetch_statement ?????) |
---|
298 | |
---|
299 | inversion (fetch_statement ?????) |
---|
300 | qed. |
---|