Changeset 2662
 Timestamp:
 Feb 12, 2013, 6:56:41 PM (6 years ago)
 File:

 1 edited
Legend:
 Unmodified
 Added
 Removed

src/ERTLptr/ERTLtoERTLptrOK.ma
r2645 r2662 84 84 qed. 85 85 86 (*87 lemma sigma_is_pop_commute :88 ∀prog,sigma,is,bv,is'.89 is_pop (sigma_is prog sigma is) =90 return 〈sigma_beval prog sigma bv,sigma_is prog sigma is'〉 →91 is_pop is = return 〈bv,is'〉.92 93 94 ∀prf : sigma_is_opt prog sigma is ≠ None ?.95 res_preserve …96 (λpr.sigma_beval_opt prog sigma (\fst pr) ≠ None ? ∧97 sigma_is_opt prog sigma (\snd pr) ≠ None ?)98 (λpr,prf.〈sigma_beval … (proj1 … prf), sigma_is … (proj2 … prf)〉)99 (is_pop is) (is_pop (sigma_is … prf)).100 #prog #sigma * [#bv1#bv1 #bv2] #prf101 [ @res_preserve_error102 *:103 whd in match sigma_is in ⊢ (?????????%); normalize nodelta104 @opt_safe_elim #is'105 #H @('bind_inversion H) H #bv1' #EQ1106 [2: #H @('bind_inversion H) H #bv2' #EQ2 ]107 whd in ⊢ (??%%→?); #EQ destruct(EQ)108 @mfr_return_eq109 [1,3: @hide_prf %%110 *: whd in match sigma_beval; whd in match sigma_is;111 normalize nodelta @opt_safe_elim #bv1'' @opt_safe_elim #is''112 ]113 [2,4,5,6: whd in match sigma_is_opt; normalize nodelta [1,3: >EQ1 ]114 whd in ⊢ (??%%→?); #EQ destruct(EQ) ]115 [1,3: >EQ2 *: >EQ1 ] #EQ' destruct(EQ') %116 ]117 qed.118 119 definition well_formed_mem :120 ∀prog : ertl_program.121 sigma_map prog →122 bemem → Prop ≝123 λprog,sigma,m.124 ∀b,z.block_id b < nextblock m → low_bound m b ≤ z → z < high_bound m b →125 sigma_beval_opt prog sigma (contents (blocks m b) z) ≠ None ?.126 *)127 128 129 86 definition sigma_mem : 130 87 ∀prog : ertl_program . sigma_map prog → bemem → bemem ≝ … … 142 99 (nextblock m) 143 100 (nextblock_pos m). 144 (* 145 @hide_prf 146 lapply prf'' lapply prf' prf' prf'' 147 @Zltb_elim_Type0 [2: #_ * ] 148 #bid_ok * 149 @Zleb_elim_Type0 [2: #_ * ] 150 @Zltb_elim_Type0 [2: #_ #_ * ] 151 #zh #zl * @(prf … bid_ok zl zh) 152 qed. 153 *) 154 155 (*DOPPIONI DEI CORRISPONDENTI LEMMI IN LINEARISE_PROOF.MA *) 156 (*lemma andb_false : ∀b1,b2.andb b1 b2 = false → b1 = false ∨ b2 = false. 157 ** /2 by or_introl, or_intror/ normalize #ABS destruct(ABS) qed. 158 *) 159 101 102 (*DOPPIONE ASSIOMA IN LINEARISE_PROOF.MA *) 160 103 axiom mem_ext_eq : 161 104 ∀m1,m2 : mem. … … 166 109 nextblock m1 = nextblock m2 → m1 = m2. 167 110 168 (*169 170 lemma beloadv_sigma_commute:171 ∀prog,sigma,ptr.172 preserving … opt_preserve …173 (sigma_mem prog sigma)174 (sigma_beval prog sigma)175 (λm.beloadv m ptr)176 (λm.beloadv m ptr).177 #prog #sigma #ptr #m #prf #bv178 whd in match beloadv;179 whd in match do_if_in_bounds;180 whd in match sigma_mem;181 normalize nodelta182 @If_elim #block_ok >block_ok normalize nodelta183 [2: whd in ⊢ (???%→?); #ABS destruct(ABS) ]184 @If_elim #H185 [ elim (andb_true … H)186 #H1 #H2187 whd in match sigma_beval; normalize nodelta188 @opt_safe_elim #bv' #EQ_bv' >H1 >H2 normalize nodelta189 whd in ⊢ (???%→?); #EQ' destruct190 >EQ_bv' % [ % #ABS destruct(ABS) ] @opt_to_opt_safe191  elim (andb_false … H) H #H >H192 [2: >commutative_andb ] normalize nodelta193 whd in ⊢ (???%→?); #ABS destruct(ABS)194 ]195 qed.196 197 include alias "common/GenMem.ma".198 199 lemma bestorev_sigma_commute :200 ∀prog,sigma,ptr.201 preserving2 ?? opt_preserve …202 (sigma_mem prog sigma)203 (sigma_beval prog sigma)204 (sigma_mem prog sigma)205 (λm.bestorev m ptr)206 (λm.bestorev m ptr).207 #prog #sigma #ptr #m #bv #prf1 #prf2 #m'208 whd in match bestorev;209 whd in match do_if_in_bounds;210 whd in match sigma_mem;211 whd in match update_block;212 normalize nodelta213 @If_elim #block_ok >block_ok normalize nodelta214 [2: whd in ⊢ ((???%) → ?); #ABS destruct(ABS)]215 @Zleb_elim_Type0 #H1216 [ @Zltb_elim_Type0 #H2 ]217 [2,3: #ABS normalize in ABS; destruct(ABS) ]218 normalize nodelta whd in ⊢ (???%→?); #EQ destruct(EQ)219 %220 [2: whd in ⊢ (???%);221 @eq_f222 @mem_ext_eq [2: % ]223 #b @if_elim224 [2: #B225 @If_elim #prf1 @If_elim #prf2226 [2,3: @⊥ >prf1 in prf2; * /2 by I/ ] [2: % [%%] #z % ]227 whd in match low_bound; whd in match high_bound;228 normalize nodelta229 cut (Not (bool_to_Prop (eq_block b (pblock ptr))))230 [ % #ABS >ABS in B; * ]231 B #B % [ >B %% ] #z232 @If_elim #prf3233 @If_elim #prf4234 [2,3: @⊥ >B in prf4; normalize nodelta >prf3 * /2 by I/ 4: % ]235 whd in match sigma_beval in ⊢ (??%%); normalize nodelta236 @opt_safe_elim @opt_safe_elim #bv1 #EQ1 #bv2 #EQ2 >B in EQ1;237 >EQ2 #EQ destruct(EQ) %238  #B cut (b = pblock ptr) [ lapply B @eq_block_elim // #_ * ]239 #EQ destruct(EQ)240 @If_elim whd in match low_bound; whd in match high_bound;241 normalize nodelta242 [2: >block_ok * #ABS elim (ABS I) ]243 #prf3 % [ >B %% ]244 #z whd in match update; normalize nodelta245 @eqZb_elim normalize nodelta #prf4246 [2: @If_elim #prf5 @If_elim #prf6247 [2,3: @⊥ >B in prf6; >prf5 * /2 by I/ 4: % ]248 whd in match sigma_beval in ⊢ (??%%); normalize nodelta249 @opt_safe_elim @opt_safe_elim #bv1 #EQ1 #bv2 #EQ2 >B in EQ1;250 normalize nodelta >(eqZb_false … prf4) >EQ2251 #EQ destruct(EQ) %252  @If_elim #prf5253 [2: >B in prf5; normalize nodelta254 >prf4 >(Zle_to_Zleb_true … H1) >(Zlt_to_Zltb_true … H2) * #ABS elim (ABS I) ]255 whd in match sigma_beval in ⊢ (??%%); normalize nodelta256 @opt_safe_elim @opt_safe_elim #bv1 #EQ1 #bv2 #EQ2 >B in EQ1;257 normalize nodelta >prf4 >eqZb_z_z >EQ2 #EQ destruct(EQ) %258 ]259 ]260  whd #b #z #h1 whd in match low_bound; whd in match high_bound; normalize nodelta261 @eq_block_elim #H normalize nodelta destruct262 #h2 #h3 whd in match update; normalize nodelta263 [ @eqZb_elim #H destruct normalize nodelta [ assumption ]]264 @prf1 assumption265 ]266 qed.267 268 include alias "common/Identifiers.ma".269 include alias "common/PositiveMap.ma".270 271 let rec map_inf A B (b : positive_map A) on b :272 (∀a : A.(Σp:Pos. lookup_opt A p b = Some ? a) → B) → positive_map B ≝273 λf.274 (match b return λx.x=b → ? with275 [ pm_leaf ⇒ λ_.pm_leaf ?276  pm_node a l r ⇒ λprf.pm_node ?277 ((match a return λx.a=x→? with278 [Some x ⇒ λprf1.return f x «one,?»279 None ⇒ λ_.None ?280 ]) (refl ? a))281 (map_inf ?? l (λa1,prf1.f a1 «p0 ?,?»))282 (map_inf ?? r (λa1,prf1.f a1 «p1 ?,?»))283 ]) (refl ? b).284 [ @hide_prf <prf normalize assumption285 *: [1,3: @hide_prf] cases prf1 #tl #H [4,3 : @tl] <prf assumption286 ] qed.287 288 289 definition map_inf1 : ∀A, B: Type[0].290 ∀tag: identifierTag.291 ∀m:identifier_map tag A.292 (∀a:A.(Σid. lookup tag A m id = Some A a) → B) →293 identifier_map tag B ≝294 λA,B,tag,m.295 (match m return λx.(∀a:A.(Σid. lookup tag A x id = Some A a) → B) → ? with296 [an_id_map b ⇒ λF.an_id_map …297 (map_inf A B b (λa,prf.F a «an_identifier tag ?,?»))]).298 [@hide_prf] cases prf #pos #H assumption299 qed.300 301 lemma ext_map_inf_eq : ∀A , B : Type[0].302 ∀ m : positive_map A.303 ∀ F, F' : (∀a:A.(Σp:Pos. lookup_opt A p m = Some ? a) → B).304 (∀a',id',id'',prf,prf'. F a' «id',prf» = F' a' «id'',prf'») →305 map_inf A B m F = map_inf A B m F'.306 #A #B #m elim m [#F #F' #eqFF' %] * [2:#a] normalize nodelta #l #r #Hl #Hr #F #F'307 #eqFF' normalize [>(eqFF' a one one (refl ? (Some A a)) (refl ? (Some A a)))]308 @eq_f2 [1,3: @Hl *: @Hr] #a' #id' #id'' #prf' #prf'' @eqFF'309 qed.310 311 312 lemma map_inf_add : ∀ A, B : Type[0].313 ∀tag : identifierTag.314 ∀m: identifier_map tag A.315 ∀F :(∀a:A.(Σid. lookup tag A m id = Some A a) → B).316 ∀a,id.317 let m' ≝ (add tag A m id a) in318 ∀F' :(∀a:A.(Σid. lookup tag A m' id = Some A a) → B).319 (∀a',id',id'',prf,prf'. F a' «id',prf» = F' a' «id'',prf'») →320 ∃ prf.321 map_inf1 A B tag m' F' =322 add tag B (map_inf1 A B tag m F) id (F' a «id,prf»).323 #A #B #tag #m #F #a #id normalize nodelta #F' #eqFF' %324 [@hide_prf @(lookup_add_hit tag A m ? ?)]325 lapply eqFF' eqFF' lapply F' F' lapply id id lapply a a lapply F F326 cases m m #m elim m327 [ #F #a * #id elim id [#F' #eqFF' %] #x #Hx #F' #eqFF' whd in ⊢ (??%%);328 normalize nodelta @eq_f whd in match insert; normalize nodelta329 whd in ⊢ (??%%); normalize nodelta @eq_f2 try %330 lapply(Hx ??)331 [2,5: #a1 ** #id1 #prf1 @F' [1,3: @a1]332 [%{(an_identifier tag (p1 id1))} %{(an_identifier tag (p0 id1))}] @prf1333 1,4: #a' * #id' * #id'' #prf #prf' normalize nodelta @eqFF'334 *: normalize nodelta whd in ⊢ (??%% → ?); normalize nodelta #EQ destruct(EQ)335 lapply e0 e0 whd in ⊢ (??%% → ?); normalize nodelta normalize in ⊢ (??(???%?)? → ?);336 #EQ <EQ %337 ]338  #opt_a #l1 #r1 #Hl1 #Hr1 #F #a ** [*: #x] #F' #eqFF'339 [ normalize @eq_f @eq_f2 @ext_map_inf_eq #a' #id' #id'' #prf' #prf'' >eqFF' [1,4:%*:]340 *: normalize @eq_f lapply eqFF' eqFF' lapply F' F' lapply F F cases opt_a341 [2,4: #a1] normalize nodelta #F #F' #eqFF'342 [3,4: @eq_f2*: >(eqFF' a1 (an_identifier tag one) (an_identifier tag one)343 (refl (option A) (Some A a1)) (refl (option A) (Some A a1)))344 @eq_f2]345 [1,4,5,8: @ext_map_inf_eq #a' #id' #id'' #prf' #prf'' >eqFF' [1,4,7,10:%*:]346 2,6: lapply (Hr1 ? a (an_identifier tag x) ? ?)347 *: lapply (Hl1 ? a (an_identifier tag x) ? ?)348 ]349 [2,3,6,7,10,11,14,15: #a ** #id #prf [2,4,6,8: @F *: @F'] try @a %350 [1,3,9,11: % @(p1 id) 5,7,13,15: % @(p0 id) *: @hide_prf <prf %]351 1,5,9,13: #a * #id' * #id'' #prf #prf' normalize nodelta @eqFF'352 *: normalize in ⊢ (%→ ?); #EQ destruct(EQ) >e0 %353 ]354 ]355 ]356 qed.357 *)358 111 359 112 … … 371 124 [an_id_map p ⇒ id_is_in A x p] 372 125 ]. 373 (* 374 lemma lookup_map : ∀A,B : Type[0]. 375 ∀tag : identifierTag. 376 ∀m : identifier_map tag A. 377 ∀ F : (∀a:A.(Σid. lookup tag A m id = Some A a) → B). 378 ∀ id,opt_a. lookup tag A m id =opt_a → 379 lookup tag B (map_inf1 A B tag m F) id = 380 (match opt_a return λx.opt_a = x→ ? with 381 [Some a ⇒ λprf.Some ? (F a «id,?») 382 None ⇒ λ_.None ? 383 ])(refl ? (opt_a)). 384 [2: @hide_prf //] 385 #A #B #tag * #m elim m [2: * [2: #a] #l #r #Hl #Hr] #F ** [1,4,7: *: #x] 386 * [2,4,6,8,10,12,14,16,18: #a1] normalize in ⊢ (% → ?); [1,2,3,8,9,10: #EQ destruct] 387 // normalize nodelta 388 #EQ 389 [1,3: lapply(Hr ? (an_identifier tag x) (Some ? a1) EQ) 390 [1,3: #a2 * * #id2 #id2_spec @F [1,3: @a2 *: %{(an_identifier tag (p1 id2))} <id2_spec %]] 391 2,4: lapply(Hl ? (an_identifier tag x) (Some ? a1) EQ) 392 [1,3: #a2 * * #id2 #id2_spec @F [1,3: @a2 *: %{(an_identifier tag (p0 id2))} <id2_spec %]] 393 5,7: lapply(Hr ? (an_identifier tag x) (None ?) EQ) 394 [1,3: #a2 * * #id2 #id2_spec @F [1,3: @a2 *: %{(an_identifier tag (p1 id2))} <id2_spec %]] 395 6,8: lapply(Hl ? (an_identifier tag x) (None ?) EQ) 396 [1,3: #a2 * * #id2 #id2_spec @F [1,3: @a2 *: %{(an_identifier tag (p0 id2))} <id2_spec %]] 397 ] normalize #EQ1 <EQ1 % 398 qed. 399 400 (* 401 lemma lookup_map_weak : ∀ A,B : Type[0]. 402 ∀tag : identifierTag. 403 ∀m : identifier_map tag A. 404 ∀ F : (∀a:A.(Σid. lookup tag A m id = Some A a) → B). 405 ∀ id,a,prf. 406 lookup tag B (map_inf1 A B tag m F) id = Some ? (F a «id,prf»). 407 #A #B #tag #m #F #id #a #prf >(lookup_map … prf) normalize % 408 qed. 409 410 411 lemma lookup_map_fail : ∀A,B : Type[0]. 412 ∀tag : identifierTag. 413 ∀m : identifier_map tag A. 414 ∀ F : (∀a:A.(Σid. lookup tag A m id = Some A a) → B). 415 ∀ id. lookup tag A m id = None ? → 416 lookup tag B (map_inf1 A B tag m F) id = None ?. 417 cases daemon 418 qed.*) 419 420 *) 421 126 422 127 lemma lookup_eq : ∀ A : Type[0]. 423 128 ∀m,m' : positive_map A. … … 529 234 qed. 530 235 531 532 236 lemma update_ok_to_lookup : ∀ A : Type[0]. 533 237 ∀ tag : identifierTag. … … 582 286 ] 583 287 qed. 288 289 584 290 (* 585 291 … … 1069 775 fresh_for_univ … reg (joint_if_runiverse … def_out))) (f_regs l)) 1070 776 ; multi_fetch_ok : let def_out ≝ translate_internal … def_in in 1071 ∀f_step,f_fin.∀l,s.stmt_at … (joint_if_code … def_in) l = Some ? s → 777 let f_step ≝ translate_step ? in 778 let f_fin ≝ translate_fin_step ? in 779 ∀l,s.stmt_at … (joint_if_code … def_in) l = Some ? s → 1072 780 ∃lbls,regs.f_lbls l = Some ? lbls ∧ f_regs l = Some ? regs ∧ 1073 781 match s with … … 1875 1583 set_sp ? ptr (sigma_state prog good st restr) = 1876 1584 sigma_state prog good (set_sp ? ptr st) restr. 1877 cases daemon 1585 #prog #good #restr #ptr #st whd in match set_sp; whd in match sigma_state; 1586 normalize nodelta @eq_f2 [2: %] whd in match (save_sp ???); 1587 whd in match (save_sp ???); whd in match sigma_regs; normalize nodelta 1588 cases(regs ? st) #psd_env #hw_regs normalize nodelta @eq_f 1589 whd in match hwreg_store_sp; normalize nodelta whd in match sigma_hw_register_env; 1590 normalize nodelta whd in match hwreg_store; normalize nodelta @eq_f2 [2: %] 1591 >insert_map @eq_f >insert_map % 1878 1592 qed. 1879 1593 … … 1913 1627 ] 1914 1628  #i 1915 change with (member ? ? ? (((prog_var_names (joint_function ERTL)) ℕ prog)) → ?)1916 1629 #i_spec 1917 1630 change with ((dpl_reg ERTL) → ?) … … 2052 1765 qed. 2053 1766 2054 2055 xxxxxxxxxxxxxxxxx 1767 lemma partial_inj_sigma : ∀ prog : ertl_program. 1768 ∀good : (∀fn.good_state_transformation prog fn). 1769 let sigma ≝ (get_sigma_from_good_state … good) in 1770 ∀fn,lbl1,lbl2. sigma fn lbl1 ≠ None ? → sigma fn lbl1 = sigma fn lbl2 → lbl1 = lbl2. 1771 #prog #good #fn #lbl1 #lbl2 inversion(get_sigma_from_good_state … lbl1) 1772 [#_ * #H @⊥ @H %] #lbl1' whd in match get_sigma_from_good_state; normalize nodelta 1773 #H @('bind_inversion H) H * #lbl1'' #stmt1 #H1 whd in ⊢ (??%? → ?); #EQ destruct 1774 #_ #H lapply(sym_eq ??? H) H #H @('bind_inversion H) H * #lbl2' #stmt2 #H2 1775 whd in ⊢ (??%? → ?); #EQ destruct lapply(find_predicate ?????? H1) 1776 lapply(find_predicate ?????? H2) cases(f_lbls ????) normalize nodelta [*] 1777 * normalize nodelta 1778 [@eq_identifier_elim #EQ1 * @eq_identifier_elim #EQ2 * >EQ1 >EQ2 % ] 1779 #lb #tl @eq_identifier_elim #EQ1 * @eq_identifier_elim #EQ2 * >EQ1 >EQ2 % 1780 qed. 1781 1782 lemma pc_of_label_eq : 1783 ∀p,p'.let pars ≝ make_sem_graph_params p p' in 1784 ∀globals,ge,bl,i_fn,lbl. 1785 fetch_internal_function ? ge bl = return i_fn → 1786 pc_of_label pars globals ge bl lbl = 1787 OK ? (pc_of_point ERTL_semantics bl lbl). 1788 #p #p' #globals #ge #bl #i_fn #lbl #EQf 1789 whd in match pc_of_label; 1790 normalize nodelta >EQf >m_return_bind % 1791 qed. 1792 1793 lemma pop_ra_ok : 1794 ∀prog : ertl_program. 1795 ∀good : (∀fn.good_state_transformation prog fn). 1796 ∀restr. 1797 preserving1 … res_preserve1 … 1798 (λst.sigma_state prog good st restr) 1799 (λx.let 〈st,pc〉 ≝ x in 1800 let sigma ≝ (get_sigma_from_good_state … good) in 1801 〈sigma_state prog good st restr, 1802 sigma_stored_pc ? sigma pc〉) 1803 (pop_ra ERTL_semantics) 1804 (pop_ra ERTLptr_semantics). 1805 #prog #good #restr #st whd in match pop_ra; normalize nodelta @mfr_bind1 1806 [  @pop_ok ] * #bv #st1 @mfr_bind1 [  @pop_ok] * #bv1 #st2 @mfr_bind1 1807 [ @(sigma_stored_pc ? (get_sigma_from_good_state … good)) 1808  whd in match pc_of_bevals; normalize nodelta 1809 cases bv [   #ptr1 #ptr2 #p  #by  #p  #ptr #p  #pc #p] 1810 whd in match sigma_beval; normalize nodelta try @res_preserve_error1 1811 inversion(sigma_pc_opt ? ? ?) normalize nodelta [ #_ @res_preserve_error1] 1812 #sigma_pc #sigma_pc_spec normalize nodelta cases bv1 1813 [   #ptr1 #ptr2 #p  #by  #p  #ptr #p  #pc1 #p1] 1814 normalize nodelta try @res_preserve_error1 1815 inversion(sigma_pc_opt ? ? ?) normalize nodelta [#_ @res_preserve_error1] 1816 #sigma_pc1 #sigma_pc1_spec @if_elim [2: #_ @res_preserve_error1] 1817 @andb_elim @if_elim [2: #_ *] @andb_elim @if_elim [2: #_ *] 1818 #_ #H >H @eq_program_counter_elim [2: #_ *] 1819 #EQspc * @eq_program_counter_elim 1820 [#_ normalize nodelta @mfr_return_eq1 whd in match sigma_stored_pc; normalize nodelta 1821 >sigma_pc1_spec %] * #H1 @⊥ @H1 >EQspc in sigma_pc_spec; <sigma_pc1_spec 1822 whd in match sigma_pc_opt; normalize nodelta @if_elim 1823 [ #H2 #EQ lapply(sym_eq ??? EQ) EQ @if_elim [#_ whd in ⊢ (??%% → ?); #EQ destruct %] 1824 #H3 #H @('bind_inversion H) H #x #_ #H @('bind_inversion H) H #y #_ 1825 cases sigma_pc1 in H2; #bl_pc1 #z #H2 whd in ⊢ (??%? → ?); #EQ destruct >H2 in H3; * 1826  #H2 @if_elim 1827 [ #H3 #H @('bind_inversion H) H #x1 #_ #H @('bind_inversion H) H #lbl1 #_ 1828 cases pc in H2; #bl #z #H2 whd in match pc_of_point; normalize nodelta whd in ⊢ (??%? → ?); 1829 #EQ destruct >H3 in H2; * 1830  #H3 lapply sigma_pc1_spec; whd in match sigma_pc_opt; normalize nodelta @if_elim 1831 [#H >H in H3; *] #_ #EQ >EQ @('bind_inversion EQ) EQ #x #x_spec 1832 lapply(res_eq_from_opt ??? x_spec) x_spec #x_spec #H @('bind_inversion H) * #lbl 1833 #lbl_spec whd in match pc_of_point; normalize nodelta cases sigma_pc1 #bl1 #lbl1 1834 whd in match (offset_of_point ??); whd in ⊢ (??%? → ?); #EQ destruct cases pc #bl2 #p2 1835 #H @('bind_inversion H) H #x1 #x1_spec lapply(res_eq_from_opt ??? x1_spec) x1_spec #x1_spec 1836 #H @('bind_inversion H) H * #lbl2 #lbl2_spec 1837 whd in match (offset_of_point ??); whd in ⊢ (??%? → ?); #EQ destruct 1838 <lbl_spec in lbl2_spec; #EQsig >x_spec in x1_spec; whd in ⊢ (??%% → ?); #EQ destruct 1839 lapply(partial_inj_sigma … EQsig) 1840 [>EQsig >lbl_spec % #ABS destruct] whd in match point_of_pc; normalize nodelta 1841 whd in match (point_of_offset ??); whd in match (point_of_offset ??); 1842 #EQ destruct cases pc1 #bl #p % 1843 ] 1844 ] 1845  #pc @mfr_return_eq1 % 1846 ] 1847 qed. 1848 1849 lemma pc_block_eq : ∀prog : ertl_program. 1850 ∀sigma : sigma_map prog. 1851 ∀pc,id,fn. 1852 fetch_internal_function (joint_closed_internal_function ERTL 1853 (prog_var_names (joint_function ERTL) ℕ prog)) 1854 (globalenv_noinit (joint_function ERTL) prog) (pc_block … pc) 1855 = return 〈id,fn〉→ 1856 sigma fn (point_of_pc ERTL_semantics pc) ≠ None ? → 1857 pc_block … pc = pc_block … (sigma_stored_pc prog sigma pc). 1858 #prog #sigma * #bl #pos #id #fn #EQfn #EQlbl whd in match sigma_stored_pc; 1859 normalize nodelta whd in match sigma_pc_opt; normalize nodelta @if_elim [ #_ %] 1860 #_ >EQfn >m_return_bind >(opt_to_opt_safe … EQlbl) >m_return_bind % 1861 qed. 1862 1863 inductive ex_Type1 (A:Type[1]) (P:A → Prop) : Prop ≝ 1864 ex1_intro: ∀ x:A. P x → ex_Type1 A P. 1865 (*interpretation "exists in Type[1]" 'exists x = (ex_Type1 ? x).*) 1866 1867 include "joint/semantics_blocks.ma". 1868 1869 lemma fetch_internal_function_no_zero : 1870 ∀F,V,i,p,bl. 1871 block_id (pi1 … bl) = 0 → 1872 fetch_internal_function ? 1873 1874 (globalenv (λvars.fundef (F vars)) V i p) bl = 1875 Error ? [MSG BadFunction]. 1876 #F #V #i #p #bl #EQbl whd in match fetch_internal_function; 1877 normalize nodelta >fetch_function_no_zero [2: assumption] % 1878 qed. 1879 1880 lemma fetch_statement_no_zero : 1881 ∀pars,prog,stack_size,pc. 1882 block_id(pi1 … (pc_block pc)) = 0 → 1883 fetch_statement pars (prog_var_names … prog) 1884 (ev_genv (mk_prog_params pars prog stack_size)) pc = 1885 Error ? [MSG BadFunction]. 1886 #pars #vars #ge #pc #EQpc whd in match fetch_statement; normalize nodelta 1887 >fetch_internal_function_no_zero [2: assumption] % 1888 qed. 1889 1890 lemma foo : 1891 ∀P1_unser,P2_unser: unserialized_params. 1892 ∀P1_sem_unser,P2_sem_unser. 1893 let P1_sem ≝ make_sem_graph_params P1_unser P1_sem_unser in 1894 let P2_sem ≝ make_sem_graph_params P2_unser P2_sem_unser in 1895 ∀init,translate_step. 1896 ∀translate_fin_step. 1897 ∀closed_graph_translate. 1898 let translate_internal : 1899 ∀globals. 1900 joint_closed_internal_function P1_sem globals → 1901 joint_closed_internal_function P2_sem globals 1902 ≝ 1903 λglobals,fun. 1904 «b_graph_translate (mk_graph_params P1_sem) (mk_graph_params P2_sem) globals 1905 (init globals) 1906 (translate_step globals) 1907 (translate_fin_step globals) 1908 (pi1 … fun), closed_graph_translate globals fun» in 1909 ∀prog. 1910 let trans_prog ≝ transform_program ??? prog (λvarnames. transf_fundef ?? (translate_internal varnames)) in 1911 ∀stack_size. 1912 ∀sigma_state_pc. 1913 (∀s. pc_block (pc … (sigma_state_pc s)) = pc_block … (pc … s)) → 1914 ∀st : state_pc P2_sem. 1915 ∀st' : state_pc P1_sem. 1916 ∀f. 1917 ∀fn: joint_closed_internal_function P1_sem (globals (mk_prog_params P1_sem prog stack_size)). 1918 luniverse_ok … fn → 1919 ∀stmt,nxt. 1920 (∀pre_Instrs',last_Instrs',dst. 1921 ∃st''.∃st'''.∃st''''. 1922 repeat_eval_seq_no_pc (mk_prog_params P2_sem trans_prog stack_size) 1923 f (translate_internal ? fn) (map_eval ?? pre_Instrs' dst) st = return st''' ∧ 1924 eval_seq_no_pc ? (prog_var_names … trans_prog) (ev_genv … (mk_prog_params P2_sem trans_prog stack_size)) 1925 f (translate_internal … fn) (last_Instrs' dst) st''' = return st'''' ∧ 1926 st'' = (mk_state_pc (mk_prog_params P2_sem trans_prog stack_size) 1927 st'''' (pc_of_point P2_sem (pc_block (pc … (sigma_state_pc st))) dst) (last_pop … st)) ∧ 1928 st' = sigma_state_pc st'' ∧ 1929 let P2_prog_params ≝ mk_prog_params P2_sem trans_prog stack_size in 1930 let P2_globals ≝ globals P2_prog_params in 1931 All 1932 (joint_seq … P2_globals) 1933 (no_cost_label … P2_globals) 1934 (map_eval (code_point P2_sem) (joint_seq … P2_globals) pre_Instrs' dst)) → 1935 fetch_statement … 1936 (prog_var_names (joint_function P1_sem) ℕ prog) 1937 (ev_genv (mk_prog_params P1_sem prog stack_size)) 1938 (pc … (sigma_state_pc st)) = 1939 return 〈f, fn, sequential … (step_seq P1_sem … stmt) nxt〉 → 1940 eval_state … 1941 (prog_var_names (joint_function P1_sem) ℕ prog) 1942 (ev_genv … (mk_prog_params P1_sem prog stack_size)) 1943 (sigma_state_pc st) = return st' → 1944 ∃st''. (*CSC: this needs to be linked back again st' = sigma_state_pc ? good st'' ∧*) 1945 ∃taf : trace_any_any_free (joint_abstract_status (mk_prog_params P2_sem trans_prog stack_size)) st st''. 1946 True (* the length of taf is the same of the length of ??? *). 1947 #P1_unser #P2_unser #P1_sem_unser #P2_sem_unser 1948 letin P1_sem ≝ (make_sem_graph_params P1_unser P1_sem_unser) 1949 letin P2_sem ≝ (make_sem_graph_params P2_unser P2_sem_unser) 1950 #init #translate_step #translate_fin_step #closed_graph_translate. 1951 letin translate_internal ≝ 1952 (λglobals,fun. 1953 «b_graph_translate (mk_graph_params P1_sem) (mk_graph_params P2_sem) globals 1954 (init globals) 1955 (translate_step globals) 1956 (translate_fin_step globals) 1957 (pi1 … fun), closed_graph_translate globals fun») 1958 #prog 1959 letin trans_prog ≝ (transform_program ??? prog (λvarnames. transf_fundef ?? (translate_internal varnames))) 1960 #stack_size #sigma_state_pc #sigma_state_pc_ok #st #st' #f #fn #fn_universe_ok #stmt #nxt #Hpass 1961 #EQfetch lapply(fetch_statement_inv … EQfetch) * #EQfn #EQstmt 1962 cases 1963 (b_graph_translate_ok … (init …) (translate_step …) (translate_fin_step …) … fn_universe_ok) 1964 #_ * #MK_fresh_labels * #MK_fresh_registers **** #_ #_ #_ #_ (*CSC: useful things thrown out here *) 1965 #MULTI_FETCH_OK cases (MULTI_FETCH_OK … EQstmt) 1966 #list_b_last * #fresh_registers ** #EQlist_b_last #EQfresh_registers 1967 normalize nodelta * #Instrs * #fresh_registers_spec whd in ⊢ (% → ?); 1968 @pair_elim #pre_Instrs #last_Instrs #EQInstrs * #dst * #Multi_fetch #STEP_in_code 1969 #EQeval 1970 cut((list 1971 (code_point P2_sem 1972 →joint_seq P2_sem (prog_var_names (joint_function P1_sem) ℕ prog)))) [ cases daemon (*Paolo should fix the lemma*)] 1973 #pre_Instrs' 1974 cut((code_point P2_sem 1975 →joint_seq P2_sem (prog_var_names (joint_function P1_sem) ℕ prog))) [ cases daemon (*Paolo should fix the lemma*)] 1976 #last_Instrs' 1977 cases (Hpass pre_Instrs' last_Instrs' dst (* MANY MORE HERE *)) 1978 #st'' * #st''' * #st'''' **** #REPEAT #EVAL_NO_PC_Last #EQst'' #EQst' #NO_COSTED 1979 lapply(produce_trace_any_any_free … NO_COSTED … REPEAT) 1980 [ cases daemon (* should be @Multi_fetch *) 1981  <sigma_state_pc_ok @(fetch_internal_function_transf … (λvars.translate_internal vars)) 1982 assumption 1983  @dst 1984  @list_b_last (*wrong, should dst be destination or the last of list_b_last *) 1985 ] #TAAF 1986 lapply 1987 (produce_step_trace (mk_prog_params P2_sem trans_prog stack_size) 1988 (mk_state_pc (mk_prog_params P2_sem trans_prog stack_size) 1989 st''' (pc_of_point P2_sem (pc_block (pc … st)) dst) (last_pop … st)) 1990 f (translate_internal ? fn) (last_Instrs' dst) nxt st'''' … EVAL_NO_PC_Last) 1991 [ cases daemon (* should be @STEP_In_code *) 1992  <sigma_state_pc_ok 1993 @(fetch_internal_function_transf … (λvars. translate_internal vars) … EQfn) ] 1994 #LAST_STEP 1995 1996 1997 lemma eval_seq_no_call_ok : 1998 ∀prog. 1999 let trans_prog ≝ ertl_to_ertlptr prog in 2000 ∀good : (∀fn.good_state_transformation prog fn). 2001 ∀stack_sizes. 2002 (*? →*) 2003 ∀st : state_pc ERTLptr_semantics. 2004 ∀st' : state_pc ERTL_semantics. 2005 ∀f,fn,stmt,nxt. 2006 fetch_statement ERTL_semantics 2007 (prog_var_names (joint_function ERTL_semantics) ℕ prog) 2008 (ev_genv (mk_prog_params ERTL_semantics prog stack_sizes)) 2009 (pc … (sigma_state_pc ? good st)) = 2010 return 〈f, fn, sequential … (step_seq ERTL … stmt) nxt〉 → 2011 eval_state ERTL_semantics 2012 (prog_var_names (joint_function ERTL_semantics) ℕ prog) 2013 (ev_genv … (mk_prog_params ERTL_semantics prog stack_sizes)) 2014 (sigma_state_pc ? good st) = 2015 return st' → 2016 ∃st''. st' = sigma_state_pc ? good st'' ∧ 2017 ∃taf : trace_any_any_free (ERTLptr_status trans_prog stack_sizes) 2018 st 2019 st''. 2020 bool_to_Prop (taaf_non_empty … taf). 2021 #prog #good #stack_size #st #st' #f #fn #stmt #nxt 2022 whd in match sigma_state_pc in ⊢ (% → ?); normalize nodelta @if_elim 2023 [ #_ >fetch_statement_no_zero [2,4: %] whd in ⊢ (???% → ?); #ABS destruct] 2024 #EQbl inversion(fetch_internal_function ?? (pc_block (pc ? st))) normalize nodelta 2025 [2: #err #_ >fetch_statement_no_zero [2,4: %] whd in ⊢ (???% → ?); #ABS destruct] 2026 * #id1 #fn1 #EQfn normalize nodelta #EQfetch lapply(fetch_statement_inv … EQfetch) 2027 * >EQfn #EQ destruct normalize nodelta #EQstmt 2028 cases(multi_fetch_ok … (good fn) ?? EQstmt) 2029 #list_b_last * #fresh_registers ** #EQlist_b_last #EQfresh_registers 2030 normalize nodelta * #Instrs * #fresh_registers_spec whd in ⊢ (% → ?); 2031 @pair_elim #pre_Instrs #last_Instrs #EQInstrs * #dst * #Multi_fetch #STEP_in_code 2032 #EQeval 2033 cut((list 2034 (code_point ERTLptr 2035 →joint_seq ERTLptr (prog_var_names (joint_function ERTL) ℕ prog)))) [ cases daemon (*Paolo should fix the lemma*)] 2036 #pre_Instrs' 2037 cut((code_point ERTLptr 2038 →joint_seq ERTLptr (prog_var_names (joint_function ERTL) ℕ prog))) [ cases daemon (*Paolo should fix the lemma*)] 2039 #last_Instrs' 2040 letin list_map ≝ cic:/matita/basics/lists/list/map.fix(0,3,1) 2041 cut(∃st''.∃st'''.∃st''''. 2042 repeat_eval_seq_no_pc (mk_prog_params ERTLptr_semantics (ertl_to_ertlptr prog) stack_size) 2043 f (translate_internal ? fn) (map_eval ?? pre_Instrs' dst) st = return st''' ∧ 2044 eval_seq_no_pc ? (prog_var_names … (ertl_to_ertlptr prog)) (ev_genv … (mk_prog_params ERTLptr_semantics (ertl_to_ertlptr prog) stack_size)) 2045 f (translate_internal … fn) (last_Instrs' dst) st''' = return st'''' ∧ 2046 st'' = (mk_state_pc (mk_prog_params ERTLptr_semantics (ertl_to_ertlptr prog) stack_size) 2047 st'''' (pc_of_point ERTLptr_semantics (pc_block (pc … st)) dst) 2048 (last_pop … st)) ∧ 2049 st' = sigma_state_pc ? good st'') 2050 [ cases daemon (*to be generalized and TO be moved into an other lemma *)] 2051 * #st'' * #st''' * #st'''' *** #REPEAT #EVAL_NO_PC_Last #EQst'' #EQst' %{st''} % [assumption] 2052 lapply(produce_trace_any_any_free … REPEAT) 2053 [ cases daemon (* Pass dependent *) 2054  cases daemon (* should be @Multi_fetch *) 2055  @(fetch_internal_function_transf … (λvars. translate_internal …) … EQfn) 2056  @dst 2057  @list_b_last (*wrong, should dst be destination or the last of list_b_last *) 2058 ] #TAAF 2059 lapply(produce_step_trace (mk_prog_params ERTLptr_semantics (ertl_to_ertlptr prog) stack_size) 2060 (mk_state_pc (mk_prog_params ERTLptr_semantics (ertl_to_ertlptr prog) stack_size) 2061 st''' (pc_of_point ERTLptr_semantics (pc_block (pc … st)) dst) 2062 (last_pop … st)) f (translate_internal ? fn) (last_Instrs' dst) nxt st'''' (fetch_internal_function_transf … (λvars. translate_internal …) … EQfn) 2063 ? EVAL_NO_PC_Last) [cases daemon (* should be @STEP_in_code *)] 2064 #LAST_STEP 2065 letin taaf_last ≝ (taaf_step ???? TAAF LAST_STEP) 2066 2067 cut(dst = (point_of_pc 2068 (mk_prog_params ERTLptr_semantics (ertl_to_ertlptr prog) stack_size) 2069 (pc … st))) [cases daemon (*TODO it is true since pre_Instr is empty *)] 2070 #EQ <EQ whd in match step_in_code; normalize nodelta 2071 cases STEP_in_code #x * #x_spec #x_spec' %{x} % 2072 [ >x_spec in ⊢ (??%?); @eq_f @eq_f2 [2: %] cases daemon (*should be % *)  2073 [<EVAL_NO_PC_Last in ⊢ (???%); @eq_f % 2074 2075 2076 2077 whd in match eval_state; normalize nodelta >EQfetch >m_return_bind 2078 lapply EQfetch EQfetch whd in match sigma_state_pc in ⊢ (% → ?); 2079 normalize nodelta @if_elim 2080 [ #_ >fetch_statement_no_zero [2,4: %] whd in ⊢ (???% → ?); #ABS destruct] 2081 #EQbl inversion(fetch_internal_function ?? (pc_block (pc ? st))) normalize nodelta 2082 [2: #err #_ >fetch_statement_no_zero [2,4: %] whd in ⊢ (???% → ?); #ABS destruct] 2083 * #id1 #fn1 #EQfn normalize nodelta #EQfetch lapply(fetch_statement_inv … EQfetch) 2084 * >EQfn #EQ destruct normalize nodelta #EQstmt 2085 whd in match sigma_state_pc in ⊢ (% → ?); normalize nodelta @if_elim 2086 [#H >H in EQbl; *] #_ >EQfn normalize nodelta whd in match eval_statement_no_pc; 2087 normalize nodelta #H @('bind_inversion H) H #ex_st_nopc 2088 #H lapply (err_eq_from_io ????? H) H #EQnopc whd in match eval_statement_advance; 2089 normalize nodelta whd in match set_no_pc; normalize nodelta 2090 whd in ⊢ (??%% → ?); #EQ destruct cases(eval_seq_no_pc_no_call_ok … EQnopc) 2091 #sigma_st_nopc * #EQsigma_st_nopc #sem_rel % 2092 [ % [@sigma_st_nopc 2093  @(succ_pc ERTL_semantics (pc ERTLptr_semantics st) nxt) 2094  @(last_pop … st) 2095 ] 2096 ] % whd in match sigma_state_pc; 2097 2098 2099 2100 qed. 2101 2102 lemma ertl_to_ertlptr_ok: 2103 ∀prog. 2104 let trans_prog ≝ ertl_to_ertlptr prog in 2105 ∀good : (∀fn.good_state_transformation prog fn). 2106 ∀stack_sizes. 2107 ex_Type1 … (λR. 2108 status_simulation 2109 (ERTL_status prog stack_sizes) (ERTLptr_status trans_prog stack_sizes) R). 2110 #prog #good #stack_size % [@ERTLptrStatusSimulation assumption] 2111 whd in match status_simulation; normalize nodelta 2112 whd in match ERTL_status; whd in match ERTLptr_status; normalize nodelta 2113 whd in ⊢ (% → % → % → % → ?); #st1 #st1' #st2 2114 change with 2115 (eval_state ERTL_semantics (prog_var_names ???) ?? = ? → ?) 2116 #EQeval @('bind_inversion EQeval) 2117 ** #id #fn #stmt #H lapply (err_eq_from_io ????? H) H #EQfetch 2118 #_ whd in match ERTLptrStatusSimulation; normalize nodelta #EQst2 destruct 2119 cases stmt in EQfetch; stmt 2120 [ * [ #called_id #args #dest #reg #lbl  #seq] #nxt  #fin_step  *] #EQfetch 2121 change with (joint_classify ??) in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ? ]); 2122 [ (*CALL*) cases daemon 2123  (*COND*) cases daemon 2124  (*seq*) whd in match joint_classify; normalize nodelta >EQfetch >m_return_bind 2125 normalize nodelta cases (eval_seq_no_call_ok ????????? EQfetch EQeval) 2126 #st3 * #EQ destruct * #taf #tafne %{st3} %{taf} >tafne normalize nodelta 2127 % [% //] whd >as_label_ok [2:assumption] % 2128 2129 2130 lapply(produce_trace_any_any_free 2131 (mk_prog_params ERTLptr_semantics (ertl_to_ertlptr prog) stack_size) 2132 st2 id (translate_internal ? fn)) #PRODUCE_TAAF 2133 cases stmt in EQfetch; stmt 2134 [ * [ #called_id #args #dest #reg #lbl  #seq] #nxt  #fin_step  *] #EQfetch 2135 normalize nodelta 2136 2137 2138 lapply EQfetch EQfetch whd in match sigma_state_pc in ⊢ (% → ?); 2139 normalize nodelta @if_elim 2140 [ #_ >fetch_statement_no_zero [2,4: %] whd in ⊢ (???% → ?); #ABS destruct] 2141 #EQbl inversion(fetch_internal_function ?? (pc_block (pc ? st2))) normalize nodelta 2142 [2: #err #_ >fetch_statement_no_zero [2,4: %] whd in ⊢ (???% → ?); #ABS destruct] 2143 * #id1 #fn1 #EQfn normalize nodelta #EQfetch lapply(fetch_statement_inv … EQfetch) 2144 * >EQfn #EQ destruct normalize nodelta #EQstmt 2145 2146 ? ? ?? ? ???) 2147 2148 2149 2150 cases stmt in EQfetch; stmt 2151 [ * [ #called_id #args #dest #reg #lbl  #seq] #nxt  #fin_step  *] #EQstmt 2152 change with (joint_classify ??) in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ? ]); 2153 whd in match joint_classify; normalize nodelta >EQstmt >m_return_bind 2154 normalize nodelta lapply(fetch_statement_inv … EQstmt) * #fn_spec 2155 #stmt_spec 2156 cases(multi_fetch_ok … (good fn) ?? stmt_spec) #f_labs * #f_regs ** #f_labs_spec 2157 #f_regs_spec normalize nodelta * #list_instr * #b_new_f_regs 2158 whd in ⊢ (% → ?); normalize nodelta 2159 [1,2,3: @pair_elim #list_instr1 #rgt #last_ne_spec * #last_lab * 2160 #list_instr1_spec #last_step 2161 lapply(fetch_internal_function_transf … 2162 (λvars. translate_internal …) … fn_spec) 2163 change with ((fetch_internal_function 2164 (joint_closed_internal_function ? (prog_var_names … (ertl_to_ertlptr prog))) 2165 (globalenv_noinit … (ertl_to_ertlptr prog)) ?) = ? → ?) 2166 #EQtrans_fn 2167 check prog_params 2168 lapply(produce_trace_any_any_free 2169 (mk_prog_params ERTLptr_semantics (ertl_to_ertlptr prog) stack_size) 2170 ? id (translate_internal ? fn) ? ? ?? EQtrans_fn ???) [2: @EQtrans_fn 2171 2172 2173 2174 2175 2176 lapply EQstmt whd in match sigma_state_pc in ⊢ (% → ?); 2177 normalize nodelta @if_elim 2178 [1,3: #_ >fetch_statement_no_zero [2,4: %] whd in ⊢ (???% → ?); #ABS destruct] 2179 #EQbl inversion(fetch_internal_function ?? (pc_block (pc ? st2))) normalize nodelta 2180 [2,4: #err #_ >fetch_statement_no_zero [2,4: %] whd in ⊢ (???% → ?); #ABS destruct] 2181 * #id1 #fn1 #EQfn1 normalize nodelta #EQstmt1 lapply(fetch_statement_inv … EQstmt1) 2182 * >EQfn1 #EQ destruct normalize nodelta #EQstmtat 2183 2184 2185 2186 2187 [ (*CALL*) 2188 cases daemon (*TODO*) 2189  whd in match joint_classify; normalize nodelta 2190 >EQfetch in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ? ]); 2191 normalize nodelta 2192 #n_cost 2193 cases (eval_cond_ok … EQfetch EQeval n_cost) 2194 #st3 * #EQ destruct * #taf #tafne %{st3} %{taf} 2195 % [ % [2: %] >tafne normalize nodelta @I] whd >as_label_ok % 2196  whd in match joint_classify; normalize nodelta 2197 >EQfetch in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ? ]); 2198 normalize nodelta 2199 cases (eval_seq_no_call_ok ????????? EQfetch EQeval) 2200 #st3 * #EQ destruct * #taf #tafne %{st3} %{taf} >tafne normalize nodelta 2201 % [% //] whd >as_label_ok [2:assumption] % 2202  (*FIN*) 2203 cases fin_step in EQfetch; 2204 [ (*GOTO*) #lbl #EQfetch whd in match joint_classify; normalize nodelta 2205 >EQfetch in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ? ]); normalize nodelta 2206 cases (eval_goto_ok … EQfetch EQeval) 2207 #st3 * #EQ destruct * #taf #tarne %{st3} %{taf} >tarne normalize nodelta 2208 % [% //] whd >as_label_ok [2:assumption] % 2209  (*RETURN*) #EQfetch 2210 whd in match joint_classify; normalize nodelta 2211 >EQfetch in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ? ]); normalize nodelta 2212 cases (eval_return_ok … EQfetch EQeval) #is_ret 2213 * #st3 * #EQ destruct * #after_ret * #taf ** #taf_prf #EQeval' #ret_prf 2214 % [2: % [2: % [2: %{(taa_base …)} %{taf}] *: ] *:] 2215 % [2: whd >as_label_ok %] % [2: assumption] % [2: %] % [2: assumption] 2216 % assumption 2217  (*TAILCALL*) #fl #called #args #EQfetch 2218 cases (eval_tailcall_ok … EQfetch EQeval) #st3 * #EQ destruct * #is_tailcall 2219 * #is_tailcall' * #eq_call #EQeval' >is_tailcall normalize nodelta 2220 #prf %{«?, is_tailcall'»} %{eq_call} 2221 % [2: % [2: %{(taa_base …)} %{(taa_base …)} % [ %{EQeval'} % ]  ]  ] 2222 whd >as_label_ok % 2223 ] 2224 ] 2225 qed. 2226 2227 @('bind_inversion EQfetch) * #id1 #fn1 #EQfn #H @('bind_inversion H) H 2228 #stmt1 #H lapply(opt_eq_from_res ???? H) H #EQstmt whd in ⊢ (??%% → ?); 2229 #EQ destruct 2230 2231 (* 2232 lemma push_ra_ok : ∀prog : ertl_program. 2233 ∀good : (∀fn.good_state_transformation prog fn).∀restr. 2234 preserving21 … res_preserve1 … 2235 (sigma_state_pc prog good) 2236 (\l 2237 (λst.sigma_state prog good st restr) 2238 (push_ra ERTL_semantics) 2239 (push_ra ERTLptr_semantics). 2240 #prog #good #restr #st #pc whd in match push_ra; normalize nodelta @mfr_bind1 2241 [2: whd in match sigma_stored_pc; normalize nodelta 2242 2243 [2: #x 2244 2245 2246 lemma ertlptr_save_frame_ok : ∀prog : ertl_program. 2247 ∀good : (∀fn.good_state_transformation prog fn). 2248 ∀id. 2249 preserving1 … res_preserve1 … 2250 (sigma_state_pc prog good) 2251 (λst. match get_internal_function_from_ident 2252 ERTL_semantics (prog_var_names … prog) 2253 (globalenv_noinit … prog) id with 2254 [None ⇒ dummy_state 2255 Some fd ⇒ 2256 sigma_state prog good st (added_registers … fd (f_regs … (good fd))) 2257 ]) 2258 (ertl_save_frame ID it id) 2259 (ertlptr_save_frame ID it id). 2260 #prog #good #id #st whd in match ertl_save_frame; whd in match ertlptr_save_frame; 2261 normalize nodelta @mfr_bind1 2262 [2: whd in match push_ra; normalize nodelta @mfr_bind1 2263 xxxxxxxxxxxx 2264 2265 2056 2266 2057 2267 lemma fetch_statement_commute : … … 2203 2413 qed. 2204 2414 2205 lemma pc_of_label_eq :2206 ∀p,p'.let pars ≝ make_sem_graph_params p p' in2207 ∀globals,ge,bl,i_fn,lbl.2208 fetch_internal_function ? ge bl = return i_fn →2209 pc_of_label pars globals ge bl lbl =2210 OK ? (pc_of_point ERTL_semantics bl lbl).2211 #p #p' #globals #ge #bl #i_fn #lbl #EQf2212 whd in match pc_of_label;2213 normalize nodelta >EQf >m_return_bind %2214 qed.2215 2415 2216 2416 lemma eval_goto_ok : … … 2280 2480 ] 2281 2481 qed. 2282 2283 axiom partial_inj_sigma : ∀ prog : ertlptr_program. 2284 ∀sigma :sigma_map prog. 2285 ∀fn,lbl1,lbl2. sigma fn lbl1 ≠ None ? → sigma fn lbl1 = sigma fn lbl2 → lbl1 = lbl2. 2286 2287 lemma pop_ra_ok : 2288 ∀prog : ertl_program. 2289 let trans_prog ≝ ertl_to_ertlptr prog in 2290 ∀sigma : sigma_map trans_prog. 2291 ∀stack_size. 2292 ∀fn : (joint_closed_internal_function ? (globals (mk_prog_params ERTL_semantics prog stack_size))). 2293 preserving1 … res_preserve1 … 2294 (λst.sigma_state trans_prog sigma st (joint_if_locals ERTL ? fn)) 2295 (λx.let 〈st,pc〉 ≝ x in 2296 〈sigma_state trans_prog sigma st (joint_if_locals ERTL ? fn), 2297 sigma_stored_pc ? sigma pc〉) 2298 (pop_ra ERTL_semantics) 2299 (pop_ra ERTLptr_semantics). 2300 #prog #sigma #stack_size #fn #st whd in match pop_ra; normalize nodelta @mfr_bind1 2301 [  @pop_ok ] * #bv #st1 @mfr_bind1 [  @pop_ok] * #bv1 #st2 @mfr_bind1 2302 [ @(sigma_stored_pc ? sigma)  whd in match pc_of_bevals; normalize nodelta 2303 cases bv [   #ptr1 #ptr2 #p  #by  #p  #ptr #p  #pc #p] 2304 whd in match sigma_beval; normalize nodelta try @res_preserve_error1 2305 inversion(sigma_pc_opt ? ? ?) normalize nodelta [ #_ @res_preserve_error1] 2306 #sigma_pc #sigma_pc_spec normalize nodelta cases bv1 2307 [   #ptr1 #ptr2 #p  #by  #p  #ptr #p  #pc1 #p1] 2308 normalize nodelta try @res_preserve_error1 2309 inversion(sigma_pc_opt ? ? ?) normalize nodelta [#_ @res_preserve_error1] 2310 #sigma_pc1 #sigma_pc1_spec @if_elim [2: #_ @res_preserve_error1] 2311 @andb_elim @if_elim [2: #_ *] @andb_elim @if_elim [2: #_ *] 2312 #_ #H >H @eq_program_counter_elim [2: #_ *] 2313 #EQspc * @eq_program_counter_elim 2314 [#_ normalize nodelta @mfr_return_eq1 whd in match sigma_stored_pc; normalize nodelta 2315 >sigma_pc1_spec %] * #H1 @⊥ @H1 >EQspc in sigma_pc_spec; <sigma_pc1_spec 2316 whd in match sigma_pc_opt; normalize nodelta @if_elim 2317 [ #H2 #EQ lapply(sym_eq ??? EQ) EQ @if_elim [#_ whd in ⊢ (??%% → ?); #EQ destruct %] 2318 #H3 #H @('bind_inversion H) H #x #_ #H @('bind_inversion H) H #y #_ 2319 cases sigma_pc1 in H2; #bl_pc1 #z #H2 whd in ⊢ (??%? → ?); #EQ destruct >H2 in H3; * 2320  #H2 @if_elim 2321 [ #H3 #H @('bind_inversion H) H #x1 #_ #H @('bind_inversion H) H #lbl1 #_ 2322 cases pc in H2; #bl #z #H2 whd in match pc_of_point; normalize nodelta whd in ⊢ (??%? → ?); 2323 #EQ destruct >H3 in H2; * 2324  #H3 lapply sigma_pc1_spec; whd in match sigma_pc_opt; normalize nodelta @if_elim 2325 [#H >H in H3; *] #_ #EQ >EQ @('bind_inversion EQ) EQ #x #x_spec 2326 lapply(res_eq_from_opt ??? x_spec) x_spec #x_spec #H @('bind_inversion H) * #lbl 2327 #lbl_spec whd in match pc_of_point; normalize nodelta cases sigma_pc1 #bl1 #lbl1 2328 whd in match (offset_of_point ??); whd in ⊢ (??%? → ?); #EQ destruct cases pc #bl2 #p2 2329 #H @('bind_inversion H) H #x1 #x1_spec lapply(res_eq_from_opt ??? x1_spec) x1_spec #x1_spec 2330 #H @('bind_inversion H) H * #lbl2 #lbl2_spec 2331 whd in match (offset_of_point ??); whd in ⊢ (??%? → ?); #EQ destruct 2332 <lbl_spec in lbl2_spec; #EQsig >x_spec in x1_spec; whd in ⊢ (??%% → ?); #EQ destruct 2333 lapply(partial_inj_sigma (ertl_to_ertlptr prog) sigma ???? EQsig) 2334 [>EQsig >lbl_spec % #ABS destruct] whd in match point_of_pc; normalize nodelta 2335 whd in match (point_of_offset ??); whd in match (point_of_offset ??); 2336 #EQ destruct cases pc1 #bl #p % 2337 ] 2338 ] 2339  #pc @mfr_return_eq1 % 2340 ] 2341 qed. 2342 2343 lemma pc_block_eq : ∀prog : ertl_program. 2344 let trans_prog ≝ ertl_to_ertlptr prog in 2345 ∀sigma : sigma_map trans_prog. 2346 ∀pc,id,fn. 2347 fetch_internal_function (joint_closed_internal_function ERTLptr 2348 (prog_var_names (joint_function ERTLptr) ℕ trans_prog)) 2349 (globalenv_noinit (joint_function ERTLptr) trans_prog) (pc_block … pc) = return 〈id,fn〉→ 2350 sigma fn (point_of_pc ERTL_semantics pc) ≠ None ? → 2351 pc_block … pc = pc_block … (sigma_stored_pc trans_prog sigma pc). 2352 #prog #sigma * #bl #pos #id #fn #EQfn #EQlbl whd in match sigma_stored_pc; 2353 normalize nodelta whd in match sigma_pc_opt; normalize nodelta @if_elim [ #_ %] 2354 #_ >EQfn >m_return_bind >(opt_to_opt_safe … EQlbl) >m_return_bind % 2355 qed. 2482 *) 2483 2484 2356 2485 2357 2486 … … 2713 2842 qed. 2714 2843 2715 inductive ex_Type1 (A:Type[1]) (P:A → Prop) : Prop ≝2716 ex1_intro: ∀ x:A. P x → ex_Type1 A P.2717 (*interpretation "exists in Type[1]" 'exists x = (ex_Type1 ? x).*)2718 2844 2719 2845 lemma … … 2733 2859 2734 2860 2735 lemma ertl_to_ertlptr_ok: 2736 ∀prog. 2737 let trans_prog ≝ ertl_to_ertlptr prog in 2738 ∀stack_sizes. sigma_map trans_prog → 2739 ex_Type1 … (λR. 2740 status_simulation 2741 (ERTL_status prog stack_sizes) (ERTLptr_status trans_prog stack_sizes) R). 2742 #prog #stack_size #sigma % [@ERTLptrStatusSimulation assumption] 2743 whd in match status_simulation; normalize nodelta 2744 whd in match ERTL_status; whd in match ERTLptr_status; normalize nodelta 2745 whd in ⊢ (% → % → % → % → ?); #st1 #st1' #st2 2746 change with 2747 (eval_state ERTL_semantics (prog_var_names ???) ?? = ? → ?) 2748 #EQeval @('bind_inversion EQeval) 2749 ** #id #fn #stmt #H lapply (err_eq_from_io ????? H) H #EQfetch 2750 #_ whd in match ERTLptrStatusSimulation; normalize nodelta #EQst2 destruct 2751 cases stmt in EQfetch; stmt 2752 [ * [#called #c_arg #c_dest  #reg #lbl  #seq ] #succ_pc  #fin_step  *] 2753 normalize nodelta #EQfetch 2754 change with (joint_classify ??) in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ? ]); 2755 [ (*CALL*) 2756 cases daemon (*TODO*) 2757  whd in match joint_classify; normalize nodelta 2758 >EQfetch in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ? ]); 2759 normalize nodelta 2760 #n_cost 2761 cases (eval_cond_ok … EQfetch EQeval n_cost) 2762 #st3 * #EQ destruct * #taf #tafne %{st3} %{taf} 2763 % [ % [2: %] >tafne normalize nodelta @I] whd >as_label_ok % 2764  whd in match joint_classify; normalize nodelta 2765 >EQfetch in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ? ]); 2766 normalize nodelta 2767 cases (eval_seq_no_call_ok ????????? EQfetch EQeval) 2768 #st3 * #EQ destruct * #taf #tafne %{st3} %{taf} >tafne normalize nodelta 2769 % [% //] whd >as_label_ok [2:assumption] % 2770  (*FIN*) 2771 cases fin_step in EQfetch; 2772 [ (*GOTO*) #lbl #EQfetch whd in match joint_classify; normalize nodelta 2773 >EQfetch in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ? ]); normalize nodelta 2774 cases (eval_goto_ok … EQfetch EQeval) 2775 #st3 * #EQ destruct * #taf #tarne %{st3} %{taf} >tarne normalize nodelta 2776 % [% //] whd >as_label_ok [2:assumption] % 2777  (*RETURN*) #EQfetch 2778 whd in match joint_classify; normalize nodelta 2779 >EQfetch in ⊢ (match % with [ _ ⇒ ?  _ ⇒ ? ]); normalize nodelta 2780 cases (eval_return_ok … EQfetch EQeval) #is_ret 2781 * #st3 * #EQ destruct * #after_ret * #taf ** #taf_prf #EQeval' #ret_prf 2782 % [2: % [2: % [2: %{(taa_base …)} %{taf}] *: ] *:] 2783 % [2: whd >as_label_ok %] % [2: assumption] % [2: %] % [2: assumption] 2784 % assumption 2785  (*TAILCALL*) #fl #called #args #EQfetch 2786 cases (eval_tailcall_ok … EQfetch EQeval) #st3 * #EQ destruct * #is_tailcall 2787 * #is_tailcall' * #eq_call #EQeval' >is_tailcall normalize nodelta 2788 #prf %{«?, is_tailcall'»} %{eq_call} 2789 % [2: % [2: %{(taa_base …)} %{(taa_base …)} % [ %{EQeval'} % ]  ]  ] 2790 whd >as_label_ok % 2791 ] 2792 ] 2793 qed. 2794 2795 2796 2861 2862 2863 2864
Note: See TracChangeset
for help on using the changeset viewer.