Changeset 2883 for src/joint

Timestamp:

Mar 15, 2013, 6:33:18 PM (8 years ago)

Author:

piccolo

Message:

partial commit

Location:

src/joint

Files:

• StatusSimulationHelper.ma (modified) (9 diffs)
• semantics_blocks.ma (modified) (2 diffs)

src/joint/StatusSimulationHelper.ma

@@ -44 +44 @@
  @Hr
 ]
-qed. 
-
-check joint_classify
-check as_label
+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.
+ 
 
 record good_state_relation (P_in : sem_graph_params) 
@@ -59 +75 @@
                                 stack_sizes) 
         → Prop) : Prop ≝ 
-{ pc_eq_sigma_commute : ∀st1,st2.R st1 st2 → pc … st1 = pc … st2
+{ pc_eq_sigma_commute : ∀st1,st2,f,fn,stmt.R st1 st2 → 
+                 fetch_statement ? (prog_var_names … prog) 
+                     (globalenv_noinit … prog) (pc … st1)  = return 〈f,fn,stmt〉 → 
+                 pc … st1 = pc … st2
 ; as_label_ok : ∀st1 : joint_abstract_status (mk_prog_params P_in prog stack_sizes).
                 ∀st2 : joint_abstract_status ?. 
@@ -70 +89 @@
     ∀st1,st1' : joint_abstract_status (mk_prog_params P_in prog stack_sizes) .
     ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes).
-    ∀f,fn,a,ltrue,lfalse. 
-    eval_state P_in (prog_var_names … ℕ prog) (ev_genv … (mk_prog_params P_in prog stack_sizes)) 
-    st1 = return st1' →
+    ∀f,fn,a,ltrue,lfalse.
     let cond ≝ (COND P_in ? a ltrue) in
     fetch_statement P_in … (ev_genv … (mk_prog_params P_in prog stack_sizes)) (pc … st1) = 
-    return 〈f, fn,  sequential … cond lfalse〉 → 
+    return 〈f, fn,  sequential … cond lfalse〉 →  
+    eval_state P_in (prog_var_names … ℕ prog) (ev_genv … (mk_prog_params P_in prog stack_sizes)) 
+    st1 = return st1' → 
     R st1 st2 → 
     ∀t_fn.
@@ -82 +101 @@
     bind_new_P' ??
      (λregs1.λdata.bind_new_P' ?? 
-     (λregs2.λblp.
-        ∀mid,nxt1.
+     (λregs2.λblp.(\snd blp) = [ ] ∧
+        ∀mid.
           stmt_at ? (prog_var_names … trans_prog) (joint_if_code ?? t_fn) mid
-          = return sequential P_out ? ((\snd (\fst blp)) mid) nxt1→ 
+          = return sequential P_out ? ((\snd (\fst blp)) mid) lfalse→ 
          ∃st2_pre_mid_no_pc. 
             repeat_eval_seq_no_pc (mk_prog_params P_out trans_prog stack_sizes) f (map_eval ?? (\fst (\fst blp)) mid) 
@@ -95 +114 @@
                                 ((\snd (\fst blp)) mid)  = cl_jump ∧
             cost_label_of_stmt (mk_prog_params P_out trans_prog stack_sizes) 
-                               (sequential P_out ? ((\snd (\fst blp)) mid) nxt1) = None ? ∧
-            (\snd blp) = [ ] ∧
+                               (sequential P_out ? ((\snd (\fst blp)) mid) lfalse) = None ? ∧
             ∃st2_mid .
                 eval_state P_out (prog_var_names … trans_prog) 
@@ -103 +121 @@
    )  (f_step … data (point_of_pc P_in (pc … st1)) cond)   
   ) (init ? fn)
+; seq_commutation :
+  let trans_prog ≝ b_graph_transform_program P_in P_out init prog in 
+  ∀st1,st1' : joint_abstract_status (mk_prog_params P_in prog stack_sizes) .
+  ∀st2 : joint_abstract_status (mk_prog_params P_out trans_prog stack_sizes).
+  ∀f,fn,stmt,nxt.
+  let seq ≝ (step_seq P_in ? stmt) in
+  fetch_statement P_in … (ev_genv … (mk_prog_params P_in prog stack_sizes)) (pc … st1) = 
+  return 〈f, fn,  sequential … seq nxt〉 →  
+  eval_state P_in (prog_var_names … ℕ prog) (ev_genv … (mk_prog_params P_in prog stack_sizes)) 
+  st1 = return st1' → 
+  R st1 st2 → 
+  ∀t_fn.
+  fetch_internal_function … (globalenv_noinit … trans_prog) (pc_block (pc … st2)) =
+  return 〈f,t_fn〉 → 
+  bind_new_P' ??
+     (λregs1.λdata.bind_new_P' ?? 
+     (λregs2.λblp.
+           ∀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
+           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 ∧
+           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)
+      ) (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.
@@ -135 +190 @@
 #f #fn #a #ltrue #lfalse #Rst1st2 #EQfetch #EQeval #n_costed 
 cases(b_graph_transform_program_fetch_statement … good … EQfetch)
-#init_data * #t_fn1 **  >(pc_eq_sigma_commute … goodR … Rst1st2)
+#init_data * #t_fn1 **  >(pc_eq_sigma_commute … goodR … Rst1st2 EQfetch)
 #EQt_fn1 whd in ⊢ (% → ?); #Hinit 
 * #labs * #regs 
@@ -142 +197 @@
 [ @eq_identifier_elim [2: #_ *] whd in match point_of_pc; normalize nodelta 
   whd in match (point_of_offset ??); #ABS #_ lapply(fetch_statement_inv … EQfetch) 
-  * #_ >(pc_eq_sigma_commute … goodR … Rst1st2) whd in match point_of_pc; 
+  * #_ >(pc_eq_sigma_commute … goodR … Rst1st2 EQfetch) whd in match point_of_pc; 
   normalize nodelta whd in match (point_of_offset ??); <ABS 
   cases(entry_is_cost … (pi2 ?? fn)) #nxt1 * #c #EQ >EQ #EQ1 destruct(EQ1)
 ]
-#_ <(pc_eq_sigma_commute … goodR … Rst1st2) #EQbl whd in ⊢ (% → ?); * #l1 * #mid1 
+#_ <(pc_eq_sigma_commute … goodR … Rst1st2 EQfetch) #EQbl whd in ⊢ (% → ?); * #l1 * #mid1 
 * #mid2 * #l2 *** #EQmid1 whd in ⊢ (% → ?); #seq_pre_l whd in ⊢ (% → ?); * #nxt1 
 * #EQmid change with nxt1 in ⊢ (??%? → ?); #EQ destruct(EQ)
-cases(bind_new_bind_new_instantiates … EQbl 
-            (bind_new_bind_new_instantiates … Hinit
-               (cond_commutation … goodR … EQeval EQfetch Rst1st2 t_fn1 EQt_fn1))
-            … EQmid)    
-#st_pre_mid_no_pc * #EQst_pre_mid_no_pc *** #CL_JUMP #COST #EQ destruct(EQ) *
-#st2_mid * #EQst2mid #Hst2_mid whd in ⊢(% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2)
-%{st2_mid} %{Hst2_mid} 
->(pc_eq_sigma_commute … goodR … Rst1st2) in seq_pre_l; #seq_pre_l
+cases(bind_new_bind_new_instantiates … EQbl (bind_new_bind_new_instantiates … Hinit
+               (cond_commutation … goodR … EQfetch EQeval Rst1st2 t_fn1 EQt_fn1)))
+#EQ destruct(EQ) #APP whd in ⊢ (% → ?); * #EQ1 #EQ2 destruct(EQ1 EQ2)
+cases(APP … EQmid) -APP 
+#st_pre_mid_no_pc * #EQst_pre_mid_no_pc ** #CL_JUMP #COST *
+#st2_mid * #EQst2mid #Hst2_mid %{st2_mid} %{Hst2_mid} 
+>(pc_eq_sigma_commute … goodR … Rst1st2 EQfetch) in seq_pre_l; #seq_pre_l
 lapply(taaf_to_taa ??? 
            (produce_trace_any_any_free ? st2 f t_fn1 ??? st_pre_mid_no_pc EQt_fn1
@@ -174 +228 @@
 qed.
 
+(*
+let rec taa_to_taaf  S st1 st2 (taa : trace_any_any S st1 st2) on taa :
+trace_any_any_free S st1 st2 ≝ 
+(match taa in trace_any_any return λs1,s2.λx.st1 = s1 → st2 = s2 → taa ≃ x → trace_any_any_free S s1 s2 with
+[taa_base st1' ⇒ λprf.? 
+|taa_step st1' st2' st3' H I J tl ⇒ λprf.?
+]) (refl … st1) (refl … st2) (refl_jmeq ? taa).
+*)
+
+lemma general_eval_seq_no_call_ok : ∀ P_in , P_out: sem_graph_params.
+∀prog : joint_program P_in.
+∀stack_sizes.
+∀ f_lbls,f_regs.∀f_bl_r.∀init.
+∀good : b_graph_transform_program_props P_in P_out init prog f_bl_r f_lbls f_regs.
+let prog_pars_in ≝ mk_prog_params P_in prog stack_sizes in
+let trans_prog  ≝ b_graph_transform_program P_in P_out init prog in
+let prog_pars_out ≝ mk_prog_params P_out trans_prog stack_sizes in
+∀ R : joint_abstract_status prog_pars_in → joint_abstract_status prog_pars_out → Prop.
+good_state_relation P_in P_out prog stack_sizes init R → 
+∀st1,st1' : joint_abstract_status prog_pars_in.
+∀st2 : joint_abstract_status prog_pars_out.
+∀f.
+∀fn : joint_closed_internal_function P_in (prog_var_names … prog).
+∀stmt,nxt.
+R st1 st2 → 
+    let seq ≝ (step_seq P_in ? stmt) in
+ fetch_statement P_in …
+  (globalenv_noinit ? prog) (pc … st1) = 
+    return 〈f, fn,  sequential ?? seq nxt〉 → 
+ eval_state P_in (prog_var_names … ℕ prog) (ev_genv … prog_pars_in) 
+            st1 = return st1' → 
+∃st2'. R st1' st2' ∧            
+∃taf : trace_any_any_free (joint_abstract_status prog_pars_out) st2 st2'.            
+ 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').
+#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
+[ @eq_identifier_elim [2: #_ *] whd in match point_of_pc; normalize nodelta 
+  whd in match (point_of_offset ??); #ABS #_ lapply(fetch_statement_inv … EQfetch) 
+  * #_ >(pc_eq_sigma_commute … goodR … Rst1st2 EQfetch) whd in match point_of_pc; 
+  normalize nodelta whd in match (point_of_offset ??); <ABS 
+  cases(entry_is_cost … (pi2 ?? fn)) #nxt1 * #c #EQ >EQ #EQ1 destruct(EQ1)
+]
+#_ <(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)
+#_
+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
+%{(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.
+*)

src/joint/semantics_blocks.ma

@@ -146 +146 @@
   seq_list_in_code … (joint_if_code … curr_fn) src b l dst →
   repeat_eval_seq_no_pc p curr_id b st = return st' →
-  trace_any_any_free (joint_abstract_status p) st
-    (mk_state_pc ? st' (pc_of_point p (pc_block (pc … st)) dst) (last_pop … st)) ≝
+  Σtaaf :trace_any_any_free (joint_abstract_status p) st
+    (mk_state_pc ? st' (pc_of_point p (pc_block (pc … st)) dst) (last_pop … st)).
+    (not_empty … b ↔ bool_to_Prop (taaf_non_empty … taaf)) ≝
   λp,st,curr_id,curr_fn,b,l,dst,st',prf1,prf2,prf3.
   produce_trace_any_any_free_aux p st curr_id curr_fn b l dst st' prf1 prf2 prf3.
@@ -175 +176 @@
   #H #G
   %2{(taa_base …)} assumption
-| #hd #tl #_ #EQ <EQ -hd -tl @produce_trace_any_any_free assumption
+| #hd #tl #_ #EQ <EQ -hd -tl #H1 #H2 @(produce_trace_any_any_free …) assumption
 ]
 qed.