Changeset 2464 for src/joint/lineariseProof.ma

Timestamp:

Nov 14, 2012, 5:38:57 PM (8 years ago)

Author:

piccolo

Message:

adapted lineariseProof to new semantics

File:

• src/joint/lineariseProof.ma (modified) (3 diffs)

src/joint/lineariseProof.ma

@@ -16 +16 @@
 include "common/StatusSimulation.ma".   
 include "joint/Traces.ma".
-include "joint/SemanticUtils.ma".
-
-definition graph_prog_params:
-  ∀p:unserialized_params. 
-  (∀F.sem_unserialized_params p F) →
-    joint_program (mk_graph_params p) →
-   prog_params
- ≝
- λp,p',prog.
-  (mk_prog_params
-   (make_sem_graph_params (mk_graph_params p) p')
-   prog).
-
-definition lin_prog_params:
-  ∀p:unserialized_params. 
-  (∀F.sem_unserialized_params p F) →
-    joint_program (mk_lin_params p) →
-   prog_params
- ≝
- λp,p',prog.
-  (mk_prog_params
-   (make_sem_lin_params (mk_lin_params p) p')
-   prog).
-
-(*CSC: Paolo, come to the rescue*)
-axiom choose_sigma:
-  ∀p:unserialized_params. 
-  (∀F.sem_unserialized_params p F) →
-    joint_program (mk_graph_params p) →
-   identifier LabelTag → option ℕ.
-
-(*CSC: Paolo, come to the rescue*)
-axiom linearise_code_spec:
- ∀p : unserialized_params.
- ∀p':(∀F.sem_unserialized_params p F).
- ∀graph_prog:joint_program (mk_graph_params p).
- ∀graph_fun:joint_closed_internal_function (mk_graph_params p)
-                           (globals (graph_prog_params p p' graph_prog)).
- let sigma ≝ choose_sigma p p' graph_prog in
- let lin_fun ≝ linearise_int_fun … graph_fun in
- let g ≝ joint_if_code ?? (pi1 … graph_fun) in
- let c ≝ joint_if_code ?? (pi1 … lin_fun) in
- ∀entry : (Σl.bool_to_Prop (code_has_label … g l)).
-      code_closed … c ∧
-      sigma entry = Some ? 0 ∧
-      ∀l,n.sigma l = Some ? n →
-        ∃s. lookup … g l = Some ? s ∧
-          opt_Exists ?
-            (λls.let 〈lopt, ts〉 ≝ ls in
-              opt_All ? (eq ? l) lopt ∧
-              ts = graph_to_lin_statement … s ∧
-              opt_All ?
-                (λnext.Or (sigma next = Some ? (S n))
-                (nth_opt … (S n) c = Some ? 〈None ?, GOTO … next〉))
-                (stmt_implicit_label … s)) (nth_opt … n c). 
-   
+include "joint/semanticsUtils.ma".
+
+definition good_local_sigma :
+  ∀p:unserialized_params.
+  ∀p':(∀F.sem_unserialized_params p F).
+  ∀globals.
+  joint_closed_internal_function (mk_graph_params p) globals →
+  (label → option ℕ) → Prop ≝
+  λp,p',globals,graph_fun,sigma.
+   let lin_fun ≝ linearise_int_fun … graph_fun in
+   let g ≝ joint_if_code ?? (pi1 … graph_fun) in
+   let c ≝ joint_if_code ?? (pi1 … lin_fun) in
+   ∀entry : (Σl.bool_to_Prop (code_has_label … g l)).
+        code_closed … c ∧
+        sigma entry = Some ? 0 ∧
+        ∀l,n.sigma l = Some ? n →
+          lt n 2^offset_size →
+          ∃s. lookup … g l = Some ? s ∧
+            opt_Exists ?
+              (λls.let 〈lopt, ts〉 ≝ ls in
+                opt_All ? (eq ? l) lopt ∧
+                ts = graph_to_lin_statement … s ∧
+                opt_All ?
+                  (λnext.Or (sigma next = Some ? (S n))
+                  (nth_opt … (S n) c = Some ? 〈None ?, GOTO … next〉))
+                  (stmt_implicit_label … s)) (nth_opt … n c). 
+
+axiom prog_if_of_function :
+  ∀p.∀prog : joint_program p.
+  (Σi.is_internal_function_of_program … prog i) →
+    joint_closed_internal_function p (prog_var_names … prog).
+
+definition if_in_global_env_to_if_in_prog :
+  ∀prog_pars : prog_params.∀f : Σi.is_internal_function … (ev_genv prog_pars) i.
+  Σi.is_internal_function_of_program ? (prog prog_pars) i ≝
+  λprog_pars,f.pi1 ?? f.
+@is_internal_function_of_program_ok @(pi2 … f) qed.
+
+coercion if_in_prog_from_if_in_global_env nocomposites :
+  ∀prog_pars : prog_params.∀f : Σi.is_internal_function … (ev_genv prog_pars) i.
+  Σi.is_internal_function_of_program ? (prog prog_pars) i ≝
+  if_in_global_env_to_if_in_prog
+  on _f : Sig ident (λi.is_internal_function ??? i)
+  to Sig ident (λi.is_internal_function_of_program ?? i).
+
+definition good_sigma :
+  ∀p:unserialized_params.
+  ∀p':(∀F.sem_unserialized_params p F).
+  ∀prog : joint_program (mk_graph_params p).
+  ((Σi.is_internal_function_of_program … prog i) → label → option ℕ) → Prop ≝
+  λp,p',graph_prog,sigma.
+  ∀i.
+  let graph_fun ≝ prog_if_of_function ?? i in
+  let sigma_local ≝ sigma i in
+  good_local_sigma ? p' ? graph_fun sigma_local.
+
+definition graph_prog_params ≝
+λp,p',prog,stack_sizes.
+mk_prog_params (make_sem_graph_params p p') prog stack_sizes.
+
 definition graph_abstract_status:
  ∀p:unserialized_params. 
   (∀F.sem_unserialized_params p F) →
-    joint_program (mk_graph_params p) →
+    ∀prog : joint_program (mk_graph_params p).
+  ((Σi.is_internal_function_of_program … prog i) → ℕ) → 
      abstract_status
  ≝
- λp,p',prog.
-  joint_abstract_status (graph_prog_params p p' prog).
+ λp,p',prog,stack_sizes.
+ joint_abstract_status (graph_prog_params ? p' prog stack_sizes).
+
+definition lin_prog_params ≝
+λp,p',prog,stack_sizes.
+mk_prog_params (make_sem_lin_params p p') prog stack_sizes.
 
 definition lin_abstract_status:
  ∀p:unserialized_params. 
   (∀F.sem_unserialized_params p F) →
-    joint_program (mk_lin_params p) →
+    ∀prog : joint_program (mk_lin_params p).
+  ((Σi.is_internal_function_of_program … prog i) → ℕ) → 
      abstract_status
  ≝
- λp,p',prog.
-  joint_abstract_status (lin_prog_params p p' prog).
-
-(*CSC: BUG, the natural must be ≤ 2^16! *)
-(*CSC: already defined? *)
-definition pointer_of_block_and_lin_offset :
- ∀b:block. block_region b = Code → nat → cpointer ≝
-  λb,p,n. «mk_pointer b (mk_offset (bitvector_of_nat … n)), p».
+ λp,p',prog,stack_sizes.
+ joint_abstract_status (lin_prog_params ? p' prog stack_sizes).
+
+definition sigma_pc_opt:
+ ∀p,p',graph_prog,stack_sizes.
+  ((Σi.is_internal_function_of_program … graph_prog i) → 
+    code_point (mk_graph_params p) → option ℕ) →
+   cpointer → option cpointer
+ ≝
+  λp,p',prog,stack_sizes,sigma,pc.
+  let pars ≝ graph_prog_params p p' prog stack_sizes in
+  let ge ≝ ev_genv pars in
+  ! f ← int_funct_of_block ?? ge (pblock pc) ;
+  ! lin_point ← sigma f (point_of_pointer … pars pc) ;
+  res_to_opt … (pointer_of_point ? (make_sem_lin_params ? p') pc lin_point).
+
+definition well_formed_pc:
+ ∀p,p',graph_prog,stack_sizes.
+  ((Σi.is_internal_function_of_program … graph_prog i) → 
+    label → option ℕ) →
+   cpointer → Prop
+ ≝
+ λp,p',prog,stack_sizes,sigma,pc.
+  sigma_pc_opt p p' prog stack_sizes sigma pc
+   ≠ None ….
 
 definition well_formed_status:
+ ∀p,p',graph_prog,stack_sizes.
+  ((Σi.is_internal_function_of_program … graph_prog i) → 
+    label → option ℕ) →
+  state_pc (make_sem_graph_params p p') → Prop ≝
+ λp,p',prog,stack_sizes,sigma,st.
+ well_formed_pc p p' prog stack_sizes sigma (pc … st) ∧ ?.
+cases daemon (* TODO *)
+qed.
+
+(* 
+lemma prova : ∀p,s,st,prf.sigma_pc_of_status p s st prf = ?.
+[ #p #s #st #prf
+  whd in match sigma_pc_of_status; normalize nodelta
+  @opt_safe_elim
+  #n
+  lapply (refl …  (int_funct_of_block (joint_closed_internal_function p) (globals p)
+        (ev_genv p) (pblock (pc p st))))
+  elim (int_funct_of_block (joint_closed_internal_function p) (globals p)
+        (ev_genv p) (pblock (pc p st))) in ⊢ (???%→%);
+  [ #_ #ABS normalize in ABS; destruct(ABS) ]
+  #f #EQ >m_return_bind
+*)
+
+
+(*
+lemma wf_status_to_wf_pc : 
+∀p,p',graph_prog,stack_sizes.
+∀sigma : ((Σi.is_internal_function_of_program … graph_prog i) → 
+    code_point (mk_graph_params p) → option ℕ).
+∀st.
+well_formed_status p p' graph_prog stack_sizes sigma st →
+well_formed_pc p p' graph_prog stack_sizes sigma (pc ? st).
+#p #p' #graph_prog #stack_sizes #sigma #st whd in ⊢ (% → ?); * #H #_ @H
+qed.
+
+lemma sigma_pc_of_status_ok:
+  ∀p,p',graph_prog,stack_sizes.
+  ∀sigma.
+   ∀st.
+    ∀prf:well_formed_status p p' graph_prog stack_sizes sigma st.
+    sigma_pc_opt p p' graph_prog stack_sizes sigma (pc ? st) =
+    Some … (sigma_pc_of_status p p' graph_prog stack_sizes sigma st prf).
+    #p #p' #graph_prog #stack_sizes #sigma #st #prf @opt_to_opt_safe qed.
+
+*)
+
+definition sigma_pc :
+∀p,p',graph_prog,stack_sizes.
+∀sigma : ((Σi.is_internal_function_of_program … graph_prog i) → 
+    label → option ℕ).
+∀pc.
+∀prf : well_formed_pc p p' graph_prog stack_sizes sigma pc.
+cpointer ≝ 
+λp,p',graph_prog,stack_sizes,sigma,st.opt_safe ….
+
+definition sigma_state :
+ ∀p.
+ ∀p':∀F.sem_unserialized_params p F.
+ ∀graph_prog,stack_sizes.
+  ∀sigma.
+(*   let lin_prog ≝ linearise ? graph_prog in *)
+    ∀s:state_pc (p' ?). (* = graph_abstract_status p p' graph_prog stack_sizes *)
+     well_formed_status p p' graph_prog stack_sizes sigma s →
+      state_pc (make_sem_lin_params p p') (* = lin_abstract_status p p' lin_prog ? *)
+≝
+ λp,p',graph_prog,stack_sizes,sigma,s,prf.
+ let pc' ≝ sigma_pc … (proj1 … prf) in
+ mk_state_pc ? ? pc'.
+ cases daemon (* TODO *) qed.
+
+lemma sigma_pc_commute:
+ ∀p,p',graph_prog,stack_sizes,sigma,st.
+ ∀prf : well_formed_status p p' graph_prog stack_sizes sigma st.
+ sigma_pc … (pc ? st) (proj1 … prf) =
+ pc ? (sigma_state … st prf).
+#p #p' #prog #stack_sizes #sigma #st #prf %
+qed.
+
+lemma res_eq_from_opt :
+  ∀A,m,v.res_to_opt A m = return v → m = return v. 
+#A * #x #v normalize #EQ destruct % qed.
+
+lemma if_propagate :
+∀pars_in, pars_out : sem_params.
+∀trans : ∀globals.joint_closed_internal_function pars_in globals →
+                  joint_closed_internal_function pars_out globals.
+∀prog_in : program (joint_function pars_in) ℕ.
+let prog_out ≝
+  transform_program … prog_in (λglobals.transf_fundef ?? (trans globals)) in
+∀i.is_internal_function_of_program … prog_in i →
+is_internal_function_of_program … prog_out i.
+cases daemon (* TODO by paolo *) qed.
+
+definition stack_sizes_lift :
+∀pars_in, pars_out : sem_params.
+∀trans : ∀globals.joint_closed_internal_function pars_in globals →
+                  joint_closed_internal_function pars_out globals.
+∀prog_in : program (joint_function pars_in) ℕ.
+let prog_out ≝
+  transform_program … prog_in (λglobals.transf_fundef ?? (trans globals)) in
+((Σi.is_internal_function_of_program … prog_out i) → ℕ) →
+((Σi.is_internal_function_of_program … prog_in i) → ℕ) ≝
+λpars_in,pars_out,prog_in,trans,stack_sizes.
+λi.stack_sizes «i, if_propagate … (pi2 … i)».
+
+axiom ok_is_internal_function_of_program :
+  ∀p.∀prog:joint_program p.∀i.
+  is_internal_function_of_program p prog i →
+  is_internal_function ?? (globalenv_noinit ? prog) i.
+
+
+definition sigma_function_name :
  ∀p,p',graph_prog.
-  ∀sigma: identifier LabelTag → option ℕ. 
-  graph_abstract_status p p' graph_prog → Prop
- ≝
- λp,p',graph_prog,sigma,s.
-  sigma (point_of_pointer ? (make_sem_graph_params … (mk_graph_params … p) p') (pc ? s))
-   ≠ None ….
-
-definition sigma_pc_of_status:
+ let lin_prog ≝ linearise p graph_prog in
+ ∀lin_stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ.
+ let graph_stack_sizes ≝
+  stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
+    ? graph_prog lin_stack_sizes in
+  (Σf.is_internal_function … (ev_genv (graph_prog_params p p' graph_prog graph_stack_sizes)) f) →
+  (Σf.is_internal_function … (ev_genv (lin_prog_params p p' lin_prog lin_stack_sizes)) f) ≝
+λp,p',graph_prog,lin_stack_sizes,f.pi1 … f.
+@ok_is_internal_function_of_program
+@(if_propagate (make_sem_graph_params p p') (make_sem_lin_params p p'))
+@is_internal_function_of_program_ok
+@(pi2 … f)
+qed.
+
+lemma fetch_function_sigma_commute :
  ∀p,p',graph_prog.
-  ∀sigma: identifier LabelTag → option ℕ.
-   ∀s:graph_abstract_status p p' graph_prog.
-    well_formed_status … sigma s → ℕ
- ≝
-  λp,p',prog,sigma,s.
-   match sigma (point_of_pointer ? (make_sem_graph_params … (mk_graph_params … p) p') (pc ? s))
-   return λx. x ≠ None ? → ℕ
-   with
-   [ None ⇒ λprf.⊥
-   | Some n ⇒ λ_.n ].
- @(absurd ?? prf) //
-qed.
-
-lemma sigma_pc_of_status_ok:
-  ∀p,p',graph_prog.
-  ∀sigma: identifier LabelTag → option ℕ.
-   ∀s:graph_abstract_status p p' graph_prog.
-    ∀prf:well_formed_status … sigma s.
-     sigma (point_of_pointer ? (make_sem_graph_params … (mk_graph_params … p) p') (pc ? s))
-     = Some … (sigma_pc_of_status … prf).
- #p #p' #prog #sigma #s whd in ⊢ (% → ?);
- whd in match sigma_pc_of_status; normalize nodelta cases (sigma ?) //
- #abs cases (absurd ?? abs)
-qed.
-
-definition linearise_status_fun:
- ∀p,p',graph_prog.
-  ∀sigma: identifier LabelTag → option ℕ.
-   let lin_prog ≝ linearise ? graph_prog in
-    ∀s:graph_abstract_status p p' graph_prog.
-     well_formed_status … sigma s →
-      lin_abstract_status p p' lin_prog
-≝
- λp,p',graph_prog,sigma,s,prf.
-  mk_state_pc ??
-   (pointer_of_block_and_lin_offset (pblock (pc ? s)) …
-    (sigma_pc_of_status … sigma … prf)).
-[2: cases (pc ??) * normalize //
-| cases daemon (* TODO *) ]
-qed.
-
-lemma sigma_pc_commute:
- ∀p,p',graph_prog,s1,prf.
- sigma_pc_of_status p p' graph_prog (choose_sigma p p' graph_prog) s1 prf =
- point_of_pointer (lin_prog_params p p' (linearise p graph_prog))
- (lin_prog_params p p' (linearise p graph_prog))
-  (pc (lin_prog_params p p' (linearise p graph_prog))
-   (linearise_status_fun p p' graph_prog (choose_sigma p p' graph_prog) s1 prf)).
-#p #p' #prog #s #prf whd in ⊢ (??%%); change with (? = nat_of_bitvector ??);
-whd in match (pc … (linearise_status_fun …));
->nat_of_bitvector_bitvector_of_nat_inverse //
-cases daemon (* CSC: Paolo, you must prove this additional invariant! *)
+ let lin_prog ≝ linearise p graph_prog in
+ ∀lin_stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ.
+ let graph_stack_sizes ≝
+  stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
+    ? graph_prog lin_stack_sizes in
+ ∀sigma,pc,f.
+  ∀prf : well_formed_pc p p' graph_prog graph_stack_sizes sigma pc.
+ fetch_function … (ev_genv (graph_prog_params p p' graph_prog graph_stack_sizes)) pc = 
+  return f
+→ fetch_function … (ev_genv (lin_prog_params p p' lin_prog lin_stack_sizes)) (sigma_pc … pc prf) =
+  return sigma_function_name … f.
+ #p #p' #graph_prog #stack_sizes #sigma #pc #f #prf
+(* whd in match fetch_function; normalize nodelta
+whd in match function_of_block; normalize nodelta
+#H elim (bind_inversion ????? H) -H #fn *
+#H lapply (opt_eq_from_res ???? H) -H
+#H >(find_funct_ptr_transf … (λglobals.transf_fundef … (linearise_int_fun … globals)) … H)
+-H #H >m_return_bind cases fn in H; normalize nodelta #arg #EQ whd in EQ:(??%%);
+destruct // *)
+cases daemon
+qed.
+
+lemma if_of_function_commute:
+ ∀p,p',graph_prog,stack_sizes.
+ ∀graph_fun.
+ let graph_fd ≝ if_of_function ??? graph_fun in
+ let lin_fun ≝ sigma_function_name p p' graph_prog stack_sizes graph_fun in
+ let lin_fd ≝ if_of_function … lin_fun in
+ lin_fd = linearise_int_fun … graph_fd.
+(* usare match_opt_prf_elim ? *)
+cases daemon qed.
+
+lemma stmt_at_sigma_commute:
+ ∀p,p',graph_prog,stack_sizes,graph_fun,lbl.
+ let lin_prog ≝ linearise ? graph_prog in
+ let lin_fun ≝ sigma_function_name p p' graph_prog stack_sizes graph_fun in
+ ∀sigma.good_sigma p p' graph_prog sigma →
+ ∀prf:sigma graph_fun lbl ≠ None ….
+ ∃stmt.
+   stmt_at …
+    (joint_if_code ?? (if_of_function ??? graph_fun))  
+    lbl = Some ? stmt ∧
+   stmt_at …
+    (joint_if_code ?? (if_of_function ??? lin_fun))
+    (opt_safe … (sigma graph_fun lbl) prf) = Some ? (graph_to_lin_statement … stmt).  
+ #p #p' #graph_prog #stack_sizes #graph_fun #lbl #sigma #good #prf
+ @opt_safe_elim -prf #n #prf
+ (*
+ whd in match (stmt_at ????);
+ whd in match (stmt_at ????);
+ cases (linearise_code_spec … p' graph_prog graph_fun
+         (joint_if_entry … graph_fun))
+ * #lin_code_closed #sigma_entry_is_zero #sigma_spec
+ lapply (sigma_spec
+         (point_of_pointer ? (graph_prog_params … p' graph_prog) (pc … s1)))
+ -sigma_spec #sigma_spec cases (sigma_spec ??) [3: @(sigma_pc_of_status_ok … prf) |2: skip ]
+ -sigma_spec #graph_stmt * #graph_lookup_ok >graph_lookup_ok -graph_lookup_ok
+ whd in ⊢ (? → ???%); #sigma_spec whd in sigma_spec;
+ inversion (nth_opt ???) in sigma_spec; [ #H whd in ⊢ (% → ?); #abs cases abs ]
+ * #optlabel #lin_stm #lin_lookup_ok whd in ⊢ (% → ?); ** #_
+ #related_lin_stm_graph_stm #_ <related_lin_stm_graph_stm -related_lin_stm_graph_stm
+ <sigma_pc_commute >lin_lookup_ok // *)
+ cases daemon
+qed.
+
+lemma fetch_statement_sigma_commute:
+  ∀p,p',graph_prog,lin_stack_sizes,pc,fn,stmt.
+  let lin_prog ≝ linearise ? graph_prog in
+  let graph_stack_sizes ≝
+   stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
+    ? graph_prog lin_stack_sizes in
+  ∀sigma.good_sigma p p' graph_prog sigma →
+  ∀prf : well_formed_pc p p' graph_prog graph_stack_sizes sigma pc.
+  fetch_statement ? (make_sem_graph_params p p') … (ev_genv (graph_prog_params p p' graph_prog graph_stack_sizes)) pc =
+    return 〈fn,stmt〉 →
+  fetch_statement ? (make_sem_lin_params p p') … (ev_genv (lin_prog_params p p' lin_prog lin_stack_sizes))
+   (sigma_pc … pc prf) =
+    return 〈sigma_function_name … fn, graph_to_lin_statement … stmt〉.
+ #p #p' #graph_prog #stack_sizes #pc #fn #stmt #good #prf
+(* @opt_safe_elim -prf #n #prf
+ whd in match fetch_statement; normalize nodelta
+ >fetch_function_sigma_commute
+ cases (fetch_function ????) [2://]
+ #graph_fun whd in ⊢ (??%%);
+ whd in ⊢ (???(match % with [ _ ⇒ ? | _ ⇒ ?]));
+ >stm_at_sigma_commute cases (stmt_at ????) // *)
+cases daemon
 qed.
 
 definition linearise_status_rel:
  ∀p,p',graph_prog.
-  ∀sigma: identifier LabelTag → option ℕ.
-  let lin_prog ≝ linearise ? graph_prog in
+ let lin_prog ≝ linearise p graph_prog in
+ ∀stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ.
+ let stack_sizes' ≝
+  stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
+    ? graph_prog stack_sizes in
+ ∀sigma.
+ good_sigma p p' graph_prog sigma →
    status_rel
-    (graph_abstract_status p p' graph_prog)
-    (lin_abstract_status p p' lin_prog)
- ≝ λp,p',graph_prog,sigma.mk_status_rel …
-    (λs1,s2.
-     ∃prf: well_formed_status … sigma s1.
-      s2 = linearise_status_fun p p' graph_prog sigma s1 prf) ….
- cases daemon (* TODO *)
+    (graph_abstract_status p p' graph_prog stack_sizes')
+    (lin_abstract_status p p' lin_prog stack_sizes)
+ ≝ λp,p',graph_prog,stack_sizes,sigma,good.
+   let stack_sizes' ≝
+    stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
+      ? graph_prog ? in
+   mk_status_rel …
+    (* sem_rel ≝ *) (λs1,s2.
+     ∃prf: well_formed_status p p' graph_prog stack_sizes' sigma s1.
+      s2 = sigma_state … s1 prf)
+    (* call_rel ≝ *) (λs1,s2.
+      ∃prf:well_formed_status p p' graph_prog stack_sizes' sigma s1.
+      pc ? s2 = sigma_pc … (pc ? s1) (proj1 … prf))
+    (* sim_final ≝ *) ?.
+#st1 #st2 * #prf #EQ2
+%
+whd in ⊢ (%→%);
+#H lapply (opt_to_opt_safe … H)
+@opt_safe_elim -H
+#res #_
+#H lapply (res_eq_from_opt ??? H) -H
+#H elim (bind_inversion ????? H)
+* #f #stmt *
+whd in ⊢ (??%?→?);
+cases daemon
 qed.
 
 (* To be added to common/Globalenvs, it strenghtens
    find_funct_ptr_transf *)
+(*   
 lemma
   find_funct_ptr_transf_eq:
@@ -189 +394 @@
  | #f #H >(find_funct_ptr_transf A B … H) // ]
 qed.
-
-lemma fetch_function_sigma_commute:
+*)
+
+
+(*lemma fetch_function_sigma_commute:
  ∀p,p',graph_prog,sigma,st1.
  ∀prf:well_formed_status ??? sigma st1.
  let lin_prog ≝ linearise ? graph_prog in
-  fetch_function
+  fetch_function                
    (lin_prog_params p p' lin_prog)
    (globals (lin_prog_params p p' lin_prog))
@@ -213 +420 @@
 cases (find_funct_ptr ???) // * //
 qed.
-
-lemma stm_at_sigma_commute:
- ∀p,p',graph_prog,graph_fun,s1.
- let lin_prog ≝ linearise ? graph_prog in
- let sigma ≝ choose_sigma p p' graph_prog in
- ∀prf:well_formed_status ??? sigma s1.
-  stmt_at (lin_prog_params p p' (linearise p graph_prog))
-   (globals (lin_prog_params p p' (linearise p graph_prog)))
-   (joint_if_code (lin_prog_params p p' (linearise p graph_prog))
-    (globals (lin_prog_params p p' (linearise p graph_prog)))
-    (linearise_int_fun p (globals (graph_prog_params p p' graph_prog)) graph_fun))
-   (point_of_pointer (lin_prog_params p p' (linearise p graph_prog))
-    (lin_prog_params p p' (linearise p graph_prog))
-    (pc (lin_prog_params p p' (linearise p graph_prog))
-     (linearise_status_fun p p' graph_prog sigma s1 prf)))
- =
-  option_map …
-   (graph_to_lin_statement …)
-   (stmt_at (graph_prog_params p p' graph_prog)
-    (globals (graph_prog_params p p' graph_prog))
-    (joint_if_code (graph_prog_params p p' graph_prog)
-     (globals (graph_prog_params p p' graph_prog)) graph_fun)
-    (point_of_pointer (graph_prog_params p p' graph_prog)
-     (graph_prog_params p p' graph_prog)
-     (pc (graph_prog_params p p' graph_prog) s1))).
- #p #p' #graph_prog #graph_fun #s1 #prf
- whd in match (stmt_at ????);
- whd in match (stmt_at ????);
- cases (linearise_code_spec … p' graph_prog graph_fun
-         (joint_if_entry … graph_fun))
- * #lin_code_closed #sigma_entry_is_zero #sigma_spec
- lapply (sigma_spec
-         (point_of_pointer ? (graph_prog_params … p' graph_prog) (pc … s1)))
- -sigma_spec #sigma_spec cases (sigma_spec ??) [3: @(sigma_pc_of_status_ok … prf) |2: skip ]
- -sigma_spec #graph_stmt * #graph_lookup_ok >graph_lookup_ok -graph_lookup_ok
- whd in ⊢ (? → ???%); #sigma_spec whd in sigma_spec;
- inversion (nth_opt ???) in sigma_spec; [ #H whd in ⊢ (% → ?); #abs cases abs ]
- * #optlabel #lin_stm #lin_lookup_ok whd in ⊢ (% → ?); ** #_
- #related_lin_stm_graph_stm #_ <related_lin_stm_graph_stm -related_lin_stm_graph_stm
- <sigma_pc_commute >lin_lookup_ok //
-qed.
-
-lemma fetch_statement_sigma_commute:
- ∀p,p',graph_prog,st1.
- let sigma ≝ choose_sigma p p' graph_prog in
- let lin_prog ≝ linearise ? graph_prog in
- ∀prf.
-  fetch_statement
-   (lin_prog_params p p' lin_prog)
-   (lin_prog_params p p' lin_prog)
-   (globals (lin_prog_params p p' lin_prog))
-   (ev_genv (lin_prog_params p p' lin_prog))
-   (pc (lin_prog_params p p' lin_prog)
-    (linearise_status_fun p p' graph_prog sigma st1 prf))
- =
-  m_map …
-   (λfun_stm.
-     let 〈fun,stm〉 ≝ fun_stm in
-      〈linearise_int_fun ?? fun, graph_to_lin_statement ?? stm〉)
-   (fetch_statement
-    (graph_prog_params p p' graph_prog)
-    (graph_prog_params p p' graph_prog)
-    (globals (graph_prog_params p p' graph_prog))
-    (ev_genv (graph_prog_params p p' graph_prog))
-    (pc (graph_prog_params p p' graph_prog) st1)).
- #p #p' #graph_prog #s1 #prf
- whd in match fetch_statement; normalize nodelta
- >fetch_function_sigma_commute
- cases (fetch_function ????) [2://]
- #graph_fun whd in ⊢ (??%%);
- whd in ⊢ (???(match % with [ _ ⇒ ? | _ ⇒ ?]));
- >stm_at_sigma_commute cases (stmt_at ????) //
-qed.
+*)
+        
+inductive ex_Type1 (A:Type[1]) (P:A → Prop) : Prop ≝
+    ex1_intro: ∀ x:A. P x →  ex_Type1 A P.
+interpretation "exists in Type[1]" 'exists x = (ex_Type1 ? x).
 
 lemma linearise_ok:
  ∀p,p',graph_prog.
   let lin_prog ≝ linearise ? graph_prog in
+ ∀lin_stack_sizes : (Σi.is_internal_function_of_program … lin_prog i) → ℕ.
+ let graph_stack_sizes ≝
+  stack_sizes_lift (make_sem_graph_params p p') (make_sem_lin_params p p')
+    ? graph_prog lin_stack_sizes in
+   ∃R.
    status_simulation
-    (graph_abstract_status p p' graph_prog)
-    (lin_abstract_status p p' lin_prog) ≝
- λp,p',graph_prog.
-  let sigma ≝ choose_sigma p p' graph_prog in
-   mk_status_simulation … (linearise_status_rel p p' graph_prog sigma) ….
+    (graph_abstract_status p p' graph_prog graph_stack_sizes)
+    (lin_abstract_status p p' lin_prog lin_stack_sizes) R.
+ #p #p' #graph_prog
+ cut (∃sigma.good_sigma p p' graph_prog sigma)
+ [ cases daemon (* TODO by Paolo *) ] * #sigma #good
+ #lin_stack_sizes
+ %{(linearise_status_rel p p' graph_prog lin_stack_sizes sigma good)}
+ whd 
 #st1 #cl #st1' #st2 #move_st1_st1' #rel_st1_st2 #classified_st1_cl
 cases cl in classified_st1_cl; -cl #classified_st1_cl whd