Changeset 2891


Ignore:
Timestamp:
Mar 16, 2013, 10:42:43 AM (4 years ago)
Author:
piccolo
Message:

added precondition on seq statement and tested correct in the ERTl-ERTLptr passed

Location:
src
Files:
3 edited

Legend:

Unmodified
Added
Removed
  • src/ERTL/ERTLtoERTLptrOK.ma

    r2883 r2891  
    160160
    161161include "joint/StatusSimulationHelper.ma".
     162include alias "basics/lists/listb.ma".
    162163
    163164lemma make_ERTL_To_ERTLptr_good_state_relation :
     
    209210  change with (pc_block (pc … st2)) in match (pc_block ?);
    210211  <(fetch_stmt_ok_sigma_pc_ok … EQfetch) >EQfn %
     212| #st1 #st1' #st2 #f #fn #stmt #nxt #EQfetch whd in match eval_state;
     213  whd in match eval_statement_no_pc; normalize nodelta >EQfetch >m_return_bind
     214  normalize nodelta #H @('bind_inversion H) -H #st1_no_pc' #EQst1_no_pc'
     215  whd in ⊢ (??%% → ?); #EQ destruct(EQ) whd in ⊢ (%→?); #EQ destruct(EQ)
     216  whd in match sigma_state_pc in EQst1_no_pc'; normalize  nodelta in EQst1_no_pc';
     217  cases(fetch_statement_inv … EQfetch) >(fetch_stmt_ok_sigma_pc_ok … EQfetch)
     218  #EQfn #EQstmt >EQfn in EQst1_no_pc'; normalize nodelta #EQst1_no_pc'
     219  #t_fn #EQt_fn whd % [2: %{(refl …)} |] lapply(err_eq_from_io ????? EQst1_no_pc')
     220  -EQst1_no_pc' #EQst1_no_pc'
     221  cases(eval_seq_no_pc_no_call_ok prog f_lbls f_regs ???????? EQst1_no_pc')
     222  [ #st2_no_pc' * #EQst2_no_pc' #EQ destruct(EQ)
     223  %{(mk_state_pc ? st2_no_pc'
     224     (pc_of_point ERTLptr_semantics (pc_block (pc … st2)) nxt)
     225     (last_pop … st2))} %
     226     [ whd in ⊢ (??%?); >EQst2_no_pc' %
     227     | whd whd in match sigma_state_pc; normalize nodelta >EQfn %
     228     ]
     229  |  #lbl whd in match code_has_label; whd in match code_has_point; normalize nodelta
     230  inversion(stmt_at ????) [#_ *] #stmt1 #EQstmt1 #_
     231  cut(fetch_statement ERTL_semantics (prog_var_names … prog) (globalenv_noinit … prog)
     232                      (pc_of_point ERTL_semantics (pc_block (pc … st2)) lbl) =
     233                 return 〈f,fn,stmt1〉)
     234   [ whd in ⊢ (??%?); >EQfn normalize nodelta >point_of_pc_of_point >EQstmt1 %] #EQf_stmt1
     235  cases(b_graph_transform_program_fetch_statement_plus … good … EQf_stmt1)
     236  #init * #t_fn' ** #EQt_fn' whd in ⊢ (% → ?); cases(init_regs ?) [2: #x #y *]
     237  normalize nodelta #EQ destruct(EQ) * #labels * #registers
     238  ******* #EQlabels >point_of_pc_of_point change with (pc_block (pc … st2)) in match (pc_block ?);
     239  #EQregisters #_ #_ #_ #_ #fresh_regs #_ >EQregisters
     240  cases(excluded_middle_list ? (λreg.bool_to_Prop(¬(reg∈registers)))
     241         (get_used_registers_from_seq … (functs ERTL) stmt) ?)
     242  [3: #a #_ cases(¬a∈registers) // |1: #H assumption] #H @⊥
     243  cases(Exists_All … H (regs_are_in_univers … (pi2 ?? fn) … EQstmt))
     244   #reg ** #H1 #H2 @H1 -H1 @notb_Prop % #H1 lapply(fresh_regs … lbl) >EQregisters
     245  #H3 lapply(All_memb … H3 H1) ** #H4 #_ @H4 assumption
     246  ]
    211247]
    212248qed.
  • src/ERTL/ERTLtoERTLptrUtils.ma

    r2845 r2891  
    413413     (be_op2 b op).
    414414#prog #sigma #b #op #bv #bv1 whd in match be_op2; normalize nodelta
    415 cases bv
     415cases daemon
     416qed. (*TODO*)
     417(*cases bv
    416418[ | | #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc1 #p1]
    417 normalize nodelta [@res_preserve_error1] whd in match sigma_beval;
     419normalize nodelta [cases op normalize nodelta @res_preserve_error1] whd in match sigma_beval;
    418420normalize nodelta
    419421cases bv1
     
    499501      ]
    500502]
    501 qed.
     503qed.*)
    502504
    503505lemma pointer_of_address_ok : ∀prog : ertl_program.∀f_lbls : lbl_funct.
     
    10491051        sigma_stored_pc prog f_lbls pc〉)
    10501052     (pop_ra ERTL_semantics)
    1051      (pop_ra ERTLptr_semantics).   
     1053     (pop_ra ERTLptr_semantics).
     1054cases daemon (*TODO*) qed.
     1055(*       
    10521056#prog #f_lbls #f_regs #restr1 #st whd in match pop_ra; normalize nodelta
    10531057@mfr_bind1
     
    10881092| #pc @mfr_return_eq1 %
    10891093]
    1090 qed.
     1094qed.*)
    10911095
    10921096lemma pc_block_eq : ∀prog : ertl_program. ∀f_lbls,pc.
  • src/joint/StatusSimulationHelper.ma

    r2886 r2891  
    4545]
    4646qed.
    47 
    48 
    49 definition step_to_seq : ∀p : prog_params.∀stmt : joint_step p (globals p).
    50 joint_classify_step p stmt = cl_other →
    51 (∀c.stmt ≠ COST_LABEL ?? c) → Σ seq.stmt = step_seq ?? seq ≝
    52 λp,stmt,CL_OTHER,COST.
    53 (match stmt return λx.x = stmt → ? with
    54 [ COST_LABEL c ⇒ λprf.⊥
    55 | CALL id args dest ⇒ λprf.⊥
    56 | COND r lab ⇒ λprf.⊥
    57 | step_seq seq ⇒ λprf.«seq,?»
    58 ])(refl …).
    59 @hide_prf
    60 [ lapply(COST c) * #H @H >prf %
    61 |2,3: <prf in CL_OTHER; whd in match (joint_classify_step ??); #EQ destruct(EQ)
    62 | >prf %
    63 ]
    64 qed.
    65 
    66 check ensure_step_block
    6747
    6848record good_state_relation (P_in : sem_graph_params)
     
    141121       ∃l : list (joint_seq (mk_prog_params P_out trans_prog stack_sizes)
    142122                            (globals (mk_prog_params P_out trans_prog stack_sizes))).
    143                             blp = (ensure_step_block ?? l) ∧ True
    144        (*
    145        TUTTO IL RESTO PARLA DI R
    146        
    147            ∀mid,mid1.
    148             stmt_at ? (prog_var_names … trans_prog) (joint_if_code ?? t_fn) mid
    149             = return sequential P_out ? ((\snd (\fst blp)) mid) mid1→
    150             ∃CL_OTHER : joint_classify_step (mk_prog_params P_out trans_prog stack_sizes)
    151                           ((\snd (\fst blp)) mid)  = cl_other.
    152             ∃COST : cost_label_of_stmt (mk_prog_params P_out trans_prog stack_sizes)
    153                          (sequential P_out ? ((\snd (\fst blp)) mid) mid1) = None ?.
    154             ∃st2_fin_no_pc.
    155             let pre ≝ (map_eval ?? (\fst (\fst blp)) mid) in
    156             let middle ≝ [pi1 ?? (step_to_seq (mk_prog_params P_out trans_prog stack_sizes)
    157                                   ((\snd (\fst blp)) mid) CL_OTHER ?)] in
     123                            blp = (ensure_step_block ?? l) ∧
     124       ∃st2_fin_no_pc.
    158125           repeat_eval_seq_no_pc (mk_prog_params P_out trans_prog stack_sizes) f
    159               (pre@ middle @ (\snd blp))  (st_no_pc … st2)= return st2_fin_no_pc ∧
     126              l  (st_no_pc … st2)= return st2_fin_no_pc ∧
    160127           let st2_fin ≝
    161128           mk_state_pc ? st2_fin_no_pc
    162129                         (pc_of_point P_out (pc_block(pc … st2)) nxt)
    163130                         (last_pop … st2) in
    164            R st1' st2_fin *) ) (f_step ??? data (point_of_pc P_in (pc … st1)) seq)
     131           R st1' st2_fin) (f_step ??? data (point_of_pc P_in (pc … st1)) seq)
    165132      ) (init ? fn)         
    166133}.
    167 (*@hide_prf #c % #EQ >EQ in COST; whd in ⊢ (??%% → ?); #EQ destruct(EQ)
    168 qed.*)
    169134
    170135lemma general_eval_cond_ok : ∀ P_in , P_out: sem_graph_params.
     
    270235 if taaf_non_empty … taf then True else  (*IT CAN BE SIMPLIFIED *)
    271236(¬as_costed (joint_abstract_status (mk_prog_params P_in prog stack_sizes)) st1 ∨
    272  ¬as_costed (joint_abstract_status (mk_prog_params P_in prog stack_sizes)) st1').
    273 cases daemon qed.
    274  
    275 (*
     237 ¬as_costed (joint_abstract_status (mk_prog_params P_in prog stack_sizes)) st1').
    276238#P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_bl_r #init #good #R #goodR #st1 #st1'
    277239#st2 #f #fn #stmt #nxt #Rst1st2 #EQfetch #EQeval
    278240cases(b_graph_transform_program_fetch_statement … good … EQfetch)
    279241#init_data * #t_fn ** >(pc_eq_sigma_commute … goodR … Rst1st2 EQfetch)
    280 #EQt_fn #Hinit * #labs * #regs ** #EQlabs #EQregs normalize nodelta ***
    281 #blp #blm #bls * @if_elim
     242#EQt_fn #Hinit * #labs * #regs ** #EQlabs #EQregs normalize nodelta * #bl * @if_elim
    282243[ @eq_identifier_elim [2: #_ *] whd in match point_of_pc; normalize nodelta
    283244  whd in match (point_of_offset ??); #ABS #_ lapply(fetch_statement_inv … EQfetch)
     
    287248]
    288249#_ <(pc_eq_sigma_commute … goodR … Rst1st2 EQfetch) #EQbl
    289 >(pc_eq_sigma_commute … goodR … Rst1st2 EQfetch) #SBiC lapply SBiC
    290 whd in ⊢ (% → ?); * #l1 * #mid1 * #mid2 * #l2 *** #EQmid1 whd in ⊢ (% → ?);
    291 #_ whd in ⊢ (% → ?); * #nxt1 * #EQmid change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ)
    292 #_
     250>(pc_eq_sigma_commute … goodR … Rst1st2 EQfetch) #SBiC
    293251cases(bind_new_bind_new_instantiates … EQbl (bind_new_bind_new_instantiates … Hinit
    294252               (seq_commutation … goodR … EQfetch EQeval Rst1st2 t_fn EQt_fn)))
    295 [4: @EQmid |*:] #COST * #CL_OTHER * #st2_fin_no_pc normalize nodelta cases(step_to_seq ????)
    296     #seq_mid cases daemon (*TODO*)
    297     qed.
    298        
    299     cases(blm mid1) in
    300 #stmt_at_middle #EQstmt_at_middle normalize nodelta * >EQstmt_at_middle in SBiC;  destruct(EQ) whd in ⊢ (??%% → ?);#EQ destruct(EQ)
    301 
    302 
    303 * #EQst2_pre_mid_no_pc
    304 * #st2_mid * #EQst2_mid * #st2_fin_no_pc * #EQst2_fin_no_pc #Hfin
     253#l * #EQ destruct(EQ) * #st2_fin_no_pc * #EQst2_fin_no_pc #Rsem
    305254%{(mk_state_pc ? st2_fin_no_pc (pc_of_point P_out (pc_block (pc … st2)) nxt) (last_pop … st2))}
    306 %{Hfin}
    307 lapply(taaf_to_taa ???
    308            (produce_trace_any_any_free ? st2 f t_fn ??? st2_pre_mid_no_pc EQt_fn
    309                                        seq_pre_l EQst2_pre_mid_no_pc) ?)
    310 [ @if_elim #_ [2: @I] % whd in match as_costed; normalize nodelta
    311   whd in match (as_label ??); whd in match fetch_statement; normalize nodelta
    312   >EQt_fn >m_return_bind whd in match (as_pc_of ??); whd in match point_of_pc;
    313   normalize nodelta >point_of_offset_of_point >EQmid >m_return_bind
    314   normalize nodelta >COST * #H @H %]
    315 #taa1
    316 letin st2_mid_pc ≝ (mk_state_pc ? st2_mid
    317                                 (pc_of_point P_out (pc_block (pc … st2)) mid2)
    318                                 (last_pop … st2))
    319 <(point_of_pc_of_point P_out (pc_block (pc … st2)) mid2) in seq_post_l;
    320 #seq_post_l
    321 lapply (produce_trace_any_any_free (mk_prog_params P_out ? stack_sizes)
    322                      st2_mid_pc f t_fn ??? st2_fin_no_pc EQt_fn
    323                                        (seq_post_l) EQst2_fin_no_pc)
    324 * #taaf2 * #taaf2_prf1 #taaf2_prf2
    325 %{(taaf_append_taaf ???? (taaf_step ???? taa1 ??) taaf2 ?)}
    326 [ @hide_prf @if_elim [2: #_ %] @andb_elim @if_elim [2: #_ *] #H #_
    327   % whd in match (as_costed ??); whd in match (as_label ??);
    328   whd in match (as_pc_of ??); whd in match fetch_statement; normalize nodelta
    329   >EQt_fn >m_return_bind whd in match point_of_pc; normalize nodelta
    330   >point_of_offset_of_point lapply(taaf2_prf2 H) lapply seq_post_l cases bls
    331   [ #_ *] #stmt1 #tl * #lbl1 * #rest ** #EQ destruct(EQ) * #nxt1 * #EQstmt1
    332   >point_of_pc_of_point change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) #_ #_
    333   >point_of_pc_of_point in EQstmt1; #EQstmt1 >EQstmt1 >m_return_bind normalize nodelta
    334   * #H @H %
    335 | @hide_prf whd whd in match eval_state; normalize nodelta whd in match fetch_statement;
    336   normalize nodelta >EQt_fn >m_return_bind >point_of_pc_of_point >EQmid
    337   >m_return_bind >EQst2_mid >m_return_bind whd in match eval_statement_advance;
    338   normalize nodelta lapply COST lapply CL_OTHER lapply EQmid cases(blm mid1)
    339   normalize nodelta
    340   [ #c #_ #_ whd in ⊢ (??%? → ?); #EQ destruct(EQ)
    341   | #id #args #dest #_ whd in ⊢ (??%? → ?); #EQ destruct(EQ)
    342   | #r #lbl #_ whd in ⊢ (??%? → ?); #EQ destruct(EQ)
    343   | #jseq #EQjseq #_ #_ %
    344   ]
    345 | @hide_prf whd whd in ⊢ (??%?); whd in match fetch_statement; normalize nodelta >EQt_fn
    346   >m_return_bind >point_of_pc_of_point >EQmid >m_return_bind assumption
    347 | @if_elim #_ [%] % % whd in ⊢ (% → ?); * #H @H -H whd in ⊢ (??%?); >EQfetch %
    348 ]
    349 qed.
    350 *)
     255%{Rsem} 
     256%{(produce_trace_any_any_free_coerced ? st2 f t_fn l ?? st2_fin_no_pc EQt_fn
     257                                      SBiC EQst2_fin_no_pc)}
     258@if_elim #_ [@I] % % whd in ⊢ (% → ?); * #H @H -H whd in ⊢ (??%?); >EQfetch %
     259qed.
Note: See TracChangeset for help on using the changeset viewer.