 Timestamp:
 Apr 1, 2013, 5:18:05 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/StatusSimulationHelper.ma
r2991 r3050 17 17 include "common/StatusSimulation.ma". 18 18 include "joint/semantics_blocks.ma". 19 include "utilities/listb_extra.ma". 20 include "utilities/lists.ma". 19 21 20 22 lemma set_no_pc_eta: … … 46 48 qed. 47 49 48 let rec bind_instantiate sB X (b : bind_new B X) (l : list B) on b : (option X) ≝50 let rec bind_instantiate B X (b : bind_new B X) (l : list B) on b : (option X) ≝ 49 51 match b with 50 52 [ bret B ⇒ … … 57 59 [ nil ⇒ None ? 58 60  cons r l' ⇒ 59 bind_instantiate sB X (f r) l'61 bind_instantiate B X (f r) l' 60 62 ] 61 63 ]. 62 64 63 lemma bind_instantiates_ bind_new_instantiates: ∀B,X.∀b : bind_new B X.65 lemma bind_instantiates_to_instantiate : ∀B,X.∀b : bind_new B X. 64 66 ∀l : list B.∀x : X. 65 bind_instantiate sB X b l = Some ? x →67 bind_instantiate B X b l = Some ? x → 66 68 bind_new_instantiates B X x b l. 67 69 #B #X #b elim b … … 72 74 qed. 73 75 74 lemma bind_ new_instantiates_bind_instantiates : ∀B,X.∀b : bind_new B X.76 lemma bind_instantiate_instantiates : ∀B,X.∀b : bind_new B X. 75 77 ∀l : list B.∀x : X. 76 78 bind_new_instantiates B X x b l → 77 bind_instantiate sB X b l = Some ? x.79 bind_instantiate B X b l = Some ? x. 78 80 #B #X #b elim b 79 81 [ #x1 * [2: #hd #tl] #x whd in ⊢ (% → ?); [*] #EQ destruct(EQ) % … … 82 84 qed. 83 85 84 85 definition joint_state_relation ≝ 86 λP_in,P_out.program_counter → state P_in → state P_out → Prop. 87 88 definition joint_state_pc_relation ≝ λP_in,P_out.state_pc P_in → state_pc P_out → Prop. 86 coercion bind_instantiate_instantiates : ∀B,X.∀b : bind_new B X. 87 ∀l : list B.∀x : X. 88 ∀prf : bind_new_instantiates B X x b l. 89 bind_instantiate B X b l = Some ? x ≝ 90 bind_instantiate_instantiates 91 on _prf : bind_new_instantiates ????? 92 to eq (option ?) (bind_instantiate ????) (Some ??). 89 93 90 94 definition lbl_funct_type ≝ block → label → (list label). 91 95 definition regs_funct_type ≝ block → label → (list register). 96 92 97 93 98 definition preamble_length ≝ … … 99 104 λf_regs : regs_funct_type.λbl : block.λlbl : label. 100 105 ! bl ← code_block_of_block bl ; 101 ! 〈id,fn〉 ← res_to_opt … (fetch_internal_function … (prog_var_names … prog)106 ! 〈id,fn〉 ← res_to_opt … (fetch_internal_function … 102 107 (joint_globalenv P_in prog stack_size) bl); 103 ! stmt ← stmt_at P_in (prog_var_names … prog)(joint_if_code … fn) lbl;104 ! data ← bind_instantiate s?? (init … fn) (init_regs bl);108 ! stmt ← stmt_at P_in … (joint_if_code … fn) lbl; 109 ! data ← bind_instantiate ?? (init … fn) (init_regs bl); 105 110 match stmt with 106 111 [ sequential step nxt ⇒ 107 ! step_block ← bind_instantiate s?? (f_step … data lbl step) (f_regs bl lbl);112 ! step_block ← bind_instantiate ?? (f_step … data lbl step) (f_regs bl lbl); 108 113 return \fst (\fst step_block) 109 114  final fin ⇒ 110 ! fin_block ← bind_instantiate s?? (f_fin … data lbl fin) (f_regs bl lbl);115 ! fin_block ← bind_instantiate ?? (f_fin … data lbl fin) (f_regs bl lbl); 111 116 return \fst fin_block 112 117  FCOND abs _ _ _ ⇒ Ⓧabs … … 122 127 λp_in,p_out,prog,stack_size,init,init_regs,f_lbls,f_regs,bl,searched. 123 128 ! bl ← code_block_of_block bl ; 124 ! 〈id,fn〉 ← res_to_opt … (fetch_internal_function … (prog_var_names … prog)129 ! 〈id,fn〉 ← res_to_opt … (fetch_internal_function … 125 130 (joint_globalenv p_in prog stack_size) bl); 126 131 ! 〈res,s〉 ← … … 200 205 qed. 201 206 207 lemma match_reg_elim : ∀ A : Type[0]. ∀ P : A → Prop. ∀ r : region. 208 ∀f : (r = XData) → A. ∀g : (r = Code) → A. (∀ prf : r = XData.P (f prf)) → 209 (∀ prf : r = Code.P (g prf)) → 210 P ((match r return λx.(r = x → ?) with 211 [XData ⇒ f  Code ⇒ g])(refl ? r)). 212 #A #P * #f #g #H1 #H2 normalize nodelta [ @H1  @H2] 213 qed. 214 202 215 definition sigma_stored_pc ≝ 203 216 λp_in,p_out,prog,stack_size,init,init_regs,f_lbls,f_regs,pc. 204 217 match sigma_pc_opt p_in p_out prog stack_size init init_regs f_lbls f_regs pc with 205 218 [None ⇒ null_pc (pc_offset … pc)  Some x ⇒ x]. 219 220 lemma code_block_of_block_eq : ∀bl : Σb.block_region b = Code. 221 code_block_of_block bl = return bl. 222 * #bl #prf whd in match code_block_of_block; normalize nodelta @match_reg_elim 223 [ >prf in ⊢ (% → ?); #ABS destruct(ABS)] #prf1 % 224 qed. 225 226 (*TO BE MOVED*) 227 lemma Exists_append1 : ∀A.∀l1,l2 : list A.∀P.Exists A P l1 → Exists A P (l1@l2). 228 #A #l1 elim l1 [#l2 #P *] #hd #tl #IH * 229 [#P normalize // ] #hd1 #tl1 #P normalize * [#H % assumption  #H %2 @IH assumption] 230 qed. 231 232 lemma Exists_append2 : ∀A.∀l1,l2 : list A.∀P.Exists A P l2 → Exists A P (l1@l2). 233 #A #l1 #l2 lapply l1 l1 elim l2 [#l1 #a *] #hd #tl #IH * 234 [#a normalize // ] #hd1 #tl1 #a normalize * 235 [ #H %2 >append_cons @Exists_append1 elim tl1 [% assumption] #hd2 #tl2 #H1 normalize %2 // 236  #H %2 >append_cons @IH assumption] 237 qed. 238 239 lemma seq_list_in_code_length : ∀p : params. ∀globals : list ident. 240 ∀code : codeT p globals.∀src : code_point p.∀l1,l2,dst. 241 seq_list_in_code p globals code src l1 l2 dst → l1 = l2. 242 #p #globals #code #src #l1 lapply src src elim l1 243 [ #src * [ #dst #_ %] #hd #tl #dst whd in ⊢ (% → ?); * #EQ destruct] 244 #hd #tl #IH #src * [ #dst whd in ⊢ (% → ?); * #mid * #rest ** #EQ destruct] 245 #hd1 #tl1 #dst whd in ⊢ (% → ?); * #mid * #rest ** #EQ destruct * #nxt1 * #EQstnt 246 #EQsucc #H whd in ⊢ (??%%); @eq_f @(IH … H) 247 qed. 248 249 lemma sigma_label_spec : ∀p_in,p_out,prog,stack_size,init,init_regs. 250 ∀f_lbls : lbl_funct_type.∀f_regs. 251 b_graph_transform_program_props p_in p_out stack_size init prog init_regs f_lbls f_regs → 252 ∀id,fn. 253 ∀bl:Σb.block_region b = Code. ∀pt,stmt. 254 block_id … bl ≠ 1 → 255 fetch_internal_function … 256 (joint_globalenv p_in prog stack_size) bl = return 〈id,fn〉 → 257 stmt_at p_in … (joint_if_code … fn) pt = return stmt → 258 ∃n.preamble_length … prog stack_size init init_regs f_regs bl pt = return n ∧ 259 match n with 260 [ O ⇒ sigma_label p_in p_out prog stack_size init init_regs f_lbls f_regs bl pt = return pt 261  S m ⇒ ∃lbl.nth_opt ? m (f_lbls bl pt) = return lbl ∧ 262 sigma_label p_in p_out prog stack_size init init_regs f_lbls f_regs bl lbl = return pt 263 ]. 264 #p_in #p_out #prog #stack_size #init #init_regs #f_lbls #f_regs #good #id #fn 265 #bl #pt #stmt * #Hbl #EQfn #EQstmt 266 lapply(b_graph_transform_program_fetch_internal_function … good … bl id fn) 267 @eqZb_elim [ #EQ >EQ in Hbl; #H @⊥ @H %] #_ normalize nodelta #H cases(H EQfn) H 268 #data * #t_fn ** #EQt_fn #Hinit * #_ #_ #_ #pp_labs #_ #fresh_lab #_ #_ #_ #H 269 lapply(H … EQstmt) H normalize nodelta cases stmt in EQstmt; stmt 270 [ #j_step #nxt  #fin  * ] #EQstmt normalize nodelta ** 271 [ * #pre_instr #instr #post_instr  #pre_instr #instr] * 272 [ cases(added_prologue ????) [2: #hd_instr #tl_instrs ] normalize nodelta 273 [ @eq_identifier_elim #EQentry normalize nodelta 274 [ whd in ⊢ (% → ?); inversion (f_regs ??) [2: #x #y #_ #_ *] #EQregs normalize nodelta 275 whd in ⊢ (???% → ?); #EQ destruct(EQ) 276 *: #Hregs 277 ] 278  #Hregs 279 ] 280  #Hregs 281 ] 282 #syntax_spec 283 [4: cases(added_prologue ????) [2: #hd_instr #tl_instrs ] normalize nodelta ] #_ 284 [1,2,4,5: %{(pre_instr)}  %{O}] 285 cut(? : Prop) 286 [3,6,9,12,15: #EQn %{EQn} whd in EQn; normalize nodelta 287 [1,2,3,4: cases pre_instr in Hregs syntax_spec EQn; [2,4,6,8: #hd #tl] #Hregs #syntax_spec 288 whd in match (length ??); #EQn whd in match (length ??); normalize nodelta] 289 [5,6,7,8,9: whd in match sigma_label; normalize nodelta >code_block_of_block_eq 290 >m_return_bind >EQfn >m_return_bind inversion(find ????) 291 [1,3,5,7,9: #EQfind @⊥ lapply(find_none ?????? EQfind EQstmt) >EQn normalize nodelta 292 @eq_identifier_elim [1,3,5,7,9: #_ *] * #H #_ @H % ] * #lbl1 #stmt1 #EQfind 293 >m_return_bind @eq_f lapply(find_predicate ?????? EQfind) whd in match preamble_length; 294 normalize nodelta >code_block_of_block_eq >m_return_bind >EQfn >m_return_bind 295 whd in match (stmt_at ????); >(find_lookup ?????? EQfind) >m_return_bind >Hinit 296 >m_return_bind cases stmt1 in EQfind; stmt1 297 [1,4,7,10,13: #j_step1 #nxt1 2,5,8,11,14: #fin1 *: *] #EQfind normalize nodelta 298 cases(bind_instantiate ????) [1,3,5,7,9,11,13,15,17,19: *] 299 [1,2,3,4,5: ** #pre_instr1 #instr1 #post_instr1 *: * #pre_instr1 #instr1 ] 300 >m_return_bind cases pre_instr1 pre_instr1 [2,4,6,8,10,12,14,16,18,20: #hd #tl] 301 whd in match (length ??); normalize nodelta 302 [11,12,13,14,15,16,17,18,19,20: @eq_identifier_elim [2,4,6,8,10,12,14,16,18,20: #_ *] #EQ #_ >EQ %] 303 whd in match (nth_opt ???); inversion(nth_opt ???) [1,3,5,7,9,11,13,15,17,19: #_ *] 304 #lbl2 #EQlbl2 normalize nodelta @eq_identifier_elim [2,4,6,8,10,12,14,16,18,20: #_ *] 305 #EQ lapply EQlbl2 destruct(EQ) #EQlbl2 @⊥ 306 cases(Exists_All … (nth_opt_Exists … EQlbl2) (fresh_lab lbl1)) #x * #EQ destruct(EQ) ** 307 #H #_ @H @(code_is_in_universe … (pi2 ?? fn)) whd in match code_has_label; 308 whd in match code_has_point; normalize nodelta >EQstmt @I 309 *: cases syntax_spec syntax_spec #pre * #mid1 [3,4: * #mid2 * #post] ** [1,2: *] 310 cases pre pre [1,3,5,7: #_ * #x * #y ** #ABS destruct(ABS)] #hd1 #tl1 whd in ⊢ (??%% → ?); 311 #EQ destruct(EQ) EQ #pre_spec whd in ⊢ (% → ?); 312 [1,2: * #nxt1 * #EQt_stmt change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) #post_spec 313 *: #EQt_stmt 314 ] 315 %{mid1} cut(? : Prop) 316 [3,6,9,12: #EQnth_opt %{EQnth_opt} whd in match sigma_label; normalize nodelta 317 >code_block_of_block_eq >m_return_bind >EQfn >m_return_bind inversion(find ????) 318 [1,3,5,7: #EQfind @⊥ lapply(find_none ?????? EQfind EQstmt) >EQn normalize nodelta 319 whd in match (nth_opt ???); >EQnth_opt normalize nodelta @eq_identifier_elim 320 [1,3,5,7: #_ *] * #H #_ @H % ] * #lbl1 #stmt1 #EQfind >m_return_bind @eq_f 321 lapply(find_predicate ?????? EQfind) whd in match preamble_length; 322 normalize nodelta >code_block_of_block_eq >m_return_bind >EQfn >m_return_bind 323 whd in match (stmt_at ????); >(find_lookup ?????? EQfind) >m_return_bind >Hinit 324 >m_return_bind cases stmt1 in EQfind; stmt1 325 [1,4,7,10: #j_step1 #nxt1 2,5,8,11: #fin1 *: *] #EQfind normalize nodelta 326 cases(bind_instantiate ????) [1,3,5,7,9,11,13,15: *] 327 [1,2,3,4: ** #pre_instr1 #instr1 #post_instr1 *: * #pre_instr1 #instr1] 328 >m_return_bind cases pre_instr1 pre_instr1 [2,4,6,8,10,12,14,16: #hd1 #tl1] 329 whd in match (length ??); normalize nodelta whd in match (nth_opt ???); 330 [1,2,3,4,5,6,7,8: inversion(nth_opt ???) [1,3,5,7,9,11,13,15: #_ *] #lbl2 331 #EQlbl2 normalize nodelta @eq_identifier_elim [2,4,6,8,10,12,14,16: #_ *] 332 #EQ lapply EQlbl2 destruct(EQ) #EQlbl2 #_ @(proj2 … pp_labs ?? lbl2) 333 @Exists_memb [1,3,5,7,9,11,13,15: @(nth_opt_Exists … EQlbl2)] 334 >e0 @Exists_append2 % % 335 *: @eq_identifier_elim [2,4,6,8,10,12,14,16: #_ *] #EQ destruct(EQ) @⊥ 336 lapply(fresh_lab hd1) >e0 #H cases(append_All … H) #_ * H ** #H #_ #_ @H 337 @(code_is_in_universe … (pi2 ?? fn)) whd in match code_has_label; 338 whd in match code_has_point; normalize nodelta whd in match (stmt_at ????); 339 >(find_lookup ?????? EQfind) @I 340 ] 341 2,5,8,11: >e0 cases pre_spec #fst * #rest ** #EQ destruct(EQ) 342 whd in ⊢ (% → ?); * #nxt1 * #_ change with nxt1 in ⊢ (??%? → ?); 343 #EQ destruct(EQ) #H lapply(seq_list_in_code_length … H) 344 [1,2: >length_map] H #H >H >nth_opt_append_r cases(rest) 345 try % try( #n %) #n <minus_n_n % 346 *: 347 ] 348 ] 349 2,5,8,11,14: whd in match preamble_length; normalize nodelta >code_block_of_block_eq 350 >m_return_bind >EQfn >m_return_bind >EQstmt >m_return_bind >Hinit >m_return_bind 351 normalize nodelta 352 [1,2,3,4: >Hregs % 353  >EQregs <EQentry in EQstmt; cases(entry_is_cost … (pi2 ?? fn)) #succ * #c 354 #EQstmt >EQstmt whd in ⊢ (???% → ?); #EQ destruct(EQ) >(f_step_on_cost … data) 355 whd in match (bind_instantiate ????); % 356 ] 357 *: 358 ] 359 qed. 360 361 lemma pc_block_eq : ∀p_in,p_out,prog,stack_sizes,init,init_regs,f_lbls, 362 f_regs,pc. 363 sigma_pc_opt p_in p_out prog stack_sizes init 364 init_regs f_lbls f_regs pc ≠ None ? → 365 pc_block … pc = 366 pc_block … (sigma_stored_pc p_in p_out prog stack_sizes init 367 init_regs f_lbls f_regs pc). 368 #p_in #p_out #prog #stack_sizes #init #init_regs #f_lbls #f_regs #pc 369 whd in match sigma_stored_pc; normalize nodelta 370 inversion(sigma_pc_opt ?????????) [ #_ * #ABS @⊥ @ABS %] #pc1 371 whd in match sigma_pc_opt; normalize nodelta @eqZb_elim #_ normalize nodelta 372 [ whd in ⊢ (??%? → ?); #EQ destruct #_ %] #H @('bind_inversion H) H 373 #lbl #_ whd in ⊢ (??%? → ?); #EQ destruct #_ % 374 qed. 375 376 lemma fetch_statement_sigma_stored_pc : 377 ∀p_in,p_out,prog,stack_sizes, 378 init,init_regs,f_lbls,f_regs,pc,f,fn,stmt. 379 b_graph_transform_program_props p_in p_out stack_sizes 380 init prog init_regs f_lbls f_regs → 381 block_id … (pc_block pc) ≠ 1 → 382 let trans_prog ≝ b_graph_transform_program p_in p_out init prog in 383 fetch_statement p_in … (joint_globalenv p_in prog stack_sizes) pc = 384 return 〈f,fn,stmt〉 → 385 ∃data.bind_instantiate ?? (init … fn) (init_regs (pc_block pc)) = return data ∧ 386 match stmt with 387 [ sequential step nxt ⇒ 388 ∃step_block. bind_instantiate ?? (f_step … data (point_of_pc p_in pc) step) 389 (f_regs (pc_block pc) (point_of_pc p_in pc)) = return step_block ∧ 390 ∃pc'.sigma_stored_pc p_in p_out prog stack_sizes init 391 init_regs f_lbls f_regs pc' = pc ∧ 392 ∃fn',nxt'. 393 fetch_statement p_out … (joint_globalenv p_out trans_prog stack_sizes) pc' = 394 if not_emptyb … (added_prologue … data) ∧ 395 eq_identifier … (point_of_pc p_in pc) (joint_if_entry … fn) 396 then return 〈f,fn',sequential ?? (NOOP …) nxt'〉 397 else return 〈f,fn',sequential ?? ((\snd(\fst step_block)) (point_of_pc p_in pc')) nxt'〉 398  final fin ⇒ 399 ∃fin_block.bind_instantiate ?? (f_fin … data (point_of_pc p_in pc) fin) 400 (f_regs (pc_block pc) (point_of_pc p_in pc)) = return fin_block ∧ 401 ∃pc'.sigma_stored_pc p_in p_out prog stack_sizes init 402 init_regs f_lbls f_regs pc' = pc ∧ 403 ∃fn'.fetch_statement p_out … 404 (joint_globalenv p_out trans_prog stack_sizes) pc' 405 = return 〈f,fn',final ?? (\snd fin_block)〉 406  FCOND abs _ _ _ ⇒ Ⓧabs 407 ]. 408 #p_in #p_out #prog #stack_sizes #init #init_regs #f_lbls #f_regs #pc #f #fn #stmt 409 #good #Hbl #EQfetch 410 lapply(b_graph_transform_program_fetch_statement … good pc f fn ?) 411 [2: @eqZb_elim [1,3: #ABS @⊥ >ABS in Hbl; * #H @H %] #_ normalize nodelta 412 #H cases(H EQfetch) H *:] 413 #data * #t_fn ** #EQt_fn #Hinit #H %{data} >Hinit %{(refl …)} cases stmt in EQfetch H; 414 [ #step #nxt  #fin  *] normalize nodelta #EQfetch stmt 415 [ cases(added_prologue ??? data) [2: #hd #tl] normalize nodelta 416 [ @eq_identifier_elim #EQentry normalize nodelta ] ] 417 * #block * 418 [ whd in ⊢ (% → ?); inversion(f_regs ??) [2: #x #y #_ #_ *] #EQregs normalize nodelta 419 #EQ destruct(EQ) whd in ⊢ (% → ?); * #pre * #mid1 * #mid2 * #post *** #EQmid1 420 whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in ⊢ (% → ?); * #nxt1 421 * #EQt_stmt change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) whd in ⊢ (% → ?); 422 * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in EQmid1 : (??%%); destruct(EQmid1) 423 *: #Hregs #syntax_spec 424 ] 425 cases(fetch_statement_inv … EQfetch) #EQfn normalize nodelta #EQstmt 426 [ whd in match (point_of_pc ??) in EQstmt EQentry; <EQentry in EQstmt; 427 cases(entry_is_cost … (pi2 ?? fn)) #nxt1 * #c #EQstmt >EQstmt #EQ destruct(EQ) 428 % [2: % [ >(f_step_on_cost … data) in ⊢ (??%?); % ] ] %{pc} 429 whd in match sigma_stored_pc; whd in match sigma_pc_opt; normalize nodelta 430 @eqZb_elim normalize nodelta [#ABS >ABS in Hbl; * #H @⊥ @H %] #_ 431 *: %{block} >Hregs %{(refl …)} 432 ] 433 cases(sigma_label_spec … good … Hbl EQfn EQstmt) * [2,4,6,8: #n ] * #EQpreamble 434 normalize nodelta [1,2,3,4: * #lbl * #EQnth_opt] #EQsigma_lab 435 [ whd in match (point_of_pc ??) in e0; <EQentry in e0; #e0 >e0 in EQnth_opt; 436 whd in ⊢ (??%% → ?); #EQ destruct(EQ) 437 5: whd in match (point_of_pc ??); <EQentry >EQsigma_lab >m_return_bind 438 normalize nodelta >EQentry % [ cases pc #bl #off %] %{t_fn} %{nxt} 439 whd in match fetch_statement; normalize nodelta >EQt_fn >m_return_bind 440 >EQt_stmt >m_return_bind @eq_identifier_elim [#_ %] * #H @⊥ @H % 441 2,3,4: %{(pc_of_point p_out (pc_block pc) lbl)} 442 6,7,8: %{pc} 443 ] 444 whd in match sigma_stored_pc; whd in match sigma_pc_opt; normalize nodelta 445 @eqZb_elim [1,3,5,7,9,11: #H >H in Hbl; * #H1 @⊥ @H1 %] #_ normalize nodelta 446 [1,2,3: >point_of_pc_of_point] >EQsigma_lab >m_return_bind >(pc_of_point_of_pc … pc) 447 %{(refl …)} %{t_fn} cases block in Hregs syntax_spec; block 448 [1,2,4,5: * #pre #instr #post *: #pre #instr ] #Hregs * 449 [1,2,3,4: #l1 * #mid1 * #mid2 * #l2 *** 450 *: #l1 * #mid ** 451 ] 452 #EQmid #EQpre whd in ⊢ (% → ?); 453 [1,2,3,4: * #nxt1 *] #EQt_stmt 454 [1,2,3,4: change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) #EQpost %{mid2}] 455 whd in match fetch_statement; normalize nodelta >EQt_fn >m_return_bind 456 @('bind_inversion EQpreamble) #bl1 >code_block_of_block_eq whd in ⊢ (??%? → ?); 457 #EQ destruct(EQ) >EQfn >m_return_bind >EQstmt >m_return_bind >Hinit >m_return_bind 458 normalize nodelta >Hregs >m_return_bind cases pre in Hregs EQpre; pre 459 [1,3,6,8,9,12: [3,4,6: #x #y] #_ #_ whd in match (length ??); whd in ⊢ (??%? → ?); 460 #EQ destruct(EQ)] 461 [1,2,5: #hd1 #tl1 ] #Hregs cases l1 in EQmid; 462 [1,3,5,8,10,12: [4,5,6: #x #y] #_ whd in ⊢ (% → ?); [1,2,3: * #EQ1 #EQ2 destruct] 463 * #mid * #rest ** #EQ destruct(EQ)] 464 [1,2,3: #hd2 #tl2] whd in ⊢ (??%% → ?); #EQ destruct(EQ) whd in ⊢ (% → ?); 465 [4,5,6: * #_ #EQ #_ >EQ >EQt_stmt [2,3: %] @eq_identifier_elim [2: #_ %] 466 #EQ <EQ in EQentry; * #H @⊥ @H %] 467 * #mid' * #rest ** #EQ1 destruct(EQ1) #H1 #H2 whd in match (length ??); 468 whd in ⊢ (??%? → ?); #EQ1 destruct(EQ1) >e0 in EQnth_opt; 469 lapply(seq_list_in_code_length … H2) [1,2: >length_map] #EQ1 >EQ1 470 >nth_opt_append_r [2,4,6: %] cut(restrest=O) [1,3,5: cases(rest) //] 471 #EQ2 >EQ2 whd in ⊢ (??%% → ?); #EQ3 EQ2 EQ1 472 [1,2: destruct(EQ3) >point_of_pc_of_point >EQt_stmt [2: >point_of_pc_of_point %] 473 @eq_identifier_elim [#EQ4 <EQ4 in EQentry; * #H3 @⊥ @H3 %] #_ 474 >point_of_pc_of_point %] 475 destruct(EQ3) >point_of_pc_of_point >EQt_stmt % 476 qed. 477 478 definition make_is_relation_from_beval : (beval → beval → Prop) → 479 internal_stack → internal_stack → Prop≝ 480 λR,is1,is2. 481 match is1 with 482 [ empty_is ⇒ match is2 with [ empty_is ⇒ True  _ ⇒ False] 483  one_is b ⇒ match is2 with [ one_is b' ⇒ R b b'  _ ⇒ False ] 484  both_is b1 b2 ⇒ match is2 with [ both_is b1' b2' ⇒ R b1 b1' ∧ R b2 b2'  _ ⇒ False ] 485 ]. 486 487 lemma is_push_ok : ∀Rbeval : beval → beval → Prop. 488 ∀Ristack1 : internal_stack → internal_stack → Prop. 489 ∀Ristack2 : internal_stack → internal_stack → Prop. 490 (∀is1,is2.Ristack1 is1 is2 → make_is_relation_from_beval Rbeval is1 is2) → 491 (∀bv1,bv2.Ristack1 empty_is empty_is → Rbeval bv1 bv2 → 492 Ristack2 (one_is bv1) (one_is bv2)) → 493 (∀bv1,bv2,bv3,bv4.Rbeval bv1 bv2 → Rbeval bv3 bv4 → 494 Ristack2 (both_is bv3 bv1) (both_is bv4 bv2)) → 495 gen_preserving2 ?? gen_res_preserve … 496 Ristack1 Rbeval Ristack2 is_push is_push. 497 #Rbeval #Ristack1 #Ristack2 #H #H1 #H2 #is1 #is2 #bv1 #bv2 #H3 #H4 498 whd in match is_push; normalize nodelta cases is1 in H3; normalize nodelta 499 [2:#x3: #x #y #_ @res_preserve_error_gen] 500 cases is2 normalize nodelta 501 [1,3,5,6: [ #z #w  #z  #z #w] #H5 cases(H … H5)  #y] #H5 @m_gen_return 502 [@H2 [assumption  @(H … H5) ]  @H1 assumption] 503 qed. 504 (* 505 lemma is_push_ok : ∀R : beval → beval → Prop. 506 gen_preserving2 ?? gen_res_preserve … 507 (make_is_relation_from_beval R) R 508 (make_is_relation_from_beval R) 509 is_push is_push. 510 #R @is_push_ok_gen // #bv1 #bv2 #bv3 #bv4 #H #H1 %{H1 H} 511 qed. 512 *) 513 lemma is_pop_ok: ∀Rbeval : beval → beval → Prop. 514 ∀Ristack1 : internal_stack → internal_stack → Prop. 515 ∀Ristack2 : internal_stack → internal_stack → Prop. 516 (∀is1,is2.Ristack1 is1 is2 → make_is_relation_from_beval Rbeval is1 is2) → 517 Ristack2 empty_is empty_is → 518 (∀bv1,bv2.Rbeval bv1 bv2 → Ristack2 (one_is bv1) (one_is bv2)) → 519 gen_preserving ?? gen_res_preserve … 520 Ristack1 521 (λx,y.Rbeval (\fst x) (\fst y) ∧ 522 Ristack2 (\snd x) (\snd y)) is_pop is_pop. 523 #Rbeval #Ristack1 #Ristack2 #H #H1 #H2 #is1 #is2 whd in match is_pop; normalize nodelta 524 cases is1 normalize nodelta [#_ @res_preserve_error_gen] #x [#y] cases is2 525 [1,3,4,5: [#x #y#x] #H3 cases(H … H3)  #y  #z #w] #H3 normalize nodelta 526 @m_gen_return [ % [ @(H … H3)  assumption ]  cases(H … H3) #H4 #H5 %{H5} @(H2 … H4) 527 qed. 528 529 (* 530 lemma is_pop_ok1 : ∀R : beval → beval → Prop. 531 gen_preserving ?? gen_res_preserve … 532 (make_is_relation_from_beval R) 533 (λx,y.R (\fst x) (\fst y) ∧ 534 (make_is_relation_from_beval R) (\snd x) (\snd y)) 535 is_pop is_pop. 536 #R @is_pop_ok // 537 qed. 538 539 540 definition make_weak_state_relation ≝ 541 λp_in,p_out.λR : (beval → beval → Prop).λst1 : state p_in.λst2 : state p_out. 542 (make_is_relation_from_beval R) (istack … st1) (istack … st2). 543 *) 544 545 546 lemma push_ok : ∀p_in,p_out,Rbeval,Rstate1,Rstate2. 547 (∀is1,is2,st1,st2.istack ? st1 = is1 → istack ? st2 = is2 → Rstate1 st1 st2 → 548 make_is_relation_from_beval Rbeval is1 is2) → 549 (∀st1,st2,bv1,bv2. Rstate1 st1 st2 → Rbeval bv1 bv2 → 550 Rstate2 (set_istack p_in (one_is bv1) st1) (set_istack p_out (one_is bv2) st2)) → 551 (∀st1,st2,bv1,bv2,bv3,bv4.Rstate1 st1 st2 → Rbeval bv1 bv2 → Rbeval bv3 bv4 → 552 Rstate2 (set_istack p_in (both_is bv1 bv3) st1) (set_istack p_out (both_is bv2 bv4) st2)) → 553 gen_preserving2 ?? gen_res_preserve … Rstate1 Rbeval Rstate2 554 (push p_in) (push p_out). 555 #p_in #p_out #Rbeval #Rstate1 #Rstate2 #H #H1 #H2 #st1 #st2 #bv1 #bv2 #H3 #H4 556 whd in match push; normalize nodelta 557 @(m_gen_bind_inversion … (make_is_relation_from_beval Rbeval)) 558 [ @(is_push_ok Rbeval (make_is_relation_from_beval Rbeval)) // 559 [ #bv1 #bv2 #bv3 #bv4 #H5 #H6 whd %{H6 H5} 560  @(H … H3) % 561 ] 562  * [#x#x1 #x2] * [1,4,7:2,5,8: #y *: #y1 #y2] #H5 #H6 whd in ⊢ (% → ?); 563 [1,2,3,4,6,7,8,9: * [2: #H7 #H8]  #H7] @m_gen_return 564 [ @(H2 … H3) assumption 565  cases(istack … st1) in H5; [2,3: #z [2: #w]] whd in ⊢ (??%% → ?); 566 #EQ destruct(EQ) 567  @(H1 … H3) assumption 568 ] 569 ] 570 qed. 571 572 573 lemma pop_ok : ∀p_in,p_out,Rbeval,Rstate1,Rstate2. 574 (∀is1,is2,st1,st2.istack ? st1 = is1 → istack ? st2 = is2 → Rstate1 st1 st2 → 575 make_is_relation_from_beval Rbeval is1 is2) → 576 (∀st1,st2.Rstate1 st1 st2 → 577 Rstate2 (set_istack p_in (empty_is) st1) (set_istack p_out (empty_is) st2)) → 578 (∀st1,st2,bv1,bv2. Rstate1 st1 st2 → Rbeval bv1 bv2 → 579 Rstate2 (set_istack p_in (one_is bv1) st1) (set_istack p_out (one_is bv2) st2)) → 580 gen_preserving ?? gen_res_preserve … 581 Rstate1 582 (λx,y.Rbeval (\fst x) (\fst y) ∧ 583 Rstate2(\snd x) (\snd y)) 584 (pop p_in) (pop p_out). 585 #p_in #p_out #Rbeval #Rstate1 #Rstate2 #H #H1 #H2 #st1 #st2 #H3 586 whd in match pop; normalize nodelta 587 @(m_gen_bind_inversion … (λx,y.Rbeval (\fst x) (\fst y) ∧ 588 (make_is_relation_from_beval Rbeval (\snd x) (\snd y)))) 589 [ @(is_pop_ok Rbeval (make_is_relation_from_beval Rbeval)) // @(H … H3) % 590  * #bv1 * [#x#x1 #x2] * #bv2 * 591 [1,4,7:2,5,8: #y 592 *: #y1 #y2 [1,2: #_ #_ * #_ *] cases(istack … st1) [#z#z #w] whd in ⊢ (??%% → ?); #EQ destruct ] 593 #_ #_ * #H4 [2,3,4,6: * #_  whd in ⊢ (% → ?); #H5] @m_gen_return 594 % // [ @(H1 … H3)  @(H2 … H3) assumption] 595 qed. 596 597 598 definition joint_state_relation ≝ 599 λP_in,P_out.program_counter → state P_in → state P_out → Prop. 600 601 definition joint_state_pc_relation ≝ λP_in,P_out.state_pc P_in → state_pc P_out → Prop. 206 602 207 603 … … 219 615 ; fetch_ok_sigma_state_ok : 220 616 ∀st1,st2,f,fn. st_rel st1 st2 → 221 fetch_internal_function … (prog_var_names … prog)617 fetch_internal_function … 222 618 (joint_globalenv P_in prog stack_sizes) (pc_block (pc … st1)) 223 619 = return 〈f,fn〉 → … … 225 621 ; fetch_ok_pc_ok : 226 622 ∀st1,st2,f,fn.st_rel st1 st2 → 227 fetch_internal_function … (prog_var_names … prog)623 fetch_internal_function … 228 624 (joint_globalenv P_in prog stack_sizes) (pc_block (pc … st1)) 229 625 = return 〈f,fn〉 → … … 231 627 ; fetch_ok_sigma_last_pop_ok : 232 628 ∀st1,st2,f,fn.st_rel st1 st2 → 233 fetch_internal_function … (prog_var_names … prog)629 fetch_internal_function … 234 630 (joint_globalenv P_in prog stack_sizes) (pc_block (pc … st1)) 235 631 = return 〈f,fn〉 → … … 238 634 ; st_rel_def : 239 635 ∀st1,st2,pc,lp1,lp2,f,fn. 240 fetch_internal_function … (prog_var_names … prog)636 fetch_internal_function … 241 637 (joint_globalenv P_in prog stack_sizes) (pc_block pc) = return 〈f,fn〉 → 242 638 st_no_pc_rel pc st1 st2 → … … 247 643 let trans_prog ≝ b_graph_transform_program P_in P_out init prog in 248 644 ∀st1,st2,f,fn,stmt. 249 fetch_statement … (prog_var_names … prog)645 fetch_statement … 250 646 (joint_globalenv P_in prog stack_sizes) (pc … st1) = return〈f,fn,stmt〉 → 251 647 st_rel st1 st2 → point_of_pc P_in (pc … st1) ≠ joint_if_entry … fn → … … 262 658 joint_classify … (mk_prog_params P_in prog stack_sizes) st1 = 263 659 joint_classify … (mk_prog_params P_out trans_prog stack_sizes) st2 ∧ 264 (eval_state P_in (prog_var_names … prog)(joint_globalenv P_in prog stack_sizes)660 (eval_state P_in … (joint_globalenv P_in prog stack_sizes) 265 661 st1 = return st1' → 266 662 ∃st2'. st_rel st1' st2' ∧ 267 eval_state P_out (prog_var_names … trans_prog)663 eval_state P_out … 268 664 (joint_globalenv P_out trans_prog stack_sizes) st2 = return st2') 269 665 ; cond_commutation : 270 666 let trans_prog ≝ b_graph_transform_program P_in P_out init prog in 271 ∀st1 ,st1': joint_abstract_status (mk_prog_params P_in prog stack_sizes) .667 ∀st1 : joint_abstract_status (mk_prog_params P_in prog stack_sizes) . 272 668 ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes). 273 ∀f,fn,a,ltrue,lfalse .669 ∀f,fn,a,ltrue,lfalse,bv,b. 274 670 block_id … (pc_block (pc … st1)) ≠ 1 → 275 671 let cond ≝ (COND P_in ? a ltrue) in 276 672 fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) = 277 673 return 〈f, fn, sequential … cond lfalse〉 → 278 eval_state P_in (prog_var_names … prog)279 (joint_globalenv P_in prog stack_sizes) st1 = return st1'→674 acca_retrieve … P_in (st_no_pc … st1) a = return bv → 675 bool_of_beval … bv = return b → 280 676 st_rel st1 st2 → 281 677 ∀t_fn. 282 fetch_internal_function … (prog_var_names … trans_prog)678 fetch_internal_function … 283 679 (joint_globalenv P_out trans_prog stack_sizes) (pc_block (pc … st2)) = 284 680 return 〈f,t_fn〉 → … … 287 683 (λregs2.λblp.(\snd blp) = [ ] ∧ 288 684 ∀mid. 289 stmt_at ? (prog_var_names … trans_prog)(joint_if_code ?? t_fn) mid685 stmt_at P_out … (joint_if_code ?? t_fn) mid 290 686 = return sequential P_out ? ((\snd (\fst blp)) mid) lfalse→ 291 687 ∃st2_pre_mid_no_pc. 292 repeat_eval_seq_no_pc …(mk_prog_params P_out trans_prog stack_sizes) f688 repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f 293 689 (map_eval ?? (\fst (\fst blp)) mid) (st_no_pc ? st2) 294 690 = return st2_pre_mid_no_pc ∧ 295 st_no_pc_rel (pc … st1') (st_no_pc … st1') (st2_pre_mid_no_pc) ∧ 296 joint_classify_step … ((\snd (\fst blp)) mid) = cl_jump ∧ 297 cost_label_of_stmt P_out (prog_var_names … trans_prog) 298 (sequential P_out ? ((\snd (\fst blp)) mid) lfalse) = None ? ∧ 299 let st2_pre_mid ≝ mk_state_pc P_out st2_pre_mid_no_pc 691 let new_pc ≝ if b then 692 (pc_of_point P_in (pc_block (pc … st1)) ltrue) 693 else 694 (pc_of_point P_in (pc_block (pc … st1)) lfalse) in 695 st_no_pc_rel new_pc (st_no_pc … st1) (st2_pre_mid_no_pc) ∧ 696 ∃a'. ((\snd (\fst blp)) mid) = COND P_out ? a' ltrue ∧ 697 ∃bv'. acca_retrieve … P_out st2_pre_mid_no_pc a' = return bv' ∧ 698 bool_of_beval … bv' = return b 699 (*let st2_pre_mid ≝ mk_state_pc P_out st2_pre_mid_no_pc 300 700 (pc_of_point P_out (pc_block (pc … st2)) mid) (last_pop … st2) in 301 701 let st2' ≝ mk_state_pc P_out st2_pre_mid_no_pc (pc … st1') (last_pop … st2) in 302 702 eval_statement_advance P_out (prog_var_names … trans_prog) 303 703 (joint_globalenv P_out trans_prog stack_sizes) f t_fn 304 (sequential P_out ? ((\snd (\fst blp)) mid) lfalse) st2_pre_mid = return st2' 704 (sequential P_out ? ((\snd (\fst blp)) mid) lfalse) st2_pre_mid = return st2'*) 305 705 ) (f_step … data (point_of_pc P_in (pc … st1)) cond) 306 706 ) (init ? fn) … … 314 714 fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) = 315 715 return 〈f, fn, sequential … seq nxt〉 → 316 eval_state P_in (prog_var_names … prog)(joint_globalenv P_in prog stack_sizes)716 eval_state P_in … (joint_globalenv P_in prog stack_sizes) 317 717 st1 = return st1' → 318 718 st_rel st1 st2 → 319 719 ∀t_fn. 320 fetch_internal_function … (prog_var_names … trans_prog)720 fetch_internal_function … 321 721 (joint_globalenv P_out trans_prog stack_sizes) (pc_block (pc … st2)) = 322 722 return 〈f,t_fn〉 → … … 324 724 (λregs1.λdata.bind_new_P' ?? 325 725 (λregs2.λblp. 326 ∃l : list (joint_seq P_out ( prog_var_names … trans_prog)).726 ∃l : list (joint_seq P_out (globals ? (mk_prog_params P_out trans_prog stack_sizes))). 327 727 blp = (ensure_step_block ?? l) ∧ 328 728 ∃st2_fin_no_pc. 329 repeat_eval_seq_no_pc …(mk_prog_params P_out trans_prog stack_sizes) f729 repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f 330 730 l (st_no_pc … st2)= return st2_fin_no_pc ∧ 331 731 st_no_pc_rel (pc … st1') (st_no_pc … st1') st2_fin_no_pc … … 341 741 st_no_pc_rel (pc_of_point P_in (pc_block pc) nxt) st1 st2 342 742 }. 343 344 (*TO BE MOVED*)345 lemma decidable_In : ∀A.∀l : list A. ∀a : A. (∀a'.decidable (a = a')) →346 decidable (In A l a).347 #A #l elim l [ #a #_ %2 % *] #hd #tl #IH #a #DEC cases(IH a DEC)348 [ #H % %2 assumption  * #H cases (DEC hd)349 [ #H1 %1 %1 assumption  * #H1 %2 % * [ #H2 @H1 assumption  #H2 @H assumption]]350 qed.351 352 lemma In_all : ∀A.∀l : list A. ∀ a : A.¬In A l a → All A (λx.x≠a) l.353 #A #l elim l [ #a #_ @I] #hd #tl #IH #a * #H % [2: @IH % #H1 @H %2 assumption]354 % #H1 @H % >H1 %355 qed.356 357 lemma All_In : ∀A.∀l : list A. ∀ a : A.All A (λx.x≠a) l → ¬In A l a.358 #A #l elim l [#a #_ % *] #hd #tl #IH #a ** #H1 #H2 % *359 [ #H3 @H1 >H3 %  cases(IH a H2) #H3 #H4 @H3 assumption]360 qed.361 743 362 744 lemma fetch_stmt_ok_succ_ok : ∀p : sem_graph_params. … … 415 797 ∀f,fn,stmt,st1,st2. 416 798 good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs 417 st_no_pc_rel st_rel 799 st_no_pc_rel st_rel→ 418 800 st_rel st1 st2 → 419 801 fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) = … … 477 859 qed.*) 478 860 479 (*TO BE MOVED*)480 lemma append_All : ∀A : Type[0]. ∀ P : A → Prop. ∀l1,l2 : list A.481 All ? P (l1 @ l2) → All ? P l1 ∧ All ? P l2.482 #A #P #l1 elim l1483 [ #l2 change with l2 in ⊢ (???% → ?); #H % //]484 #a #tl #IH #l2 change with (P a ∧ All A P (tl @ l2)) in ⊢ (% → ?);485 * #H1 #H2 lapply(IH … H2) * #H3 #H4 % // whd % //486 qed.487 861 488 862 lemma general_eval_cond_ok : ∀ P_in , P_out: sem_graph_params. … … 495 869 let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in 496 870 good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs 497 st_no_pc_rel st_rel →871 st_no_pc_rel st_rel → 498 872 ∀st1,st1' : joint_abstract_status prog_pars_in. 499 873 ∀st2 : joint_abstract_status prog_pars_out. 500 ∀f .501 ∀fn : joint_closed_internal_function P_in (prog_var_names … prog).874 ∀f : ident. 875 ∀fn : joint_closed_internal_function P_in ?. 502 876 ∀a,ltrue,lfalse. 503 877 block_id … (pc_block (pc … st1)) ≠ 1 → 504 878 st_rel st1 st2 → 505 879 let cond ≝ (COND P_in ? a ltrue) in 506 fetch_statement P_in …880 fetch_statement P_in ? 507 881 (joint_globalenv P_in prog stack_sizes) (pc … st1) = 508 return 〈f, fn, 509 eval_state P_in (prog_var_names … prog)882 return 〈f, fn, sequential … cond lfalse〉 → 883 eval_state P_in … 510 884 (joint_globalenv P_in prog stack_sizes) st1 = return st1' → 511 885 as_costed (joint_abstract_status prog_pars_in) st1' → … … 514 888 bool_to_Prop (taaf_non_empty … taf). 515 889 #P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_bl_r #init #st_no_pc_rel 516 #st_rel #goodR #st1 #st1' #st2 #f #fn #a #ltrue #lfalse * #Hbl #Rst1st2 #EQfetch517 #EQ eval890 #st_rel #goodR #st1 #st1' #st2 #f #fn #a #ltrue #lfalse * #Hbl #Rst1st2 891 #EQfetch #EQeval 518 892 @('bind_inversion EQeval) #x >EQfetch whd in ⊢ (??%% → ?); #EQ destruct(EQ) 519 893 whd in match eval_statement_no_pc; normalize nodelta >m_return_bind … … 543 917 * #EQmid change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) 544 918 cases(bind_new_bind_new_instantiates … EQbl (bind_new_bind_new_instantiates … Hinit 545 (cond_commutation … goodR … EQfetch EQ eval Rst1st2 t_fn1 EQt_fn1)))919 (cond_commutation … goodR … EQfetch EQbv EQbool Rst1st2 t_fn1 EQt_fn1))) 546 920 [2,4: % assumption] 547 921 #EQ destruct(EQ) #APP whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2) 548 cases(APP … EQmid) APP #st_pre_mid_no_pc **** whd in match set_no_pc; normalize nodelta 549 #EQst_pre_mid_no_pc #Hsem #CL_JUMP #COST #Hst2_mid 922 cases(APP … EQmid) APP #st_pre_mid_no_pc * #EQst_pre_mid_no_pc * 923 normalize nodelta 924 #Hsem * #a' * #EQt_cond * #bv' * #EQbv' #rel_v_v' 550 925 [ %{(mk_state_pc ? st_pre_mid_no_pc (pc_of_point P_in (pc_block (pc … st1)) ltrue) 551 926 (last_pop … st2))} … … 572 947 whd in match fetch_statement; normalize nodelta >EQt_fn1 >m_return_bind 573 948 whd in match (as_pc_of ??); whd in match point_of_pc; normalize nodelta 574 >point_of_offset_of_point >EQmid >m_return_bind normalize nodelta > COST*949 >point_of_offset_of_point >EQmid >m_return_bind normalize nodelta >EQt_cond * 575 950 #H @H % 576 951 ] … … 594 969 2,5: whd whd in match (as_classify ??); whd in match fetch_statement; normalize nodelta 595 970 >EQt_fn1 >m_return_bind >point_of_pc_of_point >EQmid normalize nodelta 596 assumption971 >EQt_cond % 597 972 *: whd whd in match eval_state; whd in match fetch_statement; normalize nodelta 598 >EQt_fn1 >m_return_bind >point_of_pc_of_point >EQmid >m_return_bind 599 cases(blm mid1) in CL_JUMP COST Hst2_mid; 600 [1,5: #c #_ whd in ⊢ (??%% → ?); #EQ destruct(EQ) 601 2,4,6,8: [1,3: #c_id #args #dest *: #seq] whd in ⊢ (??%% → ?); #EQ destruct(EQ) 602 ] 603 #r #ltrue #_ #_ #Hst2_mid whd in match eval_statement_no_pc; normalize nodelta 604 >m_return_bind assumption 973 >EQt_fn1 >m_return_bind >point_of_pc_of_point >EQmid >m_return_bind >EQt_cond 974 whd in match eval_statement_no_pc; normalize nodelta >m_return_bind 975 whd in match eval_statement_advance; normalize nodelta >EQbv' >m_return_bind 976 >rel_v_v' >m_return_bind normalize nodelta 977 [ whd in match goto; normalize nodelta >(pc_of_label_eq … EQt_fn1)] 978 >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 … EQfetch) % 605 979 ] 606 980 qed. … … 619 993 ∀st1,st1' : joint_abstract_status prog_pars_in. 620 994 ∀st2 : joint_abstract_status prog_pars_out. 621 ∀f.∀fn : joint_closed_internal_function P_in (prog_var_names … prog).995 ∀f.∀fn : joint_closed_internal_function P_in ?. 622 996 ∀stmt,nxt. 623 997 block_id … (pc_block (pc … st1)) ≠ 1 → … … 627 1001 (joint_globalenv P_in prog stack_sizes) (pc … st1) = 628 1002 return 〈f, fn, sequential ?? seq nxt〉 → 629 eval_state P_in (prog_var_names … prog)(joint_globalenv P_in prog stack_sizes)1003 eval_state P_in … (joint_globalenv P_in prog stack_sizes) 630 1004 st1 = return st1' → 631 1005 ∃st2'. st_rel st1' st2' ∧ … … 688 1062 ∀st2 : joint_abstract_status prog_pars_out. 689 1063 ∀f. 690 ∀fn : joint_closed_internal_function P_in (prog_var_names … prog).∀c,nxt.1064 ∀fn : joint_closed_internal_function P_in ?.∀c,nxt. 691 1065 block_id … (pc_block (pc … st1)) ≠ 1 → 692 1066 st_rel st1 st2 → … … 695 1069 (joint_globalenv P_in prog stack_sizes) (pc … st1) = 696 1070 return 〈f, fn, sequential ?? cost nxt〉 → 697 eval_state P_in (prog_var_names … prog)(ev_genv … prog_pars_in)1071 eval_state P_in … (ev_genv … prog_pars_in) 698 1072 st1 = return st1' → 699 1073 ∃ st2'. st_rel st1' st2' ∧
Note: See TracChangeset
for help on using the changeset viewer.