Changeset 2891

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

Location:

src

Files:

• ERTL/ERTLtoERTLptrOK.ma (modified) (2 diffs)
• ERTL/ERTLtoERTLptrUtils.ma (modified) (4 diffs)
• joint/StatusSimulationHelper.ma (modified) (4 diffs)

src/ERTL/ERTLtoERTLptrOK.ma

@@ -160 +160 @@
 
 include "joint/StatusSimulationHelper.ma".
+include alias "basics/lists/listb.ma".
 
 lemma make_ERTL_To_ERTLptr_good_state_relation :
@@ -209 +210 @@
   change with (pc_block (pc … st2)) in match (pc_block ?);
   <(fetch_stmt_ok_sigma_pc_ok … EQfetch) >EQfn %
+| #st1 #st1' #st2 #f #fn #stmt #nxt #EQfetch whd in match eval_state;
+  whd in match eval_statement_no_pc; normalize nodelta >EQfetch >m_return_bind 
+  normalize nodelta #H @('bind_inversion H) -H #st1_no_pc' #EQst1_no_pc'
+  whd in ⊢ (??%% → ?); #EQ destruct(EQ) whd in ⊢ (%→?); #EQ destruct(EQ)
+  whd in match sigma_state_pc in EQst1_no_pc'; normalize  nodelta in EQst1_no_pc';
+  cases(fetch_statement_inv … EQfetch) >(fetch_stmt_ok_sigma_pc_ok … EQfetch)
+  #EQfn #EQstmt >EQfn in EQst1_no_pc'; normalize nodelta #EQst1_no_pc'
+  #t_fn #EQt_fn whd % [2: %{(refl …)} |] lapply(err_eq_from_io ????? EQst1_no_pc')
+  -EQst1_no_pc' #EQst1_no_pc'
+  cases(eval_seq_no_pc_no_call_ok prog f_lbls f_regs ???????? EQst1_no_pc')
+  [ #st2_no_pc' * #EQst2_no_pc' #EQ destruct(EQ)
+  %{(mk_state_pc ? st2_no_pc' 
+     (pc_of_point ERTLptr_semantics (pc_block (pc … st2)) nxt)
+     (last_pop … st2))} %
+     [ whd in ⊢ (??%?); >EQst2_no_pc' %
+     | whd whd in match sigma_state_pc; normalize nodelta >EQfn %
+     ]
+  |  #lbl whd in match code_has_label; whd in match code_has_point; normalize nodelta
+  inversion(stmt_at ????) [#_ *] #stmt1 #EQstmt1 #_ 
+  cut(fetch_statement ERTL_semantics (prog_var_names … prog) (globalenv_noinit … prog)
+                      (pc_of_point ERTL_semantics (pc_block (pc … st2)) lbl) =
+                 return 〈f,fn,stmt1〉)
+   [ whd in ⊢ (??%?); >EQfn normalize nodelta >point_of_pc_of_point >EQstmt1 %] #EQf_stmt1
+  cases(b_graph_transform_program_fetch_statement_plus … good … EQf_stmt1)
+  #init * #t_fn' ** #EQt_fn' whd in ⊢ (% → ?); cases(init_regs ?) [2: #x #y *]
+  normalize nodelta #EQ destruct(EQ) * #labels * #registers
+  ******* #EQlabels >point_of_pc_of_point change with (pc_block (pc … st2)) in match (pc_block ?); 
+  #EQregisters #_ #_ #_ #_ #fresh_regs #_ >EQregisters
+  cases(excluded_middle_list ? (λreg.bool_to_Prop(¬(reg∈registers))) 
+         (get_used_registers_from_seq … (functs ERTL) stmt) ?) 
+  [3: #a #_ cases(¬a∈registers) // |1: #H assumption] #H @⊥
+  cases(Exists_All … H (regs_are_in_univers … (pi2 ?? fn) … EQstmt))
+   #reg ** #H1 #H2 @H1 -H1 @notb_Prop % #H1 lapply(fresh_regs … lbl) >EQregisters 
+  #H3 lapply(All_memb … H3 H1) ** #H4 #_ @H4 assumption
+  ]
 ]
 qed.

src/ERTL/ERTLtoERTLptrUtils.ma

@@ -413 +413 @@
      (be_op2 b op).
 #prog #sigma #b #op #bv #bv1 whd in match be_op2; normalize nodelta
-cases bv
+cases daemon
+qed. (*TODO*)
+(*cases bv
 [ | | #ptr1 #ptr2 #p | #by | #p | #ptr #p | #pc1 #p1]
-normalize nodelta [@res_preserve_error1] whd in match sigma_beval;
+normalize nodelta [cases op normalize nodelta @res_preserve_error1] whd in match sigma_beval;
 normalize nodelta
 cases bv1
@@ -499 +501 @@
       ]
 ]
-qed.
+qed.*)
 
 lemma pointer_of_address_ok : ∀prog : ertl_program.∀f_lbls : lbl_funct.
@@ -1049 +1051 @@
         sigma_stored_pc prog f_lbls pc〉)
      (pop_ra ERTL_semantics)
-     (pop_ra ERTLptr_semantics).   
+     (pop_ra ERTLptr_semantics).
+cases daemon (*TODO*) qed.
+(*        
 #prog #f_lbls #f_regs #restr1 #st whd in match pop_ra; normalize nodelta 
 @mfr_bind1
@@ -1088 +1092 @@
 | #pc @mfr_return_eq1 %
 ]
-qed.
+qed.*)
 
 lemma pc_block_eq : ∀prog : ertl_program. ∀f_lbls,pc. 

src/joint/StatusSimulationHelper.ma

@@ -45 +45 @@
 ]
 qed.
-
-
-definition step_to_seq : ∀p : prog_params.∀stmt : joint_step p (globals p).
-joint_classify_step p stmt = cl_other → 
-(∀c.stmt ≠ COST_LABEL ?? c) → Σ seq.stmt = step_seq ?? seq ≝ 
-λp,stmt,CL_OTHER,COST.
-(match stmt return λx.x = stmt → ? with
-[ COST_LABEL c ⇒ λprf.⊥
-| CALL id args dest ⇒ λprf.⊥
-| COND r lab ⇒ λprf.⊥
-| step_seq seq ⇒ λprf.«seq,?»
-])(refl …).
-@hide_prf
-[ lapply(COST c) * #H @H >prf %
-|2,3: <prf in CL_OTHER; whd in match (joint_classify_step ??); #EQ destruct(EQ)
-| >prf %
-]
-qed.
-
-check ensure_step_block 
 
 record good_state_relation (P_in : sem_graph_params) 
@@ -141 +121 @@
        ∃l : list (joint_seq (mk_prog_params P_out trans_prog stack_sizes)
                             (globals (mk_prog_params P_out trans_prog stack_sizes))).
-                            blp = (ensure_step_block ?? l) ∧ True
-       (*
-       TUTTO IL RESTO PARLA DI R
-       
-           ∀mid,mid1.
-            stmt_at ? (prog_var_names … trans_prog) (joint_if_code ?? t_fn) mid
-            = return sequential P_out ? ((\snd (\fst blp)) mid) mid1→ 
-            ∃CL_OTHER : joint_classify_step (mk_prog_params P_out trans_prog stack_sizes) 
-                          ((\snd (\fst blp)) mid)  = cl_other.
-            ∃COST : cost_label_of_stmt (mk_prog_params P_out trans_prog stack_sizes) 
-                         (sequential P_out ? ((\snd (\fst blp)) mid) mid1) = None ?.
-            ∃st2_fin_no_pc.
-            let pre ≝ (map_eval ?? (\fst (\fst blp)) mid) in
-            let middle ≝ [pi1 ?? (step_to_seq (mk_prog_params P_out trans_prog stack_sizes) 
-                                  ((\snd (\fst blp)) mid) CL_OTHER ?)] in
+                            blp = (ensure_step_block ?? l) ∧
+       ∃st2_fin_no_pc.
            repeat_eval_seq_no_pc (mk_prog_params P_out trans_prog stack_sizes) f 
-              (pre@ middle @ (\snd blp))  (st_no_pc … st2)= return st2_fin_no_pc ∧
+              l  (st_no_pc … st2)= return st2_fin_no_pc ∧
            let st2_fin ≝ 
            mk_state_pc ? st2_fin_no_pc 
                          (pc_of_point P_out (pc_block(pc … st2)) nxt) 
                          (last_pop … st2) in
-           R st1' st2_fin *) ) (f_step ??? data (point_of_pc P_in (pc … st1)) seq)
+           R st1' st2_fin) (f_step ??? data (point_of_pc P_in (pc … st1)) seq)
       ) (init ? fn)          
 }.
-(*@hide_prf #c % #EQ >EQ in COST; whd in ⊢ (??%% → ?); #EQ destruct(EQ)
-qed.*)
 
 lemma general_eval_cond_ok : ∀ P_in , P_out: sem_graph_params.
@@ -270 +235 @@
  if taaf_non_empty … taf then True else  (*IT CAN BE SIMPLIFIED *)
 (¬as_costed (joint_abstract_status (mk_prog_params P_in prog stack_sizes)) st1 ∨ 
- ¬as_costed (joint_abstract_status (mk_prog_params P_in prog stack_sizes)) st1').
-cases daemon qed. 
- 
-(* 
+ ¬as_costed (joint_abstract_status (mk_prog_params P_in prog stack_sizes)) st1'). 
 #P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_bl_r #init #good #R #goodR #st1 #st1'
 #st2 #f #fn #stmt #nxt #Rst1st2 #EQfetch #EQeval
 cases(b_graph_transform_program_fetch_statement … good … EQfetch)
 #init_data * #t_fn ** >(pc_eq_sigma_commute … goodR … Rst1st2 EQfetch) 
-#EQt_fn #Hinit * #labs * #regs ** #EQlabs #EQregs normalize nodelta *** 
-#blp #blm #bls * @if_elim
+#EQt_fn #Hinit * #labs * #regs ** #EQlabs #EQregs normalize nodelta * #bl * @if_elim
 [ @eq_identifier_elim [2: #_ *] whd in match point_of_pc; normalize nodelta 
   whd in match (point_of_offset ??); #ABS #_ lapply(fetch_statement_inv … EQfetch) 
@@ -287 +248 @@
 ]
 #_ <(pc_eq_sigma_commute … goodR … Rst1st2 EQfetch) #EQbl 
->(pc_eq_sigma_commute … goodR … Rst1st2 EQfetch) #SBiC lapply SBiC
-whd in ⊢ (% → ?); * #l1 * #mid1 * #mid2 * #l2 *** #EQmid1 whd in ⊢ (% → ?);
-#_ whd in ⊢ (% → ?); * #nxt1 * #EQmid change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ)
-#_
+>(pc_eq_sigma_commute … goodR … Rst1st2 EQfetch) #SBiC 
 cases(bind_new_bind_new_instantiates … EQbl (bind_new_bind_new_instantiates … Hinit
                (seq_commutation … goodR … EQfetch EQeval Rst1st2 t_fn EQt_fn)))
-[4: @EQmid |*:] #COST * #CL_OTHER * #st2_fin_no_pc normalize nodelta cases(step_to_seq ????)
-    #seq_mid cases daemon (*TODO*)
-    qed.
-        
-    cases(blm mid1) in 
-#stmt_at_middle #EQstmt_at_middle normalize nodelta * >EQstmt_at_middle in SBiC;  destruct(EQ) whd in ⊢ (??%% → ?);#EQ destruct(EQ)
-
-
-* #EQst2_pre_mid_no_pc
-* #st2_mid * #EQst2_mid * #st2_fin_no_pc * #EQst2_fin_no_pc #Hfin
+#l * #EQ destruct(EQ) * #st2_fin_no_pc * #EQst2_fin_no_pc #Rsem
 %{(mk_state_pc ? st2_fin_no_pc (pc_of_point P_out (pc_block (pc … st2)) nxt) (last_pop … st2))}
-%{Hfin}
-lapply(taaf_to_taa ??? 
-           (produce_trace_any_any_free ? st2 f t_fn ??? st2_pre_mid_no_pc EQt_fn
-                                       seq_pre_l EQst2_pre_mid_no_pc) ?)
-[ @if_elim #_ [2: @I] % whd in match as_costed; normalize nodelta
-  whd in match (as_label ??); whd in match fetch_statement; normalize nodelta 
-  >EQt_fn >m_return_bind whd in match (as_pc_of ??); whd in match point_of_pc;
-  normalize nodelta >point_of_offset_of_point >EQmid >m_return_bind
-  normalize nodelta >COST * #H @H %]
-#taa1 
-letin st2_mid_pc ≝ (mk_state_pc ? st2_mid 
-                                (pc_of_point P_out (pc_block (pc … st2)) mid2)
-                                (last_pop … st2))
-<(point_of_pc_of_point P_out (pc_block (pc … st2)) mid2) in seq_post_l;
-#seq_post_l
-lapply (produce_trace_any_any_free (mk_prog_params P_out ? stack_sizes) 
-                     st2_mid_pc f t_fn ??? st2_fin_no_pc EQt_fn
-                                       (seq_post_l) EQst2_fin_no_pc)
-* #taaf2 * #taaf2_prf1 #taaf2_prf2 
-%{(taaf_append_taaf ???? (taaf_step ???? taa1 ??) taaf2 ?)} 
-[ @hide_prf @if_elim [2: #_ %] @andb_elim @if_elim [2: #_ *] #H #_ 
-  % whd in match (as_costed ??); whd in match (as_label ??);
-  whd in match (as_pc_of ??); whd in match fetch_statement; normalize nodelta
-  >EQt_fn >m_return_bind whd in match point_of_pc; normalize nodelta
-  >point_of_offset_of_point lapply(taaf2_prf2 H) lapply seq_post_l cases bls
-  [ #_ *] #stmt1 #tl * #lbl1 * #rest ** #EQ destruct(EQ) * #nxt1 * #EQstmt1
-  >point_of_pc_of_point change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ) #_ #_
-  >point_of_pc_of_point in EQstmt1; #EQstmt1 >EQstmt1 >m_return_bind normalize nodelta
-  * #H @H %
-| @hide_prf whd whd in match eval_state; normalize nodelta whd in match fetch_statement;
-  normalize nodelta >EQt_fn >m_return_bind >point_of_pc_of_point >EQmid
-  >m_return_bind >EQst2_mid >m_return_bind whd in match eval_statement_advance;
-  normalize nodelta lapply COST lapply CL_OTHER lapply EQmid cases(blm mid1) 
-  normalize nodelta
-  [ #c #_ #_ whd in ⊢ (??%? → ?); #EQ destruct(EQ)
-  | #id #args #dest #_ whd in ⊢ (??%? → ?); #EQ destruct(EQ)
-  | #r #lbl #_ whd in ⊢ (??%? → ?); #EQ destruct(EQ)
-  | #jseq #EQjseq #_ #_ %
-  ]
-| @hide_prf whd whd in ⊢ (??%?); whd in match fetch_statement; normalize nodelta >EQt_fn
-  >m_return_bind >point_of_pc_of_point >EQmid >m_return_bind assumption
-| @if_elim #_ [%] % % whd in ⊢ (% → ?); * #H @H -H whd in ⊢ (??%?); >EQfetch %
-]
-qed.
-*)
+%{Rsem}  
+%{(produce_trace_any_any_free_coerced ? st2 f t_fn l ?? st2_fin_no_pc EQt_fn 
+                                      SBiC EQst2_fin_no_pc)}
+@if_elim #_ [@I] % % whd in ⊢ (% → ?); * #H @H -H whd in ⊢ (??%?); >EQfetch %
+qed.