Changeset 2939

Timestamp:

Mar 22, 2013, 10:11:53 AM (8 years ago)

Author:

sacerdot

Message:

Major problem: in order to accomodate the ERTLptrToLTL proof pass, the
relation between states must be parameterized over the current label.

This makes the previous proof fail:

if s1 == s2 then it is not automatically true that s1' == s2'

because the relation at s1' is no longer constrained to have any
relationship with the one at s1. More conditions are required, but
which ones?

File:

• src/joint/StatusSimulationHelper.ma (modified) (8 diffs)

src/joint/StatusSimulationHelper.ma

@@ -47 +47 @@
 
 definition joint_state_relation ≝ 
-λP_in,P_out.(Σb:block.block_region b=Code) → state P_in → state P_out → Prop.
+λP_in,P_out.(Σb:block.block_region b=Code) → label → state P_in → state P_out → Prop.
 
 definition joint_state_pc_relation ≝ λP_in,P_out.state_pc P_in → state_pc P_out → Prop.
@@ -98 +98 @@
     fetch_internal_function ? (globalenv_noinit … prog) 
      (pc_block (pc … st1))  = return 〈f,fn〉 →
-     st_no_pc_rel (pc_block(pc … st1)) (st_no_pc … st1) (st_no_pc … st2)
+     st_no_pc_rel (pc_block(pc … st1))
+     (point_of_pc P_in (pc … st1))
+     (st_no_pc … st1) (st_no_pc … st2)
 ; fetch_ok_pc_ok : 
   ∀st1,st2,f,fn.st_rel st1 st2 → 
@@ -112 +114 @@
   ∀st1,st2,pc,lp1,lp2,f,fn.
   fetch_internal_function ? (globalenv_noinit … prog) 
-   (pc_block pc) = return 〈f,fn〉 → st_no_pc_rel (pc_block pc) st1 st2 →
+   (pc_block pc) = return 〈f,fn〉 →
+   st_no_pc_rel (pc_block pc) (point_of_pc P_in pc) st1 st2 →
    lp1 = sigma_stored_pc P_in P_out prog f_lbls lp2 → 
   st_rel (mk_state_pc ? st1 pc lp1) (mk_state_pc ? st2 pc lp2)
-; as_label_ok :     let trans_prog ≝ b_graph_transform_program P_in P_out init prog in 
+; as_label_ok :
+  let trans_prog ≝ b_graph_transform_program P_in P_out init prog in 
   ∀st1,st2,f,fn,stmt. 
    fetch_statement ? (prog_var_names … prog)
@@ -146 +150 @@
                                    (st_no_pc ? st2) 
             = return st2_pre_mid_no_pc ∧
-            st_no_pc_rel (pc_block(pc … st1)) (st_no_pc … st1') (st2_pre_mid_no_pc) ∧
+            st_no_pc_rel (pc_block(pc … st1))
+             (point_of_pc P_in … (pc … st1)) (st_no_pc … st1') (st2_pre_mid_no_pc) ∧
             joint_classify_step (mk_prog_params P_out trans_prog stack_sizes) 
                                 ((\snd (\fst blp)) mid)  = cl_jump ∧
@@ -182 +187 @@
            repeat_eval_seq_no_pc (mk_prog_params P_out trans_prog stack_sizes) f 
               l  (st_no_pc … st2)= return st2_fin_no_pc ∧
-           st_no_pc_rel (pc_block (pc … st1)) (st_no_pc … st1') st2_fin_no_pc
+           st_no_pc_rel (pc_block (pc … st1))
+            (point_of_pc P_in … (pc … st1))
+            (st_no_pc … st1') st2_fin_no_pc
       ) (f_step … data (point_of_pc P_in (pc … st1)) seq)
      ) (init ? fn)
@@ -199 +206 @@
 fetch_statement P_in … (ev_genv … (mk_prog_params P_in prog stack_sizes)) (pc … st1) =
  return 〈f,fn,stmt〉 → 
-st_no_pc_rel (pc_block (pc … st1)) (st_no_pc … st1) (st_no_pc … st2).
+st_no_pc_rel (pc_block (pc … st1)) (point_of_pc P_in … (pc … st1)) (st_no_pc … st1) (st_no_pc … st2).
 #P_in #P_out #prog #stack_sizes #f_lbls #f_regs #f_lb_r #init #good #st_no_pc_rel
 #st_rel #f #fn #stmt #st1 #st2 #goodR #Hst_rel #EQfetch
@@ -264 +271 @@
 qed.
 *)
- 
+
+(*CSC: Isn't this already proved somewhere else??? *) 
+lemma point_of_pc_pc_of_point:
+ ∀P_in: sem_graph_params.∀l,st.
+   point_of_pc P_in
+    (pc_of_point (mk_sem_graph_params (sgp_pars P_in) (sgp_sup P_in))
+     (pc_block (pc P_in st)) l) = l.
+ #P * //
+qed.
 
 lemma general_eval_cond_ok : ∀ P_in , P_out: sem_graph_params.
@@ -334 +349 @@
 [1,3: @(st_rel_def … goodR … f fn ?) 
       [1,4: change with (pc_block (pc … st1)) in match (pc_block ?); assumption
-      |2,5: assumption
+      |2,5: >point_of_pc_pc_of_point assumption
       |3,6: @(fetch_stmt_ok_sigma_last_pop_ok … goodR … EQfetch) assumption
       ]