Changeset 2891 for src/joint


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

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

File:
1 edited

Legend:

Unmodified
Added
Removed
  • 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.