Changeset 2843


Ignore:
Timestamp:
Mar 11, 2013, 1:02:02 PM (4 years ago)
Author:
piccolo
Message:

1) Fixed a litte bug in Joint.ma
2) ERTL to ERTLptr correctness proof in place

Location:
src
Files:
7 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLToERTLptr.ma

    r2820 r2843  
    100100| * #called #args #dest whd in match translate_step; normalize nodelta whd
    101101  [ #l' %{I} %{I} %{I} %
    102   | #r #l' whd %{I} % [2: %{I I} ] % [2: % [2: % [2: %{I} ]]] % try @I %{I} %1 %
     102  | #r #l' whd %{I} %
     103    [2: whd %{I} whd in match step_forall_registers; normalize nodelta
     104        whd in match step_registers; whd in match get_used_registers_from_step;
     105        normalize nodelta normalize cases(\fst called) [#r1 | #b1]
     106        normalize nodelta cases(\snd called) [1,3: #r2 |*: #b2 ]
     107        normalize nodelta /2 by All_mp, I/ % // [1,3,4: %2 % %]
     108        % [%2 %2 % %] %
     109    | %  [2: % [2: % [2: %{I} ]]] % try @I %{I} %1 %
     110    ]
    103111  ]
    104112| #a #l_true whd #l %{I} %{I} % %{I} [ %2 ] %1 %
     
    111119qed.
    112120
     121
    113122definition ertl_to_ertlptr: ertl_program → ertlptr_program ≝
    114123  b_graph_transform_program ERTL ERTLptr translate_data.
  • src/ERTL/ERTLtoERTLptrOK.ma

    r2801 r2843  
    122122∀f_bl_r.
    123123b_graph_transform_program_props ERTL_semantics ERTLptr_semantics
    124      translate_data prog f_bl_r f_lbls f_regs →
     124     (λglobals,fn.«translate_data globals fn,(refl …)») prog f_bl_r f_lbls f_regs →
    125125∀st,fn,id,stmt.
    126126fetch_statement ERTL_semantics (prog_var_names … prog)
     
    167167 ∀f_bl_r.
    168168 b_graph_transform_program_props ERTL_semantics ERTLptr_semantics
    169      translate_data prog f_bl_r f_lbls f_regs →
     169     (λglobals,fn.«translate_data globals fn,(refl …)») prog f_bl_r f_lbls f_regs →
    170170 ∀st2 : state_pc ERTLptr_semantics.
    171171 let st1 ≝ sigma_state_pc prog f_lbls f_regs st2 in
     
    197197normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct(EQ) lapply EQfetch
    198198>(fetch_stmt_ok_sigma_pc_ok … EQfetch) #EQfetch'
    199 lapply(fetch_statement_inv … EQfetch') * #EQfn #EQstmt
    200 cases(b_graph_transform_program_fetch_internal_function … good … EQfn)
     199cases(b_graph_transform_program_fetch_statement_plus … good … EQfetch')
    201200#init_data * #t_fn1 ** #EQt_fn1 whd in ⊢ (% → ?); cases (f_bl_r ?) normalize nodelta
    202 [2: #r #tl *] #EQ destruct(EQ) * #_ #_ #_ #_ #_ #_ #_ #fresh_regs #_ #_ #stmt_at_spec
    203 cases(stmt_at_spec … EQstmt) #labs * #regs ** #EQlabs #EQregs normalize nodelta
    204 >if_merge_right in ⊢ (% → ?); [2: %] whd in ⊢ (% → ?); * #bl * whd in ⊢ (% → ?);
    205 cases regs in EQregs; -regs [2: #x #y #_ *] #EQregs normalize nodelta #EQ destruct(EQ)
    206 #eval_spec
     201[2: #r #tl *] #EQ destruct(EQ) * #labs * #regs ******* #EQlabs #EQregs #_ #_ #_ #_
     202#fresh_regs * #bl * >if_merge_right in ⊢ (% → ?); [2: %]
     203whd in ⊢ (% → ?); cases regs in EQregs; normalize nodelta [2: #x #y #_ *] #EQregs
     204#EQ destruct(EQ) #eval_spec
    207205lapply(err_eq_from_io ????? EQnopc) -EQnopc >(fetch_stmt_ok_sigma_state_ok … EQfetch)
    208206#EQnopc
    209 cases(eval_seq_no_pc_no_call_ok prog f_lbls f_regs ????????? EQnopc)
    210 [2: @(t_fn1)
    211 | #stnopc'' * #EQstnopc'' #EQsem %
     207cases(eval_seq_no_pc_no_call_ok prog f_lbls f_regs ???????? EQnopc)
     208[ #stnopc'' * #EQstnopc'' #EQsem %
    212209  [ % [@stnopc'' | @(succ_pc ERTL_semantics (pc … st2) nxt) | @(last_pop … st2)]]
    213210  %
     
    221218    normalize nodelta * #H @H whd in ⊢ (??%?); >EQfetch %
    222219| #lbl whd in match code_has_label; whd in match code_has_point; normalize nodelta
    223   inversion(stmt_at ????) [#_ *] #stmt1 #EQstmt1 #_ cases(stmt_at_spec … EQstmt1)
    224   #labels * #registers ** #_ #EQregisters #_ -labels >EQregisters whd
    225   check excluded_middle_list
     220  inversion(stmt_at ????) [#_ *] #stmt1 #EQstmt1 #_
     221  cut(fetch_statement ERTL_semantics (prog_var_names … prog) (globalenv_noinit … prog)
     222                      (pc_of_point ERTL_semantics (pc_block (pc … st2)) lbl) =
     223                 return 〈f,fn,stmt1〉)
     224   [ lapply(fetch_statement_inv … EQfetch') * #EQfn #_ whd in ⊢ (??%?);
     225     >EQfn normalize nodelta >point_of_pc_of_point >EQstmt1 %] #EQf_stmt1
     226  cases(b_graph_transform_program_fetch_statement_plus … good … EQf_stmt1)
     227  #init * #t_fn' ** #EQt_fn' whd in ⊢ (% → ?); cases(f_bl_r ?) [2: #x #y *]
     228  normalize nodelta #EQ destruct(EQ) * #labels * #registers
     229  ******* #EQlabels >point_of_pc_of_point change with (pc_block (pc … st2)) in match (pc_block ?);
     230  #EQregisters #_ #_ #_ #_ #_ #_ >EQregisters
    226231  cases(excluded_middle_list ? (λreg.bool_to_Prop(¬(reg∈registers)))
    227          (get_used_registers_from_seq … (functs ERTL) stmt) ?)
    228   [3: #a #_ cases(¬a∈registers) // |1: #H assumption] #H @⊥
     232         (get_used_registers_from_seq … (functs ERTL) stmt) ?)
     233  [3: #a #_ cases(¬a∈registers) // |1: #H assumption] #H @⊥
     234  lapply(fetch_statement_inv … EQfetch') * #_ normalize nodelta #EQstmt
    229235  cases(Exists_All … H (regs_are_in_univers … (pi2 ?? fn) … EQstmt))
    230   #reg ** #H1 #H2 @H1 -H1 @notb_Prop % #H1 lapply(fresh_regs … lbl) >EQregisters
     236   #reg ** #H1 #H2 @H1 -H1 @notb_Prop % #H1 lapply(fresh_regs … lbl) >EQregisters
    231237  whd in ⊢ (% → ?); #H3 lapply(All_memb … H3 H1) ** #H4 #_ @H4 assumption
    232238]
     
    239245 ∀f_bl_r.
    240246 b_graph_transform_program_props ERTL_semantics ERTLptr_semantics
    241      translate_data prog f_bl_r f_lbls f_regs →
     247     (λglobals,fn.«translate_data globals fn,(refl …)») prog f_bl_r f_lbls f_regs →
    242248 ∀st2.
    243249 let st1 ≝ (sigma_state_pc prog f_lbls f_regs st2) in
     
    456462 ∀f_bl_r.
    457463 ∀ good :b_graph_transform_program_props ERTL_semantics ERTLptr_semantics
    458      translate_data prog f_bl_r f_lbls f_regs.
     464     (λglobals,fn.«translate_data globals fn,(refl …)») prog f_bl_r f_lbls f_regs.
    459465∀st2,st1',f,fn,a,ltrue,lfalse.
    460466let st1 ≝ sigma_state_pc prog f_lbls f_regs st2 in
     
    561567 ∀f_bl_r.
    562568 ∀ good :b_graph_transform_program_props ERTL_semantics ERTLptr_semantics
    563      translate_data prog f_bl_r f_lbls f_regs.
     569     (λglobals,fn.«translate_data globals fn,(refl …)») prog f_bl_r f_lbls f_regs.
    564570∀st2,st1',f,fn,c,nxt.
    565571let st1 ≝ sigma_state_pc prog f_lbls f_regs st2 in
     
    609615 ∀f_bl_r.
    610616 ∀ good :b_graph_transform_program_props ERTL_semantics ERTLptr_semantics
    611      translate_data prog f_bl_r f_lbls f_regs.
     617     (λglobals,fn.«translate_data globals fn,(refl …)») prog f_bl_r f_lbls f_regs.
    612618 ∀st2,st1',f,fn,called,args,dest,nxt.
    613619 let st1 ≝ sigma_state_pc prog f_lbls f_regs st2 in
     
    628634 (ev_genv … (mk_prog_params ERTLptr_semantics trans_prog stack_sizes)) st2_pre_call
    629635 =return st2'.
    630 #prog #f_lbls #f_regs #stack_size #f_bl_r #good #st2 #st1' #f #fn * [#c_id | #c_ptr]
     636#prog #f_lbls #f_regs #stack_size #f_bl_r #good #st2 #st1' #f #fn * [#c_id | * #c_ptr1 #c_ptr2 ]
    631637#args #dest #nxt #EQfetch whd in match eval_state; normalize nodelta >EQfetch
    632638>m_return_bind whd in match eval_statement_no_pc; normalize nodelta >m_return_bind
     
    652658lapply EQfetch >(fetch_stmt_ok_sigma_pc_ok … EQfetch) in ⊢ (% → ?);
    653659#EQfetch' lapply(fetch_statement_inv … EQfetch') * #EQfn normalize nodelta #EQstmt
    654 cases(b_graph_transform_program_fetch_internal_function … good … EQfn)
     660cases(b_graph_transform_program_fetch_statement_plus … good … EQfetch')
    655661#init_data * #calling' ** #EQcalling' whd in ⊢ (% → ?); cases(f_bl_r ?)
    656 [2,4: #x #y *] normalize nodelta #EQ destruct(EQ) * #_ #_ #_ #_ #_
    657 #_ #_ #_ #_ #_ #H cases(H … EQstmt) -H #labels * #registers
    658 ** #EQlabels #EQregisters normalize nodelta >if_merge_right [2,4: %]
    659 whd in match translate_step; normalize nodelta * #bl *
    660 cases registers in EQregisters; -registers normalize nodelta
    661 [2,3: [ #x #y] #_ *|4: #r #tl] #EQregisters
     662[2,4: #x #y *] normalize nodelta #EQ destruct(EQ) * #labels * #registers
     663******* #EQlabels #EQregisters #_ #_ #_ #_ #fresh_regs
     664normalize nodelta >if_merge_right [2,4: %] whd in match translate_step;
     665normalize nodelta * #bl * cases registers in EQregisters; -registers
     666normalize nodelta [2,3: [ #x #y] #_ *|4: #r #tl] #EQregisters
    662667[ whd in ⊢ (% → ?); cases tl in EQregisters; -tl [2: #x #y #_ *] normalize nodelta
    663668#EQregisters | whd in ⊢ (% → ?);] #EQ destruct(EQ)
     
    673678[1,3: @hide_prf whd in ⊢ (??%?); >EQfetch %]
    674679cases(ertl_save_frame_ok prog f_lbls f_regs ?
    675   (added_registers ERTL (prog_var_names … prog) fn (f_regs (pc_block (pc … st2))))
    676   ? st1''' ?)
     680  (added_registers ERTL (prog_var_names … prog) fn1 (f_regs c_bl')) ? st1''' ?)
    677681[2: @PTR
    678682|3,7: [ %{(mk_state_pc ? (st_no_pc … st2)
     
    704708  whd in match set_no_pc; normalize nodelta]
    705709#EQst_no_pc_after_call #EQ destruct(EQ)
    706 [ %{(mk_state_pc ? st_no_pc_pre_call
     710[ letin pairpc ≝ (beval_pair_of_pc
     711                     (pc_of_point ERTLptr_semantics (pc_block (pc … st2)) mid1))
     712  %{(mk_state_pc ? (set_regs ERTL_state
     713                      (〈add ?? (\fst (regs … st2)) r (\snd pairpc),\snd(regs … st2)〉)
     714                      st_no_pc_pre_call)
    707715                   (pc_of_point ERTLptr_semantics (pc_block (pc … st2)) mid1)
    708716                   (last_pop … st2))}
     
    732740  ]
    733741|4: %{(taa_base …)}
    734 | lapply(produce_trace_any_any_free (mk_prog_params ERTLptr_semantics (ertl_to_ertlptr prog) stack_size)
     742| %{(taaf_to_taa ???
     743      (produce_trace_any_any_free
     744           (mk_prog_params ERTLptr_semantics (ertl_to_ertlptr prog) stack_size)
    735745           st2 ?????
    736            (mk_state_pc ? st_no_pc_pre_call
    737                    (pc_of_point ERTLptr_semantics (pc_block (pc … st2)) mid1)
    738                    (last_pop … st2)) EQcalling' m_fetch_pre ?)
    739   [2: #taaf inversion(taaf)
    740       [ #s #EQ #EQ1 @⊥ destruct(EQ EQ1) cases s in EQ1 EQst_no_pc_pre_call;
    741         * #fms #is #bb #regs #m #y #z #EQ #H @('bind_inversion H) -H #a1
    742         #H @('bind_inversion H) -H #is1 whd in ⊢ (??%% → ?); cases is in EQ;
    743         [2: #bv1 |3: #bv1 #bv2] #EQ whd in ⊢ (??%% → ?); #EQ1 destruct(EQ1)
    744         whd in ⊢ (??%% → ??%% → ?); #EQ1 destruct(EQ1) normalize nodelta
    745         whd in ⊢ (??%% → ?); #EQ1 destruct(EQ1) destruct(EQ)
    746       |3: #s1 #s2 #s3 #taa #H1 #H2 #H3 #EQ #EQ1 @⊥ destruct(EQ EQ1)
    747           lapply H3 -H3 whd in ⊢ (% → ?); whd in match (as_label ??);
    748           whd in match fetch_statement; normalize nodelta
    749           whd in match (as_pc_of ??); >EQcalling' >m_return_bind
    750           whd in match point_of_pc; normalize nodelta; >point_of_offset_of_point
    751           >EQcall normalize nodelta whd in match cost_label_of_stmt;
    752           normalize nodelta * #H @H %
    753       ]
    754       #s1 #s2 #s3 #taa #H1 #H2 #EQst2 #EQs3 #_ <EQst2 in taa; <EQs3 in H1; #H1 #taa
    755        %{(taa_append_taa … taa (taa_step … H1 … (taa_base …)))}
    756                  xxxxxxxxxxxxxxxxxxxx
    757 |3,7: whd in match sigma_pc_opt; normalize nodelta @if_elim
    758       [1,3: @eqZb_elim [2,4: #_ *] #EQbl >fetch_internal_function_no_minus_one in EQfn;
    759            [1,3: #EQ destruct(EQ) |*: assumption]]
    760       #_ [
    761 
    762 
    763 whd in ⊢ (% → ?);
    764 [ * #mid * #resg ** #EQ destruct(EQ) whd in ⊢ (% → ?);
    765   * #nxt1 * #EQlow change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ)
    766   whd in ⊢ (% → ?); * #mid3 * #rest1 ** #EQ destruct(EQ) * #nxt1 *
    767   #EQpush1 change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ)
    768   whd in ⊢ (% → ?); * #mid4 * #rest2 ** #EQ destruct(EQ) * #nxt1 * #EQhigh
    769   change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) whd in ⊢ (% → ?);
    770   * #mid5 * #rest3 ** #EQ destruct(EQ) * #nxt1 * #EQpush2
    771   change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) whd in ⊢ (% → ?);
    772 ] * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in EQmid1 : (??%%); destruct(EQmid1)
    773 whd in ⊢ (% → ?); * #nxt1 * #EQcall #EQ destruct(EQ) whd in ⊢ (% → ?);
    774 * #EQ destruct(EQ) change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ)
    775 
    776 
    777 
    778 
    779 
    780 
    781 
    782 
    783 
    784 
    785  
    786 [ letin pairpc ≝ (beval_pair_of_pc (pc_of_point ERTLptr_semantics (pc_block (pc … st2)) mid1))
    787   letin st2_pre ≝ (mk_state_pc ?
    788     (mk_state ? (st_frms … st2) (both_is (\fst pairpc) (\snd pairpc))
    789     (carry … st2) (〈add ?? (\fst (regs … st2)) r (\snd pairpc),\snd(regs … st2)〉)
    790     (m … st2))
    791     (pc_of_point ERTLptr_semantics (pc_block (pc … st2)) mid1)
    792     (last_pop … st2))
    793  %{st2_pre}
    794 | %{st2}
    795 ] % 
    796 [1,3: @hide_prf whd in ⊢ (??%?); whd in match fetch_statement; normalize nodelta
    797       >EQcalling' >m_return_bind [>point_of_pc_of_point ] >EQcall >m_return_bind % ]
     746           (mk_state_pc ?
     747                (set_regs ERTL_state
     748                      (〈add ?? (\fst (regs … st2)) r (\snd pairpc),\snd(regs … st2)〉)
     749                      st_no_pc_pre_call)
     750                (pc_of_point ERTLptr_semantics (pc_block (pc … st2)) mid1)
     751                (last_pop … st2))
     752           EQcalling' m_fetch_pre ?) ?)}
     753  [ @if_elim [2: #_ @I] #_ % whd in ⊢ (% → ?); whd in match (as_label ??);
     754    whd in match (as_pc_of ??); whd in match fetch_statement; normalize nodelta
     755    >EQcalling' >m_return_bind whd in match point_of_pc; normalize nodelta
     756    >point_of_offset_of_point >EQcall >m_return_bind normalize nodelta
     757    whd in match cost_label_of_stmt; normalize nodelta * #H @H %
     758  | whd in match repeat_eval_seq_no_pc; normalize nodelta whd in ⊢ (??%?);
     759    whd in match eval_seq_no_pc in ⊢ (??match % with [_ ⇒ ?| _ ⇒ ?]?);
     760    normalize nodelta whd in match (eval_ext_seq ????????);
     761    whd in match (get_pc_from_label ?????); whd in match block_of_funct_id;
     762    normalize nodelta @('bind_inversion EQfn) * #f2 * #fn2
     763    whd in match fetch_function; normalize nodelta #H
     764    lapply(opt_eq_from_res ???? H) -H #H @('bind_inversion H) -H #f3 #EQf3
     765    #H @('bind_inversion H) -H #fn4 #_ whd in ⊢ (??%%→ ??%% → ?); #EQ1 #EQ2
     766    destruct(EQ1 EQ2)
     767    >(find_symbol_transf …
     768            (λvars.transf_fundef … (λfn.(b_graph_translate … fn))) prog f)
     769    >(symbol_of_block_rev … EQf3) >m_return_bind >code_block_of_block_eq
     770    normalize nodelta >(pc_of_label_eq … EQcalling') normalize nodelta
     771    whd in ⊢ (??%?);
     772    whd in match eval_seq_no_pc in ⊢ (??match % with [_ ⇒ ?| _ ⇒ ?]?);
     773    normalize nodelta whd in match (eval_ext_seq ????????);
     774    whd in match acca_arg_retrieve; normalize nodelta
     775    change with (ps_reg_retrieve ??) in match (acca_arg_retrieve_ ?????);
     776    whd in match ps_reg_retrieve; whd in match reg_retrieve; normalize nodelta
     777    >lookup_add_hit >m_return_bind whd in match set_regs; normalize nodelta
     778    @('bind_inversion EQst_no_pc_pre_call) #new_st whd in match push in ⊢ (%→ ?);
     779    normalize nodelta #H @('bind_inversion H) -H #is1 #EQis1 whd in ⊢ (??%% → ?);
     780    #EQ destruct(EQ) #H @('bind_inversion H) -H #is2 #EQis2 whd in match set_istack;
     781    normalize nodelta whd in ⊢ (??%% → ?); #EQ destruct(EQ) whd in match push;
     782    normalize nodelta >EQis1 >m_return_bind whd in match set_istack; normalize nodelta
     783    whd in ⊢ (??%?); whd in match eval_seq_no_pc in ⊢ (??match % with [_ ⇒ ?| _ ⇒ ?]?);
     784    normalize nodelta whd in match (eval_ext_seq ????????);
     785    whd in match (get_pc_from_label ?????); whd in match block_of_funct_id;
     786    normalize nodelta
     787    >(find_symbol_transf …
     788            (λvars.transf_fundef … (λfn.(b_graph_translate … fn))) prog f)
     789    >(symbol_of_block_rev … EQf3) >m_return_bind >code_block_of_block_eq
     790    normalize nodelta >(pc_of_label_eq … EQcalling') normalize nodelta
     791    whd in ⊢ (??%?);
     792    whd in match eval_seq_no_pc in ⊢ (??match % with [_ ⇒ ?| _ ⇒ ?]?);
     793    normalize nodelta whd in match (eval_ext_seq ????????);
     794    whd in match acca_arg_retrieve; normalize nodelta
     795    change with (ps_reg_retrieve ??) in match (acca_arg_retrieve_ ?????);
     796    whd in match ps_reg_retrieve; whd in match reg_retrieve; normalize nodelta
     797    >lookup_add_hit >m_return_bind whd in match set_regs; normalize nodelta
     798    whd in match push; normalize nodelta >EQis2 >m_return_bind normalize nodelta
     799    whd in ⊢ (??%?); @eq_f whd in match set_istack; normalize nodelta
     800    whd in match reg_store; normalize  nodelta >add_idempotent %
     801  | cut(∀st,st',kind.ertlptr_save_frame kind it st = return st' →
     802                ∃hd,tl.st_frms … st' = return (cons ? hd tl) ∧
     803                \snd hd = pc_block (pc … st))
     804    [ #st * #frms #is #b #regs #m * whd in match ertlptr_save_frame;
     805      normalize nodelta [ >m_return_bind | #H @('bind_inversion H) -H #st'' #EQst'']
     806      #H @('bind_inversion H) -H #frames #H lapply(opt_eq_from_res ???? H) -H
     807      #EQframes whd in ⊢ (??%% → ?); whd in match set_frms; whd in match set_regs;
     808      normalize nodelta #EQ destruct(EQ) %{(〈\fst (regs ERTLptr_semantics ?),pc_block (pc … st)〉)}
     809      [2,4: %{frames} % [1,3: %] |1,3:] %]
     810    ] #save_frame_non_empty cases(save_frame_non_empty … EQst_no_pc_after_call)
     811    * #fst_hd #snd_hd * #rest * #EQrest #EQhd
     812  ]
     813cases(b_graph_transform_program_fetch_internal_function … good c_bl' f1 fn1 ?)
     814[2,4: whd in match fetch_internal_function; normalize nodelta >EQfn1 %]
     815#init * #t_fn1 ** #EQt_fn1 #_ * #_ #_ #_ #EQentry #_ #_ #_ #_ #_ #_ #_
     816[ %{(mk_state_pc ? st_no_pc_after_call
     817        (pc_of_point
     818            (mk_prog_params ERTLptr_semantics (ertl_to_ertlptr prog) stack_size)
     819             c_bl' (joint_if_entry … t_fn1))
     820        (last_pop … st2))}
     821|
     822%{(mk_state_pc ? (set_frms ERTL_state (〈(add ?? (fst_hd) r (\snd pairpc)),snd_hd〉
     823                                 :: rest)
     824                          st_no_pc_after_call)
     825        (pc_of_point
     826            (mk_prog_params ERTLptr_semantics (ertl_to_ertlptr prog) stack_size)
     827             c_bl' (joint_if_entry … t_fn1))
     828        (last_pop … st2))}
     829]
    798830%
    799 [1,3: %
    800   [1,3: whd in ⊢ (??%%); whd in match fetch_statement in ⊢ (??%?);
    801         normalize nodelta >EQcalling' in ⊢ (??(match % with [_ ⇒ ? | _ ⇒ ?])?);
    802         >m_return_bind in ⊢ (??(match % with [_ ⇒ ? | _ ⇒ ?])?);
    803        [ >point_of_pc_of_point in ⊢ (??(match % with [_ ⇒ ? | _ ⇒ ?])?);]
    804        >EQcall in ⊢ (??(match % with [_ ⇒ ? | _ ⇒ ?])?); normalize nodelta
    805        >(fetch_stmt_ok_sigma_pc_ok … EQfetch) in ⊢ (???(match % with [_ ⇒ ? | _ ⇒ ?]));
    806        >EQfetch' in ⊢ (???(match % with [_ ⇒ ? | _ ⇒ ?])); %
    807   |*: whd in match sigma_stored_pc; whd in match sigma_pc_opt; normalize nodelta
    808       @if_elim change with (pc_block(pc … st2)) in match (pc_block ?);
    809       [1,3: @eqZb_elim [2,4: #_ *] #EQbl #_
    810       >fetch_internal_function_no_minus_one in EQcalling'; [2,4: assumption]
    811       whd in ⊢ (???% → ?); #ABS destruct(ABS) ] #_
    812       [ >point_of_pc_of_point >(get_sigma_last … good … EQfn EQstmt EQlabels)
    813       | >(get_sigma_idempotent … good … EQfn EQstmt EQlabels)
    814       ]
    815       >m_return_bind >pc_of_point_of_pc %
    816   ]
    817 |4: %{(taa_base …)}
    818 |2: letin st2'' ≝ (mk_state_pc ?
    819                    (mk_state ? (st_frms … st2) (empty_is) (carry … st2)
    820                       (〈add ?? (\fst (regs … st2)) r (\fst pairpc),\snd(regs … st2)〉)
    821                       (m … st2)) (pc_of_point ERTLptr_semantics (pc_block (pc … st2)) mid)
    822                       (last_pop … st2))
    823     letin st2''' ≝ (mk_state_pc ? (set_istack ? (one_is (\fst pairpc)) st2'')
    824                     (pc_of_point ERTLptr_semantics (pc_block (pc … st2)) mid3)
    825                     (last_pop … st2))
    826     letin st2''''≝ (mk_state_pc ? (mk_state ? (st_frms … st2) (istack … st2''')
    827     (carry … st2)
    828     (〈add ?? (\fst (regs … st2''')) r (\snd pairpc),\snd (regs … st2)〉) (m … st2'''))
    829     (pc_of_point ERTLptr_semantics (pc_block (pc … st2)) mid4) (last_pop … st2))
    830     %{(taa_step ? st2 st2'' st2_pre ???
    831         (taa_step ? st2'' st2''' st2_pre ???
    832            (taa_step ? st2''' st2'''' st2_pre ???
    833               (taa_step ? st2'''' st2_pre st2_pre ??? (taa_base …)))))}
    834    [3,6,7,10: % whd in ⊢ (% → ?); * #H @H whd in ⊢ (??%?);
    835               whd in match fetch_statement; normalize nodelta >EQcalling' >m_return_bind
    836               [ >point_of_pc_of_point >EQhigh
    837               | >point_of_pc_of_point >EQcall
    838               | >point_of_pc_of_point >EQpush2
    839               | >point_of_pc_of_point >EQpush1 ] %
    840    |1,2,4,5,8,9,11,12: whd
    841        [1,3,6,8: whd in match eval_state; normalize nodelta
    842        |*: whd in ⊢ (??%?);
     831[1,3: whd in match sigma_state_pc; normalize nodelta
     832      whd in match pc_of_point in ⊢ (???%); normalize nodelta
     833      whd in match fetch_internal_function; normalize nodelta >EQfn1
     834      >m_return_bind normalize nodelta @eq_f3
     835      [1,3,6: % |2,5: >EQentry %]
     836      whd in match sigma_state; normalize nodelta
     837      cut(∀ a1,a2,b1,b2,c1,c2,d1,d2,e1,e2.
     838                    a1=a2 → b1 = b2 → c1 = c2 → d1 = d2 → e1 = e2 →
     839                      mk_state ERTL_semantics a1 b1 c1 d1 e1 =
     840                      mk_state ERTL_semantics a2 b2 c2 d2 e2)
     841       [1,3: #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14
     842                    #H15 //] #APP @APP try %
     843       whd in match set_frms; normalize nodelta >EQrest
     844       whd in match sigma_frames; normalize nodelta >m_return_bind
     845       >m_return_bind whd in match sigma_frames_opt; whd in match m_list_map;
     846       normalize nodelta whd in match (foldr ?????) in ⊢ (???%);
     847       normalize nodelta >EQhd >EQfn >m_return_bind normalize nodelta
     848       whd in match (foldr ?????); normalize nodelta
     849       >EQfn >m_return_bind normalize nodelta 
     850       change with (sigma_frames_opt prog f_lbls f_regs ?)
     851                                            in match (foldr ?????);
     852       change with (sigma_frames_opt prog f_lbls f_regs ?)
     853                                                         in match (foldr ?????);
     854       cases(sigma_frames_opt ????) [%] #t_rest >m_return_bind >m_return_bind
     855       @eq_f @eq_f2 [2: %] @eq_f2 [2: %]
     856       change with (pc_block (pc … st2)) in match (pc_block ?);
     857       change with (pc_block (pc … st2)) in match (pc_block ?);
     858       whd in match sigma_register_env; normalize nodelta
     859       >map_add >set_minus_add [%] @list_as_set_mem @in_added_registers
     860       [@(point_of_pc ERTL_semantics (pc ERTLptr_semantics st2))
     861       | whd in match code_has_label; whd in match code_has_point; normalize nodelta
     862         >EQstmt % | >EQregisters % % ]
     863|*:    whd in match fetch_statement; normalize nodelta; >EQcalling' >m_return_bind
     864       [2: >point_of_pc_of_point ] >EQcall >m_return_bind normalize nodelta
     865       >m_return_bind
     866       [2: >EQc_bl' >m_return_bind
     867       | whd in match block_of_call; normalize nodelta
     868         @('bind_inversion EQst_no_pc_pre_call) #st3 #H @('bind_inversion H) -H
     869         #is3 inversion(istack … st2) [2: #bv |3: #bv1 #bv2] #EQis3
     870         whd in match is_push; normalize nodelta whd in ⊢ (??%% → ??%% → ?);
     871         #EQ1 #EQ2 destruct(EQ1 EQ2) #H @('bind_inversion H) -H #is3
     872         whd in ⊢ (??%% → ??%% → ?); #EQ1 #EQ2 destruct(EQ1 EQ2)
     873         whd in match set_regs; whd in match dpl_arg_retrieve; normalize nodelta
     874         change with (ps_arg_retrieve ??) in match (dpl_arg_retrieve_ ?????);
     875         @('bind_inversion EQc_bl') #c_bl'' whd in match dpl_arg_retrieve; normalize nodelta
     876         change with (ps_arg_retrieve ??) in match (dpl_arg_retrieve_ ?????);
     877         #H @('bind_inversion H) -H #bv_ptr1 whd in match ps_arg_retrieve;
     878         normalize nodelta cases (c_ptr1) in EQstmt; [#r_ptr1 | #b_ptr1] #EQstmt
     879         normalize nodelta
     880         [ whd in match ps_reg_retrieve; whd in match reg_retrieve; normalize nodelta
     881           #H lapply(opt_eq_from_res ???? H) -H #EQbv_ptr1
     882         | whd in ⊢ (??%% → ?); #EQ destruct(EQ)
     883         ]
     884         whd in match dph_arg_retrieve; normalize nodelta
     885         change with (ps_arg_retrieve ??) in match (dph_arg_retrieve_ ?????);
     886         whd in match ps_arg_retrieve; normalize nodelta cases c_ptr2 in EQstmt;
     887         [1,3: #r_ptr2 |*: #b_ptr2] #EQstmt normalize nodelta
     888         [1,2: whd in match ps_reg_retrieve; whd in match reg_retrieve;
     889               normalize nodelta #H @('bind_inversion H) -H
     890               #bv_ptr2 #H lapply(opt_eq_from_res ???? H) -H #EQbv_ptr2
     891         |*:   >m_return_bind
     892         ] #H @('bind_inversion H) -H #ptr #EQptr @if_elim #ptr_ok whd in ⊢ (??%% → ?);
     893         #EQ destruct(EQ) #H lapply(opt_eq_from_res ???? H) -H #EQptr_code
     894         [2,4: >m_return_bind
     895         |*: >lookup_add_miss
     896             [1,3: >EQbv_ptr1 >m_return_bind
     897             |*: % #ABS destruct(ABS)
     898                lapply(fresh_regs (point_of_pc ERTL_semantics (pc … st2)))
     899                >EQregisters whd in ⊢ (% → ?); *** #ABS #_ #_ @ABS
     900                lapply(regs_are_in_univers … (pi2 ?? fn) … EQstmt) whd in match stmt_registers;
     901                whd in match get_used_registers_from_step; normalize nodelta
     902                whd in ⊢ (???% → ?); * //
     903             ]
     904         ]
     905         change with (ps_arg_retrieve ??) in match (dph_arg_retrieve_ ?????);
     906         whd in match ps_arg_retrieve; normalize nodelta
     907         [2,4: >m_return_bind   
     908         |*: whd in match ps_reg_retrieve; whd in match reg_retrieve;
     909             normalize nodelta >lookup_add_miss
     910             [1,3: >EQbv_ptr2 >m_return_bind
     911             |*: % #ABS destruct(ABS)
     912                lapply(fresh_regs (point_of_pc ERTL_semantics (pc … st2)))
     913                >EQregisters whd in ⊢ (% → ?); *** #ABS #_ #_ @ABS
     914                lapply(regs_are_in_univers … (pi2 ?? fn) … EQstmt) whd in match stmt_registers;
     915                whd in match get_used_registers_from_step; normalize nodelta
     916                whd in ⊢ (???% → ?); * // #_ * //
     917             ]
     918         ]
     919         >EQptr >m_return_bind @if_elim [2,4,6,8: >ptr_ok *] #_ >m_return_bind
     920         >EQptr_code >m_return_bind
    843921       ]
    844        whd in match fetch_statement; normalize nodelta >EQcalling' >m_return_bind
    845        [1,5: >point_of_pc_of_point >EQpush1 >m_return_bind [2: %]
    846        |2,6: >point_of_pc_of_point >EQpush2 >m_return_bind [2: %]
    847        |3,7: >point_of_pc_of_point >EQhigh >m_return_bind [2: %]
    848        |*: >EQlow >m_return_bind [2: %]
     922       @('bind_inversion EQt_fn1) * #f2 * #fn2 #EQfn2 normalize nodelta
     923       whd in ⊢ (??%% → ?); #EQ destruct(EQ) >EQfn2 >m_return_bind normalize nodelta
     924       [   change with (ertlptr_save_frame ? it ?) in match (save_frame ??????);
     925           cut(st2 = mk_state_pc ? st2 (pc … st2) (last_pop … st2))
     926           [ cases st2 #H1 #H2 #H3 %] #EQ <EQ -EQ >EQst_no_pc_after_call
     927           >m_return_bind
     928       |*: change with (ertlptr_save_frame PTR it ?) in match (save_frame ??????);
     929           @('bind_inversion EQst_no_pc_after_call) #st4 whd in ⊢ (??%% → ?);
     930           #EQ destruct(EQ) #H @('bind_inversion H) -H #frms4 #H
     931           lapply(opt_eq_from_res ???? H) -H #EQfrms4 whd in ⊢ (??%% → ?);
     932           #EQ destruct(EQ) whd in match ertlptr_save_frame; normalize nodelta
     933           >m_return_bind whd in EQrest : (???%); destruct(EQrest) >EQfrms4
     934           >m_return_bind
    849935       ]
    850        whd in match eval_statement_no_pc; whd in match eval_seq_no_pc; normalize nodelta
    851        whd in match (eval_ext_seq ?????????); whd in match (get_pc_from_label ?????);
    852        whd in match block_of_funct_id; normalize nodelta
    853        [1,2: whd in match acca_arg_retrieve; normalize nodelta
    854              change with (ps_reg_retrieve ??) in match (acca_arg_retrieve_ ?????);
    855              whd in match ps_reg_retrieve; whd in match reg_retrieve; normalize nodelta
    856              >lookup_add_hit >m_return_bind [%| >add_idempotent %]
    857        |*: @('bind_inversion EQfn) * #f2 * #fn2 whd in match fetch_function;
    858            normalize nodelta #H lapply(opt_eq_from_res ???? H) -H
    859            #H @('bind_inversion H) -H #f3 #EQf3 #H @('bind_inversion H) -H
    860            #fn4 #_ whd in ⊢ (??%%→ ??%% → ?); #EQ1 #EQ2 destruct(EQ1 EQ2)
    861           >(find_symbol_transf …
    862              (λvars.transf_fundef … (λfn.(b_graph_translate … fn))) prog f)
    863           >(symbol_of_block_rev … EQf3) >m_return_bind >code_block_of_block_eq
    864           normalize nodelta >(pc_of_label_eq … EQcalling') normalize nodelta
    865           whd in match ps_reg_store_status; normalize nodelta >m_return_bind [%]
    866           whd in match eval_statement_advance; normalize nodelta whd in match set_no_pc;
    867           normalize nodelta whd in match next; whd in match set_pc; normalize nodelta
    868           @eq_f @eq_f3 [2,3: %] whd in match set_regs; normalize nodelta
    869           cut(istack … st2 = empty_is)
    870           [ @('bind_inversion EQst1'') #new_st whd in match push_ra; normalize nodelta
    871             #H @('bind_inversion H) -H #new_st' whd in match push; normalize nodelta
    872             #H @('bind_inversion H) -H #new_is whd in match sigma_state; normalize nodelta
    873             cases(istack ? st2) [ #_ #_ #_ #_ % |3: #bv1 #bv2 whd in ⊢ (??%% → ?); #EQ destruct]
    874             #bv1 whd in ⊢ (??%% → ?); #EQ destruct(EQ) whd in match set_istack; normalize nodelta
    875             whd in ⊢ (??%% → ?); #EQ destruct #H @('bind_inversion H) -H #new_is2 whd in ⊢ (??%% → ?);
    876             #EQ destruct(EQ) ] #EQ >EQ %
    877        ]
    878    ]
     936       change with (stack_size ?) in match (stack_sizes ????); >EQs_size
     937       >m_return_bind %
    879938]
    880 cases(b_graph_transform_program_fetch_internal_function … good c_bl' f1 fn1 ?)
    881 [2,4: whd in match fetch_internal_function; normalize nodelta lapply(err_eq_from_io ????? EQfn1)
    882       -EQfn1 #EQfn1 >EQfn1 %]
    883 #init * #t_fn1 ** #EQt_fn1 #_ * #_ #_ #_ #EQentry #_ #_ #_ #_ #_ #_ #_
    884 [2: %{(mk_state_pc ? (set_frms ERTL_state (〈\fst (regs … st2_pre),pc_block(pc … st2)〉 :: (st_frms … st2))
    885                                  (set_regs ERTL_state (〈empty_map …,\snd (regs … st2)〉) st2_pre))
    886                      (pc_of_point (mk_prog_params ERTLptr_semantics (ertl_to_ertlptr prog) stack_size)
    887                          c_bl' (joint_if_entry … t_fn1))
    888                      (last_pop … st2))}
    889 | @('bind_inversion EQst1'') #new_st
    890   cut(pc … st2 = sigma_stored_pc prog f_lbls (pc … st2))
    891   [ whd in match sigma_stored_pc; whd in match sigma_pc_opt; normalize nodelta
    892     @if_elim [ @eqZb_elim [2: #_ *] #EQbl >fetch_internal_function_no_minus_one in EQfn; [2: //] #EQ destruct]
    893     #_ >(get_sigma_idempotent … good … EQfn EQstmt EQlabels) >m_return_bind >pc_of_point_of_pc %]
    894  #EQ >EQ #EQnew_st cases(push_ra_ok … EQnew_st)
    895  [2: lapply EQ whd in match sigma_stored_pc; normalize nodelta cases(sigma_pc_opt ???) [2: #x #_ % #EQ destruct]
    896      normalize  nodelta #ABS >fetch_internal_function_no_zero in EQfn; [2: >ABS %] #EQ destruct]
    897  #t_new_st * #EQt_new_st #new_st_t_new_st whd in ⊢ (???% → ?); #EQ destruct(EQ)
    898  %{(mk_state_pc ? (set_frms ERTL_state (〈(\fst (regs … t_new_st)), pc_block (pc … st2)〉 :: (st_frms … st2))
    899                              (set_regs ERTL_state (〈empty_map …,\snd(regs … st2)〉) t_new_st))
    900                    (pc_of_point (mk_prog_params ERTLptr_semantics (ertl_to_ertlptr prog) stack_size)
    901                          c_bl' (joint_if_entry … t_fn1))
    902                    (last_pop … st2))}
    903 ] %
    904 [1,3: whd in match sigma_state_pc; normalize nodelta whd in match fetch_internal_function;
    905       normalize nodelta lapply(err_eq_from_io ????? EQfn1) -EQfn1 #EQfn1 >EQfn1 >m_return_bind
    906       normalize nodelta @eq_f3 try % [2,4: >EQentry %] whd in match sigma_state; normalize nodelta
    907       whd in match set_frms; whd in match set_regs; normalize nodelta
    908       [ @('bind_inversion EQst1'') #new_st #H @('bind_inversion H) -H #new_st1
    909         #H @('bind_inversion H) -H #new_is whd in match is_push; normalize nodelta
    910         whd in match sigma_state; normalize nodelta cases (istack … st2) normalize nodelta
    911         [3: #bv1 #bv2 whd in ⊢ (???% → ?); #EQ destruct(EQ) |2: #bv] whd in ⊢ (??%% → ?);
    912         #EQ destruct(EQ) whd in ⊢ (??%% → ?); #EQ destruct(EQ) whd in ⊢ (??%% → ?); #EQ destruct
    913         whd in ⊢ (???% → ?); #EQ destruct(EQ)
    914       ]
    915       cut(∀ a1,a2,b1,b2,c1,c2,d1,d2,e1,e2.a1=a2 → b1 = b2 → c1 = c2 → d1 = d2 → e1 = e2 →
    916             mk_state ERTL_semantics a1 b1 c1 d1 e1 =
    917             mk_state ERTL_semantics a2 b2 c2 d2 e2)
    918        [1,3: #H1 #H2 #H3 #H4 #H5 #H6 #H7 #H8 #H9 #H10 #H11 #H12 #H13 #H14 #H15 //]
    919        #APP @APP
    920        [ whd in match sigma_frames in ⊢ (???%); normalize nodelta whd in match sigma_frames_opt;
    921          whd in match m_list_map; normalize nodelta whd in match (foldr ?????);
    922          normalize nodelta >EQfn >m_return_bind normalize nodelta
    923          check coerced_step_list_in_code
    924          whd in match sigma_frames; whd in match sigma_frames_opt; whd in match m_list_map;
    925          normalize nodelta cases(foldr ? (Option ?) ???) [%
    926         //
    927         whd in ⊢
    928       xxxxxxxxxxxxxxxxxxxxxxxx
    929      
    930       change with c_bl' in match (pc_block ?) in ⊢ (???%); >EQfn1               
    931 change with (ge … (ev_genv (mk_prog_params ERTL_semantics prog stack_size)))
    932  in match (globalenv_noinit ? prog); >EQfn1
    933 change with 
    934  
    935           #EQnew_st whd in ⊢ (???% → ?); #EQ destruct(EQ) cases(push_ra_ok ???????? EQnew_st)
    936          
    937           xxxxxxxxxxx
    938           lapply EQfn whd in match fetch_internal_function; whd in match fetch_function;
    939           normalize nodelta
    940           check find_symbol
    941 letin (*〈addrl,addrh〉*) x ≝  beval_pair_of_pc ? %
    942 
    943 
    944 
    945 %{(mk_state_pc ?
    946     (mk_state ? (st_frms … st2)
    947     (both_is (\snd (beval_pair_of_pc (pc … st2)))
    948              (\fst (beval_pair_of_pc (pc … st2))))
    949     (carry … st2) (regs … st2) (m … st2))
    950     (pc … st2)
    951     (last_pop … st2))}
    952 
    953 
    954 
    955 
    956 
    957 
    958 
    959 
    960 
     939qed.
     940         
    961941
    962942inductive ex_Type1 (A:Type[1]) (P:A → Prop) : Prop ≝
     
    965945
    966946lemma ertl_to_ertlptr_ok:
    967 ∀prog.
     947∀prog.∀stack_sizes.
    968948let trans_prog ≝ ertl_to_ertlptr prog in
    969 ∀ f_lbls,f_regs,stack_sizes.
    970  ∀f_bl_r.
    971  b_graph_transform_program_props ERTL_semantics ERTLptr_semantics
    972      translate_data prog f_bl_r f_lbls f_regs →
    973949   ex_Type1 … (λR.
    974950   status_simulation
    975951    (ERTL_status prog stack_sizes) (ERTLptr_status trans_prog stack_sizes) R).
    976 #prog #f_lbls #f_regs #stack_size #f_bl_r #good %
     952#prog #stack_size
     953cases(make_b_graph_transform_program_props ERTL_semantics ERTLptr_semantics
     954          (λglobals,fn.«translate_data globals fn,(refl …)») prog)
     955#fregs * #f_lbls * #f_bl_r #good %
    977956[@ERTLptrStatusSimulation assumption]
    978957whd in match status_simulation; normalize nodelta
     
    987966[ * [ #cost | #called_id #args #dest| #reg #lbl | #seq] #nxt | #fin_step | *]
    988967#EQfetch
    989 change with (joint_classify ??) in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]);
    990 [ (*COST*) whd in match joint_classify; normalize nodelta >EQfetch >m_return_bind
    991   normalize nodelta
     968change with (joint_classify ??) in
     969                     ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? | _ ⇒ ? ]);
     970[ (*COST*) whd in match joint_classify; normalize nodelta >EQfetch normalize nodelta
    992971  cases(eval_cost_ok … good … EQfetch EQeval) #st2' * #EQst2' * #taf #tafne
    993972  %{st2'} %{taf} >tafne normalize nodelta % [ % [@I | assumption]]
    994973  whd >EQst2' >(as_label_ok … good … st2') [%] cases daemon (* needs lemma see below!! *)
    995 | (*CALL*)  whd in match joint_classify; normalize nodelta >EQfetch >m_return_bind
     974| (*CALL*)  whd in match joint_classify; normalize nodelta >EQfetch
    996975          normalize nodelta #is_call_st1
    997976          cases(eval_call_ok … good … EQfetch EQeval) #is_call_st1'
     
    1001980          %{st2'} %{st2'} %{taa} %{(taa_base …)} % [ % assumption]
    1002981          whd >sem_rel >(as_label_ok … good … st2') [%] cases daemon (*TODO*)
    1003 | (*COND*) whd in match joint_classify; normalize nodelta >EQfetch >m_return_bind
     982| (*COND*) whd in match joint_classify; normalize nodelta >EQfetch
    1004983          normalize nodelta #n_costed
    1005984          cases(eval_cond_ok … good … EQfetch EQeval) [2: @n_costed]
    1006985          #st2' * #EQst2' * #taf #tafne %{st2'} %{taf} >tafne % [% [@I|assumption]]
    1007986          whd >EQst2' >(as_label_ok … good … st2') [%] cases daemon (*TODO*)
    1008 | (*seq*) whd in match joint_classify; normalize nodelta >EQfetch >m_return_bind
     987| (*seq*) whd in match joint_classify; normalize nodelta >EQfetch
    1009988          normalize nodelta
    1010989          cases (eval_seq_no_call_ok … good … EQfetch EQeval)
     
    1014993|  cases fin_step in EQfetch;
    1015994  [ (*GOTO*) #lbl #EQfetch  whd in match joint_classify; normalize nodelta
    1016      >EQfetch in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]); normalize nodelta
     995     >EQfetch normalize nodelta
    1017996    cases (eval_goto_ok … good  … EQfetch EQeval)
    1018997    #st3 * #EQ destruct * #taf #tarne %{st3} %{taf} >tarne normalize nodelta
     
    10211000  | (*RETURN*) #EQfetch
    10221001     whd in match joint_classify; normalize nodelta
    1023     >EQfetch in ⊢ (match % with [ _ ⇒ ? | _ ⇒ ? ]); normalize nodelta
     1002    >EQfetch normalize nodelta
    10241003    cases (eval_return_ok … good … EQfetch EQeval) #is_ret
    10251004    * #st3 * #EQ destruct * #after_ret * #taf ** #taf_prf #EQeval' #ret_prf
  • src/ERTL/ERTLtoERTLptrUtils.ma

    r2801 r2843  
    2929
    3030definition sigma_map ≝  block → label → option label.
    31 definition lbl_funct ≝  block → label → option (list label).
    32 definition regs_funct ≝ block → label → option (list register).
     31definition lbl_funct ≝  block → label → (list label).
     32definition regs_funct ≝ block → label → (list register).
    3333
    3434(*TO BE MOVED*)
     
    4949! 〈id,fn〉 ← res_to_opt … (fetch_internal_function … ge bl);
    5050!〈res,s〉 ← find ?? (joint_if_code … fn)
    51                 (λlbl.λ_. match f_lbls bl lbl with
    52                           [None ⇒ false
    53                           |Some lbls ⇒
    54                              match split_on_last … lbls with
    55                                 [None ⇒ eq_identifier … searched lbl
    56                                 |Some x ⇒ eq_identifier … searched (\snd x)
    57                                 ]
     51                (λlbl.λ_. match split_on_last … (f_lbls bl lbl) with
     52                          [None ⇒ eq_identifier … searched lbl
     53                          |Some x ⇒ eq_identifier … searched (\snd x)
    5854                          ]);
    5955return res.
     
    682678∀globals : list ident.∀fn,f_regs,r.
    683679(∀lbl. code_has_label p globals (joint_if_code … fn) lbl →
    684        opt_All … (λl.¬(bool_to_Prop (r ∈ l))) (f_regs lbl)) →
     680       ¬(bool_to_Prop (r ∈ (f_regs lbl)))) →
    685681¬ (r ∈ (set_from_list RegisterTag (added_registers p globals fn f_regs))).
    686682#p #globals #fn #f_regs #r #H whd in match added_registers; normalize nodelta
     
    689685lapply(H lbl ?)
    690686 [whd in match code_has_label; whd in match code_has_point; normalize nodelta
    691   whd in match (stmt_at ????); >EQstmt @I] cases(f_regs lbl)
    692   [ #_ @notb_Prop % assumption]
    693 #l whd in ⊢ (% → ?); normalize nodelta * #H1 @notb_elim @if_elim [2: #_ @I] #ABS
     687  whd in match (stmt_at ????); >EQstmt @I]
     688* #H1 @notb_elim @if_elim [2: #_ @I] #ABS
    694689lapply(mem_list_as_set … ABS) #ABS' cases(Exists_append … ABS') #ABS''
    695 [ @H1 @Exists_memb lapply ABS'' elim l [ *] #hd #tl #IH whd in ⊢ (% → %);
     690[ @H1 @Exists_memb lapply ABS'' elim (f_regs lbl) [ *] #hd #tl #IH whd in ⊢ (% → %);
    696691  * [ #EQ >EQ % %] #H %2 @IH @H
    697692| @IH @list_as_set_mem assumption
     
    699694qed.
    700695
     696lemma Exists_append1 : ∀A.∀l1,l2 : list A.∀a : A.In A l1 a → In A (l1@l2) a.
     697#A #l1 elim l1 [#l2 #a *] #hd #tl #IH *
     698[#a normalize * [#H % assumption | #H %2 >append_nil assumption]]
     699#hd1 #tl1 #a normalize * [#H % assumption | #H %2 @IH assumption]
     700qed.
     701
     702lemma Exists_append2 : ∀A.∀l1,l2 : list A.∀a : A.In A l2 a → In A (l1@l2) a.
     703#A #l1 #l2 lapply l1 -l1 elim l2 [#l1 #a *] #hd #tl #IH *
     704[#a normalize * [#H %1 assumption| #H %2 assumption]]
     705#hd1 #tl1 #a normalize *
     706[ #H %2 >append_cons @Exists_append1 >H elim tl1 [% %] #hd2 #tl2 #H1 normalize %2 //
     707| #H %2 >append_cons @IH assumption]
     708qed.
     709
     710lemma append_All : ∀A : Type[0]. ∀ P : A → Prop. ∀l1,l2 : list A.
     711All ? P (l1 @ l2) → All ? P l1 ∧ All ? P l2.
     712#A #P #l1 elim l1
     713[ #l2 change with l2 in ⊢ (???% → ?); #H % //]
     714#a #tl #IH #l2 change with (P a ∧ All A P (tl @ l2)) in ⊢ (% → ?);
     715* #H1 #H2 lapply(IH … H2) * #H3 #H4 % // whd % //
     716qed.
     717
     718include alias "common/PositiveMap.ma".
     719
     720lemma added_register_pm : ∀A,B. ∀m : positive_map A.
     721∀f : Pos → list B.∀b.
     722let added ≝ fold A (list B) (λp.λ_.λacc.(f p)@acc) m [ ] in
     723All B (λx.x≠b) added →
     724(∀i. lookup_opt unit i (domain_of_pm A m) ≠ None ? → All B (λx.x≠b) (f i)).
     725#A #B #m #f #b normalize nodelta @pm_fold_ind
     726[ #_ #i normalize * #H @⊥ @H %
     727| #p #ps #a #lst #H #H1 #H2 #H3 #i cases(decidable_eq_pos i p)
     728  [1,3: #EQ destruct(EQ) #_ cases(append_All … H3) //
     729  |*: #Hi >lookup_opt_insert_miss [2,4: assumption] @H2
     730      cases(append_All … H3) //
     731  ]
     732]
     733qed.
     734
     735lemma decidable_In : ∀A.∀l : list A. ∀a : A. (∀a'.decidable (a = a')) → 
     736decidable (In A l a).
     737#A #l elim l [ #a #_ %2 % *] #hd #tl #IH #a #DEC cases(IH a DEC)
     738[ #H % %2 assumption | * #H cases (DEC hd)
     739[ #H1 %1 %1 assumption | * #H1 %2 % * [ #H2 @H1 assumption | #H2 @H assumption]]
     740qed.
     741
     742lemma In_all : ∀A.∀l : list A. ∀ a : A.¬In A l a → All A (λx.x≠a) l.
     743#A #l elim l [ #a #_ @I] #hd #tl #IH #a * #H % [2: @IH % #H1 @H %2 assumption]
     744% #H1 @H % >H1 %
     745qed.
     746
     747lemma All_In : ∀A.∀l : list A. ∀ a : A.All A (λx.x≠a) l → ¬In A l a.
     748#A #l elim l [#a #_ % *] #hd #tl #IH #a ** #H1 #H2 % *
     749[ #H3 @H1 >H3 % | cases(IH a H2) #H3 #H4 @H3 assumption]
     750qed.
     751
     752lemma added_register_aux : ∀tag,A,B.∀m : identifier_map tag A.
     753∀f : identifier tag → list B.(∀b,b' : B.decidable (b=b')) →
     754let added ≝ foldi A (list B) tag (λl.λ_.λacc. (f l)@acc) m [ ] in
     755∀i,a,b.lookup tag A m i = Some ? a → In B (f i) b → In B added b.
     756#tag #A #B * #m #f #DEC * #i #a #b whd in ⊢ (??%? → ?); normalize nodelta
     757#H #H1
     758cases(decidable_In ? (foldi A (list B) tag
     759            (λl.λ_.λacc.(f l)@acc)
     760              (an_id_map tag A m) []) b (DEC b)) [//]
     761#H3 @⊥ lapply(In_all ??? H3) -H3 #H3
     762lapply(added_register_pm ?? m ?? H3 i ?)
     763[cases(domain_of_pm_present ? m i) #H4 #_ @H4 >H % #EQ destruct]
     764lapply H1 elim (f ?) [*] #hd #tl #IH * [#EQ * >EQ * #H4 #_ @H4 %]
     765#H4 * #_ @IH assumption
     766qed.
     767
     768lemma in_added_registers : ∀p : graph_params.
     769∀globals : list ident.∀fn,f_regs,r.
     770∀lbl.code_has_label p globals (joint_if_code … fn) lbl →
     771 In ? (f_regs lbl) r →
     772In ? (added_registers p globals fn f_regs) r.
     773#p #globals #fn #f_regs #r #lbl whd in match code_has_label;
     774whd in match code_has_point; normalize nodelta whd in match (stmt_at ????);
     775inversion(lookup LabelTag ???) [ #_ *] #stmt #EQstmt #_
     776#H @(added_register_aux …  EQstmt H)
     777* #p * #p' cases(decidable_eq_pos p p') [ #EQ destruct % % | * #H1 %2 % #EQ destruct @H1 %]
     778qed.
     779
    701780
    702781include alias "basics/lists/listb.ma".
    703782
    704 check eval_seq_no_pc
    705 
    706 xxxxxxxxxxxxxxxxxxxxxxxx
     783(*
     784definition get_internal_function_from_ident :
     785∀ p: sem_params. ∀ globals : list ident . ∀ge : genv_t (joint_function p globals).
     786ident → option (joint_closed_internal_function p globals) ≝
     787λp,globals,ge,id.
     788! bl  ← (find_symbol (joint_function p globals) ge id);
     789! bl' ← (code_block_of_block bl);
     790! 〈f,fn〉 ← res_to_opt … (fetch_internal_function ? ge bl');
     791return fn.
     792
     793lemma get_internal_function_from_ident_ok :
     794∀p : sem_params. ∀globals : list ident. ∀ge : genv_t (joint_function p globals).
     795∀bl,f,fn. fetch_internal_function ? ge bl = return 〈f,fn〉 →
     796get_internal_function_from_ident p globals ge f= return fn.
     797#p #globals #ge #bl #f #fn #EQf
     798@('bind_inversion EQf) * #f1 * #fn1 whd in match fetch_function;
     799normalize nodelta #H lapply(opt_eq_from_res ???? H) -H #H @('bind_inversion H) -H
     800#f2 #EQf2 #H @('bind_inversion H) -H #fn2 #EQfn2 whd in ⊢ (??%% → ??%% → ?);
     801#EQ1 #EQ2 destruct whd in match get_internal_function_from_ident; normalize nodelta
     802>(symbol_of_block_rev … EQf2) >m_return_bind
     803cut(code_block_of_block bl = return bl)
     804 [ whd in match code_block_of_block; normalize nodelta @match_reg_elim
     805   [ >(pi2 ?? bl) #ABS destruct] elim bl #bl1 #EQ #prf % ] #EQbl >EQbl
     806>m_return_bind >EQf %
     807qed.
     808*)
    707809
    708810lemma eval_seq_no_pc_no_call_ok :
     
    712814∀stack_size.
    713815∀bl.∀id.
    714 ∀seq.
    715 (∀fn : joint_closed_internal_function ERTL (prog_var_names … prog).
    716 ∀l. code_has_label … (joint_if_code … fn) l → 
    717 opt_All …
    718        (λlabs.(All … (λreg.bool_to_Prop(¬(reg ∈ labs)))
    719               (get_used_registers_from_seq … (functs … ERTL) seq)))
    720        (f_regs bl l))  →
     816∀fn : joint_closed_internal_function ERTL (prog_var_names … prog).∀seq.
     817(∀l. code_has_label … (joint_if_code … fn) l → 
     818(All … (λreg.bool_to_Prop(¬(reg ∈ (f_regs bl l))))
     819       (get_used_registers_from_seq … (functs … ERTL) seq)))  →
    721820   preserving1 ?? res_preserve1 ????
    722821      (sigma_state prog f_lbls f_regs (added_registers … fn (f_regs bl)))
     
    729828             (ev_genv (mk_prog_params ERTLptr_semantics trans_prog stack_size))
    730829             id (seq_embed … seq)).
    731 #prog #f_lbls #f_regs #stack_size #bl #f #seq #fresh_regs
     830#prog #f_lbls #f_regs #stack_size #bl #f #fn #seq #fresh_regs
    732831cases seq in fresh_regs;
    733832[ #c #_ #st @mfr_return1
     
    738837       * [#r1 | #R1] #m_src [2: #_ @I] normalize nodelta #fresh_regs
    739838       @not_in_added_registers #lbl #Hlbl lapply(fresh_regs lbl Hlbl)
    740        cases(f_regs bl lbl) [ #_ @I] #labs whd in ⊢ (% → %); * #H #_ @Prop_notb @H
     839       whd in ⊢ (% → %); * #H #_ @Prop_notb @H
    741840  | | #regs  @mfr_return_eq1 %
    742841  ]
     
    744843  [2:  @pop_ok |
    745844  | * #bv #st whd in match acca_store; normalize nodelta @mfr_bind1
    746     [2: @ps_reg_store_ok @not_in_added_registers #lbl #Hlbl
    747        lapply(fresh_regs lbl Hlbl)
    748        cases(f_regs bl lbl) [ #_ @I] #labs whd in ⊢ (% → %); * #H #_ @Prop_notb @H |
    749     | #regs  @mfr_return_eq1 %
     845    [2: @ps_reg_store_ok       
     846        @not_in_added_registers #lbl #Hlbl lapply(fresh_regs lbl Hlbl)
     847       whd in ⊢ (% → %); * #H #_ @Prop_notb @H
    750848    ]
    751849  ]
     
    769867       change with (sigma_beval prog f_lbls (BVptr …))
    770868                                               in ⊢ (???????(?????%?)?);
    771        @ps_reg_store_ok @not_in_added_registers #lbl #Hlbl lapply(fresh_regs lbl Hlbl)
    772        cases(f_regs bl lbl) [ #_ @I] #labs whd in ⊢ (% → %); * #H #_ @Prop_notb @H |
     869       @ps_reg_store_ok
     870              @not_in_added_registers #lbl #Hlbl lapply(fresh_regs lbl Hlbl)
     871       whd in ⊢ (% → %); * #H #_ @Prop_notb @H |
    773872    | #regs  @mfr_return_eq1 %
    774873    ]
     
    781880                                               in ⊢ (???????(?????%?)?);
    782881      @ps_reg_store_ok @not_in_added_registers #lbl #Hlbl lapply(fresh_regs lbl Hlbl)
    783        cases(f_regs bl lbl) [ #_ @I] #labs whd in ⊢ (% → %); * #_ whd in ⊢ (% → ?); * #H
    784        #_ @Prop_notb @H|
     882       whd in ⊢ (% → %); * #_ * #H #_ @Prop_notb @H |
    785883    | #regs  @mfr_return_eq1 %
    786884    ]
     
    798896       | whd in match acca_store; normalize nodelta @mfr_bind1
    799897         [2: @ps_reg_store_ok @not_in_added_registers #lbl #Hlbl
    800              lapply(fresh_regs lbl Hlbl)
    801              cases(f_regs bl lbl) [ #_ @I] #labs whd in ⊢ (% → %); * #H #_ @Prop_notb @H |
     898             lapply(fresh_regs lbl Hlbl) whd in ⊢ (% → %); * #H #_ @Prop_notb @H |
    802899         | #regs  @mfr_return_eq1 %
    803900         ]
     
    805902         [2: whd in match sigma_state; normalize nodelta
    806903            @ps_reg_store_ok @not_in_added_registers #lbl #Hlbl
    807             lapply(fresh_regs lbl Hlbl)
    808             cases(f_regs bl lbl) [ #_ @I] #labs whd in ⊢ (% → %); * #_ * #H #_
    809             @Prop_notb @H |
     904            lapply(fresh_regs lbl Hlbl) whd in ⊢ (% → %); * #_ * #H #_ @Prop_notb @H |
    810905         | #regs  @mfr_return_eq1 %
    811906         ]         
     
    823918      [2: whd in match sigma_state; normalize nodelta @ps_reg_store_ok
    824919          @not_in_added_registers #lbl #Hlbl lapply(fresh_regs lbl Hlbl)
    825        cases(f_regs bl lbl) [ #_ @I] #labs whd in ⊢ (% → %); * #H #_ @Prop_notb @H |
     920       whd in ⊢ (% → %); * #H #_ @Prop_notb @H |
    826921      | #regs  @mfr_return_eq1 %
    827922      ]
     
    837932        [ @(sigma_state prog f_lbls f_regs (added_registers … fn (f_regs bl)))
    838933        | whd in match acca_store; normalize nodelta @mfr_bind1
    839           [2: whd in match sigma_state; normalize nodelta @ps_reg_store_ok 
     934          [2: whd in match sigma_state; normalize nodelta @ps_reg_store_ok
    840935              @not_in_added_registers #lbl #Hlbl lapply(fresh_regs lbl Hlbl)
    841               cases(f_regs bl lbl) [ #_ @I] #labs whd in ⊢ (% → %); * #H #_ @Prop_notb @H |
     936              whd in ⊢ (% → %); * #H #_ @Prop_notb @H |
    842937          | #regs  @mfr_return_eq1 %
    843938          ]
     
    860955        | #bv2 whd in match acca_store; normalize nodelta @mfr_bind1
    861956          [2: whd in match sigma_state; normalize nodelta @ps_reg_store_ok
    862               @not_in_added_registers #lbl #Hlbl lapply(fresh_regs lbl Hlbl)
    863               cases(f_regs bl lbl) [ #_ @I] #labs whd in ⊢ (% → %); * #H #_ @Prop_notb @H |
     957          @not_in_added_registers #lbl #Hlbl lapply(fresh_regs lbl Hlbl)
     958          whd in ⊢ (% → %); * #H #_ @Prop_notb @H |
    864959          | #regs  @mfr_return_eq1 %
    865960          ]
     
    898993          change with (sigma_beval prog f_lbls (BVByte ?))
    899994               in ⊢ (???????(??%?)?);
    900           @ps_reg_store_ok @not_in_added_registers #lbl #Hlbl lapply(fresh_regs lbl Hlbl)
    901           cases(f_regs bl lbl) [ #_ @I] #labs whd in ⊢ (% → %); * #H #_ @Prop_notb @H
    902       |
     995          @ps_reg_store_ok  @not_in_added_registers #lbl #Hlbl
     996          lapply(fresh_regs lbl Hlbl) whd in ⊢ (% → %); * #H #_ @Prop_notb @H |
    903997      | #regs @mfr_return_eq1 %
    904998      ]
    905     ]
     999    ] 
    9061000  ]     
    9071001]
     1002#regs @mfr_return_eq1 %
    9081003qed.
    9091004
     
    9211016#H @('bind_inversion H) -H * #lbl2' #stmt2 #H2
    9221017whd in ⊢ (??%? → ?); #EQ destruct lapply(find_predicate ?????? H1)
    923 lapply(find_predicate ?????? H2) cases(good ??) normalize nodelta [*]
    924 *
     1018lapply(find_predicate ?????? H2) cases(good ??) normalize nodelta
    9251019  [ normalize nodelta @eq_identifier_elim #EQ1 *
    9261020    @eq_identifier_elim #EQ2 * >EQ1 >EQ2 %
     
    11891283qed.
    11901284
    1191 lemma append_All : ∀A : Type[0]. ∀ P : A → Prop. ∀l1,l2 : list A.
    1192 All ? P (l1 @ l2) → All ? P l1 ∧ All ? P l2.
    1193 #A #P #l1 elim l1
    1194 [ #l2 change with l2 in ⊢ (???% → ?); #H % //]
    1195 #a #tl #IH #l2 change with (P a ∧ All A P (tl @ l2)) in ⊢ (% → ?);
    1196 * #H1 #H2 lapply(IH … H2) * #H3 #H4 % // whd % //
    1197 qed.
    1198 
    11991285include alias "common/Identifiers.ma".
    12001286
     
    12041290 ∀f_bl_r.
    12051291 b_graph_transform_program_props ERTL_semantics ERTLptr_semantics
    1206      translate_data prog f_bl_r f_lbls f_regs →
     1292     (λglobals,fn.«translate_data globals fn,(refl …)») prog f_bl_r f_lbls f_regs →
    12071293∀id,fn,bl,pt,stmt.
    12081294fetch_internal_function … (globalenv_noinit … prog) bl = return 〈id,fn〉 →
    12091295stmt_at ERTL (prog_var_names … prog) (joint_if_code … fn) pt = return stmt → 
    1210 f_lbls bl pt = return [ ] → get_sigma prog f_lbls bl pt = return pt.
     1296f_lbls bl pt = [ ] → get_sigma prog f_lbls bl pt = return pt.
    12111297#prog #f_lbls #f_regs #f_bl_r #good #id #fn #bl #pt #stmt #EQfn #EQstmt #EQlabels
    12121298cases(b_graph_transform_program_fetch_internal_function … good … EQfn)
    12131299#init_data * #calling' ** #EQcalling' whd in ⊢ (% → ?); cases(f_bl_r ?)
    12141300[2,4: #x #y *] normalize nodelta #EQ destruct(EQ) * #_ #_ #_ #_ #_
    1215 #_ #fresh_labs #_ #_ #_ #H lapply(H … EQstmt) -H * #lbls * #regs ** >EQlabels
    1216 whd in ⊢ (??%? → ?); #EQ destruct(EQ) #EQregs cases stmt in EQstmt; normalize nodelta
    1217 [3: * |2: * [#lbl || *] #EQstmt * #bl * whd in ⊢ (% → ?); cases regs in EQregs;
    1218     [2,4: #x #y #_ *] #EQregs normalize nodelta #EQ destruct(EQ) whd in ⊢ (%→?);
    1219     * #pref * #mid ** #EQmid whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2)
    1220     whd in ⊢ (% → ?); #EQt_stmt
     1301#_ #fresh_labs #_ #_ #_ #H lapply(H … EQstmt) -H cases stmt in EQstmt;
     1302[3: *
     1303|2: * [#lbl || *] #EQstmt normalize nodelta * #bl * whd in ⊢ (% → ?);
     1304   inversion (f_regs ??) [2,4: #x #y #_ #_ *] #EQregs normalize nodelta
     1305   #EQ destruct(EQ) whd in ⊢ (%→?); * #pref * #mid ** #EQmid whd in ⊢ (% → ?);
     1306   * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in ⊢ (% → ?); #EQt_stmt
    12211307| * [#c | * [#c_id|#c_ptr] #args #dest | #r #lbl | #seq ] #nxt #EQstmt
    12221308  whd in ⊢ (% → ?); * #bl >if_merge_right [2,4,6,8,10: %] * whd in ⊢ (% → ?);
    1223   cases regs in  EQregs; normalize nodelta
    1224   [2,4,5,8,10: [1,2,4,5: #x #y] #_ *|6: #r * [2: #x #y] ]
    1225   #EQregs [1,2: whd in ⊢ (% → ?); [*]] #EQ destruct(EQ) whd in ⊢ (% → ?);
     1309  inversion(f_regs ??) normalize nodelta
     1310  [2,4,5,8,10: [1,2,4,5: #x #y] #_ [1,2,3,4: #_] *|6: #r * [2: #x #y] ]
     1311  [1,2: #_] #EQregs [1,2: whd in ⊢ (% → ?); [*]] #EQ destruct(EQ) whd in ⊢ (% → ?);
    12261312  * #l1 * #mid1 * #mid2 * #l2 *** #EQmid1 whd in ⊢ (%→ ?);
    12271313  [ * #mid * #rest ** #EQ destruct(EQ) whd in ⊢ (% → ?); * #nxt1 *
    12281314    #EQlow change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ)
    12291315    whd in ⊢ (% → ?); * #mid3 * #rest1 ** #EQ destruct(EQ)
    1230      whd in EQmid1 : (???%); destruct(EQmid1) whd in e0 : (???%);
    1231      destruct(e0) ] * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in EQmid1 : (???%);
    1232      destruct(EQmid1) whd in ⊢ (% → ?); * #nxt1 * #EQt_stmt #EQ destruct(EQ)
    1233      whd in ⊢ (% → ?); * #_ #EQ destruct(EQ)
    1234 ] whd in match get_sigma; normalize nodelta >code_block_of_block_eq >m_return_bind
     1316     whd in EQmid1 : (???%); destruct(EQmid1) whd in e0 : (???%); >EQlabels in e0;
     1317    #e0 destruct(e0) ] * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in EQmid1 : (???%);
     1318     destruct(EQmid1) whd in ⊢ (% → ?); * #nxt1 * #EQt_stmt
     1319     change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) whd in ⊢ (% → ?);
     1320     * #_ #EQ destruct(EQ) ]
     1321whd in match get_sigma; normalize nodelta >code_block_of_block_eq >m_return_bind
    12351322>EQfn >m_return_bind inversion(find ????)
    12361323[1,3,5,7,9,11: #EQfind @⊥ lapply(find_none ?????? EQfind EQstmt) >EQlabels
    12371324  normalize nodelta @eq_identifier_elim [1,3,5,7,9,11: #_ * |*: * #H #_ @H %]]
    12381325* #lbl #s #EQfind >m_return_bind lapply(find_predicate ?????? EQfind)
    1239 inversion(f_lbls ??) [1,3,5,7,9,11: #_ *] #l @(list_elim_left … l …)
    1240 normalize nodelta [1,3,5,7,9,11: #_ @eq_identifier_elim
    1241                          [1,3,5,7,9,11: #EQ destruct(EQ) #_ % |*: #_ *]]
    1242 #last #pre #_ #EQlbl >split_on_last_append normalize nodelta @eq_identifier_elim
     1326inversion(f_lbls ??)
     1327[1,3,5,7,9,11: #_ normalize nodelta @eq_identifier_elim [2,4,6,8,10,12: #_ *] #EQ #_ >EQ %]
     1328#lb #l @(list_elim_left … l …) normalize nodelta
     1329[1,3,5,7,9,11: #_ #EQlb @eq_identifier_elim
     1330               [1,3,5,7,9,11: #EQ destruct(EQ) #_ @⊥ |*: #_ *]
     1331               lapply(fresh_labs lbl) >EQlb *** #H #_ #_ @H
     1332               @(code_is_in_universe … (pi2 ?? fn)) whd in match code_has_label;
     1333               whd in match code_has_point; normalize nodelta >EQstmt @I ]
     1334#last #pre #_ #_ #EQlbl >(split_on_last_append … (lb::pre) last)
     1335normalize nodelta @eq_identifier_elim
    12431336[2,4,6,8,10,12: #_ *] #EQ lapply EQlbl destruct(EQ) #EQlbl #_ @⊥
    1244 lapply(fresh_labs lbl) >EQlbl whd in ⊢ (% → ?); #H lapply(append_All … H) -H
     1337lapply(fresh_labs lbl) >EQlbl whd in ⊢ (% → ?); * #_ #H lapply(append_All … H) -H
    12451338* #_ whd in ⊢ (% → ?); *** #H #_ #_ @H -H @(code_is_in_universe … (pi2 ?? fn))
    12461339whd in match code_has_label; whd in match code_has_point; normalize nodelta
     
    12611354qed.
    12621355
     1356
    12631357lemma get_sigma_last :
    12641358∀prog : ertl_program.
     
    12661360 ∀f_bl_r.
    12671361 b_graph_transform_program_props ERTL_semantics ERTLptr_semantics
    1268      translate_data prog f_bl_r f_lbls f_regs →
     1362     (λglobals,fn.«translate_data globals fn,(refl …)») prog f_bl_r f_lbls f_regs →
    12691363∀id,fn,bl,pt,stmt,pre,last.
    12701364fetch_internal_function … (globalenv_noinit … prog) bl = return 〈id,fn〉 →
    12711365stmt_at ERTL (prog_var_names … prog) (joint_if_code … fn) pt = return stmt → 
    1272 f_lbls bl pt = return (pre@[last]) → get_sigma prog f_lbls bl last = return pt.
     1366f_lbls bl pt = pre@[last] → get_sigma prog f_lbls bl last = return pt.
    12731367#prog #f_lbls #f_regs #f_bl_r #good #id #fn #bl #pt #stmt #pre #last
    12741368#EQfn #EQstmt #EQlabels
    12751369cases(b_graph_transform_program_fetch_internal_function … good … EQfn)
    12761370#init_data * #calling' ** #EQcalling' whd in ⊢ (% → ?); cases(f_bl_r ?)
    1277 [2,4: #x #y *] normalize nodelta #EQ destruct(EQ) * #_ #_ #_ #_ #pp_labs
    1278 #_ #fresh_labs #_ #_ #_ #H lapply(H … EQstmt) -H * #lbls * #regs ** >EQlabels
    1279 whd in ⊢ (??%? → ?); #EQ destruct(EQ) #EQregs cases stmt in EQstmt; normalize nodelta
     1371[2: #x #y *] normalize nodelta #EQ destruct(EQ) * #_ #_ #_ #_ #pp_labs
     1372#_ #fresh_labs #_ #_ #_ #H lapply(H … EQstmt) -H normalize nodelta
     1373cases stmt in EQstmt; normalize nodelta
    12801374[3: *
    12811375|2: * [#lbl || *] #EQstmt whd in ⊢ (%→ ?); * #bl *
    12821376|*: * [#c | * [ #c_id | #c_ptr] #args #dest | #r #lbl | #seq ] #nxt #EQstmt
    12831377    >if_merge_right [2,4,6,8,10: %] whd in ⊢ (% → ?); * #bl *
    1284 ] whd in ⊢ (% → ?); cases regs in EQregs; normalize nodelta
    1285 [2,4,6,8,9,12,14: [1,2,3,4,6,7: #x #y] #_ *|10: #r #tl] #EQregs
     1378]
     1379whd in ⊢ (% → ?); inversion(f_regs ??) normalize nodelta
     1380[2,4,6,8,9,12,14: [1,2,3,4,6,7: #x #y #_] #_ *|10: #r #tl #_] #EQregs
    12861381[ whd in ⊢ (% → ?); cases tl in EQregs; normalize nodelta [2: #x #y #_ *] #EQregs]
    12871382#EQbl destruct(EQbl) whd in ⊢ (%→?); [2,3: * #pref * #mid **|*: * #l1 * #mid1 * #mid2 * #l2 ***]
    12881383#EQmid1 whd in ⊢ (% → ?);
    1289 [1,2,4,5,6,7: * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in EQmid1 : (??%%); destruct(EQmid1)
     1384[1,2,4,5,6,7: * #EQ1 #EQ2 destruct(EQ1 EQ2) whd in EQmid1 : (??%%); destruct(EQmid1)              
    12901385[3,4,5,6: whd in ⊢ (% → ?); * #nxt1 * #EQt_stmt  #EQ destruct(EQ) ]
    1291 whd in ⊢ (% → ?); * [1,2,3,4: #e0] @⊥ @(append_absurd ??? e0)]
     1386whd in ⊢ (% → ?); * [1,2,3,4: #e0] @⊥ >EQlabels in e0; #e0 @(append_absurd ??? e0)]
    12921387* #mid * #rest ** #EQ destruct(EQ) whd in ⊢ (% → ?); * #nxt1 * #_
    12931388change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) whd in ⊢ (% → ?);
     
    13041399>code_block_of_block_eq >m_return_bind >EQfn >m_return_bind
    13051400inversion(find ????)
    1306 [ #EQfind @⊥ lapply(find_none ?????? EQfind EQstmt) >EQlabels
     1401[ #EQfind @⊥ lapply(find_none ?????? EQfind EQstmt) >e0
    13071402  normalize nodelta @eq_identifier_elim [ #_ *] * #H #_ @H
    1308   whd in EQmid1 : (??%%); destruct(EQmid1) @(last_append_eq ????? e1) ]
     1403  >(last_append_eq ????? EQlabels) % ]
    13091404* #lbl #s #EQfind >m_return_bind lapply(find_predicate ?????? EQfind)
    1310 inversion(f_lbls ??) [ #_ normalize nodelta *] #labels
    1311 @(list_elim_left … labels …) -labels normalize nodelta
    1312 [ #EQl @eq_identifier_elim [2: #_ *] #EQ lapply EQl destruct(EQ) #EQl
    1313   lapply(fresh_labs pt) >EQlabels <e0 whd in ⊢ (% → ?);
    1314   #H lapply(append_All … H) -H * #_ whd in ⊢ (% → ?); *** #H #_ #_ #_ @⊥ @H
    1315   @(code_is_in_universe … (pi2 ?? fn)) whd in match code_has_label;
     1405inversion(f_lbls ??)
     1406[ #EQlbl normalize nodelta @eq_identifier_elim [2: #_ *] #EQ destruct(EQ)
     1407  lapply(last_append_eq ????? EQlabels) #EQ destruct(EQ) @⊥
     1408  lapply(fresh_labs pt) >e0 * #_ * #_ * #_ *** #H #_ #_ @H -H
     1409   @(code_is_in_universe … (pi2 ?? fn)) whd in match code_has_label;
    13161410  whd in match code_has_point; normalize nodelta whd in match (stmt_at ????);
    13171411  >(find_lookup ?????? EQfind) @I
    1318 | #last1 #pre1 #_ #EQl >split_on_last_append normalize nodelta @eq_identifier_elim
    1319   [2: #_ *] #EQ lapply EQl destruct(EQ) #EQl #_ lapply pp_labs
    1320   whd in match partial_partition; normalize nodelta * #_ #H lapply(H lbl pt)
    1321   >EQl <e0 in EQlabels; #EQlabels >EQlabels whd in ⊢ (% → ?); -H #H
    1322   >(H last1 ? ?) [%] >(memb_append_l2 ? last1 ? [last1] ?) /2 by /
    1323 ]
    1324 qed.
     1412]
     1413#lb #labels #_  @(list_elim_left … (labels) …) -labels normalize nodelta
     1414[2: #last1 #pre #_] #EQl [ >(split_on_last_append … (lb::pre) last1) ]
     1415normalize nodelta @eq_identifier_elim [2,4: #_ *] #EQ destruct(EQ) #_
     1416lapply(last_append_eq ????? EQlabels) #EQ destruct(EQ)
     1417lapply pp_labs whd in match partial_partition; normalize nodelta * #_ #H
     1418lapply(H lbl pt) >e0 whd in EQmid : (??%%); >EQl
     1419#H [ >(H last1 ? ?) | >(H lb ? ?) ] [1,4: %
     1420               |6: whd in match (memb ???); @if_elim [#_ @I]
     1421                  #H lapply(Prop_notb ? H) * -H #H @⊥ @H cases lb #x normalize
     1422                  @if_elim [#_ %] #H lapply(Prop_notb ? H) * -H #H @H >(eqb_n_n x) %
     1423               |5: >(memb_append_l2 ? lb ? [lb] ?) /2 by /
     1424               |*: >(memb_append_l2 ? last1 ? [last1] ?) /2 by /
     1425                   @Exists_memb %2 elim pre [ % % | #hd #tl #IH %2 @IH]
     1426               ]
     1427qed.
     1428
    13251429
    13261430lemma fetch_call_commute :
     
    13301434 ∀f_bl_r.
    13311435 b_graph_transform_program_props ERTL_semantics ERTLptr_semantics
    1332      translate_data prog f_bl_r f_lbls f_regs →
     1436     (λglobals,fn.«translate_data globals fn,(refl …)») prog f_bl_r f_lbls f_regs →
    13331437∀id,fn,c_id,c_args,c_dest,nxt,pc.
    13341438fetch_statement ERTL_semantics
     
    13431447cases(b_graph_transform_program_fetch_internal_function … good … EQfn)
    13441448#init_data * #calling' ** #EQcalling' whd in ⊢ (% → ?); cases(f_bl_r ?)
    1345 [2,4: #x #y *] normalize nodelta #EQ destruct(EQ) * #_ #_ #_ #_ #pp_labs
    1346 #_ #fresh_labs #_ #_ #_ #H cases(H … EQstmt) -H #labels * #registers
    1347 ** #EQlabels #EQregisters normalize nodelta >if_merge_right [2,4: %]
    1348 whd in match translate_step;
    1349 normalize nodelta whd in ⊢ (% → ?); * #bl * whd in ⊢ (% → ?);
    1350 cases registers in EQregisters; -registers normalize nodelta
    1351 [2,3: [ #x #y] #_ *|4: #r #tl] #EQregisters
    1352 [ whd in ⊢ (% → ?); cases tl in EQregisters; -tl [2: #x #y #_ *] normalize nodelta
    1353 #EQregisters] #EQ destruct(EQ) whd in ⊢ (% → ?); *
    1354 #pre_l * #mid1 * #mid2 * #post_l *** #EQmid1 whd in ⊢ (% → ?);
    1355 [ * #mid * #resg ** #EQ destruct(EQ) whd in ⊢ (% → ?);
     1449[2,4: #x #y *] normalize nodelta #EQ destruct(EQ) * #_ #_ #_ #_ #_
     1450#_ #_ #_ #_ #_ #H cases(H … EQstmt) -H #bl whd in ⊢ (% → ?); *
     1451>if_merge_right [2,4: %] whd in match translate_step;
     1452normalize nodelta whd in ⊢ (% → ?); inversion(f_regs ??) normalize nodelta
     1453[|2,3:[ #x #y #_] #_ * |4: #r #tl #_ ] #EQregs
     1454[ | cases tl in EQregs; [2: #x #y #_ *] #EQregs whd in ⊢ (% → ?);] #EQ destruct(EQ)
     1455whd in ⊢ (% → ?); * #pre_l * #mid1 * #mid2 * #post_l *** #EQmid1 whd in ⊢ (% → ?);
     1456[2: * #mid * #resg ** #EQ destruct(EQ) whd in ⊢ (% → ?);
    13561457  * #nxt1 * #EQlow change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ)
    13571458  whd in ⊢ (% → ?); * #mid3 * #rest1 ** #EQ destruct(EQ) * #nxt1 *
     
    13721473      [1,3: #EQbl >fetch_internal_function_no_minus_one in EQfn; try assumption
    13731474            #EQ destruct(EQ)] #_ normalize nodelta
    1374             [2: >(get_sigma_idempotent … good … EQfn EQstmt EQlabels)
     1475            [2: >(get_sigma_idempotent … good … EQfn EQstmt EQ)
    13751476            |*: change with (pc_block pc) in match (pc_block ?);
    1376                 >point_of_pc_of_point >(get_sigma_last … good … EQfn EQstmt EQlabels)
     1477                >point_of_pc_of_point >(get_sigma_last … good … EQfn EQstmt e0)
    13771478            ] >m_return_bind normalize nodelta >pc_of_point_of_pc %
    13781479|*: whd in match fetch_statement; normalize nodelta >EQcalling' >m_return_bind
     
    13871488∀ f_lbls,f_regs.∀f_bl_r.
    13881489b_graph_transform_program_props ERTL_semantics ERTLptr_semantics
    1389      translate_data prog f_bl_r f_lbls f_regs →
     1490     (λglobals,fn.«translate_data globals fn,(refl …)») prog f_bl_r f_lbls f_regs →
    13901491∀pc,lb.
    13911492next_of_call_pc ERTL_semantics (prog_var_names … prog) (globalenv_noinit … prog)
     
    16031704]
    16041705qed.
     1706
     1707
  • src/common/ExtraIdentifiers.ma

    r2801 r2843  
    241241qed.
    242242
    243 
     243lemma map_opt_none : ∀A,B.∀m : positive_map A.
     244      map_opt A B (λx.None ?) m = pm_leaf B.
     245#A #B #m elim m [%] #opt_a #l #r #EQ1 #EQ2 cases opt_a [2: #a] normalize
     246>EQ1 >EQ2 %
     247qed.
     248
     249lemma set_minus_add :∀tag,A,B.∀a:identifier_map tag A.∀b:identifier_map tag B.
     250           ∀i,v.i∈b→ (add tag A a i v)∖b = a ∖ b.
     251#tag #A #B * #a * #b * #i #v normalize inversion(lookup_opt B i b) [ #_ *]
     252#v1 #EQv1 #_ @eq_f lapply EQv1 -EQv1 lapply v1 -v1 lapply v -v lapply b -b
     253lapply i -i elim a
     254[ #i elim i [ * [2: #opt_v #l #r] #v1 #v2 normalize #EQb destruct(EQb) %]
     255#i1 #IH * [2,4: #opt_v #l #r] #v1 #v2 normalize [3,4: #ABS destruct(ABS)]
     256cases opt_v [2,4: #v'] normalize nodelta #EQb >(IH … EQb) >map_opt_none %
     257| #opt_v #l #r #IHl #IHr #i * [#v1 #v2 normalize #EQ destruct] #opt_v1 #l1 #r1
     258  #c1 #c2 normalize cases i [2,3: #x] normalize [3: #EQ destruct] normalize nodelta
     259[ %] #EQc2 cases opt_v [2,4: #c3] normalize cases opt_v1 [2,4,6,8: #c4] normalize
     260[1,3,4,5,7: >(IHr … EQc2) inversion(merge A B A ? l l1) //
     261            [2: #opt_v4 #l4 #r4 #_ #_] #EQ <EQ >(IHl … EQc2) //
     262|*: >(IHl … EQc2) //
     263]
     264qed.           
     265
  • src/joint/Joint.ma

    r2824 r2843  
    190190match step with
    191191[ COST_LABEL c ⇒ [ ]
    192 | CALL id args dest ⇒ (f_call_args … functs args) @ (f_call_dest … functs dest)
     192| CALL id args dest ⇒
     193     let r_id ≝  match id with
     194                   [ inl _ ⇒ [ ]
     195                   | inr ptr ⇒ ((dpl_args … functs) (\fst ptr)) @
     196                                                 ((dph_args … functs) (\snd ptr))
     197                   ] in
     198    r_id @ (f_call_args … functs args) @ (f_call_dest … functs dest)
    193199| COND r lbl ⇒  acc_a_regs … functs r
    194200| step_seq s ⇒ get_used_registers_from_seq … functs s
  • src/joint/TranslateUtils.ma

    r2823 r2843  
    606606definition added_registers :
    607607  ∀p : graph_params.∀g.
    608   joint_internal_function p g → (label → option (list register)) → list register ≝
     608  joint_internal_function p g → (label → list register) → list register ≝
    609609  λp,g,def,f_regs.
    610   let f ≝ λlbl : label.λ_.λacc.
    611     match f_regs lbl with [ None ⇒ acc | Some regs ⇒ regs@acc ] in
     610  let f ≝ λlbl : label.λ_.λacc.(f_regs lbl)@acc in
    612611  foldi … f (joint_if_code p g def) [ ].
    613612
     
    615614  ∀p,g,def,f_regs.
    616615  ∀l,s.stmt_at … (joint_if_code … def) l = Some ? s →
    617   opt_All … (All … (λlbl.bool_to_Prop (lbl ∈ added_registers p g def f_regs))) (f_regs l).
     616  (All … (λlbl.bool_to_Prop (lbl ∈ added_registers p g def f_regs)) (f_regs l)).
    618617
    619618(*(* translation without register allocation (more or less an alias) *)
  • src/joint/semanticsUtils.ma

    r2816 r2843  
    633633| % [2: % [2: % [% %]] | skip] @(multi_fetch_ok … H3 … EQstmt_at) ]
    634634qed.
     635
     636lemma b_graph_transform_program_fetch_statement_plus :
     637 ∀src,dst:sem_graph_params.
     638 ∀data : ∀globals.joint_closed_internal_function src globals →
     639  bound_b_graph_translate_data src dst globals.
     640 ∀prog_in : joint_program src.
     641 ∀init_regs : block → list register.
     642 ∀f_lbls : block → label → list label.
     643 ∀f_regs : block → label → list register.
     644 b_graph_transform_program_props … data prog_in init_regs f_lbls f_regs →
     645 let prog_out ≝ b_graph_transform_program … data prog_in in
     646 let src_genv ≝ globalenv_noinit ? prog_in in
     647 let dst_genv ≝ globalenv_noinit ? prog_out in
     648 ∀pc,id,def_in,s.
     649 fetch_statement … src_genv pc = return 〈id, def_in, s〉 →
     650 ∃init_data,def_out.
     651 let bl ≝ pc_block pc in
     652 fetch_internal_function … dst_genv bl = return 〈id, def_out〉 ∧
     653 bind_new_instantiates … init_data (data … def_in) (init_regs bl) ∧
     654 let l ≝ point_of_pc dst pc in
     655 ∃lbls,regs.
     656 f_lbls bl l = lbls ∧
     657 f_regs bl l = regs ∧
     658 joint_if_entry … def_out = joint_if_entry … def_in ∧
     659 partial_partition … (f_lbls bl) ∧
     660 partial_partition … (f_regs bl) ∧
     661 (∀l.All …
     662    (λlbl.¬fresh_for_univ … lbl (joint_if_luniverse … def_in) ∧
     663           fresh_for_univ … lbl (joint_if_luniverse … def_out)) (f_lbls bl l)) ∧
     664  (∀l.All …
     665    (λreg.¬fresh_for_univ … reg (joint_if_runiverse … def_in) ∧
     666           fresh_for_univ … reg (joint_if_runiverse … def_out)) (f_regs bl l)) ∧
     667  match s with
     668  [ sequential s' nxt ⇒
     669    let block ≝
     670      if eq_identifier … (joint_if_entry … def_in) l then
     671        append_seq_list … (f_step … init_data l s') (added_prologue … init_data)
     672      else
     673        f_step … init_data l s' in
     674    l ~❨block, l::lbls, regs❩~> nxt in joint_if_code … def_out
     675  | final s' ⇒
     676    l ~❨f_fin … init_data l s', l::lbls, regs❩~> it in joint_if_code … def_out
     677  | FCOND abs _ _ _ ⇒ Ⓧabs
     678  ].
     679#src #dst #data #prog_in
     680#init_regs #f_lbls #f_regs #props
     681#pc #id #def_in #s
     682#H @('bind_inversion H) * #id' #def_in' -H
     683#EQfif
     684#H @('bind_inversion H) -H #s
     685#H lapply (opt_eq_from_res ???? H) -H
     686#EQstmt_at whd in ⊢ (??%%→?); #EQ destruct
     687cases (b_graph_transform_program_fetch_internal_function … props … EQfif)
     688#a * #b ** #H1 #H2 #H3 %{a} %{b} %
     689[ %{H1 H2}
     690| %
     691   [2:
     692      %
     693        [2: %
     694            [%
     695               [%
     696                  [%
     697                     [%
     698                        [%
     699                           [%
     700                              %
     701                            | @(entry_eq … H3)
     702                            ]
     703                        | @(partition_lbls … H3)
     704                        ]
     705                     |  @(partition_regs … H3)
     706                     ]
     707                  | @(freshness_lbls … H3)
     708                  ]
     709               |  @(freshness_regs … H3)
     710               ]
     711            |  @(multi_fetch_ok … H3 … EQstmt_at)
     712            ]
     713        |
     714        ]
     715   |
     716   ]
     717]         
     718qed.
Note: See TracChangeset for help on using the changeset viewer.