Changeset 2662 for src


Ignore:
Timestamp:
Feb 12, 2013, 6:56:41 PM (7 years ago)
Author:
piccolo
Message:

Towards a very generalized lemma that summarizes all of Paolo's results.

File:
1 edited

Legend:

Unmodified
Added
Removed
  • src/ERTLptr/ERTLtoERTLptrOK.ma

    r2645 r2662  
    8484qed.
    8585
    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] #prf
    101 [ @res_preserve_error
    102 |*:
    103  whd in match sigma_is in ⊢ (?????????%); normalize nodelta
    104  @opt_safe_elim #is'
    105   #H @('bind_inversion H) -H #bv1' #EQ1
    106   [2: #H @('bind_inversion H) -H #bv2' #EQ2 ]
    107  whd in ⊢ (??%%→?); #EQ destruct(EQ)
    108  @mfr_return_eq
    109  [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 
    12986definition sigma_mem :
    13087 ∀prog : ertl_program . sigma_map prog → bemem → bemem ≝
     
    14299  (nextblock m)
    143100  (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 *)
    160103axiom mem_ext_eq :
    161104  ∀m1,m2 : mem.
     
    166109  nextblock m1 = nextblock m2 → m1 = m2.
    167110
    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 #bv
    178 whd in match beloadv;
    179 whd in match do_if_in_bounds;
    180 whd in match sigma_mem;
    181 normalize nodelta
    182 @If_elim #block_ok >block_ok normalize nodelta
    183 [2: whd in ⊢ (???%→?); #ABS destruct(ABS) ]
    184 @If_elim #H
    185 [ elim (andb_true … H)
    186   #H1 #H2
    187   whd in match sigma_beval; normalize nodelta
    188   @opt_safe_elim #bv' #EQ_bv' >H1 >H2 normalize nodelta
    189   whd in ⊢ (???%→?); #EQ' destruct
    190   >EQ_bv' % [ % #ABS destruct(ABS) ] @opt_to_opt_safe
    191 | elim (andb_false … H) -H #H >H
    192   [2: >commutative_andb ] normalize nodelta
    193   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 nodelta
    213 @If_elim #block_ok >block_ok normalize nodelta
    214 [2: whd in ⊢ ((???%) → ?); #ABS destruct(ABS)]
    215 @Zleb_elim_Type0 #H1
    216 [ @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_f
    222   @mem_ext_eq [2: % ]
    223   #b @if_elim
    224   [2: #B
    225     @If_elim #prf1 @If_elim #prf2
    226     [2,3: @⊥ >prf1 in prf2; * /2 by I/ ] [2: % [%%] #z % ]
    227     whd in match low_bound; whd in match high_bound;
    228     normalize nodelta
    229     cut (Not (bool_to_Prop (eq_block b (pblock ptr))))
    230     [ % #ABS >ABS in B; * ]
    231     -B #B % [ >B %% ] #z
    232     @If_elim #prf3 
    233     @If_elim #prf4
    234     [2,3: @⊥ >B in prf4; normalize nodelta >prf3 * /2 by I/ |4: % ]
    235     whd in match sigma_beval in ⊢ (??%%); normalize nodelta
    236     @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 nodelta
    242     [2: >block_ok * #ABS elim (ABS I) ]
    243     #prf3 % [ >B %% ]
    244     #z whd in match update; normalize nodelta
    245     @eqZb_elim normalize nodelta #prf4
    246     [2: @If_elim #prf5 @If_elim #prf6
    247       [2,3: @⊥ >B in prf6; >prf5 * /2 by I/ |4: % ]
    248       whd in match sigma_beval in ⊢ (??%%); normalize nodelta
    249       @opt_safe_elim @opt_safe_elim #bv1 #EQ1 #bv2 #EQ2 >B in EQ1;
    250       normalize nodelta >(eqZb_false … prf4) >EQ2
    251       #EQ destruct(EQ) %
    252     | @If_elim #prf5
    253       [2: >B in prf5; normalize nodelta
    254         >prf4 >(Zle_to_Zleb_true … H1) >(Zlt_to_Zltb_true … H2) * #ABS elim (ABS I) ]
    255       whd in match sigma_beval in ⊢ (??%%); normalize nodelta
    256       @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 nodelta
    261   @eq_block_elim #H normalize nodelta destruct
    262   #h2 #h3 whd in match update; normalize nodelta
    263   [ @eqZb_elim #H destruct normalize nodelta [ assumption ]]
    264   @prf1 assumption
    265 ]
    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 → ? with
    275 [ pm_leaf ⇒ λ_.pm_leaf ?
    276 | pm_node a l r ⇒ λprf.pm_node ?
    277 ((match a return λx.a=x→? with
    278         [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 assumption
    285 |*: [1,3: @hide_prf] cases prf1 #tl #H [4,3 : @tl] <prf assumption
    286 ] 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) → ? with
    296   [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 assumption
    299 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) in
    318   ∀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 -F
    326 cases m -m #m elim m
    327 [ #F #a * #id elim id [#F' #eqFF' %] #x #Hx #F' #eqFF' whd in ⊢ (??%%);
    328   normalize nodelta @eq_f whd in match insert; normalize nodelta
    329   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))}] @prf1
    333     |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_a
    341       [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 *)
    358111
    359112
     
    371124                              [an_id_map p ⇒ id_is_in A x p]
    372125     ].
    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     
    422127lemma lookup_eq : ∀ A : Type[0].
    423128∀m,m' : positive_map A.
     
    529234qed.
    530235
    531 
    532236lemma update_ok_to_lookup : ∀ A : Type[0].
    533237∀ tag : identifierTag.
     
    582286    ]
    583287qed.
     288
     289
    584290(*
    585291               
     
    1069775           fresh_for_univ … reg (joint_if_runiverse … def_out))) (f_regs l))
    1070776; 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 →
    1072780  ∃lbls,regs.f_lbls l = Some ? lbls ∧ f_regs l = Some ? regs ∧
    1073781  match s with
     
    18751583set_sp ? ptr (sigma_state prog good st restr) =
    18761584sigma_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;
     1586normalize nodelta @eq_f2 [2: %] whd in match (save_sp ???);
     1587whd in match (save_sp ???); whd in match sigma_regs; normalize nodelta
     1588cases(regs ? st) #psd_env #hw_regs normalize nodelta @eq_f
     1589whd in match hwreg_store_sp; normalize nodelta whd in match sigma_hw_register_env;
     1590normalize nodelta whd in match hwreg_store; normalize nodelta @eq_f2 [2: %]
     1591>insert_map @eq_f >insert_map %
    18781592qed.
    18791593
     
    19131627  ]
    19141628| #i
    1915   change with (member ? ? ? (((prog_var_names (joint_function ERTL)) ℕ prog)) → ?)
    19161629  #i_spec
    19171630  change with ((dpl_reg ERTL) → ?)
     
    20521765qed.
    20531766
    2054 
    2055 xxxxxxxxxxxxxxxxx
     1767lemma partial_inj_sigma : ∀ prog : ertl_program.
     1768∀good : (∀fn.good_state_transformation prog fn).
     1769let 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
     1775whd in ⊢ (??%? → ?); #EQ destruct lapply(find_predicate ?????? H1)
     1776lapply(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 %
     1780qed.
     1781
     1782lemma 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
     1789whd in match pc_of_label;
     1790normalize nodelta >EQf >m_return_bind %
     1791qed.
     1792
     1793lemma pop_ra_ok :
     1794∀prog : ertl_program.
     1795∀good : (∀fn.good_state_transformation prog fn).
     1796∀restr.
     1797preserving1 … 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]
     1847qed.
     1848
     1849lemma pc_block_eq : ∀prog : ertl_program.
     1850∀sigma : sigma_map prog.
     1851∀pc,id,fn.
     1852fetch_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〉→
     1856sigma 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;
     1859normalize nodelta whd in match sigma_pc_opt; normalize nodelta @if_elim [ #_ %]
     1860#_ >EQfn >m_return_bind >(opt_to_opt_safe … EQlbl) >m_return_bind %
     1861qed.
     1862
     1863inductive 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
     1867include "joint/semantics_blocks.ma".
     1868
     1869lemma 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;
     1877normalize nodelta >fetch_function_no_zero [2: assumption] %
     1878qed.
     1879
     1880lemma fetch_statement_no_zero :
     1881∀pars,prog,stack_size,pc.
     1882block_id(pi1 … (pc_block pc)) = 0 →
     1883fetch_statement pars (prog_var_names … prog)
     1884(ev_genv (mk_prog_params pars prog stack_size)) pc =
     1885Error ? [MSG BadFunction].
     1886#pars #vars #ge #pc #EQpc whd in match fetch_statement; normalize nodelta
     1887>fetch_internal_function_no_zero [2: assumption] %
     1888qed.
     1889
     1890lemma 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
     1948letin P1_sem ≝ (make_sem_graph_params P1_unser P1_sem_unser)
     1949letin P2_sem ≝ (make_sem_graph_params P2_unser P2_sem_unser)
     1950#init #translate_step #translate_fin_step #closed_graph_translate.
     1951letin 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
     1959letin 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
     1962cases
     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
     1967normalize nodelta * #Instrs * #fresh_registers_spec whd in ⊢ (% → ?);
     1968@pair_elim #pre_Instrs #last_Instrs #EQInstrs * #dst * #Multi_fetch #STEP_in_code
     1969#EQeval
     1970cut((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'
     1974cut((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'
     1977cases (Hpass pre_Instrs' last_Instrs' dst (* MANY MORE HERE *))
     1978#st'' * #st''' * #st'''' **** #REPEAT #EVAL_NO_PC_Last #EQst'' #EQst' #NO_COSTED
     1979lapply(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
     1986lapply
     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
     1997lemma 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
     2022whd 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
     2028cases(multi_fetch_ok … (good fn) ?? EQstmt)
     2029#list_b_last * #fresh_registers ** #EQlist_b_last #EQfresh_registers
     2030normalize nodelta * #Instrs * #fresh_registers_spec whd in ⊢ (% → ?);
     2031@pair_elim #pre_Instrs #last_Instrs #EQInstrs * #dst * #Multi_fetch #STEP_in_code
     2032#EQeval
     2033cut((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'
     2037cut((code_point ERTLptr
     2038   →joint_seq ERTLptr (prog_var_names (joint_function ERTL) ℕ prog))) [ cases daemon (*Paolo should fix the lemma*)]
     2039#last_Instrs'
     2040letin list_map ≝ cic:/matita/basics/lists/list/map.fix(0,3,1)
     2041cut(∃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]
     2052lapply(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
     2059lapply(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
     2065letin 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
     2077whd in match eval_state; normalize nodelta >EQfetch >m_return_bind
     2078lapply EQfetch -EQfetch whd in match sigma_state_pc in ⊢ (% → ?);
     2079normalize 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
     2085whd 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;
     2087normalize 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;
     2089normalize nodelta whd in match set_no_pc; normalize nodelta
     2090whd 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
     2100qed.
     2101
     2102lemma ertl_to_ertlptr_ok:
     2103∀prog.
     2104let 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]
     2111whd in match status_simulation; normalize nodelta
     2112whd in match ERTL_status; whd in match ERTLptr_status; normalize nodelta
     2113whd in ⊢ (% → % → % → % → ?); #st1 #st1' #st2
     2114change 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
     2119cases stmt in EQfetch; -stmt
     2120[ * [ #called_id #args #dest| #reg #lbl | #seq] #nxt | #fin_step | *] #EQfetch
     2121change 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
     2130lapply(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
     2133cases stmt in EQfetch; -stmt
     2134[ * [ #called_id #args #dest| #reg #lbl | #seq] #nxt | #fin_step | *] #EQfetch
     2135normalize nodelta
     2136
     2137     
     2138lapply EQfetch -EQfetch whd in match sigma_state_pc in ⊢ (% → ?);
     2139normalize 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
     2150cases stmt in EQfetch; -stmt
     2151[ * [ #called_id #args #dest| #reg #lbl | #seq] #nxt | #fin_step | *] #EQstmt
     2152change with (joint_classify ??) in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]);
     2153whd in match joint_classify; normalize nodelta >EQstmt >m_return_bind
     2154normalize nodelta lapply(fetch_statement_inv … EQstmt) * #fn_spec
     2155#stmt_spec
     2156cases(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
     2158whd 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
     2176lapply EQstmt whd in match sigma_state_pc in ⊢ (% → ?);
     2177normalize 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]
     2225qed.
     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(*
     2232lemma push_ra_ok : ∀prog : ertl_program.
     2233∀good :  (∀fn.good_state_transformation prog fn).∀restr.
     2234preserving21 … 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
     2246lemma 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;
     2261normalize nodelta @mfr_bind1
     2262[2: whd in match push_ra; normalize nodelta @mfr_bind1
     2263xxxxxxxxxxxx
     2264
     2265
    20562266
    20572267lemma fetch_statement_commute :
     
    22032413qed.
    22042414
    2205 lemma pc_of_label_eq :
    2206   ∀p,p'.let pars ≝ make_sem_graph_params p p' in
    2207   ∀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 #EQf
    2212 whd in match pc_of_label;
    2213 normalize nodelta >EQf >m_return_bind %
    2214 qed.
    22152415
    22162416lemma eval_goto_ok :
     
    22802480]
    22812481qed.
    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
    23562485                       
    23572486
     
    27132842qed.
    27142843       
    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).*)
    27182844
    27192845lemma
     
    27332859
    27342860
    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.