1 | include "joint/joint_semantics.ma". |
---|
2 | include "common/StructuredTraces.ma". |
---|
3 | |
---|
4 | record evaluation_params : Type[1] ≝ |
---|
5 | { globals: list ident |
---|
6 | ; sparams:> sem_params |
---|
7 | ; ev_genv: genv sparams globals |
---|
8 | (* ; io_env : state sparams → ∀o:io_out.res (io_in o) *) |
---|
9 | }. |
---|
10 | |
---|
11 | |
---|
12 | |
---|
13 | record prog_params : Type[1] ≝ |
---|
14 | { prog_spars : sem_params |
---|
15 | ; prog : joint_program prog_spars |
---|
16 | ; stack_sizes : ident → option ℕ |
---|
17 | (* ; prog_io : state prog_spars → ∀o.res (io_in o) *) |
---|
18 | }. |
---|
19 | |
---|
20 | lemma map_Exists : ∀A,B,f,P,l.Exists B P (map A B f l) → Exists ? (λx.P (f x)) l. |
---|
21 | #A #B #f #P #l elim l -l [*] |
---|
22 | #hd #tl #IH * |
---|
23 | [ #Phd %1{Phd} |
---|
24 | | #Ptl %2{(IH Ptl)} |
---|
25 | ] |
---|
26 | qed. |
---|
27 | |
---|
28 | lemma Exists_In : ∀A,P,l.Exists A P l → ∃x.In A l x ∧ P x. |
---|
29 | #A #P #l elim l -l [*] #hd #tl #IH * |
---|
30 | [ #Phd %{hd} %{Phd} %1 % |
---|
31 | | #Ptl elim (IH Ptl) #x * #H1 #H2 %{x} %{H2} %2{H1} |
---|
32 | ] |
---|
33 | qed. |
---|
34 | |
---|
35 | lemma In_Exists : ∀A,P,l,x.In A l x → P x → Exists A P l. |
---|
36 | #A #P #l elim l -l [ #x *] #hd #tl #IH #x * |
---|
37 | [ #EQ >EQ #H %1{H} |
---|
38 | | #Intl #Px %2{(IH … Intl Px)} |
---|
39 | ] |
---|
40 | qed. |
---|
41 | |
---|
42 | lemma Exists_mp : ∀A,P,Q,l.(∀x.P x → Q x) → Exists A P l → Exists A Q l. |
---|
43 | #A #P #Q #l #H elim l -l [*] #hd #tl #IH * #G [ %1 | %2 ] /2/ qed. |
---|
44 | |
---|
45 | definition make_global : prog_params → evaluation_params |
---|
46 | ≝ |
---|
47 | λpars. |
---|
48 | let p ≝ prog pars in |
---|
49 | let spars ≝ prog_spars pars in |
---|
50 | let genv ≝ globalenv_noinit ? p in |
---|
51 | let get_pc_lbl ≝ λid,lbl. |
---|
52 | ! bl ← block_of_funct_id … spars genv id ; |
---|
53 | pc_of_label … genv bl lbl in |
---|
54 | mk_evaluation_params |
---|
55 | (prog_var_names … p) |
---|
56 | spars |
---|
57 | (mk_genv_gen ?? genv ? (stack_sizes pars) get_pc_lbl) |
---|
58 | (* (prog_io pars) *). |
---|
59 | #s #H |
---|
60 | elim (find_symbol_exists … p s ?) |
---|
61 | [ #bl #EQ >EQ % #ABS destruct(ABS)|*:] |
---|
62 | @Exists_append_r |
---|
63 | @(Exists_mp … H) // |
---|
64 | qed. |
---|
65 | |
---|
66 | coercion prog_params_to_ev_params : ∀p : prog_params.evaluation_params |
---|
67 | ≝ make_global on _p : prog_params to evaluation_params. |
---|
68 | |
---|
69 | definition make_initial_state : |
---|
70 | ∀pars: prog_params.res (state_pc pars) ≝ |
---|
71 | λpars.let p ≝ prog pars in |
---|
72 | let sem_globals : evaluation_params ≝ pars in |
---|
73 | let ge ≝ ev_genv sem_globals in |
---|
74 | let m0 ≝ alloc_mem … p in |
---|
75 | let 〈m,spb〉 as H ≝ alloc … m0 0 external_ram_size in |
---|
76 | let spp : xpointer ≝ |
---|
77 | «mk_pointer spb (mk_offset (bitvector_of_Z ? external_ram_size)), |
---|
78 | pi2 … spb» in |
---|
79 | (* let ispp : xpointer ≝ mk_pointer ispb (mk_offset (bitvector_of_nat ? 47)) in *) |
---|
80 | let main ≝ prog_main … p in |
---|
81 | let st0 ≝ mk_state pars (empty_framesT …) empty_is (BBbit false) (empty_regsT … spp) m in |
---|
82 | (* use exit_pc as ra and call_dest_for_main as dest *) |
---|
83 | let st0' ≝ mk_state_pc … (set_sp … spp st0) exit_pc exit_pc in |
---|
84 | ! st0_no_pc ← save_frame ?? sem_globals ID (call_dest_for_main … pars) (prog_main … p) st0' ; |
---|
85 | let st0'' ≝ set_no_pc … st0_no_pc st0' in |
---|
86 | ! bl ← block_of_call … ge (inl … main) st0''; |
---|
87 | ! 〈i, fn〉 ← fetch_function … ge bl ; |
---|
88 | match fn with |
---|
89 | [ Internal ifn ⇒ |
---|
90 | ! st' ← eval_internal_call … ge i ifn (call_args_for_main … pars) st0'' ; |
---|
91 | let pc' ≝ pc_of_point … bl (joint_if_entry … ifn) in |
---|
92 | return mk_state_pc … st' pc' exit_pc |
---|
93 | | External _ ⇒ Error … [MSG BadMain; CTX ? main] (* External main not supported: why? *) |
---|
94 | ]. |
---|
95 | cases m0 in H; #m1 #m2 #m3 #H |
---|
96 | whd in H:(???%); destruct whd in ⊢(??%?); @Zleb_elim_Type0 // #abs @⊥ |
---|
97 | @(absurd … (irreflexive_Zlt …)) % #I cases (I OZ) /3 by Zlt_to_Zle_to_Zlt/ |
---|
98 | qed. |
---|
99 | |
---|
100 | definition joint_classify_step : |
---|
101 | ∀p : evaluation_params.state p → joint_step p (globals … p) → status_class ≝ |
---|
102 | λp,st,stmt. |
---|
103 | match stmt with |
---|
104 | [ step_seq _ ⇒ cl_other |
---|
105 | | CALL f args dest ⇒ |
---|
106 | match (! bl ← block_of_call … (ev_genv p) f st ; |
---|
107 | fetch_function … (ev_genv p) bl) with |
---|
108 | [ OK id_fn ⇒ |
---|
109 | match \snd id_fn with |
---|
110 | [ Internal _ ⇒ cl_call |
---|
111 | | External _ ⇒ cl_other |
---|
112 | ] |
---|
113 | | Error _ ⇒ cl_other |
---|
114 | ] |
---|
115 | | COND _ _ ⇒ cl_jump |
---|
116 | ]. |
---|
117 | |
---|
118 | definition joint_classify_final : |
---|
119 | ∀p : evaluation_params.state p → joint_fin_step p → status_class ≝ |
---|
120 | λp,st,stmt. |
---|
121 | match stmt with |
---|
122 | [ GOTO _ ⇒ cl_other |
---|
123 | | RETURN ⇒ cl_return |
---|
124 | | TAILCALL _ f args ⇒ |
---|
125 | match (! bl ← block_of_call … (ev_genv p) f st ; |
---|
126 | fetch_function … (ev_genv p) bl) with |
---|
127 | [ OK id_fn ⇒ |
---|
128 | match \snd id_fn with |
---|
129 | [ Internal _ ⇒ cl_tailcall |
---|
130 | | External _ ⇒ cl_return |
---|
131 | ] |
---|
132 | | Error _ ⇒ cl_other |
---|
133 | ] |
---|
134 | ]. |
---|
135 | |
---|
136 | definition joint_classify : |
---|
137 | ∀p : evaluation_params.state_pc p → option status_class ≝ |
---|
138 | λp,st. |
---|
139 | ! 〈i,f,s〉 ← res_to_opt … (fetch_statement … (ev_genv p) (pc … st)) ; |
---|
140 | match s with |
---|
141 | [ sequential s _ ⇒ Some ? (joint_classify_step p st s) |
---|
142 | | final s ⇒ Some ? (joint_classify_final p st s) |
---|
143 | | FCOND _ _ _ _ ⇒ Some ? cl_jump |
---|
144 | ]. |
---|
145 | |
---|
146 | definition no_cost_label : ∀p,g.joint_seq p g → Prop ≝ |
---|
147 | λp,g,s.match s with |
---|
148 | [ COST_LABEL _ ⇒ False |
---|
149 | | _ ⇒ True |
---|
150 | ]. |
---|
151 | |
---|
152 | lemma joint_classify_call : ∀p : evaluation_params.∀st. |
---|
153 | joint_classify p st = Some ? cl_call → |
---|
154 | ∃i_f,f',args,dest,next,bl,i',fd'. |
---|
155 | fetch_statement … (ev_genv p) (pc … st) = |
---|
156 | OK ? 〈i_f, sequential … (CALL … f' args dest) next〉 ∧ |
---|
157 | block_of_call … (ev_genv p) f' st = OK ? bl ∧ |
---|
158 | fetch_internal_function … (ev_genv p) bl = OK ? 〈i', fd'〉. |
---|
159 | #p #st |
---|
160 | whd in match joint_classify; normalize nodelta |
---|
161 | inversion (fetch_statement … (ev_genv p) (pc … st)) |
---|
162 | [2: #e #_ whd in ⊢ (??%?→?); #ABS destruct(ABS) ] |
---|
163 | * #i_f * [2,3: [ * [ #lbl | | #fl #f #args ] | #fl #a #ltrue #lfalse ] #_ |
---|
164 | >m_return_bind normalize nodelta |
---|
165 | [3: whd in match joint_classify_final; normalize nodelta |
---|
166 | generalize in ⊢ (??(?? (match % with [ _ ⇒ ? | _ ⇒ ?]))?→?); * [* #i' * #fd | #e ] |
---|
167 | normalize nodelta ] |
---|
168 | #ABS destruct(ABS) ] |
---|
169 | * [ #f' #args #dest | #a #lbl | #s ] #nxt #fetch >m_return_bind |
---|
170 | normalize nodelta |
---|
171 | [2,3: normalize in ⊢ (%→?); #ABS destruct(ABS) ] |
---|
172 | whd in match joint_classify_step; |
---|
173 | normalize nodelta |
---|
174 | inversion (block_of_call ?????) |
---|
175 | [ #bl #block_of_c >m_return_bind |
---|
176 | inversion (fetch_function ???) |
---|
177 | [ * #i' * |
---|
178 | [ #fd' #fetch' #_ |
---|
179 | %{i_f} %{f'} %{args} %{dest} %{nxt} %{bl} %{i'} %{fd'} |
---|
180 | % [ %{block_of_c} % ] |
---|
181 | whd in match fetch_internal_function; normalize nodelta |
---|
182 | >fetch' % |
---|
183 | ] |
---|
184 | ] |
---|
185 | ] |
---|
186 | #x #_ normalize in ⊢ (%→?); #ABS destruct(ABS) |
---|
187 | qed. |
---|
188 | |
---|
189 | definition joint_after_ret : ∀p:evaluation_params. |
---|
190 | (Σs : state_pc p.joint_classify p s = Some ? cl_call) → state_pc p → Prop ≝ |
---|
191 | λp,s1,s2. |
---|
192 | match fetch_statement … (ev_genv p) (pc … s1) with |
---|
193 | [ OK x ⇒ |
---|
194 | match \snd x with |
---|
195 | [ sequential s next ⇒ |
---|
196 | last_pop … s2 = pc … s1 ∧ |
---|
197 | pc … s2 = succ_pc p (pc … s1) next |
---|
198 | | _ ⇒ False (* never happens *) |
---|
199 | ] |
---|
200 | | _ ⇒ False (* never happens *) |
---|
201 | ]. |
---|
202 | |
---|
203 | definition joint_call_ident : ∀p:evaluation_params. |
---|
204 | (Σs : state_pc p.joint_classify p s = Some ? cl_call) → ident ≝ |
---|
205 | (* this is a definition without a dummy ident : |
---|
206 | λp,st. |
---|
207 | match ? |
---|
208 | return λx. |
---|
209 | !〈f, s〉 ← fetch_statement ? p … (ev_genv p) (pc … st) ; |
---|
210 | match s with |
---|
211 | [ sequential s next ⇒ |
---|
212 | match s with |
---|
213 | [ step_seq s ⇒ |
---|
214 | match s with |
---|
215 | [ CALL f' args dest ⇒ |
---|
216 | function_of_call … (ev_genv p) st f' |
---|
217 | | _ ⇒ Error … [ ] |
---|
218 | ] |
---|
219 | | _ ⇒ Error … [ ] |
---|
220 | ] |
---|
221 | | _ ⇒ Error … [ ] |
---|
222 | ] = x → ? with |
---|
223 | [ OK v ⇒ λ_.v |
---|
224 | | Error e ⇒ λABS.⊥ |
---|
225 | ] (refl …). |
---|
226 | @hide_prf |
---|
227 | elim (joint_classify_call … (pi2 … st)) |
---|
228 | #f *#f' *#args *#dest *#next *#fn *#fd ** #EQ1 #EQ2 #EQ3 |
---|
229 | lapply ABS -ABS |
---|
230 | >EQ1 >m_return_bind normalize nodelta >EQ2 #ABS destruct(ABS) |
---|
231 | qed. *) |
---|
232 | (* with a dummy ident (which is never used as seen above in the commented script) |
---|
233 | I think handling of the function is easier *) |
---|
234 | λp,st. |
---|
235 | let dummy : ident ≝ an_identifier ? one in (* used where it cannot ever happen *) |
---|
236 | match fetch_statement … (ev_genv p) (pc … st) with |
---|
237 | [ OK x ⇒ |
---|
238 | match \snd x with |
---|
239 | [ sequential s next ⇒ |
---|
240 | match s with |
---|
241 | [ step_seq s ⇒ |
---|
242 | match s with |
---|
243 | [ CALL f' args dest ⇒ |
---|
244 | match |
---|
245 | (! bl ← block_of_call … (ev_genv p) f' st; |
---|
246 | fetch_internal_function … (ev_genv p) bl) with |
---|
247 | [ OK i_f ⇒ \fst i_f |
---|
248 | | _ ⇒ dummy |
---|
249 | ] |
---|
250 | | _ ⇒ dummy |
---|
251 | ] |
---|
252 | | _ ⇒ dummy |
---|
253 | ] |
---|
254 | | _ ⇒ dummy |
---|
255 | ] |
---|
256 | | _ ⇒ dummy |
---|
257 | ]. |
---|
258 | |
---|
259 | definition joint_tailcall_ident : ∀p:evaluation_params. |
---|
260 | (Σs : state_pc p.joint_classify p s = Some ? cl_tailcall) → ident ≝ |
---|
261 | λp,st. |
---|
262 | let dummy : ident ≝ an_identifier ? one in (* used where it cannot ever happen *) |
---|
263 | match fetch_statement … (ev_genv p) (pc … st) with |
---|
264 | [ OK x ⇒ |
---|
265 | match \snd x with |
---|
266 | [ final s ⇒ |
---|
267 | match s with |
---|
268 | [ TAILCALL _ f' args ⇒ |
---|
269 | match |
---|
270 | (! bl ← block_of_call … (ev_genv p) f' st; |
---|
271 | fetch_internal_function … (ev_genv p) bl) with |
---|
272 | [ OK i_f ⇒ \fst i_f |
---|
273 | | _ ⇒ dummy |
---|
274 | ] |
---|
275 | | _ ⇒ dummy |
---|
276 | ] |
---|
277 | | _ ⇒ dummy |
---|
278 | ] |
---|
279 | | _ ⇒ dummy |
---|
280 | ]. |
---|
281 | |
---|
282 | definition pcDeq ≝ mk_DeqSet program_counter eq_program_counter ?. |
---|
283 | *#p1 #EQ1 * #p2 #EQ2 @eq_program_counter_elim |
---|
284 | [ #EQ destruct % #H % |
---|
285 | | * #NEQ % #ABS destruct elim (NEQ ?) % |
---|
286 | ] |
---|
287 | qed. |
---|
288 | |
---|
289 | (* |
---|
290 | let rec io_evaluate O I X (env : ∀o.res (I o)) (c : IO O I X) on c : res X ≝ |
---|
291 | match c with |
---|
292 | [ Value x ⇒ OK … x |
---|
293 | | Interact o f ⇒ |
---|
294 | ! i ← env o ; |
---|
295 | io_evaluate O I X env (f i) |
---|
296 | | Wrong e ⇒ Error … e |
---|
297 | ]. |
---|
298 | *) |
---|
299 | |
---|
300 | definition cost_label_of_stmt : |
---|
301 | ∀p : evaluation_params.joint_statement p (globals p) → option costlabel ≝ |
---|
302 | λp,s.match s with |
---|
303 | [ sequential s _ ⇒ |
---|
304 | match s with |
---|
305 | [ step_seq s ⇒ |
---|
306 | match s with |
---|
307 | [ COST_LABEL lbl ⇒ Some ? lbl |
---|
308 | | _ ⇒ None ? |
---|
309 | ] |
---|
310 | | _ ⇒ None ? |
---|
311 | ] |
---|
312 | | _ ⇒ None ? |
---|
313 | ]. |
---|
314 | |
---|
315 | |
---|
316 | lemma no_label_uncosted : ∀p : evaluation_params.∀s,nxt. |
---|
317 | no_cost_label p (globals p) s → |
---|
318 | cost_label_of_stmt … (sequential … s nxt) = None ?. |
---|
319 | #p * // #lbl #next * |
---|
320 | qed. |
---|
321 | |
---|
322 | definition joint_abstract_status : |
---|
323 | ∀p : evaluation_params. |
---|
324 | abstract_status ≝ |
---|
325 | λp. |
---|
326 | mk_abstract_status |
---|
327 | (* as_status ≝ *) (state_pc p) |
---|
328 | (* as_execute ≝ *) |
---|
329 | (λs1,s2.(* io_evaluate … (io_env p s1) *) (eval_state … (ev_genv p) s1) = return s2) |
---|
330 | (* as_pc ≝ *) pcDeq |
---|
331 | (* as_pc_of ≝ *) (pc …) |
---|
332 | (* as_classify ≝ *) (joint_classify p) |
---|
333 | (* as_label_of_pc ≝ *) |
---|
334 | (λpc. |
---|
335 | match fetch_statement … (ev_genv p) pc with |
---|
336 | [ OK fn_stmt ⇒ cost_label_of_stmt … (\snd fn_stmt) |
---|
337 | | _ ⇒ None ? |
---|
338 | ]) |
---|
339 | (* as_after_return ≝ *) (joint_after_ret p) |
---|
340 | (* as_final ≝ *) (λs.is_final p (globals ?) (ev_genv p) exit_pc s ≠ None ?) |
---|
341 | (* as_call_ident ≝ *) (joint_call_ident p) |
---|
342 | (* as_tailcall_ident ≝ *) (joint_tailcall_ident p). |
---|