Changeset 3154 for src/joint/StatusSimulationHelper.ma
 Timestamp:
 Apr 17, 2013, 2:53:45 PM (7 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/joint/StatusSimulationHelper.ma
r3118 r3154 13 13 (**************************************************************************) 14 14 15 include "joint/semanticsUtils.ma". 16 include "joint/Traces.ma". 17 include "common/StatusSimulation.ma". 18 include "joint/semantics_blocks.ma". 19 include "utilities/listb_extra.ma". 20 include "utilities/lists.ma". 21 22 lemma set_no_pc_eta: 23 ∀P.∀st1: state_pc P. set_no_pc P st1 st1 = st1. 24 #P * // 25 qed. 26 27 lemma pc_of_label_eq : 28 ∀pars: sem_graph_params. 29 ∀globals,ge,bl,i_fn,lbl. 30 fetch_internal_function ? globals ge bl = return i_fn → 31 pc_of_label pars globals ge bl lbl = 32 OK ? (pc_of_point pars bl lbl). 33 #p #globals #ge #bl #i_fn #lbl #EQf 34 whd in match pc_of_label; 35 normalize nodelta >EQf >m_return_bind % 36 qed. 37 38 39 lemma bind_new_bind_new_instantiates : 40 ∀B,X : Type[0]. ∀ m : bind_new B X. ∀ x : X. ∀l : list B.∀P. 41 bind_new_instantiates B X x m l → bind_new_P' ?? P m → 42 P l x. 43 #B #X #m elim m normalize nodelta 44 [#x #y * normalize // #B #l' #P * 45  #f #IH #x #l elim l normalize [#P *] #hd #tl normalize #_ #P #H #Hr @(IH … H) 46 @Hr 47 ] 48 qed. 49 50 let rec bind_instantiate B X (b : bind_new B X) (l : list B) on b : (option X) ≝ 51 match b with 52 [ bret B ⇒ 53 match l with 54 [ nil ⇒ Some ? B 55  _ ⇒ None ? 56 ] 57  bnew f ⇒ 58 match l with 59 [ nil ⇒ None ? 60  cons r l' ⇒ 61 bind_instantiate B X (f r) l' 62 ] 63 ]. 64 65 lemma bind_instantiates_to_instantiate : ∀B,X.∀b : bind_new B X. 66 ∀l : list B.∀x : X. 67 bind_instantiate B X b l = Some ? x → 68 bind_new_instantiates B X x b l. 69 #B #X #b elim b 70 [#x1 * [2: #hd #tl] #x whd in ⊢ (??%? → ?); #EQ destruct(EQ) % 71 #f #IH * [2: #hd #tl] #x whd in ⊢ (??%? → ?); [2: #EQ destruct(EQ)] #H 72 whd @IH assumption 73 ] 74 qed. 75 76 lemma bind_instantiate_instantiates : ∀B,X.∀b : bind_new B X. 77 ∀l : list B.∀x : X. 78 bind_new_instantiates B X x b l → 79 bind_instantiate B X b l = Some ? x. 80 #B #X #b elim b 81 [ #x1 * [2: #hd #tl] #x whd in ⊢ (% → ?); [*] #EQ destruct(EQ) % 82  #f #IH * [2: #hd #tl] #x whd in ⊢ (% → ?); [2: *] #H whd in ⊢ (??%?); @IH @H 83 ] 84 qed. 85 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 ??). 93 94 definition lbl_funct_type ≝ block → label → (list label). 95 definition regs_funct_type ≝ block → label → (list register). 96 97 98 definition preamble_length ≝ 99 λP_in : sem_graph_params.λP_out : sem_graph_params.λprog : joint_program P_in. 100 λstack_size : (ident → option ℕ). 101 λinit : ∀globals.joint_closed_internal_function P_in globals 102 →bound_b_graph_translate_data P_in P_out globals. 103 λinit_regs : block → list register. 104 λf_regs : regs_funct_type.λbl : block.λlbl : label. 105 ! bl ← code_block_of_block bl ; 106 ! 〈id,fn〉 ← res_to_opt … (fetch_internal_function … 107 (joint_globalenv P_in prog stack_size) bl); 108 ! stmt ← stmt_at P_in … (joint_if_code … fn) lbl; 109 ! data ← bind_instantiate ?? (init … fn) (init_regs bl); 110 match stmt with 111 [ sequential step nxt ⇒ 112 ! step_block ← bind_instantiate ?? (f_step … data lbl step) (f_regs bl lbl); 113 return \fst (\fst step_block) 114  final fin ⇒ 115 ! fin_block ← bind_instantiate ?? (f_fin … data lbl fin) (f_regs bl lbl); 116 return \fst fin_block 117  FCOND abs _ _ _ ⇒ Ⓧabs 118 ]. 119 120 121 definition sigma_label : ∀p_in,p_out : sem_graph_params. 122 joint_program p_in → (ident → option ℕ) → 123 (∀globals.joint_closed_internal_function p_in globals 124 →bound_b_graph_translate_data p_in p_out globals) → 125 (block → list register) → lbl_funct_type → regs_funct_type → 126 block → label → option label ≝ 127 λp_in,p_out,prog,stack_size,init,init_regs,f_lbls,f_regs,bl,searched. 128 ! bl ← code_block_of_block bl ; 129 ! 〈id,fn〉 ← res_to_opt … (fetch_internal_function … 130 (joint_globalenv p_in prog stack_size) bl); 131 ! 〈res,s〉 ← 132 find ?? (joint_if_code ?? fn) 133 (λlbl.λ_.match preamble_length … prog stack_size init init_regs f_regs bl lbl with 134 [ None ⇒ false 135  Some n ⇒ match nth_opt ? n (lbl::(f_lbls bl lbl)) with 136 [ None ⇒ false 137  Some x ⇒ eq_identifier … searched x 138 ] 139 ]); 140 return res. 141 142 143 144 145 lemma partial_inj_sigma_label : 146 ∀p_in,p_out,prog,stack_size,init,init_regs. 147 ∀f_lbls : lbl_funct_type.∀f_regs,bl,lbl1,lbl2. 148 sigma_label p_in p_out prog stack_size init init_regs f_lbls f_regs bl lbl1 ≠ None ?→ 149 sigma_label p_in p_out prog stack_size init init_regs f_lbls f_regs bl lbl1 = 150 sigma_label p_in p_out prog stack_size init init_regs f_lbls f_regs bl lbl2 → 151 lbl1 = lbl2. 152 #p_in #p_out #prog #stack_size #init #init_regs #f_lbls #f_regs #bl #lbl1 #lbl2 153 inversion(sigma_label ????????? lbl1) 154 [ #_ * #H @⊥ @H %] 155 #lbl1' #H @('bind_inversion H) H #bl' #EQbl' 156 #H @('bind_inversion H) H * #f #fn #H lapply(res_eq_from_opt ??? H) H 157 #EQfn #H @('bind_inversion H) H * #res #stmt #H1 whd in ⊢ (??%? → ?); 158 #EQ destruct(EQ) #_ #H lapply(sym_eq ??? H) H #H @('bind_inversion H) H 159 #bl'' >EQbl' #EQ destruct(EQ) >EQfn >m_return_bind #H @('bind_inversion H) H 160 * #lbl2' #stmt' #H2 whd in ⊢ (??%? → ?); #EQ destruct(EQ) 161 lapply(find_predicate ?????? H1) lapply(find_predicate ?????? H2) 162 cases (preamble_length ?????????) normalize nodelta [*] #n cases(nth_opt ???) 163 normalize nodelta 164 [*] #lbl @eq_identifier_elim [2: #_ *] #EQ destruct(EQ) #_ @eq_identifier_elim 165 [2: #_ *] #EQ destruct(EQ) #_ % 166 qed. 167 168 definition sigma_pc_opt : 169 ∀p_in,p_out : sem_graph_params. 170 joint_program p_in → (ident → option ℕ) → 171 (∀globals.joint_closed_internal_function p_in globals 172 →bound_b_graph_translate_data p_in p_out globals) → 173 (block → list register) → lbl_funct_type → regs_funct_type → 174 program_counter → option program_counter ≝ 175 λp_in,p_out,prog,stack_size,init,init_regs,f_lbls,f_regs,pc. 176 let target_point ≝ point_of_pc p_out pc in 177 if eqZb (block_id (pc_block pc)) (1) then 178 return pc 179 else 180 ! source_point ← sigma_label p_in p_out prog stack_size init init_regs 181 f_lbls f_regs (pc_block pc) target_point; 182 return pc_of_point p_in (pc_block pc) source_point. 183 184 lemma sigma_stored_pc_inj : 185 ∀p_in,p_out,prog,stack_size,init,init_regs,f_lbls,f_regs,pc,pc'. 186 sigma_pc_opt p_in p_out prog stack_size init init_regs f_lbls f_regs pc ≠ None ? → 187 sigma_pc_opt p_in p_out prog stack_size init init_regs f_lbls f_regs pc = 188 sigma_pc_opt p_in p_out prog stack_size init init_regs f_lbls f_regs pc' → 189 pc = pc'. 190 #p_in #p_out #prog #stack_size #init #init_regs #f_lbls #f_regs 191 * #bl1 #p1 * #bl2 #p2 192 inversion(sigma_pc_opt ??????) [#_ * #H @⊥ @H %] #pc1 193 whd in match sigma_pc_opt in ⊢ (% → ?); normalize nodelta 194 @eqZb_elim [2: *] normalize nodelta #Hbl 195 [ #H @('bind_inversion H) H * #pt1 #EQpt1] 196 whd in ⊢ (??%? → ?); #EQ destruct(EQ) 197 #_ #H lapply(sym_eq ??? H) H whd in match sigma_pc_opt; 198 normalize nodelta @eqZb_elim [2,4: *] #Hbl1 normalize nodelta 199 [1,2: #H @('bind_inversion H) H * #pt2 #EQpt2] whd in match pc_of_point; 200 normalize nodelta whd in match (offset_of_point ??); 201 whd in ⊢ (??%% → ?); #EQ destruct(EQ) 202 [2,3: @⊥ [ >Hbl in Hbl1;  >Hbl1 in Hbl;] #H @H % 4: %] 203 whd in match (offset_of_point ??) in EQpt2; 204 <EQpt1 in EQpt2; #H lapply(partial_inj_sigma_label … (sym_eq ??? H)) 205 [ >EQpt1 % #EQ prog destruct(EQ)] whd in match point_of_pc; normalize nodelta 206 whd in match (point_of_offset ??); whd in match (point_of_offset ??); 207 #EQ prog destruct(EQ) % 208 qed. 209 210 lemma match_reg_elim : ∀ A : Type[0]. ∀ P : A → Prop. ∀ r : region. 211 ∀f : (r = XData) → A. ∀g : (r = Code) → A. (∀ prf : r = XData.P (f prf)) → 212 (∀ prf : r = Code.P (g prf)) → 213 P ((match r return λx.(r = x → ?) with 214 [XData ⇒ f  Code ⇒ g])(refl ? r)). 215 #A #P * #f #g #H1 #H2 normalize nodelta [ @H1  @H2] 216 qed. 217 218 definition sigma_stored_pc ≝ 219 λp_in,p_out,prog,stack_size,init,init_regs,f_lbls,f_regs,pc. 220 match sigma_pc_opt p_in p_out prog stack_size init init_regs f_lbls f_regs pc with 221 [None ⇒ null_pc (pc_offset … pc)  Some x ⇒ x]. 222 223 lemma code_block_of_block_eq : ∀bl : Σb.block_region b = Code. 224 code_block_of_block bl = return bl. 225 * #bl #prf whd in match code_block_of_block; normalize nodelta @match_reg_elim 226 [ >prf in ⊢ (% → ?); #ABS destruct(ABS)] #prf1 % 227 qed. 228 229 (*TO BE MOVED*) 230 lemma Exists_append1 : ∀A.∀l1,l2 : list A.∀P.Exists A P l1 → Exists A P (l1@l2). 231 #A #l1 elim l1 [#l2 #P *] #hd #tl #IH * 232 [#P normalize // ] #hd1 #tl1 #P normalize * [#H % assumption  #H %2 @IH assumption] 233 qed. 234 235 lemma Exists_append2 : ∀A.∀l1,l2 : list A.∀P.Exists A P l2 → Exists A P (l1@l2). 236 #A #l1 #l2 lapply l1 l1 elim l2 [#l1 #a *] #hd #tl #IH * 237 [#a normalize // ] #hd1 #tl1 #a normalize * 238 [ #H %2 >append_cons @Exists_append1 elim tl1 [% assumption] #hd2 #tl2 #H1 normalize %2 // 239  #H %2 >append_cons @IH assumption] 240 qed. 241 242 lemma seq_list_in_code_length : ∀p : params. ∀globals : list ident. 243 ∀code : codeT p globals.∀src : code_point p.∀l1,l2,dst. 244 seq_list_in_code p globals code src l1 l2 dst → l1 = l2. 245 #p #globals #code #src #l1 lapply src src elim l1 246 [ #src * [ #dst #_ %] #hd #tl #dst whd in ⊢ (% → ?); * #EQ destruct] 247 #hd #tl #IH #src * [ #dst whd in ⊢ (% → ?); * #mid * #rest ** #EQ destruct] 248 #hd1 #tl1 #dst whd in ⊢ (% → ?); * #mid * #rest ** #EQ destruct * #nxt1 * #EQstnt 249 #EQsucc #H whd in ⊢ (??%%); @eq_f @(IH … H) 250 qed. 251 252 lemma fetch_stmt_ok_succ_ok : ∀p : sem_graph_params. 253 ∀prog : joint_program p.∀stack_size,f,fn,stmt,pc,pc',lbl. 254 In ? (stmt_labels p ? stmt) lbl→ 255 fetch_statement p … (joint_globalenv p prog stack_size) pc = return 〈f,fn,stmt〉 → 256 pc' = pc_of_point p (pc_block pc) lbl → 257 ∃stmt'.fetch_statement p … (joint_globalenv p prog stack_size) pc' = return 〈f,fn,stmt'〉. 258 #p #prog #stack_size #f #fn #stmt #pc #pc' #lbl #Hlbl #EQfetch 259 cases(fetch_statement_inv … EQfetch) #EQfn normalize nodelta #EQstmt 260 #EQ destruct(EQ) lapply(code_is_closed … (pi2 ?? fn) … EQstmt) * 261 cases(decidable_In ? (stmt_explicit_labels … stmt) lbl ?) 262 [3: * cases lbl #x #y cases(decidable_eq_pos … x y) 263 [#EQ destruct % %  * #H %2 % #H1 @H destruct %] 264  whd in ⊢ (% → ?); #H1 #H2 cases(Exists_All … H1 H2) #lbl1 * #EQ destruct 265 whd in match code_has_label; whd in match code_has_point; normalize nodelta 266 inversion(stmt_at ????) [#_ *] #stmt' #EQstmt' #_ #_ %{stmt'} 267 whd in match fetch_statement; normalize nodelta >EQfn >m_return_bind 268 >point_of_pc_of_point >EQstmt' % 269  #H lapply(In_all ??? H) H cases(Exists_append … Hlbl) 270 [ cases stmt [ #step #nxt  #fin  *] whd in match stmt_implicit_label; 271 normalize nodelta [2: *] * [2: *] #EQ destruct(EQ) #_ #_ 272 whd in match stmt_forall_succ; whd in match code_has_point; normalize nodelta 273 inversion(stmt_at ????) [#_ *] #stmt' #EQstmt' #_ %{stmt'} 274 whd in match fetch_statement; normalize nodelta >EQfn >m_return_bind 275 >point_of_pc_of_point >EQstmt' % 276  #H1 #H2 cases(Exists_All … H1 H2) #x * #EQ destruct * #H @⊥ @H % 277 ] 278 ] 279 qed. 280 281 282 lemma fetch_stmt_ok_nxt_ok : ∀p : sem_graph_params. 283 ∀prog : joint_program p.∀stack_size,f,fn,stmt,bl,pt,nxt. 284 fetch_internal_function … (joint_globalenv p prog stack_size) bl = 285 return 〈f,fn〉→ 286 stmt_at p … (joint_if_code … fn) pt = return sequential p ? stmt nxt → 287 ∃stmt'. 288 stmt_at p … (joint_if_code … fn) nxt = return stmt'. 289 #p #prog #stack_size #f #fn #stmt #bl #pt #nxt #EQfn #EQstmt 290 cases(fetch_stmt_ok_succ_ok … 291 prog stack_size f fn (sequential p … stmt nxt) (pc_of_point p bl pt) 292 (pc_of_point p bl nxt) nxt ???) 293 [ #stmt' #H cases(fetch_statement_inv … H) H #_ >point_of_pc_of_point normalize nodelta 294 #EQstmt' %{stmt'} assumption 295  whd in match stmt_labels; normalize nodelta % % 296  whd in match fetch_statement; normalize nodelta >EQfn >m_return_bind 297 >point_of_pc_of_point >EQstmt % 298  % 299 ] 300 qed. 301 302 303 lemma sigma_label_spec : ∀p_in,p_out,prog,stack_size,init,init_regs. 304 ∀f_lbls : lbl_funct_type.∀f_regs. 305 b_graph_transform_program_props p_in p_out stack_size init prog init_regs f_lbls f_regs → 306 ∀id,fn. 307 ∀bl:Σb.block_region b = Code. ∀pt,stmt. 308 block_id … bl ≠ 1 → 309 fetch_internal_function … 310 (joint_globalenv p_in prog stack_size) bl = return 〈id,fn〉 → 311 stmt_at p_in … (joint_if_code … fn) pt = return stmt → 312 ∃n.preamble_length … prog stack_size init init_regs f_regs bl pt = return n ∧ 313 match n with 314 [ O ⇒ sigma_label p_in p_out prog stack_size init init_regs f_lbls f_regs bl pt = return pt 315  S m ⇒ ∃lbl.nth_opt ? m (f_lbls bl pt) = return lbl ∧ 316 sigma_label p_in p_out prog stack_size init init_regs f_lbls f_regs bl lbl = return pt 317 ]. 318 #p_in #p_out #prog #stack_size #init #init_regs #f_lbls #f_regs #good #id #fn 319 #bl #pt #stmt * #Hbl #EQfn #EQstmt 320 lapply(b_graph_transform_program_fetch_internal_function … good … bl id fn) 321 @eqZb_elim [ #EQ >EQ in Hbl; #H @⊥ @H %] #_ normalize nodelta #H cases(H EQfn) H 322 #data * #t_fn ** #EQt_fn #Hinit * #_ #_ #_ #pp_labs #_ #fresh_lab #_ #_ #_ #H 323 lapply(H … EQstmt) H normalize nodelta cases stmt in EQstmt; stmt 324 [ #j_step #nxt  #fin  * ] #EQstmt normalize nodelta ** 325 [ * #pre_instr #instr #post_instr  #pre_instr #instr] * 326 [ cases(added_prologue ????) [2: #hd_instr #tl_instrs ] normalize nodelta 327 [ @eq_identifier_elim #EQentry normalize nodelta 328 [ whd in ⊢ (% → ?); inversion (f_regs ??) [2: #x #y #_ #_ *] #EQregs normalize nodelta 329 whd in ⊢ (???% → ?); #EQ destruct(EQ) 330 *: #Hregs 331 ] 332  #Hregs 333 ] 334  #Hregs 335 ] 336 #syntax_spec 337 [4: cases(added_prologue ????) [2: #hd_instr #tl_instrs ] normalize nodelta ] #_ 338 [1,2,4,5: %{(pre_instr)}  %{O}] 339 cut(? : Prop) 340 [3,6,9,12,15: #EQn %{EQn} whd in EQn; normalize nodelta 341 [1,2,3,4: cases pre_instr in Hregs syntax_spec EQn; [2,4,6,8: #hd #tl] #Hregs #syntax_spec 342 whd in match (length ??); #EQn whd in match (length ??); normalize nodelta] 343 [5,6,7,8,9: whd in match sigma_label; normalize nodelta >code_block_of_block_eq 344 >m_return_bind >EQfn >m_return_bind inversion(find ????) 345 [1,3,5,7,9: #EQfind @⊥ lapply(find_none ?????? EQfind EQstmt) >EQn normalize nodelta 346 @eq_identifier_elim [1,3,5,7,9: #_ *] * #H #_ @H % ] * #lbl1 #stmt1 #EQfind 347 >m_return_bind @eq_f lapply(find_predicate ?????? EQfind) whd in match preamble_length; 348 normalize nodelta >code_block_of_block_eq >m_return_bind >EQfn >m_return_bind 349 whd in match (stmt_at ????); >(find_lookup ?????? EQfind) >m_return_bind >Hinit 350 >m_return_bind cases stmt1 in EQfind; stmt1 351 [1,4,7,10,13: #j_step1 #nxt1 2,5,8,11,14: #fin1 *: *] #EQfind normalize nodelta 352 cases(bind_instantiate ????) [1,3,5,7,9,11,13,15,17,19: *] 353 [1,2,3,4,5: ** #pre_instr1 #instr1 #post_instr1 *: * #pre_instr1 #instr1 ] 354 >m_return_bind cases pre_instr1 pre_instr1 [2,4,6,8,10,12,14,16,18,20: #hd #tl] 355 whd in match (length ??); normalize nodelta 356 [11,12,13,14,15,16,17,18,19,20: @eq_identifier_elim [2,4,6,8,10,12,14,16,18,20: #_ *] 357 #EQ #_ >EQ %] 358 whd in match (nth_opt ???); inversion(nth_opt ???) [1,3,5,7,9,11,13,15,17,19: #_ *] 359 #lbl2 #EQlbl2 normalize nodelta @eq_identifier_elim [2,4,6,8,10,12,14,16,18,20: #_ *] 360 #EQ lapply EQlbl2 destruct(EQ) #EQlbl2 @⊥ 361 cases(Exists_All … (nth_opt_Exists … EQlbl2) (fresh_lab lbl1)) #x * #EQ destruct(EQ) 362 ** #H #_ @H @(code_is_in_universe … (pi2 ?? fn)) whd in match code_has_label; 363 whd in match code_has_point; normalize nodelta >EQstmt @I 364 *: cases syntax_spec syntax_spec #pre * #mid1 [3,4: * #mid2 * #post] ** [1,2: *] 365 cases pre pre [1,3,5,7: #_ * #x * #y ** #ABS destruct(ABS)] #hd1 #tl1 whd in ⊢ (??%% → ?); 366 #EQ destruct(EQ) EQ #pre_spec whd in ⊢ (% → ?); 367 [1,2: * #nxt1 * #EQt_stmt change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) #post_spec 368 *: #EQt_stmt 369 ] 370 %{mid1} cut(? : Prop) 371 [3,6,9,12: #EQnth_opt %{EQnth_opt} whd in match sigma_label; normalize nodelta 372 >code_block_of_block_eq >m_return_bind >EQfn >m_return_bind inversion(find ????) 373 [1,3,5,7: #EQfind @⊥ lapply(find_none ?????? EQfind EQstmt) >EQn normalize nodelta 374 whd in match (nth_opt ???); >EQnth_opt normalize nodelta @eq_identifier_elim 375 [1,3,5,7: #_ *] * #H #_ @H % ] * #lbl1 #stmt1 #EQfind >m_return_bind @eq_f 376 lapply(find_predicate ?????? EQfind) whd in match preamble_length; 377 normalize nodelta >code_block_of_block_eq >m_return_bind >EQfn >m_return_bind 378 whd in match (stmt_at ????); >(find_lookup ?????? EQfind) >m_return_bind >Hinit 379 >m_return_bind cases stmt1 in EQfind; stmt1 380 [1,4,7,10: #j_step1 #nxt1 2,5,8,11: #fin1 *: *] #EQfind normalize nodelta 381 cases(bind_instantiate ????) [1,3,5,7,9,11,13,15: *] 382 [1,2,3,4: ** #pre_instr1 #instr1 #post_instr1 *: * #pre_instr1 #instr1] 383 >m_return_bind cases pre_instr1 pre_instr1 [2,4,6,8,10,12,14,16: #hd1 #tl1] 384 whd in match (length ??); normalize nodelta whd in match (nth_opt ???); 385 [1,2,3,4,5,6,7,8: inversion(nth_opt ???) [1,3,5,7,9,11,13,15: #_ *] #lbl2 386 #EQlbl2 normalize nodelta @eq_identifier_elim [2,4,6,8,10,12,14,16: #_ *] 387 #EQ lapply EQlbl2 destruct(EQ) #EQlbl2 #_ @(proj2 … pp_labs ?? lbl2) 388 @Exists_memb [1,3,5,7,9,11,13,15: @(nth_opt_Exists … EQlbl2)] 389 >e0 @Exists_append2 % % 390 *: @eq_identifier_elim [2,4,6,8,10,12,14,16: #_ *] #EQ destruct(EQ) @⊥ 391 lapply(fresh_lab hd1) >e0 #H cases(append_All … H) #_ * H ** #H #_ #_ @H 392 @(code_is_in_universe … (pi2 ?? fn)) whd in match code_has_label; 393 whd in match code_has_point; normalize nodelta whd in match (stmt_at ????); 394 >(find_lookup ?????? EQfind) @I 395 ] 396 2,5,8,11: >e0 cases pre_spec #fst * #rest ** #EQ destruct(EQ) 397 whd in ⊢ (% → ?); * #nxt1 * #_ change with nxt1 in ⊢ (??%? → ?); 398 #EQ destruct(EQ) #H lapply(seq_list_in_code_length … H) 399 [1,2: >length_map] H #H >H >nth_opt_append_r cases(rest) 400 try % try( #n %) #n <minus_n_n % 401 *: 402 ] 403 ] 404 2,5,8,11,14: whd in match preamble_length; normalize nodelta >code_block_of_block_eq 405 >m_return_bind >EQfn >m_return_bind >EQstmt >m_return_bind >Hinit >m_return_bind 406 normalize nodelta 407 [1,2,3,4: >Hregs % 408  >EQregs <EQentry in EQstmt; cases(entry_is_cost … (pi2 ?? fn)) #succ * #c 409 #EQstmt >EQstmt whd in ⊢ (???% → ?); #EQ destruct(EQ) >(f_step_on_cost … data) 410 whd in match (bind_instantiate ????); % 411 ] 412 *: 413 ] 414 qed. 415 416 lemma pc_block_eq : ∀p_in,p_out,prog,stack_sizes,init,init_regs,f_lbls, 417 f_regs,pc. 418 sigma_pc_opt p_in p_out prog stack_sizes init 419 init_regs f_lbls f_regs pc ≠ None ? → 420 pc_block … pc = 421 pc_block … (sigma_stored_pc p_in p_out prog stack_sizes init 422 init_regs f_lbls f_regs pc). 423 #p_in #p_out #prog #stack_sizes #init #init_regs #f_lbls #f_regs #pc 424 whd in match sigma_stored_pc; normalize nodelta 425 inversion(sigma_pc_opt ?????????) [ #_ * #ABS @⊥ @ABS %] #pc1 426 whd in match sigma_pc_opt; normalize nodelta @eqZb_elim #_ normalize nodelta 427 [ whd in ⊢ (??%? → ?); #EQ destruct #_ %] #H @('bind_inversion H) H 428 #lbl #_ whd in ⊢ (??%? → ?); #EQ destruct #_ % 429 qed. 430 431 definition stmt_get_next : ∀p,globals.joint_statement p globals → option (succ p) ≝ 432 λp,globals,stmt. 433 match stmt with 434 [sequential stmt nxt ⇒ Some ? nxt 435  _ ⇒ None ? 436 ]. 437 438 439 definition sigma_next : ∀p_in,p_out : sem_graph_params. 440 joint_program p_in → (ident → option ℕ) → 441 (∀globals.joint_closed_internal_function p_in globals 442 →bound_b_graph_translate_data p_in p_out globals) → 443 (block → list register) → lbl_funct_type → regs_funct_type → 444 block → label → option label ≝ 445 λp_in,p_out,prog,stack_size,init,init_regs,f_lbls,f_regs,bl,searched. 446 ! bl ← code_block_of_block bl ; 447 ! 〈id,fn〉 ← res_to_opt … (fetch_internal_function … 448 (joint_globalenv p_in prog stack_size) bl); 449 ! 〈res,s〉 ← 450 find ?? (joint_if_code ?? fn) 451 (λlbl.λstmt.match stmt_get_next … stmt with 452 [ None ⇒ false 453  Some nxt ⇒ 454 match preamble_length … prog stack_size init init_regs f_regs bl lbl with 455 [ None ⇒ false 456  Some n ⇒ match nth_opt ? n ((f_lbls bl lbl) @ [nxt]) with 457 [ None ⇒ false 458  Some x ⇒ eq_identifier … searched x 459 ] 460 ] 461 ]); 462 stmt_get_next … s. 463 464 lemma fetch_statement_sigma_stored_pc : 465 ∀p_in,p_out,prog,stack_sizes, 466 init,init_regs,f_lbls,f_regs,pc,f,fn,stmt. 467 b_graph_transform_program_props p_in p_out stack_sizes 468 init prog init_regs f_lbls f_regs → 469 block_id … (pc_block pc) ≠ 1 → 470 let trans_prog ≝ b_graph_transform_program p_in p_out init prog in 471 fetch_statement p_in … (joint_globalenv p_in prog stack_sizes) pc = 472 return 〈f,fn,stmt〉 → 473 ∃data.bind_instantiate ?? (init … fn) (init_regs (pc_block pc)) = return data ∧ 474 match stmt with 475 [ sequential step nxt ⇒ 476 ∃step_block : step_block p_out (prog_names … trans_prog). 477 bind_instantiate ?? (f_step … data (point_of_pc p_in pc) step) 478 (f_regs (pc_block pc) (point_of_pc p_in pc)) = return step_block ∧ 479 ∃pc'.sigma_stored_pc p_in p_out prog stack_sizes init 480 init_regs f_lbls f_regs pc' = pc ∧ 481 ∃fn',nxt',l1,l2. 482 fetch_statement p_out … (joint_globalenv p_out trans_prog stack_sizes) pc' = 483 if not_emptyb … (added_prologue … data) ∧ 484 eq_identifier … (point_of_pc p_in pc) (joint_if_entry … fn) 485 then OK ? 〈f,fn',sequential ?? (NOOP …) nxt'〉 486 else OK ? 〈f,fn',sequential ?? ((\snd(\fst step_block)) (point_of_pc p_in pc')) nxt'〉 ∧ 487 seq_list_in_code p_out (prog_names … trans_prog) (joint_if_code … fn') (point_of_pc p_out pc) 488 (map_eval … (\fst (\fst step_block)) (point_of_pc p_out pc')) 489 l1 (point_of_pc p_out pc') 490 ∧ seq_list_in_code p_out ? (joint_if_code … fn') nxt' (\snd step_block) l2 nxt 491 ∧ sigma_next p_in p_out prog stack_sizes init init_regs f_lbls f_regs (pc_block pc) nxt' = return nxt 492  final fin ⇒ 493 ∃fin_block.bind_instantiate ?? (f_fin … data (point_of_pc p_in pc) fin) 494 (f_regs (pc_block pc) (point_of_pc p_in pc)) = return fin_block ∧ 495 ∃pc'.sigma_stored_pc p_in p_out prog stack_sizes init 496 init_regs f_lbls f_regs pc' = pc ∧ 497 ∃fn'.fetch_statement p_out … 498 (joint_globalenv p_out trans_prog stack_sizes) pc' 499 = return 〈f,fn',final ?? (\snd fin_block)〉 500  FCOND abs _ _ _ ⇒ Ⓧabs 501 ]. 502 #p_in #p_out #prog #stack_sizes #init #init_regs #f_lbls #f_regs #pc #f #fn #stmt 503 #good #Hbl #EQfetch cases(fetch_statement_inv … EQfetch) #EQfn normalize nodelta 504 #EQstmt 505 lapply(b_graph_transform_program_fetch_internal_function … good … (pc_block pc) f fn) 506 @eqZb_elim [ #EQ >EQ in Hbl; * #H @⊥ @H %] #_ normalize nodelta #H cases(H EQfn) H 507 #data * #t_fn ** #EQt_fn #Hinit * #_ #_ #_ #pp_labs #_ #fresh_labs #_ #_ #_ #H 508 lapply(H … EQstmt) H normalize nodelta #H #_ %{data} >Hinit %{(refl …)} 509 EQfetch cases stmt in EQstmt H; 510 [ #step #nxt  #fin  *] normalize nodelta #EQstmt stmt 511 [ cases(added_prologue ??? data) [2: #hd #tl] normalize nodelta 512 [ @eq_identifier_elim #EQentry normalize nodelta ] ] 513 * #block * 514 [ whd in ⊢ (% → ?); inversion(f_regs ??) [2: #x #y #_ #_ *] #EQregs normalize nodelta 515 #EQ destruct(EQ) whd in ⊢ (% → ?); * #pre * #mid1 * #mid2 * #post *** #EQmid1 516 whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in ⊢ (% → ?); * #nxt1 517 * #EQt_stmt change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) whd in ⊢ (% → ?); 518 * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in EQmid1 : (??%%); destruct(EQmid1) 519 *: #Hregs #syntax_spec 520 ] 521 [ whd in match (point_of_pc ??) in EQstmt EQentry; <EQentry in EQstmt; 522 cases(entry_is_cost … (pi2 ?? fn)) #nxt1 * #c #EQstmt >EQstmt #EQ destruct(EQ) 523 % [2: % [ >(f_step_on_cost … data) in ⊢ (??%?); % ] ] %{pc} 524 whd in match sigma_stored_pc; whd in match sigma_pc_opt; normalize nodelta 525 @eqZb_elim normalize nodelta [#ABS >ABS in Hbl; * #H @⊥ @H %] #_ 526 *: %{block} >Hregs %{(refl …)} 527 ] 528 cases(sigma_label_spec … good … Hbl EQfn EQstmt) * [2,4,6,8: #n ] * #EQpreamble 529 normalize nodelta [1,2,3,4: * #lbl * #EQnth_opt] #EQsigma_lab 530 [ whd in match (point_of_pc ??) in e0; <EQentry in e0; #e0 >e0 in EQnth_opt; 531 whd in ⊢ (??%% → ?); #EQ destruct(EQ) 532 5: whd in match (point_of_pc ??); <EQentry >EQsigma_lab >m_return_bind 533 normalize nodelta >EQentry % [ cases pc #bl #off %] %{t_fn} %{nxt} %{[ ]} %{[ ]} 534 whd in match fetch_statement; normalize nodelta >EQt_fn >m_return_bind 535 >EQt_stmt >m_return_bind % 536 [ % [ % [ @eq_identifier_elim [#_ %] * #H @⊥ @H %  %{(refl …) (refl …)}]  %{(refl …) (refl …)}]] 537 whd in match sigma_next; normalize nodelta >code_block_of_block_eq 538 >m_return_bind >EQfn >m_return_bind inversion(find ????) 539 [ #EQfind @⊥ lapply(find_none … EQfind EQstmt) normalize nodelta 540 >EQpreamble normalize nodelta >EQentry >e0 normalize nodelta 541 @eq_identifier_elim [#_ *] * #H #_ @H %] 542 * #lbl1 #stmt1 #EQfind >m_return_bind lapply(find_predicate ?????? EQfind) 543 inversion(stmt_get_next … stmt1) [#_ *] #nxt1 #EQnxt1 normalize nodelta 544 inversion(preamble_length ?????????) [#_ *] #m whd in match preamble_length; 545 normalize nodelta >code_block_of_block_eq >m_return_bind >EQfn >m_return_bind 546 whd in match (stmt_at ????); >(find_lookup ?????? EQfind) >m_return_bind 547 >Hinit >m_return_bind cases stmt1 in EQfind; [#j_step #succ  #fin  *] 548 #EQfind normalize nodelta cases(bind_instantiate ???) 549 [1,3: whd in ⊢ (??%% → ?); #EQ destruct] #bl1 >m_return_bind whd in ⊢ (??%? → ?); 550 #EQ destruct(EQ) inversion(nth_opt ???) [1,3: #_ *] #lbl2 #EQlbl2 normalize nodelta 551 @eq_identifier_elim [2,4: #_ *] #EQ lapply EQlbl2 destruct(EQ) #EQlbl2 552 cases(Exists_append … (nth_opt_Exists ???? EQlbl2)) [2,4: * [2,4: *] #EQ >EQ #_ %] 553 #H @⊥ cases(Exists_All … H (fresh_labs lbl1)) #x * #EQ destruct(EQ) ** H #H #_ 554 @H @(code_is_in_universe … (pi2 ?? fn)) whd in match code_has_label; 555 whd in match code_has_point; normalize nodelta 556 cases(fetch_stmt_ok_nxt_ok … EQfn EQstmt) #stmt2 #EQ >EQ @I 557 2,3,4: %{(pc_of_point p_out (pc_block pc) lbl)} 558 6,7,8: %{pc} 559 ] 560 whd in match sigma_stored_pc; whd in match sigma_pc_opt; normalize nodelta 561 @eqZb_elim [1,3,5,7,9,11: #H >H in Hbl; * #H1 @⊥ @H1 %] #_ normalize nodelta 562 [1,2,3: >point_of_pc_of_point] >EQsigma_lab >m_return_bind >(pc_of_point_of_pc … pc) 563 %{(refl …)} %{t_fn} cases block in Hregs syntax_spec; block 564 [1,2,4,5: * #pre #instr #post *: #pre #instr ] #Hregs * 565 [1,2,3,4: #l1 * #mid1 * #mid2 * #l2 *** 566 *: #l1 * #mid ** 567 ] 568 #EQmid #EQpre whd in ⊢ (% → ?); 569 [1,2,3,4: * #nxt1 *] #EQt_stmt 570 [1,2,3,4: change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) #EQpost %{mid2} %{l1} %{l2} %] 571 [1,3,5,7,9,10: whd in match fetch_statement; normalize nodelta >EQt_fn >m_return_bind 572 @('bind_inversion EQpreamble) #bl1 >code_block_of_block_eq whd in ⊢ (??%? → ?); 573 #EQ destruct(EQ) >EQfn >m_return_bind >EQstmt >m_return_bind >Hinit >m_return_bind 574 normalize nodelta >Hregs >m_return_bind cases pre in Hregs EQpre; pre 575 [1,3,6,8,9,12: [3,4,6: #x #y] #_ #_ whd in match (length ??); whd in ⊢ (??%? → ?); 576 #EQ destruct(EQ)] 577 [1,2,5: #hd1 #tl1 ] #Hregs cases l1 in EQmid; 578 [1,3,5,8,10,12: [4,5,6: #x #y] #_ whd in ⊢ (% → ?); [1,2,3: * #EQ1 #EQ2 destruct] 579 * #mid * #rest ** #EQ destruct(EQ)] 580 [1,2,3: #hd2 #tl2] whd in ⊢ (??%% → ?); #EQ destruct(EQ) whd in ⊢ (% → ?); 581 [4,5,6: * #_ #EQ #_ >EQ >EQt_stmt [2,3: % [ %{(refl …)} %{(refl …) (refl …)} ] assumption] 582 @eq_identifier_elim [2: #_ % [ %{(refl …)} %{(refl …) (refl …)}  assumption] ] 583 #EQ <EQ in EQentry; * #H @⊥ @H %] 584 * #mid' * #rest ** #EQ1 destruct(EQ1) #H1 #H2 whd in match (length ??); 585 whd in ⊢ (??%? → ?); #EQ1 destruct(EQ1) >e0 in EQnth_opt; 586 lapply(seq_list_in_code_length … H2) [1,2: >length_map] #EQ1 >EQ1 587 >nth_opt_append_r [2,4,6: %] cut(restrest=O) [1,3,5: cases(rest) //] 588 #EQ2 >EQ2 whd in ⊢ (??%% → ?); #EQ3 EQ2 EQ1 589 [1,2: destruct(EQ3) >point_of_pc_of_point >EQt_stmt 590 [2: >point_of_pc_of_point % [%{(refl …)} whd %{mid'} %{rest} % [2: assumption] % [2: assumption] %] 591 assumption] 592 @eq_identifier_elim [#EQ4 <EQ4 in EQentry; * #H3 @⊥ @H3 %] #_ >point_of_pc_of_point % 593 [ %{(refl …)} whd %{mid'} %{rest} % [ %{(refl …)} assumption ] assumption  assumption ] ] 594 destruct(EQ3) >point_of_pc_of_point >EQt_stmt %] 595 whd in match sigma_next; normalize nodelta >code_block_of_block_eq >m_return_bind 596 >EQfn >m_return_bind inversion(find ????) 597 [1,3,5,7: #EQfind @⊥ lapply(find_none … EQfind EQstmt) normalize nodelta >EQpreamble 598 normalize nodelta cases post in Hregs EQpost; 599 [1,3,5,7: #Hregs * #EQ1 #EQ2 destruct(EQ1 EQ2) @('bind_inversion EQpreamble) 600 #bl' >code_block_of_block_eq whd in ⊢ (??%? → ?); #EQ destruct(EQ) >EQfn 601 >m_return_bind >EQstmt >m_return_bind >Hinit >m_return_bind normalize nodelta 602 >Hregs >m_return_bind cases pre in EQpre Hregs; 603 [1,3,6,8: [3,4: #x #y] #_ #_ whd in match (length ??); whd in ⊢ (??%? → ?); #EQ destruct 604 2,4: #fst #remaining] * 605 [1,2: #lab1 * #rest ** #EQ destruct(EQ) * #nxt' * #EQpc change with nxt' in ⊢ (??%? → ?); 606 #EQ destruct(EQ) #Hrest #Hregs whd in match (length ??); whd in ⊢ (??%? → ?); 607 #EQ destruct(EQ) whd in EQmid : (??%%); destruct(EQmid) >e0 608 lapply(seq_list_in_code_length … Hrest) >length_map #EQ >EQ 609 >nth_opt_append_r 610 [2,4: >length_append whd in match (length ? [mid1]); 611 whd in match (length ? [ ]); cases(rest) //] 612 >length_append whd in match (length ? [mid1]); whd in match (length ? [ ]); 613 cut(S (rest)  (rest + 1) = O) 614 [1,3: cases(rest) // #m normalize cases m // #m1 normalize nodelta 615 cut(m1 + 1 = S m1) [1,3: //] #EQ1 >EQ1 <minus_n_n % ] 616 #EQ1 >EQ1 normalize nodelta @eq_identifier_elim [1,3: #_ *] * #H #_ @H % 617 *: #EQ1 #EQ2 destruct(EQ1 EQ2) #EQregs #_ whd in EQmid : (??%%); destruct(EQmid) 618 >e0 normalize nodelta @eq_identifier_elim [1,3: #_ *] * #H #_ @H % 619 ] 620 *: #fst #rems #Hregs * #lab1 * #rest ** #EQ destruct(EQ) * #nxt1 * #EQmid2 621 change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) #EQrest @('bind_inversion EQpreamble) 622 #bl' >code_block_of_block_eq whd in ⊢ (??%? → ?); #EQ destruct(EQ) >EQfn 623 >m_return_bind >EQstmt >m_return_bind >Hinit >m_return_bind normalize nodelta 624 >Hregs >m_return_bind cases pre in EQpre Hregs; 625 [1,3,6,8: [3,4: #x #y] #_ #_ whd in ⊢ (??%? → ?); whd in match (length ??); 626 #EQ destruct2,4: #hd1 #tl1] * 627 [1,2: #lab1 * #rest1 ** #EQ destruct(EQ) * #nxt1 * #EQpc 628 change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) #EQrest1 #Hregs 629 whd in match (length ??); whd in ⊢ (??%? → ?); #EQ destruct(EQ) 630 *: #EQ1 #EQ2 destruct(EQ1 EQ2) #Hregs #_ 631 ] 632 whd in EQmid : (??%%); destruct(EQmid) >e0 normalize nodelta 633 [3,4: @eq_identifier_elim [1,3: #_ *] * #H #_ @H %] 634 lapply(seq_list_in_code_length … EQrest1) >length_map #EQ >EQ 635 >nth_opt_append_l [2,4: >length_append whd in match (length ? (mid1::?)); 636 whd in match (length ? (mid2::rest)); cases(rest1) //] >append_cons 637 >append_cons >nth_opt_append_l 638 [2,4: >length_append >length_append whd in match (length ? [ ? ]); 639 whd in match (length ? [ ]); cases(rest1) // ] 640 >nth_opt_append_r 641 [2,4: >length_append whd in match (length ? [ ? ]); whd in match (length ? [ ]); 642 cases(rest1) // ] 643 >length_append whd in match (length ? [ ? ]); whd in match (length ? [ ]); 644 cut(S(rest1)  (rest1+1) = 0) 645 [1,3: cases(rest1) // #m normalize cases m // #m1 normalize nodelta 646 cut(m1 + 1 = S m1) [1,3: //] #EQ1 >EQ1 <minus_n_n % ] #EQ1 >EQ1 647 normalize nodelta @eq_identifier_elim [1,3: #_ *] * #H #_ @H % 648 ] 649 *: * #lab2 * [1,4,7,10: #j_step #nxt1 2,5,8,11: #fin1 *: *] #EQfind 650 lapply(find_predicate ?????? EQfind) normalize nodelta [5,6,7,8: *] 651 cases(preamble_length ?????????) normalize nodelta [1,3,5,7: *] #n 652 inversion(nth_opt ???) normalize nodelta [1,3,5,7: #_ *] #lab1 #EQlab1 653 @eq_identifier_elim [2,4,6,8: #_ *] #EQ destruct(EQ) 654 cases(Exists_append … (nth_opt_Exists ???? EQlab1)) 655 [2,4,6,8: * [2,4,6,8: *] #EQ destruct(EQ) cases post in Hregs EQpost; 656 [1,3,5,7: #Hregs * #EQ1 #EQ2 destruct(EQ1 EQ2) #_ %] #hd1 #tl1 #Hregs * 657 #lab3 * #rest3 ** #EQ destruct(EQ) * #nxt2 * #EQt_lab1 658 change with nxt2 in ⊢ (??%? → ?); #EQ destruct(EQ) #EQrest3 659 @('bind_inversion EQpreamble) #bl' >code_block_of_block_eq 660 whd in ⊢ (??%? → ?); #EQ destruct(EQ) >EQfn >m_return_bind >EQstmt 661 >m_return_bind >Hinit >m_return_bind normalize nodelta >Hregs 662 >m_return_bind cases pre in Hregs EQpre; 663 [1,3,6,8: [3,4: #x #y] #_ #_ whd in match (length ??); whd in ⊢ (??%? → ?); 664 #EQ destruct(EQ) 2,4: #hd1 #tl1] #Hregs * 665 [1,2: #lab4 * #rest4 ** #EQ destruct(EQ) * #nxt2 * #EQpc 666 change with nxt2 in ⊢ (??%? → ?); #EQ destruct(EQ) #EQrest4 667 whd in match (length ??); whd in ⊢ (??%? → ?); #EQ destruct(EQ) #_ 668 *: #EQ1 #EQ2 destruct(EQ1 EQ2) #_ #_ 669 ] 670 whd in EQmid : (??%%); destruct(EQmid) @⊥ lapply(fresh_labs (point_of_pc p_in pc)) 671 >e0 672 [1,2: #H cases(append_All … H) #_ * #_ *** H #H #_ #_ @H 673 *: *** #H #_ #_ @H 674 ] 675 @(code_is_in_universe … (pi2 ?? fn)) whd in match code_has_label; 676 whd in match code_has_point; normalize nodelta 677 cases(fetch_stmt_ok_nxt_ok … EQfn (find_lookup ?????? EQfind)) 678 #stmt' #EQstmt' >EQstmt' @I 679 *: #Hlab2 cases post in Hregs EQpost; 680 [1,3,5,7: #Hregs * #EQ1 #EQ2 destruct(EQ1 EQ2) 681 cases(Exists_All … Hlab2 (fresh_labs lab2)) #x * #EQ destruct(EQ) ** #H 682 @⊥ @H @(code_is_in_universe … (pi2 ?? fn)) whd in match code_has_label; 683 whd in match code_has_point; normalize nodelta 684 cases(fetch_stmt_ok_nxt_ok … EQfn EQstmt) #stmt' #EQstmt' >EQstmt' @I 685 *: #hd1 #tl1 #Hregs * #lab3 * #rest3 ** #EQ destruct(EQ) * #nxt2 * 686 #EQt_lab1 change with nxt2 in ⊢ (??%? → ?); #EQ destruct(EQ) #EQrest3 687 @('bind_inversion EQpreamble) #bl' >code_block_of_block_eq 688 whd in ⊢ (??%? → ?); #EQ destruct(EQ) >EQfn >m_return_bind >EQstmt 689 >m_return_bind >Hinit >m_return_bind normalize nodelta >Hregs 690 >m_return_bind cases pre in Hregs EQpre; 691 [1,3,6,8: [3,4: #x #y] #_ #_ whd in match (length ??); whd in ⊢ (??%? → ?); 692 #EQ destruct(EQ) 693 2,4: #hd1 #tl1] 694 #Hregs * 695 [1,2: #lab4 * #rest4 ** #EQ destruct(EQ) * #nxt2 * #EQpc 696 change with nxt2 in ⊢ (??%? → ?); #EQ destruct(EQ) #EQrest4 697 whd in match (length ??); whd in ⊢ (??%? → ?); #EQ destruct(EQ) #_ 698 *: #EQ1 #EQ2 destruct(EQ1 EQ2) #_ #_ 699 ] 700 whd in EQmid : (??%%); destruct(EQmid) cases(pp_labs) #_ #H 701 lapply(H lab2 (point_of_pc p_in pc) lab1 ? ?) 702 [3,6,9,12: #EQ destruct(EQ) whd in match (stmt_at ????) in EQstmt; 703 >(find_lookup ?????? EQfind) in EQstmt; #EQ destruct(EQ) % 704 1,4,7,10: >e0 [3,4: whd in match (memb ???); @eqb_elim 705 [2,4: * #H @⊥ @H %] #_ @I] >memb_append_l2 [1,3: @I] 706 whd in match (memb ???); @if_elim [1,3: #_ %] #_ 707 whd in match (memb ???); @eqb_elim [1,3: #_ %] * #H1 @⊥ @H1 % 708 *: @Exists_memb assumption 709 ] 710 ] 711 ] 712 ] 713 qed. 714 715 716 definition make_is_relation_from_beval : (beval → beval → Prop) → 717 internal_stack → internal_stack → Prop≝ 718 λR,is1,is2. 719 match is1 with 720 [ empty_is ⇒ match is2 with [ empty_is ⇒ True  _ ⇒ False] 721  one_is b ⇒ match is2 with [ one_is b' ⇒ R b b'  _ ⇒ False ] 722  both_is b1 b2 ⇒ match is2 with [ both_is b1' b2' ⇒ R b1 b1' ∧ R b2 b2'  _ ⇒ False ] 723 ]. 724 725 lemma is_push_ok : ∀Rbeval : beval → beval → Prop. 726 ∀Ristack1 : internal_stack → internal_stack → Prop. 727 ∀Ristack2 : internal_stack → internal_stack → Prop. 728 (∀is1,is2.Ristack1 is1 is2 → make_is_relation_from_beval Rbeval is1 is2) → 729 (∀bv1,bv2.Ristack1 empty_is empty_is → Rbeval bv1 bv2 → 730 Ristack2 (one_is bv1) (one_is bv2)) → 731 (∀bv1,bv2,bv3,bv4.Rbeval bv1 bv2 → Rbeval bv3 bv4 → 732 Ristack2 (both_is bv3 bv1) (both_is bv4 bv2)) → 733 gen_preserving2 ?? gen_res_preserve … 734 Ristack1 Rbeval Ristack2 is_push is_push. 735 #Rbeval #Ristack1 #Ristack2 #H #H1 #H2 #is1 #is2 #bv1 #bv2 #H3 #H4 736 whd in match is_push; normalize nodelta cases is1 in H3; normalize nodelta 737 [2:#x3: #x #y #_ @res_preserve_error_gen] 738 cases is2 normalize nodelta 739 [1,3,5,6: [ #z #w  #z  #z #w] #H5 cases(H … H5)  #y] #H5 @m_gen_return 740 [@H2 [assumption  @(H … H5) ]  @H1 assumption] 741 qed. 742 (* 743 lemma is_push_ok : ∀R : beval → beval → Prop. 744 gen_preserving2 ?? gen_res_preserve … 745 (make_is_relation_from_beval R) R 746 (make_is_relation_from_beval R) 747 is_push is_push. 748 #R @is_push_ok_gen // #bv1 #bv2 #bv3 #bv4 #H #H1 %{H1 H} 749 qed. 750 *) 751 lemma is_pop_ok: ∀Rbeval : beval → beval → Prop. 752 ∀Ristack1 : internal_stack → internal_stack → Prop. 753 ∀Ristack2 : internal_stack → internal_stack → Prop. 754 (∀is1,is2.Ristack1 is1 is2 → make_is_relation_from_beval Rbeval is1 is2) → 755 Ristack2 empty_is empty_is → 756 (∀bv1,bv2.Rbeval bv1 bv2 → Ristack2 (one_is bv1) (one_is bv2)) → 757 gen_preserving ?? gen_res_preserve … 758 Ristack1 759 (λx,y.Rbeval (\fst x) (\fst y) ∧ 760 Ristack2 (\snd x) (\snd y)) is_pop is_pop. 761 #Rbeval #Ristack1 #Ristack2 #H #H1 #H2 #is1 #is2 whd in match is_pop; normalize nodelta 762 cases is1 normalize nodelta [#_ @res_preserve_error_gen] #x [#y] cases is2 763 [1,3,4,5: [#x #y#x] #H3 cases(H … H3)  #y  #z #w] #H3 normalize nodelta 764 @m_gen_return [ % [ @(H … H3)  assumption ]  cases(H … H3) #H4 #H5 %{H5} @(H2 … H4) 765 qed. 766 767 (* 768 lemma is_pop_ok1 : ∀R : beval → beval → Prop. 769 gen_preserving ?? gen_res_preserve … 770 (make_is_relation_from_beval R) 771 (λx,y.R (\fst x) (\fst y) ∧ 772 (make_is_relation_from_beval R) (\snd x) (\snd y)) 773 is_pop is_pop. 774 #R @is_pop_ok // 775 qed. 776 777 778 definition make_weak_state_relation ≝ 779 λp_in,p_out.λR : (beval → beval → Prop).λst1 : state p_in.λst2 : state p_out. 780 (make_is_relation_from_beval R) (istack … st1) (istack … st2). 781 *) 782 783 784 lemma push_ok : ∀p_in,p_out,Rbeval,Rstate1,Rstate2. 785 (∀is1,is2,st1,st2.istack ? st1 = is1 → istack ? st2 = is2 → Rstate1 st1 st2 → 786 make_is_relation_from_beval Rbeval is1 is2) → 787 (∀st1,st2,bv1,bv2. Rstate1 st1 st2 → Rbeval bv1 bv2 → 788 Rstate2 (set_istack p_in (one_is bv1) st1) (set_istack p_out (one_is bv2) st2)) → 789 (∀st1,st2,bv1,bv2,bv3,bv4.Rstate1 st1 st2 → Rbeval bv1 bv2 → Rbeval bv3 bv4 → 790 Rstate2 (set_istack p_in (both_is bv1 bv3) st1) (set_istack p_out (both_is bv2 bv4) st2)) → 791 gen_preserving2 ?? gen_res_preserve … Rstate1 Rbeval Rstate2 792 (push p_in) (push p_out). 793 #p_in #p_out #Rbeval #Rstate1 #Rstate2 #H #H1 #H2 #st1 #st2 #bv1 #bv2 #H3 #H4 794 whd in match push; normalize nodelta 795 @(m_gen_bind_inversion … (make_is_relation_from_beval Rbeval)) 796 [ @(is_push_ok Rbeval (make_is_relation_from_beval Rbeval)) // 797 [ #bv1 #bv2 #bv3 #bv4 #H5 #H6 whd %{H6 H5} 798  @(H … H3) % 799 ] 800  * [#x#x1 #x2] * [1,4,7:2,5,8: #y *: #y1 #y2] #H5 #H6 whd in ⊢ (% → ?); 801 [1,2,3,4,6,7,8,9: * [2: #H7 #H8]  #H7] @m_gen_return 802 [ @(H2 … H3) assumption 803  cases(istack … st1) in H5; [2,3: #z [2: #w]] whd in ⊢ (??%% → ?); 804 #EQ destruct(EQ) 805  @(H1 … H3) assumption 806 ] 807 ] 808 qed. 809 810 811 lemma pop_ok : ∀p_in,p_out,Rbeval,Rstate1,Rstate2. 812 (∀is1,is2,st1,st2.istack ? st1 = is1 → istack ? st2 = is2 → Rstate1 st1 st2 → 813 make_is_relation_from_beval Rbeval is1 is2) → 814 (∀st1,st2.Rstate1 st1 st2 → 815 Rstate2 (set_istack p_in (empty_is) st1) (set_istack p_out (empty_is) st2)) → 816 (∀st1,st2,bv1,bv2. Rstate1 st1 st2 → Rbeval bv1 bv2 → 817 Rstate2 (set_istack p_in (one_is bv1) st1) (set_istack p_out (one_is bv2) st2)) → 818 gen_preserving ?? gen_res_preserve … 819 Rstate1 820 (λx,y.Rbeval (\fst x) (\fst y) ∧ 821 Rstate2(\snd x) (\snd y)) 822 (pop p_in) (pop p_out). 823 #p_in #p_out #Rbeval #Rstate1 #Rstate2 #H #H1 #H2 #st1 #st2 #H3 824 whd in match pop; normalize nodelta 825 @(m_gen_bind_inversion … (λx,y.Rbeval (\fst x) (\fst y) ∧ 826 (make_is_relation_from_beval Rbeval (\snd x) (\snd y)))) 827 [ @(is_pop_ok Rbeval (make_is_relation_from_beval Rbeval)) // @(H … H3) % 828  * #bv1 * [#x#x1 #x2] * #bv2 * 829 [1,4,7:2,5,8: #y 830 *: #y1 #y2 [1,2: #_ #_ * #_ *] cases(istack … st1) [#z#z #w] whd in ⊢ (??%% → ?); #EQ destruct ] 831 #_ #_ * #H4 [2,3,4,6: * #_  whd in ⊢ (% → ?); #H5] @m_gen_return 832 % // [ @(H1 … H3)  @(H2 … H3) assumption] 833 qed. 834 835 lemma fetch_internal_function_no_zero : 836 ∀p,prog,stack_size,bl. 837 block_id (pi1 … bl) = 0 → 838 fetch_internal_function … (joint_globalenv p prog stack_size) bl = 839 Error ? [MSG BadFunction]. 840 #p #prg #stack_size #bl #Hbl whd in match fetch_internal_function; 841 whd in match fetch_function; normalize nodelta @eqZb_elim 842 [ >Hbl #EQ @⊥ cases(not_eq_OZ_neg one) #H @H assumption ] 843 #_ normalize nodelta cases(symbol_for_block ???) [%] #id >m_return_bind 844 cases bl in Hbl; * #id #prf #EQ destruct(EQ) 845 change with (mk_block OZ) in match (mk_block ?); 846 cut(find_funct_ptr 847 (fundef (joint_closed_internal_function p (prog_names p prg))) 848 (joint_globalenv p prg stack_size) (mk_block OZ) = None ?) [%] 849 #EQ >EQ % 850 qed. 851 852 lemma next_of_call_pc_ok : ∀P_in,P_out : sem_graph_params. 853 ∀init,prog,stack_sizes,init_regs,f_lbls,f_regs. 854 b_graph_transform_program_props P_in P_out stack_sizes 855 init prog init_regs f_lbls f_regs → 856 let trans_prog ≝ b_graph_transform_program P_in P_out init prog in 857 ∀bl :Σb.block_region b =Code.block_id bl ≠ 1 → 858 ∀f,fn. 859 fetch_internal_function … (joint_globalenv P_in prog stack_sizes) bl = 860 return 〈f,fn〉 → 861 (∀id,args,dest,lbl. 862 bind_new_P' ?? 863 (λregs1.λdata.bind_new_P' ?? 864 (λregs2.λblp. 865 ∀lbl.∃id',args',dest'.((\snd (\fst blp)) lbl) = CALL P_out ? id' args' dest') 866 (f_step … data lbl (CALL P_in ? id args dest))) 867 (init ? fn)) → 868 gen_preserving ?? gen_res_preserve ???? 869 (λpc1,pc2 : Σpc.pc_block pc = bl. 870 sigma_stored_pc P_in P_out prog stack_sizes init 871 init_regs f_lbls f_regs pc2 = pc1) 872 (λn1,n2.sigma_next P_in P_out prog stack_sizes init init_regs f_lbls f_regs bl n2 = return n1) 873 (next_of_call_pc P_in … (joint_globalenv P_in prog stack_sizes)) 874 (next_of_call_pc P_out … (joint_globalenv P_out trans_prog stack_sizes)). 875 #p_in #p_out #init #prog #stack_sizes #init_regs #f_lbls #f_regs #good #bl #Hbl 876 #f #fn #EQfn #Hcall #pc1 #pc2 #Hpc1pc2 #lbl1 #H @('bind_inversion H) H ** #f1 #fn1 * 877 [ * [#c #id #args #dest  #r #lb  #seq ] #nxt  #fin  *] 878 whd in match fetch_statement; normalize nodelta >(pi2 ?? pc1) >EQfn >m_return_bind 879 #H @('bind_inversion H) H #stmt #H lapply(opt_eq_from_res ???? H) H 880 #EQstmt whd in ⊢ (??%% → ??%% → ?); #EQ1 #EQ2 destruct(EQ1 EQ2) 881 cases(fetch_statement_sigma_stored_pc … pc1 f1 fn1 … good …) 882 [3: >(pi2 ?? pc1) assumption 883 4: whd in match fetch_statement; normalize nodelta >(pi2 ?? pc1) in ⊢ (??%?); 884 >EQfn in ⊢ (??%?); >m_return_bind in ⊢ (??%?); >EQstmt in ⊢ (??%?); % 2:] 885 #data * #Hdata normalize nodelta * #st_bl * #Hst_bl * #pc' * #EQpc' * #t_fn 886 * #nxt1 * #l1 * #l2 *** #EQt_fetch #_ #_ #nxt1rel %{nxt1} % [2: <(pi2 ?? pc1) assumption] 887 whd in match next_of_call_pc; normalize nodelta <EQpc' in Hpc1pc2; 888 #H lapply(sym_eq ??? H) H whd in match sigma_stored_pc; normalize nodelta 889 inversion(sigma_pc_opt ?????????) 890 [ #ABS @⊥ whd in match sigma_stored_pc in EQpc'; normalize nodelta in EQpc'; 891 >ABS in EQpc'; normalize nodelta #EQ <(pi2 ?? pc1) in EQfn; 892 >fetch_internal_function_no_zero [2: <EQ %] whd in ⊢ (???% → ?); #EQ1 destruct(EQ1) ] 893 #sigma_pc' #EQsigma_pc' normalize nodelta inversion(sigma_pc_opt ?????????) 894 [ #_ normalize nodelta #EQ destruct(EQ) @⊥ lapply EQt_fetch @if_elim #_ #EQf 895 cases(fetch_statement_inv … EQf) >fetch_internal_function_no_zero [1,3: #EQ destruct] 896 >(pc_block_eq p_in p_out prog stack_sizes init init_regs f_lbls f_regs) 897 [1,3: whd in match sigma_stored_pc; normalize nodelta >EQsigma_pc' % 898 *: >EQsigma_pc' % #EQ destruct 899 ] 900 ] 901 #pc3 #EQpc3 normalize nodelta #EQ destruct(EQ) <EQsigma_pc' in EQpc3; #H 902 lapply(sym_eq ??? H) H #EQp lapply(sigma_stored_pc_inj … EQp) [>EQsigma_pc' % #EQ destruct] 903 #EQ destruct(EQ) >EQt_fetch @eq_identifier_elim 904 [ #EQ1 >EQ1 in EQstmt; cases(entry_is_cost … (pi2 ?? fn1)) #nxt2 * #c #ABS >ABS #EQ1 destruct(EQ1) ] 905 #_ cases(not_emptyb ??) normalize nodelta >m_return_bind normalize nodelta 906 lapply(bind_new_bind_new_instantiates … (bind_instantiates_to_instantiate … Hst_bl) 907 (bind_new_bind_new_instantiates … (bind_instantiates_to_instantiate … Hdata) 908 (Hcall id args dest (point_of_pc p_in pc1)))) 909 #H cases(H (point_of_pc p_in pc2)) #id' * #args' * #dest' #EQ >EQ % 910 qed. 911 912 definition joint_state_relation ≝ 913 λP_in,P_out.program_counter → state P_in → state P_out → Prop. 914 915 definition joint_state_pc_relation ≝ λP_in,P_out.state_pc P_in → state_pc P_out → Prop. 916 917 record good_state_relation (P_in : sem_graph_params) 918 (P_out : sem_graph_params) (prog : joint_program P_in) 919 (stack_sizes : ident → option ℕ) 920 (init : ∀globals.joint_closed_internal_function P_in globals 921 →bound_b_graph_translate_data P_in P_out globals) 922 (init_regs : block → list register) (f_lbls : lbl_funct_type) 923 (f_regs : regs_funct_type) 924 (st_no_pc_rel : joint_state_relation P_in P_out) 925 (st_rel : joint_state_pc_relation P_in P_out) : Prop ≝ 926 { good_translation :> b_graph_transform_program_props P_in P_out stack_sizes init 927 prog init_regs f_lbls f_regs 928 ; fetch_ok_sigma_state_ok : 929 ∀st1,st2,f,fn. st_rel st1 st2 → 930 fetch_internal_function … 931 (joint_globalenv P_in prog stack_sizes) (pc_block (pc … st1)) 932 = return 〈f,fn〉 → 933 st_no_pc_rel (pc … st1) (st_no_pc … st1) (st_no_pc … st2) 934 ; fetch_ok_pc_ok : 935 ∀st1,st2,f,fn.st_rel st1 st2 → 936 fetch_internal_function … 937 (joint_globalenv P_in prog stack_sizes) (pc_block (pc … st1)) 938 = return 〈f,fn〉 → 939 pc … st1 = pc … st2 940 ; fetch_ok_sigma_last_pop_ok : 941 ∀st1,st2,f,fn.st_rel st1 st2 → 942 fetch_internal_function … 943 (joint_globalenv P_in prog stack_sizes) (pc_block (pc … st1)) 944 = return 〈f,fn〉 → 945 (last_pop … st1) = sigma_stored_pc P_in P_out prog stack_sizes init init_regs 946 f_lbls f_regs (last_pop … st2) 947 ; st_rel_def : 948 ∀st1,st2,pc,lp1,lp2,f,fn. 949 fetch_internal_function … 950 (joint_globalenv P_in prog stack_sizes) (pc_block pc) = return 〈f,fn〉 → 951 st_no_pc_rel pc st1 st2 → 952 lp1 = sigma_stored_pc P_in P_out prog stack_sizes init init_regs 953 f_lbls f_regs lp2 → 954 st_rel (mk_state_pc ? st1 pc lp1) (mk_state_pc ? st2 pc lp2) 955 ; as_label_ok_non_entry : 956 let trans_prog ≝ b_graph_transform_program P_in P_out init prog in 957 ∀st1,st2,f,fn,stmt. 958 fetch_statement … 959 (joint_globalenv P_in prog stack_sizes) (pc … st1) = return〈f,fn,stmt〉 → 960 st_rel st1 st2 → point_of_pc P_in (pc … st1) ≠ joint_if_entry … fn → 961 as_label (joint_status P_in prog stack_sizes) st1 = 962 as_label (joint_status P_out trans_prog stack_sizes) st2 963 ; pre_main_ok : 964 let trans_prog ≝ b_graph_transform_program P_in P_out init prog in 965 ∀st1,st1' : joint_abstract_status (mk_prog_params P_in prog stack_sizes) . 966 ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes). 967 block_id … (pc_block (pc … st1)) = 1 → 968 st_rel st1 st2 → 969 as_label (joint_status P_in prog stack_sizes) st1 = 970 as_label (joint_status P_out trans_prog stack_sizes) st2 ∧ 971 joint_classify … (mk_prog_params P_in prog stack_sizes) st1 = 972 joint_classify … (mk_prog_params P_out trans_prog stack_sizes) st2 ∧ 973 (eval_state P_in … (joint_globalenv P_in prog stack_sizes) 974 st1 = return st1' → 975 ∃st2'. st_rel st1' st2' ∧ 976 eval_state P_out … 977 (joint_globalenv P_out trans_prog stack_sizes) st2 = return st2') 978 ; cond_commutation : 979 let trans_prog ≝ b_graph_transform_program P_in P_out init prog in 980 ∀st1 : joint_abstract_status (mk_prog_params P_in prog stack_sizes) . 981 ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes). 982 ∀f,fn,a,ltrue,lfalse,bv,b. 983 block_id … (pc_block (pc … st1)) ≠ 1 → 984 let cond ≝ (COND P_in ? a ltrue) in 985 fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) = 986 return 〈f, fn, sequential … cond lfalse〉 → 987 acca_retrieve … P_in (st_no_pc … st1) a = return bv → 988 bool_of_beval … bv = return b → 989 st_rel st1 st2 → 990 ∀t_fn. 991 fetch_internal_function … 992 (joint_globalenv P_out trans_prog stack_sizes) (pc_block (pc … st2)) = 993 return 〈f,t_fn〉 → 994 bind_new_P' ?? 995 (λregs1.λdata.bind_new_P' ?? 996 (λregs2.λblp.(\snd blp) = [ ] ∧ 997 ∀mid. 998 stmt_at P_out … (joint_if_code ?? t_fn) mid 999 = return sequential P_out ? ((\snd (\fst blp)) mid) lfalse→ 1000 ∃st2_pre_mid_no_pc. 1001 repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f 1002 (map_eval ?? (\fst (\fst blp)) mid) (st_no_pc ? st2) 1003 = return st2_pre_mid_no_pc ∧ 1004 let new_pc ≝ if b then 1005 (pc_of_point P_in (pc_block (pc … st1)) ltrue) 1006 else 1007 (pc_of_point P_in (pc_block (pc … st1)) lfalse) in 1008 st_no_pc_rel new_pc (st_no_pc … st1) (st2_pre_mid_no_pc) ∧ 1009 ∃a'. ((\snd (\fst blp)) mid) = COND P_out ? a' ltrue ∧ 1010 ∃bv'. acca_retrieve … P_out st2_pre_mid_no_pc a' = return bv' ∧ 1011 bool_of_beval … bv' = return b 1012 ) (f_step … data (point_of_pc P_in (pc … st1)) cond) 1013 ) (init ? fn) 1014 ; seq_commutation : 1015 let trans_prog ≝ b_graph_transform_program P_in P_out init prog in 1016 ∀st1,st1' : joint_abstract_status (mk_prog_params P_in prog stack_sizes) . 1017 ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes). 1018 ∀f,fn,stmt,nxt. 1019 block_id … (pc_block (pc … st1)) ≠ 1 → 1020 let seq ≝ (step_seq P_in ? stmt) in 1021 fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) = 1022 return 〈f, fn, sequential … seq nxt〉 → 1023 eval_state P_in … (joint_globalenv P_in prog stack_sizes) 1024 st1 = return st1' → 1025 st_rel st1 st2 → 1026 ∀t_fn. 1027 fetch_internal_function … 1028 (joint_globalenv P_out trans_prog stack_sizes) (pc_block (pc … st2)) = 1029 return 〈f,t_fn〉 → 1030 bind_new_P' ?? 1031 (λregs1.λdata.bind_new_P' ?? 1032 (λregs2.λblp. 1033 ∃l : list (joint_seq P_out (globals ? (mk_prog_params P_out trans_prog stack_sizes))). 1034 blp = (ensure_step_block ?? l) ∧ 1035 ∃st2_fin_no_pc. 1036 repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f 1037 l (st_no_pc … st2)= return st2_fin_no_pc ∧ 1038 st_no_pc_rel (pc … st1') (st_no_pc … st1') st2_fin_no_pc 1039 ) (f_step … data (point_of_pc P_in (pc … st1)) seq) 1040 ) (init ? fn) 1041 ; call_is_call :∀f,fn,bl. 1042 fetch_internal_function … 1043 (joint_globalenv P_in prog stack_sizes) bl = return 〈f,fn〉 → 1044 ∀id,args,dest,lbl. 1045 bind_new_P' ?? 1046 (λregs1.λdata.bind_new_P' ?? 1047 (λregs2.λblp. 1048 ∀lbl.∃id',args',dest'.((\snd (\fst blp)) lbl) = CALL P_out ? id' args' dest') 1049 (f_step … data lbl (CALL P_in ? id args dest))) 1050 (init ? fn) 1051 ; cost_commutation : 1052 let trans_prog ≝ b_graph_transform_program P_in P_out init prog in 1053 ∀st1,st2,pc.∀f,fn,c,nxt. 1054 block_id … (pc_block pc) ≠ 1 → 1055 st_no_pc_rel pc st1 st2 → 1056 fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) pc = 1057 return 〈f, fn, sequential ?? (COST_LABEL ?? c) nxt〉 → 1058 st_no_pc_rel (pc_of_point P_in (pc_block pc) nxt) st1 st2 1059 ; return_commutation : 1060 let trans_prog ≝ b_graph_transform_program P_in P_out init prog in 1061 ∀st1 : joint_abstract_status (mk_prog_params P_in prog stack_sizes) . 1062 ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes). 1063 ∀f,fn. 1064 block_id … (pc_block (pc … st1)) ≠ 1 → 1065 fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) = 1066 return 〈f, fn, final P_in ? (RETURN …)〉 → 1067 ∀n. stack_sizes f = return n → 1068 let curr_ret ≝ joint_if_result … fn in 1069 ∀st_pop,pc_pop. 1070 pop_frame ?? P_in ? (joint_globalenv P_in prog stack_sizes) f curr_ret 1071 (st_no_pc … st1) = return 〈st_pop,pc_pop〉 → 1072 ∀nxt.∀f1,fn1,id,args,dest. 1073 fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) pc_pop = 1074 return 〈f1,fn1,sequential P_in … (CALL P_in ? id args dest) nxt〉 → 1075 st_rel st1 st2 → 1076 ∀t_fn. 1077 fetch_internal_function … 1078 (joint_globalenv P_out trans_prog stack_sizes) (pc_block (pc … st2)) = 1079 return 〈f,t_fn〉 → 1080 bind_new_P' ?? 1081 (λregs1.λdata. 1082 bind_new_P' ?? 1083 (λregs2.λblp. 1084 \snd blp = (RETURN …) ∧ 1085 ∃st_fin. repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f 1086 (\fst blp) (st_no_pc … st2)= return st_fin ∧ 1087 ∃t_st_pop,t_pc_pop. 1088 pop_frame ?? P_out ? (joint_globalenv P_out trans_prog stack_sizes) f 1089 (joint_if_result … t_fn) st_fin = return 〈t_st_pop,t_pc_pop〉 ∧ 1090 sigma_stored_pc P_in P_out prog stack_sizes init init_regs f_lbls f_regs 1091 t_pc_pop = pc_pop ∧ 1092 if eqZb (block_id (pc_block pc_pop)) (1) then 1093 st_no_pc_rel (pc_of_point P_in (pc_block pc_pop) nxt) 1094 (decrement_stack_usage ? n st_pop) (decrement_stack_usage ? n t_st_pop) (*pre_main*) 1095 else 1096 bind_new_P' ?? 1097 (λregs4.λdata1. 1098 bind_new_P' ?? 1099 (λregs3.λblp1. 1100 ∃st2'. repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f1 1101 (\snd blp1) (decrement_stack_usage ? n t_st_pop) = return st2' ∧ 1102 st_no_pc_rel (pc_of_point P_in (pc_block pc_pop) nxt) 1103 (decrement_stack_usage ? n st_pop) st2' 1104 ) (f_step … data1 (point_of_pc P_in pc_pop) (CALL P_in ? id args dest)) 1105 ) (init ? fn1) 1106 ) (f_fin … data (point_of_pc P_in (pc … st1)) (RETURN …)) 1107 ) (init ? fn) 1108 ; call_commutation : 1109 let trans_prog ≝ b_graph_transform_program P_in P_out init prog in 1110 ∀st1 : joint_abstract_status (mk_prog_params P_in prog stack_sizes) . 1111 ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes). 1112 ∀f,fn,id,arg,dest,nxt. 1113 block_id … (pc_block (pc … st1)) ≠ 1 → 1114 fetch_statement P_in … (joint_globalenv P_in prog stack_sizes) (pc … st1) = 1115 return 〈f, fn, sequential P_in ? (CALL P_in ? id arg dest) nxt〉 → 1116 ∀bl. 1117 block_of_call P_in … (joint_globalenv P_in prog stack_sizes) id (st_no_pc … st1) 1118 = return bl → 1119 ∀f1,fn1. 1120 fetch_internal_function … 1121 (joint_globalenv P_in prog stack_sizes) bl = return 〈f1,fn1〉 → 1122 ∀st1_pre. 1123 save_frame … P_in (kind_of_call P_in id) dest st1 = return st1_pre → 1124 ∀n.stack_sizes f1 = return n → 1125 ∀st1'. 1126 setup_call ?? P_in n (joint_if_params … fn1) arg st1_pre = return st1' → 1127 st_rel st1 st2 → 1128 ∀t_fn. 1129 fetch_internal_function … 1130 (joint_globalenv P_out trans_prog stack_sizes) (pc_block (pc … st2)) = 1131 return 〈f,t_fn〉 → 1132 ∀t_fn1. 1133 fetch_internal_function … (joint_globalenv P_out trans_prog stack_sizes) bl = 1134 return 〈f1,t_fn1〉 → 1135 bind_new_P' ?? 1136 (λregs1.λdata. 1137 bind_new_P' ?? 1138 (λregs2.λblp. 1139 ∀mid,id',arg',dest',nxt1. 1140 stmt_at P_out … (joint_if_code ?? t_fn) mid 1141 = return sequential P_out ? ((\snd (\fst blp)) mid) nxt1→ 1142 ((\snd (\fst blp)) mid) = (CALL P_out ? id' arg' dest') → 1143 ∃st2_pre_call. 1144 repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f 1145 (map_eval ?? (\fst (\fst blp)) mid) (st_no_pc ? st2) = return st2_pre_call ∧ 1146 block_of_call P_out … (joint_globalenv P_out trans_prog stack_sizes) id' 1147 st2_pre_call = return bl ∧ 1148 ∃st2_pre. 1149 save_frame … P_out (kind_of_call P_out id') dest' 1150 (mk_state_pc ? st2_pre_call (pc_of_point P_out (pc_block(pc … st2)) mid) 1151 (last_pop … st2)) = return st2_pre ∧ 1152 ∃st2_after_call. 1153 setup_call ?? P_out n (joint_if_params … t_fn1) arg' st2_pre 1154 = return st2_after_call ∧ 1155 bind_new_P' ?? 1156 (λregs11.λdata1. 1157 ∃st2'. 1158 repeat_eval_seq_no_pc ? (mk_prog_params P_out trans_prog stack_sizes) f1 1159 (added_prologue … data1) (increment_stack_usage P_out n st2_after_call) = 1160 return st2' ∧ 1161 st_no_pc_rel (pc_of_point P_in bl (joint_if_entry … fn1)) 1162 (increment_stack_usage P_in n st1') st2' 1163 1164 ) (init ? fn1) 1165 ) 1166 (f_step … data (point_of_pc P_in (pc … st1)) (CALL P_in ? id arg dest)) 1167 ) (init ? fn) 1168 }. 1169 1170 definition JointStatusSimulation : 1171 ∀p_in,p_out : sem_graph_params. 1172 ∀ prog.∀stack_sizes. 1173 ∀ f_lbls, f_regs. ∀init_regs.∀init.∀st_no_pc_rel,st_rel. 1174 good_state_relation p_in p_out prog stack_sizes init init_regs f_lbls f_regs 1175 st_no_pc_rel st_rel → 1176 let trans_prog ≝ b_graph_transform_program p_in p_out init prog in 1177 status_rel (joint_abstract_status (mk_prog_params p_in prog stack_sizes)) 1178 (joint_abstract_status (mk_prog_params p_out trans_prog stack_sizes)) ≝ 1179 λp_in,p_out,prog,stack_sizes,f_lbls,f_regs,init_regs,init,st_no_pc_rel,st_rel,good. 1180 mk_status_rel ?? 1181 (* sem_rel ≝ *) (λs1 : (joint_abstract_status (mk_prog_params p_in ??)). 1182 λs2 : (joint_abstract_status (mk_prog_params p_out ??)).st_rel s1 s2) 1183 (* call_rel ≝ *) 1184 (λs1:Σs: (joint_abstract_status (mk_prog_params p_in ??)).as_classifier ? s cl_call 1185 .λs2:Σs:(joint_abstract_status (mk_prog_params p_out ??)).as_classifier ? s cl_call 1186 .pc ? s1 = 1187 sigma_stored_pc p_in p_out prog stack_sizes init init_regs f_lbls f_regs (pc ? s2)). 1188 1189 (* 1190 lemma fetch_stmt_ok_succs_ok : ∀p : sem_graph_params. 1191 ∀prog : joint_program p.∀stack_size,f,fn,stmt,pc,pc',lbl. 1192 In ? (stmt_labels p ? stmt) lbl→ 1193 fetch_statement p … (joint_globalenv p prog stack_size) pc = return 〈f,fn,stmt〉 → 1194 pc' = pc_of_point p (pc_block pc) lbl → 1195 ∃stmt'.fetch_statement p … (joint_globalenv p prog stack_size) pc' = return 〈f,fn,stmt'〉. 1196 #p #prog #stack_size #f #fn #stmt #pc #pc' #lbl #Hlbl #EQfetch 1197 cases(fetch_statement_inv … EQfetch) #EQfn normalize nodelta #EQstmt 1198 #EQ destruct(EQ) lapply(code_is_closed … (pi2 ?? fn) … EQstmt) * 1199 cases(decidable_In ? (stmt_explicit_labels … stmt) lbl ?) 1200 [3: * cases lbl #x #y cases(decidable_eq_pos … x y) 1201 [#EQ destruct % %  * #H %2 % #H1 @H destruct %] 1202  whd in ⊢ (% → ?); #H1 #H2 cases(Exists_All … H1 H2) #lbl1 * #EQ destruct 1203 whd in match code_has_label; whd in match code_has_point; normalize nodelta 1204 inversion(stmt_at ????) [#_ *] #stmt' #EQstmt' #_ #_ %{stmt'} 1205 whd in match fetch_statement; normalize nodelta >EQfn >m_return_bind 1206 >point_of_pc_of_point >EQstmt' % 1207  #H lapply(In_all ??? H) H cases(Exists_append … Hlbl) 1208 [ cases stmt [ #step #nxt  #fin  *] whd in match stmt_implicit_label; 1209 normalize nodelta [2: *] * [2: *] #EQ destruct(EQ) #_ #_ 1210 whd in match stmt_forall_succ; whd in match code_has_point; normalize nodelta 1211 inversion(stmt_at ????) [#_ *] #stmt' #EQstmt' #_ %{stmt'} 1212 whd in match fetch_statement; normalize nodelta >EQfn >m_return_bind 1213 >point_of_pc_of_point >EQstmt' % 1214  #H1 #H2 cases(Exists_All … H1 H2) #x * #EQ destruct * #H @⊥ @H % 1215 ] 1216 ] 1217 qed. 1218 *) 1219 15 include "joint/StatusSimulationUtils.ma". 1220 16 1221 17 lemma fetch_stmt_ok_sigma_state_ok : ∀ P_in , P_out: sem_graph_params. … … 1274 70 qed. 1275 71 1276 (* 1277 lemma fetch_stmt_ok_st_rel_def : ∀ P_in , P_out: sem_graph_params. 72 lemma as_label_ok_non_entry : ∀ P_in , P_out: sem_graph_params. 1278 73 ∀prog : joint_program P_in. 1279 74 ∀stack_sizes. 1280 75 ∀ f_lbls,f_regs.∀f_bl_r.∀init. 1281 ∀good : b_graph_transform_program_props P_in P_out init prog f_bl_r f_lbls f_regs.1282 76 ∀st_no_pc_rel,st_rel. 1283 ∀f,fn,stmt,st1,st2. 1284 good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs good 77 let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in 78 let trans_prog ≝ b_graph_transform_program P_in P_out init prog in 79 let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in 80 good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs 1285 81 st_no_pc_rel st_rel → 1286 st_no_pc_rel (st_no_pc … st1) (st_no_pc … st2) → (pc … st1) = (pc … st2) → 1287 (last_pop … st1) = sigma_stored_pc P_in P_out prog f_lbls (last_pop … st2) → 1288 fetch_statement P_in … (ev_genv … (mk_prog_params P_in prog stack_sizes)) (pc … st1) = 1289 return 〈f,fn,stmt〉 → st_rel st1 st2. 1290 #P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_bl_r #init #good #st_no_pc_rel 1291 #st_rel #f #fn #stmt * #st1 #pc1 #lp1 * #st2 #pc2 #lp2 #goodR #Hno_pc #EQ destruct(EQ) 1292 #EQlp1 #EQfetch cases(fetch_statement_inv … EQfetch) #EQfn #EQstmt 1293 @(st_rel_def … goodR … EQfn) assumption 82 ∀st1,st2,f,fn,stmt. 83 fetch_statement … 84 (joint_globalenv P_in prog stack_sizes) (pc … st1) = return〈f,fn,stmt〉 → 85 block_id … (pc_block (pc … st1)) ≠ 1 → 86 st_rel st1 st2 → point_of_pc P_in (pc … st1) ≠ joint_if_entry … fn → 87 as_label (joint_status P_in prog stack_sizes) st1 = 88 as_label (joint_status P_out trans_prog stack_sizes) st2. 89 #p_in #p_out #prog #stack_size #f_lbls #f_regs #init_regs #init #st_no_pc_rel #st_rel 90 #good #st1 #st2 #f #fn #stmt #EQfetch * #Hbl #Rst1st2 * #Hentry 91 whd in ⊢ (??%%); >EQfetch normalize nodelta 92 lapply(b_graph_transform_program_fetch_statement … good (pc … st1) f fn ?) 93 [2: @eqZb_elim [1: #ABS @⊥ >ABS in Hbl; #H @H %] #_ normalize nodelta 94 #H cases(H EQfetch) H *:] #data * #t_fn ** #EQt_fn #Hdata #H 95 whd in match fetch_statement; normalize nodelta 96 >(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in EQt_fn; #EQt_fn >EQt_fn 97 >m_return_bind cases stmt in EQfetch H; 98 [ * [ #c  #id #args #dest  #r #lb  #seq] #nxt  * [ #lb   #has #id #args ]  * ] 99 #EQfetch normalize nodelta * #bl 100 [1,2,3,4: @eq_identifier_elim 101 [1,3,5,7: #EQ @⊥ @Hentry >EQ % 102 *: #_ cut(∀b.andb b false = false) [1,3,5,7: * %] #EQ >EQ EQ normalize nodelta 103 ] 104 ] 105 * 106 [ >(f_step_on_cost … data) whd in ⊢ (% → ?); cases(f_regs ??) [2: # x #y *] 107 normalize nodelta #EQ destruct(EQ) * #l1 * #mid1 * #mid2 * #l2 *** #EQmid1 108 whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2) * #nxt1 * #EQcost 109 change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) * #EQ1 #EQ2 destruct(EQ1 EQ2) 110 >(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in EQcost; #EQcost >EQcost % 111 ] 112 #Hregs * 113 [1,2,3: * [2,4,6: #hd #tl * #mid1 * #mid2 * #l2 *** #EQmid1 cases(\fst (\fst bl)) 114 [1,3,5: whd in ⊢ (% → ?); * #EQ destruct(EQ)] #hd1 #tl1 whd in ⊢ (% → ?); 115 * #mid3 * #rest ** #EQ destruct(EQ) * #nxt1 * #EQ 116 change with nxt1 in ⊢ (??%? → ?); #EQ1 destruct(EQ1) #_ #_ #_ 117 >(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in EQ; #EQ >EQ % ] 118 * #mid1 * #mid2 * #l2 *** #_ cases bl in Hregs; ** 119 [2,4,6: #x #y #z #w #_ whd in ⊢ (% → ?); * #a * #b ** #EQ destruct(EQ)] 120 #instr #post #Hregs whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2) * 121 #nxt1 * #EQ change with nxt1 in ⊢ (??%? → ?); #EQ1 destruct(EQ1) 122 >(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in EQ; #EQ #_ >EQ 123 inversion(instr ?) 124 [2,3,4,6,7,8,10,11,12: [1,4,7: #id1 #arg1 #dest1 2,5,8: #r1 #lb1 *: #seq] 125 #EQ1 >EQ1 %] #c1 #EQc1 126 lapply(bind_new_bind_new_instantiates … Hregs (cost_in_f_step … data … c1) … 127 (jmeq_to_eq ??? EQc1)) #EQ destruct(EQ) 128 *: * [2,4,6: #hd #tl * #mid ** #_ cases (\fst bl) [1,3,5: * #EQ destruct(EQ)] 129 #hd1 #tl1 whd in ⊢ (% → ?); * #mid1 * #rest ** #EQ destruct(EQ) whd in ⊢ (% → ?); 130 * #nxt1 * #EQ change with nxt1 in ⊢ (??%? → ?); #EQ1 destruct(EQ1) #_ #_ 131 >(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in EQ; #EQ >EQ % 132 *: * #mid ** #_ cases bl in Hregs; * [2,4,6: #x #y #z #_ * #w * #a ** #EQ destruct] 133 #instr #_ * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in ⊢ (% → ?); 134 >(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) #EQ >EQ % 135 ] 136 ] 137 qed. 138 139 140 lemma eval_goto_ok : ∀ P_in , P_out: sem_graph_params. 141 ∀prog : joint_program P_in. 142 ∀stack_sizes. 143 ∀ f_lbls,f_regs.∀f_bl_r.∀init. 144 ∀st_no_pc_rel,st_rel. 145 let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in 146 let trans_prog ≝ b_graph_transform_program P_in P_out init prog in 147 let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in 148 good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs 149 st_no_pc_rel st_rel → 150 ∀st1,st1' : joint_abstract_status prog_pars_in. 151 ∀st2 : joint_abstract_status prog_pars_out. 152 ∀f : ident. 153 ∀fn : joint_closed_internal_function P_in ?. 154 ∀lbl. 155 block_id … (pc_block (pc … st1)) ≠ 1 → 156 st_rel st1 st2 → 157 let goto ≝ (GOTO P_in lbl) in 158 fetch_statement P_in ? 159 (joint_globalenv P_in prog stack_sizes) (pc … st1) = 160 return 〈f, fn, final … goto〉 → 161 eval_state P_in … 162 (joint_globalenv P_in prog stack_sizes) st1 = return st1' → 163 ∃ st2'. st_rel st1' st2' ∧ 164 ∃taf : trace_any_any_free (joint_abstract_status prog_pars_out) st2 st2'. 165 bool_to_Prop (taaf_non_empty … taf) ∧ 166 as_label (joint_abstract_status prog_pars_in) st1' = 167 as_label (joint_abstract_status prog_pars_out) st2'. 168 #p_in #p_out #prog #stack_size #f_lbls #f_regs #init_regs #init #st_no_pc_rel 169 #st_rel #good #st1 #st1' #st2 #f #fn #lbl * #Hbl #Rst1st2 #EQfetch 170 whd in match eval_state; normalize nodelta >EQfetch >m_return_bind 171 whd in match eval_statement_no_pc; normalize nodelta >m_return_bind 172 whd in match eval_statement_advance; normalize nodelta whd in match goto; 173 normalize nodelta >pc_of_label_eq 174 [2: @(proj1 … (fetch_statement_inv … EQfetch)) *: ] 175 >m_return_bind whd in match set_no_pc; 176 whd in match set_pc; normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct(EQ) 177 lapply(b_graph_transform_program_fetch_statement … good (pc … st1) f fn ?) 178 [2,4: @eqZb_elim [1,3: #ABS @⊥ >ABS in Hbl; #H @H %] #_ normalize nodelta 179 #H cases(H EQfetch) H *:] 180 #data * #t_fn ** #EQt_fn #Hdata normalize nodelta ** #pre #instr * #Hregs 181 * #l1 * #mid ** #EQmid #EQl1 whd in ⊢ (% → ?); #EQfin 182 cases(bind_new_bind_new_instantiates' … Hregs 183 (bind_new_bind_new_instantiates' … Hdata (goto_commutation … good … 184 EQfetch Rst1st2 …))) 185 [2: % assumption 186 4: <(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in ⊢ (??%?); assumption 187 3: 188 ] 189 #st2_fin ** #EQst2_fin #EQ destruct(EQ) #Hfin_rel 190 %{(mk_state_pc ? st2_fin (pc_of_point p_out (pc_block (pc … st2)) lbl) 191 (last_pop … st2))} 192 cut(? : Prop) 193 [3: #Rst1st2' %{Rst1st2'} 194  195  <(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) @(st_rel_def … good) 196 [3: @(proj1 … (fetch_statement_inv … EQfetch)) 1,2: 197 5: @(fetch_stmt_ok_sigma_last_pop_ok … good … Rst1st2 EQfetch) 198  assumption 199 ] 200 ] 201 >(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in EQl1; #EQl1 202 lapply(taaf_to_taa … (produce_trace_any_any_free … st2 … … EQl1 … EQst2_fin) ?) 203 [ @if_elim #_ [2: @I] % whd in ⊢ (% → ?); * #H @H H whd in ⊢ (??%?); 204 whd in match (as_pc_of ??); whd in match fetch_statement; normalize nodelta 205 <(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) >EQt_fn >m_return_bind 206 whd in match point_of_pc; normalize nodelta >point_of_offset_of_point 207 >EQfin % 208  <(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) >EQt_fn % 209 ] 210 #taa %{(taaf_step … taa …)} 211 [3: %{I} 212 *: whd [ whd in ⊢ (??%?);  whd in match eval_state;] whd in match fetch_statement; 213 normalize nodelta <(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) >EQt_fn 214 >m_return_bind >point_of_pc_of_point >EQfin [%] >m_return_bind 215 whd in match eval_statement_no_pc; normalize nodelta >m_return_bind 216 whd in match eval_statement_advance; whd in match goto; normalize nodelta 217 >pc_of_label_eq 218 [2: whd in match (pc_block ?); >EQt_fn in ⊢ (??%?); % 3:] % 219 ] 220 cases(fetch_stmt_ok_succ_ok … lbl … EQfetch) [4: %3: % % *:] 221 #stmt' #EQstmt' 222 @(as_label_ok_non_entry … good) 223 [4: <(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in ⊢ (??%?); @EQstmt' 224 1,2,3: 225  <(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) % assumption 226  <(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in ⊢ (?%?); assumption 227  <(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) 228 cases(entry_unused ??? (pi2 ?? fn) ?? (proj2 ?? (fetch_statement_inv … EQfetch))) 229 * whd in match (point_of_label ????); * #H #_ #_ % >point_of_pc_of_point #EQ destruct(EQ) 230 @H % 231 ] 1294 232 qed. 1295 *) 1296 1297 (* 1298 (*CSC: Isn't this already proved somewhere else??? *) 1299 lemma point_of_pc_pc_of_point: 1300 ∀P_in: sem_graph_params.∀l,st. 1301 point_of_pc P_in 1302 (pc_of_point (mk_sem_graph_params (sgp_pars P_in) (sgp_sup P_in)) 1303 (pc_block (pc P_in st)) l) = l. 1304 #P * // 1305 qed.*) 1306 1307 1308 lemma general_eval_cond_ok : ∀ P_in , P_out: sem_graph_params. 233 234 lemma eval_goto_premain_ok : ∀ P_in , P_out: sem_graph_params. 235 ∀prog : joint_program P_in. 236 ∀stack_sizes. 237 ∀ f_lbls,f_regs.∀f_bl_r.∀init. 238 ∀st_no_pc_rel,st_rel. 239 let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in 240 let trans_prog ≝ b_graph_transform_program P_in P_out init prog in 241 let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in 242 good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs 243 st_no_pc_rel st_rel → 244 ∀st1,st1' : joint_abstract_status prog_pars_in. 245 ∀st2 : joint_abstract_status prog_pars_out. 246 ∀f : ident. 247 ∀fn : joint_closed_internal_function P_in ?. 248 ∀lbl. 249 block_id … (pc_block (pc … st1)) = 1 → 250 st_rel st1 st2 → 251 let goto ≝ (GOTO P_in lbl) in 252 fetch_statement P_in ? 253 (joint_globalenv P_in prog stack_sizes) (pc … st1) = 254 return 〈f, fn, final … goto〉 → 255 eval_state P_in … 256 (joint_globalenv P_in prog stack_sizes) st1 = return st1' → 257 ∃ st2'. st_rel st1' st2' ∧ 258 ∃taf : trace_any_any_free (joint_abstract_status prog_pars_out) st2 st2'. 259 bool_to_Prop (taaf_non_empty … taf) ∧ 260 as_label (joint_abstract_status prog_pars_in) st1' = 261 as_label (joint_abstract_status prog_pars_out) st2'. 262 #p_in #p_out #prog #stack_sizes #f_lbls #f_regs #init_regs #init #st_no_pc_rel 263 #st_rel #good #st1 #st1' #st2 #f #fn #lbl #EQbl #Rst1st2 #EQfetch #EQeval 264 cases(pre_main_ok … good … EQbl EQeval Rst1st2) #Hclass * #st2' ** #Rst1st2' 265 #EQst2' #Hlab %{st2'} % [assumption] %{(taaf_step … (taa_base …)…)} 266 [ whd change with (joint_classify ???) in ⊢ (??%?); <Hclass whd in match joint_classify; 267 normalize nodelta >EQfetch % 268  assumption ] %{I} assumption 269 qed. 270 271 272 lemma eval_tailcall_ok : ∀ P_in , P_out: sem_graph_params. 273 ∀prog : joint_program P_in. 274 ∀stack_sizes. 275 ∀ f_lbls,f_regs.∀f_bl_r.∀init. 276 ∀st_no_pc_rel,st_rel. 277 let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in 278 let trans_prog ≝ b_graph_transform_program P_in P_out init prog in 279 let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in 280 good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs 281 st_no_pc_rel st_rel → 282 ∀st1,st1' : joint_abstract_status prog_pars_in. 283 ∀st2 : joint_abstract_status prog_pars_out. 284 ∀f : ident. 285 ∀fn : joint_closed_internal_function P_in ?. 286 ∀has_tail,id,arg. 287 block_id … (pc_block (pc … st1)) ≠ 1 → 288 st_rel st1 st2 → 289 fetch_statement P_in ? 290 (joint_globalenv P_in prog stack_sizes) (pc … st1) = 291 return 〈f, fn, final … (TAILCALL P_in has_tail id arg)〉 → 292 eval_state P_in … 293 (joint_globalenv P_in prog stack_sizes) st1 = return st1' → 294 ∃is_tail,st2_pre_call,t_is_tail. 295 as_tailcall_ident ? («st2_pre_call,t_is_tail») = as_tailcall_ident ? («st1, is_tail») ∧ 296 ∃st2_after_call,st2' : joint_abstract_status prog_pars_out. 297 ∃taa2 : trace_any_any … st2 st2_pre_call. 298 ∃taa2' : trace_any_any … st2_after_call st2'. 299 eval_state P_out … (joint_globalenv P_out trans_prog stack_sizes) 300 st2_pre_call = return st2_after_call ∧ 301 st_rel st1' st2' ∧ 302 as_label (joint_abstract_status prog_pars_in) st1' = 303 as_label (joint_abstract_status prog_pars_out) st2_after_call. 304 #p_in #p_out #prog #stack_size #f_lbls #f_regs #init_regs #init #st_no_pc_rel #st_rel 305 #good #st1 #st1' #st2 #f #fn #has_tail #id #arg * #Hbl #Rst1st2 #EQfetch 306 whd in match eval_state in ⊢ (% → ?); normalize nodelta >EQfetch >m_return_bind 307 whd in match eval_statement_no_pc; normalize nodelta >m_return_bind 308 whd in match eval_statement_advance; whd in match eval_tailcall; normalize nodelta 309 >set_no_pc_eta #H @('bind_inversion H) H #bl #EQbl lapply(err_eq_from_io ????? EQbl) 310 EQbl #EQbl #H @('bind_inversion H) H 311 * #id1 * #fn1 #H lapply(err_eq_from_io ????? H) H #EQfn1 normalize nodelta 312 [2: #H @('bind_inversion H) H #x whd in match eval_external_call; normalize nodelta 313 #H @('bind_inversion H) H #y #_ #H @('bind_inversion H) H #z #_ 314 #H @('bind_inversion H) H #w whd in ⊢ (??%%→ ?); #ABS destruct(ABS) ] 315 whd in match (stack_sizes ????); #H lapply(err_eq_from_io ????? H) H 316 #H @('bind_inversion H) H #ssize_f #H lapply(opt_eq_from_res ???? H) H #EQssize_f 317 #H @('bind_inversion H) H #st1_fin whd in match eval_internal_call; 318 normalize nodelta whd in match (stack_sizes ????); #H @('bind_inversion H) H 319 #ssize_f1 #H lapply(opt_eq_from_res ???? H) H #EQssize_f1 #H @('bind_inversion H) H 320 #st1_setup #EQst1_setup whd in ⊢ (??%% → ??%% → ?); #EQ1 #EQ2 destruct(EQ1 EQ2) 321 % [@hide_prf whd in ⊢ (??%?); >EQfetch %] 322 lapply(b_graph_transform_program_fetch_statement … good (pc … st1) f fn ?) 323 [2,4: @eqZb_elim [1,3: #ABS @⊥ >ABS in Hbl; #H @H %] #_ normalize nodelta 324 #H cases(H EQfetch) H *:] 325 #data * #t_fn ** #EQt_fn #Hdata normalize nodelta ** #pre #instr * #Hregs * 326 #l1 * #mid ** #EQmid #EQpre whd in ⊢ (% → ?); #EQmid 327 cut(? : Prop) 328 [3: #EQint_fn1 329 lapply(b_graph_transform_program_fetch_internal_function … good bl id1 fn1) 330 @eqZb_elim [ #ABS cases(block_of_call_no_minus_one … EQbl) >ABS #H @⊥ @H % ] 331 #_ normalize nodelta 332 #H cases(H EQint_fn1) H #data1 * #t_fn1 ** #EQt_fn1 #Hregs1 #good1 333 cases(bind_new_bind_new_instantiates' … Hregs 334 (bind_new_bind_new_instantiates' ?????? Hdata 335 (tailcall_commutation ?????????? good ???????? EQfetch ? EQbl … EQint_fn1 … 336 EQssize_f … EQssize_f1 … EQst1_setup … Rst1st2 … EQt_fn1))) [2: % assumption] 337 #has_tail' * #id' * #arg' * #EQ destruct(EQ) * #st2_pre ** #EQst2_pre #EQt_bl 338 * #st2_after * #EQst2_after #H cases(bind_new_bind_new_instantiates' … Hregs1 H) 339 H #st2' * #EQst2' #fin_sem_rel 340 2: whd in match fetch_internal_function; normalize nodelta >EQfn1 % 341  342 ] 343 %{(mk_state_pc ? st2_pre (pc_of_point p_out (pc_block … (pc … st2)) mid) (last_pop … st2))} 344 % 345 [ @hide_prf whd in ⊢ (??%?); whd in match fetch_statement; normalize nodelta 346 <(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) >EQt_fn >m_return_bind 347 >point_of_pc_of_point >EQmid % ] 348 % 349 [ whd in ⊢ (??%%); >EQfetch in ⊢ (???(match % with [_ ⇒ ?  _ ⇒ ?])); 350 whd in match fetch_statement; normalize nodelta 351 <(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in 352 ⊢ (??(match % with [_ ⇒ ?  _ ⇒ ?])?); 353 >EQt_fn in ⊢ (??(match % with [_ ⇒ ?  _ ⇒ ?])?); 354 >m_return_bind in ⊢ (??(match % with [_ ⇒ ?  _ ⇒ ?])?); 355 >point_of_pc_of_point in ⊢ (??(match % with [_ ⇒ ?  _ ⇒ ?])?); 356 >EQmid in ⊢ (??(match % with [_ ⇒ ?  _ ⇒ ?])?); normalize nodelta 357 >EQbl >EQt_bl >m_return_bind >m_return_bind >EQt_fn1 >EQint_fn1 % 358 ] 359 %{(mk_state_pc ? (increment_stack_usage p_out ssize_f1 st2_after) 360 (pc_of_point p_out bl (joint_if_entry … t_fn1)) (last_pop … st2))} 361 %{(mk_state_pc ? st2' (pc_of_point p_out bl (joint_if_entry … fn1)) (last_pop … st2))} 362 >(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in EQt_fn; #EQt_fn 363 >(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in EQpre; #EQpre 364 %{(taaf_to_taa … (produce_trace_any_any_free … st2 … EQt_fn … EQpre EQst2_pre) …)} 365 [ @if_elim #_ [2: @I] % whd in ⊢ (% → ?); * #H @H H whd in ⊢ (??%?); 366 whd in match fetch_statement; normalize nodelta >EQt_fn >m_return_bind 367 >point_of_pc_of_point >EQmid % ] 368 cases good1 good1 #_ #_ #_ #_ #_ #_ #_ #_ #_ cases(entry_is_cost … (pi2 ?? fn1)) 369 #nxt1 * #c #EQin #H lapply(H … EQin) H normalize nodelta >(f_step_on_cost … data1) 370 * #st_bl @eq_identifier_elim [2: * #H @⊥ @H % #_ ] #_ 371 cases(added_prologue … data1) in EQst2'; 372 [ whd in ⊢ (??%% → ?); #EQ destruct(EQ) normalize nodelta * whd in ⊢ (% → ?); 373 inversion(f_regs ??) normalize nodelta [2: #x #y #_ #_ *] #EQregs #EQ destruct(EQ) 374 * #l1 * #mid1 * #mid2 * #l2 *** #EQmid1 * #EQ1 #EQ2 destruct(EQ1 EQ2) * 375 #nxt2 * #EQt_cost change with nxt2 in ⊢ (??%? → ?); #EQ destruct(EQ) * 376 #EQ1 #EQ2 destruct(EQ1 EQ2) #EQentry >EQentry %{(taa_base …)} 377  #hd #tl #EQst2' * normalize nodelta whd in ⊢ (% → ?); inversion(f_regs ??) 378 [2: #x #y #_ #_ *] #EQregs normalize nodelta #EQ destruct(EQ) * #l1 * #mid1 * #mid2 379 * #l2 *** #EQmid1 whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in ⊢ (% → ?); 380 * #nxt2 * #EQnop change with nxt2 in ⊢ (??%? → ?); #EQ destruct(EQ) whd in ⊢ (% → ?); 381 * #EQ1 #EQ2 destruct(EQ1 EQ2) * #star * #_ whd in ⊢ (% → ?); * #l3 * #mid3 * #mid4 382 * #l4 *** #_ * #EQ1 #EQ2 destruct(EQ1 EQ2) * #nxt2 * #EQt_cost 383 change with nxt2 in ⊢ (??%? → ?); #EQ destruct(EQ) #EQl4 384 letin trans_prog ≝ (b_graph_transform_program ????) 385 lapply(taaf_to_taa … 386 (produce_trace_any_any_free … (mk_prog_params p_out trans_prog stack_size) 387 (mk_state_pc ? (increment_stack_usage p_out ssize_f1 st2_after) 388 (pc_of_point p_out bl mid4) (last_pop … st2)) … EQt_fn1 … EQst2') ?) 389 [4: >point_of_pc_of_point in ⊢ (????%???); assumption 390  @if_elim #_ [2: @I] % * #H @H H whd in ⊢ (??%?); whd in match fetch_statement; 391 normalize nodelta >EQt_fn1 >m_return_bind >point_of_pc_of_point >EQnop % 392 *:] 393 #taa %{(taa_step … taa)} 394 [ % * #H @H whd in ⊢ (??%?); whd in match fetch_statement; normalize nodelta 395 >EQt_fn1 >m_return_bind >point_of_pc_of_point cases EQl4 #mid5 * #rest ** 396 #EQ destruct(EQ) * #nxt3 * #EQ #_ #_ >EQ % 397 2,3: whd [ whd in ⊢ (??%?);  whd in match eval_state; ] 398 whd in match fetch_statement; normalize nodelta >EQt_fn1 399 >m_return_bind >point_of_pc_of_point >EQt_cost [2: %] >m_return_bind % 400 ] 401 ] 402 % 403 [2,4: whd in ⊢ (??%%); whd in match (as_pc_of ??); whd in match (as_pc_of ??); 404 whd in match fetch_statement; normalize nodelta >EQint_fn1 >EQt_fn1 405 >m_return_bind >m_return_bind whd in match point_of_pc; normalize nodelta 406 >point_of_offset_of_point >point_of_offset_of_point >EQin >m_return_bind 407 normalize nodelta >EQt_cost >m_return_bind normalize nodelta [ %] 408 whd in match get_first_costlabel; normalize nodelta whd in ⊢ (??%%); 409 whd in match (get_first_costlabel_next ???); 410 generalize in match (refl ??); 411 >EQin in ⊢ (∀e:???%. ???(??(???(match % return ? with [_ ⇒ ?  _ ⇒ ?]?)))); 412 #EQcost' normalize nodelta % 413 ] 414 % 415 [1,3: whd in match eval_state; whd in match fetch_statement; normalize nodelta 416 >EQt_fn >m_return_bind >point_of_pc_of_point >EQmid >m_return_bind 417 whd in match eval_statement_no_pc; normalize nodelta >m_return_bind 418 whd in match eval_statement_advance; whd in match eval_tailcall; 419 normalize nodelta >EQt_bl >m_return_bind @('bind_inversion EQt_fn1) 420 * #id2 * #fn2 normalize nodelta #EQ whd in ⊢ (??%% → ?); #EQ1 destruct(EQ1) 421 >EQ EQ >m_return_bind normalize nodelta whd in match (stack_sizes ????); 422 >EQssize_f >m_return_bind whd in match eval_internal_call; normalize nodelta 423 whd in match (stack_sizes ????); >EQssize_f1 >m_return_bind >EQst2_after 424 >m_return_bind [2: %] whd in match set_no_pc; normalize nodelta >EQentry % 425 *: @(st_rel_def … good … fin_sem_rel …) [3,7: @EQint_fn1 1,2,5,6:] 426 @(fetch_stmt_ok_sigma_last_pop_ok … good … EQfetch) assumption 427 ] 428 qed. 429 430 lemma eval_tailcall_premain_ok : ∀ P_in , P_out: sem_graph_params. 431 ∀prog : joint_program P_in. 432 ∀stack_sizes. 433 ∀ f_lbls,f_regs.∀f_bl_r.∀init. 434 ∀st_no_pc_rel,st_rel. 435 let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in 436 let trans_prog ≝ b_graph_transform_program P_in P_out init prog in 437 let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in 438 good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs 439 st_no_pc_rel st_rel → 440 ∀st1,st1' : joint_abstract_status prog_pars_in. 441 ∀st2 : joint_abstract_status prog_pars_out. 442 ∀f : ident. 443 ∀fn : joint_closed_internal_function P_in ?. 444 ∀has_tail,id,arg. 445 block_id … (pc_block (pc … st1)) = 1 → 446 st_rel st1 st2 → 447 fetch_statement P_in ? 448 (joint_globalenv P_in prog stack_sizes) (pc … st1) = 449 return 〈f, fn, final … (TAILCALL P_in has_tail id arg)〉 → 450 eval_state P_in … 451 (joint_globalenv P_in prog stack_sizes) st1 = return st1' → 452 ∃is_tail,st2_pre_call,t_is_tail. 453 as_tailcall_ident ? («st2_pre_call,t_is_tail») = as_tailcall_ident ? («st1, is_tail») ∧ 454 ∃st2_after_call,st2' : joint_abstract_status prog_pars_out. 455 ∃taa2 : trace_any_any … st2 st2_pre_call. 456 ∃taa2' : trace_any_any … st2_after_call st2'. 457 eval_state P_out … (joint_globalenv P_out trans_prog stack_sizes) 458 st2_pre_call = return st2_after_call ∧ 459 st_rel st1' st2' ∧ 460 as_label (joint_abstract_status prog_pars_in) st1' = 461 as_label (joint_abstract_status prog_pars_out) st2_after_call. 462 #p_in #p_out #prog #stack_size #f_lbls #f_regs #init_regs #init #st_no_pc_rel 463 #st_rel #good #st1 #st1' #st2 #f #fn #has #id #arg #EQbl #Rst1st2 #EQfetch 464 #EQeval cases(pre_main_ok … good … EQbl EQeval Rst1st2) #Hclass * #st2' ** 465 #Rst1st2' #EQst2' #Hlab % [ @hide_prf whd in ⊢ (??%?); >EQfetch %] %{st2} 466 % [ @hide_prf change with (joint_classify ???) in ⊢ (??%?); <Hclass 467 whd in ⊢ (??%?); >EQfetch %] 468 % 469 [ letin trans_prog ≝ (b_graph_transform_program p_in p_out init prog) 470 cut(∃f',fn',has',id',arg'. 471 fetch_statement p_out … (joint_globalenv p_out trans_prog stack_size) 472 (pc … st2) = return 〈f',fn',final ?? (TAILCALL p_out has' id' arg')〉) 473 [ lapply Hclass whd in ⊢ (??%? → ?); >EQfetch whd in match joint_classify_final; 474 normalize nodelta whd in match joint_classify; normalize nodelta 475 inversion (fetch_statement ????) [2: #e #_ normalize nodelta #EQ destruct(EQ)] 476 ** #f' #fn' * 477 [ * [ #c  #c_id #arg #dest  #r #lbl  #seq ] #nxt  * [ #lbl   #has' #id' #arg' ]  *] 478 #EQt_fetch normalize nodelta whd in ⊢ (???% → ?); #EQ destruct(EQ) 479 %{f'} %{fn'} %{has'} %{id'} %{arg'} % ] 480 * #f' * #fn' * #has' * #id' * #arg' #EQt_fetch 481 @('bind_inversion EQeval) #x >EQfetch in ⊢ (% → ?); whd in ⊢ (??%% → ?); 482 #EQ destruct(EQ) whd in match eval_statement_no_pc; normalize nodelta >m_return_bind 483 whd in match eval_statement_advance; whd in match eval_tailcall; normalize nodelta 484 #H @('bind_inversion H) H #bl #H lapply(err_eq_from_io ????? H) H #EQbl 485 #H @('bind_inversion H) H * #f1 * #fn1 #H lapply(err_eq_from_io ????? H) H 486 #EQfn1 normalize nodelta 487 [2: #H @('bind_inversion H) H #st whd in match eval_external_call; normalize nodelta 488 #H @('bind_inversion H) H #x #_ #H @('bind_inversion H) H #y #_ 489 #H @('bind_inversion H) H #z whd in ⊢ (??%% → ?); #EQ destruct(EQ) 490 ] 491 #H lapply(err_eq_from_io ????? H) H #H@('bind_inversion H) H #f_ssize 492 #H lapply(opt_eq_from_res ???? H) H whd in match (stack_sizes ????); #EQf_ssize 493 #H @('bind_inversion H) H #st1_fin whd in match eval_internal_call; normalize nodelta 494 #H @('bind_inversion H) H #f1_ssize #H lapply(opt_eq_from_res ???? H) H 495 whd in match (stack_sizes ????); #EQf1_ssize #H @('bind_inversion H) H 496 #st1_setup #EQst1_setup whd in ⊢ (??%% → ??%% → ?); #EQ1 #EQ2 destruct(EQ1 EQ2) 497 @('bind_inversion EQst2') #x >EQt_fetch in ⊢ (% → ?); whd in ⊢ (??%% → ?); 498 #EQ destruct(EQ) whd in match eval_statement_no_pc; normalize nodelta 499 >m_return_bind whd in match eval_statement_advance; whd in match eval_tailcall; 500 normalize nodelta #H @('bind_inversion H) H #bl' #H lapply(err_eq_from_io ????? H) 501 H #EQbl' #H @('bind_inversion H) H * #f1' * #fn1' #H lapply(err_eq_from_io ????? H) 502 H #EQfn1' normalize nodelta 503 [2: #H @('bind_inversion H) H #st whd in match eval_external_call; normalize nodelta 504 #H @('bind_inversion H) H #x #_ #H @('bind_inversion H) H #y #_ 505 #H @('bind_inversion H) H #z whd in ⊢ (??%% → ?); #EQ destruct(EQ) 506 ] 507 #H lapply(err_eq_from_io ????? H) H #H @('bind_inversion H) H #f_ssize' 508 #H lapply(opt_eq_from_res ???? H) H whd in match (stack_sizes ????); #EQf_ssize' 509 #H @('bind_inversion H) H #st2_fin whd in match eval_internal_call; 510 normalize nodelta #H @('bind_inversion H) H #f1_ssize' #H lapply(opt_eq_from_res ???? H) 511 H whd in match (stack_sizes ????); #EQf1_ssize' #H @('bind_inversion H) H 512 #st2_setup #EQst2_setup whd in ⊢ (??%% → ??%% → ?); #EQ1 #EQ2 destruct(EQ1 EQ2) 513 whd in ⊢ (??%%); >EQfetch in ⊢ (???(match % with [ _ ⇒ ?  _ ⇒ ? ])); 514 normalize nodelta >EQt_fetch in ⊢ (??(match % with [ _ ⇒ ?  _ ⇒ ? ])?); 515 normalize nodelta >EQbl >EQbl' >m_return_bind >m_return_bind 516 whd in match fetch_internal_function; normalize nodelta 517 lapply(fetch_ok_pc_ok … good … Rst1st2' ?) 518 [ whd in match fetch_internal_function; normalize nodelta >EQfn1 in ⊢ (??%?); % 519 *: 520 ] 521 whd in match pc_of_point in ⊢ (% → ?); normalize nodelta #EQ destruct(EQ) 522 >EQfn1 >EQfn1' >m_return_bind >m_return_bind normalize nodelta 523 lapply EQfn1 whd in match fetch_function; normalize nodelta 524 @eqZb_elim [ #ABS @⊥ cases(block_of_call_no_minus_one … EQbl) #H @H assumption] 525 #Hbl' normalize nodelta #H lapply(opt_eq_from_res ???? H) H #H @('bind_inversion H) 526 #f2 #EQf2 #H @('bind_inversion H) H #fn2 #_ whd in ⊢ (??%? → ?); e0 EQ 527 #EQ destruct(EQ) H lapply EQfn1' whd in match fetch_function; normalize nodelta 528 @eqZb_elim [ #ABS >ABS in Hbl'; * #H @⊥ @H %] #_ normalize nodelta 529 #H lapply(opt_eq_from_res ???? H) H 530 whd in match joint_globalenv in ⊢ (% → ?); normalize nodelta 531 whd in match b_graph_transform_program in ⊢ (% → ?); normalize nodelta 532 whd in match transform_joint_program; normalize nodelta 533 >(symbol_for_block_transf ??? (λx.x) prog 534 (λvars.transf_fundef ?? (λdef_in.b_graph_translate ??? (init ? def_in) def_in)) bl') in ⊢ (% → ?); 535 >EQf2 >m_return_bind in ⊢ (% → ?); #H @('bind_inversion H) H #fn2' #_ 536 whd in ⊢ (??%% → ?); #EQ destruct(EQ) % 537 ] 538 %{st2'} %{st2'} %{(taa_base …)} %{(taa_base …)} % [2: assumption] %{EQst2' Rst1st2'} 539 qed. 540 541 542 lemma eval_cond_ok : ∀ P_in , P_out: sem_graph_params. 1309 543 ∀prog : joint_program P_in. 1310 544 ∀stack_sizes. … … 1332 566 ∃ st2'. st_rel st1' st2' ∧ 1333 567 ∃taf : trace_any_any_free (joint_abstract_status prog_pars_out) st2 st2'. 1334 bool_to_Prop (taaf_non_empty … taf). 568 bool_to_Prop (taaf_non_empty … taf) ∧ 569 as_label (joint_abstract_status prog_pars_in) st1' = 570 as_label (joint_abstract_status prog_pars_out) st2'. 1335 571 #P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_bl_r #init #st_no_pc_rel 1336 572 #st_rel #goodR #st1 #st1' #st2 #f #fn #a #ltrue #lfalse * #Hbl #Rst1st2 … … 1362 598 #l1 * #mid1 * #mid2 * #l2 *** #EQmid1 whd in ⊢ (% → ?); #seq_pre_l whd in ⊢ (% → ?); * #nxt1 1363 599 * #EQmid change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) 1364 cases(bind_new_bind_new_instantiates … EQbl (bind_new_bind_new_instantiates… Hinit600 cases(bind_new_bind_new_instantiates' … EQbl (bind_new_bind_new_instantiates' … Hinit 1365 601 (cond_commutation … goodR … EQfetch EQbv EQbool Rst1st2 t_fn1 EQt_fn1))) 1366 602 [2,4: % assumption] … … 1396 632 #H @H % 1397 633 ] 1398 #taa_pre_mid %{(taaf_step_jump ? ??? taa_pre_mid ???) I}1399 [1, 4: cases(fetch_stmt_ok_succ_ok … (pc … st1) (pc … st1') … EQfetch ?)634 #taa_pre_mid %{(taaf_step_jump ? ??? taa_pre_mid ???)} 635 [1,5: cases(fetch_stmt_ok_succ_ok … (pc … st1) (pc … st1') … EQfetch ?) 1400 636 [2: @ltrue3: %2 % % 4: % 6: @lfalse 7: % % 8: %] #stmt' #EQstmt' 1401 whd <(as_label_ok_non_entry … goodR … EQstmt' H_fin)1402 [1, 3: assumption1403 2, 4: cases(entry_unused … (pi2 ?? fn) … EQstmt)637 whd <(as_label_ok_non_entry … goodR … EQstmt' ? H_fin) 638 [1,4: assumption 639 2,5: cases(entry_unused … (pi2 ?? fn) … EQstmt) 1404 640 [ whd in match stmt_forall_labels; whd in match stmt_labels; 1405 641 normalize nodelta #H cases(append_All … H) #_ … … 1412 648 >point_of_offset_of_point % 1413 649 ] 650 *: % assumption 1414 651 ] 1415 2, 5: whd whd in match (as_classify ??); whd in match fetch_statement; normalize nodelta652 2,6: whd whd in match (as_classify ??); whd in match fetch_statement; normalize nodelta 1416 653 >EQt_fn1 >m_return_bind >point_of_pc_of_point >EQmid normalize nodelta 1417 654 >EQt_cond % 1418  *: whd whd in match eval_state; whd in match fetch_statement; normalize nodelta655 3,7: whd whd in match eval_state; whd in match fetch_statement; normalize nodelta 1419 656 >EQt_fn1 >m_return_bind >point_of_pc_of_point >EQmid >m_return_bind >EQt_cond 1420 657 whd in match eval_statement_no_pc; normalize nodelta >m_return_bind … … 1423 660 [ whd in match goto; normalize nodelta >(pc_of_label_eq … EQt_fn1)] 1424 661 >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 … EQfetch) % 1425 ] 662 *: %{I} cases(fetch_stmt_ok_succ_ok … (pc … st1') … EQfetch) 663 [4,8: % 664 3: whd in match stmt_labels; normalize nodelta @Exists_append2 665 whd in match stmt_explicit_labels; whd in match step_labels; 666 normalize nodelta %1 // 667 7: @Exists_append1 %1 % 668 2,6: 669 ] 670 #stmt' #EQstmt' @(as_label_ok_non_entry … goodR) 671 [4,11: @EQstmt' 672 1,2,3,8,9,10: 673 5,12: % assumption 674 6,13: assumption 675 *: cases(entry_unused ??? (pi2 ?? fn) ?? (proj2 ?? (fetch_statement_inv … EQfetch))) 676 [ * #_ ** whd in match (point_of_label ????); #H #_ #_ % #H1 @H <H1 677 >point_of_pc_of_point % 678  ** whd in match (point_of_label ????); #H #_ #_ % #H1 @H <H1 679 >point_of_pc_of_point % 680 ] 681 ] 682 ] 683 qed. 684 685 lemma eval_cond_premain_ok : ∀ P_in , P_out: sem_graph_params. 686 ∀prog : joint_program P_in. 687 ∀stack_sizes. 688 ∀ f_lbls,f_regs.∀f_bl_r.∀init. 689 ∀st_no_pc_rel,st_rel. 690 let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in 691 let trans_prog ≝ b_graph_transform_program P_in P_out init prog in 692 let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in 693 good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs 694 st_no_pc_rel st_rel → 695 ∀st1,st1' : joint_abstract_status prog_pars_in. 696 ∀st2 : joint_abstract_status prog_pars_out. 697 ∀f : ident. 698 ∀fn : joint_closed_internal_function P_in ?. 699 ∀a,ltrue,lfalse. 700 block_id … (pc_block (pc … st1)) = 1 → 701 st_rel st1 st2 → 702 let cond ≝ (COND P_in ? a ltrue) in 703 fetch_statement P_in ? 704 (joint_globalenv P_in prog stack_sizes) (pc … st1) = 705 return 〈f, fn, sequential … cond lfalse〉 → 706 eval_state P_in … 707 (joint_globalenv P_in prog stack_sizes) st1 = return st1' → 708 as_costed (joint_abstract_status prog_pars_in) st1' → 709 ∃ st2'. st_rel st1' st2' ∧ 710 ∃taf : trace_any_any_free (joint_abstract_status prog_pars_out) st2 st2'. 711 bool_to_Prop (taaf_non_empty … taf) ∧ 712 as_label (joint_abstract_status prog_pars_in) st1' = 713 as_label (joint_abstract_status prog_pars_out) st2'. 714 #p_in #p_out #prog #stack_size #f_lbls #f_regs #init_regs #init #st_no_pc_rel 715 #st_rel #good #st1 #st1' #st2 #f #fn #a #ltrue #lfalse #EQbl #Rst1st2 #EQfetch 716 #EQeval cases(pre_main_ok … good … EQbl EQeval Rst1st2) #Hclass * #st2' 717 ** #Rst1st2' #EQst2' #Hlab whd in ⊢ (% → ?); * #ncost %{st2'} %{Rst1st2'} 718 %{(taaf_step_jump … (taa_base …) …)} 719 [ whd <Hlab % assumption 720  whd change with (joint_classify ???) in ⊢ (??%?); <Hclass 721 whd in match joint_classify; normalize nodelta >EQfetch % 722  assumption 723 ] 724 %{I} assumption 1426 725 qed. 1427 726 … … 1453 752 if taaf_non_empty … taf then True else (*IT CAN BE SIMPLIFIED *) 1454 753 (¬as_costed (joint_abstract_status (mk_prog_params P_in prog stack_sizes)) st1 ∨ 1455 ¬as_costed (joint_abstract_status (mk_prog_params P_in prog stack_sizes)) st1'). 754 ¬as_costed (joint_abstract_status (mk_prog_params P_in prog stack_sizes)) st1') ∧ 755 as_label (joint_abstract_status prog_pars_in) st1' = 756 as_label (joint_abstract_status prog_pars_out) st2'. 1456 757 #P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_bl_r #init #st_no_pc_rel #st_rel 1457 758 #goodR #st1 #st1' #st2 #f #fn #stmt #nxt * #Hbl #Rst1st2 #EQfetch #EQeval … … 1474 775 #_ <(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) #EQbl 1475 776 >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) #SBiC 1476 cases(bind_new_bind_new_instantiates … EQbl (bind_new_bind_new_instantiates… Hinit777 cases(bind_new_bind_new_instantiates' … EQbl (bind_new_bind_new_instantiates' … Hinit 1477 778 (seq_commutation … goodR … EQfetch EQeval Rst1st2 t_fn EQt_fn))) 1478 779 [2: % assumption] … … 1480 781 %{(mk_state_pc ? st2_fin_no_pc (pc_of_point P_out (pc_block (pc … st2)) nxt) (last_pop … st2))} 1481 782 cases(fetch_statement_inv … EQfetch) >(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) 1482 #EQfn #_ 1483 % 1484 [ @(st_rel_def ?????????? goodR … f fn) 783 #EQfn #_ cut(? : Prop) [3: #Hfin % [@Hfin] 1: 784  @(st_rel_def ?????????? goodR … f fn) 1485 785 [ change with (pc_block (pc … st2)) in match (pc_block ?); assumption 1486 786  <(fetch_stmt_ok_sigma_pc_ok … goodR … EQfetch) assumption … … 1490 790 %{(produce_trace_any_any_free_coerced ? st2 f t_fn l ?? st2_fin_no_pc EQt_fn 1491 791 SBiC EQst2_fin_no_pc)} 1492 @if_elim #_ [@I] % % whd in ⊢ (% → ?); * #H @H H whd in ⊢ (??%?); >EQfetch % 792 % [ @if_elim #_ [@I] % % whd in ⊢ (% → ?); * #H @H H whd in ⊢ (??%?); >EQfetch % ] 793 cases(fetch_stmt_ok_succ_ok … nxt … EQfetch) [4: % 3: % % 2:] 794 #stmt' #EQstmt' @(as_label_ok_non_entry … goodR) 795 [4: <(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) in ⊢ (??%?); @EQstmt' 796 1,2,3: 797  % <(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) assumption 798  assumption 799  cases(entry_unused ??? (pi2 ?? fn) ?? (proj2 ?? (fetch_statement_inv … EQfetch))) 800 * whd in match (point_of_label ????); * #H #_ #_ % #H1 @H <H1 whd in match succ_pc; 801 whd in match point_of_pc; whd in match pc_of_point; normalize nodelta 802 >point_of_offset_of_point % 803 ] 1493 804 qed. 1494 805 806 lemma general_eval_seq_no_call_premain_ok :∀ P_in , P_out: sem_graph_params. 807 ∀prog : joint_program P_in. 808 ∀stack_sizes. 809 ∀ f_lbls,f_regs.∀f_bl_r.∀init. 810 ∀st_no_pc_rel,st_rel. 811 let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in 812 let trans_prog ≝ b_graph_transform_program P_in P_out init prog in 813 let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in 814 good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs 815 st_no_pc_rel st_rel → 816 ∀st1,st1' : joint_abstract_status prog_pars_in. 817 ∀st2 : joint_abstract_status prog_pars_out. 818 ∀f.∀fn : joint_closed_internal_function P_in ?. 819 ∀stmt,nxt. 820 block_id … (pc_block (pc … st1)) = 1 → 821 st_rel st1 st2 → 822 let seq ≝ (step_seq P_in ? stmt) in 823 fetch_statement P_in … 824 (joint_globalenv P_in prog stack_sizes) (pc … st1) = 825 return 〈f, fn, sequential ?? seq nxt〉 → 826 eval_state P_in … (joint_globalenv P_in prog stack_sizes) 827 st1 = return st1' → 828 ∃st2'. st_rel st1' st2' ∧ 829 ∃taf : trace_any_any_free (joint_abstract_status prog_pars_out) st2 st2'. 830 bool_to_Prop (taaf_non_empty … taf) ∧ 831 as_label (joint_abstract_status prog_pars_in) st1' = 832 as_label (joint_abstract_status prog_pars_out) st2'. 833 #p_in #p_out #prog #stack_size #f_lbls #f_regs #init_regs #init #st_no_pc_rel 834 #st_rel #good #st1 #st1' #st2 #f #fn #stmt #nxt #EQbl #Rst1st2 #EQfetch 835 #EQeval cases(pre_main_ok … good … EQbl EQeval Rst1st2) #Hclass * #st2' 836 ** #Rst1st2' #EQst2' #Hlab %{st2'} %{Rst1st2'} %{(taaf_step … (taa_base …) …)} 837 [ whd change with (joint_classify ???) in ⊢ (??%?); <Hclass whd in match joint_classify; 838 normalize nodelta >EQfetch % 839  assumption 840 ] 841 %{I} assumption 842 qed. 1495 843 1496 844 lemma general_eval_cost_ok : … … 1521 869 (joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes)) 1522 870 st2 st2'. 1523 bool_to_Prop (taaf_non_empty … taf). 871 bool_to_Prop (taaf_non_empty … taf) ∧ 872 as_label (joint_abstract_status prog_pars_in) st1' = 873 as_label (joint_abstract_status prog_pars_out) st2'. 1524 874 #P_in #P_out #prog #stack_size #f_lbls #f_regs #f_bl_r #init #st_no_pc_rel 1525 875 #st_rel #goodR #st1 #st1' #st2 #f #fn #c #nxt * #Hbl #Rst1st2 normalize nodelta … … 1529 879 #EQ destruct(EQ) 1530 880 %{(mk_state_pc ? (st_no_pc … st2) (pc_of_point P_out (pc_block (pc … st2)) nxt) 1531 (last_pop … st2))} % 1532 [ cases(fetch_statement_inv … EQfetch) #EQfn #_ 881 (last_pop … st2))} 882 cut(? : Prop) [3: #Hfin % [@Hfin]  883  cases(fetch_statement_inv … EQfetch) #EQfn #_ 1533 884 <(fetch_stmt_ok_sigma_pc_ok … goodR … Rst1st2 EQfetch) 1534 885 whd in match (succ_pc ???); whd in match (point_of_succ ???); … … 1540 891  @(fetch_stmt_ok_sigma_last_pop_ok … goodR … Rst1st2 EQfetch) 1541 892 ] 1542  lapply(b_graph_transform_program_fetch_statement … goodR (pc … st1) f fn ?) 893 ] 894 lapply(b_graph_transform_program_fetch_statement … goodR (pc … st1) f fn ?) 1543 895 [2: @eqZb_elim [ #ABS @⊥ >ABS in Hbl; #H @H %] #_ normalize nodelta 1544 896 #H cases(H EQfetch) H *:] … … 1564 916 ] 1565 917 %{(taaf_step … (taa_base …) …)} 1566 [3,6,9: @I918 [3,6,9: %{I} 1567 919 *: whd whd in ⊢ (??%?); whd in match fetch_statement; normalize nodelta 1568 920 >EQt_fn >m_return_bind >EQt_stmt >m_return_bind % 1569 921 ] 922 cases(fetch_stmt_ok_succ_ok … nxt … EQfetch) [4,8,12: % 2,6,10: 3,7,11: % %] 923 #stmt' #EQstmt' @(as_label_ok_non_entry … goodR) 924 [4,11,18: @EQstmt' 925 1,2,3,8,9,10,15,16,17: 926 5,12,19: % assumption 927 6,13,20: assumption 928 *: cases(entry_unused ??? (pi2 ?? fn) ?? (proj2 ?? (fetch_statement_inv … EQfetch))) 929 * whd in match (point_of_label ????); * #H #_ #_ % #H1 @H <H1 whd in match succ_pc; 930 whd in match point_of_pc; whd in match pc_of_point; normalize nodelta 931 >point_of_offset_of_point % 1570 932 ] 1571 933 qed. 1572 934 1573 lemma next_of_call_pc_error : ∀pars.∀prog. ∀stack_size,pc. 1574 block_id (pi1 … (pc_block pc)) = 0→ 1575 next_of_call_pc pars … (ev_genv … (mk_prog_params pars prog stack_size)) 1576 pc = Error ? [MSG BadFunction]. 1577 #pars #prg #init #pc #EQ whd in match next_of_call_pc; normalize nodelta 1578 whd in match fetch_statement; normalize nodelta 1579 >fetch_internal_function_no_zero // 935 lemma general_eval_cost_premain_ok : 936 ∀ P_in , P_out: sem_graph_params. 937 ∀prog : joint_program P_in. 938 ∀stack_sizes. 939 ∀ f_lbls,f_regs.∀f_bl_r.∀init. 940 ∀st_no_pc_rel,st_rel. 941 let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in 942 let trans_prog ≝ b_graph_transform_program P_in P_out init prog in 943 let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in 944 good_state_relation P_in P_out prog stack_sizes init f_bl_r f_lbls f_regs 945 st_no_pc_rel st_rel → 946 ∀st1,st1' : joint_abstract_status prog_pars_in. 947 ∀st2 : joint_abstract_status prog_pars_out. 948 ∀f. 949 ∀fn : joint_closed_internal_function P_in ?.∀c,nxt. 950 block_id … (pc_block (pc … st1)) = 1 → 951 st_rel st1 st2 → 952 let cost ≝ COST_LABEL P_in ? c in 953 fetch_statement P_in … 954 (joint_globalenv P_in prog stack_sizes) (pc … st1) = 955 return 〈f, fn, sequential ?? cost nxt〉 → 956 eval_state P_in … (ev_genv … prog_pars_in) 957 st1 = return st1' → 958 ∃ st2'. st_rel st1' st2' ∧ 959 ∃taf : trace_any_any_free 960 (joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes)) 961 st2 st2'. 962 bool_to_Prop (taaf_non_empty … taf) ∧ 963 as_label (joint_abstract_status prog_pars_in) st1' = 964 as_label (joint_abstract_status prog_pars_out) st2'. 965 #p_in #p_out #prog #stack_size #f_lbls #f_regs #init_regs #init #st_no_pc_rel #st_rel 966 #good #st1 #st1' #st2 #f #fn #c #nxt #EQbl #Rst1st2 #EQfetch #EQeval 967 cases(pre_main_ok … good … EQbl EQeval Rst1st2) #Hclass * #st2' 968 ** #Rst1st2' #EQst2' #Hlab %{st2'} %{Rst1st2'} %{(taaf_step … (taa_base …) …)} 969 [ whd change with (joint_classify ???) in ⊢ (??%?); <Hclass 970 whd in match joint_classify; normalize nodelta >EQfetch % 971  assumption 972 ] 973 %{I} assumption 1580 974 qed. 1581 975 … … 1598 992 ∀p_in,p_out,prog,stack_size,init,init_regs,f_lbls,f_regs,pc,pc'. 1599 993 sigma_pc_opt p_in p_out prog stack_size init init_regs f_lbls f_regs pc ≠ None ? → 994 block_id (pc_block pc) ≠ OZ → 1600 995 sigma_stored_pc p_in p_out prog stack_size init init_regs f_lbls f_regs pc = 1601 996 sigma_stored_pc p_in p_out prog stack_size init init_regs f_lbls f_regs pc' → 1602 997 pc = pc'. 1603 #p_in #p_out #prog #stack_size #init #init_regs #f_lbls #f_regs #pc #pc' #H 998 #p_in #p_out #prog #stack_size #init #init_regs #f_lbls #f_regs #pc #pc' #H *#H1 1604 999 whd in match sigma_stored_pc; normalize nodelta 1605 inversion(sigma_pc_opt ?????????) [ #ABS >ABS in H; * #H @⊥ @H %] #pc1 #EQpc11000 inversion(sigma_pc_opt ?????????) [ #ABS >ABS in H; * #H @⊥ @H %] #pc1 #EQpc1 1606 1001 normalize nodelta inversion(sigma_pc_opt ?????????) 1607 [ #ABS normalize nodelta #EQ destruct(EQ) lapply EQpc1; whd in match sigma_pc_opt; 1608 normalize nodelta @eqZb_elim 1609 [ #ABS1 whd in ⊢ (??%? → ?); #EQ destruct(EQ) whd in ABS1 : (??%%); destruct] 1002 [ #ABS normalize nodelta #EQ destruct(EQ) lapply EQpc1 whd in match sigma_pc_opt; 1003 normalize nodelta @if_elim 1004 [ #Hbl whd in ⊢ (??%? → ?); #EQ destruct(EQ) lapply(Hbl) Hbl @eqZb_elim 1005 [whd in ⊢ (??%% → ?); #EQ destruct(EQ)] @eqZb_elim [#ABS >ABS in H1; #H @⊥ @H %] 1006 @⊥ @H1 %] 1610 1007 #Hbl normalize nodelta #H @('bind_inversion H) H #lbl whd in match sigma_label; 1611 1008 normalize nodelta >code_block_of_block_eq >m_return_bind … … 1617 1014 [ assumption] >EQpc1 >EQpc2 % 1618 1015 qed. 1619 1620 1621 1622 1623 1016 1624 1017 lemma eval_return_ok : … … 1650 1043 as_classifier … st2_ret cl_return ∧ 1651 1044 as_execute … st2_ret st2_after_ret ∧ st_rel st1' st2' ∧ 1652 ret_rel ?? (JointStatusSimulation … good) st1' st2_after_ret. 1045 ret_rel ?? (JointStatusSimulation … good) st1' st2_after_ret ∧ 1046 as_label (joint_abstract_status prog_pars_in) st1' = 1047 as_label (joint_abstract_status prog_pars_out) st2'. 1653 1048 #p_in #p_out #prog #stack_size #f_lbls #f_regs #init_regs #init #st_no_pc_rel 1654 1049 #st_rel #good #st1 #st1' #st2 #f #fn #Hbl #Rst1st2 #EQfetch … … 1669 1064 cases(next_of_call_pc_inv … EQnext_of_call) #f1 * #fn1 * #id * #args * #dest #EQcall 1670 1065 <(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in Hregs; #Hregs 1671 cases(bind_new_bind_new_instantiates … Hregs (bind_new_bind_new_instantiates… Hinit1066 cases(bind_new_bind_new_instantiates' … Hregs (bind_new_bind_new_instantiates' … Hinit 1672 1067 (return_commutation ?????????? good … Hbl EQfetch … EQssize … EQpop … EQcall … 1673 1068 Rst1st2 t_fn EQt_fn))) #EQ destruct(EQ) * #st_fin * #EQst_fin * #t_st_pop * #t_pc_pop 1674 1069 ** #EQt_pop #EQt_pc_pop @eqZb_elim #Hbl_pcpop normalize nodelta 1675 [ #sem_rel (*premain case TODO *) cases daemon ] 1070 [ * #sem_rel #EQt_next 1071 %{(mk_state_pc ? st_fin (pc_of_point p_out (pc_block (pc … st2)) mid) (last_pop … st2))} 1072 %{(mk_state_pc ? (decrement_stack_usage p_out ssize t_st_pop) 1073 (pc_of_point p_out (pc_block t_pc_pop) next_of_call) t_pc_pop)} 1074 %{(mk_state_pc ? (decrement_stack_usage p_out ssize t_st_pop) 1075 (pc_of_point p_out (pc_block t_pc_pop) next_of_call) t_pc_pop)} 1076 %{((taaf_to_taa … 1077 (produce_trace_any_any_free ? st2 f t_fn … EQt_fn EQpre EQst_fin) ?))} 1078 [ @if_elim #_ [2: @I] % * #H @H H whd in ⊢ (??%?); whd in match fetch_statement; 1079 normalize nodelta >EQt_fn >m_return_bind >point_of_pc_of_point >EQt_stmt % ] 1080 %{(taaf_base …)} cut(? : Prop) 1081 [3: #Hfin % [ % 1082 [ % [ % [%{I} ] 1083 whd [whd in ⊢ (??%?);  whd in match eval_state;] whd in match fetch_statement; 1084 normalize nodelta >EQt_fn >m_return_bind >point_of_pc_of_point >EQt_stmt [%] 1085 >m_return_bind whd in match eval_statement_no_pc; normalize nodelta 1086 >m_return_bind whd in match eval_statement_advance; whd in match eval_return; 1087 normalize nodelta whd in match (stack_sizes ????); >EQssize >m_return_bind 1088 >EQt_pop >m_return_bind >EQt_next >m_return_bind % 1089  @Hfin 1090 ] 1091  whd * #s1_pre #s1_call cases (joint_classify_call … s1_call) * #calling_i 1092 #calling * #id1 * #arg1 * #dest1 * #nxt' #EQfetch_call * #s2_pre #s2_call 1093 whd in ⊢ (% → ?); >EQfetch_call normalize nodelta * #EQ destruct(EQ) 1094 whd in ⊢ (??%% → ?); whd in match (point_of_succ ???); 1095 whd in match (point_of_succ ???); #EQ cut(next_of_call =nxt') 1096 [ lapply(eq_to_jmeq ??? EQ) EQ #EQ destruct(EQ) cases next_of_call in e0; #x 1097 normalize nodelta whd in match (offset_of_point ??); cases nxt' #y 1098 normalize nodelta #EQ1 destruct(EQ1) % ] 1099 EQ #EQ destruct(EQ) whd in ⊢ (% → ?); <EQt_pc_pop #EQ1 1100 lapply(stored_pc_inj … EQ1) 1101 [2: % #ABS cases(fetch_statement_inv … EQcall) <EQt_pc_pop 1102 >fetch_internal_function_no_zero [#EQ destruct] whd in match sigma_stored_pc; 1103 normalize nodelta >ABS % 1104  % #ABS cases(next_of_call_pc_inv … EQt_next) #x * #y * #z * #w * #a 1105 whd in match fetch_statement; normalize nodelta >fetch_internal_function_no_zero 1106 [whd in ⊢ (??%% → ?); #EQ destruct(EQ) ] assumption 1107 ] #EQ2 destruct(EQ2) whd 1108 cases(next_of_call_pc_inv … EQt_next) #id'' * #fn'' * #c_id'' * #c_args'' 1109 * #c_dest'' #EQ3 >EQ3 normalize nodelta % [%] % ] ] 1110 2: whd in match succ_pc; normalize nodelta whd in match (point_of_succ ???); 1111 destruct(EQt_pc_pop) lapply(proj1 ?? (fetch_statement_inv … EQcall)) 1112 <pc_block_eq in Hbl_pcpop sem_rel ⊢ %; 1113 [2: % #H cases(fetch_statement_inv … EQcall) >fetch_internal_function_no_zero 1114 [ #EQ destruct] whd in match sigma_stored_pc; normalize nodelta >H %] 1115 #Hbl_pcpop #sem_rel #EQ @(st_rel_def … good … sem_rel … ) [3: @EQ 1,2:] % 1116  1117 ] 1118 cases(fetch_stmt_ok_succ_ok … next_of_call … EQcall) [4: % 3: % % 2:] 1119 #stmt' #EQstmt' cases(decidable_eq_Z (block_id (pc_block pc_pop)) (neg one)) 1120 [ #Hbl @(as_label_premain_ok ?????????? good) [assumption  assumption ] 1121  #Hbl_pc_pop @(as_label_ok_non_entry … good) 1122 [4: @EQstmt' 1123 1,2,3: 1124  assumption 1125  assumption 1126  cases(entry_unused ??? (pi2 ?? fn1) ?? (proj2 ?? (fetch_statement_inv … EQcall))) 1127 * whd in match (point_of_label ????); * #H #_ #_ % >point_of_pc_of_point 1128 #H1 @H <H1 % 1129 ] 1130 ] 1131 ] 1676 1132 cases(fetch_statement_sigma_stored_pc … good … Hbl_pcpop … EQcall) #data1 * #Hinit1 1677 1133 normalize nodelta *** #pre_c #instr_c #post_c * #Hregs1 * #pc1 * destruct(EQt_pc_pop) … … 1690 1146 cases(fetch_statement_inv … EQcall) #_ normalize nodelta >ABS #EQ destruct(EQ) ] 1691 1147 #_ cut(∀x : bool.andb x false = false) [* %] #EQ >EQ EQ normalize nodelta *** 1692 cases(bind_new_bind_new_instantiates … (bind_instantiates_to_instantiate … Hregs1)1693 (bind_new_bind_new_instantiates … (bind_instantiates_to_instantiate … Hinit1)1148 cases(bind_new_bind_new_instantiates' … (bind_instantiates_to_instantiate … Hregs1) 1149 (bind_new_bind_new_instantiates' … (bind_instantiates_to_instantiate … Hinit1) 1694 1150 ((call_is_call … good … (proj1 … (fetch_statement_inv … EQcall))) id args dest ?)) (point_of_pc p_in pc1)) 1695 1151 #id' * #args' * #dest' #EQ >EQ EQ #EQt_call #EQpre_c #EQpost_c #EQnxt1 #H 1696 cases(bind_new_bind_new_instantiates … (bind_instantiates_to_instantiate … Hregs1)1697 (bind_new_bind_new_instantiates … (bind_instantiates_to_instantiate … Hinit1) H))1152 cases(bind_new_bind_new_instantiates' … (bind_instantiates_to_instantiate … Hregs1) 1153 (bind_new_bind_new_instantiates' … (bind_instantiates_to_instantiate … Hinit1) H)) 1698 1154 H #st2' * #EQst2' #fin_sem_rel 1699 1155 %{(mk_state_pc ? st_fin (pc_of_point p_out (pc_block (pc … st2)) mid) (last_pop … st2))} … … 1718 1174 *: 1719 1175 ] 1720 % 1721 [ %1176 cut(? : Prop) 1177 [3: #Hfin % 1722 1178 [ % 1723 1179 [ % 1724 [ @if_elim [2: #_ @I] #H lapply(prf H) cases post_c in EQpost_c; [#_ *] 1725 #hd #tl whd in ⊢ (% → ?); * #lab * #rest ** #EQ destruct(EQ) * 1726 #succ * #EQnxt1 change with succ in ⊢ (??%? → ?); #EQ destruct(EQ) 1727 #EQrest #_ % whd in ⊢ (% → ?); whd in match (as_label ??); 1728 whd in match (as_pc_of ??); whd in match (point_of_succ ???); 1729 change with (pc_block pc1) in match (pc_block ?); 1730 whd in match fetch_statement; normalize nodelta 1731 >(proj1 … (fetch_statement_inv … EQt_call)) >m_return_bind 1732 whd in match point_of_pc; normalize nodelta >point_of_offset_of_point 1733 >EQnxt1 >m_return_bind normalize nodelta whd in match cost_label_of_stmt; 1734 normalize nodelta * #H @H % ] 1180 [2: @Hfin 1181  % 1182 [ % 1183 [ @if_elim [2: #_ @I] #H lapply(prf H) cases post_c in EQpost_c; [#_ *] 1184 #hd #tl whd in ⊢ (% → ?); * #lab * #rest ** #EQ destruct(EQ) * 1185 #succ * #EQnxt1 change with succ in ⊢ (??%? → ?); #EQ destruct(EQ) 1186 #EQrest #_ % whd in ⊢ (% → ?); whd in match (as_label ??); 1187 whd in match (as_pc_of ??); whd in match (point_of_succ ???); 1188 change with (pc_block pc1) in match (pc_block ?); 1189 whd in match fetch_statement; normalize nodelta 1190 >(proj1 … (fetch_statement_inv … EQt_call)) >m_return_bind 1191 whd in match point_of_pc; normalize nodelta >point_of_offset_of_point 1192 >EQnxt1 >m_return_bind normalize nodelta whd in match cost_label_of_stmt; 1193 normalize nodelta * #H @H % ] 1735 1194 ] 1736 1195 whd [ whd in match (as_classify ??);  whd in match eval_state; normalize nodelta] … … 1741 1200 >EQssize >m_return_bind >EQt_pop >m_return_bind whd in match next_of_call_pc; 1742 1201 normalize nodelta >EQt_call >m_return_bind % 1743  whd in match succ_pc; normalize nodelta <(pc_block_eq) [2: >EQpc2 % #EQ destruct] 1744 whd in match (point_of_succ ???); @(st_rel_def … good) 1202 ] 1203 ] 1204 ] 1205  1206  whd in match succ_pc; normalize nodelta <(pc_block_eq) [2: >EQpc2 % #EQ destruct] 1207 whd in match (point_of_succ ???); @(st_rel_def … good) 1745 1208 [3: change with (pc_block pc1) in match (pc_block ?); 1746 1209 lapply(proj1 ?? (fetch_statement_inv … EQcall)) <pc_block_eq in ⊢ (% → ?); … … 1751 1214 ] 1752 1215 ] 1753 ] 1754 whd * #s1_pre #s1_call cases (joint_classify_call … s1_call) * #calling_i 1755 #calling * #call_spec * #arg * #dest * #nxt' #EQfetch_call * #s2_pre #s2_call 1216 [ whd * #s1_pre #s1_call cases (joint_classify_call … s1_call) * #calling_i 1217 #calling * #call_spec * #arg * #dest * #nxt' #EQfetch_call * #s2_pre #s2_call 1756 1218 whd in ⊢ (% → ?); >EQfetch_call normalize nodelta * #EQpc1_pc_s1_pre #EQsucc_pc 1757 1219 whd in ⊢ (% → ?); #EQpc_s1_pre >EQpc_s1_pre in EQfetch_call; #EQfetch_call … … 1760 1222 #data2 * #EQdata2 normalize nodelta * #bl2 * #EQbl2 * #pc3 * #EQstored 1761 1223 lapply(stored_pc_inj … (sym_eq ??? EQstored)) 1762 [ % #ABS cases(fetch_statement_inv … EQfetch_call) >fetch_internal_function_no_zero 1763 [ #EQ destruct(EQ)] whd in match sigma_stored_pc; normalize nodelta >ABS % ] 1224 [2: % #ABS cases(fetch_statement_inv … EQfetch_call) >fetch_internal_function_no_zero 1225 [ #EQ destruct(EQ)] whd in match sigma_stored_pc; normalize nodelta >ABS % 1226  % #ABS cases(fetch_statement_inv … EQfetch_call) >fetch_internal_function_no_zero 1227 [2: <pc_block_eq [assumption] % #ABS1 cases(fetch_statement_inv … EQfetch_call) 1228 whd in match sigma_stored_pc; normalize nodelta >ABS1 1229 >fetch_internal_function_no_zero [2: %] ] whd in ⊢ (??%% → ?); #EQ destruct 1230 ] 1764 1231 #EQ destruct(EQ) * #fn' * #nxt'' * #l1 * #l2 @eq_identifier_elim 1765 1232 [ #EQentry cases(fetch_statement_inv … EQfetch_call) #_ >EQentry normalize nodelta … … 1771 1238 2: @(stored_pc_inj p_in p_out prog stack_size init init_regs f_lbls f_regs … ) 1772 1239 [ % #ABS cases(fetch_statement_inv … EQcall) >fetch_internal_function_no_zero 1773 [#EQ destruct] whd in match sigma_stored_pc; normalize nodelta >ABS % ] 1774 >EQpc1_pc_s1_pre assumption 1240 [#EQ destruct] whd in match sigma_stored_pc; normalize nodelta >ABS % 1241 3: >EQpc1_pc_s1_pre assumption 1242  % #ABS cases(fetch_statement_inv … EQt_call) >fetch_internal_function_no_zero 1243 [2: assumption] #EQ destruct 1244 ] 1775 1245 ] 1776 1246 destruct(H) … … 1784 1254 #EQ destruct(EQ) >EQcall in EQfetch_call; >EQt_call in EQt_fetch_call; 1785 1255 whd in ⊢ (? → ??%? → ?); #EQ1 #EQ2 lapply(eq_to_jmeq ??? EQ1) EQ1 #EQ1 destruct(EQ1) % 1256 ] 1257 cases(fetch_stmt_ok_succ_ok … next_of_call … EQcall) [4: % 3: % % 2:] 1258 #stmt' #EQstmt' cases(decidable_eq_Z (block_id (pc_block pc1)) (neg one)) 1259 [ #Hbl @(as_label_premain_ok ?????????? good) 1260 [ change with (pc_block (sigma_stored_pc ?????????)) in match (pc_block ?); 1261 <pc_block_eq [ assumption] % #ABS cases(fetch_statement_inv … EQstmt') 1262 >fetch_internal_function_no_zero [#EQ destruct] whd in match sigma_stored_pc; 1263 normalize nodelta >ABS % 1264  assumption 1265 ] 1266  #Hbl_pc_pop @(as_label_ok_non_entry … good) 1267 [4: @EQstmt' 1268 1,2,3: 1269  assumption 1270  assumption 1271  cases(entry_unused ??? (pi2 ?? fn1) ?? (proj2 ?? (fetch_statement_inv … EQcall))) 1272 * whd in match (point_of_label ????); * #H #_ #_ % >point_of_pc_of_point 1273 #H1 @H <H1 % 1274 ] 1275 ] 1786 1276 qed. 1787 1277 1278 lemma eval_call_ok : ∀ P_in , P_out: sem_graph_params. 1279 ∀prog : joint_program P_in. 1280 ∀stack_size. 1281 ∀ f_lbls,f_regs.∀init_regs.∀init. 1282 ∀st_no_pc_rel,st_rel. 1283 let prog_pars_in ≝ mk_prog_params P_in prog stack_size in 1284 let trans_prog ≝ b_graph_transform_program P_in P_out init prog in 1285 let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_size in 1286 ∀good : good_state_relation P_in P_out prog stack_size init init_regs f_lbls f_regs 1287 st_no_pc_rel st_rel. 1288 ∀st1,st1' : joint_abstract_status prog_pars_in. 1289 ∀st2 : joint_abstract_status prog_pars_out. 1290 ∀f. 1291 ∀fn : joint_closed_internal_function P_in ?. 1292 ∀id,arg,dest,nxt. 1293 block_id … (pc_block (pc … st1)) ≠ 1 → 1294 st_rel st1 st2 → 1295 fetch_statement P_in … 1296 (joint_globalenv P_in prog stack_size) (pc … st1) = 1297 return 〈f, fn,sequential P_in ? (CALL ?? id arg dest) nxt〉 → 1298 eval_state P_in … (ev_genv … prog_pars_in) 1299 st1 = return st1' → 1300 ∃is_call,st2_pre_call,t_is_call. 1301 as_call_ident (joint_abstract_status prog_pars_in) «st1,is_call» = 1302 as_call_ident (joint_abstract_status prog_pars_out) «st2_pre_call,t_is_call» ∧ 1303 (pc … st1) = sigma_stored_pc P_in P_out prog stack_size 1304 init init_regs f_lbls f_regs (pc … st2_pre_call) ∧ 1305 ∃st2_after_call,st2' : joint_abstract_status prog_pars_out. 1306 ∃taa2 : trace_any_any … st2 st2_pre_call. 1307 ∃taa2' : trace_any_any … st2_after_call st2'. 1308 eval_state P_out … (joint_globalenv P_out trans_prog stack_size) st2_pre_call = 1309 return st2_after_call ∧ 1310 st_rel st1' st2' ∧ 1311 as_label (joint_abstract_status prog_pars_in) st1' = 1312 as_label (joint_abstract_status prog_pars_out) st2_after_call. 1313 #p_in #p_out #prog #stack_size #f_lbls #f_regs #init_regs #init #st_no_pc_rel #st_rel 1314 #good #st1 #st1' #st2 #f #fn #id #arg #dest #nxt #Hbl #Rst1st2 #EQfetch 1315 whd in match eval_state in ⊢ (% → ?); normalize nodelta >EQfetch >m_return_bind 1316 whd in match eval_statement_no_pc; normalize nodelta >m_return_bind 1317 #H @('bind_inversion H) H #bl >set_no_pc_eta #H lapply(err_eq_from_io ????? H) H 1318 #EQbl #H @('bind_inversion H) H * #f1 * 1319 #fn1 #H lapply(err_eq_from_io ????? H) H #EQfn1 normalize nodelta 1320 [2: #H @('bind_inversion H) H #x whd in match eval_external_call; normalize nodelta 1321 #H @('bind_inversion H) H #y #_ #H @('bind_inversion H) H #z #_ 1322 #H @('bind_inversion H) H #w whd in ⊢ (??%% → ?); #ABS destruct(ABS) ] 1323 #H lapply(err_eq_from_io ????? H) H #H @('bind_inversion H) H #st1_save #EQst1_save 1324 #H @('bind_inversion H) H #st1_no_pc' whd in match eval_internal_call; 1325 normalize nodelta change with (stack_size ?) in match (stack_sizes ????); #H 1326 @('bind_inversion H) H #ssize #H lapply(opt_eq_from_res ???? H) H #EQssize 1327 #H @('bind_inversion H) H #st1_no_pc'' #EQst1_no_pc'' whd in ⊢ (??%% → ?); 1328 #EQ destruct(EQ) whd in ⊢ (??%% → ?); #EQ destruct(EQ) 1329 % [@hide_prf whd in ⊢ (??%?); >EQfetch %] 1330 cases(fetch_statement_sigma_stored_pc … good … Hbl EQfetch) 1331 #data * #EQdata normalize nodelta *** #pre #instr #post * #Hregs * #pc' * #EQpc' 1332 * #t_fn * #nxt' * #l1 * #l2 @eq_identifier_elim 1333 [ #EQentry cases(fetch_statement_inv … EQfetch) #_ >EQentry normalize nodelta 1334 cases(entry_is_cost … (pi2 ?? fn)) #nxt1 * #c #EQ >EQ #ABS destruct(ABS) ] 1335 #_ cut(∀b.andb b false = false) [* %] #EQ ** >EQ EQ normalize nodelta * 1336 #EQt_call #EQpre #EQpost #_ 1337 lapply(b_graph_transform_program_fetch_internal_function … good … bl f1 fn1) 1338 @eqZb_elim [ normalize nodelta #ABS @⊥ cases(block_of_call_no_minus_one … EQbl) >ABS #H @H %] 1339 #_ normalize nodelta #H cut(? : Prop) 1340 [3: #EQint_fn cases(H EQint_fn) H 1341 2: whd in match fetch_internal_function; normalize nodelta >EQfn1 %*:] 1342 #data1 * #t_fn1 ** #EQt_fn1 #Hdata1 #good1 1343 cases(bind_new_bind_new_instantiates' … (bind_instantiates_to_instantiate … Hregs) 1344 (bind_new_bind_new_instantiates' … (bind_instantiates_to_instantiate … EQdata) 1345 (call_is_call … good … )) … (point_of_pc p_out pc')) 1346 [4: @(proj1 … (fetch_statement_inv … EQfetch)) *:] 1347 #id' * #args' * #dest' #EQinstr 1348 cases(bind_new_bind_new_instantiates' … (bind_instantiates_to_instantiate … Hregs) 1349 (bind_new_bind_new_instantiates' … (bind_instantiates_to_instantiate … EQdata) 1350 (call_commutation … good … Hbl EQfetch bl EQbl … EQint_fn … EQst1_save … EQssize … 1351 EQst1_no_pc'' … Rst1st2 … EQt_fn1)) … EQpc' EQt_call EQinstr) 1352 #st2_pre ** #EQst2_pre #EQt_bl * #st2_save * #EQst2_save * #st2_after * #EQst2_after 1353 #Hprologue 1354 %{(mk_state_pc ? st2_pre pc' (last_pop … st2))} 1355 % 1356 [ @hide_prf whd in ⊢ (??%?); >EQt_call >EQinstr %] 1357 % 1358 [ % [2: @sym_eq assumption] whd in ⊢ (??%%); 1359 >EQfetch in ⊢ (??(match % with [ _ ⇒ ?  _ ⇒ ? ])?); 1360 >EQt_call in ⊢ (???(match % with [ _ ⇒ ?  _ ⇒ ? ])); normalize nodelta >EQbl 1361 >m_return_bind >EQint_fn normalize nodelta >EQinstr normalize nodelta 1362 >EQt_bl >m_return_bind >EQt_fn1 % ] 1363 %{(mk_state_pc ? (increment_stack_usage p_out ssize st2_after) 1364 (pc_of_point p_out bl (joint_if_entry … t_fn1)) (last_pop … st2))} 1365 cases(bind_new_bind_new_instantiates' … Hdata1 Hprologue) Hprologue #st2' * #EQst2' 1366 #fin_sem_rel cases good1 #_ #_ #_ #_ #_ #_ #_ #_ #_ cases(entry_is_cost … (pi2 ?? fn1)) 1367 #nxt1 * #c #EQcost #H lapply(H … EQcost) H good1 normalize nodelta 1368 >(f_step_on_cost … data1) *** #pre1 #instr1 #post1 @eq_identifier_elim [2: * #H @⊥ @H %] 1369 #_ cases(added_prologue … data1) in EQst2'; normalize nodelta 1370 [ whd in ⊢ (??%% → ?); #EQ destruct(EQ) 1371  #hd #tl #EQst2' 1372 ] 1373 * whd in ⊢ (% → ?); inversion(f_regs ??) normalize nodelta [2,4: #x #y #_ #_ *] 1374 #EQf_regs #EQ [2: whd in EQ : (???%);] destruct(EQ) * #l1 * #mid1 * #mid2 * #l2 *** 1375 #EQmid1 whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in ⊢ (% → ?); * 1376 #nxt2 * [ #EQnop  #EQt_cost ] change with nxt2 in ⊢ (??%? → ?); #EQ destruct(EQ) 1377 whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2) 1378 [ * #star_lab * #Hstar_lab * #l1 * #mid1 * #mid2 * #l2 *** #EQmid1' whd in ⊢ (% → ?); 1379 * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in ⊢ (% → ?); * #nxt2 * #EQt_cost 1380 change with nxt2 in ⊢ (??%? → ?); #EQ destruct(EQ) #EQl2 1381  #EQentry 1382 ] 1383 whd in EQmid1 : (??%%); destruct(EQmid1) 1384 %{(mk_state_pc ? ? (pc_of_point p_out bl (joint_if_entry … fn1)) (last_pop … st2))} 1385 [ @st2' 3: @(increment_stack_usage p_out ssize st2_after)] 1386 >(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) in EQpre; #EQpre 1387 lapply(taaf_to_taa … (produce_trace_any_any_free … st2 f t_fn … EQpre … EQst2_pre) ?) 1388 [3,6: <(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) <EQpc' <pc_block_eq 1389 [2,4: inversion (sigma_pc_opt ?????????) [2,4: #x #_ % #ABS destruct(ABS) ] 1390 #ABS cases(fetch_statement_inv … EQfetch) <EQpc' 1391 >fetch_internal_function_no_zero [1,3: #EQ destruct] 1392 whd in match sigma_stored_pc; normalize nodelta >ABS %] 1393 >(pc_of_point_of_pc … pc') #taa1 %{taa1} 1394 1,4: @if_elim #_ [2,4: @I] % whd in ⊢ (% → ?); * #H @H H whd in ⊢ (??%?); 1395 <(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) <EQpc' <pc_block_eq 1396 [2,4: inversion (sigma_pc_opt ?????????) [2,4: #x #_ % #ABS destruct(ABS) ] 1397 #ABS cases(fetch_statement_inv … EQfetch) <EQpc' 1398 >fetch_internal_function_no_zero [1,3: #EQ destruct] 1399 whd in match sigma_stored_pc; normalize nodelta >ABS %] 1400 >(pc_of_point_of_pc … pc') whd in match (as_pc_of ??); >EQt_call 1401 >EQinstr % 1402 2,5: <(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) <EQpc' <pc_block_eq 1403 [2,4: inversion (sigma_pc_opt ?????????) [2,4: #x #_ % #ABS destruct(ABS) ] 1404 #ABS cases(fetch_statement_inv … EQfetch) <EQpc' 1405 >fetch_internal_function_no_zero [1,3: #EQ destruct] 1406 whd in match sigma_stored_pc; normalize nodelta >ABS %] 1407 @(proj1 … (fetch_statement_inv … EQt_call)) 1408 ] 1409 taa1 1410 [ letin trans_prog ≝ (b_graph_transform_program ????) 1411 lapply(produce_trace_any_any_free (mk_prog_params p_out trans_prog stack_size) 1412 (mk_state_pc ? (increment_stack_usage p_out ssize st2_after) 1413 (pc_of_point p_out bl mid2) (last_pop … st2)) … EQst2') 1414 [ >point_of_pc_of_point in ⊢ (????%???); @EQl2 1415  change with bl in match (pc_block ?); assumption 1416 *: 1417 ] 1418 #taaf %{(taaf_to_taa … (taa_append_taaf … (taa_step … (taa_base …) …) taaf) ?)} 1419 [1,2: [ @if_elim #_ [2: @I] ] % whd in ⊢ (% → ?); * #H @H H whd in ⊢ (??%?); 1420 whd in match (as_pc_of ??); whd in match fetch_statement; normalize nodelta 1421 >EQt_fn1 >m_return_bind whd in match point_of_pc; normalize nodelta 1422 >point_of_offset_of_point [ >EQnop %] cases EQl2 #mid * #rest ** 1423 #EQ destruct(EQ) * #nxt2 * #EQmid2 change with nxt2 in ⊢ (??%? → ?); 1424 #EQ destruct(EQ) #_ >EQmid2 % 1425 3,4: whd [ whd in ⊢ (??%?);  whd in match eval_state; ] 1426 whd in match fetch_statement; normalize nodelta 1427 >EQt_fn1 >m_return_bind >point_of_pc_of_point >EQt_cost [%] >m_return_bind 1428 whd in match eval_statement_no_pc; normalize nodelta >m_return_bind % 1429 ] 1430  >EQentry %{(taa_base …)} 1431 ] 1432 % 1433 [2,4: whd in ⊢ (??%%); whd in match (as_pc_of ??); whd in match (as_pc_of ??); 1434 whd in match fetch_statement; normalize nodelta >EQint_fn >EQt_fn1 1435 >m_return_bind >m_return_bind whd in match point_of_pc; normalize nodelta 1436 >point_of_offset_of_point >point_of_offset_of_point >EQcost >m_return_bind 1437 normalize nodelta >EQt_cost >m_return_bind [2: %] normalize nodelta 1438 whd in match get_first_costlabel; normalize nodelta whd in ⊢ (??%%); 1439 whd in match (get_first_costlabel_next ???); 1440 generalize in match (refl ??); 1441 >EQcost in ⊢ (∀e:???%. ???(??(???(match % return ? with [_ ⇒ ?  _ ⇒ ?]?)))); 1442 #EQcost' normalize nodelta % 1443 ] 1444 % 1445 [1,3: whd in match eval_state; normalize nodelta >EQt_call >m_return_bind 1446 whd in match eval_statement_no_pc; normalize nodelta >EQinstr normalize nodelta 1447 >m_return_bind whd in match eval_statement_advance; whd in match eval_call; 1448 normalize nodelta >EQt_bl >m_return_bind @('bind_inversion EQt_fn1) 1449 * #f2 * #fn2 #EQ normalize nodelta whd in ⊢ (??%% → ?); #EQ1 destruct(EQ1) 1450 >EQ EQ >m_return_bind normalize nodelta >EQst2_save >m_return_bind 1451 whd in match eval_internal_call; normalize nodelta whd in match (stack_sizes ????); 1452 >EQssize >m_return_bind >EQst2_after >m_return_bind [%] >EQentry % 1453 *: @(st_rel_def … good … fin_sem_rel …) [3,7: @EQint_fn 1,2,5,6:] 1454 @(fetch_stmt_ok_sigma_last_pop_ok … good … EQfetch) assumption 1455 ] 1456 qed. 1457 1458 lemma eval_call_premain_ok : ∀ P_in , P_out: sem_graph_params. 1459 ∀prog : joint_program P_in. 1460 ∀stack_size. 1461 ∀ f_lbls,f_regs.∀init_regs.∀init. 1462 ∀st_no_pc_rel,st_rel. 1463 let prog_pars_in ≝ mk_prog_params P_in prog stack_size in 1464 let trans_prog ≝ b_graph_transform_program P_in P_out init prog in 1465 let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_size in 1466 ∀good : good_state_relation P_in P_out prog stack_size init init_regs f_lbls f_regs 1467 st_no_pc_rel st_rel. 1468 ∀st1,st1' : joint_abstract_status prog_pars_in. 1469 ∀st2 : joint_abstract_status prog_pars_out. 1470 ∀f. 1471 ∀fn : joint_closed_internal_function P_in ?. 1472 ∀id,arg,dest,nxt. 1473 block_id … (pc_block (pc … st1)) = 1 → 1474 st_rel st1 st2 → 1475 fetch_statement P_in … 1476 (joint_globalenv P_in prog stack_size) (pc … st1) = 1477 return 〈f, fn,sequential P_in ? (CALL ?? id arg dest) nxt〉 → 1478 eval_state P_in … (ev_genv … prog_pars_in) 1479 st1 = return st1' → 1480 ∃is_call,st2_pre_call,t_is_call. 1481 as_call_ident (joint_abstract_status prog_pars_in) «st1,is_call» = 1482 as_call_ident (joint_abstract_status prog_pars_out) «st2_pre_call,t_is_call» ∧ 1483 (pc … st1) = sigma_stored_pc P_in P_out prog stack_size 1484 init init_regs f_lbls f_regs (pc … st2_pre_call) ∧ 1485 ∃st2_after_call,st2' : joint_abstract_status prog_pars_out. 1486 ∃taa2 : trace_any_any … st2 st2_pre_call. 1487 ∃taa2' : trace_any_any … st2_after_call st2'. 1488 eval_state P_out … (joint_globalenv P_out trans_prog stack_size) st2_pre_call = 1489 return st2_after_call ∧ 1490 st_rel st1' st2' ∧ 1491 as_label (joint_abstract_status prog_pars_in) st1' = 1492 as_label (joint_abstract_status prog_pars_out) st2_after_call. 1493 #p_in #p_out #prog #stack_size #f_lbls #f_regs #init_regs #init #st_no_pc_rel #st_rel 1494 #good #st1 #st1' #st2 #f #fn #id #arg #dest #nxt #EQbl #Rst1st2 #EQfetch #EQeval 1495 % [ whd in ⊢ (??%?); >EQfetch %] %{st2} cases(pre_main_ok … good … EQbl EQeval Rst1st2) 1496 #Hclass * #st2' ** #Rst1st2' #EQst2' #Hlab % 1497 [ change with (joint_classify ???) in ⊢ (??%?); <Hclass whd in ⊢ (??%?); >EQfetch %] 1498 % [ % [2: whd in match sigma_stored_pc; whd in match sigma_pc_opt; normalize nodelta 1499 <(fetch_stmt_ok_sigma_pc_ok … good … Rst1st2 EQfetch) >EQbl % ] 1500  %{st2'} %{st2'} %{(taa_base …)} %{(taa_base …)} % [%{EQst2' Rst1st2'}] 1501 assumption 1502 ] 1503 whd in ⊢ (??%%); >EQfetch in ⊢ (??(match % with [_ ⇒ ?  _ ⇒ ?])?); normalize nodelta 1504 lapply Hclass whd in ⊢ (??%% → ?); >EQfetch in ⊢ (% → ?); whd in match joint_classify_step; 1505 normalize nodelta inversion(fetch_statement ????) [2: #e #_ normalize nodelta #EQ destruct] 1506 ** #f' #fn' * 1507 [ * [ #c  #id' #arg' #dest'  #r #lbl  #seq ] #nxt  * [ #lb  #h #id' #arg']  *] 1508 #EQt_fetch whd in ⊢ (??%% → ?); #EQ destruct normalize nodelta @('bind_inversion EQeval) 1509 #x >EQfetch whd in ⊢ (??%% → ?); #EQ destruct(EQ) whd in match eval_statement_no_pc; 1510 normalize nodelta >m_return_bind whd in match eval_statement_advance; 1511 whd in match eval_call; normalize nodelta #H @('bind_inversion H) H #bl #H 1512 lapply(err_eq_from_io ????? H) H #EQbl #H @('bind_inversion H) H * #f1 1513 * #fn1 #H lapply(err_eq_from_io ????? H) H #EQfn1 normalize nodelta 1514 [2: #H @('bind_inversion H) H #st whd in match eval_external_call; normalize nodelta 1515 #H @('bind_inversion H) H #x #_ #H @('bind_inversion H) H #y #_ 1516 #H @('bind_inversion H) H #z whd in ⊢ (??%% → ?); #EQ destruct(EQ) ] 1517 #H lapply(err_eq_from_io ????? H) H #H @('bind_inversion H) H #st1_save 1518 #_ #H @('bind_inversion H) H #st1_fin #_ whd in ⊢ (??%% → ?); #EQ destruct(EQ) 1519 >EQbl >m_return_bind whd in match fetch_internal_function; normalize nodelta 1520 >EQfn1 >m_return_bind normalize nodelta @('bind_inversion EQst2') #x 1521 >EQt_fetch whd in ⊢ (??%% → ?); #EQ destruct(EQ) whd in match eval_statement_no_pc; 1522 normalize nodelta >m_return_bind whd in match eval_statement_advance; 1523 whd in match eval_call; normalize nodelta #H @('bind_inversion H) H 1524 #bl' >set_no_pc_eta #H lapply(err_eq_from_io ????? H) H #EQbl' 1525 #H @('bind_inversion H) H * #f1' * #fn1' #H lapply(err_eq_from_io ????? H) H 1526 #EQfn1' normalize nodelta 1527 [2: #H @('bind_inversion H) H #st whd in match eval_external_call; normalize nodelta 1528 #H @('bind_inversion H) H #x #_ #H @('bind_inversion H) H #y #_ 1529 #H @('bind_inversion H) H #z whd in ⊢ (??%% → ?); #EQ destruct(EQ) ] 1530 #H lapply(err_eq_from_io ????? H) H #H @('bind_inversion H) H 1531 #st2_save #_ #H @('bind_inversion H) H #st2_fin #_ whd in ⊢ (??%% → ?); 1532 #EQ destruct(EQ) >EQbl' >m_return_bind >EQfn1' >m_return_bind normalize nodelta 1533 lapply(fetch_ok_pc_ok … good … Rst1st2' ?) 1534 [ whd in match fetch_internal_function; normalize nodelta >EQfn1 in ⊢ (??%?); % 1535 *: 1536 ] 1537 whd in match pc_of_point in ⊢ (% → ?); normalize nodelta #EQ destruct(EQ) 1538 lapply EQfn1 whd in match fetch_function; normalize nodelta 1539 @eqZb_elim [ #ABS @⊥ cases(block_of_call_no_minus_one … EQbl) #H @H assumption] 1540 #Hbl' normalize nodelta #H lapply(opt_eq_from_res ???? H) H #H @('bind_inversion H) 1541 #f2 #EQf2 #H @('bind_inversion H) H #fn2 #_ whd in ⊢ (??%? → ?); e0 EQ 1542 #EQ destruct(EQ) H lapply EQfn1' whd in match fetch_function; normalize nodelta 1543 @eqZb_elim [ #ABS >ABS in Hbl'; * #H @⊥ @H %] #_ normalize nodelta 1544 #H lapply(opt_eq_from_res ???? H) H 1545 whd in match joint_globalenv in ⊢ (% → ?); normalize nodelta 1546 whd in match b_graph_transform_program in ⊢ (% → ?); normalize nodelta 1547 whd in match transform_joint_program; normalize nodelta 1548 >(symbol_for_block_transf ??? (λx.x) prog 1549 (λvars.transf_fundef ?? (λdef_in.b_graph_translate ??? (init ? def_in) def_in)) bl') in ⊢ (% → ?); 1550 >EQf2 >m_return_bind in ⊢ (% → ?); #H @('bind_inversion H) H #fn2' #_ 1551 whd in ⊢ (??%% → ?); #EQ destruct(EQ) % 1552 qed. 1553 1554 1555 lemma pair_dep_match_elim : ∀A,B,C : Type[0].∀P : C → Prop.∀t:A×B. 1556 ∀c. 1557 (∀x,y,prf.P (c x y prf)) → 1558 P (let 〈x,y〉 as prf ≝ t in c x y prf). 1559 #A #B #C #P * // qed. 1788 1560 1789 1561 theorem joint_correctness : ∀p_in,p_out : sem_graph_params. … … 1796 1568 good_state_relation p_in p_out prog stack_size init init_regs 1797 1569 f_lbls f_regs st_no_pc_rel st_rel → 1570 good_init_relation p_in p_out prog stack_size init st_no_pc_rel → 1798 1571 let trans_prog ≝ b_graph_transform_program … init prog in 1799 1572 ∀init_in.make_initial_state (mk_prog_params p_in prog stack_size) = OK ? init_in → … … 1804 1577 (joint_abstract_status (mk_prog_params p_out trans_prog stack_size)) 1805 1578 R init_in init_out. 1806 cases daemon 1579 #p_in #p_out #prog #stack_size #init #init_regs #f_lbls #f_regs #st_no_pc_rel 1580 #st_rel #good #good_init #init_in whd in match make_initial_state; normalize nodelta 1581 #H @('bind_inversion H) H #init_m #EQinit_m @pair_dep_match_elim #m #bl #prf 1582 whd in ⊢ (??%% → ?); #EQ destruct(EQ) 1583 letin trans_prog ≝ (b_graph_transform_program ????) 1584 letin globals_size ≝ (globals_stacksize … trans_prog) 1585 letin spp ≝ 1586 («mk_pointer bl (mk_offset (bitvector_of_Z 16 (S (globals_size)))), 1587 pi2 … bl») 1588 letin st ≝ (mk_state p_out 1589 (* frames ≝ *)(Some ? (empty_framesT …)) 1590 (* internal_stack ≝ *) empty_is 1591 (* carry ≝ *)(BBbit false) 1592 (* regs ≝ *)(empty_regsT … spp) 1593 (* mem ≝ *)m 1594 (* stack_usage ≝ *)0) 1595 %{(mk_state_pc ? (set_sp … spp st) init_pc (null_pc one))} >init_mem_transf 1596 >EQinit_m >m_return_bind @pair_dep_match_elim #m1 #bl1 #prf' lapply prf 1597 lapply prf' lapply prf' <prf in ⊢ (%→?); #EQ destruct(EQ) prf' #prf' #_ 1598 %{(refl …)} %{(JointStatusSimulation … good)} % 1599 [ whd @(st_rel_def … good) 1600 [3: % 1,2: 1601  lapply(good_empty ?????? good_init ? EQinit_m) <prf' normalize nodelta #H @H 1602  % 1603 ] 1604  whd whd in ⊢ (??%%); lapply(good_init_cost_label … good_init) normalize nodelta 1605 cases(fetch_statement ????) normalize nodelta 1606 [2: #e * [ *#e' #EQ >EQ %  * #x * #EQ #EQ1 >EQ normalize nodelta >EQ1 % ] ] 1607 #x cases(cost_label_of_stmt ???) normalize nodelta 1608 [ * [ * #e' #EQ >EQ %  * #y * #EQ1 #EQ2 >EQ1 normalize nodelta >EQ2 %] 1609  #c * #y * #EQ1 #EQ2 >EQ1 normalize nodelta >EQ2 % 1610 ] 1611 ] 1612 % 1613 [ #st1 #st1' #st2 whd in ⊢ (% → ?); #EQeval @('bind_inversion EQeval) 1614 ** #f #fn #stmt #H lapply(err_eq_from_io ????? H) H cases stmt stmt 1615 [ * [ #c  #id #arg #dest  #r #lb  #seq ] #nxt  #fin  * ] #EQfetch #_ 1616 whd in ⊢ (% → ?); #Rst1st2 1617 change with (joint_classify ???) in 1618 ⊢ (match % with [ _ ⇒ ?  _ ⇒ ?  _ ⇒ ?  _ ⇒ ?  _ ⇒ ? ]); 1619 [ whd in match joint_classify; normalize nodelta >EQfetch normalize nodelta 1620 cases(decidable_eq_Z (block_id (pc_block … (pc … st1))) (neg one)) #Hbl 1621 [ cases(general_eval_cost_premain_ok … good … Hbl Rst1st2 EQfetch EQeval) 1622  cases(general_eval_cost_ok … good … Hbl Rst1st2 EQfetch EQeval) 1623 ] #st2' * #Rst1st2' * #taaf * #H #H1 %{st2'} %{taaf} >H % [1,3: %{I} assumption] 1624 assumption 1625  whd in match joint_classify; normalize nodelta >EQfetch normalize nodelta #prf 1626 cases(decidable_eq_Z (block_id (pc_block … (pc … st1))) (neg one)) #Hbl 1627 [ cases(eval_call_premain_ok … good … Hbl Rst1st2 EQfetch EQeval) 1628  cases(eval_call_ok … good … Hbl Rst1st2 EQfetch EQeval) 1629 ] 1630 #prf' * #st2_pre * #prf'' ** #EQ #EQ1 * #st2_after * #st2' * #taa * #taa1 ** #EQ2 #H #EQ3 1631 %{st2_pre} [1,3: assumption] % [1,3: % [1,3: >EQ % *: assumption ] ] 1632 %{st2_after} %{st2'} %{taa} %{taa1} % [1,3: %{EQ2 H}] assumption 1633  whd in match joint_classify; normalize nodelta >EQfetch normalize nodelta 1634 #ncost cases(decidable_eq_Z (block_id (pc_block … (pc … st1))) (neg one)) #Hbl 1635 [ cases(eval_cond_premain_ok … good … Hbl Rst1st2 EQfetch EQeval ncost) 1636  cases(eval_cond_ok … good … Hbl Rst1st2 EQfetch EQeval ncost) 1637 ] 1638 #st2' * #H * #taaf * #H1 #H2 %{st2'} %{taaf} >H1 % [1,3: %{I} assumption] 1639 assumption 1640  whd in match joint_classify; normalize nodelta >EQfetch normalize nodelta 1641 cases(decidable_eq_Z (block_id (pc_block … (pc … st1))) (neg one)) #Hbl 1642 [ cases(general_eval_seq_no_call_premain_ok … good … Hbl Rst1st2 EQfetch EQeval) 1643  cases(general_eval_seq_no_call_ok … good … Hbl Rst1st2 EQfetch EQeval) 1644 ] 1645 #st2' * #H * #taaf * #H1 #H2 %{st2'} %{taaf} % [ >H1 %{I H} 3: %{H1 H} ] 1646 assumption 1647 ] 1648  @(as_result_ok … good) 1649 ] 1650 cases fin in EQfetch; fin 1651 [ #lb #EQfetch whd in match joint_classify; normalize nodelta >EQfetch 1652 normalize nodelta 1653 cases(decidable_eq_Z (block_id (pc_block … (pc … st1))) (neg one)) 1654 #Hbl 1655 [ cases(eval_goto_premain_ok … good … Hbl Rst1st2 EQfetch EQeval) 1656  cases(eval_goto_ok … good … Hbl Rst1st2 EQfetch EQeval) 1657 ] 1658 #st2' * #H * #taaf * #H1 #H2 %{st2'} %{taaf} >H1 % [1,3: %{I H}] assumption 1659  #EQfetch whd in match joint_classify; normalize nodelta >EQfetch 1660 normalize nodelta 1661 cases(decidable_eq_Z (block_id (pc_block … (pc … st1))) (neg one)) 1662 #Hbl 1663 [ @⊥ @(pre_main_no_return … good … Hbl … EQfetch) ] 1664 cases(eval_return_ok … good … Hbl Rst1st2 EQfetch EQeval) #st2_pre * #st2_after 1665 * #st2' * #taa * #taaf ***** #H #H1 #H2 #H3 #H4 #H5 %{st2_pre} %{st2_after} 1666 %{st2'} %{taa} %{taaf} % [2: assumption] % [2: assumption] % [2: assumption] 1667 % [2: assumption] %{H H1} 1668  #has #id #arg #EQfetch whd in match joint_classify; normalize nodelta 1669 >EQfetch normalize nodelta 1670 cases(decidable_eq_Z (block_id (pc_block … (pc … st1))) (neg one)) 1671 #Hbl 1672 [ cases(eval_tailcall_premain_ok … good … Hbl Rst1st2 EQfetch EQeval) 1673  cases(eval_tailcall_ok … good … Hbl Rst1st2 EQfetch EQeval) 1674 ] 1675 #prf * #st2_pre * #t_is_call * #H * #st2_after * #st2' * #taa1 * #taa2 1676 ** #H1 #H2 #H3 #prf' %{st2_pre} [1,3: assumption] %{H} %{st2_after} %{st2'} 1677 %{taa1} %{taa2} % [2,4: assumption] %{H1 H2} 1678 ] 1807 1679 qed. 1808 1680 1809
Note: See TracChangeset
for help on using the changeset viewer.