- Timestamp:
- Dec 4, 2012, 6:16:25 PM (7 years ago)
- Location:
- src/joint
- Files:
-
- 6 edited
Legend:
- Unmodified
- Added
- Removed
-
src/joint/Traces.ma
r2484 r2529 15 15 { prog_spars : sem_params 16 16 ; prog : joint_program prog_spars 17 ; stack_sizes : (Σi.is_internal_function_of_program … prog i) →ℕ17 ; stack_sizes : ident → option ℕ 18 18 (* ; prog_io : state prog_spars → ∀o.res (io_in o) *) 19 19 }. … … 78 78 let 〈m,ispb〉 ≝ alloc … m 0 internal_ram_size XData in 79 79 let dummy_pc ≝ mk_program_counter «mk_block Code (-1), refl …» one in 80 let spp : xpointer ≝ mk_pointer spb (mk_offset (bitvector_of_Z ? external_ram_size)) in 80 let spp : xpointer ≝ 81 «mk_pointer spb (mk_offset (bitvector_of_Z ? external_ram_size)), 82 pi2 … spb» in 81 83 (* let ispp : xpointer ≝ mk_pointer ispb (mk_offset (bitvector_of_nat ? 47)) in *) 82 84 let main ≝ prog_main … p in … … 86 88 ! st0'' ← save_frame ?? sem_globals (call_dest_for_main … pars) st0' ; 87 89 let st_pc0 ≝ mk_state_pc ? st0'' dummy_pc in 88 ! main ← opt_to_res … [MSG BadMain; CTX ? main ] (funct_of_ident … gemain) ;89 match ? return λx.description_of_function … main = x → ? with90 [ Internal fn ⇒ λprf.91 let main : Σi : ident.is_internal_function ??? ≝ «main, ?» in92 ! st' ← eval_internal_call_no_pc ?? ge main (call_args_for_main … pars) st_pc0 ;93 let pc' ≝ eval_internal_call_pc … ge mainin90 ! bl ← block_of_call … ge st_pc0 (inl … main) ; 91 ! 〈i, fn〉 ← fetch_function … ge bl ; 92 match fn with 93 [ Internal ifn ⇒ 94 ! st' ← eval_internal_call_no_pc … ge i ifn (call_args_for_main … pars) st_pc0 ; 95 let pc' ≝ pc_of_point … bl (joint_if_entry … ifn) in 94 96 return mk_state_pc … st' pc' 95 | External _ ⇒ λ_.Error … [MSG BadMain; CTX ? main] (* External main not supported: why? *) 96 ] (refl …). 97 [ @(description_of_internal_function … prf) 98 | cases spb normalize // 99 ] 100 qed. 97 | External _ ⇒ Error … [MSG BadMain; CTX ? main] (* External main not supported: why? *) 98 ]. 101 99 102 100 definition joint_classify_seq : … … 105 103 match stmt with 106 104 [ CALL f args dest ⇒ 107 match function_of_call ?? (ev_genv p) st f with 108 [ OK fn ⇒ 109 match description_of_function … fn with 105 match (! bl ← block_of_call … (ev_genv p) st f ; 106 fetch_function … (ev_genv p) bl) with 107 [ OK id_fn ⇒ 108 match \snd id_fn with 110 109 [ Internal _ ⇒ cl_call 111 110 | External _ ⇒ cl_other … … 136 135 ∀p : evaluation_params.state_pc p → status_class ≝ 137 136 λp,st. 138 match fetch_statement ? p… (ev_genv p) (pc … st) with139 [ OK f_s ⇒140 match \snd f_s with137 match fetch_statement … (ev_genv p) (pc … st) with 138 [ OK i_f_s ⇒ 139 match \snd i_f_s with 141 140 [ sequential s _ ⇒ joint_classify_step p st s 142 141 | final s ⇒ joint_classify_final p s … … 145 144 ]. 146 145 146 definition no_call : ∀p,g.joint_seq p g → Prop ≝ 147 λp,g,s.match s with 148 [ CALL _ _ _ ⇒ False 149 | _ ⇒ True 150 ]. 151 152 definition no_cost_label : ∀p,g.joint_seq p g → Prop ≝ 153 λp,g,s.match s with 154 [ COST_LABEL _ ⇒ False 155 | _ ⇒ True 156 ]. 157 158 lemma no_call_advance : ∀p : evaluation_params. 159 ∀s,nxt.∀st : state_pc p. 160 no_call p (globals p) s → 161 eval_seq_advance p (globals p) (ev_genv p) s nxt st = return next … nxt st. 162 #p * // #f #args #dest #nxt #st * 163 qed. 164 165 lemma no_call_other : ∀p : evaluation_params.∀st,s. 166 no_call p (globals p) s → 167 joint_classify_seq … st s = cl_other. 168 #p #st * // #f #args #dest * 169 qed. 170 171 lemma cond_call_other : 172 ∀p,globals.∀P : joint_step p globals → Prop. 173 (∀a,lbltrue.P (COND … a lbltrue)) → 174 (∀f,args,dest.P (CALL … f args dest)) → 175 (∀s.no_call ?? s → P s) → 176 ∀s.P s. 177 #p #globals #P #H1 #H2 #H3 * // * /2 by / qed. 178 147 179 lemma joint_classify_call : ∀p : evaluation_params.∀st. 148 180 joint_classify p st = cl_call → 149 ∃ f,f',args,dest,next,fn,fd.150 fetch_statement ? p… (ev_genv p) (pc … st) =151 OK ? 〈 f, sequential … (CALL … f' args dest) next〉 ∧152 function_of_call … (ev_genv p) st f' = OK ? fn∧153 description_of_function … (ev_genv p) fn = Internal … fd.181 ∃i_f,f',args,dest,next,bl,i',fd'. 182 fetch_statement … (ev_genv p) (pc … st) = 183 OK ? 〈i_f, sequential … (CALL … f' args dest) next〉 ∧ 184 block_of_call … (ev_genv p) st f' = OK ? bl ∧ 185 fetch_internal_function … (ev_genv p) bl = OK ? 〈i', fd'〉. 154 186 #p #st 155 187 whd in match joint_classify; normalize nodelta 156 inversion (fetch_statement ? p … (ev_genv p) (pc … st)) normalize nodelta 157 [ * #f * [| * [ #lbl || #b #f #args ]] 158 [ * [| #a #lbl #next ] 159 [ * 160 [14: #f' #args #dest | #s | #lbl | #mv | #a | #a | #i #prf #dpl #dph | #op #a #b #a' #b' 161 | #op #a #a' | #op #a #a' #arg ||| #a #dpl #dph | #dpl #dph #arg 162 | #ext ] #next 163 [ whd in match joint_classify_step; whd in match joint_classify_seq; 164 normalize nodelta 165 inversion (function_of_call ?????) normalize nodelta 166 [ #fn 167 inversion (description_of_function ?? fn) #fd 168 #EQfd 169 | #e 170 ] #EQfn 171 ] 188 inversion (fetch_statement … (ev_genv p) (pc … st)) normalize nodelta 189 [2: #e #_ #ABS destruct(ABS) ] 190 * #i_f * [2: * [ #lbl | | #fl #f #args ] #_ normalize in ⊢ (%→?); #ABS destruct(ABS) ] 191 @cond_call_other 192 [ #a #lbl #nxt #_ normalize in ⊢ (%→?); #ABS destruct(ABS) 193 |3: #s #no_call #nxt #_ whd in match joint_classify_step; 194 normalize nodelta >(no_call_other … no_call) #ABS destruct(ABS) 195 ] 196 #f' #args #dest #nxt #fetch 197 whd in match joint_classify_step; whd in match joint_classify_seq; 198 normalize nodelta 199 inversion (block_of_call ?????) 200 [ #bl #block_of_c >m_return_bind 201 inversion (fetch_function ???) 202 [ * #i' * 203 [ #fd' #fetch' #_ 204 %{i_f} %{f'} %{args} %{dest} %{nxt} %{bl} %{i'} %{fd'} 205 % [ %{block_of_c} % ] 206 whd in match fetch_internal_function; normalize nodelta 207 >fetch' % 172 208 ] 173 209 ] 174 | #e 175 ] #EQfetch 176 [|*: #ABS normalize in ABS; destruct(ABS) ] 177 normalize nodelta #_ 178 %{f} %{f'} %{args} %{dest} %{next} %{fn} %{fd} 179 %{EQfd} %{EQfn} % 210 ] 211 #x #_ normalize in ⊢ (%→?); #ABS destruct(ABS) 180 212 qed. 181 213 … … 183 215 (Σs : state_pc p.joint_classify p s = cl_call) → state_pc p → Prop ≝ 184 216 λp,s1,s2. 185 match fetch_statement ? p… (ev_genv p) (pc … s1) with217 match fetch_statement … (ev_genv p) (pc … s1) with 186 218 [ OK x ⇒ 187 219 match \snd x with 188 220 [ sequential s next ⇒ 189 pc … s2 = succ_pc p p(pc … s1) next221 pc … s2 = succ_pc p (pc … s1) next 190 222 | _ ⇒ False (* never happens *) 191 223 ] … … 225 257 I think handling of the function is easier *) 226 258 λp,st. 227 let dummy : ident ≝ an_identifier ? one in 228 match fetch_statement ? p… (ev_genv p) (pc … st) with259 let dummy : ident ≝ an_identifier ? one in (* used where it cannot ever happen *) 260 match fetch_statement … (ev_genv p) (pc … st) with 229 261 [ OK x ⇒ 230 262 match \snd x with … … 234 266 match s with 235 267 [ CALL f' args dest ⇒ 236 match function_of_call … (ev_genv p) st f' with 237 [ OK f ⇒ f 268 match 269 (! bl ← block_of_call … (ev_genv p) st f' ; 270 fetch_internal_function … (ev_genv p) bl) with 271 [ OK i_f ⇒ \fst i_f 238 272 | _ ⇒ dummy 239 273 ] … … 279 313 | _ ⇒ None ? 280 314 ]. 315 316 317 lemma no_label_uncosted : ∀p : evaluation_params.∀s,nxt. 318 no_cost_label p (globals p) s → 319 cost_label_of_stmt … (sequential … s nxt) = None ?. 320 #p * // #lbl #next * 321 qed. 281 322 282 323 definition joint_abstract_status : … … 293 334 (* as_label_of_pc ≝ *) 294 335 (λpc. 295 match fetch_statement ? p… (ev_genv p) pc with336 match fetch_statement … (ev_genv p) pc with 296 337 [ OK fn_stmt ⇒ cost_label_of_stmt … (\snd fn_stmt) 297 338 | _ ⇒ None ? … … 300 341 (* as_final ≝ *) (λs.is_final p (globals ?) (ev_genv p) (exit p) s ≠ None ?) 301 342 (* as_call_ident ≝ *) (joint_call_ident p). 343 -
src/joint/linearise.ma
r2481 r2529 173 173 ] n_prf 174 174 ] (chop_ok ? (λx.x∈visited) visiting). 175 (* cases daemon qed. *)175 (* cases daemon qed. *) 176 176 whd 177 177 [ (* base case, visiting is all visited *) … … 555 555 qed. 556 556 557 558 557 definition good_local_sigma : 559 558 ∀p:unserialized_params. … … 565 564 λp,globals,g,entry,c,sigma. 566 565 sigma entry = Some ? 0 ∧ 566 (∀l,n.point_of_label … c l = Some ? n → sigma l = Some ? n) ∧ 567 567 ∀l,n.sigma l = Some ? n → 568 ∃s. lookup … g l = Some ? s ∧ 569 opt_Exists ? 570 (λls.let 〈lopt, ts〉 ≝ ls in 571 opt_All ? (eq ? l) lopt ∧ 572 ts = graph_to_lin_statement … s ∧ 573 opt_All ? 574 (λnext.Or (sigma next = Some ? (S n)) 575 (nth_opt … (S n) c = Some ? 〈None ?, GOTO … next〉)) 576 (stmt_implicit_label … s)) (nth_opt … n c). 568 ∃s. stmt_at … g l = Some ? s ∧ 569 All ? (λl.sigma l ≠ None ?) (stmt_labels … s) ∧ 570 opt_All ? 571 (λnext.Or (sigma next = Some ? (S n)) 572 (stmt_at … c (S n) = Some ? (GOTO … next))) 573 (stmt_implicit_label … s) ∧ 574 stmt_at … c n = Some ? (graph_to_lin_statement … s). 577 575 578 576 definition linearise_code: … … 624 622 #entry_O #req_vis #last_fin #labels_in_req #sigma_prop 625 623 % 626 [ % [assumption] 627 #lbl #n #eq_lookup elim (sigma_prop ?? eq_lookup) 628 #lbl_in_gen * #stmt ** #stmt_in_g #nth_opt_is_stmt #succ_is_in 629 % [2: % [ assumption ] |] 630 >nth_opt_filter_labels in ⊢ (???%); 631 >nth_opt_is_stmt >m_return_bind whd >m_return_bind 632 % [ % ] 633 [ elim (lbl ∈ required) % 634 | % 635 | lapply succ_is_in 636 lapply (refl … (stmt_implicit_label … stmt)) 637 cases (stmt_implicit_label … stmt) in ⊢ (???%→%); [#_ #_ %] 638 #next #EQ_next * 639 [ #H %1{H} ] 640 #H %2 641 >nth_opt_filter_labels >H % 624 [ % [ % [assumption]] 625 #lbl #n 626 [ change with (If ? then with prf do ? else ? = ? → ?) 627 @If_elim [2: #_ #ABS destruct(ABS) ] 628 #H lapply H 629 >occurs_exactly_once_filter_labels 630 elim (true_or_false_Prop … (occurs_exactly_once ?? lbl ?)) 631 [1,2: #H1 >H1 |*:] [2: * ] 632 elim (true_or_false_Prop … (lbl ∈ required)) #H2 >H2 * 633 lapply (in_map_domain … visited lbl) >(req_vis … H2) 634 * #n_lbl #EQsigma 635 elim (sigma_prop … EQsigma) #_ * #stmt ** #_ #EQnth_opt #_ 636 >(nth_opt_index_of_label ???? n_lbl (graph_to_lin_statement … stmt) H) 637 [ normalize in ⊢ (% → ?); #EQ destruct(EQ) assumption 638 | >nth_opt_filter_labels >EQnth_opt >m_return_bind >m_return_bind 639 >H2 % 640 ] 641 | #eq_lookup elim (sigma_prop ?? eq_lookup) 642 #lbl_in_gen * #stmt ** #stmt_in_g #nth_opt_is_stmt #succ_is_in 643 % [2: % [ % [ % [ assumption ]]] |] 644 [ @All_append 645 [ lapply succ_is_in elim (stmt_implicit_label ???) [ * % ] 646 #nxt #nxt_spec % [2: %] cases nxt_spec -nxt_spec 647 [ #EQ >EQ % #ABS destruct(ABS) 648 | #goto_in lapply (in_map_domain … visited nxt) 649 >req_vis [ * #n #EQ >EQ % #ABS destruct(ABS) ] 650 @(proj1 … (labels_in_req (S n) (GOTO … nxt) …)) 651 whd in ⊢ (??%?); >goto_in % 652 ] 653 | <graph_to_lin_labels @(All_mp … (labels_in_req …)) 654 [ #lbl #H 655 lapply (in_map_domain … visited lbl) >(req_vis … H) * #n #EQ >EQ % #ABS destruct(ABS) 656 | whd in ⊢ (??%?); >nth_opt_is_stmt % | 657 ] 658 ] 659 | lapply succ_is_in 660 cases (stmt_implicit_label … stmt) [#_ %] 661 #next * 662 [ #H %1{H} ] 663 #H %2 664 >stmt_at_filter_labels whd in ⊢ (??%?); >H % 665 | >stmt_at_filter_labels whd in ⊢ (??%?); >nth_opt_is_stmt % 666 ] 642 667 ] 643 668 | #i #s … … 711 736 [ @H2 712 737 | @H1 713 | cases H1 #H3 #H4 elim (H4… H3)714 #s * #_ >lin_code_has_point cases code715 [ *| #hd #tl #_ % ]738 | cases H1 * #H3 #H4 #H5 elim (H5 … H3) 739 #s *** #_ #_ #_ >lin_code_has_point cases code 740 [ #ABS normalize in ABS; destruct(ABS) | #hd #tl #_ % ] 716 741 ] 717 742 qed. … … 724 749 (λglobals.transf_fundef ?? (λf_in.\fst (linearise_int_fun p globals f_in))). 725 750 726 751 (* 727 752 definition good_sigma : 728 753 ∀p:unserialized_params. … … 742 767 #p #prog 743 768 letin sigma ≝ 744 (λi : Σi.is_internal_function_of_program … prog i. 745 let fn_in ≝ if_of_function … i in 769 (λi : Σi.is_internal_function_of_program … prog i. let fn_in ≝ if_of_function … i in 746 770 \snd (linearise_int_fun … fn_in)) 747 771 %{sigma} … … 751 775 normalize nodelta #prf @prf 752 776 qed. 777 *) -
src/joint/lineariseProof.ma
r2528 r2529 26 26 (∀F.sem_unserialized_params p F) → 27 27 ∀prog : joint_program (mk_graph_params p). 28 ( (Σi.is_internal_function_of_program … prog i) →ℕ) →28 (ident → option ℕ) → 29 29 abstract_status 30 30 ≝ … … 40 40 (∀F.sem_unserialized_params p F) → 41 41 ∀prog : joint_program (mk_lin_params p). 42 ( (Σi.is_internal_function_of_program … prog i) →ℕ) →42 (ident → option ℕ) → 43 43 abstract_status 44 44 ≝ … … 97 97 *) 98 98 99 definition sigma_map ≝ λp.λgraph_prog : joint_program (mk_graph_params p). 100 joint_closed_internal_function (mk_graph_params p) (prog_var_names … graph_prog) → 101 label → option ℕ. 102 99 103 definition sigma_pc_opt: 100 ∀p,p'.∀graph_prog : joint_program (mk_graph_params p). 101 ((Σi.is_internal_function_of_program … graph_prog i) → 102 code_point (mk_graph_params p) → option ℕ) → 104 ∀p,p'.∀graph_prog. 105 sigma_map p graph_prog → 103 106 program_counter → option program_counter 104 107 ≝ … … 106 109 let pars ≝ make_sem_graph_params p p' in 107 110 let ge ≝ globalenv_noinit … prog in 108 ! f ← int_funct_of_block ? ge (pc_block pc) ; 109 ! lin_point ← sigma f (point_of_pc ? pars pc) ; 110 return pc_of_point ? (make_sem_lin_params ? p') pc lin_point. 111 ! 〈i, fd〉 ← res_to_opt … (fetch_internal_function … ge (pc_block pc)) ; 112 ! lin_point ← sigma fd (point_of_pc pars pc) ; 113 return pc_of_point 114 (make_sem_lin_params ? p') (pc_block pc) lin_point. 111 115 112 116 definition well_formed_pc: 113 117 ∀p,p',graph_prog. 114 ((Σi.is_internal_function_of_program … graph_prog i) → 115 label → option ℕ) → 118 sigma_map p graph_prog → 116 119 program_counter → Prop 117 120 ≝ … … 122 125 definition sigma_beval_opt : 123 126 ∀p,p'.∀graph_prog : joint_program (mk_graph_params p). 124 ((Σi.is_internal_function_of_program … graph_prog i) → 125 code_point (mk_graph_params p) → option ℕ) → 127 sigma_map p graph_prog → 126 128 beval → option beval ≝ 127 129 λp,p',graph_prog,sigma,bv. … … 138 140 definition sigma_is_opt : 139 141 ∀p,p'.∀graph_prog : joint_program (mk_graph_params p). 140 ((Σi.is_internal_function_of_program … graph_prog i) → 141 code_point (mk_graph_params p) → option ℕ) → 142 sigma_map p graph_prog → 142 143 internal_stack → option internal_stack ≝ 143 144 λp,p',graph_prog,sigma,is. … … 167 168 definition well_formed_mem : 168 169 ∀p,p'.∀graph_prog : joint_program (mk_graph_params p). 169 ((Σi.is_internal_function_of_program … graph_prog i) → 170 code_point (mk_graph_params p) → option ℕ) → 170 sigma_map p graph_prog → 171 171 bemem → Prop ≝ 172 172 λp,p',graph_prog,sigma,m. … … 311 311 (p : unserialized_params) 312 312 (p' : ∀F.sem_unserialized_params p F) (graph_prog : ?) 313 (sigma : (Σi.is_internal_function_of_program (joint_closed_internal_function (mk_graph_params p)) 314 graph_prog i) → 315 label → option ℕ) : Type[0] ≝ 313 (sigma : sigma_map p graph_prog) : Type[0] ≝ 316 314 { well_formed_frames : framesT (make_sem_graph_params p p') → Prop 317 315 ; sigma_frames : ∀frms.well_formed_frames frms → framesT (make_sem_lin_params p p') … … 340 338 definition well_formed_state : 341 339 ∀p,p'.∀graph_prog : joint_program (mk_graph_params p). 342 ∀sigma : ((Σi.is_internal_function_of_program … graph_prog i) → 343 code_point (mk_graph_params p) → option ℕ). 340 ∀sigma. 344 341 good_sem_state_sigma p p' graph_prog sigma → 345 342 state (make_sem_graph_params p p') → Prop ≝ … … 352 349 definition sigma_state : 353 350 ∀p,p'.∀graph_prog : joint_program (mk_graph_params p). 354 ∀sigma : ((Σi.is_internal_function_of_program … graph_prog i) → 355 code_point (mk_graph_params p) → option ℕ). 351 ∀sigma. 356 352 ∀gsss : good_sem_state_sigma p p' graph_prog sigma. 357 353 ∀st : state (make_sem_graph_params p p'). … … 409 405 definition sigma_pc : 410 406 ∀p,p',graph_prog. 411 ∀sigma : ((Σi.is_internal_function_of_program … graph_prog i) → 412 label → option ℕ). 407 ∀sigma. 413 408 ∀pc. 414 409 ∀prf : well_formed_pc p p' graph_prog sigma pc. … … 447 442 let st' ≝ sigma_state … (proj2 … prf) in 448 443 mk_state_pc ? st' pc'. 449 444 (* 450 445 definition sigma_function_name : 451 446 ∀p,graph_prog. … … 454 449 (Σf.is_internal_function_of_program … lin_prog f) ≝ 455 450 λp,graph_prog,f.«f, if_propagate … (pi2 … f)». 456 451 *) 457 452 lemma m_list_map_All_ok : 458 453 ∀M : MonadProps.∀X,Y,f,l. … … 520 515 (p : unserialized_params) 521 516 (p' : ∀F.sem_unserialized_params p F) (graph_prog : ?) 522 (sigma : (Σi.is_internal_function_of_program (joint_closed_internal_function (mk_graph_params p)) 523 graph_prog i) → 524 label → option ℕ) 517 (sigma : sigma_map p graph_prog) 525 518 : Type[0] ≝ 526 519 { gsss :> good_sem_state_sigma p p' graph_prog sigma … … 557 550 ; eval_ext_seq_commute : 558 551 let lin_prog ≝ linearise p graph_prog in 559 ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ. 560 let stack_sizes' ≝ 561 stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p') 562 ? graph_prog stack_sizes in 563 ∀ext,fn,st1,st2,prf1. 564 eval_ext_seq ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes')) 565 ext fn st1 = return st2 → 552 ∀stack_sizes. 553 ∀ext,i,fn,st1,st2,prf1. 554 eval_ext_seq ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes)) 555 ext i fn st1 = return st2 → 566 556 ∃prf2. 567 557 eval_ext_seq ?? (p' ?) … (ev_genv (lin_prog_params … lin_prog stack_sizes)) 568 ext (sigma_function_name … fn) (sigma_state p p' graph_prog sigma gsss st1 prf1) =558 ext i (\fst (linearise_int_fun … fn)) (sigma_state p p' graph_prog sigma gsss st1 prf1) = 569 559 return sigma_state p p' graph_prog sigma gsss st2 prf2 570 560 ; setup_call_commute : … … 586 576 ; read_result_commute : 587 577 let lin_prog ≝ linearise p graph_prog in 588 ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ. 589 let stack_sizes' ≝ 590 stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p') 591 ? graph_prog stack_sizes in 578 ∀stack_sizes. 592 579 ∀call_dest , st1 , prf1, l1. 593 read_result ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes '))580 read_result ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes)) 594 581 call_dest st1 = return l1 → 595 582 ∃ prf : m_list_map … (sigma_beval_opt p p' graph_prog sigma) l1 ≠ None ?. … … 598 585 ; pop_frame_commute : 599 586 let lin_prog ≝ linearise p graph_prog in 600 ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ. 601 let stack_sizes' ≝ 602 stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p') 603 ? graph_prog stack_sizes in 604 ∀ st1 , prf1, curr_id ,st2. 605 pop_frame ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes')) 606 curr_id st1 = return st2 → 587 ∀stack_sizes. 588 ∀ st1 , prf1, curr_id , curr_fn ,st2. 589 pop_frame ?? (p' ?) … (ev_genv (graph_prog_params … graph_prog stack_sizes)) 590 curr_id curr_fn st1 = return st2 → 607 591 ∃prf2. 608 592 let pc' ≝ sigma_pc p p' graph_prog sigma (pc ? st2) (proj1 … prf2) in 609 593 let st2' ≝ sigma_state p p' graph_prog sigma gsss (st_no_pc ? st2) (proj2 … prf2) in 610 594 pop_frame ?? (p' ?) … (ev_genv (lin_prog_params … lin_prog stack_sizes)) 611 (sigma_function_name p graph_prog curr_id) (sigma_state p p' graph_prog sigma gsss st1 prf1) =595 curr_id (\fst (linearise_int_fun … curr_fn)) (sigma_state p p' graph_prog sigma gsss st1 prf1) = 612 596 return mk_state_pc ? st2' pc' 613 597 }. … … 672 656 λgss : good_state_sigma p p' graph_prog sigma. 673 657 store_commute … gss (acca_store__commute … gss). 674 675 676 lemma acca_store_commute : 677 ∀p,p',graph_prog,sigma. 678 ∀gss : good_state_sigma p p' graph_prog sigma. 679 ∀a,bv,st,st',prf1,prf1'. 680 acca_store ?? (p' ?) a bv st = return st' → 681 ∃prf2. 682 acca_store ?? (p' ?) a 683 (sigma_beval p p' graph_prog sigma bv prf1') 684 (sigma_state … gss st prf1) = return sigma_state … gss st' prf2 ≝ 685 λp,p',graph_prog,sigma,gss,a,bv.?. 686 * #frms #is #carry #regs #m 687 * #frms' #is' #carry' #regs' #m' 688 *** #frms_ok #is_ok #regs_ok #mem_ok 689 #bv_ok #EQ1 elim (bind_inversion ????? EQ1) 690 #regs'' * -EQ1 #EQ1 whd in ⊢ (??%%→?); #EQ destruct(EQ) 691 elim (acca_store__commute … gss … EQ1) 692 [ #prf2 #EQ2 693 % [ whd /4 by conj/ ] 694 change with (! r ← ? ; ? = ?) >EQ2 695 whd in match (sigma_state ???????); normalize nodelta 696 >m_return_bind 697 698 699 st,st',prf1,prf2,prf3.?. 700 701 702 #p #p' # 658 703 659 *) 704 660 … … 729 685 #A * #x #v normalize #EQ destruct % qed. 730 686 687 (* 731 688 lemma if_of_function_commute: 732 689 ∀p. … … 739 696 #p #graph_prog #graph_fun whd 740 697 @prog_if_of_function_transform % qed. 741 742 lemma bind_opt _inversion:743 ∀A,B: Type[0]. 744 ( ! x ← f ; g x = Some … y) →745 ∃x. (f = Some … x) ∧ (g x = Some … y).746 #A #B # f #g #y cases f normalize747 [ #H destruct (H) 748 | #a #e %{a} /2 by conj/ 749 ] qed.698 *) 699 lemma bind_option_inversion_star: 700 ∀A,B: Type[0].∀P : Prop.∀f: option A. ∀g: A → option B. ∀y: B. 701 (∀x.f = Some … x → g x = Some … y → P) → 702 (! x ← f ; g x = Some … y) → P. 703 #A #B #P #f #g #y #H #G elim (option_bind_inverse ????? G) #x * @H qed. 704 705 interpretation "option bind inversion" 'bind_inversion = 706 (bind_option_inversion_star ???????). 750 707 751 708 lemma sigma_pblock_eq_lemma : … … 758 715 #p #p' #graph_prog #sigma #pc #prf 759 716 whd in match sigma_pc; normalize nodelta 760 @opt_safe_elim #x #x_spec 761 whd in x_spec:(??%?); cases (int_funct_of_block ???) in x_spec; 762 normalize nodelta [#abs destruct] #id #H cases (bind_opt_inversion ????? H) -H 763 #offset * #_ whd in ⊢ (??%? → ?); #EQ destruct // 717 @opt_safe_elim #x @'bind_inversion * #i #fn #_ 718 @'bind_inversion #n #_ whd in ⊢ (??%?→?); 719 #EQ destruct % 764 720 qed. 765 721 … … 780 736 *) 781 737 738 (* 782 739 lemma funct_of_block_transf : 783 740 ∀A,B.∀progr : program (λvars .fundef (A vars)) ℕ. … … 887 844 #A #B #progr #transf #bl #f #prf 888 845 whd whd in match int_funct_of_block in ⊢ (??%?→?); normalize nodelta 889 #H 890 elim (bind_opt_inversion ??? ?? H) -H #x 891 * #x_spec 846 @'bind_inversion #x #x_spec 892 847 @match_int_fun [2: #fd #_ #ABS destruct(ABS) ] 893 848 #fd #EQdescr change with (Some ?? = ? → ?) #EQ destruct(EQ) … … 899 854 >(description_of_function_transf) [2: @x_prf ] 900 855 >EQdescr whd in ⊢ (??%%→?); #ABS destruct qed. 901 902 903 lemma fetch_function_sigma_commute : 904 ∀p,p',graph_prog. 905 let lin_prog ≝ linearise p graph_prog in 906 ∀sigma,pc_st,f. 907 ∀prf : well_formed_pc p p' graph_prog sigma pc_st. 908 fetch_function … (globalenv_noinit … graph_prog) pc_st = 909 return f 910 → fetch_function … (globalenv_noinit … lin_prog) (sigma_pc … pc_st prf) = 911 return sigma_function_name … f. 912 #p #p' #graph_prog #sigma #st #f #prf 856 *) 857 858 axiom symbol_for_block_transf : 859 ∀A,B,V,init.∀prog_in : program A V. 860 ∀trans : ∀vars.A vars → B vars. 861 let prog_out ≝ transform_program … prog_in trans in 862 ∀bl, i. 863 symbol_for_block … (globalenv … init prog_in) bl = Some ? i → 864 symbol_for_block … (globalenv … init prog_out) bl = Some ? i. 865 866 lemma fetch_function_transf : 867 ∀A,B,V,init.∀prog_in : program A V. 868 ∀trans : ∀vars.A vars → B vars. 869 let prog_out ≝ transform_program … prog_in trans in 870 ∀bl,i,f. 871 fetch_function … (globalenv … init prog_in) bl = 872 return 〈i, f〉 873 → fetch_function … (globalenv … init prog_out) bl = 874 return 〈i, trans … f〉. 875 #A #B #V #init #prog_in #trans #bl #i #f 913 876 whd in match fetch_function; normalize nodelta 914 >(sigma_pblock_eq_lemma … prf) #H 915 lapply (opt_eq_from_res ???? H) -H #H 916 >(int_funct_of_block_transf ?? graph_prog (λvars,graph_fun.\fst (linearise_int_fun … graph_fun)) ??? H) 917 // 877 #H lapply (opt_eq_from_res ???? H) -H 878 @'bind_inversion #id #eq_symbol_for_block 879 @'bind_inversion #fd #eq_find_funct 880 whd in ⊢ (??%?→?); #EQ destruct(EQ) 881 >(symbol_for_block_transf A B … eq_symbol_for_block) >m_return_bind 882 >(find_funct_ptr_transf A B … eq_find_funct) >m_return_bind % 883 qed. 884 885 lemma bind_inversion_star : ∀X,Y.∀P : Prop. 886 ∀m : res X.∀f : X → res Y.∀v : Y. 887 (∀x. m = return x → f x = return v → P) → 888 ! x ← m ; f x = return v → P. 889 #X #Y #P #m #f #v #H #G 890 elim (bind_inversion ????? G) #x * @H qed. 891 892 interpretation "res bind inversion" 'bind_inversion = 893 (bind_inversion_star ???????). 894 895 lemma fetch_internal_function_transf : 896 ∀A,B.∀prog_in : program (λvars.fundef (A vars)) ℕ. 897 ∀trans : ∀vars.A vars → B vars. 898 let prog_out ≝ transform_program … prog_in (λvars.transf_fundef … (trans vars)) in 899 ∀bl,i,f. 900 fetch_internal_function … (globalenv_noinit … prog_in) bl = 901 return 〈i, f〉 902 → fetch_internal_function … (globalenv_noinit … prog_out) bl = 903 return 〈i, trans … f〉. 904 #A #B #prog #trans #bl #i #f 905 whd in match fetch_internal_function; normalize nodelta 906 @'bind_inversion * #id * #fd normalize nodelta #EQfetch 907 whd in ⊢ (??%%→?); #EQ destruct(EQ) 908 >(fetch_function_transf … EQfetch) % 918 909 qed. 919 910 … … 978 969 qed. *) 979 970 980 lemma opt_Exists_elim:981 ∀A:Type[0].∀P:A → Prop.982 ∀o:option A.983 opt_Exists A P o →984 ∃v:A. o = Some … v ∧ P v.985 #A #P * normalize /3/ *986 qed.987 988 989 971 lemma stmt_at_sigma_commute: 990 ∀p,graph_prog,graph_fun,lbl,pt. 991 let lin_prog ≝ linearise ? graph_prog in 992 let lin_fun ≝ sigma_function_name p graph_prog graph_fun in 993 ∀sigma.good_sigma p graph_prog sigma → 994 sigma graph_fun lbl = return pt → 972 ∀p,globals,graph_code,entry,lin_code,lbl,pt,sigma. 973 good_local_sigma p globals graph_code entry lin_code sigma → 974 sigma lbl = return pt → 995 975 ∀stmt. 996 stmt_at … 997 (joint_if_code ?? (if_of_function ?? graph_fun)) 976 stmt_at … graph_code 998 977 lbl = return stmt → 999 stmt_at ?? 1000 (joint_if_code ?? (if_of_function ?? lin_fun)) 1001 pt = return (graph_to_lin_statement … stmt). 1002 #p #graph_prog #graph_fun #lbl #pt #sigma #good #prf #stmt 1003 cases (good graph_fun (pi2 … (sigma_function_name p graph_prog graph_fun))) 1004 #sigma_entry_is_zero #lin_stmt_spec 1005 lapply (lin_stmt_spec lbl pt prf) -lin_stmt_spec * #stmt1 * 1006 #EQlookup_stmt1 #H 1007 elim (opt_Exists_elim … H) -H * #optlbl_graph_stmt #graph_stmt 1008 * #EQnth_opt_graph_stmt normalize nodelta 1009 * #optEQlbl_optlbl_graph_stmt #next_spec 1010 whd in match (stmt_at ????) in ⊢ (% → ?); 1011 normalize nodelta 1012 >EQlookup_stmt1 whd in ⊢ ((???%) → ?); #EQ destruct(EQ) 1013 whd in match (stmt_at ????); > EQnth_opt_graph_stmt 1014 normalize nodelta elim optEQlbl_optlbl_graph_stmt #_ #EQ >EQ // 1015 qed. 978 stmt_at ?? lin_code 979 pt = return graph_to_lin_statement … stmt ∧ 980 All … (λl.sigma l ≠ None ?) (stmt_labels … stmt) ∧ 981 match stmt with 982 [ final stmt ⇒ True 983 | sequential stmt nxt ⇒ 984 (sigma nxt = Some ? (S pt) ∨ 985 (stmt_at ?? lin_code 986 (S pt) = return final (mk_lin_params p) … (GOTO … nxt))) 987 ]. 988 #p #globals #graph_code #entry #lin_code #lbl #pt #sigma 989 * #_ #lin_stmt_spec #prf 990 elim (lin_stmt_spec … prf) -lin_stmt_spec #stmt1 *** #EQstmt_at 991 #All_succs_in #next_spec 992 #EQstmt_at_graph_stmt 993 #stmt >EQstmt_at 994 whd in ⊢ (??%%→?); #EQ destruct(EQ) 995 % [ % assumption ] 996 cases stmt in next_spec; -stmt normalize nodelta [2: // ] 997 #stmt #nxt 998 whd in match opt_All; 999 whd in match stmt_implicit_label; 1000 normalize nodelta // 1001 qed. 1002 1016 1003 (* 1017 1004 … … 1036 1023 <sigma_pc_commute >lin_lookup_ok // *) 1037 1024 1038 lemma fetch_statement_sigma_commute: 1039 ∀p,p',graph_prog,pc,fn,stmt. 1025 definition good_sigma : 1026 ∀p.∀graph_prog : joint_program (mk_graph_params p). 1027 (joint_closed_internal_function ? (prog_var_names … graph_prog) → 1028 label → option ℕ) → Prop ≝ 1029 λp,graph_prog,sigma. 1030 ∀fn : joint_closed_internal_function (mk_graph_params p) ?. 1031 good_local_sigma ?? (joint_if_code … fn) (joint_if_entry … fn) 1032 (joint_if_code … (\fst (linearise_int_fun … fn))) (sigma fn). 1033 1034 lemma pc_of_label_sigma_commute : 1035 ∀p,p',graph_prog,pc,lbl,i,fn. 1040 1036 let lin_prog ≝ linearise ? graph_prog in 1041 1037 ∀sigma.good_sigma p graph_prog sigma → 1042 1038 ∀prf : well_formed_pc p p' graph_prog sigma pc. 1043 fetch_statement ? (make_sem_graph_params p p') … 1044 (globalenv_noinit … graph_prog) pc = return 〈fn,stmt〉 → 1045 fetch_statement ? (make_sem_lin_params p p') … 1039 fetch_internal_function … 1040 (globalenv_noinit … graph_prog) (pc_block pc) = return 〈i, fn〉 → 1041 let pc' ≝ pc_of_point (make_sem_graph_params p p') … (pc_block pc) lbl in 1042 code_has_label … (joint_if_code … (\fst (linearise_int_fun … fn))) lbl → 1043 ∃prf'.pc_of_label (make_sem_lin_params p p') … (globalenv_noinit … lin_prog) 1044 (pc_block (sigma_pc … pc prf)) lbl = 1045 return sigma_pc p p' graph_prog sigma pc' prf'. 1046 #p #p' #graph_prog #pc #lbl #i #fn 1047 #sigma #good cases (good fn) -good * #_ #all_labels_in 1048 #good #prf #fetchfn >lin_code_has_label #lbl_in 1049 whd in match pc_of_label; normalize nodelta 1050 >sigma_pblock_eq_lemma 1051 > (fetch_internal_function_transf … fetchfn) >m_return_bind 1052 inversion (point_of_label ????) 1053 [ (* 1054 change with (If ? then with prf do ? else ? = ? → ?) 1055 @If_elim [ #prf' whd in ⊢ (??%?→?); #ABS destruct(ABS) | #ABS >ABS in lbl_in; * ] 1056 *) whd in ⊢ (??%?→?); >lbl_in whd in ⊢ (??%?→?); #ABS destruct(ABS) 1057 | #pt #H lapply (all_labels_in … H) #EQsigma >m_return_bind 1058 % 1059 [ @hide_prf whd % 1060 | whd in match sigma_pc; normalize nodelta 1061 @opt_safe_elim #pc' 1062 ] 1063 whd in match sigma_pc_opt; normalize nodelta >fetchfn >m_return_bind 1064 >point_of_pc_of_point 1065 >EQsigma whd in ⊢ (??%?→?); #EQ destruct(EQ) % 1066 ] 1067 qed. 1068 1069 lemma graph_pc_of_label : 1070 ∀p,p'.let pars ≝ make_sem_graph_params p p' in 1071 ∀globals,ge,bl,i_fn,lbl. 1072 fetch_internal_function ? ge bl = return i_fn → 1073 pc_of_label pars globals ge bl lbl = 1074 OK ? (pc_of_point pars bl lbl). 1075 #p #p' #globals #ge #bl #fn #lbl #fetchfn 1076 whd in match pc_of_label; normalize nodelta 1077 >fetchfn % 1078 qed. 1079 1080 lemma graph_succ_pc : 1081 ∀p,p'.let pars ≝ make_sem_graph_params p p' in 1082 ∀pc,lbl. 1083 succ_pc pars pc lbl = pc_of_point pars (pc_block pc) lbl. 1084 normalize // 1085 qed. 1086 1087 lemma fetch_statement_sigma_commute: 1088 ∀p,p',graph_prog,pc,f,fn,stmt. 1089 let lin_prog ≝ linearise ? graph_prog in 1090 ∀sigma.good_sigma p graph_prog sigma → 1091 ∀prf : well_formed_pc p p' graph_prog sigma pc. 1092 fetch_statement (make_sem_graph_params p p') … 1093 (globalenv_noinit ? graph_prog) pc = return 〈f, fn,stmt〉 → 1094 fetch_statement (make_sem_lin_params p p') … 1046 1095 (globalenv_noinit … lin_prog) (sigma_pc … pc prf) = 1047 return 〈sigma_function_name … fn, graph_to_lin_statement … stmt〉. 1048 #p #p' #graph_prog #pc #fn #stmt #sigma #good #wfprf 1049 whd in match fetch_statement; normalize nodelta #H 1050 cases (bind_inversion ????? H) #id * -H #fetchfn 1051 >(fetch_function_sigma_commute … wfprf … fetchfn) >m_return_bind 1052 #H cases (bind_inversion ????? H) #fstmt * -H #H 1053 lapply (opt_eq_from_res ???? H) -H #H #EQ whd in EQ:(??%%); destruct 1054 >(stmt_at_sigma_commute … good … H) [%] 1055 whd in match sigma_pc; normalize nodelta 1056 @opt_safe_elim #pc' #H 1057 cases (bind_opt_inversion ????? H) 1058 #i * #EQ1 -H #H 1059 cases (bind_opt_inversion ????? H) 1060 #pnt * #EQ2 whd in ⊢ (??%?→?); #EQ3 destruct 1061 whd in match point_of_pc in ⊢ (???%); normalize nodelta >point_of_offset_of_point 1062 lapply (opt_eq_from_res ???? fetchfn) >EQ1 #EQ4 destruct @EQ2 1063 qed. 1096 return 〈f, \fst (linearise_int_fun … fn), graph_to_lin_statement … stmt〉 ∧ 1097 All ? (λlbl.well_formed_pc p p' graph_prog sigma 1098 (pc_of_point (make_sem_graph_params p p') (pc_block pc) lbl)) 1099 (stmt_explicit_labels … stmt) ∧ 1100 match stmt with 1101 [ sequential stmt nxt ⇒ 1102 ∃prf'. 1103 let nxt_pc ≝ succ_pc (make_sem_lin_params p p') (sigma_pc … pc prf) it in 1104 let sigma_nxt ≝ sigma_pc p p' graph_prog sigma (succ_pc (make_sem_graph_params p p') pc nxt) prf' in 1105 (nxt_pc = sigma_nxt ∨ 1106 fetch_statement (make_sem_lin_params p p') … 1107 (globalenv_noinit … lin_prog) nxt_pc = 1108 return 〈f, \fst (linearise_int_fun … fn), final (mk_lin_params p) … (GOTO … nxt)〉) 1109 | final stmt ⇒ True 1110 ]. 1111 #p #p' #graph_prog #pc #f #fn #stmt #sigma #good 1112 elim (good fn) * #_ #all_labels_in #good_local #wfprf 1113 #H 1114 elim (fetch_statement_inv … H) 1115 #fetchfn #graph_stmt 1116 whd in match fetch_statement; normalize nodelta 1117 >sigma_pblock_eq_lemma 1118 >(fetch_internal_function_transf … fetchfn) >m_return_bind 1119 whd in match sigma_pc; normalize nodelta @opt_safe_elim 1120 #lin_pc whd in match sigma_pc_opt in ⊢ (%→?); normalize nodelta 1121 >fetchfn in ⊢ (%→?); >m_return_bind 1122 inversion (sigma ??) 1123 [ #_ normalize in ⊢ (%→?); #ABS destruct(ABS) ] 1124 #lin_pt #EQsigma whd in ⊢ (??%%→?); #EQ destruct(EQ) 1125 cases (stmt_at_sigma_commute … (good fn) … EQsigma … graph_stmt) * 1126 #H1 #H2 #H3 % [ % ] 1127 [ whd in match point_of_pc; normalize nodelta >point_of_offset_of_point 1128 >H1 % 1129 | @(All_mp … (All_append_r … H2)) #lbl #prf' 1130 whd whd in match sigma_pc_opt; normalize nodelta 1131 >fetchfn >m_return_bind >point_of_pc_of_point 1132 >(opt_to_opt_safe … prf') % normalize 1133 #ABS destruct(ABS) 1134 | cases stmt in H2 H3; normalize nodelta [2: // ] 1135 -stmt #stmt #nxt * #next_in #_ #nxt_spec 1136 % 1137 [ @hide_prf whd % 1138 | @opt_safe_elim #pc' 1139 ] 1140 >graph_succ_pc whd in ⊢ (??%?→?); 1141 >fetchfn normalize nodelta >point_of_pc_of_point 1142 >(opt_to_opt_safe … next_in) whd in ⊢ (??%?→?); #EQ destruct(EQ) 1143 cases nxt_spec 1144 [ #EQsigma_nxt %1 1145 whd in match (succ_pc ???); whd in match point_of_pc; normalize nodelta 1146 >point_of_offset_of_point lapply next_in >EQsigma_nxt #N % 1147 | #EQstmt_at_nxt %2 1148 whd in match (succ_pc ???); 1149 >(fetch_internal_function_transf … fetchfn) >m_return_bind 1150 whd in match point_of_pc; 1151 normalize nodelta >point_of_offset_of_point >point_of_offset_of_point 1152 whd in match (point_of_succ ???); 1153 >EQstmt_at_nxt % 1154 ] 1155 ] 1156 qed. 1064 1157 1065 1158 lemma point_of_pc_sigma_commute : 1066 1159 ∀p,p',graph_prog. 1067 1160 let lin_prog ≝ linearise p graph_prog in 1068 ∀sigma,pc,f n,n.1161 ∀sigma,pc,f,fn,n. 1069 1162 ∀prf : well_formed_pc p p' graph_prog sigma pc. 1070 int_funct_of_block … (globalenv_noinit … graph_prog) (pc_block pc) = return fn→1071 sigma fn (point_of_pc ?(make_sem_graph_params p p') pc) = return n →1072 point_of_pc ?(make_sem_lin_params p p') (sigma_pc … pc prf) = n.1073 #p #p' #graph_prog #sigma #pc #f n #n #prf #EQfetch #EQsigma1163 fetch_internal_function … (globalenv_noinit … graph_prog) (pc_block pc) = return 〈f, fn〉 → 1164 sigma fn (point_of_pc (make_sem_graph_params p p') pc) = return n → 1165 point_of_pc (make_sem_lin_params p p') (sigma_pc … pc prf) = n. 1166 #p #p' #graph_prog #sigma #pc #f #fn #n #prf #EQfetch #EQsigma 1074 1167 whd in match sigma_pc; normalize nodelta 1075 1168 @opt_safe_elim #pc' whd in match sigma_pc_opt; 1076 1169 normalize nodelta >EQfetch >m_return_bind >EQsigma 1077 >m_return_bindwhd in ⊢ (??%?→?); #EQ destruct(EQ)1078 change with (point_of_offset ??? = ?)@point_of_offset_of_point1170 whd in ⊢ (??%?→?); #EQ destruct(EQ) 1171 @point_of_offset_of_point 1079 1172 qed. 1080 1173 … … 1082 1175 ∀p,p',graph_prog. 1083 1176 let lin_prog ≝ linearise p graph_prog in 1084 ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ. 1085 let stack_sizes' ≝ 1086 stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p') 1087 ? graph_prog stack_sizes in 1177 ∀stack_sizes. 1088 1178 ∀sigma,gss. 1089 1179 good_sigma p graph_prog sigma → 1090 1180 status_rel 1091 (graph_abstract_status p p' graph_prog stack_sizes ')1181 (graph_abstract_status p p' graph_prog stack_sizes) 1092 1182 (lin_abstract_status p p' lin_prog stack_sizes) 1093 1183 ≝ λp,p',graph_prog,stack_sizes,sigma,gss,good. … … 1114 1204 1115 1205 lemma IO_bind_inversion: 1116 ∀O,I,A,B. 1117 ( ! x ← f ; g x = return y) →1118 ∃x. (f = return x) ∧ (g x = return y).1119 #O #I #A #B # f #g #y cases f normalize1120 [ #o #f # H destruct1121 | #a # e %{a} /2 by conj/1122 | # m #H destruct (H)1206 ∀O,I,A,B.∀P : Prop.∀f: IO O I A. ∀g: A → IO O I B. ∀y: B. 1207 (∀x.f = return x → g x = return y → P) → 1208 (! x ← f ; g x = return y) → P. 1209 #O #I #A #B #P #f #g #y cases f normalize 1210 [ #o #f #_ #H destruct 1211 | #a #G #H @(G ? (refl …) H) 1212 | #e #_ #H destruct 1123 1213 ] qed. 1214 1215 interpretation "IO bind inversion" 'bind_inversion = 1216 (IO_bind_inversion ?????????). 1124 1217 1125 1218 lemma err_eq_from_io : ∀O,I,X,m,v. … … 1144 1237 cut(x = sigmais) [>H1 in H; #EQ whd in EQ : (???%); destruct(EQ) %] 1145 1238 #EQ >EQ // 1239 qed. 1240 1241 (* this should make things easier for ops using memory (where pc cant happen) *) 1242 definition bv_no_pc : beval → Prop ≝ 1243 λbv.match bv with [ BVpc _ _ ⇒ False | _ ⇒ True ]. 1244 1245 lemma bv_pc_other : 1246 ∀P : beval → Prop. 1247 (∀pc,p.P (BVpc pc p)) → 1248 (∀bv.bv_no_pc bv → P bv) → 1249 ∀bv.P bv. 1250 #P #H1 #H2 * /2/ qed. 1251 1252 lemma sigma_bv_no_pc : ∀p,p',graph_prog,sigma,bv,prf. 1253 bv_no_pc bv → 1254 sigma_beval p p' graph_prog sigma bv prf = bv. 1255 #p #p' #graph_prog #sigma * 1256 [|| #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc #p ] 1257 #prf * whd in match sigma_beval; normalize nodelta 1258 @opt_safe_elim #bv' normalize #EQ destruct(EQ) % 1146 1259 qed. 1147 1260 … … 1254 1367 ∀p,p',graph_prog. 1255 1368 let lin_prog ≝ linearise p graph_prog in 1256 ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ. 1257 let stack_sizes' ≝ 1258 stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p') 1259 ? graph_prog stack_sizes in 1260 ∀sigma.∀gss : good_state_sigma … graph_prog sigma. 1261 ∀fn,st,stmt,st'. 1369 ∀stack_sizes. 1370 ∀sigma.∀gss : good_state_sigma p p' graph_prog sigma. 1371 ∀f,fn,st,stmt,st'. 1262 1372 ∀prf : well_formed_state … gss st. 1263 eval_seq_no_pc ?? (ev_genv … (graph_prog_params … graph_prog stack_sizes'))1264 f n st stmt = return st' →1373 eval_seq_no_pc … (ev_genv … (graph_prog_params … graph_prog stack_sizes)) 1374 f fn stmt st = return st' → 1265 1375 ∃prf'. 1266 eval_seq_no_pc ??(ev_genv … (lin_prog_params … lin_prog stack_sizes))1267 (sigma_function_name … fn) (sigma_state … gss st prf) stmt=1376 eval_seq_no_pc … (ev_genv … (lin_prog_params … lin_prog stack_sizes)) 1377 f (\fst (linearise_int_fun … fn)) stmt (sigma_state … gss st prf) = 1268 1378 return sigma_state … gss st' prf'. 1269 1379 #p #p' #graph_prog #stack_sizes #sigma #gss … … 1393 1503 inversion(sigma_beval_opt ???? y) 1394 1504 [ #ABS @⊥ lapply(proj2 … (proj1 … (proj1 … prf))) 1505 xxxxxxxxxxxxxxxxxx 1506 1507 qed. 1508 1509 lemma eval_statement_no_pc_sigma_commute : 1510 ∀p,p',graph_prog. 1511 let lin_prog ≝ linearise p graph_prog in 1512 ∀stack_sizes. 1513 ∀sigma.∀gss : good_state_sigma p p' graph_prog sigma. 1514 ∀f,fn,st,stmt,st'. 1515 ∀prf : well_formed_state … gss st. 1516 eval_statement_no_pc … (ev_genv … (graph_prog_params … graph_prog stack_sizes)) 1517 f fn stmt st = return st' → 1518 ∃prf'. 1519 eval_statement_no_pc … (ev_genv … (lin_prog_params … lin_prog stack_sizes)) 1520 f (\fst (linearise_int_fun … fn)) (graph_to_lin_statement … stmt) 1521 (sigma_state … gss st prf) = 1522 return sigma_state … gss st' prf'. 1523 #p #p' #graph_prog #stack_sizes #sigma #gss 1524 #f #fn #st * [* [ #stmt | #a #lbl ] #nxt | * [ #lbl | | #fl #called #args ]] 1525 #st' #prf 1526 whd in match eval_statement_no_pc; normalize nodelta 1527 [ @eval_seq_no_pc_sigma_commute 1528 |2,3,4: whd in ⊢ (??%%→?); #EQ destruct(EQ) %{prf} % 1529 | (* tailcall, follow proof of CALL in previous lemma *) 1530 cases daemon 1531 ] 1532 qed. 1533 1534 ======= 1395 1535 whd in match sigma_is_opt; >H normalize nodelta >ABS 1396 1536 whd in ⊢ ((?(??%?))→?); * #h1 @h1 % … … 1581 1721 | (*C_OP1*) 1582 1722 1723 >>>>>>> .r2528 1583 1724 inductive ex_Type1 (A:Type[1]) (P:A → Prop) : Prop ≝ 1584 1725 ex1_intro: ∀ x:A. P x → ex_Type1 A P. … … 1588 1729 ∀p,p',graph_prog. 1589 1730 let lin_prog ≝ linearise ? graph_prog in 1590 ∀lin_stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ. 1591 let graph_stack_sizes ≝ 1592 stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p') 1593 ? graph_prog lin_stack_sizes in 1594 (∀sigma.good_sigma_state p p' graph_prog sigma) → 1731 ∀stack_sizes. 1732 (∀sigma.good_state_sigma p p' graph_prog sigma) → 1595 1733 ex_Type1 … (λR. 1596 1734 status_simulation 1597 (graph_abstract_status p p' graph_prog graph_stack_sizes)1598 (lin_abstract_status p p' lin_prog lin_stack_sizes) R).1735 (graph_abstract_status p p' graph_prog stack_sizes) 1736 (lin_abstract_status p p' lin_prog stack_sizes) R). 1599 1737 #p #p' #graph_prog 1600 cases (linearise_spec … graph_prog) #sigma #good 1601 #lin_stack_sizes 1738 letin sigma ≝ (λfn.\snd (linearise_int_fun … fn) : sigma_map … graph_prog) 1739 cut (∀fn.good_local_sigma … (sigma fn)) 1740 [6: #fn @(pi2 … (linearise_int_fun … fn)) |*:] 1741 #good 1742 #stack_sizes 1602 1743 #gss lapply (gss sigma) -gss #gss 1603 %{(linearise_status_rel p p' graph_prog lin_stack_sizes sigma gss good)}1744 %{(linearise_status_rel p p' graph_prog stack_sizes sigma gss good)} 1604 1745 whd in match graph_abstract_status; 1605 1746 whd in match lin_abstract_status; … … 1616 1757 (eval_state (make_sem_graph_params p p') (prog_var_names ???) ?? = ? → ?) 1617 1758 whd in match eval_state in ⊢ (%→?); normalize nodelta 1618 change with (Σi.is_internal_function_of_program ? graph_prog i) in 1619 match (Sig ??) in ⊢ (%→?); 1620 letin globals ≝ (prog_var_names ?? graph_prog) 1621 change with (fetch_statement ??? (globalenv_noinit ? graph_prog) ?) in 1622 match (fetch_statement ?????) in ⊢ (%→?); 1623 #ex 1624 cases (IO_bind_inversion ??????? ex) in ⊢ ?; * #fn #stmt * -ex 1625 #EQfetch lapply (err_eq_from_io ????? EQfetch) -EQfetch 1626 #EQfetch 1627 cases (bind_inversion ????? EQfetch) 1628 #f_id * #H lapply (opt_eq_from_res ???? H) -H 1629 #EQfunc_of_block 1630 #H elim (bind_inversion ????? H) -H #stmt' * 1631 #H lapply (opt_eq_from_res ???? H) -H #EQstmt_at 1632 whd in ⊢ (??%%→?); #EQ destruct(EQ) 1633 #EQeval 1634 cases (good fn (pi2 … (sigma_function_name p graph_prog fn))) 1635 letin graph_fun ≝ (if_of_function … fn) in EQstmt_at; #EQstmt_at 1636 #entry_0 1637 #good_local 1638 * * #wf_pc #wf_state #EQst2 1759 @'bind_inversion 1760 ** #curr_f #curr_fn #stmt #H lapply (err_eq_from_io ????? H) -H #EQfetch_stmt 1761 cases (fetch_statement_inv … EQfetch_stmt) #EQfetchfn #_ 1762 @'bind_inversion 1763 #st1_no_pc' #ex lapply (err_eq_from_io ????? ex) -ex #ex #ex_advance 1764 * #wf_prf #st2_EQ 1765 1766 cases (fetch_statement_sigma_commute … good … (hide_prf … (proj1 … wf_prf)) EQfetch_stmt) 1767 * #EQfetch_stmt' #all_labels_in 1768 1769 letin lin_prog ≝ (linearise … graph_prog) 1770 lapply (refl … (eval_state … (ev_genv (mk_prog_params (make_sem_lin_params p p') lin_prog stack_sizes)) st2)) 1771 whd in match eval_state in ⊢ (???%→?); 1772 >st2_EQ in ⊢ (???%→?); normalize nodelta 1773 >EQfetch_stmt' in ⊢ (%→?); >m_return_bind in ⊢ (???%→?); 1774 cases (eval_statement_no_pc_sigma_commute … gss … (hide_prf … (proj2 … wf_prf)) ex) in ⊢ ?; 1775 #wf_st1_no_pc_prf #ex' >ex' in ⊢ (???%→?); >m_return_bind in ⊢ (???%→?); 1776 1777 whd in match (as_classify ??) in ⊢ (?→?→match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]); 1778 >EQfetch_stmt in ⊢ (?→?→match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]); 1779 normalize nodelta 1780 1781 cases stmt in ex ex_advance; -stmt whd in match graph_to_lin_statement; 1782 normalize nodelta 1783 [ whd in match joint_classify_step; @cond_call_other 1784 [ (* COND *) #a #lbltrue #nxt 1785 #ex whd in match eval_statement_advance in ⊢ (%→%→?); normalize nodelta 1786 #H @('bind_inversion (err_eq_from_io ????? H)) -H @bv_pc_other 1787 [ #bv_pc #p #bv whd in ⊢ (??%%→?); #ABS destruct(ABS) ] 1788 #bv #bv_no_pc #EQretrieve 1789 cases (retrieve_commute … (acca_retrieve_commute … gss) … wf_st1_no_pc_prf … EQretrieve) 1790 #ignore >(sigma_bv_no_pc … bv_no_pc) 1791 change with (acca_retrieve ?? (make_sem_lin_params p p') ?? = ? → ?) 1792 #EQretrieve' >EQretrieve' in ⊢ (?→%→?); >m_return_bind in ⊢ (?→%→?); 1793 #H @('bind_inversion H) -H * normalize nodelta #EQbool_of_bv 1794 >EQbool_of_bv in ⊢ (?→%→?); >m_return_bind in ⊢ (?→%→?); normalize nodelta 1795 [ whd in match goto; normalize nodelta 1796 >(graph_pc_of_label … EQfetchfn) whd in ⊢ (??%%→?); 1797 #EQ destruct(EQ) #ex_advance #ex_advance' 1798 % [2: %{(tal_base_not_return …)} [3: @ex_advance' 1799 | (* CALL *) #f #args #dest #nxt 1800 | (* other *) #stmt #no_call #nxt 1801 ] normalize nodelta 1802 [ #ex 1803 #ex_advance #ex_advance' 1804 | whd in ⊢ (??%%→?); #EQ destruct(EQ) 1805 #H @('bind_inversion H) -H #called_block 1806 #H lapply (err_eq_from_io ????? H) -H #EQcalled_block 1807 #H @('bind_inversion H) -H * #called * #called_fn 1808 #H lapply (err_eq_from_io ????? H) -H #EQcalled 1809 normalize nodelta 1810 [ #H lapply (err_eq_from_io ????? H) -H ] 1811 #H @('bind_inversion H) -H 1812 | @('bind_inversion H) ] -H #st1_no_pc'' #save_frame_EQ ] 1813 #ex_advance #ex_advance' 1814 whd in match joint_classify_seq; normalize nodelta 1815 >EQcalled_block in ⊢ (?→match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]); 1816 1817 cut (∀p,p',graph_prog,sigma,gss,st,f,bl. 1818 ∀prf : well_formed_state p p' graph_prog sigma gss st. 1819 block_of_call (make_sem_graph_params p p') ? 1820 (globalenv_noinit ? graph_prog) st f = return bl → 1821 block_of_call (make_sem_lin_params p p') ? 1822 (globalenv_noinit ? (linearise … graph_prog)) 1823 (sigma_state … st prf) f = return bl) 1824 [1,3: (*TODO lemma *) cases daemon ] #block_of_call_sigma_commute 1825 whd in match eval_seq_advance; normalize nodelta 1826 >(block_of_call_sigma_commute … EQcalled_block) in ⊢ (???%→?); 1827 >m_return_bind in ⊢ (???%→?); 1828 >(fetch_function_transf … EQcalled : 1829 fetch_function … (globalenv_noinit … lin_prog) called_block = ?) in ⊢ (???%→?); 1830 >m_return_bind in ⊢ (???%→?); 1831 whd in match (transf_fundef); normalize nodelta 1832 1833 1834 #block_of_call_sigma_commute 1835 @match_int_fun #called_descr #EQcalled_descr 1836 [ #H @('bind_inversion H) -H #st1_frame_saved #EQ_frame_saved ] 1837 #ex_advance 1838 cut 1839 (∀A,B.∀prog : program (λvars.fundef (A vars)) ℕ. 1840 ∀trans : ∀vars.A vars → B vars. 1841 let prog_out : program (λvars.fundef (B vars)) ℕ ≝ 1842 transform_program ??? prog (λvars.transf_fundef … (trans vars)) in 1843 ∀i.is_function … (globalenv_noinit … prog) i → 1844 is_function … (globalenv_noinit … prog_out) i) [1,3: (* TODO lemma *) cases daemon ] 1845 #f_propagate 1846 letin sigma_function ≝ (λA,B,prog,trans. 1847 λf : Σi.is_function ? (globalenv_noinit ? prog) i. 1848 «pi1 ?? f, f_propagate A B prog trans ? (pi2 ?? f)») in ⊢ ?; (* TODO def *) 1849 cut (∀p,p',graph_prog. 1850 let lin_prog ≝ linearise ? graph_prog in 1851 ∀sigma.∀gss : good_state_sigma … graph_prog sigma. 1852 ∀f,st,fn. 1853 ∀prf : well_formed_state … gss st. 1854 function_of_call (make_sem_graph_params p p') … (globalenv_noinit … graph_prog) 1855 st f = return fn → 1856 function_of_call (make_sem_lin_params p p') … (globalenv_noinit … lin_prog) 1857 (sigma_state … gss st prf) f = return sigma_function … fn) 1858 [1,3: (* TODO lemma *) cases daemon ] 1859 #function_of_call_sigma_commute 1860 whd in match joint_classify_step; whd in match joint_classify_seq; 1861 normalize nodelta #next_spec 1862 >(function_of_call_sigma_commute … EQcalled) in ⊢ (%→?); 1863 >m_return_bind in ⊢ (%→?); 1864 @match_int_fun 1865 [2,3: #EQdescr' lapply EQdescr' 1866 >description_of_function_transf in EQdescr'; 1867 1868 1869 whd in match sigma_beval; normalize nodelta 1870 cases bv 1871 [|| #ptr1 #ptr2 #p | #by | #p | #ptr #p | #bv_pc #p ] 1872 whd in match (sigma_beval_opt ?????) in ⊢ (%→%→?); 1873 [7: #ignore #_ 1874 #ignore whd in match (opt_safe ???) in ⊢ (%→?); #EQretrieve 1875 whd in match (bool_of_beval ?) in ⊢ (% → ?); 1876 3: >no_call_advance [2: @no_call] 1877 1878 1879 1639 1880 generalize in match wf_pc in ⊢ ?; 1640 1881 whd in ⊢ (%→?); … … 1656 1897 * 1657 1898 #EQnth_opt ** #opt_lbl_spec #EQ destruct(EQ) #next_spec 1658 letin lin_prog ≝ (linearise … graph_prog)1659 lapply (refl … (eval_state ? globals (ev_genv (lin_prog_params p p' lin_prog lin_stack_sizes)) st2))1660 1899 destruct(EQst2) 1661 1900 whd in match eval_state in ⊢ (???%→?); normalize nodelta 1662 letin st2 ≝ (sigma_state_pc ????? st1 ?)1663 >(fetch_statement_sigma_commute … good … EQfetch) in ⊢ (%→?);1664 >m_return_bind in ⊢ (%→?);1665 #ex'1666 1901 (* resolve classifier *) 1667 whd in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]);1668 >EQfetch in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]);1669 normalize nodelta1670 cases stmt in EQfetch EQeval EQstmt_at EQnth_opt next_spec ex';1671 1902 [ * 1672 1903 [ #stmt #nxt -
src/joint/semantics.ma
r2491 r2529 16 16 { ge :> genv_t (fundef (F globals)) 17 17 ; find_symbol_in_globals : ∀s.In … globals s → find_symbol … ge s ≠ None ? 18 ; stack_sizes : (Σi.is_internal_function ? ge i) →ℕ18 ; stack_sizes : ident → option ℕ 19 19 }. 20 21 definition stack_sizes_lift :22 ∀pars_in, pars_out : params.23 ∀trans : ∀globals.joint_closed_internal_function pars_in globals →24 joint_closed_internal_function pars_out globals.25 ∀prog_in : program (joint_function pars_in) ℕ.26 let prog_out ≝27 transform_program … prog_in (λglobals.transf_fundef ?? (trans globals)) in28 ((Σi.is_internal_function_of_program … prog_out i) → ℕ) →29 ((Σi.is_internal_function_of_program … prog_in i) → ℕ) ≝30 λpars_in,pars_out,prog_in,trans,stack_sizes.31 λi.stack_sizes «i, if_propagate … (pi2 … i)».32 20 33 21 definition genv ≝ λp.genv_gen (joint_closed_internal_function p). … … 122 110 *) 123 111 124 (* bevals hold a function pointer (BVptr) *)125 definition funct_of_bevals : ∀F,ge.126 beval → beval → option (Σi.is_function F ge i) ≝127 λF,ge,dpl,dph.128 ! ptr ← res_to_opt … (pointer_of_address 〈dpl, dph〉) ;129 if eq_bv … (bv_zero …) (offv (poff ptr)) ∧ (* ← check this condition in front end *)130 match ptype ptr with [ Code ⇒ true | _ ⇒ false] then (* ← already checked in funct_of_block? *)131 funct_of_block … (pblock ptr)132 else None ?.133 134 112 axiom ProgramCounterOutOfCode : String. 135 113 axiom PointNotFound : String. … … 144 122 definition fetch_function: 145 123 ∀F. 124 ∀ge : genv_t F. 125 (Σb.block_region b = Code) → 126 res (ident×F) ≝ 127 λF,ge,bl. 128 opt_to_res … [MSG BadFunction] 129 (! id ← symbol_for_block … ge bl ; 130 ! fd ← find_funct_ptr … ge bl ; 131 return 〈id, fd〉). 132 133 definition fetch_internal_function : 134 ∀F. 146 135 ∀ge : genv_t (fundef F). 147 program_counter → 148 res (Σi.is_internal_function … ge i) ≝ 149 λpars,ge,p. 150 opt_to_res … [MSG BadFunction; MSG BadPointer] 151 (int_funct_of_block … ge (pc_block p)). 136 (Σb.block_region b = Code) → 137 res (ident×F) ≝ 138 λF,ge,bl. 139 ! 〈id, fd〉 ← fetch_function … ge bl ; 140 match fd with 141 [ Internal ifd ⇒ return 〈id, ifd〉 142 | _ ⇒ Error … [MSG BadFunction] 143 ]. 152 144 153 145 record sem_unserialized_params … … 171 163 ; pair_reg_move_ : regsT st_pars → pair_move uns_pars → res (regsT st_pars) 172 164 165 (* Paolo: save_frame separated from call_setup to factorize tailcall code *) 173 166 ; allocate_locals_ : localsT uns_pars → regsT st_pars → regsT st_pars 174 (* Paolo: save_frame separated from call_setup to factorize tailcall code *)175 167 ; save_frame: call_dest uns_pars → state_pc st_pars → res (state st_pars) 176 168 (*CSC: setup_call returns a res only because we can call a function with the wrong number and … … 187 179 ; read_result: ∀globals.genv_gen F globals → call_dest uns_pars → state st_pars → res (list beval) 188 180 ; eval_ext_seq: ∀globals.∀ge : genv_gen F globals.ext_seq uns_pars → 189 (Σi.is_internal_function … ge i) (* current *) → state st_pars → IO io_out io_in(state st_pars)181 ident → F globals (* current *) → state st_pars → res (state st_pars) 190 182 ; pop_frame: ∀globals.∀ge : genv_gen F globals. 191 (Σi.is_internal_function … ge i)(* current *) → state st_pars → res (state_pc st_pars)183 ident → F globals (* current *) → state st_pars → res (state_pc st_pars) 192 184 }. 193 185 … … 241 233 return 〈bv, set_istack … is st〉. 242 234 243 definition save_ra : ∀p. state p → program_counter → res (state p) ≝235 definition push_ra : ∀p. state p → program_counter → res (state p) ≝ 244 236 λp,st,l. 245 237 let 〈addrl,addrh〉 ≝ beval_pair_of_pc l in … … 247 239 push … st' addrh. 248 240 249 definition load_ra : ∀p.state p → res (program_counter × (state p)) ≝241 definition pop_ra : ∀p.state p → res (program_counter × (state p)) ≝ 250 242 λp,st. 251 243 ! 〈addrh, st'〉 ← pop … st; … … 255 247 256 248 (* parameters that are defined by serialization *) 257 record more_sem_params (pp : params) : Type[1] ≝ 258 { msu_pars :> sem_unserialized_params pp (joint_closed_internal_function pp) 259 ; offset_of_point : code_point pp → Pos 260 ; point_of_offset : Pos → code_point pp 249 record sem_params : Type[1] ≝ 250 { spp :> params 251 ; msu_pars :> sem_unserialized_params spp (joint_closed_internal_function spp) 252 ; offset_of_point : code_point spp → Pos 253 ; point_of_offset : Pos → code_point spp 261 254 ; point_of_offset_of_point : 262 255 ∀pt.point_of_offset (offset_of_point pt) = pt … … 278 271 ss_pars_of_ms_pars on _msp : more_sem_params ? to sem_state_params.*) 279 272 280 definition pc_of_point : ∀p .more_sem_params p→281 program_counter →code_point p → program_counter ≝282 λp, msp,ptr,pt.283 mk_program_counter (pc_block ptr) (offset_of_point ? msp pt).273 definition pc_of_point : ∀p:sem_params.(Σb.block_region b = Code) → 274 code_point p → program_counter ≝ 275 λp,bl,pt. 276 mk_program_counter bl (offset_of_point p pt). 284 277 285 278 definition point_of_pc : 286 ∀p.more_sem_params p → program_counter → code_point p ≝ 287 λp,msp,ptr.point_of_offset p msp (pc_offset ptr). 288 289 lemma point_of_pointer_of_point : 290 ∀p,msp.∀ptr,pt. 291 point_of_pc ? msp (pc_of_point p msp ptr pt) = pt. 292 #p #msp #ptr #pt normalize // qed. 293 294 lemma pointer_of_point_block : 295 ∀p,msp,ptr,pt. 296 pc_block (pc_of_point p msp ptr pt) = pc_block ptr. 297 #p #msp #ptr #pt % qed. (* can probably do without *) 298 299 lemma pointer_of_point_uses_block : 300 ∀p,msp.∀ptr1,ptr2.∀pt.pc_block ptr1 = pc_block ptr2 → 301 pc_of_point p msp ptr1 pt = pc_of_point p msp ptr2 pt. 302 #p #msp #ptr1 #ptr2 #pc #EQ normalize >EQ % qed. 303 304 lemma pointer_of_point_of_pointer : 305 ∀p,msp.∀ptr1,ptr2. 306 pc_block ptr1 = pc_block ptr2 → 307 pc_of_point p msp ptr1 (point_of_pc p msp ptr2) = ptr2. 308 #p #msp #ptr1 * #bl2 #o2 #EQ normalize >offset_of_point_of_offset >EQ % qed. 309 310 definition fetch_statement: ∀p : params.∀ msp : more_sem_params p.∀globals. 279 ∀p:sem_params.program_counter → code_point p ≝ 280 λp,ptr.point_of_offset p (pc_offset ptr). 281 282 lemma point_of_pc_of_point : 283 ∀p,bl,pt. 284 point_of_pc p (pc_of_point p bl pt) = pt. 285 #p #bl #pt normalize // qed. 286 287 lemma pc_of_point_of_pc : 288 ∀p,ptr. 289 pc_of_point p (pc_block ptr) (point_of_pc p ptr) = ptr. 290 #p * #bl #off normalize >offset_of_point_of_offset % qed. 291 292 definition fetch_statement: ∀p : sem_params.∀globals. 311 293 ∀ge : genv_t (joint_function p globals). program_counter → 312 res ((Σi.is_internal_function … ge i) × (joint_statement p globals)) ≝ 313 λp,msp,globals,ge,ptr. 314 ! f ← fetch_function … ge ptr ; 315 let fn ≝ if_of_function … f in 316 let pt ≝ point_of_pc ? msp ptr in 294 res (ident × (joint_closed_internal_function p globals) × (joint_statement p globals)) ≝ 295 λp,globals,ge,ptr. 296 ! 〈id, fn〉 ← fetch_internal_function … ge (pc_block ptr) ; 297 let pt ≝ point_of_pc p ptr in 317 298 ! stmt ← opt_to_res … (msg ProgramCounterOutOfCode) (stmt_at … (joint_if_code … fn) pt); 318 return 〈f, stmt〉. 319 320 definition pc_of_label : ∀p : params.∀ msp : more_sem_params p.∀globals. 321 genv_t (joint_function p globals) → program_counter → label → res program_counter ≝ 322 λp,msp,globals,ge,ptr,lbl. 323 ! f ← fetch_function … ge ptr ; 324 let fn ≝ if_of_function … ge f in 299 return 〈id, fn, stmt〉. 300 301 definition pc_of_label : ∀p : sem_params.∀globals. 302 genv_t (joint_function p globals) → (Σb.block_region b = Code) → label → res program_counter ≝ 303 λp,globals,ge,bl,lbl. 304 ! 〈i, fn〉 ← fetch_internal_function … ge bl ; 325 305 ! pt ← opt_to_res … [MSG LabelNotFound ; CTX ? lbl] 326 306 (point_of_label … (joint_if_code … fn) lbl) ; 327 return pc_of_point p msp ptr pt.328 329 definition succ_pc : ∀p : params.∀ msp : more_sem_params p.307 return mk_program_counter bl (offset_of_point p pt). 308 309 definition succ_pc : ∀p : sem_params. 330 310 program_counter → succ p → program_counter ≝ 331 λp,msp,ptr,nxt. 332 let curr ≝ point_of_pc p msp ptr in 333 pc_of_point p msp ptr (point_of_succ p curr nxt). 334 311 λp,ptr,nxt. 312 let curr ≝ point_of_pc p ptr in 313 pc_of_point p (pc_block ptr) (point_of_succ p curr nxt). 314 315 (* 335 316 record sem_params : Type[1] ≝ 336 317 { spp :> params 337 318 ; more_sem_pars :> more_sem_params spp 338 319 }. 339 320 *) 340 321 (* definition msu_pars_of_s_pars : 341 322 ∀p : sem_params.more_sem_unserialized_params (spp p) (λglobals.joint_internal_function globals (spp p)) … … 371 352 372 353 definition goto: ∀p : sem_params.∀globals. 373 genv_t (joint_function p globals) → label → state p → program_counter→ res (state_pc p) ≝374 λp,globals,ge,l,st ,b.375 ! newpc ← pc_of_label ? p … ge bl ;376 return mk_state_pc ?st newpc.354 genv_t (joint_function p globals) → label → state_pc p → res (state_pc p) ≝ 355 λp,globals,ge,l,st. 356 ! newpc ← pc_of_label … ge (pc_block (pc … st)) l ; 357 return mk_state_pc … st newpc. 377 358 378 359 (* … … 383 364 definition next : ∀p : sem_params.succ p → state_pc p → state_pc p ≝ 384 365 λp,l,st. 385 let newpc ≝ succ_pc ? p… (pc … st) l in366 let newpc ≝ succ_pc … (pc … st) l in 386 367 mk_state_pc … st newpc. 387 368 388 389 definition function_of_call ≝ λp:sem_params.λglobals. 369 definition code_block_of_block : block → option (Σb.block_region b = Code) ≝ 370 λbl.match block_region bl 371 return λx.block_region bl = x → option (Σb.block_region b = Code) with 372 [ Code ⇒ λprf.Some ? «bl, prf» 373 | XData ⇒ λ_.None ? 374 ] (refl …). 375 376 definition block_of_call ≝ λp:sem_params.λglobals. 390 377 λge: genv_t (joint_function p globals).λst : state p.λf. 391 match f with 392 [ inl id ⇒ 393 opt_to_res … [MSG BadFunction; MSG MissingSymbol; CTX ? id] (funct_of_ident … ge id) 394 | inr addr ⇒ 395 ! addr_l ← dpl_arg_retrieve … st (\fst addr) ; 396 ! addr_h ← dph_arg_retrieve … st (\snd addr) ; 397 opt_to_res … [MSG BadFunction; MSG BadPointer] (funct_of_bevals … ge addr_l addr_h) 398 ]. 378 ! bl ← match f with 379 [ inl id ⇒ opt_to_res … [MSG BadFunction; CTX … id] (find_symbol … ge id) 380 | inr addr ⇒ 381 ! addr_l ← dpl_arg_retrieve … st (\fst addr) ; 382 ! addr_h ← dph_arg_retrieve … st (\snd addr) ; 383 ! ptr ← pointer_of_bevals … [addr_l ; addr_h ] ; 384 if eq_bv … (bv_zero …) (offv (poff ptr)) then 385 return (pblock … ptr) 386 else 387 Error … [MSG BadFunction; MSG BadPointer] 388 ] ; 389 opt_to_res … [MSG BadFunction; MSG BadPointer] (code_block_of_block bl). 399 390 400 391 (* Paolo: why external calls do not need args?? *) 401 392 definition eval_external_call ≝ 402 λp ,F.λp' : sem_unserialized_params p F.λfn,args,dest,st.403 ! params ← fetch_external_args … p 'fn st args : IO ???;393 λp : sem_params.λfn,args,dest,st. 394 ! params ← fetch_external_args … p fn st args : IO ???; 404 395 ! evargs ← check_eventval_list params (sig_args (ef_sig fn)) : IO ???; 405 396 ! evres ← do_io (ef_id fn) evargs (proj_sig_res (ef_sig fn)); … … 408 399 fixed once we fully implement external functions. *) 409 400 let vs ≝ [mk_val ? evres] in 410 set_result … p' vs dest st. 411 412 definition eval_internal_call_pc ≝ 413 λp : sem_params.λglobals : list ident.λge : genv_t (joint_function p globals).λi. 414 let fn ≝ if_of_function … ge i in 415 let l' ≝ joint_if_entry ?? fn in 416 mk_program_counter (block_of_funct … ge (pi1 … i)) (offset_of_point ? p … l'). 417 [ @block_of_funct_ident_is_code 418 | cases i /2 by internal_function_is_function/ 419 ] 420 qed. 401 set_result … p vs dest st. 402 403 axiom MissingStackSize : String. 421 404 422 405 definition eval_internal_call_no_pc ≝ 423 λp : sem_params.λglobals : list ident.λge : genv p globals.λi,args,st. 424 let fn ≝ if_of_function … ge i in 425 let stack_size ≝ stack_sizes … ge i in 426 ! st' ← setup_call … stack_size (joint_if_params … fn) args st ; 406 λp : sem_params.λglobals : list ident.λge : genv p globals.λi,fn,args,st. 407 ! stack_size ← opt_to_res … [MSG MissingStackSize; CTX … i] (stack_sizes … ge i) ; 408 ! st' ← setup_call … stack_size (joint_if_params … globals fn) args st ; 427 409 return allocate_locals … p (joint_if_locals … fn) st. 428 410 411 axiom NoSuccessor : String. 412 definition next_of_pc : ∀p : sem_params.∀globals.genv_t (joint_function p globals) → 413 program_counter → res (succ p) ≝ 414 λp,globals,ge,pc. 415 ! 〈id_fn, stmt〉 ← fetch_statement … ge pc ; 416 match stmt with 417 [ sequential _ nxt ⇒ return nxt 418 | _ ⇒ Error … [MSG NoSuccessor] 419 ]. 420 429 421 definition eval_seq_no_pc : 430 ∀p:sem_params.∀globals.∀ge:genv p globals. (Σi.is_internal_function … ge i) → 431 state p → joint_seq p globals → 432 IO io_out io_in (state p) ≝ 433 λp,globals,ge,curr_fn,st,seq. 434 match seq return λx.IO ??? with 422 ∀p:sem_params.∀globals.∀ge:genv p globals.ident → 423 joint_closed_internal_function p globals → 424 joint_seq p globals → state p → 425 res (state p) ≝ 426 λp,globals,ge,curr_id,curr_fn,seq,st. 427 match seq with 435 428 [ extension_seq c ⇒ 436 eval_ext_seq … ge c curr_ fn st429 eval_ext_seq … ge c curr_id curr_fn st 437 430 | LOAD dst addrl addrh ⇒ 438 431 ! vaddrh ← dph_arg_retrieve … st addrh ; … … 481 474 | MOVE dst_src ⇒ 482 475 pair_reg_move … st dst_src 483 | CALL f args dest ⇒ 484 ! fn ← function_of_call … ge st f : IO ???; 485 match description_of_function … fn return λx.description_of_function … fn = x → ? with 486 [ Internal fd ⇒ λprf. 487 eval_internal_call_no_pc … ge «fn, ?» args st (* only pc changes *) 488 | External fd ⇒ λ_.eval_external_call … fd args dest st 489 ] (refl …) 490 | _ ⇒ return st 476 | _ ⇒ return st (* for calls do everything in eval_seq_advance *) 491 477 ]. 492 [@hide_prf478 @hide_prf 493 479 @find_symbol_in_globals 494 480 lapply prf … … 497 483 [@eq_identifier_elim #H * >H %1 % ] 498 484 #G %2 @IH @G 499 | @(description_of_internal_function … prf)500 ]501 485 qed. 502 486 503 definition eval_seq_pc : 487 definition eval_seq_call ≝ 488 λp : sem_params.λglobals : list ident.λge : genv p globals.λf,args,dest,nxt. 489 λst : state_pc p. 490 ! bl ← block_of_call … ge st f : IO ???; 491 ! 〈i, fd〉 ← fetch_function … ge bl : IO ???; 492 match fd with 493 [ Internal ifd ⇒ 494 ! st' ← save_frame … dest st ; 495 ! st'' ← eval_internal_call_no_pc p globals ge i ifd args st' ; 496 let pc ≝ pc_of_point p bl (joint_if_entry … ifd) in 497 return mk_state_pc … st'' pc 498 | External efd ⇒ 499 ! st' ← eval_external_call … efd args dest st ; 500 return mk_state_pc … st' (succ_pc p (pc … st) nxt) 501 ]. 502 503 definition eval_seq_advance : 504 504 ∀p:sem_params.∀globals.∀ge:genv p globals. 505 state_pc p → ? → joint_seq p globals→506 res(state_pc p) ≝507 λp,globals,ge,s t,nxt,s.505 joint_seq p globals → succ p → state_pc p → 506 IO io_out io_in (state_pc p) ≝ 507 λp,globals,ge,s,nxt,st. 508 508 match s with 509 509 [ CALL f args dest ⇒ 510 ! fn ← function_of_call … ge st f; 511 match ? return λx.description_of_function … fn = x → ? with 512 [ Internal _ ⇒ λprf. 513 let pc ≝ eval_internal_call_pc … ge «fn, ?» in 514 ! st' ← save_frame … dest st ; 515 return mk_state_pc … st' pc 516 | External _ ⇒ λ_.return next p nxt st 517 ] (refl …) 518 | _ ⇒ return next p nxt st 510 eval_seq_call … ge f args dest nxt st 511 | _ ⇒ return next … nxt st 519 512 ]. 520 @(description_of_internal_function … prf) 521 qed. 522 523 definition eval_statement : 513 514 definition eval_statement_no_pc : 524 515 ∀p:sem_params.∀globals.∀ge:genv p globals. 525 (Σi.is_internal_function … ge i) → state_pc p → 526 ∀s:joint_statement p globals. 527 IO io_out io_in (state_pc p) ≝ 528 λp,g,ge,curr_fn,st,s. 516 ident → joint_closed_internal_function p globals (* current *) → 517 joint_statement p globals → state p → res (state p) ≝ 518 λp,globals,ge,curr_id,curr_fn,s,st. 529 519 match s with 530 520 [ sequential s next ⇒ 521 match s with 522 [ step_seq s ⇒ eval_seq_no_pc … ge curr_id curr_fn s st 523 | COND a l ⇒ return st 524 ] 525 | final s ⇒ return st 526 ]. 527 528 definition eval_return ≝ 529 λp : sem_params.λglobals : list ident.λge : genv p globals. 530 λcurr_id.λcurr_fn : joint_closed_internal_function ??. 531 λst : state p. 532 ! st' ← pop_frame … ge curr_id curr_fn st ; 533 ! nxt ← next_of_pc … ge (pc … st') ; 534 return next … nxt st' (* now address pushed on stack are calling ones! *). 535 536 definition eval_tailcall ≝ 537 λp : sem_params.λglobals : list ident.λge : genv p globals.λf,args,curr_f. 538 λcurr_fn : joint_closed_internal_function ??. 539 λst : state_pc p. 540 ! bl ← block_of_call … ge st f : IO ???; 541 ! 〈i, fd〉 ← fetch_function … ge bl : IO ???; 542 match fd with 543 [ Internal ifd ⇒ 544 ! st' ← eval_internal_call_no_pc p globals ge i ifd args st ; 545 let pc ≝ pc_of_point p bl (joint_if_entry … ifd) in 546 return mk_state_pc … st' pc 547 | External efd ⇒ 548 let curr_dest ≝ joint_if_result ?? curr_fn in 549 ! st' ← eval_external_call … efd args curr_dest st ; 550 eval_return … ge curr_f curr_fn st 551 ]. 552 553 definition eval_statement_advance : 554 ∀p:sem_params.∀globals.∀ge:genv p globals. 555 ident → joint_closed_internal_function p globals → 556 joint_statement p globals → state_pc p → 557 IO io_out io_in (state_pc p) ≝ 558 λp,g,ge,curr_id,curr_fn,s,st. 559 match s with 560 [ sequential s nxt ⇒ 531 561 match s return λ_.IO ??? with 532 562 [ step_seq s ⇒ 533 ! st' ← eval_seq_no_pc … ge curr_fn st s ; 534 let st'' ≝ mk_state_pc … st' (pc … st) in 535 eval_seq_pc ?? ge st'' next s 563 eval_seq_advance … ge s nxt st 536 564 | COND a l ⇒ 537 565 ! v ← acca_retrieve … st a ; 538 566 ! b ← bool_of_beval … v ; 539 ! pc' ← 540 if b then 541 pc_of_label ? p … ge (pc … st) l 542 else 543 return succ_pc ? p (pc … st) next ; 544 return mk_state_pc … st pc' 567 if b then 568 goto … ge l st 569 else 570 return next … nxt st 545 571 ] 546 572 | final s ⇒ 547 573 match s with 548 [ GOTO l ⇒ 549 ! pc' ← pc_of_label ? p ? ge (pc … st) l ; 550 return mk_state_pc … st pc' 551 | RETURN ⇒ pop_frame … curr_fn st 574 [ GOTO l ⇒ goto … ge l st 575 | RETURN ⇒ eval_return … ge curr_id curr_fn st 552 576 | TAILCALL _ f args ⇒ 553 ! fn ← function_of_call … ge st f : IO ???; 554 match ? return λx.description_of_function … fn = x → ? with 555 [ Internal _ ⇒ λprf. 556 let pc' ≝ eval_internal_call_pc … ge «fn, ?» in 557 return mk_state_pc … st pc' 558 | External fd ⇒ λ_. 559 let curr_dest ≝ joint_if_result ?? (if_of_function … curr_fn) in 560 ! st' ← eval_external_call ??? fd args curr_dest st ; 561 pop_frame … curr_fn st' 562 ] (refl …) 577 eval_tailcall … ge f args curr_id curr_fn st 563 578 ] 564 579 ]. 565 @(description_of_internal_function … prf)566 qed.567 580 568 581 definition eval_state : ∀p:sem_params. ∀globals: list ident. … … 570 583 state_pc p → IO io_out io_in (state_pc p) ≝ 571 584 λp,globals,ge,st. 572 ! 〈fn,s〉 ← fetch_statement ? p … ge (pc … st) : IO ???; 573 eval_statement … ge fn st s. 585 ! 〈id,fn,s〉 ← fetch_statement … ge (pc … st) : IO ???; 586 ! st' ← eval_statement_no_pc … ge id fn s st : IO ???; 587 let st'' ≝ mk_state_pc … st' (pc … st) in 588 eval_statement_advance … ge id fn s st''. 574 589 575 590 (* Paolo: what if in an intermediate language main finishes with an external … … 579 594 genv p globals → program_counter → state_pc p → option int ≝ 580 595 λp,globals,ge,exit,st.res_to_opt ? ( 581 do 〈f,s〉 ← fetch_statement ? p … ge (pc … st); 582 let fn ≝ if_of_function … f in 596 do 〈id,fn,s〉 ← fetch_statement … ge (pc … st); 583 597 match s with 584 598 [ final s' ⇒ 585 599 match s' with 586 600 [ RETURN ⇒ 587 do st' ← pop_frame … ge f st; 588 if eq_program_counter (pc … st') exit then 589 do vals ← read_result … ge (joint_if_result … fn) st' ; 601 do st' ← pop_frame … ge id fn st; 602 ! nxt ← next_of_pc … ge (pc … st') ; 603 let pc' ≝ succ_pc … (pc … st') nxt in 604 if eq_program_counter pc' exit then 605 do vals ← read_result … ge (joint_if_result … fn) st ; 590 606 Word_of_list_beval vals 591 607 else -
src/joint/semanticsUtils.ma
r2470 r2529 75 75 mk_sem_params 76 76 g_pars 77 (mk_more_sem_params 78 g_pars 79 (spars ?) 80 (word_of_identifier ?) 81 (an_identifier ?) 82 ? (refl …) 83 ). 77 (spars ?) 78 (word_of_identifier ?) 79 (an_identifier ?) 80 ? (refl …). 84 81 * #p % qed. 85 82 … … 89 86 @pos_elim [%] 90 87 #p #IH >nat_possucc whd in ⊢ (??%?); >IH % qed. 91 92 88 93 89 definition make_sem_lin_params : … … 99 95 mk_sem_params 100 96 lin_pars 101 (mk_more_sem_params 102 lin_pars 103 (spars ?) 104 succ_pos_of_nat 105 (λp.pred (nat_of_pos p)) 106 ?? 107 ). 108 [ @pos_cases [%] #p >nat_possucc @succ_pos_of_nat_of_pos 109 | #n >nat_succ_pos % 97 (spars ?) 98 succ_pos_of_nat 99 (λp.pred (nat_of_pos p)) 100 ??. 101 [ #n >nat_succ_pos % 102 | @pos_cases [%] #p >nat_possucc @succ_pos_of_nat_of_pos 110 103 ] qed. 104 105 106 107 108 lemma fetch_statement_eq : ∀p:sem_params.∀g. 109 ∀ge : genv_t (joint_function p g).∀ptr : program_counter. 110 ∀i,fn,s. 111 fetch_internal_function … ge (pc_block ptr) = OK … 〈i, fn〉 → 112 let pt ≝ point_of_pc … ptr in 113 stmt_at … (joint_if_code … fn) pt = Some ? s → 114 fetch_statement … ge ptr = OK … 〈i, fn, s〉. 115 #p #g #ge #ptr #i #f #s #EQ1 #EQ2 116 whd in match fetch_statement; normalize nodelta >EQ1 >m_return_bind 117 >EQ2 % 118 qed. 119 120 lemma fetch_statement_inv : ∀p:sem_params.∀g. 121 ∀ge : genv_t (joint_function p g).∀ptr : program_counter. 122 ∀i,fn,s. 123 fetch_statement … ge ptr = OK … 〈i, fn, s〉 → 124 fetch_internal_function … ge (pc_block ptr) = OK … 〈i, fn〉 ∧ 125 let pt ≝ point_of_pc p ptr in 126 stmt_at … (joint_if_code … fn) pt = Some ? s. 127 #p #g #ge #ptr #i #fn #s #H 128 elim (bind_inversion ????? H) * #i #f' * #EQ1 -H #H 129 elim (bind_inversion ????? H) #s' * #H 130 lapply (opt_eq_from_res ???? H) -H #EQ2 131 whd in ⊢ (??%%→?); #EQ destruct(EQ) %{EQ1 EQ2} 132 qed. 133 -
src/joint/semantics_blocks.ma
r2422 r2529 1 1 include "joint/blocks.ma". 2 2 include "joint/Traces.ma". 3 include "joint/semanticsUtils.ma". 3 4 4 5 (* let rec seq_list_labels p g (b : list (joint_step p g)) on b : list label ≝ … … 8 9 ].*) 9 10 10 lemma fetch_statement_eq : ∀p:sem_params.∀g.∀ge : genv p g.∀ptr : cpointer. 11 ∀fn,pt,s. 12 fetch_function … ge ptr = OK … fn → 13 point_of_pointer ? p … ptr = pt → 14 stmt_at … (joint_if_code … fn) pt = Some ? s → 15 fetch_statement ? p … ge ptr = OK … 〈fn, s〉. 16 #p #g #ge #ptr #fn #pt #s #EQ1 #EQ2 #EQ3 17 whd in match fetch_statement; normalize nodelta >EQ1 >m_return_bind 18 >EQ2 >EQ3 >m_return_bind % 19 qed. 20 21 include alias "basics/logic.ma". 22 lemma io_evaluate_bind : ∀O,I,X,Y,env. 23 ∀m : IO O I X.∀f : X → IO O I Y. 24 io_evaluate O I Y env (! x ← m ; f x) = 25 ! x ← io_evaluate O I X env m ; 26 io_evaluate O I Y env (f x). 27 #O #I #X #Y #env #m elim m 28 [ #o #g #IH #f whd in match (! x ← Interact ????? ; ?); 29 change with (! y ← ? ; ?) in ⊢ (??%(????%?)); 30 >m_bind_bind @m_bind_ext_eq #i @IH 31 | #x #f % 32 | #e #f % 33 ] 34 qed. 35 36 lemma fetch_function_from_block_eq : 37 ∀p,g,ge. 38 ∀ptr1,ptr2 : cpointer. pblock ptr1 = pblock ptr2 → 39 fetch_function p g ge ptr1 = fetch_function p g ge ptr2. 40 #p #g #ge #ptr1 #ptr2 #EQ 41 whd in match fetch_function; normalize nodelta >EQ 42 @m_bind_ext_eq // qed. 43 44 let rec repeat_eval_seq_no_pc 45 (p : evaluation_params) env curr_fn 46 (l : list (joint_seq p (globals p))) on l : 47 state p → res (state p) ≝ 48 λst.match l with 49 [ nil ⇒ return st 50 | cons hd tl ⇒ 51 ! st' ← io_evaluate … (env st) (eval_seq_no_pc p (globals p) (ev_genv p) curr_fn st hd) ; 52 repeat_eval_seq_no_pc p env curr_fn tl st' 53 ]. 54 55 lemma err_to_io_evaluate : ∀O,I,X,env,m. 56 io_evaluate O I X env (err_to_io … m) = m. 57 #O#I#X#env * // qed. 11 definition repeat_eval_seq_no_pc ≝ 12 λp : evaluation_params.λcurr_id,curr_fn. 13 m_fold … (eval_seq_no_pc … (ev_genv … p) curr_id curr_fn). 58 14 59 15 definition list_not_empty ≝ λA.λl : list A.match l with [ nil ⇒ false | _ ⇒ true ]. 60 16 61 definition no_call_nor_label : ∀p,g.joint_seq p g → bool ≝62 λp,g,s.match s with63 [ COST_LABEL _ ⇒ false64 | CALL_ID _ _ _ ⇒ false65 | extension_call _ ⇒ false66 | _ ⇒ true67 ].68 69 lemma no_call_nor_label_proceed : ∀p : evaluation_params.70 ∀st : state p. ∀s.71 no_call_nor_label p (globals p) s →72 eval_seq_pc p (globals p) (ev_genv p) st s = return Proceed ???.73 #p #st * // [ #f #args #dest | #c ] *74 qed.75 76 lemma no_call_nor_label_other : ∀p : evaluation_params.∀s.77 no_call_nor_label p (globals p) s →78 step_classifier … s = cl_other.79 #p * // [ #f #args #dest | #c ] *80 qed.81 82 lemma no_call_nor_label_uncosted : ∀p : evaluation_params.∀s,nxt.83 no_call_nor_label p (globals p) s →84 cost_label_of_stmt … (sequential … s nxt) = None ?.85 #p * // #lbl#next *86 qed.87 88 definition code_compact : ∀p:sem_params.∀g.codeT p g → Prop ≝89 λp,g,c.code_closed … c∧90 ∀pt,ptr.code_has_point … c pt → ∃ptr'.pointer_of_point p p ptr pt = return ptr'.91 92 definition pointer_of_point_step_in_code : ∀p:sem_params.∀g.93 ∀c,pc,step,dst.94 code_compact p g c → step_in_code … c (point_of_pointer p p pc) step dst →95 Σpc'.pointer_of_point p p pc dst = return pc' ≝96 λp,g,c,pc,step,dst,c_compact,step_in.97 match pointer_of_point p p pc dst98 return λx.pointer_of_point p p pc dst = x → ?99 with100 [ OK pc' ⇒ mk_Sig ?? pc'101 | Error e ⇒ λEQ.⊥102 ] (refl …).103 cases step_in #nxt * #EQ1 #EQ2104 cases c_compact -c_compact #c_closed #c_compact105 elim (c_compact dst pc ?)106 [ >EQ #pc' normalize #ABS destruct(ABS)107 | elim (c_closed … EQ1) #_ whd in ⊢ (%→?);108 >EQ2 #H @H109 ]110 qed.111 112 let rec pointer_of_point_in_code113 p g c pc dst b on b :114 ∀l.code_compact p g c → point_of_pointer p p pc ~❨b,l❩~> dst in c →115 Σpc'.pointer_of_point p p pc dst = return pc' ≝116 match b117 return λb.? → ? → ? ~❨b,?❩~> ? in ? → Σptr'.pointer_of_point p p pc dst = return ptr'118 with119 [ nil ⇒120 λl,c_compact,in_code.121 match pointer_of_point p p pc dst122 return λx.pointer_of_point p p pc dst = x → ? with123 [ OK ptr' ⇒ mk_Sig ?? ptr'124 | Error e ⇒ λEQ.⊥125 ] (refl …)126 | cons hd tl ⇒127 λl.match l return λl.? → ? → Σptr'.? with128 [ nil ⇒ λc_compact,in_code.⊥129 | cons mid rest ⇒ λc_compact,in_code.130 let mid_pc ≝ pointer_of_point_step_in_code … c pc hd mid c_compact ? in131 pi1 … (pointer_of_point_in_code ?? c mid_pc dst tl rest c_compact ?)132 ]133 ].134 [ cases l in in_code; [2: #mid #rest * ]135 whd in ⊢ (%→?); #EQ' <EQ' in EQ; >pointer_of_point_of_pointer [2: %]136 normalize #ABS destruct(ABS)137 | cases (pointer_of_point_in_code ?????????)138 #ptr' >pointer_of_point_uses_block139 [ #H @H |*:]140 cases mid_pc -mid_pc #mid_pc @pointer_of_point_block141 | elim in_code142 | cases mid_pc -mid_pc #mid_pc #EQ143 >(point_of_pointer_of_point … EQ)144 cases in_code #_ #H @H145 | cases in_code #H #_ @H146 ]147 qed.148 149 17 let rec produce_trace_any_any 150 18 (p : evaluation_params) 151 (st : state_pc p) fd 19 (st : state_pc p) 20 curr_id curr_fn 152 21 (b : list (joint_seq p (globals p))) on b : 153 22 ∀l : list (code_point p). 154 23 ∀dst : code_point p. 155 24 ∀st' : state p. 156 fetch_ function p ? (ev_genv p) (pc … st) = return fd →157 ∀prf1 : code_compact p (globals p) (joint_if_code … fd).158 let src ≝ point_of_p ointer pp (pc … st) in25 fetch_internal_function … (ev_genv p) (pc_block (pc … st)) = 26 return 〈curr_id, curr_fn〉 → 27 let src ≝ point_of_pc p (pc … st) in 159 28 if list_not_empty ? b then 160 ! x ← stmt_at ?? (joint_if_code … fd) dst ; cost_label_of_stmt … x = None ?29 ! x ← stmt_at ?? (joint_if_code … curr_fn) dst ; cost_label_of_stmt … x = None ? 161 30 else 162 31 True → 163 ∀prf2 : src ~❨b, l❩~> dst in joint_if_code … fd.164 All ? (λx. bool_to_Prop (no_call_nor_label … x)) b →165 repeat_eval_seq_no_pc p (io_env p) fdb st = return st' →32 src ~❨b, l❩~> dst in joint_if_code … curr_fn → 33 All ? (λx.And (no_call … x) (no_cost_label … x)) b → 34 repeat_eval_seq_no_pc p curr_id curr_fn b st = return st' → 166 35 trace_any_any (joint_abstract_status p) st 167 (mk_state_pc ? st' (pointer_of_point_in_code … prf1 prf2)) ≝ 168 match b 169 return λx.∀l,dst.?→?→?→?→?→?→?→? 36 (mk_state_pc ? st' (pc_of_point p (pc_block (pc … st)) dst)) ≝ match b 37 return λb.∀l,dst.?→?→?→?→?→?→? 170 38 with 171 39 [ nil ⇒ 172 λl,dst,st',fd_prf, c_compact,dst_prf,in_code,all_other,EQ1.40 λl,dst,st',fd_prf,dst_prf,in_code,all_other,EQ1. 173 41 (taa_base (joint_abstract_status p) st) 174 ⌈trace_any_any (joint_abstract_status p) st st↦ ?⌉42 ⌈trace_any_any ??? ↦ ?⌉ 175 43 | cons hd tl ⇒ 176 44 λl. 177 match l return λx. ?→?→?→?→?→?→?→?→? with178 [ nil ⇒ λdst _pc,st',fd_prf,src_prf,dst_prf,in_code.⊥45 match l return λx.∀dst,st'.?→?→?→?→?→? with 46 [ nil ⇒ λdst,st',fd_prf,dst_prf,in_code.⊥ 179 47 | cons mid rest ⇒ 180 λdst,st',fd_prf,c_compact,dst_prf,in_code,all_other,EQ1. 181 let mid_pc ≝ 182 pointer_of_point_step_in_code p ? (joint_if_code … fd) (pc … st) 183 hd mid c_compact ? in 184 match io_evaluate ??? (io_env p st) (eval_seq_no_pc … (ev_genv p) fd st hd) 185 return λx.io_evaluate ??? (io_env p st) (eval_seq_no_pc … (ev_genv p) fd st hd) = x → ? 186 with 187 [ OK st_mid ⇒ λEQ2. 48 λdst,st',fd_prf,dst_prf,in_code,all_other,EQ1. 49 let mid_pc ≝ pc_of_point p (pc_block (pc … st)) mid in 50 match eval_seq_no_pc … (ev_genv p) curr_id curr_fn hd st 51 return λx.eval_seq_no_pc … (ev_genv p) curr_id curr_fn hd st = x → 52 trace_any_any (joint_abstract_status p) st 53 (mk_state_pc ? st' (pc_of_point p (pc_block (pc … st)) dst)) with 54 [ Value st_mid ⇒ λEQ2. 188 55 let tr_tl ≝ produce_trace_any_any ? 189 56 (mk_state_pc ? st_mid mid_pc) 190 fd tl rest dst ??????? in 191 (* works fast only in interactive mode: 192 taa_step … tr_tl *) ? 193 | Error _ ⇒ λEQ2.⊥ 57 curr_id curr_fn tl rest dst ?????? in 58 taa_step … tr_tl 59 | _ ⇒ λEQ2.⊥ 194 60 ] (refl …) 195 61 ] 196 ].[3: @(taa_step … tr_tl) |*:] 197 try (cases mid_pc -mid_pc #mid_pc #EQ_mid_pc) 198 try (cases in_code * #nxt * #EQ_stmt_at #EQ_mid #rest_in_code) 199 try (cases all_other #hd_other #tl_other) 62 ]. 63 [ whd in EQ1 : (??%%); 64 cases l in in_code; whd in ⊢ (%→?); [2: #hd #tl * ] #EQ destruct 65 >pc_of_point_of_pc cases st // 66 | @in_code 67 |3,12: whd in EQ1 : (??%%); >EQ2 in EQ1; whd in ⊢ (??%?→?); #EQ1 destruct(EQ1) 68 ] 69 change with (! y ← ? ; repeat_eval_seq_no_pc ????? = ?) in EQ1; 70 >EQ2 in EQ1; >m_return_bind 71 cases in_code -in_code * #nxt * #EQ_stmt_at #EQ_mid #rest_in_code 72 cases all_other -all_other * #hd_no_call #hd_no_cost #tl_other 73 #EQ1 74 try assumption 200 75 [ whd whd in match eval_state; normalize nodelta 201 >(fetch_statement_eq … fd_prf (refl …)EQ_stmt_at)76 >(fetch_statement_eq … fd_prf EQ_stmt_at) 202 77 >m_return_bind 203 whd in match eval_statement; normalize nodelta 204 whd in match eval_step; normalize nodelta 205 >m_bind_bind 206 >(no_call_nor_label_proceed … hd_other) >m_return_bind 207 >m_bind_bind 208 >io_evaluate_bind >EQ2 >m_return_bind 209 >m_return_bind 78 whd in match eval_statement_no_pc; normalize nodelta 79 >EQ2 >m_return_bind 80 whd in match eval_statement_advance; normalize nodelta 81 >(no_call_advance … hd_no_call) 82 whd in match next; normalize nodelta 210 83 whd in match succ_pc; normalize nodelta 211 >EQ_mid >EQ_mid_pc >m_return_bind % 212 | whd %{fd} %{(sequential … hd nxt)} 213 %{(no_call_nor_label_other … hd_other)} 214 @(fetch_statement_eq … fd_prf (refl …) EQ_stmt_at) 215 |4: cases (pointer_of_point_in_code ?????????) 216 #dst_pc 217 cases l in in_code; [2: #mid #rest * ] 218 whd in ⊢ (%→?); #EQ' <EQ' 219 >pointer_of_point_of_pointer [2: %] lapply EQ1 -EQ1 220 normalize in ⊢ (%→%→?); 221 #EQ1 #EQ'' destruct cases st // 222 |5: >fetch_function_from_block_eq [ @fd_prf |*: ] 223 @(pointer_of_point_block … EQ_mid_pc) 224 |6: cases tl [ % ] #hd' #tl' @dst_prf 225 |7: assumption 226 |8,9: 227 lapply EQ1 whd in ⊢ (??%?→?); >EQ2 normalize nodelta 228 [ #H @H 229 | normalize #ABS destruct(ABS) 84 >EQ_mid % 85 | whd whd in ⊢ (??%?); 86 >(fetch_statement_eq … fd_prf EQ_stmt_at) normalize nodelta 87 @(no_call_other … hd_no_call) 88 | whd in ⊢ (?%); 89 whd in match as_label; normalize nodelta 90 %* #H @H -H whd in ⊢ (??%?); 91 whd in match (as_pc_of ??); 92 inversion (fetch_statement ????) normalize nodelta 93 [2: // ] 94 ** #i' #f' #stmt' #EQ 95 elim (fetch_statement_inv … EQ) 96 >fd_prf 97 whd in ⊢ (??%?→?); #EQ destruct(EQ) 98 whd in ⊢ (%→?); 99 whd in match (point_of_pc ??); >point_of_offset_of_point 100 #EQ' 101 cases tl in tl_other rest_in_code; 102 [ * cases rest [2: #hd' #tl' * ] whd in ⊢ (%→?); #EQ destruct(EQ) 103 >EQ' in dst_prf; >m_return_bind #H @H 104 | #hd' #tl' ** #_ #hd_no_cost' #_ 105 cases rest [ * ] #mid' #rest' * * #nxt' * #EQ_stmt_at' #EQ_mid' #_ 106 >EQ_stmt_at' in EQ'; #EQ' destruct(EQ') 107 @(no_label_uncosted … hd_no_cost') 230 108 ] 231 |3: 232 %* #H @H -H 233 lapply tl_other lapply rest_in_code 234 cases tl [2: #hd' #tl' ] 235 cases rest [2,4: #mid' #rest'] 236 [2,3: * ] 237 [2: whd in ⊢ (%→?); #EQ' destruct(EQ') * 238 | ** #nxt' * #at_mid #_ #_ * #mid_other #_ 239 ] 240 whd in ⊢ (??%?); 241 [ lapply dst_prf ] 242 whd in match as_label; 243 whd in match (as_pc_of ??); 244 whd in match fetch_statement; 245 normalize nodelta 246 >(point_of_pointer_of_point … EQ_mid_pc) 247 >(fetch_function_from_block_eq … (pointer_of_point_block … EQ_mid_pc)) 248 >fd_prf >m_return_bind 249 [ cases (stmt_at ????) [ #_ % ] 250 #stmt #H @H 251 | >at_mid >m_return_bind normalize nodelta 252 @(no_call_nor_label_uncosted … mid_other) 253 ] 109 | >dst_prf cases (list_not_empty ??) % 110 | normalize nodelta >point_of_pc_of_point assumption 254 111 ] 255 112 qed.
Note: See TracChangeset
for help on using the changeset viewer.