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

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

File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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
Note: See TracChangeset for help on using the changeset viewer.