Changeset 1949 for src/joint/semantics_blocks.ma
 Timestamp:
 May 15, 2012, 5:51:25 PM (8 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/semantics_blocks.ma
r1882 r1949 2 2 include "joint/semantics_paolo.ma". 3 3 4 (* WARNING: all the following breaks apart if statements are allowed to depend 5 on flow. Execution of blocks does not update flow information in the state 6 (e.g. the program counter) until the end *) 7 8 definition goto_no_seq : ∀g.∀p:sem_params.genv g p → label → 9 state p → Z → res (state_pc p) ≝ λg,p,ge,lbl,st,id. 10 ! newpc ← pointer_of_label ? p … ge 11 (mk_pointer Code (mk_block Code id) ? (mk_offset 0)) lbl ; 12 return mk_state_pc … st newpc. % qed. 13 14 lemma goto_no_seq_to_normal : ∀p : sem_params.∀g,ge.∀st : state_pc p.∀id,lbl. 15 block_id (pblock (pc p st)) = id → 16 goto_no_seq g p ge lbl st id = goto g p ge lbl st. 17 #p #g #ge * #st ** #typ * #r #id 18 #H inversion H [1,3: #r'] #id' 19 #EQ1 #EQ2 #EQ3 #o #EQ4 #id'' #lbl #EQ5 destruct 20 whd in match goto_no_seq; 21 whd in match goto; normalize nodelta // 22 qed. 23 24 (* executes a block of instructions, until its end or before if a 25 function call or a redirection is encountered. If executed until end, 26 or is a nontail call is encountered, the next program counter must be 27 provided *) 28 let rec eval_block_cont globals (p:sem_params) (ge : genv globals p) 29 (st : state p) id (b : block_cont p globals) (dst : option cpointer) on b : 30 IO io_out io_in (trace×(state_pc p)) ≝ 4 5 axiom ExecutingInternalCallInBlock : String. 6 7 let rec seq_list_labels p g (b : list (joint_step p g)) on b : list label ≝ 31 8 match b with 32 [ Skip ⇒ 33 ! nxt ← opt_to_res … (msg SuccessorNotProvided) dst ; 34 return 〈E0, mk_state_pc ? st nxt〉 35  Final s ⇒ 36 ! 〈flow, tr, st'〉 ← eval_statement_no_seq … ge st s; 37 ! st ← eval_stmt_flow_no_seq … ge st' id flow; 38 return 〈tr, st〉 39  Cons hd tl ⇒ 40 ! 〈flow, tr1, st'〉 ← eval_step ?? ge st hd ; 9 [ nil ⇒ [ ] 10  cons hd tl ⇒ step_labels … hd @ seq_list_labels … tl 11 ]. 12 13 definition 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 23 coercion 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 28 definition 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 35 coercion 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 40 let 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 53 definition 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 63 coercion 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 68 definition 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 75 coercion 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 80 definition 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 87 definition 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 lemma m_pred 117 118 lemma 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 122 definition 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 129 definition 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 136 definition 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 154 definition unbranching ≝ λp,globals,ge,s.never_calls p globals ge s ∧ step_labels … s = [ ]. 155 156 lemma 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 * // 159 qed. 160 161 lemma pred_io_True : ∀O,I,X,m.pred_io O I X (λ_.True) (λ_.True) m. 162 #O #I #X #m elim m // qed. 163 lemma pred_res_True : ∀X,m.pred_res X (λ_.True) (λ_.True) m. 164 #X #m elim m // qed. 165 166 lemma 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 ] 204 qed. 205 206 lemma 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 211 lapply (never_calls_no_init … H st) @m_pred_mp 212 >G * * 213 [ * #lbl *  #id #fd #args #dest ] #st * % 214 qed. 215 216 lemma 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 ] 224 qed. 225 226 lemma 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 ] 261 qed. 262 263 lemma 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 ] 278 qed. 279 280 lemma 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 ] 288 qed. 289 290 lemma 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 % 303 qed. 304 305 lemma 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 309 whd in match (〈?,?〉@?); whd in ⊢ (??%?); 310 >seq_list_labels_append 311 >associative_append 312 >associative_append 313 >associative_append % 314 qed. 315 316 lemma 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. 41 323 match flow with 42 [ Proceed ⇒ 43 ! 〈tr2, st〉 ← eval_block_cont globals p ge st id tl dst ; 44 return 〈tr1 ⧺ tr2, st〉 45  Init id fn args dest ⇒ 46 ! ra ← opt_to_res … (msg SuccessorNotProvided) dst ; 47 let st' ≝ set_frms … (save_frame … ra dest st) st in 48 ! st ← do_call ?? ge st' id fn args ; 49 return 〈tr1, st〉 50  Redirect l ⇒ 51 ! st ← goto_no_seq ? p … ge l st id ; 52 return 〈tr1, st〉 53 ] 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 345 whd in match (〈?,?〉@?); 346 whd 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) 54 358 ]. 55 56 lemma Eapp_E0 : ∀tr1 : trace.tr1 ⧺ E0 = tr1 ≝ append_nil …. 57 58 (* just like repeat, but without the full_exec infrastructure *) 59 let rec repeat_eval_state n globals (p:sem_params) (ge : genv globals p) 359 #globals#p#ty#ge#st*#l1#s1*#l2#s2 360 whd in match (〈?,?〉@?); 361 whd 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 ] % ] 369 change with (! x ← ? ; ?) in match (eval_seq_list ???? (?::?)); 370 >m_bind_bind whd in match stmt_type_if; 371 normalize 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 %  % ] 376 qed. 377 378 379 380 (* just like repeat, but without the full_exec infrastructure, and it 381 stops upon a nonproceed flow cmd *) 382 let rec repeat_eval_state_flag n globals (p:sem_params) (ge : genv globals p) 60 383 (st : state_pc p) on n : 61 IO io_out io_in ( trace×(state_pc p)) ≝384 IO io_out io_in (bool × (state_pc p)) ≝ 62 385 match n with 63 [ O ⇒ return 〈 E0,st〉386 [ O ⇒ return 〈false,st〉 64 387  S k ⇒ 65 ! 〈tr1, st〉 ← eval_state globals p ge st ; 66 ! 〈tr2, st〉 ← repeat_eval_state k globals p ge st ; 67 return 〈tr1 ⧺ tr2, st〉 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' 68 390 ]. 69 391 70 lemma repeat_eval_state_plus : ∀n1,n2,globals, p, ge, st. 71 repeat_eval_state (n1 + n2) globals p ge st = 72 ! 〈tr1, st〉 ← repeat_eval_state n1 globals p ge st ; 73 ! 〈tr2, st〉 ← repeat_eval_state n2 globals p ge st ; 74 return 〈tr1 ⧺ tr2, st〉. 392 definition block_size : ∀p,g,ty.block_cont p g ty → ℕ ≝ 393 λp,g,ty,b.S (\fst b). 394 395 interpretation "block cont size" 'norm b = (block_size ??? b). 396 397 lemma 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. 75 401 #n1 elim n1 n1 [ #n1 #IH] 76 402 #n2 #globals #p #ge #st 77 [ >m_return_bind change with n2 in match (0 + n2); 78 change with (! x ← ? ; ?) in ⊢ (???%); 79 <(m_bind_return … (repeat_eval_state ?????)) in ⊢ (??%?); 80 @m_bind_ext_eq * // 81  change with (! 〈tr',st'〉 ← ? ; ?) in match (repeat_eval_state (S ?) ????); 82 change with (! 〈tr',st'〉 ← ? ; ?) in match (repeat_eval_state (S n1) ????); 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) ????); 83 406 >m_bind_bind in ⊢ (???%); 84 @m_bind_ext_eq * #tr1 #st1 85 >IH >m_bind_bind in ⊢ (??%?); >m_bind_bind in ⊢ (???%); 86 @m_bind_ext_eq * #tr2 #st2 >m_return_bind 87 >m_bind_bind @m_bind_ext_eq * #tr3 #st3 >m_return_bind >Eapp_assoc % 88 ] 89 qed. 90 91 lemma repeat_eval_state_one : ∀globals, p, ge, st. 92 repeat_eval_state 1 globals p ge st = eval_state globals p ge st. 407 @m_bind_ext_eq ** #st' normalize nodelta 408 [ %  @IH ] 409 ] 410 qed. 411 412 lemma 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. 93 414 #globals #p #ge #st 94 change with (! 〈tr',st'〉 ← ? ; ?) in match (repeat_eval_state (S ?) ????); 95 <(m_bind_return … (eval_state ????)) in ⊢ (???%); 96 @m_bind_ext_eq * #tr1 #st1 >m_return_bind >Eapp_E0 % 97 qed. 98 99 lemma If_true : ∀A.∀b : bool.∀f : b → A.∀g.∀prf' : bool_to_Prop b.If b then with prf do f prf else with prf do g prf = f prf'. 100 #A * #f #g * normalize % qed. 415 change with (! st' ← ? ; ?) in match (repeat_eval_state_flag (S ?) ????); 416 <(m_bind_return … (eval_state_flag ????)) in ⊢ (???%); 417 @m_bind_ext_eq ** #st % 418 qed. 101 419 102 420 lemma eval_tunnel_step : … … 105 423 point_of_pointer ? p … (pc … st) = OK … src → 106 424 src ~~> dst in joint_if_code … fn → 107 eval_state g p ge st =108 OK … 〈E0,set_pc … (pointer_of_point ? p (pc … st) dst) st〉.425 eval_state_flag g p ge st = 426 return 〈true,set_pc … (pointer_of_point ? p (pc … st) dst) st〉. 109 427 #p #g #ge #st #fn #src #dst #fetch_fn #pc_pt * #lbl * #EQ1 #EQ2 110 change with (! s ← ? ; ?) in match (eval_state ????);428 change with (! s ← ? ; ?) in match (eval_state_flag ????); 111 429 change with (! fn ← ? ; ?) in match (fetch_statement ?????); 112 430 >pc_pt in ⊢ (??%?); >m_return_bind 113 431 >fetch_fn in ⊢ (??%?); >m_return_bind 114 432 >EQ1 in ⊢ (??%?); >m_return_bind 115 >EQ2 in ⊢ (??%?); >m_return_bind 116 change with (! st ← ? ; ?) in ⊢ (??%?); 117 whd in match eval_stmt_flow; normalize nodelta 118 change with (! ptr ← ? ; ?) in match (goto ?????); 119 whd in match pointer_of_label; normalize nodelta 433 >EQ2 in ⊢ (??%?); 434 change with (! st ← ? ; ?) in match (eval_statement ?????); 435 whd in match eval_fin_step; normalize nodelta 436 >m_return_bind 437 whd in match eval_fin_step_flow; normalize nodelta 438 change with (! ptr ← ? ; ?) in match (goto ??????); 439 whd in match pointer_of_label_in_block; normalize nodelta 440 whd in match fetch_function in fetch_fn; 441 normalize nodelta in fetch_fn; 120 442 >fetch_fn in ⊢ (??%?); >m_return_bind 121 >EQ2 in ⊢ (??%?); >m_return_bind % 122 qed. 123 443 >EQ2 in ⊢ (??%?); >m_return_bind 444 cases st #st' ** #ty ** #id #H #o #EQ destruct(EQ) 445 elim (pointer_compat_from_ind … H) % 446 qed. 124 447 125 448 lemma fetch_function_from_block_eq : … … 131 454 @m_bind_ext_eq // qed. 132 455 456 (* 133 457 lemma eval_tunnel : 134 458 ∀p : sem_params.∀g.∀ge : genv g p.∀st : state_pc p.∀fn,src,dst. … … 137 461 src ~~>^* dst in joint_if_code … fn → 138 462 ∃n.repeat_eval_state n g p ge st = 139 OK … 〈E0,set_pc … (pointer_of_point ? p (pc … st) dst) st〉.463 return 〈f,set_pc … (pointer_of_point ? p (pc … st) dst) st〉. 140 464 #p #g #ge #st #fn #src #dst #fetch_fn #pc_pt * #through 141 465 lapply pc_pt pc_pt lapply fetch_fn fetch_fn lapply src src lapply st st … … 153 477 ] 154 478 #n' #EQ %{(S n')} 155 change with (! 〈tr1,st1〉← ? ; ?) in match (repeat_eval_state ?????);479 change with (! st1 ← ? ; ?) in match (repeat_eval_state ?????); 156 480 >(eval_tunnel_step … fetch_fn pc_pt H1) >m_return_bind 157 >EQ >m_return_bind%481 >EQ % 158 482 qed. 159 483 … … 164 488 src ~~>^+ dst in joint_if_code … fn → 165 489 ∃n.repeat_eval_state (S n) g p ge st = 166 OK … 〈E0, set_pc … (pointer_of_point ? p (pc … st) dst) st〉.490 return set_pc … (pointer_of_point ? p (pc … st) dst) st. 167 491 #p #g #ge #st #fn #src #dst #fetch_fn #pc_pt * #mid * #H1 #H2 168 492 letin st' ≝ (set_pc p (pointer_of_point p p (pc p st) mid) st) … … 174 498 ] 175 499 #n #EQ %{n} 176 change with (! 〈tr1,st1〉← ? ; ?) in match (repeat_eval_state ?????);500 change with (! st1 ← ? ; ?) in match (repeat_eval_state ?????); 177 501 >(eval_tunnel_step … fetch_fn pc_pt H1) >m_return_bind 178 >EQ >m_return_bind % 179 qed. 502 >EQ % 503 qed. 504 *) 180 505 181 506 lemma fetch_statement_eq : ∀p:sem_params.∀g.∀ge : genv g p.∀ptr : cpointer. … … 190 515 qed. 191 516 192 lemma eval_ block_cont_in_code :517 lemma eval_seq_list_in_code : 193 518 ∀p : sem_params.∀g.∀ge : genv g p.∀st : state_pc p.∀fn,src,B,dst. 194 519 fetch_function … ge (pc … st) = OK … fn → 195 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 536 lapply 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 ] 577 qed. 578 579 definition 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 593 lemma 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) → 196 598 src ~❨B❩~> dst in joint_if_code … fn → 197 ∃n.repeat_eval_state n g p ge st = 198 eval_block_cont g p ge st (block_id (pblock (pc … st))) B (! x ← dst; return pointer_of_point … p (pc … st) x). 199 #p #g #ge #st #fn #src #B lapply src src 200 lapply st st elim B [#s#s #B' #IH] 201 #st #src #dst #fetch_fn #pc_pt 202 [ cases dst [*] #z @eval_tunnel assumption 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 603 change with (1 + l) in match (?); 604 >commutative_plus 605 >repeat_eval_state_flag_plus 606 change 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' 611 normalize 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 ] 643 qed. 644 cases dst [*] #z @eval_tunnel assumption 203 645  cases dst [2: #z *]] 204 646 * #mid * #tunn [#H  * #n * #H #G ]
Note: See TracChangeset
for help on using the changeset viewer.