source: src/joint/lineariseProof.ma @ 2447

Last change on this file since 2447 was 2447, checked in by piccolo, 7 years ago

All axioms opened so far and that must be closed here have been
closed.

File size: 12.0 KB
Line 
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
15include "joint/linearise.ma".
16include "common/StatusSimulation.ma".   
17include "joint/Traces.ma".
18include "joint/SemanticUtils.ma".
19
20definition 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
31definition 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*)
43axiom 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*)
50axiom 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   
74definition 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
83definition 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? *)
94definition 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
98definition 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
107definition 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) //
120qed.
121
122lemma 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)
132qed.
133
134definition 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 *) ]
148qed.
149
150lemma 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#p #p' #prog #s #prf whd in ⊢ (??%%); change with (? = nat_of_bitvector ??);
158whd in match (pc … (linearise_status_fun …));
159>nat_of_bitvector_bitvector_of_nat_inverse //
160cases daemon (* CSC: Paolo, you must prove this additional invariant! *)
161qed.
162
163definition linearise_status_rel:
164 ∀p,p',graph_prog.
165  ∀sigma: identifier LabelTag → option ℕ.
166  let lin_prog ≝ linearise ? graph_prog in
167   status_rel
168    (graph_abstract_status p p' graph_prog)
169    (lin_abstract_status p p' lin_prog)
170 ≝ λp,p',graph_prog,sigma.mk_status_rel …
171    (λs1,s2.
172     ∃prf: well_formed_status … sigma s1.
173      s2 = linearise_status_fun p p' graph_prog sigma s1 prf) ….
174 cases daemon (* TODO *)
175qed.
176
177(* To be added to common/Globalenvs, it strenghtens
178   find_funct_ptr_transf *)
179lemma
180  find_funct_ptr_transf_eq:
181    ∀A,B,V,iV. ∀p: program A V. ∀transf: (∀vs. A vs → B vs).
182    ∀b: block.
183    find_funct_ptr ? (globalenv … iV (transform_program … p transf)) b =
184     m_map ???
185      (transf …)
186      (find_funct_ptr ? (globalenv … iV p) b).
187 #A #B #V #iV #p #transf #b inversion (find_funct_ptr ???) in ⊢ (???%);
188 [ cases daemon (* TODO in Globalenvs.ma *)
189 | #f #H >(find_funct_ptr_transf A B … H) // ]
190qed.
191
192lemma fetch_function_sigma_commute:
193 ∀p,p',graph_prog,sigma,st1.
194 ∀prf:well_formed_status ??? sigma st1.
195 let lin_prog ≝ linearise ? graph_prog in
196  fetch_function
197   (lin_prog_params p p' lin_prog)
198   (globals (lin_prog_params p p' lin_prog))
199   (ev_genv (lin_prog_params p p' lin_prog))
200   (pc (lin_prog_params p p' lin_prog)
201    (linearise_status_fun p p' graph_prog sigma st1 prf))
202 =
203  m_map …
204   (linearise_int_fun ??)
205   (fetch_function
206    (graph_prog_params p p' graph_prog)
207    (globals (graph_prog_params p p' graph_prog))
208    (ev_genv (graph_prog_params p p' graph_prog))
209    (pc (graph_prog_params p p' graph_prog) st1)).
210#p #p' #prog #sigma #st #prf whd in match fetch_function; normalize nodelta
211whd in match function_of_block; normalize nodelta
212>(find_funct_ptr_transf_eq … (λglobals.transf_fundef … (linearise_int_fun … globals)) …)
213cases (find_funct_ptr ???) // * //
214qed.
215
216lemma stm_at_sigma_commute:
217 ∀p,p',graph_prog,graph_fun,s1.
218 let lin_prog ≝ linearise ? graph_prog in
219 let sigma ≝ choose_sigma p p' graph_prog in
220 ∀prf:well_formed_status ??? sigma s1.
221  stmt_at (lin_prog_params p p' (linearise p graph_prog))
222   (globals (lin_prog_params p p' (linearise p graph_prog)))
223   (joint_if_code (lin_prog_params p p' (linearise p graph_prog))
224    (globals (lin_prog_params p p' (linearise p graph_prog)))
225    (linearise_int_fun p (globals (graph_prog_params p p' graph_prog)) graph_fun))
226   (point_of_pointer (lin_prog_params p p' (linearise p graph_prog))
227    (lin_prog_params p p' (linearise p graph_prog))
228    (pc (lin_prog_params p p' (linearise p graph_prog))
229     (linearise_status_fun p p' graph_prog sigma s1 prf)))
230 =
231  option_map …
232   (graph_to_lin_statement …)
233   (stmt_at (graph_prog_params p p' graph_prog)
234    (globals (graph_prog_params p p' graph_prog))
235    (joint_if_code (graph_prog_params p p' graph_prog)
236     (globals (graph_prog_params p p' graph_prog)) graph_fun)
237    (point_of_pointer (graph_prog_params p p' graph_prog)
238     (graph_prog_params p p' graph_prog)
239     (pc (graph_prog_params p p' graph_prog) s1))).
240 #p #p' #graph_prog #graph_fun #s1 #prf
241 whd in match (stmt_at ????);
242 whd in match (stmt_at ????);
243 cases (linearise_code_spec … p' graph_prog graph_fun
244         (joint_if_entry … graph_fun))
245 * #lin_code_closed #sigma_entry_is_zero #sigma_spec
246 lapply (sigma_spec
247         (point_of_pointer ? (graph_prog_params … p' graph_prog) (pc … s1)))
248 -sigma_spec #sigma_spec cases (sigma_spec ??) [3: @(sigma_pc_of_status_ok … prf) |2: skip ]
249 -sigma_spec #graph_stmt * #graph_lookup_ok >graph_lookup_ok -graph_lookup_ok
250 whd in ⊢ (? → ???%); #sigma_spec whd in sigma_spec;
251 inversion (nth_opt ???) in sigma_spec; [ #H whd in ⊢ (% → ?); #abs cases abs ]
252 * #optlabel #lin_stm #lin_lookup_ok whd in ⊢ (% → ?); ** #_
253 #related_lin_stm_graph_stm #_ <related_lin_stm_graph_stm -related_lin_stm_graph_stm
254 <sigma_pc_commute >lin_lookup_ok //
255qed.
256
257lemma fetch_statement_sigma_commute:
258 ∀p,p',graph_prog,st1.
259 let sigma ≝ choose_sigma p p' graph_prog in
260 let lin_prog ≝ linearise ? graph_prog in
261 ∀prf.
262  fetch_statement
263   (lin_prog_params p p' lin_prog)
264   (lin_prog_params p p' lin_prog)
265   (globals (lin_prog_params p p' lin_prog))
266   (ev_genv (lin_prog_params p p' lin_prog))
267   (pc (lin_prog_params p p' lin_prog)
268    (linearise_status_fun p p' graph_prog sigma st1 prf))
269 =
270  m_map …
271   (λfun_stm.
272     let 〈fun,stm〉 ≝ fun_stm in
273      〈linearise_int_fun ?? fun, graph_to_lin_statement ?? stm〉)
274   (fetch_statement
275    (graph_prog_params p p' graph_prog)
276    (graph_prog_params p p' graph_prog)
277    (globals (graph_prog_params p p' graph_prog))
278    (ev_genv (graph_prog_params p p' graph_prog))
279    (pc (graph_prog_params p p' graph_prog) st1)).
280 #p #p' #graph_prog #s1 #prf
281 whd in match fetch_statement; normalize nodelta
282 >fetch_function_sigma_commute
283 cases (fetch_function ????) [2://]
284 #graph_fun whd in ⊢ (??%%);
285 whd in ⊢ (???(match % with [ _ ⇒ ? | _ ⇒ ?]));
286 >stm_at_sigma_commute cases (stmt_at ????) //
287qed.
288
289lemma linearise_ok:
290 ∀p,p',graph_prog.
291  let lin_prog ≝ linearise ? graph_prog in
292   status_simulation
293    (graph_abstract_status p p' graph_prog)
294    (lin_abstract_status p p' lin_prog) ≝
295 λp,p',graph_prog.
296  let sigma ≝ choose_sigma p p' graph_prog in
297   mk_status_simulation … (linearise_status_rel p p' graph_prog sigma) ….
298#st1 #cl #st1' #st2 #move_st1_st1' #rel_st1_st2 #classified_st1_cl
299cases cl in classified_st1_cl; -cl #classified_st1_cl whd
300[4:
301 cases rel_st1_st2 -rel_st1_st2 #wf_st1 #rel_st1_st2 >rel_st1_st2 -st2
302 whd in move_st1_st1';
303 letin lin_prog ≝ (linearise ? graph_prog)
304 letin st2' ≝ (eval_state (globals (lin_prog_params p p' lin_prog)) …
305               (ev_genv (lin_prog_params p p' lin_prog))
306               (linearise_status_fun … sigma st1 wf_st1))
307 whd in st2';
308 whd in match (fetch_statement ?????) in st2';
309 >fetch_function_sigma_commute in st2';
310 whd in match (fetch_function ????) in st2';
311 XXX
312 check fetch_statement
313 CSC
314 %{}
315
316whd in classified_st1_cl;
317whd in classified_st1_cl:(??%?);
318inversion (fetch_statement ?????) in classified_st1_cl;
319
320<classified_st1_cl -cl
321whd in ⊢ (match % with [_ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ] ?);
322inversion (fetch_statement ?????)
323
324inversion (fetch_statement ?????)
325qed.
Note: See TracBrowser for help on using the repository browser.