source: src/joint/lineariseProof.ma @ 2445

Last change on this file since 2445 was 2445, checked in by piccolo, 8 years ago
  1. sigma function axiomatically defined (together with its spec). It should come from Paolo's linearise function, but there it is existentially (not sigma) quantified and Paolo's records for simulation relations are in Type and not in Prop. One of the two things need to be changed (hopefully the records...)
  2. sigma extended to statuses (PC only atm)
  3. some preliminary lemmas about commutation of sigma with fetching
File size: 9.4 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   
42definition graph_abstract_status:
43 ∀p:unserialized_params.
44  (∀F.sem_unserialized_params p F) →
45    joint_program (mk_graph_params p) →
46     abstract_status
47 ≝
48 λp,p',prog.
49  joint_abstract_status (graph_prog_params p p' prog).
50
51definition lin_abstract_status:
52 ∀p:unserialized_params.
53  (∀F.sem_unserialized_params p F) →
54    joint_program (mk_lin_params p) →
55     abstract_status
56 ≝
57 λp,p',prog.
58  joint_abstract_status (lin_prog_params p p' prog).
59
60(*CSC: BUG, the natural must be ≤ 2^16! *)
61(*CSC: already defined? *)
62definition pointer_of_block_and_lin_offset :
63 ∀b:block. block_region b = Code → nat → cpointer ≝
64  λb,p,n. «mk_pointer b (mk_offset (bitvector_of_nat … n)), p».
65
66definition well_formed_status:
67 ∀p,p',graph_prog.
68  ∀sigma: identifier LabelTag → option ℕ.
69  graph_abstract_status p p' graph_prog → Prop
70 ≝
71 λp,p',graph_prog,sigma,s.
72  sigma (point_of_pointer ? (make_sem_graph_params … (mk_graph_params … p) p') (pc ? s))
73   ≠ None ….
74
75definition sigma_pc_of_status:
76 ∀p,p',graph_prog.
77  ∀sigma: identifier LabelTag → option ℕ.
78   ∀s:graph_abstract_status p p' graph_prog.
79    well_formed_status … sigma s → ℕ
80 ≝
81  λp,p',prog,sigma,s.
82   match sigma (point_of_pointer ? (make_sem_graph_params … (mk_graph_params … p) p') (pc ? s))
83   return λx. x ≠ None ? → ℕ
84   with
85   [ None ⇒ λprf.⊥
86   | Some n ⇒ λ_.n ].
87 @(absurd ?? prf) //
88qed.
89   
90definition linearise_status_fun:
91 ∀p,p',graph_prog.
92  ∀sigma: identifier LabelTag → option ℕ.
93   let lin_prog ≝ linearise ? graph_prog in
94    ∀s:graph_abstract_status p p' graph_prog.
95     well_formed_status … sigma s →
96      lin_abstract_status p p' lin_prog
97
98 λp,p',graph_prog,sigma,s,prf.
99  mk_state_pc ??
100   (pointer_of_block_and_lin_offset (pblock (pc ? s)) …
101    (sigma_pc_of_status … sigma … prf)).
102[2: cases (pc ??) * normalize //
103| cases daemon (* TODO *) ]
104qed.
105
106definition linearise_status_rel:
107 ∀p,p',graph_prog.
108  ∀sigma: identifier LabelTag → option ℕ.
109  let lin_prog ≝ linearise ? graph_prog in
110   status_rel
111    (graph_abstract_status p p' graph_prog)
112    (lin_abstract_status p p' lin_prog)
113 ≝ λp,p',graph_prog,sigma.mk_status_rel …
114    (λs1,s2.
115     ∃prf: well_formed_status … sigma s1.
116      s2 = linearise_status_fun p p' graph_prog sigma s1 prf) ….
117 cases daemon (* TODO *)
118qed.
119
120(*CSC: Paolo, come to the rescue*)
121axiom choose_sigma:
122  ∀p:unserialized_params.
123  (∀F.sem_unserialized_params p F) →
124    joint_program (mk_graph_params p) →
125   identifier LabelTag → option ℕ.
126
127(*CSC: Paolo, come to the rescue*)
128axiom linearise_code_spec:
129 ∀p : unserialized_params.
130 ∀p':(∀F.sem_unserialized_params p F).
131 ∀graph_prog:joint_program (mk_graph_params p).
132 ∀graph_fun:joint_closed_internal_function (mk_graph_params p)
133                           (globals (graph_prog_params p p' graph_prog)).
134 let sigma ≝ choose_sigma p p' graph_prog in
135 let lin_fun ≝ linearise_int_fun … graph_fun in
136 let g ≝ joint_if_code ?? (pi1 … graph_fun) in
137 let c ≝ joint_if_code ?? (pi1 … lin_fun) in
138 ∀entry : (Σl.bool_to_Prop (code_has_label … g l)).
139      code_closed … c ∧
140      sigma entry = Some ? 0 ∧
141      ∀l,n.sigma l = Some ? n →
142        ∃s. lookup … g l = Some ? s ∧
143          opt_Exists ?
144            (λls.let 〈lopt, ts〉 ≝ ls in
145              opt_All ? (eq ? l) lopt ∧
146              ts = graph_to_lin_statement … s ∧
147              opt_All ?
148                (λnext.Or (sigma next = Some ? (S n))
149                (nth_opt … (S n) c = Some ? 〈None ?, GOTO … next〉))
150                (stmt_implicit_label … s)) (nth_opt … n c).
151
152axiom fetch_function_sigma_commute:
153 ∀p,p',graph_prog,sigma,st1.
154 ∀prf:well_formed_status ??? sigma st1.
155 let lin_prog ≝ linearise ? graph_prog in
156  fetch_function
157   (lin_prog_params p p' lin_prog)
158   (globals (lin_prog_params p p' lin_prog))
159   (ev_genv (lin_prog_params p p' lin_prog))
160   (pc (lin_prog_params p p' lin_prog)
161    (linearise_status_fun p p' graph_prog sigma st1 prf))
162 =
163  m_map …
164   (linearise_int_fun ??)
165   (fetch_function
166    (graph_prog_params p p' graph_prog)
167    (globals (graph_prog_params p p' graph_prog))
168    (ev_genv (graph_prog_params p p' graph_prog))
169    (pc (graph_prog_params p p' graph_prog) st1)).
170
171lemma stm_at_sigma_commute:
172 ∀p,p',graph_prog,graph_fun,s1.
173 let lin_prog ≝ linearise ? graph_prog in
174 let sigma ≝ choose_sigma p p' graph_prog in
175 ∀prf:well_formed_status ??? sigma s1.
176  stmt_at (lin_prog_params p p' (linearise p graph_prog))
177   (globals (lin_prog_params p p' (linearise p graph_prog)))
178   (joint_if_code (lin_prog_params p p' (linearise p graph_prog))
179    (globals (lin_prog_params p p' (linearise p graph_prog)))
180    (linearise_int_fun p (globals (graph_prog_params p p' graph_prog)) graph_fun))
181   (point_of_pointer (lin_prog_params p p' (linearise p graph_prog))
182    (lin_prog_params p p' (linearise p graph_prog))
183    (pc (lin_prog_params p p' (linearise p graph_prog))
184     (linearise_status_fun p p' graph_prog sigma s1 prf)))
185 =
186  option_map …
187   (graph_to_lin_statement …)
188   (stmt_at (graph_prog_params p p' graph_prog)
189    (globals (graph_prog_params p p' graph_prog))
190    (joint_if_code (graph_prog_params p p' graph_prog)
191     (globals (graph_prog_params p p' graph_prog)) graph_fun)
192    (point_of_pointer (graph_prog_params p p' graph_prog)
193     (graph_prog_params p p' graph_prog)
194     (pc (graph_prog_params p p' graph_prog) s1))).
195 #p #p' #graph_prog #graph_fun #s1 #prf
196 whd in match (stmt_at ????);
197 whd in match (stmt_at ????);
198
199================================
200  normalize nodelta
201
202lemma fetch_statement_sigma_commute:
203 ∀p,p',graph_prog,sigma,st1.
204 let lin_prog ≝ linearise ? graph_prog in
205  fetch_statement
206   (lin_prog_params p p' lin_prog)
207   (lin_prog_params p p' lin_prog)
208   (globals (lin_prog_params p p' lin_prog))
209   (ev_genv (lin_prog_params p p' lin_prog))
210   (pc (lin_prog_params p p' lin_prog)
211    (linearise_status_fun p p' graph_prog sigma st1))
212 =
213  m_map …
214   (λfun_stm.
215     let 〈fun,stm〉 ≝ fun_stm in
216      〈linearise_int_fun ?? fun, graph_to_lin_statement ?? stm〉)
217   (fetch_statement
218    (graph_prog_params p p' graph_prog)
219    (graph_prog_params p p' graph_prog)
220    (globals (graph_prog_params p p' graph_prog))
221    (ev_genv (graph_prog_params p p' graph_prog))
222    (pc (graph_prog_params p p' graph_prog) st1)).
223 #p #p' #graph_prog #sigma #s1
224 whd in match fetch_statement; normalize nodelta
225 >fetch_function_sigma_commute
226 cases (fetch_function ????) [2://]
227 #graph_fun whd in ⊢ (??%%);
228 whd in ⊢ (???(match % with [ _ ⇒ ? | _ ⇒ ?]));
229 >stm_at_sigma_commute
230 cases (stmt_at ????) //
231qed.
232
233lemma linearise_ok:
234 ∀p,p',graph_prog.
235  let lin_prog ≝ linearise ? graph_prog in
236   status_simulation
237    (graph_abstract_status p p' graph_prog)
238    (lin_abstract_status p p' lin_prog) ≝
239 λp,p',graph_prog.
240  let sigma ≝ choose_sigma p p' graph_prog in
241   mk_status_simulation … (linearise_status_rel p p' graph_prog sigma) ….
242#st1 #cl #st1' #st2 #move_st1_st1' #rel_st1_st2 #classified_st1_cl
243cases cl in classified_st1_cl; -cl #classified_st1_cl whd
244[4:
245 whd in rel_st1_st2; >rel_st1_st2 -st2
246 whd in move_st1_st1';
247 letin lin_prog ≝ (linearise ? graph_prog)
248 letin st2' ≝ (eval_state (globals (lin_prog_params p p' lin_prog)) …
249               (ev_genv (lin_prog_params p p' lin_prog))
250               (linearise_status_fun … sigma st1))
251 whd in st2';
252 whd in match (fetch_statement ?????) in st2';
253 >fetch_function_sigma_commute in st2';
254 whd in match (fetch_function ????) in st2';
255 XXX
256 check fetch_statement
257 CSC
258 %{}
259
260whd in classified_st1_cl;
261whd in classified_st1_cl:(??%?);
262inversion (fetch_statement ?????) in classified_st1_cl;
263
264<classified_st1_cl -cl
265whd in ⊢ (match % with [_ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ] ?);
266inversion (fetch_statement ?????)
267
268inversion (fetch_statement ?????)
269qed.
Note: See TracBrowser for help on using the repository browser.