source: src/joint/semantics_blocks.ma @ 2125

Last change on this file since 2125 was 2043, checked in by sacerdot, 8 years ago

Broken code commented out.

File size: 24.9 KB
Line 
1include "joint/blocks.ma".
2include "joint/semantics_paolo.ma".
3
4
5axiom ExecutingInternalCallInBlock : String.
6
7let rec seq_list_labels p g (b : list (joint_step p g)) on b : list label ≝
8  match b with
9  [ nil ⇒ [ ]
10  | cons hd tl ⇒ step_labels … hd @ seq_list_labels … tl
11  ].
12
13definition step_flow_change_labels :
14  ∀p,g,lbls1,lbls2.(∀x.In ? lbls1 x → In ? lbls2 x) →
15    step_flow p g lbls1 → step_flow p g lbls2 ≝
16  λp,g,lbls1,lbls2,prf,flow.
17  match flow with
18  [ Redirect l ⇒ Redirect ??? «l, prf ? (pi2 … l)»
19  | Init id b args dest ⇒ Init … id b args dest
20  | Proceed ⇒ Proceed ???
21  ].
22
23coercion step_flow_diff_lbls :
24  ∀p,g,lbls1,lbls2.(∀x.In ? lbls1 x → In ? lbls2 x) →
25  ∀flow : step_flow p g lbls1.step_flow p g lbls2 ≝
26  step_flow_change_labels on _flow : step_flow ??? to step_flow ???.
27
28definition monad_step_flow_times_coerc :
29  ∀p,g,lbls1,lbls2,M,A.(∀x.In ? lbls1 x → In ? lbls2 x) →
30    monad M ((step_flow p g lbls1) × A) → monad M ((step_flow p g lbls2) × A) ≝
31    λp,g,lbls1,lbls2,M,A,H,m.
32    ! 〈flow,a〉 ← m ;
33    return 〈(flow : step_flow ?? lbls2),a〉. assumption qed.
34
35coercion step_flow_monad_times :
36  ∀p,g,lbls1,lbls2,M,A.(∀x.In ? lbls1 x → In ? lbls2 x) →
37    ∀m : monad M ((step_flow p g lbls1) × A).monad M ((step_flow p g lbls2) × A) ≝
38  monad_step_flow_times_coerc on _m : monad ? ((step_flow ???) × ?) to monad ? ((step_flow ???) × ?).
39
40let rec eval_seq_list globals (p:sem_params) (ge : genv globals p)
41  (st : state p) (b : list (joint_step p globals)) on b :
42    IO io_out io_in ((step_flow p globals (seq_list_labels … b)) × (state p)) ≝
43    match b return λx.IO ?? ((step_flow ?? (seq_list_labels … x)) × ?) with
44    [ nil ⇒ return 〈Proceed ???, st〉
45    | cons hd tl ⇒
46      ! 〈flow, st'〉 ← eval_step … ge st hd ;
47      match flow return λ_.IO ?? ((step_flow ?? (seq_list_labels … (hd :: tl))) × ?) with
48      [ Proceed ⇒ eval_seq_list globals p ge st' tl
49      | _ ⇒ return 〈flow, st'〉
50      ]
51    ]. /2 by Exists_append_r, Exists_append_l/ qed.
52
53definition fin_step_flow_change_labels :
54  ∀p,g,lbls1,lbls2.(∀x.In ? lbls1 x → In ? lbls2 x) →
55    fin_step_flow p g lbls1 → fin_step_flow p g lbls2 ≝
56  λp,g,lbls1,lbls2,prf,flow.
57  match flow with
58  [ FRedirect l ⇒ FRedirect ??? «l, prf ? (pi2 … l)»
59  | FTailInit id b args ⇒ FTailInit … id b args
60  | FEnd ⇒ FEnd ???
61  ].
62
63coercion fin_step_flow_diff_lbls :
64  ∀p,g,lbls1,lbls2.(∀x.In ? lbls1 x → In ? lbls2 x) →
65  ∀flow : fin_step_flow p g lbls1.fin_step_flow p g lbls2 ≝
66  fin_step_flow_change_labels on _flow : fin_step_flow ??? to fin_step_flow ???.
67
68definition monad_fin_step_flow_times_coerc :
69  ∀p,g,lbls1,lbls2,M,A.(∀x.In ? lbls1 x → In ? lbls2 x) →
70    monad M ((fin_step_flow p g lbls1) × A) → monad M ((fin_step_flow p g lbls2) × A) ≝
71    λp,g,lbls1,lbls2,M,A,H,m.
72    ! 〈flow,a〉 ← m ;
73    return 〈(flow : fin_step_flow ?? lbls2),a〉. assumption qed.
74
75coercion fin_step_flow_monad_times :
76  ∀p,g,lbls1,lbls2,M,A.(∀x.In ? lbls1 x → In ? lbls2 x) →
77    ∀m : monad M ((fin_step_flow p g lbls1) × A).monad M ((fin_step_flow p g lbls2) × A) ≝
78  monad_fin_step_flow_times_coerc on _m : monad ? ((fin_step_flow ???) × ?) to monad ? ((fin_step_flow ???) × ?).
79
80definition block_cont_labels ≝ λp,g,ty.λb : block_cont p g ty.
81  seq_list_labels … (\fst b) @
82  match ty return λx.stmt_type_if ? x ??? → ? with
83  [ SEQ ⇒ step_labels …
84  | FIN ⇒ fin_step_labels …
85  ] (\snd b).
86
87definition eval_block_cont :
88  ∀globals.∀p : sem_params.∀ty.genv globals p →
89  state p → ∀b : block_cont p globals ty.
90  IO io_out io_in (
91    (stmt_type_if ? ty step_flow fin_step_flow p globals (block_cont_labels … b)) ×
92    (state p)) ≝ λglobals,p,ty,ge,st.
93  match ty return λx.∀b : block_cont p globals x.
94    IO io_out io_in (
95      (stmt_type_if ? x step_flow fin_step_flow p globals (block_cont_labels … b)) ×
96      (state p))
97  with
98  [ SEQ ⇒ λb.
99    ! 〈flow, st'〉 ← eval_seq_list globals p ge st (\fst b) ;
100    match flow return λ_.IO ?? (step_flow … ((block_cont_labels … b))×?) with
101    [ Redirect l ⇒ return 〈Redirect ??? «l,?», st'〉
102    | Proceed ⇒ eval_step … ge st' (\snd b)
103    | Init _ _ _ _ ⇒
104      Error … (msg ExecutingInternalCallInBlock)
105    ]
106  | FIN ⇒ λb.
107    ! 〈flow, st'〉 ← eval_seq_list globals p ge st (\fst b) ;
108    match flow return λ_.IO ?? ((fin_step_flow … (block_cont_labels … b))×?) with
109    [ Redirect l ⇒ return 〈FRedirect ??? «l,?», st'〉
110    | Proceed ⇒ eval_fin_step … ge st' (\snd b)
111    | Init _ _ _ _ ⇒
112      Error … (msg ExecutingInternalCallInBlock)
113    ]
114  ]. try cases l /2 by Exists_append_r, Exists_append_l/ qed.
115
116(*
117lemma m_pred
118
119lemma attach_m_pred_bind : ∀M.∀MP : MonadPred P.∀P,X,Y.m : monad M X.
120  ∀f : X → monad M Y.m_pred MP P … m →
121  ! x ← m ; f x = ! x ← 
122*)
123
124definition no_init : ∀p,globals,lbls,A.((step_flow p globals lbls)×A)→Prop ≝
125  λp,globals,lbls,A,flp.
126  match \fst flp with
127  [ Init _ _ _ _ ⇒ False
128  | _ ⇒ True
129  ].
130
131definition truly_sequential : ∀p,globals,lbls,A.((step_flow p globals lbls)×A)→Prop ≝
132  λp,globals,lbls,A,flp.
133  match \fst flp with
134  [ Proceed ⇒ True
135  | _ ⇒ False
136  ].
137
138definition never_calls : ∀p : sem_params.∀globals.genv globals p → joint_step p globals → Prop ≝
139λp,globals,ge,s.match s with
140[ CALL_ID f args dest ⇒
141  Try
142    ! b ← find_symbol … ge f ;
143    ! fd ← find_funct_ptr … ge b ;
144    match fd with
145    [ Internal _ ⇒ return False
146    | External _ ⇒ return True
147    ]
148  catch ⇒
149    True
150| extension c ⇒
151  ∀st : state p.
152  pred_io … (λ_.True) (no_init …) (exec_extended … ge c st)
153| _ ⇒ True
154].
155
156definition unbranching ≝ λp,globals,ge,s.never_calls p globals ge s ∧ step_labels … s = [ ].
157
158lemma err_to_io_bind : ∀O,I,X,Y.∀m : res X.∀f : X → res Y.
159  err_to_io O I ? (! x ← m ; f x) = ! x ← m : IO O I X ; f x.
160#O #I #X #Y * //
161qed.
162
163lemma pred_io_True : ∀O,I,X,m.pred_io O I X (λ_.True) (λ_.True) m.
164#O #I #X #m elim m // qed.
165
166(*
167lemma pred_res_True : ∀X,m.pred_res X (λ_.True) (λ_.True) m.
168#X #m elim m // qed.
169*)
170
171(*
172lemma never_calls_no_init : ∀p,globals,ge,s.
173  never_calls p globals ge s →
174  ∀st : state p.
175  pred_io … (λ_.True) (no_init …) (eval_step … ge st s).
176#p#g#ge * //
177[10,12:
178|*:
179  #a #b #c try #d try #e try #f try #g
180  @res_io_pred
181  @(mp_bind … (λ_.True) … (pred_res_True …))
182  #st *  try (@mp_return @I)
183  @(mp_bind … (λ_.True) … (pred_res_True …))
184  #st * [9: elim st] normalize nodelta try (@mp_return @I)
185  @(mp_bind … (λ_.True) … (pred_res_True …))
186  #st *  try (@mp_return @I)
187  @(mp_bind … (λ_.True) … (pred_res_True …))
188  #st * [elim (opaccs ????) #by1 #by2 normalize nodelta]
189  @(mp_bind … (λ_.True) … (pred_res_True …))
190  #st * [2: elim (op2 ?????) #by #bit  normalize nodelta]
191  try (@mp_return @I)
192  @(mp_bind … (λ_.True) … (pred_res_True …))
193  #st * @mp_return @I
194]
195[ #id #args #dest #H whd in H;
196  #st change with (! x ← ? ; ?) in match (eval_step ?????);
197  elim (find_symbol ???) in H ⊢ %; [//]
198  #b >m_return_bind  >m_return_bind
199  change with (! x ← ? ; ?) in match (eval_call_block ?????????);
200  elim (find_funct_ptr ???) [//]
201  #fd >m_return_bind  >m_return_bind
202  elim fd #fn normalize nodelta *
203  @(mp_bind … (λ_.True)) [//]
204  #st * @(mp_bind … (λ_.True) … (pred_io_True …))
205  #st * @(mp_bind … (λ_.True) … (pred_io_True …))
206  #st * @(mp_bind … (λ_.True) … (pred_io_True …))
207  #st * @mp_return %
208| #s #H @H
209]
210qed.
211
212lemma unbranching_truly_sequential : ∀p,globals,ge,s.
213  unbranching p globals ge s →
214  ∀st : state p.
215  pred_io … (λ_.True) (truly_sequential …) (eval_step … ge st s).
216#p#globals#ge#s * #H #G #st
217lapply (never_calls_no_init … H st) @m_pred_mp
218>G * *
219[ * #lbl * | #id #fd #args #dest ] #st * %
220qed.
221*)
222
223lemma seq_list_labels_append : ∀p,globals,b1,b2.
224  seq_list_labels p globals (b1 @ b2) =
225  seq_list_labels … b1 @ seq_list_labels … b2.
226#p #g #b1 elim b1
227[ //
228| #hd #tl #IH #b2 whd in ⊢ (??%%);
229  >associative_append <IH %
230]
231qed.
232
233(*
234lemma eval_seq_list_append : ∀globals,p,ge,st,b1,b2.
235  eval_seq_list globals p ge st (b1@b2) =
236  ! 〈flow, st'〉 ← eval_seq_list … ge st b1 ;
237  match flow with
238  [ Proceed ⇒
239    ! 〈flow',st''〉 ← eval_seq_list … ge st' b2 ;
240    return 〈(flow' : step_flow … (seq_list_labels … (b1@b2))), st''〉
241  | _ ⇒ return 〈(flow : step_flow … (seq_list_labels … (b1@b2))), st'〉
242  ].
243[2,3,4:
244  #lbl #H >seq_list_labels_append
245  [1,2: @Exists_append_l | @Exists_append_r ] @H ]
246#globals#p#ge#st#b1 lapply st -st elim b1
247[ #st #b2 >m_return_bind normalize nodelta
248  <(m_bind_return … (eval_seq_list … b2)) in ⊢ (??%?);
249  @m_bind_ext_eq **
250  [ * #lbl #H | #id #fd #args #dest ] #st' %
251| #hd #tl #IH #st #b2
252  whd in match (? @ b2);
253  whd in match (eval_seq_list ?????);
254  whd in match (eval_seq_list ???? (hd :: tl));
255  >m_bind_bind
256  @m_bind_ext_eq
257  ** [ #lbl | #id #fd #args #dest] #st' normalize nodelta
258  [1,2: @m_return_bind]
259  >m_bind_bind
260  >IH >m_bind_bind
261  @m_bind_ext_eq **
262  [#lbl | #id #fd #args #dest ] #st' normalize nodelta
263  >m_return_bind
264  [1,2: @m_return_bind ]
265  >m_bind_bind normalize nodelta
266  @m_bind_ext_eq **
267  [#lbl|#id #fd #args #dest] #st'' >m_return_bind %
268]
269qed.
270
271lemma eval_seq_list_unbranching :
272∀globals,p,ge,st,b.
273  All ? (unbranching … ge) b →
274  pred_io … (λ_.True) (truly_sequential …)
275    (eval_seq_list globals p ge st b).
276#globals#p#ge#st #b lapply st -st elim b
277[ #st * %
278| #hd #tl #IH #st * #hd_ok #tl_ok
279  @mp_bind
280  [2: @(unbranching_truly_sequential … hd_ok st) |]
281  ** [#lbl|#id#fd#args#dest] #st' *
282  normalize nodelta
283  @mp_bind [2: @(IH st' tl_ok)|]
284  ** [#lbl|#id#fd#args#dest] #st'' * %
285]
286qed.
287
288lemma io_pred_as_rel : ∀O,I,A,Perr,P,v.
289  pred_io O I A Perr P v →
290  rel_io O I (eq …) … (λx,y.x = y ∧ P x) v v.
291#O #I #A #Perr #P #v elim v
292[ #o #f #IH whd in ⊢ (%→%);
293  #H %{(refl …)} #i @IH @H
294|*: /2/
295]
296qed.
297
298lemma eval_seq_list_append_unbranching : ∀globals,p,ge,st,b1,b2.
299  All ? (unbranching … ge) b1 →
300  eval_seq_list globals p ge st (b1@b2) =
301  ! 〈flow, st'〉 ← eval_seq_list … ge st b1 ;
302  ! 〈flow', st''〉 ← eval_seq_list … ge st' b2 ;
303  return 〈(flow' : step_flow … (seq_list_labels … (b1@b2))), st''〉.
304[2: #lbl #H >seq_list_labels_append @Exists_append_r @H ]
305#globals #p #ge #st #b1 #b2 #H
306>eval_seq_list_append
307@mr_bind
308[2: @(io_pred_as_rel … (eval_seq_list_unbranching … H)) |]
309** [#lbl|#id#fd#args#dest] #st
310#y * #EQ <EQ -y * @rel_io_eq normalize nodelta %
311qed.
312*)
313lemma block_cont_labels_append : ∀p,globals,ty,b1,b2.
314  block_cont_labels p globals ty (b1 @ b2) =
315  block_cont_labels … b1 @ block_cont_labels … b2.
316#p #g #ty * #l1 #s1 * #l2 #s2
317whd in match (〈?,?〉@?); whd in ⊢ (??%?);
318>seq_list_labels_append
319>associative_append
320>associative_append
321>associative_append %
322qed.
323(*
324lemma eval_block_cont_append : ∀globals.∀p : sem_params.∀ty,ge,st.
325  ∀b1 : block_cont p globals SEQ.∀b2 : block_cont p globals ty.
326  eval_block_cont ??? ge st (b1@b2) =
327  ! 〈flow, st'〉 ← eval_block_cont ??? ge st b1 ;
328  match ty return λx.
329    block_cont p globals x → IO ?? ((stmt_type_if ? x  step_flow fin_step_flow ???) × ?) with
330  [ SEQ ⇒ λb2.
331    match flow with
332    [ Proceed ⇒
333      ! 〈flow',st''〉 ← eval_block_cont … ge st' b2 ;
334      return 〈?, st''〉
335    | Redirect l ⇒ return 〈Redirect ??? «l,?», st'〉
336    | _ ⇒ Error … (msg ExecutingInternalCallInBlock)
337    ]
338  | FIN ⇒ λb2.
339    match flow with
340    [ Proceed ⇒
341      ! 〈flow',st''〉 ← eval_block_cont … ge st' b2 ;
342      return 〈?, st''〉
343    | Redirect l ⇒ return 〈FRedirect ??? «l,?», st'〉
344    | _ ⇒ Error … (msg ExecutingInternalCallInBlock)
345    ]
346  ] b2.
347[3,5: whd in flow'; @flow'
348  #lbl >block_cont_labels_append @Exists_append_r
349|2,4: cases l -l #l >block_cont_labels_append @Exists_append_l
350]
351#globals#p * whd in match stmt_type_if; normalize nodelta
352#ge#st * #l1 #s1 * #l2 #s2
353whd in match (〈?,?〉@?);
354whd in match eval_block_cont; normalize nodelta
355>m_bind_bind
356>eval_seq_list_append
357>m_bind_bind
358@m_bind_ext_eq
359
360 whd in ⊢ (??%?);
361    match ty return λx.IO ?? ((stmt_type_if ? x ?????) × ?) with
362    [ SEQ ⇒
363    | FIN ⇒ return 〈FRedirect ??? «l,?», st'〉
364    ]
365  | _ ⇒ Error … (msg ExecutingInternalCallInBlock)
366  ].
367#globals#p#ty#ge#st*#l1#s1*#l2#s2
368whd in match (〈?,?〉@?);
369whd in match eval_block_cont; normalize nodelta
370>m_bind_bind
371>eval_seq_list_append
372>m_bind_bind
373@m_bind_ext_eq
374** [#l|#id#fd#args#dest] normalize nodelta #st'
375[1,2:>m_return_bind normalize nodelta
376  [ >m_return_bind ] % ]
377change with (! x ← ? ; ?) in match (eval_seq_list ???? (?::?));
378>m_bind_bind whd in match stmt_type_if;
379normalize nodelta
380>m_bind_bind
381@m_bind_ext_eq
382**[#l|#id#fd#args#dest] normalize nodelta #st''
383[1,2: >m_return_bind normalize nodelta % | % ]
384qed.
385*)
386
387
388(* just like repeat, but without the full_exec infrastructure, and it
389   stops upon a non-proceed flow cmd *)
390let rec repeat_eval_state_flag n globals (p:sem_params) (ge : genv globals p)
391  (st : state_pc p) on n :
392    IO io_out io_in (bool × (state_pc p)) ≝
393match n with
394[ O ⇒ return 〈false,st〉
395| S k ⇒
396  ! 〈flag,st'〉 ← eval_state_flag globals p ge st ;
397  if flag then return 〈true,st'〉 else repeat_eval_state_flag k globals p ge st'
398].
399
400definition block_size : ∀p,g,ty.block_cont p g ty → ℕ ≝
401λp,g,ty,b.S (|\fst b|).
402
403interpretation "block cont size" 'norm b = (block_size ??? b).
404
405lemma repeat_eval_state_flag_plus : ∀n1,n2,globals, p, ge, st.
406  repeat_eval_state_flag (n1 + n2) globals p ge st =
407  ! 〈flag,st〉 ← repeat_eval_state_flag n1 globals p ge st ;
408  if flag then return 〈true, st〉 else repeat_eval_state_flag n2 globals p ge st.
409#n1 elim n1 -n1 [| #n1 #IH]
410#n2 #globals #p #ge #st
411[ @m_return_bind
412| change with (! st' ← ? ; ?) in match (repeat_eval_state_flag (S ?) ????);
413  change with (! st' ← ? ; ?) in match (repeat_eval_state_flag (S n1) ????);
414  >m_bind_bind in ⊢ (???%);
415  @m_bind_ext_eq ** #st' normalize nodelta
416  [ % | @IH ]
417]
418qed.
419
420lemma repeat_eval_state_flag_one : ∀globals, p, ge, st.
421  repeat_eval_state_flag 1 globals p ge st = eval_state_flag globals p ge st.
422#globals #p #ge #st
423change with (! st' ← ? ; ?) in match (repeat_eval_state_flag (S ?) ????);
424<(m_bind_return … (eval_state_flag ????)) in ⊢ (???%);
425@m_bind_ext_eq ** #st %
426qed.
427
428lemma eval_tunnel_step :
429  ∀p : sem_params.∀g.∀ge : genv g p.∀st : state_pc p.∀fn,src,dst.
430  fetch_function … ge (pc … st) = OK … fn →
431  point_of_pointer ? p … (pc … st) = OK … src →
432  src ~~> dst in joint_if_code … fn →
433  eval_state_flag g p ge st =
434    return 〈true,set_pc … (pointer_of_point ? p (pc … st) dst) st〉.
435#p #g #ge #st #fn #src #dst #fetch_fn #pc_pt * #lbl * #EQ1 #EQ2
436change with (! s ← ? ; ?) in match (eval_state_flag ????);
437change with (! fn ← ? ; ?) in match (fetch_statement ?????);
438>pc_pt in ⊢ (??%?); >m_return_bind
439>fetch_fn in ⊢ (??%?); >m_return_bind
440>EQ1 in ⊢ (??%?);  >m_return_bind
441>EQ2 in ⊢ (??%?);
442change with (! st ← ? ; ?) in match (eval_statement ?????);
443whd in match eval_fin_step; normalize nodelta
444>m_return_bind
445whd in match eval_fin_step_flow; normalize nodelta
446change with (! ptr ← ? ; ?) in match (goto ??????);
447whd in match pointer_of_label_in_block; normalize nodelta
448whd in match fetch_function in fetch_fn;
449normalize nodelta in fetch_fn;
450>fetch_fn in ⊢ (??%?); >m_return_bind
451>EQ2 in ⊢ (??%?); >m_return_bind
452cases st #st' ** #ty ** #id #H #o #EQ destruct(EQ)
453elim (pointer_compat_from_ind … H) %
454qed.
455
456lemma fetch_function_from_block_eq :
457  ∀p,g,ge.
458  ∀ptr1,ptr2 : cpointer. pblock ptr1 = pblock ptr2 →
459  fetch_function p g ge ptr1 = fetch_function p g ge ptr2.
460#p #g #ge #ptr1 #ptr2 #EQ
461whd in match fetch_function; normalize nodelta >EQ
462@m_bind_ext_eq // qed.
463
464(*
465lemma eval_tunnel :
466  ∀p : sem_params.∀g.∀ge : genv g p.∀st : state_pc p.∀fn,src,dst.
467  fetch_function … ge (pc … st) = OK … fn →
468  point_of_pointer ? p … (pc … st) = OK … src →
469  src ~~>^* dst in joint_if_code … fn →
470  ∃n.repeat_eval_state n g p ge st =
471    return 〈f,set_pc … (pointer_of_point ? p (pc … st) dst) st〉.
472#p #g #ge #st #fn #src #dst #fetch_fn #pc_pt * #through
473lapply pc_pt -pc_pt lapply fetch_fn -fetch_fn lapply src -src lapply st -st
474elim through [2: #hd #tl #IH]
475#st #src #fetch_fn #pc_pt
476[2: #EQ <EQ %{0}
477  >(pointer_of_point_of_pointer … (refl …) pc_pt) cases st // ]
478* #H1 #H2
479letin st' ≝ (set_pc p (pointer_of_point p p (pc p st) hd) st)
480elim (IH st' … H2)
481[3: >fetch_function_from_block_eq [@fetch_fn ||] whd in match st';
482  @pointer_of_point_block
483|2:
484  whd in match st'; >point_of_pointer_of_point %
485]
486#n' #EQ %{(S n')}
487change with (! st1 ← ? ; ?) in match (repeat_eval_state ?????);
488>(eval_tunnel_step … fetch_fn pc_pt H1) >m_return_bind
489>EQ %
490qed.
491
492lemma eval_tunnel_plus :
493  ∀p : sem_params.∀g.∀ge : genv g p.∀st : state_pc p.∀fn,src,dst.
494  fetch_function … ge (pc … st) = OK … fn →
495  point_of_pointer ? p … (pc … st) = OK … src →
496  src ~~>^+ dst in joint_if_code … fn →
497  ∃n.repeat_eval_state (S n) g p ge st =
498    return set_pc … (pointer_of_point ? p (pc … st) dst) st.
499#p #g #ge #st #fn #src #dst #fetch_fn #pc_pt * #mid * #H1 #H2
500letin st' ≝ (set_pc p (pointer_of_point p p (pc p st) mid) st)
501elim (eval_tunnel … ge st' … H2)
502[3: >fetch_function_from_block_eq [@fetch_fn ||] whd in match st';
503  @pointer_of_point_block
504|2:
505  whd in match st'; >point_of_pointer_of_point %
506]
507#n #EQ %{n}
508change with (! st1 ← ? ; ?) in match (repeat_eval_state ?????);
509>(eval_tunnel_step … fetch_fn pc_pt H1) >m_return_bind
510>EQ %
511qed.
512*)
513
514lemma fetch_statement_eq : ∀p:sem_params.∀g.∀ge : genv g p.∀ptr : cpointer.
515  ∀fn,pt,s.
516  fetch_function … ge ptr = OK … fn →
517  point_of_pointer ? p … ptr = OK … pt →
518  stmt_at … (joint_if_code … fn) pt = Some ? s →
519  fetch_statement ? p … ge ptr = OK … s.
520#p #g #ge #ptr #fn #pt #s #EQ1 #EQ2 #EQ3
521whd in match fetch_statement; normalize nodelta >EQ2 >m_return_bind
522>EQ1 >m_return_bind >EQ3 %
523qed.
524(*
525lemma eval_seq_list_in_code :
526  ∀p : sem_params.∀g.∀ge : genv g p.∀st : state_pc p.∀fn,src,B,dst.
527  fetch_function … ge (pc … st) = OK … fn →
528  point_of_pointer ? p … (pc … st) = OK … src →
529  All ? (never_calls … ge) B →
530  seq_list_in_code … (joint_if_code … fn) src B dst →
531  repeat_eval_state_flag (|B|) g p ge st =
532   ! 〈flow,st'〉 ← eval_seq_list g p ge st B ;
533   match flow with
534   [ Redirect l ⇒
535     ! st'' ← goto ?? ge l st' (pblock … (pc ? st)) ;
536     return 〈true, st''〉
537   | Init id fn args dest ⇒ Error … (msg ExecutingInternalCallInBlock)
538       (* dummy, never happens *)
539   | Proceed ⇒
540     let nxt_ptr ≝ pointer_of_point p p … (pc … st) dst in
541     return 〈false, mk_state_pc ? st' nxt_ptr〉
542   ].
543#p #g #ge #st #fn #src #B lapply src -src
544lapply st -st elim B [|#hd #tl #IH]
545#st #src #dst #fetch_fn #pc_pt * [2: #hd_ok #tl_ok]
546[2: #EQ normalize in EQ; <EQ
547  whd in match (eval_seq_list ???? [ ]);
548  >m_return_bind normalize nodelta
549  >(pointer_of_point_of_pointer … (refl …) pc_pt) cases st //
550|1: * #n * #EQat #H
551  change with (! st' ← ? ; ?) in match (eval_seq_list ?????);
552  change with (! st' ← ? ; ?) in match (repeat_eval_state_flag ?????);
553  >m_bind_bind
554  >(fetch_statement_eq … fetch_fn pc_pt EQat) >m_return_bind
555  >m_bind_bind >m_bind_bind
556  lapply (never_calls_no_init … hd_ok st) #hd_ok'
557  @(mr_bind …
558    (λfst1,fst2.fst1 = fst2 ∧ no_init … fst1))
559  [ lapply hd_ok' elim (eval_step ?????)
560    [ #o #f #IH'
561      whd in ⊢ (%→%); #G
562      %{(refl …)} #i @IH' @G
563    |*: #v whd in ⊢ (%→%); #H
564      % [ % ] @H
565    ]
566  | ** [#lbl | #id #fd #args #dest ] #st'
567    #y * #EQ <EQ -y * normalize nodelta @rel_io_eq
568    whd in match succ_pc; normalize nodelta
569    >pc_pt >m_return_bind
570    letin src' ≝ (point_of_succ p src n) in H ⊢ %;
571    letin pc' ≝ (pointer_of_point p p … (pc ? st) src') #H
572    [>m_return_bind whd in match eval_step_flow; normalize nodelta
573     whd in match (pblock ?);
574     elim (goto … ge lbl st' ?)
575     [ #st'' >m_return_bind %
576     | #e %
577     ]
578    | normalize nodelta in IH ⊢ %; @(IH … tl_ok H)
579      [ @fetch_fn
580      | @point_of_pointer_of_point
581      ]
582    ]
583  ]
584]
585qed.
586
587definition eval_block_cont_pc :
588  ∀globals.∀p : sem_params.∀ty.genv globals p →
589  state_pc p → block_cont p globals ty → stmt_type_if ? ty (code_point p) unit →
590  IO io_out io_in (bool × (state_pc p)) ≝
591  λglobals,p,ty,ge,st,b,nxt.
592  ! 〈flow, st'〉 ← eval_block_cont globals p ty ge st b ;
593  match ty return λx.stmt_type_if ? x ?? → stmt_type_if ? x ?? → ? with
594  [ SEQ ⇒ λflow,nxt.eval_step_flow ?? ge st'
595        (pointer_of_point ? p (pc ? st) nxt) flow
596  | FIN ⇒ λflow.λ_.
597    ! st' ← eval_fin_step_flow ?? ge st' (pblock … (pc ? st)) flow ;
598    return 〈true, st'〉
599  ] flow nxt.
600
601lemma eval_block_cont_in_code :
602  ∀p : sem_params.∀g,ty.∀ge : genv g p.∀st : state_pc p.∀fn,src,B,dst.
603  fetch_function … ge (pc … st) = OK … fn →
604  point_of_pointer ? p … (pc … st) = OK … src →
605  All ? (never_calls … ge) (\fst B) →
606  src ~❨B❩~> dst in joint_if_code … fn →
607  repeat_eval_state_flag (|B|) g p ge st =
608    eval_block_cont_pc g p ty ge st B dst.
609#p #g #ty #ge #st #fn #src * #l #s #dst #fetch_fn #pc_pt #l_ok
610* #mid * #l_in_code #s_in_code
611change with (1 + |l|) in match (|?|);
612>commutative_plus
613>repeat_eval_state_flag_plus
614change with (! x ← ? ; ?) in ⊢ (???%);
615>m_bind_bind
616>(eval_seq_list_in_code … fetch_fn pc_pt l_ok l_in_code)
617>m_bind_bind
618@m_bind_ext_eq ** [#lbl | #id #fd #args #dest] #st'
619normalize nodelta
620[ -s_in_code lapply dst -dst cases ty
621  whd in match stmt_type_if; normalize nodelta
622  #dst >m_return_bind
623  [whd in match eval_step_flow; | whd in match eval_fin_step_flow; ]
624  normalize nodelta
625  whd in match (pblock ?);
626  elim (goto g p ge lbl st' ?) #x //
627| %
628| >m_return_bind normalize nodelta
629  >repeat_eval_state_flag_one
630  >m_bind_bind
631  lapply s_in_code -s_in_code lapply dst -dst lapply s -s cases ty
632  whd in match stmt_type_if; normalize nodelta
633  #s #dst [* #n * ] #s_in_code [ #n_is_dst ]
634  whd in match eval_state_flag; normalize nodelta
635  letin pc' ≝ (pointer_of_point p p (pc ? st) mid)
636  letin st_pc' ≝ (mk_state_pc ? st' pc')
637  >(fetch_statement_eq … ?? s_in_code)
638  [2,5: @point_of_pointer_of_point
639  |3,6: @fetch_fn
640  |*: >m_return_bind
641    whd in match eval_statement; normalize nodelta
642    @m_bind_ext_eq * #flow #st'' >m_return_bind [2:%]
643    whd in match succ_pc; normalize nodelta
644    >point_of_pointer_of_point >m_return_bind
645    >pointer_of_point_of_pointer [2: @refl |*:]
646    [ >point_of_pointer_of_point >n_is_dst %
647    | %
648    ]
649  ]
650]
651qed.
652     cases dst [*] #z @eval_tunnel assumption
653| cases dst [2: #z *]]
654* #mid * #tunn [#H | * #n * #H #G ]
655  elim (eval_tunnel … fetch_fn pc_pt tunn)
656  #n
657  letin st' ≝ (set_pc p (pointer_of_point p p (pc p st) mid) st)
658  #EQ1
659  cut (point_of_pointer ? p … (pc … st') = OK … mid)
660  [1,3:
661    whd in match st'; >point_of_pointer_of_point % ] #pc_pt'
662  cut (fetch_function p … ge (pc … st') = OK … fn)
663  [1,3: >fetch_function_from_block_eq [1,4:@fetch_fn |*:] whd in match st';
664    @pointer_of_point_block] #fetch_fn'
665  [ %{(n + 1)}
666  >repeat_eval_state_plus >EQ1 >m_return_bind
667  >repeat_eval_state_one change with (None ?) in match (! x ← None ? ; ?);
668  change with (! 〈flow,tr,st〉 ← ? ; ?) in match (eval_block_cont ??????);
669  change with (! s ← ? ; ?) in match (eval_state ????);
670  >(fetch_statement_eq … fetch_fn' pc_pt' H) >m_return_bind
671  >m_bind_bind
672  change with ( ! x ← ? ; ?) in match (eval_block_cont ???????);
673  cases s *
674 
675  @m_bind_ext_eq' ** #flow #tr1 #st1 normalize nodelta
676  >m_bind_bind change with st' in match (set_pc ???); @m_bind_ext_eq
677  change with (! fn ← ? ; ?) in match (fetch_statement ?????);
678  >m_bind_bind in ⊢ (??%?);
679  change with (pointer_of_point ????) in match (pc ??);
680  >point_of_pointer_of_point >m_return_bind
681  >(fetch_function_from_block_eq ???? (pc … st))
682  [2: @pointer_of_point_block ]
683  >fetch_fn >m_return_bind >H2 >m_return_bind
684  >m_bind_bind
685  change with (! x ← ? ; ?) in ⊢ (???%);
686  >fetch_fn n ⊢ (??(????%?)?); >m_return_bind
687  >(stmt_at_to_safe … src_prf) in ⊢ (??(????%?)?);
688  >H1 in ⊢ (??(????%?)?);
689  whd in ⊢ (??(λ_.???%));
690elim b
691[ #st #dst #fetch_fn #prf #through
692  #H elim (block_cont_to_tunnel … H) #dst'
693  * #EQdst >EQdst >m_return_bind #G
694  elim (eval_tunnel … fetch_fn prf … G) #x #EQ %{x}
695  >EQ %
696|
697
698 #dst #fetch_fn #prf #through
699lapply prf -prf lapply fetch_fn -fetch_fn
700lapply b -b lapply st -st
701elim through [2: #hd #tl #IH]
702[2:
703 
704#st * [1,4,7,10:|2,5,8,11:#s|3,6,9,12:#s#b'] #fetch_fn #prf
705normalize in ⊢(%→?);
706[8: #EQ1 |*: * [5: |*: *] #lbl [ |*: *] * #H1 #H2 [|*: #H3] #x [ *
707[ * || * | * #lbl
708 * #lbl * [*] #H1 #H2 [#H3]
709 
710let rec block_cont_in_code (p : sem_params) g (b : block_cont p g)
711  (following : option (succ p)) (c : codeT p g) (at : cpointer) on b : Prop ≝
712  match b with
713  [ Skip ⇒
714    match following with
715    [ Some l ⇒ succ_pc p p
716*)
Note: See TracBrowser for help on using the repository browser.