source: src/joint/semantics_blocks.ma @ 2042

Last change on this file since 2042 was 1999, checked in by campbell, 8 years ago

Make back-end use the main global envs.

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