source: src/joint/lineariseProof.ma @ 2446

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

Fetch commutation proof reduced to one simple (?) lemma.

File size: 11.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
150axiom 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
158definition 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 *)
170qed.
171
172axiom 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
191lemma 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 //
230qed.
231
232lemma 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 ????) //
262qed.
263
264lemma 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
274cases 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
291whd in classified_st1_cl;
292whd in classified_st1_cl:(??%?);
293inversion (fetch_statement ?????) in classified_st1_cl;
294
295<classified_st1_cl -cl
296whd in ⊢ (match % with [_ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ] ?);
297inversion (fetch_statement ?????)
298
299inversion (fetch_statement ?????)
300qed.
Note: See TracBrowser for help on using the repository browser.